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 ι
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
refine_2 :
  ∀ (f : ContinuousMultilinearMap 𝕜 E G)
    (hf :
      Membership.mem (γ := Set (ContinuousMultilinearMap 𝕜 E G))
        (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 δ) f)
    (x : (i : ι) → E i) (hx : x ∈ (s, r).1),
    Membership.mem.{wG, wG} (α := G) (γ := Set G) (closedBall 0 (s, r).2) ((f : (a : (i : ι) → E i) → G) x : G)
⊢ ∃ 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:
refine ⟨δ, hδ₀, fun f hf x hx ↦ ?_⟩
-- 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_1 : 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
f : ContinuousMultilinearMap 𝕜 E G
hf :
  Membership.mem (γ := Set (ContinuousMultilinearMap 𝕜 E G))
    (Seminorm.ball (ContinuousMultilinearMap.seminorm 𝕜 E G) 0 δ) f
x : (i : ι) → E i
hx : x ∈ (s, r).1
refine_2 :
  ∀ (hf : (ContinuousMultilinearMap.seminorm 𝕜 E G : (a : ContinuousMultilinearMap 𝕜 E G) → ℝ) f < δ),
    Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ r
⊢ Membership.mem.{wG, wG} (α := G) (γ := Set G) (closedBall 0 (s, r).2) ((f : (a : (i : ι) → E i) → G) x : G)

Tactic:
simp only [Seminorm.mem_ball_zero, mem_closedBall_zero_iff] at hf ⊢

Premises used: Seminorm.mem_ball_zero, mem_closedBall_zero_iff
-- 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_1 : 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
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hx : x ∈ (s, r).1
hf : (ContinuousMultilinearMap.seminorm 𝕜 E G : (a : ContinuousMultilinearMap 𝕜 E G) → ℝ) f < δ
⊢ ‖f‖ ≤ δ

Tactic:
replace hf : ‖f‖ ≤ δ := hf.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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x_1 : 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
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hx : x ∈ (s, r).1
hf : ‖f‖ ≤ δ
⊢ ‖x‖ ≤ ε

Tactic:
replace hx : ‖x‖ ≤ ε := hε x hx
-- 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_1 : 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
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
⊢ Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ ‖f‖ * ε ^ Fintype.card ι

Tactic:
le_opNorm_mul_pow_card_of_le f hx

Premises used: 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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x_1 : 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
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
⊢ 0 ≤ ε

Tactic:
have := (norm_nonneg x).trans hx
-- 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_1 : 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
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
this : 0 ≤ ε
ha : 0 ≤ ε ^ Fintype.card ι
⊢ ‖f‖ * ε ^ Fintype.card ι ≤ δ * ε ^ Fintype.card ι

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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x_1 : 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
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
⊢ δ * ε ^ Fintype.card ι ≤ r

Tactic:
(mul_comm _ _).trans_le hδ.le

Premises used: LT.lt.le, Eq.trans_le, mul_comm
-- 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_1 : 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
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
ε₁ : ‖f‖ * ε ^ Fintype.card ι ≤ δ * ε ^ Fintype.card ι
⊢ Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) x : G) ≤ r

Tactic:
calc
      ‖f x‖ ≤ ‖f‖ * ε ^ Fintype.card ι := le_opNorm_mul_pow_card_of_le f hx
      _ ≤ δ * ε ^ Fintype.card ι := by have := (norm_nonneg x).trans hx; gcongr
      _ ≤ r := (mul_comm _ _).trans_le hδ.le

Premises used: Fintype.card, LT.lt.le, Eq.trans_le, ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le, mul_comm, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
𝕜' : Type u_1
inst_11 : SeminormedRing 𝕜'
inst_12 : Module 𝕜' G
inst_13 : IsBoundedSMul 𝕜' G
inst_14 : SMulCommClass 𝕜 𝕜' G
⊢ IsBoundedSMul 𝕜' (ContinuousMultilinearMap 𝕜 E G)

