awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
pos : natDegree (R := R) ((expand R p : (a : R[X]) → R[X]) 0) = natDegree.{u} (R := R) 0 * p
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have pos₁ : natDegree.{u} (R := R) 0 = natDegree.{u} (R := R) 0 * p
Tactic: rw [hf, map_zero, natDegree_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
pos : natDegree (R := R) ((expand R p : (a : R[X]) → R[X]) 0) = natDegree.{u} (R := R) 0 * p
pos₁ : natDegree.{u} (R := R) 0 = natDegree.{u} (R := R) 0 * p
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have pos₂ : 0 = 0 * p
Tactic: rw [hf, map_zero, natDegree_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
pos : natDegree (R := R) ((expand R p : (a : R[X]) → R[X]) 0) = natDegree.{u} (R := R) 0 * p
pos₁ : natDegree.{u} (R := R) 0 = natDegree.{u} (R := R) 0 * p
pos₂ : 0 = 0 * p
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have pos₃ : Eq (α := ℕ) 0 0
Tactic: rw [hf, map_zero, natDegree_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
Tactic: have hf1 : expand R p f ≠ 0 := mt (expand_eq_zero hp).1 hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = f.natDegree * p
have neg : degree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = (↑(f.natDegree * p) : WithBot ℕ)
Tactic: rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hf1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ degree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = (↑(f.natDegree * p) : WithBot ℕ)
have neg : ∀ (n : ℕ) (hn : LT.lt (α := WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ) (↑n : WithBot ℕ)),
  Eq.{u + 1} (α := R) (coeff ((expand R p : (a : R[X]) → R[X]) f) n) 0
Tactic: refine le_antisymm ((degree_le_iff_coeff_zero _ _).2 fun n hn => ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
neg :
  ∀ (n : ℕ) (hn : LT.lt (α := WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ) (↑n : WithBot ℕ)),
    Eq.{u + 1} (α := R) (coeff ((expand R p : (a : R[X]) → R[X]) f) n) 0
⊢ degree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f) = (↑(f.natDegree * p) : WithBot ℕ)
have neg₁ : (↑(f.natDegree * p) : WithBot ℕ) ≤ degree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f)
Tactic: refine le_antisymm ((degree_le_iff_coeff_zero _ _).2 fun n hn => ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hn : LT.lt (α := WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ) (↑n : WithBot ℕ)
⊢ Eq.{u + 1} (α := R) (coeff ((expand R p : (a : R[X]) → R[X]) f) n) 0
have neg : (if p ∣ n then f.coeff (n / p) else 0) = 0
Tactic: rw [coeff_expand hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hn : LT.lt (α := WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ) (↑n : WithBot ℕ)
⊢ (if p ∣ n then f.coeff (n / p) else 0) = 0
have pos : ∀ (hpn : p ∣ n), f.coeff (n / p) = 0
Tactic: split_ifs with hpn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hn : LT.lt (α := WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ) (↑n : WithBot ℕ)
pos : ∀ (hpn : p ∣ n), f.coeff (n / p) = 0
⊢ (if p ∣ n then f.coeff (n / p) else 0) = 0
have neg : ∀ (hpn : ¬p ∣ n), Eq.{u + 1} (α := R) 0 0
Tactic: split_ifs with hpn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hn : LT.lt (α := WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ) (↑n : WithBot ℕ)
hpn : p ∣ n
⊢ f.coeff (n / p) = 0
have pos : f.natDegree < n / p
Tactic: rw [coeff_eq_zero_of_natDegree_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hn : LT.lt (α := WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ) (↑n : WithBot ℕ)
hpn : p ∣ n
⊢ f.natDegree < n / p
have pos : ∀ (hn : n / p ≤ f.natDegree), LE.le (α := WithBot ℕ) (↑n : WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ)
Tactic: contrapose! hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
⊢ LE.le (α := WithBot ℕ) (↑n : WithBot ℕ) (↑(f.natDegree * p) : WithBot ℕ)
have pos : n ≤ f.natDegree * p
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
n : ℕ
hpn : p ∣ n
hn : n / p ≤ f.natDegree
⊢ n ≤ f.natDegree * p
have pos : n / p * p ≤ f.natDegree * p
Tactic: rw [← Nat.div_mul_cancel hpn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ (↑(f.natDegree * p) : WithBot ℕ) ≤ degree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f)
have neg : Ne.{u + 1} (α := R) (coeff ((expand R p : (a : R[X]) → R[X]) f) (f.natDegree * p)) 0
Tactic: refine le_degree_of_ne_zero ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : Ne (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ Ne.{u + 1} (α := R) (coeff ((expand R p : (a : R[X]) → R[X]) f) (f.natDegree * p)) 0
have neg : f.leadingCoeff ≠ 0
Tactic: rw [coeff_expand_mul hp, ← leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
⊢ leadingCoeff ((expand R p : (a : R[X]) → R[X]) f) = f.leadingCoeff
have simp_rw : coeff ((expand R p : (a : R[X]) → R[X]) f) (natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f)) =
  f.coeff f.natDegree
Tactic: simp_rw [leadingCoeff, natDegree_expand, coeff_expand_mul hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
simp_rw :
  coeff ((expand R p : (a : R[X]) → R[X]) f) (natDegree.{u} (R := R) ((expand R p : (a : R[X]) → R[X]) f)) =
    f.coeff f.natDegree
⊢ leadingCoeff ((expand R p : (a : R[X]) → R[X]) f) = f.leadingCoeff
have simp_rw₁ : coeff ((expand R p : (a : R[X]) → R[X]) f) (f.natDegree * p) = f.coeff f.natDegree
Tactic: simp_rw [leadingCoeff, natDegree_expand, coeff_expand_mul hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
⊢ map f ((expand R p : (a : R[X]) → R[X]) q) = (expand S p : (a : S[X]) → S[X]) (map f q)
have pos : ∀ (hp : p = 0), map f ((expand R p : (a : R[X]) → R[X]) q) = (expand S p : (a : S[X]) → S[X]) (map f q)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
pos : ∀ (hp : p = 0), map f ((expand R p : (a : R[X]) → R[X]) q) = (expand S p : (a : S[X]) → S[X]) (map f q)
⊢ map f ((expand R p : (a : R[X]) → R[X]) q) = (expand S p : (a : S[X]) → S[X]) (map f q)
have neg : ∀ (hp : ¬p = 0), map f ((expand R p : (a : R[X]) → R[X]) q) = (expand S p : (a : S[X]) → S[X]) (map f q)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
⊢ map f ((expand R p : (a : R[X]) → R[X]) q) = (expand S p : (a : S[X]) → S[X]) (map f q)
have neg : ∀ (n : ℕ), (map f ((expand R p : (a : R[X]) → R[X]) q)).coeff n = coeff ((expand S p : (a : S[X]) → S[X]) (map f q)) n
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n : ℕ
⊢ (map f ((expand R p : (a : R[X]) → R[X]) q)).coeff n = coeff ((expand S p : (a : S[X]) → S[X]) (map f q)) n
have neg : (f : (a : R) → S) (if p ∣ n then q.coeff (n / p) else 0) = if p ∣ n then (map f q).coeff (n / p) else 0
Tactic: rw [coeff_map, coeff_expand (Nat.pos_of_ne_zero hp), coeff_expand (Nat.pos_of_ne_zero hp)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n : ℕ
⊢ (f : (a : R) → S) (if p ∣ n then q.coeff (n / p) else 0) = if p ∣ n then (map f q).coeff (n / p) else 0
have pos : p ∣ n → (f : (a : R) → S) (q.coeff (n / p)) = (map f q).coeff (n / p)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n : ℕ
pos : p ∣ n → (f : (a : R) → S) (q.coeff (n / p)) = (map f q).coeff (n / p)
⊢ (f : (a : R) → S) (if p ∣ n then q.coeff (n / p) else 0) = if p ∣ n then (map f q).coeff (n / p) else 0
have neg : ¬p ∣ n → Eq.{v + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
P : R[X]
r : R
⊢ eval r ((expand R p : (a : R[X]) → R[X]) P) = eval (r ^ p) P
have refine : ∀ (f g : R[X]) (hf : eval r ((expand R p : (a : R[X]) → R[X]) f) = eval (r ^ p) f)
  (hg : eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) g),
  eval r ((expand R p : (a : R[X]) → R[X]) (f + g)) = eval (r ^ p) (f + g)
Tactic: refine Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => ?_) fun n a _ => by simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p : (a : R[X]) → R[X]) f) = eval (r ^ p) f
hg : eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) g
⊢ eval r ((expand R p : (a : R[X]) → R[X]) (f + g)) = eval (r ^ p) (f + g)
have rw : eval r
    (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
      ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
  eval (r ^ p) (f + g)
Tactic: rw [map_add, eval_add, eval_add, hf, hg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p : (a : R[X]) → R[X]) f) = eval (r ^ p) f
hg : eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) g
rw :
  eval r
      (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
        ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
    eval (r ^ p) (f + g)
⊢ eval r ((expand R p : (a : R[X]) → R[X]) (f + g)) = eval (r ^ p) (f + g)
have rw₁ : eval r ((expand R p : (a : R[X]) → R[X]) f) + eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) (f + g)
Tactic: rw [map_add, eval_add, eval_add, hf, hg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p : (a : R[X]) → R[X]) f) = eval (r ^ p) f
hg : eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) g
rw :
  eval r
      (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
        ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
    eval (r ^ p) (f + g)
rw₁ : eval r ((expand R p : (a : R[X]) → R[X]) f) + eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) (f + g)
⊢ eval r ((expand R p : (a : R[X]) → R[X]) (f + g)) = eval (r ^ p) (f + g)
have rw₂ : eval r ((expand R p : (a : R[X]) → R[X]) f) + eval r ((expand R p : (a : R[X]) → R[X]) g) =
  eval (r ^ p) f + eval (r ^ p) g
Tactic: rw [map_add, eval_add, eval_add, hf, hg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p : (a : R[X]) → R[X]) f) = eval (r ^ p) f
hg : eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) g
rw :
  eval r
      (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
        ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
    eval (r ^ p) (f + g)
rw₁ : eval r ((expand R p : (a : R[X]) → R[X]) f) + eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) (f + g)
rw₂ :
  eval r ((expand R p : (a : R[X]) → R[X]) f) + eval r ((expand R p : (a : R[X]) → R[X]) g) =
    eval (r ^ p) f + eval (r ^ p) g
