case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ Associates.mk a ⊓ Associates.mk b = 1 → ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d

case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ (∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d) → Associates.mk a ⊓ Associates.mk b = 1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ Associates.mk a ⊓ Associates.mk b = 1 ↔ ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d
constructor
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
ha : p ∣ a
hb : p ∣ b
hp : Prime p
⊢ False
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ Associates.mk a ⊓ Associates.mk b = 1 → ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d
intro hg p ha hb hp
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
ha : p ∣ a
hb : p ∣ b
hp : Prime p
⊢ Associates.mk p ∣ 1
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
ha : p ∣ a
hb : p ∣ b
hp : Prime p
⊢ False
refine' ((Associates.prime_mk _).mpr hp).not_unit (isUnit_of_dvd_one _)
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
ha : p ∣ a
hb : p ∣ b
hp : Prime p
⊢ Associates.mk p ∣ Associates.mk a ⊓ Associates.mk b
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
ha : p ∣ a
hb : p ∣ b
hp : Prime p
⊢ Associates.mk p ∣ 1
rw [← hg]
no goals
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
ha : p ∣ a
hb : p ∣ b
hp : Prime p
⊢ Associates.mk p ∣ Associates.mk a ⊓ Associates.mk b
exact le_inf (mk_le_mk_of_dvd ha) (mk_le_mk_of_dvd hb)
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ ¬Associates.mk a ⊓ Associates.mk b = 1 → ¬∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ (∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d) → Associates.mk a ⊓ Associates.mk b = 1
contrapose
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : ¬Associates.mk a ⊓ Associates.mk b = 1
hc : ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d
⊢ False
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ ¬Associates.mk a ⊓ Associates.mk b = 1 → ¬∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d
intro hg hc
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : ¬Associates.mk a ⊓ Associates.mk b = 1
hc : ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d
p : α
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ False
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : ¬Associates.mk a ⊓ Associates.mk b = 1
hc : ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d
⊢ False
obtain ⟨p, hp, hpa, hpb⟩ := exists_prime_dvd_of_not_inf_one ha0 hb0 hg
no goals
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : ¬Associates.mk a ⊓ Associates.mk b = 1
hc : ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d
p : α
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ False
exact hc hpa hpb hp