Tactic:
.of_norm_smul_le opNorm_smul_le

Premises used: ContinuousMultilinearMap.opNorm_smul_le, IsBoundedSMul.of_norm_smul_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
m : (i : ι) → E i
push_cast : Norm.norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ ‖f‖ * ∏ x : ι, ‖m x‖
⊢ (↑(nnnorm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G)) : ℝ) ≤ (↑(‖f‖₊ * ∏ i : ι, ‖m i‖₊) : ℝ)

Tactic:
push_cast
-- 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‖ * ∏ x : ι, ‖m x‖

Tactic:
f.le_opNorm m

Premises used: ContinuousMultilinearMap.le_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‖ * ∏ x : ι, ‖m x‖

Tactic:
exact f.le_opNorm m

Premises used: ContinuousMultilinearMap.le_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 : ℝ≥0
h : ‖f‖₊ ≤ C
m : (i : ι) → E i
⊢ nnnorm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖₊

Tactic:
(f.le_opNNNorm m).trans <| mul_le_mul' h le_rfl

Premises used: le_rfl, LE.le.trans, ContinuousMultilinearMap.le_opNNNorm, mul_le_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 : ContinuousMultilinearMap 𝕜 E G
C : ℝ≥0
⊢ (↑‖f‖₊ : ℝ) ≤ (↑C : ℝ) ↔
    ∀ (m : (i : ι) → E i),
      (↑(nnnorm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G)) : ℝ) ≤ (↑(C * ∏ i : ι, ‖m i‖₊) : ℝ)

Tactic:
simp [opNorm_le_iff C.coe_nonneg, NNReal.coe_prod]

Premises used: NNReal.coe_prod, NNReal.coe_nonneg, ContinuousMultilinearMap.opNorm_le_iff
-- 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 | ∀ (m : (i : ι) → E i), nnnorm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖₊}
    ‖f‖₊

Tactic:
simpa only [← opNNNorm_le_iff] using isLeast_Ici

Premises used: isLeast_Ici, ContinuousMultilinearMap.opNNNorm_le_iff
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
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 : SeminormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
inst_7 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
g : ContinuousMultilinearMap 𝕜 E G'
x : ℝ≥0
⊢ ‖f.prod (M₁ := E) g‖₊ ≤ x ↔ max ‖f‖₊ ‖g‖₊ ≤ x

Tactic:
simp only [opNNNorm_le_iff, prod_apply, Prod.nnnorm_def, max_le_iff, forall_and]

Premises used: Prod.nnnorm_def, max_le_iff, ContinuousMultilinearMap.opNNNorm_le_iff, ContinuousMultilinearMap.prod_apply, forall_and
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
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 : SeminormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
inst_7 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
g : ContinuousMultilinearMap 𝕜 E G'
⊢ ‖f.prod (M₁ := E) g‖ = max ‖f‖ ‖g‖

Tactic:
congr_arg NNReal.toReal (opNNNorm_prod f g)

