α : 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 t) * ε ≤
    ↑(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))),
            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)))).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 t) * ε ≤ ↑(card (nonuniformWitnesses G ε s t).snd)
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
⊢ ↑(card t) * ε ≤
    ↑(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))),
            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)))).snd)
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.2.1