awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (Q.coeff (j + 1 + k) • f (k + P.natDegree - 1))
hintsum :
  IsIntegral R
    (z * B.gen ^ (P.natDegree - (j + 2)) -
      HAdd.hAdd (α := L) (∑ x ∈ (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + x) • f (x + P.natDegree - 1))
        (∑ x ∈ range (j + 1), g x • B.gen ^ x * B.gen ^ (P.natDegree - (j + 2))))
r : R
hQ :
  Eq.{v + 1} (α := K)
    ((algebraMap R K : (a : R) → K)
        (Q.coeff (j + 1) ^ B.dim *
          (HPow.hPow (α := R) (-1) B.dim * coeff (minpoly R B.gen) 0) ^ (j + 1 + (P.natDegree - (j + 2)))) :
      K)
    ((algebraMap R K : (a : R) → K) (p ^ B.dim * r) : K)
hr :
  Eq.{v + 1} (α := K) ((algebraMap R K : (a : R) → K) r : K)
    ((Algebra.norm K : (a : L) → K)
        (z * B.gen ^ (P.natDegree - (j + 2)) -
          HAdd.hAdd (α := L) (∑ x ∈ (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + x) • f (x + P.natDegree - 1))
            (∑ x ∈ range (j + 1), g x • B.gen ^ x * B.gen ^ (P.natDegree - (j + 2)))) :
      K)
⊢ p ^ B.dim ∣ p ^ B.dim * r

Tactic:
have hppdiv : p ^ B.dim ∣ p ^ B.dim * r := dvd_mul_of_dvd_left dvd_rfl _
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (HPow.hPow (β := ℕ) p 0 • z)
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z

Tactic:
simpa using hz
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
n : ℕ
hn : ∀ (hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p ^ n • z)), Membership.mem (γ := Subalgebra R L) R[B.gen] z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p ^ (n + 1) • z)
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] (p • p ^ n • z)

Tactic:
rw [_root_.pow_succ', mul_smul] at hz

Premises used: SemigroupAction.mul_smul, pow_succ'
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
n : ℕ
hn : ∀ (hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p ^ n • z)), Membership.mem (γ := Subalgebra R L) R[B.gen] z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p • p ^ n • z)
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z

Tactic:
hn (mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt hp hBint (hzint.smul _) hz hei)

Premises used: IsIntegral.smul, mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
n : ℕ
hn : ∀ (hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p ^ n • z)), Membership.mem (γ := Subalgebra R L) R[B.gen] z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p • p ^ n • z)
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z

Tactic:
exact
      hn (mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt hp hBint (hzint.smul _) hz hei)

Premises used: IsIntegral.smul, mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
n : ℕ
z : L
hzint : IsIntegral R z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p ^ n • z)
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
zero :
  ∀ (hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (HPow.hPow (β := ℕ) p 0 • z)),
    Membership.mem (γ := Subalgebra R L) R[B.gen] z
succ :
  ∀ (n : ℕ)
    (hn :
      ∀ (hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p ^ n • z)),
        Membership.mem (γ := Subalgebra R L) R[B.gen] z)
    (hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p ^ (n + 1) • z)),
    Membership.mem (γ := Subalgebra R L) R[B.gen] z
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z

Tactic:
induction n with
  | zero => simpa using hz
  | succ n hn =>
    rw [_root_.pow_succ', mul_smul] at hz
    exact
      hn (mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt hp hBint (hzint.smul _) hz hei)

Premises used: Nat.zero, Nat.succ, SemigroupAction.mul_smul, pow_succ'
-- 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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
refine_2 :
  ∀
    (this :
      Membership.mem (γ := Subsemiring g.SplittingField[X])
        (lifts (R := ↥(integralClosure R g.SplittingField))
          (algebraMap (↥(integralClosure R g.SplittingField)) g.SplittingField))
        (map (algebraMap K g.SplittingField) g)),
    Membership.mem (γ := Subsemiring K[X]) (lifts (R := ↥(integralClosure R K)) (algebraMap (↥(integralClosure R K)) K))
      g
refine_1 :
  ∀ (a : g.SplittingField)
    (ha : Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) g)) a),
    Membership.mem (γ := Multiset g.SplittingField) (f.aroots g.SplittingField) a
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ↥(integralClosure R K)) (algebraMap (↥(integralClosure R K)) K)) g

Tactic:
have := (SplittingField.splits g).mem_lift_of_roots_mem_range (hg.map _)
    (algebraMap (integralClosure R g.SplittingField) g.SplittingField)
     fun a ha =>
      (SetLike.ext_iff.mp (integralClosure R g.SplittingField).range_algebraMap _).mpr <|
        roots_mem_integralClosure hf ?_
-- 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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  Membership.mem (γ := Subsemiring g.SplittingField[X])
    (lifts (R := ↥(integralClosure R g.SplittingField))
      (algebraMap (↥(integralClosure R g.SplittingField)) g.SplittingField))
    (map (algebraMap K g.SplittingField) g)
