α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ ↑(card s) * ε ≤
    ↑(card (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd))
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ ↑(card s) * ε ≤ ↑(card (nonuniformWitness 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 : ¬IsUniform G ε s t
h✝ : WellOrderingRel s t
⊢ ↑(card s) * ε ≤ ↑(card (nonuniformWitnesses G ε s t).fst)

case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
h✝ : ¬WellOrderingRel s t
⊢ ↑(card s) * ε ≤ ↑(card (nonuniformWitnesses G ε t s).snd)
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ ↑(card s) * ε ≤
    ↑(card (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd))
split_ifs
no goals
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
h✝ : WellOrderingRel s t
⊢ ↑(card s) * ε ≤ ↑(card (nonuniformWitnesses G ε s t).fst)
exact G.left_nonuniformWitnesses_card h
no goals
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
h✝ : ¬WellOrderingRel s t
⊢ ↑(card s) * ε ≤ ↑(card (nonuniformWitnesses G ε t s).snd)
exact G.right_nonuniformWitnesses_card fun i => h i.symm