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 ι
inst_6 : DecidableEq ι
f : ContinuousMultilinearMap 𝕜 E G
m₁ m₂ : (i : ι) → E i
⊢ ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G) ((f : (a : (i : ι) → E i) → G) m₂ : G)‖ ≤
    ‖f‖ * ∑ 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' (norm_nonneg _) f.le_opNorm _ _

Premises used: MultilinearMap.norm_image_sub_le_of_bound', ContinuousMultilinearMap.le_opNorm, ContinuousMultilinearMap.toMultilinearMap, 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 ι
f : ContinuousMultilinearMap 𝕜 E G
m₁ m₂ : (i : ι) → E i
⊢ ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G) ((f : (a : (i : ι) → E i) → G) m₂ : G)‖ ≤
    ‖f‖ * (↑(Fintype.card ι) : ℝ) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

Tactic:
f.toMultilinearMap.norm_image_sub_le_of_bound (norm_nonneg _) f.le_opNorm _ _

Premises used: ContinuousMultilinearMap.le_opNorm, MultilinearMap.norm_image_sub_le_of_bound, ContinuousMultilinearMap.toMultilinearMap, 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 ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
⊢ ‖f.mkContinuous (E := E) C H‖ ≤ C

Tactic:
ContinuousMultilinearMap.opNorm_le_bound hC fun m => H m

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

Tactic:
positivity
-- 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 : ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n) ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
hC : 0 ≤ ‖f‖ * ‖z‖ ^ (n - k)
⊢ ‖f.restr s hk z‖ ≤ ‖f‖ * ‖z‖ ^ (n - k)

Tactic:
apply MultilinearMap.mkContinuous_norm_le

Premises used: MultilinearMap.mkContinuous_norm_le
-- 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 : ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n) ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
⊢ 0 ≤ ‖f‖ * ‖z‖ ^ (n - k)

Tactic:
mul_nonneg (norm_nonneg _) (pow_nonneg (norm_nonneg _) _)

Premises used: mul_nonneg, pow_nonneg, norm_nonneg
-- 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 : ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n) ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
⊢ 0 ≤ ‖f‖ * ‖z‖ ^ (n - k)

Tactic:
exact mul_nonneg (norm_nonneg _) (pow_nonneg (norm_nonneg _) _)

Premises used: mul_nonneg, pow_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : Nonempty ι
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) ≤ 1

Tactic:
opNorm_le_bound zero_le_one fun m => ?_

Premises used: zero_le_one, ContinuousMultilinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : Nonempty ι
refine :
  ∀ (m : (i : ι) → A),
    norm.{u_1} (E := A)
        (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
              (a : (i : ι) → A) → A)
            m :
          A) ≤
      HMul.hMul (α := ℝ) 1 (∏ i : ι, ‖m i‖)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) ≤ 1

Tactic:
refine opNorm_le_bound zero_le_one fun m => ?_

Premises used: zero_le_one, ContinuousMultilinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : Nonempty ι
m : (i : ι) → A
simp : norm.{u_1} (E := A) (∏ i : ι, m i) ≤ ∏ i : ι, ‖m i‖
⊢ norm.{u_1} (E := A)
      (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
            (a : (i : ι) → A) → A)
          m :
        A) ≤
    HMul.hMul (α := ℝ) 1 (∏ i : ι, ‖m i‖)

Tactic:
simp only [ContinuousMultilinearMap.mkPiAlgebra_apply, one_mul]

Premises used: ContinuousMultilinearMap.mkPiAlgebra_apply, one_mul
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : Nonempty ι
m : (i : ι) → A
⊢ norm.{u_1} (E := A) (∏ i : ι, m i) ≤ ∏ i : ι, ‖m i‖

Tactic:
norm_prod_le' _ univ_nonempty _

Premises used: Finset.univ_nonempty, Finset.norm_prod_le'
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : Nonempty ι
m : (i : ι) → A
⊢ norm.{u_1} (E := A) (∏ i : ι, m i) ≤ ∏ i : ι, ‖m i‖

Tactic:
exact norm_prod_le' _ univ_nonempty _

Premises used: Finset.univ_nonempty, Finset.norm_prod_le'
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsEmpty ι
a :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) ≤
    norm.{u_1} (E := A) 1
a₁ :
  norm.{u_1} (E := A) 1 ≤
    norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) =
    norm.{u_1} (E := A) 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsEmpty ι
a : 0 ≤ norm.{u_1} (E := A) 1
a₁ :
  ∀ (m : (i : ι) → A),
    norm.{u_1} (E := A)
        (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
              (a : (i : ι) → A) → A)
            m :
          A) ≤
      norm.{u_1} (E := A) 1 * ∏ i : ι, ‖m i‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) ≤
    norm.{u_1} (E := A) 1

