awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : (sphere z r).Nonempty
⊢ ContinuousOn (Y := ℝ) (fun (w : ℂ) ↦ ‖f w‖) (sphere z r)

Tactic:
have e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r) := continuous_norm.comp_continuousOn hf
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : (sphere z r).Nonempty
e2 : ContinuousOn (Y := ℝ) (fun (w : ℂ) ↦ ‖f w‖) (sphere z r)
obtain :
  ∀ (x : ℂ) (hx : x ∈ sphere z r) (hx' : IsMaxOn (β := ℝ) (fun (w : ℂ) ↦ ‖f w‖) (sphere z r) x),
    ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L

Tactic:
obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_isMaxOn e1 e2

Premises used: isCompact_sphere, IsCompact.exists_isMaxOn
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : (sphere z r).Nonempty
e2 : ContinuousOn (Y := ℝ) (fun (w : ℂ) ↦ ‖f w‖) (sphere z r)
x : ℂ
hx : x ∈ sphere z r
hx' : IsMaxOn (β := ℝ) (fun (w : ℂ) ↦ ‖f w‖) (sphere z r) x
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L

Tactic:
⟨‖f x‖, hfM x hx, hx'⟩

Premises used: Norm.norm, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : (sphere z r).Nonempty
e2 : ContinuousOn (Y := ℝ) (fun (w : ℂ) ↦ ‖f w‖) (sphere z r)
x : ℂ
hx : x ∈ sphere z r
hx' : IsMaxOn (β := ℝ) (fun (w : ℂ) ↦ ‖f w‖) (sphere z r) x
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L

Tactic:
exact ⟨‖f x‖, hfM x hx, hx'⟩
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
obtain : ∀ (L : ℝ) (hL1 : L < M) (hL2 : ∀ w ∈ sphere z r, ‖f w‖ ≤ L), ‖cderiv r f z‖ < M / r
⊢ ‖cderiv r f z‖ < M / r

Tactic:
obtain ⟨L, hL1, hL2⟩ : ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L := by
    have e1 : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
    have e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r) := continuous_norm.comp_continuousOn hf
    obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_isMaxOn e1 e2
    exact ⟨‖f x‖, hfM x hx, hx'⟩

Premises used: Metric.sphere
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
L : ℝ
hL1 : L < M
hL2 : ∀ w ∈ sphere z r, ‖f w‖ ≤ L
⊢ ‖cderiv r f z‖ < M / r

Tactic:
(norm_cderiv_le hr hL2).trans_lt ((div_lt_div_iff_of_pos_right hr).mpr hL1)

Premises used: Iff.mpr, div_lt_div_iff_of_pos_right, Complex.norm_cderiv_le, LE.le.trans_lt
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
L : ℝ
hL1 : L < M
hL2 : ∀ w ∈ sphere z r, ‖f w‖ ≤ L
⊢ ‖cderiv r f z‖ < M / r

Tactic:
exact (norm_cderiv_le hr hL2).trans_lt ((div_lt_div_iff_of_pos_right hr).mpr hL1)

Premises used: Iff.mpr, div_lt_div_iff_of_pos_right, Complex.norm_cderiv_le, LE.le.trans_lt
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f g : ℂ → E
hr : 0 < r
hfg : ∀ w ∈ sphere z r, ‖f w - g w‖ < M
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
⊢ ‖cderiv r f z - cderiv r g z‖ < M / r

Tactic:
cderiv_sub hr hf hg ▸ norm_cderiv_lt hr hfg (hf.sub hg)

Premises used: ContinuousOn.sub, Eq.rec, Complex.cderiv_sub, Complex.norm_cderiv_lt
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : TendstoUniformlyOn F f φ (cthickening δ K)
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
inl :
  ∀ (hF : TendstoUniformlyOn F f ⊥ (cthickening δ K)) (hFn : ∀ᶠ (n : ι) in ⊥, ContinuousOn (F n) (cthickening δ K)),
    TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) ⊥ K
