awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
s : Set β
rw : Metric.diam.{u} (α := α) ((⇑h.symm : (a : β) → α) '' s) = Metric.diam s
rw₁ rw₂ : Metric.diam s = Metric.diam s
⊢ Metric.diam.{u} (α := α) ((⇑h : (a : α) → β) ⁻¹' s) = Metric.diam s

Tactic:
rw [← image_symm, diam_image]

Premises used: IsometryEquiv.diam_image, IsometryEquiv.image_symm
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
⊢ Metric.diam.{u} (α := α) univ = Metric.diam.{v} (α := β) univ

Tactic:
congr_arg ENNReal.toReal h.ediam_univ

Premises used: IsometryEquiv.ediam_univ, congr_arg, ENNReal.toReal, Metric.diam
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
rw :
  Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.ball x r)
    (preimage.{u, v} (β := β) ((⇑h : (a : α) → β) : (a : α) → β)
      (Metric.ball ((h : (a : α) → β) ((h.symm : (a : β) → α) x : α)) r : Set β))
rw₁ rw₂ : Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.ball x r) ((⇑h : (a : α) → β) ⁻¹' Metric.ball x r)
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.ball x r : Set α)
    (Metric.ball ((h.symm : (a : β) → α) x) r : Set α)

Tactic:
rw [← h.isometry.preimage_ball (h.symm x) r, h.apply_symm_apply]

Premises used: Isometry.preimage_ball, IsometryEquiv.apply_symm_apply, IsometryEquiv.symm, DFunLike.coe, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
rw :
  Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.sphere x r)
    (preimage.{u, v} (β := β) ((⇑h : (a : α) → β) : (a : α) → β)
      (Metric.sphere ((h : (a : α) → β) ((h.symm : (a : β) → α) x : α)) r : Set β))
rw₁ rw₂ : Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.sphere x r) ((⇑h : (a : α) → β) ⁻¹' Metric.sphere x r)
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.sphere x r : Set α)
    (Metric.sphere ((h.symm : (a : β) → α) x) r : Set α)

Tactic:
rw [← h.isometry.preimage_sphere (h.symm x) r, h.apply_symm_apply]

Premises used: IsometryEquiv.apply_symm_apply, IsometryEquiv.symm, Isometry.preimage_sphere, DFunLike.coe, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
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 β))
rw₁ rw₂ :
  Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.closedBall x r) ((⇑h : (a : α) → β) ⁻¹' Metric.closedBall x r)
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.closedBall x r : Set α)
    (Metric.closedBall ((h.symm : (a : β) → α) x) r : Set α)

Tactic:
rw [← h.isometry.preimage_closedBall (h.symm x) r, h.apply_symm_apply]

