awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsDomain T
inst_6 : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
hy : eval₂ (algebraMap R T) ((σ₂ : (a : S) → T) x) (minpoly R x) = 0
hy₁ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₂ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
hy₂ : eval₂ (↑σ₂ : S →+* T) ((σ₂ : (a : S) → T) x) (map (algebraMap R S) (minpoly R x)) = 0
hy₃ : eval₂ (↑σ₂ : S →+* T) (((↑σ₂ : S →+* T) : (a : S) → T) x) (map (algebraMap R S) (minpoly R x)) = 0
hy₄ : Eq.{u_1 + 1} (α := T) (((↑σ₂ : S →+* T) : (a : S) → T) (eval x (map (algebraMap R S) (minpoly R x))) : T) (0 : T)
hy₅ : Eq.{u_1 + 1} (α := T) (((↑σ₂ : S →+* T) : (a : S) → T) ((aeval x : (a : R[X]) → S) (minpoly R x) : S) : T) (0 : T)
⊢ eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₁ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
have hy₆ : Eq.{u_1 + 1} (α := T) (((↑σ₂ : S →+* T) : (a : S) → T) 0 : T) (0 : T)
Tactic: rw [AlgHom.comp_algebraMap, ← σ₂.comp_algebraMap, ← eval₂_map, ← RingHom.coe_coe, eval₂_hom,
    eval_map_algebraMap, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : IsDomain T
inst_6 : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
hy : eval₂ (algebraMap R T) ((σ₂ : (a : S) → T) x) (minpoly R x) = 0
hy₁ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₂ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
hy₂ : eval₂ (↑σ₂ : S →+* T) ((σ₂ : (a : S) → T) x) (map (algebraMap R S) (minpoly R x)) = 0
hy₃ : eval₂ (↑σ₂ : S →+* T) (((↑σ₂ : S →+* T) : (a : S) → T) x) (map (algebraMap R S) (minpoly R x)) = 0
hy₄ : Eq.{u_1 + 1} (α := T) (((↑σ₂ : S →+* T) : (a : S) → T) (eval x (map (algebraMap R S) (minpoly R x))) : T) (0 : T)
hy₅ : Eq.{u_1 + 1} (α := T) (((↑σ₂ : S →+* T) : (a : S) → T) ((aeval x : (a : R[X]) → S) (minpoly R x) : S) : T) (0 : T)
hy₆ : Eq.{u_1 + 1} (α := T) (((↑σ₂ : S →+* T) : (a : S) → T) 0 : T) (0 : T)
⊢ eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ₁ : S →+* T) (algebraMap R S)) ((σ₂ : (a : S) → T) x)
      (minpoly R x) =
    0
have hy₇ : Eq.{u_1 + 1} (α := T) 0 0
Tactic: rw [AlgHom.comp_algebraMap, ← σ₂.comp_algebraMap, ← eval₂_map, ← RingHom.coe_coe, eval₂_hom,
    eval_map_algebraMap, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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 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
have hy₁ : eval₂ (RingHom.comp (RingHom.id S) (algebraMap R S)) y (minpoly R x) = 0
Tactic: rw [eval, eval₂_minpolyDiv_of_eval₂_eq_zero, RingHom.id_apply, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
i : ℕ
⊢ Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) i)
have by_contra : ∀ (H : coeff (minpolyDiv R x) i ∉ R[x]), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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)))
⊢ False
have succ : Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) (i + j))
Tactic: apply IH
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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] (coeff (minpolyDiv R x) (i + j))
have 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))
Tactic: rw [coeff_minpolyDiv]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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))
have succ : Membership.mem (α := S) (γ := Subalgebra R S) R[x]
  ((algebraMap R S : (a : R) → S) (coeff (minpoly R x) (i + j + 1)) : S)