⊢ eval r ((expand R p : (a : R[X]) → R[X]) (f + g)) = eval (r ^ p) (f + g)
have rw₃ : eval (r ^ p) f + eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) f + eval (r ^ p) g
Tactic: rw [map_add, eval_add, eval_add, hf, hg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p : (a : R[X]) → R[X]) f) = eval (r ^ p) f
hg : eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) g
rw :
  eval r
      (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
        ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
    eval (r ^ p) (f + g)
rw₁ : eval r ((expand R p : (a : R[X]) → R[X]) f) + eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) (f + g)
rw₂ :
  eval r ((expand R p : (a : R[X]) → R[X]) f) + eval r ((expand R p : (a : R[X]) → R[X]) g) =
    eval (r ^ p) f + eval (r ^ p) g
rw₃ : eval (r ^ p) f + eval r ((expand R p : (a : R[X]) → R[X]) g) = eval (r ^ p) f + eval (r ^ p) g
⊢ eval r ((expand R p : (a : R[X]) → R[X]) (f + g)) = eval (r ^ p) (f + g)
have rw₄ : eval (r ^ p) f + eval (r ^ p) g = eval (r ^ p) f + eval (r ^ p) g
Tactic: rw [map_add, eval_add, eval_add, hf, hg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type u_1
inst_1 : Semiring A
inst_2 : Algebra R A
p : ℕ
P : R[X]
r : A
⊢ Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) P : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) P : A)
have refine : ∀ (f g : R[X])
  (hf :
    Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
      ((aeval (r ^ p) : (a : R[X]) → A) f : A))
  (hg :
    Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A)
      ((aeval (r ^ p) : (a : R[X]) → A) g : A)),
  Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) (f + g) : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)
