awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ
a : R
rw :
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (X s) =
    HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X s) 1)
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (X s) =
    (monomial (Finsupp.single s 1) : (a : R) → MvPolynomial σ R) a
have rw₁ : HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    (X s) =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    (X s)
Tactic: rw [← C_mul_X_pow_eq_monomial, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
a : R
⊢ (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
have rw : (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
Tactic: rw [← monomial_sum_one, C_mul', ← (monomial _).map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
a : R
rw :
  (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
⊢ (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
have rw₁ : (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
  HSMul.hSMul (β := MvPolynomial σ R) a ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) 1)
Tactic: rw [← monomial_sum_one, C_mul', ← (monomial _).map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
a : R
rw :
  (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
rw₁ :
  (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HSMul.hSMul (β := MvPolynomial σ R) a ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) 1)
⊢ (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
have rw₂ : Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
  ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) (HSMul.hSMul (β := R) a 1) : MvPolynomial σ R)
Tactic: rw [← monomial_sum_one, C_mul', ← (monomial _).map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
a : R
rw :
  (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
rw₁ :
  (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HSMul.hSMul (β := MvPolynomial σ R) a ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) 1)
rw₂ :
  Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) (HSMul.hSMul (β := R) a 1) : MvPolynomial σ R)
⊢ (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
have rw₃ : Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
  ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) (a * 1) : MvPolynomial σ R)
Tactic: rw [← monomial_sum_one, C_mul', ← (monomial _).map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
a : R
rw :
  (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
rw₁ :
  (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HSMul.hSMul (β := MvPolynomial σ R) a ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) 1)
rw₂ :
  Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) (HSMul.hSMul (β := R) a 1) : MvPolynomial σ R)
rw₃ :
  Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) (a * 1) : MvPolynomial σ R)
⊢ (monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
have rw₄ : Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
  ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
Tactic: rw [← monomial_sum_one, C_mul', ← (monomial _).map_smul, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
g : α → R
⊢ Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) (∏ i ∈ s, g i))
    (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i))
have simp_rw : HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (∏ i ∈ s, g i))
    (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1) =
  ∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i)
Tactic: simp_rw [monomial_sum_index, map_prod, ← Finset.prod_mul_distrib, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
g : α → R
simp_rw :
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (∏ i ∈ s, g i))
      (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1) =
    ∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i)
⊢ Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) (∏ i ∈ s, g i))
    (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i))
have simp_rw₁ : HMul.hMul (α := MvPolynomial σ R) (∏ x ∈ s, (C : (a : R) → MvPolynomial σ R) (g x))
    (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1) =
  ∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i)
Tactic: simp_rw [monomial_sum_index, map_prod, ← Finset.prod_mul_distrib, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
g : α → R
simp_rw :
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (∏ i ∈ s, g i))
      (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1) =
    ∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i)
simp_rw₁ :
  HMul.hMul (α := MvPolynomial σ R) (∏ x ∈ s, (C : (a : R) → MvPolynomial σ R) (g x))
      (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1) =
    ∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i)
⊢ Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) (∏ i ∈ s, g i))
    (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i))
have simp_rw₂ : Eq (α := MvPolynomial σ R)
  (∏ x ∈ s,
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) (g x) : MvPolynomial σ R)
      ((monomial (f x) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R))
  (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i))
Tactic: simp_rw [monomial_sum_index, map_prod, ← Finset.prod_mul_distrib, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
g : α → R
simp_rw :
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (∏ i ∈ s, g i))
      (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1) =
    ∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i)
simp_rw₁ :
  HMul.hMul (α := MvPolynomial σ R) (∏ x ∈ s, (C : (a : R) → MvPolynomial σ R) (g x))
      (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) 1) =
    ∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i)
simp_rw₂ :
  Eq (α := MvPolynomial σ R)
    (∏ x ∈ s,
      HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial σ R) (g x) : MvPolynomial σ R)
        ((monomial (f x) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R))
    (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i))
⊢ Eq (α := MvPolynomial σ R) ((monomial (∑ i ∈ s, f i) : (a : R) → MvPolynomial σ R) (∏ i ∈ s, g i))
    (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i))
have simp_rw₃ : Eq (α := MvPolynomial σ R) (∏ x ∈ s, (monomial (f x) : (a : R) → MvPolynomial σ R) (g x * 1))
  (∏ i ∈ s, (monomial (f i) : (a : R) → MvPolynomial σ R) (g i))