inr : ∀ (hne : φ.NeBot), TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
⊢ TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ 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
K : Set ℂ
δ : ℝ
F : ι → ℂ → E
f : ℂ → E
hδ : 0 < δ
hF : TendstoUniformlyOn F f ⊥ (cthickening δ K)
hFn : ∀ᶠ (n : ι) in ⊥, ContinuousOn (F n) (cthickening δ K)
⊢ TendstoUniformlyOn (cderiv δ ∘ F) (cderiv δ 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
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : TendstoUniformlyOn F f φ (cthickening δ K)
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
⊢ ContinuousOn f (cthickening δ K)

Tactic:
have e1 : ContinuousOn f (cthickening δ K) := TendstoUniformlyOn.continuousOn hF hFn.frequently
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : TendstoUniformlyOn F f φ (cthickening δ K)
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
inr :
  ∀ (hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε) (hδ : 0 < δ)
    (hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)) (hne : φ.NeBot)
    (e1 : ContinuousOn f (cthickening δ K)),
    ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ K, dist (Complex.cderiv δ f x) ((Complex.cderiv δ ∘ F) n x) < ε
⊢ TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K

Tactic:
rw [tendstoUniformlyOn_iff] at hF ⊢

Premises used: Metric.tendstoUniformlyOn_iff
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
h :
  ∀ (n : ι) (h : ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε * δ) (h' : ContinuousOn (F n) (cthickening δ K)) (z : ℂ)
    (hz : z ∈ K), dist (Complex.cderiv δ f z) ((Complex.cderiv δ ∘ F) n z) < ε
⊢ ∀ᶠ (n : ι) in φ, ∀ x ∈ K, dist (Complex.cderiv δ f x) ((Complex.cderiv δ ∘ F) n x) < ε

Tactic:
filter_upwards [hF (ε * δ) (mul_pos hε hδ), hFn] with n h h' z hz

Premises used: HMul.hMul, mul_pos
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h : ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε * δ
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h₁ : ∀ (h : ∀ x ∈ cthickening δ K, ‖f x - F n x‖ < ε * δ), ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
⊢ dist (Complex.cderiv δ f z) ((Complex.cderiv δ ∘ F) n z) < ε

Tactic:
simp_rw [dist_eq_norm] at h ⊢

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ x ∈ cthickening δ K, ‖f x - F n x‖ < ε * δ
⊢ ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ

Tactic:
have e2 : ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ := fun w hw1 =>
    h w (closedBall_subset_cthickening hz δ (sphere_subset_closedBall hw1))
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ x ∈ cthickening δ K, ‖f x - F n x‖ < ε * δ
e2 : ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ
⊢ sphere z δ ⊆ cthickening δ K

Tactic:
have e3 := sphere_subset_closedBall.trans (closedBall_subset_cthickening hz δ)
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ x ∈ cthickening δ K, ‖f x - F n x‖ < ε * δ
e2 : ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ
e3 : sphere z δ ⊆ cthickening δ K
⊢ ContinuousOn f (sphere z δ)

Tactic:
have hf : ContinuousOn f (sphere z δ) :=
    e1.mono (sphere_subset_closedBall.trans (closedBall_subset_cthickening hz δ))
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
K : Set ℂ
δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : φ.NeBot
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ x ∈ cthickening δ K, ‖f x - F n x‖ < ε * δ
e2 : ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ
e3 : sphere z δ ⊆ cthickening δ K
hf : ContinuousOn f (sphere z δ)
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε

Tactic:
simpa only [mul_div_cancel_right₀ _ hδ.ne.symm] using norm_cderiv_sub_lt hδ e2 hf (h'.mono e3)

Premises used: Ne.symm, mul_div_cancel_right₀, Complex.norm_cderiv_sub_lt, ContinuousOn.mono, LT.lt.ne
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
n : ι
h : DifferentiableOn ℂ (F n) U
⊢ ContinuousOn (F n) (cthickening δ K)

Tactic:
h.continuousOn.mono hKU

Premises used: DifferentiableOn.continuousOn, ContinuousOn.mono
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ DifferentiableOn ℂ (F n) U) x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ ContinuousOn (F n) (cthickening δ K)) x} x}
      a
h₁ h₂ : ∀ (n : ι) (h : DifferentiableOn ℂ (F n) U), ContinuousOn (F n) (cthickening δ K)
⊢ ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)

Tactic:
filter_upwards [hF] with n h using h.continuousOn.mono hKU
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
⊢ ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)

Tactic:
have h1 : ∀ᶠ n in φ, ContinuousOn (F n) (cthickening δ K) := by
    filter_upwards [hF] with n h using h.continuousOn.mono hKU
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
⊢ IsCompact (cthickening δ K)

Tactic:
have h2 : IsCompact (cthickening δ K) := hK.cthickening
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
h2 : IsCompact (cthickening δ K)
⊢ TendstoUniformlyOn F f φ (cthickening δ K)