Premises used: congr_arg, ContinuousMultilinearMap.opNNNorm_prod, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E' : ι' → Type wE'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : Fintype ι
inst_5 : (i' : ι') → SeminormedAddCommGroup (E' i')
inst_6 : (i' : ι') → NormedSpace.{u, wE'} 𝕜 (E' i')
f : (i' : ι') → ContinuousMultilinearMap.{u, v, wE, wE'} 𝕜 E (E' i')
x : ℝ≥0
⊢ ‖pi (M₁ := E) (M' := E') f‖₊ ≤ x ↔ ‖f‖₊ ≤ x

Tactic:
simpa [opNNNorm_le_iff, pi_nnnorm_le_iff] using forall_comm

Premises used: pi_nnnorm_le_iff, forall_comm, ContinuousMultilinearMap.opNNNorm_le_iff
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : Fintype ι
ι' : Type v'
inst_4 : Fintype ι'
E' : ι' → Type wE'
inst_5 : (i' : ι') → SeminormedAddCommGroup (E' i')
inst_6 : (i' : ι') → NormedSpace.{u, wE'} 𝕜 (E' i')
f : (i' : ι') → ContinuousMultilinearMap.{u, v, wE, wE'} 𝕜 E (E' i')
⊢ ‖pi (M₁ := E) (M' := E') f‖ = ‖f‖

Tactic:
congr_arg NNReal.toReal (opNNNorm_pi f)

Premises used: Multiset.foldr, Finset.fold, NNReal.mk, NNReal, congr_arg, ContinuousMultilinearMap.opNNNorm_pi, Finset.sup, NNReal.toReal, Multiset.fold
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : SeminormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
inst_5 : Fintype ι
inst_6 : Subsingleton ι
i : ι
f : G →L[𝕜] G'
this : Unique ι := uniqueOfSubsingleton i
⊢ Norm.norm (E := ContinuousMultilinearMap.{u, v, wG, wG'} 𝕜 (fun (x : ι) ↦ G) G')
      ((ofSubsingleton 𝕜 G G' i : (a : G →L[𝕜] G') → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) G') f :
        ContinuousMultilinearMap.{u, v, wG, wG'} 𝕜 (fun (x : ι) ↦ G) G') =
    ‖f‖

Tactic:
simp [norm_def, ContinuousLinearMap.norm_def, (Equiv.funUnique _ _).symm.surjective.forall]

Premises used: Function.Surjective.forall, ContinuousLinearMap.norm_def, Equiv.funUnique, Equiv.surjective, Equiv.symm, ContinuousMultilinearMap.norm_def
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : SeminormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
inst_5 : Fintype ι
inst_6 : Subsingleton ι
i : ι
f : G →L[𝕜] G'
⊢ nnnorm (E := ContinuousMultilinearMap.{u, v, wG, wG'} 𝕜 (fun (x : ι) ↦ G) G')
      ((ofSubsingleton 𝕜 G G' i : (a : G →L[𝕜] G') → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) G') f :
        ContinuousMultilinearMap.{u, v, wG, wG'} 𝕜 (fun (x : ι) ↦ G) G') =
    ‖f‖₊

Tactic:
NNReal.eq <| norm_ofSubsingleton i f

Premises used: NNReal.eq, ContinuousMultilinearMap.norm_ofSubsingleton
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : Fintype ι
inst_4 : Subsingleton ι
i : ι
rw : Norm.norm (E := G →L[𝕜] G) (ContinuousLinearMap.id 𝕜 G) ≤ 1
⊢ Norm.norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) G)
      ((ofSubsingleton 𝕜 G G i : (a : G →L[𝕜] G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) G)
          (ContinuousLinearMap.id 𝕜 G) :
        ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) G) ≤
    1

Tactic:
rw [norm_ofSubsingleton]

Premises used: ContinuousMultilinearMap.norm_ofSubsingleton
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : Fintype ι
inst_4 : Subsingleton ι
i : ι
⊢ Norm.norm (E := G →L[𝕜] G) (ContinuousLinearMap.id 𝕜 G) ≤ 1

Tactic:
apply ContinuousLinearMap.norm_id_le

Premises used: ContinuousLinearMap.norm_id_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : Fintype ι
inst_4 : Subsingleton ι
i : ι
⊢ nnnorm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) G)
      ((ofSubsingleton 𝕜 G G i : (a : G →L[𝕜] G) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) G)
          (ContinuousLinearMap.id 𝕜 G) :
        ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) G) ≤
    1

Tactic:
norm_ofSubsingleton_id_le _ _ _

Premises used: ContinuousMultilinearMap.norm_ofSubsingleton_id_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 ι
inst_6 : IsEmpty ι
x : G
a : Norm.norm (E := ContinuousMultilinearMap 𝕜 E G) (constOfIsEmpty 𝕜 E x) ≤ ‖x‖
a₁ : ‖x‖ ≤ Norm.norm (E := ContinuousMultilinearMap 𝕜 E G) (constOfIsEmpty 𝕜 E x)
⊢ Norm.norm (E := ContinuousMultilinearMap 𝕜 E G) (constOfIsEmpty 𝕜 E x) = ‖x‖

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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 ι
inst_6 : IsEmpty ι
x : G
⊢ Norm.norm (E := ContinuousMultilinearMap 𝕜 E G) (constOfIsEmpty 𝕜 E x) ≤ ‖x‖

