-- Mathlib/Analysis/Complex/LocallyUniformLimit.lean
theorem tendstoUniformlyOn_deriv_of_cthickening_subset (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

Proof state:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : 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

Tactic:
have h2 : IsCompact (cthickening δ K) := hK.cthickening

Result:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : 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

Proof state:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : 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

Tactic:
have h1 : ∀ᶠ n in φ, ContinuousOn (F n) (cthickening δ K) := by
  filter_upwards [hF] with n h using h.continuousOn.mono hKU

Result:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : 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

Proof state:
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : 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)

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : 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

Tactic:
have h3 : TendstoUniformlyOn F f φ (cthickening δ K) :=
  (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).mp hf (cthickening δ K) hKU h2

Result:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : 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

Proof state:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : 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

Tactic:
filter_upwards [hF] with n h z hz

Result:
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : 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

Proof state:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : 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:
filter_upwards [hF] with n h using h.continuousOn.mono hKU

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : 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

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

Result:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U K : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝ : 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