awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Curry
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
⊢ ‖f.curryLeft‖ = ‖f‖

Tactic:
f.toContinuousMultilinearMap.curryLeft_norm

Premises used: ContinuousAlternatingMap.curryLeft, setOf, ContinuousMultilinearMap.curryLeft_norm, ContinuousLinearMap.opNorm, ContinuousMultilinearMap.curryLeft, MultilinearMap.mkContinuous, ContinuousAlternatingMap.toContinuousMultilinearMap, AlternatingMap.mkContinuousLinear, AlternatingMap.mkContinuous, MultilinearMap.mkContinuousLinear, LinearMap.mkContinuous
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Curry
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
x : E
v : Fin n → E
⊢ Eq.{u_3 + 1} (α := F)
    ((((f.curryLeft : (a : E) → E [⋀^Fin n]→L[𝕜] F) x : E [⋀^Fin n]→L[𝕜] F) : (a : Fin n → E) → F) v : F)
    ((f : (a : Fin (n + 1) → E) → F) (Matrix.vecCons x v) : F)

Tactic:
rfl

Premises used: Matrix.vecCons, rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Curry
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 : ℕ
⊢ Eq (α := E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) (curryLeft 0) 0

Tactic:
rfl

Premises used: ContinuousAlternatingMap.curryLeft, MultilinearMap.mk', AlternatingMap.mkContinuousLinear, AlternatingMap.mkContinuous, LinearMap.mkContinuous, rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Curry
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 g : E [⋀^Fin (n + 1)]→L[𝕜] F
⊢ (f + g).curryLeft = f.curryLeft + g.curryLeft

Tactic:
rfl

Premises used: ContinuousAlternatingMap.curryLeft, MultilinearMap.mk', AlternatingMap.mkContinuousLinear, AlternatingMap.mkContinuous, LinearMap.mkContinuous, rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Curry
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 : ℕ
r : 𝕜
f : E [⋀^Fin (n + 1)]→L[𝕜] F
⊢ (r • f).curryLeft = r • f.curryLeft

Tactic:
rfl

Premises used: ContinuousAlternatingMap.curryLeft, MultilinearMap.mk', AlternatingMap.mkContinuousLinear, AlternatingMap.mkContinuous, LinearMap.mkContinuous, rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Curry
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 + 2)]→L[𝕜] F
x : E
x_1 : Fin n → E
⊢ Eq.{u_2 + 1} (α := E)
    (Fin.cons (α := fun (x : Fin (n + 1).succ) ↦ E) x (Fin.cons (α := fun (x : Fin n.succ) ↦ E) x x_1) 0 : E)
    (Fin.cons (α := fun (x : Fin (n + 1).succ) ↦ E) x (Fin.cons (α := fun (x : Fin n.succ) ↦ E) x x_1) 1 : E)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Curry
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 →L[𝕜] G
f : E [⋀^Fin (n + 1)]→L[𝕜] F
x : E
⊢ Eq (α := E [⋀^Fin n]→L[𝕜] G)
    (((g.compContinuousAlternatingMap f).curryLeft : (a : E) → E [⋀^Fin n]→L[𝕜] G) x : E [⋀^Fin n]→L[𝕜] G)
    (g.compContinuousAlternatingMap ((f.curryLeft : (a : E) → E [⋀^Fin n]→L[𝕜] F) x) : E [⋀^Fin n]→L[𝕜] G)

Tactic:
rfl

Premises used: ContinuousLinearMap.compContinuousMultilinearMap, ContinuousLinearMap.compContinuousAlternatingMap, MultilinearMap.mk', AlternatingMap.mkContinuous, LinearMap.compMultilinearMap, rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Curry
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
⊢ 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)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Curry
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
⊢ 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:
simp
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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
p : Fin (n + 1)
x : E
v : Fin n → E
⊢ (f : (a : Fin (n + 1) → E) → F) (p.insertNth (α := fun (a : Fin (n + 1)) ↦ E) x v) =
    HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑p : ℕ)) ((f : (a : Fin (n + 1) → E) → F) (Matrix.vecCons x v) : F)

Tactic:
f.toAlternatingMap.map_insertNth p x v

Premises used: ContinuousAlternatingMap.toAlternatingMap, AlternatingMap.map_insertNth
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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
p : Fin (n + 1)
x : E
v : Fin n → E
⊢ HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑p : ℕ))
      ((f : (a : Fin (n + 1) → E) → F) (p.insertNth (α := fun (a : Fin (n + 1)) ↦ E) x v) : F) =
    (f : (a : Fin (n + 1) → E) → F) (Matrix.vecCons x v)

