awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
this : a + b = i
ha : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s
⊢ Membership.mem (α := MvPolynomial σ R)
    (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
    ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
have hb : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) b ≤ t
Tactic: have hb : b.toMultiset ≤ t := by simp [b, Multiset.inter_le_right]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x
i : σ →₀ ℕ
hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t
a : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ)
    (HSub.hSub (α := Multiset σ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i : Multiset σ) t)
b : σ →₀ ℕ :=
  (Multiset.toFinsupp : (a : Multiset σ) → σ →₀ ℕ) ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ⊓ t : Multiset σ)
this : a + b = i
ha : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) a ≤ s
hb : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) b ≤ t
⊢ Membership.mem (α := MvPolynomial σ R)
    (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
    ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
have rw : HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((monomial a : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
    ((monomial b : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) ∈
  HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t)
Tactic: rw [show monomial i (x.coeff i) = monomial a (x.coeff i) * monomial b 1 by simp [this]]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) = HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t)
have rw : degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
  HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ≤ degreesLE R σ (s + t)
Tactic: classical
  rw [le_antisymm_iff, Submodule.mul_le]
  refine ⟨fun x hx ↦ x.as_sum ▸ sum_mem fun i hi ↦ ?_,
    fun x hx y hy ↦ degrees_mul_le.trans (add_le_add hx hy)⟩
  replace hi : i.toMultiset ≤ s + t := (Finset.le_sup hi).trans hx
  let a := (i.toMultiset - t).toFinsupp
  let b := (i.toMultiset ⊓ t).toFinsupp
  have : a + b = i := Multiset.toFinsupp.symm.injective (by simp [a, b, Multiset.sub_add_inter])
  have ha : a.toMultiset ≤ s := by simpa [a, add_comm (a := t)] using hi
  have hb : b.toMultiset ≤ t := by simp [b, Multiset.inter_le_right]
  rw [show monomial i (x.coeff i) = monomial a (x.coeff i) * monomial b 1 by simp [this]]
  exact Submodule.mul_mem_mul ((degrees_monomial _ _).trans ha) ((degrees_monomial _ _).trans hb)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
rw :
  degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
    HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ≤ degreesLE R σ (s + t)
⊢ degreesLE R σ (s + t) = HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t)
have rw₁ : degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
  ∀ (m : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) m →
      ∀ (n : MvPolynomial σ R),
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ t) n →
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) (m * n)
Tactic: classical
  rw [le_antisymm_iff, Submodule.mul_le]
  refine ⟨fun x hx ↦ x.as_sum ▸ sum_mem fun i hi ↦ ?_,
    fun x hx y hy ↦ degrees_mul_le.trans (add_le_add hx hy)⟩
  replace hi : i.toMultiset ≤ s + t := (Finset.le_sup hi).trans hx
  let a := (i.toMultiset - t).toFinsupp
  let b := (i.toMultiset ⊓ t).toFinsupp
  have : a + b = i := Multiset.toFinsupp.symm.injective (by simp [a, b, Multiset.sub_add_inter])
  have ha : a.toMultiset ≤ s := by simpa [a, add_comm (a := t)] using hi
  have hb : b.toMultiset ≤ t := by simp [b, Multiset.inter_le_right]
  rw [show monomial i (x.coeff i) = monomial a (x.coeff i) * monomial b 1 by simp [this]]
  exact Submodule.mul_mem_mul ((degrees_monomial _ _).trans ha) ((degrees_monomial _ _).trans hb)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
rw :
  degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
    HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ≤ degreesLE R σ (s + t)
rw₁ rw₂ rw₃ :
  degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
    ∀ (m : MvPolynomial σ R),
      Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) m →
        ∀ (n : MvPolynomial σ R),
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ t) n →
            Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) (m * n)
