α : Type ?u.28943
M₀ : Type ?u.28946
G₀ : Type u_1
M₀' : Type ?u.28952
G₀' : Type ?u.28955
F : Type ?u.28958
F' : Type ?u.28961
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : 0 ≠ 0
ha : a = 0
⊢ False
α : Type ?u.28943
M₀ : Type ?u.28946
G₀ : Type u_1
M₀' : Type ?u.28952
G₀' : Type ?u.28955
F : Type ?u.28958
F' : Type ?u.28961
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : 1 / a ≠ 0
ha : a = 0
⊢ False
rw [ha, div_zero] at h
no goals
α : Type ?u.28943
M₀ : Type ?u.28946
G₀ : Type u_1
M₀' : Type ?u.28952
G₀' : Type ?u.28955
F : Type ?u.28958
F' : Type ?u.28961
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
h : 0 ≠ 0
ha : a = 0
⊢ False
contradiction