Tactic:
f.toAlternatingMap.neg_one_pow_smul_map_insertNth p x v

Premises used: ContinuousAlternatingMap.toAlternatingMap, AlternatingMap.neg_one_pow_smul_map_insertNth
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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]→L[𝕜] F
v : Fin (n + 1) → E
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
        ((f : (a : Fin n → E) → F) (i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) : F) +
      HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
        ((f : (a : Fin n → E) → F) (j.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) : F) =
    0

Tactic:
f.toAlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq hvij hij

Premises used: ContinuousAlternatingMap.toAlternatingMap, AlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 [⋀^Fin n]→L[𝕜] F
v : Fin (n + 1) → E
⊢ Eq.{u_3 + 1} (α := F)
    ((((aux : (a : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) → E [⋀^Fin (n + 1)]→ₗ[𝕜] F) f : E [⋀^Fin (n + 1)]→ₗ[𝕜] F) :
          (a : Fin (n + 1) → E) → F)
        v :
      F)
    (∑ i : Fin (n + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((((f : (a : E) → E [⋀^Fin n]→L[𝕜] F) (v i) : E [⋀^Fin n]→L[𝕜] F) : (a : Fin n → E) → F)
              (i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) :
            F) :
      F)

Tactic:
simp [aux, AlternatingMap.alternatizeUncurryFin_apply]

Premises used: _private.0.ContinuousAlternatingMap.alternatizeUncurryFinCLM.aux, AlternatingMap.alternatizeUncurryFin_apply
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 [⋀^Fin n]→L[𝕜] F
⊢ (alternatizeUncurryFinCLM 𝕜 E F : (a : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) → E [⋀^Fin (n + 1)]→L[𝕜] F) f =
    alternatizeUncurryFin f

Tactic:
rfl

Premises used: ContinuousAlternatingMap.alternatizeUncurryFin, rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 [⋀^Fin n]→L[𝕜] F
⊢ ‖alternatizeUncurryFin f‖ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖f‖

Tactic:
(alternatizeUncurryFinCLM 𝕜 E F).le_of_opNorm_le norm_alternatizeUncurryFinCLM_le f

Premises used: ContinuousLinearMap.le_of_opNorm_le
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 [⋀^Fin n]→L[𝕜] F
v : Fin (n + 1) → E
rw :
  Eq.{u_3 + 1} (α := F)
    ((((sorry : (a : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) → E [⋀^Fin (n + 1)]→L[𝕜] F) f : E [⋀^Fin (n + 1)]→L[𝕜] F) :
          (a : Fin (n + 1) → E) → F)
        v :
      F)
    (∑ i : Fin (n + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((((f : (a : E) → E [⋀^Fin n]→L[𝕜] F) (v i) : E [⋀^Fin n]→L[𝕜] F) : (a : Fin n → E) → F)
              (i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) :
            F) :
      F)
⊢ Eq.{u_3 + 1} (α := F) ((alternatizeUncurryFin f : (a : Fin (n + 1) → E) → F) v : F)
    (∑ i : Fin (n + 1),
        HSMul.hSMul (β := F) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((((f : (a : E) → E [⋀^Fin n]→L[𝕜] F) (v i) : E [⋀^Fin n]→L[𝕜] F) : (a : Fin n → E) → F)
              (i.removeNth (α := fun (i : Fin (n + 1)) ↦ E) v) :
            F) :
      F)

Tactic:
rw [alternatizeUncurryFin, alternatizeUncurryFinCLM]

Premises used: ContinuousAlternatingMap.alternatizeUncurryFinCLM, ContinuousAlternatingMap.alternatizeUncurryFin
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 [⋀^Fin n]→L[𝕜] F
H :
  ∀ (x : Fin (n + 1) → E),
    Eq.{u_3 + 1} (α := F) (((alternatizeUncurryFin f).toAlternatingMap : (a : Fin (n + 1) → E) → F) x : F)
      ((AlternatingMap.alternatizeUncurryFin (toAlternatingMapLinear ∘ₗ (↑f : E →ₗ[𝕜] E [⋀^Fin n]→L[𝕜] F)) :
            (a : Fin (n + 1) → E) → F)
          x :
        F)
⊢ (alternatizeUncurryFin f).toAlternatingMap =
    AlternatingMap.alternatizeUncurryFin (toAlternatingMapLinear ∘ₗ (↑f : E →ₗ[𝕜] E [⋀^Fin n]→L[𝕜] F))

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 [⋀^Fin n]→L[𝕜] F
x : Fin (n + 1) → E
⊢ Eq.{u_3 + 1} (α := F) (((alternatizeUncurryFin f).toAlternatingMap : (a : Fin (n + 1) → E) → F) x : F)
    ((AlternatingMap.alternatizeUncurryFin (toAlternatingMapLinear ∘ₗ (↑f : E →ₗ[𝕜] E [⋀^Fin n]→L[𝕜] F)) :
          (a : Fin (n + 1) → E) → F)
        x :
      F)

Tactic:
simp [alternatizeUncurryFin_apply, AlternatingMap.alternatizeUncurryFin_apply]

Premises used: AlternatingMap.alternatizeUncurryFin_apply, ContinuousAlternatingMap.alternatizeUncurryFin_apply
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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 g : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
⊢ alternatizeUncurryFin (f + g) = alternatizeUncurryFin f + alternatizeUncurryFin g

Tactic:
map_add (alternatizeUncurryFinCLM 𝕜 E F) f g

Premises used: ContinuousAlternatingMap.alternatizeUncurryFinCLM, map_add, ContinuousAlternatingMap.alternatizeUncurryFin
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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
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)
⊢ alternatizeUncurryFin f.curryLeft = (n + 1) • f

Tactic:
ext v
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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
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:
simp [alternatizeUncurryFin_apply, ← map_insertNth]

Premises used: ContinuousAlternatingMap.map_insertNth, ContinuousAlternatingMap.alternatizeUncurryFin_apply
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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
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)
⊢ alternatizeUncurryFin (c • f) = c • alternatizeUncurryFin f

