-- Mathlib/RingTheory/Polynomial/GaussLemma.lean
theorem IsIntegrallyClosed.eq_map_mul_C_of_dvd [IsIntegrallyClosed R] {f : R[X]} (hf : f.Monic)
    {g : K[X]} (hg : g ∣ f.map (algebraMap R K)) :
    ∃ g' : R[X], g'.map (algebraMap R K) * (C <| leadingCoeff g) = g

Proof state:
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✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
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 g.leadingCoeff⁻¹
⊢ map (algebraMap R K) g' * C g.leadingCoeff = g

Tactic:
rw [hg', mul_assoc, ← C_mul, inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
this : (algebraMap R K).comp (↑algeq).toRingHom = (integralClosure R K).toSubring.subtype
⊢ ∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹

Tactic:
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)

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
this : (algebraMap R K).comp (↑algeq).toRingHom = (integralClosure R K).toSubring.subtype
H : ∃ q, map (algebraMap (↥(integralClosure R K)) K) q = g * C g.leadingCoeff⁻¹
⊢ ∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹

Proof state:
case 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✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
this : (algebraMap R K).comp (↑algeq).toRingHom = (integralClosure R K).toSubring.subtype
H : ∃ q, map (algebraMap (↥(integralClosure R K)) K) q = g * C g.leadingCoeff⁻¹
⊢ map (integralClosure R K).toSubring.subtype (Classical.choose H) = g * C g.leadingCoeff⁻¹

Tactic:
exact Classical.choose_spec H

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f

Tactic:
rwa [Associated.dvd_iff_dvd_left (show Associated (g * C g.leadingCoeff⁻¹) g from _)]

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ Associated (g * C g.leadingCoeff⁻¹) g

Proof state:
case 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✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
this : (algebraMap R K).comp (↑algeq).toRingHom = (integralClosure R K).toSubring.subtype
H : ∃ q, map (algebraMap (↥(integralClosure R K)) K) q = g * C g.leadingCoeff⁻¹
⊢ (↥(integralClosure R K))[X]

Tactic:
use! Classical.choose H

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
⊢ (algebraMap R K).comp (↑algeq).toRingHom = (integralClosure R K).toSubring.subtype

Tactic:
ext x

Result:
case a
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
x : ↥(integralClosure R K)
⊢ ((algebraMap R K).comp (↑algeq).toRingHom) x = (integralClosure R K).toSubring.subtype x

Proof state:
case 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✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
this : (algebraMap R K).comp (↑algeq).toRingHom = (integralClosure R K).toSubring.subtype
H : ∃ q, map (algebraMap (↥(integralClosure R K)) K) q = g * C g.leadingCoeff⁻¹
⊢ map (algebraMap R K) (map (↑algeq).toRingHom (Classical.choose H)) = g * C g.leadingCoeff⁻¹

Tactic:
rw [map_map, this]

Result:
case 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✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
this : (algebraMap R K).comp (↑algeq).toRingHom = (integralClosure R K).toSubring.subtype
H : ∃ q, map (algebraMap (↥(integralClosure R K)) K) q = g * C g.leadingCoeff⁻¹
⊢ map (integralClosure R K).toSubring.subtype (Classical.choose H) = g * C g.leadingCoeff⁻¹

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ IsUnit (C g.leadingCoeff⁻¹)

Tactic:
exact isUnit_C.mpr (inv_ne_zero <| leadingCoeff_ne_zero.mpr g_ne_0).isUnit

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
⊢ ∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹

Tactic:
let algeq :=
  (Subalgebra.equivOfEq _ _ <| integralClosure_eq_bot R _).trans
    (Algebra.botEquivOfInjective <| IsFractionRing.injective R <| K)

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
⊢ ∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