awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
inst_3 : φ.NeBot
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left : δ > 0
left_1 : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
⊢ TendstoLocallyUniformlyOn F f φ (interior K)

Tactic:
have h4 : TendstoLocallyUniformlyOn F f φ (interior K) := hf.mono h2
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
inst_3 : φ.NeBot
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left : δ > 0
left_1 : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
⊢ TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K)

Tactic:
have h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K) :=
    h1.tendstoLocallyUniformlyOn.mono interior_subset
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
inst_3 : φ.NeBot
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left : δ > 0
left_1 : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K)
⊢ ∀ x ∈ interior K, HasDerivAt f (cderiv δ f x) x

Tactic:
have h6 : ∀ x ∈ interior K, HasDerivAt f (cderiv δ f x) x := fun x h =>
    hasDerivAt_of_tendsto_locally_uniformly_on' isOpen_interior h5 h3 (fun _ => h4.tendsto_at) h
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
inst_3 : φ.NeBot
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left : δ > 0
left_1 : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K)
h6 : ∀ x ∈ interior K, HasDerivAt f (cderiv δ f x) x
⊢ DifferentiableOn ℂ f (interior K)

Tactic:
have h7 : DifferentiableOn ℂ f (interior K) := fun x hx =>
    (h6 x hx).differentiableAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
inst_3 : φ.NeBot
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left : δ > 0
left_1 : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K)
h6 : ∀ x ∈ interior K, HasDerivAt f (cderiv δ f x) x
h7 : DifferentiableOn ℂ f (interior K)
⊢ DifferentiableWithinAt ℂ f U x

Tactic:
(h7.differentiableAt (interior_mem_nhds.mpr hKx)).differentiableWithinAt

Premises used: Iff.mpr, DifferentiableAt.differentiableWithinAt, DifferentiableOn.differentiableAt, interior_mem_nhds
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
inst_3 : φ.NeBot
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left : δ > 0
left_1 : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K)
h6 : ∀ x ∈ interior K, HasDerivAt f (cderiv δ f x) x
h7 : DifferentiableOn ℂ f (interior K)
⊢ DifferentiableWithinAt ℂ f U x

Tactic:
exact (h7.differentiableAt (interior_mem_nhds.mpr hKx)).differentiableWithinAt

Premises used: Iff.mpr, DifferentiableAt.differentiableWithinAt, DifferentiableOn.differentiableAt, interior_mem_nhds
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
rw : ∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
⊢ TendstoLocallyUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ U

Tactic:
rw [tendstoLocallyUniformlyOn_iff_forall_isCompact hU]

Premises used: tendstoLocallyUniformlyOn_iff_forall_isCompact
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
inl :
  ∀ (hf : TendstoLocallyUniformlyOn F f ⊥ U) (hF : ∀ᶠ (n : ι) in ⊥, DifferentiableOn ℂ (F n) U),
    ∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) ⊥ K
inr : ∀ (hne : φ.NeBot), ∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
⊢ ∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K

Tactic:
rcases φ.eq_or_neBot with rfl | hne

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hU : IsOpen U
hf : TendstoLocallyUniformlyOn F f ⊥ U
hF : ∀ᶠ (n : ι) in ⊥, DifferentiableOn ℂ (F n) U
⊢ ∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (deriv ∘ F) (deriv f) ⊥ K

Tactic:
simp only [TendstoUniformlyOn, eventually_bot, imp_true_iff]

Premises used: TendstoUniformlyOn, imp_true_iff, Filter.eventually_bot
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : φ.NeBot
K : Set ℂ
hKU : K ⊆ U
hK : IsCompact K
inr :
  ∀ (δ : ℝ) (hδ : δ > 0) (hK4 : cthickening δ K ⊆ U) (h : TendstoUniformlyOn (_root_.deriv ∘ F) (cderiv δ f) φ K),
    TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
⊢ TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K

Tactic:
obtain ⟨δ, hδ, hK4, h⟩ := exists_cthickening_tendstoUniformlyOn hf hF hK hU hKU

Premises used: Complex.exists_cthickening_tendstoUniformlyOn
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : φ.NeBot
K : Set ℂ
hKU : K ⊆ U
hK : IsCompact K
δ : ℝ
hδ : δ > 0
hK4 : cthickening δ K ⊆ U
h : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
⊢ TendstoUniformlyOn (deriv ∘ F) (deriv f) φ K

Tactic:
h.congr_right fun z hz => cderiv_eq_deriv hU (hf.differentiableOn hF hU) hδ ?_

Premises used: Complex.cderiv_eq_deriv, TendstoUniformlyOn.congr_right, TendstoLocallyUniformlyOn.differentiableOn
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : φ.NeBot
K : Set ℂ
hKU : K ⊆ U
hK : IsCompact K
δ : ℝ
hδ : δ > 0
hK4 : cthickening δ K ⊆ U
h : TendstoUniformlyOn (_root_.deriv ∘ F) (cderiv δ f) φ K
inr : ∀ (z : ℂ) (hz : z ∈ K), closedBall z δ ⊆ U
⊢ TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K

