awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
rw : IsUnit (M := K[X]) ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
⊢ Associated (HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])) g

Tactic:
rw [associated_mul_isUnit_left_iff]

Premises used: associated_mul_isUnit_left_iff
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
⊢ IsUnit (M := K[X]) ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])

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

Premises used: Iff.mpr, Ne.isUnit, Polynomial.isUnit_C, Polynomial.leadingCoeff_ne_zero, inv_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
⊢ IsUnit (M := K[X]) ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])

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

Premises used: Iff.mpr, Ne.isUnit, Polynomial.isUnit_C, Polynomial.leadingCoeff_ne_zero, inv_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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

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
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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 ⋯)
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)
⊢ 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:
ext x
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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)
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)
| (((Subring.subtype (Subalgebra.toSubring (integralClosure R K)) :
          ↥(Subalgebra.toSubring (integralClosure R K)) →+* K) :
        (a : ↥(integralClosure R K)) → K)
      x :
    K)

Tactic:
rw [← algeq.symm_apply_apply x]

Premises used: AlgEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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)
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)
⊢ 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:
conv_rhs => rw [← algeq.symm_apply_apply x]

Premises used: AlgEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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)
        ((algeq.symm : (a : R) → ↥(integralClosure R K)) ((algeq : (a : ↥(integralClosure R K)) → R) x) :
          ↥(integralClosure R K)) :
      K)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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)))

Tactic:
have :
    (algebraMap R _).comp algeq.toAlgHom.toRingHom = (integralClosure R _).toSubring.subtype := by
    ext x; (conv_rhs => rw [← algeq.symm_apply_apply x]); rfl
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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)))
⊢ ∃ (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)
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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])

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

Premises used: AlgEquiv.toAlgHom, AlgHom.toRingHom, Exists.intro, Polynomial.map
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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]
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])
⊢ ∃ (g' : R[X]), map (algebraMap R K) g' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])

Tactic:
refine ⟨map algeq.toAlgHom.toRingHom ?_, ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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])
⊢ (↥(integralClosure R K))[X]

Tactic:
use! Classical.choose H

Premises used: Classical.choose
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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_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])
⊢ 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:
rw [map_map, this]

Premises used: Polynomial.map_map
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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 (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:
Classical.choose_spec H

Premises used: Set.Mem, Subring.subtype, Classical.choose_spec
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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 (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:
exact Classical.choose_spec H

Premises used: Classical.choose_spec
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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)

Tactic:
⟨(mapRingHom φ).isUnit_map, fun h => ?_⟩

Premises used: Polynomial.mapRingHom, Iff.intro, RingHom.isUnit_map
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
refine : ∀ (h : IsUnit (map φ f)), IsUnit f
⊢ IsUnit f ↔ IsUnit (map φ f)

Tactic:
refine ⟨(mapRingHom φ).isUnit_map, fun h => ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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)
rcases : ∀ (u : Sˣ) (hu : (C : (a : S) → S[X]) (↑u : S) = map φ f), IsUnit f
⊢ IsUnit f

Tactic:
rcases isUnit_iff.1 h with ⟨_, ⟨u, rfl⟩, hu⟩

Premises used: Polynomial.isUnit_iff, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
⊢ degree.{u_2} (R := S) ((C : (a : S) → S[X]) (↑u : S)) = 0

Tactic:
have hdeg := degree_C u.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
⊢ f.degree = 0

Tactic:
rw [hu, degree_map_eq_of_injective hinj] at hdeg

Premises used: Polynomial.degree_map_eq_of_injective
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
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])
⊢ IsUnit f

Tactic:
rw [eq_C_of_degree_eq_zero hdeg] at hf ⊢

Premises used: Polynomial.eq_C_of_degree_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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 : 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:
isUnit_C.mpr (isPrimitive_iff_isUnit_of_C_dvd.mp hf (f.coeff 0) dvd_rfl)

Premises used: Iff.mpr, Polynomial.isPrimitive_iff_isUnit_of_C_dvd, Polynomial.isUnit_C, Polynomial.coeff, Iff.mp, dvd_rfl, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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 : 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:
exact isUnit_C.mpr (isPrimitive_iff_isUnit_of_C_dvd.mp hf (f.coeff 0) dvd_rfl)

Premises used: Iff.mpr, Polynomial.isPrimitive_iff_isUnit_of_C_dvd, Polynomial.isUnit_C, Polynomial.coeff, Iff.mp, dvd_rfl, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
rw₁ rw₂ : map φ a * map φ b = map φ a * map φ b
⊢ map φ f = map φ a * map φ b

Tactic:
rw [h, Polynomial.map_mul]

Premises used: Polynomial.map_mul
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
refine_2 : ∀ (a b : R[X]) (h : f = a * b), IsUnit (map φ b) → IsUnit b
⊢ Irreducible f

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 ?_ ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
apply : a ∣ f
⊢ IsUnit (map φ a) → IsUnit a

Tactic:
apply ((isPrimitive_of_dvd hf _).isUnit_iff_isUnit_map_of_injective hinj).mpr

Premises used: Iff.mpr, Polynomial.IsPrimitive.isUnit_iff_isUnit_map_of_injective, Polynomial.isPrimitive_of_dvd
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
apply : b ∣ f
⊢ IsUnit (map φ b) → IsUnit b

Tactic:
apply ((isPrimitive_of_dvd hf _).isUnit_iff_isUnit_map_of_injective hinj).mpr

Premises used: Iff.mpr, Polynomial.IsPrimitive.isUnit_iff_isUnit_map_of_injective, Polynomial.isPrimitive_of_dvd
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
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
⊢ a ∣ f

Tactic:
Dvd.intro _ h.symm

Premises used: Dvd.intro, Eq.symm