awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
j : ℕ
hj : j ∈ Set.Iio i
⊢ Membership.mem (γ := Set S) ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)) ((fun (x_1 : ℕ) ↦ x ^ x_1 * x) j)
have hj₁ : j < i
Tactic: rw [Set.mem_Iio] at hj
Cleared hypotheses: hj
-- 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 : ℕ
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)
have zero : ∀ (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: induction i with
  | zero => simp [(minpolyDiv_monic hx).leadingCoeff]
  | succ i IH =>
    rw [coeff_minpolyDiv, add_sub_assoc, pow_succ, ← sub_mul, Algebra.algebraMap_eq_smul_one]
    refine add_mem ?_ ?_
    · apply Submodule.smul_mem
      apply Submodule.subset_span
      exact ⟨0, Nat.zero_lt_succ _, pow_zero _⟩
    · rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left (b := 1) hi)]
      apply SetLike.le_def.mp ?_
        (Submodule.mul_mem_mul (IH ((Nat.le_succ _).trans hi))
          (Submodule.mem_span_singleton_self x))
      rw [Submodule.span_mul_span, Set.mul_singleton, Set.image_image]
      apply Submodule.span_mono
      rintro _ ⟨j, hj, rfl⟩
      rw [Set.mem_Iio] at hj
      exact ⟨j + 1, Nat.add_lt_of_lt_sub hj, pow_succ x j⟩
Cleared hypotheses: i, 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 : ℕ
hi : i ≤ natDegree (minpolyDiv R x)
zero :
  ∀ (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)
⊢ 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)
have succ : ∀ (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))
Tactic: induction i with
  | zero => simp [(minpolyDiv_monic hx).leadingCoeff]
  | succ i IH =>
    rw [coeff_minpolyDiv, add_sub_assoc, pow_succ, ← sub_mul, Algebra.algebraMap_eq_smul_one]
    refine add_mem ?_ ?_
    · apply Submodule.smul_mem
      apply Submodule.subset_span
      exact ⟨0, Nat.zero_lt_succ _, pow_zero _⟩
    · rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left (b := 1) hi)]
      apply SetLike.le_def.mp ?_
        (Submodule.mul_mem_mul (IH ((Nat.le_succ _).trans hi))
          (Submodule.mem_span_singleton_self x))
      rw [Submodule.span_mul_span, Set.mul_singleton, Set.image_image]
      apply Submodule.span_mono
      rintro _ ⟨j, hj, rfl⟩
      rw [Set.mem_Iio] at hj
      exact ⟨j + 1, Nat.add_lt_of_lt_sub hj, pow_succ x j⟩
Cleared hypotheses: i, hi
-- 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
⊢ Eq (α := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x])
have a : Nontrivial S
Tactic: nontriviality S
-- 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
⊢ Eq (α := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x])
have a : LE.le (α := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
  ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x])
Tactic: apply le_antisymm
-- 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
a :
  LE.le (α := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x])
⊢ Eq (α := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x])
have a₁ : LE.le (α := Submodule R S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x] : Submodule R S)
  (Submodule.span R (Set.range (coeff (minpolyDiv R x))) : Submodule R S)
Tactic: apply le_antisymm
-- 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
⊢ LE.le (α := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x])
have a : Set.range (coeff (minpolyDiv R x)) ⊆
  (↑((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x] : Submodule R S) : Set S)
Tactic: rw [Submodule.span_le]
-- 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
⊢ LE.le (α := Submodule R S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x] : Submodule R S)
    (Submodule.span R (Set.range (coeff (minpolyDiv R x))) : Submodule R S)
have a : (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly R x)))) : Set S) ⊆
  (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)
Tactic: rw [← Submodule.span_range_natDegree_eq_adjoin (minpoly.monic hx) (minpoly.aeval _ _),
      Submodule.span_le]
-- 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
⊢ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly R x)))) : Set S) ⊆
    (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)
have a : Set.Iio (natDegree (minpoly R x)) ⊆
  (fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)
Tactic: simp only [Finset.coe_image, Finset.coe_range, Set.image_subset_iff]
-- 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
i : ℕ
⊢ i ∈ Set.Iio (natDegree (minpoly R x)) →
    Membership.mem (γ := Set ℕ)
      ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) i
have a : ∀ (i : ℕ)
  (hi :
    ∀ m < i,
      m ∈ Set.Iio (natDegree (minpoly R x)) →
        Membership.mem (γ := Set ℕ)
          ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) m),
  i ∈ Set.Iio (natDegree (minpoly R x)) →
    Membership.mem (γ := Set ℕ)
      ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) i
Tactic: induction i using Nat.strongRecOn with | ind i hi => ?_
Cleared hypotheses: i
-- 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
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (natDegree (minpoly R x)) →
      Membership.mem (γ := Set ℕ)
        ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) m
hi' : i ∈ Set.Iio (natDegree (minpoly R x))
⊢ Membership.mem (γ := Set ℕ)
    ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) i
have this : Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
  (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))
Tactic: have : coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) ∈
        Submodule.span R (Set.range (coeff (minpolyDiv R x))) :=
      Submodule.subset_span (Set.mem_range_self _)
-- 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
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (natDegree (minpoly R x)) →
      Membership.mem (γ := Set ℕ)
        ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) m
hi' : i ∈ Set.Iio (natDegree (minpoly R x))
this :
  Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))
⊢ Membership.mem (γ := Set ℕ)
    ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) i
have a : Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
  (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i)
Tactic: rw [Set.mem_preimage, SetLike.mem_coe, ← Submodule.sub_mem_iff_right _ 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
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (natDegree (minpoly R x)) →
      Membership.mem (γ := Set ℕ)
        ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) m
hi' : i ∈ Set.Iio (natDegree (minpoly R x))
this :
  Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i)
have a : LE.le (α := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio i))
  (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
Tactic: refine SetLike.le_def.mp ?_ (coeff_minpolyDiv_sub_pow_mem_span 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
h : Nontrivial S
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (natDegree (minpoly R x)) →
      Membership.mem (γ := Set ℕ)
        ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) m
hi' : i ∈ Set.Iio (natDegree (minpoly R x))
this :
  Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))
a :
  LE.le (α := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio i))
    (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i)
have a₁ : i ≤ natDegree (minpolyDiv R x)
Tactic: refine SetLike.le_def.mp ?_ (coeff_minpolyDiv_sub_pow_mem_span 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
h : Nontrivial S
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (natDegree (minpoly R x)) →
      Membership.mem (γ := Set ℕ)
        ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) m
hi' : i ∈ Set.Iio (natDegree (minpoly R x))
this :
  Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))
⊢ LE.le (α := Submodule R S) (Submodule.span R ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio i))
    (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
have a : Set.Iio i ⊆ (fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)
Tactic: rw [Submodule.span_le, Set.image_subset_iff]
-- 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
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (natDegree (minpoly R x)) →
      Membership.mem (γ := Set ℕ)
        ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) m
hi' : i ∈ Set.Iio (natDegree (minpoly R x))
this :
  Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))
j : ℕ
⊢ j ∈ Set.Iio i →
    Membership.mem (γ := Set ℕ)
      ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) j
have a : ∀ (hj : j < i),
  Membership.mem (γ := Set ℕ)
    ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) j
Tactic: (hj : j < i)
-- 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
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (natDegree (minpoly R x)) →
      Membership.mem (γ := Set ℕ)
        ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) m
hi' : i ∈ Set.Iio (natDegree (minpoly R x))
this :
  Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))
⊢ i ≤ natDegree (minpolyDiv R x)
have a : ∀ (hi' : i ∈ Set.Iio (natDegree (minpolyDiv R x) + 1))
  (this :
    Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))),
  i ≤ natDegree (minpolyDiv R x)
Tactic: rwa [← natDegree_minpolyDiv_succ hx, Set.mem_Iio, Nat.lt_succ_iff] at hi'
Cleared hypotheses: hi', 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
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (natDegree (minpoly R x)) →
      Membership.mem (γ := Set ℕ)
        ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) m
hi' : i ∈ Set.Iio (natDegree (minpoly R x))
this :
  Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))
a :
  ∀ (hi' : i ∈ Set.Iio (natDegree (minpolyDiv R x) + 1))
    (this :
      Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
        (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))),
    i ≤ natDegree (minpolyDiv R x)
⊢ i ≤ natDegree (minpolyDiv R x)
have a₁ : ∀ (hi' : i < natDegree (minpolyDiv R x) + 1)
  (this :
    Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))),
  i ≤ natDegree (minpolyDiv R x)
Tactic: rwa [← natDegree_minpolyDiv_succ hx, Set.mem_Iio, Nat.lt_succ_iff] at hi'
Cleared hypotheses: hi', 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
i : ℕ
hi :
  ∀ m < i,
    m ∈ Set.Iio (natDegree (minpoly R x)) →
      Membership.mem (γ := Set ℕ)
        ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) m
hi' : i ∈ Set.Iio (natDegree (minpoly R x))
this :
  Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))
a :
  ∀ (hi' : i ∈ Set.Iio (natDegree (minpolyDiv R x) + 1))
    (this :
      Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
        (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))),
    i ≤ natDegree (minpolyDiv R x)
a₁ :
  ∀ (hi' : i < natDegree (minpolyDiv R x) + 1)
    (this :
      Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
        (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))),
    i ≤ natDegree (minpolyDiv R x)
⊢ i ≤ natDegree (minpolyDiv R x)
have a₂ : ∀ (hi' : i ≤ natDegree (minpolyDiv R x))
  (this :
    Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
      (coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i))),
  i ≤ natDegree (minpolyDiv R x)
