awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
⊢ g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b =
    (↑isunit_gb.unit⁻¹ : R) •
      (HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b) - m.degree (g b')) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b)) :
            MvPolynomial σ R)
          (g b') -
        HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b') - m.degree (g b)) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b')) :
            MvPolynomial σ R)
          (g b))
have inl : ∀ (h : m.degree (g b') = m.degree (g b)),
  g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b =
    (↑isunit_gb.unit⁻¹ : R) •
      (HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b) - m.degree (g b')) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b)) :
            MvPolynomial σ R)
          (g b') -
        HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b') - m.degree (g b)) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b')) :
            MvPolynomial σ R)
          (g b))
Tactic: obtain (⟨h, -⟩ | h) := hd b' hb'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd :
  LT.lt.{u_4} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b + ∑ b ∈ B, g b)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)
h :
  ∀ (hd : ∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0)
    (hfd :
      LT.lt.{u_4} (α := m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) : m.syn)),
    ∃ (c : ι → ι → R),
      Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
inl :
  ∀ (h : m.degree (g b') = m.degree (g b)),
    g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b =
      (↑isunit_gb.unit⁻¹ : R) •
        (HMul.hMul (α := MvPolynomial σ R)
            ((monomial (m.degree (g b) - m.degree (g b')) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b)) :
              MvPolynomial σ R)
            (g b') -
          HMul.hMul (α := MvPolynomial σ R)
            ((monomial (m.degree (g b') - m.degree (g b)) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b')) :
              MvPolynomial σ R)
            (g b))
⊢ g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b =
    (↑isunit_gb.unit⁻¹ : R) •
      (HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b) - m.degree (g b')) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b)) :
            MvPolynomial σ R)
          (g b') -
        HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b') - m.degree (g b)) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b')) :
            MvPolynomial σ R)
          (g b))
have inr : ∀ (h : g b' = 0),
  g b' - (m.leadingCoeff (g b') * (↑isunit_gb.unit⁻¹ : R)) • g b =
    (↑isunit_gb.unit⁻¹ : R) •
      (HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b) - m.degree (g b')) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b)) :
            MvPolynomial σ R)
          (g b') -
        HMul.hMul (α := MvPolynomial σ R)
          ((monomial (m.degree (g b') - m.degree (g b)) : (a : R) → MvPolynomial σ R) (m.leadingCoeff (g b')) :
            MvPolynomial σ R)
          (g b))
Tactic: obtain (⟨h, -⟩ | h) := hd b' hb'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
B : Finset ι
g : ι → MvPolynomial σ R
hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d
⊢ ∃ (c : ι → ι → R),
    Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
have empty : ∀
  (hd :
    ∀ (b : ι),
      Membership.mem (γ := Finset ι) ∅ b →
        (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
  (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ ∅, g b)) < d),
  ∃ (c : ι → ι → R),
    Eq (α := MvPolynomial σ R) (∑ b ∈ ∅, g b) (∑ b₁ ∈ ∅, ∑ b₂ ∈ ∅, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
Tactic: induction B using Finset.induction_on with
  | empty => simp
  | insert b B hb h =>
    by_cases hb0 : g b = 0
    · simp_all
    simp? [Finset.sum_insert hb, hb0] at hfd hd says
      simp only [Finset.sum_insert hb, Finset.mem_insert, forall_eq_or_imp, hb0, or_false]
        at hfd hd
    obtain ⟨⟨rfl, isunit_gb⟩, hd⟩ := hd
    use fun b₁ b₂ ↦ if b₂ = b then ↑isunit_gb.unit⁻¹ else 0
    simp? [Finset.sum_insert hb, hb] says
      simp only [Finset.sum_insert hb, ite_smul, zero_smul, ↓reduceIte, Finset.sum_ite_eq', hb,
        add_zero, sPolynomial_self, smul_zero, zero_add]
    simp only [m.toSyn.injective.eq_iff] at *
    trans ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * ↑isunit_gb.unit⁻¹) • g b)
    · suffices (-(∑ i ∈ B, m.leadingCoeff (g i))) = m.leadingCoeff (g b) by
        rw [add_comm, Finset.sum_sub_distrib, sub_eq_add_neg, ← Finset.sum_smul, ← Finset.sum_mul,
          ← neg_smul, ← neg_mul, this, isunit_gb.mul_val_inv, one_smul]
      rw [← add_eq_zero_iff_neg_eq']
      trans (g b).coeff (m.degree <| g b) + ∑ i ∈ B, (g i).coeff (m.degree <| g b)
      · unfold leadingCoeff
        congr 1
        apply Finset.sum_congr rfl
        intro b' hb'
        rcases hd b' hb' with h | h <;> simp [h]
      · rw [← coeff_sum, ← coeff_add, ← notMem_support_iff]
        exact m.notMem_support_of_degree_lt hfd
    · apply Finset.sum_congr rfl
      intro b' hb'
      rw [sPolynomial]
      obtain (⟨h, -⟩ | h) := hd b' hb' <;>
        simp [h, ← smul_eq_C_mul, smul_sub, ← mul_smul, mul_comm (m.leadingCoeff (g b'))]
Cleared hypotheses: B, hd, hfd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : CommRing R
d : m.syn
ι : Type u_3
B : Finset ι
g : ι → MvPolynomial σ R
hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d
⊢ ∃ (c : ι → ι → R),
    Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
have empty : ∀
  (hd :
    ∀ (b : ι),
      Membership.mem (γ := Finset ι) ∅ b →
        (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
  (hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ ∅, g b)) < d),
  ∃ (c : ι → ι → R),
    Eq (α := MvPolynomial σ R) (∑ b ∈ ∅, g b) (∑ b₁ ∈ ∅, ∑ b₂ ∈ ∅, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
Tactic: classical
  induction B using Finset.induction_on with
  | empty => simp
  | insert b B hb h =>
    by_cases hb0 : g b = 0
    · simp_all
    simp? [Finset.sum_insert hb, hb0] at hfd hd says
      simp only [Finset.sum_insert hb, Finset.mem_insert, forall_eq_or_imp, hb0, or_false]
        at hfd hd
    obtain ⟨⟨rfl, isunit_gb⟩, hd⟩ := hd
    use fun b₁ b₂ ↦ if b₂ = b then ↑isunit_gb.unit⁻¹ else 0
    simp? [Finset.sum_insert hb, hb] says
      simp only [Finset.sum_insert hb, ite_smul, zero_smul, ↓reduceIte, Finset.sum_ite_eq', hb,
        add_zero, sPolynomial_self, smul_zero, zero_add]
    simp only [m.toSyn.injective.eq_iff] at *
    trans ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * ↑isunit_gb.unit⁻¹) • g b)
    · suffices (-(∑ i ∈ B, m.leadingCoeff (g i))) = m.leadingCoeff (g b) by
        rw [add_comm, Finset.sum_sub_distrib, sub_eq_add_neg, ← Finset.sum_smul, ← Finset.sum_mul,
          ← neg_smul, ← neg_mul, this, isunit_gb.mul_val_inv, one_smul]
      rw [← add_eq_zero_iff_neg_eq']
      trans (g b).coeff (m.degree <| g b) + ∑ i ∈ B, (g i).coeff (m.degree <| g b)
      · unfold leadingCoeff
        congr 1
        apply Finset.sum_congr rfl
        intro b' hb'
        rcases hd b' hb' with h | h <;> simp [h]
      · rw [← coeff_sum, ← coeff_add, ← notMem_support_iff]
        exact m.notMem_support_of_degree_lt hfd
    · apply Finset.sum_congr rfl
      intro b' hb'
      rw [sPolynomial]
      obtain (⟨h, -⟩ | h) := hd b' hb' <;>
        simp [h, ← smul_eq_C_mul, smul_sub, ← mul_smul, mul_comm (m.leadingCoeff (g b'))]
Cleared hypotheses: B, hd, hfd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_4} σ
R : Type u_2
inst : Field R
d : m.syn
ι : Type u_3
B : Finset ι
g : ι → MvPolynomial σ R
hd : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∨ g b = 0
hfd : (m.toSyn : (a : σ →₀ ℕ) → m.syn) (degree.{u_1, u_2, u_4} m (R := R) (∑ b ∈ B, g b)) < d
⊢ ∃ (c : ι → ι → R),
    Eq (α := MvPolynomial σ R) (∑ b ∈ B, g b) (∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂))
have refine : ∀ b ∈ B, (m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0
Tactic: refine m.sPolynomial_decomposition ?_ hfd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
⊢ m.degree
      (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
        ((C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R)) =
    single i 1
have rw : LT.lt.{u_4} (α := m.syn)
  ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) ((C : (a : R) → MvPolynomial ι R) r)) : m.syn)
  ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) (X i)) : m.syn)
Tactic: rw [degree_add_of_lt, degree_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
⊢ LT.lt.{u_4} (α := m.syn)
    ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) ((C : (a : R) → MvPolynomial ι R) r)) : m.syn)
    ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) (X i)) : m.syn)
