awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
S : Type u_1
inst_1 : SMulZeroClass S R
inst_2 : SMulZeroClass.{u_1, u} Sᵐᵒᵖ R
inst_3 : IsCentralScalar S R
m_1 : S
toFinsupp : R[ℕ]
⊢ MulOpposite.op m_1 • { toFinsupp := toFinsupp : R[X] } = m_1 • { toFinsupp := toFinsupp : R[X] }
have simp_rw : { toFinsupp := MulOpposite.op m_1 • toFinsupp : R[X] } = { toFinsupp := m_1 • toFinsupp }
Tactic: simp_rw [← ofFinsupp_smul, op_smul_eq_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Module S R
inst_3 : IsTorsionFree S R
s : S
hs : IsRegular s
f g : R[ℕ]
hfg : Eq.{u + 1} (α := R[X]) ((fun (x : R[X]) ↦ s • x) { toFinsupp := f }) ((fun (x : R[X]) ↦ s • x) { toFinsupp := g })
⊢ { toFinsupp := f : R[X] } = { toFinsupp := g }
have e_toFinsupp : f = g
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Module S R
inst_3 : IsTorsionFree S R
s : S
hs : IsRegular s
f g : R[ℕ]
hfg : Eq.{u + 1} (α := R[X]) ((fun (x : R[X]) ↦ s • x) { toFinsupp := f }) ((fun (x : R[X]) ↦ s • x) { toFinsupp := g })
⊢ f = g
have e_toFinsupp : Eq.{u + 1} (α := R[ℕ]) ((fun (x : R[ℕ]) ↦ s • x) f) ((fun (x : R[ℕ]) ↦ s • x) g)
Tactic: apply hs.isSMulRegular
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
inst_1 : Subsingleton R
x : R[ℕ]
⊢ { toFinsupp := x : R[X] } = default
have apply : x = 0
Tactic: apply congr_arg ofFinsupp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[ℕ]
⊢ { toFinsupp := p : R[X] }.support = p.support
have rw : p.support = p.support
Tactic: rw [support]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.toFinsupp.support = p.support
have rw : p.toFinsupp.support = p.toFinsupp.support
Tactic: rw [support]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.support = ∅ ↔ p = 0
have rcases : ∀ (toFinsupp : R[ℕ]), { toFinsupp := toFinsupp : R[X] }.support = ∅ ↔ { toFinsupp := toFinsupp : R[X] } = 0
Tactic: rcases p with ⟨⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
k : ℕ
⊢ HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) k = (monomial (n * k) : (a : R) → R[X]) (r ^ k)
have zero : HPow.hPow (α := R[X]) (β := ℕ) ((monomial n : (a : R) → R[X]) r : R[X]) 0 =
  (monomial (n * 0) : (a : R) → R[X]) (HPow.hPow (β := ℕ) r 0)
Tactic: induction k with
  | zero => simp [pow_zero, monomial_zero_one]
  | succ k ih => simp [pow_succ, ih, monomial_mul_monomial, mul_add, add_comm]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
k : ℕ
zero :
  HPow.hPow (α := R[X]) (β := ℕ) ((monomial n : (a : R) → R[X]) r : R[X]) 0 =
    (monomial (n * 0) : (a : R) → R[X]) (HPow.hPow (β := ℕ) r 0)
⊢ HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) k = (monomial (n * k) : (a : R) → R[X]) (r ^ k)
have succ : ∀ (k : ℕ)
  (ih : HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) k = (monomial (n * k) : (a : R) → R[X]) (r ^ k)),
  HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (k + 1) =
    (monomial (n * (k + 1)) : (a : R) → R[X]) (r ^ (k + 1))
Tactic: induction k with
  | zero => simp [pow_zero, monomial_zero_one]
  | succ k ih => simp [pow_succ, ih, monomial_mul_monomial, mul_add, add_comm]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
m n : ℕ
a b : R
⊢ Eq (α := R[X]) ((monomial m : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X]) ↔
    m = n ∧ a = b ∨ a = 0 ∧ b = 0
have rw : Eq.{u + 1} (α := R[ℕ]) (toFinsupp ((monomial m : (a : R) → R[X]) a)) (toFinsupp ((monomial n : (a : R) → R[X]) b)) ↔
  m = n ∧ a = b ∨ a = 0 ∧ b = 0
