-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem _root_.IsOpen.exists_iUnion_isClosed {U : Set α} (hU : IsOpen U) :
    ∃ F : ℕ → Set α, (∀ n, IsClosed (F n)) ∧ (∀ n, F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F

Proof state:
case intro.intro.refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEdist x Uᶜ = 0
B : 0 < infEdist x Uᶜ
⊢ x ∈ ⋃ n, F n

Tactic:
have : Filter.Tendsto (fun n => a ^ n) atTop (𝓝 0) :=
  ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one a_lt_one

Result:
case intro.intro.refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEdist x Uᶜ = 0
B : 0 < infEdist x Uᶜ
this : Tendsto (fun n => a ^ n) atTop (𝓝 0)
⊢ x ∈ ⋃ n, F n

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F

Tactic:
let F := fun n : ℕ => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F

Tactic:
refine ⟨F, fun n => IsClosed.preimage continuous_infEdist isClosed_Ici, F_subset, ?_, ?_⟩

Result:
case intro.intro.refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ⋃ n, F n = U

case intro.intro.refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ Monotone F

Proof state:
case intro.intro.refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEdist x Uᶜ = 0
⊢ x ∈ ⋃ n, F n

Tactic:
have B : 0 < infEdist x Uᶜ := by simpa [pos_iff_ne_zero] using this

Result:
case intro.intro.refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEdist x Uᶜ = 0
B : 0 < infEdist x Uᶜ
⊢ x ∈ ⋃ n, F n

Proof state:
case intro.intro.refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEdist x Uᶜ = 0
B : 0 < infEdist x Uᶜ
this : Tendsto (fun n => a ^ n) atTop (𝓝 0)
⊢ x ∈ ⋃ n, F n

Tactic:
rcases ((tendsto_order.1 this).2 _ B).exists with ⟨n, hn⟩

Result:
case intro.intro.refine_1.intro
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this✝ : ¬infEdist x Uᶜ = 0
B : 0 < infEdist x Uᶜ
this : Tendsto (fun n => a ^ n) atTop (𝓝 0)
n : ℕ
hn : a ^ n < infEdist x Uᶜ
⊢ x ∈ ⋃ n, F n

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F

Tactic:
obtain ⟨a, a_pos, a_lt_one⟩ : ∃ a : ℝ≥0∞, 0 < a ∧ a < 1 := exists_between zero_lt_one

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
⊢ ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
h : x ∉ U
this : infEdist x Uᶜ ≠ 0
⊢ False

Tactic:
exact this (infEdist_zero_of_mem h)

Result:
no goals