awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
f : E [⋀^Fin (n + 1)]→L[𝕜] F
⊢ alternatizeUncurryFin f.curryLeft = (n + 1) • f
have H : ∀ (v : Fin (n + 1) → E),
  Eq.{u_3 + 1} (α := F) ((alternatizeUncurryFin f.curryLeft : (a : Fin (n + 1) → E) → F) v : F)
    (((n + 1) • f : (a : Fin (n + 1) → E) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
S : Type u_5
inst_5 : Monoid S
inst_6 : DistribMulAction S F
inst_7 : ContinuousConstSMul S F
inst_8 : SMulCommClass 𝕜 S F
c : S
f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
⊢ alternatizeUncurryFin (c • f) = c • alternatizeUncurryFin f
have H : ∀ (v : Fin (n + 1) → E),
  Eq.{u_3 + 1} (α := F) ((alternatizeUncurryFin (c • f) : (a : Fin (n + 1) → E) → F) v : F)
    ((c • alternatizeUncurryFin f : (a : Fin (n + 1) → E) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
⊢ Eq (α := E [⋀^Fin (HAdd.hAdd (α := ℕ) 0 1)]→L[𝕜] F)
    (alternatizeUncurryFin
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        (↑(↑(constOfIsEmptyLIE 𝕜 E F (Fin 0)) : F ≃L[𝕜] E [⋀^Fin 0]→L[𝕜] F) : F →L[𝕜] E [⋀^Fin 0]→L[𝕜] F) f))
    ((ofSubsingleton 𝕜 E F 0 : (a : E →L[𝕜] F) → E [⋀^Fin 1]→L[𝕜] F) f)
have H : ∀ (x : Fin (HAdd.hAdd (α := ℕ) 0 1) → E),
  Eq.{u_3 + 1} (α := F)
    ((alternatizeUncurryFin
            (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
              (↑(↑(constOfIsEmptyLIE 𝕜 E F (Fin 0)) : F ≃L[𝕜] E [⋀^Fin 0]→L[𝕜] F) : F →L[𝕜] E [⋀^Fin 0]→L[𝕜] F) f) :
          (a : Fin (0 + 1) → E) → F)
        x :
      F)
    ((((ofSubsingleton 𝕜 E F 0 : (a : E →L[𝕜] F) → E [⋀^Fin 1]→L[𝕜] F) f : E [⋀^Fin 1]→L[𝕜] F) :
          (a : Fin (0 + 1) → E) → F)
        x :
      F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
f : E →L[𝕜] E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
hf :
  ∀ (x y : E),
    Eq (α := E [⋀^Fin n]→L[𝕜] F)
      ((((f : (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) x : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) : (a : E) → E [⋀^Fin n]→L[𝕜] F) y :
        E [⋀^Fin n]→L[𝕜] F)
      ((((f : (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) y : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) : (a : E) → E [⋀^Fin n]→L[𝕜] F) x :
        E [⋀^Fin n]→L[𝕜] F)
⊢ alternatizeUncurryFin (alternatizeUncurryFinCLM 𝕜 E F ∘SL f) = 0
have H : ∀ (v : Fin (n + 1 + 1) → E),
  Eq.{u_3 + 1} (α := F)
    ((alternatizeUncurryFin (alternatizeUncurryFinCLM 𝕜 E F ∘SL f) : (a : Fin (n + 1 + 1) → E) → F) v : F)
    ((0 : (a : Fin (n + 1 + 1) → E) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (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 : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
g : E →L[𝕜] F
⊢ Eq (α := (E →L[𝕜] F) →L[𝕜] E [⋀^Fin (n + 1)]→L[𝕜] G) (f.fderivCompContinuousLinearMap g)
    (alternatizeUncurryFinCLM 𝕜 E G ∘SL ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft))
have h : ∀ (dg : E →L[𝕜] F) (v : Fin (n + 1) → E),
  Eq.{u_4 + 1} (α := G)
    ((((f.fderivCompContinuousLinearMap g : (a : E →L[𝕜] F) → E [⋀^Fin (n + 1)]→L[𝕜] G) dg : E [⋀^Fin (n + 1)]→L[𝕜] G) :
          (a : Fin (n + 1) → E) → G)
        v :
      G)
    ((((alternatizeUncurryFinCLM 𝕜 E G ∘SL
                  ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) :
                (a : E →L[𝕜] F) → E [⋀^Fin (n + 1)]→L[𝕜] G)
              dg :
            E [⋀^Fin (n + 1)]→L[𝕜] G) :
          (a : Fin (n + 1) → E) → G)
        v :
      G)
Tactic: ext dg v
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (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 : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
g : E →L[𝕜] F
dg : E →L[𝕜] F
v : Fin (n + 1) → E
i j : Fin (n + 1)
⊢ Eq.{u_3 + 1} (α := F)
    (((i.insertNth (α := fun (x : Fin (n + 1)) ↦ E →L[𝕜] F) dg (fun (x : Fin n) ↦ g) j : E →L[𝕜] F) : (a : E) → F)
        (v j) :
      F)
    (i.insertNth (α := fun (x : Fin (n + 1)) ↦ F) ((dg : (a : E) → F) (v i))
        ((⇑g : (a : E) → F) ∘ i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) j :
      F)
have x : Eq.{u_3 + 1} (α := F)
  (((i.insertNth (α := fun (x : Fin (n + 1)) ↦ E →L[𝕜] F) dg (fun (x : Fin n) ↦ g) i : E →L[𝕜] F) : (a : E) → F) (v i) :
    F)
  (i.insertNth (α := fun (x : Fin (n + 1)) ↦ F) ((dg : (a : E) → F) (v i))
      ((⇑g : (a : E) → F) ∘ i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) i :
    F)
Tactic: cases j using i.succAboveCases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (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 : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
g : E →L[𝕜] F
dg : E →L[𝕜] F
v : Fin (n + 1) → E
i j : Fin (n + 1)
x :
  Eq.{u_3 + 1} (α := F)
    (((i.insertNth (α := fun (x : Fin (n + 1)) ↦ E →L[𝕜] F) dg (fun (x : Fin n) ↦ g) i : E →L[𝕜] F) : (a : E) → F)
        (v i) :
      F)
    (i.insertNth (α := fun (x : Fin (n + 1)) ↦ F) ((dg : (a : E) → F) (v i))
        ((⇑g : (a : E) → F) ∘ i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) i :
      F)
⊢ Eq.{u_3 + 1} (α := F)
    (((i.insertNth (α := fun (x : Fin (n + 1)) ↦ E →L[𝕜] F) dg (fun (x : Fin n) ↦ g) j : E →L[𝕜] F) : (a : E) → F)
        (v j) :
      F)
    (i.insertNth (α := fun (x : Fin (n + 1)) ↦ F) ((dg : (a : E) → F) (v i))
        ((⇑g : (a : E) → F) ∘ i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) j :
      F)
have p : ∀ (j : Fin n),
  Eq.{u_3 + 1} (α := F)
    (((i.insertNth (α := fun (x : Fin (n + 1)) ↦ E →L[𝕜] F) dg (fun (x : Fin n) ↦ g) (i.succAbove j) : E →L[𝕜] F) :
          (a : E) → F)
        (v (i.succAbove j)) :
      F)
    (i.insertNth (α := fun (x : Fin (n + 1)) ↦ F) ((dg : (a : E) → F) (v i))
        ((⇑g : (a : E) → F) ∘ i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) (i.succAbove j) :
      F)
Tactic: cases j using i.succAboveCases
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (hypothesis)
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 : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
g : E →L[𝕜] F
dg : E →L[𝕜] F
v : Fin (n + 1) → E
⊢ Eq.{u_4 + 1} (α := G)
    ((((f.fderivCompContinuousLinearMap g : (a : E →L[𝕜] F) → E [⋀^Fin (n + 1)]→L[𝕜] G) dg : E [⋀^Fin (n + 1)]→L[𝕜] G) :
          (a : Fin (n + 1) → E) → G)
        v :
      G)
    ((((alternatizeUncurryFinCLM 𝕜 E G ∘SL
                  ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) :
                (a : E →L[𝕜] F) → E [⋀^Fin (n + 1)]→L[𝕜] G)
              dg :
            E [⋀^Fin (n + 1)]→L[𝕜] G) :
          (a : Fin (n + 1) → E) → G)
        v :
      G)
have this : ∀ (i j : Fin (n + 1)),
  Eq.{u_3 + 1} (α := F)
    (((i.insertNth (α := fun (x : Fin (n + 1)) ↦ E →L[𝕜] F) dg (fun (x : Fin n) ↦ g) j : E →L[𝕜] F) : (a : E) → F)
        (v j) :
      F)
    (i.insertNth (α := fun (x : Fin (n + 1)) ↦ F) ((dg : (a : E) → F) (v i))
        ((⇑g : (a : E) → F) ∘ i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) j :
      F)
Tactic: have (i j : Fin (n + 1)) :
      i.insertNth (α := fun _ ↦ E →L[𝕜] F) dg (fun _ ↦ g) j (v j) =
        i.insertNth (α := fun _ ↦ F) (dg (v i)) (g ∘ i.removeNth v) j := by
    cases j using i.succAboveCases <;> simp [Fin.removeNth]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (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
g : E →L[𝕜] F
h : E →L[𝕜] E →L[𝕜] F
hsymm :
  ∀ (x y : E),
    Eq.{u_3 + 1} (α := F) ((((h : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
      ((((h : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
n : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
⊢ Eq (α := E [⋀^Fin (n + 1 + 1)]→L[𝕜] G)
    (alternatizeUncurryFin (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (f.fderivCompContinuousLinearMap g) h)) 0
have succ : ∀ (x y : E),
  Eq (α := E [⋀^Fin n]→L[𝕜] G)
    ((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
              x :
            E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
          (a : E) → E [⋀^Fin n]→L[𝕜] G)
        y :
      E [⋀^Fin n]→L[𝕜] G)
    ((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
              y :
            E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
          (a : E) → E [⋀^Fin n]→L[𝕜] G)
        x :
      E [⋀^Fin n]→L[𝕜] G)
Tactic: rw [fderivCompContinuousLinearMap_eq_alternatizeUncurryFin,
      ContinuousLinearMap.comp_assoc,
      alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (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
g : E →L[𝕜] F
h : E →L[𝕜] E →L[𝕜] F
hsymm :
  ∀ (x y : E),
    Eq.{u_3 + 1} (α := F) ((((h : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
      ((((h : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
n : ℕ
f : F [⋀^Fin (n + 1)]→L[𝕜] G
x y : E
⊢ Eq (α := E [⋀^Fin n]→L[𝕜] G)
    ((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
              x :
            E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
          (a : E) → E [⋀^Fin n]→L[𝕜] G)
        y :
      E [⋀^Fin n]→L[𝕜] G)
    ((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
              y :
            E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
          (a : E) → E [⋀^Fin n]→L[𝕜] G)
        x :
      E [⋀^Fin n]→L[𝕜] G)
have succ : ∀ (v : Fin n → E),
  Eq.{u_4 + 1} (α := G)
    ((((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                      (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
                    x :
                  E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
                (a : E) → E [⋀^Fin n]→L[𝕜] G)
              y :
            E [⋀^Fin n]→L[𝕜] G) :
          (a : Fin n → E) → G)
        v :
      G)
    ((((((ContinuousLinearMap.postcomp E (compContinuousLinearMapCLM g ∘SL f.curryLeft) ∘SL h :
                      (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] G)
                    y :
                  E →L[𝕜] E [⋀^Fin n]→L[𝕜] G) :
                (a : E) → E [⋀^Fin n]→L[𝕜] G)
              x :
            E [⋀^Fin n]→L[𝕜] G) :
          (a : Fin n → E) → G)
        v :
      G)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (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 : ℕ
f : F [⋀^Fin n]→L[𝕜] G
g : E →L[𝕜] F
h : E →L[𝕜] E →L[𝕜] F
hsymm :
  ∀ (x y : E),
    Eq.{u_3 + 1} (α := F) ((((h : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
      ((((h : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
⊢ Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (alternatizeUncurryFin (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (f.fderivCompContinuousLinearMap g) h)) 0
have zero : ∀ (f : F [⋀^Fin 0]→L[𝕜] G),
  Eq (α := E [⋀^Fin (HAdd.hAdd (α := ℕ) 0 1)]→L[𝕜] G)
    (alternatizeUncurryFin (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (f.fderivCompContinuousLinearMap g) h)) 0
Tactic: cases n with
  | zero =>
    simp [fderivCompContinuousLinearMap_of_isEmpty, ← alternatizeUncurryFinCLM_apply]
  | succ n =>
    rw [fderivCompContinuousLinearMap_eq_alternatizeUncurryFin,
      ContinuousLinearMap.comp_assoc,
      alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric]
    intro x y
    ext v
    simp [hsymm]
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin (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 : ℕ
f : F [⋀^Fin n]→L[𝕜] G
g : E →L[𝕜] F
h : E →L[𝕜] E →L[𝕜] F
hsymm :
  ∀ (x y : E),
    Eq.{u_3 + 1} (α := F) ((((h : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
      ((((h : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
zero :
  ∀ (f : F [⋀^Fin 0]→L[𝕜] G),
    Eq (α := E [⋀^Fin (HAdd.hAdd (α := ℕ) 0 1)]→L[𝕜] G)
      (alternatizeUncurryFin (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (f.fderivCompContinuousLinearMap g) h)) 0
⊢ Eq (α := E [⋀^Fin (n + 1)]→L[𝕜] G)
    (alternatizeUncurryFin (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (f.fderivCompContinuousLinearMap g) h)) 0
have succ : ∀ (n : ℕ) (f : F [⋀^Fin (n + 1)]→L[𝕜] G),
  Eq (α := E [⋀^Fin (n + 1 + 1)]→L[𝕜] G)
    (alternatizeUncurryFin (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (f.fderivCompContinuousLinearMap g) h)) 0
Tactic: cases n with
  | zero =>
    simp [fderivCompContinuousLinearMap_of_isEmpty, ← alternatizeUncurryFinCLM_apply]
  | succ n =>
    rw [fderivCompContinuousLinearMap_eq_alternatizeUncurryFin,
      ContinuousLinearMap.comp_assoc,
      alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric]
    intro x y
    ext v
    simp [hsymm]
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Action (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
c : (↑(sphere 0 1) : Type u_1)
x : (↑(sphere 0 r) : Type u_3)
⊢ ‖(↑c : 𝕜) • (↑x : E)‖ = r
have rw : ‖(↑c : 𝕜)‖ * ‖(↑x : E)‖ = r
Tactic: rw [norm_smul, mem_sphere_zero_iff_norm.1 c.coe_prop, mem_sphere_zero_iff_norm.1 x.coe_prop,
          one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Action (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
c : (↑(sphere 0 1) : Type u_1)
x : (↑(sphere 0 r) : Type u_3)
rw : ‖(↑c : 𝕜)‖ * ‖(↑x : E)‖ = r
⊢ ‖(↑c : 𝕜) • (↑x : E)‖ = r
have rw₁ : 1 * ‖(↑x : E)‖ = r
Tactic: rw [norm_smul, mem_sphere_zero_iff_norm.1 c.coe_prop, mem_sphere_zero_iff_norm.1 x.coe_prop,
          one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Action (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
c : (↑(sphere 0 1) : Type u_1)
x : (↑(sphere 0 r) : Type u_3)
rw : ‖(↑c : 𝕜)‖ * ‖(↑x : E)‖ = r
rw₁ : 1 * ‖(↑x : E)‖ = r
⊢ ‖(↑c : 𝕜) • (↑x : E)‖ = r
have rw₂ : 1 * r = r
Tactic: rw [norm_smul, mem_sphere_zero_iff_norm.1 c.coe_prop, mem_sphere_zero_iff_norm.1 x.coe_prop,
          one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Action (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedField 𝕜'
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜' E
r : ℝ
c : (↑(sphere 0 1) : Type u_1)
x : (↑(sphere 0 r) : Type u_3)
rw : ‖(↑c : 𝕜)‖ * ‖(↑x : E)‖ = r
rw₁ : 1 * ‖(↑x : E)‖ = r
rw₂ : 1 * r = r
⊢ ‖(↑c : 𝕜) • (↑x : E)‖ = r
have rw₃ : r = r
Tactic: rw [norm_smul, mem_sphere_zero_iff_norm.1 c.coe_prop, mem_sphere_zero_iff_norm.1 x.coe_prop,
          one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Action (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : (↑(sphere 0 r) : Type u_3)
this : IsAddTorsionFree E
h : x = -x
| (↑x : E)
have rw : (↑(-x) : E)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Action (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : (↑(sphere 0 r) : Type u_3)
this : IsAddTorsionFree E
h : x = -x
⊢ (↑x : E) = -(↑x : E)
have conv_lhs : (↑(-x) : E) = -(↑x : E)
Tactic: conv_lhs => rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
⊢ Membership.mem (γ := Set E) (ball 0 1) ((√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x)
have this : 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: have : 0 < 1 + ‖x‖ ^ 2 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
this : 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2
⊢ Membership.mem (γ := Set E) (ball 0 1) ((√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x)
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [mem_ball_zero_iff, norm_smul, Real.norm_eq_abs, abs_inv, ← _root_.div_eq_inv_mul,
      div_lt_one (abs_pos.mpr <| Real.sqrt_ne_zero'.mpr this), ← abs_norm x, ← sq_lt_sq,
      abs_norm, Real.sq_sqrt this.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
⊢ (√(1 - HPow.hPow (β := ℕ) ‖(√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x‖ 2))⁻¹ • (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x =
    x
have match_scalars : (√(1 - HPow.hPow (β := ℕ) ‖(√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x‖ 2))⁻¹ * ((√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ * 1) =
  1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
⊢ (√(1 - HPow.hPow (β := ℕ) ‖(√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x‖ 2))⁻¹ *
      ((√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ * 1) =
    1
have simp : (√(1 - HPow.hPow (β := ℕ) (|√(1 + HPow.hPow (β := ℕ) ‖x‖ 2)|⁻¹ * ‖x‖) 2))⁻¹ * (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ = 1
Tactic: simp [norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
h : Membership.mem (γ := Set E) univ x
⊢ (√(1 - HPow.hPow (β := ℕ) (|√(1 + HPow.hPow (β := ℕ) ‖x‖ 2)|⁻¹ * ‖x‖) 2))⁻¹ * (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ = 1
have field_simp : 1 /
    √((HPow.hPow (β := ℕ) |√(1 + HPow.hPow (β := ℕ) ‖x‖ 2)| 2 - HPow.hPow (β := ℕ) ‖x‖ 2) /
        HPow.hPow (β := ℕ) |√(1 + HPow.hPow (β := ℕ) ‖x‖ 2)| 2) =
  √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
⊢ 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
have nlinarith : 1 - HPow.hPow (β := ℕ) ‖y‖ 2 ≤ 0 → 1 - HPow.hPow (β := ℕ) ‖y‖ 2 - 0 + (‖y‖ - 1) + (0 - (0 - ‖y‖) * (‖y‖ - 1)) = 0
Tactic: nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
⊢ (√(1 + HPow.hPow (β := ℕ) ‖(√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ • y‖ 2))⁻¹ • (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ • y =
    y
have this : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: have : 0 < 1 - ‖y‖ ^ 2 := by nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
this : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
⊢ (√(1 + HPow.hPow (β := ℕ) ‖(√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ • y‖ 2))⁻¹ • (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ • y =
    y
have match_scalars : (√(1 + HPow.hPow (β := ℕ) ‖(√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ • y‖ 2))⁻¹ * ((√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ * 1) =
  1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
this : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
⊢ (√(1 + HPow.hPow (β := ℕ) ‖(√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ • y‖ 2))⁻¹ *
      ((√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ * 1) =
    1
have simp : (√(1 + HPow.hPow (β := ℕ) (|√(1 - HPow.hPow (β := ℕ) ‖y‖ 2)|⁻¹ * ‖y‖) 2))⁻¹ * (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ = 1
Tactic: simp [norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
y : E
hy : Membership.mem (γ := Set E) (ball 0 1) y
this : 0 < 1 - HPow.hPow (β := ℕ) ‖y‖ 2
⊢ (√(1 + HPow.hPow (β := ℕ) (|√(1 - HPow.hPow (β := ℕ) ‖y‖ 2)|⁻¹ * ‖y‖) 2))⁻¹ * (√(1 - HPow.hPow (β := ℕ) ‖y‖ 2))⁻¹ = 1
have field_simp : 1 =
  √((HPow.hPow (β := ℕ) |√(1 - HPow.hPow (β := ℕ) ‖y‖ 2)| 2 + HPow.hPow (β := ℕ) ‖y‖ 2) /
        HPow.hPow (β := ℕ) |√(1 - HPow.hPow (β := ℕ) ‖y‖ 2)| 2) *
    √(1 - HPow.hPow (β := ℕ) ‖y‖ 2)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
this : Continuous (Y := ℝ) fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹
⊢ ContinuousOn (Y := E) (fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x) univ
have funProp : ∀ (x : E), Membership.mem (γ := Set E) univ x → √(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Homeomorph (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
this : Continuous (Y := ℝ) fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹
funProp : ∀ (x : E), Membership.mem (γ := Set E) univ x → √(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ≠ 0
⊢ ContinuousOn (Y := E) (fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹ • x) univ
have funProp₁ : ∀ (x : ℝ), x ≠ 0
Tactic: fun_prop