Tactic:
refine h.congr_right fun z hz => cderiv_eq_deriv hU (hf.differentiableOn hF hU) hδ ?_

Premises used: Complex.cderiv_eq_deriv, TendstoUniformlyOn.congr_right, TendstoLocallyUniformlyOn.differentiableOn
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : φ.NeBot
K : Set ℂ
hKU : K ⊆ U
hK : IsCompact K
δ : ℝ
hδ : δ > 0
hK4 : cthickening δ K ⊆ U
h : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
z : ℂ
hz : z ∈ K
⊢ closedBall z δ ⊆ U

Tactic:
(closedBall_subset_cthickening hz δ).trans hK4

Premises used: HasSubset.Subset.trans, Metric.closedBall_subset_cthickening
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : φ.NeBot
K : Set ℂ
hKU : K ⊆ U
hK : IsCompact K
δ : ℝ
hδ : δ > 0
hK4 : cthickening δ K ⊆ U
h : TendstoUniformlyOn (_root_.deriv ∘ F) (cderiv δ f) φ K
z : ℂ
hz : z ∈ K
⊢ closedBall z δ ⊆ U

Tactic:
exact (closedBall_subset_cthickening hz δ).trans hK4

Premises used: HasSubset.Subset.trans, Metric.closedBall_subset_cthickening
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
⊢ TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U

Tactic:
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hc :
  TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
⊢ DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (w : ℂ) ↦ ∑' (i : ι), F i w) U

Tactic:
hc.differentiableOn (Eventually.of_forall fun s => ?_) hU

Premises used: Filter.Eventually.of_forall, TendstoLocallyUniformlyOn.differentiableOn
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hc :
  TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
refine : ∀ (s : Finset ι), DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (x : ℂ) ↦ ∑ n ∈ s, F n x) U
⊢ DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (w : ℂ) ↦ ∑' (i : ι), F i w) U

Tactic:
refine hc.differentiableOn (Eventually.of_forall fun s => ?_) hU

Premises used: Filter.Eventually.of_forall, TendstoLocallyUniformlyOn.differentiableOn
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hc :
  TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
s : Finset ι
⊢ DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (x : ℂ) ↦ ∑ n ∈ s, F n x) U

Tactic:
DifferentiableOn.fun_sum fun i _ => hf i

Premises used: DifferentiableOn.fun_sum
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hc :
  TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
s : Finset ι
⊢ DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (x : ℂ) ↦ ∑ n ∈ s, F n x) U

Tactic:
exact DifferentiableOn.fun_sum fun i _ => hf i

