-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Curry (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ
g : F [⋀^Fin (n + 1)]→L[𝕜] G
f : E →L[𝕜] F
x : E
v : Fin n → E
i : Fin (n + 1)
zero :
  Eq.{u_3 + 1} (α := F)
    (((fun (i : Fin (n + 1)) ↦
              ((↑((fun (x : Fin (n + 1)) ↦ f) i) :
                  LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin (n + 1)) ↦ E) i)
                    ((fun (x : Fin (n + 1)) ↦ F) i)) :
                LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin (n + 1)) ↦ E) i)
                  ((fun (x : Fin (n + 1)) ↦ F) i)))
            0 :
          (a : (fun (x : Fin (n + 1)) ↦ E) 0) → (fun (x : Fin (n + 1)) ↦ F) 0)
        (Fin.cons (α := fun (x : Fin n.succ) ↦ E) x v 0 : E) :
      (fun (x : Fin (n + 1)) ↦ F) 0)
    (Fin.cons (α := fun (x : Fin n.succ) ↦ F) ((f : (a : E) → F) x)
        (fun (i : Fin n) ↦
          ((fun (i : Fin n) ↦
                  ((↑((fun (x : Fin n) ↦ f) i) :
                      LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin n) ↦ E) i)
                        ((fun (x : Fin n) ↦ F) i)) :
                    LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin n) ↦ E) i) ((fun (x : Fin n) ↦ F) i)))
                i :
              (a : (fun (x : Fin n) ↦ E) i) → (fun (x : Fin n) ↦ F) i)
            (v i))
        0 :
      F)
⊢ Eq.{u_3 + 1} (α := F)
    (((fun (i : Fin (n + 1)) ↦
              ((↑((fun (x : Fin (n + 1)) ↦ f) i) :
                  LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin (n + 1)) ↦ E) i)
                    ((fun (x : Fin (n + 1)) ↦ F) i)) :
                LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin (n + 1)) ↦ E) i)
                  ((fun (x : Fin (n + 1)) ↦ F) i)))
            i :
          (a : (fun (x : Fin (n + 1)) ↦ E) i) → (fun (x : Fin (n + 1)) ↦ F) i)
        (Fin.cons (α := fun (x : Fin n.succ) ↦ E) x v i : E) :
      (fun (x : Fin (n + 1)) ↦ F) i)
    (Fin.cons (α := fun (x : Fin n.succ) ↦ F) ((f : (a : E) → F) x)
        (fun (i : Fin n) ↦
          ((fun (i : Fin n) ↦
                  ((↑((fun (x : Fin n) ↦ f) i) :
                      LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin n) ↦ E) i)
                        ((fun (x : Fin n) ↦ F) i)) :
                    LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin n) ↦ E) i) ((fun (x : Fin n) ↦ F) i)))
                i :
              (a : (fun (x : Fin n) ↦ E) i) → (fun (x : Fin n) ↦ F) i)
            (v i))
        i :
      F)
have succ : ∀ (i : Fin n),
  Eq.{u_3 + 1} (α := F)
    (((fun (i : Fin (n + 1)) ↦
              ((↑((fun (x : Fin (n + 1)) ↦ f) i) :
                  LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin (n + 1)) ↦ E) i)
                    ((fun (x : Fin (n + 1)) ↦ F) i)) :
                LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin (n + 1)) ↦ E) i)
                  ((fun (x : Fin (n + 1)) ↦ F) i)))
            i.succ :
          (a : (fun (x : Fin (n + 1)) ↦ E) i.succ) → (fun (x : Fin (n + 1)) ↦ F) i.succ)
        (Fin.cons (α := fun (x : Fin n.succ) ↦ E) x v i.succ : E) :
      (fun (x : Fin (n + 1)) ↦ F) i.succ)
    (Fin.cons (α := fun (x : Fin n.succ) ↦ F) ((f : (a : E) → F) x)
        (fun (i : Fin n) ↦
          ((fun (i : Fin n) ↦
                  ((↑((fun (x : Fin n) ↦ f) i) :
                      LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin n) ↦ E) i)
                        ((fun (x : Fin n) ↦ F) i)) :
                    LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) ((fun (x : Fin n) ↦ E) i) ((fun (x : Fin n) ↦ F) i)))
                i :
              (a : (fun (x : Fin n) ↦ E) i) → (fun (x : Fin n) ↦ F) i)
            (v i))
        i.succ :
      F)
Tactic: cases i using Fin.cases
Cleared hypotheses: i