Tactic:
opNorm_le_bound (norm_nonneg _) fun x => ?_

Premises used: ContinuousMultilinearMap.opNorm_le_bound, 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 ι
inst_6 : IsEmpty ι
x : G
a :
  ∀ (x_1 : (i : ι) → E i),
    Norm.norm.{wG} (E := G) ((constOfIsEmpty 𝕜 E x : (a : (i : ι) → E i) → G) x_1 : G) ≤ ‖x‖ * ∏ i : ι, ‖x_1 i‖
⊢ Norm.norm (E := ContinuousMultilinearMap 𝕜 E G) (constOfIsEmpty 𝕜 E x) ≤ ‖x‖

Tactic:
refine opNorm_le_bound (norm_nonneg _) fun x => ?_

Premises used: ContinuousMultilinearMap.opNorm_le_bound, 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 ι
inst_6 : IsEmpty ι
x_1 : G
x : (i : ι) → E i
a : Norm.norm.{wG} (E := G) ((constOfIsEmpty 𝕜 E x_1 : (a : (i : ι) → E i) → G) x : G) ≤ ‖x_1‖ * 1
a₁ : Norm.norm.{wG} (E := G) ((constOfIsEmpty 𝕜 E x_1 : (a : (i : ι) → E i) → G) x : G) ≤ ‖x_1‖
a₂ a₃ : ‖x_1‖ ≤ ‖x_1‖
⊢ Norm.norm.{wG} (E := G) ((constOfIsEmpty 𝕜 E x_1 : (a : (i : ι) → E i) → G) x : G) ≤ ‖x_1‖ * ∏ i : ι, ‖x i‖

Tactic:
rw [Fintype.prod_empty, mul_one, constOfIsEmpty_apply]

Premises used: ContinuousMultilinearMap.constOfIsEmpty_apply, mul_one, Fintype.prod_empty
-- 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 ι
inst_6 : IsEmpty ι
x : G
⊢ ‖x‖ ≤ Norm.norm (E := ContinuousMultilinearMap 𝕜 E G) (constOfIsEmpty 𝕜 E x)

Tactic:
simpa using (constOfIsEmpty 𝕜 E x).le_opNorm 0

Premises used: ContinuousMultilinearMap.le_opNorm, ContinuousMultilinearMap.constOfIsEmpty, 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 ι
inst_6 : IsEmpty ι
x : G
⊢ nnnorm (E := ContinuousMultilinearMap 𝕜 E G) (constOfIsEmpty 𝕜 E x) = ‖x‖₊

Tactic:
NNReal.eq <| norm_constOfIsEmpty _ _ _

Premises used: NNReal.eq, ContinuousMultilinearMap.norm_constOfIsEmpty
-- 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 : NontriviallyNormedField 𝕜'
inst_7 : NormedAlgebra 𝕜' 𝕜
inst_8 : NormedSpace 𝕜' G
inst_9 : IsScalarTower 𝕜' 𝕜 G
inst_10 : (i : ι) → NormedSpace.{u_1, wE} 𝕜' (E i)
inst_11 : ∀ (i : ι), IsScalarTower.{u_1, u, wE} 𝕜' 𝕜 (E i)
f : ContinuousMultilinearMap 𝕜 E G
⊢ Norm.norm (E := ContinuousMultilinearMap 𝕜' E G) (restrictScalars 𝕜' (M₁ := E) f) = ‖f‖

Tactic:
rfl

Premises used: setOf, ContinuousMultilinearMap.restrictScalars, ContinuousMultilinearMap.opNorm, rfl