-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem cthickening_eq_iInter_cthickening' {δ : ℝ} (s : Set ℝ) (hsδ : s ⊆ Ioi δ)
    (hs : ∀ ε, δ < ε → (s ∩ Ioc δ ε).Nonempty) (E : Set α) :
    cthickening δ E = ⋂ ε ∈ s, cthickening ε E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E = ⋂ ε ∈ s, cthickening ε E

Tactic:
apply Subset.antisymm

Result:
case h₁
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E ⊆ ⋂ ε ∈ s, cthickening ε E

case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ ε ∈ s, cthickening ε E ⊆ cthickening δ E

Proof state:
case h₂.h.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ ENNReal.ofReal (δ + ↑η) ≤ ENNReal.ofReal δ + ENNReal.ofReal ↑η

Tactic:
exact ENNReal.ofReal_add_le

Result:
no goals

Proof state:
case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEdist x E ≤ ENNReal.ofReal i
⊢ infEdist x E ≤ ENNReal.ofReal δ

Tactic:
apply ENNReal.le_of_forall_pos_le_add

Result:
case h₂.h
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEdist x E ≤ ENNReal.ofReal i
⊢ ∀ (ε : ℝ≥0), 0 < ε → ENNReal.ofReal δ < ⊤ → infEdist x E ≤ ENNReal.ofReal δ + ↑ε

Proof state:
case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : x ∈ ⋂ ε ∈ s, {x | infEdist x E ≤ ENNReal.ofReal ε}
⊢ x ∈ {x | infEdist x E ≤ ENNReal.ofReal δ}

Tactic:
simp only [mem_iInter, mem_setOf_eq] at *

Result:
case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEdist x E ≤ ENNReal.ofReal i
⊢ infEdist x E ≤ ENNReal.ofReal δ

Proof state:
case h₂.h
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
⊢ infEdist x E ≤ ENNReal.ofReal δ + ↑η

Tactic:
rcases hs (δ + η) (lt_add_of_pos_right _ (NNReal.coe_pos.mpr η_pos)) with ⟨ε, ⟨hsε, hε⟩⟩

Result:
case h₂.h.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ infEdist x E ≤ ENNReal.ofReal δ + ↑η

Proof state:
case h₂.h
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEdist x E ≤ ENNReal.ofReal i
⊢ ∀ (ε : ℝ≥0), 0 < ε → ENNReal.ofReal δ < ⊤ → infEdist x E ≤ ENNReal.ofReal δ + ↑ε

Tactic:
intro η η_pos _

Result:
case h₂.h
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
⊢ infEdist x E ≤ ENNReal.ofReal δ + ↑η

Proof state:
case h₁
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E ⊆ ⋂ ε ∈ s, cthickening ε E

Tactic:
exact subset_iInter₂ fun _ hε => cthickening_mono (le_of_lt (hsδ hε)) E

Result:
no goals

Proof state:
case h₂.h.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ infEdist x E ≤ ENNReal.ofReal δ + ↑η

Tactic:
apply ((hx ε hsε).trans (ENNReal.ofReal_le_ofReal hε.2)).trans

Result:
case h₂.h.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ ENNReal.ofReal (δ + ↑η) ≤ ENNReal.ofReal δ + ↑η

Proof state:
case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ ε ∈ s, {x | infEdist x E ≤ ENNReal.ofReal ε} ⊆ {x | infEdist x E ≤ ENNReal.ofReal δ}

Tactic:
intro x hx

Result:
case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : x ∈ ⋂ ε ∈ s, {x | infEdist x E ≤ ENNReal.ofReal ε}
⊢ x ∈ {x | infEdist x E ≤ ENNReal.ofReal δ}

Proof state:
case h₂.h.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ ENNReal.ofReal (δ + ↑η) ≤ ENNReal.ofReal δ + ↑η

Tactic:
rw [ENNReal.coe_nnreal_eq η]

Result:
case h₂.h.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ i ∈ s, infEdist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
a✝ : ENNReal.ofReal δ < ⊤
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + ↑η)
⊢ ENNReal.ofReal (δ + ↑η) ≤ ENNReal.ofReal δ + ENNReal.ofReal ↑η

Proof state:
case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ ε ∈ s, cthickening ε E ⊆ cthickening δ E

Tactic:
unfold cthickening

Result:
case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ ε ∈ s, {x | infEdist x E ≤ ENNReal.ofReal ε} ⊆ {x | infEdist x E ≤ ENNReal.ofReal δ}