awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
m : (i : ι) → E i
⊢ ⨅ (p : (↑(lifts (s := E) (⨂ₜ[𝕜] (i : ι), m i)) : Type (max (max uE uι) u𝕜))),
      projectiveSeminormAux (E := E) (↑p : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ≤
    projectiveSeminormAux.{uι, u𝕜, uE} (𝕜 := 𝕜) (E := E)
      (↑(Subtype.mk (p := fun (x : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦
            Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i)))) (lifts (s := E) (⨂ₜ[𝕜] (i : ι), m i)) x)
            (FreeAddMonoid.of (1, m)) ⋯) :
        FreeAddMonoid (𝕜 × ((i : ι) → E i)))

Tactic:
ciInf_le (bddBelow_projectiveSemiNormAux _) ⟨FreeAddMonoid.of ((1 : 𝕜), m), ?_⟩

Premises used: FreeAddMonoid.of, PiTensorProduct.bddBelow_projectiveSemiNormAux, Prod.mk, Subtype.mk, ciInf_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
m : (i : ι) → E i
h :
  ∏ i : ι, ‖m i‖ =
    projectiveSeminormAux.{uι, u𝕜, uE} (𝕜 := 𝕜) (E := E)
      (↑(Subtype.mk (p := fun (x : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦
            Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i)))) (lifts (s := E) (⨂ₜ[𝕜] (i : ι), m i)) x)
            (FreeAddMonoid.of (1, m)) ⋯) :
        FreeAddMonoid (𝕜 × ((i : ι) → E i)))
convert_2 :
  Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i)))) (lifts (s := E) (⨂ₜ[𝕜] (i : ι), m i))
    (FreeAddMonoid.of (1, m))
⊢ LE.le (α := ℝ) ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) (⨂ₜ[𝕜] (i : ι), m i) : ℝ)
    (∏ i : ι, ‖m i‖ : ℝ)

Tactic:
convert! ciInf_le (bddBelow_projectiveSemiNormAux _) ⟨FreeAddMonoid.of ((1 : 𝕜), m), ?_⟩

Premises used: FreeAddMonoid.of, PiTensorProduct.bddBelow_projectiveSemiNormAux, Prod.mk, Subtype.mk, ciInf_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
m : (i : ι) → E i
⊢ ∏ i : ι, ‖m i‖ =
    projectiveSeminormAux.{uι, u𝕜, uE} (𝕜 := 𝕜) (E := E)
      (↑(Subtype.mk (p := fun (x : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦
            Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i)))) (lifts (s := E) (⨂ₜ[𝕜] (i : ι), m i)) x)
            (FreeAddMonoid.of (1, m)) ⋯) :
        FreeAddMonoid (𝕜 × ((i : ι) → E i)))

Tactic:
simp [projectiveSeminormAux]

Premises used: PiTensorProduct.projectiveSeminormAux
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
m : (i : ι) → E i
⊢ Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i)))) (lifts (s := E) (⨂ₜ[𝕜] (i : ι), m i))
    (FreeAddMonoid.of (1, m))

Tactic:
simp [mem_lifts_iff]

Premises used: PiTensorProduct.mem_lifts_iff
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
rw :
  norm.{u_1} (E := G)
      ((((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
            (a : ⨂[𝕜] (i : ι), E i) → G)
          x :
        G) ≤
    ⨅ (i : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))),
      projectiveSeminormAux (E := E) (↑i : FreeAddMonoid (𝕜 × ((i : ι) → E i))) * ‖f‖
