-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem liftIsometry_comp_mapL (h : ContinuousMultilinearMap 𝕜 E' F) :
    liftIsometry 𝕜 E' F h ∘L mapL f = liftIsometry 𝕜 E F (h.compContinuousLinearMap f)

Proof state:
ι : Type uι
inst✝⁷ : Fintype ι
𝕜 : Type u𝕜
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
F : Type uF
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
h : ContinuousMultilinearMap 𝕜 E' F
⊢ ((liftIsometry 𝕜 E' F) h).comp (mapL f) = (liftIsometry 𝕜 E F) (h.compContinuousLinearMap f)

Tactic:
apply ContinuousLinearMap.coe_injective

Result:
case a
ι : Type uι
inst✝⁷ : Fintype ι
𝕜 : Type u𝕜
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
F : Type uF
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
h : ContinuousMultilinearMap 𝕜 E' F
⊢ ↑(((liftIsometry 𝕜 E' F) h).comp (mapL f)) = ↑((liftIsometry 𝕜 E F) (h.compContinuousLinearMap f))

Proof state:
case a
ι : Type uι
inst✝⁷ : Fintype ι
𝕜 : Type u𝕜
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
F : Type uF
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
h : ContinuousMultilinearMap 𝕜 E' F
⊢ ↑(((liftIsometry 𝕜 E' F) h).comp (mapL f)) = ↑((liftIsometry 𝕜 E F) (h.compContinuousLinearMap f))

Tactic:
ext

Result:
case a.H.H
ι : Type uι
inst✝⁷ : Fintype ι
𝕜 : Type u𝕜
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
F : Type uF
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
h : ContinuousMultilinearMap 𝕜 E' F
x✝ : (i : ι) → E i
⊢ ((↑(((liftIsometry 𝕜 E' F) h).comp (mapL f))).compMultilinearMap (tprod 𝕜)) x✝ =
    ((↑((liftIsometry 𝕜 E F) (h.compContinuousLinearMap f))).compMultilinearMap (tprod 𝕜)) x✝

Proof state:
case a.H.H
ι : Type uι
inst✝⁷ : Fintype ι
𝕜 : Type u𝕜
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
F : Type uF
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
h : ContinuousMultilinearMap 𝕜 E' F
x✝ : (i : ι) → E i
⊢ ((↑(((liftIsometry 𝕜 E' F) h).comp (mapL f))).compMultilinearMap (tprod 𝕜)) x✝ =
    ((↑((liftIsometry 𝕜 E F) (h.compContinuousLinearMap f))).compMultilinearMap (tprod 𝕜)) x✝

Tactic:
simp only [ContinuousLinearMap.coe_comp, mapL_coe, LinearMap.compMultilinearMap_apply,
  LinearMap.coe_comp, ContinuousLinearMap.coe_coe, Function.comp_apply, map_tprod,
  liftIsometry_apply_apply, lift.tprod, ContinuousMultilinearMap.coe_coe,
  ContinuousMultilinearMap.compContinuousLinearMap_apply]

Result:
no goals