case pos
α : Type ?u.16951
M₀ : Type ?u.16954
G₀ : Type u_1
M₀' : Type ?u.16960
G₀' : Type ?u.16963
F : Type ?u.16966
F' : Type ?u.16969
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b a : G₀
h : a = 0
⊢ a = 0 ∨ ∃ u, a = ↑u

case neg
α : Type ?u.16951
M₀ : Type ?u.16954
G₀ : Type u_1
M₀' : Type ?u.16960
G₀' : Type ?u.16963
F : Type ?u.16966
F' : Type ?u.16969
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b a : G₀
h : ¬a = 0
⊢ a = 0 ∨ ∃ u, a = ↑u
α : Type ?u.16951
M₀ : Type ?u.16954
G₀ : Type u_1
M₀' : Type ?u.16960
G₀' : Type ?u.16963
F : Type ?u.16966
F' : Type ?u.16969
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b a : G₀
⊢ a = 0 ∨ ∃ u, a = ↑u
by_cases h : a = 0
case pos.h
α : Type ?u.16951
M₀ : Type ?u.16954
G₀ : Type u_1
M₀' : Type ?u.16960
G₀' : Type ?u.16963
F : Type ?u.16966
F' : Type ?u.16969
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b a : G₀
h : a = 0
⊢ a = 0
case pos
α : Type ?u.16951
M₀ : Type ?u.16954
G₀ : Type u_1
M₀' : Type ?u.16960
G₀' : Type ?u.16963
F : Type ?u.16966
F' : Type ?u.16969
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b a : G₀
h : a = 0
⊢ a = 0 ∨ ∃ u, a = ↑u
left
no goals
case pos.h
α : Type ?u.16951
M₀ : Type ?u.16954
G₀ : Type u_1
M₀' : Type ?u.16960
G₀' : Type ?u.16963
F : Type ?u.16966
F' : Type ?u.16969
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b a : G₀
h : a = 0
⊢ a = 0
exact h
case neg.h
α : Type ?u.16951
M₀ : Type ?u.16954
G₀ : Type u_1
M₀' : Type ?u.16960
G₀' : Type ?u.16963
F : Type ?u.16966
F' : Type ?u.16969
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b a : G₀
h : ¬a = 0
⊢ ∃ u, a = ↑u
case neg
α : Type ?u.16951
M₀ : Type ?u.16954
G₀ : Type u_1
M₀' : Type ?u.16960
G₀' : Type ?u.16963
F : Type ?u.16966
F' : Type ?u.16969
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b a : G₀
h : ¬a = 0
⊢ a = 0 ∨ ∃ u, a = ↑u
right
no goals
case neg.h
α : Type ?u.16951
M₀ : Type ?u.16954
G₀ : Type u_1
M₀' : Type ?u.16960
G₀' : Type ?u.16963
F : Type ?u.16966
F' : Type ?u.16969
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b a : G₀
h : ¬a = 0
⊢ ∃ u, a = ↑u
simpa only [eq_comm] using Units.exists_iff_ne_zero.mpr h