awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
⊢ HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
have h : HMul.hMul (β := K[X]) (HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]))
    ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) =
  g
Tactic: rw [hg', mul_assoc, ← C_mul, inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
h :
  HMul.hMul (β := K[X]) (HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]))
      ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) =
    g
⊢ HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
have h₁ : g *
    HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
      ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) =
  g
Tactic: rw [hg', mul_assoc, ← C_mul, inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
h :
  HMul.hMul (β := K[X]) (HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]))
      ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) =
    g
h₁ :
  g *
      HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
        ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) =
    g
⊢ HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
have h₂ : HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) (g.leadingCoeff⁻¹ * g.leadingCoeff) : K[X]) = g
Tactic: rw [hg', mul_assoc, ← C_mul, inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
h :
  HMul.hMul (β := K[X]) (HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]))
      ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) =
    g
h₁ :
  g *
      HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
        ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) =
    g
h₂ : HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) (g.leadingCoeff⁻¹ * g.leadingCoeff) : K[X]) = g
⊢ HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
have h₃ : g * (C : (a : K) → K[X]) 1 = g
Tactic: rw [hg', mul_assoc, ← C_mul, inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
h :
  HMul.hMul (β := K[X]) (HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]))
      ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) =
    g
h₁ :
  g *
      HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
        ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) =
    g
h₂ : HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) (g.leadingCoeff⁻¹ * g.leadingCoeff) : K[X]) = g
h₃ : g * (C : (a : K) → K[X]) 1 = g
⊢ HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
have h₄ : g * 1 = g
Tactic: rw [hg', mul_assoc, ← C_mul, inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
h :
  HMul.hMul (β := K[X]) (HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]))
      ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) =
    g
h₁ :
  g *
      HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
        ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) =
    g
h₂ : HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) (g.leadingCoeff⁻¹ * g.leadingCoeff) : K[X]) = g
h₃ : g * (C : (a : K) → K[X]) 1 = g
h₄ : g * 1 = g
⊢ HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
have h₅ : g = g
Tactic: rw [hg', mul_assoc, ← C_mul, inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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]),
    HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
have suffices : ∃ (g' : R[X]), map (algebraMap R K) g' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]) ∣ map (algebraMap R K) f
have rwa : Associated (HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])) g
Tactic: rwa [Associated.dvd_iff_dvd_left (show Associated (g * C g.leadingCoeff⁻¹) g from _)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ Associated (HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])) g
have rw : IsUnit (M := K[X]) ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
Tactic: rw [associated_mul_isUnit_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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]), map (algebraMap R K) g' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
have g_mul_dvd : HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]) ∣ map (algebraMap R K) f
Tactic: 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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 : HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]) ∣ map (algebraMap R K) f
algeq : AlgEquiv.{u_1, u_2, u_1} R (↥(integralClosure R K)) R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ ⋯) (Algebra.botEquivOfInjective ⋯)
⊢ Eq (α := ↥(integralClosure R K) →+* K)
    (RingHom.comp (algebraMap R K) (↑algeq : ↥(integralClosure R K) →ₐ[R] R).toRingHom)
    (Subring.subtype (Subalgebra.toSubring (integralClosure R K)))
have a : ∀ (x : ↥(integralClosure R K)),
  Eq (α := K)
    ((RingHom.comp (algebraMap R K) (↑algeq : ↥(integralClosure R K) →ₐ[R] R).toRingHom :
          (a : ↥(integralClosure R K)) → K)
        x :
      K)
    (((Subring.subtype (Subalgebra.toSubring (integralClosure R K)) :
            ↥(Subalgebra.toSubring (integralClosure R K)) →+* K) :
          (a : ↥(integralClosure R K)) → K)
        x :
      K)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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 : HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]) ∣ map (algebraMap R K) f
algeq : AlgEquiv.{u_1, u_2, u_1} R (↥(integralClosure R K)) R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ ⋯) (Algebra.botEquivOfInjective ⋯)
x : ↥(integralClosure R K)
| (((Subring.subtype (Subalgebra.toSubring (integralClosure R K)) :
          ↥(Subalgebra.toSubring (integralClosure R K)) →+* K) :
        (a : ↥(integralClosure R K)) → K)
      x :
    K)
have rw : (((Subring.subtype (Subalgebra.toSubring (integralClosure R K)) : ↥(Subalgebra.toSubring (integralClosure R K)) →+* K) :
      (a : ↥(integralClosure R K)) → K)
    ((algeq.symm : (a : R) → ↥(integralClosure R K)) ((algeq : (a : ↥(integralClosure R K)) → R) x) :
      ↥(integralClosure R K)) :
  K)
