case inl
M : Type u_3
M' : Type u_1
M₁ : Type ?u.57271
R : Type ?u.57274
R' : Type ?u.57277
F : Type u_2
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M'
inst✝ : MonoidWithZeroHomClass F M M'
f : F
hf : Function.Injective ↑f
S : Submonoid M
hS : S ≤ M⁰
h✝ : Subsingleton M
⊢ Submonoid.map f S ≤ M'⁰

case inr
M : Type u_3
M' : Type u_1
M₁ : Type ?u.57271
R : Type ?u.57274
R' : Type ?u.57277
F : Type u_2
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M'
inst✝ : MonoidWithZeroHomClass F M M'
f : F
hf : Function.Injective ↑f
S : Submonoid M
hS : S ≤ M⁰
h✝ : Nontrivial M
⊢ Submonoid.map f S ≤ M'⁰
M : Type u_3
M' : Type u_1
M₁ : Type ?u.57271
R : Type ?u.57274
R' : Type ?u.57277
F : Type u_2
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M'
inst✝ : MonoidWithZeroHomClass F M M'
f : F
hf : Function.Injective ↑f
S : Submonoid M
hS : S ≤ M⁰
⊢ Submonoid.map f S ≤ M'⁰
cases subsingleton_or_nontrivial M
no goals
case inl
M : Type u_3
M' : Type u_1
M₁ : Type ?u.57271
R : Type ?u.57274
R' : Type ?u.57277
F : Type u_2
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M'
inst✝ : MonoidWithZeroHomClass F M M'
f : F
hf : Function.Injective ↑f
S : Submonoid M
hS : S ≤ M⁰
h✝ : Subsingleton M
⊢ Submonoid.map f S ≤ M'⁰
simp [Subsingleton.elim S ⊥]
no goals
case inr
M : Type u_3
M' : Type u_1
M₁ : Type ?u.57271
R : Type ?u.57274
R' : Type ?u.57277
F : Type u_2
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M'
inst✝ : MonoidWithZeroHomClass F M M'
f : F
hf : Function.Injective ↑f
S : Submonoid M
hS : S ≤ M⁰
h✝ : Nontrivial M
⊢ Submonoid.map f S ≤ M'⁰
exact le_nonZeroDivisors_of_noZeroDivisors fun h ↦
  let ⟨x, hx, hx0⟩ := h
  zero_ne_one (hS (hf (hx0.trans (map_zero f).symm) ▸ hx : 0 ∈ S) 1 (mul_zero 1)).symm