-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem Metric.uniformity_edist_aux {α} (d : α → α → ℝ≥0) :
    ⨅ ε > (0 : ℝ), 𝓟 { p : α × α | ↑(d p.1 p.2) < ε } =
      ⨅ ε > (0 : ℝ≥0∞), 𝓟 { p : α × α | ↑(d p.1 p.2) < ε }

Proof state:
case refine_2.intro
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0
hε : ↑ε > 0
⊢ {p | ↑(d p.1 p.2) < ↑ε} ∈ 𝓟 {p | ↑(d p.1 p.2) < ↑ε}

Tactic:
exact fun _ => ENNReal.coe_lt_coe.1

Result:
no goals

Proof state:
case refine_1.intro.intro
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ {p | ↑(d p.1 p.2) < ε} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

Tactic:
refine mem_iInf_of_mem (ε' : ℝ) (mem_iInf_of_mem (ENNReal.coe_pos.1 ε'0) ?_)

Result:
case refine_1.intro.intro
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ {p | ↑(d p.1 p.2) < ε} ∈ 𝓟 {p | ↑(d p.1 p.2) < ↑ε'}

Proof state:
case refine_2.intro
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0
hε : ↑ε > 0
⊢ {p | ↑(d p.1 p.2) < ↑ε} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

Tactic:
refine mem_iInf_of_mem (ε : ℝ≥0∞) (mem_iInf_of_mem (ENNReal.coe_pos.2 hε) ?_)

Result:
case refine_2.intro
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0
hε : ↑ε > 0
⊢ {p | ↑(d p.1 p.2) < ↑ε} ∈ 𝓟 {p | ↑(d p.1 p.2) < ↑ε}

Proof state:
case refine_1
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
⊢ {p | ↑(d p.1 p.2) < ε} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hε with ⟨ε', ε'0, ε'ε⟩

Result:
case refine_1.intro.intro
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ {p | ↑(d p.1 p.2) < ε} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

Proof state:
α : Type u_3
d : α → α → ℝ≥0
⊢ (∀ i > 0, {p | ↑(d p.1 p.2) < i} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}) ∧
    ∀ i > 0, {p | ↑(d p.1 p.2) < i} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

Tactic:
refine ⟨fun ε hε => ?_, fun ε hε => ?_⟩

Result:
case refine_1
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
⊢ {p | ↑(d p.1 p.2) < ε} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

case refine_2
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ
hε : ε > 0
⊢ {p | ↑(d p.1 p.2) < ε} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

Proof state:
case refine_2
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ
hε : ε > 0
⊢ {p | ↑(d p.1 p.2) < ε} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

Tactic:
lift ε to ℝ≥0 using le_of_lt hε

Result:
case refine_2.intro
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0
hε : ↑ε > 0
⊢ {p | ↑(d p.1 p.2) < ↑ε} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

Proof state:
case refine_1.intro.intro
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ {p | ↑(d p.1 p.2) < ε} ∈ 𝓟 {p | ↑(d p.1 p.2) < ↑ε'}

Tactic:
exact fun x hx => lt_trans (ENNReal.coe_lt_coe.2 hx) ε'ε

Result:
no goals

Proof state:
α : Type u_3
d : α → α → ℝ≥0
⊢ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε} = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

Tactic:
simp only [le_antisymm_iff, le_iInf_iff, le_principal_iff]

Result:
α : Type u_3
d : α → α → ℝ≥0
⊢ (∀ i > 0, {p | ↑(d p.1 p.2) < i} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}) ∧
    ∀ i > 0, {p | ↑(d p.1 p.2) < i} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}