Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case h.«0».«0»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case h.«0».«1»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

pp: case h.«0».«2»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))

pp: case h.«1».«0»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case h.«1».«1»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

pp: case h.«1».«2»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))

pp: case h.«2».«0»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case h.«2».«1»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

pp: case h.«2».«2»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))

Tactic:
<;>

Goal state after:
case h.«0».«0»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

case h.«0».«1»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

case h.«0».«2»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))

case h.«1».«0»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

case h.«1».«1»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

case h.«1».«2»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))

case h.«2».«0»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

case h.«2».«1»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

case h.«2».«2»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))