awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
⊢ Eq.{v + 1} (α := F)
    (∑ x_1 : { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 },
      (f.toFormalMultilinearSeries (E := E) (1 + (Fintype.card ι - 1)) :
          (a : (i : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) → F)
        ((↑x_1 : Finset (Fin (1 + (Fintype.card ι - 1)))).piecewise (π := fun (i : Fin (1 + (Fintype.card ι - 1))) ↦
          (i : ι) → E i) (fun (x_2 : Fin (1 + (Fintype.card ι - 1))) ↦ x) fun (x : Fin (1 + (Fintype.card ι - 1))) ↦ y))
    (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)))

Tactic:
(Fintype.sum_bijective (?_ ∘ Fintype.equivFinOfCardEq (Nat.add_sub_of_le
    Fintype.card_pos).symm) (.comp ?_ <| Equiv.bijective _) _ _ fun i ↦ ?_).symm

Premises used: Equiv.bijective, Fintype.equivFinOfCardEq, Function.comp, Nat.add_sub_of_le, Fintype.sum_bijective, Function.Bijective.comp, Eq.symm, DFunLike.coe, Fintype.card_pos
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h_1 : Nonempty ι
h :
  Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0)) →
    { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 }
h₁ :
  Function.Bijective (β := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
    fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
    Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ ⋯
h₂ :
  ∀ (i : ι),
    Eq.{v + 1} (α := F) ((f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
      ((f.toFormalMultilinearSeries (E := E) (1 + (Fintype.card ι - 1)) :
            (a : (i : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) → F)
          (Finset.piecewise (π := fun (i : Fin (1 + (Fintype.card ι - 1))) ↦ (i : ι) → E i)
            (↑(((fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
                      Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ
                        ⋯) ∘
                    (⇑(Fintype.equivFinOfCardEq ⋯) : (a : ι) → Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))))
                  i) :
              Finset (Fin (1 + (Fintype.card ι - 1))))
            (fun (x_1 : Fin (1 + (Fintype.card ι - 1))) ↦ x) fun (x : Fin (1 + (Fintype.card ι - 1))) ↦ y) :
        F)
⊢ Eq.{v + 1} (α := F)
    (∑ x_1 : { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 },
      (f.toFormalMultilinearSeries (E := E) (1 + (Fintype.card ι - 1)) :
          (a : (i : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) → F)
        ((↑x_1 : Finset (Fin (1 + (Fintype.card ι - 1)))).piecewise (π := fun (i : Fin (1 + (Fintype.card ι - 1))) ↦
          (i : ι) → E i) (fun (x_2 : Fin (1 + (Fintype.card ι - 1))) ↦ x) fun (x : Fin (1 + (Fintype.card ι - 1))) ↦ y))
    (∑ i : ι, (f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)))

Tactic:
refine (Fintype.sum_bijective (?_ ∘ Fintype.equivFinOfCardEq (Nat.add_sub_of_le
    Fintype.card_pos).symm) (.comp ?_ <| Equiv.bijective _) _ _ fun i ↦ ?_).symm

Premises used: Equiv.bijective, Fintype.equivFinOfCardEq, Function.comp, Nat.add_sub_of_le, Fintype.sum_bijective, Function.Bijective.comp, Eq.symm, DFunLike.coe, Fintype.card_pos
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
⊢ Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0)) →
    { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 }

Tactic:
exact (⟨{·}ᶜ, by
      rw [card_compl, Fintype.card_fin, Finset.card_singleton, Nat.add_sub_cancel_left]⟩)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
right :
  Function.Surjective (β := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
    fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
    Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ ⋯
⊢ Function.Bijective (β := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
    fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
    Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ ⋯

Tactic:
use fun _ _ ↦ (singleton_injective <| compl_injective <| Subtype.ext_iff.mp ·)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
rw : Fintype.card (Fin (1 + (Fintype.card ι - 1))) - #s = 1
rw₁ : Fintype.card (Fin (1 + (Fintype.card ι - 1))) - (Fintype.card ι - 1) = 1
rw₂ : 1 + (Fintype.card ι - 1) - (Fintype.card ι - 1) = 1
rw₃ rw₄ : Eq (α := ℕ) 1 1
⊢ #sᶜ = 1

Tactic:
rw [card_compl, hs, Fintype.card_fin, Nat.add_sub_cancel]

Premises used: Fintype.card_fin, Finset.card_compl, Nat.add_sub_cancel
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
⊢ #sᶜ = 1

Tactic:
have h : #sᶜ = 1 := by rw [card_compl, hs, Fintype.card_fin, Nat.add_sub_cancel]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h_1 : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
h : #sᶜ = 1
right :
  ∀ (a : Fin (1 + (Fintype.card ι - 1))) (ha : sᶜ = {a}),
    ∃ (a : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))),
      Eq (α := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
        ((fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
            (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ ⋯ :
              { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 }))
          a)
        (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) s hs)
