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 ι
f : MultilinearMap 𝕜 E G
C : ℝ
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
⊢ Eq (α := (a : (i : ι) → E i) → G) (⇑(f.mkContinuous (E := E) C H) : (a : (i : ι) → E i) → G)
    (⇑f : (a : (i : ι) → E i) → G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : SeminormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
k n : ℕ
f : MultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (x : Fin n) ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : (i : Fin n) → G), norm.{wG'} (E := G') ((f : (a : (i : Fin n) → G) → G') m : G') ≤ C * ∏ i : Fin n, ‖m i‖
v : Fin k → G
rw :
  norm.{wG'} (E := G') ((f.restr s hk z : (a : (i : Fin k) → G) → G') v : G') ≤
    C * ((∏ i : Fin k, ‖v i‖) * ‖z‖ ^ (n - k))
⊢ norm.{wG'} (E := G') ((f.restr s hk z : (a : (i : Fin k) → G) → G') v : G') ≤ C * ‖z‖ ^ (n - k) * ∏ i : Fin k, ‖v i‖

Tactic:
rw [mul_right_comm, mul_assoc]

Premises used: mul_assoc, mul_right_comm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : SeminormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
k n : ℕ
f : MultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (x : Fin n) ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : (i : Fin n) → G), norm.{wG'} (E := G') ((f : (a : (i : Fin n) → G) → G') m : G') ≤ C * ∏ i : Fin n, ‖m i‖
v : Fin k → G
⊢ norm.{wG'} (E := G')
      ((f : (a : (i : Fin n) → G) → G') fun (j : Fin n) ↦
          if h : j ∈ s then
            v ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k) (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) j h))
          else z :
        G') ≤
    C *
      ∏ i : Fin n,
        norm.{wG} (E := G)
          (if h : i ∈ s then
            v ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k) (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) i h))
          else z)

Tactic:
H _
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : SeminormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
k n : ℕ
f : MultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (x : Fin n) ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : (i : Fin n) → G), norm.{wG'} (E := G') ((f : (a : (i : Fin n) → G) → G') m : G') ≤ C * ∏ i : Fin n, ‖m i‖
v : Fin k → G
h :
  (∏ i : Fin k, ‖v i‖) * ‖z‖ ^ (n - k) =
    ∏ i : Fin n,
      norm.{wG} (E := G)
        (if h : i ∈ s then
          v ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k) (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) i h))
        else z)
⊢ norm.{wG'} (E := G') ((f.restr s hk z : (a : (i : Fin k) → G) → G') v : G') ≤
    C * ((∏ i : Fin k, ‖v i‖) * ‖z‖ ^ (n - k))

Tactic:
convert! H _ using 2
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : SeminormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
k n : ℕ
f : MultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (x : Fin n) ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : (i : Fin n) → G), norm.{wG'} (E := G') ((f : (a : (i : Fin n) → G) → G') m : G') ≤ C * ∏ i : Fin n, ‖m i‖
v : Fin k → G
h :
  (∏ i : ↥s, ‖v ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k) i)‖) * ‖z‖ ^ (n - k) =
    (∏ a : ↥s,
        ‖v
            ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k)
              (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) (↑a : Fin n) ⋯))‖) *
      ‖z‖ ^ (n - k)
⊢ (∏ i : Fin k, ‖v i‖) * ‖z‖ ^ (n - k) =
    ∏ i : Fin n,
      norm.{wG} (E := G)
        (if h : i ∈ s then
          v ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k) (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) i h))
        else z)

Tactic:
simp only [apply_dite norm, Fintype.prod_dite, prod_const ‖z‖, Finset.card_univ,
    Fintype.card_of_subtype sᶜ fun _ => mem_compl, card_compl, Fintype.card_fin, hk, ←
    (s.orderIsoOfFin hk).symm.bijective.prod_comp fun x => ‖v x‖]

