awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ nnnorm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ ‖f‖₊ * ∏ i : ι, ‖m i‖₊

Tactic:
f.1.le_opNNNorm m

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.le_opNNNorm
-- 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
h : ‖f‖₊ ≤ C
m : ι → E
⊢ nnnorm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖₊

Tactic:
f.1.le_of_opNNNorm_le h m

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

Tactic:
f.1.opNNNorm_le_iff

Premises used: ContinuousMultilinearMap.opNNNorm_le_iff
-- 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 | ∀ (m : ι → E), nnnorm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖₊} ‖f‖₊

Tactic:
f.1.isLeast_opNNNorm

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

Tactic:
f.1.opNNNorm_prod g.1

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

Tactic:
f.1.opNorm_prod g.1

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.opNorm_prod, ContinuousMultilinearMap.prod
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Fintype ι
ι' : Type u_1
inst_4 : Fintype ι'
F : ι' → Type u_2
inst_5 : (i' : ι') → SeminormedAddCommGroup (F i')
inst_6 : (i' : ι') → NormedSpace.{u, u_2} 𝕜 (F i')
f : (i' : ι') → ContinuousAlternatingMap.{u, wE, u_2, v} 𝕜 E (F i') ι
⊢ ‖pi (M' := F) f‖₊ = ‖f‖₊

Tactic:
ContinuousMultilinearMap.opNNNorm_pi fun i ↦ (f i).1

Premises used: ContinuousMultilinearMap.pi, ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.opNNNorm_pi
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Fintype ι
ι' : Type u_1
inst_4 : Fintype ι'
F : ι' → Type u_2
inst_5 : (i' : ι') → SeminormedAddCommGroup (F i')
inst_6 : (i' : ι') → NormedSpace.{u, u_2} 𝕜 (F i')
f : (i' : ι') → ContinuousAlternatingMap.{u, wE, u_2, v} 𝕜 E (F i') ι
⊢ ‖pi (M' := F) f‖ = ‖f‖

Tactic:
ContinuousMultilinearMap.opNorm_pi fun i ↦ (f i).1

Premises used: ContinuousMultilinearMap.pi, ContinuousMultilinearMap.opNorm_pi, 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 ι
inst_6 : Subsingleton ι
i : ι
f : E →L[𝕜] F
⊢ norm (E := E [⋀^ι]→L[𝕜] F) ((ofSubsingleton 𝕜 E F i : (a : E →L[𝕜] F) → E [⋀^ι]→L[𝕜] F) f : E [⋀^ι]→L[𝕜] F) = ‖f‖

Tactic:
ContinuousMultilinearMap.norm_ofSubsingleton i f

Premises used: ContinuousMultilinearMap.norm_ofSubsingleton
-- 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 : Subsingleton ι
i : ι
f : E →L[𝕜] F
⊢ nnnorm (E := E [⋀^ι]→L[𝕜] F) ((ofSubsingleton 𝕜 E F i : (a : E →L[𝕜] F) → E [⋀^ι]→L[𝕜] F) f : E [⋀^ι]→L[𝕜] F) = ‖f‖₊

Tactic:
NNReal.eq <| norm_ofSubsingleton i f

Premises used: ContinuousAlternatingMap.norm_ofSubsingleton, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : Subsingleton ι
i : ι
⊢ norm (E := E [⋀^ι]→L[𝕜] E)
      ((ofSubsingleton 𝕜 E E i : (a : E →L[𝕜] E) → E [⋀^ι]→L[𝕜] E) (ContinuousLinearMap.id 𝕜 E) : E [⋀^ι]→L[𝕜] E) ≤
    1

Tactic:
ContinuousMultilinearMap.norm_ofSubsingleton_id_le ..

Premises used: ContinuousMultilinearMap.norm_ofSubsingleton_id_le
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : Subsingleton ι
i : ι
⊢ nnnorm (E := E [⋀^ι]→L[𝕜] E)
      ((ofSubsingleton 𝕜 E E i : (a : E →L[𝕜] E) → E [⋀^ι]→L[𝕜] E) (ContinuousLinearMap.id 𝕜 E) : E [⋀^ι]→L[𝕜] E) ≤
    1

Tactic:
ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le ..

Premises used: ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_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 ι
inst_6 : IsEmpty ι
x : F
⊢ norm (E := E [⋀^ι]→L[𝕜] F) (constOfIsEmpty 𝕜 E ι x) = ‖x‖

Tactic:
ContinuousMultilinearMap.norm_constOfIsEmpty _ _ _

Premises used: ContinuousMultilinearMap.constOfIsEmpty, ContinuousMultilinearMap.norm_constOfIsEmpty
-- 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 : IsEmpty ι
x : F
⊢ nnnorm (E := E [⋀^ι]→L[𝕜] F) (constOfIsEmpty 𝕜 E ι x) = ‖x‖₊

Tactic:
NNReal.eq <| norm_constOfIsEmpty _ _ _

Premises used: ContinuousAlternatingMap.norm_constOfIsEmpty, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f : E [⋀^ι]→L[𝕜] F
m : ι → E
inst_8 : IsEmpty ι
x : F
⊢ (fun (f : E [⋀^ι]→L[𝕜] F) ↦ ((f : (a : ι → E) → F) 0 : F)) (constOfIsEmpty 𝕜 E ι x) = x

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f_1 : E [⋀^ι]→L[𝕜] F
m : ι → E
inst_8 : IsEmpty ι
f : E [⋀^ι]→L[𝕜] F
H :
  ∀ (x : ι → E),
    Eq.{wF + 1} (α := F)
      ((constOfIsEmpty 𝕜 E ι ((fun (f : E [⋀^ι]→L[𝕜] F) ↦ ((f : (a : ι → E) → F) 0 : F)) f) : (a : ι → E) → F) x : F)
      ((f : (a : ι → E) → F) x : F)
⊢ constOfIsEmpty 𝕜 E ι ((fun (f : E [⋀^ι]→L[𝕜] F) ↦ ((f : (a : ι → E) → F) 0 : F)) f) = f

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f_1 : E [⋀^ι]→L[𝕜] F
m : ι → E
inst_8 : IsEmpty ι
f : E [⋀^ι]→L[𝕜] F
x : ι → E
⊢ Eq.{wF + 1} (α := F)
    ((constOfIsEmpty 𝕜 E ι ((fun (f : E [⋀^ι]→L[𝕜] F) ↦ ((f : (a : ι → E) → F) 0 : F)) f) : (a : ι → E) → F) x : F)
    ((f : (a : ι → E) → F) x : F)

Tactic:
simp [Subsingleton.allEq x 0]

Premises used: Subsingleton.allEq, OfNat.ofNat
-- 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
𝕜' : Type u_1
inst_6 : NontriviallyNormedField 𝕜'
inst_7 : NormedAlgebra 𝕜' 𝕜
inst_8 : NormedSpace 𝕜' F
inst_9 : IsScalarTower 𝕜' 𝕜 F
inst_10 : NormedSpace 𝕜' E
inst_11 : IsScalarTower 𝕜' 𝕜 E
⊢ norm (E := E [⋀^ι]→L[𝕜'] F) (restrictScalars 𝕜' f) = ‖f‖

Tactic:
rfl

Premises used: setOf, ContinuousMultilinearMap.restrictScalars, 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 ι
inst_6 : DecidableEq ι
f : E [⋀^ι]→L[𝕜] F
m₁ m₂ : ι → E
⊢ ‖HSub.hSub (α := F) (β := F) ((f : (a : ι → E) → F) m₁ : F) ((f : (a : ι → E) → F) m₂ : F)‖ ≤
    ‖f‖ * ∑ i : ι, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
f.1.norm_image_sub_le' m₁ m₂

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.norm_image_sub_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₁ m₂ : ι → E
⊢ ‖HSub.hSub (α := F) (β := F) ((f : (a : ι → E) → F) m₁ : F) ((f : (a : ι → E) → F) m₂ : F)‖ ≤
    ‖f‖ * (↑(Fintype.card ι) : ℝ) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

Tactic:
f.1.norm_image_sub_le m₁ m₂

Premises used: ContinuousMultilinearMap.norm_image_sub_le, 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 [⋀^ι]→ₗ[𝕜] F
C : ℝ
hC : 0 ≤ C
H : ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖
⊢ ‖f.mkContinuous C H‖ ≤ C

Tactic:
f.toMultilinearMap.mkContinuous_norm_le hC H

Premises used: MultilinearMap.mkContinuous, AlternatingMap.toMultilinearMap, MultilinearMap.mkContinuous_norm_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 [⋀^ι]→ₗ[𝕜] F
C : ℝ
H : ∀ (m : ι → E), norm.{wF} (E := F) ((f : (a : ι → E) → F) m : F) ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E
hbc : C ≤ max C 0
⊢ C * ∏ i : ι, ‖m i‖ ≤ max C 0 * ∏ i : ι, ‖m i‖

Tactic:
gcongr
-- 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‖
m : (i : ι) → E
⊢ C ≤ max C 0

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : F →L[𝕜] G
f : E [⋀^ι]→L[𝕜] F
⊢ ‖g.compContinuousAlternatingMap f‖ ≤ ‖g‖ * ‖f‖

Tactic:
g.norm_compContinuousMultilinearMap_le f.1

Premises used: ContinuousLinearMap.norm_compContinuousMultilinearMap_le, ContinuousLinearMap.compContinuousMultilinearMap, ContinuousAlternatingMap.toContinuousMultilinearMap
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f : F →L[𝕜] E [⋀^ι]→L[𝕜] G
v : ι → E
i j : ι
hv : v i = v j
hne : i ≠ j
h :
  ∀ (x : F),
    Eq.{wG + 1} (α := G)
      (((ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜 ∘SL f).flipMultilinear (E := fun (x : ι) ↦
                      E).toMultilinearMap
                  (M₁ := fun (x : ι) ↦ E).toFun
              (M₁ := fun (x : ι) ↦ E) v :
            (a : F) → G)
          x :
        G)
      ((0 : (a : F) → G) x : G)
⊢ (ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜 ∘SL f).flipMultilinear (E := fun (x : ι) ↦
              E).toMultilinearMap
          (M₁ := fun (x : ι) ↦ E).toFun
      (M₁ := fun (x : ι) ↦ E) v =
    0

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f : F →L[𝕜] E [⋀^ι]→L[𝕜] G
v : ι → E
i j : ι
hv : v i = v j
hne : i ≠ j
x : F
⊢ Eq.{wG + 1} (α := G)
    (((ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜 ∘SL f).flipMultilinear (E := fun (x : ι) ↦
                    E).toMultilinearMap
                (M₁ := fun (x : ι) ↦ E).toFun
            (M₁ := fun (x : ι) ↦ E) v :
          (a : F) → G)
        x :
      G)
    ((0 : (a : F) → G) x : G)

Tactic:
simp [(f x).map_eq_zero_of_eq v hv hne]

Premises used: ContinuousAlternatingMap.map_eq_zero_of_eq, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : F →ₗᵢ[𝕜] G
f : E [⋀^ι]→L[𝕜] F
⊢ ‖g.toContinuousLinearMap.compContinuousAlternatingMap f‖ = ‖f‖

Tactic:
g.norm_compContinuousMultilinearMap f.1

Premises used: ContinuousLinearMap.compContinuousMultilinearMap, LinearIsometry.norm_compContinuousMultilinearMap, ContinuousAlternatingMap.toContinuousMultilinearMap
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f : F [⋀^ι]→L[𝕜] G
g : E →L[𝕜] F
⊢ ‖f.toContinuousMultilinearMap‖ * ∏ i : ι, ‖g‖ = ‖f‖ * ‖g‖ ^ Fintype.card ι

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Finite ι
rcases :
  ∀ (val : Fintype ι), Continuous (X := E →L[𝕜] F) (Y := F [⋀^ι]→L[𝕜] G →L[𝕜] E [⋀^ι]→L[𝕜] G) compContinuousLinearMapCLM
⊢ Continuous (X := E →L[𝕜] F) (Y := F [⋀^ι]→L[𝕜] G →L[𝕜] E [⋀^ι]→L[𝕜] G) compContinuousLinearMapCLM

Tactic:
rcases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Finite ι
val : Fintype ι
⊢ Continuous (X := E →L[𝕜] F) (Y := F [⋀^ι]→L[𝕜] G →L[𝕜] E [⋀^ι]→L[𝕜] G) compContinuousLinearMapCLM

Tactic:
UniformConvergenceCLM.isUniformInducing_postcomp (.id 𝕜)
    (toContinuousMultilinearMapCLM 𝕜 : (E [⋀^ι]→L[𝕜] G) →L[𝕜] _)
    isUniformEmbedding_toContinuousMultilinearMap.isUniformInducing _ |>.isInducing
    |>.continuous_iff |>.mpr ?_

Premises used: Iff.mpr, ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, Topology.IsInducing.continuous_iff, IsUniformInducing.isInducing, IsUniformEmbedding.isUniformInducing, RingHom.id, ContinuousAlternatingMap.toContinuousMultilinearMapCLM, UniformConvergenceCLM, UniformConvergenceCLM.isUniformInducing_postcomp
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Finite ι
val : Fintype ι
refine :
  Continuous (X := E →L[𝕜] F) (Y :=
    UniformConvergenceCLM (RingHom.id 𝕜) (E := F [⋀^ι]→L[𝕜] G)
      (ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G)
      {S : Set (F [⋀^ι]→L[𝕜] G) | Bornology.IsVonNBounded 𝕜 S})
    (ContinuousLinearMap.comp (toContinuousMultilinearMapCLM 𝕜) ∘ compContinuousLinearMapCLM)
⊢ Continuous (X := E →L[𝕜] F) (Y := F [⋀^ι]→L[𝕜] G →L[𝕜] E [⋀^ι]→L[𝕜] G) compContinuousLinearMapCLM

Tactic:
refine UniformConvergenceCLM.isUniformInducing_postcomp (.id 𝕜)
    (toContinuousMultilinearMapCLM 𝕜 : (E [⋀^ι]→L[𝕜] G) →L[𝕜] _)
    isUniformEmbedding_toContinuousMultilinearMap.isUniformInducing _ |>.isInducing
    |>.continuous_iff |>.mpr ?_

Premises used: Iff.mpr, ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMap, Topology.IsInducing.continuous_iff, IsUniformInducing.isInducing, IsUniformEmbedding.isUniformInducing, RingHom.id, ContinuousAlternatingMap.toContinuousMultilinearMapCLM, UniformConvergenceCLM.isUniformInducing_postcomp
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Finite ι
val : Fintype ι
change :
  Continuous (X := E →L[𝕜] F) (Y := F [⋀^ι]→L[𝕜] G →L[𝕜] ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G)
    (Function.comp (β :=
      ContinuousMultilinearMap.{u, v, wF, wG} 𝕜 (fun (x : ι) ↦ F) G →L[𝕜]
        ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G)
      (⇑(ContinuousLinearMap.precomp (ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G)
            (toContinuousMultilinearMapCLM 𝕜)) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ F) G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G) →
          F [⋀^ι]→L[𝕜] G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G)
      (Function.comp (β := (i : ι) → E →L[𝕜] F)
        (⇑(ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 (fun (x : ι) ↦ E) (fun (x : ι) ↦ F)
              G) :
          (a : (i : ι) → E →L[𝕜] F) →
            ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ F) G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G)
        fun (f : E →L[𝕜] F) (x : ι) ↦ f))
⊢ Continuous (X := E →L[𝕜] F) (Y :=
    UniformConvergenceCLM (RingHom.id 𝕜) (E := F [⋀^ι]→L[𝕜] G)
      (ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G)
      {S : Set (F [⋀^ι]→L[𝕜] G) | Bornology.IsVonNBounded 𝕜 S})
    (ContinuousLinearMap.comp (toContinuousMultilinearMapCLM 𝕜) ∘ compContinuousLinearMapCLM)

Tactic:
change Continuous <|
    (toContinuousMultilinearMapCLM 𝕜 : (F [⋀^ι]→L[𝕜] G) →L[𝕜] _).precomp _ ∘
      ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜
        (fun _ : ι ↦ E) (fun _ ↦ F) G ∘
      (fun f _ ↦ f)

Premises used: Continuous, ContinuousLinearMap.precomp, ContinuousAlternatingMap.toContinuousMultilinearMapCLM, ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Finite ι
val : Fintype ι
⊢ Continuous (X := E →L[𝕜] F) (Y := F [⋀^ι]→L[𝕜] G →L[𝕜] ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G)
    (Function.comp (β :=
      ContinuousMultilinearMap.{u, v, wF, wG} 𝕜 (fun (x : ι) ↦ F) G →L[𝕜]
        ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G)
      (⇑(ContinuousLinearMap.precomp (ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G)
            (toContinuousMultilinearMapCLM 𝕜)) :
        (a : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ F) G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G) →
          F [⋀^ι]→L[𝕜] G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G)
      (Function.comp (β := (i : ι) → E →L[𝕜] F)
        (⇑(ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 (fun (x : ι) ↦ E) (fun (x : ι) ↦ F)
              G) :
          (a : (i : ι) → E →L[𝕜] F) →
            ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ F) G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G)
        fun (f : E →L[𝕜] F) (x : ι) ↦ f))

Tactic:
fun_prop