-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
F : Type uF
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x_1 : ⨂[𝕜] (i : ι), E i
G : Type (max (max uE u𝕜) uι) :=
  HasQuotient.Quotient (⨂[𝕜] (i : ι), E i) (B := Submodule 𝕜 (⨂[𝕜] (i : ι), E i))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := F) (τ₁₂ := RingHom.id 𝕜)
      ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E))))
G' : Submodule 𝕜 F :=
  LinearMap.range (R := 𝕜) (M := ⨂[𝕜] (i : ι), E i) (τ₁₂ := RingHom.id 𝕜)
    ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E)))
e : HasQuotient.Quotient (⨂[𝕜] (i : ι), E i) (B := Submodule 𝕜 (⨂[𝕜] (i : ι), E i))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := F) (τ₁₂ := RingHom.id 𝕜)
      ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E)))) ≃ₗ[𝕜]
  ↥(LinearMap.range (R := 𝕜) (M := ⨂[𝕜] (i : ι), E i) (τ₁₂ := RingHom.id 𝕜)
      ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E)))) :=
  LinearMap.quotKerEquivRange
    ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E)))
this_1 : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E
  (HasQuotient.Quotient (⨂[𝕜] (i : ι), E i) (B := Submodule 𝕜 (⨂[𝕜] (i : ι), E i))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := F) (τ₁₂ := RingHom.id 𝕜)
      ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E))))) :=
  (LinearEquiv.symm (lift (s := E)) :
      (a :
          (⨂[𝕜] (i : ι), E i) →ₗ[𝕜]
            (⨂[𝕜] (i : ι), E i) ⧸
              ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker) →
        MultilinearMap 𝕜 E
          ((⨂[𝕜] (i : ι), E i) ⧸
            ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker))
    ((↑e.symm :
        ↥((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).range →ₗ[𝕜]
          (⨂[𝕜] (i : ι), E i) ⧸
            ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker) ∘ₗ
      LinearMap.rangeRestrict
        ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E))))
x : (i : ι) → E i
⊢ norm (E :=
      HasQuotient.Quotient (⨂[𝕜] (i : ι), E i) (B := Submodule 𝕜 (⨂[𝕜] (i : ι), E i))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := F) (τ₁₂ := RingHom.id 𝕜)
          ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E)))))
      ((f'₀ :
            (a : (i : ι) → E i) →
              (⨂[𝕜] (i : ι), E i) ⧸
                ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker)
          x :
        HasQuotient.Quotient (⨂[𝕜] (i : ι), E i) (B := Submodule 𝕜 (⨂[𝕜] (i : ι), E i))
          (LinearMap.ker (R₂ := 𝕜) (M₂ := F) (τ₁₂ := RingHom.id 𝕜)
            ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F)
              (f.toMultilinearMap (M₁ := E))))) ≤
    ‖f‖ * ∏ i : ι, ‖x i‖
have change : norm.{uF} (E :=
    ↥(LinearMap.range (R := 𝕜) (M := ⨂[𝕜] (i : ι), E i) (τ₁₂ := RingHom.id 𝕜)
        ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E)))))
    ((e :
          (a :
              (⨂[𝕜] (i : ι), E i) ⧸
                ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker) →
            ↥((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).range)
        ((f'₀ :
            (a : (i : ι) → E i) →
              (⨂[𝕜] (i : ι), E i) ⧸
                ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker)
          x) :
      ↥(LinearMap.range (R := 𝕜) (M := ⨂[𝕜] (i : ι), E i) (τ₁₂ := RingHom.id 𝕜)
          ((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F)
            (f.toMultilinearMap (M₁ := E))))) ≤
  ‖f‖ * ∏ i : ι, ‖x i‖
Tactic: change ‖e (f'₀ x)‖ ≤ _