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

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
⊢ (nonuniformWitnesses G ε t s).snd ⊆ s
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ (if WellOrderingRel s t then (nonuniformWitnesses G ε s t).fst else (nonuniformWitnesses G ε t s).snd) ⊆ s
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
⊢ (nonuniformWitnesses G ε s t).fst ⊆ s
exact G.left_nonuniformWitnesses_subset 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
⊢ (nonuniformWitnesses G ε t s).snd ⊆ s
exact G.right_nonuniformWitnesses_subset fun i => h i.symm