case pos
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
hp1 : p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), Monic f → Monic g → f * g = p → natDegree f = 0 ∨ natDegree g = 0

case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
hp1 : ¬p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), Monic f → Monic g → f * g = p → natDegree f = 0 ∨ natDegree g = 0
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), Monic f → Monic g → f * g = p → natDegree f = 0 ∨ natDegree g = 0
by_cases hp1 : p = 1
case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
hp1 : ¬p = 1
⊢ (∀ (f g : R[X]), Monic f → Monic g → f * g = p → f = 1 ∨ g = 1) ↔
    ∀ (f g : R[X]), Monic f → Monic g → f * g = p → natDegree f = 0 ∨ natDegree g = 0
case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
hp1 : ¬p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), Monic f → Monic g → f * g = p → natDegree f = 0 ∨ natDegree g = 0
rw [irreducible_of_monic hp hp1, and_iff_right hp1]
case neg
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
hp1 : ¬p = 1
a b : R[X]
ha : Monic a
hb : Monic b
⊢ a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → natDegree a = 0 ∨ natDegree b = 0
case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
hp1 : ¬p = 1
⊢ (∀ (f g : R[X]), Monic f → Monic g → f * g = p → f = 1 ∨ g = 1) ↔
    ∀ (f g : R[X]), Monic f → Monic g → f * g = p → natDegree f = 0 ∨ natDegree g = 0
refine' forall₄_congr fun a b ha hb => _
no goals
case neg
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
hp1 : ¬p = 1
a b : R[X]
ha : Monic a
hb : Monic b
⊢ a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → natDegree a = 0 ∨ natDegree b = 0
rw [ha.natDegree_eq_zero_iff_eq_one, hb.natDegree_eq_zero_iff_eq_one]
no goals
case pos
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : Monic p
hp1 : p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), Monic f → Monic g → f * g = p → natDegree f = 0 ∨ natDegree g = 0
simp [hp1]