awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
⊢ (map (iterateFrobenius R p 0) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (HPow.hPow (β := ℕ) p 0) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ HPow.hPow (β := ℕ) p 0

Tactic:
simp [map_id]

Premises used: MvPolynomial.map_id
-- Module: Mathlib.RingTheory.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ k
succ :
  f ^ p ^ (k + 1) =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)
⊢ (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ (k + 1)

Tactic:
symm
-- Module: Mathlib.RingTheory.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ k
rw :
  HPow.hPow (α := MvPolynomial σ R)
    ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
      MvPolynomial σ R)
    p
| f ^ p ^ (k + 1)

Tactic:
rw [pow_succ, pow_mul, ← n_ih]

Premises used: pow_succ, pow_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih :
  (map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ k
succ :
  HPow.hPow (α := MvPolynomial σ R)
      ((map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) :
        MvPolynomial σ R)
      p =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)
⊢ f ^ p ^ (k + 1) =
    (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f)

Tactic:
conv_lhs => rw [pow_succ, pow_mul, ← n_ih]

Premises used: pow_succ, pow_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Expand
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : MvPolynomial σ R
n : ℕ
zero :
  (map (iterateFrobenius R p 0) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (HPow.hPow (β := ℕ) p 0) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ HPow.hPow (β := ℕ) p 0
succ :
  ∀ (k : ℕ)
    (n_ih :
      (map (iterateFrobenius R p k) : (a : MvPolynomial σ R) → MvPolynomial σ R)
          ((expand (p ^ k) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
        f ^ p ^ k),
    (map (iterateFrobenius R p (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
        ((expand (p ^ (k + 1)) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
      f ^ p ^ (k + 1)
⊢ (map (iterateFrobenius R p n) : (a : MvPolynomial σ R) → MvPolynomial σ R)
      ((expand (p ^ n) : (a : MvPolynomial σ R) → MvPolynomial σ R) f) =
    f ^ p ^ n

Tactic:
induction n with
  | zero => simp [map_id]
  | succ k n_ih =>
    symm
    conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
    simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]

Premises used: MvPolynomial.map_map, MvPolynomial.map_expand, MvPolynomial.map_frobenius_expand, pow_succ, pow_mul, iterateFrobenius_add, MvPolynomial.expand_mul, iterateFrobenius_one, pow_succ', MvPolynomial.map_id
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : (i : ι) × ↥(monoms i) → R
i : ι
⊢ ∀ (a : κ →₀ ℕ),
    a ∈
        {m ∈ monoms i |
          ∃ (hm : m ∈ monoms i),
            p (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm)) ≠
              0} ↔
      Ne.{u_3 + 1} (α := R)
        (if hm : a ∈ monoms i then
          p (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) a hm))
        else 0)
        0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }
a :
  ∀ (i : ι) (m : κ →₀ ℕ),
    coeff m
        ((↑((fun (p : (i : ι) × ↥(monoms i) → R) ↦
                  (Subtype.mk (p := fun (p : ι → MvPolynomial κ R) ↦ ∀ (i : ι), (p i).support ⊆ monoms i)
                      (fun (i : ι) ↦
                        {
                          support :=
                            {m ∈ monoms i |
                              ∃ (hm : m ∈ monoms i),
                                p
                                    (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                                      (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm)) ≠
                                  0},
                          toFun := fun (m : κ →₀ ℕ) ↦
                            if hm : m ∈ monoms i then
                              p
                                (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                                  (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm))
                            else 0,
                          mem_support_toFun := ⋯ })
                      ⋯ :
                    { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }))
                ((fun (p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i })
                      (i : (i : ι) × ↥(monoms i)) ↦
                    coeff (↑(i.snd (β := fun (i : ι) ↦ ↥(monoms i))) : κ →₀ ℕ)
                      ((↑p : ι → MvPolynomial κ R) (i.fst (β := fun (i : ι) ↦ ↥(monoms i)))))
                  p)) :
            ι → MvPolynomial κ R)
          i) =
      coeff m ((↑p : ι → MvPolynomial κ R) i)
⊢ (fun (p : (i : ι) × ↥(monoms i) → R) ↦
        (Subtype.mk (p := fun (p : ι → MvPolynomial κ R) ↦ ∀ (i : ι), (p i).support ⊆ monoms i)
            (fun (i : ι) ↦
              {
                support :=
                  {m ∈ monoms i |
                    ∃ (hm : m ∈ monoms i),
                      p
                          (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                            (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm)) ≠
                        0},
                toFun := fun (m : κ →₀ ℕ) ↦
                  if hm : m ∈ monoms i then
                    p
                      (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                        (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm))
                  else 0,
                mem_support_toFun := ⋯ })
            ⋯ :
          { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }))
      ((fun (p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }) (i : (i : ι) × ↥(monoms i)) ↦
          coeff (↑(i.snd (β := fun (i : ι) ↦ ↥(monoms i))) : κ →₀ ℕ)
            ((↑p : ι → MvPolynomial κ R) (i.fst (β := fun (i : ι) ↦ ↥(monoms i)))))
        p) =
    p

Tactic:
ext i m
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }
i : ι
m : κ →₀ ℕ
a : m ∉ monoms i → Eq.{u_3 + 1} (α := R) (0 : R) (((↑p : ι → MvPolynomial κ R) i : (a : κ →₀ ℕ) → R) m : R)
⊢ coeff m
      ((↑((fun (p : (i : ι) × ↥(monoms i) → R) ↦
                (Subtype.mk (p := fun (p : ι → MvPolynomial κ R) ↦ ∀ (i : ι), (p i).support ⊆ monoms i)
                    (fun (i : ι) ↦
                      {
                        support :=
                          {m ∈ monoms i |
                            ∃ (hm : m ∈ monoms i),
                              p
                                  (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                                    (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm)) ≠
                                0},
                        toFun := fun (m : κ →₀ ℕ) ↦
                          if hm : m ∈ monoms i then
                            p
                              (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                                (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm))
                          else 0,
                        mem_support_toFun := ⋯ })
                    ⋯ :
                  { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }))
              ((fun (p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i })
                    (i : (i : ι) × ↥(monoms i)) ↦
                  coeff (↑(i.snd (β := fun (i : ι) ↦ ↥(monoms i))) : κ →₀ ℕ)
                    ((↑p : ι → MvPolynomial κ R) (i.fst (β := fun (i : ι) ↦ ↥(monoms i)))))
                p)) :
          ι → MvPolynomial κ R)
        i) =
    coeff m ((↑p : ι → MvPolynomial κ R) i)

