awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
p : α → Prop
a : { a : α // p a }
r : ℝ
rw :
  image (α := { a : α // p a }) (val (p := fun (a : α) ↦ p a))
      (val (p := fun (a : α) ↦ p a) ⁻¹' closedBall (↑a : α) r) =
    closedBall (↑a : α) r ∩ {a : α | p a}
rw₁ :
  closedBall (↑a : α) r ∩ range (ι := { a : α // p a }) (val (p := fun (a : α) ↦ p a)) =
    closedBall (↑a : α) r ∩ {a : α | p a}
⊢ val (p := fun (a : α) ↦ p a) '' closedBall a r = closedBall (↑a : α) r ∩ {a : α | p a}
have rw₂ : closedBall (↑a : α) r ∩ {x : α | p x} = closedBall (↑a : α) r ∩ {a : α | p a}
Tactic: rw [← preimage_closedBall, image_preimage_eq_inter_range, range_val_subtype]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
a b x : ℝ≥0
⊢ nndist a b ≤ x ↔ max (a - b) (b - a) ≤ x
have simp : nndist a b ≤ x ↔ a ≤ x + b ∧ b ≤ x + a
Tactic: simp only [max_le_iff, tsub_le_iff_right (α := ℝ≥0)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
z : ℝ≥0
⊢ nndist z 0 = z
have rw : nndist 0 z = z
Tactic: rw [nndist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
a b : ℝ≥0
this : (↑a : ℝ) ≤ (↑b : ℝ) + dist a b
⊢ a ≤ b + nndist a b
have rwa : (↑a : ℝ) ≤ (↑(b + nndist a b) : ℝ)
Tactic: rwa [← NNReal.coe_le_coe, NNReal.coe_add, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
a b : ℝ≥0
this : (↑a : ℝ) ≤ (↑b : ℝ) + dist a b
rwa : (↑a : ℝ) ≤ (↑(b + nndist a b) : ℝ)
⊢ a ≤ b + nndist a b
have rwa₁ : (↑a : ℝ) ≤ (↑b : ℝ) + (↑(nndist a b) : ℝ)
Tactic: rwa [← NNReal.coe_le_coe, NNReal.coe_add, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
a b : ℝ≥0
⊢ (↑a : ℝ) ≤ (↑b : ℝ) + dist a b
have rw : (↑a : ℝ) - (↑b : ℝ) ≤ dist a b
Tactic: rw [← sub_le_iff_le_add']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
c : ℝ≥0
⊢ ball 0 (↑c : ℝ) = Ico 0 c
have h : ∀ (x : ℝ≥0), Membership.mem (γ := Set ℝ≥0) (ball 0 (↑c : ℝ)) x ↔ x ∈ Ico 0 c
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
c : ℝ
⊢ ball 0 c = Ico 0 c.toNNReal
have pos : ∀ (c_pos : 0 < c), ball 0 c = Ico 0 c.toNNReal
Tactic: by_cases! c_pos : 0 < c
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
c : ℝ
pos : ∀ (c_pos : 0 < c), ball 0 c = Ico 0 c.toNNReal
⊢ ball 0 c = Ico 0 c.toNNReal
have neg : ∀ (c_pos : c ≤ 0), ball 0 c = Ico 0 c.toNNReal
Tactic: by_cases! c_pos : 0 < c
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
c : ℝ
c_pos : 0 < c
⊢ ball 0 c = Ico 0 c.toNNReal
have h : c.toNNReal = NNReal.mk c sorry
Tactic: convert! NNReal.ball_zero_eq_Ico' (NNReal.mk c c_pos.le)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
c : ℝ≥0
⊢ closedBall 0 (↑c : ℝ) = Icc 0 c
have h : ∀ (x : ℝ≥0), Membership.mem (γ := Set ℝ≥0) (closedBall 0 (↑c : ℝ)) x ↔ x ∈ Icc 0 c
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
c : ℝ
c_nn : 0 ≤ c
⊢ closedBall 0 c = Icc 0 c.toNNReal
have h : c.toNNReal = NNReal.mk c c_nn
Tactic: convert! NNReal.closedBall_zero_eq_Icc' (NNReal.mk c c_nn)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
i : PseudoMetricSpace (α × β) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun (x y : α × β) ↦ max (dist x.1 y.1) (dist x.2 y.2)) ⋯ ⋯
s : Set (α × β)
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s
have simp : (∀ᶠ (x : ℝ) in atTop,
    ∀ (x_1 : α × β) (x_2 : x_1 ∈ s) (x_3 : α × β) (x_4 : x_3 ∈ s), max (dist x_1.1 x_3.1) (dist x_1.2 x_3.2) ≤ x) ↔
  ∀ᶠ (C : ℝ) in atTop, ∀ ⦃x : α × β⦄, x ∈ s → ∀ ⦃y : α × β⦄, y ∈ s → dist x y ≤ C
Tactic: simp only [← isBounded_image_fst_and_snd, isBounded_iff_eventually, forall_mem_image, ←
      eventually_and, ← forall_and, ← max_le_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
r : ℝ
⊢ sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
have inl : ∀ (hr : r < 0), sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
Tactic: obtain hr | rfl | hr := lt_trichotomy r 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
r : ℝ
inl : ∀ (hr : r < 0), sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
⊢ sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
have inr : sphere x 0 = sphere x.1 0 ×ˢ closedBall x.2 0 ∪ closedBall x.1 0 ×ˢ sphere x.2 0
Tactic: obtain hr | rfl | hr := lt_trichotomy r 0
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
r : ℝ
inl : ∀ (hr : r < 0), sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
inr : sphere x 0 = sphere x.1 0 ×ˢ closedBall x.2 0 ∪ closedBall x.1 0 ×ˢ sphere x.2 0
⊢ sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
have inr₁ : ∀ (hr : 0 < r), sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
Tactic: obtain hr | rfl | hr := lt_trichotomy r 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
⊢ sphere x 0 = sphere x.1 0 ×ˢ closedBall x.2 0 ∪ closedBall x.1 0 ×ˢ sphere x.2 0
have inr : ∀ (fst : α) (snd : β),
  sphere (fst, snd) 0 =
    sphere (fst, snd).1 0 ×ˢ closedBall (fst, snd).2 0 ∪ closedBall (fst, snd).1 0 ×ˢ sphere (fst, snd).2 0
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
fst : α
snd : β
⊢ sphere (fst, snd) 0 =
    sphere (fst, snd).1 0 ×ˢ closedBall (fst, snd).2 0 ∪ closedBall (fst, snd).1 0 ×ˢ sphere (fst, snd).2 0
have inr : sphere (fst, snd) 0 = sphere fst 0 ×ˢ closedBall snd 0 ∪ closedBall fst 0 ×ˢ sphere snd 0
Tactic: simp_rw [← closedBall_eq_sphere_of_nonpos le_rfl, union_self, closedBall_prod_same]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
fst : α
snd : β
inr inr₁ : sphere (fst, snd) 0 = sphere fst 0 ×ˢ closedBall snd 0 ∪ closedBall fst 0 ×ˢ sphere snd 0
⊢ sphere (fst, snd) 0 =
    sphere (fst, snd).1 0 ×ˢ closedBall (fst, snd).2 0 ∪ closedBall (fst, snd).1 0 ×ˢ sphere (fst, snd).2 0
have inr₂ : closedBall (fst, snd) 0 = closedBall fst 0 ×ˢ closedBall snd 0 ∪ closedBall fst 0 ×ˢ closedBall snd 0
Tactic: simp_rw [← closedBall_eq_sphere_of_nonpos le_rfl, union_self, closedBall_prod_same]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
fst : α
snd : β
inr inr₁ : sphere (fst, snd) 0 = sphere fst 0 ×ˢ closedBall snd 0 ∪ closedBall fst 0 ×ˢ sphere snd 0
inr₂ : closedBall (fst, snd) 0 = closedBall fst 0 ×ˢ closedBall snd 0 ∪ closedBall fst 0 ×ˢ closedBall snd 0
⊢ sphere (fst, snd) 0 =
    sphere (fst, snd).1 0 ×ˢ closedBall (fst, snd).2 0 ∪ closedBall (fst, snd).1 0 ×ˢ sphere (fst, snd).2 0
have inr₃ : closedBall (fst, snd) 0 = closedBall fst 0 ×ˢ closedBall snd 0
Tactic: simp_rw [← closedBall_eq_sphere_of_nonpos le_rfl, union_self, closedBall_prod_same]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
⊢ sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
have inr : ∀ (x' : α) (y' : β),
  (x', y') ∈ sphere x r ↔ (x', y') ∈ sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
Tactic: ext ⟨x', y'⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ (x', y') ∈ sphere x r ↔ (x', y') ∈ sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
have inr : dist x' x.1 = r ∧ dist y' x.2 ≤ dist x' x.1 ∨ dist y' x.2 = r ∧ dist x' x.1 ≤ dist y' x.2 ↔
  dist x' x.1 = r ∧ dist y' x.2 ≤ r ∨ dist x' x.1 ≤ r ∧ dist y' x.2 = r
Tactic: simp_rw [Set.mem_union, Set.mem_prod, Metric.mem_closedBall, Metric.mem_sphere, Prod.dist_eq,
      max_eq_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ dist x' x.1 = r ∧ dist y' x.2 ≤ dist x' x.1 ∨ dist y' x.2 = r ∧ dist x' x.1 ≤ dist y' x.2 ↔
    dist x' x.1 = r ∧ dist y' x.2 ≤ r ∨ dist x' x.1 ≤ r ∧ dist y' x.2 = r
have inr : dist x' x.1 = r → (dist y' x.2 ≤ dist x' x.1 ↔ dist y' x.2 ≤ r)
Tactic: refine or_congr (and_congr_right ?_) (and_comm.trans (and_congr_left ?_))
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
inr : dist x' x.1 = r → (dist y' x.2 ≤ dist x' x.1 ↔ dist y' x.2 ≤ r)
⊢ dist x' x.1 = r ∧ dist y' x.2 ≤ dist x' x.1 ∨ dist y' x.2 = r ∧ dist x' x.1 ≤ dist y' x.2 ↔
    dist x' x.1 = r ∧ dist y' x.2 ≤ r ∨ dist x' x.1 ≤ r ∧ dist y' x.2 = r
have inr₁ : dist y' x.2 = r → (dist x' x.1 ≤ dist y' x.2 ↔ dist x' x.1 ≤ r)
Tactic: refine or_congr (and_congr_right ?_) (and_comm.trans (and_congr_left ?_))
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)
have inl : ∀
  (hs :
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} ∅),
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (∅ ∪ t)
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
inl :
  ∀
    (hs :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} ∅),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
      (∅ ∪ t)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)
have inr : ∀ (x : α) (hx : x ∈ s),
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)
have inr : ∀
  (ht :
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} ∅),
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ ∅)
Tactic: rcases t.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
inr :
  ∀
    (ht :
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} ∅),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
      (s ∪ ∅)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)
