α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
⊢ ε ≤
    ↑(abs
        (edgeDensity G
            (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd)
            (if WellOrderingRel t s then (nonuniformWitnesses G ε t s).fst else (nonuniformWitnesses G ε s t).snd) -
          edgeDensity G s t))
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
⊢ ε ≤ ↑(abs (edgeDensity G (nonuniformWitness G ε s t) (nonuniformWitness G ε t s) - edgeDensity G s t))
unfold nonuniformWitness
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
lt : WellOrderingRel s t
⊢ ε ≤
    ↑(abs
        (edgeDensity G
            (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd)
            (if WellOrderingRel t s then (nonuniformWitnesses G ε t s).fst else (nonuniformWitnesses G ε s t).snd) -
          edgeDensity G s t))

case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s : Finset α
a b : α
h₁ : s ≠ s
h₂ : ¬IsUniform G ε s s
⊢ ε ≤
    ↑(abs
        (edgeDensity G
            (if WellOrderingRel s s then (nonuniformWitnesses G ε s s).fst else (nonuniformWitnesses G ε s s).snd)
            (if WellOrderingRel s s then (nonuniformWitnesses G ε s s).fst else (nonuniformWitnesses G ε s s).snd) -
          edgeDensity G s s))

case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
gt : WellOrderingRel t s
⊢ ε ≤
    ↑(abs
        (edgeDensity G
            (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd)
            (if WellOrderingRel t s then (nonuniformWitnesses G ε t s).fst else (nonuniformWitnesses G ε s t).snd) -
          edgeDensity G s t))
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
⊢ ε ≤
    ↑(abs
        (edgeDensity G
            (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd)
            (if WellOrderingRel t s then (nonuniformWitnesses G ε t s).fst else (nonuniformWitnesses G ε s t).snd) -
          edgeDensity G s t))
rcases trichotomous_of WellOrderingRel s t with (lt | rfl | gt)
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
lt : WellOrderingRel s t
⊢ ε ≤ ↑(abs (edgeDensity G (nonuniformWitnesses G ε s t).fst (nonuniformWitnesses G ε s t).snd - edgeDensity G s t))
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
lt : WellOrderingRel s t
⊢ ε ≤
    ↑(abs
        (edgeDensity G
            (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd)
            (if WellOrderingRel t s then (nonuniformWitnesses G ε t s).fst else (nonuniformWitnesses G ε s t).snd) -
          edgeDensity G s t))
rw [if_pos lt, if_neg (asymm lt)]
no goals
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
lt : WellOrderingRel s t
⊢ ε ≤ ↑(abs (edgeDensity G (nonuniformWitnesses G ε s t).fst (nonuniformWitnesses G ε s t).snd - edgeDensity G s t))
exact G.nonuniformWitnesses_spec h₂
no goals
case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s : Finset α
a b : α
h₁ : s ≠ s
h₂ : ¬IsUniform G ε s s
⊢ ε ≤
    ↑(abs
        (edgeDensity G
            (if WellOrderingRel s s then (nonuniformWitnesses G ε s s).fst else (nonuniformWitnesses G ε s s).snd)
            (if WellOrderingRel s s then (nonuniformWitnesses G ε s s).fst else (nonuniformWitnesses G ε s s).snd) -
          edgeDensity G s s))
cases h₁ rfl
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
gt : WellOrderingRel t s
⊢ ε ≤ ↑(abs (edgeDensity G (nonuniformWitnesses G ε t s).fst (nonuniformWitnesses G ε t s).snd - edgeDensity G t s))
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
gt : WellOrderingRel t s
⊢ ε ≤
    ↑(abs
        (edgeDensity G
            (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd)
            (if WellOrderingRel t s then (nonuniformWitnesses G ε t s).fst else (nonuniformWitnesses G ε s t).snd) -
          edgeDensity G s t))
rw [if_neg (asymm gt), if_pos gt, edgeDensity_comm, edgeDensity_comm _ s]
no goals
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h₁ : s ≠ t
h₂ : ¬IsUniform G ε s t
gt : WellOrderingRel t s
⊢ ε ≤ ↑(abs (edgeDensity G (nonuniformWitnesses G ε t s).fst (nonuniformWitnesses G ε t s).snd - edgeDensity G t s))
apply G.nonuniformWitnesses_spec fun i => h₂ i.symm