-- 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 : ⨂[𝕜] (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))))
hf'₀ :
  ∀ (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‖
f' : ContinuousMultilinearMap 𝕜 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'₀.mkContinuous (E := E) ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
heq :
  Eq.{uF + 1} (α := F)
    ((↑((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)
            ((((lift (s := E) :
                      (a :
                          MultilinearMap 𝕜 E
                            ((⨂[𝕜] (i : ι), E i) ⧸
                              ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F)
                                  f.toMultilinearMap).ker)) →
                        (⨂[𝕜] (i : ι), E i) →ₗ[𝕜]
                          (⨂[𝕜] (i : ι), E i) ⧸
                            ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker)
                    (f'.toMultilinearMap (M₁ := E)) :
                  (⨂[𝕜] (i : ι), E i) →ₗ[𝕜]
                    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))))) :
                (a : ⨂[𝕜] (i : ι), E i) →
                  (⨂[𝕜] (i : ι), E i) ⧸
                    ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker)
              x)) :
        F) :
      F)
    ((((lift (s := E) : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) (f.toMultilinearMap (M₁ := E)) :
            (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
          (a : ⨂[𝕜] (i : ι), E i) → F)
        x :
      F)
hle :
  LE.le (α := Seminorm 𝕜 (⨂[𝕜] (i : ι), E i))
    (Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
      (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
      (toDualContinuousMultilinearMap (E := E) G))
    (injectiveSeminorm (E := E))
⊢ 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)))))
      ((((lift (s := E) :
                  (a :
                      MultilinearMap 𝕜 E
                        ((⨂[𝕜] (i : ι), E i) ⧸
                          ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker)) →
                    (⨂[𝕜] (i : ι), E i) →ₗ[𝕜]
                      (⨂[𝕜] (i : ι), E i) ⧸
                        ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker)
                (f'.toMultilinearMap (M₁ := E)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜]
                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))))) :
            (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))))) ≤
    HMul.hMul (β := ℝ) ‖f'‖ ((injectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x : ℝ)
have refine : 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)))))
    ((((lift (s := E) :
                (a :
                    MultilinearMap 𝕜 E
                      ((⨂[𝕜] (i : ι), E i) ⧸
                        ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker)) →
                  (⨂[𝕜] (i : ι), E i) →ₗ[𝕜]
                    (⨂[𝕜] (i : ι), E i) ⧸
                      ((lift : (a : MultilinearMap 𝕜 E F) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) f.toMultilinearMap).ker)
              (f'.toMultilinearMap (M₁ := E)) :
            (⨂[𝕜] (i : ι), E i) →ₗ[𝕜]
              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))))) :
          (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'‖ *
    (fun (f : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) ↦ ((⇑f : (a : ⨂[𝕜] (i : ι), E i) → ℝ) : (a : ⨂[𝕜] (i : ι), E i) → ℝ))
      (Seminorm.comp (E₂ := ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) (σ₁₂ := RingHom.id 𝕜)
        (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G) : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
        (toDualContinuousMultilinearMap (E := E) G))
      x
Tactic: refine le_trans ?_ (mul_le_mul_of_nonneg_left (hle x) (norm_nonneg f'))