-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem piTensorHomMapFun₂_add (φ ψ : ⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) :
    piTensorHomMapFun₂ (φ + ψ) = piTensorHomMapFun₂ φ + piTensorHomMapFun₂ ψ

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
φ ψ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
⊢ lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (φ + ψ))) =
    lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ)) +
      lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) ψ))

Tactic:
ext

Result:
case H.H.H.H
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
φ ψ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
x✝¹ : (i : ι) → s i
x✝ : (i : ι) → t i
⊢ ((((lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (φ + ψ)))).compMultilinearMap (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝ =
    ((((lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ)) +
                  lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) ψ))).compMultilinearMap
              (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝

Proof state:
case H.H.H.H
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
φ ψ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
x✝¹ : (i : ι) → s i
x✝ : (i : ι) → t i
⊢ ((((lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (φ + ψ)))).compMultilinearMap (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝ =
    ((((lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ)) +
                  lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) ψ))).compMultilinearMap
              (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝

Tactic:
simp only [map_add, LinearMap.compMultilinearMap_apply,
lift.tprod, add_apply, LinearMap.add_apply]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
φ ψ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
⊢ (φ + ψ).piTensorHomMapFun₂ = φ.piTensorHomMapFun₂ + ψ.piTensorHomMapFun₂

Tactic:
dsimp [piTensorHomMapFun₂]

Result:
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
φ ψ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
⊢ lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (φ + ψ))) =
    lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ)) +
      lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) ψ))