awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
p q : MvPolynomial σ R
h_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) p
h_2 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) q
hp :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
    n • p
hq :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R) =
    n • q
refine_3 :
  ∑ x : σ,
      w x •
        (X x *
          HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • (p + q)
refine_3₁ :
  ∑ x : σ,
      w x •
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) +
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • (p + q)
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q) : MvPolynomial σ R) =
    n • (p + q)
have refine_3₂ : ∑ x : σ,
    (w x •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) +
      w x •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
  n • p + n • q
Tactic: simp_rw [map_add, left_distrib, smul_add, sum_add_distrib, hp, hq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
p q : MvPolynomial σ R
h_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) p
h_2 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) q
hp :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
    n • p
hq :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R) =
    n • q
refine_3 :
  ∑ x : σ,
      w x •
        (X x *
          HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • (p + q)
refine_3₁ :
  ∑ x : σ,
      w x •
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) +
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • (p + q)
refine_3₂ :
  ∑ x : σ,
      (w x •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) +
        w x •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • p + n • q
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q) : MvPolynomial σ R) =
    n • (p + q)
have refine_3₃ : HAdd.hAdd (α := MvPolynomial σ R)
    (∑ x : σ,
      w x •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R))
    (∑ x : σ,
      w x •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
  n • p + n • q
Tactic: simp_rw [map_add, left_distrib, smul_add, sum_add_distrib, hp, hq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
p q : MvPolynomial σ R
h_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) p
h_2 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) q
hp :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
    n • p
hq :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R) =
    n • q
refine_3 :
  ∑ x : σ,
      w x •
        (X x *
          HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • (p + q)
refine_3₁ :
  ∑ x : σ,
      w x •
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) +
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • (p + q)
refine_3₂ :
  ∑ x : σ,
      (w x •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) +
        w x •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • p + n • q
refine_3₃ :
  HAdd.hAdd (α := MvPolynomial σ R)
      (∑ x : σ,
        w x •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R))
      (∑ x : σ,
        w x •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • p + n • q
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q) : MvPolynomial σ R) =
    n • (p + q)
have refine_3₄ : n • p +
    ∑ x : σ,
      w x •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R) =
  n • p + n • q
Tactic: simp_rw [map_add, left_distrib, smul_add, sum_add_distrib, hp, hq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
r : R
p : MvPolynomial σ R
h_2 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) p
h :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
    n • p
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (r • p) : MvPolynomial σ R) =
    n • r • p
