awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
inst_3 : IsDomain S
inst_4 : DecidableEq S
y : S
hy : Eq.{u_1 + 1} (α := S) ((aeval y : (a : R[X]) → S) (minpoly R x) : S) (0 : S)
hy₁ : eval₂ (RingHom.comp (RingHom.id S) (algebraMap R S)) y (minpoly R x) = 0
⊢ eval y (minpolyDiv R x) =
    if x = y then (aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) (minpoly R x) : R[X]) else 0

Tactic:
rw [eval, eval₂_minpolyDiv_of_eval₂_eq_zero, RingHom.id_apply, RingHom.id_apply]

Premises used: Polynomial.eval, eval₂_minpolyDiv_of_eval₂_eq_zero, RingHom.id_apply
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
inst_3 : IsDomain S
inst_4 : DecidableEq S
y : S
hy : Eq.{u_1 + 1} (α := S) ((aeval y : (a : R[X]) → S) (minpoly R x) : S) (0 : S)
⊢ eval₂ (RingHom.comp (RingHom.id S) (algebraMap R S)) y (minpoly R x) = 0

Tactic:
simpa [aeval_def] using hy

Premises used: Polynomial.aeval_def
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
by_contra : ∀ (H : coeff (minpolyDiv R x) i ∉ R[x]), False
⊢ Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) i)

Tactic:
by_contra H
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H : coeff (minpolyDiv R x) i ∉ R[x]
⊢ coeff (minpolyDiv R x) (i + 0) ∉ R[x]

Tactic:
H

Premises used: Set.Mem
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H : coeff (minpolyDiv R x) i ∉ R[x]
⊢ coeff (minpolyDiv R x) (i + 0) ∉ R[x]

Tactic:
exact H
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H_1 : coeff (minpolyDiv R x) i ∉ R[x]
j : ℕ
IH : coeff (minpolyDiv R x) (i + j) ∉ R[x]
H : Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) (i + (j + 1)))
succ : Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) (i + j))
⊢ False

Tactic:
apply IH
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H_1 : coeff (minpolyDiv R x) i ∉ R[x]
j : ℕ
IH : coeff (minpolyDiv R x) (i + j) ∉ R[x]
H : Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) (i + (j + 1)))
succ :
  Membership.mem (γ := Subalgebra R S) R[x]
    (HAdd.hAdd (α := S) ((algebraMap R S : (a : R) → S) (coeff (minpoly R x) (i + j + 1)) : S)
      (coeff (minpolyDiv R x) (i + j + 1) * x))
⊢ Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) (i + j))

Tactic:
rw [coeff_minpolyDiv]

Premises used: coeff_minpolyDiv
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H_1 : coeff (minpolyDiv R x) i ∉ R[x]
j : ℕ
IH : coeff (minpolyDiv R x) (i + j) ∉ R[x]
H : Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) (i + (j + 1)))
⊢ Membership.mem (γ := Subalgebra R S) R[x]
    (HAdd.hAdd (α := S) ((algebraMap R S : (a : R) → S) (coeff (minpoly R x) (i + j + 1)) : S)
      (coeff (minpolyDiv R x) (i + j + 1) * x))

Tactic:
add_mem ?_ (mul_mem H (self_mem_adjoin_singleton R x))

Premises used: AddMemClass.add_mem, Algebra.self_mem_adjoin_singleton, MulMemClass.mul_mem
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H_1 : coeff (minpolyDiv R x) i ∉ R[x]
j : ℕ
IH : coeff (minpolyDiv R x) (i + j) ∉ R[x]
H : Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) (i + (j + 1)))
succ :
  Membership.mem (α := S) (γ := Subalgebra R S) R[x]
    ((algebraMap R S : (a : R) → S) (coeff (minpoly R x) (i + j + 1)) : S)
⊢ Membership.mem (γ := Subalgebra R S) R[x]
    (HAdd.hAdd (α := S) ((algebraMap R S : (a : R) → S) (coeff (minpoly R x) (i + j + 1)) : S)
      (coeff (minpolyDiv R x) (i + j + 1) * x))

Tactic:
refine add_mem ?_ (mul_mem H (self_mem_adjoin_singleton R x))

Premises used: AddMemClass.add_mem, Algebra.self_mem_adjoin_singleton, MulMemClass.mul_mem
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H_1 : coeff (minpolyDiv R x) i ∉ R[x]
j : ℕ
IH : coeff (minpolyDiv R x) (i + j) ∉ R[x]
H : Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) (i + (j + 1)))
⊢ Membership.mem (α := S) (γ := Subalgebra R S) R[x]
    ((algebraMap R S : (a : R) → S) (coeff (minpoly R x) (i + j + 1)) : S)