Tactic: refine Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => ?_) fun n a _ => by simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type u_1
inst_1 : Semiring A
inst_2 : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf :
  Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) f : A)
hg :
  Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) g : A)
⊢ Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) (f + g) : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)
have rw : Eq.{u_1 + 1} (α := A)
  ((aeval r : (a : R[X]) → A)
      (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
        ((expand R p : (a : R[X]) → R[X]) g : R[X])) :
    A)
  ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)
Tactic: rw [map_add, aeval_add, aeval_add, hf, hg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type u_1
inst_1 : Semiring A
inst_2 : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf :
  Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) f : A)
hg :
  Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) g : A)
rw :
  Eq.{u_1 + 1} (α := A)
    ((aeval r : (a : R[X]) → A)
        (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
          ((expand R p : (a : R[X]) → R[X]) g : R[X])) :
      A)
    ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)
⊢ Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) (f + g) : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)
have rw₁ : HAdd.hAdd (α := A) (β := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
    ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A) =
  (aeval (r ^ p) : (a : R[X]) → A) (f + g)
Tactic: rw [map_add, aeval_add, aeval_add, hf, hg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type u_1
inst_1 : Semiring A
inst_2 : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf :
  Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) f : A)
hg :
  Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) g : A)
rw :
  Eq.{u_1 + 1} (α := A)
    ((aeval r : (a : R[X]) → A)
        (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
          ((expand R p : (a : R[X]) → R[X]) g : R[X])) :
      A)
    ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)
