-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem piTensorHomMapFun₂_smul (r : R) (φ : ⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) :
    piTensorHomMapFun₂ (r • φ) = r • 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 : R
φ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
⊢ lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (r • φ))) =
    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 : R
φ : ⨂[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))) (r • φ)))).compMultilinearMap (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝ =
    ((((r • lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ))).compMultilinearMap (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝

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 : R
φ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
⊢ (r • φ).piTensorHomMapFun₂ = r • φ.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 : R
φ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
⊢ lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (r • φ))) =
    r • lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ))

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 : R
φ : ⨂[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))) (r • φ)))).compMultilinearMap (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝ =
    ((((r • lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ))).compMultilinearMap (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝

Tactic:
simp only [map_smul, LinearMap.compMultilinearMap_apply,
lift.tprod, smul_apply, LinearMap.smul_apply]

Result:
no goals