Premises used: IsometryEquiv.apply_symm_apply, IsometryEquiv.symm, Isometry.preimage_closedBall, DFunLike.coe, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
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 β)
rw₂ rw₃ :
  Eq.{v + 1} (α := Set β) (Metric.ball ((h : (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 β)

Tactic:
rw [← h.preimage_symm, h.symm.preimage_ball, symm_symm]

Premises used: IsometryEquiv.symm, IsometryEquiv.symm_symm, IsometryEquiv.preimage_symm, IsometryEquiv.preimage_ball
-- Module: Mathlib.Topology.MetricSpace.Isometry
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 β)
rw₂ rw₃ :
  Eq.{v + 1} (α := Set β) (Metric.sphere ((h : (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 β)

Tactic:
rw [← h.preimage_symm, h.symm.preimage_sphere, symm_symm]

Premises used: IsometryEquiv.preimage_sphere, IsometryEquiv.symm, IsometryEquiv.symm_symm, IsometryEquiv.preimage_symm
-- Module: Mathlib.Topology.MetricSpace.Isometry
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 β)
rw₂ rw₃ :
  Eq.{v + 1} (α := Set β) (Metric.closedBall ((h : (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 β)

Tactic:
rw [← h.preimage_symm, h.symm.preimage_closedBall, symm_symm]

Premises used: IsometryEquiv.symm, IsometryEquiv.symm_symm, IsometryEquiv.preimage_symm, IsometryEquiv.preimage_closedBall
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β
g : β → γ
K : ℝ≥0
h : Isometry g
⊢ LipschitzWith K (g ∘ f) ↔ LipschitzWith K f

Tactic:
simp [LipschitzWith, h.edist_eq]

Premises used: LipschitzWith, Isometry.edist_eq
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : EquivLike F α β
inst_3 : IsometryClass F α β
f : F
⊢ Eq (α := (a : α) → β) (⇑(↑f : α ≃ᵢ β) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : EquivLike F α β
inst_3 : IsometryClass F α β
⊢ Injective (α := F) (β := α ≃ᵢ β) toIsometryEquiv

Tactic:
fun _ _ e ↦ DFunLike.ext _ _ fun a ↦ DFunLike.congr_fun e a

Premises used: DFunLike.congr_fun, DFunLike.ext, Function.Injective
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
n : ℕ
inst : MetricSpace α
x : ℕ → α
a : α
h : Membership.mem (γ := Set ℝ) (upperBounds (range fun (i : ℕ) ↦ ‖dist a (x i) - dist (x 0) (x i)‖)) (dist a (x 0))
⊢ BddAbove (α := ℝ) (range fun (i : ℕ) ↦ ‖dist a (x i) - dist (x 0) (x i)‖)

Tactic:
use dist a (x 0)

Premises used: Dist.dist, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
n_1 : ℕ
inst : MetricSpace α
x : ℕ → α
a : α
n : ℕ
⊢ (fun (i : ℕ) ↦ ‖dist a (x i) - dist (x 0) (x i)‖) n ≤ dist a (x 0)

Tactic:
abs_dist_sub_le _ _ _

Premises used: abs_dist_sub_le
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
n_1 : ℕ
inst : MetricSpace α
x : ℕ → α
a : α
n : ℕ
⊢ (fun (i : ℕ) ↦ ‖dist a (x i) - dist (x 0) (x i)‖) n ≤ dist a (x 0)

Tactic:
exact abs_dist_sub_le _ _ _

Premises used: abs_dist_sub_le
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
n : ℕ
inst : MetricSpace α
x : ℕ → α
a : α
⊢ (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n = dist a (x n) - dist (x 0) (x n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
a b : α
rw : ‖embeddingOfSubset x a - embeddingOfSubset x b‖ ≤ dist a b
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) ≤ dist a b

Tactic:
rw [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
a b : α
⊢ ‖embeddingOfSubset x a - embeddingOfSubset x b‖ ≤ dist a b

Tactic:
lp.norm_le_of_forall_le dist_nonneg fun n => ?_

Premises used: ENNReal.ofNNReal, Set.Mem, setOf, dist_nonneg, WithTop.some, lp.norm_le_of_forall_le
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
a b : α
refine : ∀ (n : ℕ), ‖(↑(embeddingOfSubset x a - embeddingOfSubset x b) : (i : ℕ) → ℝ) n‖ ≤ dist a b
⊢ ‖embeddingOfSubset x a - embeddingOfSubset x b‖ ≤ dist a b

Tactic:
refine lp.norm_le_of_forall_le dist_nonneg fun n => ?_

Premises used: dist_nonneg, lp.norm_le_of_forall_le
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
a b : α
n : ℕ
⊢ |dist a (x n) - dist b (x n)| ≤ dist a b

Tactic:
abs_dist_sub_le a b (x n)

Premises used: abs_dist_sub_le
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
a b : α
n : ℕ
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)
⊢ ‖dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n))‖ ≤ dist a b

Tactic:
convert! abs_dist_sub_le a b (x n) using 2

Premises used: abs_dist_sub_le
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
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 (x n) - dist b (x n)

Tactic:
ring
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
⊢ Isometry (embeddingOfSubset x)

Tactic:
Isometry.of_dist_eq fun a b => ?_

Premises used: Isometry.of_dist_eq
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
refine : ∀ (a b : α), dist (embeddingOfSubset x a) (embeddingOfSubset x b) = dist a b
⊢ Isometry (embeddingOfSubset x)

Tactic:
refine Isometry.of_dist_eq fun a b => ?_

Premises used: Isometry.of_dist_eq
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) = dist a b

Tactic:
(embeddingOfSubset_dist_le x a b).antisymm (le_of_forall_pos_le_add fun e epos => ?_)

Premises used: ENNReal.ofNNReal, Set.Mem, setOf, le_of_forall_pos_le_add, LE.le.antisymm, WithTop.some, KuratowskiEmbedding.embeddingOfSubset_dist_le
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
refine : ∀ (e : ℝ) (epos : 0 < e), dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) = dist a b

Tactic:
refine (embeddingOfSubset_dist_le x a b).antisymm (le_of_forall_pos_le_add fun e epos => ?_)

Premises used: le_of_forall_pos_le_add, LE.le.antisymm, KuratowskiEmbedding.embeddingOfSubset_dist_le
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
rcases : ∀ (n : ℕ) (hn : dist a (x n) < e / 2), dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
⊢ 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⟩

Premises used: half_pos, HDiv.hDiv, Metric.mem_closure_range_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
⊢ 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:
simp only [embeddingOfSubset_coe, sub_sub_sub_cancel_right]

Premises used: sub_sub_sub_cancel_right, KuratowskiEmbedding.embeddingOfSubset_coe
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
⊢ 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]
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
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
simp : dist a (x n) + dist b (x n) = 2 * dist a (x n) + (dist b (x n) - dist a (x n))
⊢ dist a (x n) + dist (x n) b = 2 * dist a (x n) + (dist b (x n) - dist a (x n))

Tactic:
simp [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
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 b (x n) = 2 * dist a (x n) + (dist b (x n) - dist a (x n))

Tactic:
ring
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
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
grw 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))
⊢ 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]

Premises used: le_abs_self
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
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
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|
⊢ 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|

Tactic:
rw [C]
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
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
bc : LE.le (α := ℝ) 0 2
⊢ 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:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
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
bc :
  |(↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
        (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n| ≤
    dist (embeddingOfSubset x b) (embeddingOfSubset x a)
⊢ 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)

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
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
bc :
  |(↑(embeddingOfSubset x b) : (i : ℕ) → ℝ) n - (↑(embeddingOfSubset x a) : (i : ℕ) → ℝ) n| ≤
    ‖embeddingOfSubset x b - embeddingOfSubset x a‖
⊢ |(↑(embeddingOfSubset x b) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n -
        (↑(embeddingOfSubset x a) : (i : ℕ) → (fun (x : ℕ) ↦ ℝ) i) n| ≤
    dist (embeddingOfSubset x b) (embeddingOfSubset x a)

Tactic:
simp only [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
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 : ℕ) → ℝ) n - (↑(embeddingOfSubset x a) : (i : ℕ) → ℝ) n| ≤
    ‖embeddingOfSubset x b - embeddingOfSubset x a‖

Tactic:
lp.norm_apply_le_norm ENNReal.top_ne_zero
          (embeddingOfSubset x b - embeddingOfSubset x a) n

Premises used: lp.norm_apply_le_norm, ENNReal.ofNNReal, Set.Mem, setOf, HSub.hSub, WithTop.some, ENNReal.top_ne_zero, KuratowskiEmbedding.embeddingOfSubset
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
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 : ℕ) → ℝ) n - (↑(embeddingOfSubset x a) : (i : ℕ) → ℝ) n| ≤
    ‖embeddingOfSubset x b - embeddingOfSubset x a‖

Tactic:
exact lp.norm_apply_le_norm ENNReal.top_ne_zero
          (embeddingOfSubset x b - embeddingOfSubset x a) n

Premises used: lp.norm_apply_le_norm, HSub.hSub, ENNReal.top_ne_zero, KuratowskiEmbedding.embeddingOfSubset
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
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) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) =
    dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e

