[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
ε' : 𝕜
h : ε ≤ ε'
hε : IsUniform G ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) * ε' ≤ ↑(card s')
ht : ↑(card t) * ε' ≤ ↑(card t')
⊢ |↑(edgeDensity G s' t') - ↑(edgeDensity G s t)| < ε'
[PROOFSTEP]
refine' (hε hs' ht' (le_trans _ hs) (le_trans _ ht)).trans_le h
[GOAL]
case refine'_1
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
ε' : 𝕜
h : ε ≤ ε'
hε : IsUniform G ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) * ε' ≤ ↑(card s')
ht : ↑(card t) * ε' ≤ ↑(card t')
⊢ ↑(card s) * ε ≤ ↑(card s) * ε'
[PROOFSTEP]
gcongr
[GOAL]
case refine'_2
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
ε' : 𝕜
h : ε ≤ ε'
hε : IsUniform G ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) * ε' ≤ ↑(card s')
ht : ↑(card t) * ε' ≤ ↑(card t')
⊢ ↑(card t) * ε ≤ ↑(card t) * ε'
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s✝ t✝ : Finset α
a b : α
s t : Finset α
h : IsUniform G ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : ↑(card t) * ε ≤ ↑(card t')
hs : ↑(card s) * ε ≤ ↑(card s')
⊢ |↑(edgeDensity G t' s') - ↑(edgeDensity G t s)| < ε
[PROOFSTEP]
rw [edgeDensity_comm _ t', edgeDensity_comm _ t]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s✝ t✝ : Finset α
a b : α
s t : Finset α
h : IsUniform G ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : ↑(card t) * ε ≤ ↑(card t')
hs : ↑(card s) * ε ≤ ↑(card s')
⊢ |↑(edgeDensity G s' t') - ↑(edgeDensity G s t)| < ε
[PROOFSTEP]
exact h hs' ht' hs ht
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
⊢ IsUniform G ε {a} {b}
[PROOFSTEP]
intro s' hs' t' ht' hs ht
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ↑(card {a}) * ε ≤ ↑(card s')
ht : ↑(card {b}) * ε ≤ ↑(card t')
⊢ |↑(edgeDensity G s' t') - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
rw [card_singleton, Nat.cast_one, one_mul] at hs ht 
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ε ≤ ↑(card s')
ht : ε ≤ ↑(card t')
⊢ |↑(edgeDensity G s' t') - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
obtain rfl | rfl := Finset.subset_singleton_iff.1 hs'
[GOAL]
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : ∅ ⊆ {a}
hs : ε ≤ ↑(card ∅)
⊢ |↑(edgeDensity G ∅ t') - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
replace hs : ε ≤ 0 := by simpa using hs
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : ∅ ⊆ {a}
hs : ε ≤ ↑(card ∅)
⊢ ε ≤ 0
[PROOFSTEP]
simpa using hs
[GOAL]
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : ∅ ⊆ {a}
hs : ε ≤ 0
⊢ |↑(edgeDensity G ∅ t') - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
exact (hε.not_le hs).elim
[GOAL]
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(card t')
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
⊢ |↑(edgeDensity G {a} t') - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
obtain rfl | rfl := Finset.subset_singleton_iff.1 ht'
[GOAL]
case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : ∅ ⊆ {b}
ht : ε ≤ ↑(card ∅)
⊢ |↑(edgeDensity G {a} ∅) - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
replace ht : ε ≤ 0 := by simpa using ht
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : ∅ ⊆ {b}
ht : ε ≤ ↑(card ∅)
⊢ ε ≤ 0
[PROOFSTEP]
simpa using ht
[GOAL]
case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : ∅ ⊆ {b}
ht : ε ≤ 0
⊢ |↑(edgeDensity G {a} ∅) - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
exact (hε.not_le ht).elim
[GOAL]
case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(card {a})
ht' : {b} ⊆ {b}
ht : ε ≤ ↑(card {b})
⊢ |↑(edgeDensity G {a} {b}) - ↑(edgeDensity G {a} {b})| < ε
[PROOFSTEP]
rwa [sub_self, abs_zero]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : IsUniform G 0 s t
⊢ ↑(card s) * 0 ≤ ↑(card ∅)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : IsUniform G 0 s t
⊢ ↑(card t) * 0 ≤ ↑(card ∅)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
⊢ IsUniform G 1 s t
[PROOFSTEP]
intro s' hs' t' ht' hs ht
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) * 1 ≤ ↑(card s')
ht : ↑(card t) * 1 ≤ ↑(card t')
⊢ |↑(edgeDensity G s' t') - ↑(edgeDensity G s t)| < 1
[PROOFSTEP]
rw [mul_one] at hs ht 
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) ≤ ↑(card s')
ht : ↑(card t) ≤ ↑(card t')
⊢ |↑(edgeDensity G s' t') - ↑(edgeDensity G s t)| < 1
[PROOFSTEP]
rw [eq_of_subset_of_card_le hs' (Nat.cast_le.1 hs), eq_of_subset_of_card_le ht' (Nat.cast_le.1 ht), sub_self, abs_zero]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(card s) ≤ ↑(card s')
ht : ↑(card t) ≤ ↑(card t')
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
⊢ ¬IsUniform G ε s t ↔
    ∃ s',
      s' ⊆ s ∧
        ∃ t',
          t' ⊆ t ∧
            ↑(card s) * ε ≤ ↑(card s') ∧ ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|
[PROOFSTEP]
unfold IsUniform
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
⊢ (¬∀ ⦃s' : Finset α⦄,
        s' ⊆ s →
          ∀ ⦃t' : Finset α⦄,
            t' ⊆ t →
              ↑(card s) * ε ≤ ↑(card s') →
                ↑(card t) * ε ≤ ↑(card t') → |↑(edgeDensity G s' t') - ↑(edgeDensity G s t)| < ε) ↔
    ∃ s',
      s' ⊆ s ∧
        ∃ t',
          t' ⊆ t ∧
            ↑(card s) * ε ≤ ↑(card s') ∧ ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|
[PROOFSTEP]
simp only [not_forall, not_lt, exists_prop, exists_and_left, Rat.cast_abs, Rat.cast_sub]
[GOAL]
α : 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
[PROOFSTEP]
rw [nonuniformWitnesses, dif_pos h]
[GOAL]
α : 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') ∧ ε ≤ ↑|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') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))) ∧
                  ↑(card t) * ε ≤ ↑(card t') ∧
                    ε ≤
                      ↑|edgeDensity G
                              (Exists.choose
                                (_ :
                                  ∃ s',
                                    s' ⊆ s ∧
                                      ∃ t',
                                        t' ⊆ t ∧
                                          ↑(card s) * ε ≤ ↑(card s') ∧
                                            ↑(card t) * ε ≤ ↑(card t') ∧
                                              ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))
                              t' -
                            edgeDensity G s t|)).fst ⊆
    s
[PROOFSTEP]
exact (not_isUniform_iff.1 h).choose_spec.1
[GOAL]
α : 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 (nonuniformWitnesses G ε s t).fst)
[PROOFSTEP]
rw [nonuniformWitnesses, dif_pos h]
[GOAL]
α : 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
        (Exists.choose
              (_ :
                ∃ s',
                  s' ⊆ s ∧
                    ∃ t',
                      t' ⊆ t ∧
                        ↑(card s) * ε ≤ ↑(card s') ∧
                          ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|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') ∧
                                            ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))) ∧
                      ↑(card t) * ε ≤ ↑(card t') ∧
                        ε ≤
                          ↑|edgeDensity G
                                  (Exists.choose
                                    (_ :
                                      ∃ s',
                                        s' ⊆ s ∧
                                          ∃ t',
                                            t' ⊆ t ∧
                                              ↑(card s) * ε ≤ ↑(card s') ∧
                                                ↑(card t) * ε ≤ ↑(card t') ∧
                                                  ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))
                                  t' -
                                edgeDensity G s t|)).fst)
[PROOFSTEP]
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.1
[GOAL]
α : 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).snd ⊆ t
[PROOFSTEP]
rw [nonuniformWitnesses, dif_pos h]
[GOAL]
α : 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') ∧ ε ≤ ↑|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') ∧ ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))) ∧
                  ↑(card t) * ε ≤ ↑(card t') ∧
                    ε ≤
                      ↑|edgeDensity G
                              (Exists.choose
                                (_ :
                                  ∃ s',
                                    s' ⊆ s ∧
                                      ∃ t',
                                        t' ⊆ t ∧
                                          ↑(card s) * ε ≤ ↑(card s') ∧
                                            ↑(card t) * ε ≤ ↑(card t') ∧
                                              ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))
                              t' -
                            edgeDensity G s t|)).snd ⊆
    t
[PROOFSTEP]
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.1
[GOAL]
α : 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)
[PROOFSTEP]
rw [nonuniformWitnesses, dif_pos h]
[GOAL]
α : 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') ∧ ε ≤ ↑|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') ∧
                                            ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))) ∧
                      ↑(card t) * ε ≤ ↑(card t') ∧
                        ε ≤
                          ↑|edgeDensity G
                                  (Exists.choose
                                    (_ :
                                      ∃ s',
                                        s' ⊆ s ∧
                                          ∃ t',
                                            t' ⊆ t ∧
                                              ↑(card s) * ε ≤ ↑(card s') ∧
                                                ↑(card t) * ε ≤ ↑(card t') ∧
                                                  ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))
                                  t' -
                                edgeDensity G s t|)).snd)
[PROOFSTEP]
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.2.1
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ ε ≤ ↑|edgeDensity G (nonuniformWitnesses G ε s t).fst (nonuniformWitnesses G ε s t).snd - edgeDensity G s t|
[PROOFSTEP]
rw [nonuniformWitnesses, dif_pos h]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
a b : α
h : ¬IsUniform G ε s t
⊢ ε ≤
    ↑|edgeDensity G
            (Exists.choose
                  (_ :
                    ∃ s',
                      s' ⊆ s ∧
                        ∃ t',
                          t' ⊆ t ∧
                            ↑(card s) * ε ≤ ↑(card s') ∧
                              ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|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') ∧
                                                ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))) ∧
                          ↑(card t) * ε ≤ ↑(card t') ∧
                            ε ≤
                              ↑|edgeDensity G
                                      (Exists.choose
                                        (_ :
                                          ∃ s',
                                            s' ⊆ s ∧
                                              ∃ t',
                                                t' ⊆ t ∧
                                                  ↑(card s) * ε ≤ ↑(card s') ∧
                                                    ↑(card t) * ε ≤ ↑(card t') ∧
                                                      ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))
                                      t' -
                                    edgeDensity G s t|)).fst
            (Exists.choose
                  (_ :
                    ∃ s',
                      s' ⊆ s ∧
                        ∃ t',
                          t' ⊆ t ∧
                            ↑(card s) * ε ≤ ↑(card s') ∧
                              ↑(card t) * ε ≤ ↑(card t') ∧ ε ≤ ↑|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') ∧
                                                ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))) ∧
                          ↑(card t) * ε ≤ ↑(card t') ∧
                            ε ≤
                              ↑|edgeDensity G
                                      (Exists.choose
                                        (_ :
                                          ∃ s',
                                            s' ⊆ s ∧
                                              ∃ t',
                                                t' ⊆ t ∧
                                                  ↑(card s) * ε ≤ ↑(card s') ∧
                                                    ↑(card t) * ε ≤ ↑(card t') ∧
                                                      ε ≤ ↑|edgeDensity G s' t' - edgeDensity G s t|))
                                      t' -
                                    edgeDensity G s t|)).snd -
          edgeDensity G s t|
[PROOFSTEP]
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.2.2
[GOAL]
α : 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
[PROOFSTEP]
unfold nonuniformWitness
[GOAL]
α : 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
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : 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
[PROOFSTEP]
exact G.left_nonuniformWitnesses_subset h
[GOAL]
case neg
α : 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
[PROOFSTEP]
exact G.right_nonuniformWitnesses_subset fun i => h i.symm
[GOAL]
α : 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))
[PROOFSTEP]
unfold nonuniformWitness
[GOAL]
α : 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))
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : 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)
[PROOFSTEP]
exact G.left_nonuniformWitnesses_card h
[GOAL]
case neg
α : 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)
[PROOFSTEP]
exact G.right_nonuniformWitnesses_card fun i => h i.symm
[GOAL]
α : 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
⊢ ε ≤ ↑|edgeDensity G (nonuniformWitness G ε s t) (nonuniformWitness G ε t s) - edgeDensity G s t|
[PROOFSTEP]
unfold nonuniformWitness
[GOAL]
α : 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
⊢ ε ≤
    ↑|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|
[PROOFSTEP]
rcases trichotomous_of WellOrderingRel s t with (lt | rfl | gt)
[GOAL]
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
⊢ ε ≤
    ↑|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|
[PROOFSTEP]
rw [if_pos lt, if_neg (asymm lt)]
[GOAL]
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
⊢ ε ≤ ↑|edgeDensity G (nonuniformWitnesses G ε s t).fst (nonuniformWitnesses G ε s t).snd - edgeDensity G s t|
[PROOFSTEP]
exact G.nonuniformWitnesses_spec h₂
[GOAL]
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
⊢ ε ≤
    ↑|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|
[PROOFSTEP]
cases h₁ rfl
[GOAL]
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
⊢ ε ≤
    ↑|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|
[PROOFSTEP]
rw [if_neg (asymm gt), if_pos gt, edgeDensity_comm, edgeDensity_comm _ s]
[GOAL]
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
⊢ ε ≤ ↑|edgeDensity G (nonuniformWitnesses G ε t s).fst (nonuniformWitnesses G ε t s).snd - edgeDensity G t s|
[PROOFSTEP]
apply G.nonuniformWitnesses_spec fun i => h₂ i.symm
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε✝ : 𝕜
u v : Finset α
ε : 𝕜
⊢ (u, v) ∈ nonUniforms P G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬SimpleGraph.IsUniform G ε u v
[PROOFSTEP]
rw [nonUniforms, mem_filter, mem_offDiag, and_assoc, and_assoc]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ nonUniforms ⊥ G ε = ∅
[PROOFSTEP]
rw [eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ ∀ (x : Finset α × Finset α), ¬x ∈ nonUniforms ⊥ G ε
[PROOFSTEP]
rintro ⟨u, v⟩
[GOAL]
case mk
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ¬(u, v) ∈ nonUniforms ⊥ G ε
[PROOFSTEP]
simp only [Finpartition.mk_mem_nonUniforms_iff, Finpartition.parts_bot, mem_map, not_and, Classical.not_not, exists_imp]
[GOAL]
case mk
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ∀ (x : α),
    x ∈ A ∧ ↑{ toFun := singleton, inj' := (_ : Function.Injective singleton) } x = u →
      ∀ (x : α),
        x ∈ A ∧ ↑{ toFun := singleton, inj' := (_ : Function.Injective singleton) } x = v →
          u ≠ v → SimpleGraph.IsUniform G ε u v
[PROOFSTEP]
dsimp
[GOAL]
case mk
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ∀ (x : α), x ∈ A ∧ {x} = u → ∀ (x : α), x ∈ A ∧ {x} = v → ¬u = v → SimpleGraph.IsUniform G ε u v
[PROOFSTEP]
rintro x ⟨_, xu⟩ y ⟨_, yv⟩ _
[GOAL]
case mk.intro.intro
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
x : α
left✝¹ : x ∈ A
xu : {x} = u
y : α
left✝ : y ∈ A
yv : {y} = v
a✝ : ¬u = v
⊢ SimpleGraph.IsUniform G ε u v
[PROOFSTEP]
rw [← xu, ← yv]
[GOAL]
case mk.intro.intro
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
x : α
left✝¹ : x ∈ A
xu : {x} = u
y : α
left✝ : y ∈ A
yv : {y} = v
a✝ : ¬u = v
⊢ SimpleGraph.IsUniform G ε {x} {y}
[PROOFSTEP]
exact G.isUniform_singleton hε
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ IsUniform ⊥ G ε
[PROOFSTEP]
rw [Finpartition.IsUniform, Finpartition.card_bot, nonUniforms_bot _ hε, Finset.card_empty, Nat.cast_zero]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ 0 ≤ ↑(card A * (card A - 1)) * ε
[PROOFSTEP]
exact mul_nonneg (Nat.cast_nonneg _) hε.le
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
⊢ IsUniform P G 1
[PROOFSTEP]
rw [IsUniform, mul_one, Nat.cast_le]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
⊢ card (nonUniforms P G 1) ≤ card P.parts * (card P.parts - 1)
[PROOFSTEP]
refine' (card_filter_le _ (fun uv => ¬SimpleGraph.IsUniform G 1 (Prod.fst uv) (Prod.snd uv))).trans _
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
⊢ card (offDiag P.parts) ≤ card P.parts * (card P.parts - 1)
[PROOFSTEP]
rw [offDiag_card, Nat.mul_sub_left_distrib, mul_one]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε✝ ε ε' : 𝕜
hP : IsUniform P G ε
h : ε ≤ ε'
⊢ ↑(card P.parts * (card P.parts - 1)) * ε ≤ ↑(card P.parts * (card P.parts - 1)) * ε'
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.parts = ∅
⊢ IsUniform P G ε
[PROOFSTEP]
simp [IsUniform, hP, nonUniforms]
