-- Mathlib/RingTheory/MvPolynomial/FreeCommRing.lean
theorem lift_genericPolyMap [DecidableEq κ] [CommRing R]
    [DecidableEq R] (monoms : ι → Finset (κ →₀ ℕ))
    (f : (i : ι) × { x // x ∈ monoms i } ⊕ κ → R) (i : ι) :
    FreeCommRing.lift f (genericPolyMap monoms i) =
      MvPolynomial.eval (f ∘ Sum.inr)
        (((mvPolynomialSupportLEEquiv monoms).symm
          (f ∘ Sum.inl)).1 i)

Proof state:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × { x // x ∈ monoms i } ⊕ κ → R
i : ι
⊢ (lift f) (genericPolyMap monoms i) =
    (eval (f ∘ Sum.inr)) (↑((mvPolynomialSupportLEEquiv monoms).symm (f ∘ Sum.inl)) i)

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

Result:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × { x // x ∈ monoms i } ⊕ κ → R
i : ι
⊢ ∑ x ∈ (monoms i).attach, f (Sum.inl ⟨i, x⟩) * (lift f) ((↑x).prod fun j n => of (Sum.inr j) ^ n) =
    ∑ a ∈ monoms i,
      if ∃ (h : a ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨a, ⋯⟩⟩) = 0 then
        (if h : a ∈ monoms i then f (Sum.inl ⟨i, ⟨a, ⋯⟩⟩) else 0) * ∏ x ∈ a.support, f (Sum.inr x) ^ a x
      else 0

Proof state:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × { x // x ∈ monoms i } ⊕ κ → R
i : ι
⊢ ∑ x ∈ (monoms i).attach, f (Sum.inl ⟨i, x⟩) * (lift f) ((↑x).prod fun j n => of (Sum.inr j) ^ n) =
    ∑ a ∈ monoms i,
      if ∃ (h : a ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨a, ⋯⟩⟩) = 0 then
        (if h : a ∈ monoms i then f (Sum.inl ⟨i, ⟨a, ⋯⟩⟩) else 0) * ∏ x ∈ a.support, f (Sum.inr x) ^ a x
      else 0

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

Result:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × { x // x ∈ monoms i } ⊕ κ → R
i : ι
⊢ ∑ x ∈ (monoms i).attach, f (Sum.inl ⟨i, x⟩) * (lift f) ((↑x).prod fun j n => of (Sum.inr j) ^ n) =
    ∑ x ∈ (monoms i).attach,
      if ∃ (h : ↑x ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨↑x, ⋯⟩⟩) = 0 then
        (if h : ↑x ∈ monoms i then f (Sum.inl ⟨i, ⟨↑x, ⋯⟩⟩) else 0) * ∏ x_1 ∈ (↑x).support, f (Sum.inr x_1) ^ ↑x x_1
      else 0

Proof state:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × { x // x ∈ monoms i } ⊕ κ → R
i : ι
m : { x // x ∈ monoms i }
a✝ : m ∈ (monoms i).attach
⊢ f (Sum.inl ⟨i, m⟩) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x =
    if f (Sum.inl ⟨i, m⟩) = 0 then 0 else f (Sum.inl ⟨i, m⟩) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x

Tactic:
split_ifs with h0 <;> simp_all

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × { x // x ∈ monoms i } ⊕ κ → R
i : ι
m : { x // x ∈ monoms i }
a✝ : m ∈ (monoms i).attach
⊢ f (Sum.inl ⟨i, m⟩) * (lift f) ((↑m).prod fun j n => of (Sum.inr j) ^ n) =
    if ∃ (h : ↑m ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨↑m, ⋯⟩⟩) = 0 then
      (if h : ↑m ∈ monoms i then f (Sum.inl ⟨i, ⟨↑m, ⋯⟩⟩) else 0) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x
    else 0

Tactic:
simp only [Finsupp.prod, map_prod, map_pow, lift_of, Subtype.coe_eta, Finset.coe_mem,
  exists_prop, true_and, dite_eq_ite, ite_true, ite_not]

Result:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × { x // x ∈ monoms i } ⊕ κ → R
i : ι
m : { x // x ∈ monoms i }
a✝ : m ∈ (monoms i).attach
⊢ f (Sum.inl ⟨i, m⟩) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x =
    if f (Sum.inl ⟨i, m⟩) = 0 then 0 else f (Sum.inl ⟨i, m⟩) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x

Proof state:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × { x // x ∈ monoms i } ⊕ κ → R
i : ι
⊢ ∑ x ∈ (monoms i).attach, f (Sum.inl ⟨i, x⟩) * (lift f) ((↑x).prod fun j n => of (Sum.inr j) ^ n) =
    ∑ x ∈ (monoms i).attach,
      if ∃ (h : ↑x ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨↑x, ⋯⟩⟩) = 0 then
        (if h : ↑x ∈ monoms i then f (Sum.inl ⟨i, ⟨↑x, ⋯⟩⟩) else 0) * ∏ x_1 ∈ (↑x).support, f (Sum.inr x_1) ^ ↑x x_1
      else 0

Tactic:
refine Finset.sum_congr rfl ?_

Result:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × { x // x ∈ monoms i } ⊕ κ → R
i : ι
⊢ ∀ x ∈ (monoms i).attach,
    f (Sum.inl ⟨i, x⟩) * (lift f) ((↑x).prod fun j n => of (Sum.inr j) ^ n) =
      if ∃ (h : ↑x ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨↑x, ⋯⟩⟩) = 0 then
        (if h : ↑x ∈ monoms i then f (Sum.inl ⟨i, ⟨↑x, ⋯⟩⟩) else 0) * ∏ x_1 ∈ (↑x).support, f (Sum.inr x_1) ^ ↑x x_1
      else 0

Proof state:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × { x // x ∈ monoms i } ⊕ κ → R
i : ι
⊢ ∀ x ∈ (monoms i).attach,
    f (Sum.inl ⟨i, x⟩) * (lift f) ((↑x).prod fun j n => of (Sum.inr j) ^ n) =
      if ∃ (h : ↑x ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨↑x, ⋯⟩⟩) = 0 then
        (if h : ↑x ∈ monoms i then f (Sum.inl ⟨i, ⟨↑x, ⋯⟩⟩) else 0) * ∏ x_1 ∈ (↑x).support, f (Sum.inr x_1) ^ ↑x x_1
      else 0

Tactic:
intros m _

Result:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × { x // x ∈ monoms i } ⊕ κ → R
i : ι
m : { x // x ∈ monoms i }
a✝ : m ∈ (monoms i).attach
⊢ f (Sum.inl ⟨i, m⟩) * (lift f) ((↑m).prod fun j n => of (Sum.inr j) ^ n) =
    if ∃ (h : ↑m ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨↑m, ⋯⟩⟩) = 0 then
      (if h : ↑m ∈ monoms i then f (Sum.inl ⟨i, ⟨↑m, ⋯⟩⟩) else 0) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x
    else 0