awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
trans :
  Eq.{wG + 1} (α := G)
    (((((f.fderivCompContinuousLinearMap (E := fun (x : ι) ↦ E) (E₁ := fun (x : ι) ↦ F) fun (x : ι) ↦ g) ∘SL
                  ContinuousLinearMap.pi (φ := fun (i : ι) ↦ E →L[𝕜] F) fun (x : ι) ↦
                    ContinuousLinearMap.id 𝕜 (E →L[𝕜] F) :
                (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G)
              dg :
            ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G) :
          (a : (i : ι) → E) → G)
        v :
      G)
    (∑ i : ι,
        (f : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
      G)
trans₁ :
  Eq.{wG + 1} (α := G)
    (∑ i : ι,
      (f : (a : ι → F) → G) fun (j : ι) ↦
        ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F) (v j))
    0
⊢ Eq.{wG + 1} (α := G)
    (((((f.fderivCompContinuousLinearMap (E := fun (x : ι) ↦ E) (E₁ := fun (x : ι) ↦ F) fun (x : ι) ↦ g) ∘SL
                  ContinuousLinearMap.pi (φ := fun (i : ι) ↦ E →L[𝕜] F) fun (x : ι) ↦
                    ContinuousLinearMap.id 𝕜 (E →L[𝕜] F) :
                (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G)
              dg :
            ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G) :
          (a : (i : ι) → E) → G)
        v :
      G)
    (0 : G)

Tactic:
trans ∑ i, f fun j ↦ Function.update (fun _ ↦ g) i dg j (v j)
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ Eq.{wG + 1} (α := G)
    (((((f.fderivCompContinuousLinearMap (E := fun (x : ι) ↦ E) (E₁ := fun (x : ι) ↦ F) fun (x : ι) ↦ g) ∘SL
                  ContinuousLinearMap.pi (φ := fun (i : ι) ↦ E →L[𝕜] F) fun (x : ι) ↦
                    ContinuousLinearMap.id 𝕜 (E →L[𝕜] F) :
                (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ E) G)
              dg :
            ContinuousMultilinearMap.{u, v, wE, wG} 𝕜 (fun (x : ι) ↦ E) G) :
          (a : (i : ι) → E) → G)
        v :
      G)
    (∑ i : ι,
        (f : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
      G)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
rw :
  HAdd.hAdd (α := G) (β := G)
      ((f : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
        G)
      ((f : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
        G) =
    0
rw₁ :
  ∀ (x : ι),
    Membership.mem (γ := Finset ι) {a, b}ᶜ x →
      Eq.{wG + 1} (α := G)
        ((f : (a : ι → F) → G) fun (j : ι) ↦
            ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) x dg j : E →L[𝕜] F) : (a : E) → F)
              (v j) :
          G)
        (0 : G)
⊢ Eq.{wG + 1} (α := G)
    (∑ i : ι,
      (f : (a : ι → F) → G) fun (j : ι) ↦
        ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F) (v j))
    0

Tactic:
rw [← Finset.sum_add_sum_compl {a, b}, Finset.sum_pair hne, Finset.sum_eq_zero, add_zero]

Premises used: Finset.sum_pair, Finset.sum_eq_zero, Insert.insert, add_zero, Singleton.singleton, Finset.sum_add_sum_compl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ HAdd.hAdd (α := G) (β := G)
      ((f.toAlternatingMap : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
        G)
      ((f.toAlternatingMap : (a : ι → F) → G)
          ((fun (j : ι) ↦
              ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F)
                (v j)) ∘
            (⇑(Equiv.swap a b) : (a : ι) → ι)) :
        G) =
    0

Tactic:
f.map_add_swap _ hne

Premises used: ContinuousAlternatingMap.toAlternatingMap, AlternatingMap.map_add_swap
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
h :
  ∀ (i : ι),
    Eq.{wF + 1} (α := F)
      (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg i : E →L[𝕜] F) : (a : E) → F) (v i) : F)
      (((fun (j : ι) ↦
              ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F)
                (v j)) ∘
            (⇑(Equiv.swap a b) : (a : ι) → ι))
          i :
        F)