⊢ ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)

Tactic:
rw [lifts_iff_coeff_lifts, ← RingHom.coe_range, Subalgebra.range_algebraMap] at this

Premises used: Polynomial.lifts_iff_coeff_lifts, Subalgebra.range_algebraMap, RingHom.coe_range
-- 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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ↥(integralClosure R K)) (algebraMap (↥(integralClosure R K)) K)) g

Tactic:
(lifts_iff_coeff_lifts _).2 fun n => ?_

Premises used: Iff.mpr, Polynomial.lifts_iff_coeff_lifts
-- 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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
refine_2 :
  ∀ (n : ℕ),
    Membership.mem (γ := Set K)
      (Set.range (ι := ↥(integralClosure R K))
        (⇑(algebraMap (↥(integralClosure R K)) K) : (a : ↥(integralClosure R K)) → K))
      (g.coeff n)
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ↥(integralClosure R K)) (algebraMap (↥(integralClosure R K)) K)) g

Tactic:
refine (lifts_iff_coeff_lifts _).2 fun n => ?_

Premises used: Iff.mpr, Polynomial.lifts_iff_coeff_lifts
-- 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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
n : ℕ
refine_2 : g.coeff n ∈ (↑(Subalgebra.toSubring (integralClosure R K)) : Set K)
⊢ Membership.mem (γ := Set K)
    (Set.range (ι := ↥(integralClosure R K))
      (⇑(algebraMap (↥(integralClosure R K)) K) : (a : ↥(integralClosure R K)) → K))
    (g.coeff n)

Tactic:
rw [← RingHom.coe_range, Subalgebra.range_algebraMap]

Premises used: Subalgebra.range_algebraMap, RingHom.coe_range
-- 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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
n : ℕ
refine_2 :
  ∀ (p : R[X]) (hp : p.Monic)
    (he :
      Eq (α := g.SplittingField)
        (eval₂ (algebraMap R g.SplittingField) (coeff (map (algebraMap K g.SplittingField) g) n) p) 0),
    g.coeff n ∈ (↑(Subalgebra.toSubring (integralClosure R K)) : Set K)
⊢ g.coeff n ∈ (↑(Subalgebra.toSubring (integralClosure R K)) : Set K)

Tactic:
obtain ⟨p, hp, he⟩ := SetLike.mem_coe.mp (this n)

Premises used: SetLike.mem_coe, Iff.mp
-- 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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
n : ℕ
p : R[X]
hp : p.Monic
he :
  Eq (α := g.SplittingField) (eval₂ (algebraMap R g.SplittingField) (coeff (map (algebraMap K g.SplittingField) g) n) p)
    0
right : eval₂ (algebraMap R K) (g.coeff n) p = 0
⊢ g.coeff n ∈ (↑(Subalgebra.toSubring (integralClosure R K)) : Set K)

Tactic:
use p, hp
-- 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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
n : ℕ
p : R[X]
hp : p.Monic
he :
  Eq (α := g.SplittingField) (eval₂ (algebraMap R g.SplittingField) (coeff (map (algebraMap K g.SplittingField) g) n) p)
    0
⊢ Eq (α := g.SplittingField)
    ((algebraMap K g.SplittingField : (a : K) → g.SplittingField) (eval (g.coeff n) (map (algebraMap R K) p)) :
      g.SplittingField)
    (0 : g.SplittingField)

Tactic:
rw [IsScalarTower.algebraMap_eq R K, coeff_map, ← eval₂_map, eval₂_at_apply] at he

Premises used: Polynomial.coeff_map, Polynomial.eval₂_map, IsScalarTower.algebraMap_eq, Polynomial.eval₂_at_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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
n : ℕ
p : R[X]
hp : p.Monic
he :
  Eq (α := g.SplittingField)
    ((algebraMap K g.SplittingField : (a : K) → g.SplittingField) (eval (g.coeff n) (map (algebraMap R K) p)) :
      g.SplittingField)
    (0 : g.SplittingField)
right : eval (g.coeff n) (map (algebraMap R K) p) = 0
⊢ eval₂ (algebraMap R K) (g.coeff n) p = 0

Tactic:
rw [eval₂_eq_eval_map]

Premises used: Polynomial.eval₂_eq_eval_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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
n : ℕ
p : R[X]
hp : p.Monic
he :
  Eq (α := g.SplittingField)
    ((algebraMap K g.SplittingField : (a : K) → g.SplittingField) (eval (g.coeff n) (map (algebraMap R K) p)) :
      g.SplittingField)
    (0 : g.SplittingField)
apply :
  Function.Injective (α := K) (β := g.SplittingField) (⇑(algebraMap K g.SplittingField) : (a : K) → g.SplittingField)
⊢ eval (g.coeff n) (map (algebraMap R K) p) = 0

