awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
𝕜' : Type u_1
inst_6 : SeminormedRing 𝕜'
inst_7 : Module 𝕜' G
inst_8 : IsBoundedSMul 𝕜' G
inst_9 : SMulCommClass 𝕜 𝕜' G
c : 𝕜'
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
grw : ‖HSMul.hSMul (β := G) c ((f : (a : (i : ι) → E i) → G) m : G)‖ ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
grw₁ : ‖c‖ * Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖
grw₂ : ‖c‖ * Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ ‖c‖ * (‖f‖ * ∏ i : ι, ‖m i‖)
grw₃ grw₄ : ‖c‖ * (‖f‖ * ∏ i : ι, ‖m i‖) ≤ ‖c‖ * (‖f‖ * ∏ i : ι, ‖m i‖)
⊢ Norm.norm.{wG} (E := G) ((c • f : (a : (i : ι) → E i) → G) m : G) ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖

Tactic:
grw [smul_apply, norm_smul_le, mul_assoc, le_opNorm]

Premises used: norm_smul_le, mul_assoc, ContinuousMultilinearMap.le_opNorm, ContinuousMultilinearMap.smul_apply
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G
rw : ‖-(-f.1 + f.2)‖ = ‖f.1 - f.2‖
rw₁ : ‖- -f.1 + -f.2‖ = ‖f.1 - f.2‖
rw₂ : ‖f.1 + -f.2‖ = ‖f.1 - f.2‖
rw₃ rw₄ : ‖f.1 + -f.2‖ = ‖f.1 + -f.2‖
⊢ ‖-f.1 + f.2‖ = ‖f.1 - f.2‖

Tactic:
rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, neg_add, neg_neg, ContinuousMultilinearMap.opNorm_neg
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
⊢ ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖

Tactic:
have A (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G) :
      ‖-f.1 + f.2‖ = ‖f.1 - f.2‖ := by rw [← opNorm_neg, neg_add, neg_neg, sub_eq_add_neg]
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
simp :
  Eq (α := Filter (ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G))
    (𝓤 (ContinuousMultilinearMap 𝕜 E G))
    (⨅ (r : ℝ),
      ⨅ (_ : r > 0), 𝓟 {f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G | ‖f.1 - f.2‖ < r})
⊢ Eq (α := Filter (ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G))
    (𝓤 (ContinuousMultilinearMap 𝕜 E G))
    (⨅ (r : ℝ),
      ⨅ (_ : r > 0), 𝓟 {f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G | ‖-f.1 + f.2‖ < r})

Tactic:
simp only [A]
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
⊢ Eq (α := Filter (ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G))
    (𝓤 (ContinuousMultilinearMap 𝕜 E G))
    (⨅ (r : ℝ),
      ⨅ (_ : r > 0), 𝓟 {f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G | ‖f.1 - f.2‖ < r})

Tactic:
(ContinuousMultilinearMap.seminorm 𝕜 E G).uniformity_eq_of_hasBasis
    (ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis Metric.nhds_basis_closedBall)
    ?_ fun (s, r) ⟨hs, hr⟩ ↦ ?_

Premises used: _private.0.ContinuousMultilinearMap.uniformity_eq_seminorm.match_1, setOf, Exists, Prod.mk, HasSubset.Subset, Prod.fst, GT.gt, And, Seminorm.ball, ContinuousMultilinearMap.seminorm, Set.MapsTo, ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis, Metric.nhds_basis_closedBall, _private.0.ContinuousMultilinearMap.uniformity_eq_seminorm.match_2, Metric.closedBall, OfNat.ofNat, Prod.snd, DFunLike.coe, ContinuousMultilinearMap.opNorm, Seminorm.uniformity_eq_of_hasBasis
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
refine_1 :
  ∃ (r : ℝ),
    Membership.mem (γ := Filter (ContinuousMultilinearMap 𝕜 E G)) (𝓝 0)
      (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)