Premises used: Norm.norm, Fintype.prod_dite, Finset.card_univ, apply_dite, Finset.orderIsoOfFin, Fintype.card_fin, OrderIso.bijective, Compl.compl, Finset.card_compl, Finset.mem_compl, Finset.prod_const, OrderIso.symm, Function.Bijective.prod_comp, Fintype.card_of_subtype
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : SeminormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
k n : ℕ
f : MultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (x : Fin n) ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : (i : Fin n) → G), norm.{wG'} (E := G') ((f : (a : (i : Fin n) → G) → G') m : G') ≤ C * ∏ i : Fin n, ‖m i‖
v : Fin k → G
⊢ (∏ i : ↥s, ‖v ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k) i)‖) * ‖z‖ ^ (n - k) =
    (∏ i : ↥s, ‖v ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k) i)‖) * ‖z‖ ^ (n - k)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : SeminormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
k n : ℕ
f : MultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (x : Fin n) ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : (i : Fin n) → G), norm.{wG'} (E := G') ((f : (a : (i : Fin n) → G) → G') m : G') ≤ C * ∏ i : Fin n, ‖m i‖
v : Fin k → G
⊢ (∏ i : ↥s, ‖v ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k) i)‖) * ‖z‖ ^ (n - k) =
    (∏ a : ↥s,
        ‖v
            ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k)
              (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) (↑a : Fin n) ⋯))‖) *
      ‖z‖ ^ (n - k)

Tactic:
convert! rfl

Premises used: rfl
-- 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
⊢ ∃ (C : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
f.toMultilinearMap.exists_bound_of_continuous f.2

Premises used: MultilinearMap.exists_bound_of_continuous, ContinuousMultilinearMap.cont, ContinuousMultilinearMap.toMultilinearMap
-- 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
⊢ ‖f‖ =
    sInf
      {c : ℝ |
        0 ≤ c ∧
          ∀ (m : (i : ι) → E i), Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ c * ∏ i : ι, ‖m i‖}

Tactic:
rfl

Premises used: ContinuousMultilinearMap.opNorm, rfl
-- 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
⊢ ∃ (c : ℝ),
    Membership.mem (γ := Set ℝ)
      {c : ℝ |
        0 ≤ c ∧
          ∀ (m : (i : ι) → E i), Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ c * ∏ i : ι, ‖m i‖}
      c

Tactic:
let ⟨M, hMp, hMb⟩ := f.bound
  ⟨M, le_of_lt hMp, hMb⟩

Premises used: setOf, le_of_lt, Membership.mem, Exists, LE.le, And, _private.0.ContinuousMultilinearMap.bounds_nonempty.match_1, And.intro, Exists.intro, ContinuousMultilinearMap.bound, 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 ι
f : ContinuousMultilinearMap 𝕜 E G
⊢ BddBelow (α := ℝ)
    {c : ℝ |
      0 ≤ c ∧ ∀ (m : (i : ι) → E i), Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ c * ∏ i : ι, ‖m i‖}

Tactic:
⟨0, fun _ ⟨hn, _⟩ => hn⟩

Premises used: _private.0.ContinuousMultilinearMap.bounds_bddBelow.match_1, LE.le, Set.Nonempty, BddBelow, Exists.intro, 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 ι
f : ContinuousMultilinearMap 𝕜 E G
⊢ IsLeast
    {c : ℝ |
      0 ≤ c ∧ ∀ (m : (i : ι) → E i), Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ c * ∏ i : ι, ‖m i‖}
    ‖f‖

Tactic:
IsClosed.isLeast_csInf ?_ bounds_nonempty bounds_bddBelow

Premises used: ContinuousMultilinearMap.bounds_bddBelow, ContinuousMultilinearMap.bounds_nonempty, IsClosed.isLeast_csInf, ContinuousMultilinearMap.opNorm
-- 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
refine :
  IsClosed (X := ℝ)
    {c : ℝ |
      0 ≤ c ∧ ∀ (m : (i : ι) → E i), Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ c * ∏ i : ι, ‖m i‖}
⊢ IsLeast
    {c : ℝ |
      0 ≤ c ∧ ∀ (m : (i : ι) → E i), Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ c * ∏ i : ι, ‖m i‖}
    ‖f‖

Tactic:
refine IsClosed.isLeast_csInf ?_ bounds_nonempty bounds_bddBelow

Premises used: ContinuousMultilinearMap.bounds_bddBelow, ContinuousMultilinearMap.bounds_nonempty, IsClosed.isLeast_csInf
-- 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
simp :
  IsClosed (X := ℝ)
    ({a : ℝ | 0 ≤ a} ∩
      ⋂ (i : (i : ι) → E i),
        {x : ℝ | Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) i : G) ≤ x * ∏ i_1 : ι, ‖i i_1‖})