Tactic: rw [← toFinsupp_inj, toFinsupp_monomial, toFinsupp_monomial, Finsupp.single_eq_single_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
m n : ℕ
a b : R
rw :
  Eq.{u + 1} (α := R[ℕ]) (toFinsupp ((monomial m : (a : R) → R[X]) a)) (toFinsupp ((monomial n : (a : R) → R[X]) b)) ↔
    m = n ∧ a = b ∨ a = 0 ∧ b = 0
⊢ Eq (α := R[X]) ((monomial m : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X]) ↔
    m = n ∧ a = b ∨ a = 0 ∧ b = 0
have rw₁ : Eq (α := R[ℕ]) (single m a) (toFinsupp ((monomial n : (a : R) → R[X]) b)) ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
Tactic: rw [← toFinsupp_inj, toFinsupp_monomial, toFinsupp_monomial, Finsupp.single_eq_single_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
m n : ℕ
a b : R
rw :
  Eq.{u + 1} (α := R[ℕ]) (toFinsupp ((monomial m : (a : R) → R[X]) a)) (toFinsupp ((monomial n : (a : R) → R[X]) b)) ↔
    m = n ∧ a = b ∨ a = 0 ∧ b = 0
rw₁ : Eq (α := R[ℕ]) (single m a) (toFinsupp ((monomial n : (a : R) → R[X]) b)) ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
⊢ Eq (α := R[X]) ((monomial m : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X]) ↔
    m = n ∧ a = b ∨ a = 0 ∧ b = 0
have rw₂ : Eq (α := R[ℕ]) (single m a) (single n b) ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
Tactic: rw [← toFinsupp_inj, toFinsupp_monomial, toFinsupp_monomial, Finsupp.single_eq_single_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
m n : ℕ
a b : R
rw :
  Eq.{u + 1} (α := R[ℕ]) (toFinsupp ((monomial m : (a : R) → R[X]) a)) (toFinsupp ((monomial n : (a : R) → R[X]) b)) ↔
    m = n ∧ a = b ∨ a = 0 ∧ b = 0
rw₁ : Eq (α := R[ℕ]) (single m a) (toFinsupp ((monomial n : (a : R) → R[X]) b)) ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
rw₂ : Eq (α := R[ℕ]) (single m a) (single n b) ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
⊢ Eq (α := R[X]) ((monomial m : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X]) ↔
    m = n ∧ a = b ∨ a = 0 ∧ b = 0
have rw₃ : m = n ∧ a = b ∨ a = 0 ∧ b = 0 ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
Tactic: rw [← toFinsupp_inj, toFinsupp_monomial, toFinsupp_monomial, Finsupp.single_eq_single_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
ih : (monomial n : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n
⊢ (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X (n + 1)
have succ : (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n * X
Tactic: rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
ih : (monomial n : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n
succ : (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n * X
⊢ (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X (n + 1)
have succ₁ : (monomial (n + 1) : (a : R) → R[X]) 1 = HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) 1) X
Tactic: rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
ih : (monomial n : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n
succ : (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n * X
succ₁ : (monomial (n + 1) : (a : R) → R[X]) 1 = HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) 1) X
⊢ (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X (n + 1)
have succ₂ : (monomial (n + 1) : (a : R) → R[X]) 1 =
  HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) 1) ((monomial 1 : (a : R) → R[X]) 1)
Tactic: rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
ih : (monomial n : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n
succ : (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n * X
succ₁ : (monomial (n + 1) : (a : R) → R[X]) 1 = HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) 1) X
succ₂ :
  (monomial (n + 1) : (a : R) → R[X]) 1 =
    HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) 1) ((monomial 1 : (a : R) → R[X]) 1)
⊢ (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X (n + 1)
have succ₃ : Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) 1 : R[X])
  ((monomial (n + 1) : (a : R) → R[X]) (HMul.hMul (α := R) 1 1) : R[X])
Tactic: rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
ih : (monomial n : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n
succ : (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n * X
succ₁ : (monomial (n + 1) : (a : R) → R[X]) 1 = HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) 1) X
succ₂ :
  (monomial (n + 1) : (a : R) → R[X]) 1 =
    HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) 1) ((monomial 1 : (a : R) → R[X]) 1)
succ₃ :
  Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) 1 : R[X])
    ((monomial (n + 1) : (a : R) → R[X]) (HMul.hMul (α := R) 1 1) : R[X])
