∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ (ε ε_1 : 𝕜),
      ε = ε_1 →
        ∀ [inst_2 : Fintype α] {inst_3 : DecidableRel G.Adj} [inst_4 : DecidableRel G_1.Adj],
          G.FarFromTriangleFree ε = G_1.FarFromTriangleFree ε_1