-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem EMetric.mk_uniformity_basis_le {β : Type*} {p : β → Prop} {f : β → ℝ≥0∞}
    (hf₀ : ∀ x, p x → 0 < f x) (hf : ∀ ε, 0 < ε → ∃ x, p x ∧ f x ≤ ε) :
    (𝓤 α).HasBasis p fun x => { p : α × α | edist p.1 p.2 ≤ f x }

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun x => {p | edist p.1 p.2 ≤ f x}

Tactic:
refine ⟨fun s => uniformity_basis_edist.mem_iff.trans ?_⟩

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) ↔ ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.1 p.2 < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
i : β
hi : p i
H : f i ≤ ε'
⊢ ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s

Tactic:
exact ⟨i, hi, fun x hx => hε <| lt_of_le_of_lt (le_trans hx.out H) hε'.2⟩

Result:
no goals

Proof state:
case mpr
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s) → ∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s

Tactic:
exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x hx => H (le_of_lt hx.out)⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.1 p.2 < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
⊢ ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s

Tactic:
rcases hf ε' hε'.1 with ⟨i, hi, H⟩

Result:
case mp.intro.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.1 p.2 < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
i : β
hi : p i
H : f i ≤ ε'
⊢ ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s

Proof state:
case mp.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.1 p.2 < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s

Tactic:
rcases exists_between ε₀ with ⟨ε', hε'⟩

Result:
case mp.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.1 p.2 < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
⊢ ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) ↔ ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s

Tactic:
constructor

Result:
case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) → ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s

case mpr
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s) → ∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s

Proof state:
case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) → ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s

Tactic:
rintro ⟨ε, ε₀, hε⟩

Result:
case mp.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.1 p.2 < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s