⊢ IsClosed (X := ℝ)
    {c : ℝ |
      0 ≤ c ∧ ∀ (m : (i : ι) → E i), Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ c * ∏ i : ι, ‖m i‖}

Tactic:
simp only [Set.setOf_and, Set.setOf_forall]

Premises used: Set.setOf_and, Set.setOf_forall
-- 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
m : (i : ι) → E i
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ x * ∏ i : ι, ‖m i‖

Tactic:
fun_prop
-- 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
⊢ IsClosed (X := ℝ)
    ({a : ℝ | 0 ≤ a} ∩
      ⋂ (i : (i : ι) → E i),
        {x : ℝ | Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) i : G) ≤ x * ∏ i_1 : ι, ‖i i_1‖})

Tactic:
exact isClosed_Ici.inter (isClosed_iInter fun m ↦ isClosed_le continuous_const (by fun_prop))

Premises used: continuous_const, isClosed_le, IsClosed.inter, isClosed_iInter, isClosed_Ici
-- 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
⊢ 0 ≤ ‖f‖

Tactic:
Real.sInf_nonneg fun _ ⟨hx, _⟩ => hx

Premises used: _private.0.ContinuousMultilinearMap.bounds_bddBelow.match_1, LE.le, Real.sInf_nonneg, OfNat.ofNat, ContinuousMultilinearMap.opNorm
-- 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
m : (i : ι) → E i
⊢ Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ ‖f‖ * ∏ i : ι, ‖m i‖

Tactic:
f.isLeast_opNorm.1.2 m

Premises used: ContinuousMultilinearMap.isLeast_opNorm, And.right, And.left
-- 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
m : (i : ι) → E i
C : ℝ
b : ι → ℝ
hC : ‖f‖ ≤ C
hm : ∀ (i : ι), ‖m i‖ ≤ b i
b0 : 0 ≤ C
h₂ : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → ‖m i‖ ≤ b i
⊢ ‖f‖ * ∏ i : ι, ‖m i‖ ≤ C * ∏ i : ι, b i

Tactic:
gcongr
-- 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
m : (i : ι) → E i
C : ℝ
b : ι → ℝ
hC : ‖f‖ ≤ C
hm : ∀ (i : ι), ‖m i‖ ≤ b i
⊢ 0 ≤ C

Tactic:
f.opNorm_nonneg.trans hC

Premises used: ContinuousMultilinearMap.opNorm_nonneg, LE.le.trans
-- 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
m : (i : ι) → E i
C : ℝ
b : ι → ℝ
hC : ‖f‖ ≤ C
hm : ∀ (i : ι), ‖m i‖ ≤ b i
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ ‖m i‖ ≤ b i

Tactic:
hm _
-- 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
m : (i : ι) → E i
C : ℝ
b : ι → ℝ
hC : ‖f‖ ≤ C
hm : ∀ (i : ι), ‖m i‖ ≤ b i
⊢ 0 ≤ C

Tactic:
exacts [f.opNorm_nonneg.trans hC, hm _]

Premises used: ContinuousMultilinearMap.opNorm_nonneg, LE.le.trans
-- 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
m : (i : ι) → E i
b : ι → ℝ
hm : ∀ (i : ι), ‖m i‖ ≤ b i
⊢ Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ ‖f‖ * ∏ i : ι, b i

Tactic:
le_mul_prod_of_opNorm_le_of_le le_rfl hm

Premises used: ContinuousMultilinearMap.le_mul_prod_of_opNorm_le_of_le, le_rfl
-- 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
m : (i : ι) → E i
b : ℝ
hm : ‖m‖ ≤ b
⊢ Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ ‖f‖ * b ^ Fintype.card ι

Tactic:
simpa only [prod_const] using f.le_opNorm_mul_prod_of_le fun i => (norm_le_pi_norm m i).trans hm

