awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
ih : ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n), n ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n + 1
hp : P ≠ 0
η : R
η_root : η ∈ P.roots
η_pos : 0 < η
⊢ n + 1 ≤ P.signVariations
have succ : ∀ (Q : R[X])
  (h :
    Multiset.countP (fun (x : R) ↦ 0 < x)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots =
      n + 1)
  (hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q ≠ 0)
  (η_root : η ∈ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots),
  n + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).signVariations
Tactic: obtain ⟨Q, rfl⟩ := dvd_iff_isRoot.mpr (isRoot_of_mem_roots η_root)
Cleared hypotheses: P, h, hp, η_root
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
ih : ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n), n ≤ P.signVariations
η : R
η_pos : 0 < η
Q : R[X]
h :
  Multiset.countP (fun (x : R) ↦ 0 < x)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots =
    n + 1
hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q ≠ 0
η_root : η ∈ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots
⊢ n + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).signVariations
have succ : Q ≠ 0
Tactic: grw [ih Q, succ_signVariations_le_X_sub_C_mul η_pos]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
ih : ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n), n ≤ P.signVariations
η : R
η_pos : 0 < η
Q : R[X]
h :
  Multiset.countP (fun (x : R) ↦ 0 < x)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots =
    n + 1
hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q ≠ 0
η_root : η ∈ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots
succ : Q ≠ 0
⊢ n + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).signVariations
have succ₁ : Multiset.countP (fun (x : R) ↦ 0 < x) Q.roots = n
Tactic: grw [ih Q, succ_signVariations_le_X_sub_C_mul η_pos]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
⊢ span R ((↑S : ℕ → R[X]) '' Set.Iio m) = degreeLT R m
have h₁ : (↑S : ℕ → R[X]) '' Set.Iio m ⊆ (↑(degreeLT R m) : Set R[X])
Tactic: apply span_eq_of_le
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h₁ : (↑S : ℕ → R[X]) '' Set.Iio m ⊆ (↑(degreeLT R m) : Set R[X])
⊢ span R ((↑S : ℕ → R[X]) '' Set.Iio m) = degreeLT R m
have h₂ : degreeLT R m ≤ span R ((↑S : ℕ → R[X]) '' Set.Iio m)
Tactic: apply span_eq_of_le
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
hP : P ∈ (↑S : ℕ → R[X]) '' Set.Iio m
⊢ P ∈ (↑(degreeLT R m) : Set R[X])
have h₁ : ∀ (i : ℕ) (hi : i ∈ Set.Iio m) (hP : (↑S : ℕ → R[X]) i ∈ (↑S : ℕ → R[X]) '' Set.Iio m),
  (↑S : ℕ → R[X]) i ∈ (↑(degreeLT R m) : Set R[X])
Tactic: obtain ⟨i, hi, rfl⟩ := (Set.mem_image _ _ _).mp hP
Cleared hypotheses: P, hP
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
i : ℕ
hi : i ∈ Set.Iio m
hP : (↑S : ℕ → R[X]) i ∈ (↑S : ℕ → R[X]) '' Set.Iio m
⊢ (↑S : ℕ → R[X]) i ∈ (↑(degreeLT R m) : Set R[X])
have h₁ : i < m
Tactic: rw [SetLike.mem_coe, Polynomial.mem_degreeLT, S.degree_eq i, Nat.cast_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
have a : Nontrivial R
Tactic: nontriviality R using Subsingleton.eq_zero P
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
h : Nontrivial R
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
have generalize : ∀ (n : ℕ) (hp : P.natDegree = n), Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
Tactic: generalize hp : P.natDegree = n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
have pos : ∀ (p_ne_zero : P = 0), Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
Tactic: by_cases! p_ne_zero : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
pos : ∀ (p_ne_zero : P = 0), Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
have neg : ∀ (p_ne_zero : P ≠ 0), Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
Tactic: by_cases! p_ne_zero : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
⊢ n < m
have hP₁ : P.degree < (↑m : WithBot ℕ)
Tactic: rw [Polynomial.mem_degreeLT] at hP
Cleared hypotheses: hP, hp, p_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : P.degree < (↑m : WithBot ℕ)
hp : P.natDegree = n
p_ne_zero : P ≠ 0
⊢ n < m
have this : P.degree = (↑P.natDegree : WithBot ℕ)
Tactic: have := Polynomial.degree_eq_natDegree p_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
have hn : n < m
Tactic: have hn : n < m := by
      rw [Polynomial.mem_degreeLT] at hP
      have := Polynomial.degree_eq_natDegree p_ne_zero
      aesop
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
have neg : ∀ (u : R) (leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1) (rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1),
  Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
Tactic: obtain ⟨u, leftinv, rightinv⟩ := isUnit_iff_exists.mp <| hCoeff n hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
have in_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) ((↑S : ℕ → R[X]) n)
Tactic: have in_span : S n ∈ span R (S '' Set.Iio m) := subset_span ⟨n, by simp [hn], rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
in_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) ((↑S : ℕ → R[X]) n)
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
have smul_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m))
  ((P.leadingCoeff • u) • (↑S : ℕ → R[X]) n)
