awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
i : ι
⊢ |g a i - g a₀ i| ≤ (↑K : ℝ) * dist a a₀

Tactic:
lipschitzWith_iff_dist_le_mul.1 (hg i) a a₀

Premises used: lipschitzWith_iff_dist_le_mul, Iff.mp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
i : ι
⊢ |g a i - g a₀ i| ≤ (↑K : ℝ) * dist a a₀

Tactic:
exact lipschitzWith_iff_dist_le_mul.1 (hg i) a a₀

Premises used: lipschitzWith_iff_dist_le_mul, Iff.mp
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
i : ι
⊢ |g a₀ i| ≤ M

Tactic:
hM ⟨i, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
i : ι
⊢ |g a₀ i| ≤ M

Tactic:
exact hM ⟨i, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith (β := ℝ) K fun (x : α) ↦ g x i
a₀ a : α
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : ι) ↦ ‖g a₀ i‖)) M
i : ι
a₁ : |g a i| = |g a i - g a₀ i + g a₀ i|
a₂ : |g a i - g a₀ i| + |g a₀ i| ≤ (↑K : ℝ) * dist a a₀ + M
⊢ (fun (i : ι) ↦ ‖g a i‖) i ≤ (↑K : ℝ) * dist a a₀ + M

Tactic:
calc
    |g a i| = |g a i - g a₀ i + g a₀ i| := by simp
    _ ≤ |g a i - g a₀ i| + |g a₀ i| := abs_add_le _ _
    _ ≤ ↑K * dist a a₀ + M := by
        gcongr
        · exact lipschitzWith_iff_dist_le_mul.1 (hg i) a a₀
        · exact hM ⟨i, rfl⟩

Premises used: Dist.dist, abs_add_le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
simp_rw :
  (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y) ↔
    ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
⊢ LipschitzOnWith K f s ↔
    ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s

Tactic:
simp_rw [lipschitzOnWith_iff_dist_le_mul]

Premises used: lipschitzOnWith_iff_dist_le_mul
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
mp :
  (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y) →
    ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
mpr :
  (∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y) →
    ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y
⊢ (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y) ↔
    ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hfl : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y
