[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝ : Group G
a b : G
⊢ (fun b => b⁻¹ * a) ((fun b => a / b) b) = b
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝ : Group G
a b : G
⊢ (fun b => a / b) ((fun b => b⁻¹ * a) b) = b
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝ : Group G
a b : G
⊢ (fun b => b * a) ((fun b => b / a) b) = b
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
A : Type u_4
B : Type u_5
M : Type u_6
N : Type u_7
P : Type u_8
Q : Type u_9
G : Type u_10
H : Type u_11
inst✝ : Group G
a b : G
⊢ (fun b => b / a) ((fun b => b * a) b) = b
[PROOFSTEP]
simp [div_eq_mul_inv]
