-- Mathlib/Topology/MetricSpace/Kuratowski.lean
theorem embeddingOfSubset_isometry (H : DenseRange x) : Isometry (embeddingOfSubset x)

Proof state:
α : 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) n - ↑(embeddingOfSubset x a) 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:
apply_rules [add_le_add_left, le_abs_self]

Result:
no goals

Proof state:
α : 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) n - ↑(embeddingOfSubset x a) n
⊢ 2 * dist a (x n) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤
    2 * (e / 2) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n|

Tactic:
gcongr

Result:
no goals

Proof state:
case bc
α : 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) n - ↑(embeddingOfSubset x a) n
⊢ |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) 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

Result:
no goals

Proof state:
α : 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) n - ↑(embeddingOfSubset x a) 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]

Result:
α : 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) n - ↑(embeddingOfSubset x a) n
⊢ dist a (x n) + dist b (x n) = 2 * dist a (x n) + (dist b (x n) - dist a (x n))

Proof state:
α : 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) n - ↑(embeddingOfSubset x a) n

Tactic:
simp only [embeddingOfSubset_coe, sub_sub_sub_cancel_right]

Result:
no goals

Proof state:
case intro
α : 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

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]

Result:
case intro
α : 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) n - ↑(embeddingOfSubset x a) n
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e

Proof state:
case intro
α : 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) n - ↑(embeddingOfSubset x a) 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

Result:
no goals

Proof state:
α : 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) n - ↑(embeddingOfSubset x a) n
⊢ 2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) =
    dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e

Tactic:
ring

Result:
no goals

Proof state:
α : 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) n - ↑(embeddingOfSubset x a) n
⊢ dist a (x n) + dist b (x n) = 2 * dist a (x n) + (dist b (x n) - dist a (x n))

Tactic:
ring

Result:
no goals

Proof state:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
⊢ Isometry (embeddingOfSubset x)

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

Result:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) = dist a b

Proof state:
α : 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) n - ↑(embeddingOfSubset x a) n
⊢ 2 * dist a (x n) + |dist b (x n) - dist a (x n)| ≤
    2 * (e / 2) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n|

Tactic:
rw [C]

Result:
α : 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) n - ↑(embeddingOfSubset x a) n
⊢ 2 * dist a (x n) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤
    2 * (e / 2) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n|

Proof state:
α : 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) n - ↑(embeddingOfSubset x a) n
⊢ 2 * (e / 2) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤
    2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a)

Tactic:
gcongr

Result:
case bc
α : 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) n - ↑(embeddingOfSubset x a) n
⊢ |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a)

Proof state:
case bc
α : 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) n - ↑(embeddingOfSubset x a) n
⊢ |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a)

Tactic:
simp only [dist_eq_norm]

Result:
case bc
α : 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) n - ↑(embeddingOfSubset x a) n
⊢ |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤ ‖embeddingOfSubset x b - embeddingOfSubset x a‖

Proof state:
α : 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

Tactic:
rcases Metric.mem_closure_range_iff.1 (H a) (e / 2) (half_pos epos) with ⟨n, hn⟩

Result:
case intro
α : 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

Proof state:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
⊢ 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 => ?_)

Result:
α : 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