awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1) =
    ∑ i ∈ range n, (↑(n.choose (i + 1)) : R[X]) * HPow.hPow (α := R[X]) X i
have a : ∀ (i : ℕ),
  (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i =
    coeff (∑ i ∈ range n, (↑(n.choose (i + 1)) : R[X]) * HPow.hPow (α := R[X]) X i) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n i : ℕ
⊢ (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i =
    coeff (∑ i ∈ range n, (↑(n.choose (i + 1)) : R[X]) * HPow.hPow (α := R[X]) X i) i
have trans : (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i = (↑(n.choose (i + 1)) : R)
Tactic: trans (n.choose (i + 1) : R)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n i : ℕ
trans :
  (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i = (↑(n.choose (i + 1)) : R)
⊢ (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i =
    coeff (∑ i ∈ range n, (↑(n.choose (i + 1)) : R[X]) * HPow.hPow (α := R[X]) X i) i
have trans₁ : Eq.{u + 1} (α := R) (↑(n.choose (i + 1)) : R)
  (coeff (∑ i ∈ range n, (↑(n.choose (i + 1)) : R[X]) * HPow.hPow (α := R[X]) X i) i)
Tactic: trans (n.choose (i + 1) : R)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n i : ℕ
⊢ Eq.{u + 1} (α := R) (↑(n.choose (i + 1)) : R)
    (coeff (∑ i ∈ range n, (↑(n.choose (i + 1)) : R[X]) * HPow.hPow (α := R[X]) X i) i)
have simp : Eq.{u + 1} (α := R) (↑(n.choose (i + 1)) : R) (∑ x ∈ range n, if i = x then (↑(n.choose (x + 1)) : R) else 0)
Tactic: simp only [finsetSum_coeff, ← C_eq_natCast, coeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n i : ℕ
⊢ Eq.{u + 1} (α := R) (↑(n.choose (i + 1)) : R) (∑ x ∈ range n, if i = x then (↑(n.choose (x + 1)) : R) else 0)
have h₀ : ∀ b ∈ range n, b ≠ i → Eq.{u + 1} (α := R) (if i = b then (↑(n.choose (b + 1)) : R) else 0) 0
Tactic: rw [Finset.sum_eq_single i, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n i : ℕ
h₀ : ∀ b ∈ range n, b ≠ i → Eq.{u + 1} (α := R) (if i = b then (↑(n.choose (b + 1)) : R) else 0) 0
⊢ Eq.{u + 1} (α := R) (↑(n.choose (i + 1)) : R) (∑ x ∈ range n, if i = x then (↑(n.choose (x + 1)) : R) else 0)
have h₁ : i ∉ range n → Eq.{u + 1} (α := R) (if i = i then (↑(n.choose (i + 1)) : R) else 0) 0
Tactic: rw [Finset.sum_eq_single i, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n i : ℕ
⊢ (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i = (↑(n.choose (i + 1)) : R)
have zero : ∀ (i : ℕ),
  (comp (∑ i ∈ range 0, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i = (↑(Nat.choose 0 (i + 1)) : R)
Tactic: induction n generalizing i with
  | zero => dsimp; simp only [zero_comp, coeff_zero, Nat.cast_zero]
  | succ n ih =>
    simp only [geom_sum_succ', ih, add_comp, X_pow_comp, coeff_add, Nat.choose_succ_succ,
      Nat.cast_add, coeff_X_add_one_pow]
Cleared hypotheses: n, i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n i : ℕ
zero :
  ∀ (i : ℕ),
    (comp (∑ i ∈ range 0, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i =
      (↑(Nat.choose 0 (i + 1)) : R)
⊢ (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i = (↑(n.choose (i + 1)) : R)
have succ : ∀ (n : ℕ)
  (ih :
    ∀ (i : ℕ),
      (comp (∑ i ∈ range n, HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i = (↑(n.choose (i + 1)) : R))
  (i : ℕ),
  (comp (∑ i ∈ range (n + 1), HPow.hPow (α := R[X]) X i) (HAdd.hAdd (α := R[X]) X 1)).coeff i =
    (↑((n + 1).choose (i + 1)) : R)
Tactic: induction n generalizing i with
  | zero => dsimp; simp only [zero_comp, coeff_zero, Nat.cast_zero]
  | succ n ih =>
    simp only [geom_sum_succ', ih, add_comp, X_pow_comp, coeff_add, Nat.choose_succ_succ,
      Nat.cast_add, coeff_X_add_one_pow]
Cleared hypotheses: n, i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
n : ℕ
hn : n ≠ 0
⊢ Monic.{u} (R := R) (∑ i ∈ range n, P ^ i)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
n : ℕ
hn : n ≠ 0
h : Nontrivial R
⊢ Monic.{u} (R := R) (∑ i ∈ range n, P ^ i)
have obtain : ∀ (n : ℕ) (hn : n.succ ≠ 0), Monic.{u} (R := R) (∑ i ∈ range n.succ, P ^ i)
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ Monic.{u} (R := R) (∑ i ∈ range n.succ, P ^ i)
have rw : (P ^ n + ∑ i ∈ range n, P ^ i).Monic
Tactic: rw [geom_sum_succ']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ (P ^ n + ∑ i ∈ range n, P ^ i).Monic
have refine : degree.{u} (R := R) (∑ i ∈ range n, P ^ i) < (P ^ n).degree
Tactic: refine (hP.pow _).add_of_left ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ degree.{u} (R := R) (∑ i ∈ range n, P ^ i) < (P ^ n).degree
have refine : ((range n).sup fun (b : ℕ) ↦ (P ^ b).degree) < (P ^ n).degree
Tactic: refine lt_of_le_of_lt (degree_sum_le _ _) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ ((range n).sup fun (b : ℕ) ↦ (P ^ b).degree) < (P ^ n).degree
have rw : ∀ b ∈ range n, (P ^ b).degree < (P ^ n).degree
Tactic: rw [Finset.sup_lt_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
rw : ∀ b ∈ range n, (P ^ b).degree < (P ^ n).degree
⊢ ((range n).sup fun (b : ℕ) ↦ (P ^ b).degree) < (P ^ n).degree
have rw₁ : ⊥ < (P ^ n).degree
Tactic: rw [Finset.sup_lt_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ ∀ b ∈ range n, (P ^ b).degree < (P ^ n).degree
have simp : ∀ b < n, LT.lt (α := WithBot ℕ) (↑(P ^ b).natDegree : WithBot ℕ) (↑(P ^ n).natDegree : WithBot ℕ)
Tactic: simp only [Finset.mem_range, degree_eq_natDegree (hP.pow _).ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ ∀ b < n, LT.lt (α := WithBot ℕ) (↑(P ^ b).natDegree : WithBot ℕ) (↑(P ^ n).natDegree : WithBot ℕ)
have simp : ∀ b < n, b * P.natDegree < n * P.natDegree
Tactic: simp only [Nat.cast_lt, hP.natDegree_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
h : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ ⊥ < (P ^ n).degree
have rw : ¬P ^ n = 0
Tactic: rw [bot_lt_iff_ne_bot, Ne, degree_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : n ≠ 0
⊢ Monic.{u} (R := R) (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : n ≠ 0
h : Nontrivial R
⊢ Monic.{u} (R := R) (∑ i ∈ range n, HPow.hPow (α := R[X]) X i)
have apply : 0 < natDegree.{u} (R := R) X
Tactic: apply monic_X.geom_sum _ hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
⊢ (↑(p.restriction.coeff n) : R) = p.coeff n
have simp : (↑(if p.coeff n = 0 then 0
      else
        Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x)
          (p.coeff n) sorry) :
    R) =
  p.coeff n
Tactic: simp only [restriction, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
⊢ (↑(if p.coeff n = 0 then 0
        else
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x)
            (p.coeff n) ⋯) :
      R) =
    p.coeff n
have pos : ∀ (h : p.coeff n = 0), (↑0 : R) = p.coeff n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
pos : ∀ (h : p.coeff n = 0), (↑0 : R) = p.coeff n
⊢ (↑(if p.coeff n = 0 then 0
        else
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x)
            (p.coeff n) ⋯) :
      R) =
    p.coeff n
have neg : ∀ (h : ¬p.coeff n = 0),
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x) (p.coeff n)
          sorry) :
      R) =
    p.coeff n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ (↑0 : R) = p.coeff n
have pos : Eq.{u + 1} (α := R) (↑0 : R) 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
⊢ (↑(p.restriction.coeff n) : R) = p.coeff n
have simp : (↑(if p.coeff n = 0 then 0
      else
        Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x)
          (p.coeff n) sorry) :
    R) =
  p.coeff n
Tactic: classical
  simp only [restriction, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
simp :
  (↑(if p.coeff n = 0 then 0
        else
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x)
            (p.coeff n) ⋯) :
      R) =
    p.coeff n
⊢ (↑(p.restriction.coeff n) : R) = p.coeff n
have pos : ∀ (h : p.coeff n = 0), (↑0 : R) = p.coeff n
Tactic: classical
  simp only [restriction, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
n : ℕ
simp :
  (↑(if p.coeff n = 0 then 0
        else
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x)
            (p.coeff n) ⋯) :
      R) =
    p.coeff n
pos : ∀ (h : p.coeff n = 0), (↑0 : R) = p.coeff n
⊢ (↑(p.restriction.coeff n) : R) = p.coeff n
have neg : ∀ (h : ¬p.coeff n = 0),
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subring R) (Subring.closure (↑p.coeffs : Set R)) x) (p.coeff n)
          sorry) :
      R) =
    p.coeff n
Tactic: classical
  simp only [restriction, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ p.restriction.support = p.support
have h : ∀ (i : ℕ), i ∈ p.restriction.support ↔ i ∈ p.support
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
i : ℕ
⊢ i ∈ p.restriction.support ↔ i ∈ p.support
have h : p.restriction.coeff i = 0 ↔ p.coeff i = 0
Tactic: simp only [mem_support_iff, not_iff_not, Ne]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
i : ℕ
| p.coeff i = 0
have rw : (↑(p.restriction.coeff i) : R) = 0
Tactic: rw [← coeff_restriction]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
i : ℕ
⊢ p.restriction.coeff i = 0 ↔ p.coeff i = 0
have h : p.restriction.coeff i = 0 ↔ (↑(p.restriction.coeff i) : R) = 0
Tactic: conv_rhs => rw [← coeff_restriction]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
i : ℕ
H : p.restriction.coeff i = 0
⊢ (↑(p.restriction.coeff i) : R) = 0
have rw : Eq.{u + 1} (α := R) (↑0 : R) 0
Tactic: rw [H, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
i : ℕ
H : p.restriction.coeff i = 0
rw : Eq.{u + 1} (α := R) (↑0 : R) 0
⊢ (↑(p.restriction.coeff i) : R) = 0
have rw₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [H, ZeroMemClass.coe_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
n : ℕ
⊢ coeff (map (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) R) p.restriction) n = p.coeff n
have rw : (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) R : (a : ↥(Subring.closure (↑p.coeffs : Set R))) → R)
    (p.restriction.coeff n) =
  p.coeff n
Tactic: rw [coeff_map, Algebra.algebraMap_ofSubsemiring_apply, coeff_restriction]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
n : ℕ
rw :
  (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) R : (a : ↥(Subring.closure (↑p.coeffs : Set R))) → R)
      (p.restriction.coeff n) =
    p.coeff n
⊢ coeff (map (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) R) p.restriction) n = p.coeff n
have rw₁ : (↑(p.restriction.coeff n) : R) = p.coeff n
Tactic: rw [coeff_map, Algebra.algebraMap_ofSubsemiring_apply, coeff_restriction]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
n : ℕ
rw :
  (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) R : (a : ↥(Subring.closure (↑p.coeffs : Set R))) → R)
      (p.restriction.coeff n) =
    p.coeff n
rw₁ : (↑(p.restriction.coeff n) : R) = p.coeff n
⊢ coeff (map (algebraMap (↥(Subring.closure (↑p.coeffs : Set R))) R) p.restriction) n = p.coeff n
have rw₂ : p.coeff n = p.coeff n
Tactic: rw [coeff_map, Algebra.algebraMap_ofSubsemiring_apply, coeff_restriction]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ p.restriction.Monic ↔ p.Monic
have simp : p.restriction.coeff p.natDegree = 1 ↔ p.coeff p.natDegree = 1
Tactic: simp only [Monic, leadingCoeff, natDegree_restriction]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ p.restriction.coeff p.natDegree = 1 ↔ p.coeff p.natDegree = 1
have rw : p.restriction.coeff p.natDegree = 1 ↔ (↑(p.restriction.coeff p.natDegree) : R) = 1
Tactic: rw [← @coeff_restriction _ _ p]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
H : p.restriction.coeff p.natDegree = 1
⊢ (↑(p.restriction.coeff p.natDegree) : R) = 1
have rw : Eq.{u + 1} (α := R) (↑1 : R) 1
Tactic: rw [H, OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
H : p.restriction.coeff p.natDegree = 1
rw : Eq.{u + 1} (α := R) (↑1 : R) 1
⊢ (↑(p.restriction.coeff p.natDegree) : R) = 1
have rw₁ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [H, OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
i : ℕ
⊢ Eq.{u + 1} (α := R) (↑(coeff (restriction 1) i) : R) (↑(coeff 1 i) : R)
have rw : Eq.{u + 1} (α := R) (if i = 0 then 1 else 0) (↑(if i = 0 then 1 else 0) : R)
Tactic: rw [coeff_restriction', coeff_one, coeff_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
i : ℕ
⊢ Eq.{u + 1} (α := R) (if i = 0 then 1 else 0) (↑(if i = 0 then 1 else 0) : R)
have pos : i = 0 → Eq.{u + 1} (α := R) 1 (↑1 : R)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
i : ℕ
pos : i = 0 → Eq.{u + 1} (α := R) 1 (↑1 : R)
⊢ Eq.{u + 1} (α := R) (if i = 0 then 1 else 0) (↑(if i = 0 then 1 else 0) : R)
have neg : ¬i = 0 → Eq.{u + 1} (α := R) 0 (↑0 : R)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : Semiring R
I : Ideal R[X]
c : R
x : R[X]
H : x ∈ I.carrier
⊢ c • x ∈ I.carrier
have rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) x ∈ I.carrier
Tactic: rw [← C_mul']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
⊢ Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f ↔ ∀ (n : ℕ), f.coeff n ∈ I
have mp : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f → ∀ (n : ℕ), f.coeff n ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
mp : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f → ∀ (n : ℕ), f.coeff n ∈ I
⊢ Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f ↔ ∀ (n : ℕ), f.coeff n ∈ I
have mpr : (∀ (n : ℕ), f.coeff n ∈ I) → Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f
⊢ ∀ (n : ℕ), f.coeff n ∈ I
have mp : ∀ (x : R[X]) (h : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) x) (n : ℕ), x.coeff n ∈ I
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f
mp : ∀ (x : R[X]) (h : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) x) (n : ℕ), x.coeff n ∈ I
⊢ ∀ (n : ℕ), f.coeff n ∈ I
have mp₁ : ∀ (n : ℕ), coeff 0 n ∈ I
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f
mp : ∀ (x : R[X]) (h : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) x) (n : ℕ), x.coeff n ∈ I
mp₁ : ∀ (n : ℕ), coeff 0 n ∈ I
⊢ ∀ (n : ℕ), f.coeff n ∈ I
have mp₂ : ∀ (x y : R[X])
  (hx : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) x)
  (hy : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) y),
  (∀ (n : ℕ), x.coeff n ∈ I) → (∀ (n : ℕ), y.coeff n ∈ I) → ∀ (n : ℕ), (x + y).coeff n ∈ I
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f
mp : ∀ (x : R[X]) (h : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) x) (n : ℕ), x.coeff n ∈ I
mp₁ : ∀ (n : ℕ), coeff 0 n ∈ I
mp₂ :
  ∀ (x y : R[X])
    (hx : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) x)
    (hy : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) y),
    (∀ (n : ℕ), x.coeff n ∈ I) → (∀ (n : ℕ), y.coeff n ∈ I) → ∀ (n : ℕ), (x + y).coeff n ∈ I
⊢ ∀ (n : ℕ), f.coeff n ∈ I
have mp₃ : ∀ (a x : R[X])
  (hx : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) x),
  (∀ (n : ℕ), x.coeff n ∈ I) → ∀ (n : ℕ), (a • x).coeff n ∈ I
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf_1 : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f : R[X]
hf : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) f
n : ℕ
⊢ f.coeff n ∈ I
have mp : ∀ (x : R) (hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → R[X]) x = f), f.coeff n ∈ I
Tactic: obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf_1 : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f : R[X]
hf : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) f
n : ℕ
x : R
hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → R[X]) x = f
⊢ f.coeff n ∈ I
have mp : (if n = 0 then x else 0) ∈ I
Tactic: rw [← hx.right, coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf_1 : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f : R[X]
hf : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) f
n : ℕ
x : R
hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → R[X]) x = f
⊢ (if n = 0 then x else 0) ∈ I
have pos : ∀ (h : n = 0), (if n = 0 then x else 0) ∈ I
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf_1 : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f : R[X]
hf : Membership.mem (γ := Set R[X]) ((⇑C : (a : R) → R[X]) '' (↑I : Set R)) f
n : ℕ
x : R
hx : x ∈ (↑I : Set R) ∧ (C : (a : R) → R[X]) x = f
pos : ∀ (h : n = 0), (if n = 0 then x else 0) ∈ I
⊢ (if n = 0 then x else 0) ∈ I
have neg : ∀ (h : ¬n = 0), (if n = 0 then x else 0) ∈ I
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f g : R[X]
h : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) g
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ (f • g).coeff n ∈ I
have mp : ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * g.coeff x.2 ∈ I
Tactic: rw [smul_eq_mul, coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
⊢ Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f
have mpr : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I)
  (f.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a)
Tactic: rw [← sum_monomial_eq f]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
⊢ Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I)
    (f.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a)
have mpr : ∀ n ∈ f.support,
  Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C I)
    ((fun (n : ℕ) (a : R) ↦ ((monomial n : (a : R) → R[X]) a : R[X])) n (f.coeff n))
Tactic: refine (I.map C : Ideal R[X]).sum_mem fun n _ => ?_