Theorem: inv_one_eq_one (src/Group.lean)

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

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

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

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