Tactic:
apply opNorm_le_bound

Premises used: ContinuousMultilinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsEmpty ι
⊢ 0 ≤ norm.{u_1} (E := A) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsEmpty ι
⊢ ∀ (m : (i : ι) → A),
    norm.{u_1} (E := A)
        (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
              (a : (i : ι) → A) → A)
            m :
          A) ≤
      norm.{u_1} (E := A) 1 * ∏ i : ι, ‖m i‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsEmpty ι
⊢ norm.{u_1} (E := A)
        (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
              (a : (i : ι) → A) → A)
            fun (x : ι) ↦ 1 :
          A) /
      ∏ i : ι, norm.{u_1} (E := A) 1 ≤
    norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A)

Tactic:
ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun _ => 1

Premises used: ContinuousMultilinearMap.ratio_le_opNorm, OfNat.ofNat, ContinuousMultilinearMap.mkPiAlgebra
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsEmpty ι
h :
  norm.{u_1} (E := A) 1 =
    norm.{u_1} (E := A)
        (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
              (a : (i : ι) → A) → A)
            fun (x : ι) ↦ 1 :
          A) /
      ∏ i : ι, norm.{u_1} (E := A) 1
⊢ norm.{u_1} (E := A) 1 ≤
    norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A)

Tactic:
convert! ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun _ => 1

Premises used: ContinuousMultilinearMap.ratio_le_opNorm, OfNat.ofNat, ContinuousMultilinearMap.mkPiAlgebra
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsEmpty ι
⊢ norm.{u_1} (E := A) 1 =
    norm.{u_1} (E := A)
        (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
              (a : (i : ι) → A) → A)
            fun (x : ι) ↦ 1 :
          A) /
      ∏ i : ι, norm.{u_1} (E := A) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : NormOneClass A
inl :
  IsEmpty ι →
    norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) = 1
inr :
  Nonempty ι →
    norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) = 1
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) = 1

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : NormOneClass A
h : IsEmpty ι
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) = 1

Tactic:
simp [norm_mkPiAlgebra_of_empty]

Premises used: ContinuousMultilinearMap.norm_mkPiAlgebra_of_empty
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : NormOneClass A
h : Nonempty ι
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) = 1

Tactic:
le_antisymm norm_mkPiAlgebra_le ?_

Premises used: ContinuousMultilinearMap.norm_mkPiAlgebra_le, le_antisymm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : NormOneClass A
h : Nonempty ι
inr : 1 ≤ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) = 1

Tactic:
refine le_antisymm norm_mkPiAlgebra_le ?_

Premises used: ContinuousMultilinearMap.norm_mkPiAlgebra_le, le_antisymm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : NormOneClass A
h : Nonempty ι
⊢ norm.{u_1} (E := A)
        (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
              (a : (i : ι) → A) → A)
            fun (x : ι) ↦ 1 :
          A) /
      ∏ i : ι, norm.{u_1} (E := A) 1 ≤
    norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A)

Tactic:
ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun _ => 1

Premises used: ContinuousMultilinearMap.ratio_le_opNorm, OfNat.ofNat, ContinuousMultilinearMap.mkPiAlgebra
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : NormOneClass A
h_1 : Nonempty ι
h :
  1 =
    norm.{u_1} (E := A)
        (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
              (a : (i : ι) → A) → A)
            fun (x : ι) ↦ 1 :
          A) /
      ∏ i : ι, norm.{u_1} (E := A) 1
⊢ 1 ≤ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A)

Tactic:
convert! ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun _ => 1

Premises used: ContinuousMultilinearMap.ratio_le_opNorm, OfNat.ofNat, ContinuousMultilinearMap.mkPiAlgebra
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
A : Type u_1
inst_2 : NormedCommRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : NormOneClass A
h : Nonempty ι
⊢ 1 =
    norm.{u_1} (E := A)
        (((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ A) A) :
              (a : (i : ι) → A) → A)
            fun (x : ι) ↦ 1 :
          A) /
      ∏ i : ι, norm.{u_1} (E := A) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A) ≤
    1

Tactic:
opNorm_le_bound zero_le_one fun m => ?_

Premises used: zero_le_one, ContinuousMultilinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
refine :
  ∀ (m : (i : Fin n.succ) → A),
    norm (E := A) ((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A : (a : (i : Fin n.succ) → A) → A) m : A) ≤
      HMul.hMul (α := ℝ) 1 (∏ i : Fin n.succ, ‖m i‖)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A) ≤
    1