have simp : LT.lt.{u_4} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (single i 1) : m.syn)
Tactic: simp only [degree_C, map_zero, degree_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
⊢ LT.lt.{u_4} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (single i 1) : m.syn)
have rw : Ne.{u_4 + 1} (α := m.syn) ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (single i 1) : m.syn)
  ((m.toSyn : (a : ι →₀ ℕ) → m.syn) 0 : m.syn)
Tactic: rw [← bot_eq_zero, bot_lt_iff_ne_bot, bot_eq_zero, ← map_zero m.toSyn]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
⊢ m.degree
      (HSub.hSub (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
        ((C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R)) =
    single i 1
have rw : m.degree
    (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
      (-(C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R)) =
  single i 1
Tactic: rw [sub_eq_add_neg, ← map_neg, degree_X_add_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
rw :
  m.degree
      (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
        (-(C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R)) =
    single i 1
⊢ m.degree
      (HSub.hSub (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
        ((C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R)) =
    single i 1
have rw₁ : m.degree
    (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
      ((C : (a : R) → MvPolynomial ι R) (-r) : MvPolynomial ι R)) =
  single i 1
Tactic: rw [sub_eq_add_neg, ← map_neg, degree_X_add_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
rw :
  m.degree
      (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
        (-(C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R)) =
    single i 1
rw₁ :
  m.degree
      (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
        ((C : (a : R) → MvPolynomial ι R) (-r) : MvPolynomial ι R)) =
    single i 1
⊢ m.degree
      (HSub.hSub (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
        ((C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R)) =
    single i 1
have rw₂ : Eq (α := ι →₀ ℕ) (single i 1) (single i 1)
Tactic: rw [sub_eq_add_neg, ← map_neg, degree_X_add_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
⊢ m.Monic
    (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
      ((C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R))
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
h : Nontrivial R
⊢ m.Monic
    (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
      ((C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R))
have apply : LT.lt.{u_4} (α := m.syn)
  ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) ((C : (a : R) → MvPolynomial ι R) r)) : m.syn)
  ((m.toSyn : (a : ι →₀ ℕ) → m.syn) (degree.{u_3, u_2, u_4} m (R := R) (X i)) : m.syn)
Tactic: apply monic_X.add_of_lt
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
m : MonomialOrder.{u_3, u_4} ι
i : ι
r : R
⊢ m.Monic
    (HSub.hSub (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
      ((C : (a : R) → MvPolynomial ι R) r : MvPolynomial ι R))
have rw : m.Monic
  (HAdd.hAdd (α := MvPolynomial ι R) (β := MvPolynomial ι R) (X i)
    ((C : (a : R) → MvPolynomial ι R) (-r) : MvPolynomial ι R))
Tactic: rw [sub_eq_add_neg, ← map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
σ : Type u_2
f : σ → R
s : Finset σ
n : ℕ
⊢ (map f s.val).esymm n = ∑ t ∈ Finset.powersetCard n s, t.prod f
have simp : Eq.{u_1 + 1} (α := R)
  (sum
    (map ((fun (x : Multiset R) ↦ x.prod) ∘ (fun (x : Multiset σ) ↦ map f x) ∘ Finset.val)
      (Finset.powersetCard n s).val))
  (∑ t ∈ Finset.powersetCard n s, t.prod f)
Tactic: simp only [esymm, powersetCard_map, ← Finset.map_val_val_powersetCard, map_map]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ s ^ n • m.esymm n = esymm (map (fun (x : R) ↦ s • x) m) n
have rw : Eq (α := R) (sum (map ((fun (x : R) ↦ s ^ n • x) ∘ prod) (powersetCard n m))) (esymm (map (fun (x : R) ↦ s • x) m) n)
Tactic: rw [esymm, smul_sum, map_map]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ Eq (α := R) (sum (map ((fun (x : R) ↦ s ^ n • x) ∘ prod) (powersetCard n m))) (esymm (map (fun (x : R) ↦ s • x) m) n)
have trans : Eq (α := R) (sum (map ((fun (x : R) ↦ s ^ n • x) ∘ prod) (powersetCard n m)))
  (sum (map (fun (x : Multiset R) ↦ s ^ x.card • x.prod) (powersetCard n m)))
Tactic: trans ((powersetCard n m).map (fun x : Multiset R ↦ s ^ card x • x.prod)).sum
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
trans :
  Eq (α := R) (sum (map ((fun (x : R) ↦ s ^ n • x) ∘ prod) (powersetCard n m)))
    (sum (map (fun (x : Multiset R) ↦ s ^ x.card • x.prod) (powersetCard n m)))
⊢ Eq (α := R) (sum (map ((fun (x : R) ↦ s ^ n • x) ∘ prod) (powersetCard n m))) (esymm (map (fun (x : R) ↦ s • x) m) n)
have trans₁ : Eq (α := R) (sum (map (fun (x : Multiset R) ↦ s ^ x.card • x.prod) (powersetCard n m)))
  (esymm (map (fun (x : R) ↦ s • x) m) n)
Tactic: trans ((powersetCard n m).map (fun x : Multiset R ↦ s ^ card x • x.prod)).sum
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ Eq (α := R) (sum (map ((fun (x : R) ↦ s ^ n • x) ∘ prod) (powersetCard n m)))
    (sum (map (fun (x : Multiset R) ↦ s ^ x.card • x.prod) (powersetCard n m)))
have refine : ∀ (x : Multiset R) (hx : x ∈ powersetCard n m), ((fun (x : R) ↦ s ^ n • x) ∘ prod) x = s ^ x.card • x.prod
Tactic: refine congr_arg _ (map_congr rfl (fun x hx ↦ ?_))
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m x : Multiset R
hx : x ∈ powersetCard n m
⊢ ((fun (x : R) ↦ s ^ n • x) ∘ prod) x = s ^ x.card • x.prod
have rw : s ^ n • x.prod = s ^ x.card • x.prod
Tactic: rw [Function.comp_apply, (mem_powersetCard.1 hx).2]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m x : Multiset R
hx : x ∈ powersetCard n m
rw : s ^ n • x.prod = s ^ x.card • x.prod
⊢ ((fun (x : R) ↦ s ^ n • x) ∘ prod) x = s ^ x.card • x.prod
have rw₁ : s ^ n • x.prod = s ^ n • x.prod
Tactic: rw [Function.comp_apply, (mem_powersetCard.1 hx).2]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ Eq (α := R) (sum (map (fun (x : Multiset R) ↦ s ^ x.card • x.prod) (powersetCard n m)))
    (esymm (map (fun (x : R) ↦ s • x) m) n)
have simp_rw : Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
  (esymm (map (fun (x : R) ↦ s • x) m) n)
Tactic: simp_rw [smul_prod, esymm, powersetCard_map, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
simp_rw :
  Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
    (esymm (map (fun (x : R) ↦ s • x) m) n)
⊢ Eq (α := R) (sum (map (fun (x : Multiset R) ↦ s ^ x.card • x.prod) (powersetCard n m)))
    (esymm (map (fun (x : R) ↦ s • x) m) n)
have simp_rw₁ : Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
  (sum (map prod (powersetCard n (map (fun (x : R) ↦ s • x) m))))
Tactic: simp_rw [smul_prod, esymm, powersetCard_map, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
simp_rw :
  Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
    (esymm (map (fun (x : R) ↦ s • x) m) n)
simp_rw₁ :
  Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
    (sum (map prod (powersetCard n (map (fun (x : R) ↦ s • x) m))))
⊢ Eq (α := R) (sum (map (fun (x : Multiset R) ↦ s ^ x.card • x.prod) (powersetCard n m)))
    (esymm (map (fun (x : R) ↦ s • x) m) n)
have simp_rw₂ : Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
  (sum (map (fun (x : Multiset R) ↦ x.prod) (map (map fun (x : R) ↦ s • x) (powersetCard n m))))
Tactic: simp_rw [smul_prod, esymm, powersetCard_map, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
simp_rw :
  Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
    (esymm (map (fun (x : R) ↦ s • x) m) n)
simp_rw₁ :
  Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
    (sum (map prod (powersetCard n (map (fun (x : R) ↦ s • x) m))))
simp_rw₂ :
  Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
    (sum (map (fun (x : Multiset R) ↦ x.prod) (map (map fun (x : R) ↦ s • x) (powersetCard n m))))
⊢ Eq (α := R) (sum (map (fun (x : Multiset R) ↦ s ^ x.card • x.prod) (powersetCard n m)))
    (esymm (map (fun (x : R) ↦ s • x) m) n)
have simp_rw₃ : Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
  (sum (map ((fun (x : Multiset R) ↦ x.prod) ∘ map fun (x : R) ↦ s • x) (powersetCard n m)))
Tactic: simp_rw [smul_prod, esymm, powersetCard_map, map_map, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ_1 : Type u_1
τ : Type u_2
R_1 : Type u_3
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) (setOf IsSymmetric) a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) (setOf IsSymmetric) b
e : Perm σ
⊢ (rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) (a * b) = a * b
have rw : HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) b : MvPolynomial σ R) =
  a * b
Tactic: rw [map_mul, ha, hb]