⊢ HAdd.hAdd (α := G) (β := G)
      ((f : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
        G)
      ((f : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
        G) =
    0

Tactic:
convert! f.map_add_swap _ hne with i

Premises used: ContinuousAlternatingMap.toAlternatingMap, AlternatingMap.map_add_swap
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
i : ι
h :
  ∀ (heq : v i = v b) (hne : i ≠ b),
    Eq.{wF + 1} (α := F)
      (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg i : E →L[𝕜] F) : (a : E) → F) (v i) : F)
      (((fun (j : ι) ↦
              ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F)
                (v j)) ∘
            (⇑(Equiv.swap i b) : (a : ι) → ι))
          i :
        F)
h₁ :
  ∀ (hia : i ≠ a),
    Eq.{wF + 1} (α := F)
      (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg i : E →L[𝕜] F) : (a : E) → F) (v i) : F)
      (((fun (j : ι) ↦
              ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F)
                (v j)) ∘
            (⇑(Equiv.swap a b) : (a : ι) → ι))
          i :
        F)
⊢ Eq.{wF + 1} (α := F)
    (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg i : E →L[𝕜] F) : (a : E) → F) (v i) : F)
    (((fun (j : ι) ↦
            ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F)
              (v j)) ∘
          (⇑(Equiv.swap a b) : (a : ι) → ι))
        i :
      F)

Tactic:
rcases eq_or_ne i a with rfl | hia

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
b i : ι
heq : v i = v b
hne : i ≠ b
⊢ Eq.{wF + 1} (α := F)
    (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg i : E →L[𝕜] F) : (a : E) → F) (v i) : F)
    (((fun (j : ι) ↦
            ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F)
              (v j)) ∘
          (⇑(Equiv.swap i b) : (a : ι) → ι))
        i :
      F)

Tactic:
simp [heq, hne, hne.symm]

Premises used: Ne.symm
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
i : ι
hia : i ≠ a
h :
  ∀ (heq : v a = v i) (hne : a ≠ i),
    Eq.{wF + 1} (α := F)
      (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg i : E →L[𝕜] F) : (a : E) → F) (v i) : F)
      (((fun (j : ι) ↦
              ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F)
                (v j)) ∘
            (⇑(Equiv.swap a i) : (a : ι) → ι))
          i :
        F)
h₁ :
  ∀ (hib : i ≠ b),
    Eq.{wF + 1} (α := F)
      (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg i : E →L[𝕜] F) : (a : E) → F) (v i) : F)
      (((fun (j : ι) ↦
              ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F)
                (v j)) ∘
            (⇑(Equiv.swap a b) : (a : ι) → ι))
          i :
        F)
⊢ Eq.{wF + 1} (α := F)
    (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg i : E →L[𝕜] F) : (a : E) → F) (v i) : F)
    (((fun (j : ι) ↦
            ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F)
              (v j)) ∘
          (⇑(Equiv.swap a b) : (a : ι) → ι))
        i :
      F)

Tactic:
rcases eq_or_ne i b with rfl | hib

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a i : ι
hia : i ≠ a
heq : v a = v i
hne : a ≠ i
⊢ Eq.{wF + 1} (α := F)
    (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg i : E →L[𝕜] F) : (a : E) → F) (v i) : F)
    (((fun (j : ι) ↦
            ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F)
              (v j)) ∘
          (⇑(Equiv.swap a i) : (a : ι) → ι))
        i :
      F)

Tactic:
simp [Function.update_apply, heq]

Premises used: Function.update_apply
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
i : ι
hia : i ≠ a
hib : i ≠ b
⊢ Eq.{wF + 1} (α := F)
    (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) b dg i : E →L[𝕜] F) : (a : E) → F) (v i) : F)
    (((fun (j : ι) ↦
            ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) a dg j : E →L[𝕜] F) : (a : E) → F)
              (v j)) ∘
          (⇑(Equiv.swap a b) : (a : ι) → ι))
        i :
      F)

Tactic:
simp [Function.update_apply, Equiv.swap_apply_of_ne_of_ne, *]

