case refine'_1
ι : Sort ?u.141817
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
ε : ℝ
hε : ε ∈ s
⊢ cthickening δ E ⊆ thickening ε E

case refine'_2
ι : Sort ?u.141817
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ (⋂ (i : ℝ) (_ : i ∈ s), thickening i E) ⊆ cthickening δ E
ι : Sort ?u.141817
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ cthickening δ E = ⋂ (ε : ℝ) (_ : ε ∈ s), thickening ε E
refine' (subset_iInter₂ fun ε hε => _).antisymm _
case refine'_1.intro.intro
ι : Sort ?u.141817
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
ε : ℝ
hε : ε ∈ s
ε' : ℝ
hε' : ε' ∈ Ioc δ ε
⊢ cthickening δ E ⊆ thickening ε E
case refine'_1
ι : Sort ?u.141817
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
ε : ℝ
hε : ε ∈ s
⊢ cthickening δ E ⊆ thickening ε E
obtain ⟨ε', -, hε'⟩ := hs ε (hsδ hε)
case refine'_1.intro.intro
ι : Sort ?u.141817
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
ε : ℝ
hε : ε ∈ s
ε' : ℝ
hε' : ε' ∈ Ioc δ ε
ss : cthickening δ E ⊆ thickening ε' E
⊢ cthickening δ E ⊆ thickening ε E
case refine'_1.intro.intro
ι : Sort ?u.141817
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
ε : ℝ
hε : ε ∈ s
ε' : ℝ
hε' : ε' ∈ Ioc δ ε
⊢ cthickening δ E ⊆ thickening ε E
have ss := cthickening_subset_thickening' (lt_of_le_of_lt δ_nn hε'.1) hε'.1 E
no goals
case refine'_1.intro.intro
ι : Sort ?u.141817
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
ε : ℝ
hε : ε ∈ s
ε' : ℝ
hε' : ε' ∈ Ioc δ ε
ss : cthickening δ E ⊆ thickening ε' E
⊢ cthickening δ E ⊆ thickening ε E
exact ss.trans (thickening_mono hε'.2 E)
case refine'_2
ι : Sort ?u.141817
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ (⋂ (i : ℝ) (_ : i ∈ s), thickening i E) ⊆ ⋂ (ε : ℝ) (_ : ε ∈ s), cthickening ε E
case refine'_2
ι : Sort ?u.141817
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ (⋂ (i : ℝ) (_ : i ∈ s), thickening i E) ⊆ cthickening δ E
rw [cthickening_eq_iInter_cthickening' s hsδ hs E]
no goals
case refine'_2
ι : Sort ?u.141817
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s✝ t : Set α
x : α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → Set.Nonempty (s ∩ Ioc δ ε)
E : Set α
⊢ (⋂ (i : ℝ) (_ : i ∈ s), thickening i E) ⊆ ⋂ (ε : ℝ) (_ : ε ∈ s), cthickening ε E
exact iInter₂_mono fun ε _ => thickening_subset_cthickening ε E