awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ
H :
  ∀ᵐ (x : E) ∂μ,
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x
x : E
hx :
  x ∈ s →
    DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
      ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x
xs : x ∈ s
this :
  f =
    Function.comp (β := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        (⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) → F)
        (⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘
      f
⊢ DifferentiableWithinAt ℝ (F := F)
    (Function.comp (β := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        (⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) → F)
        (⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘
      f)
    s x

Tactic:
exact A.symm.differentiableAt.comp_differentiableWithinAt x (hx xs)

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.differentiableAt, DifferentiableAt.comp_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ
suffices :
  ∀ᵐ (x : E) ∂μ,
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
suffices H : ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ (A ∘ f) s x by
    filter_upwards [H] with x hx xs
    have : f = (A.symm ∘ A) ∘ f := by
      simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]
    rw [this]
    exact A.symm.differentiableAt.comp_differentiableWithinAt x (hx xs)
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ
hf₁ :
  LipschitzOnWith (β := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
    (‖(↑A : F →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)‖₊ * C)
    ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s
C₁ : ℝ≥0
⊢ ∀ᵐ (x : E) ∂μ,
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x

Tactic:
apply ae_differentiableWithinAt_of_mem_pi

Premises used: LipschitzOnWith.ae_differentiableWithinAt_of_mem_pi
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ
⊢ LipschitzOnWith (β := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
    (‖(↑A : F →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)‖₊ * C)
    ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s

Tactic:
A.lipschitz.comp_lipschitzOnWith hf

Premises used: LipschitzWith.comp_lipschitzOnWith, ContinuousLinearEquiv.lipschitz
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
hs : MeasurableSet s
rw : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
⊢ ∀ᵐ (x : E) ∂μ.restrict s, DifferentiableWithinAt ℝ f s x

Tactic:
rw [ae_restrict_iff' hs]

Premises used: MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
hf.ae_differentiableWithinAt_of_mem

Premises used: LipschitzOnWith.ae_differentiableWithinAt_of_mem
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
hs : MeasurableSet s
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
exact hf.ae_differentiableWithinAt_of_mem

Premises used: LipschitzOnWith.ae_differentiableWithinAt_of_mem
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
h : LipschitzWith C f
⊢ LipschitzOnWith C f univ

Tactic:
rw [← lipschitzOnWith_univ] at h

Premises used: lipschitzOnWith_univ
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
F : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
C : ℝ≥0
μ : Measure E
inst_6 : FiniteDimensional ℝ E
inst_7 : FiniteDimensional ℝ F
inst_8 : μ.IsAddHaarMeasure
f : E → F
h : LipschitzOnWith C f univ
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x

Tactic:
simpa [differentiableWithinAt_univ] using h.ae_differentiableWithinAt_of_mem

Premises used: LipschitzOnWith.ae_differentiableWithinAt_of_mem, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x

Tactic:
lipschitzWith_one_norm.ae_differentiableAt

Premises used: LipschitzWith.ae_differentiableAt
-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
⊢ Dense.{u_1} (X := E) {x : E | DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) x}

Tactic:
let _ : MeasurableSpace E := borel E
  have _ : BorelSpace E := ⟨rfl⟩
  let w := Basis.ofVectorSpace ℝ E
  MeasureTheory.Measure.dense_of_ae (ae_differentiableAt_norm (μ := w.addHaar))

Premises used: Real, MeasureTheory.Measure.dense_of_ae, ae_differentiableAt_norm, borel, Module.Basis.ofVectorSpace, BorelSpace.mk, rfl
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable.{u_5, u_1} (α := F) fun (x : α) ↦ f x x₀
hx : x ∈ s
haveI : ∀ (this : DecidableEq α), Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x
⊢ Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x

Tactic:
haveI := Classical.decEq α
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable.{u_5, u_1} (α := F) fun (x : α) ↦ f x x₀
hx : x ∈ s
this : DecidableEq α
rw :
  ∀ (hf0 : CauchySeq.{u_5, u_1} (α := F) fun (s : Finset α) ↦ ∑ b ∈ s, f b x₀) (hx : x ∈ s) (this : DecidableEq α),
    CauchySeq.{u_5, u_1} (α := F) fun (s : Finset α) ↦ ∑ b ∈ s, f b x
⊢ Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x

Tactic:
rw [summable_iff_cauchySeq_finset] at hf0 ⊢

Premises used: summable_iff_cauchySeq_finset
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq.{u_5, u_1} (α := F) fun (s : Finset α) ↦ ∑ b ∈ s, f b x₀
hx : x ∈ s
this : DecidableEq α
⊢ UniformCauchySeqOn (β := E →L[𝕜] F) (fun (t : Finset α) (x : E) ↦ ∑ i ∈ t, f' i x) atTop s

Tactic:
have A : UniformCauchySeqOn (fun t : Finset α => fun x => ∑ i ∈ t, f' i x) atTop s :=
    (tendstoUniformlyOn_tsum hu hf').uniformCauchySeqOn
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq.{u_5, u_1} (α := F) fun (s : Finset α) ↦ ∑ b ∈ s, f b x₀
hx : x ∈ s
this : DecidableEq α
A : UniformCauchySeqOn (β := E →L[𝕜] F) (fun (t : Finset α) (x : E) ↦ ∑ i ∈ t, f' i x) atTop s
⊢ CauchySeq.{u_5, u_1} (α := F) fun (s : Finset α) ↦ ∑ b ∈ s, f b x

Tactic:
cauchy_map_of_uniformCauchySeqOn_fderiv (f := fun t x ↦ ∑ i ∈ t, f i x)
    hs h's A (fun t y hy => ?_) hx₀ hx hf0

Premises used: CauchySeq, cauchy_map_of_uniformCauchySeqOn_fderiv
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq.{u_5, u_1} (α := F) fun (s : Finset α) ↦ ∑ b ∈ s, f b x₀
hx : x ∈ s
this : DecidableEq α
A : UniformCauchySeqOn (β := E →L[𝕜] F) (fun (t : Finset α) (x : E) ↦ ∑ i ∈ t, f' i x) atTop s
refine :
  ∀ (t : Finset α) (y : E) (hy : y ∈ s),
    HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) ((fun (t : Finset α) (x : E) ↦ (∑ i ∈ t, f i x : F)) t)
      (∑ i ∈ t, f' i y) y
⊢ CauchySeq.{u_5, u_1} (α := F) fun (s : Finset α) ↦ ∑ b ∈ s, f b x

Tactic:
refine cauchy_map_of_uniformCauchySeqOn_fderiv (f := fun t x ↦ ∑ i ∈ t, f i x)
    hs h's A (fun t y hy => ?_) hx₀ hx hf0

Premises used: cauchy_map_of_uniformCauchySeqOn_fderiv
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq.{u_5, u_1} (α := F) fun (s : Finset α) ↦ ∑ b ∈ s, f b x₀
hx : x ∈ s
this : DecidableEq α
A : UniformCauchySeqOn (β := E →L[𝕜] F) (fun (t : Finset α) (x : E) ↦ ∑ i ∈ t, f' i x) atTop s
t : Finset α
y : E
hy : y ∈ s
⊢ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) ((fun (t : Finset α) (x : E) ↦ (∑ i ∈ t, f i x : F)) t)
    (∑ i ∈ t, f' i y) y

Tactic:
HasFDerivAt.fun_sum fun i _ => hf i y hy

Premises used: HasFDerivAt.fun_sum
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : CauchySeq.{u_5, u_1} (α := F) fun (s : Finset α) ↦ ∑ b ∈ s, f b x₀
hx : x ∈ s
this : DecidableEq α
A : UniformCauchySeqOn (β := E →L[𝕜] F) (fun (t : Finset α) (x : E) ↦ ∑ i ∈ t, f' i x) atTop s
t : Finset α
y : E
hy : y ∈ s
⊢ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) ((fun (t : Finset α) (x : E) ↦ (∑ i ∈ t, f i x : F)) t)
    (∑ i ∈ t, f' i y) y

Tactic:
exact HasFDerivAt.fun_sum fun i _ => hf i y hy

Premises used: HasFDerivAt.fun_sum
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg : ∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable.{u_5, u_1} (α := F) fun (x : α) ↦ g x y₀
hy : y ∈ t
⊢ ∀ (n : α), ∀ y ∈ t, HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y

Tactic:
simp_rw [hasDerivAt_iff_hasFDerivAt] at hg

Premises used: hasDerivAt_iff_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable.{u_5, u_1} (α := F) fun (x : α) ↦ g x y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
⊢ Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y

Tactic:
summable_of_summable_hasFDerivAt_of_isPreconnected hu ht h't hg ?_ hy₀ hg0 hy

Premises used: summable_of_summable_hasFDerivAt_of_isPreconnected
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable.{u_5, u_1} (α := F) fun (x : α) ↦ g x y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
refine : ∀ (n : α), ∀ x ∈ t, norm (E := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n x)) ≤ u n
⊢ Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y

Tactic:
refine summable_of_summable_hasFDerivAt_of_isPreconnected hu ht h't hg ?_ hy₀ hg0 hy

Premises used: summable_of_summable_hasFDerivAt_of_isPreconnected
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace F
u : α → ℝ
inst_4 : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable.{u_5, u_1} (α := F) fun (x : α) ↦ g x y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
⊢ ∀ (n : α), ∀ x ∈ t, norm (E := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n x)) ≤ u n

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
hx : x ∈ s
y : E
hy : y ∈ s
ha : Summable.{u_5, u_1} (α := F) (fun (b : α) ↦ f b y) { filter := sInf (range fun (a : Finset α) ↦ 𝓟 (Ici a)) }
⊢ Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n y) atTop (𝓝 (∑' (n : α), f n y))

Tactic:
apply Summable.hasSum

Premises used: Summable.hasSum
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
hx : x ∈ s
y : E
hy : y ∈ s
⊢ Summable.{u_5, u_1} (α := F) (fun (b : α) ↦ f b y) { filter := sInf (range fun (a : Finset α) ↦ 𝓟 (Ici a)) }

Tactic:
summable_of_summable_hasFDerivAt_of_isPreconnected hu hs h's hf hf' hx₀ hf0 hy

Premises used: iInf, Filter.atTop, summable_of_summable_hasFDerivAt_of_isPreconnected, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
hx : x ∈ s
y : E
hy : y ∈ s
⊢ Summable.{u_5, u_1} (α := F) (fun (b : α) ↦ f b y) { filter := sInf (range fun (a : Finset α) ↦ 𝓟 (Ici a)) }

Tactic:
exact summable_of_summable_hasFDerivAt_of_isPreconnected hu hs h's hf hf' hx₀ hf0 hy

Premises used: summable_of_summable_hasFDerivAt_of_isPreconnected
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
hx : x ∈ s
⊢ ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))

Tactic:
have A :
      ∀ x : E, x ∈ s → Tendsto (fun t : Finset α => ∑ n ∈ t, f n x) atTop (𝓝 (∑' n, f n x)) := by
      intro y hy
      apply Summable.hasSum
      exact summable_of_summable_hasFDerivAt_of_isPreconnected hu hs h's hf hf' hx₀ hf0 hy
-- Module: Mathlib.Analysis.Calculus.SmoothSeries
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
u : α → ℝ
inst_6 : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x₀
hx : x ∈ s
A : ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))
⊢ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑' (n : α), f n y) (∑' (n : α), f' n x) x

Tactic:
hasFDerivAt_of_tendstoUniformlyOn hs (tendstoUniformlyOn_tsum hu hf')
      (fun t y hy => ?_) A hx

Premises used: tendstoUniformlyOn_tsum, hasFDerivAt_of_tendstoUniformlyOn