Tactic:
have h3 : TendstoUniformlyOn F f φ (cthickening δ K) :=
    (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).mp hf (cthickening δ K) hKU h2
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
h2 : IsCompact (cthickening δ K)
h3 : TendstoUniformlyOn F f φ (cthickening δ K)
apply : ∀ᶠ (n : ι) in φ, EqOn ((cderiv δ ∘ F) n) ((deriv ∘ F) n) K
⊢ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K

Tactic:
apply (h3.cderiv hδ h1).congr

Premises used: TendstoUniformlyOn.congr, TendstoUniformlyOn.cderiv
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
h2 : IsCompact (cthickening δ K)
h3 : TendstoUniformlyOn F f φ (cthickening δ K)
h : ∀ (n : ι) (h : DifferentiableOn ℂ (F n) U) ⦃z : ℂ⦄ (hz : z ∈ K), (cderiv δ ∘ F) n z = (deriv ∘ F) n z
⊢ ∀ᶠ (n : ι) in φ, EqOn ((cderiv δ ∘ F) n) ((deriv ∘ F) n) K

Tactic:
filter_upwards [hF] with n h z hz
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
h2 : IsCompact (cthickening δ K)
h3 : TendstoUniformlyOn F f φ (cthickening δ K)
n : ι
h : DifferentiableOn ℂ (F n) U
z : ℂ
hz : z ∈ K
⊢ (cderiv δ ∘ F) n z = (deriv ∘ F) n z

Tactic:
cderiv_eq_deriv hU h hδ ((closedBall_subset_cthickening hz δ).trans hKU)

Premises used: Complex.cderiv_eq_deriv, deriv, Complex.cderiv, 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 K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
h2 : IsCompact (cthickening δ K)
h3 : TendstoUniformlyOn F f φ (cthickening δ K)
n : ι
h : DifferentiableOn ℂ (F n) U
z : ℂ
hz : z ∈ K
⊢ (cderiv δ ∘ F) n z = (deriv ∘ F) n z

Tactic:
exact cderiv_eq_deriv hU h hδ ((closedBall_subset_cthickening hz δ).trans hKU)

Premises used: Complex.cderiv_eq_deriv, 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 K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
obtain :
  ∀ (δ : ℝ) (hδ : 0 < δ) (hKδ : cthickening δ K ⊆ U),
    ∃ δ > 0, cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
⊢ ∃ δ > 0, cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K

Tactic:
obtain ⟨δ, hδ, hKδ⟩ := hK.exists_cthickening_subset_open hU hKU

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

Tactic:
⟨δ, hδ, hKδ, tendstoUniformlyOn_deriv_of_cthickening_subset hf hF hδ hK hU hKδ⟩

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

Tactic:
exact ⟨δ, hδ, hKδ, tendstoUniformlyOn_deriv_of_cthickening_subset hf hF hδ hK hU hKδ⟩
-- 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
obtain : ∀ (K : Set ℂ) (hKU : K ⊆ U) (hKx : K ∈ 𝓝 x) (hK : IsCompact K), DifferentiableWithinAt ℂ f U x
⊢ DifferentiableWithinAt ℂ f U x

Tactic:
obtain ⟨K, ⟨hKx, hK⟩, hKU⟩ := (compact_basis_nhds x).mem_iff.mp (hU.mem_nhds hx)

Premises used: Filter.HasBasis.mem_iff, compact_basis_nhds, IsOpen.mem_nhds, Iff.mp
-- 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
obtain :
  ∀ δ > 0,
    cthickening δ K ⊆ U → ∀ (h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K), DifferentiableWithinAt ℂ f U x
⊢ DifferentiableWithinAt ℂ f U x

Tactic:
obtain ⟨δ, _, _, h1⟩ := 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
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
⊢ interior K ⊆ U

Tactic:
have h2 : interior K ⊆ U := interior_subset.trans hKU
-- 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
n : ι
h : DifferentiableOn ℂ (F n) U
⊢ DifferentiableOn ℂ (F n) (interior K)

Tactic:
h.mono h2

Premises used: DifferentiableOn.mono
-- 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
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ DifferentiableOn ℂ (F n) U) x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ DifferentiableOn ℂ (F n) (interior K)) x} x}
      a
h₁ h₂ : ∀ (n : ι) (h : DifferentiableOn ℂ (F n) U), DifferentiableOn ℂ (F n) (interior K)
⊢ ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)

Tactic:
filter_upwards [hF] with n h using h.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
⊢ ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)

Tactic:
have h3 : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) (interior K) := by
    filter_upwards [hF] with n h using h.mono h2