Tactic: simp_rw [monomial_sum_index, map_prod, ← Finset.prod_mul_distrib, C_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : σ → ℕ
t : Finset σ
⊢ Eq (α := MvPolynomial σ R) (∏ y ∈ t, HPow.hPow (α := MvPolynomial σ R) (X y) (x y))
    ((monomial (Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i) : (a : R) → MvPolynomial σ R) 1)
have rw : Eq (α := MvPolynomial σ R) (∏ y ∈ t, HPow.hPow (α := MvPolynomial σ R) (X y) (x y))
  (∏ x_1 ∈ t,
    HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X x_1)
      ((Finsupp.indicator t fun (i : σ) (x_2 : i ∈ t) ↦ x i : (a : σ) → ℕ) x_1 : ℕ))
Tactic: rw [monomial_eq, C_1, one_mul, Finsupp.prod, Finset.prod_subset (support_indicator_subset _ _)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : σ → ℕ
t : Finset σ
rw :
  Eq (α := MvPolynomial σ R) (∏ y ∈ t, HPow.hPow (α := MvPolynomial σ R) (X y) (x y))
    (∏ x_1 ∈ t,
      HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X x_1)
        ((Finsupp.indicator t fun (i : σ) (x_2 : i ∈ t) ↦ x i : (a : σ) → ℕ) x_1 : ℕ))
⊢ Eq (α := MvPolynomial σ R) (∏ y ∈ t, HPow.hPow (α := MvPolynomial σ R) (X y) (x y))
    ((monomial (Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i) : (a : R) → MvPolynomial σ R) 1)
have rw₁ : ∀ x_1 ∈ t,
  x_1 ∉ Finsupp.support (M := ℕ) (Finsupp.indicator t fun (i : σ) (x_2 : i ∈ t) ↦ x i) →
    HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X x_1)
        ((Finsupp.indicator t fun (i : σ) (x_2 : i ∈ t) ↦ x i : (a : σ) → ℕ) x_1 : ℕ) =
      1
Tactic: rw [monomial_eq, C_1, one_mul, Finsupp.prod, Finset.prod_subset (support_indicator_subset _ _)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
hi' : i ∉ Finsupp.support (M := ℕ) (Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i)
⊢ HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i)
      ((Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i : (a : σ) → ℕ) i : ℕ) =
    1
have hi'₁ : Eq (α := ℕ) ((Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: rw [Finsupp.mem_support_iff, ne_eq, not_not] at hi'
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
hi' : Eq (α := ℕ) ((Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i)
      ((Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i : (a : σ) → ℕ) i : ℕ) =
    1
have rw : HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0 = 1
Tactic: rw [hi', pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
hi' : Eq (α := ℕ) ((Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
rw : HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i) 0 = 1
⊢ HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X i)
      ((Finsupp.indicator t fun (i : σ) (x_1 : i ∈ t) ↦ x i : (a : σ) → ℕ) i : ℕ) =
    1
have rw₁ : Eq (α := MvPolynomial σ R) 1 1
Tactic: rw [hi', pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
⊢ motive ((monomial s : (a : R) → MvPolynomial σ R) a)
have zero : motive ((monomial 0 : (a : R) → MvPolynomial σ R) a)
Tactic: apply @Finsupp.induction σ ℕ _ _ s
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
zero : motive ((monomial 0 : (a : R) → MvPolynomial σ R) a)
⊢ motive ((monomial s : (a : R) → MvPolynomial σ R) a)
have single_add : ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
  a_1 ∉ f.support →
    b ≠ 0 →
      motive ((monomial f : (a : R) → MvPolynomial σ R) a) →
        motive ((monomial (Finsupp.single a_1 b + f) : (a : R) → MvPolynomial σ R) a)
Tactic: apply @Finsupp.induction σ ℕ _ _ s
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e_1 : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e_1 ≠ 0
ih : motive ((monomial p : (a : R) → MvPolynomial σ R) a)
e : ℕ
⊢ motive
    (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X n) e))
have zero : motive
  (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X n) 0))
Tactic: induction e with
      | zero => simp [ih]
      | succ e e_ih => simp [pow_succ, (mul_assoc _ _ _).symm, mul_X, e_ih]
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e_1 : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e_1 ≠ 0
ih : motive ((monomial p : (a : R) → MvPolynomial σ R) a)
e : ℕ
zero :
  motive
    (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X n) 0))
⊢ motive
    (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X n) e))