Tactic:
simp only [coeff, ne_eq, exists_prop, dite_eq_ite, Finsupp.coe_mk, ite_eq_left_iff]

Premises used: ite_eq_left_iff, exists_prop, ne_eq, MvPolynomial.coeff, dite_eq_ite, Finsupp.coe_mk
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }
i : ι
m : κ →₀ ℕ
hm : m ∉ monoms i
⊢ m ∉ ((↑p : ι → MvPolynomial κ R) i).support

Tactic:
have : m ∉ (p.1 i).support := fun h => hm (p.2 i h)
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }
i : ι
m : κ →₀ ℕ
hm : m ∉ monoms i
this : m ∉ ((↑p : ι → MvPolynomial κ R) i).support
⊢ Eq.{u_3 + 1} (α := R) (0 : R) (((↑p : ι → MvPolynomial κ R) i : (a : κ →₀ ℕ) → R) m : R)

Tactic:
simpa [coeff, eq_comm, MvPolynomial.mem_support_iff] using this

Premises used: MvPolynomial.mem_support_iff, eq_comm, MvPolynomial.coeff
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : (i : ι) × ↥(monoms i) → R
h :
  ∀ (x : (i : ι) × ↥(monoms i)),
    (fun (p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }) (i : (i : ι) × ↥(monoms i)) ↦
          coeff (↑(i.snd (β := fun (i : ι) ↦ ↥(monoms i))) : κ →₀ ℕ)
            ((↑p : ι → MvPolynomial κ R) (i.fst (β := fun (i : ι) ↦ ↥(monoms i)))))
        ((fun (p : (i : ι) × ↥(monoms i) → R) ↦
            (Subtype.mk (p := fun (p : ι → MvPolynomial κ R) ↦ ∀ (i : ι), (p i).support ⊆ monoms i)
                (fun (i : ι) ↦
                  {
                    support :=
                      {m ∈ monoms i |
                        ∃ (hm : m ∈ monoms i),
                          p
                              (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                                (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm)) ≠
                            0},
                    toFun := fun (m : κ →₀ ℕ) ↦
                      if hm : m ∈ monoms i then
                        p
                          (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                            (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm))
                      else 0,
                    mem_support_toFun := ⋯ })
                ⋯ :
              { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }))
          p)
        x =
      p x