Tactic: have smul_span := smul_mem (span R (S '' Set.Iio m)) (P.leadingCoeff • u) in_span
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
in_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) ((↑S : ℕ → R[X]) n)
smul_span :
  Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m))
    ((P.leadingCoeff • u) • (↑S : ℕ → R[X]) n)
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
have rwa : ∀
  (smul_span :
    Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m))
      (P.leadingCoeff • u • (↑S : ℕ → R[X]) n)),
  Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
Tactic: rwa [smul_assoc] at smul_span
Cleared hypotheses: smul_span
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
have head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
Tactic: have head_mem_span : head ∈ span R (S '' Set.Iio m) := by
      have in_span : S n ∈ span R (S '' Set.Iio m) := subset_span ⟨n, by simp [hn], rfl⟩
      have smul_span := smul_mem (span R (S '' Set.Iio m)) (P.leadingCoeff • u) in_span
      rwa [smul_assoc] at smul_span
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
have pos : ∀ (tail_eq_zero : tail = 0), Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
Tactic: by_cases tail_eq_zero : tail = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
pos : ∀ (tail_eq_zero : tail = 0), Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
have neg : ∀ (tail_eq_zero : ¬tail = 0), Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
Tactic: by_cases tail_eq_zero : tail = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
tail_eq_zero : ¬tail = 0
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
have neg : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) (P - head)
Tactic: apply sub_mem_iff_left _ head_mem_span |>.mp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
tail_eq_zero : ¬tail = 0
this : tail.degree < (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) (P - head)
have refine : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) (P - head)
Tactic: refine ih tail.natDegree ((natDegree_lt_iff_degree_lt tail_eq_zero).mpr this) ?_ rfl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
tail_eq_zero : ¬tail = 0
this : tail.degree < (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R m) (P - head)
have this₁ : tail.degree < (↑m : WithBot ℕ)
Tactic: grw [(Nat.cast_lt (α := WithBot ℕ)).mpr hn] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
tail_eq_zero : ¬tail = 0
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) (P - head)
have neg : tail.degree < (↑n : WithBot ℕ)
Tactic: suffices tail.degree < n by
      refine ih tail.natDegree ((natDegree_lt_iff_degree_lt tail_eq_zero).mpr this) ?_ rfl
      grw [(Nat.cast_lt (α := WithBot ℕ)).mpr hn] at this
      rwa [Polynomial.mem_degreeLT]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
tail_eq_zero : ¬tail = 0
⊢ tail.degree < (↑n : WithBot ℕ)
have isRightRegular_smul_leadingCoeff : IsRightRegular (u • (↑S : ℕ → R[X]) n).leadingCoeff
Tactic: have isRightRegular_smul_leadingCoeff : IsRightRegular (u • S n).leadingCoeff := by
      simpa [leadingCoeff_smul_of_smul_regular, IsSMulRegular.of_mul_eq_one leftinv, rightinv]
        using isRegular_one.right
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • (↑S : ℕ → R[X]) n).leadingCoeff
⊢ tail.degree < (↑n : WithBot ℕ)
have u_degree_same : (u • (↑S : ℕ → R[X]) n).degree = ((↑S : ℕ → R[X]) n).degree
Tactic: have u_degree_same := degree_smul_of_isRightRegular_leadingCoeff
      (left_ne_zero_of_mul_eq_one rightinv) (hCoeff n hn).isRegular.right