[GOAL]
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : Monic f
g : K[X]
hg : Monic g
hd : g ∣ map (algebraMap R K) f
⊢ g ∈ lifts (algebraMap { x // x ∈ integralClosure R K } K)
[PROOFSTEP]
have :=
  mem_lift_of_splits_of_roots_mem_range (integralClosure R g.SplittingField)
    ((splits_id_iff_splits _).2 <| SplittingField.splits g) (hg.map _) fun a ha =>
    (SetLike.ext_iff.mp (integralClosure R g.SplittingField).range_algebraMap _).mpr <| roots_mem_integralClosure hf ?_
[GOAL]
case refine_2
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : Monic f
g : K[X]
hg : Monic g
hd : g ∣ map (algebraMap R K) f
this :
  map (algebraMap K (SplittingField g)) g ∈
    lifts (algebraMap { x // x ∈ integralClosure R (SplittingField g) } (SplittingField g))
⊢ g ∈ lifts (algebraMap { x // x ∈ integralClosure R K } K)
[PROOFSTEP]
rw [lifts_iff_coeff_lifts, ← RingHom.coe_range, Subalgebra.range_algebraMap] at this
[GOAL]
case refine_2
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : Monic f
g : K[X]
hg : Monic g
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K (SplittingField g)) g) n ∈ ↑(Subalgebra.toSubring (integralClosure R (SplittingField g)))
⊢ g ∈ lifts (algebraMap { x // x ∈ integralClosure R K } K)
[PROOFSTEP]
refine' (lifts_iff_coeff_lifts _).2 fun n => _
[GOAL]
case refine_2
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : Monic f
g : K[X]
hg : Monic g
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K (SplittingField g)) g) n ∈ ↑(Subalgebra.toSubring (integralClosure R (SplittingField g)))
n : ℕ
⊢ coeff g n ∈ Set.range ↑(algebraMap { x // x ∈ integralClosure R K } K)
[PROOFSTEP]
rw [← RingHom.coe_range, Subalgebra.range_algebraMap]
[GOAL]
case refine_2
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : Monic f
g : K[X]
hg : Monic g
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K (SplittingField g)) g) n ∈ ↑(Subalgebra.toSubring (integralClosure R (SplittingField g)))
n : ℕ
⊢ coeff g n ∈ ↑(Subalgebra.toSubring (integralClosure R K))
[PROOFSTEP]
obtain ⟨p, hp, he⟩ := SetLike.mem_coe.mp (this n)
[GOAL]
case refine_2.intro.intro
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : Monic f
g : K[X]
hg : Monic g
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K (SplittingField g)) g) n ∈ ↑(Subalgebra.toSubring (integralClosure R (SplittingField g)))
n : ℕ
p : R[X]
hp : Monic p
he : eval₂ (algebraMap R (SplittingField g)) (coeff (map (algebraMap K (SplittingField g)) g) n) p = 0
⊢ coeff g n ∈ ↑(Subalgebra.toSubring (integralClosure R K))
[PROOFSTEP]
use p, hp
[GOAL]
case right
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : Monic f
g : K[X]
hg : Monic g
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K (SplittingField g)) g) n ∈ ↑(Subalgebra.toSubring (integralClosure R (SplittingField g)))
n : ℕ
p : R[X]
hp : Monic p
he : eval₂ (algebraMap R (SplittingField g)) (coeff (map (algebraMap K (SplittingField g)) g) n) p = 0
⊢ eval₂ (algebraMap R K) (coeff g n) p = 0
[PROOFSTEP]
rw [IsScalarTower.algebraMap_eq R K, coeff_map, ← eval₂_map, eval₂_at_apply] at he
[GOAL]
case right
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : Monic f
g : K[X]
hg : Monic g
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K (SplittingField g)) g) n ∈ ↑(Subalgebra.toSubring (integralClosure R (SplittingField g)))
n : ℕ
p : R[X]
hp : Monic p
he : ↑(algebraMap K (SplittingField g)) (eval (coeff g n) (map (algebraMap R K) p)) = 0
⊢ eval₂ (algebraMap R K) (coeff g n) p = 0
[PROOFSTEP]
rw [eval₂_eq_eval_map]
[GOAL]
case right
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : Monic f
g : K[X]
hg : Monic g
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K (SplittingField g)) g) n ∈ ↑(Subalgebra.toSubring (integralClosure R (SplittingField g)))
n : ℕ
p : R[X]
hp : Monic p
he : ↑(algebraMap K (SplittingField g)) (eval (coeff g n) (map (algebraMap R K) p)) = 0
⊢ eval (coeff g n) (map (algebraMap R K) p) = 0
[PROOFSTEP]
apply (injective_iff_map_eq_zero _).1 _ _ he
[GOAL]
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : Monic f
g : K[X]
hg : Monic g
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K (SplittingField g)) g) n ∈ ↑(Subalgebra.toSubring (integralClosure R (SplittingField g)))
n : ℕ
p : R[X]
hp : Monic p
he : ↑(algebraMap K (SplittingField g)) (eval (coeff g n) (map (algebraMap R K) p)) = 0
⊢ Function.Injective ↑(algebraMap K (SplittingField g))
[PROOFSTEP]
apply RingHom.injective
[GOAL]
case refine_1
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : Monic f
g : K[X]
hg : Monic g
hd : g ∣ map (algebraMap R K) f
a : SplittingField g
ha : a ∈ roots (map (algebraMap K (SplittingField g)) g)
⊢ a ∈ roots (map (algebraMap R (SplittingField g)) f)
[PROOFSTEP]
rw [IsScalarTower.algebraMap_eq R K _, ← map_map]
[GOAL]
case refine_1
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : Monic f
g : K[X]
hg : Monic g
hd : g ∣ map (algebraMap R K) f
a : SplittingField g
ha : a ∈ roots (map (algebraMap K (SplittingField g)) g)
⊢ a ∈ roots (map (algebraMap K (SplittingField g)) (map (algebraMap R K) f))
[PROOFSTEP]
refine' Multiset.mem_of_le (roots.le_of_dvd ((hf.map _).map _).ne_zero _) ha
[GOAL]
case refine_1
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : Monic f
g : K[X]
hg : Monic g
hd : g ∣ map (algebraMap R K) f
a : SplittingField g
ha : a ∈ roots (map (algebraMap K (SplittingField g)) g)
⊢ map (algebraMap K (SplittingField g)) g ∣ map (algebraMap K (SplittingField g)) (map (algebraMap R K) f)
[PROOFSTEP]
exact map_dvd (algebraMap K g.SplittingField) hd
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
⊢ ∃ g', map (algebraMap R K) g' * ↑C (leadingCoeff g) = g
[PROOFSTEP]
have g_ne_0 : g ≠ 0 := ne_zero_of_dvd_ne_zero (Monic.ne_zero <| hf.map (algebraMap R K)) hg
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ ∃ g', map (algebraMap R K) g' * ↑C (leadingCoeff g) = g
[PROOFSTEP]
suffices lem : ∃ g' : R[X], g'.map (algebraMap R K) = g * C g.leadingCoeff⁻¹
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
lem : ∃ g', map (algebraMap R K) g' = g * ↑C (leadingCoeff g)⁻¹
⊢ ∃ g', map (algebraMap R K) g' * ↑C (leadingCoeff g) = g
[PROOFSTEP]
obtain ⟨g', hg'⟩ := lem
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g' : R[X]
hg' : map (algebraMap R K) g' = g * ↑C (leadingCoeff g)⁻¹
⊢ ∃ g', map (algebraMap R K) g' * ↑C (leadingCoeff g) = g
[PROOFSTEP]
use g'
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g' : R[X]
hg' : map (algebraMap R K) g' = g * ↑C (leadingCoeff g)⁻¹
⊢ map (algebraMap R K) g' * ↑C (leadingCoeff g) = g
[PROOFSTEP]
rw [hg', mul_assoc, ← C_mul, inv_mul_cancel (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]
[GOAL]
case lem
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ ∃ g', map (algebraMap R K) g' = g * ↑C (leadingCoeff g)⁻¹
[PROOFSTEP]
have g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ f.map (algebraMap R K) :=
  by
  rwa [Associated.dvd_iff_dvd_left (show Associated (g * C g.leadingCoeff⁻¹) g from _)]
  rw [associated_mul_isUnit_left_iff]
  exact isUnit_C.mpr (inv_ne_zero <| leadingCoeff_ne_zero.mpr g_ne_0).isUnit
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
[PROOFSTEP]
rwa [Associated.dvd_iff_dvd_left (show Associated (g * C g.leadingCoeff⁻¹) g from _)]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ Associated (g * ↑C (leadingCoeff g)⁻¹) g
[PROOFSTEP]
rw [associated_mul_isUnit_left_iff]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ IsUnit (↑C (leadingCoeff g)⁻¹)
[PROOFSTEP]
exact isUnit_C.mpr (inv_ne_zero <| leadingCoeff_ne_zero.mpr g_ne_0).isUnit
[GOAL]
case lem
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
⊢ ∃ g', map (algebraMap R K) g' = g * ↑C (leadingCoeff g)⁻¹
[PROOFSTEP]
let algeq :=
  (Subalgebra.equivOfEq _ _ <| integralClosure_eq_bot R _).trans
    (Algebra.botEquivOfInjective <| IsFractionRing.injective R <| K)
[GOAL]
case lem
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
algeq : { x // x ∈ integralClosure R K } ≃ₐ[R] R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ (_ : integralClosure R K = ⊥))
    (Algebra.botEquivOfInjective (_ : Function.Injective ↑(algebraMap R K)))
⊢ ∃ g', map (algebraMap R K) g' = g * ↑C (leadingCoeff g)⁻¹
[PROOFSTEP]
have : (algebraMap R _).comp algeq.toAlgHom.toRingHom = (integralClosure R _).toSubring.subtype := by ext x;
  conv_rhs => rw [← algeq.symm_apply_apply x]; rfl
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
algeq : { x // x ∈ integralClosure R K } ≃ₐ[R] R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ (_ : integralClosure R K = ⊥))
    (Algebra.botEquivOfInjective (_ : Function.Injective ↑(algebraMap R K)))
⊢ RingHom.comp (algebraMap R K) ↑↑algeq = Subring.subtype (Subalgebra.toSubring (integralClosure R K))
[PROOFSTEP]
ext x
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
algeq : { x // x ∈ integralClosure R K } ≃ₐ[R] R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ (_ : integralClosure R K = ⊥))
    (Algebra.botEquivOfInjective (_ : Function.Injective ↑(algebraMap R K)))
x : { x // x ∈ integralClosure R K }
⊢ ↑(RingHom.comp (algebraMap R K) ↑↑algeq) x = ↑(Subring.subtype (Subalgebra.toSubring (integralClosure R K))) x
[PROOFSTEP]
conv_rhs => rw [← algeq.symm_apply_apply x]; rfl
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
algeq : { x // x ∈ integralClosure R K } ≃ₐ[R] R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ (_ : integralClosure R K = ⊥))
    (Algebra.botEquivOfInjective (_ : Function.Injective ↑(algebraMap R K)))
x : { x // x ∈ integralClosure R K }
| ↑(Subring.subtype (Subalgebra.toSubring (integralClosure R K))) x
[PROOFSTEP]
rw [← algeq.symm_apply_apply x]; rfl
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
algeq : { x // x ∈ integralClosure R K } ≃ₐ[R] R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ (_ : integralClosure R K = ⊥))
    (Algebra.botEquivOfInjective (_ : Function.Injective ↑(algebraMap R K)))
x : { x // x ∈ integralClosure R K }
| ↑(Subring.subtype (Subalgebra.toSubring (integralClosure R K))) x
[PROOFSTEP]
rw [← algeq.symm_apply_apply x]; rfl
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
algeq : { x // x ∈ integralClosure R K } ≃ₐ[R] R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ (_ : integralClosure R K = ⊥))
    (Algebra.botEquivOfInjective (_ : Function.Injective ↑(algebraMap R K)))
x : { x // x ∈ integralClosure R K }
| ↑(Subring.subtype (Subalgebra.toSubring (integralClosure R K))) x
[PROOFSTEP]
rw [← algeq.symm_apply_apply x]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
algeq : { x // x ∈ integralClosure R K } ≃ₐ[R] R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ (_ : integralClosure R K = ⊥))
    (Algebra.botEquivOfInjective (_ : Function.Injective ↑(algebraMap R K)))
x : { x // x ∈ integralClosure R K }
| ↑(Subring.subtype (Subalgebra.toSubring (integralClosure R K))) (↑(AlgEquiv.symm algeq) (↑algeq x))
[PROOFSTEP]
rfl
[GOAL]
case lem
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
algeq : { x // x ∈ integralClosure R K } ≃ₐ[R] R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ (_ : integralClosure R K = ⊥))
    (Algebra.botEquivOfInjective (_ : Function.Injective ↑(algebraMap R K)))
this : RingHom.comp (algebraMap R K) ↑↑algeq = Subring.subtype (Subalgebra.toSubring (integralClosure R K))
⊢ ∃ g', map (algebraMap R K) g' = g * ↑C (leadingCoeff g)⁻¹
[PROOFSTEP]
have H :=
  (mem_lifts _).1 (integralClosure.mem_lifts_of_monic_of_dvd_map K hf (monic_mul_leadingCoeff_inv g_ne_0) g_mul_dvd)
[GOAL]
case lem
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
algeq : { x // x ∈ integralClosure R K } ≃ₐ[R] R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ (_ : integralClosure R K = ⊥))
    (Algebra.botEquivOfInjective (_ : Function.Injective ↑(algebraMap R K)))
this : RingHom.comp (algebraMap R K) ↑↑algeq = Subring.subtype (Subalgebra.toSubring (integralClosure R K))
H : ∃ q, map (algebraMap { x // x ∈ integralClosure R K } K) q = g * ↑C (leadingCoeff g)⁻¹
⊢ ∃ g', map (algebraMap R K) g' = g * ↑C (leadingCoeff g)⁻¹
[PROOFSTEP]
refine' ⟨map algeq.toAlgHom.toRingHom _, _⟩
[GOAL]
case lem.refine'_1
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
algeq : { x // x ∈ integralClosure R K } ≃ₐ[R] R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ (_ : integralClosure R K = ⊥))
    (Algebra.botEquivOfInjective (_ : Function.Injective ↑(algebraMap R K)))
this : RingHom.comp (algebraMap R K) ↑↑algeq = Subring.subtype (Subalgebra.toSubring (integralClosure R K))
H : ∃ q, map (algebraMap { x // x ∈ integralClosure R K } K) q = g * ↑C (leadingCoeff g)⁻¹
⊢ { x // x ∈ integralClosure R K }[X]
[PROOFSTEP]
use! Classical.choose H
[GOAL]
case lem.refine'_2
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
algeq : { x // x ∈ integralClosure R K } ≃ₐ[R] R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ (_ : integralClosure R K = ⊥))
    (Algebra.botEquivOfInjective (_ : Function.Injective ↑(algebraMap R K)))
this : RingHom.comp (algebraMap R K) ↑↑algeq = Subring.subtype (Subalgebra.toSubring (integralClosure R K))
H : ∃ q, map (algebraMap { x // x ∈ integralClosure R K } K) q = g * ↑C (leadingCoeff g)⁻¹
⊢ map (algebraMap R K) (map (↑↑algeq) (Classical.choose H)) = g * ↑C (leadingCoeff g)⁻¹
[PROOFSTEP]
rw [map_map, this]
[GOAL]
case lem.refine'_2
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : Monic f
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * ↑C (leadingCoeff g)⁻¹ ∣ map (algebraMap R K) f
algeq : { x // x ∈ integralClosure R K } ≃ₐ[R] R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ (_ : integralClosure R K = ⊥))
    (Algebra.botEquivOfInjective (_ : Function.Injective ↑(algebraMap R K)))
this : RingHom.comp (algebraMap R K) ↑↑algeq = Subring.subtype (Subalgebra.toSubring (integralClosure R K))
H : ∃ q, map (algebraMap { x // x ∈ integralClosure R K } K) q = g * ↑C (leadingCoeff g)⁻¹
⊢ map (Subring.subtype (Subalgebra.toSubring (integralClosure R K))) (Classical.choose H) = g * ↑C (leadingCoeff g)⁻¹
[PROOFSTEP]
exact Classical.choose_spec H
[GOAL]
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive f
⊢ IsUnit f ↔ IsUnit (map φ f)
[PROOFSTEP]
refine' ⟨(mapRingHom φ).isUnit_map, fun h => _⟩
[GOAL]
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive f
h : IsUnit (map φ f)
⊢ IsUnit f
[PROOFSTEP]
rcases isUnit_iff.1 h with ⟨_, ⟨u, rfl⟩, hu⟩
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive f
h : IsUnit (map φ f)
u : Sˣ
hu : ↑C ↑u = map φ f
⊢ IsUnit f
[PROOFSTEP]
have hdeg := degree_C u.ne_zero
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive f
h : IsUnit (map φ f)
u : Sˣ
hu : ↑C ↑u = map φ f
hdeg : degree (↑C ↑u) = 0
⊢ IsUnit f
[PROOFSTEP]
rw [hu, degree_map_eq_of_injective hinj] at hdeg
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive f
h : IsUnit (map φ f)
u : Sˣ
hu : ↑C ↑u = map φ f
hdeg : degree f = 0
⊢ IsUnit f
[PROOFSTEP]
rw [eq_C_of_degree_eq_zero hdeg] at hf ⊢
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive (↑C (coeff f 0))
h : IsUnit (map φ f)
u : Sˣ
hu : ↑C ↑u = map φ f
hdeg : degree f = 0
⊢ IsUnit (↑C (coeff f 0))
[PROOFSTEP]
exact isUnit_C.mpr (isPrimitive_iff_isUnit_of_C_dvd.mp hf (f.coeff 0) dvd_rfl)
[GOAL]
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive f
h_irr : Irreducible (map φ f)
⊢ Irreducible f
[PROOFSTEP]
refine'
  ⟨fun h => h_irr.not_unit (IsUnit.map (mapRingHom φ) h), fun a b h =>
    (h_irr.isUnit_or_isUnit <| by rw [h, Polynomial.map_mul]).imp _ _⟩
[GOAL]
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive f
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ map φ f = ?m.200623 a b h * ?m.200624 a b h
[PROOFSTEP]
rw [h, Polynomial.map_mul]
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive f
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit (map φ a) → IsUnit a
case refine'_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive f
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit (map φ b) → IsUnit b
[PROOFSTEP]
all_goals apply ((isPrimitive_of_dvd hf _).isUnit_iff_isUnit_map_of_injective hinj).mpr
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive f
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit (map φ a) → IsUnit a
[PROOFSTEP]
apply ((isPrimitive_of_dvd hf _).isUnit_iff_isUnit_map_of_injective hinj).mpr
[GOAL]
case refine'_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive f
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ IsUnit (map φ b) → IsUnit b
[PROOFSTEP]
apply ((isPrimitive_of_dvd hf _).isUnit_iff_isUnit_map_of_injective hinj).mpr
[GOAL]
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive f
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ a ∣ f
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ↑φ
f : R[X]
hf : IsPrimitive f
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ b ∣ f
[PROOFSTEP]
exacts [Dvd.intro _ h.symm, Dvd.intro_left _ h.symm]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
⊢ Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p)
[PROOFSTEP]
refine'
  ⟨fun hp =>
    irreducible_iff.mpr
      ⟨hp.not_unit.imp h.isPrimitive.isUnit_iff_isUnit_map.mpr, fun a b H => or_iff_not_imp_left.mpr fun hₐ => _⟩,
    fun hp => h.isPrimitive.irreducible_of_irreducible_map_of_injective (IsFractionRing.injective R K) hp⟩
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
⊢ IsUnit b
[PROOFSTEP]
obtain ⟨a', ha⟩ := eq_map_mul_C_of_dvd K h (dvd_of_mul_right_eq b H.symm)
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * ↑C (Polynomial.leadingCoeff a) = a
⊢ IsUnit b
[PROOFSTEP]
obtain ⟨b', hb⟩ := eq_map_mul_C_of_dvd K h (dvd_of_mul_left_eq a H.symm)
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * ↑C (Polynomial.leadingCoeff a) = a
b' : R[X]
hb : Polynomial.map (algebraMap R K) b' * ↑C (Polynomial.leadingCoeff b) = b
⊢ IsUnit b
[PROOFSTEP]
have : a.leadingCoeff * b.leadingCoeff = 1 := by
  rw [← leadingCoeff_mul, ← H, Monic.leadingCoeff (h.map <| algebraMap R K)]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * ↑C (Polynomial.leadingCoeff a) = a
b' : R[X]
hb : Polynomial.map (algebraMap R K) b' * ↑C (Polynomial.leadingCoeff b) = b
⊢ Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
[PROOFSTEP]
rw [← leadingCoeff_mul, ← H, Monic.leadingCoeff (h.map <| algebraMap R K)]
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
H : Polynomial.map (algebraMap R K) p = a * b
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * ↑C (Polynomial.leadingCoeff a) = a
b' : R[X]
hb : Polynomial.map (algebraMap R K) b' * ↑C (Polynomial.leadingCoeff b) = b
this : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ IsUnit b
[PROOFSTEP]
rw [← ha, ← hb, mul_comm _ (C b.leadingCoeff), mul_assoc, ← mul_assoc (C a.leadingCoeff), ← C_mul, this, C_1, one_mul, ←
  Polynomial.map_mul] at H
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * ↑C (Polynomial.leadingCoeff a) = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * ↑C (Polynomial.leadingCoeff b) = b
this : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ IsUnit b
[PROOFSTEP]
rw [← hb, ← Polynomial.coe_mapRingHom]
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * ↑C (Polynomial.leadingCoeff a) = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * ↑C (Polynomial.leadingCoeff b) = b
this : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ IsUnit (↑(mapRingHom (algebraMap R K)) b' * ↑C (Polynomial.leadingCoeff b))
[PROOFSTEP]
refine'
  IsUnit.mul (IsUnit.map _ (Or.resolve_left (hp.isUnit_or_isUnit _) (show ¬IsUnit a' from _)))
    (isUnit_iff_exists_inv'.mpr (Exists.intro (C a.leadingCoeff) <| by rw [← C_mul, this, C_1]))
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * ↑C (Polynomial.leadingCoeff a) = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * ↑C (Polynomial.leadingCoeff b) = b
this : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ ↑C (Polynomial.leadingCoeff a) * ↑C (Polynomial.leadingCoeff b) = 1
[PROOFSTEP]
rw [← C_mul, this, C_1]
[GOAL]
case intro.intro.refine'_1
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * ↑C (Polynomial.leadingCoeff a) = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * ↑C (Polynomial.leadingCoeff b) = b
this : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ p = a' * b'
[PROOFSTEP]
exact Polynomial.map_injective _ (IsFractionRing.injective R K) H
[GOAL]
case intro.intro.refine'_2
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * ↑C (Polynomial.leadingCoeff a) = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * ↑C (Polynomial.leadingCoeff b) = b
this : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
⊢ ¬IsUnit a'
[PROOFSTEP]
by_contra h_contra
[GOAL]
case intro.intro.refine'_2
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * ↑C (Polynomial.leadingCoeff a) = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * ↑C (Polynomial.leadingCoeff b) = b
this : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
h_contra : IsUnit a'
⊢ False
[PROOFSTEP]
refine' hₐ _
[GOAL]
case intro.intro.refine'_2
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * ↑C (Polynomial.leadingCoeff a) = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * ↑C (Polynomial.leadingCoeff b) = b
this : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
h_contra : IsUnit a'
⊢ IsUnit a
[PROOFSTEP]
rw [← ha, ← Polynomial.coe_mapRingHom]
[GOAL]
case intro.intro.refine'_2
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * ↑C (Polynomial.leadingCoeff a) = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * ↑C (Polynomial.leadingCoeff b) = b
this : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
h_contra : IsUnit a'
⊢ IsUnit (↑(mapRingHom (algebraMap R K)) a' * ↑C (Polynomial.leadingCoeff a))
[PROOFSTEP]
exact
  IsUnit.mul (IsUnit.map _ h_contra)
    (isUnit_iff_exists_inv.mpr (Exists.intro (C b.leadingCoeff) <| by rw [← C_mul, this, C_1]))
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p : R[X]
h : Monic p
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * ↑C (Polynomial.leadingCoeff a) = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * ↑C (Polynomial.leadingCoeff b) = b
this : Polynomial.leadingCoeff a * Polynomial.leadingCoeff b = 1
h_contra : IsUnit a'
⊢ ↑C (Polynomial.leadingCoeff a) * ↑C (Polynomial.leadingCoeff b) = 1
[PROOFSTEP]
rw [← C_mul, this, C_1]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
⊢ IsIntegrallyClosed R ↔ ∀ (p : R[X]), Monic p → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
⊢ IsIntegrallyClosed R → ∀ (p : R[X]), Monic p → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))
[PROOFSTEP]
intro hR p hp
[GOAL]
case mp
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
hR : IsIntegrallyClosed R
p : R[X]
hp : Monic p
⊢ Irreducible p ↔ Irreducible (map (algebraMap R K) p)
[PROOFSTEP]
exact Monic.irreducible_iff_irreducible_map_fraction_map hp
[GOAL]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
⊢ (∀ (p : R[X]), Monic p → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))) → IsIntegrallyClosed R
[PROOFSTEP]
intro H
[GOAL]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
H : ∀ (p : R[X]), Monic p → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))
⊢ IsIntegrallyClosed R
[PROOFSTEP]
refine' (isIntegrallyClosed_iff K).mpr fun {x} hx => RingHom.mem_range.mp <| minpoly.mem_range_of_degree_eq_one R x _
[GOAL]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
H : ∀ (p : R[X]), Monic p → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))
x : K
hx : IsIntegral R x
⊢ degree (minpoly R x) = 1
[PROOFSTEP]
rw [← Monic.degree_map (minpoly.monic hx) (algebraMap R K)]
[GOAL]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
H : ∀ (p : R[X]), Monic p → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))
x : K
hx : IsIntegral R x
⊢ degree (map (algebraMap R K) (minpoly R x)) = 1
[PROOFSTEP]
apply degree_eq_one_of_irreducible_of_root ((H _ <| minpoly.monic hx).mp (minpoly.irreducible hx))
[GOAL]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
H : ∀ (p : R[X]), Monic p → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))
x : K
hx : IsIntegral R x
⊢ IsRoot (map (algebraMap R K) (minpoly R x)) ?m.306193
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
H : ∀ (p : R[X]), Monic p → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))
x : K
hx : IsIntegral R x
⊢ K
[PROOFSTEP]
rw [IsRoot, eval_map, ← aeval_def, minpoly.aeval R x]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p q : R[X]
hp : Monic p
hq : Monic q
h : Polynomial.map (algebraMap R K) q ∣ Polynomial.map (algebraMap R K) p
⊢ q ∣ p
[PROOFSTEP]
obtain ⟨r, hr⟩ := h
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p q : R[X]
hp : Monic p
hq : Monic q
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
⊢ q ∣ p
[PROOFSTEP]
obtain ⟨d', hr'⟩ := IsIntegrallyClosed.eq_map_mul_C_of_dvd K hp (dvd_of_mul_left_eq _ hr.symm)
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p q : R[X]
hp : Monic p
hq : Monic q
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' * ↑C (Polynomial.leadingCoeff r) = r
⊢ q ∣ p
[PROOFSTEP]
rw [Monic.leadingCoeff, C_1, mul_one] at hr'
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p q : R[X]
hp : Monic p
hq : Monic q
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' = r
⊢ q ∣ p
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p q : R[X]
hp : Monic p
hq : Monic q
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' * ↑C (Polynomial.leadingCoeff r) = r
⊢ Monic r
[PROOFSTEP]
rw [← hr', ← Polynomial.map_mul] at hr
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p q : R[X]
hp : Monic p
hq : Monic q
r : K[X]
d' : R[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (q * d')
hr' : Polynomial.map (algebraMap R K) d' = r
⊢ q ∣ p
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p q : R[X]
hp : Monic p
hq : Monic q
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' * ↑C (Polynomial.leadingCoeff r) = r
⊢ Monic r
[PROOFSTEP]
exact dvd_of_mul_right_eq _ (Polynomial.map_injective _ (IsFractionRing.injective R K) hr.symm)
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p q : R[X]
hp : Monic p
hq : Monic q
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' * ↑C (Polynomial.leadingCoeff r) = r
⊢ Monic r
[PROOFSTEP]
exact Monic.of_mul_monic_left (hq.map (algebraMap R K)) (by simpa [← hr] using hp.map _)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
p q : R[X]
hp : Monic p
hq : Monic q
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' * ↑C (Polynomial.leadingCoeff r) = r
⊢ Monic (Polynomial.map (algebraMap R K) q * r)
[PROOFSTEP]
simpa [← hr] using hp.map _
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ p))
⊢ IsUnit p
[PROOFSTEP]
rcases isUnit_iff.1 h with ⟨_, ⟨u, rfl⟩, hu⟩
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : ↑C ↑u = primPart (integerNormalization R⁰ p)
⊢ IsUnit p
[PROOFSTEP]
obtain ⟨⟨c, c0⟩, hc⟩ := integerNormalization_map_to_map R⁰ p
[GOAL]
case intro.intro.intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : ↑C ↑u = primPart (integerNormalization R⁰ p)
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = ↑{ val := c, property := c0 } • p
⊢ IsUnit p
[PROOFSTEP]
rw [Subtype.coe_mk, Algebra.smul_def, algebraMap_apply] at hc
[GOAL]
case intro.intro.intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : ↑C ↑u = primPart (integerNormalization R⁰ p)
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = ↑C (↑(algebraMap R K) c) * p
⊢ IsUnit p
[PROOFSTEP]
apply isUnit_of_mul_isUnit_right
[GOAL]
case intro.intro.intro.intro.mk.hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : ↑C ↑u = primPart (integerNormalization R⁰ p)
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = ↑C (↑(algebraMap R K) c) * p
⊢ IsUnit (?intro.intro.intro.intro.mk.x * p)
case intro.intro.intro.intro.mk.x
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : ↑C ↑u = primPart (integerNormalization R⁰ p)
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = ↑C (↑(algebraMap R K) c) * p
⊢ K[X]
[PROOFSTEP]
rw [← hc, (integerNormalization R⁰ p).eq_C_content_mul_primPart, ← hu, ← RingHom.map_mul, isUnit_iff]
[GOAL]
case intro.intro.intro.intro.mk.hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : ↑C ↑u = primPart (integerNormalization R⁰ p)
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = ↑C (↑(algebraMap R K) c) * p
⊢ ∃ r, IsUnit r ∧ ↑C r = map (algebraMap R K) (↑C (content (integerNormalization R⁰ p) * ↑u))
[PROOFSTEP]
refine' ⟨algebraMap R K ((integerNormalization R⁰ p).content * ↑u), isUnit_iff_ne_zero.2 fun con => _, by simp⟩
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : ↑C ↑u = primPart (integerNormalization R⁰ p)
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = ↑C (↑(algebraMap R K) c) * p
⊢ ↑C (↑(algebraMap R K) (content (integerNormalization R⁰ p) * ↑u)) =
    map (algebraMap R K) (↑C (content (integerNormalization R⁰ p) * ↑u))
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro.intro.mk.hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : ↑C ↑u = primPart (integerNormalization R⁰ p)
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = ↑C (↑(algebraMap R K) c) * p
con : ↑(algebraMap R K) (content (integerNormalization R⁰ p) * ↑u) = 0
⊢ False
[PROOFSTEP]
replace con := (injective_iff_map_eq_zero (algebraMap R K)).1 (IsFractionRing.injective _ _) _ con
[GOAL]
case intro.intro.intro.intro.mk.hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : ↑C ↑u = primPart (integerNormalization R⁰ p)
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = ↑C (↑(algebraMap R K) c) * p
con : content (integerNormalization R⁰ p) * ↑u = 0
⊢ False
[PROOFSTEP]
rw [mul_eq_zero, content_eq_zero_iff, IsFractionRing.integerNormalization_eq_zero_iff] at con
[GOAL]
case intro.intro.intro.intro.mk.hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : ↑C ↑u = primPart (integerNormalization R⁰ p)
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = ↑C (↑(algebraMap R K) c) * p
con : p = 0 ∨ ↑u = 0
⊢ False
[PROOFSTEP]
rcases con with (con | con)
[GOAL]
case intro.intro.intro.intro.mk.hu.inl
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : ↑C ↑u = primPart (integerNormalization R⁰ p)
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = ↑C (↑(algebraMap R K) c) * p
con : p = 0
⊢ False
[PROOFSTEP]
apply h0 con
[GOAL]
case intro.intro.intro.intro.mk.hu.inr
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : ↑C ↑u = primPart (integerNormalization R⁰ p)
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = ↑C (↑(algebraMap R K) c) * p
con : ↑u = 0
⊢ False
[PROOFSTEP]
apply Units.ne_zero _ con
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
⊢ Irreducible p ↔ Irreducible (map (algebraMap R K) p)
[PROOFSTEP]
refine'
  ⟨fun hi => ⟨fun h => hi.not_unit (hp.isUnit_iff_isUnit_map.2 h), fun a b hab => _⟩,
    hp.irreducible_of_irreducible_map_of_injective (IsFractionRing.injective R K)⟩
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
obtain ⟨⟨c, c0⟩, hc⟩ := integerNormalization_map_to_map R⁰ a
[GOAL]
case intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑{ val := c, property := c0 } • a
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
obtain ⟨⟨d, d0⟩, hd⟩ := integerNormalization_map_to_map R⁰ b
[GOAL]
case intro.mk.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑{ val := c, property := c0 } • a
d : R
d0 : d ∈ R⁰
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑{ val := d, property := d0 } • b
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
rw [Algebra.smul_def, algebraMap_apply, Subtype.coe_mk] at hc hd
[GOAL]
case intro.mk.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ∈ R⁰
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
rw [mem_nonZeroDivisors_iff_ne_zero] at c0 d0
[GOAL]
case intro.mk.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
have hcd0 : c * d ≠ 0 := mul_ne_zero c0 d0
[GOAL]
case intro.mk.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : c * d ≠ 0
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
rw [Ne.def, ← C_eq_zero] at hcd0
[GOAL]
case intro.mk.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
have h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b :=
  by
  apply map_injective (algebraMap R K) (IsFractionRing.injective _ _) _
  rw [Polynomial.map_mul, Polynomial.map_mul, Polynomial.map_mul, hc, hd, map_C, map_C, hab]
  ring
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
⊢ ↑C c * ↑C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b
[PROOFSTEP]
apply map_injective (algebraMap R K) (IsFractionRing.injective _ _) _
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
⊢ map (algebraMap R K) (↑C c * ↑C d * p) = map (algebraMap R K) (integerNormalization R⁰ a * integerNormalization R⁰ b)
[PROOFSTEP]
rw [Polynomial.map_mul, Polynomial.map_mul, Polynomial.map_mul, hc, hd, map_C, map_C, hab]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
⊢ ↑C (↑(algebraMap R K) c) * ↑C (↑(algebraMap R K) d) * (a * b) =
    ↑C (↑(algebraMap R K) c) * a * (↑C (↑(algebraMap R K) d) * b)
[PROOFSTEP]
ring
[GOAL]
case intro.mk.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
h1 : ↑C c * ↑C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
obtain ⟨u, hu⟩ : Associated (c * d) (content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)) := by
  rw [← dvd_dvd_iff_associated, ← normalize_eq_normalize_iff, normalize.map_mul, normalize.map_mul, normalize_content,
    normalize_content, ← mul_one (normalize c * normalize d), ← hp.content_eq_one, ← content_C, ← content_C, ←
    content_mul, ← content_mul, ← content_mul, h1]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
h1 : ↑C c * ↑C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b
⊢ Associated (c * d) (content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b))
[PROOFSTEP]
rw [← dvd_dvd_iff_associated, ← normalize_eq_normalize_iff, normalize.map_mul, normalize.map_mul, normalize_content,
  normalize_content, ← mul_one (normalize c * normalize d), ← hp.content_eq_one, ← content_C, ← content_C, ←
  content_mul, ← content_mul, ← content_mul, h1]
[GOAL]
case intro.mk.intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
h1 : ↑C c * ↑C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b
u : Rˣ
hu : c * d * ↑u = content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
rw [← RingHom.map_mul, eq_comm, (integerNormalization R⁰ a).eq_C_content_mul_primPart,
  (integerNormalization R⁰ b).eq_C_content_mul_primPart, mul_assoc, mul_comm _ (C _ * _), ← mul_assoc, ← mul_assoc, ←
  RingHom.map_mul, ← hu, RingHom.map_mul, mul_assoc, mul_assoc, ← mul_assoc (C (u : R))] at h1
[GOAL]
case intro.mk.intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
u : Rˣ
h1 : ↑C (c * d) * (↑C ↑u * primPart (integerNormalization R⁰ b) * primPart (integerNormalization R⁰ a)) = ↑C (c * d) * p
hu : c * d * ↑u = content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
have h0 : a ≠ 0 ∧ b ≠ 0 := by
  classical
  rw [Ne.def, Ne.def, ← not_or, ← mul_eq_zero, ← hab]
  intro con
  apply hp.ne_zero (map_injective (algebraMap R K) (IsFractionRing.injective _ _) _)
  simp [con]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
u : Rˣ
h1 : ↑C (c * d) * (↑C ↑u * primPart (integerNormalization R⁰ b) * primPart (integerNormalization R⁰ a)) = ↑C (c * d) * p
hu : c * d * ↑u = content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)
⊢ a ≠ 0 ∧ b ≠ 0
[PROOFSTEP]
classical
rw [Ne.def, Ne.def, ← not_or, ← mul_eq_zero, ← hab]
intro con
apply hp.ne_zero (map_injective (algebraMap R K) (IsFractionRing.injective _ _) _)
simp [con]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
u : Rˣ
h1 : ↑C (c * d) * (↑C ↑u * primPart (integerNormalization R⁰ b) * primPart (integerNormalization R⁰ a)) = ↑C (c * d) * p
hu : c * d * ↑u = content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)
⊢ a ≠ 0 ∧ b ≠ 0
[PROOFSTEP]
rw [Ne.def, Ne.def, ← not_or, ← mul_eq_zero, ← hab]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
u : Rˣ
h1 : ↑C (c * d) * (↑C ↑u * primPart (integerNormalization R⁰ b) * primPart (integerNormalization R⁰ a)) = ↑C (c * d) * p
hu : c * d * ↑u = content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)
⊢ ¬map (algebraMap R K) p = 0
[PROOFSTEP]
intro con
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
u : Rˣ
h1 : ↑C (c * d) * (↑C ↑u * primPart (integerNormalization R⁰ b) * primPart (integerNormalization R⁰ a)) = ↑C (c * d) * p
hu : c * d * ↑u = content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)
con : map (algebraMap R K) p = 0
⊢ False
[PROOFSTEP]
apply hp.ne_zero (map_injective (algebraMap R K) (IsFractionRing.injective _ _) _)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
u : Rˣ
h1 : ↑C (c * d) * (↑C ↑u * primPart (integerNormalization R⁰ b) * primPart (integerNormalization R⁰ a)) = ↑C (c * d) * p
hu : c * d * ↑u = content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)
con : map (algebraMap R K) p = 0
⊢ map (algebraMap R K) p = map (algebraMap R K) 0
[PROOFSTEP]
simp [con]
[GOAL]
case intro.mk.intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
u : Rˣ
h1 : ↑C (c * d) * (↑C ↑u * primPart (integerNormalization R⁰ b) * primPart (integerNormalization R⁰ a)) = ↑C (c * d) * p
hu : c * d * ↑u = content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)
h0 : a ≠ 0 ∧ b ≠ 0
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
rcases hi.isUnit_or_isUnit (mul_left_cancel₀ hcd0 h1).symm with (h | h)
[GOAL]
case intro.mk.intro.mk.intro.inl
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
u : Rˣ
h1 : ↑C (c * d) * (↑C ↑u * primPart (integerNormalization R⁰ b) * primPart (integerNormalization R⁰ a)) = ↑C (c * d) * p
hu : c * d * ↑u = content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)
h0 : a ≠ 0 ∧ b ≠ 0
h : IsUnit (↑C ↑u * primPart (integerNormalization R⁰ b))
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
right
[GOAL]
case intro.mk.intro.mk.intro.inl.h
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
u : Rˣ
h1 : ↑C (c * d) * (↑C ↑u * primPart (integerNormalization R⁰ b) * primPart (integerNormalization R⁰ a)) = ↑C (c * d) * p
hu : c * d * ↑u = content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)
h0 : a ≠ 0 ∧ b ≠ 0
h : IsUnit (↑C ↑u * primPart (integerNormalization R⁰ b))
⊢ IsUnit b
[PROOFSTEP]
apply isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart h0.2 (isUnit_of_mul_isUnit_right h)
[GOAL]
case intro.mk.intro.mk.intro.inr
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
u : Rˣ
h1 : ↑C (c * d) * (↑C ↑u * primPart (integerNormalization R⁰ b) * primPart (integerNormalization R⁰ a)) = ↑C (c * d) * p
hu : c * d * ↑u = content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)
h0 : a ≠ 0 ∧ b ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ a))
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
left
[GOAL]
case intro.mk.intro.mk.intro.inr.h
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : IsPrimitive p
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = ↑C (↑(algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = ↑C (↑(algebraMap R K) d) * b
hcd0 : ¬↑C (c * d) = 0
u : Rˣ
h1 : ↑C (c * d) * (↑C ↑u * primPart (integerNormalization R⁰ b) * primPart (integerNormalization R⁰ a)) = ↑C (c * d) * p
hu : c * d * ↑u = content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)
h0 : a ≠ 0 ∧ b ≠ 0
h : IsUnit (primPart (integerNormalization R⁰ a))
⊢ IsUnit a
[PROOFSTEP]
apply isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart h0.1 h
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
h_dvd : map (algebraMap R K) p ∣ map (algebraMap R K) q
⊢ p ∣ q
[PROOFSTEP]
rcases h_dvd with ⟨r, hr⟩
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
⊢ p ∣ q
[PROOFSTEP]
obtain ⟨⟨s, s0⟩, hs⟩ := integerNormalization_map_to_map R⁰ r
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑{ val := s, property := s0 } • r
⊢ p ∣ q
[PROOFSTEP]
rw [Subtype.coe_mk, Algebra.smul_def, algebraMap_apply] at hs
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
⊢ p ∣ q
[PROOFSTEP]
have h : p ∣ q * C s := by
  use integerNormalization R⁰ r
  apply map_injective (algebraMap R K) (IsFractionRing.injective _ _)
  rw [Polynomial.map_mul, Polynomial.map_mul, hs, hr, mul_assoc, mul_comm r]
  simp
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
⊢ p ∣ q * ↑C s
[PROOFSTEP]
use integerNormalization R⁰ r
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
⊢ q * ↑C s = p * integerNormalization R⁰ r
[PROOFSTEP]
apply map_injective (algebraMap R K) (IsFractionRing.injective _ _)
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
⊢ map (algebraMap R K) (q * ↑C s) = map (algebraMap R K) (p * integerNormalization R⁰ r)
[PROOFSTEP]
rw [Polynomial.map_mul, Polynomial.map_mul, hs, hr, mul_assoc, mul_comm r]
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
⊢ map (algebraMap R K) p * (map (algebraMap R K) (↑C s) * r) = map (algebraMap R K) p * (↑C (↑(algebraMap R K) s) * r)
[PROOFSTEP]
simp
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * ↑C s
⊢ p ∣ q
[PROOFSTEP]
rw [← hp.dvd_primPart_iff_dvd, primPart_mul, hq.primPart_eq, Associated.dvd_iff_dvd_right] at h
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h✝ : p ∣ q * primPart (↑C s)
h : p ∣ ?m.732534
⊢ p ∣ q
[PROOFSTEP]
exact h
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * primPart (↑C s)
⊢ Associated (q * primPart (↑C s)) q
[PROOFSTEP]
symm
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * primPart (↑C s)
⊢ Associated q (q * primPart (↑C s))
[PROOFSTEP]
rcases isUnit_primPart_C s with ⟨u, hu⟩
[GOAL]
case intro.intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * primPart (↑C s)
u : R[X]ˣ
hu : ↑u = primPart (↑C s)
⊢ Associated q (q * primPart (↑C s))
[PROOFSTEP]
use u
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * primPart (↑C s)
u : R[X]ˣ
hu : ↑u = primPart (↑C s)
⊢ q * ↑u = q * primPart (↑C s)
[PROOFSTEP]
rw [hu]
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ primPart (q * ↑C s)
⊢ q * ↑C s ≠ 0
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * ↑C s
⊢ q * ↑C s ≠ 0
[PROOFSTEP]
iterate 2
  apply mul_ne_zero hq.ne_zero
  rw [Ne.def, C_eq_zero]
  contrapose! s0
  simp [s0, mem_nonZeroDivisors_iff_ne_zero]
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ primPart (q * ↑C s)
⊢ q * ↑C s ≠ 0
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * ↑C s
⊢ q * ↑C s ≠ 0
[PROOFSTEP]
apply mul_ne_zero hq.ne_zero
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ primPart (q * ↑C s)
⊢ ↑C s ≠ 0
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * ↑C s
⊢ q * ↑C s ≠ 0
[PROOFSTEP]
rw [Ne.def, C_eq_zero]
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ primPart (q * ↑C s)
⊢ ¬s = 0
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * ↑C s
⊢ q * ↑C s ≠ 0
[PROOFSTEP]
contrapose! s0
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ primPart (q * ↑C s)
s0 : s = 0
⊢ ¬s ∈ R⁰
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * ↑C s
⊢ q * ↑C s ≠ 0
[PROOFSTEP]
simp [s0, mem_nonZeroDivisors_iff_ne_zero]
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * ↑C s
⊢ q * ↑C s ≠ 0
[PROOFSTEP]
apply mul_ne_zero hq.ne_zero
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * ↑C s
⊢ ↑C s ≠ 0
[PROOFSTEP]
rw [Ne.def, C_eq_zero]
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : s ∈ R⁰
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * ↑C s
⊢ ¬s = 0
[PROOFSTEP]
contrapose! s0
[GOAL]
case intro.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
hs : map (algebraMap R K) (integerNormalization R⁰ r) = ↑C (↑(algebraMap R K) s) * r
h : p ∣ q * ↑C s
s0 : s = 0
⊢ ¬s ∈ R⁰
[PROOFSTEP]
simp [s0, mem_nonZeroDivisors_iff_ne_zero]


[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
⊢ Submonoid.map (algebraMap R S) M ≤ IsUnit.submonoid S
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
a : R
ha : a ∈ ↑M
⊢ ↑(algebraMap R S) a ∈ IsUnit.submonoid S
[PROOFSTEP]
exact IsLocalization.map_units S ⟨_, ha⟩
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
⊢ m • ↑(↑(toInvSubmonoid M S) m) = 1
[PROOFSTEP]
convert mul_toInvSubmonoid M S m
[GOAL]
case h.e'_2.h.e
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
⊢ HSMul.hSMul m = HMul.hMul (↑(algebraMap R S) ↑m)
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h.e.h
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
x✝ : S
⊢ m • x✝ = ↑(algebraMap R S) ↑m * x✝
[PROOFSTEP]
rw [← Algebra.smul_def]
[GOAL]
case h.e'_2.h.e.h
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
m : { x // x ∈ M }
x✝ : S
⊢ m • x✝ = ↑m • x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
⊢ ∃ r m, z = r • ↑(↑(toInvSubmonoid M S) m)
[PROOFSTEP]
rcases IsLocalization.surj M z with ⟨⟨r, m⟩, e : z * _ = algebraMap R S r⟩
[GOAL]
case intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
r : R
m : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(r, m).snd = ↑(algebraMap R S) r
⊢ ∃ r m, z = r • ↑(↑(toInvSubmonoid M S) m)
[PROOFSTEP]
refine' ⟨r, m, _⟩
[GOAL]
case intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
r : R
m : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(r, m).snd = ↑(algebraMap R S) r
⊢ z = r • ↑(↑(toInvSubmonoid M S) m)
[PROOFSTEP]
rw [Algebra.smul_def, ← e, mul_assoc]
[GOAL]
case intro.mk
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
z : S
r : R
m : { x // x ∈ M }
e : z * ↑(algebraMap R S) ↑(r, m).snd = ↑(algebraMap R S) r
⊢ z = z * (↑(algebraMap R S) ↑(r, m).snd * ↑(↑(toInvSubmonoid M S) m))
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : { x // x ∈ M }
⊢ ↑(↑(toInvSubmonoid M S) x) = mk' S 1 x
[PROOFSTEP]
rw [← (IsLocalization.map_units S x).mul_left_inj]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : { x // x ∈ M }
⊢ ↑(↑(toInvSubmonoid M S) x) * ↑(algebraMap R S) ↑x = mk' S 1 x * ↑(algebraMap R S) ↑x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : S
⊢ x ∈ invSubmonoid M S ↔ ∃ m, mk' S 1 m = x
[PROOFSTEP]
simp_rw [← toInvSubmonoid_eq_mk']
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : S
⊢ x ∈ invSubmonoid M S ↔ ∃ m, ↑(↑(toInvSubmonoid M S) m) = x
[PROOFSTEP]
exact
  ⟨fun h => ⟨_, congr_arg Subtype.val (toInvSubmonoid_surjective M S ⟨x, h⟩).choose_spec⟩, fun h =>
    h.choose_spec ▸ (toInvSubmonoid M S h.choose).prop⟩
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
⊢ Submodule.span R ↑(invSubmonoid M S) = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
⊢ ⊤ ≤ Submodule.span R ↑(invSubmonoid M S)
[PROOFSTEP]
rintro x -
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : S
⊢ x ∈ Submodule.span R ↑(invSubmonoid M S)
[PROOFSTEP]
rcases IsLocalization.surj'' M x with ⟨r, m, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
r : R
m : { x // x ∈ M }
⊢ r • ↑(↑(toInvSubmonoid M S) m) ∈ Submodule.span R ↑(invSubmonoid M S)
[PROOFSTEP]
exact Submodule.smul_mem _ _ (Submodule.subset_span (toInvSubmonoid M S m).prop)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
⊢ Algebra.FiniteType R S
[PROOFSTEP]
have := Monoid.fg_of_surjective _ (toInvSubmonoid_surjective M S)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
this : Monoid.FG { x // x ∈ invSubmonoid M S }
⊢ Algebra.FiniteType R S
[PROOFSTEP]
rw [Monoid.fg_iff_submonoid_fg] at this
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
this : Submonoid.FG (invSubmonoid M S)
⊢ Algebra.FiniteType R S
[PROOFSTEP]
rcases this with ⟨s, hs⟩
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
⊢ Algebra.FiniteType R S
[PROOFSTEP]
refine' ⟨⟨s, _⟩⟩
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
⊢ Algebra.adjoin R ↑s = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
⊢ ⊤ ≤ Algebra.adjoin R ↑s
[PROOFSTEP]
rintro x -
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ Algebra.adjoin R ↑s
[PROOFSTEP]
change x ∈ (Subalgebra.toSubmodule (Algebra.adjoin R _ : Subalgebra R S) : Set S)
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ ↑(↑Subalgebra.toSubmodule (Algebra.adjoin R ↑s))
[PROOFSTEP]
rw [Algebra.adjoin_eq_span, hs, span_invSubmonoid]
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG { x // x ∈ M }
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ ↑⊤
[PROOFSTEP]
trivial