no goals
α : Type u_1
β : Type ?u.40597
A : Type ?u.40600
B : Type ?u.40603
M : Type ?u.40606
N : Type ?u.40609
P : Type ?u.40612
R : Type ?u.40615
S : Type ?u.40618
G : Type u_2
M₀ : Type ?u.40624
G₀ : Type ?u.40627
ι : Sort ?u.40630
inst✝ : DivisionMonoid G
f g : α → G
⊢ (fun a b => a * b⁻¹) 1 1 = 1
simp