Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Let x2 of type ι be given.
Assume H1: x2 ∈ x0.
Let x3 of type ι be given.
Assume H2: x3 ∈ x0.
Apply H0 with
x1 (x1 x3 x2) (x1 x3 x2) = explicit_Group_identity x0 x1.
Assume H4:
and (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x1 x4 x5 ∈ x0) (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x1 x4 (x1 x5 x6) = x1 (x1 x4 x5) x6).
Apply H4 with
(∃ x4 . and (x4 ∈ x0) (and (∀ x5 . x5 ∈ x0 ⟶ and (x1 x4 x5 = x5) (x1 x5 x4 = x5)) (∀ x5 . x5 ∈ x0 ⟶ ∃ x6 . and (x6 ∈ x0) (and (x1 x5 x6 = x4) (x1 x6 x5 = x4))))) ⟶ x1 (x1 x3 x2) (x1 x3 x2) = explicit_Group_identity x0 x1.
Assume H5: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x1 x4 x5 ∈ x0.
Assume H6: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x1 x4 (x1 x5 x6) = x1 (x1 x4 x5) x6.
Assume H7:
∃ x4 . and (x4 ∈ x0) (and (∀ x5 . x5 ∈ x0 ⟶ and (x1 x4 x5 = x5) (x1 x5 x4 = x5)) (∀ x5 . x5 ∈ x0 ⟶ ∃ x6 . and (x6 ∈ x0) (and (x1 x5 x6 = x4) (x1 x6 x5 = x4)))).
Apply explicit_Group_rcancel with
x0,
x1,
x1 (x1 x3 x2) (x1 x3 x2),
explicit_Group_identity x0 x1,
x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L11.
Apply explicit_Group_identity_in with
x0,
x1.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply explicit_Group_identity_lid with
x0,
x1,
x3,
λ x4 x5 . x1 (x1 (x1 x3 x2) (x1 x3 x2)) x3 = x5 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply H6 with
x1 x3 x2,
x1 x3 x2,
x3,
λ x4 x5 . x4 = x3 leaving 4 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L10.
The subproof is completed by applying H2.
Apply H6 with
x3,
x2,
x3,
λ x4 x5 . x1 (x1 x3 x2) x4 = x3 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply H6 with
x3,
x2,
x1 x3 (x1 x2 x3),
λ x4 x5 . x4 = x3 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
The subproof is completed by applying L9.
Apply H6 with
x2,
x3,
x1 x2 x3,
λ x4 x5 . ... leaving 4 subgoals.