Apparent equality... but cannot conclude it

Stream: mathlib4

[H Segawa]

hello...im newbie to lean

my innocent brain tells these are apparently equal, but cannot prove it.

⊢ ⟨|-x' 0 + y' 0|, ⋯⟩ = ⟨|x' 0 - y' 0|, ⋯⟩

but cannot prove the equality

import Mathlib.Data.Real.Basic
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Tactic.FinCases
import Mathlib.Analysis.ODE.Gronwall

--set_option pp.proofs true

open Metric Real
open scoped NNReal Matrix Fintype

example {t a: ℝ}{m : Matrix (Fin 2) (Fin 2) ℝ}
  (hm : m = (![![0,1],![-1,0]]: Matrix (Fin 2) (Fin 2) ℝ))
    :
     LipschitzWith 1 ((fun t'' v  => m *ᵥ v) t') := by
    rw[LipschitzWith]
    intro x' y'
    have ⟨ hx , hy ⟩ : x' = ![x' 0 , x' 1] ∧ y' = ![y' 0, y' 1] := by
      constructor <;> ext i <;> fin_cases i <;> simp
    rw[hx,hy]
    rw[hm]
    repeat dsimp[edist]
    repeat simp[PseudoEMetricSpace.toEDist]
    repeat dsimp[PseudoMetricSpace.edist]
    intro i
    fin_cases i
    -- subproof
    simp[Matrix.mulVec]
    apply Finset.le_sup_of_le
    change 1 ∈ (Fin.fintype 2).1
    rw[Fintype.elems]
    apply Finset.insert_eq_self.mp rfl
    simp
    -- subproof
    simp[Matrix.mulVec]
    apply Finset.le_sup_of_le
    change 0 ∈ (Fin.fintype 2).1
    rw[Fintype.elems]
    apply Finset.insert_eq_self.mp rfl
    simp
    apply le_of_eq
    admit

[Vincent Beffara]

import Mathlib.Data.Real.Basic
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Tactic.FinCases
import Mathlib.Analysis.ODE.Gronwall
--set_option pp.proofs true

open Metric Real
open scoped NNReal Matrix Fintype

example {t a: ℝ}{m : Matrix (Fin 2) (Fin 2) ℝ}
  (hm : m = (![![0,1],![-1,0]]: Matrix (Fin 2) (Fin 2) ℝ))
    :
     LipschitzWith 1 ((fun t'' v  => m *ᵥ v) t') := by
    rw[LipschitzWith]
    intro x' y'
    have ⟨ hx , hy ⟩ : x' = ![x' 0 , x' 1] ∧ y' = ![y' 0, y' 1] := by
      constructor <;> ext i <;> fin_cases i <;> simp
    rw[hx,hy]
    rw[hm]
    repeat dsimp[edist]
    repeat simp[PseudoEMetricSpace.toEDist]
    repeat dsimp[PseudoMetricSpace.edist]
    intro i
    fin_cases i
    -- subproof
    simp[Matrix.mulVec]
    apply Finset.le_sup_of_le
    change 1 ∈ (Fin.fintype 2).1
    rw[Fintype.elems]
    apply Finset.insert_eq_self.mp rfl
    simp
    -- subproof
    simp[Matrix.mulVec]
    apply Finset.le_sup_of_le
    change 0 ∈ (Fin.fintype 2).1
    rw[Fintype.elems]
    apply Finset.insert_eq_self.mp rfl
    simp
    apply le_of_eq

    congr 1
    apply abs_eq_abs.mpr
    ring_nf
    simp

[H Segawa]

Thank you.
congr 1 is the key to the equality.