awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
s t s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : HMul.hMul (α := 𝕜) (↑(#s) : 𝕜) 1 ≤ (↑(#s') : 𝕜)
ht : HMul.hMul (α := 𝕜) (↑(#t) : 𝕜) 1 ≤ (↑(#t') : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity s t) : 𝕜)| < 1
have hs₁ : LE.le.{u_2} (α := 𝕜) (↑(#s) : 𝕜) (↑(#s') : 𝕜)
Tactic: rw [mul_one] at hs ht
Cleared hypotheses: hs, ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
s t s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : HMul.hMul (α := 𝕜) (↑(#s) : 𝕜) 1 ≤ (↑(#s') : 𝕜)
ht : HMul.hMul (α := 𝕜) (↑(#t) : 𝕜) 1 ≤ (↑(#t') : 𝕜)
hs₁ : LE.le.{u_2} (α := 𝕜) (↑(#s) : 𝕜) (↑(#s') : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity s t) : 𝕜)| < 1
have ht₁ : LE.le.{u_2} (α := 𝕜) (↑(#t) : 𝕜) (↑(#t') : 𝕜)
Tactic: rw [mul_one] at hs ht
Cleared hypotheses: hs, ht
-- 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 s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : LE.le.{u_2} (α := 𝕜) (↑(#s) : 𝕜) (↑(#s') : 𝕜)
ht : LE.le.{u_2} (α := 𝕜) (↑(#t) : 𝕜) (↑(#t') : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity s t) : 𝕜)| < 1
have rw : LT.lt.{u_2} (α := 𝕜) 0 1
Tactic: 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]
-- 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
ε : 𝕜
a b : α
⊢ G.IsUniform ε {a} {b} ↔ 0 < ε
have refine : ∀ (hε : 0 < ε) (s' : Finset α) (hs' : s' ⊆ {a}) (t' : Finset α) (ht' : t' ⊆ {b})
  (hs : (↑(card (α := α) {a}) : 𝕜) * ε ≤ (↑(#s') : 𝕜)) (ht : (↑(card (α := α) {b}) : 𝕜) * ε ≤ (↑(#t') : 𝕜)),
  |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
Tactic: refine ⟨IsUniform.pos, fun hε s' hs' t' ht' hs ht ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (hypothesis)
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 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : (↑(card (α := α) {a}) : 𝕜) * ε ≤ (↑(#s') : 𝕜)
ht : (↑(card (α := α) {b}) : 𝕜) * ε ≤ (↑(#t') : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
have hs₁ : ε ≤ (↑(#s') : 𝕜)
Tactic: rw [card_singleton, Nat.cast_one, one_mul] at hs ht
Cleared hypotheses: hs, ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (hypothesis)
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 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : (↑(card (α := α) {a}) : 𝕜) * ε ≤ (↑(#s') : 𝕜)
ht : (↑(card (α := α) {b}) : 𝕜) * ε ≤ (↑(#t') : 𝕜)
hs₁ : ε ≤ (↑(#s') : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
have ht₁ : ε ≤ (↑(#t') : 𝕜)
Tactic: rw [card_singleton, Nat.cast_one, one_mul] at hs ht
Cleared hypotheses: hs, ht
-- 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
ε : 𝕜
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ε ≤ (↑(#s') : 𝕜)
ht : ε ≤ (↑(#t') : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
have inl : ∀ (hs' : Subset (α := Finset α) ∅ {a}) (hs : ε ≤ (↑(card.{u_1} (α := α) ∅) : 𝕜)),
  |HSub.hSub (α := 𝕜) (↑(G.edgeDensity ∅ t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
Tactic: obtain rfl | rfl := Finset.subset_singleton_iff.1 hs'
Cleared hypotheses: s', hs', hs
-- 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
ε : 𝕜
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ε ≤ (↑(#s') : 𝕜)
ht : ε ≤ (↑(#t') : 𝕜)
inl :
  ∀ (hs' : Subset (α := Finset α) ∅ {a}) (hs : ε ≤ (↑(card.{u_1} (α := α) ∅) : 𝕜)),
    |HSub.hSub (α := 𝕜) (↑(G.edgeDensity ∅ t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
have inr : ∀ (hs' : Subset (α := Finset α) {a} {a}) (hs : ε ≤ (↑(card (α := α) {a}) : 𝕜)),
  |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
Tactic: obtain rfl | rfl := Finset.subset_singleton_iff.1 hs'
Cleared hypotheses: s', hs', hs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (hypothesis)
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}
hs : ε ≤ (↑(card.{u_1} (α := α) ∅) : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity ∅ t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
have hs₁ : ε ≤ 0
Tactic: replace hs : ε ≤ 0 := by simpa using hs
Cleared hypotheses: hs
-- 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
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ (↑(#t') : 𝕜)
hs' : Subset (α := Finset α) {a} {a}
hs : ε ≤ (↑(card (α := α) {a}) : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
have inr : ∀ (ht' : Subset (α := Finset α) ∅ {b}) (ht : ε ≤ (↑(card.{u_1} (α := α) ∅) : 𝕜)),
  |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} ∅) : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
Tactic: obtain rfl | rfl := Finset.subset_singleton_iff.1 ht'
Cleared hypotheses: t', ht', ht
-- 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
ε : 𝕜
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}) : 𝕜)| < ε
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
have inr₁ : ∀ (ht' : Subset (α := Finset α) {b} {b}) (ht : ε ≤ (↑(card (α := α) {b}) : 𝕜)),
  |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
Tactic: obtain rfl | rfl := Finset.subset_singleton_iff.1 ht'
Cleared hypotheses: t', ht', ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (hypothesis)
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} (α := α) ∅) : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} ∅) : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
have ht₁ : ε ≤ 0
Tactic: replace ht : ε ≤ 0 := by simpa using ht
Cleared hypotheses: ht
-- 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
ε : 𝕜
a b : α
hε : 0 < ε
hs' : Subset (α := Finset α) {a} {a}
hs : ε ≤ (↑(card (α := α) {a}) : 𝕜)
ht' : Subset (α := Finset α) {b} {b}
ht : ε ≤ (↑(card (α := α) {b}) : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
have inr : |0| < ε
Tactic: rwa [sub_self, abs_zero]
-- 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.nonuniformWitnesses ε s t).1 ⊆ s
have rw : (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 ⊆
  s
Tactic: rw [nonuniformWitnesses, dif_pos h]
-- 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
⊢ (↑(#s) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitnesses ε s t).1) : 𝕜)
have rw : (↑(#s) : 𝕜) * ε ≤
  (↑(#(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) :
    𝕜)
Tactic: rw [nonuniformWitnesses, dif_pos h]
-- 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.nonuniformWitnesses ε s t).2 ⊆ t
have rw : (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 ⊆
  t
Tactic: rw [nonuniformWitnesses, dif_pos h]
-- 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
⊢ (↑(#t) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitnesses ε s t).2) : 𝕜)
have rw : (↑(#t) : 𝕜) * ε ≤
  (↑(#(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) :
    𝕜)
Tactic: rw [nonuniformWitnesses, dif_pos h]
-- 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
⊢ (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2) ⊆ s
have pos : WellOrderingRel s t → (G.nonuniformWitnesses ε s t).1 ⊆ s
Tactic: split_ifs
-- 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
pos : WellOrderingRel s t → (G.nonuniformWitnesses ε s t).1 ⊆ s
⊢ (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2) ⊆ s
have neg : ¬WellOrderingRel s t → (G.nonuniformWitnesses ε t s).2 ⊆ s
Tactic: split_ifs
-- 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
⊢ (↑(#s) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitness ε s t)) : 𝕜)
have unfold : (↑(#s) : 𝕜) * ε ≤
  (↑(#(if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)) : 𝕜)
Tactic: unfold nonuniformWitness
-- 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
⊢ (↑(#s) : 𝕜) * ε ≤
    (↑(#(if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)) : 𝕜)
have pos : WellOrderingRel s t → (↑(#s) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitnesses ε s t).1) : 𝕜)
Tactic: split_ifs
-- 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
pos : WellOrderingRel s t → (↑(#s) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitnesses ε s t).1) : 𝕜)
⊢ (↑(#s) : 𝕜) * ε ≤
    (↑(#(if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)) : 𝕜)
have neg : ¬WellOrderingRel s t → (↑(#s) : 𝕜) * ε ≤ (↑(#(G.nonuniformWitnesses ε t s).2) : 𝕜)
Tactic: split_ifs
-- 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₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
⊢ ε ≤ (↑|G.edgeDensity (G.nonuniformWitness ε s t) (G.nonuniformWitness ε t s) - G.edgeDensity s t| : 𝕜)
have 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| :
    𝕜)
Tactic: unfold nonuniformWitness
-- 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₁ : s ≠ t
h₂ : ¬G.IsUniform ε 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| :
      𝕜)
have 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| :
      𝕜)
Tactic: rcases trichotomous_of WellOrderingRel s t with (lt | rfl | gt)
-- 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₁ : 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| :
        𝕜)
⊢ ε ≤
    (↑|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| :
      𝕜)
have 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| :
      𝕜)
Tactic: rcases trichotomous_of WellOrderingRel s t with (lt | rfl | gt)
Cleared hypotheses: t, h₁, h₂
-- 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₁ : 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| :
        𝕜)
⊢ ε ≤
    (↑|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| :
      𝕜)
have 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| :
      𝕜)
Tactic: rcases trichotomous_of WellOrderingRel s t with (lt | rfl | gt)
-- 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₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
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| :
      𝕜)
have inl : ε ≤ (↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t| : 𝕜)
Tactic: rw [if_pos lt, if_neg (asymm lt)]