awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
α : Type u_1
inst_6 : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : Equiv.{u_1 + 1, v + 1} α (↑s : Type v)
inst_7 : DecidablePred fun (x : ι) ↦ x ∈ s
x : (i : ι) → E₁ i
⊢ ‖f.iteratedFDerivComponent (E₁ := E₁) (s := s) e‖ * ∏ i : { a : ι // a ∉ s }, norm (E := E₁ (↑i : ι)) (x (↑i : ι)) ≤
    ‖f‖ * ∏ _i : { a : ι // a ∉ s }, ‖x‖
have h₁ : ‖f.iteratedFDerivComponent (E₁ := E₁) (s := s) e‖ ≤ ‖f‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
α : Type u_1
inst_6 : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : Equiv.{u_1 + 1, v + 1} α (↑s : Type v)
inst_7 : DecidablePred fun (x : ι) ↦ x ∈ s
x : (i : ι) → E₁ i
h₁ : ‖f.iteratedFDerivComponent (E₁ := E₁) (s := s) e‖ ≤ ‖f‖
⊢ ‖f.iteratedFDerivComponent (E₁ := E₁) (s := s) e‖ * ∏ i : { a : ι // a ∉ s }, norm (E := E₁ (↑i : ι)) (x (↑i : ι)) ≤
    ‖f‖ * ∏ _i : { a : ι // a ∉ s }, ‖x‖
have h₂ : ∀ (i : { a : ι // a ∉ s }),
  Membership.mem (γ := Finset { a : ι // a ∉ s }) univ i → norm (E := E₁ (↑i : ι)) (x (↑i : ι)) ≤ ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
α : Type u_1
inst_6 : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : Equiv.{u_1 + 1, v + 1} α (↑s : Type v)
inst_7 : DecidablePred fun (x : ι) ↦ x ∈ s
x : (i : ι) → E₁ i
⊢ ‖f‖ * ∏ _i : { a : ι // a ∉ s }, ‖x‖ = ‖f‖ * ‖x‖ ^ Fintype.card.{v} { a : ι // a ∉ s }
have rw : ‖f‖ * ‖x‖ ^ card.{v} (α := { a : ι // a ∉ s }) univ = ‖f‖ * ‖x‖ ^ Fintype.card.{v} { a : ι // a ∉ s }
Tactic: rw [prod_const, card_univ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
Goal:
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_2 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
α : Type u_1
inst_6 : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : Equiv.{u_1 + 1, v + 1} α (↑s : Type v)
inst_7 : DecidablePred fun (x : ι) ↦ x ∈ s
x : (i : ι) → E₁ i
rw : ‖f‖ * ‖x‖ ^ card.{v} (α := { a : ι // a ∉ s }) univ = ‖f‖ * ‖x‖ ^ Fintype.card.{v} { a : ι // a ∉ s }
⊢ ‖f‖ * ∏ _i : { a : ι // a ∉ s }, ‖x‖ = ‖f‖ * ‖x‖ ^ Fintype.card.{v} { a : ι // a ∉ s }
have rw₁ : ‖f‖ * ‖x‖ ^ Fintype.card.{v} { a : ι // a ∉ s } = ‖f‖ * ‖x‖ ^ Fintype.card.{v} { a : ι // a ∉ s }
Tactic: rw [prod_const, card_univ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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
⊢ 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))
have 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)
Tactic: gcongr with e _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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
⊢ ‖f.iteratedFDeriv (E₁ := E₁) k x‖ ≤ (↑((Fintype.card ι).descFactorial k) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)
have 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))
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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))
⊢ ‖f.iteratedFDeriv (E₁ := E₁) k x‖ ≤ (↑((Fintype.card ι).descFactorial k) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)
have calc₁ : ∑ x_1 : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) =
  (↑((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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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
⊢ ‖f.iteratedFDeriv (E₁ := E₁) k x‖ ≤ (↑((Fintype.card ι).descFactorial k) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)
have 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))
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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))
⊢ ‖f.iteratedFDeriv (E₁ := E₁) k x‖ ≤ (↑((Fintype.card ι).descFactorial k) : ℝ) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)
have calc₁ : ∑ x_1 : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) =
  (↑((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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m_1 : G) = 0
have rw : norm.{wG} (E := G) 0 = 0
Tactic: rw [map_coord_zero f _ (norm_eq_zero.1 h), norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m_1 : G) = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [map_coord_zero f _ (norm_eq_zero.1 h), norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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‖ * ∏ j : Fin n.succ, ‖m j‖
have 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))
Tactic: rw [i.prod_univ_succAbove, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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.succ, ‖m i‖
have 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))
Tactic: rw [prod_univ_castSucc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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
⊢ f.uncurryLeft (Ei := Ei).curryLeft (Ei := Ei) = f
have h : ∀ (m : Ei 0) (x : (i : Fin n) → Ei i.succ),
  Eq.{wG + 1} (α := G)
    ((((f.uncurryLeft (Ei := Ei).curryLeft (Ei := Ei) :
                (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G)
              m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
Tactic: ext m x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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 : Ei 0
x : (i : Fin n) → Ei i.succ
⊢ Eq.{wG + 1} (α := G)
    ((((f.uncurryLeft (Ei := Ei).curryLeft (Ei := Ei) :
                (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G)
              m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
have h : Eq.{wG + 1} (α := G) ((f.uncurryLeft (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) (Fin.cons (α := Ei) m x) : G)
  ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
          ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
        (a : (i : Fin n) → Ei i.succ) → G)
      x :
    G)
Tactic: rw [ContinuousMultilinearMap.curryLeft_apply, ContinuousLinearMap.uncurryLeft_apply, tail_cons,
    cons_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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 : Ei 0
x : (i : Fin n) → Ei i.succ
h :
  Eq.{wG + 1} (α := G) ((f.uncurryLeft (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) (Fin.cons (α := Ei) m x) : G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
⊢ Eq.{wG + 1} (α := G)
    ((((f.uncurryLeft (Ei := Ei).curryLeft (Ei := Ei) :
                (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G)
              m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
have h₁ : Eq.{wG + 1} (α := G)
  ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) (Fin.cons (α := Ei) m x 0) :
          ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
        (a : (i : Fin n) → Ei i.succ) → G)
      (tail (α := Ei) (Fin.cons (α := Ei) m x)) :
    G)
  ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
          ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
        (a : (i : Fin n) → Ei i.succ) → G)
      x :
    G)
Tactic: rw [ContinuousMultilinearMap.curryLeft_apply, ContinuousLinearMap.uncurryLeft_apply, tail_cons,
    cons_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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 : Ei 0
x : (i : Fin n) → Ei i.succ
h :
  Eq.{wG + 1} (α := G) ((f.uncurryLeft (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) (Fin.cons (α := Ei) m x) : G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
h₁ :
  Eq.{wG + 1} (α := G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) (Fin.cons (α := Ei) m x 0) :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        (tail (α := Ei) (Fin.cons (α := Ei) m x)) :
      G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
⊢ Eq.{wG + 1} (α := G)
    ((((f.uncurryLeft (Ei := Ei).curryLeft (Ei := Ei) :
                (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G)
              m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
have h₂ : Eq.{wG + 1} (α := G)
  ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) (Fin.cons (α := Ei) m x 0) :
          ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
        (a : (i : Fin n) → Ei i.succ) → G)
      x :
    G)
  ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
          ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
        (a : (i : Fin n) → Ei i.succ) → G)
      x :
    G)
Tactic: rw [ContinuousMultilinearMap.curryLeft_apply, ContinuousLinearMap.uncurryLeft_apply, tail_cons,
    cons_zero]