Theorem: inv_invo (src/Group.lean)

State before:
α : Type u_1
g : group α
⊢ ∀ (a : α), group.inv (group.inv a) = a
Tactic:
intro a
State after:
α : Type u_1
g : group α
a : α
⊢ group.inv (group.inv a) = a

State before:
α : Type u_1
g : group α
a : α
⊢ group.inv (group.inv a) = a
Tactic:
have h := (g.mul_left_inv (g.inv a))
State after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ group.inv (group.inv a) = a

State before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ group.inv (group.inv a) = a
Tactic:
have h2 : g.inv (g.inv a) * (g.inv a) * a = a := by {
  rw[h]
  apply g.one_mul
}
State after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) * group.inv a * a = a
⊢ group.inv (group.inv a) = a

State before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) * group.inv a * a = a
⊢ group.inv (group.inv a) = a
Tactic:
rw [g.mul_assoc] at h2
State after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) * (group.inv a * a) = a
⊢ group.inv (group.inv a) = a

State before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) * (group.inv a * a) = a
⊢ group.inv (group.inv a) = a
Tactic:
rw [g.mul_left_inv a] at h2
State after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) * has_one.one = a
⊢ group.inv (group.inv a) = a

State before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) * has_one.one = a
⊢ group.inv (group.inv a) = a
Tactic:
rw [g.mul_one] at h2
State after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) = a
⊢ group.inv (group.inv a) = a

State before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
h2 : group.inv (group.inv a) = a
⊢ group.inv (group.inv a) = a
Tactic:
exact h2
State after:
no goals

State before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ group.inv (group.inv a) * group.inv a * a = a
Tactic:
rw[h]
State after:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ has_one.one * a = a

State before:
α : Type u_1
g : group α
a : α
h : group.inv (group.inv a) * group.inv a = has_one.one
⊢ has_one.one * a = a
Tactic:
apply g.one_mul
State after:
no goals