case inl
α : Type ?u.10029
M₀ : Type u_1
G₀ : Type ?u.10035
M₀' : Type ?u.10038
G₀' : Type ?u.10041
F : Type ?u.10044
F' : Type ?u.10047
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit (Ring.inverse a)
h✝ : Subsingleton M₀
⊢ IsUnit a

case inr
α : Type ?u.10029
M₀ : Type u_1
G₀ : Type ?u.10035
M₀' : Type ?u.10038
G₀' : Type ?u.10041
F : Type ?u.10044
F' : Type ?u.10047
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit (Ring.inverse a)
h✝ : Nontrivial M₀
⊢ IsUnit a
α : Type ?u.10029
M₀ : Type u_1
G₀ : Type ?u.10035
M₀' : Type ?u.10038
G₀' : Type ?u.10041
F : Type ?u.10044
F' : Type ?u.10047
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit (Ring.inverse a)
⊢ IsUnit a
cases subsingleton_or_nontrivial M₀
no goals
case inl
α : Type ?u.10029
M₀ : Type u_1
G₀ : Type ?u.10035
M₀' : Type ?u.10038
G₀' : Type ?u.10041
F : Type ?u.10044
F' : Type ?u.10047
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit (Ring.inverse a)
h✝ : Subsingleton M₀
⊢ IsUnit a
convert h
case inr
α : Type ?u.10029
M₀ : Type u_1
G₀ : Type ?u.10035
M₀' : Type ?u.10038
G₀' : Type ?u.10041
F : Type ?u.10044
F' : Type ?u.10047
inst✝ : MonoidWithZero M₀
a : M₀
h✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit (Ring.inverse a)
case inr
α : Type ?u.10029
M₀ : Type u_1
G₀ : Type ?u.10035
M₀' : Type ?u.10038
G₀' : Type ?u.10041
F : Type ?u.10044
F' : Type ?u.10047
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit (Ring.inverse a)
h✝ : Nontrivial M₀
⊢ IsUnit a
contrapose h
case inr
α : Type ?u.10029
M₀ : Type u_1
G₀ : Type ?u.10035
M₀' : Type ?u.10038
G₀' : Type ?u.10041
F : Type ?u.10044
F' : Type ?u.10047
inst✝ : MonoidWithZero M₀
a : M₀
h✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit 0
case inr
α : Type ?u.10029
M₀ : Type u_1
G₀ : Type ?u.10035
M₀' : Type ?u.10038
G₀' : Type ?u.10041
F : Type ?u.10044
F' : Type ?u.10047
inst✝ : MonoidWithZero M₀
a : M₀
h✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit (Ring.inverse a)
rw [Ring.inverse_non_unit _ h]
no goals
case inr
α : Type ?u.10029
M₀ : Type u_1
G₀ : Type ?u.10035
M₀' : Type ?u.10038
G₀' : Type ?u.10041
F : Type ?u.10044
F' : Type ?u.10047
inst✝ : MonoidWithZero M₀
a : M₀
h✝ : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit 0
exact not_isUnit_zero