⊢ degreesLE R σ (s + t) = HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t)
have rw₄ : ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x)
  (i : σ →₀ ℕ) (hi : i ∈ x.support),
  Membership.mem (α := MvPolynomial σ R)
    (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
    ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
Tactic: classical
  rw [le_antisymm_iff, Submodule.mul_le]
  refine ⟨fun x hx ↦ x.as_sum ▸ sum_mem fun i hi ↦ ?_,
    fun x hx y hy ↦ degrees_mul_le.trans (add_le_add hx hy)⟩
  replace hi : i.toMultiset ≤ s + t := (Finset.le_sup hi).trans hx
  let a := (i.toMultiset - t).toFinsupp
  let b := (i.toMultiset ⊓ t).toFinsupp
  have : a + b = i := Multiset.toFinsupp.symm.injective (by simp [a, b, Multiset.sub_add_inter])
  have ha : a.toMultiset ≤ s := by simpa [a, add_comm (a := t)] using hi
  have hb : b.toMultiset ≤ t := by simp [b, Multiset.inter_le_right]
  rw [show monomial i (x.coeff i) = monomial a (x.coeff i) * monomial b 1 by simp [this]]
  exact Submodule.mul_mem_mul ((degrees_monomial _ _).trans ha) ((degrees_monomial _ _).trans hb)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : Multiset σ
rw :
  degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
    HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ≤ degreesLE R σ (s + t)
rw₁ rw₂ rw₃ :
  degreesLE R σ (s + t) ≤ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t) ∧
    ∀ (m : MvPolynomial σ R),
      Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) m →
        ∀ (n : MvPolynomial σ R),
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ t) n →
            Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) (m * n)
rw₄ :
  ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x)
    (i : σ →₀ ℕ) (hi : i ∈ x.support),
    Membership.mem (α := MvPolynomial σ R)
      (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
      ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
⊢ degreesLE R σ (s + t) = HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t)
have rw₅ : ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ (s + t)) x)
  (i : σ →₀ ℕ) (hi : (toMultiset : (a : σ →₀ ℕ) → Multiset σ) i ≤ s + t),
  Membership.mem (α := MvPolynomial σ R)
    (HMul.hMul (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ s) (degreesLE R σ t))
    ((monomial i : (a : R) → MvPolynomial σ R) (coeff i x) : MvPolynomial σ R)
Tactic: classical
  rw [le_antisymm_iff, Submodule.mul_le]
  refine ⟨fun x hx ↦ x.as_sum ▸ sum_mem fun i hi ↦ ?_,
    fun x hx y hy ↦ degrees_mul_le.trans (add_le_add hx hy)⟩
  replace hi : i.toMultiset ≤ s + t := (Finset.le_sup hi).trans hx
  let a := (i.toMultiset - t).toFinsupp
  let b := (i.toMultiset ⊓ t).toFinsupp
  have : a + b = i := Multiset.toFinsupp.symm.injective (by simp [a, b, Multiset.sub_add_inter])
  have ha : a.toMultiset ≤ s := by simpa [a, add_comm (a := t)] using hi
  have hb : b.toMultiset ≤ t := by simp [b, Multiset.inter_le_right]
  rw [show monomial i (x.coeff i) = monomial a (x.coeff i) * monomial b 1 by simp [this]]
  exact Submodule.mul_mem_mul ((degrees_monomial _ _).trans ha) ((degrees_monomial _ _).trans hb)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (degreesLE R σ 0) 1
have refine : ∀ (x : MvPolynomial σ R) (hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ 0) x),
  Membership.mem (γ := Submodule R (MvPolynomial σ R)) 1 x
Tactic: refine le_antisymm (fun x hx ↦ ?_) (by simp)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : MvPolynomial σ R
hx : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (degreesLE R σ 0) x
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) 1 x
have hx₁ : x.degrees = 0
Tactic: simp only [mem_degreesLE, nonpos_iff_eq_zero] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
x : MvPolynomial σ R
hx : x.degrees = 0
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) 1 x
have this : x = (C : (a : R) → MvPolynomial σ R) (coeff 0 x)
Tactic: have := (totalDegree_eq_zero_iff_eq_C (p := x)).mp
    (Nat.eq_zero_of_le_zero (x.totalDegree_le_degrees_card.trans (by simp [hx])))
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
⊢ HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) f : A) =
    HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)
