awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ι : Type u_3
inst_6 : Fintype ι
f : E → ι → ℝ
s : Set E
hf : LipschitzOnWith C f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
this : ∀ (i : ι), ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x i) s x
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
have h : ∀ (x : E) (hx : ∀ (i : ι), x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x i) s x) (xs : x ∈ s),
  DifferentiableWithinAt ℝ f s x
Tactic: filter_upwards [ae_all_iff.2 this] with x hx xs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
have have : ∀ (A : F ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ), ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
Tactic: have A := (Basis.ofVectorSpace ℝ F).equivFun.toContinuousLinearEquiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
have h : ∀ (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), DifferentiableWithinAt ℝ f s x
Tactic: filter_upwards [H] with x hx xs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
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
⊢ DifferentiableWithinAt ℝ f s x
have 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
Tactic: have : f = (A.symm ∘ A) ∘ f := by
      simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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 s x
have h : 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: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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) → ℝ
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
have 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
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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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) → ℝ
⊢ ∀ᵐ (x : E) ∂μ,
    x ∈ s →
      DifferentiableWithinAt ℝ (F := (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ)
        ((⇑A : (a : F) → (↑(Basis.ofVectorSpaceIndex ℝ F) : Type u_2) → ℝ) ∘ f) s x
have 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
Tactic: apply ae_differentiableWithinAt_of_mem_pi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
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) ∂μ.restrict s, DifferentiableWithinAt ℝ f s x
have rw : ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
Tactic: rw [ae_restrict_iff' hs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
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
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
have h₁ : LipschitzOnWith C f univ
Tactic: rw [← lipschitzOnWith_univ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
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
⊢ Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x
have haveI : ∀ (this : DecidableEq α), Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x
Tactic: haveI := Classical.decEq α
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
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 α
⊢ Summable.{u_5, u_1} (α := F) fun (n : α) ↦ f n x
have 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
Tactic: rw [summable_iff_cauchySeq_finset] at hf0 ⊢
Cleared hypotheses: hf0, hx, this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (hypothesis)
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 α
⊢ CauchySeq.{u_5, u_1} (α := F) fun (s : Finset α) ↦ ∑ b ∈ s, f b x
have A : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
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
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (hypothesis)
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
⊢ Summable.{u_5, u_1} (α := F) fun (n : α) ↦ g n y
have hg₁ : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
Tactic: simp_rw [hasDerivAt_iff_hasFDerivAt] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
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
have refine : ∀ (n : α), ∀ x ∈ t, norm (E := 𝕜 →L[𝕜] F) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n x)) ≤ u n
Tactic: refine summable_of_summable_hasFDerivAt_of_isPreconnected hu ht h't hg ?_ hy₀ hg0 hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
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
⊢ Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n y) atTop (𝓝 (∑' (n : α), f n y))
have ha : Summable.{u_5, u_1} (α := F) (fun (b : α) ↦ f b y) { filter := sInf (range fun (a : Finset α) ↦ 𝓟 (Ici a)) }
Tactic: apply Summable.hasSum
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (hypothesis)
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
⊢ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑' (n : α), f n y) (∑' (n : α), f' n x) x
have A : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
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
have refine : ∀ (t : Finset α) (y : E) (hy : y ∈ s),
  HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∑ n ∈ t, f n x) (∑ n ∈ t, f' n y) y
Tactic: refine hasFDerivAt_of_tendstoUniformlyOn hs (tendstoUniformlyOn_tsum hu hf')
      (fun t y hy => ?_) A hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
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
⊢ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑' (n : α), f n y) (∑' (n : α), f' n x) x
have have : ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))
Tactic: classical
    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
    refine hasFDerivAt_of_tendstoUniformlyOn hs (tendstoUniformlyOn_tsum hu hf')
      (fun t y hy => ?_) A hx
    exact HasFDerivAt.fun_sum fun n _ => hf n y hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
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
have : ∀ 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
have have₁ : ∀ (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: classical
    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
    refine hasFDerivAt_of_tendstoUniformlyOn hs (tendstoUniformlyOn_tsum hu hf')
      (fun t y hy => ?_) A hx
    exact HasFDerivAt.fun_sum fun n _ => hf n y hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (goal)
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
have : ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))
have₁ :
  ∀ (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
have₂ : ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))
have₃ have₄ :
  ∀ (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
⊢ HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑' (n : α), f n y) (∑' (n : α), f' n x) x
have have₅ : ∀ (A : ∀ x ∈ s, Tendsto.{u_1, u_5} (β := F) (fun (t : Finset α) ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x)))
  (t : Finset α) (y : E) (hy : y ∈ s),
  HasFDerivAt.{u_3, u_4, u_5} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∑ n ∈ t, f n x) (∑ n ∈ t, f' n y) y
Tactic: classical
    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
    refine hasFDerivAt_of_tendstoUniformlyOn hs (tendstoUniformlyOn_tsum hu hf')
      (fun t y hy => ?_) A hx
    exact HasFDerivAt.fun_sum fun n _ => hf n y hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.SmoothSeries (hypothesis)
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 (n : α) ↦ g n y₀
hy : y ∈ t
⊢ HasDerivAt.{u_3, u_5} (F := F) (fun (z : 𝕜) ↦ ∑' (n : α), g n z) (∑' (n : α), g' n y) y
have hg₁ : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (𝕜 := 𝕜) (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
Tactic: simp_rw [hasDerivAt_iff_hasFDerivAt] at hg ⊢
Cleared hypotheses: hg