-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
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
⊢ ε ≤ (↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t| : 𝕜)
have rw : ε ≤
  (↑|G.edgeDensity
            (sorry.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) : 𝕜) * ε ≤
                        (↑(#(sorry.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
                                    (sorry.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| :
                            𝕜))
                  sorry).1
            (sorry.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) : 𝕜) * ε ≤
                        (↑(#(sorry.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
                                    (sorry.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| :
                            𝕜))
                  sorry).2 -
          G.edgeDensity s t| :
    𝕜)
Tactic: rw [nonuniformWitnesses, dif_pos h]