awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ (↑(#t') : 𝕜)
hs' : Subset (α := Finset α) {a} {a}
hs : ε ≤ (↑(card (α := α) {a}) : 𝕜)
inr :
  ∀ (ht' : Subset (α := Finset α) ∅ {b}) (ht : ε ≤ (↑(card.{u_1} (α := α) ∅) : 𝕜)),
    |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} ∅) : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
inr₁ :
  ∀ (ht' : Subset (α := Finset α) {b} {b}) (ht : ε ≤ (↑(card (α := α) {b}) : 𝕜)),
    |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε

Tactic:
obtain rfl | rfl := Finset.subset_singleton_iff.1 ht'

Premises used: Iff.mp, Finset.subset_singleton_iff, rfl
-- 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
ε : 𝕜
a b : α
hε : 0 < ε
hs' : Subset (α := Finset α) {a} {a}
hs : ε ≤ (↑(card (α := α) {a}) : 𝕜)
ht' : Subset (α := Finset α) ∅ {b}
ht : ε ≤ (↑(card.{u_1} (α := α) ∅) : 𝕜)
⊢ ε ≤ 0

Tactic:
simpa using ht
-- 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
ε : 𝕜
a b : α
hε : 0 < ε
hs' : Subset (α := Finset α) {a} {a}
hs : ε ≤ (↑(card (α := α) {a}) : 𝕜)
ht' : Subset (α := Finset α) ∅ {b}
ht : ε ≤ (↑(card.{u_1} (α := α) ∅) : 𝕜)
⊢ ε ≤ 0

Tactic:
replace ht : ε ≤ 0 := by simpa using ht
-- 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
ε : 𝕜
a b : α
hε : 0 < ε
hs' : Subset (α := Finset α) {a} {a}
hs : ε ≤ (↑(card (α := α) {a}) : 𝕜)
ht' : Subset (α := Finset α) ∅ {b}
ht : ε ≤ 0
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} ∅) : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε

Tactic:
(hε.not_ge ht).elim

Premises used: False.elim, LT.lt.not_ge
-- 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
ε : 𝕜
a b : α
hε : 0 < ε
hs' : Subset (α := Finset α) {a} {a}
hs : ε ≤ (↑(card (α := α) {a}) : 𝕜)
ht' : Subset (α := Finset α) ∅ {b}
ht : ε ≤ 0
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} ∅) : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε

Tactic:
exact (hε.not_ge ht).elim

Premises used: False.elim, LT.lt.not_ge
-- 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
ε : 𝕜
a b : α
hε : 0 < ε
hs' : Subset (α := Finset α) {a} {a}
hs : ε ≤ (↑(card (α := α) {a}) : 𝕜)
ht' : Subset (α := Finset α) {b} {b}
ht : ε ≤ (↑(card (α := α) {b}) : 𝕜)
inr : |0| < ε
inr₁ inr₂ inr₃ inr₄ : 0 < ε
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε

Tactic:
rwa [sub_self, abs_zero]

Premises used: sub_self, abs_zero
-- 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 : IsUniform.{u_1, u_2} (𝕜 := 𝕜) G 0 s t
⊢ HMul.hMul (α := 𝕜) (↑(#s) : 𝕜) 0 ≤ (↑(card.{u_1} (α := α) ∅) : 𝕜)

Tactic:
simp
-- 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 : IsUniform.{u_1, u_2} (𝕜 := 𝕜) G 0 s t
⊢ HMul.hMul (α := 𝕜) (↑(#t) : 𝕜) 0 ≤ (↑(card.{u_1} (α := α) ∅) : 𝕜)

Tactic:
simp
-- 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 α
⊢ (¬∀ ⦃s' : Finset α⦄,
        s' ⊆ s →
          ∀ ⦃t' : Finset α⦄,
            t' ⊆ t →
              (↑(#s) : 𝕜) * ε ≤ (↑(#s') : 𝕜) →
                (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜) →
                  |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity s t) : 𝕜)| < ε) ↔
    ∃ s' ⊆ s,
      ∃ t' ⊆ t,
        (↑(#s) : 𝕜) * ε ≤ (↑(#s') : 𝕜) ∧
          (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜) ∧ ε ≤ (↑|G.edgeDensity s' t' - G.edgeDensity s t| : 𝕜)

Tactic:
simp only [not_forall, not_lt, exists_prop, Rat.cast_abs, Rat.cast_sub]

Premises used: exists_prop, Rat.cast_abs, not_lt, Classical.not_forall, Rat.cast_sub
-- 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 :
  (⋯.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 ⊆
    s
⊢ (G.nonuniformWitnesses ε s t).1 ⊆ s

Tactic:
rw [nonuniformWitnesses, dif_pos h]

Premises used: SimpleGraph.nonuniformWitnesses, dif_pos
-- 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
⊢ (⋯.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 ⊆
    s

Tactic:
(not_isUniform_iff.1 h).choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, setOf, SimpleGraph.not_isUniform_iff, And.left, Iff.mp
-- 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
⊢ (⋯.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 ⊆
    s

Tactic:
exact (not_isUniform_iff.1 h).choose_spec.1

Premises used: Exists.choose_spec, SimpleGraph.not_isUniform_iff, And.left, Iff.mp
-- 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 :
  (↑(#s) : 𝕜) * ε ≤
    (↑(#(⋯.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) :
      𝕜)
⊢ (↑(#s) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitnesses ε s t).1) : 𝕜)

Tactic:
rw [nonuniformWitnesses, dif_pos h]

Premises used: SimpleGraph.nonuniformWitnesses, dif_pos
-- 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
⊢ (↑(#s) : 𝕜) * ε ≤
    (↑(#(⋯.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) :
      𝕜)

Tactic:
(not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.1

Premises used: Exists.choose_spec, SimpleGraph.not_isUniform_iff, And.right, And.left, Iff.mp, Classical.choose
-- 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
⊢ (↑(#s) : 𝕜) * ε ≤
    (↑(#(⋯.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) :
      𝕜)

Tactic:
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.1

Premises used: Exists.choose_spec, SimpleGraph.not_isUniform_iff, And.right, And.left, Iff.mp
-- 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 :
  (⋯.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 ⊆
    t
⊢ (G.nonuniformWitnesses ε s t).2 ⊆ t

Tactic:
rw [nonuniformWitnesses, dif_pos h]

Premises used: SimpleGraph.nonuniformWitnesses, dif_pos
-- 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
⊢ (⋯.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 ⊆
    t

Tactic:
(not_isUniform_iff.1 h).choose_spec.2.choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, setOf, SimpleGraph.not_isUniform_iff, And.right, And.left, Iff.mp
-- 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
⊢ (⋯.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 ⊆
    t

Tactic:
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.1

Premises used: Exists.choose_spec, SimpleGraph.not_isUniform_iff, And.right, And.left, Iff.mp
-- 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 :
  (↑(#t) : 𝕜) * ε ≤
    (↑(#(⋯.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) :
      𝕜)
⊢ (↑(#t) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitnesses ε s t).2) : 𝕜)

Tactic:
rw [nonuniformWitnesses, dif_pos h]

Premises used: SimpleGraph.nonuniformWitnesses, dif_pos