-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
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)
refine :
  Membership.mem (γ := Set (Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)))
    {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
      ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
        p =
          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)}
    (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))
⊢ 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))
    (sSup
      {p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i) |
        ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
          p =
            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)})

Tactic:
refine le_csSup dualSeminorms_bounded ?_

Premises used: PiTensorProduct.dualSeminorms_bounded, le_csSup