Tactic: refine add_mem ?_ (mul_mem H (self_mem_adjoin_singleton R x))
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (hypothesis)
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]
⊢ False
have this : ∀ (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 _ _
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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]
⊢ False
have apply : Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) (i + (natDegree (minpolyDiv R x) + 1)))
Tactic: apply this (natDegree (minpolyDiv R x) + 1)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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] (coeff (minpolyDiv R x) (i + (natDegree (minpolyDiv R x) + 1)))
have rw : Membership.mem (γ := Subalgebra R S) R[x] 0
Tactic: rw [coeff_eq_zero_of_natDegree_lt]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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
⊢ Membership.mem (γ := Subalgebra R S) R[x] (coeff (minpolyDiv R x) (i + (natDegree (minpolyDiv R x) + 1)))
have rw₁ : natDegree (minpolyDiv R x) < i + (natDegree (minpolyDiv R x) + 1)
Tactic: rw [coeff_eq_zero_of_natDegree_lt]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (hypothesis)
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
⊢ False
have 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)
Tactic: have := minpolyDiv_spec R x
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (hypothesis)
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)
⊢ False
have this₁ : Eq (α := S[X]) 0 (map (algebraMap R S) (minpoly R x))
Tactic: rw [e, zero_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (hypothesis)
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
⊢ Monic (minpolyDiv R x)
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (hypothesis)
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
⊢ Monic (minpolyDiv R x)
have 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))
Tactic: have := congr_arg leadingCoeff (minpolyDiv_spec R x)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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))
⊢ Monic (minpolyDiv R x)
have 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)
Tactic: rw [leadingCoeff_mul', ((minpoly.monic hx).map (algebraMap R S)).leadingCoeff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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)
⊢ Monic (minpolyDiv R x)
have rw₁ : leadingCoeff (minpolyDiv R x) * (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).leadingCoeff ≠ 0
Tactic: rw [leadingCoeff_mul', ((minpoly.monic hx).map (algebraMap R S)).leadingCoeff] at this
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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 (minpoly R x)
have 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
Tactic: rw [← (minpoly.monic hx).natDegree_map (algebraMap R S), ← minpolyDiv_spec, natDegree_mul']
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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
⊢ natDegree (minpolyDiv R x) + 1 = natDegree (minpoly R x)
have rw₁ : leadingCoeff (minpolyDiv R x) * (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])).leadingCoeff ≠ 0
Tactic: rw [← (minpoly.monic hx).natDegree_map (algebraMap R S), ← minpolyDiv_spec, natDegree_mul']
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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 (minpoly R x)
have rw : natDegree (minpolyDiv R x) < natDegree (minpolyDiv R x) + 1
Tactic: rw [← natDegree_minpolyDiv_succ hx]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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
⊢ 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])
have 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])
Tactic: rw [IsScalarTower.algebraMap_eq R K S, ← map_map,
    ← minpoly.isIntegrallyClosed_eq_field_fractions' _ hx]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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])
⊢ 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])
have 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])
Tactic: rw [IsScalarTower.algebraMap_eq R K S, ← map_map,
    ← minpoly.isIntegrallyClosed_eq_field_fractions' _ hx]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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])
⊢ 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])
have 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])
Tactic: rw [IsScalarTower.algebraMap_eq R K S, ← map_map,
    ← minpoly.isIntegrallyClosed_eq_field_fractions' _ hx]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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)))
    (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - (i + 1)) - x ^ (i + 1))
have 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)
Tactic: rw [coeff_minpolyDiv, add_sub_assoc, pow_succ, ← sub_mul, Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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)
have 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)
Tactic: refine add_mem ?_ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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)
⊢ 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)
have 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)
Tactic: refine add_mem ?_ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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)
have succ : Membership.mem (γ := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1))) 1
Tactic: apply Submodule.smul_mem
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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))) 1
have succ : Membership.mem (γ := Set S) ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)) 1
Tactic: apply Submodule.subset_span
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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)))
    ((coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - (i + 1) + 1) - x ^ i) * x)
have 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)
Tactic: rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left (b := 1) hi)]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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)))
    ((coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i) * x)
have apply : HMul.hMul (α := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio i)) (R ∙ x) ≤
  Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1))
Tactic: apply SetLike.le_def.mp ?_
        (Submodule.mul_mem_mul (IH ((Nat.le_succ _).trans hi))
          (Submodule.mem_span_singleton_self x))
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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)
⊢ HMul.hMul (α := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio i)) (R ∙ x) ≤
    Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1))
have rw : LE.le.{u_1} (α := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1 * x) '' Set.Iio i))
  (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)))
Tactic: rw [Submodule.span_mul_span, Set.mul_singleton, Set.image_image]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
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)
⊢ LE.le.{u_1} (α := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1 * x) '' Set.Iio i))
    (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)))
have h : Subset.{u_1} (α := Set S) ((fun (x_1 : ℕ) ↦ x ^ x_1 * x) '' Set.Iio i) ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1))
Tactic: apply Submodule.span_mono