Tactic:
Subalgebra.algebraMap_mem _ _

Premises used: Subalgebra.algebraMap_mem
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H_1 : coeff (minpolyDiv R x) i ∉ R[x]
j : ℕ
IH : coeff (minpolyDiv R x) (i + j) ∉ R[x]
H : Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) (i + (j + 1)))
⊢ Membership.mem (α := S) (γ := Subalgebra R S) R[x]
    ((algebraMap R S : (a : R) → S) (coeff (minpoly R x) (i + j + 1)) : S)

Tactic:
exact Subalgebra.algebraMap_mem _ _

Premises used: Subalgebra.algebraMap_mem
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H : coeff (minpolyDiv R x) i ∉ R[x]
⊢ ∀ (j : ℕ), coeff (minpolyDiv R x) (i + j) ∉ R[x]

Tactic:
have : ∀ j, coeff (minpolyDiv R x) (i + j) ∉ R[x] := by
    intro j; induction j with
    | zero => exact H
    | succ j IH =>
      intro H; apply IH
      rw [coeff_minpolyDiv]
      refine add_mem ?_ (mul_mem H (self_mem_adjoin_singleton R x))
      exact Subalgebra.algebraMap_mem _ _
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H : coeff (minpolyDiv R x) i ∉ R[x]
this : ∀ (j : ℕ), coeff (minpolyDiv R x) (i + j) ∉ R[x]
apply : Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) (i + (natDegree (minpolyDiv R x) + 1)))
⊢ False

Tactic:
apply this (natDegree (minpolyDiv R x) + 1)

Premises used: HAdd.hAdd, minpolyDiv, Polynomial.natDegree, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H : coeff (minpolyDiv R x) i ∉ R[x]
this : ∀ (j : ℕ), coeff (minpolyDiv R x) (i + j) ∉ R[x]
rw : Membership.mem (γ := Subalgebra R S) R[x] 0
rw₁ : natDegree (minpolyDiv R x) < i + (natDegree (minpolyDiv R x) + 1)
⊢ Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) (i + (natDegree (minpolyDiv R x) + 1)))

Tactic:
rw [coeff_eq_zero_of_natDegree_lt]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H : coeff (minpolyDiv R x) i ∉ R[x]
this : ∀ (j : ℕ), coeff (minpolyDiv R x) (i + j) ∉ R[x]
⊢ Membership.mem (γ := Subalgebra R S) R[x] 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H : coeff (minpolyDiv R x) i ∉ R[x]
this : ∀ (j : ℕ), coeff (minpolyDiv R x) (i + j) ∉ R[x]
⊢ Membership.mem (γ := Subalgebra R S) R[x] 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
H : coeff (minpolyDiv R x) i ∉ R[x]
this : ∀ (j : ℕ), coeff (minpolyDiv R x) (i + j) ∉ R[x]
⊢ natDegree (minpolyDiv R x) < i + (natDegree (minpolyDiv R x) + 1)

Tactic:
lia
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
inst_3 : Nontrivial S
e : Eq (α := S[X]) (minpolyDiv R x) 0
⊢ minpolyDiv R x * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    map (algebraMap R S) (minpoly R x)

Tactic:
have := minpolyDiv_spec R x
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
inst_3 : Nontrivial S
e : Eq (α := S[X]) (minpolyDiv R x) 0
this :
  minpolyDiv R x * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    map (algebraMap R S) (minpoly R x)
⊢ Eq (α := S[X]) 0 (map (algebraMap R S) (minpoly R x))

Tactic:
rw [e, zero_mul] at this

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
inst_3 : Nontrivial S
e : Eq (α := S[X]) (minpolyDiv R x) 0
this : Eq (α := S[X]) 0 (map (algebraMap R S) (minpoly R x))
⊢ False

Tactic:
((minpoly.monic hx).map (algebraMap R S)).ne_zero this.symm

Premises used: minpoly.monic, Algebra.algebraMap, Polynomial.Monic.map, Eq.symm, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
inst_3 : Nontrivial S
e : Eq (α := S[X]) (minpolyDiv R x) 0
this : Eq (α := S[X]) 0 (map (algebraMap R S) (minpoly R x))
⊢ False

Tactic:
exact ((minpoly.monic hx).map (algebraMap R S)).ne_zero this.symm

Premises used: minpoly.monic, Algebra.algebraMap, Polynomial.Monic.map, Eq.symm, Polynomial.Monic.ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
⊢ Nontrivial S