⊢ (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X (n + 1)
have succ₄ : Eq.{u + 1} (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) 1) ((monomial (n + 1) : (a : R) → R[X]) 1)
Tactic: rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ (monomial n : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n
have zero : (monomial 0 : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) (β := ℕ) X 0
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
zero : (monomial 0 : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) (β := ℕ) X 0
⊢ (monomial n : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n
have succ : ∀ (n : ℕ) (ih : (monomial n : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n),
  (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ X * p = p * X
have rcases : ∀ (toFinsupp : R[ℕ]), X * { toFinsupp := toFinsupp : R[X] } = { toFinsupp := toFinsupp : R[X] } * X
Tactic: rcases p with ⟨⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
toFinsupp : R[ℕ]
⊢ X * { toFinsupp := toFinsupp : R[X] } = { toFinsupp := toFinsupp : R[X] } * X
have simp : single 1 1 * toFinsupp = toFinsupp * single 1 1
Tactic: simp only [X, ← ofFinsupp_single, ← ofFinsupp_mul, ofFinsupp.injEq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
toFinsupp : R[ℕ]
⊢ single 1 1 * toFinsupp = toFinsupp * single 1 1
have hfg : ∀ (m : ℕ), Eq (α := R) ((single 1 1 * toFinsupp : (a : ℕ) → R) m : R) ((toFinsupp * single 1 1 : (a : ℕ) → R) m : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n
| HPow.hPow (α := R[X]) X (n + 1) * p
have rw : HPow.hPow (α := R[X]) X n * X * p
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n
⊢ HPow.hPow (α := R[X]) X (n + 1) * p = p * HPow.hPow (α := R[X]) X (n + 1)
have succ : HPow.hPow (α := R[X]) X n * X * p = p * HPow.hPow (α := R[X]) X (n + 1)
Tactic: conv_lhs => rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n
⊢ HPow.hPow (α := R[X]) X n * X * p = p * HPow.hPow (α := R[X]) X (n + 1)
have succ : HPow.hPow (α := R[X]) X n * (X * p) = p * HPow.hPow (α := R[X]) X (n + 1)
Tactic: rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n
succ : HPow.hPow (α := R[X]) X n * (X * p) = p * HPow.hPow (α := R[X]) X (n + 1)
⊢ HPow.hPow (α := R[X]) X n * X * p = p * HPow.hPow (α := R[X]) X (n + 1)
have succ₁ : HPow.hPow (α := R[X]) X n * (p * X) = p * HPow.hPow (α := R[X]) X (n + 1)
Tactic: rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n
succ : HPow.hPow (α := R[X]) X n * (X * p) = p * HPow.hPow (α := R[X]) X (n + 1)
succ₁ : HPow.hPow (α := R[X]) X n * (p * X) = p * HPow.hPow (α := R[X]) X (n + 1)
⊢ HPow.hPow (α := R[X]) X n * X * p = p * HPow.hPow (α := R[X]) X (n + 1)
have succ₂ : HPow.hPow (α := R[X]) X n * p * X = p * HPow.hPow (α := R[X]) X (n + 1)
Tactic: rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n
succ : HPow.hPow (α := R[X]) X n * (X * p) = p * HPow.hPow (α := R[X]) X (n + 1)
succ₁ : HPow.hPow (α := R[X]) X n * (p * X) = p * HPow.hPow (α := R[X]) X (n + 1)
succ₂ : HPow.hPow (α := R[X]) X n * p * X = p * HPow.hPow (α := R[X]) X (n + 1)
⊢ HPow.hPow (α := R[X]) X n * X * p = p * HPow.hPow (α := R[X]) X (n + 1)
have succ₃ : p * HPow.hPow (α := R[X]) X n * X = p * HPow.hPow (α := R[X]) X (n + 1)
Tactic: rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n
succ : HPow.hPow (α := R[X]) X n * (X * p) = p * HPow.hPow (α := R[X]) X (n + 1)
succ₁ : HPow.hPow (α := R[X]) X n * (p * X) = p * HPow.hPow (α := R[X]) X (n + 1)
succ₂ : HPow.hPow (α := R[X]) X n * p * X = p * HPow.hPow (α := R[X]) X (n + 1)
succ₃ : p * HPow.hPow (α := R[X]) X n * X = p * HPow.hPow (α := R[X]) X (n + 1)
⊢ HPow.hPow (α := R[X]) X n * X * p = p * HPow.hPow (α := R[X]) X (n + 1)
have succ₄ : p * (HPow.hPow (α := R[X]) X n * X) = p * HPow.hPow (α := R[X]) X (n + 1)
Tactic: rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n
succ : HPow.hPow (α := R[X]) X n * (X * p) = p * HPow.hPow (α := R[X]) X (n + 1)
succ₁ : HPow.hPow (α := R[X]) X n * (p * X) = p * HPow.hPow (α := R[X]) X (n + 1)
succ₂ : HPow.hPow (α := R[X]) X n * p * X = p * HPow.hPow (α := R[X]) X (n + 1)
succ₃ : p * HPow.hPow (α := R[X]) X n * X = p * HPow.hPow (α := R[X]) X (n + 1)
succ₄ : p * (HPow.hPow (α := R[X]) X n * X) = p * HPow.hPow (α := R[X]) X (n + 1)
⊢ HPow.hPow (α := R[X]) X n * X * p = p * HPow.hPow (α := R[X]) X (n + 1)
have succ₅ : p * HPow.hPow (α := R[X]) X (n + 1) = p * HPow.hPow (α := R[X]) X (n + 1)
Tactic: rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n
have zero : HPow.hPow (α := R[X]) (β := ℕ) X 0 * p = p * HPow.hPow (α := R[X]) (β := ℕ) X 0
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    conv_lhs => rw [pow_succ]
    rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
zero : HPow.hPow (α := R[X]) (β := ℕ) X 0 * p = p * HPow.hPow (α := R[X]) (β := ℕ) X 0
⊢ HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n
have succ : ∀ (n : ℕ) (ih : HPow.hPow (α := R[X]) X n * p = p * HPow.hPow (α := R[X]) X n),
  HPow.hPow (α := R[X]) X (n + 1) * p = p * HPow.hPow (α := R[X]) X (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    conv_lhs => rw [pow_succ]
    rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
⊢ p * HPow.hPow (α := R[X]) X n * q = p * q * HPow.hPow (α := R[X]) X n
have rw : p * (HPow.hPow (α := R[X]) X n * q) = p * q * HPow.hPow (α := R[X]) X n
Tactic: rw [mul_assoc, X_pow_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
rw : p * (HPow.hPow (α := R[X]) X n * q) = p * q * HPow.hPow (α := R[X]) X n
⊢ p * HPow.hPow (α := R[X]) X n * q = p * q * HPow.hPow (α := R[X]) X n
have rw₁ : p * (q * HPow.hPow (α := R[X]) X n) = p * q * HPow.hPow (α := R[X]) X n
Tactic: rw [mul_assoc, X_pow_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
rw : p * (HPow.hPow (α := R[X]) X n * q) = p * q * HPow.hPow (α := R[X]) X n
rw₁ : p * (q * HPow.hPow (α := R[X]) X n) = p * q * HPow.hPow (α := R[X]) X n
⊢ p * HPow.hPow (α := R[X]) X n * q = p * q * HPow.hPow (α := R[X]) X n
have rw₂ : p * q * HPow.hPow (α := R[X]) X n = p * q * HPow.hPow (α := R[X]) X n
Tactic: rw [mul_assoc, X_pow_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) X = (monomial (n + 1) : (a : R) → R[X]) r
have rw : HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) ((monomial 1 : (a : R) → R[X]) 1 : R[X]) =
  (monomial (n + 1) : (a : R) → R[X]) r
Tactic: rw [X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
rw :
  HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) ((monomial 1 : (a : R) → R[X]) 1 : R[X]) =
    (monomial (n + 1) : (a : R) → R[X]) r
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) X = (monomial (n + 1) : (a : R) → R[X]) r
have rw₁ : Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) (r * 1) : R[X]) ((monomial (n + 1) : (a : R) → R[X]) r : R[X])
Tactic: rw [X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
rw :
  HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) ((monomial 1 : (a : R) → R[X]) 1 : R[X]) =
    (monomial (n + 1) : (a : R) → R[X]) r
rw₁ : Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) (r * 1) : R[X]) ((monomial (n + 1) : (a : R) → R[X]) r : R[X])
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) X = (monomial (n + 1) : (a : R) → R[X]) r
have rw₂ : Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) r : R[X]) ((monomial (n + 1) : (a : R) → R[X]) r : R[X])
Tactic: rw [X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
k : ℕ
⊢ HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k) =
    (monomial (n + k) : (a : R) → R[X]) r