Tactic:
apply (injective_iff_map_eq_zero _).1 _ _ he

Premises used: injective_iff_map_eq_zero, Iff.mp
-- 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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  ∀ (n : ℕ),
    coeff (map (algebraMap K g.SplittingField) g) n ∈
      (↑(Subalgebra.toSubring (integralClosure R g.SplittingField)) : Set g.SplittingField)
n : ℕ
p : R[X]
hp : p.Monic
he :
  Eq (α := g.SplittingField)
    ((algebraMap K g.SplittingField : (a : K) → g.SplittingField) (eval (g.coeff n) (map (algebraMap R K) p)) :
      g.SplittingField)
    (0 : g.SplittingField)
⊢ Function.Injective (α := K) (β := g.SplittingField) (⇑(algebraMap K g.SplittingField) : (a : K) → g.SplittingField)

Tactic:
apply RingHom.injective

Premises used: RingHom.injective
-- 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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
a : g.SplittingField
ha : Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) g)) a
refine_1 :
  Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) (map (algebraMap R K) f)))
    a
⊢ Membership.mem (γ := Multiset g.SplittingField) (f.aroots g.SplittingField) a

Tactic:
rw [aroots_def, IsScalarTower.algebraMap_eq R K _, ← map_map]

Premises used: IsScalarTower.algebraMap_eq, Polynomial.map_map, Polynomial.aroots_def
-- 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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
a : g.SplittingField
ha : Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) g)) a
⊢ Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) (map (algebraMap R K) f)))
    a

Tactic:
Multiset.mem_of_le (roots.le_of_dvd ((hf.map _).map _).ne_zero ?_) ha

Premises used: Multiset.mem_of_le, Polynomial.roots.le_of_dvd, Polynomial.Monic.map, Polynomial.Monic.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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
a : g.SplittingField
ha : Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) g)) a
refine_1 :
  Dvd.dvd (α := g.SplittingField[X]) (map (algebraMap K g.SplittingField) g)
    (map (algebraMap K g.SplittingField) (map (algebraMap R K) f))
⊢ Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) (map (algebraMap R K) f)))
    a

Tactic:
refine Multiset.mem_of_le (roots.le_of_dvd ((hf.map _).map _).ne_zero ?_) ha

Premises used: Multiset.mem_of_le, Polynomial.roots.le_of_dvd, Polynomial.Monic.map, Polynomial.Monic.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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
a : g.SplittingField
ha : Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) g)) a
⊢ Dvd.dvd (α := g.SplittingField[X]) (map (algebraMap K g.SplittingField) g)
    (map (algebraMap K g.SplittingField) (map (algebraMap R K) f))

Tactic:
map_dvd (algebraMap K g.SplittingField) hd

Premises used: Algebra.algebraMap, Polynomial.map_dvd, Polynomial.SplittingField
-- 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
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
a : g.SplittingField
ha : Membership.mem (γ := Multiset g.SplittingField) (roots (map (algebraMap K g.SplittingField) g)) a
⊢ Dvd.dvd (α := g.SplittingField[X]) (map (algebraMap K g.SplittingField) g)
    (map (algebraMap K g.SplittingField) (map (algebraMap R K) f))

Tactic:
exact map_dvd (algebraMap K g.SplittingField) hd

Premises used: Algebra.algebraMap, Polynomial.map_dvd, Polynomial.SplittingField
-- 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 ≠ 0

Tactic:
have g_ne_0 : g ≠ 0 := ne_zero_of_dvd_ne_zero (Monic.ne_zero <| hf.map (algebraMap R K)) hg
-- 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
lem : ∃ (g' : R[X]), map (algebraMap R K) g' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
obtain :
  ∀ (g' : R[X])
    (hg' : map (algebraMap R K) g' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])),
    ∃ (g' : R[X]),
      HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
⊢ ∃ (g' : R[X]),
    HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g

Tactic:
obtain ⟨g', hg'⟩ := lem
-- 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' : 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]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g
⊢ ∃ (g' : R[X]),
    HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = g

Tactic:
use g'
-- 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' : 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
h₅ h₆ : g = g
⊢ HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((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]

Premises used: Iff.mpr, Polynomial.C_1, mul_assoc, Polynomial.leadingCoeff_ne_zero, Polynomial.C_mul, mul_one, inv_mul_cancel₀
-- 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
suffices :
  ∃ (g' : R[X]), map (algebraMap R K) g' = HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])
⊢ ∃ (g' : R[X]),
    HMul.hMul (α := K[X]) (β := K[X]) (map (algebraMap R K) g') ((C : (a : K) → K[X]) g.leadingCoeff : K[X]) = 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]
-- 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
rwa : Associated (HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X])) g
⊢ HMul.hMul (β := K[X]) g ((C : (a : K) → K[X]) g.leadingCoeff⁻¹ : K[X]) ∣ map (algebraMap R K) f

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

Premises used: Associated.dvd_iff_dvd_left