R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Monic f
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit a ∨ IsUnit b
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Monic f
h_irr : Irreducible (Polynomial.map φ f)
⊢ Irreducible f
refine' ⟨h_irr.not_unit ∘ IsUnit.map (mapRingHom φ), fun a b h => _⟩
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit a ∨ IsUnit b
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Monic f
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit a ∨ IsUnit b
dsimp [Monic] at h_mon
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = Polynomial.leadingCoeff (a * b)
⊢ IsUnit a ∨ IsUnit b
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit a ∨ IsUnit b
have q := (leadingCoeff_mul a b).symm
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ IsUnit a ∨ IsUnit b
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = Polynomial.leadingCoeff (a * b)
⊢ IsUnit a ∨ IsUnit b
rw [← h, h_mon] at q
case refine'_1.hf.h
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ Polynomial.leadingCoeff a * ?refine'_1.hf.b = 1

case refine'_1.hf.b
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ R

case refine'_2.hf.h
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ Polynomial.leadingCoeff b * ?refine'_2.hf.b = 1

case refine'_2.hf.b
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ R
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ IsUnit a ∨ IsUnit b
refine' (h_irr.isUnit_or_isUnit <|
  (congr_arg (Polynomial.map φ) h).trans (Polynomial.map_mul φ)).imp _ _ <;>
    apply isUnit_of_isUnit_leadingCoeff_of_isUnit_map <;>
  apply isUnit_of_mul_eq_one
no goals
case refine'_1.hf.h
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ Polynomial.leadingCoeff a * ?refine'_1.hf.b = 1
exact q
case refine'_2.hf.h
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ ?refine'_2.hf.h.b * Polynomial.leadingCoeff b = 1

case refine'_2.hf.h.b
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ R
case refine'_2.hf.h
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ Polynomial.leadingCoeff b * ?refine'_2.hf.b = 1
rw [mul_comm]
no goals
case refine'_2.hf.h
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ ?refine'_2.hf.h.b * Polynomial.leadingCoeff b = 1

case refine'_2.hf.h.b
R : Type u
S : Type v
T : Type w
a✝ b✝ : R
n : ℕ
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : Polynomial.leadingCoeff f = 1
h_irr : Irreducible (Polynomial.map φ f)
a b : R[X]
h : f = a * b
q : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ R
exact q