α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (Associates.mk p ≠ 0 ∧
      ¬IsUnit (Associates.mk p) ∧
        ∀ (a : α) (b : Associates α),
          Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prime (Associates.mk p) ↔ Prime p
rw [Prime, _root_.Prime, forall_associated]
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (Associates.mk p ≠ 0 ∧
      ¬IsUnit (Associates.mk p) ∧
        ∀ (a : α) (b : Associates α),
          Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?m.319210

α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ ?m.319210 ↔ p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b

α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (Associates.mk p ≠ 0 ∧
      ¬IsUnit (Associates.mk p) ∧
        ∀ (a : α) (b : Associates α),
          Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
trans
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (¬IsUnit (Associates.mk p) ∧
      ∀ (a a_1 : α),
        Associates.mk p ∣ Associates.mk a * Associates.mk a_1 →
          Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ Associates.mk a_1) ↔
    ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (Associates.mk p ≠ 0 ∧
      ¬IsUnit (Associates.mk p) ∧
        ∀ (a a_1 : α),
          Associates.mk p ∣ Associates.mk a * Associates.mk a_1 →
            Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ Associates.mk a_1) ↔
    p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
apply and_congr mk_ne_zero
case h₁
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ ¬IsUnit (Associates.mk p) ↔ ¬IsUnit p

case h₂
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (∀ (a a_1 : α),
      Associates.mk p ∣ Associates.mk a * Associates.mk a_1 →
        Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ Associates.mk a_1) ↔
    ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (¬IsUnit (Associates.mk p) ∧
      ∀ (a a_1 : α),
        Associates.mk p ∣ Associates.mk a * Associates.mk a_1 →
          Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ Associates.mk a_1) ↔
    ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
apply and_congr
case h₂
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p a b : α
⊢ Associates.mk p ∣ Associates.mk a * Associates.mk b →
      Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ Associates.mk b ↔
    p ∣ a * b → p ∣ a ∨ p ∣ b
case h₂
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (∀ (a a_1 : α),
      Associates.mk p ∣ Associates.mk a * Associates.mk a_1 →
        Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ Associates.mk a_1) ↔
    ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
refine' forall₂_congr fun a b => _
no goals
case h₂
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p a b : α
⊢ Associates.mk p ∣ Associates.mk a * Associates.mk b →
      Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ Associates.mk b ↔
    p ∣ a * b → p ∣ a ∨ p ∣ b
rw [mk_mul_mk, mk_dvd_mk, mk_dvd_mk, mk_dvd_mk]
case h₁
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Associates.mk p ≠ 0 ↔ ?c

case h₂
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (¬IsUnit (Associates.mk p) ∧
      ∀ (a : α) (b : Associates α),
        Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?d

case c
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop

case d
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (Associates.mk p ≠ 0 ∧
      ¬IsUnit (Associates.mk p) ∧
        ∀ (a : α) (b : Associates α),
          Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?m.319210
apply and_congr
case h₂
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (¬IsUnit (Associates.mk p) ∧
      ∀ (a : α) (b : Associates α),
        Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?d

case d
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop
case h₁
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Associates.mk p ≠ 0 ↔ ?c

case h₂
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (¬IsUnit (Associates.mk p) ∧
      ∀ (a : α) (b : Associates α),
        Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?d

case c
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop

case d
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop
rfl
case h₂.h₁
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ ¬IsUnit (Associates.mk p) ↔ ?h₂.c

case h₂.h₂
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (∀ (a : α) (b : Associates α),
      Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?h₂.d

case h₂.c
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop

case h₂.d
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop
case h₂
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (¬IsUnit (Associates.mk p) ∧
      ∀ (a : α) (b : Associates α),
        Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?d

case d
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop
apply and_congr
case h₂.h₂
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (∀ (a : α) (b : Associates α),
      Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?h₂.d

case h₂.d
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop
case h₂.h₁
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ ¬IsUnit (Associates.mk p) ↔ ?h₂.c

case h₂.h₂
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (∀ (a : α) (b : Associates α),
      Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?h₂.d

case h₂.c
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop

case h₂.d
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop
rfl
case h₂.h₂.h
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ ∀ (a : α),
    (∀ (b : Associates α),
        Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
      ?h₂.h₂.q a

case h₂.h₂.q
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ α → Prop
case h₂.h₂
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ (∀ (a : α) (b : Associates α),
      Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?h₂.d

case h₂.d
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ Prop
apply forall_congr'
case h₂.h₂.h
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p a : α
⊢ (∀ (b : Associates α),
      Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?h₂.h₂.q a

case h₂.h₂.q
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ α → Prop
case h₂.h₂.h
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ ∀ (a : α),
    (∀ (b : Associates α),
        Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
      ?h₂.h₂.q a

case h₂.h₂.q
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ α → Prop
intro a
no goals
case h₂.h₂.h
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p a : α
⊢ (∀ (b : Associates α),
      Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔
    ?h₂.h₂.q a

case h₂.h₂.q
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ α → Prop
exact forall_associated
no goals
case h₁
α : Type u_1
β : Type ?u.318602
γ : Type ?u.318605
δ : Type ?u.318608
inst✝ : CommMonoidWithZero α
p : α
⊢ ¬IsUnit (Associates.mk p) ↔ ¬IsUnit p
rw [isUnit_mk]