Tactic:
nontriviality S
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
h : Nontrivial S
⊢ (minpolyDiv R x * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).leadingCoeff =
    leadingCoeff (map (algebraMap R S) (minpoly R x))

Tactic:
have := congr_arg leadingCoeff (minpolyDiv_spec R x)
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
h : Nontrivial S
this :
  (minpolyDiv R x * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).leadingCoeff =
    leadingCoeff (map (algebraMap R S) (minpoly R x))
rw :
  ∀
    (this :
      leadingCoeff (minpolyDiv R x) *
          (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).leadingCoeff =
        1),
    Monic (minpolyDiv R x)
rw₁ :
  leadingCoeff (minpolyDiv R x) * (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).leadingCoeff ≠ 0
⊢ Monic (minpolyDiv R x)

Tactic:
rw [leadingCoeff_mul', ((minpoly.monic hx).map (algebraMap R S)).leadingCoeff] at this

Premises used: minpoly.monic, Algebra.algebraMap, Polynomial.leadingCoeff_mul', Polynomial.Monic.leadingCoeff, Polynomial.Monic.map
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
h : Nontrivial S
this :
  leadingCoeff (minpolyDiv R x) * (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).leadingCoeff = 1
⊢ Monic (minpolyDiv R x)

Tactic:
simpa using this
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
h : Nontrivial S
this :
  (minpolyDiv R x * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).leadingCoeff =
    leadingCoeff (map (algebraMap R S) (minpoly R x))
⊢ leadingCoeff (minpolyDiv R x) * (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).leadingCoeff ≠ 0

Tactic:
simpa using minpolyDiv_ne_zero hx

Premises used: minpolyDiv_ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
inst_3 : Nontrivial S
rw :
  natDegree (minpolyDiv R x) + 1 =
    natDegree (minpolyDiv R x) + (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).natDegree
rw₁ :
  leadingCoeff (minpolyDiv R x) * (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).leadingCoeff ≠ 0
⊢ natDegree (minpolyDiv R x) + 1 = natDegree (minpoly R x)

Tactic:
rw [← (minpoly.monic hx).natDegree_map (algebraMap R S), ← minpolyDiv_spec, natDegree_mul']

Premises used: minpoly.monic, Algebra.algebraMap, Polynomial.natDegree_mul', Polynomial.Monic.natDegree_map, minpolyDiv_spec
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
inst_3 : Nontrivial S
⊢ natDegree (minpolyDiv R x) + 1 =
    natDegree (minpolyDiv R x) + (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).natDegree

Tactic:
simp
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
inst_3 : Nontrivial S
⊢ leadingCoeff (minpolyDiv R x) * (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).leadingCoeff ≠ 0

Tactic:
simpa using minpolyDiv_ne_zero hx

Premises used: minpolyDiv_ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
inst_3 : Nontrivial S
rw : natDegree (minpolyDiv R x) < natDegree (minpolyDiv R x) + 1
⊢ natDegree (minpolyDiv R x) < natDegree (minpoly R x)

Tactic:
rw [← natDegree_minpolyDiv_succ hx]

Premises used: natDegree_minpolyDiv_succ
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
inst_3 : Nontrivial S
⊢ natDegree (minpolyDiv R x) < natDegree (minpolyDiv R x) + 1

Tactic:
Nat.lt_succ_self _

Premises used: Nat.lt_succ_self
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
inst_3 : Nontrivial S
⊢ natDegree (minpolyDiv R x) < natDegree (minpolyDiv R x) + 1

Tactic:
exact Nat.lt_succ_self _

Premises used: Nat.lt_succ_self
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_1
K : Type u_3
S : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : CommRing S
inst_3 : Algebra R S
x : S
hx : IsIntegral R x
inst_4 : IsDomain R
inst_5 : IsIntegrallyClosed R
inst_6 : IsDomain S
inst_7 : Algebra R K
inst_8 : Algebra K S
inst_9 : IsScalarTower R K S
inst_10 : IsFractionRing R K
rw :
  map (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K S) (algebraMap R K)) (minpoly R x) /ₘ
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    map (algebraMap K S) (minpoly K x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])
rw₁ :
  map (algebraMap K S) (map (algebraMap R K) (minpoly R x)) /ₘ
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    map (algebraMap K S) (minpoly K x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])
rw₂ rw₃ :
  map (algebraMap K S) (minpoly K x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    map (algebraMap K S) (minpoly K x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])
⊢ map (algebraMap R S) (minpoly R x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) =
    map (algebraMap K S) (minpoly K x) /ₘ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])