⊢ (fun (p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }) (i : (i : ι) × ↥(monoms i)) ↦
        coeff (↑(i.snd (β := fun (i : ι) ↦ ↥(monoms i))) : κ →₀ ℕ)
          ((↑p : ι → MvPolynomial κ R) (i.fst (β := fun (i : ι) ↦ ↥(monoms i)))))
      ((fun (p : (i : ι) × ↥(monoms i) → R) ↦
          (Subtype.mk (p := fun (p : ι → MvPolynomial κ R) ↦ ∀ (i : ι), (p i).support ⊆ monoms i)
              (fun (i : ι) ↦
                {
                  support :=
                    {m ∈ monoms i |
                      ∃ (hm : m ∈ monoms i),
                        p
                            (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                              (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm)) ≠
                          0},
                  toFun := fun (m : κ →₀ ℕ) ↦
                    if hm : m ∈ monoms i then
                      p
                        (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                          (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm))
                    else 0,
                  mem_support_toFun := ⋯ })
              ⋯ :
            { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }))
        p) =
    p

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : (i : ι) × ↥(monoms i) → R
x : (i : ι) × ↥(monoms i)
⊢ (fun (p : { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }) (i : (i : ι) × ↥(monoms i)) ↦
        coeff (↑(i.snd (β := fun (i : ι) ↦ ↥(monoms i))) : κ →₀ ℕ)
          ((↑p : ι → MvPolynomial κ R) (i.fst (β := fun (i : ι) ↦ ↥(monoms i)))))
      ((fun (p : (i : ι) × ↥(monoms i) → R) ↦
          (Subtype.mk (p := fun (p : ι → MvPolynomial κ R) ↦ ∀ (i : ι), (p i).support ⊆ monoms i)
              (fun (i : ι) ↦
                {
                  support :=
                    {m ∈ monoms i |
                      ∃ (hm : m ∈ monoms i),
                        p
                            (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                              (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm)) ≠
                          0},
                  toFun := fun (m : κ →₀ ℕ) ↦
                    if hm : m ∈ monoms i then
                      p
                        (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                          (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) m hm))
                    else 0,
                  mem_support_toFun := ⋯ })
              ⋯ :
            { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i }))
        p)
      x =
    p x

Tactic:
simp [coeff]

Premises used: MvPolynomial.coeff
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
p : ι → MvPolynomial κ R
⊢ Eq (α := { p_1 : ι → MvPolynomial κ R // ∀ (i : ι), (p_1 i).support ⊆ (p i).support })
    ((Equiv.symm (mvPolynomialSupportLEEquiv fun (i : ι) ↦ (p i).support) :
        (a : (i : ι) × ↥(p i).support → R) →
          { p_1 : ι → MvPolynomial κ R // ∀ (i : ι), (p_1 i).support ⊆ (p i).support })
      fun (i : (i : ι) × ↥(p i).support) ↦
      coeff (↑(i.snd (β := fun (i : ι) ↦ ↥(p i).support)) : κ →₀ ℕ) (p (i.fst (β := fun (i : ι) ↦ ↥(p i).support))))
    (Subtype.mk (p := fun (p_1 : ι → MvPolynomial κ R) ↦ ∀ (i : ι), (p_1 i).support ⊆ (p i).support) p ⋯)

Tactic:
(mvPolynomialSupportLEEquiv (R := R) (fun i : ι => (p i).support)).symm_apply_apply
    ⟨p, fun _ => Finset.Subset.refl _⟩

Premises used: Equiv.symm_apply_apply, Finset.Subset.refl, MvPolynomial.support, MvPolynomial.coeff, Subtype.mk, FirstOrder.Ring.mvPolynomialSupportLEEquiv
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
simp :
  Eq.{u_3 + 1} (α := R)
    (∑ x ∈ (monoms i).attach,
      HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i x)))
        ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
                FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
              (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
            ((↑x : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
              HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
          R))
    (∑ a ∈ monoms i,
      if
          ∃ (h : a ∈ monoms i),
            ¬f
                  (Sum.inl
                    (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                      (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) a ⋯))) =
                0 then
        HMul.hMul (α := R)
          (if h : a ∈ monoms i then
            f
              (Sum.inl
                (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) a ⋯)))
          else 0)
          (∏ x ∈ a.support, HPow.hPow (β := ℕ) (f (Sum.inr x)) ((a : (a : κ) → ℕ) x : ℕ))
      else 0)
