when `apply_linearCombination` is not enough

Stream: Is there code for X?

[Antoine Chambert-Loir]

Is there a way to golf this proof? (see below for explanation)

import Mathlib.LinearAlgebra.Finsupp
import Mathlib.Algebra.MvPolynomial.Basic


open Finsupp MvPolynomial

variable {σ : Type*} {R : Type*} [CommRing R]

example {ι : Type*} (f : ι → MvPolynomial σ R) (g : ι →₀ MvPolynomial σ R) (x : σ → R) :
    eval x (linearCombination _ f g)
      = linearCombination R (eval x ∘ f) (mapRange (eval x) (map_zero _) g) := by
  classical
  simp [linearCombination]
  rw [Finsupp.sum, eval_sum]
  rw [Finsupp.sum_of_support_subset (s := g.support)]
  · apply Finset.sum_congr rfl
    intro i hi
    simp
  · intro i
    simp only [Finsupp.mem_support_iff, mapRange_apply, ne_eq]
    rw [not_imp_not]
    intro hi
    simp only [hi, map_zero]

In my context, it is natural to come up with this docs#Finsupp.linearCombination, because f : ι → MvPolynomial σ R is given, g : ι →₀ MvPolynomial σ R is found by some process, and docs#Finsupp.linearCombination is the easiest way ove writing Σ i, f i * g i.
The point is that docs#Finsupp.apply_linearCombination is too restricted to apply and it's hard to guess the general pattern.

[Eric Wieser]

Here's a shorter version:

import Mathlib.LinearAlgebra.Finsupp
import Mathlib.Algebra.MvPolynomial.Basic


open Finsupp MvPolynomial

variable {σ : Type*} {R : Type*} [CommRing R]

example {ι : Type*} (f : ι → MvPolynomial σ R) (g : ι →₀ MvPolynomial σ R) (x : σ → R) :
    eval x (linearCombination _ f g)
      = linearCombination R (eval x ∘ f) (mapRange (eval x) (map_zero _) g) := by
  rw [linearCombination_apply, linearCombination_apply, map_finsupp_sum, sum_mapRange_index fun i => ?_]
  simp_rw [smul_eq_mul, map_mul, Function.comp]
  exact zero_smul _ _

[Eric Wieser]

I think this is the general statement?

import Mathlib.LinearAlgebra.Finsupp
import Mathlib.Algebra.MvPolynomial.Basic


open Finsupp

variable {σ : Type*} {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R B] [Algebra R A]

example {ι : Type*} (E : B →ₐ[R] A) (f : ι → B) (g : ι →₀ R) :
    E (linearCombination R f g)
      = linearCombination A (E ∘ f) (mapRange (E.comp <| Algebra.ofId _ _) (map_zero _) g) := by
  rw [linearCombination_apply, linearCombination_apply, map_finsupp_sum, sum_mapRange_index fun i => ?_]
  simp_rw [Function.comp, AlgHom.comp_apply, Algebra.ofId_apply, AlgHom.commutes, algebraMap_smul,
    map_smul]
  exact zero_smul _ _

[Eric Wieser]

(checking again, that's not the right generality, sorry!)

[Antoine Chambert-Loir]

That's OK, at least that showed me that combining docs#linearCombination_apply and docs#map_finsupp_sum was enough to do most of the job.