have refine_4 : ∑ x : σ,
    w x •
      (X x *
        HSMul.hSMul (β := MvPolynomial σ R) r
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
  n • r • p
Tactic: simp_rw [(pderiv _).map_smul, nsmul_eq_mul, mul_smul_comm, ← Finset.smul_sum, ← nsmul_eq_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
r : R
p : MvPolynomial σ R
h_2 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) p
h :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
    n • p
refine_4 :
  ∑ x : σ,
      w x •
        (X x *
          HSMul.hSMul (β := MvPolynomial σ R) r
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    n • r • p
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (r • p) : MvPolynomial σ R) =
    n • r • p
have refine_4₁ : ∑ x : σ,
    (↑(w x) : MvPolynomial σ R) *
      (X x *
        HSMul.hSMul (β := MvPolynomial σ R) r
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
  (↑n : MvPolynomial σ R) * r • p
Tactic: simp_rw [(pderiv _).map_smul, nsmul_eq_mul, mul_smul_comm, ← Finset.smul_sum, ← nsmul_eq_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
r : R
p : MvPolynomial σ R
h_2 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) p
h :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
    n • p
refine_4 :
  ∑ x : σ,
      w x •
        (X x *
          HSMul.hSMul (β := MvPolynomial σ R) r
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    n • r • p
refine_4₁ :
  ∑ x : σ,
      (↑(w x) : MvPolynomial σ R) *
        (X x *
          HSMul.hSMul (β := MvPolynomial σ R) r
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    (↑n : MvPolynomial σ R) * r • p
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (r • p) : MvPolynomial σ R) =
    n • r • p
have refine_4₂ : ∑ x : σ,
    r •
      ((↑(w x) : MvPolynomial σ R) *
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
  r • ((↑n : MvPolynomial σ R) * p)
Tactic: simp_rw [(pderiv _).map_smul, nsmul_eq_mul, mul_smul_comm, ← Finset.smul_sum, ← nsmul_eq_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
r : R
p : MvPolynomial σ R
h_2 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) p
h :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
    n • p
refine_4 :
  ∑ x : σ,
      w x •
        (X x *
          HSMul.hSMul (β := MvPolynomial σ R) r
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    n • r • p
refine_4₁ :
  ∑ x : σ,
      (↑(w x) : MvPolynomial σ R) *
        (X x *
          HSMul.hSMul (β := MvPolynomial σ R) r
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    (↑n : MvPolynomial σ R) * r • p
refine_4₂ :
  ∑ x : σ,
      r •
        ((↑(w x) : MvPolynomial σ R) *
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    r • ((↑n : MvPolynomial σ R) * p)
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (r • p) : MvPolynomial σ R) =
    n • r • p
have refine_4₃ : HSMul.hSMul (β := MvPolynomial σ R) r
    (∑ x : σ,
      (↑(w x) : MvPolynomial σ R) *
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
  r • ((↑n : MvPolynomial σ R) * p)
Tactic: simp_rw [(pderiv _).map_smul, nsmul_eq_mul, mul_smul_comm, ← Finset.smul_sum, ← nsmul_eq_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
r : R
p : MvPolynomial σ R
h_2 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) p
h :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
    n • p
refine_4 :
  ∑ x : σ,
      w x •
        (X x *
          HSMul.hSMul (β := MvPolynomial σ R) r
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    n • r • p
refine_4₁ :
  ∑ x : σ,
      (↑(w x) : MvPolynomial σ R) *
        (X x *
          HSMul.hSMul (β := MvPolynomial σ R) r
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    (↑n : MvPolynomial σ R) * r • p
refine_4₂ :
  ∑ x : σ,
      r •
        ((↑(w x) : MvPolynomial σ R) *
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    r • ((↑n : MvPolynomial σ R) * p)
refine_4₃ :
  HSMul.hSMul (β := MvPolynomial σ R) r
      (∑ x : σ,
        (↑(w x) : MvPolynomial σ R) *
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
    r • ((↑n : MvPolynomial σ R) * p)
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (r • p) : MvPolynomial σ R) =
    n • r • p
have refine_4₄ : HSMul.hSMul (β := MvPolynomial σ R) r
    (∑ x : σ,
      w x •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
          ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)) =
  r • n • p
Tactic: simp_rw [(pderiv _).map_smul, nsmul_eq_mul, mul_smul_comm, ← Finset.smul_sum, ← nsmul_eq_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
h : φ.IsHomogeneous n
⊢ ∑ i : σ,
      HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R) =
    n • φ
have simp_rw : Eq (α := MvPolynomial σ R)
  (∑ i : σ,
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R))
  (∑ i : σ,
    HSMul.hSMul (α := ℕ) (1 i)
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)))
Tactic: simp_rw [← h.sum_weight_X_mul_pderiv, Pi.one_apply, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.EulerIdentity (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
h : φ.IsHomogeneous n
simp_rw :
  Eq (α := MvPolynomial σ R)
    (∑ i : σ,
      HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R))
    (∑ i : σ,
      HSMul.hSMul (α := ℕ) (1 i)
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)))
⊢ ∑ i : σ,
      HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
        ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R) =
    n • φ
have simp_rw₁ : Eq (α := MvPolynomial σ R)
  (∑ i : σ,
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
      ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R))
  (∑ x : σ,
    HSMul.hSMul (α := ℕ) 1
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
        ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) φ : MvPolynomial σ R)))
Tactic: simp_rw [← h.sum_weight_X_mul_pderiv, Pi.one_apply, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f x x_1 : MvPolynomial σ R
ha :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x) =
    x ^ p
hb :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) =
    x_1 ^ p
⊢ (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (x + x_1)) =
    (x + x_1) ^ p
have rw : (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
    (HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)) =
  (x + x_1) ^ p
Tactic: rw [map_add, map_add, ha, hb, add_pow_expChar]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f x x_1 : MvPolynomial σ R
ha :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x) =
    x ^ p
hb :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) =
    x_1 ^ p
rw :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)) =
    (x + x_1) ^ p
⊢ (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (x + x_1)) =
    (x + x_1) ^ p
have rw₁ : HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x) :
      MvPolynomial σ R)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) :
      MvPolynomial σ R) =
  (x + x_1) ^ p
Tactic: rw [map_add, map_add, ha, hb, add_pow_expChar]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Expand (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f x x_1 : MvPolynomial σ R
ha :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x) =
    x ^ p
hb :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) =
    x_1 ^ p
rw :
  (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      (HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x : MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1 : MvPolynomial σ R)) =
    (x + x_1) ^ p
rw₁ :
  HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x) :
        MvPolynomial σ R)
      ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) :
        MvPolynomial σ R) =
    (x + x_1) ^ p
⊢ (map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) (x + x_1)) =
    (x + x_1) ^ p
have rw₂ : HAdd.hAdd (β := MvPolynomial σ R) (x ^ p)
    ((map (frobenius R p) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand p : (a : MvPolynomial σ R) → MvPolynomial σ R) x_1) :
      MvPolynomial σ R) =
  (x + x_1) ^ p
Tactic: rw [map_add, map_add, ha, hb, add_pow_expChar]