α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ (Exists.choose
          (_ :
            ∃ s',
              s' ⊆ s ∧
                ∃ t',
                  t' ⊆ t ∧
                    ↑(card s) * ε ≤ ↑(card s') ∧
                      ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑(abs (edgeDensity G s' t' - edgeDensity G s t))),
        Exists.choose
          (_ :
            ∃ t',
              t' ⊆ t ∧
                ↑(card s) * ε ≤
                    ↑(card
                        (Exists.choose
                          (_ :
                            ∃ s',
                              s' ⊆ s ∧
                                ∃ t',
                                  t' ⊆ t ∧
                                    ↑(card s) * ε ≤ ↑(card s') ∧
                                      ↑(card t) * ε ≤ ↑(card t') ∧
                                        ε ≤ ↑(abs (edgeDensity G s' t' - edgeDensity G s t))))) ∧
                  ↑(card t) * ε ≤ ↑(card t') ∧
                    ε ≤
                      ↑(abs
                          (edgeDensity G
                              (Exists.choose
                                (_ :
                                  ∃ s',
                                    s' ⊆ s ∧
                                      ∃ t',
                                        t' ⊆ t ∧
                                          ↑(card s) * ε ≤ ↑(card s') ∧
                                            ↑(card t) * ε ≤ ↑(card t') ∧
                                              ε ≤ ↑(abs (edgeDensity G s' t' - edgeDensity G s t))))
                              t' -
                            edgeDensity G s t)))).fst ⊆
    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
⊢ (nonuniformWitnesses G ε s t).fst ⊆ s
rw [nonuniformWitnesses, dif_pos h]
no goals
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ (Exists.choose
          (_ :
            ∃ s',
              s' ⊆ s ∧
                ∃ t',
                  t' ⊆ t ∧
                    ↑(card s) * ε ≤ ↑(card s') ∧
                      ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑(abs (edgeDensity G s' t' - edgeDensity G s t))),
        Exists.choose
          (_ :
            ∃ t',
              t' ⊆ t ∧
                ↑(card s) * ε ≤
                    ↑(card
                        (Exists.choose
                          (_ :
                            ∃ s',
                              s' ⊆ s ∧
                                ∃ t',
                                  t' ⊆ t ∧
                                    ↑(card s) * ε ≤ ↑(card s') ∧
                                      ↑(card t) * ε ≤ ↑(card t') ∧
                                        ε ≤ ↑(abs (edgeDensity G s' t' - edgeDensity G s t))))) ∧
                  ↑(card t) * ε ≤ ↑(card t') ∧
                    ε ≤
                      ↑(abs
                          (edgeDensity G
                              (Exists.choose
                                (_ :
                                  ∃ s',
                                    s' ⊆ s ∧
                                      ∃ t',
                                        t' ⊆ t ∧
                                          ↑(card s) * ε ≤ ↑(card s') ∧
                                            ↑(card t) * ε ≤ ↑(card t') ∧
                                              ε ≤ ↑(abs (edgeDensity G s' t' - edgeDensity G s t))))
                              t' -
                            edgeDensity G s t)))).fst ⊆
    s
exact (not_isUniform_iff.1 h).choose_spec.1