Premises used: DifferentiableOn.fun_sum
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
have have₁ have₂ :
  ∀
    (hc :
      TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
        (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U),
    DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (w : ℂ) ↦ ∑' (i : ι), F i w) U
have₃ :
  ∀
    (hc :
      TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
        (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U)
    (s : Finset ι), DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (x : ℂ) ↦ ∑ n ∈ s, F n x) U
⊢ DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (w : ℂ) ↦ ∑' (i : ι), F i w) U

Tactic:
classical
  have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
  refine hc.differentiableOn (Eventually.of_forall fun s => ?_) hU
  exact DifferentiableOn.fun_sum fun i _ => hf i

Premises used: DifferentiableOn.fun_sum
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
z : ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hz : z ∈ U
⊢ TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U

Tactic:
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
z : ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hz : z ∈ U
hc :
  TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
⊢ Tendsto.{u_2, u_1} (β := E) (fun (i : Finset ι) ↦ (deriv ∘ fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x) i z) atTop
    (𝓝 (deriv (fun (x : ℂ) ↦ ∑' (n : ι), F n x) z))

Tactic:
(hc.deriv (Eventually.of_forall fun s => DifferentiableOn.fun_sum fun i _ => hf i)
          hU).tendsto_at
      hz

Premises used: Filter.Eventually.of_forall, TendstoLocallyUniformlyOn.deriv, DifferentiableOn.fun_sum, TendstoLocallyUniformlyOn.tendsto_at
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
z : ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hz : z ∈ U
hc :
  TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
h :
  Eq (α := Finset ι → E) (fun (s : Finset ι) ↦ ∑ b ∈ s, deriv (F b) z) fun (i : Finset ι) ↦
    (deriv ∘ fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x) i z
⊢ Tendsto.{u_2, u_1} (β := E) (fun (s : Finset ι) ↦ ∑ b ∈ s, deriv (F b) z) (SummationFilter.unconditional ι).filter
    (𝓝 (deriv (fun (w : ℂ) ↦ ∑' (i : ι), F i w) z))

Tactic:
convert!
    (hc.deriv (Eventually.of_forall fun s => DifferentiableOn.fun_sum fun i _ => hf i)
          hU).tendsto_at
      hz using 1

Premises used: Filter.Eventually.of_forall, TendstoLocallyUniformlyOn.deriv, DifferentiableOn.fun_sum, TendstoLocallyUniformlyOn.tendsto_at
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
z : ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hz : z ∈ U
hc :
  TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
h :
  ∀ (s : Finset ι),
    Eq.{u_1 + 1} (α := E) (∑ b ∈ s, deriv (F b) z : E) ((deriv ∘ fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x) s z : E)
⊢ Eq (α := Finset ι → E) (fun (s : Finset ι) ↦ ∑ b ∈ s, deriv (F b) z) fun (i : Finset ι) ↦
    (deriv ∘ fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x) i z

Tactic:
ext1 s
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
z : ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hz : z ∈ U
hc :
  TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
s : Finset ι
⊢ Eq.{u_1 + 1} (α := E) (∑ b ∈ s, deriv (F b) z : E) ((deriv ∘ fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x) s z : E)

Tactic:
(deriv_fun_sum fun i _ => (hf i).differentiableAt (hU.mem_nhds hz)).symm

Premises used: deriv_fun_sum, deriv, DifferentiableOn.differentiableAt, IsOpen.mem_nhds, Eq.symm
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
z : ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hz : z ∈ U
hc :
  TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
s : Finset ι
⊢ Eq.{u_1 + 1} (α := E) (∑ b ∈ s, deriv (F b) z : E) ((deriv ∘ fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x) s z : E)

Tactic:
exact (deriv_fun_sum fun i _ => (hf i).differentiableAt (hU.mem_nhds hz)).symm

Premises used: deriv_fun_sum, DifferentiableOn.differentiableAt, IsOpen.mem_nhds, Eq.symm
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
ι : Type u_3
p : Filter ι
f : ι → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
hs : IsOpen s
x : ℂ
hx : x ∈ s
hF : TendstoLocallyUniformlyOn f g p s
hf : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (f n) s
hg : g x ≠ 0
⊢ Tendsto (fun (n : ι) ↦ logDeriv (f n) x) p (𝓝 (logDeriv g x))

Tactic:
((hF.deriv hf hs).tendsto_at hx).div (hF.tendsto_at hx) hg

Premises used: logDeriv, deriv, Filter.Tendsto.div, TendstoLocallyUniformlyOn.deriv, TendstoLocallyUniformlyOn.tendsto_at
-- Module: Mathlib.Analysis.Complex.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
rw : circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = f w
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c R = f w

Tactic:
rw [← circleAverage_abs_radius]

Premises used: Real.circleAverage_abs_radius
-- Module: Mathlib.Analysis.Complex.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
inl : ∀ (hR : |R| ≤ 0), circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = f w
inr : ∀ (hR : 0 < |R|), circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = f w
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = f w

Tactic:
rcases le_or_gt |R| 0 with hR | hR

Premises used: abs, le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : |R| ≤ 0
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = f w

Tactic:
simp_all [ball_eq_empty.2 hR]

Premises used: Iff.mpr, Metric.ball_eq_empty
-- Module: Mathlib.Analysis.Complex.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
simp :
  Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, |R|), (z - c)⁻¹ • ((z - c) * (z - w)⁻¹) • f z)
    (∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z)
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) * (z - w)⁻¹) • f z) c |R| =
    HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z)

Tactic:
simp only [circleAverage_eq_circleIntegral hR.ne', mul_inv_rev, inv_I, neg_mul, neg_smul,
      neg_inj, ne_eq, mul_eq_zero, I_ne_zero, inv_eq_zero, ofReal_eq_zero, pi_ne_zero,
      OfNat.ofNat_ne_zero, or_self, not_false_eq_true, smul_right_inj]

Premises used: inv_eq_zero, Complex.inv_I, neg_smul, OfNat.ofNat_ne_zero, Real.circleAverage_eq_circleIntegral, Complex.I_ne_zero, mul_eq_zero, ne_eq, LT.lt.ne', Complex.ofReal_eq_zero, neg_inj, or_self, neg_mul, mul_inv_rev, not_false_eq_true, smul_right_inj, Real.pi_ne_zero
-- Module: Mathlib.Analysis.Complex.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
apply :
  EqOn.{0, u_1} (β := E) (fun (z : ℂ) ↦ (z - c)⁻¹ • ((z - c) * (z - w)⁻¹) • f z) (fun (z : ℂ) ↦ (z - w)⁻¹ • f z)
    (sphere c |R|)
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, |R|), (z - c)⁻¹ • ((z - c) * (z - w)⁻¹) • f z)
    (∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z)

Tactic:
apply circleIntegral.integral_congr hR.le

Premises used: circleIntegral.integral_congr, LT.lt.le