no goals
f✝ g f g₁ g₂ : CircleDeg1Lift
h : Semiconj ↑f ↑g₁ ↑g₂
⊢ dist (↑g₁ 0) (↑f (↑g₁ 0) - ↑f 0) + dist (↑f (↑g₁ 0) - ↑f 0) (↑g₂ 0) =
    dist (↑f 0 + ↑g₁ 0) (↑f (↑g₁ 0)) + dist (↑g₂ 0 + ↑f 0) (↑g₂ (↑f 0))
simp only [h.eq, Real.dist_eq, sub_sub, add_comm (f 0), sub_sub_eq_add_sub,
  abs_sub_comm (g₂ (f 0))]