case mp
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
⊢ comp p q = 0 → p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)

case mpr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0) → comp p q = 0
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
⊢ comp p q = 0 ↔ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
constructor
case mp
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : comp p q = 0
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
case mp
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
⊢ comp p q = 0 → p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
intro h
case mp
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : comp p q = 0
key : natDegree p = 0 ∨ natDegree q = 0
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
case mp
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : comp p q = 0
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
have key : p.natDegree = 0 ∨ q.natDegree = 0 := by
  rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]
case mp
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : comp p q = 0
key : p = ↑C (coeff p 0) ∨ q = ↑C (coeff q 0)
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
case mp
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : comp p q = 0
key : natDegree p = 0 ∨ natDegree q = 0
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
replace key := Or.imp eq_C_of_natDegree_eq_zero eq_C_of_natDegree_eq_zero key
case mp.inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : comp p q = 0
key : p = ↑C (coeff p 0)
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)

case mp.inr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : comp p q = 0
key : q = ↑C (coeff q 0)
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
case mp
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : comp p q = 0
key : p = ↑C (coeff p 0) ∨ q = ↑C (coeff q 0)
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
cases' key with key key
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : comp p q = 0
⊢ natDegree p = 0 ∨ natDegree q = 0
rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]
case mp.inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : ↑C (coeff p 0) = 0
key : p = ↑C (coeff p 0)
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
case mp.inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : comp p q = 0
key : p = ↑C (coeff p 0)
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
rw [key, C_comp] at h
no goals
case mp.inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : ↑C (coeff p 0) = 0
key : p = ↑C (coeff p 0)
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
exact Or.inl (key.trans h)
case mp.inr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : eval (coeff q 0) p = 0
key : q = ↑C (coeff q 0)
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
case mp.inr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : comp p q = 0
key : q = ↑C (coeff q 0)
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
rw [key, comp_C, C_eq_zero] at h
no goals
case mp.inr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : eval (coeff q 0) p = 0
key : q = ↑C (coeff q 0)
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
exact Or.inr ⟨h, key⟩
no goals
case mpr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
⊢ p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0) → comp p q = 0
exact fun h =>
  Or.rec (fun h => by rw [h, zero_comp]) (fun h => by rw [h.2, comp_C, h.1, C_0]) h
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h✝ : p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
h : p = 0
⊢ comp p q = 0
rw [h, zero_comp]
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h✝ : p = 0 ∨ eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
h : eval (coeff q 0) p = 0 ∧ q = ↑C (coeff q 0)
⊢ comp p q = 0
rw [h.2, comp_C, h.1, C_0]