Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case h.«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
j : Fin (Nat.succ 0).succ.succ
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] j) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] j)

pp: case h.«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
j : Fin (Nat.succ 0).succ.succ
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] j) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] j)

pp: case h.«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
j : Fin (Nat.succ 0).succ.succ
hij : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] j) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] j)

Tactic:
<;>

Goal state after:
case h.«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
j : Fin (Nat.succ 0).succ.succ
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] j) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] j)

case h.«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
j : Fin (Nat.succ 0).succ.succ
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] j) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] j)

case h.«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
j : Fin (Nat.succ 0).succ.succ
hij : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] j) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] j)