awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
x y : X
refine : d x y = 0 ↔ ∀ (i : ℕ), True → (x, y) ∈ U i
⊢ d x y = 0 ↔ Inseparable x y

Tactic:
refine Iff.trans ?_ hB.inseparable_iff_uniformity.symm

Premises used: Filter.HasAntitoneBasis.toHasBasis, Iff.trans, Iff.symm, Filter.HasBasis.inseparable_iff_uniformity
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
x y : X
simp :
  Eq (α := ℝ≥0) (if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0) 0 ↔
    ∀ (i : ℕ), (x, y) ∈ U i
⊢ d x y = 0 ↔ ∀ (i : ℕ), True → (x, y) ∈ U i

Tactic:
simp only [d, true_imp_iff]

Premises used: true_imp_iff
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
x y : X
pos :
  ∀ (h : ∃ (n : ℕ), (x, y) ∉ U n), (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i
neg : ∀ (h : ¬∃ (n : ℕ), (x, y) ∉ U n), Eq (α := ℝ≥0) 0 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i
⊢ Eq (α := ℝ≥0) (if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0) 0 ↔
    ∀ (i : ℕ), (x, y) ∈ U i

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
x y : X
h : ∃ (n : ℕ), (x, y) ∉ U n
⊢ (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h = 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i

Tactic:
simp [h, pow_eq_zero_iff']

Premises used: pow_eq_zero_iff'
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
x y : X
h : ¬∃ (n : ℕ), (x, y) ∉ U n
⊢ Eq (α := ℝ≥0) 0 0 ↔ ∀ (i : ℕ), (x, y) ∈ U i

Tactic:
simpa only [not_exists, Classical.not_not, eq_self_iff_true, true_iff] using h

Premises used: Classical.not_not, true_iff, not_exists, eq_self_iff_true
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
⊢ ∀ {x y : X}, d x y = 0 ↔ Inseparable x y

Tactic:
have hd₀ : ∀ {x y}, d x y = 0 ↔ Inseparable x y := by
    intro x y
    refine Iff.trans ?_ hB.inseparable_iff_uniformity.symm
    simp only [d, true_imp_iff]
    split_ifs with h
    · simp [h, pow_eq_zero_iff']
    · simpa only [not_exists, Classical.not_not, eq_self_iff_true, true_iff] using h
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
x y : X
⊢ d x y = d y x

Tactic:
simp only [d, (U _).comm]

Premises used: SetRel.comm
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
⊢ ∀ (x y : X), d x y = d y x

Tactic:
have hd_symm x y : d x y = d y x := by simp only [d, (U _).comm]
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
⊢ Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)

Tactic:
have hr : (1 / 2 : ℝ≥0) ∈ Ioo (0 : ℝ≥0) 1 := ⟨half_pos one_pos, NNReal.half_lt_self one_ne_zero⟩
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
⊢ ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)

Tactic:
have hdist_le : ∀ x y, dist x y ≤ d x y := PseudoMetricSpace.dist_ofPreNNDist_le _ _ _
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
x y : X
n : ℕ
dsimp :
  ((1 / 2) ^ n ≤ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0) ↔
    (x, y) ∉ U n
⊢ (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n

Tactic:
dsimp only [d]
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
x y : X
n : ℕ
pos :
  ∀ (h : ∃ (n : ℕ), (x, y) ∉ U n), (1 / 2) ^ n ≤ (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h ↔ (x, y) ∉ U n
neg : ∀ (h : ¬∃ (n : ℕ), (x, y) ∉ U n), (1 / 2) ^ n ≤ 0 ↔ (x, y) ∉ U n
⊢ ((1 / 2) ^ n ≤ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0) ↔
    (x, y) ∉ U n

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
x y : X
n : ℕ
h : ∃ (n : ℕ), (x, y) ∉ U n
pos : (∃ m ≤ n, (x, y) ∉ U m) ↔ (x, y) ∉ U n
⊢ (1 / 2) ^ n ≤ (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h ↔ (x, y) ∉ U n

Tactic:
rw [(pow_right_strictAnti₀ hr.1 hr.2).le_iff_ge, Nat.find_le_iff]

Premises used: Nat.find_le_iff, pow_right_strictAnti₀, And.right, StrictAnti.le_iff_ge, And.left
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
x y : X
n : ℕ
h : ∃ (n : ℕ), (x, y) ∉ U n
⊢ (∃ m ≤ n, (x, y) ∉ U m) ↔ (x, y) ∉ U n

Tactic:
⟨fun ⟨m, hmn, hm⟩ hn => hm (hB.antitone hmn hn), fun h => ⟨n, le_rfl, h⟩⟩

Premises used: False, le_rfl, _private.0.UniformSpace.metrizable_uniformity.match_5, And.intro, Iff.intro, Exists.intro, Filter.HasAntitoneBasis.antitone
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
x y : X
n : ℕ
h : ∃ (n : ℕ), (x, y) ∉ U n
⊢ (∃ m ≤ n, (x, y) ∉ U m) ↔ (x, y) ∉ U n

Tactic:
exact ⟨fun ⟨m, hmn, hm⟩ hn => hm (hB.antitone hmn hn), fun h => ⟨n, le_rfl, h⟩⟩
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
x y : X
n : ℕ
h : ¬∃ (n : ℕ), (x, y) ∉ U n
⊢ ∀ (n : ℕ), (x, y) ∈ U n

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
x y : X
n : ℕ
h : ∀ (n : ℕ), (x, y) ∈ U n
⊢ (1 / 2) ^ n ≤ 0 ↔ (x, y) ∉ U n

Tactic:
simp only [h, not_true, (pow_pos hr.1 _).not_ge]

Premises used: pow_pos, And.left, not_true, LT.lt.not_ge
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
⊢ ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n

Tactic:
have hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n := by
    intro x y n
    dsimp only [d]
    split_ifs with h
    · rw [(pow_right_strictAnti₀ hr.1 hr.2).le_iff_ge, Nat.find_le_iff]
      exact ⟨fun ⟨m, hmn, hm⟩ hn => hm (hB.antitone hmn hn), fun h => ⟨n, le_rfl, h⟩⟩
    · push Not at h
      simp only [h, not_true, (pow_pos hr.1 _).not_ge]
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
⊢ ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y

Tactic:
PseudoMetricSpace.le_two_mul_dist_ofPreNNDist _ _ _ fun x₁ x₂ x₃ x₄ => ?_

Premises used: PseudoMetricSpace.le_two_mul_dist_ofPreNNDist
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
refine : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
⊢ ∀ (x y : X), (↑(d x y) : ℝ) ≤ 2 * dist x y

Tactic:
refine PseudoMetricSpace.le_two_mul_dist_ofPreNNDist _ _ _ fun x₁ x₂ x₃ x₄ => ?_

Premises used: PseudoMetricSpace.le_two_mul_dist_ofPreNNDist
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
x₁ x₂ x₃ x₄ : X
pos : ∀ (H : ∃ (n : ℕ), (x₁, x₄) ∉ U n), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
neg : ∀ (H : ¬∃ (n : ℕ), (x₁, x₄) ∉ U n), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
⊢ d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))

Tactic:
by_cases H : ∃ n, (x₁, x₄) ∉ U n

Premises used: Prod.mk
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
x₁ x₂ x₃ x₄ : X
H : ∃ (n : ℕ), (x₁, x₄) ∉ U n
⊢ d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))

Tactic:
(dif_pos H).trans_le ?_

Premises used: dif_pos, Eq.trans_le
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
x₁ x₂ x₃ x₄ : X
H : ∃ (n : ℕ), (x₁, x₄) ∉ U n
pos : (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
⊢ d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))

