awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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) 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: 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
ι : 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 : ContinuousMultilinearMap 𝕜 Ei G
inst_11 : DecidableEq (Fin n)
m : (i : Fin n) → Ei i.castSucc
i : Fin n
x y : Ei i.castSucc
⊢ LinearMap.mkContinuous
      ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
        (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (x + y)))
      (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (x + y) i_1‖) ⋯ =
    HAdd.hAdd (α := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
      (LinearMap.mkContinuous
        ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
          (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x))
        (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x i_1‖) ⋯)
      (LinearMap.mkContinuous
        ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
          (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i y))
        (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i y i_1‖) ⋯)
have h : ∀ (x_1 : Ei (last n)),
  Eq.{wG + 1} (α := G)
    ((LinearMap.mkContinuous
            ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
              (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (x + y)))
            (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (x + y) i_1‖) sorry :
          (a : Ei (last n)) → G)
        x_1 :
      G)
    ((HAdd.hAdd (α := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
            (LinearMap.mkContinuous
              ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                  (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
                (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x))
              (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x i_1‖) sorry)
            (LinearMap.mkContinuous
              ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                  (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
                (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i y))
              (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i y i_1‖) sorry) :
          (a : Ei (last n)) → G)
        x_1 :
      G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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 : ContinuousMultilinearMap 𝕜 Ei G
inst_11 : DecidableEq (Fin n)
m : (i : Fin n) → Ei i.castSucc
i : Fin n
c : 𝕜
x : Ei i.castSucc
⊢ LinearMap.mkContinuous
      ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
        (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (c • x)))
      (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (c • x) i_1‖) ⋯ =
    HSMul.hSMul (β := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) c
      (LinearMap.mkContinuous
        ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
          (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x))
        (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x i_1‖) ⋯)
