-- 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:
α : 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
⊢ x ∈ U

Tactic:
by_contra h

Result:
α : 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
⊢ False

Proof state:
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

Tactic:
intro m n hmn x hx

Result:
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
m n : ℕ
hmn : m ≤ n
x : α
hx : x ∈ F m
⊢ x ∈ F n

Proof state:
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ᶜ
⊢ ∃ i, x ∈ F i

Tactic:
exact ⟨n, hn.le⟩

Result:
no goals

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
⊢ x ∈ ⋃ n, F n

Tactic:
have : ¬x ∈ Uᶜ := by simpa using hx

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 : x ∉ Uᶜ
⊢ x ∈ ⋃ n, F n

Proof state:
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

Tactic:
simp only [mem_iUnion, mem_Ici, mem_preimage]

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ᶜ
⊢ ∃ i, x ∈ F i

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)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this : ¬infEdist x Uᶜ = 0
⊢ 0 < infEdist x Uᶜ

Tactic:
simpa [pos_iff_ne_zero] using this

Result:
no goals

Proof state:
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
m n : ℕ
hmn : m ≤ n
x : α
hx : a ^ m ≤ infEdist x Uᶜ
⊢ a ^ n ≤ infEdist x Uᶜ

Tactic:
apply le_trans (pow_le_pow_right_of_le_one' a_lt_one.le hmn) hx

Result:
no goals

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 : x ∉ Uᶜ
⊢ x ∈ ⋃ n, F n

Tactic:
rw [mem_iff_infEdist_zero_of_closed hU.isClosed_compl] at 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
⊢ 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
⊢ ⋃ n, F n = U

Tactic:
refine Subset.antisymm (by simp only [iUnion_subset_iff, F_subset, forall_const]) fun x hx => ?_

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
⊢ x ∈ ⋃ n, F n

Proof state:
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
m n : ℕ
hmn : m ≤ n
x : α
hx : x ∈ F m
⊢ x ∈ F n

Tactic:
simp only [F, mem_Ici, mem_preimage] at hx ⊢

Result:
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
m n : ℕ
hmn : m ≤ n
x : α
hx : a ^ m ≤ infEdist x Uᶜ
⊢ a ^ n ≤ infEdist x Uᶜ

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
⊢ False

Tactic:
have : infEdist x Uᶜ ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'

Result:
α : 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

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, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F

Tactic:
have F_subset : ∀ n, F n ⊆ U := fun n x hx ↦ by
  by_contra h
  have : infEdist x Uᶜ ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'
  exact this (infEdist_zero_of_mem h)

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_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ∃ 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)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ⋃ n, F n ⊆ U

Tactic:
simp only [iUnion_subset_iff, F_subset, forall_const]

Result:
no goals

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)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
⊢ x ∉ Uᶜ

Tactic:
simpa using hx

Result:
no goals