have zero : HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0) =
  (monomial (n + 0) : (a : R) → R[X]) r
Tactic: induction k with
  | zero => simp
  | succ k ih => simp [ih, pow_succ, ← mul_assoc, add_assoc]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
k : ℕ
zero :
  HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0) =
    (monomial (n + 0) : (a : R) → R[X]) r
⊢ HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k) =
    (monomial (n + k) : (a : R) → R[X]) r
have succ : ∀ (k : ℕ)
  (ih :
    HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k) =
      (monomial (n + k) : (a : R) → R[X]) r),
  HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (k + 1)) =
    (monomial (n + (k + 1)) : (a : R) → R[X]) r
Tactic: induction k with
  | zero => simp
  | succ k ih => simp [ih, pow_succ, ← mul_assoc, add_assoc]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
⊢ HMul.hMul (α := R[X]) (β := R[X]) X ((monomial n : (a : R) → R[X]) r : R[X]) = (monomial (n + 1) : (a : R) → R[X]) r
have rw : HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) X = (monomial (n + 1) : (a : R) → R[X]) r
Tactic: rw [X_mul, monomial_mul_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
rw :
  HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) X = (monomial (n + 1) : (a : R) → R[X]) r
⊢ HMul.hMul (α := R[X]) (β := R[X]) X ((monomial n : (a : R) → R[X]) r : R[X]) = (monomial (n + 1) : (a : R) → R[X]) r
have rw₁ : Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) r : R[X]) ((monomial (n + 1) : (a : R) → R[X]) r : R[X])
Tactic: rw [X_mul, monomial_mul_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
k n : ℕ
r : R
⊢ HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) X k) ((monomial n : (a : R) → R[X]) r : R[X]) =
    (monomial (n + k) : (a : R) → R[X]) r