Tactic: rw [← algeq.symm_apply_apply x]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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 : HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]) ∣ map (algebraMap R K) f
algeq : AlgEquiv.{u_1, u_2, u_1} R (↥(integralClosure R K)) R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ ⋯) (Algebra.botEquivOfInjective ⋯)
x : ↥(integralClosure R K)
⊢ Eq (α := K)
    ((RingHom.comp (algebraMap R K) (↑algeq : ↥(integralClosure R K) →ₐ[R] R).toRingHom :
          (a : ↥(integralClosure R K)) → K)
        x :
      K)
    (((Subring.subtype (Subalgebra.toSubring (integralClosure R K)) :
            ↥(Subalgebra.toSubring (integralClosure R K)) →+* K) :
          (a : ↥(integralClosure R K)) → K)
        x :
      K)
have a : Eq (α := K)
  ((RingHom.comp (algebraMap R K) (↑algeq : ↥(integralClosure R K) →ₐ[R] R).toRingHom :
        (a : ↥(integralClosure R K)) → K)
      x :
    K)
  (((Subring.subtype (Subalgebra.toSubring (integralClosure R K)) :
          ↥(Subalgebra.toSubring (integralClosure R K)) →+* K) :
        (a : ↥(integralClosure R K)) → K)
      ((algeq.symm : (a : R) → ↥(integralClosure R K)) ((algeq : (a : ↥(integralClosure R K)) → R) x) :
        ↥(integralClosure R K)) :
    K)
Tactic: conv_rhs => rw [← algeq.symm_apply_apply x]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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 : HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]) ∣ map (algebraMap R K) f
algeq : AlgEquiv.{u_1, u_2, u_1} R (↥(integralClosure R K)) R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ ⋯) (Algebra.botEquivOfInjective ⋯)
⊢ ∃ (g' : R[X]), map (algebraMap R K) g' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
have this : Eq (α := ↥(integralClosure R K) →+* K)
  (RingHom.comp (algebraMap R K) (↑algeq : ↥(integralClosure R K) →ₐ[R] R).toRingHom)
  (Subring.subtype (Subalgebra.toSubring (integralClosure R K)))
Tactic: have :
    (algebraMap R _).comp algeq.toAlgHom.toRingHom = (integralClosure R _).toSubring.subtype := by
    ext x; (conv_rhs => rw [← algeq.symm_apply_apply x]); rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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 : HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]) ∣ map (algebraMap R K) f
algeq : AlgEquiv.{u_1, u_2, u_1} R (↥(integralClosure R K)) R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ ⋯) (Algebra.botEquivOfInjective ⋯)
this :
  Eq (α := ↥(integralClosure R K) →+* K)
    (RingHom.comp (algebraMap R K) (↑algeq : ↥(integralClosure R K) →ₐ[R] R).toRingHom)
    (Subring.subtype (Subalgebra.toSubring (integralClosure R K)))
⊢ ∃ (g' : R[X]), map (algebraMap R K) g' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
have H : ∃ (q : (↥(integralClosure R K))[X]),
  map (algebraMap (↥(integralClosure R K)) K) q = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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 : HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]) ∣ map (algebraMap R K) f
algeq : AlgEquiv.{u_1, u_2, u_1} R (↥(integralClosure R K)) R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ ⋯) (Algebra.botEquivOfInjective ⋯)
this :
  Eq (α := ↥(integralClosure R K) →+* K)
    (RingHom.comp (algebraMap R K) (↑algeq : ↥(integralClosure R K) →ₐ[R] R).toRingHom)
    (Subring.subtype (Subalgebra.toSubring (integralClosure R K)))
H :
  ∃ (q : (↥(integralClosure R K))[X]),
    map (algebraMap (↥(integralClosure R K)) K) q =
      HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
⊢ ∃ (g' : R[X]), map (algebraMap R K) g' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
have refine_1 : (↥(integralClosure R K))[X]
Tactic: refine ⟨map algeq.toAlgHom.toRingHom ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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 : HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]) ∣ map (algebraMap R K) f
algeq : AlgEquiv.{u_1, u_2, u_1} R (↥(integralClosure R K)) R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ ⋯) (Algebra.botEquivOfInjective ⋯)
this :
  Eq (α := ↥(integralClosure R K) →+* K)
    (RingHom.comp (algebraMap R K) (↑algeq : ↥(integralClosure R K) →ₐ[R] R).toRingHom)
    (Subring.subtype (Subalgebra.toSubring (integralClosure R K)))
H :
  ∃ (q : (↥(integralClosure R K))[X]),
    map (algebraMap (↥(integralClosure R K)) K) q =
      HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
refine_1 : (↥(integralClosure R K))[X]
⊢ ∃ (g' : R[X]), map (algebraMap R K) g' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
have refine_2 : map (algebraMap R K)
    (map (↑algeq : ↥(integralClosure R K) →ₐ[R] R).toRingHom
      (Classical.choose (p := fun (x : (↥(integralClosure R K))[X]) ↦
        map (algebraMap (↥(integralClosure R K)) K) x =
          HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]))
        H)) =
  HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
