Module: Mathlib.Geometry.Euclidean.Congruence

Goal state before:
pp: P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
i j : Fin 3
⊢ dist (![a, b, c] i) (![a, b, c] j) = dist (![a', b', c'] i) (![a', b', c'] j)

Tactic:
fin_cases i <;> fin_cases j

Goal state after:
case «0».«0»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

case «0».«1»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

case «0».«2»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))

case «1».«0»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

case «1».«1»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

case «1».«2»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))

case «2».«0»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

case «2».«1»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

case «2».«2»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))