Tactic:
ring
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
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 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
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
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
this : dist a b ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e

Tactic:
simpa [dist_comm] using this

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
inl : ∀ (h : Eq.{u + 1} (α := Set α) univ ∅), ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
inr : ∀ (h : Set.Nonempty.{u} (α := α) univ), ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f

Tactic:
rcases (univ : Set α).eq_empty_or_nonempty with h | h

Premises used: Set.univ, Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) univ ∅
h₁ : Isometry (β := ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)) fun (x : α) ↦ 0
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f

Tactic:
use fun _ => 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) univ ∅
x : α
⊢ ∀ (x2 : α),
    edist (α := ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)) ((fun (x : α) ↦ (0 : ↥(lp (fun (x : ℕ) ↦ ℝ) ∞))) x)
        ((fun (x : α) ↦ (0 : ↥(lp (fun (x : ℕ) ↦ ℝ) ∞))) x2) =
      edist x x2

Tactic:
absurd h (Nonempty.ne_empty ⟨x, mem_univ x⟩)

Premises used: Set.Nonempty.ne_empty, absurd, Exists.intro, Set.mem_univ
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) univ ∅
x : α
⊢ ∀ (x2 : α),
    edist (α := ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)) ((fun (x : α) ↦ (0 : ↥(lp (fun (x : ℕ) ↦ ℝ) ∞))) x)
        ((fun (x : α) ↦ (0 : ↥(lp (fun (x : ℕ) ↦ ℝ) ∞))) x2) =
      edist x x2

Tactic:
exact absurd h (Nonempty.ne_empty ⟨x, mem_univ x⟩)

Premises used: Set.Nonempty.ne_empty, absurd, Exists.intro, Set.mem_univ
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
h : Set.Nonempty.{u} (α := α) univ
inr : ∀ (basepoint : α), Membership.mem (γ := Set α) univ basepoint → ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f

Tactic:
rcases h with ⟨basepoint⟩
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
basepoint : α
h : Membership.mem (γ := Set α) univ basepoint
inr : ∀ (this : Inhabited α), ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f
⊢ ∃ (f : α → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞)), Isometry f

Tactic:
haveI : Inhabited α := ⟨basepoint⟩
-- Module: Mathlib.Topology.MetricSpace.Kuratowski
Goal:
α : Type u
inst : MetricSpace α
inst_1 : SeparableSpace α
basepoint : α
h : Membership.mem (γ := Set α) univ basepoint
this : Inhabited α
⊢ ∃ (s : Set α), s.Countable ∧ Dense s

Tactic:
have : ∃ s : Set α, s.Countable ∧ Dense s := exists_countable_dense α