α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
⊢ (∀ (i : ℝ≥0∞), i > 0 → {p | ↑(d p.fst p.snd) < i} ∈ ⨅ (ε : ℝ) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}) ∧
    ∀ (i : ℝ), i > 0 → {p | ↑(d p.fst p.snd) < i} ∈ ⨅ (ε : ℝ≥0∞) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
⊢ (⨅ (ε : ℝ) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}) = ⨅ (ε : ℝ≥0∞) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}
simp only [le_antisymm_iff, le_iInf_iff, le_principal_iff]
case refine_1
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
⊢ {p | ↑(d p.fst p.snd) < ε} ∈ ⨅ (ε : ℝ) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}

case refine_2
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
ε : ℝ
hε : ε > 0
⊢ {p | ↑(d p.fst p.snd) < ε} ∈ ⨅ (ε : ℝ≥0∞) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
⊢ (∀ (i : ℝ≥0∞), i > 0 → {p | ↑(d p.fst p.snd) < i} ∈ ⨅ (ε : ℝ) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}) ∧
    ∀ (i : ℝ), i > 0 → {p | ↑(d p.fst p.snd) < i} ∈ ⨅ (ε : ℝ≥0∞) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}
refine ⟨fun ε hε => ?_, fun ε hε => ?_⟩
case refine_1.intro.intro
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ {p | ↑(d p.fst p.snd) < ε} ∈ ⨅ (ε : ℝ) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}
case refine_1
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
⊢ {p | ↑(d p.fst p.snd) < ε} ∈ ⨅ (ε : ℝ) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hε with ⟨ε', ε'0, ε'ε⟩
case refine_1.intro.intro
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ {p | ↑(d p.fst p.snd) < ε} ∈ 𝓟 {p | ↑(d p.fst p.snd) < ↑ε'}
case refine_1.intro.intro
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ {p | ↑(d p.fst p.snd) < ε} ∈ ⨅ (ε : ℝ) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}
refine mem_iInf_of_mem (ε' : ℝ) (mem_iInf_of_mem (ENNReal.coe_pos.1 ε'0) ?_)
no goals
case refine_1.intro.intro
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ {p | ↑(d p.fst p.snd) < ε} ∈ 𝓟 {p | ↑(d p.fst p.snd) < ↑ε'}
exact fun x hx => lt_trans (ENNReal.coe_lt_coe.2 hx) ε'ε
case refine_2.intro
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
ε : ℝ≥0
hε : ↑ε > 0
⊢ {p | ↑(d p.fst p.snd) < ↑ε} ∈ ⨅ (ε : ℝ≥0∞) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}
case refine_2
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
ε : ℝ
hε : ε > 0
⊢ {p | ↑(d p.fst p.snd) < ε} ∈ ⨅ (ε : ℝ≥0∞) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}
lift ε to ℝ≥0 using le_of_lt hε
case refine_2.intro
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
ε : ℝ≥0
hε : ↑ε > 0
⊢ {p | ↑(d p.fst p.snd) < ↑ε} ∈ 𝓟 {p | ↑(d p.fst p.snd) < ↑ε}
case refine_2.intro
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
ε : ℝ≥0
hε : ↑ε > 0
⊢ {p | ↑(d p.fst p.snd) < ↑ε} ∈ ⨅ (ε : ℝ≥0∞) (_ : ε > 0), 𝓟 {p | ↑(d p.fst p.snd) < ε}
refine mem_iInf_of_mem (ε : ℝ≥0∞) (mem_iInf_of_mem (ENNReal.coe_pos.2 hε) ?_)
no goals
case refine_2.intro
α✝ : Type u
β : Type v
X : Type ?u.156823
ι : Type ?u.156826
inst✝ : PseudoMetricSpace α✝
α : Type u_1
d : α → α → ℝ≥0
ε : ℝ≥0
hε : ↑ε > 0
⊢ {p | ↑(d p.fst p.snd) < ↑ε} ∈ 𝓟 {p | ↑(d p.fst p.snd) < ↑ε}
exact fun _ => ENNReal.coe_lt_coe.1