awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E₁ G
k : ℕ
x : (i : ι) → E₁ i
h :
  ∀ (e : Fin k ↪ ι),
    Membership.mem (γ := Finset (Fin k ↪ ι)) univ e →
      norm (E := ContinuousMultilinearMap 𝕜 (fun (x : Fin k) ↦ (i : ι) → E₁ i) G)
          ((f.iteratedFDerivComponent (E₁ := E₁) (s := Set.range (ι := Fin k) (⇑e : (a : Fin k) → ι)) e.toEquivRange :
              (a : (i : { a : ι // a ∉ Set.range (⇑e : (a : Fin k) → ι) }) → E₁ (↑i : ι)) →
                ContinuousMultilinearMap 𝕜 (fun (x : Fin k) ↦ (i : ι) → E₁ i) G)
            fun (i : { a : ι // a ∉ Set.range (ι := Fin k) (⇑e : (a : Fin k) → ι) }) ↦ x (↑i : ι)) ≤
        ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)
⊢ LE.le (α := ℝ)
    (∑ e : Fin k ↪ ι,
      norm (E := ContinuousMultilinearMap 𝕜 (fun (x : Fin k) ↦ (i : ι) → E₁ i) G)
        ((f.iteratedFDerivComponent (E₁ := E₁) (s := Set.range (ι := Fin k) (⇑e : (a : Fin k) → ι)) e.toEquivRange :
            (a : (i : { a : ι // a ∉ Set.range (⇑e : (a : Fin k) → ι) }) → E₁ (↑i : ι)) →
              ContinuousMultilinearMap 𝕜 (fun (x : Fin k) ↦ (i : ι) → E₁ i) G)
          fun (i : { a : ι // a ∉ Set.range (ι := Fin k) (⇑e : (a : Fin k) → ι) }) ↦ x (↑i : ι)))
    (∑ x_1 : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k))

Tactic:
gcongr with e _
-- 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
k : ℕ
x : (i : ι) → E₁ i
e : Fin k ↪ ι
h : Membership.mem (γ := Finset (Fin k ↪ ι)) univ e
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (x : Fin k) ↦ (i : ι) → E₁ i) G)
      ((f.iteratedFDerivComponent (E₁ := E₁) (s := Set.range (ι := Fin k) (⇑e : (a : Fin k) → ι)) e.toEquivRange :
          (a : (i : { a : ι // a ∉ Set.range (⇑e : (a : Fin k) → ι) }) → E₁ (↑i : ι)) →
            ContinuousMultilinearMap 𝕜 (fun (x : Fin k) ↦ (i : ι) → E₁ i) G)
        fun (i : { a : ι // a ∉ Set.range (ι := Fin k) (⇑e : (a : Fin k) → ι) }) ↦ x (↑i : ι)) ≤
    ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Tactic:
simpa using norm_iteratedFDerivComponent_le f e.toEquivRange x

Premises used: ContinuousMultilinearMap.norm_iteratedFDerivComponent_le, Function.Embedding.toEquivRange
-- 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
k : ℕ
x : (i : ι) → E₁ i
⊢ ∑ x_1 : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) =
    (↑((Fintype.card ι).descFactorial k) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Tactic:
simp [card_univ, mul_assoc]

Premises used: Finset.card_univ, mul_assoc
-- 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
k : ℕ
x : (i : ι) → E₁ i
calc :
  LE.le (α := ℝ)
    (∑ e : Fin k ↪ ι,
      norm (E := ContinuousMultilinearMap 𝕜 (fun (x : Fin k) ↦ (i : ι) → E₁ i) G)
        ((f.iteratedFDerivComponent (E₁ := E₁) (s := Set.range (ι := Fin k) (⇑e : (a : Fin k) → ι)) e.toEquivRange :
            (a : (i : { a : ι // a ∉ Set.range (⇑e : (a : Fin k) → ι) }) → E₁ (↑i : ι)) →
              ContinuousMultilinearMap 𝕜 (fun (x : Fin k) ↦ (i : ι) → E₁ i) G)
          fun (i : { a : ι // a ∉ Set.range (ι := Fin k) (⇑e : (a : Fin k) → ι) }) ↦ x (↑i : ι)))
    (∑ x_1 : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k))
calc₁ :
  ∑ x_1 : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) =
    (↑((Fintype.card ι).descFactorial k) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)
⊢ ‖f.iteratedFDeriv (E₁ := E₁) k x‖ ≤ (↑((Fintype.card ι).descFactorial k) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Tactic:
calc ‖f.iteratedFDeriv k x‖
  _ ≤ ∑ e : Fin k ↪ ι, ‖iteratedFDerivComponent f e.toEquivRange (fun i ↦ x i)‖ := norm_sum_le _ _
  _ ≤ ∑ _ : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
    gcongr with e _
    simpa using norm_iteratedFDerivComponent_le f e.toEquivRange x
  _ = Nat.descFactorial (Fintype.card ι) k * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
    simp [card_univ, mul_assoc]

Premises used: HSub.hSub, Fintype.card, ContinuousMultilinearMap.iteratedFDeriv, Fin, norm_sum_le, Nat.descFactorial
-- 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
k : ℕ
x : (i : ι) → E₁ i
calc :
  LE.le (α := ℝ)
    (∑ e : Fin k ↪ ι,
      norm (E := ContinuousMultilinearMap 𝕜 (fun (x : Fin k) ↦ (i : ι) → E₁ i) G)
        ((f.iteratedFDerivComponent (E₁ := E₁) (s := Set.range (ι := Fin k) (⇑e : (a : Fin k) → ι)) e.toEquivRange :
            (a : (i : { a : ι // a ∉ Set.range (⇑e : (a : Fin k) → ι) }) → E₁ (↑i : ι)) →
              ContinuousMultilinearMap 𝕜 (fun (x : Fin k) ↦ (i : ι) → E₁ i) G)
          fun (i : { a : ι // a ∉ Set.range (ι := Fin k) (⇑e : (a : Fin k) → ι) }) ↦ x (↑i : ι)))
    (∑ x_1 : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k))
calc₁ :
  ∑ x_1 : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) =
    (↑((Fintype.card ι).descFactorial k) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)
⊢ ‖f.iteratedFDeriv (E₁ := E₁) k x‖ ≤ (↑((Fintype.card ι).descFactorial k) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Tactic:
classical
  calc ‖f.iteratedFDeriv k x‖
  _ ≤ ∑ e : Fin k ↪ ι, ‖iteratedFDerivComponent f e.toEquivRange (fun i ↦ x i)‖ := norm_sum_le _ _
  _ ≤ ∑ _ : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
    gcongr with e _
    simpa using norm_iteratedFDerivComponent_le f e.toEquivRange x
  _ = Nat.descFactorial (Fintype.card ι) k * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
    simp [card_univ, mul_assoc]

Premises used: HSub.hSub, Fintype.card, ContinuousMultilinearMap.iteratedFDeriv, Fin, norm_sum_le, Nat.descFactorial
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : Fintype ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
⊢ ‖f‖ = 0 ↔ f = 0

Tactic:
simp [← (opNorm_nonneg f).ge_iff_eq', opNorm_le_iff le_rfl, ContinuousMultilinearMap.ext_iff]

Premises used: le_rfl, ContinuousMultilinearMap.opNorm_nonneg, LE.le.ge_iff_eq', ContinuousMultilinearMap.ext_iff, ContinuousMultilinearMap.opNorm_le_iff
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
G : Type wG
inst : Fintype ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace 𝕜 G
inst_4 : Subsingleton ι
inst_5 : Nontrivial G
i : ι
⊢ 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:
simp [ContinuousLinearMap.norm_id]

Premises used: ContinuousLinearMap.norm_id
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
G : Type wG
inst : Fintype ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace 𝕜 G
inst_4 : Subsingleton ι
inst_5 : Nontrivial G
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:
NNReal.eq <| norm_ofSubsingleton_id ..

Premises used: NNReal.eq, ContinuousMultilinearMap.norm_ofSubsingleton_id
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : Fintype ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : MultilinearMap 𝕜 E G
ε : ι → ℝ
C : ℝ
c : ι → 𝕜
hε : ∀ (i : ι), 0 < ε i
hc : ∀ (i : ι), 1 < ‖c i‖
hf :
  ∀ (m : (i : ι) → E i),
    (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) →
      (∀ (i : ι), ‖m i‖ < ε i) → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m m_1 : (i : ι) → E i
i : ι
h : ‖m_1 i‖ = 0
rw : norm.{wG} (E := G) 0 = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m_1 : G) = 0

Tactic:
rw [map_coord_zero f _ (norm_eq_zero.1 h), norm_zero]

Premises used: norm_eq_zero, norm_zero, MultilinearMap.map_coord_zero, Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
i : Fin (n + 1)
f : Ei i →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (j : Fin n) ↦ Ei (i.succAbove j)) G
m : (i : Fin n.succ) → Ei i
rw :
  norm.{wG} (E := G)
      ((((f : (a : Ei i) → ContinuousMultilinearMap 𝕜 (fun (j : Fin n) ↦ Ei (i.succAbove j)) G) (m i) :
              ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (j : Fin n) ↦ Ei (i.succAbove j)) G) :
            (a : (i_1 : Fin n) → Ei (i.succAbove i_1)) → G)
          (i.removeNth (α := Ei) m) :
        G) ≤
    ‖f‖ * ‖m i‖ * ∏ i_1 : Fin n, norm (E := Ei (i.succAbove i_1)) (m (i.succAbove i_1))
⊢ norm.{wG} (E := G)
      ((((f : (a : Ei i) → ContinuousMultilinearMap 𝕜 (fun (j : Fin n) ↦ Ei (i.succAbove j)) G) (m i) :
              ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (j : Fin n) ↦ Ei (i.succAbove j)) G) :
            (a : (i_1 : Fin n) → Ei (i.succAbove i_1)) → G)
          (i.removeNth (α := Ei) m) :
        G) ≤
    ‖f‖ * ∏ j : Fin n.succ, ‖m j‖

Tactic:
rw [i.prod_univ_succAbove, ← mul_assoc]

Premises used: mul_assoc, Fin.prod_univ_succAbove
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
i : Fin (n + 1)
f : Ei i →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (j : Fin n) ↦ Ei (i.succAbove j)) G
m : (i : Fin n.succ) → Ei i
⊢ norm.{wG} (E := G)
      ((((f : (a : Ei i) → ContinuousMultilinearMap 𝕜 (fun (j : Fin n) ↦ Ei (i.succAbove j)) G) (m i) :
              ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (j : Fin n) ↦ Ei (i.succAbove j)) G) :
            (a : (i_1 : Fin n) → Ei (i.succAbove i_1)) → G)
          (i.removeNth (α := Ei) m) :
        G) ≤
    ‖f‖ * ‖m i‖ * ∏ i_1 : Fin n, norm (E := Ei (i.succAbove i_1)) (m (i.succAbove i_1))

Tactic:
(f (m i)).le_of_opNorm_le (f.le_opNorm _) _

Premises used: ContinuousLinearMap.le_opNorm, Fin.removeNth, ContinuousMultilinearMap.le_of_opNorm_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
i : Fin (n + 1)
f : Ei i →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (j : Fin n) ↦ Ei (i.succAbove j)) G
m : (i : Fin n.succ) → Ei i
⊢ norm.{wG} (E := G)
      ((((f : (a : Ei i) → ContinuousMultilinearMap 𝕜 (fun (j : Fin n) ↦ Ei (i.succAbove j)) G) (m i) :
              ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (j : Fin n) ↦ Ei (i.succAbove j)) G) :
            (a : (i_1 : Fin n) → Ei (i.succAbove i_1)) → G)
          (i.removeNth (α := Ei) m) :
        G) ≤
    ‖f‖ * ‖m i‖ * ∏ i_1 : Fin n, norm (E := Ei (i.succAbove i_1)) (m (i.succAbove i_1))

Tactic:
exact (f (m i)).le_of_opNorm_le (f.le_opNorm _) _

Premises used: ContinuousLinearMap.le_opNorm, ContinuousMultilinearMap.le_of_opNorm_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G
m : (i : Fin n.succ) → Ei i
⊢ norm.{wG} (E := G)
      ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) (m 0) :
              ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
            (a : (i : Fin n) → Ei i.succ) → G)
          (tail (α := Ei) m) :
        G) ≤
    ‖f‖ * ∏ i : Fin n.succ, ‖m i‖

Tactic:
ContinuousLinearMap.norm_map_removeNth_le (i := 0) f m

Premises used: Fin.succAbove, Fin.succ, Fin.removeNth, Fin.tail, ContinuousLinearMap.norm_map_removeNth_le, ite
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f :
  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
    (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
m : (i : Fin n.succ) → Ei i
rw :
  norm.{wG} (E := G)
      ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) (init (α := Ei) m) :
              ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
            (a : Ei (last n)) → G)
          (m (last n)) :
        G) ≤
    (‖f‖ * ∏ i : Fin n, norm (E := Ei i.castSucc) (m i.castSucc)) * norm (E := Ei (last n)) (m (last n))
⊢ norm.{wG} (E := G)
      ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) (init (α := Ei) m) :
              ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
            (a : Ei (last n)) → G)
          (m (last n)) :
        G) ≤
    ‖f‖ * ∏ i : Fin n.succ, ‖m i‖

Tactic:
rw [prod_univ_castSucc, ← mul_assoc]

Premises used: mul_assoc, Fin.prod_univ_castSucc
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f :
  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
    (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
m : (i : Fin n.succ) → Ei i
⊢ norm.{wG} (E := G)
      ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) (init (α := Ei) m) :
              ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
            (a : Ei (last n)) → G)
          (m (last n)) :
        G) ≤
    (‖f‖ * ∏ i : Fin n, norm (E := Ei i.castSucc) (m i.castSucc)) * norm (E := Ei (last n)) (m (last n))

Tactic:
(f (init m)).le_of_opNorm_le (f.le_opNorm _) _

Premises used: ContinuousMultilinearMap.le_opNorm, Fin.init, ContinuousLinearMap.le_of_opNorm_le, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f :
  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
    (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
m : (i : Fin n.succ) → Ei i
⊢ norm.{wG} (E := G)
      ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) (init (α := Ei) m) :
              ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
            (a : Ei (last n)) → G)
          (m (last n)) :
        G) ≤
    (‖f‖ * ∏ i : Fin n, norm (E := Ei i.castSucc) (m i.castSucc)) * norm (E := Ei (last n)) (m (last n))

Tactic:
exact (f (init m)).le_of_opNorm_le (f.le_opNorm _) _

Premises used: ContinuousMultilinearMap.le_opNorm, Fin.init, ContinuousLinearMap.le_of_opNorm_le, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
i : Fin (n + 1)
x : Ei i
m : (j : Fin n) → Ei (i.succAbove j)
⊢ norm.{wG} (E := G) ((f : (a : (i : Fin n.succ) → Ei i) → G) (i.insertNth (α := Ei) x m) : G) ≤
    ‖f‖ * ‖x‖ * ∏ i_1 : Fin n, ‖m i_1‖

Tactic:
simpa [i.prod_univ_succAbove, mul_assoc] using f.le_opNorm (i.insertNth x m)

Premises used: mul_assoc, Fin.prod_univ_succAbove, ContinuousMultilinearMap.le_opNorm, Fin.insertNth
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
x : Ei 0
m : (i : Fin n) → Ei i.succ
⊢ norm.{wG} (E := G) ((f : (a : (i : Fin n.succ) → Ei i) → G) (Fin.cons (α := Ei) x m) : G) ≤
    ‖f‖ * ‖x‖ * ∏ i : Fin n, ‖m i‖

Tactic:
simpa [prod_univ_succ, mul_assoc] using f.le_opNorm (cons x m)

Premises used: mul_assoc, ContinuousMultilinearMap.le_opNorm, Fin.cons, Fin.prod_univ_succ
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n) → Ei i.castSucc
x : Ei (last n)
⊢ norm.{wG} (E := G) ((f : (a : (i : Fin n.succ) → Ei i) → G) (snoc (α := Ei) m x) : G) ≤
    (‖f‖ * ∏ i : Fin n, ‖m i‖) * ‖x‖

Tactic:
simpa [prod_univ_castSucc, mul_assoc] using f.le_opNorm (snoc m x)

Premises used: mul_assoc, ContinuousMultilinearMap.le_opNorm, Fin.snoc, Fin.prod_univ_castSucc
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
f : Ei 0 →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G
m : (i : Fin n.succ) → Ei i
⊢ norm.{wG} (E := G)
      (((toMultilinearMapLinear (M₁ := fun (i : Fin n) ↦ Ei i.succ) ∘ₗ
                  (↑f : Ei 0 →ₗ[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G)).uncurryLeft
              (M := Ei) :
            (a : (i : Fin n.succ) → Ei i) → G)
          m :
        G) ≤
    ‖f‖ * ∏ i : Fin n.succ, ‖m i‖

Tactic:
ContinuousLinearMap.norm_map_tail_le f m

Premises used: ContinuousLinearMap.norm_map_tail_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
f : Ei 0 →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G
m : (i : Fin n.succ) → Ei i
⊢ norm.{wG} (E := G)
      (((toMultilinearMapLinear (M₁ := fun (i : Fin n) ↦ Ei i.succ) ∘ₗ
                  (↑f : Ei 0 →ₗ[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G)).uncurryLeft
              (M := Ei) :
            (a : (i : Fin n.succ) → Ei i) → G)
          m :
        G) ≤
    ‖f‖ * ∏ i : Fin n.succ, ‖m i‖

Tactic:
exact ContinuousLinearMap.norm_map_tail_le f m

Premises used: ContinuousLinearMap.norm_map_tail_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G
m : (i : Fin n.succ) → Ei i
⊢ Eq.{wG + 1} (α := G) ((f.uncurryLeft (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) m : G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) (m 0) :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        (tail (α := Ei) m) :
      G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
x : Ei 0
m : (i : Fin n) → Ei i.succ
⊢ Eq.{wG + 1} (α := G)
    ((((f.curryLeft (Ei := Ei) : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) x :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        m :
      G)
    ((f : (a : (i : Fin n.succ) → Ei i) → G) (Fin.cons (α := Ei) x m) : G)

Tactic:
rfl

Premises used: rfl