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

Tactic:
rw [associated_mul_isUnit_left_iff]

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
⊢ IsUnit (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
lem : ∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹
⊢ ∃ g', map (algebraMap R K) g' * C g.leadingCoeff = g

Tactic:
obtain ⟨g', hg'⟩ := lem

Result:
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✝ : 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⁻¹
⊢ ∃ g', map (algebraMap R K) g' * C g.leadingCoeff = g

Proof state:
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✝ : 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⁻¹
⊢ ∃ g', map (algebraMap R K) g' * C g.leadingCoeff = g

Tactic:
use g'

Result:
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

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
H : ∃ q, map (algebraMap (↥(integralClosure R K)) K) q = g * C g.leadingCoeff⁻¹
⊢ ∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹

Tactic:
refine ⟨map algeq.toAlgHom.toRingHom ?_, ?_⟩

Result:
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]

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 ?refine_1) = 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
⊢ ∃ g', map (algebraMap R K) g' * C g.leadingCoeff = g

Tactic:
suffices lem : ∃ g' : R[X], g'.map (algebraMap R K) = g * C g.leadingCoeff⁻¹ by
  obtain ⟨g', hg'⟩ := lem
  use g'
  rw [hg', mul_assoc, ← C_mul, inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]

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', map (algebraMap R K) g' = 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
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⁻¹

Tactic:
have :
  (algebraMap R _).comp algeq.toAlgHom.toRingHom = (integralClosure R _).toSubring.subtype := by
  ext x; (conv_rhs => rw [← algeq.symm_apply_apply x]); rfl

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
⊢ ∃ g', map (algebraMap R K) g' = 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', map (algebraMap R K) g' * C g.leadingCoeff = g

Tactic:
have g_ne_0 : g ≠ 0 := ne_zero_of_dvd_ne_zero (Monic.ne_zero <| hf.map (algebraMap R K)) hg

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', map (algebraMap R K) g' * C g.leadingCoeff = g

Proof state:
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 (algeq.symm (algeq x))

Tactic:
rfl

Result:
no goals