Tactic:
refine opNorm_le_bound zero_le_one fun m => ?_

Premises used: zero_le_one, ContinuousMultilinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
m : (i : Fin n.succ) → A
simp :
  ‖(List.map m (List.finRange n.succ)).prod‖ ≤
    List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))
⊢ norm (E := A) ((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A : (a : (i : Fin n.succ) → A) → A) m : A) ≤
    HMul.hMul (α := ℝ) 1 (∏ i : Fin n.succ, ‖m i‖)

Tactic:
simp only [ContinuousMultilinearMap.mkPiAlgebraFin_apply, one_mul, List.ofFn_eq_map,
    Fin.prod_univ_def]

Premises used: ContinuousMultilinearMap.mkPiAlgebraFin_apply, Fin.prod_univ_def, List.ofFn_eq_map, one_mul
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
m : (i : Fin n.succ) → A
⊢ ‖(List.map m (List.finRange n.succ)).prod‖ ≤
    List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))

Tactic:
(List.norm_prod_le' ?_).trans_eq ?_

Premises used: LE.le.trans_eq, List.norm_prod_le'
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
m : (i : Fin n.succ) → A
refine_1 : List.map m (List.finRange n.succ) ≠ []
refine_2 :
  (List.map norm (List.map m (List.finRange n.succ))).prod =
    List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))
⊢ ‖(List.map m (List.finRange n.succ)).prod‖ ≤
    List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))

Tactic:
refine (List.norm_prod_le' ?_).trans_eq ?_

Premises used: LE.le.trans_eq, List.norm_prod_le'
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
m : (i : Fin n.succ) → A
refine_1 : ¬n.succ = 0
⊢ List.map m (List.finRange n.succ) ≠ []

Tactic:
rw [Ne, List.map_eq_nil_iff, List.finRange_eq_nil_iff]

Premises used: List.map_eq_nil_iff, List.finRange_eq_nil_iff, Ne
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
m : (i : Fin n.succ) → A
⊢ ¬n.succ = 0

Tactic:
Nat.succ_ne_zero _

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
m : (i : Fin n.succ) → A
⊢ ¬n.succ = 0

Tactic:
exact Nat.succ_ne_zero _

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
m : (i : Fin n.succ) → A
refine_2 :
  (List.map (norm ∘ m) (List.finRange n.succ)).prod =
    List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))
refine_2₁ refine_2₂ :
  Eq (α := ℝ) (List.prod (List.map (fun (x : Fin n.succ) ↦ ‖m x‖) (List.finRange n.succ)))
    (List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ)))
⊢ (List.map norm (List.map m (List.finRange n.succ))).prod =
    List.prod (List.map (fun (i : Fin n.succ) ↦ ‖m i‖) (List.finRange n.succ))

Tactic:
rw [List.map_map, Function.comp_def]

Premises used: List.map_map, Function.comp_def
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
hn : 0 < n
obtain :
  ∀ (n : ℕ) (hn : 0 < n.succ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ A) A)
        (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A) ≤
      1
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A) ≤ 1

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'

Premises used: LT.lt.ne', Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
n : ℕ
hn : 0 < n.succ
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A) ≤
    1

Tactic:
norm_mkPiAlgebraFin_succ_le

Premises used: ContinuousMultilinearMap.norm_mkPiAlgebraFin_succ_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
n : ℕ
hn : 0 < n.succ
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ A) A)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A) ≤
    1

Tactic:
exact norm_mkPiAlgebraFin_succ_le

Premises used: ContinuousMultilinearMap.norm_mkPiAlgebraFin_succ_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) =
    norm.{u_1} (E := A) 1

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
refine_1 :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) ≤
    norm.{u_1} (E := A) 1
refine_2 :
  norm.{u_1} (E := A) 1 ≤
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) =
    norm.{u_1} (E := A) 1

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) ≤
    norm.{u_1} (E := A) 1

Tactic:
opNorm_le_bound (norm_nonneg (1 : A)) ?_

Premises used: ContinuousMultilinearMap.opNorm_le_bound, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
A : Type u_1
inst_1 : SeminormedRing A
inst_2 : NormedAlgebra 𝕜 A
refine_1 :
  ∀ (m : (i : Fin 0) → A),
    norm (E := A) ((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A : (a : (i : Fin 0) → A) → A) m : A) ≤
      norm.{u_1} (E := A) 1 * ∏ i : Fin 0, ‖m i‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) ≤
    norm.{u_1} (E := A) 1

Tactic:
refine opNorm_le_bound (norm_nonneg (1 : A)) ?_

Premises used: ContinuousMultilinearMap.opNorm_le_bound, OfNat.ofNat, norm_nonneg