case mp
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ Multiset.prod s = 0 → ∃ r x, r = 0

case mpr
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ (∃ r x, r = 0) → Multiset.prod s = 0
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ Multiset.prod s = 0 ↔ ∃ r x, r = 0
constructor
case mpr
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ (∃ r x, r = 0) → Multiset.prod s = 0

case mp
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ Multiset.prod s = 0 → ∃ r x, r = 0
case mp
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ Multiset.prod s = 0 → ∃ r x, r = 0

case mpr
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ (∃ r x, r = 0) → Multiset.prod s = 0
swap
case mp.empty
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
⊢ Multiset.prod 0 = 0 → ∃ r x, r = 0

case mp.cons
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
⊢ Multiset.prod (a ::ₘ s) = 0 → ∃ r x, r = 0
case mp
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ Multiset.prod s = 0 → ∃ r x, r = 0
induction' s using Multiset.induction_on with a s ih
case mpr.intro.intro
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
hrs : 0 ∈ s
⊢ Multiset.prod s = 0
case mpr
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
⊢ (∃ r x, r = 0) → Multiset.prod s = 0
rintro ⟨r, hrs, rfl⟩
no goals
case mpr.intro.intro
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
s : Multiset M₁
hrs : 0 ∈ s
⊢ Multiset.prod s = 0
exact Multiset.prod_eq_zero hrs
case mp.empty
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
habs : Multiset.prod 0 = 0
⊢ ∃ r x, r = 0
case mp.empty
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
⊢ Multiset.prod 0 = 0 → ∃ r x, r = 0
intro habs
no goals
case mp.empty
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
habs : Multiset.prod 0 = 0
⊢ ∃ r x, r = 0
simp at habs
case mp.cons
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
⊢ a * Multiset.prod s = 0 → ∃ r x, r = 0
case mp.cons
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
⊢ Multiset.prod (a ::ₘ s) = 0 → ∃ r x, r = 0
rw [Multiset.prod_cons]
case mp.cons
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hprod : a * Multiset.prod s = 0
⊢ ∃ r x, r = 0
case mp.cons
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
⊢ a * Multiset.prod s = 0 → ∃ r x, r = 0
intro hprod
case mp.cons
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hprod : a = 0 ∨ Multiset.prod s = 0
⊢ ∃ r x, r = 0
case mp.cons
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hprod : a * Multiset.prod s = 0
⊢ ∃ r x, r = 0
replace hprod := eq_zero_or_eq_zero_of_mul_eq_zero hprod
case mp.cons.inl
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
ha : a = 0
⊢ ∃ r x, r = 0

case mp.cons.inr
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hb : Multiset.prod s = 0
⊢ ∃ r x, r = 0
case mp.cons
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hprod : a = 0 ∨ Multiset.prod s = 0
⊢ ∃ r x, r = 0
cases' hprod with ha hb
no goals
case mp.cons.inl
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
ha : a = 0
⊢ ∃ r x, r = 0
exact ⟨a, Multiset.mem_cons_self a s, ha⟩
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hb : Multiset.prod s = 0
⊢ ∀ (a_1 : M₁), (∃ x, a_1 = 0) → ∃ x, a_1 = 0
case mp.cons.inr
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hb : Multiset.prod s = 0
⊢ ∃ r x, r = 0
apply (ih hb).imp _
case intro
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hb : Multiset.prod s = 0
b : M₁
hb₁ : b ∈ s
hb₂ : b = 0
⊢ ∃ x, b = 0
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hb : Multiset.prod s = 0
⊢ ∀ (a_1 : M₁), (∃ x, a_1 = 0) → ∃ x, a_1 = 0
rintro b ⟨hb₁, hb₂⟩
no goals
case intro
M : Type ?u.75307
M' : Type ?u.75310
M₁ : Type u_1
R : Type ?u.75316
R' : Type ?u.75319
F : Type ?u.75322
inst✝⁶ : MonoidWithZero M
inst✝⁵ : MonoidWithZero M'
inst✝⁴ : CommMonoidWithZero M₁
inst✝³ : Ring R
inst✝² : CommRing R'
inst✝¹ : NoZeroDivisors M₁
inst✝ : Nontrivial M₁
a : M₁
s : Multiset M₁
ih : Multiset.prod s = 0 → ∃ r x, r = 0
hb : Multiset.prod s = 0
b : M₁
hb₁ : b ∈ s
hb₂ : b = 0
⊢ ∃ x, b = 0
exact ⟨Multiset.mem_cons_of_mem hb₁, hb₂⟩