α : Type ?u.28722
M₀ : Type ?u.28725
G₀ : Type u_1
M₀' : Type ?u.28731
G₀' : Type ?u.28734
F : Type ?u.28737
F' : Type ?u.28740
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a * a / a = a
α : Type ?u.28722
M₀ : Type ?u.28725
G₀ : Type u_1
M₀' : Type ?u.28731
G₀' : Type ?u.28734
F : Type ?u.28737
F' : Type ?u.28740
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a / (a / a) = a
rw [div_div_eq_mul_div]
no goals
α : Type ?u.28722
M₀ : Type ?u.28725
G₀ : Type u_1
M₀' : Type ?u.28731
G₀' : Type ?u.28734
F : Type ?u.28737
F' : Type ?u.28740
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
⊢ a * a / a = a
exact mul_self_div_self a