⊢ ∃ (a : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))),
    Eq (α := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
      ((fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
          (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ ⋯ :
            { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 }))
        a)
      (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) s hs)

Tactic:
obtain ⟨a, ha⟩ := card_eq_one.mp h

Premises used: Finset.card_eq_one, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h_1 : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
h : #sᶜ = 1
a : Fin (1 + (Fintype.card ι - 1))
ha : sᶜ = {a}
⊢ ∃ (a : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))),
    Eq (α := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
      ((fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
          (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ ⋯ :
            { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 }))
        a)
      (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) s hs)

Tactic:
⟨a, Subtype.ext (compl_eq_comm.mp ha)⟩

Premises used: Exists.intro, Iff.mp, compl_eq_comm, Subtype.ext
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h_1 : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
h : #sᶜ = 1
a : Fin (1 + (Fintype.card ι - 1))
ha : sᶜ = {a}
⊢ ∃ (a : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))),
    Eq (α := { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 })
      ((fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
          (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ ⋯ :
            { s : Finset (Fin (1 + (Fintype.card ι - 1))) // #s = Fintype.card ι - 1 }))
        a)
      (Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) s hs)

Tactic:
exact ⟨a, Subtype.ext (compl_eq_comm.mp ha)⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h_1 : Nonempty ι
i : ι
h :
  Eq.{v + 1} (α := F) ((f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
    ((domDomCongr (Fintype.equivFinOfCardEq ⋯)
            (f.compContinuousLinearMap (M₁ := fun (i : ι) ↦ (i : ι) → E i) (M₁' := E)
              (ContinuousLinearMap.proj (φ := E))) :
          (a : (i : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) → F)
        (Function.update (β := fun (i : Fin (1 + (Fintype.card ι - 1))) ↦ (i : ι) → E i)
            (fun (x_1 : Fin (1 + (Fintype.card ι - 1))) ↦ x)
            (((Fintype.equivFinOfCardEq ⋯ : ι ≃ Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) :
                (a : ι) → Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0)))
              i)
            y :
          (a : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) :
      F)
⊢ Eq.{v + 1} (α := F) ((f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
    ((f.toFormalMultilinearSeries (E := E) (1 + (Fintype.card ι - 1)) :
          (a : (i : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) → F)
        (Finset.piecewise (π := fun (i : Fin (1 + (Fintype.card ι - 1))) ↦ (i : ι) → E i)
          (↑(((fun (x : Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) ↦
                    Subtype.mk (p := fun (s : Finset (Fin (1 + (Fintype.card ι - 1)))) ↦ #s = Fintype.card ι - 1) {x}ᶜ
                      ⋯) ∘
                  (⇑(Fintype.equivFinOfCardEq ⋯) : (a : ι) → Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))))
                i) :
            Finset (Fin (1 + (Fintype.card ι - 1))))
          (fun (x_1 : Fin (1 + (Fintype.card ι - 1))) ↦ x) fun (x : Fin (1 + (Fintype.card ι - 1))) ↦ y) :
      F)

Tactic:
rw [Function.comp_apply, Subtype.coe_mk, compl_singleton, piecewise_erase_univ,
    toFormalMultilinearSeries, dif_pos (Nat.add_sub_of_le Fintype.card_pos).symm]

Premises used: Subtype.coe_mk, Finset.compl_singleton, Nat.add_sub_of_le, dif_pos, ContinuousMultilinearMap.toFormalMultilinearSeries, Finset.piecewise_erase_univ, Function.comp_apply, Eq.symm, Fintype.card_pos
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h_1 : Nonempty ι
i : ι
h :
  Eq.{v + 1} (α := F) ((f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
    ((f : (a : (i : ι) → E i) → F) fun (i_1 : ι) ↦ if i_1 = i then y i_1 else x i_1 : F)
⊢ Eq.{v + 1} (α := F) ((f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
    ((domDomCongr (Fintype.equivFinOfCardEq ⋯)
            (f.compContinuousLinearMap (M₁ := fun (i : ι) ↦ (i : ι) → E i) (M₁' := E)
              (ContinuousLinearMap.proj (φ := E))) :
          (a : (i : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) → F)
        (Function.update (β := fun (i : Fin (1 + (Fintype.card ι - 1))) ↦ (i : ι) → E i)
            (fun (x_1 : Fin (1 + (Fintype.card ι - 1))) ↦ x)
            (((Fintype.equivFinOfCardEq ⋯ : ι ≃ Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0))) :
                (a : ι) → Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0)))
              i)
            y :
          (a : Fin (1 + (Fintype.card ι - 1))) → (i : ι) → E i) :
      F)

Tactic:
simp_rw [domDomCongr_apply, compContinuousLinearMap_apply, ContinuousLinearMap.proj_apply,
    Function.update_apply, (Equiv.injective _).eq_iff, ite_apply]

Premises used: ite_apply, ContinuousLinearMap.proj_apply, Function.Injective.eq_iff, Function.update_apply, ContinuousMultilinearMap.compContinuousLinearMap_apply, ContinuousMultilinearMap.domDomCongr_apply, Equiv.injective
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h_1 : Nonempty ι
i : ι
h : Function.update (β := E) x i (y i) = fun (i_1 : ι) ↦ if i_1 = i then y i_1 else x i_1
⊢ Eq.{v + 1} (α := F) ((f : (a : (i : ι) → E i) → F) (Function.update (β := E) x i (y i)) : F)
    ((f : (a : (i : ι) → E i) → F) fun (i_1 : ι) ↦ if i_1 = i then y i_1 else x i_1 : F)

Tactic:
congr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
y : (i : ι) → E i
h : Nonempty ι
i : ι
⊢ Function.update (β := E) x i (y i) = fun (i_1 : ι) ↦ if i_1 = i then y i_1 else x i_1

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
rw :
  HasStrictFDerivAt (𝕜 := 𝕜) (F := F) (⇑f : (a : (i : ι) → E i) → F)
    ((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F) → ((i : ι) → E i) →L[𝕜] F)
      (changeOrigin (f.toFormalMultilinearSeries (E := E)) x 1))
    x
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := F) (⇑f : (a : (i : ι) → E i) → F) (f.linearDeriv (M₁ := E) x) x

Tactic:
rw [← changeOrigin_toFormalMultilinearSeries]

Premises used: ContinuousMultilinearMap.changeOrigin_toFormalMultilinearSeries
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := F) (⇑f : (a : (i : ι) → E i) → F)
    ((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F) → ((i : ι) → E i) →L[𝕜] F)
      (changeOrigin (f.toFormalMultilinearSeries (E := E)) x 1))
    (0 + x)

Tactic:
f.hasFiniteFPowerSeriesOnBall.hasStrictFDerivAt (y := x) ENNReal.coe_lt_top

Premises used: ContinuousMultilinearMap.hasFiniteFPowerSeriesOnBall, HasFiniteFPowerSeriesOnBall.hasStrictFDerivAt, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
h : x = 0 + x
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := F) (⇑f : (a : (i : ι) → E i) → F)
    ((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F :
        (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ (i : ι) → E i) F) → ((i : ι) → E i) →L[𝕜] F)
      (changeOrigin (f.toFormalMultilinearSeries (E := E)) x 1))
    x

Tactic:
convert! f.hasFiniteFPowerSeriesOnBall.hasStrictFDerivAt (y := x) ENNReal.coe_lt_top

Premises used: ContinuousMultilinearMap.hasFiniteFPowerSeriesOnBall, HasFiniteFPowerSeriesOnBall.hasStrictFDerivAt, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
h h₁ : x = x
⊢ x = 0 + x

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst_6 : DecidableEq ι
⊢ HasFDerivAt (𝕜 := 𝕜) (F := F) (⇑f : (a : (i : ι) → E i) → F) (f.linearDeriv (M₁ := E) x) x

Tactic:
(f.hasStrictFDerivAt _).hasFDerivAt

Premises used: ContinuousMultilinearMap.hasStrictFDerivAt, HasStrictFDerivAt.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
inst_6 : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  ContinuousLinearMap.continuousMultilinearMapOption (E := E)
    (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F))
⊢ HasStrictFDerivAt
    (fun (x : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
      (f : (a : (i : Option ι) → ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) → F)
        ((fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (x : Option ι) ↦ fx) x))
    ((f.linearDeriv (M₁ := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) fun (x : Option ι) ↦
        fa) ∘SL
      ContinuousLinearMap.pi (φ := fun (i : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
        fun (x : Option ι) ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa

Tactic:
have Hf := (f.hasStrictFDerivAt (fun _ ↦ fa)).comp (f := fun fx _ ↦ fx) fa
    (hasStrictFDerivAt_pi.2 fun _ ↦ hasStrictFDerivAt_id _)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_5 : Fintype ι
inst_6 : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  ContinuousLinearMap.continuousMultilinearMapOption (E := E)
    (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F))
Hf :
  HasStrictFDerivAt
    (fun (x : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
      (f : (a : (i : Option ι) → ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) → F)
        ((fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (x : Option ι) ↦ fx) x))
    ((f.linearDeriv (M₁ := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) fun (x : Option ι) ↦
        fa) ∘SL
      ContinuousLinearMap.pi (φ := fun (i : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
        fun (x : Option ι) ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
⊢ HasStrictFDerivAt
    (fun (x : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) ↦
      (f : (a : (i : Option ι) → ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) → F)
        ((fun (fx : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) (x : Option ι) ↦ fx) x))
    ((f.linearDeriv (M₁ := fun (x : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) fun (x : Option ι) ↦
        fa) ∘SL
      ContinuousLinearMap.pi (φ := fun (i : Option ι) ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i))
        fun (x : Option ι) ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa

Tactic:
Hf