have rw : HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k) =
  (monomial (n + k) : (a : R) → R[X]) r
Tactic: rw [X_pow_mul, monomial_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
k n : ℕ
r : R
rw :
  HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k) =
    (monomial (n + k) : (a : R) → R[X]) r
⊢ HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) X k) ((monomial n : (a : R) → R[X]) r : R[X]) =
    (monomial (n + k) : (a : R) → R[X]) r
have rw₁ : Eq (α := R[X]) ((monomial (n + k) : (a : R) → R[X]) r : R[X]) ((monomial (n + k) : (a : R) → R[X]) r : R[X])
Tactic: rw [X_pow_mul, monomial_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[ℕ]
⊢ { toFinsupp := p : R[X] }.coeff = (⇑p : (a : ℕ) → R)
have rw : Eq (α := ℕ → R) (⇑p : (a : ℕ) → R) (⇑p : (a : ℕ) → R)
Tactic: rw [coeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
i : ℕ
⊢ (f.toFinsupp : (a : ℕ) → R) i = f.coeff i
have ofFinsupp : ∀ (toFinsupp : R[ℕ]),
  ({ toFinsupp := toFinsupp : R[X] }.toFinsupp : (a : ℕ) → R) i = { toFinsupp := toFinsupp : R[X] }.coeff i
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Eq.{u + 1} (α := R) (coeff 1 n) (if n = 0 then 1 else 0)
have simp_rw : Eq.{u + 1} (α := R) (coeff 1 n) (if 0 = n then 1 else 0)
Tactic: simp_rw [eq_comm (a := n) (b := 0)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : n ≠ 1
⊢ Eq.{u + 1} (α := R) (coeff X n) 0
have rw : Eq.{u + 1} (α := R) (if 1 = n then 1 else 0) 0
Tactic: rw [coeff_X, if_neg hn.symm]