awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L
have e2 : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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)
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L
have 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
Tactic: obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_isMaxOn e1 e2
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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)
⊢ ‖cderiv r f z‖ < M / r
have obtain : ∀ (L : ℝ) (hL1 : L < M) (hL2 : ∀ w ∈ sphere z r, ‖f w‖ ≤ L), ‖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'⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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)
⊢ TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
have inl : ∀ (hF : TendstoUniformlyOn F f ⊥ (cthickening δ K)) (hFn : ∀ᶠ (n : ι) in ⊥, ContinuousOn (F n) (cthickening δ K)),
  TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) ⊥ K
Tactic: rcases φ.eq_or_neBot with rfl | hne
Cleared hypotheses: φ, hF, hFn
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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
⊢ TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
have inr : ∀ (hne : φ.NeBot), TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
Tactic: rcases φ.eq_or_neBot with rfl | hne
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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
⊢ TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
have e1 : ContinuousOn f (cthickening δ K)
Tactic: have e1 : ContinuousOn f (cthickening δ K) := TendstoUniformlyOn.continuousOn hF hFn.frequently
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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)
⊢ TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
have 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) < ε
Tactic: rw [tendstoUniformlyOn_iff] at hF ⊢
Cleared hypotheses: hF, hδ, hFn, hne, e1
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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 : ι) in φ, ∀ x ∈ K, dist (Complex.cderiv δ f x) ((Complex.cderiv δ ∘ F) n x) < ε
have 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) < ε
Tactic: filter_upwards [hF (ε * δ) (mul_pos hε hδ), hFn] with n h h' z hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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
⊢ dist (Complex.cderiv δ f z) ((Complex.cderiv δ ∘ F) n z) < ε
have h₁ : ∀ (h : ∀ x ∈ cthickening δ K, ‖f x - F n x‖ < ε * δ), ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
Tactic: simp_rw [dist_eq_norm] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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‖ < ε * δ
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
have e2 : ∀ 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))
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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‖ < ε * δ
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
have e3 : sphere z δ ⊆ cthickening δ K
Tactic: have e3 := sphere_subset_closedBall.trans (closedBall_subset_cthickening hz δ)
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
have hf : ContinuousOn f (sphere z δ)
Tactic: have hf : ContinuousOn f (sphere z δ) :=
    e1.mono (sphere_subset_closedBall.trans (closedBall_subset_cthickening hz δ))
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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)
have 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
Tactic: filter_upwards [hF] with n h using h.continuousOn.mono hKU
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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
⊢ ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
have h₁ : ∀ (a : ι), DifferentiableOn ℂ (F a) U → ContinuousOn (F a) (cthickening δ K)
Tactic: filter_upwards [hF] with n h using h.continuousOn.mono hKU
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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
⊢ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
have h1 : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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)
⊢ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
have h2 : IsCompact (cthickening δ K)
Tactic: have h2 : IsCompact (cthickening δ K) := hK.cthickening
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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 (deriv ∘ F) (cderiv δ f) φ K
have h3 : TendstoUniformlyOn F f φ (cthickening δ K)
Tactic: have h3 : TendstoUniformlyOn F f φ (cthickening δ K) :=
    (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).mp hf (cthickening δ K) hKU h2
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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)
⊢ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
have apply : ∀ᶠ (n : ι) in φ, EqOn ((cderiv δ ∘ F) n) ((deriv ∘ F) n) K
Tactic: apply (h3.cderiv hδ h1).congr
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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 : ι) in φ, EqOn ((cderiv δ ∘ F) n) ((deriv ∘ F) n) K
have h : ∀ (n : ι) (h : DifferentiableOn ℂ (F n) U) ⦃z : ℂ⦄ (hz : z ∈ K), (cderiv δ ∘ F) n z = (deriv ∘ F) n z
Tactic: filter_upwards [hF] with n h z hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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
⊢ ∃ δ > 0, cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
have obtain : ∀ (δ : ℝ) (hδ : 0 < δ) (hKδ : cthickening δ K ⊆ U),
  ∃ δ > 0, cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
Tactic: obtain ⟨δ, hδ, hKδ⟩ := hK.exists_cthickening_subset_open hU hKU
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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
⊢ DifferentiableWithinAt ℂ f U x
have obtain : ∀ (K : Set ℂ) (hKU : K ⊆ U) (hKx : K ∈ 𝓝 x) (hK : IsCompact K), DifferentiableWithinAt ℂ f U x
Tactic: obtain ⟨K, ⟨hKx, hK⟩, hKU⟩ := (compact_basis_nhds x).mem_iff.mp (hU.mem_nhds hx)
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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
⊢ DifferentiableWithinAt ℂ f U x
have obtain : ∀ δ > 0, cthickening δ K ⊆ U → ∀ (h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K), DifferentiableWithinAt ℂ f U x
Tactic: obtain ⟨δ, _, _, h1⟩ := exists_cthickening_tendstoUniformlyOn hf hF hK hU hKU
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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
⊢ DifferentiableWithinAt ℂ f U x
have h2 : interior K ⊆ U
Tactic: have h2 : interior K ⊆ U := interior_subset.trans hKU
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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)
have 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
Tactic: filter_upwards [hF] with n h using h.mono h2
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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
⊢ ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
have h₁ : ∀ (a : ι), DifferentiableOn ℂ (F a) U → DifferentiableOn ℂ (F a) (interior K)
Tactic: filter_upwards [hF] with n h using h.mono h2
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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
⊢ DifferentiableWithinAt ℂ f U x
have h3 : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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)
⊢ DifferentiableWithinAt ℂ f U x
have h4 : TendstoLocallyUniformlyOn F f φ (interior K)
Tactic: have h4 : TendstoLocallyUniformlyOn F f φ (interior K) := hf.mono h2
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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)
⊢ DifferentiableWithinAt ℂ f U x
have h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K)
Tactic: have h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K) :=
    h1.tendstoLocallyUniformlyOn.mono interior_subset
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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)
⊢ DifferentiableWithinAt ℂ f U x
have h6 : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
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
⊢ DifferentiableWithinAt ℂ f U x
have h7 : DifferentiableOn ℂ f (interior K)
Tactic: have h7 : DifferentiableOn ℂ f (interior K) := fun x hx =>
    (h6 x hx).differentiableAt.differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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
⊢ TendstoLocallyUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ U
have rw : ∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
Tactic: rw [tendstoLocallyUniformlyOn_iff_forall_isCompact hU]
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
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
⊢ ∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
have 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
Tactic: rcases φ.eq_or_neBot with rfl | hne
Cleared hypotheses: φ, hf, hF