⊢ Eq.{u_3 + 1} (α := R)
    ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
            FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
          (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
        (genericPolyMap monoms i) :
      R)
    ((eval (f ∘ Sum.inr) : (a : MvPolynomial κ R) → R)
        ((↑((Equiv.symm (mvPolynomialSupportLEEquiv monoms) :
                  (a : (i : ι) × ↥(monoms i) → R) → { p : ι → MvPolynomial κ R // ∀ (i : ι), (p i).support ⊆ monoms i })
                (f ∘ Sum.inl)) :
            ι → MvPolynomial κ R)
          i) :
      R)

Tactic:
simp only [genericPolyMap, map_sum, map_mul, lift_of, support,
    mvPolynomialSupportLEEquiv, coeff, Finset.sum_filter, MvPolynomial.eval_eq,
    ne_eq, Function.comp, Equiv.coe_fn_symm_mk, Finsupp.coe_mk]

Premises used: Equiv.coe_fn_symm_mk, FreeCommRing.lift_of, Function.comp, MvPolynomial.eval_eq, map_sum, ne_eq, MvPolynomial.support, MvPolynomial.coeff, map_mul, FirstOrder.Ring.genericPolyMap, FirstOrder.Ring.mvPolynomialSupportLEEquiv, Finsupp.coe_mk, Finset.sum_filter
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
rw :
  ∑ x ∈ (monoms i).attach,
    if
        ∃ (h : (↑x : κ →₀ ℕ) ∈ monoms i),
          ¬f
                (Sum.inl
                  (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                    (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) ⋯))) =
              0 then
      HMul.hMul (α := R)
        (if h : (↑x : κ →₀ ℕ) ∈ monoms i then
          f
            (Sum.inl
              (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) ⋯)))
        else 0)
        (∏ x_1 ∈ (↑x : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x_1)) (((↑x : κ →₀ ℕ) : (a : κ) → ℕ) x_1 : ℕ))
    else 0
| ∑ a ∈ monoms i,
    if
        ∃ (h : a ∈ monoms i),
          ¬f
                (Sum.inl
                  (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                    (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) a ⋯))) =
              0 then
      HMul.hMul (α := R)
        (if h : a ∈ monoms i then
          f
            (Sum.inl
              (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) a ⋯)))
        else 0)
        (∏ x ∈ a.support, HPow.hPow (β := ℕ) (f (Sum.inr x)) ((a : (a : κ) → ℕ) x : ℕ))
    else 0

Tactic:
rw [← Finset.sum_attach]

Premises used: Finset.sum_attach
-- Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst : DecidableEq κ
inst_1 : CommRing R
inst_2 : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
conv_rhs :
  Eq.{u_3 + 1} (α := R)
    (∑ x ∈ (monoms i).attach,
      HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i x)))
        ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
                FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
              (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
            ((↑x : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
              HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
          R))
    (∑ x ∈ (monoms i).attach,
      if
          ∃ (h : (↑x : κ →₀ ℕ) ∈ monoms i),
            ¬f
                  (Sum.inl
                    (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                      (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) ⋯))) =
                0 then
        HMul.hMul (α := R)
          (if h : (↑x : κ →₀ ℕ) ∈ monoms i then
            f
              (Sum.inl
                (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                  (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) (↑x : κ →₀ ℕ) ⋯)))
          else 0)
          (∏ x_1 ∈ (↑x : κ →₀ ℕ).support, HPow.hPow (β := ℕ) (f (Sum.inr x_1)) (((↑x : κ →₀ ℕ) : (a : κ) → ℕ) x_1 : ℕ))
      else 0)
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x ∈ (monoms i).attach,
      HMul.hMul (β := R) (f (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i x)))
        ((((lift : (a : (i : ι) × ↥(monoms i) ⊕ κ → R) → FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) f :
                FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ) →+* R) :
              (a : FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) → R)
            ((↑x : κ →₀ ℕ).prod fun (j : κ) (n : ℕ) ↦
              HPow.hPow (α := FreeCommRing ((i : ι) × ↥(monoms i) ⊕ κ)) (of (Sum.inr j)) n) :
          R))
    (∑ a ∈ monoms i,
      if
          ∃ (h : a ∈ monoms i),
            ¬f
                  (Sum.inl
                    (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i
                      (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) a ⋯))) =
                0 then
        HMul.hMul (α := R)
          (if h : a ∈ monoms i then
            f
              (Sum.inl
                (Sigma.mk (β := fun (i : ι) ↦ ↥(monoms i)) i (Subtype.mk (p := fun (x : κ →₀ ℕ) ↦ x ∈ monoms i) a ⋯)))
          else 0)
          (∏ x ∈ a.support, HPow.hPow (β := ℕ) (f (Sum.inr x)) ((a : (a : κ) → ℕ) x : ℕ))
      else 0)

Tactic:
conv_rhs => rw [← Finset.sum_attach]

Premises used: Finset.sum_attach