rw₁ :
  HAdd.hAdd (α := A) (β := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
      ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A) =
    (aeval (r ^ p) : (a : R[X]) → A) (f + g)
⊢ Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) (f + g) : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)
have rw₂ : HAdd.hAdd (α := A) (β := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
    ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A) =
  HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A) ((aeval (r ^ p) : (a : R[X]) → A) g : A)
Tactic: rw [map_add, aeval_add, aeval_add, hf, hg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type u_1
inst_1 : Semiring A
inst_2 : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf :
  Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) f : A)
hg :
  Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) g : A)
rw :
  Eq.{u_1 + 1} (α := A)
    ((aeval r : (a : R[X]) → A)
        (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
          ((expand R p : (a : R[X]) → R[X]) g : R[X])) :
      A)
    ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)
rw₁ :
  HAdd.hAdd (α := A) (β := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
      ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A) =
    (aeval (r ^ p) : (a : R[X]) → A) (f + g)
rw₂ :
  HAdd.hAdd (α := A) (β := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
      ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A) =
    HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A) ((aeval (r ^ p) : (a : R[X]) → A) g : A)
⊢ Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) (f + g) : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)
have rw₃ : HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A)
    ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A) =
  HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A) ((aeval (r ^ p) : (a : R[X]) → A) g : A)
Tactic: rw [map_add, aeval_add, aeval_add, hf, hg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type u_1
inst_1 : Semiring A
inst_2 : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf :
  Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) f : A)
hg :
  Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) g : A)
rw :
  Eq.{u_1 + 1} (α := A)
    ((aeval r : (a : R[X]) → A)
        (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
          ((expand R p : (a : R[X]) → R[X]) g : R[X])) :
      A)
    ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)
rw₁ :
  HAdd.hAdd (α := A) (β := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
      ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A) =
    (aeval (r ^ p) : (a : R[X]) → A) (f + g)
rw₂ :
  HAdd.hAdd (α := A) (β := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) f : R[X]) : A)
      ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A) =
    HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A) ((aeval (r ^ p) : (a : R[X]) → A) g : A)
rw₃ :
  HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A)
      ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) g : R[X]) : A) =
    HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A) ((aeval (r ^ p) : (a : R[X]) → A) g : A)
⊢ Eq.{u_1 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((expand R p : (a : R[X]) → R[X]) (f + g) : R[X]) : A)
    ((aeval (r ^ p) : (a : R[X]) → A) (f + g) : A)
have rw₄ : HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A) ((aeval (r ^ p) : (a : R[X]) → A) g : A) =
  HAdd.hAdd (α := A) (β := A) ((aeval (r ^ p) : (a : R[X]) → A) f : A) ((aeval (r ^ p) : (a : R[X]) → A) g : A)
Tactic: rw [map_add, aeval_add, aeval_add, hf, hg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ (contract p f).coeff n = f.coeff (n * p)
have simp : f.natDegree + 1 ≤ n → 0 = f.coeff (n * p)
Tactic: simp only [contract, coeff_monomial, sum_ite_eq', finsetSum_coeff, mem_range, not_lt,
    ite_eq_left_iff]