Premises used: norm_le_pi_norm, Finset.prod_const, ContinuousMultilinearMap.le_opNorm_mul_prod_of_le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
n : ℕ
Ei : Fin n → Type u_1
inst_3 : (i : Fin n) → SeminormedAddCommGroup (Ei i)
inst_4 : (i : Fin n) → NormedSpace.{u, u_1} 𝕜 (Ei i)
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n) → Ei i
b : ℝ
hm : ‖m‖ ≤ b
⊢ Norm.norm.{wG} (E := G) ((f : (a : (i : Fin n) → Ei i) → G) m : G) ≤ ‖f‖ * b ^ n

Tactic:
simpa only [Fintype.card_fin] using f.le_opNorm_mul_pow_card_of_le hm

Premises used: Fintype.card_fin, ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le
-- 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
C : ℝ
h : ‖f‖ ≤ C
m : (i : ι) → E i
⊢ Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
le_mul_prod_of_opNorm_le_of_le h fun _ ↦ le_rfl

Premises used: ContinuousMultilinearMap.le_mul_prod_of_opNorm_le_of_le, le_rfl
-- 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
m : (i : ι) → E i
⊢ LE.le (α := ℝ) 0 (∏ i : ι, ‖m i‖)

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 ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
h : ‖m‖ ≤ 1
⊢ ‖f‖ * HPow.hPow (α := ℝ) 1 (Fintype.card ι) ≤ ‖f‖

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 ι
f : ContinuousMultilinearMap 𝕜 E G
M : ℝ
hMp : 0 ≤ M
hM : ∀ (m : (i : ι) → E i), Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ M * ∏ i : ι, ‖m i‖
⊢ ‖f‖ ≤ M

Tactic:
csInf_le bounds_bddBelow ⟨hMp, hM⟩

Premises used: ContinuousMultilinearMap.bounds_bddBelow, And.intro, csInf_le, ContinuousMultilinearMap.opNorm
-- 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
C : ℝ
hC : 0 ≤ C
⊢ ‖f‖ ≤ C ↔ ∀ (m : (i : ι) → E i), Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
⟨fun h _ ↦ le_of_opNorm_le h _, opNorm_le_bound hC⟩

Premises used: Iff.intro, ContinuousMultilinearMap.le_of_opNorm_le, 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 ι
f g : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
rw : Norm.norm.{wG} (E := G) ((f + g : (a : (i : ι) → E i) → G) x : G) ≤ ‖f‖ * ∏ i : ι, ‖x i‖ + ‖g‖ * ∏ i : ι, ‖x i‖
⊢ Norm.norm.{wG} (E := G) ((f + g : (a : (i : ι) → E i) → G) x : G) ≤ (‖f‖ + ‖g‖) * ∏ i : ι, ‖x i‖

Tactic:
rw [add_mul]

Premises used: add_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 ι
f g : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ Norm.norm.{wG} (E := G) ((f + g : (a : (i : ι) → E i) → G) x : G) ≤ ‖f‖ * ∏ i : ι, ‖x i‖ + ‖g‖ * ∏ i : ι, ‖x i‖

Tactic:
norm_add_le_of_le (le_opNorm _ _) (le_opNorm _ _)

Premises used: ContinuousMultilinearMap.le_opNorm, norm_add_le_of_le
-- 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 g : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ Norm.norm.{wG} (E := G) ((f + g : (a : (i : ι) → E i) → G) x : G) ≤ ‖f‖ * ∏ i : ι, ‖x i‖ + ‖g‖ * ∏ i : ι, ‖x i‖

Tactic:
exact norm_add_le_of_le (le_opNorm _ _) (le_opNorm _ _)

Premises used: norm_add_le_of_le
-- 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 ι
m : (i : ι) → E i
⊢ Norm.norm.{wG} (E := G) ((0 : (a : (i : ι) → E i) → G) m : G) ≤ HMul.hMul (α := ℝ) 0 (∏ i : ι, ‖m i‖)

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 ι
f : ContinuousMultilinearMap 𝕜 E G
⊢ ‖-f‖ = ‖f‖

Tactic:
simp [norm_def]

Premises used: ContinuousMultilinearMap.norm_def