have inr₁ : ∀ (y : α) (hy : y ∈ t),
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)
Tactic: rcases t.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)
have inr : ∀ (C : ℝ) (hC : ∀ z ∈ s ∪ t, dist x z ≤ C),
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)
Tactic: rsuffices ⟨C, hC⟩ : ∃ C, ∀ z ∈ s ∪ t, dist x z ≤ C
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
inr :
  ∀ (C : ℝ) (hC : ∀ z ∈ s ∪ t, dist x z ≤ C),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
      (s ∪ t)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)
have rsuffices : ∃ (C : ℝ), ∀ z ∈ s ∪ t, dist x z ≤ C
Tactic: rsuffices ⟨C, hC⟩ : ∃ C, ∀ z ∈ s ∪ t, dist x z ≤ C
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
C : ℝ
hC : ∀ z ∈ s ∪ t, dist x z ≤ C
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} (s ∪ t)
have inr : ∀ (a : α) (ha : a ∈ s ∪ t) (b : α) (hb : b ∈ s ∪ t), dist a x + dist x b ≤ C + C
Tactic: refine ⟨C + C, fun a ha b hb => (dist_triangle a x b).trans ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} s
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
⊢ ∃ (C : ℝ), ∀ z ∈ s ∪ t, dist x z ≤ C
have rcases : ∀ (Cs : ℝ) (hs : ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ Cs), ∃ (C : ℝ), ∀ z ∈ s ∪ t, dist x z ≤ C
Tactic: rcases hs with ⟨Cs, hs⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s t : Set α
ht : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
Cs : ℝ
hs : ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ Cs
⊢ ∃ (C : ℝ), ∀ z ∈ s ∪ t, dist x z ≤ C
have rcases : ∀ (Ct : ℝ) (ht : ∀ ⦃x : α⦄, x ∈ t → ∀ ⦃y : α⦄, y ∈ t → dist x y ≤ Ct), ∃ (C : ℝ), ∀ z ∈ s ∪ t, dist x z ≤ C
Tactic: rcases ht with ⟨Ct, ht⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Sort u_3
x y : α
dist : α → α → ℝ
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
⊢ dist x y + dist y x = 2 * dist x y
have rw : dist x y + dist y x = dist x y + dist x y
Tactic: rw [two_mul, dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Sort u_3
x y : α
dist : α → α → ℝ
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
rw : dist x y + dist y x = dist x y + dist x y
⊢ dist x y + dist y x = 2 * dist x y
have rw₁ : dist y x + dist y x = dist y x + dist y x
Tactic: rw [two_mul, dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u_3
m m' : PseudoMetricSpace α
h : Eq.{u_3 + 1} (α := Dist α) toDist toDist
d : Dist α := toDist
⊢ m = m'
have obtain : ∀ [toDist : Dist α] (dist_self : ∀ (x : α), dist x x = 0) (dist_comm : ∀ (x y : α), dist x y = dist y x)
  (dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z) (edist : α → α → ℝ≥0∞)
  (hed : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)) (toUniformSpace : UniformSpace α)
  (hU : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}) (toBornology : Bornology α)
  (hB : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C})
  (h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist),
  { toDist := toDist, dist_self := dist_self, dist_comm := dist_comm, dist_triangle := dist_triangle, edist := edist,
      edist_dist := hed, toUniformSpace := toUniformSpace, uniformity_dist := hU, toBornology := toBornology,
      cobounded_sets := hB : PseudoMetricSpace α } =
    m'
