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
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (↑(#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) :
      𝕜)

Tactic:
(not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.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
⊢ (↑(#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) :
      𝕜)

Tactic:
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.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
pos : WellOrderingRel s t → (G.nonuniformWitnesses ε s t).1 ⊆ s
neg : ¬WellOrderingRel s t → (G.nonuniformWitnesses ε t s).2 ⊆ s
⊢ (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2) ⊆ s

Tactic:
split_ifs
-- 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
h_1 : WellOrderingRel s t
⊢ (G.nonuniformWitnesses ε s t).1 ⊆ s

Tactic:
G.left_nonuniformWitnesses_subset h

Premises used: SimpleGraph.left_nonuniformWitnesses_subset
-- 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
h_1 : WellOrderingRel s t
⊢ (G.nonuniformWitnesses ε s t).1 ⊆ s

Tactic:
exact G.left_nonuniformWitnesses_subset h

Premises used: SimpleGraph.left_nonuniformWitnesses_subset
-- 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
h_1 : ¬WellOrderingRel s t
⊢ (G.nonuniformWitnesses ε t s).2 ⊆ s

Tactic:
G.right_nonuniformWitnesses_subset fun i => h i.symm

Premises used: SimpleGraph.right_nonuniformWitnesses_subset, SimpleGraph.IsUniform.symm
-- 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
h_1 : ¬WellOrderingRel s t
⊢ (G.nonuniformWitnesses ε t s).2 ⊆ s

Tactic:
exact G.right_nonuniformWitnesses_subset fun i => h i.symm

Premises used: SimpleGraph.right_nonuniformWitnesses_subset, SimpleGraph.IsUniform.symm
-- 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
unfold :
  (↑(#s) : 𝕜) * ε ≤
    (↑(#(if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)) : 𝕜)
⊢ (↑(#s) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitness ε s t)) : 𝕜)

Tactic:
unfold nonuniformWitness

Premises used: SimpleGraph.nonuniformWitness
-- 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
pos : WellOrderingRel s t → (↑(#s) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitnesses ε s t).1) : 𝕜)
neg : ¬WellOrderingRel s t → (↑(#s) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitnesses ε t s).2) : 𝕜)
⊢ (↑(#s) : 𝕜) * ε ≤
    (↑(#(if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)) : 𝕜)

Tactic:
split_ifs
-- 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
h_1 : WellOrderingRel s t
⊢ (↑(#s) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitnesses ε s t).1) : 𝕜)

Tactic:
G.left_nonuniformWitnesses_card h

Premises used: SimpleGraph.left_nonuniformWitnesses_card
-- 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
h_1 : WellOrderingRel s t
⊢ (↑(#s) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitnesses ε s t).1) : 𝕜)

Tactic:
exact G.left_nonuniformWitnesses_card h

Premises used: SimpleGraph.left_nonuniformWitnesses_card
-- 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
h_1 : ¬WellOrderingRel s t
⊢ (↑(#s) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitnesses ε t s).2) : 𝕜)

Tactic:
G.right_nonuniformWitnesses_card fun i => h i.symm

Premises used: SimpleGraph.right_nonuniformWitnesses_card, SimpleGraph.IsUniform.symm
-- 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
h_1 : ¬WellOrderingRel s t
⊢ (↑(#s) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitnesses ε t s).2) : 𝕜)

Tactic:
exact G.right_nonuniformWitnesses_card fun i => h i.symm

Premises used: SimpleGraph.right_nonuniformWitnesses_card, SimpleGraph.IsUniform.symm
-- 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₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
unfold :
  ε ≤
    (↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
              (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
            G.edgeDensity s t| :
      𝕜)
⊢ ε ≤ (↑|G.edgeDensity (G.nonuniformWitness ε s t) (G.nonuniformWitness ε t s) - G.edgeDensity s t| : 𝕜)

Tactic:
unfold nonuniformWitness

Premises used: SimpleGraph.nonuniformWitness
-- 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₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
inl :
  ∀ (lt : WellOrderingRel s t),
    ε ≤
      (↑|G.edgeDensity
                (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
                (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
              G.edgeDensity s t| :
        𝕜)
inr :
  ∀ (h₁ : s ≠ s) (h₂ : ¬G.IsUniform ε s s),
    ε ≤
      (↑|G.edgeDensity
                (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2)
                (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2) -
              G.edgeDensity s s| :
        𝕜)
inr₁ :
  ∀ (gt : WellOrderingRel t s),
    ε ≤
      (↑|G.edgeDensity
                (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
                (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
              G.edgeDensity s t| :
        𝕜)
⊢ ε ≤
    (↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
              (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
            G.edgeDensity s t| :
      𝕜)

Tactic:
rcases trichotomous_of WellOrderingRel s t with (lt | rfl | gt)

Premises used: trichotomous_of, rfl, WellOrderingRel
-- 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₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
lt : WellOrderingRel s t
inl : ε ≤ (↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t| : 𝕜)
⊢ ε ≤
    (↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
              (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
            G.edgeDensity s t| :
      𝕜)

Tactic:
rw [if_pos lt, if_neg (asymm lt)]

Premises used: asymm, if_pos, if_neg
-- 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₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
lt : WellOrderingRel s t
⊢ ε ≤ (↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t| : 𝕜)

Tactic:
G.nonuniformWitnesses_spec h₂

Premises used: SimpleGraph.nonuniformWitnesses_spec
-- 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₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
lt : WellOrderingRel s t
⊢ ε ≤ (↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t| : 𝕜)

Tactic:
exact G.nonuniformWitnesses_spec h₂

Premises used: SimpleGraph.nonuniformWitnesses_spec
-- 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 : Finset α
h₁ : s ≠ s
h₂ : ¬G.IsUniform ε s s
⊢ ε ≤
    (↑|G.edgeDensity (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2)
              (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2) -
            G.edgeDensity s s| :
      𝕜)

Tactic:
cases h₁ rfl

Premises used: 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
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
inr : ε ≤ (↑|G.edgeDensity (G.nonuniformWitnesses ε t s).1 (G.nonuniformWitnesses ε t s).2 - G.edgeDensity t s| : 𝕜)
⊢ ε ≤
    (↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
              (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
            G.edgeDensity s t| :
      𝕜)

Tactic:
rw [if_neg (asymm gt), if_pos gt, edgeDensity_comm, edgeDensity_comm _ s]

Premises used: asymm, if_pos, if_neg, SimpleGraph.edgeDensity_comm
-- 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₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
⊢ ε ≤ (↑|G.edgeDensity (G.nonuniformWitnesses ε t s).1 (G.nonuniformWitnesses ε t s).2 - G.edgeDensity t s| : 𝕜)

Tactic:
apply G.nonuniformWitnesses_spec fun i => h₂ i.symm

Premises used: SimpleGraph.nonuniformWitnesses_spec, SimpleGraph.IsUniform.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
u v : Finset α
ε : 𝕜
rw :
  (u, v) ∈
      {x ∈ P.parts.offDiag |
        match (motive := Finset α × Finset α → Prop) x with
        | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε} ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
rw₁ :
  ((u, v) ∈ P.parts.offDiag ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
rw₂ :
  (((u, v).1 ∈ P.parts ∧ (u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
rw₃ :
  ((u, v).1 ∈ P.parts ∧
      ((u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
        match (motive := Finset α × Finset α → Prop) (u, v) with
        | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
rw₄ rw₅ :
  ((u, v).1 ∈ P.parts ∧
      (u, v).2 ∈ P.parts ∧
        (u, v).1 ≠ (u, v).2 ∧
          match (motive := Finset α × Finset α → Prop) (u, v) with
          | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
⊢ (u, v) ∈ P.sparsePairs G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε

Tactic:
rw [sparsePairs, mem_filter, mem_offDiag, and_assoc, and_assoc]

Premises used: and_assoc, Finset.mem_offDiag, Finset.mem_filter, Finpartition.sparsePairs
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε ε' : 𝕜
h : ε ≤ ε'
⊢ P.sparsePairs G ε ⊆ P.sparsePairs G ε'

Tactic:
monotone_filter_right _ fun _ _ ↦ h.trans_lt'

Premises used: Set.Mem, setOf, Finset.monotone_filter_right, LE.le.trans_lt'
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
u v : Finset α
rw :
  (u, v) ∈
      {x ∈ P.parts.offDiag |
        match (motive := Finset α × Finset α → Prop) x with
        | (u, v) => ¬G.IsUniform ε u v} ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
rw₁ :
  ((u, v) ∈ P.parts.offDiag ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => ¬G.IsUniform ε u v) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
rw₂ :
  (((u, v).1 ∈ P.parts ∧ (u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => ¬G.IsUniform ε u v) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
rw₃ :
  ((u, v).1 ∈ P.parts ∧
      ((u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
        match (motive := Finset α × Finset α → Prop) (u, v) with
        | (u, v) => ¬G.IsUniform ε u v) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
rw₄ rw₅ :
  ((u, v).1 ∈ P.parts ∧
      (u, v).2 ∈ P.parts ∧
        (u, v).1 ≠ (u, v).2 ∧
          match (motive := Finset α × Finset α → Prop) (u, v) with
          | (u, v) => ¬G.IsUniform ε u v) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
⊢ (u, v) ∈ P.nonUniforms G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v

Tactic:
rw [nonUniforms, mem_filter, mem_offDiag, and_assoc, and_assoc]

Premises used: and_assoc, Finpartition.nonUniforms, Finset.mem_offDiag, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε ε' : 𝕜
h : ε ≤ ε'
⊢ P.nonUniforms G ε' ⊆ P.nonUniforms G ε

Tactic:
monotone_filter_right _ fun _ _ => mt <| SimpleGraph.IsUniform.mono h

Premises used: Set.Mem, setOf, mt, Finset.monotone_filter_right, SimpleGraph.IsUniform.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
rw : ∀ (x : Finset α × Finset α), x ∉ nonUniforms (A := A) ⊥ G ε
⊢ nonUniforms (A := A) ⊥ G ε = ∅

Tactic:
rw [eq_empty_iff_forall_notMem]

Premises used: Finset.eq_empty_iff_forall_notMem
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
simp :
  ∀ (x : α),
    x ∈ A ∧ ({ toFun := singleton, inj' := ⋯ : α ↪ Finset α } : (a : α) → Finset α) x = u →
      ∀ (x : α),
        x ∈ A ∧ ({ toFun := singleton, inj' := ⋯ : α ↪ Finset α } : (a : α) → Finset α) x = v →
          u ≠ v → G.IsUniform ε u v
⊢ (u, v) ∉ nonUniforms (A := A) ⊥ G ε

Tactic:
simp only [mk_mem_nonUniforms, parts_bot, mem_map, not_and,
    Classical.not_not, exists_imp]

Premises used: Finpartition.parts_bot, Finpartition.mk_mem_nonUniforms, Classical.not_not, Finset.mem_map, exists_imp, not_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
x : α
left : x ∈ A
y : α
left_1 : y ∈ A
h : ¬Eq (α := Finset α) {x} {y}
rwa rwa₁ rwa₂ rwa₃ : 0 < ε
⊢ G.IsUniform ε {x} {y}

Tactic:
rwa [SimpleGraph.isUniform_singleton]

Premises used: SimpleGraph.isUniform_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
rw : 0 ≤ (↑(#A * (#A - 1)) : 𝕜) * ε
⊢ IsUniform (A := A) ⊥ G ε

Tactic:
rw [Finpartition.IsUniform, Finpartition.card_bot, nonUniforms_bot _ hε, Finset.card_empty,
    Nat.cast_zero]

Premises used: Finpartition.IsUniform, Finset.card_empty, Finpartition.card_bot, Finpartition.nonUniforms_bot, Nat.cast_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ 0 ≤ (↑(#A * (#A - 1)) : 𝕜) * ε

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
rw : #(nonUniforms.{u_1, u_2} (𝕜 := 𝕜) P G 1) ≤ #P.parts * (#P.parts - 1)
⊢ IsUniform.{u_1, u_2} (𝕜 := 𝕜) P G 1

Tactic:
rw [IsUniform, mul_one, Nat.cast_le]

Premises used: Finpartition.IsUniform, Nat.cast_le, mul_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
⊢ #(nonUniforms.{u_1, u_2} (𝕜 := 𝕜) P G 1) ≤ #P.parts * (#P.parts - 1)

Tactic:
(card_filter_le _
    (fun uv => ¬SimpleGraph.IsUniform G 1 (Prod.fst uv) (Prod.snd uv))).trans ?_

Premises used: Prod.fst, Finpartition.nonUniforms, SimpleGraph.IsUniform, LE.le.trans, Finset.card_filter_le, OfNat.ofNat, Prod.snd, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
refine : #P.parts.offDiag ≤ #P.parts * (#P.parts - 1)
⊢ #(nonUniforms.{u_1, u_2} (𝕜 := 𝕜) P G 1) ≤ #P.parts * (#P.parts - 1)

Tactic:
refine (card_filter_le _
    (fun uv => ¬SimpleGraph.IsUniform G 1 (Prod.fst uv) (Prod.snd uv))).trans ?_

Premises used: Prod.fst, SimpleGraph.IsUniform, LE.le.trans, Finset.card_filter_le, OfNat.ofNat, Prod.snd, Not