case refine'_1
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
h : ∀ (f g : R[X]), Monic f → Monic g → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ Monic (g * ↑C (leadingCoeff f))

case refine'_2
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
h : ∀ (f g : R[X]), Monic f → Monic g → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ Monic (f * ↑C (leadingCoeff g))

case refine'_3
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
h : ∀ (f g : R[X]), Monic f → Monic g → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ g * ↑C (leadingCoeff f) * (f * ↑C (leadingCoeff g)) = p
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 ↔ ∀ (f g : R[X]), Monic f → Monic g → f * g = p → f = 1 ∨ g = 1
refine'
  ⟨fun h f g hf hg hp => (h.2 f g hp.symm).imp hf.eq_one_of_isUnit hg.eq_one_of_isUnit, fun h =>
    ⟨hp1 ∘ hp.eq_one_of_isUnit, fun f g hfg =>
      (h (g * C f.leadingCoeff) (f * C g.leadingCoeff) _ _ _).symm.imp (isUnit_of_mul_eq_one f _)
        (isUnit_of_mul_eq_one g _)⟩⟩
no goals
case refine'_1
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
h : ∀ (f g : R[X]), Monic f → Monic g → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ Monic (g * ↑C (leadingCoeff f))
rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, mul_comm, ← hfg, ← Monic]
no goals
case refine'_2
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
h : ∀ (f g : R[X]), Monic f → Monic g → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ Monic (f * ↑C (leadingCoeff g))
rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, ← hfg, ← Monic]
no goals
case refine'_3
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
h : ∀ (f g : R[X]), Monic f → Monic g → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ g * ↑C (leadingCoeff f) * (f * ↑C (leadingCoeff g)) = p
rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
  mul_comm, ← hfg]