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

State before:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
⊢ x * a = 1 → a⁻¹ = x
Tactic:
intro h
State after:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
h : x * a = 1
⊢ a⁻¹ = x

State before:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
h : x * a = 1
⊢ a⁻¹ = x
Tactic:
apply mul_right_cancel a
State after:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
h : x * a = 1
⊢ a⁻¹ * a = x * a

State before:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
h : x * a = 1
⊢ a⁻¹ * a = x * a
Tactic:
rw [h]
State after:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
h : x * a = 1
⊢ a⁻¹ * a = 1

State before:
A : Type ?u.17097
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
h : x * a = 1
⊢ a⁻¹ * a = 1
Tactic:
simp
State after:
no goals