Tactic:
ext v
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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
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:
simp [alternatizeUncurryFin_apply, smul_comm _ c, Finset.smul_sum]

Premises used: Finset.smul_sum, SMulCommClass.smul_comm, ContinuousAlternatingMap.alternatizeUncurryFin_apply
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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
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:
simp [alternatizeUncurryFin_apply]

Premises used: ContinuousAlternatingMap.alternatizeUncurryFin_apply
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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
v : Fin (n + 2) → E
⊢ Eq.{u_3 + 1} (α := F)
    ((alternatizeUncurryFin (alternatizeUncurryFinCLM 𝕜 E F ∘SL f) : (a : Fin (n + 1 + 1) → E) → F) v : F)
    (∑ i : Fin (n + 1),
        ∑ j ∈ Finset.Ici i,
          HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)) •
            HSub.hSub (α := F) (β := F)
              ((((((f : (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) (v i.castSucc) : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) :
                          (a : E) → E [⋀^Fin n]→L[𝕜] F)
                        (v j.succ) :
                      E [⋀^Fin n]→L[𝕜] F) :
                    (a : Fin n → E) → F)
                  (j.removeNth (α := fun (i : Fin (n + 1)) ↦ E)
                    (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ E) v)) :
                F)
              ((((((f : (a : E) → E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) (v j.succ) : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) :
                          (a : E) → E [⋀^Fin n]→L[𝕜] F)
                        (v i.castSucc) :
                      E [⋀^Fin n]→L[𝕜] F) :
                    (a : Fin n → E) → F)
                  (j.removeNth (α := fun (i : Fin (n + 1)) ↦ E)
                    (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ E) v)) :
                F) :
      F)

Tactic:
simpa [alternatizeUncurryFin_apply, AlternatingMap.alternatizeUncurryFin_apply]
    using AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply
      (R := 𝕜) (M := E) (N := F)
      (f.toLinearMap₁₂.compr₂ (toAlternatingMapLinear (R := 𝕜))) v

Premises used: AlternatingMap.alternatizeUncurryFin_apply, LinearMap.compr₂, AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, ContinuousAlternatingMap.toAlternatingMapLinear, ContinuousLinearMap.toLinearMap₁₂, ContinuousAlternatingMap.alternatizeUncurryFin_apply
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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)
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)
⊢ alternatizeUncurryFin (alternatizeUncurryFinCLM 𝕜 E F ∘SL f) = 0

Tactic:
ext v
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
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)
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:
simp [alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, hf]

Premises used: ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply