Theorem: montel (RMT4/Montel.lean)

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
h1 : UniformlyBoundedOn F U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
⊢ TotallyBounded (range F)
Tactic:
choose! Q hQ1 hQ2 using h1
State after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
⊢ TotallyBounded (range F)

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
⊢ TotallyBounded (range F)
Tactic:
have l1 : range F ⊆ 𝓑 U Q := by rintro f ⟨i, rfl⟩ ; exact ⟨h2 i, fun K hK => hQ2 K hK i⟩
State after:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
l1 : range F ⊆ 𝓑 U Q
⊢ TotallyBounded (range F)

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
l1 : range F ⊆ 𝓑 U Q
⊢ TotallyBounded (range F)
Tactic:
exact totallyBounded_subset l1 <| (isCompact_𝓑 hU hQ1).totallyBounded
State after:
no goals

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
⊢ range F ⊆ 𝓑 U Q
Tactic:
rintro f ⟨i, rfl⟩
State after:
case intro
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
i : ι
⊢ F i ∈ 𝓑 U Q

State before:
case intro
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
i : ι
⊢ F i ∈ 𝓑 U Q
Tactic:
exact ⟨h2 i, fun K hK => hQ2 K hK i⟩
State after:
no goals