i : ι
x : α
hx : x ∈ s
y : α
hy : y ∈ s
simp : ‖(↑(f x) : (i : ι) → ℝ) i - (↑(f y) : (i : ι) → ℝ) i‖ ≤ ‖f x - f y‖
⊢ dist ((↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) ((↑(f y) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) ≤ dist (f x) (f y)

Tactic:
simp only [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hfl : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y
i : ι
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ‖(↑(f x) : (i : ι) → ℝ) i - (↑(f y) : (i : ι) → ℝ) i‖ ≤ ‖f x - f y‖

Tactic:
lp.norm_apply_le_norm top_ne_zero (f x - f y) i

Premises used: lp.norm_apply_le_norm, ENNReal.ofNNReal, Set.Mem, setOf, HSub.hSub, WithTop.some, ENNReal.top_ne_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hfl : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y
i : ι
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ‖(↑(f x) : (i : ι) → ℝ) i - (↑(f y) : (i : ι) → ℝ) i‖ ≤ ‖f x - f y‖

Tactic:
exact lp.norm_apply_le_norm top_ne_zero (f x - f y) i

Premises used: lp.norm_apply_le_norm, HSub.hSub, ENNReal.top_ne_zero
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hfl : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y
i : ι
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ dist (f x) (f y) ≤ (↑K : ℝ) * dist x y

Tactic:
hfl x hx y hy

Premises used: ENNReal.ofNNReal, Set.Mem, setOf, WithTop.some
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hfl : ∀ x ∈ s, ∀ y ∈ s, Dist.dist (f x) (f y) ≤ (↑K : ℝ) * Dist.dist x y
i : ι
x : α
hx : x ∈ s
y : α
hy : y ∈ s
dist :
  Dist.dist ((↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) ((↑(f y) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) ≤
    Dist.dist (f x) (f y)
⊢ Dist.dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * Dist.dist x y

Tactic:
calc
      dist (f x i) (f y i) ≤ dist (f x) (f y) := by
        simp only [dist_eq_norm]
        exact lp.norm_apply_le_norm top_ne_zero (f x - f y) i
      _ ≤ K * dist x y := hfl x hx y hy

Premises used: Dist.dist, Subtype.val
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hgl : ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
mpr : ‖f x - f y‖ ≤ (↑K : ℝ) * dist x y
⊢ dist (f x) (f y) ≤ (↑K : ℝ) * dist x y

Tactic:
rw [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hgl : ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
mpr : 0 ≤ (↑K : ℝ) * dist x y
mpr₁ : ∀ (i : ι), ‖(↑(f x - f y) : (i : ι) → ℝ) i‖ ≤ (↑K : ℝ) * dist x y
⊢ ‖f x - f y‖ ≤ (↑K : ℝ) * dist x y

Tactic:
apply lp.norm_le_of_forall_le

Premises used: lp.norm_le_of_forall_le
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hgl : ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ 0 ≤ (↑K : ℝ) * dist x y

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hgl : ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist ((↑(f x) : (i : ι) → ℝ) i) ((↑(f y) : (i : ι) → ℝ) i) ≤ (↑K : ℝ) * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
i : ι
⊢ ‖(↑(f x - f y) : (i : ι) → ℝ) i‖ ≤ (↑K : ℝ) * dist x y

Tactic:
apply hgl i x hx y hy
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
simp_rw :
  LipschitzOnWith K f Set.univ ↔ ∀ (i : ι), LipschitzOnWith (β := ℝ) K (fun (a : α) ↦ (↑(f a) : (i : ι) → ℝ) i) Set.univ
⊢ LipschitzWith K f ↔
    ∀ (i : ι), LipschitzWith (β := (fun (x : ι) ↦ ℝ) i) K fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i

Tactic:
simp_rw [← lipschitzOnWith_univ]

Premises used: lipschitzOnWith_univ
-- Module: Mathlib.Analysis.Normed.Lp.lpSpace
Goal:
α : Type u_3
ι : Type u_5
inst : PseudoMetricSpace α
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
⊢ LipschitzOnWith K f Set.univ ↔ ∀ (i : ι), LipschitzOnWith (β := ℝ) K (fun (a : α) ↦ (↑(f a) : (i : ι) → ℝ) i) Set.univ

Tactic:
apply LipschitzOnWith.coordinate

Premises used: LipschitzOnWith.coordinate
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : Finite ι
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : TopologicalSpace F
inst_5 : AddCommGroup F
inst_6 : IsTopologicalAddGroup F
inst_7 : Module 𝕜 F
⊢ ContinuousEval (E [⋀^ι]→L[𝕜] F) (ι → E) F

Tactic:
.of_continuous_forget continuous_toContinuousMultilinearMap

Premises used: ContinuousEval.of_continuous_forget, ContinuousAlternatingMap.continuous_toContinuousMultilinearMap
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E [⋀^ι]→ₗ[𝕜] F
hf : Continuous (X := ι → E) (Y := F) (⇑f : (a : ι → E) → F)
m : ι → E
i : ι
hi : ‖m i‖ = 0
⊢ norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) = 0

Tactic:
f.1.norm_map_coord_zero hf hi

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.norm_map_coord_zero
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→ₗ[𝕜] F
hf₀ : ∀ {m : ι → E} {i : ι}, ‖m i‖ = 0 → norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf :
  ∀ (m : ι → E),
    (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) →
      (∀ (i : ι), ‖m i‖ < ε i) → norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖
m : ι → E
⊢ norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
f.1.bound_of_shell_of_norm_map_coord_zero hf₀ hε hc hf m

Premises used: MultilinearMap.bound_of_shell_of_norm_map_coord_zero, AlternatingMap.toMultilinearMap
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→ₗ[𝕜] F
hfc : Continuous (X := ι → E) (Y := F) (⇑f : (a : ι → E) → F)
ε C : ℝ
hε : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf :
  ∀ (m : ι → E),
    (∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖) →
      (∀ (i : ι), ‖m i‖ < ε) → norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖
m : ι → E
⊢ norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
f.1.bound_of_shell_of_continuous hfc (fun _ ↦ hε) (fun _ ↦ hc) hf m

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.bound_of_shell_of_continuous
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→ₗ[𝕜] F
hf : Continuous (X := ι → E) (Y := F) (⇑f : (a : ι → E) → F)
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
f.1.exists_bound_of_continuous hf

Premises used: MultilinearMap.exists_bound_of_continuous, AlternatingMap.toMultilinearMap
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : E [⋀^ι]→ₗ[𝕜] F
C : ℝ
hC : 0 ≤ C
H : ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : ι → E
⊢ ‖HSub.hSub (α := F) (β := F) ((f : (a : ι → E) → F) m₁ : F) ((f : (a : ι → E) → F) m₂ : F)‖ ≤
    C * ∑ i : ι, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
f.toMultilinearMap.norm_image_sub_le_of_bound' hC H m₁ m₂

Premises used: MultilinearMap.norm_image_sub_le_of_bound', AlternatingMap.toMultilinearMap
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→ₗ[𝕜] F
C : ℝ
hC : 0 ≤ C
H : ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : ι → E
⊢ ‖HSub.hSub (α := F) (β := F) ((f : (a : ι → E) → F) m₁ : F) ((f : (a : ι → E) → F) m₂ : F)‖ ≤
    C * (↑(Fintype.card ι) : ℝ) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

Tactic:
f.toMultilinearMap.norm_image_sub_le_of_bound hC H m₁ m₂

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.norm_image_sub_le_of_bound
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→ₗ[𝕜] F
C : ℝ
H : ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖
⊢ Continuous (X := ι → E) (Y := F) (⇑f : (a : ι → E) → F)

Tactic:
f.toMultilinearMap.continuous_of_bound C H

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.continuous_of_bound
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→ₗ[𝕜] F
C : ℝ
H : ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖
⊢ Eq (α := (a : ι → E) → F) (⇑(f.mkContinuous C H) : (a : ι → E) → F) (⇑f : (a : ι → E) → F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
f.toContinuousMultilinearMap.bound

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.bound
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
⊢ ‖f.toContinuousMultilinearMap‖ = ‖f‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
⊢ ‖f.toContinuousMultilinearMap‖₊ = ‖f‖₊

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
⊢ ‖f.toContinuousMultilinearMap‖ₑ = ‖f‖ₑ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
⊢ ‖f‖ = sInf {c : ℝ | 0 ≤ c ∧ ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ c * ∏ i : ι, ‖m i‖}

Tactic:
rfl

Premises used: setOf, ContinuousMultilinearMap.opNorm, rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
⊢ ∃ (c : ℝ),
    Membership.mem (γ := Set ℝ)
      {c : ℝ | 0 ≤ c ∧ ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ c * ∏ i : ι, ‖m i‖} c

Tactic:
ContinuousMultilinearMap.bounds_nonempty

Premises used: Set.Mem, setOf, ContinuousMultilinearMap.bounds_nonempty
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
⊢ BddBelow (α := ℝ)
    {c : ℝ | 0 ≤ c ∧ ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ c * ∏ i : ι, ‖m i‖}

Tactic:
ContinuousMultilinearMap.bounds_bddBelow

Premises used: setOf, ContinuousMultilinearMap.bounds_bddBelow
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
⊢ IsLeast {c : ℝ | 0 ≤ c ∧ ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ c * ∏ i : ι, ‖m i‖} ‖f‖

Tactic:
f.1.isLeast_opNorm

Premises used: setOf, ContinuousMultilinearMap.isLeast_opNorm, ContinuousAlternatingMap.toContinuousMultilinearMap
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
m : ι → E
⊢ norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ ‖f‖ * ∏ i : ι, ‖m i‖

Tactic:
f.1.le_opNorm m

Premises used: ContinuousMultilinearMap.le_opNorm, ContinuousAlternatingMap.toContinuousMultilinearMap
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
m : ι → E
C : ℝ
b : ι → ℝ
hC : ‖f‖ ≤ C
hm : ∀ (i : ι), ‖m i‖ ≤ b i
⊢ norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, b i

Tactic:
f.1.le_mul_prod_of_opNorm_le_of_le hC hm

Premises used: ContinuousMultilinearMap.le_mul_prod_of_opNorm_le_of_le
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
m : ι → E
f : E [⋀^ι]→L[𝕜] F
b : ι → ℝ
hm : ∀ (i : ι), ‖m i‖ ≤ b i
⊢ norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ ‖f‖ * ∏ i : ι, b i

Tactic:
f.1.le_opNorm_mul_prod_of_le hm

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.le_opNorm_mul_prod_of_le
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
m : ι → E
b : ℝ
hm : ‖m‖ ≤ b
⊢ norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ ‖f‖ * b ^ Fintype.card ι

Tactic:
f.1.le_opNorm_mul_pow_card_of_le hm

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
f : E [⋀^Fin n]→L[𝕜] F
m : Fin n → E
b : ℝ
hm : ‖m‖ ≤ b
⊢ norm.{wF} (E := F) ((f : (a : Fin n → E) → F) m : F) ≤ ‖f‖ * b ^ n

Tactic:
f.1.le_opNorm_mul_pow_of_le hm

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.le_opNorm_mul_pow_of_le
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
C : ℝ
h : ‖f‖ ≤ C
m : ι → E
⊢ norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
f.1.le_of_opNorm_le h m

Premises used: ContinuousMultilinearMap.le_of_opNorm_le
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
m : ι → E
⊢ norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) / ∏ i : ι, ‖m i‖ ≤ ‖f‖

Tactic:
f.1.ratio_le_opNorm m

Premises used: ContinuousMultilinearMap.ratio_le_opNorm, ContinuousAlternatingMap.toContinuousMultilinearMap
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
m : ι → E
f : E [⋀^ι]→L[𝕜] F
h : ‖m‖ ≤ 1
⊢ norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ ‖f‖

Tactic:
f.1.unit_le_opNorm h

Premises used: ContinuousMultilinearMap.unit_le_opNorm, ContinuousAlternatingMap.toContinuousMultilinearMap
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
M : ℝ
hMp : 0 ≤ M
hM : ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ M * ∏ i : ι, ‖m i‖
⊢ ‖f‖ ≤ M

Tactic:
f.1.opNorm_le_bound hMp hM

Premises used: ContinuousMultilinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
C : ℝ
hC : 0 ≤ C
⊢ ‖f‖ ≤ C ↔ ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
f.1.opNorm_le_iff hC

Premises used: ContinuousMultilinearMap.opNorm_le_iff