Tactic: obtain ⟨_, _, _, _, hed, _, hU, _, hB⟩ := m
Cleared hypotheses: m, h, d
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u_3
m' : PseudoMetricSpace α
toDist : Dist α
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)
toUniformSpace : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
toBornology : Bornology α
hB : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist
d : Dist α := PseudoMetricSpace.toDist
d' : Dist α := PseudoMetricSpace.toDist
⊢ { toDist := toDist, dist_self := dist_self, dist_comm := dist_comm, dist_triangle := dist_triangle, edist := edist,
      edist_dist := hed, toUniformSpace := toUniformSpace, uniformity_dist := hU, toBornology := toBornology,
      cobounded_sets := hB : PseudoMetricSpace α } =
    m'
have obtain : ∀ [toDist_1 : Dist α] (dist_self_1 : ∀ (x : α), dist x x = 0) (dist_comm_1 : ∀ (x y : α), dist x y = dist y x)
  (dist_triangle_1 : ∀ (x y z : α), dist x z ≤ dist x y + dist y z) (edist_1 : α → α → ℝ≥0∞)
  (hed' : ∀ (x y : α), edist_1 x y = ENNReal.ofReal (dist x y)) (toUniformSpace_1 : UniformSpace α)
  (hU' : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}) (toBornology_1 : Bornology α)
  (hB' : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C})
  (h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist),
  { toDist := toDist, dist_self := dist_self, dist_comm := dist_comm, dist_triangle := dist_triangle, edist := edist,
      edist_dist := hed, toUniformSpace := toUniformSpace, uniformity_dist := hU, toBornology := toBornology,
      cobounded_sets := hB : PseudoMetricSpace α } =
    { toDist := toDist_1, dist_self := dist_self_1, dist_comm := dist_comm_1, dist_triangle := dist_triangle_1,
      edist := edist_1, edist_dist := hed', toUniformSpace := toUniformSpace_1, uniformity_dist := hU',
      toBornology := toBornology_1, cobounded_sets := hB' }
Tactic: obtain ⟨_, _, _, _, hed', _, hU', _, hB'⟩ := m'
Cleared hypotheses: m', h, d'