Premises used: Function.update_apply, Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
simp :
  ∀ (x : ι),
    ¬x = a →
      ¬x = b →
        Eq.{wG + 1} (α := G)
          ((f : (a : ι → F) → G) fun (j : ι) ↦
              ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) x dg j : E →L[𝕜] F) : (a : E) → F)
                (v j) :
            G)
          (0 : G)
⊢ ∀ (x : ι),
    Membership.mem (γ := Finset ι) {a, b}ᶜ x →
      Eq.{wG + 1} (α := G)
        ((f : (a : ι → F) → G) fun (j : ι) ↦
            ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) x dg j : E →L[𝕜] F) : (a : E) → F)
              (v j) :
          G)
        (0 : G)

Tactic:
simp only [mem_compl, mem_insert, mem_singleton, not_or, and_imp]

Premises used: Finset.mem_singleton, and_imp, Finset.mem_insert, Finset.mem_compl, not_or
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
i : ι
hia : ¬i = a
hib : ¬i = b
apply :
  Eq.{wF + 1} (α := F)
    (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg a : E →L[𝕜] F) : (a : E) → F) (v a) : F)
    (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg b : E →L[𝕜] F) : (a : E) → F) (v b) : F)
⊢ Eq.{wG + 1} (α := G)
    ((f : (a : ι → F) → G) fun (j : ι) ↦
        ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
      G)
    (0 : G)

Tactic:
apply f.map_eq_zero_of_eq _ _ hne

Premises used: ContinuousAlternatingMap.map_eq_zero_of_eq
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : (i : ι) → E
a b : ι
heq : v a = v b
hne : a ≠ b
i : ι
hia : ¬i = a
hib : ¬i = b
⊢ Eq.{wF + 1} (α := F)
    (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg a : E →L[𝕜] F) : (a : E) → F) (v a) : F)
    (((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg b : E →L[𝕜] F) : (a : E) → F) (v b) : F)

Tactic:
simp [*, Ne.symm]

Premises used: Ne.symm
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g : E →L[𝕜] F
⊢ toContinuousMultilinearMapCLM 𝕜 ∘SL f.fderivCompContinuousLinearMap g =
    (f.fderivCompContinuousLinearMap (E := fun (x : ι) ↦ E) (E₁ := fun (x : ι) ↦ F) fun (x : ι) ↦ g) ∘SL
      ContinuousLinearMap.pi (φ := fun (i : ι) ↦ E →L[𝕜] F) fun (x : ι) ↦ ContinuousLinearMap.id 𝕜 (E →L[𝕜] F)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, Multiset.sum, ContinuousAlternatingMap.toContinuousMultilinearMapLinear, Multiset.foldr, ContinuousMultilinearMap.fderivCompContinuousLinearMap, ContinuousMultilinearMap.linearDeriv, ContinuousAlternatingMap.toContinuousMultilinearMapCLM, Finset.sum, rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
⊢ Eq.{wG + 1} (α := G)
    ((((f.fderivCompContinuousLinearMap g : (a : E →L[𝕜] F) → E [⋀^ι]→L[𝕜] G) dg : E [⋀^ι]→L[𝕜] G) : (a : ι → E) → G)
        v :
      G)
    (∑ i : ι,
        (f : (a : ι → F) → G) fun (j : ι) ↦
          ((Function.update (β := fun (x : ι) ↦ E →L[𝕜] F) (fun (x : ι) ↦ g) i dg j : E →L[𝕜] F) : (a : E) → F) (v j) :
      G)

Tactic:
simp [fderivCompContinuousLinearMap]

Premises used: ContinuousAlternatingMap.fderivCompContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : IsEmpty ι
h :
  ∀ (x : F [⋀^ι]→L[𝕜] G) (x_1 x_2 : E →L[𝕜] F) (x_3 : ι → E),
    Eq.{wG + 1} (α := G)
      ((((x.fderivCompContinuousLinearMap x_1 : (a : E →L[𝕜] F) → E [⋀^ι]→L[𝕜] G) x_2 : E [⋀^ι]→L[𝕜] G) :
            (a : ι → E) → G)
          x_3 :
        G)
      ((((0 x x_1 : (a : E →L[𝕜] F) → E [⋀^ι]→L[𝕜] G) x_2 : E [⋀^ι]→L[𝕜] G) : (a : ι → E) → G) x_3 : G)
