awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
rw :
  Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.closedBall x r)
    (preimage.{u, v} (β := β) ((⇑h : (a : α) → β) : (a : α) → β)
      (Metric.closedBall ((h : (a : α) → β) ((h.symm : (a : β) → α) x : α)) r : Set β))
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.closedBall x r : Set α)
    (Metric.closedBall ((h.symm : (a : β) → α) x) r : Set α)
have rw₁ : Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.closedBall x r) ((⇑h : (a : α) → β) ⁻¹' Metric.closedBall x r)
Tactic: rw [← h.isometry.preimage_closedBall (h.symm x) r, h.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.ball x r : Set β) (Metric.ball ((h : (a : α) → β) x) r : Set β)
have rw : Eq.{v + 1} (α := Set β) ((⇑h.symm : (a : β) → α) ⁻¹' Metric.ball x r : Set β)
  (Metric.ball ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_ball, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
rw :
  Eq.{v + 1} (α := Set β) ((⇑h.symm : (a : β) → α) ⁻¹' Metric.ball x r : Set β)
    (Metric.ball ((h : (a : α) → β) x) r : Set β)
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.ball x r : Set β) (Metric.ball ((h : (a : α) → β) x) r : Set β)
have rw₁ : Eq.{v + 1} (α := Set β) (Metric.ball ((h.symm.symm : (a : α) → β) x) r : Set β)
  (Metric.ball ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_ball, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
rw :
  Eq.{v + 1} (α := Set β) ((⇑h.symm : (a : β) → α) ⁻¹' Metric.ball x r : Set β)
    (Metric.ball ((h : (a : α) → β) x) r : Set β)
rw₁ :
  Eq.{v + 1} (α := Set β) (Metric.ball ((h.symm.symm : (a : α) → β) x) r : Set β)
    (Metric.ball ((h : (a : α) → β) x) r : Set β)
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.ball x r : Set β) (Metric.ball ((h : (a : α) → β) x) r : Set β)
have rw₂ : Eq.{v + 1} (α := Set β) (Metric.ball ((h : (a : α) → β) x) r : Set β) (Metric.ball ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_ball, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.sphere x r : Set β)
    (Metric.sphere ((h : (a : α) → β) x) r : Set β)
have rw : Eq.{v + 1} (α := Set β) ((⇑h.symm : (a : β) → α) ⁻¹' Metric.sphere x r : Set β)
  (Metric.sphere ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_sphere, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
rw :
  Eq.{v + 1} (α := Set β) ((⇑h.symm : (a : β) → α) ⁻¹' Metric.sphere x r : Set β)
    (Metric.sphere ((h : (a : α) → β) x) r : Set β)
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.sphere x r : Set β)
    (Metric.sphere ((h : (a : α) → β) x) r : Set β)
have rw₁ : Eq.{v + 1} (α := Set β) (Metric.sphere ((h.symm.symm : (a : α) → β) x) r : Set β)
  (Metric.sphere ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_sphere, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
rw :
  Eq.{v + 1} (α := Set β) ((⇑h.symm : (a : β) → α) ⁻¹' Metric.sphere x r : Set β)
    (Metric.sphere ((h : (a : α) → β) x) r : Set β)
rw₁ :
  Eq.{v + 1} (α := Set β) (Metric.sphere ((h.symm.symm : (a : α) → β) x) r : Set β)
    (Metric.sphere ((h : (a : α) → β) x) r : Set β)
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.sphere x r : Set β)
    (Metric.sphere ((h : (a : α) → β) x) r : Set β)
have rw₂ : Eq.{v + 1} (α := Set β) (Metric.sphere ((h : (a : α) → β) x) r : Set β) (Metric.sphere ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_sphere, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.closedBall x r : Set β)
    (Metric.closedBall ((h : (a : α) → β) x) r : Set β)
have rw : Eq.{v + 1} (α := Set β) ((⇑h.symm : (a : β) → α) ⁻¹' Metric.closedBall x r : Set β)
  (Metric.closedBall ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_closedBall, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
rw :
  Eq.{v + 1} (α := Set β) ((⇑h.symm : (a : β) → α) ⁻¹' Metric.closedBall x r : Set β)
    (Metric.closedBall ((h : (a : α) → β) x) r : Set β)
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.closedBall x r : Set β)
    (Metric.closedBall ((h : (a : α) → β) x) r : Set β)
have rw₁ : Eq.{v + 1} (α := Set β) (Metric.closedBall ((h.symm.symm : (a : α) → β) x) r : Set β)
  (Metric.closedBall ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_closedBall, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
rw :
  Eq.{v + 1} (α := Set β) ((⇑h.symm : (a : β) → α) ⁻¹' Metric.closedBall x r : Set β)
    (Metric.closedBall ((h : (a : α) → β) x) r : Set β)
rw₁ :
  Eq.{v + 1} (α := Set β) (Metric.closedBall ((h.symm.symm : (a : α) → β) x) r : Set β)
    (Metric.closedBall ((h : (a : α) → β) x) r : Set β)
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.closedBall x r : Set β)
    (Metric.closedBall ((h : (a : α) → β) x) r : Set β)
have rw₂ : Eq.{v + 1} (α := Set β) (Metric.closedBall ((h : (a : α) → β) x) r : Set β)
  (Metric.closedBall ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_closedBall, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
n : ℕ
inst : MetricSpace α
x : ℕ → α
a : α
⊢ BddAbove (α := ℝ) (range fun (i : ℕ) ↦ ‖dist a (x i) - dist (x 0) (x i)‖)
have h : Membership.mem (γ := Set ℝ) (upperBounds (range fun (i : ℕ) ↦ ‖dist a (x i) - dist (x 0) (x i)‖)) (dist a (x 0))
Tactic: use dist a (x 0)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
a b : α
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) ≤ dist a b
have rw : ‖embeddingOfSubset x a - embeddingOfSubset x b‖ ≤ dist a b
Tactic: rw [dist_eq_norm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
a b : α
⊢ ‖embeddingOfSubset x a - embeddingOfSubset x b‖ ≤ dist a b
have refine : ∀ (n : ℕ), ‖(↑(embeddingOfSubset x a - embeddingOfSubset x b) : (i : ℕ) → ℝ) n‖ ≤ dist a b
Tactic: refine lp.norm_le_of_forall_le dist_nonneg fun n => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
a b : α
n : ℕ
⊢ ‖dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n))‖ ≤ dist a b
have h : dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n)) = dist a (x n) - dist b (x n)
Tactic: convert! abs_dist_sub_le a b (x n) using 2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
⊢ Isometry (embeddingOfSubset x)
have refine : ∀ (a b : α), dist (embeddingOfSubset x a) (embeddingOfSubset x b) = dist a b
Tactic: refine Isometry.of_dist_eq fun a b => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) = dist a b
have refine : ∀ (e : ℝ) (epos : 0 < e), dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
Tactic: refine (embeddingOfSubset_dist_le x a b).antisymm (le_of_forall_pos_le_add fun e epos => ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
have rcases : ∀ (n : ℕ) (hn : dist a (x n) < e / 2), dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
Tactic: rcases Metric.mem_closure_range_iff.1 (H a) (e / 2) (half_pos epos) with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (hypothesis)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
have C : dist b (x n) - dist a (x n) =
  (↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
    (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n
Tactic: have C : dist b (x n) - dist a (x n) = embeddingOfSubset x b n - embeddingOfSubset x a n := by
    simp only [embeddingOfSubset_coe, sub_sub_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C :
  dist b (x n) - dist a (x n) =
    (↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
      (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n
⊢ dist a (x n) + dist (x n) b = 2 * dist a (x n) + (dist b (x n) - dist a (x n))
have simp : dist a (x n) + dist b (x n) = 2 * dist a (x n) + (dist b (x n) - dist a (x n))
Tactic: simp [dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C :
  dist b (x n) - dist a (x n) =
    (↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
      (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n
⊢ 2 * dist a (x n) + (dist b (x n) - dist a (x n)) ≤ 2 * dist a (x n) + |dist b (x n) - dist a (x n)|
have grw : 2 * dist a (x n) + (dist b (x n) - dist a (x n)) ≤ 2 * dist a (x n) + (dist b (x n) - dist a (x n))
Tactic: grw [← le_abs_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C :
  dist b (x n) - dist a (x n) =
    (↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
      (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n
⊢ 2 * dist a (x n) + |dist b (x n) - dist a (x n)| ≤
    2 * (e / 2) +
      |(↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
          (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n|
have rw : 2 * dist a (x n) +
    |(↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
        (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n| ≤
  2 * (e / 2) +
    |(↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
        (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n|
Tactic: rw [C]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C :
  dist b (x n) - dist a (x n) =
    (↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
      (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n
⊢ 2 * dist a (x n) +
      |(↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
          (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n| ≤
    2 * (e / 2) +
      |(↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
          (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n|
have bc : LE.le (α := ℝ) 0 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C :
  dist b (x n) - dist a (x n) =
    (↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
      (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n
⊢ 2 * (e / 2) +
      |(↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
          (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n| ≤
    2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a)
have bc : |(↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
      (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n| ≤
  dist (embeddingOfSubset x b) (embeddingOfSubset x a)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C :
  dist b (x n) - dist a (x n) =
    (↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
      (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n
⊢ |(↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
        (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n| ≤
    dist (embeddingOfSubset x b) (embeddingOfSubset x a)
have bc : |(↑(embeddingOfSubset x b) : (i : ℕ) → ℝ) n - (↑(embeddingOfSubset x a) : (i : ℕ) → ℝ) n| ≤
  ‖embeddingOfSubset x b - embeddingOfSubset x a‖
Tactic: simp only [dist_eq_norm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (hypothesis)
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C :
  dist b (x n) - dist a (x n) =
    (↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
      (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
have this : dist a b ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e
Tactic: have :=
    calc
      dist a b ≤ dist a (x n) + dist (x n) b := dist_triangle _ _ _
      _ = 2 * dist a (x n) + (dist b (x n) - dist a (x n)) := by simp [dist_comm]; ring
      _ ≤ 2 * dist a (x n) + |dist b (x n) - dist a (x n)| := by grw [← le_abs_self]
      _ ≤ 2 * (e / 2) + |embeddingOfSubset x b n - embeddingOfSubset x a n| := by
        rw [C]
        gcongr
      _ ≤ 2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) := by
        gcongr
        simp only [dist_eq_norm]
        exact lp.norm_apply_le_norm ENNReal.top_ne_zero
          (embeddingOfSubset x b - embeddingOfSubset x a) n
      _ = dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e := by ring
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
have inl : ∀ (h : Eq.{u + 1} (α := Set α) univ ∅), ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
Tactic: rcases (univ : Set α).eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
inl : ∀ (h : Eq.{u + 1} (α := Set α) univ ∅), ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
have inr : ∀ (h : Set.Nonempty.{u} (α := α) univ), ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
Tactic: rcases (univ : Set α).eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) univ ∅
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
have h₁ : Isometry (β := ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)) fun (x : α) ↦ 0
Tactic: use fun _ => 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
h : Set.Nonempty.{u} (α := α) univ
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
have inr : ∀ (basepoint : α), Membership.mem (γ := Set α) univ basepoint → ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
Tactic: rcases h with ⟨basepoint⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
basepoint : α
h : Membership.mem (γ := Set α) univ basepoint
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
have inr : ∀ (this : Inhabited α), ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
Tactic: haveI : Inhabited α := ⟨basepoint⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (hypothesis)
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
basepoint : α
h : Membership.mem (γ := Set α) univ basepoint
this : Inhabited α
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
have this₁ : ∃ (s : Set α), s.Countable ∧ Dense s
Tactic: have : ∃ s : Set α, s.Countable ∧ Dense s := exists_countable_dense α
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
basepoint : α
h : Membership.mem (γ := Set α) univ basepoint
this_1 : Inhabited α
this : ∃ (s : Set α), s.Countable ∧ Dense s
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
have inr : ∀ (S : Set α) (S_countable : S.Countable) (S_dense : Dense S), ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
Tactic: rcases this with ⟨S, ⟨S_countable, S_dense⟩⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
basepoint : α
h : Membership.mem (γ := Set α) univ basepoint
this : Inhabited α
S : Set α
S_countable : S.Countable
S_dense : Dense S
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
have inr : ∀ (x : ℕ → α) (x_range : S ⊆ range x), ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
Tactic: rcases Set.countable_iff_exists_subset_range.1 S_countable with ⟨x, x_range⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl : LipschitzOnWith K f s
⊢ ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s
have hfl₁ : ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
Tactic: rw [LipschitzOnWith.coordinate] at hfl
Cleared hypotheses: hfl
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
⊢ ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s
have this : ∀ (i : ι), ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) g s
Tactic: have (i : ι) : ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s :=
    LipschitzOnWith.extend_real (hfl i)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
this : ∀ (i : ι), ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) g s
⊢ ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s
have choose : ∀ (g : (i : ι) → α → ℝ) (hgl : ∀ (i : ι), LipschitzWith K (g i))
  (hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s),
  ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s
Tactic: choose g hgl hgeq using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
⊢ ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s
have inl : ∀
  (hfl :
    ∀ (i : ι),
      LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) ∅)
  (hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) ∅),
  ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g ∅
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀_in_s⟩
Cleared hypotheses: s, hfl, hgeq
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
inl :
  ∀
    (hfl :
      ∀ (i : ι),
        LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) ∅)
    (hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) ∅),
    ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g ∅
⊢ ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s
have inr : ∀ (a₀ : α) (ha₀_in_s : a₀ ∈ s), ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀_in_s⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
⊢ ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
have apply : Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (a : ι) (a_1 : α) ↦ ℝ) g a₀) ∞
Tactic: apply LipschitzWith.uniformly_bounded (swap g) hgl a₀
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
⊢ Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (a : ι) (a_1 : α) ↦ ℝ) g a₀) ∞
have h : Membership.mem (γ := Set ℝ) (upperBounds (range fun (i : ι) ↦ ‖swap (φ := fun (a : ι) (a_1 : α) ↦ ℝ) g a₀ i‖)) ‖f a₀‖
Tactic: use ‖f a₀‖