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
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)
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))
⊢ 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:
apply SetLike.le_def.mp ?_
        (Submodule.mul_mem_mul (IH ((Nat.le_succ _).trans hi))
          (Submodule.mem_span_singleton_self x))

Premises used: Submodule.mul_mem_mul, SetLike.le_def, Nat.le_succ, Submodule.mem_span_singleton_self, Iff.mp, LE.le.trans
-- 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)
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)))
⊢ 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:
rw [Submodule.span_mul_span, Set.mul_singleton, Set.image_image]

Premises used: Set.image_image, Set.mul_singleton, Submodule.span_mul_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)
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))
⊢ 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:
apply Submodule.span_mono

Premises used: Submodule.span_mono
-- 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)
j : ℕ
hj : j ∈ Set.Iio i
⊢ j < i

Tactic:
rw [Set.mem_Iio] at hj

Premises used: Set.mem_Iio
-- 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)
j : ℕ
hj : j < i
⊢ Membership.mem (γ := Set S) ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)) ((fun (x_1 : ℕ) ↦ x ^ x_1 * x) j)

Tactic:
⟨j + 1, Nat.add_lt_of_lt_sub hj, pow_succ x j⟩

Premises used: Set.Mem, pow_succ, setOf, Nat.add_lt_of_lt_sub, HAdd.hAdd, 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)
j : ℕ
hj : j < i
⊢ Membership.mem (γ := Set S) ((fun (x_1 : ℕ) ↦ x ^ x_1) '' Set.Iio (i + 1)) ((fun (x_1 : ℕ) ↦ x ^ x_1 * x) j)

Tactic:
exact ⟨j + 1, Nat.add_lt_of_lt_sub hj, pow_succ x j⟩
-- 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 : ℕ
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)
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))
⊢ 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)

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⟩

Premises used: add_sub_assoc, Set.image_image, Set.mem_Iio, le_tsub_of_add_le_left, pow_succ, Set.mul_singleton, Submodule.span_mul_span, tsub_add_cancel_of_le, Algebra.algebraMap_eq_smul_one, sub_mul, coeff_minpolyDiv, Submodule.span_mono, AddMemClass.add_mem, tsub_tsub, Submodule.subset_span, Polynomial.Monic.leadingCoeff, minpolyDiv_monic, rfl, 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
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])
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)
⊢ Eq (α := 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

Premises used: le_antisymm
-- 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
a :
  Set.range (coeff (minpolyDiv R x)) ⊆
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x] : Submodule R S) : Set 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])

Tactic:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- 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
i : ℕ
⊢ coeff (minpolyDiv R x) i ∈
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[x] : Submodule R S) : Set S)

Tactic:
apply coeff_minpolyDiv_mem_adjoin

Premises used: coeff_minpolyDiv_mem_adjoin
-- 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
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)
⊢ 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:
rw [← Submodule.span_range_natDegree_eq_adjoin (minpoly.monic hx) (minpoly.aeval _ _),
      Submodule.span_le]

Premises used: minpoly.monic, minpoly.aeval, Submodule.span_range_natDegree_eq_adjoin, Submodule.span_le
-- 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
a :
  Set.Iio (natDegree (minpoly R x)) ⊆
    (fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set 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)

Tactic:
simp only [Finset.coe_image, Finset.coe_range, Set.image_subset_iff]

Premises used: Finset.coe_range, Finset.coe_image, Set.image_subset_iff
-- 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
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:
?_
-- 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
i : ℕ
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
⊢ 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 => ?_
-- 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
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 (γ := 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 _)
-- 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
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 :
  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)
⊢ Membership.mem (γ := Set ℕ)
    ((fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)) i

Tactic:
rw [Set.mem_preimage, SetLike.mem_coe, ← Submodule.sub_mem_iff_right _ this]

Premises used: SetLike.mem_coe, Submodule.sub_mem_iff_right, Set.mem_preimage
-- 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
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)

Tactic:
SetLike.le_def.mp ?_ (coeff_minpolyDiv_sub_pow_mem_span hx ?_)

Premises used: coeff_minpolyDiv_sub_pow_mem_span, SetLike.le_def, Iff.mp
-- 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
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))))
a₁ : i ≤ natDegree (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)

Tactic:
refine SetLike.le_def.mp ?_ (coeff_minpolyDiv_sub_pow_mem_span hx ?_)

Premises used: coeff_minpolyDiv_sub_pow_mem_span, SetLike.le_def, Iff.mp
-- 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
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 : Set.Iio i ⊆ (fun (x_1 : ℕ) ↦ x ^ x_1) ⁻¹' (↑(Submodule.span R (Set.range (coeff (minpolyDiv R x)))) : Set S)
⊢ 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:
rw [Submodule.span_le, Set.image_subset_iff]

Premises used: Set.image_subset_iff, Submodule.span_le
-- 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
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 : ℕ
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
⊢ 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

Tactic:
(hj : j < i)
-- 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
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 : ℕ
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:
hi j hj (lt_trans hj hi')

Premises used: Set.Mem, lt_trans
-- 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
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 : ℕ
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:
exact hi j hj (lt_trans hj hi')

Premises used: lt_trans
-- 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
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)
a₂ a₃ a₄ 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)
⊢ i ≤ natDegree (minpolyDiv R x)

Tactic:
rwa [← natDegree_minpolyDiv_succ hx, Set.mem_Iio, Nat.lt_succ_iff] at hi'

Premises used: Set.mem_Iio, natDegree_minpolyDiv_succ, Nat.lt_succ_iff
-- 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
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])
a₁ 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)
⊢ Eq (α := 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'

Premises used: Set.mem_Iio, minpoly.monic, natDegree_minpolyDiv_succ, Finset.coe_range, coeff_minpolyDiv_sub_pow_mem_span, SetLike.le_def, Finset.coe_image, coeff_minpolyDiv_mem_adjoin, minpoly.aeval, Submodule.span_range_natDegree_eq_adjoin, le_antisymm, Nat.lt_succ_iff, SetLike.mem_coe, Iff.mp, Set.image_subset_iff, Submodule.span_le, rfl, Set.mem_preimage
-- 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
⊢ 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
h : Nontrivial S
pos : ∀ (hx : IsIntegral R x), natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1
neg : ∀ (hx : ¬IsIntegral R x), natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1
⊢ natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1

Tactic:
by_cases hx : IsIntegral R x

Premises used: IsIntegral
-- 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
h : Nontrivial S
hx : IsIntegral R x
pos : natDegree (minpolyDiv R x) = natDegree (minpolyDiv R x) + 1 - 1
⊢ natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1

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
h : Nontrivial S
hx : IsIntegral R x
⊢ natDegree (minpolyDiv R x) = natDegree (minpolyDiv R x) + 1 - 1

Tactic:
rfl
-- 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
h : Nontrivial S
hx : ¬IsIntegral R x
neg : natDegree.{u_1} (R := S) 0 = natDegree.{u_2} (R := R) 0 - 1
⊢ natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1

Tactic:
rw [minpolyDiv_eq_zero hx, minpoly.eq_zero hx]

Premises used: minpoly.eq_zero, minpolyDiv_eq_zero