Theorem: Tutorial.mul_inv_eq_one (Solution/Advanced/Algebra/Lecture1.lean)

State before:
A : Type ?u.21692
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * b⁻¹ = 1 ↔ a = b
Tactic:
suffices a * b⁻¹ = 1 ↔ a = 1 * b by simpa using this
State after:
A : Type ?u.21692
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * b⁻¹ = 1 ↔ a = 1 * b

State before:
A : Type ?u.21692
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * b⁻¹ = 1 ↔ a = 1 * b
Tactic:
exact mul_inv_eq_iff_eq_mul
State after:
no goals

State before:
A : Type ?u.21692
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
this : a * b⁻¹ = 1 ↔ a = 1 * b
⊢ a * b⁻¹ = 1 ↔ a = b
Tactic:
simpa using this
State after:
no goals