-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
rw :
  ε ≤
    (↑|G.edgeDensity
              (⋯.choose (p := fun (s' : Finset α) ↦
                    s' ⊆ s ∧
                      ∃ t' ⊆ t,
                        (↑(#s) : 𝕜) * ε ≤ (↑(#s') : 𝕜) ∧
                          (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜) ∧ ε ≤ (↑|G.edgeDensity s' t' - G.edgeDensity s t| : 𝕜)),
                  Exists.choose (p := fun (t' : Finset α) ↦
                    t' ⊆ t ∧
                      (↑(#s) : 𝕜) * ε ≤
                          (↑(#(⋯.choose (p := fun (s' : Finset α) ↦
                                  s' ⊆ s ∧
                                    ∃ t' ⊆ t,
                                      (↑(#s) : 𝕜) * ε ≤ (↑(#s') : 𝕜) ∧
                                        (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜) ∧
                                          ε ≤ (↑|G.edgeDensity s' t' - G.edgeDensity s t| : 𝕜)))) :
                            𝕜) ∧
                        (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜) ∧
                          ε ≤
                            (↑|G.edgeDensity
                                      (⋯.choose (p := fun (s' : Finset α) ↦
                                        s' ⊆ s ∧
                                          ∃ t' ⊆ t,
                                            (↑(#s) : 𝕜) * ε ≤ (↑(#s') : 𝕜) ∧
                                              (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜) ∧
                                                ε ≤ (↑|G.edgeDensity s' t' - G.edgeDensity s t| : 𝕜)))
                                      t' -
                                    G.edgeDensity s t| :
                              𝕜))
                    ⋯).1
              (⋯.choose (p := fun (s' : Finset α) ↦
                    s' ⊆ s ∧
                      ∃ t' ⊆ t,
                        (↑(#s) : 𝕜) * ε ≤ (↑(#s') : 𝕜) ∧
                          (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜) ∧ ε ≤ (↑|G.edgeDensity s' t' - G.edgeDensity s t| : 𝕜)),
                  Exists.choose (p := fun (t' : Finset α) ↦
                    t' ⊆ t ∧
                      (↑(#s) : 𝕜) * ε ≤
                          (↑(#(⋯.choose (p := fun (s' : Finset α) ↦
                                  s' ⊆ s ∧
                                    ∃ t' ⊆ t,
                                      (↑(#s) : 𝕜) * ε ≤ (↑(#s') : 𝕜) ∧
                                        (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜) ∧
                                          ε ≤ (↑|G.edgeDensity s' t' - G.edgeDensity s t| : 𝕜)))) :
                            𝕜) ∧
                        (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜) ∧
                          ε ≤
                            (↑|G.edgeDensity
                                      (⋯.choose (p := fun (s' : Finset α) ↦
                                        s' ⊆ s ∧
                                          ∃ t' ⊆ t,
                                            (↑(#s) : 𝕜) * ε ≤ (↑(#s') : 𝕜) ∧
                                              (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜) ∧
                                                ε ≤ (↑|G.edgeDensity s' t' - G.edgeDensity s t| : 𝕜)))
                                      t' -
                                    G.edgeDensity s t| :
                              𝕜))
                    ⋯).2 -
            G.edgeDensity s t| :
      𝕜)
⊢ ε ≤ (↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t| : 𝕜)

Tactic:
rw [nonuniformWitnesses, dif_pos h]

Premises used: SimpleGraph.nonuniformWitnesses, dif_pos