Tactic:
refine (dif_pos H).trans_le ?_

Premises used: dif_pos, Eq.trans_le
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
x₁ x₂ x₃ x₄ : X
H : ∃ (n : ℕ), (x₁, x₄) ∉ U n
pos : (1 / 2) ^ (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1) ≤ max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
⊢ (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))

Tactic:
rw [← div_le_iff₀' zero_lt_two, ← mul_one_div (_ ^ _), ← pow_succ]

Premises used: pow_succ, HPow.hPow, mul_one_div, div_le_iff₀'
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
x₁ x₂ x₃ x₄ : X
H : ∃ (n : ℕ), (x₁, x₄) ∉ U n
pos :
  ¬((x₁, x₂) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1) ∧
      (x₂, x₃) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1) ∧
        (x₃, x₄) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1))
⊢ (1 / 2) ^ (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1) ≤ max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))

Tactic:
simp only [le_max_iff, hle_d, ← not_and_or]

Premises used: not_and_or, le_max_iff
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
x₁ x₂ x₃ x₄ : X
H : ∃ (n : ℕ), (x₁, x₄) ∉ U n
h₁₂ : (x₁, x₂) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1)
h₂₃ : (x₂, x₃) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1)
h₃₄ : (x₃, x₄) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1)
⊢ False

Tactic:
Nat.find_spec H (hU_comp (lt_add_one <| Nat.find H) ?_)

Premises used: lt_add_one, Nat.find, Nat.find_spec
-- Module: Mathlib.Topology.Metrizable.Uniformity
Goal:
X : Type u_2
inst : UniformSpace X
inst_1 : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 :=
  fun (x y : X) ↦ if h : ∃ (n : ℕ), (x, y) ∉ U n then (1 / 2) ^ Nat.find (p := fun (n : ℕ) ↦ (x, y) ∉ U n) h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) (1 / 2)
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ (↑(d x y) : ℝ)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
x₁ x₂ x₃ x₄ : X
H : ∃ (n : ℕ), (x₁, x₄) ∉ U n
h₁₂ : (x₁, x₂) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1)
h₂₃ : (x₂, x₃) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1)
h₃₄ : (x₃, x₄) ∈ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1)
pos :
  (x₁, x₄) ∈
    U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1) ○
      (U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1) ○ U (Nat.find (p := fun (n : ℕ) ↦ (x₁, x₄) ∉ U n) H + 1))
⊢ False

Tactic:
refine Nat.find_spec H (hU_comp (lt_add_one <| Nat.find H) ?_)

Premises used: lt_add_one, Nat.find, Nat.find_spec