α : Type ?u.938840
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d
d : R
⊢ a = 0 → b = 0 → IsUnit 0
α : Type ?u.938840
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d
d : R
⊢ 0 ∣ a → 0 ∣ b → IsUnit 0
simp only [zero_dvd_iff]
α : Type ?u.938840
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d
d : R
a✝¹ : a = 0
a✝ : b = 0
⊢ IsUnit 0
α : Type ?u.938840
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d
d : R
⊢ a = 0 → b = 0 → IsUnit 0
intros
no goals
α : Type ?u.938840
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d
d : R
a✝¹ : a = 0
a✝ : b = 0
⊢ IsUnit 0
contradiction