⊢ norm.{u_1} (E := G)
      ((((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
            (a : ⨂[𝕜] (i : ι), E i) → G)
          x :
        G) ≤
    ‖f‖ * ‖x‖

Tactic:
rw [norm_def, mul_comm, Real.iInf_mul_of_nonneg (norm_nonneg _)]

Premises used: Real.iInf_mul_of_nonneg, PiTensorProduct.norm_def, mul_comm, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
⊢ norm.{u_1} (E := G)
      ((((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
            (a : ⨂[𝕜] (i : ι), E i) → G)
          x :
        G) ≤
    ⨅ (i : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))),
      projectiveSeminormAux (E := E) (↑i : FreeAddMonoid (𝕜 × ((i : ι) → E i))) * ‖f‖

Tactic:
le_ciInf fun ⟨p, hp⟩ ↦ ?_

Premises used: Norm.norm, HMul.hMul, _private.0.PiTensorProduct.norm_eval_le_projectiveSeminorm.match_1, LE.le, PiTensorProduct.projectiveSeminormAux, le_ciInf, ContinuousMultilinearMap.toMultilinearMap, Subtype.val, PiTensorProduct.lift, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
refine :
  ∀ (x_1 : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))) (p : FreeAddMonoid (𝕜 × ((i : ι) → E i)))
    (hp : p ∈ x.lifts (s := E)),
    norm.{u_1} (E := G)
        ((((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
                (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
              (a : ⨂[𝕜] (i : ι), E i) → G)
            x :
          G) ≤
      projectiveSeminormAux (E := E)
          (↑(Subtype.mk (p := fun (x_2 : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦ x_2 ∈ x.lifts (s := E)) p hp) :
            FreeAddMonoid (𝕜 × ((i : ι) → E i))) *
        ‖f‖
⊢ norm.{u_1} (E := G)
      ((((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
            (a : ⨂[𝕜] (i : ι), E i) → G)
          x :
        G) ≤
    ⨅ (i : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))),
      projectiveSeminormAux (E := E) (↑i : FreeAddMonoid (𝕜 × ((i : ι) → E i))) * ‖f‖

Tactic:
refine le_ciInf fun ⟨p, hp⟩ ↦ ?_

Premises used: le_ciInf
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
x_1 : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts (s := E)
rw! :
  norm.{u_1} (E := G)
      (Multiset.sum
        (↑(List.map (α := 𝕜 × ((i : ι) → E i))
              (Function.comp (β := ⨂[𝕜] (i : ι), E i)
                (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G)
                        (f.toMultilinearMap (M₁ := E)) :
                      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
                  (a : ⨂[𝕜] (i : ι), E i) → G)
                fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
              ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)) :
          Multiset G)) ≤
    projectiveSeminormAux (E := E)
        (↑(Subtype.mk (p := fun (x : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦
              Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i))))
                (lifts (s := E)
                  (List.sum
                    (List.map
                      (fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
                      ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i)))
                        p))))
                x)
              p ⋯) :
          FreeAddMonoid (𝕜 × ((i : ι) → E i))) *
      ‖f‖
⊢ norm.{u_1} (E := G)
      ((((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
              (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
            (a : ⨂[𝕜] (i : ι), E i) → G)
          x :
        G) ≤
    projectiveSeminormAux (E := E)
        (↑(Subtype.mk (p := fun (x_2 : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦ x_2 ∈ x.lifts (s := E)) p hp) :
          FreeAddMonoid (𝕜 × ((i : ι) → E i))) *
      ‖f‖

Tactic:
rw! [← ((mem_lifts_iff x p).mp hp), ← List.sum_map_hom, ← Multiset.sum_coe]

Premises used: Multiset.sum_coe, List.sum_map_hom, PiTensorProduct.mem_lifts_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
x_1 : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts (s := E)
simp :
  LE.le (α := ℝ)
    (Multiset.sum
      (Multiset.map (fun (x : G) ↦ ‖x‖)
        (↑(List.map (α := 𝕜 × ((i : ι) → E i))
              (Function.comp (β := ⨂[𝕜] (i : ι), E i)
                (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G)
                        (f.toMultilinearMap (M₁ := E)) :
                      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
                  (a : ⨂[𝕜] (i : ι), E i) → G)
                fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
              ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)) :
          Multiset G)))
    (List.sum
      (List.map (fun (x : ℝ) ↦ ‖f‖ • x)
        (List.map (fun (p : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ℝ) ‖p.1‖ (∏ i : ι, ‖p.2 i‖))
          ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p))))
⊢ Multiset.sum
      (Multiset.map (fun (x : G) ↦ ‖x‖)
        (↑(List.map (α := 𝕜 × ((i : ι) → E i))
              (Function.comp (β := ⨂[𝕜] (i : ι), E i)
                (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G)
                        (f.toMultilinearMap (M₁ := E)) :
                      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
                  (a : ⨂[𝕜] (i : ι), E i) → G)
                fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
              ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)) :
          Multiset G)) ≤
    projectiveSeminormAux (E := E)
        (↑(Subtype.mk (p := fun (x : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦
              Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i))))
                (lifts (s := E)
                  (List.sum
                    (List.map
                      (fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
                      ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i)))
                        p))))
                x)
              p ⋯) :
          FreeAddMonoid (𝕜 × ((i : ι) → E i))) *
      ‖f‖

Tactic:
simp only [mul_comm, ← smul_eq_mul, List.smul_sum, projectiveSeminormAux]

Premises used: PiTensorProduct.projectiveSeminormAux, mul_comm, smul_eq_mul, List.smul_sum
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
x_1 : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts (s := E)
⊢ LE.le (α := ℝ)
    (Multiset.sum
      (Multiset.map (fun (x : G) ↦ ‖x‖)
        (↑(List.map (α := 𝕜 × ((i : ι) → E i))
              (Function.comp (β := ⨂[𝕜] (i : ι), E i)
                (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G)
                        (f.toMultilinearMap (M₁ := E)) :
                      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
                  (a : ⨂[𝕜] (i : ι), E i) → G)
                fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
              ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)) :
          Multiset G)))
    (List.sum
      (List.map (fun (x : ℝ) ↦ ‖f‖ • x)
        (List.map (fun (p : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ℝ) ‖p.1‖ (∏ i : ι, ‖p.2 i‖))
          ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p))))

Tactic:
List.Forall₂.sum_le_sum ?_

Premises used: Multiset.sum, Multiset.foldr, List.sum, List.Forall₂.sum_le_sum
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
x_1 : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts (s := E)
refine :
  List.Forall₂ (fun (x1 x2 : ℝ) ↦ x1 ≤ x2)
    (List.map (fun (x : G) ↦ ‖x‖)
      (List.map (α := 𝕜 × ((i : ι) → E i))
        (Function.comp (β := ⨂[𝕜] (i : ι), E i)
          (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
                (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
            (a : ⨂[𝕜] (i : ι), E i) → G)
          fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)))
    (List.map (fun (x : ℝ) ↦ ‖f‖ • x)
      (List.map (fun (p : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ℝ) ‖p.1‖ (∏ i : ι, ‖p.2 i‖))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)))
⊢ LE.le (α := ℝ)
    (Multiset.sum
      (Multiset.map (fun (x : G) ↦ ‖x‖)
        (↑(List.map (α := 𝕜 × ((i : ι) → E i))
              (Function.comp (β := ⨂[𝕜] (i : ι), E i)
                (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G)
                        (f.toMultilinearMap (M₁ := E)) :
                      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
                  (a : ⨂[𝕜] (i : ι), E i) → G)
                fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
              ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)) :
          Multiset G)))
    (List.sum
      (List.map (fun (x : ℝ) ↦ ‖f‖ • x)
        (List.map (fun (p : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ℝ) ‖p.1‖ (∏ i : ι, ‖p.2 i‖))
          ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p))))

Tactic:
refine List.Forall₂.sum_le_sum ?_

Premises used: List.Forall₂.sum_le_sum
-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
x_1 : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts (s := E)
⊢ List.Forall₂ (fun (x1 x2 : ℝ) ↦ x1 ≤ x2)
    (List.map (fun (x : G) ↦ ‖x‖)
      (List.map (α := 𝕜 × ((i : ι) → E i))
        (Function.comp (β := ⨂[𝕜] (i : ι), E i)
          (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) (f.toMultilinearMap (M₁ := E)) :
                (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
            (a : ⨂[𝕜] (i : ι), E i) → G)
          fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)))
    (List.map (fun (x : ℝ) ↦ ‖f‖ • x)
      (List.map (fun (p : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ℝ) ‖p.1‖ (∏ i : ι, ‖p.2 i‖))
        ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)))

Tactic:
simpa [norm_smul, ← mul_assoc, mul_comm ‖f‖ _] using
    fun a m _ ↦ mul_le_mul_of_nonneg_left (f.le_opNorm _) (norm_nonneg _)

Premises used: Norm.norm, norm_smul, mul_assoc, ContinuousMultilinearMap.le_opNorm, mul_comm, mul_le_mul_of_nonneg_left, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
z : E
⊢ norm.{u_1} (E := 𝕜) (↑‖z‖ : 𝕜) = ‖z‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
have : ‖x‖ ≠ 0 := by simp [hx]
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜)⁻¹ x‖ = 1

Tactic:
simp [field, norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
have : ‖x‖ ≠ 0 := by simp [hx]
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖x‖ : 𝕜)⁻¹ • x‖ = r

Tactic:
simp [field, norm_smul, r_nonneg, rclike_simps]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : x ≠ 0
⊢ ‖HSMul.hSMul (α := 𝕜) (β := StrongDual.{u_1, u_2} 𝕜 ↥(𝕜 ∙ x)) (↑‖x‖ : 𝕜) (coord 𝕜 x h)‖ = 1

Tactic:
simp only [norm_smul, RCLike.norm_coe_norm, coord_norm, mul_inv_cancel₀ (mt norm_eq_zero.mp h)]

Premises used: norm_eq_zero, norm_smul, mul_inv_cancel₀, mt, Iff.mp, RCLike.norm_coe_norm, ContinuousLinearEquiv.coord_norm
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
pos : ∀ (z_zero : z = 0), norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖
neg : ∀ (z_zero : ¬z = 0), norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖

Tactic:
by_cases z_zero : z = 0
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : z = 0
pos : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) 0 : 𝕜) ≤ c / r * norm.{u_2} (E := E) 0
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖

Tactic:
rw [z_zero]
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : z = 0
pos : LE.le (α := ℝ) 0 0
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) 0 : 𝕜) ≤ c / r * norm.{u_2} (E := E) 0

Tactic:
simp only [map_zero, norm_zero, mul_zero]

Premises used: norm_zero, map_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : z = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : z = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
⊢ let z₁ := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z;
  z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z

Tactic:
set z₁ := ((r : 𝕜) * (‖z‖ : 𝕜)⁻¹) • z with hz₁

Premises used: Norm.norm, HMul.hMul, RCLike.ofReal, Inv.inv
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
a : Membership.mem (γ := Set E) (sphere 0 r) z₁
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c

Tactic:
apply h