Tactic:
rw [IsScalarTower.algebraMap_eq R K S, ← map_map,
    ← minpoly.isIntegrallyClosed_eq_field_fractions' _ hx]

Premises used: IsScalarTower.algebraMap_eq, Polynomial.map_map, minpoly.isIntegrallyClosed_eq_field_fractions'
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
hi : 0 ≤ natDegree (minpolyDiv R x)
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio 0))
    (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - 0) - HPow.hPow (β := ℕ) x 0)

Tactic:
simp [(minpolyDiv_monic hx).leadingCoeff]

Premises used: Polynomial.Monic.leadingCoeff, minpolyDiv_monic
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  ∀ (hi : i ≤ natDegree (minpolyDiv R x)),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio i))
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i)
hi : i + 1 ≤ natDegree (minpolyDiv R x)
succ :
  Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)))
    (HSMul.hSMul (β := S) (coeff (minpoly R x) (natDegree (minpolyDiv R x) - (i + 1) + 1)) 1 +
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - (i + 1) + 1) - x ^ i) * x)
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)))
    (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - (i + 1)) - x ^ (i + 1))

Tactic:
rw [coeff_minpolyDiv, add_sub_assoc, pow_succ, ← sub_mul, Algebra.algebraMap_eq_smul_one]

Premises used: add_sub_assoc, pow_succ, Algebra.algebraMap_eq_smul_one, sub_mul, coeff_minpolyDiv
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  ∀ (hi : i ≤ natDegree (minpolyDiv R x)),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio i))
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i)
hi : i + 1 ≤ natDegree (minpolyDiv R x)
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)))
    (HSMul.hSMul (β := S) (coeff (minpoly R x) (natDegree (minpolyDiv R x) - (i + 1) + 1)) 1 +
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - (i + 1) + 1) - x ^ i) * x)

Tactic:
add_mem ?_ ?_

Premises used: AddMemClass.add_mem
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  ∀ (hi : i ≤ natDegree (minpolyDiv R x)),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio i))
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i)
hi : i + 1 ≤ natDegree (minpolyDiv R x)
succ :
  Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)))
    (HSMul.hSMul (β := S) (coeff (minpoly R x) (natDegree (minpolyDiv R x) - (i + 1) + 1)) 1)
succ₁ :
  Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)))
    ((coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - (i + 1) + 1) - x ^ i) * x)
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)))
    (HSMul.hSMul (β := S) (coeff (minpoly R x) (natDegree (minpolyDiv R x) - (i + 1) + 1)) 1 +
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - (i + 1) + 1) - x ^ i) * x)

Tactic:
refine add_mem ?_ ?_

Premises used: AddMemClass.add_mem
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  ∀ (hi : i ≤ natDegree (minpolyDiv R x)),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio i))
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i)
hi : i + 1 ≤ natDegree (minpolyDiv R x)
succ : Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1))) 1
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)))
    (HSMul.hSMul (β := S) (coeff (minpoly R x) (natDegree (minpolyDiv R x) - (i + 1) + 1)) 1)

Tactic:
apply Submodule.smul_mem

Premises used: Submodule.smul_mem
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  ∀ (hi : i ≤ natDegree (minpolyDiv R x)),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio i))
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i)
hi : i + 1 ≤ natDegree (minpolyDiv R x)
succ : Membership.mem (γ := Set S) ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)) 1
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1))) 1

Tactic:
apply Submodule.subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  ∀ (hi : i ≤ natDegree (minpolyDiv R x)),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio i))
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i)
hi : i + 1 ≤ natDegree (minpolyDiv R x)
⊢ Membership.mem (γ := Set S) ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)) 1

Tactic:
⟨0, Nat.zero_lt_succ _, pow_zero _⟩

Premises used: Set.Mem, Nat.zero_lt_succ, setOf, pow_zero, And.intro, Exists.intro, Set.image, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  ∀ (hi : i ≤ natDegree (minpolyDiv R x)),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio i))
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i)
hi : i + 1 ≤ natDegree (minpolyDiv R x)
⊢ Membership.mem (γ := Set S) ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)) 1

Tactic:
exact ⟨0, Nat.zero_lt_succ _, pow_zero _⟩
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  ∀ (hi : i ≤ natDegree (minpolyDiv R x)),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio i))
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i)
hi : i + 1 ≤ natDegree (minpolyDiv R x)
succ :
  Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)))
    ((coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i) * x)
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)))
    ((coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - (i + 1) + 1) - x ^ i) * x)

Tactic:
rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left (b := 1) hi)]

Premises used: le_tsub_of_add_le_left, tsub_add_cancel_of_le, tsub_tsub