have succ : ∀ (e : ℕ)
  (e_ih :
    motive
      (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        (HPow.hPow (α := MvPolynomial σ R) (X n) e))),
  motive
    (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X n) (e + 1)))
Tactic: induction e with
      | zero => simp [ih]
      | succ e e_ih => simp [pow_succ, (mul_assoc _ _ _).symm, mul_X, e_ih]
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : motive ((monomial p : (a : R) → MvPolynomial σ R) a)
⊢ motive ((monomial (Finsupp.single n e + p) : (a : R) → MvPolynomial σ R) a)
have single_add : ∀
  (this :
    ∀ (e : ℕ),
      motive
        (HMul.hMul (α := MvPolynomial σ R) ((monomial p : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
          (HPow.hPow (α := MvPolynomial σ R) (X n) e))),
  motive ((monomial (Finsupp.single n e + p) : (a : R) → MvPolynomial σ R) a)
Tactic: have : ∀ e : ℕ, motive (monomial p a * X n ^ e) := by
      intro e
      induction e with
      | zero => simp [ih]
      | succ e e_ih => simp [pow_succ, (mul_assoc _ _ _).symm, mul_X, e_ih]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
P : MvPolynomial σ R → Prop
p : MvPolynomial σ R
monomial : ∀ (u : σ →₀ ℕ) (a : R), P ((MvPolynomial.monomial u : (a : R) → MvPolynomial σ R) a)
add : ∀ (p q : MvPolynomial σ R), P p → P q → P (p + q)
this : P ((MvPolynomial.monomial 0 : (a : R) → MvPolynomial σ R) 0)
⊢ P 0
have rwa : ∀ (this : P 0), P 0
Tactic: rwa [monomial_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
f g : MvPolynomial σ R →+* A
hC :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      ((g : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
hX :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) (X i) : A) ((g : (a : MvPolynomial σ R) → A) (X i) : A)
⊢ f = g
have refine_1 : f.comp singleZeroRingHom = g.comp singleZeroRingHom
Tactic: refine AddMonoidAlgebra.ringHom_ext' ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
f g : MvPolynomial σ R →+* A
hC :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      ((g : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
hX :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) (X i) : A) ((g : (a : MvPolynomial σ R) → A) (X i) : A)
refine_1 : f.comp singleZeroRingHom = g.comp singleZeroRingHom
⊢ f = g
have refine_2 : Eq (α := MonoidHom.{u_1, u_2} (Multiplicative (σ →₀ ℕ)) A) (MonoidHom.comp (↑f : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))
  (MonoidHom.comp (↑g : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))
Tactic: refine AddMonoidAlgebra.ringHom_ext' ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
f g : MvPolynomial σ R →+* A
hC :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      ((g : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
hX :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) (X i) : A) ((g : (a : MvPolynomial σ R) → A) (X i) : A)
⊢ f.comp singleZeroRingHom = g.comp singleZeroRingHom
have refine_1 : ∀ (x : R),
  Eq.{u_2 + 1} (α := A) ((f.comp singleZeroRingHom : (a : R) → A) x : A)
    ((g.comp singleZeroRingHom : (a : R) → A) x : A)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Basic (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
f g : MvPolynomial σ R →+* A
hC :
  ∀ (r : R),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      ((g : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
hX :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := A) ((f : (a : MvPolynomial σ R) → A) (X i) : A) ((g : (a : MvPolynomial σ R) → A) (X i) : A)
⊢ Eq (α := MonoidHom.{u_1, u_2} (Multiplicative (σ →₀ ℕ)) A) (MonoidHom.comp (↑f : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))
    (MonoidHom.comp (↑g : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))
have refine_2 : ∀ (x : σ),
  Eq (α := Multiplicative ℕ →* A)
    (MonoidHom.comp (MonoidHom.comp (↑f : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))
      ((AddMonoidHom.toMultiplicative : (a : ℕ →+ σ →₀ ℕ) → Multiplicative ℕ →* Multiplicative (σ →₀ ℕ))
        (Finsupp.singleAddHom x)))
    (MonoidHom.comp (MonoidHom.comp (↑g : R[σ →₀ ℕ] →* A) (of R (σ →₀ ℕ)))
      ((AddMonoidHom.toMultiplicative : (a : ℕ →+ σ →₀ ℕ) → Multiplicative ℕ →* Multiplicative (σ →₀ ℕ))
        (Finsupp.singleAddHom x)))
Tactic: apply Finsupp.mulHom_ext'