[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c x y : RingCon R
h : (fun c => Setoid.r) x = (fun c => Setoid.r) y
⊢ x = y
[PROOFSTEP]
rcases x with ⟨⟨x, _⟩, _⟩
[GOAL]
case mk.mk
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c y : RingCon R
x : R → R → Prop
iseqv✝ : Equivalence x
add'✝ : ∀ {w x_1 y z : R}, Setoid.r w x_1 → Setoid.r y z → Setoid.r (w + y) (x_1 + z)
mul'✝ : ∀ {w x_1 y z : R}, Setoid.r w x_1 → Setoid.r y z → Setoid.r (w * y) (x_1 * z)
h :
  (fun c => Setoid.r) { toSetoid := { r := x, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ } = (fun c => Setoid.r) y
⊢ { toSetoid := { r := x, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ } = y
[PROOFSTEP]
rcases y with ⟨⟨y, _⟩, _⟩
[GOAL]
case mk.mk.mk.mk
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
x : R → R → Prop
iseqv✝¹ : Equivalence x
add'✝¹ : ∀ {w x_1 y z : R}, Setoid.r w x_1 → Setoid.r y z → Setoid.r (w + y) (x_1 + z)
mul'✝¹ : ∀ {w x_1 y z : R}, Setoid.r w x_1 → Setoid.r y z → Setoid.r (w * y) (x_1 * z)
y : R → R → Prop
iseqv✝ : Equivalence y
add'✝ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w + y_1) (x + z)
mul'✝ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w * y_1) (x * z)
h :
  (fun c => Setoid.r) { toSetoid := { r := x, iseqv := iseqv✝¹ }, add' := add'✝¹, mul' := mul'✝¹ } =
    (fun c => Setoid.r) { toSetoid := { r := y, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ }
⊢ { toSetoid := { r := x, iseqv := iseqv✝¹ }, add' := add'✝¹, mul' := mul'✝¹ } =
    { toSetoid := { r := y, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ }
[PROOFSTEP]
have : x = y := h
[GOAL]
case mk.mk.mk.mk
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
x : R → R → Prop
iseqv✝¹ : Equivalence x
add'✝¹ : ∀ {w x_1 y z : R}, Setoid.r w x_1 → Setoid.r y z → Setoid.r (w + y) (x_1 + z)
mul'✝¹ : ∀ {w x_1 y z : R}, Setoid.r w x_1 → Setoid.r y z → Setoid.r (w * y) (x_1 * z)
y : R → R → Prop
iseqv✝ : Equivalence y
add'✝ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w + y_1) (x + z)
mul'✝ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w * y_1) (x * z)
h :
  (fun c => Setoid.r) { toSetoid := { r := x, iseqv := iseqv✝¹ }, add' := add'✝¹, mul' := mul'✝¹ } =
    (fun c => Setoid.r) { toSetoid := { r := y, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ }
this : x = y
⊢ { toSetoid := { r := x, iseqv := iseqv✝¹ }, add' := add'✝¹, mul' := mul'✝¹ } =
    { toSetoid := { r := y, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ }
[PROOFSTEP]
subst x
[GOAL]
case mk.mk.mk.mk
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
y : R → R → Prop
iseqv✝¹ : Equivalence y
add'✝¹ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w + y_1) (x + z)
mul'✝¹ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w * y_1) (x * z)
iseqv✝ : Equivalence y
add'✝ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w + y_1) (x + z)
mul'✝ : ∀ {w x y_1 z : R}, Setoid.r w x → Setoid.r y_1 z → Setoid.r (w * y_1) (x * z)
h :
  (fun c => Setoid.r) { toSetoid := { r := y, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ } =
    (fun c => Setoid.r) { toSetoid := { r := y, iseqv := iseqv✝¹ }, add' := add'✝¹, mul' := mul'✝¹ }
⊢ { toSetoid := { r := y, iseqv := iseqv✝ }, add' := add'✝, mul' := mul'✝ } =
    { toSetoid := { r := y, iseqv := iseqv✝¹ }, add' := add'✝¹, mul' := mul'✝¹ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
d : (a b : R) → Decidable (↑c a b)
⊢ DecidableEq (RingCon.Quotient c)
[PROOFSTEP]
delta RingCon.Quotient
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c : RingCon R
d : (a b : R) → Decidable (↑c a b)
⊢ DecidableEq (Quotient c.toSetoid)
[PROOFSTEP]
infer_instance


[GOAL]
R : Type u_1
inst✝ : MonoidWithZero R
a✝ b✝ : R
hx₁ : a✝ ∈ {x | ∀ (z : R), z * x = 0 → z = 0}
hx₂ : b✝ ∈ {x | ∀ (z : R), z * x = 0 → z = 0}
x✝ : R
hz : x✝ * (a✝ * b✝) = 0
⊢ x✝ = 0
[PROOFSTEP]
rw [← mul_assoc] at hz
[GOAL]
R : Type u_1
inst✝ : MonoidWithZero R
a✝ b✝ : R
hx₁ : a✝ ∈ {x | ∀ (z : R), z * x = 0 → z = 0}
hx₂ : b✝ ∈ {x | ∀ (z : R), z * x = 0 → z = 0}
x✝ : R
hz : x✝ * a✝ * b✝ = 0
⊢ x✝ = 0
[PROOFSTEP]
exact hx₁ _ (hx₂ _ hz)
[GOAL]
R : Type u_1
inst✝ : MonoidWithZero R
x✝ : R
hz : x✝ * 1 = 0
⊢ x✝ = 0
[PROOFSTEP]
rwa [mul_one] at hz
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
x r : M
hr : r ∈ M⁰
⊢ x = 0 → x * r = 0
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
r x : M₁
hr : r ∈ M₁⁰
⊢ r * x = 0 ↔ x = 0
[PROOFSTEP]
rw [mul_comm, mul_right_mem_nonZeroDivisors_eq_zero_iff hr]
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
x y r : R
hr : r ∈ R⁰
⊢ x * r = y * r ↔ x = y
[PROOFSTEP]
refine ⟨fun h ↦ ?_, congrArg (· * r)⟩
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
x y r : R
hr : r ∈ R⁰
h : x * r = y * r
⊢ x = y
[PROOFSTEP]
rw [← sub_eq_zero, ← mul_right_mem_nonZeroDivisors_eq_zero_iff hr, sub_mul, h, sub_self]
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
x y r : R'
hr : r ∈ R'⁰
⊢ r * x = r * y ↔ x = y
[PROOFSTEP]
simp_rw [mul_comm r, mul_cancel_right_mem_nonZeroDivisors hr]
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
⊢ a * b ∈ M₁⁰ ↔ a ∈ M₁⁰ ∧ b ∈ M₁⁰
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
⊢ a * b ∈ M₁⁰ → a ∈ M₁⁰ ∧ b ∈ M₁⁰
[PROOFSTEP]
intro h
[GOAL]
case mp
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
⊢ a ∈ M₁⁰ ∧ b ∈ M₁⁰
[PROOFSTEP]
constructor
[GOAL]
case mp.left
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
⊢ a ∈ M₁⁰
[PROOFSTEP]
intro x h'
[GOAL]
case mp.right
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
⊢ b ∈ M₁⁰
[PROOFSTEP]
intro x h'
[GOAL]
case mp.left
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
x : M₁
h' : x * a = 0
⊢ x = 0
[PROOFSTEP]
apply h
[GOAL]
case mp.right
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
x : M₁
h' : x * b = 0
⊢ x = 0
[PROOFSTEP]
apply h
[GOAL]
case mp.left.a
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
x : M₁
h' : x * a = 0
⊢ x * (a * b) = 0
[PROOFSTEP]
rw [← mul_assoc, h', zero_mul]
[GOAL]
case mp.right.a
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
h : a * b ∈ M₁⁰
x : M₁
h' : x * b = 0
⊢ x * (a * b) = 0
[PROOFSTEP]
rw [mul_comm a b, ← mul_assoc, h', zero_mul]
[GOAL]
case mpr
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
⊢ a ∈ M₁⁰ ∧ b ∈ M₁⁰ → a * b ∈ M₁⁰
[PROOFSTEP]
rintro ⟨ha, hb⟩ x hx
[GOAL]
case mpr.intro
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
ha : a ∈ M₁⁰
hb : b ∈ M₁⁰
x : M₁
hx : x * (a * b) = 0
⊢ x = 0
[PROOFSTEP]
apply ha
[GOAL]
case mpr.intro.a
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
ha : a ∈ M₁⁰
hb : b ∈ M₁⁰
x : M₁
hx : x * (a * b) = 0
⊢ x * a = 0
[PROOFSTEP]
apply hb
[GOAL]
case mpr.intro.a.a
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
inst✝⁴ : MonoidWithZero M
inst✝³ : MonoidWithZero M'
inst✝² : CommMonoidWithZero M₁
inst✝¹ : Ring R
inst✝ : CommRing R'
a b : M₁
ha : a ∈ M₁⁰
hb : b ∈ M₁⁰
x : M₁
hx : x * (a * b) = 0
⊢ x * a * b = 0
[PROOFSTEP]
rw [mul_assoc, hx]
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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'⁰
[PROOFSTEP]
cases subsingleton_or_nontrivial M
[GOAL]
case inl
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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'⁰
[PROOFSTEP]
simp [Subsingleton.elim S ⊥]
[GOAL]
case inr
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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'⁰
[PROOFSTEP]
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
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
swap
[GOAL]
case mpr
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
rintro ⟨r, hrs, rfl⟩
[GOAL]
case mpr.intro.intro
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
exact Multiset.prod_eq_zero hrs
[GOAL]
case mp
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
induction' s using Multiset.induction_on with a s ih
[GOAL]
case mp.empty
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
intro habs
[GOAL]
case mp.empty
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
simp at habs
[GOAL]
case mp.cons
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
rw [Multiset.prod_cons]
[GOAL]
case mp.cons
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
intro hprod
[GOAL]
case mp.cons
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
replace hprod := eq_zero_or_eq_zero_of_mul_eq_zero hprod
[GOAL]
case mp.cons
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
cases' hprod with ha hb
[GOAL]
case mp.cons.inl
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
exact ⟨a, Multiset.mem_cons_self a s, ha⟩
[GOAL]
case mp.cons.inr
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
apply (ih hb).imp _
[GOAL]
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
rintro b ⟨hb₁, hb₂⟩
[GOAL]
case intro
M : Type u_1
M' : Type u_2
M₁ : Type u_3
R : Type u_4
R' : Type u_5
F : Type u_6
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
[PROOFSTEP]
exact ⟨Multiset.mem_cons_of_mem hb₁, hb₂⟩


[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a : R
s : Finset α
p : α → R
hp : ∀ (i : α), i ∈ s → Prime (p i)
hx : x * y = a * ∏ i in s, p i
⊢ ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
[PROOFSTEP]
induction' s using Finset.induction with i s his ih generalizing x y a
[GOAL]
case empty
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x✝ y✝ a✝ : R
s : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s → Prime (p i)
hx✝ : x✝ * y✝ = a✝ * ∏ i in s, p i
x y a : R
hp : ∀ (i : α), i ∈ ∅ → Prime (p i)
hx : x * y = a * ∏ i in ∅, p i
⊢ ∃ t u b c, t ∪ u = ∅ ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
[PROOFSTEP]
exact ⟨∅, ∅, x, y, by simp [hx]⟩
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x✝ y✝ a✝ : R
s : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s → Prime (p i)
hx✝ : x✝ * y✝ = a✝ * ∏ i in s, p i
x y a : R
hp : ∀ (i : α), i ∈ ∅ → Prime (p i)
hx : x * y = a * ∏ i in ∅, p i
⊢ ∅ ∪ ∅ = ∅ ∧ Disjoint ∅ ∅ ∧ a = x * y ∧ x = x * ∏ i in ∅, p i ∧ y = y * ∏ i in ∅, p i
[PROOFSTEP]
simp [hx]
[GOAL]
case insert
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x✝ y✝ a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x✝ * y✝ = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
x y a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hx : x * y = a * ∏ i in insert i s, p i
⊢ ∃ t u b c, t ∪ u = insert i s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
[PROOFSTEP]
rw [prod_insert his, ← mul_assoc] at hx
[GOAL]
case insert
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x✝ y✝ a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x✝ * y✝ = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
x y a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hx : x * y = a * p i * ∏ x in s, p x
⊢ ∃ t u b c, t ∪ u = insert i s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
[PROOFSTEP]
have hpi : Prime (p i) := hp i (mem_insert_self _ _)
[GOAL]
case insert
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x✝ y✝ a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x✝ * y✝ = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
x y a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hx : x * y = a * p i * ∏ x in s, p x
hpi : Prime (p i)
⊢ ∃ t u b c, t ∪ u = insert i s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
[PROOFSTEP]
rcases ih (fun i hi ↦ hp i (mem_insert_of_mem hi)) hx with ⟨t, u, b, c, htus, htu, hbc, rfl, rfl⟩
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i in t, p i) * (c * ∏ i in u, p i) = a * p i * ∏ x in s, p x
⊢ ∃ t_1 u_1 b_1 c_1,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c_1 ∧ b * ∏ i in t, p i = b_1 * ∏ i in t_1, p i ∧ c * ∏ i in u, p i = c_1 * ∏ i in u_1, p i
[PROOFSTEP]
have hit : i ∉ t := fun hit ↦ his (htus ▸ mem_union_left _ hit)
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i in t, p i) * (c * ∏ i in u, p i) = a * p i * ∏ x in s, p x
hit : ¬i ∈ t
⊢ ∃ t_1 u_1 b_1 c_1,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c_1 ∧ b * ∏ i in t, p i = b_1 * ∏ i in t_1, p i ∧ c * ∏ i in u, p i = c_1 * ∏ i in u_1, p i
[PROOFSTEP]
have hiu : i ∉ u := fun hiu ↦ his (htus ▸ mem_union_right _ hiu)
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i in t, p i) * (c * ∏ i in u, p i) = a * p i * ∏ x in s, p x
hit : ¬i ∈ t
hiu : ¬i ∈ u
⊢ ∃ t_1 u_1 b_1 c_1,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c_1 ∧ b * ∏ i in t, p i = b_1 * ∏ i in t_1, p i ∧ c * ∏ i in u, p i = c_1 * ∏ i in u_1, p i
[PROOFSTEP]
obtain ⟨d, rfl⟩ | ⟨d, rfl⟩ : p i ∣ b ∨ p i ∣ c
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i in t, p i) * (c * ∏ i in u, p i) = a * p i * ∏ x in s, p x
hit : ¬i ∈ t
hiu : ¬i ∈ u
⊢ p i ∣ b ∨ p i ∣ c
case insert.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : ¬i ∈ t
hiu : ¬i ∈ u
d : R
hbc : a * p i = p i * d * c
hx : (p i * d * ∏ i in t, p i) * (c * ∏ i in u, p i) = a * p i * ∏ x in s, p x
⊢ ∃ t_1 u_1 b c_1,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b * c_1 ∧ p i * d * ∏ i in t, p i = b * ∏ i in t_1, p i ∧ c * ∏ i in u, p i = c_1 * ∏ i in u_1, p i
case insert.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : ¬i ∈ t
hiu : ¬i ∈ u
d : R
hbc : a * p i = b * (p i * d)
hx : (b * ∏ i in t, p i) * (p i * d * ∏ i in u, p i) = a * p i * ∏ x in s, p x
⊢ ∃ t_1 u_1 b_1 c,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c ∧ b * ∏ i in t, p i = b_1 * ∏ i in t_1, p i ∧ p i * d * ∏ i in u, p i = c * ∏ i in u_1, p i
[PROOFSTEP]
exact hpi.dvd_or_dvd ⟨a, by rw [← hbc, mul_comm]⟩
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i in t, p i) * (c * ∏ i in u, p i) = a * p i * ∏ x in s, p x
hit : ¬i ∈ t
hiu : ¬i ∈ u
⊢ b * c = p i * a
[PROOFSTEP]
rw [← hbc, mul_comm]
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : ¬i ∈ t
hiu : ¬i ∈ u
d : R
hbc : a * p i = p i * d * c
hx : (p i * d * ∏ i in t, p i) * (c * ∏ i in u, p i) = a * p i * ∏ x in s, p x
⊢ ∃ t_1 u_1 b c_1,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b * c_1 ∧ p i * d * ∏ i in t, p i = b * ∏ i in t_1, p i ∧ c * ∏ i in u, p i = c_1 * ∏ i in u_1, p i
[PROOFSTEP]
rw [mul_assoc, mul_comm a, mul_right_inj' hpi.ne_zero] at hbc
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : ¬i ∈ t
hiu : ¬i ∈ u
d : R
hbc : a = d * c
hx : (p i * d * ∏ i in t, p i) * (c * ∏ i in u, p i) = a * p i * ∏ x in s, p x
⊢ ∃ t_1 u_1 b c_1,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b * c_1 ∧ p i * d * ∏ i in t, p i = b * ∏ i in t_1, p i ∧ c * ∏ i in u, p i = c_1 * ∏ i in u_1, p i
[PROOFSTEP]
exact
  ⟨insert i t, u, d, c, by rw [insert_union, htus], disjoint_insert_left.2 ⟨hiu, htu⟩, by
    simp [hbc, prod_insert hit, mul_assoc, mul_comm, mul_left_comm]⟩
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : ¬i ∈ t
hiu : ¬i ∈ u
d : R
hbc : a = d * c
hx : (p i * d * ∏ i in t, p i) * (c * ∏ i in u, p i) = a * p i * ∏ x in s, p x
⊢ insert i t ∪ u = insert i s
[PROOFSTEP]
rw [insert_union, htus]
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : ¬i ∈ t
hiu : ¬i ∈ u
d : R
hbc : a = d * c
hx : (p i * d * ∏ i in t, p i) * (c * ∏ i in u, p i) = a * p i * ∏ x in s, p x
⊢ a = d * c ∧ p i * d * ∏ i in t, p i = d * ∏ i in insert i t, p i ∧ c * ∏ i in u, p i = c * ∏ i in u, p i
[PROOFSTEP]
simp [hbc, prod_insert hit, mul_assoc, mul_comm, mul_left_comm]
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : ¬i ∈ t
hiu : ¬i ∈ u
d : R
hbc : a * p i = b * (p i * d)
hx : (b * ∏ i in t, p i) * (p i * d * ∏ i in u, p i) = a * p i * ∏ x in s, p x
⊢ ∃ t_1 u_1 b_1 c,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c ∧ b * ∏ i in t, p i = b_1 * ∏ i in t_1, p i ∧ p i * d * ∏ i in u, p i = c * ∏ i in u_1, p i
[PROOFSTEP]
rw [← mul_assoc, mul_right_comm b, mul_left_inj' hpi.ne_zero] at hbc
[GOAL]
case insert.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : ¬i ∈ t
hiu : ¬i ∈ u
d : R
hbc : a = b * d
hx : (b * ∏ i in t, p i) * (p i * d * ∏ i in u, p i) = a * p i * ∏ x in s, p x
⊢ ∃ t_1 u_1 b_1 c,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c ∧ b * ∏ i in t, p i = b_1 * ∏ i in t_1, p i ∧ p i * d * ∏ i in u, p i = c * ∏ i in u_1, p i
[PROOFSTEP]
exact
  ⟨t, insert i u, b, d, by rw [union_insert, htus], disjoint_insert_right.2 ⟨hit, htu⟩, by
    simp [← hbc, prod_insert hiu, mul_assoc, mul_comm, mul_left_comm]⟩
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : ¬i ∈ t
hiu : ¬i ∈ u
d : R
hbc : a = b * d
hx : (b * ∏ i in t, p i) * (p i * d * ∏ i in u, p i) = a * p i * ∏ x in s, p x
⊢ t ∪ insert i u = insert i s
[PROOFSTEP]
rw [union_insert, htus]
[GOAL]
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
x y a✝ : R
s✝ : Finset α
p : α → R
hp✝ : ∀ (i : α), i ∈ s✝ → Prime (p i)
hx✝ : x * y = a✝ * ∏ i in s✝, p i
i : α
s : Finset α
his : ¬i ∈ s
ih :
  ∀ {x y a : R},
    (∀ (i : α), i ∈ s → Prime (p i)) →
      x * y = a * ∏ i in s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i in t, p i ∧ y = c * ∏ i in u, p i
a : R
hp : ∀ (i_1 : α), i_1 ∈ insert i s → Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : ¬i ∈ t
hiu : ¬i ∈ u
d : R
hbc : a = b * d
hx : (b * ∏ i in t, p i) * (p i * d * ∏ i in u, p i) = a * p i * ∏ x in s, p x
⊢ a = b * d ∧ b * ∏ i in t, p i = b * ∏ i in t, p i ∧ p i * d * ∏ i in u, p i = d * ∏ i in insert i u, p i
[PROOFSTEP]
simp [← hbc, prod_insert hiu, mul_assoc, mul_comm, mul_left_comm]
[GOAL]
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y a p : R
n : ℕ
hp : Prime p
hx : x * y = a * p ^ n
⊢ ∃ i j b c, i + j = n ∧ a = b * c ∧ x = b * p ^ i ∧ y = c * p ^ j
[PROOFSTEP]
rcases mul_eq_mul_prime_prod (fun _ _ ↦ hp) (show x * y = a * (range n).prod fun _ ↦ p by simpa) with
  ⟨t, u, b, c, htus, htu, rfl, rfl, rfl⟩
[GOAL]
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y a p : R
n : ℕ
hp : Prime p
hx : x * y = a * p ^ n
⊢ x * y = a * ∏ x in range n, p
[PROOFSTEP]
simpa
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i in t, p) * (c * ∏ i in u, p) = b * c * p ^ n
⊢ ∃ i j b_1 c_1, i + j = n ∧ b * c = b_1 * c_1 ∧ b * ∏ i in t, p = b_1 * p ^ i ∧ c * ∏ i in u, p = c_1 * p ^ j
[PROOFSTEP]
exact ⟨t.card, u.card, b, c, by rw [← card_disjoint_union htu, htus, card_range], by simp⟩
[GOAL]
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i in t, p) * (c * ∏ i in u, p) = b * c * p ^ n
⊢ card t + card u = n
[PROOFSTEP]
rw [← card_disjoint_union htu, htus, card_range]
[GOAL]
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i in t, p) * (c * ∏ i in u, p) = b * c * p ^ n
⊢ b * c = b * c ∧ b * ∏ i in t, p = b * p ^ card t ∧ c * ∏ i in u, p = c * p ^ card u
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommRing α
p : α
hp : Prime p
⊢ Prime (-p)
[PROOFSTEP]
obtain ⟨h1, h2, h3⟩ := hp
[GOAL]
case intro.intro
α : Type u_1
inst✝ : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ Prime (-p)
[PROOFSTEP]
exact ⟨neg_ne_zero.mpr h1, by rwa [IsUnit.neg_iff], by simpa [neg_dvd] using h3⟩
[GOAL]
α : Type u_1
inst✝ : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ ¬IsUnit (-p)
[PROOFSTEP]
rwa [IsUnit.neg_iff]
[GOAL]
α : Type u_1
inst✝ : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ ∀ (a b : α), -p ∣ a * b → -p ∣ a ∨ -p ∣ b
[PROOFSTEP]
simpa [neg_dvd] using h3
[GOAL]
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
⊢ Prime |p|
[PROOFSTEP]
obtain h | h := abs_choice p
[GOAL]
case inl
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = p
⊢ Prime |p|
[PROOFSTEP]
rw [h]
[GOAL]
case inr
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = -p
⊢ Prime |p|
[PROOFSTEP]
rw [h]
[GOAL]
case inl
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = p
⊢ Prime p
[PROOFSTEP]
exact hp
[GOAL]
case inr
α : Type u_1
inst✝¹ : CommRing α
inst✝ : LinearOrder α
p : α
hp : Prime p
h : |p| = -p
⊢ Prime (-p)
[PROOFSTEP]
exact hp.neg