have h : ∀ (x_1 : Ei (last n)),
  Eq.{wG + 1} (α := G)
    ((LinearMap.mkContinuous
            ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
              (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (c • x)))
            (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (c • x) i_1‖) sorry :
          (a : Ei (last n)) → G)
        x_1 :
      G)
    ((HSMul.hSMul (β := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) c
            (LinearMap.mkContinuous
              ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                  (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
                (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x))
              (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x i_1‖) sorry) :
          (a : Ei (last n)) → G)
        x_1 :
      G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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 : ContinuousMultilinearMap 𝕜 Ei G
f' : MultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
  (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :=
  MultilinearMap.mk (M₁ := fun (i : Fin n) ↦ Ei i.castSucc)
    (fun (m : (i : Fin n) → Ei i.castSucc) ↦
      LinearMap.mkContinuous
        ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
          m)
        (‖f‖ * ∏ i : Fin n, ‖m i‖) ⋯)
    ⋯ ⋯
m : (i : Fin n) → Ei i.castSucc
⊢ norm (E := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
      ((f' : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
        ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) ≤
    ‖f‖ * ∏ i : Fin n, ‖m i‖
have simp : norm (E := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
    (LinearMap.mkContinuous
      ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G) m)
      (‖f‖ * ∏ i : Fin n, ‖m i‖) sorry) ≤
  ‖f‖ * ∏ i : Fin n, ‖m i‖
Tactic: simp only [f', MultilinearMap.coe_mk]
-- 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)
⊢ f.uncurryRight (Ei := Ei).curryRight (Ei := Ei) = f
have H : ∀ (m : (i : Fin n) → Ei i.castSucc) (x : Ei (last n)),
  Eq.{wG + 1} (α := G)
    ((((f.uncurryRight (Ei := Ei).curryRight (Ei := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → 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 :
  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
    (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
m : (i : Fin n) → Ei i.castSucc
x : Ei (last n)
⊢ Eq.{wG + 1} (α := G)
    ((((f.uncurryRight (Ei := Ei).curryRight (Ei := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
have H : Eq.{wG + 1} (α := G) ((f.uncurryRight (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) (snoc (α := Ei) m x) : G)
  ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
          ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
        (a : Ei (last n)) → G)
      x :
    G)
Tactic: rw [ContinuousMultilinearMap.curryRight_apply, ContinuousMultilinearMap.uncurryRight_apply,
    snoc_last, init_snoc]
-- 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) → Ei i.castSucc
x : Ei (last n)
H :
  Eq.{wG + 1} (α := G) ((f.uncurryRight (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) (snoc (α := Ei) m x) : G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
⊢ Eq.{wG + 1} (α := G)
    ((((f.uncurryRight (Ei := Ei).curryRight (Ei := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
have H₁ : Eq.{wG + 1} (α := G)
  ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) (init (α := Ei) (snoc (α := Ei) m x)) :
          ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
        (a : Ei (last n)) → G)
      (snoc (α := Ei) m x (last n)) :
    G)
  ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
          ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
        (a : Ei (last n)) → G)
      x :
    G)
Tactic: rw [ContinuousMultilinearMap.curryRight_apply, ContinuousMultilinearMap.uncurryRight_apply,
    snoc_last, init_snoc]
-- 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) → Ei i.castSucc
x : Ei (last n)
H :
  Eq.{wG + 1} (α := G) ((f.uncurryRight (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) (snoc (α := Ei) m x) : G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
H₁ :
  Eq.{wG + 1} (α := G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) (init (α := Ei) (snoc (α := Ei) m x)) :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        (snoc (α := Ei) m x (last n)) :
      G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
⊢ Eq.{wG + 1} (α := G)
    ((((f.uncurryRight (Ei := Ei).curryRight (Ei := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
have H₂ : Eq.{wG + 1} (α := G)
  ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) (init (α := Ei) (snoc (α := Ei) m x)) :
          ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
        (a : Ei (last n)) → G)
      x :
    G)
  ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
          ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
        (a : Ei (last n)) → G)
      x :
    G)
Tactic: rw [ContinuousMultilinearMap.curryRight_apply, ContinuousMultilinearMap.uncurryRight_apply,
    snoc_last, init_snoc]
-- 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) → Ei i.castSucc
x : Ei (last n)
H :
  Eq.{wG + 1} (α := G) ((f.uncurryRight (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) (snoc (α := Ei) m x) : G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
H₁ :
  Eq.{wG + 1} (α := G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) (init (α := Ei) (snoc (α := Ei) m x)) :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        (snoc (α := Ei) m x (last n)) :
      G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
H₂ :
  Eq.{wG + 1} (α := G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) (init (α := Ei) (snoc (α := Ei) m x)) :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
⊢ Eq.{wG + 1} (α := G)
    ((((f.uncurryRight (Ei := Ei).curryRight (Ei := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
have H₃ : Eq.{wG + 1} (α := G)
  ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
          ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
        (a : Ei (last n)) → G)
      x :
    G)
  ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
          ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
        (a : Ei (last n)) → G)
      x :
    G)
Tactic: rw [ContinuousMultilinearMap.curryRight_apply, ContinuousMultilinearMap.uncurryRight_apply,
    snoc_last, init_snoc]
-- 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 𝕜 Ei G
⊢ f.curryRight (Ei := Ei).uncurryRight (Ei := Ei) = f
have H : ∀ (m : (i : Fin n.succ) → Ei i),
  Eq.{wG + 1} (α := G) ((f.curryRight (Ei := Ei).uncurryRight (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) m : G)
    ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G)
Tactic: ext m
-- 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 𝕜 Ei G
m : (i : Fin n.succ) → Ei i
⊢ Eq.{wG + 1} (α := G) ((f.curryRight (Ei := Ei).uncurryRight (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) m : G)
    ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G)
have H : Eq.{wG + 1} (α := G)
  ((((f.curryRight (Ei := Ei) : (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 : (a : (i : Fin n.succ) → Ei i) → G) m : G)
Tactic: rw [uncurryRight_apply, curryRight_apply, snoc_init_self]
-- 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 𝕜 Ei G
m : (i : Fin n.succ) → Ei i
H :
  Eq.{wG + 1} (α := G)
    ((((f.curryRight (Ei := Ei) : (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 : (a : (i : Fin n.succ) → Ei i) → G) m : G)
⊢ Eq.{wG + 1} (α := G) ((f.curryRight (Ei := Ei).uncurryRight (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) m : G)
    ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G)
have H₁ : Eq.{wG + 1} (α := G) ((f : (a : (i : Fin n.succ) → Ei i) → G) (snoc (α := Ei) (init (α := Ei) m) (m (last n))) : G)
  ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G)
Tactic: rw [uncurryRight_apply, curryRight_apply, snoc_init_self]
-- 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 𝕜 Ei G
m : (i : Fin n.succ) → Ei i
H :
  Eq.{wG + 1} (α := G)
    ((((f.curryRight (Ei := Ei) : (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 : (a : (i : Fin n.succ) → Ei i) → G) m : G)
H₁ :
  Eq.{wG + 1} (α := G) ((f : (a : (i : Fin n.succ) → Ei i) → G) (snoc (α := Ei) (init (α := Ei) m) (m (last n))) : G)
    ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G)
⊢ Eq.{wG + 1} (α := G) ((f.curryRight (Ei := Ei).uncurryRight (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) m : G)
    ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G)
have H₂ : Eq.{wG + 1} (α := G) ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G) ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G)
Tactic: rw [uncurryRight_apply, curryRight_apply, snoc_init_self]