Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply CSNo_ReIm_split with
mul_CSNo x0 (add_CSNo x1 x2),
add_CSNo (mul_CSNo x0 x1) (mul_CSNo x0 x2) leaving 4 subgoals.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with
x0,
add_CSNo x1 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
Apply CSNo_add_CSNo with
mul_CSNo x0 x1,
mul_CSNo x0 x2 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
set y3 to be ...
Let x4 of type ι → ο be given.
Apply unknownprop_6c208b2fed212d981bc839a7f70f9c484483dc6ca9daee237131093290c06c64 with
x1,
add_CSNo x2 y3,
λ x5 . x4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
set y5 to be ...
set y6 to be ...
Apply L13 with
λ x7 . y6 x7 y5 ⟶ y6 y5 x7 leaving 2 subgoals.
Assume H14: y6 y5 y5.
The subproof is completed by applying H14.
Apply add_SNo_com_4_inner_mid with
mul_SNo (CSNo_Re y3) (CSNo_Re x4),
mul_SNo (CSNo_Re y3) (CSNo_Re y5),
minus_SNo (mul_SNo (CSNo_Im y3) (CSNo_Im x4)),
minus_SNo (mul_SNo (CSNo_Im y3) (CSNo_Im y5)),
λ x7 . y6 leaving 5 subgoals.
Apply SNo_mul_SNo with
CSNo_Re y3,
CSNo_Re x4 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L8.
Apply SNo_mul_SNo with
CSNo_Re y3,
CSNo_Re y5 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L9.
Apply SNo_minus_SNo with
mul_SNo (CSNo_Im y3) (CSNo_Im x4).
Apply SNo_mul_SNo with
CSNo_Im y3,
CSNo_Im x4 leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L11.
Apply SNo_minus_SNo with
mul_SNo (CSNo_Im y3) (CSNo_Im y5).
Apply SNo_mul_SNo with
CSNo_Im y3,
CSNo_Im y5 leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying H12.
set y7 to be ...
Let x8 of type ι → ο be given.
set y8 to be λ x8 . y7
Apply L14 with
λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H15: y8 y7 y7.
The subproof is completed by applying H15.
Apply unknownprop_af0b151803c2dc4bc6691b166645c0a8471b89f2da30fa0948427517708d6da0 with
mul_CSNo y5 y6,
mul_CSNo y5 y7,
λ x9 x10 . (λ x11 . y8) x10 x9 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
The subproof is completed by applying L14.
Let x4 of type ι → ι → ο be given.
Apply L12 with
λ x5 . x4 x5 y3 ⟶ x4 y3 x5.
Assume H13: x4 y3 y3.
The subproof is completed by applying H13.