Theorem: UniformlyBoundedOn.equicontinuousOn (RMT4/Montel.lean)

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
⊢ EquicontinuousOn F K
Tactic:
apply (equicontinuous_restrict_iff _).mp
State after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
⊢ Equicontinuous (restrict K ∘ F)

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
⊢ Equicontinuous (restrict K ∘ F)
Tactic:
rintro ⟨z, hz⟩
State after:
case mk
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }

State before:
case mk
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }
Tactic:
obtain ⟨δ, hδ, h⟩ := nhds_basis_closedBall.mem_iff.1 (hU.mem_nhds (hK.1 hz))
State after:
case mk.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }

State before:
case mk.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }
Tactic:
have : ∃ M > 0, ∀ i, MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M) := by
  obtain ⟨Q, hQ1, hQ2⟩ := h1.deriv hU h2 (closedBall z δ) ⟨h, isCompact_closedBall _ _⟩
  obtain ⟨M, hM⟩ := hQ1.isBounded.subset_closedBall 0
  refine ⟨M ⊔ 1, by simp, fun i => ?_⟩
  exact ((hQ2 i).mono_right hM).mono_right <| closedBall_subset_closedBall le_sup_left
State after:
case mk.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
this : ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }

State before:
case mk.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
this : ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }
Tactic:
obtain ⟨M, hMp, hM⟩ := this
State after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }

State before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }
Tactic:
rw [equicontinuousAt_iff]
State after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ (x : ↑K),
        dist x { val := z, property := hz } < δ →
          ∀ (i : ι), dist ((restrict K ∘ F) i { val := z, property := hz }) ((restrict K ∘ F) i x) < ε

State before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ (x : ↑K),
        dist x { val := z, property := hz } < δ →
          ∀ (i : ι), dist ((restrict K ∘ F) i { val := z, property := hz }) ((restrict K ∘ F) i x) < ε
Tactic:
rintro ε hε
State after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0,
    ∀ (x : ↑K),
      dist x { val := z, property := hz } < δ →
        ∀ (i : ι), dist ((restrict K ∘ F) i { val := z, property := hz }) ((restrict K ∘ F) i x) < ε

State before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0,
    ∀ (x : ↑K),
      dist x { val := z, property := hz } < δ →
        ∀ (i : ι), dist ((restrict K ∘ F) i { val := z, property := hz }) ((restrict K ∘ F) i x) < ε
Tactic:
refine ⟨δ ⊓ ε / M, gt_iff_lt.2 (lt_inf_iff.2 ⟨hδ, div_pos hε hMp⟩), λ w hw i => ?_⟩
State after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
⊢ dist ((restrict K ∘ F) i { val := z, property := hz }) ((restrict K ∘ F) i w) < ε

State before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
⊢ dist ((restrict K ∘ F) i { val := z, property := hz }) ((restrict K ∘ F) i w) < ε
Tactic:
simp
State after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
⊢ dist (F i z) (F i ↑w) < ε

State before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
⊢ dist (F i z) (F i ↑w) < ε
Tactic:
have e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x :=
  λ x hx => (h2 i).differentiableAt (hU.mem_nhds (h hx))
State after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
⊢ dist (F i z) (F i ↑w) < ε

State before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
⊢ dist (F i z) (F i ↑w) < ε
Tactic:
have e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M := by simpa [MapsTo] using hM i
State after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
⊢ dist (F i z) (F i ↑w) < ε

State before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
⊢ dist (F i z) (F i ↑w) < ε
Tactic:
have e3 : z ∈ closedBall z δ := mem_closedBall_self hδ.le
State after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
⊢ dist (F i z) (F i ↑w) < ε

State before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
⊢ dist (F i z) (F i ↑w) < ε
Tactic:
have e4 : w.1 ∈ closedBall z δ := by simpa using (lt_inf_iff.1 hw).1.le
State after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ dist (F i z) (F i ↑w) < ε

State before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ dist (F i z) (F i ↑w) < ε
Tactic:
rw [dist_eq_norm]
State after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ ‖F i z - F i ↑w‖ < ε

State before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ ‖F i z - F i ↑w‖ < ε
Tactic:
refine ((convex_closedBall _ _).norm_image_sub_le_of_norm_deriv_le e1 e2 e4 e3).trans_lt ?_
State after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ M * ‖z - ↑w‖ < ε

State before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ M * ‖z - ↑w‖ < ε
Tactic:
have : ‖z - w.val‖ < ε / M := by
  have := (lt_inf_iff.1 hw).2
  rwa [dist_comm, Subtype.dist_eq, dist_eq_norm] at this
State after:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
this : ‖z - ↑w‖ < ε / M
⊢ M * ‖z - ↑w‖ < ε

State before:
case mk.intro.intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
this : ‖z - ↑w‖ < ε / M
⊢ M * ‖z - ↑w‖ < ε
Tactic:
convert mul_lt_mul' le_rfl this (norm_nonneg _) hMp
State after:
case h.e'_4
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
this : ‖z - ↑w‖ < ε / M
⊢ ε = M * (ε / M)

State before:
case h.e'_4
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
this : ‖z - ↑w‖ < ε / M
⊢ ε = M * (ε / M)
Tactic:
field_simp [hMp.lt.ne.symm, mul_comm]
State after:
no goals

State before:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
⊢ ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
Tactic:
obtain ⟨Q, hQ1, hQ2⟩ := h1.deriv hU h2 (closedBall z δ) ⟨h, isCompact_closedBall _ _⟩
State after:
case intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
⊢ ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)

State before:
case intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
⊢ ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
Tactic:
obtain ⟨M, hM⟩ := hQ1.isBounded.subset_closedBall 0
State after:
case intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
⊢ ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)

State before:
case intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
⊢ ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
Tactic:
refine ⟨M ⊔ 1, by simp, fun i => ?_⟩
State after:
case intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
⊢ MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 (M ⊔ 1))

State before:
case intro.intro.intro
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
⊢ MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 (M ⊔ 1))
Tactic:
exact ((hQ2 i).mono_right hM).mono_right <| closedBall_subset_closedBall le_sup_left
State after:
no goals

State before:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
⊢ M ⊔ 1 > 0
Tactic:
simp
State after:
no goals

State before:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
⊢ ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
Tactic:
simpa [MapsTo] using hM i
State after:
no goals

State before:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
⊢ ↑w ∈ closedBall z δ
Tactic:
simpa using (lt_inf_iff.1 hw).1.le
State after:
no goals

State before:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
⊢ ‖z - ↑w‖ < ε / M
Tactic:
have := (lt_inf_iff.1 hw).2
State after:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
this : dist w { val := z, property := hz } < ε / M
⊢ ‖z - ↑w‖ < ε / M

State before:
ι : Type u_1
U K : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
this : dist w { val := z, property := hz } < ε / M
⊢ ‖z - ↑w‖ < ε / M
Tactic:
rwa [dist_comm, Subtype.dist_eq, dist_eq_norm] at this
State after:
no goals