Tactic: rwa [← natDegree_minpolyDiv_succ hx, Set.mem_Iio, Nat.lt_succ_iff] at hi'
Cleared hypotheses: hi', 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
⊢ Eq (α := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x])
have a : LE.le (α := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
  ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x])
Tactic: classical
  apply le_antisymm
  · rw [Submodule.span_le]
    rintro _ ⟨i, rfl⟩
    apply coeff_minpolyDiv_mem_adjoin
  · rw [← Submodule.span_range_natDegree_eq_adjoin (minpoly.monic hx) (minpoly.aeval _ _),
      Submodule.span_le]
    simp only [Finset.coe_image, Finset.coe_range, Set.image_subset_iff]
    intro i
    induction i using Nat.strongRecOn with | ind i hi => ?_
    intro hi'
    have : coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) ∈
        Submodule.span R (Set.range (coeff (minpolyDiv R x))) :=
      Submodule.subset_span (Set.mem_range_self _)
    rw [Set.mem_preimage, SetLike.mem_coe, ← Submodule.sub_mem_iff_right _ this]
    refine SetLike.le_def.mp ?_ (coeff_minpolyDiv_sub_pow_mem_span hx ?_)
    · rw [Submodule.span_le, Set.image_subset_iff]
      intro j (hj : j < i)
      exact hi j hj (lt_trans hj hi')
    · rwa [← natDegree_minpolyDiv_succ hx, Set.mem_Iio, Nat.lt_succ_iff] at 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
h : Nontrivial S
a :
  LE.le (α := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x])
⊢ Eq (α := Submodule R S) (Submodule.span R (Set.range (coeff (minpolyDiv R x))))
    ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x])
have a₁ : LE.le (α := Submodule R S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x] : Submodule R S)
  (Submodule.span R (Set.range (coeff (minpolyDiv R x))) : Submodule R S)
Tactic: classical
  apply le_antisymm
  · rw [Submodule.span_le]
    rintro _ ⟨i, rfl⟩
    apply coeff_minpolyDiv_mem_adjoin
  · rw [← Submodule.span_range_natDegree_eq_adjoin (minpoly.monic hx) (minpoly.aeval _ _),
      Submodule.span_le]
    simp only [Finset.coe_image, Finset.coe_range, Set.image_subset_iff]
    intro i
    induction i using Nat.strongRecOn with | ind i hi => ?_
    intro hi'
    have : coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) ∈
        Submodule.span R (Set.range (coeff (minpolyDiv R x))) :=
      Submodule.subset_span (Set.mem_range_self _)
    rw [Set.mem_preimage, SetLike.mem_coe, ← Submodule.sub_mem_iff_right _ this]
    refine SetLike.le_def.mp ?_ (coeff_minpolyDiv_sub_pow_mem_span hx ?_)
    · rw [Submodule.span_le, Set.image_subset_iff]
      intro j (hj : j < i)
      exact hi j hj (lt_trans hj hi')
    · rwa [← natDegree_minpolyDiv_succ hx, Set.mem_Iio, Nat.lt_succ_iff] at hi'
-- 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
⊢ natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1
have a : Nontrivial S
Tactic: nontriviality S
-- 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
h : Nontrivial S
⊢ natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1
have pos : ∀ (hx : IsIntegral R x), natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1
Tactic: by_cases hx : IsIntegral 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
h : Nontrivial S
pos : ∀ (hx : IsIntegral R x), natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1
⊢ natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1
have neg : ∀ (hx : ¬IsIntegral R x), natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1
Tactic: by_cases hx : IsIntegral 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
h : Nontrivial S
hx : IsIntegral R x
⊢ natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1
have pos : natDegree (minpolyDiv R x) = natDegree (minpolyDiv R x) + 1 - 1
Tactic: rw [← natDegree_minpolyDiv_succ 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
h : Nontrivial S
hx : ¬IsIntegral R x
⊢ natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1
have neg : natDegree.{u_1} (R := S) 0 = natDegree.{u_2} (R := R) 0 - 1
Tactic: rw [minpolyDiv_eq_zero hx, minpoly.eq_zero hx]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_1
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : IsAlgClosed E
inst_6 : FiniteDimensional K L
inst_7 : Algebra.IsSeparable K L
x : L
hxL : Eq (α := Subalgebra K L) K[x] ⊤
r : ℕ
hr : r < finrank K L
⊢ ∑ σ : L →ₐ[K] E,
      map (↑σ : L →+* E)
        (HSMul.hSMul (β := L[X])
          (HDiv.hDiv (β := L) (x ^ r)
            ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L))
          (minpolyDiv K x)) =
    HPow.hPow (α := E[X]) X r
have rw : ∑ σ : L →ₐ[K] E,
      map (↑σ : L →+* E)
        (HSMul.hSMul (β := L[X])
          (HDiv.hDiv (β := L) (x ^ r)
            ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L))
          (minpolyDiv K x)) -
    HPow.hPow (α := E[X]) X r =
  0
Tactic: rw [← sub_eq_zero]