have this : HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((D : (a : MvPolynomial σ R) → A) f : A) =
  (D : (a : MvPolynomial σ R) → A)
    (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f)
Tactic: have : C (σ := σ) a • D f = D (C a * f) := by simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
this :
  HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) f : A) =
    (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f)
⊢ HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) f : A) =
    HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)
have rw : (D : (a : MvPolynomial σ R) → A)
    (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f) =
  HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)
Tactic: rw [this, C_mul', D.map_smul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
this :
  HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) f : A) =
    (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f)
rw :
  (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f) =
    HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)
⊢ HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) f : A) =
    HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)
have rw₁ : (D : (a : MvPolynomial σ R) → A) (a • f) = HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)
Tactic: rw [this, C_mul', D.map_smul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
this :
  HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) f : A) =
    (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f)
rw :
  (D : (a : MvPolynomial σ R) → A)
      (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) f) =
    HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)
rw₁ : (D : (a : MvPolynomial σ R) → A) (a • f) = HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)
⊢ HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((D : (a : MvPolynomial σ R) → A) f : A) =
    HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)
have rw₂ : HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A) =
  HSMul.hSMul (β := A) a ((D : (a : MvPolynomial σ R) → A) f : A)
Tactic: rw [this, C_mul', D.map_smul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
⊢ (∀ (p q : MvPolynomial σ R),
      (D : (a : MvPolynomial σ R) → A) (p * q) =
        HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A) +
          HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A)) ↔
    ∀ (s : σ →₀ ℕ) (i : σ),
      (D : (a : MvPolynomial σ R) → A)
          (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
            ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
          HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
            ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
have refine : ∀
  (H :
    ∀ (s : σ →₀ ℕ) (i : σ),
      (D : (a : MvPolynomial σ R) → A)
          (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
            ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
          HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
            ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A))
  (p q : MvPolynomial σ R),
  (D : (a : MvPolynomial σ R) → A) (p * q) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A) +
      HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A)
Tactic: refine ⟨fun H p i => H _ _, fun H => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
r : R
⊢ Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
    (0 : A)
have rw : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) (HSMul.hSMul (β := MvPolynomial σ R) r 1) : A) (0 : A)
Tactic: rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
r : R
rw : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) (HSMul.hSMul (β := MvPolynomial σ R) r 1) : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
    (0 : A)
have rw₁ : HSMul.hSMul (β := A) r ((D : (a : MvPolynomial σ R) → A) 1 : A) = 0
Tactic: rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
r : R
rw : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) (HSMul.hSMul (β := MvPolynomial σ R) r 1) : A) (0 : A)
rw₁ : HSMul.hSMul (β := A) r ((D : (a : MvPolynomial σ R) → A) 1 : A) = 0
⊢ Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
    (0 : A)
have rw₂ : HSMul.hSMul (β := A) r 0 = 0
Tactic: rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
r : R
rw : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) (HSMul.hSMul (β := MvPolynomial σ R) r 1) : A) (0 : A)
rw₁ : HSMul.hSMul (β := A) r ((D : (a : MvPolynomial σ R) → A) 1 : A) = 0
rw₂ : HSMul.hSMul (β := A) r 0 = 0
⊢ Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
    (0 : A)
have rw₃ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
⊢ ∀ (p q : MvPolynomial σ R),
    (D : (a : MvPolynomial σ R) → A) (p * q) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A) +
        HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A)
have hC : ∀ (r : R),
  Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
    (0 : A)
Tactic: have hC : ∀ r, D (C r) = 0 := by intro r; rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]