⊢ Eq (α := (f : F [⋀^ι]→L[𝕜] G) → (g : E →L[𝕜] F) → (E →L[𝕜] F) →L[𝕜] E [⋀^ι]→L[𝕜] G) fderivCompContinuousLinearMap 0

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : IsEmpty ι
x : F [⋀^ι]→L[𝕜] G
x_1 x_2 : E →L[𝕜] F
x_3 : ι → E
⊢ Eq.{wG + 1} (α := G)
    ((((x.fderivCompContinuousLinearMap x_1 : (a : E →L[𝕜] F) → E [⋀^ι]→L[𝕜] G) x_2 : E [⋀^ι]→L[𝕜] G) : (a : ι → E) → G)
        x_3 :
      G)
    ((((0 x x_1 : (a : E →L[𝕜] F) → E [⋀^ι]→L[𝕜] G) x_2 : E [⋀^ι]→L[𝕜] G) : (a : ι → E) → G) x_3 : G)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : F [⋀^ι]→L[𝕜] G
g : E →L[𝕜] F
⊢ (fderivCompContinuousLinearMapCLM G g : (a : F [⋀^ι]→L[𝕜] G) → (E →L[𝕜] F) →L[𝕜] E [⋀^ι]→L[𝕜] G) f =
    f.fderivCompContinuousLinearMap g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H :
  ∀ (x : F) (m : ι → E),
    norm.{wG} (E := G) ((((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x : E [⋀^ι]→ₗ[𝕜] G) : (a : ι → E) → G) m : G) ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
x y : F
H₁ :
  ∀ (x_1 : ι → E),
    Eq.{wG + 1} (α := G)
      ((mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) (x + y)) (C * ‖x + y‖) ⋯ : (a : ι → E) → G) x_1 : G)
      ((mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x) (C * ‖x‖) ⋯ +
              mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) y) (C * ‖y‖) ⋯ :
            (a : ι → E) → G)
          x_1 :
        G)
⊢ mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) (x + y)) (C * ‖x + y‖) ⋯ =
    mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x) (C * ‖x‖) ⋯ +
      mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) y) (C * ‖y‖) ⋯

Tactic:
ext1
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H :
  ∀ (x : F) (m : ι → E),
    norm.{wG} (E := G) ((((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x : E [⋀^ι]→ₗ[𝕜] G) : (a : ι → E) → G) m : G) ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
x y : F
x_1 : ι → E
⊢ Eq.{wG + 1} (α := G)
    ((mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) (x + y)) (C * ‖x + y‖) ⋯ : (a : ι → E) → G) x_1 : G)
    ((mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x) (C * ‖x‖) ⋯ +
            mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) y) (C * ‖y‖) ⋯ :
          (a : ι → E) → G)
        x_1 :
      G)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Alternating.Basic
Goal:
𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H :
  ∀ (x : F) (m : ι → E),
    norm.{wG} (E := G) ((((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x : E [⋀^ι]→ₗ[𝕜] G) : (a : ι → E) → G) m : G) ≤
      C * ‖x‖ * ∏ i : ι, ‖m i‖
c : 𝕜
x : F
H₁ :
  ∀ (x_1 : ι → E),
    Eq.{wG + 1} (α := G)
      ((mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) (c • x)) (C * ‖c • x‖) ⋯ : (a : ι → E) → G) x_1 : G)
      ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
              (mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x) (C * ‖x‖) ⋯) :
            (a : ι → E) → G)
          x_1 :
        G)
⊢ mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) (c • x)) (C * ‖c • x‖) ⋯ =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (mkContinuous ((f : (a : F) → E [⋀^ι]→ₗ[𝕜] G) x) (C * ‖x‖) ⋯)

Tactic:
ext1