refine_2 :
  ∀ (x : Set ((i : ι) → E i) × ℝ) (s : Set ((i : ι) → E i)) (r : ℝ),
    Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2 →
      ∀ (hs : Bornology.IsVonNBounded 𝕜 (s, r).1) (hr : 0 < (s, r).2),
        ∃ r_1 > 0,
          Subset (α := Set (ContinuousMultilinearMap 𝕜 E G))
            (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r_1)
            {f : ContinuousMultilinearMap 𝕜 E G |
              Set.MapsTo (β := G) (⇑f : (a : (i : ι) → E i) → G) (s, r).1 (closedBall 0 (s, r).2)}
⊢ Eq (α := Filter (ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G))
    (𝓤 (ContinuousMultilinearMap 𝕜 E G))
    (⨅ (r : ℝ),
      ⨅ (_ : r > 0), 𝓟 {f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G | ‖f.1 - f.2‖ < r})

Tactic:
refine (ContinuousMultilinearMap.seminorm 𝕜 E G).uniformity_eq_of_hasBasis
    (ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis Metric.nhds_basis_closedBall)
    ?_ fun (s, r) ⟨hs, hr⟩ ↦ ?_

Premises used: _private.0.ContinuousMultilinearMap.uniformity_eq_seminorm.match_1, setOf, Exists, Prod.mk, HasSubset.Subset, Prod.fst, GT.gt, And, Seminorm.ball, ContinuousMultilinearMap.seminorm, Set.MapsTo, ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis, Metric.nhds_basis_closedBall, _private.0.ContinuousMultilinearMap.uniformity_eq_seminorm.match_2, Metric.closedBall, OfNat.ofNat, Prod.snd, DFunLike.coe, Seminorm.uniformity_eq_of_hasBasis
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
refine_1 :
  ∀ (c : 𝕜) (hc : 1 < ‖c‖),
    ∃ (r : ℝ),
      Membership.mem (γ := Filter (ContinuousMultilinearMap 𝕜 E G)) (𝓝 0)
        (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)
⊢ ∃ (r : ℝ),
    Membership.mem (γ := Filter (ContinuousMultilinearMap 𝕜 E G)) (𝓝 0)
      (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)

Tactic:
rcases NormedField.exists_lt_norm 𝕜 1 with ⟨c, hc⟩

Premises used: NormedField.exists_lt_norm, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
⊢ 0 < ‖c‖

Tactic:
have hc₀ : 0 < ‖c‖ := one_pos.trans hc
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
refine_1 :
  ∃ (r : ℝ) (a : Set ((i : ι) → E i)) (b : Set G),
    (Bornology.IsVonNBounded 𝕜 a ∧ Membership.mem (γ := Filter G) (𝓝 0) b) ∧
      Subset (α := Set (ContinuousMultilinearMap 𝕜 E G))
        {f : ContinuousMultilinearMap 𝕜 E G | Set.MapsTo (⇑f : (a : (i : ι) → E i) → G) a b}
        (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)
⊢ ∃ (r : ℝ),
    Membership.mem (γ := Filter (ContinuousMultilinearMap 𝕜 E G)) (𝓝 0)
      (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)

Tactic:
simp only [hasBasis_nhds_zero.mem_iff, Prod.exists]

Premises used: Filter.HasBasis.mem_iff, ContinuousMultilinearMap.hasBasis_nhds_zero, Prod.exists
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
h :
  (Bornology.IsVonNBounded 𝕜 (E := (i : ι) → E i) (closedBall 0 ‖c‖) ∧
      Membership.mem (γ := Filter G) (𝓝 0) (closedBall 0 1)) ∧
    Subset (α := Set (ContinuousMultilinearMap 𝕜 E G))
      {f : ContinuousMultilinearMap 𝕜 E G |
        Set.MapsTo (α := (i : ι) → E i) (β := G) (⇑f : (a : (i : ι) → E i) → G) (closedBall 0 ‖c‖) (closedBall 0 1)}
      (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 1)
⊢ ∃ (r : ℝ) (a : Set ((i : ι) → E i)) (b : Set G),
    (Bornology.IsVonNBounded 𝕜 a ∧ Membership.mem (γ := Filter G) (𝓝 0) b) ∧
      Subset (α := Set (ContinuousMultilinearMap 𝕜 E G))
        {f : ContinuousMultilinearMap 𝕜 E G | Set.MapsTo (⇑f : (a : (i : ι) → E i) → G) a b}
        (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r)

Tactic:
use 1, closedBall 0 ‖c‖, closedBall 0 1

Premises used: Norm.norm, Metric.closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
this :
  ∀ (f : ContinuousMultilinearMap 𝕜 E G),
    (∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1) → ‖f‖ ≤ 1
⊢ (Bornology.IsVonNBounded 𝕜 (E := (i : ι) → E i) (closedBall 0 ‖c‖) ∧
      Membership.mem (γ := Filter G) (𝓝 0) (closedBall 0 1)) ∧
    Subset (α := Set (ContinuousMultilinearMap 𝕜 E G))
      {f : ContinuousMultilinearMap 𝕜 E G |
        Set.MapsTo (α := (i : ι) → E i) (β := G) (⇑f : (a : (i : ι) → E i) → G) (closedBall 0 ‖c‖) (closedBall 0 1)}
      (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 1)

Tactic:
simpa [NormedSpace.isVonNBounded_closedBall, closedBall_mem_nhds, Set.subset_def, Set.MapsTo]

Premises used: Metric.closedBall_mem_nhds, Set.subset_def, NormedSpace.isVonNBounded_closedBall, Set.MapsTo
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
h :
  ∀ (f : ContinuousMultilinearMap 𝕜 E G),
    (∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1) → ‖f‖ ≤ 1
⊢ (Bornology.IsVonNBounded 𝕜 (E := (i : ι) → E i) (closedBall 0 ‖c‖) ∧
      Membership.mem (γ := Filter G) (𝓝 0) (closedBall 0 1)) ∧
    Subset (α := Set (ContinuousMultilinearMap 𝕜 E G))
      {f : ContinuousMultilinearMap 𝕜 E G |
        Set.MapsTo (α := (i : ι) → E i) (β := G) (⇑f : (a : (i : ι) → E i) → G) (closedBall 0 ‖c‖) (closedBall 0 1)}
      (Seminorm.closedBall (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 1)

Tactic:
suffices ∀ f : ContinuousMultilinearMap 𝕜 E G, (∀ x, ‖x‖ ≤ ‖c‖ → ‖f x‖ ≤ 1) → ‖f‖ ≤ 1 by
      simpa [NormedSpace.isVonNBounded_closedBall, closedBall_mem_nhds, Set.subset_def, Set.MapsTo]
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1
⊢ LE.le (α := ℝ) 0 1

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1
h :
  ∀ (x : (i : ι) → E i) (hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖) (hx : ∀ (i : ι), ‖x i‖ < ‖c‖),
    Norm.norm.{wG} (E := G) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → G) x : G) ≤
      HMul.hMul (α := ℝ) 1 (∏ i : ι, ‖x i‖)
⊢ ‖f‖ ≤ 1

Tactic:
refine opNorm_le_bound (by positivity) <|
      f.1.bound_of_shell_of_continuous f.2 (fun _ ↦ hc₀) (fun _ ↦ hc) fun x hcx hx ↦ ?_

Premises used: ContinuousMultilinearMap.cont, ContinuousMultilinearMap.toMultilinearMap, MultilinearMap.bound_of_shell_of_continuous, ContinuousMultilinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1
x : (i : ι) → E i
hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖
hx : ∀ (i : ι), ‖x i‖ < ‖c‖
⊢ Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1

Tactic:
hf _ <| (pi_norm_le_iff_of_nonneg (norm_nonneg c)).2 fun i ↦ (hx i).le

Premises used: Iff.mpr, pi_norm_le_iff_of_nonneg, LT.lt.le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1
x : (i : ι) → E i
hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖
hx : ∀ (i : ι), ‖x i‖ < ‖c‖
⊢ Eq (α := ℝ) 1 (∏ i : ι, 1)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1
x : (i : ι) → E i
hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖
hx : ∀ (i : ι), ‖x i‖ < ‖c‖
h1 : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → 1 ≤ ‖x i‖
⊢ LE.le (α := ℝ) (∏ i : ι, 1) (∏ i : ι, ‖x i‖)

Tactic:
gcongr with i
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1
x : (i : ι) → E i
hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖
hx : ∀ (i : ι), ‖x i‖ < ‖c‖
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ 1 ≤ ‖x i‖

Tactic:
simpa only [div_self hc₀.ne'] using hcx i

Premises used: LT.lt.ne', div_self
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1
x : (i : ι) → E i
hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖
hx : ∀ (i : ι), ‖x i‖ < ‖c‖
⊢ ∏ i : ι, ‖x i‖ = HMul.hMul (α := ℝ) 1 (∏ i : ι, ‖x i‖)

Tactic:
(one_mul _).symm

Premises used: Eq.symm, one_mul
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ 1
x : (i : ι) → E i
hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖
hx : ∀ (i : ι), ‖x i‖ < ‖c‖
hf₁ : Eq (α := ℝ) 1 (∏ i : ι, 1)
hf₂ : LE.le (α := ℝ) (∏ i : ι, 1) (∏ i : ι, ‖x i‖)
⊢ Norm.norm.{wG} (E := G) ((f.toMultilinearMap (M₁ := E) : (a : (i : ι) → E i) → G) x : G) ≤
    HMul.hMul (α := ℝ) 1 (∏ i : ι, ‖x i‖)

Tactic:
calc
      ‖f x‖ ≤ 1 := hf _ <| (pi_norm_le_iff_of_nonneg (norm_nonneg c)).2 fun i ↦ (hx i).le
      _ = ∏ i : ι, 1 := by simp
      _ ≤ ∏ i, ‖x i‖ := by gcongr with i; simpa only [div_self hc₀.ne'] using hcx i
      _ = 1 * ∏ i, ‖x i‖ := (one_mul _).symm

Premises used: Iff.mpr, pi_norm_le_iff_of_nonneg, LT.lt.le, Eq.symm, DFunLike.coe, norm_nonneg, one_mul
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
h : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
refine_2 :
  ∀ (ε : ℝ) (hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε),
    ∃ r_1 > 0,
      Subset (α := Set (ContinuousMultilinearMap 𝕜 E G)) (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r_1)
        {f : ContinuousMultilinearMap 𝕜 E G |
          Set.MapsTo (β := G) (⇑f : (a : (i : ι) → E i) → G) (s, r).1 (closedBall 0 (s, r).2)}
⊢ ∃ r_1 > 0,
    Subset (α := Set (ContinuousMultilinearMap 𝕜 E G)) (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r_1)
      {f : ContinuousMultilinearMap 𝕜 E G |
        Set.MapsTo (β := G) (⇑f : (a : (i : ι) → E i) → G) (s, r).1 (closedBall 0 (s, r).2)}

Tactic:
rcases (NormedSpace.isVonNBounded_iff' _).1 hs with ⟨ε, hε⟩

Premises used: NormedSpace.isVonNBounded_iff', Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
h : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
refine_2 :
  ∀ (δ : ℝ) (hδ₀ : 0 < δ) (hδ : ε ^ Fintype.card ι * δ < (s, r).2),
    ∃ r_1 > 0,
      Subset (α := Set (ContinuousMultilinearMap 𝕜 E G)) (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r_1)
        {f : ContinuousMultilinearMap 𝕜 E G |
          Set.MapsTo (β := G) (⇑f : (a : (i : ι) → E i) → G) (s, r).1 (closedBall 0 (s, r).2)}
⊢ ∃ r_1 > 0,
    Subset (α := Set (ContinuousMultilinearMap 𝕜 E G)) (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r_1)
      {f : ContinuousMultilinearMap 𝕜 E G |
        Set.MapsTo (β := G) (⇑f : (a : (i : ι) → E i) → G) (s, r).1 (closedBall 0 (s, r).2)}

Tactic:
rcases exists_pos_mul_lt hr (ε ^ Fintype.card ι) with ⟨δ, hδ₀, hδ⟩

Premises used: Fintype.card, HPow.hPow, exists_pos_mul_lt
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
h : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
⊢ ∃ r_1 > 0,
    Subset (α := Set (ContinuousMultilinearMap 𝕜 E G)) (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 r_1)
      {f : ContinuousMultilinearMap 𝕜 E G |
        Set.MapsTo (β := G) (⇑f : (a : (i : ι) → E i) → G) (s, r).1 (closedBall 0 (s, r).2)}

Tactic:
⟨δ, hδ₀, fun f hf x hx ↦ ?_⟩

Premises used: And.intro, Exists.intro