Tactic: refine ⟨map algeq.toAlgHom.toRingHom ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : 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 : HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]) ∣ map (algebraMap R K) f
algeq : AlgEquiv.{u_1, u_2, u_1} R (↥(integralClosure R K)) R :=
  AlgEquiv.trans (Subalgebra.equivOfEq (integralClosure R K) ⊥ ⋯) (Algebra.botEquivOfInjective ⋯)
this :
  Eq (α := ↥(integralClosure R K) →+* K)
    (RingHom.comp (algebraMap R K) (↑algeq : ↥(integralClosure R K) →ₐ[R] R).toRingHom)
    (Subring.subtype (Subalgebra.toSubring (integralClosure R K)))
H :
  ∃ (q : (↥(integralClosure R K))[X]),
    map (algebraMap (↥(integralClosure R K)) K) q =
      HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
⊢ map (algebraMap R K)
      (map (↑algeq : ↥(integralClosure R K) →ₐ[R] R).toRingHom
        (Classical.choose (p := fun (x : (↥(integralClosure R K))[X]) ↦
          map (algebraMap (↥(integralClosure R K)) K) x =
            HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]))
          H)) =
    HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
have refine_2 : map (Subring.subtype (Subalgebra.toSubring (integralClosure R K)))
    (Classical.choose (p := fun (x : (↥(integralClosure R K))[X]) ↦
      map (algebraMap (↥(integralClosure R K)) K) x =
        HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]))
      H) =
  HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
Tactic: rw [map_map, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
hf : f.IsPrimitive
⊢ IsUnit f ↔ IsUnit (map φ f)
have refine : ∀ (h : IsUnit (map φ f)), IsUnit f
Tactic: refine ⟨(mapRingHom φ).isUnit_map, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
hf : f.IsPrimitive
h : IsUnit (map φ f)
⊢ IsUnit f
have rcases : ∀ (u : Sˣ) (hu : (C : (a : S) → S[X]) (↑u : S) = map φ f), IsUnit f
Tactic: rcases isUnit_iff.1 h with ⟨_, ⟨u, rfl⟩, hu⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
hf : f.IsPrimitive
h : IsUnit (map φ f)
u : Sˣ
hu : (C : (a : S) → S[X]) (↑u : S) = map φ f
⊢ IsUnit f
have hdeg : degree.{u_2} (R := S) ((C : (a : S) → S[X]) (↑u : S)) = 0
Tactic: have hdeg := degree_C u.ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
hf : f.IsPrimitive
h : IsUnit (map φ f)
u : Sˣ
hu : (C : (a : S) → S[X]) (↑u : S) = map φ f
hdeg : degree.{u_2} (R := S) ((C : (a : S) → S[X]) (↑u : S)) = 0
⊢ IsUnit f
have hdeg₁ : f.degree = 0
Tactic: rw [hu, degree_map_eq_of_injective hinj] at hdeg
Cleared hypotheses: hdeg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
hf : f.IsPrimitive
h : IsUnit (map φ f)
u : Sˣ
hu : (C : (a : S) → S[X]) (↑u : S) = map φ f
hdeg : f.degree = 0
⊢ IsUnit f
have rw : ∀ (hf : IsPrimitive.{u_1} (R := R) ((C : (a : R) → R[X]) (f.coeff 0))) (h : IsUnit (map φ f)) (u : Sˣ)
  (hu : (C : (a : S) → S[X]) (↑u : S) = map φ f) (hdeg : f.degree = 0),
  IsUnit (M := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
Tactic: rw [eq_C_of_degree_eq_zero hdeg] at hf ⊢
Cleared hypotheses: hf, h, u, hu, hdeg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
⊢ map φ f = map φ a * map φ b
have rw : map φ (a * b) = map φ a * map φ b
Tactic: rw [h, Polynomial.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
rw : map φ (a * b) = map φ a * map φ b
⊢ map φ f = map φ a * map φ b
have rw₁ : map φ a * map φ b = map φ a * map φ b
Tactic: rw [h, Polynomial.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
⊢ Irreducible f
have refine_1 : ∀ (a b : R[X]) (h : f = a * b), IsUnit (map φ a) → IsUnit a
Tactic: refine
    ⟨fun h => h_irr.not_isUnit (IsUnit.map (mapRingHom φ) h), fun a b h =>
      (h_irr.isUnit_or_isUnit <| by rw [h, Polynomial.map_mul]).imp ?_ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
hinj : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
f : R[X]
hf : f.IsPrimitive
h_irr : Irreducible (map φ f)
refine_1 : ∀ (a b : R[X]) (h : f = a * b), IsUnit (map φ a) → IsUnit a
⊢ Irreducible f
have refine_2 : ∀ (a b : R[X]) (h : f = a * b), IsUnit (map φ b) → IsUnit b
Tactic: refine
    ⟨fun h => h_irr.not_isUnit (IsUnit.map (mapRingHom φ) h), fun a b h =>
      (h_irr.isUnit_or_isUnit <| by rw [h, Polynomial.map_mul]).imp ?_ ?_⟩