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

State before:
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a⁻¹ * b = 1 ↔ a = b
Tactic:
constructor
State after:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a⁻¹ * b = 1 → a = b

case mpr
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a = b → a⁻¹ * b = 1

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

State before:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h : a⁻¹ * b = 1
⊢ a = b
Tactic:
have h : a⁻¹ * b⁻¹⁻¹ = 1 := by simp [h]
State after:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h✝ : a⁻¹ * b = 1
h : a⁻¹ * b⁻¹⁻¹ = 1
⊢ a = b

State before:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h✝ : a⁻¹ * b = 1
h : a⁻¹ * b⁻¹⁻¹ = 1
⊢ a = b
Tactic:
rw [mul_inv_eq_one] at h
State after:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h✝ : a⁻¹ * b = 1
h : a⁻¹ = b⁻¹
⊢ a = b

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

State before:
case mp
A : Type ?u.23889
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
h✝ : a⁻¹ * b = 1
h : a⁻¹ = b⁻¹
⊢ a⁻¹⁻¹ = b⁻¹⁻¹
Tactic:
rw [h]
State after:
no goals

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

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

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

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

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