awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card.{u_1} (α := α) univ
dum : Finpartition (α := Finset α) univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
hsize : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ ∃ (P : Finpartition (α := Finset α) univ),
    P.IsEquipartition ∧
      t ≤ #P.parts ∧
        #P.parts ≤ stepBound^[i + 1] t ∧
          (P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(i + 1) : ℝ) ≤ (↑(P.energy G) : ℝ))

Tactic:
⟨increment hP₁ G ε, increment_isEquipartition hP₁ G ε, ?_, ?_, Or.inr <| le_trans ?_ <|
    energy_increment hP₁ ((seven_le_initialBound ε l).trans hP₂) hεl' hPα huniform hε.le hε₁⟩

Premises used: SzemerediRegularity.energy_increment, SzemerediRegularity.increment_isEquipartition, LT.lt.le, SzemerediRegularity.increment, SzemerediRegularity.seven_le_initialBound, And.intro, Exists.intro, LE.le.trans, Or.inr, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card.{u_1} (α := α) univ
dum : Finpartition (α := Finset α) univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
hsize : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
neg : t ≤ #(increment hP₁ G ε).parts
neg₁ : #(increment hP₁ G ε).parts ≤ stepBound^[i + 1] t
neg₂ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑(i + 1) : ℝ) ≤ (↑(P.energy G) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 4
⊢ ∃ (P : Finpartition (α := Finset α) univ),
    P.IsEquipartition ∧
      t ≤ #P.parts ∧
        #P.parts ≤ stepBound^[i + 1] t ∧
          (P.IsUniform G ε ∨ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(i + 1) : ℝ) ≤ (↑(P.energy G) : ℝ))

Tactic:
refine ⟨increment hP₁ G ε, increment_isEquipartition hP₁ G ε, ?_, ?_, Or.inr <| le_trans ?_ <|
    energy_increment hP₁ ((seven_le_initialBound ε l).trans hP₂) hεl' hPα huniform hε.le hε₁⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card.{u_1} (α := α) univ
dum : Finpartition (α := Finset α) univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
hsize : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
neg : t ≤ stepBound #P.parts
⊢ t ≤ #(increment hP₁ G ε).parts

Tactic:
rw [card_increment hPα huniform]

Premises used: SzemerediRegularity.card_increment
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card.{u_1} (α := α) univ
dum : Finpartition (α := Finset α) univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
hsize : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ t ≤ stepBound #P.parts

Tactic:
hP₂.trans (le_stepBound _)

Premises used: SzemerediRegularity.le_stepBound, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card.{u_1} (α := α) univ
dum : Finpartition (α := Finset α) univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
hsize : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ t ≤ stepBound #P.parts

Tactic:
exact hP₂.trans (le_stepBound _)

Premises used: SzemerediRegularity.le_stepBound, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card.{u_1} (α := α) univ
dum : Finpartition (α := Finset α) univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
hsize : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
neg : stepBound #P.parts ≤ stepBound (stepBound^[i] t)
⊢ #(increment hP₁ G ε).parts ≤ stepBound^[i + 1] t

Tactic:
rw [card_increment hPα huniform, iterate_succ_apply']

Premises used: Function.iterate_succ_apply', SzemerediRegularity.card_increment
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card.{u_1} (α := α) univ
dum : Finpartition (α := Finset α) univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
hsize : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ stepBound #P.parts ≤ stepBound (stepBound^[i] t)

Tactic:
stepBound_mono hP₃

Premises used: SzemerediRegularity.stepBound_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card.{u_1} (α := α) univ
dum : Finpartition (α := Finset α) univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
hsize : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ stepBound #P.parts ≤ stepBound (stepBound^[i] t)

Tactic:
exact stepBound_mono hP₃

Premises used: SzemerediRegularity.stepBound_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card.{u_1} (α := α) univ
dum : Finpartition (α := Finset α) univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
hsize : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
neg :
  HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) + HPow.hPow (β := ℕ) ε 5 / 4 ≤ (↑(P.energy G) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 4
⊢ HPow.hPow (β := ℕ) ε 5 / 4 * (↑(i + 1) : ℝ) ≤ (↑(P.energy G) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 4

Tactic:
rw [Nat.cast_succ, mul_add, mul_one]

Premises used: Nat.cast_succ, mul_add, mul_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card.{u_1} (α := α) univ
dum : Finpartition (α := Finset α) univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) ≤ (↑(P.energy G) : ℝ)
hεl' : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hi : (↑i : ℝ) ≤ 4 / HPow.hPow (β := ℕ) ε 5
hsize : #P.parts ≤ stepBound^[⌊4 / HPow.hPow (β := ℕ) ε 5⌋₊] t
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
⊢ HPow.hPow (β := ℕ) ε 5 / 4 * (↑i : ℝ) + HPow.hPow (β := ℕ) ε 5 / 4 ≤ (↑(P.energy G) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 4

Tactic:
gcongr
-- 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 : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : (↑(#s) : 𝕜) * ε' ≤ (↑(#s') : 𝕜)
ht : (↑(#t) : 𝕜) * ε' ≤ (↑(#t') : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity s t) : 𝕜)| < ε'

Tactic:
(hε hs' ht' (le_trans ?_ hs) (le_trans ?_ ht)).trans_le h

Premises used: LT.lt.trans_le, le_trans
-- 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 : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : (↑(#s) : 𝕜) * ε' ≤ (↑(#s') : 𝕜)
ht : (↑(#t) : 𝕜) * ε' ≤ (↑(#t') : 𝕜)
refine_1 : (↑(#s) : 𝕜) * ε ≤ (↑(#s) : 𝕜) * ε'
refine_2 : (↑(#t) : 𝕜) * ε ≤ (↑(#t) : 𝕜) * ε'
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity s t) : 𝕜)| < ε'

Tactic:
refine (hε hs' ht' (le_trans ?_ hs) (le_trans ?_ ht)).trans_le h

Premises used: LT.lt.trans_le, le_trans
-- 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 : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : (↑(#s) : 𝕜) * ε' ≤ (↑(#s') : 𝕜)
ht : (↑(#t) : 𝕜) * ε' ≤ (↑(#t') : 𝕜)
refine_1 : LE.le.{u_2} (α := 𝕜) 0 (↑(#s) : 𝕜)
⊢ (↑(#s) : 𝕜) * ε ≤ (↑(#s) : 𝕜) * ε'

Tactic:
gcongr
-- 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 : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : (↑(#s) : 𝕜) * ε' ≤ (↑(#s') : 𝕜)
ht : (↑(#t) : 𝕜) * ε' ≤ (↑(#t') : 𝕜)
refine_2 : LE.le.{u_2} (α := 𝕜) 0 (↑(#t) : 𝕜)
⊢ (↑(#t) : 𝕜) * ε ≤ (↑(#t) : 𝕜) * ε'

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : G.IsUniform ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜)
hs : (↑(#s) : 𝕜) * ε ≤ (↑(#s') : 𝕜)
rw : |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity s t) : 𝕜)| < ε
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity t' s') : 𝕜) (↑(G.edgeDensity t s) : 𝕜)| < ε

Tactic:
rw [edgeDensity_comm _ t', edgeDensity_comm _ t]

Premises used: SimpleGraph.edgeDensity_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : G.IsUniform ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜)
hs : (↑(#s) : 𝕜) * ε ≤ (↑(#s') : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity s t) : 𝕜)| < ε

Tactic:
h hs' ht' hs ht
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : G.IsUniform ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : (↑(#t) : 𝕜) * ε ≤ (↑(#t') : 𝕜)
hs : (↑(#s) : 𝕜) * ε ≤ (↑(#s') : 𝕜)
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity s t) : 𝕜)| < ε

Tactic:
exact h hs' ht' hs ht
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
⊢ G.IsUniform ε s t ↔ G.IsUniform ε t s

Tactic:
⟨fun h => h.symm, fun h => h.symm⟩

Premises used: Iff.intro, 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 s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : HMul.hMul (α := 𝕜) (↑(#s) : 𝕜) 1 ≤ (↑(#s') : 𝕜)
ht : HMul.hMul (α := 𝕜) (↑(#t) : 𝕜) 1 ≤ (↑(#t') : 𝕜)
⊢ LE.le.{u_2} (α := 𝕜) (↑(#s) : 𝕜) (↑(#s') : 𝕜)

Tactic:
rw [mul_one] at hs ht

Premises used: mul_one
-- 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 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') : 𝕜)
⊢ LE.le.{u_2} (α := 𝕜) (↑(#t) : 𝕜) (↑(#t') : 𝕜)

Tactic:
rw [mul_one] at hs ht

Premises used: mul_one
-- 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 s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : LE.le.{u_2} (α := 𝕜) (↑(#s) : 𝕜) (↑(#s') : 𝕜)
ht : LE.le.{u_2} (α := 𝕜) (↑(#t) : 𝕜) (↑(#t') : 𝕜)
rw : LT.lt.{u_2} (α := 𝕜) 0 1
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity s t) : 𝕜)| < 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]

Premises used: sub_self, abs_zero, Iff.mp, Nat.cast_le, Finset.eq_of_subset_of_card_le
-- 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 s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : LE.le.{u_2} (α := 𝕜) (↑(#s) : 𝕜) (↑(#s') : 𝕜)
ht : LE.le.{u_2} (α := 𝕜) (↑(#t) : 𝕜) (↑(#t') : 𝕜)
⊢ LT.lt.{u_2} (α := 𝕜) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- 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 s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : LE.le.{u_2} (α := 𝕜) (↑(#s) : 𝕜) (↑(#s') : 𝕜)
ht : LE.le.{u_2} (α := 𝕜) (↑(#t) : 𝕜) (↑(#t') : 𝕜)
⊢ LT.lt.{u_2} (α := 𝕜) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- 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 α
hG : G.IsUniform ε s t
hε : ε ≤ 0
⊢ (↑(#s) : 𝕜) * ε ≤ (↑(card.{u_1} (α := α) ∅) : 𝕜)

Tactic:
simpa using mul_nonpos_of_nonneg_of_nonpos (Nat.cast_nonneg _) hε

Premises used: Nat.cast_nonneg, mul_nonpos_of_nonneg_of_nonpos
-- 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 α
hG : G.IsUniform ε s t
hε : ε ≤ 0
⊢ (↑(#t) : 𝕜) * ε ≤ (↑(card.{u_1} (α := α) ∅) : 𝕜)

Tactic:
simpa using mul_nonpos_of_nonneg_of_nonpos (Nat.cast_nonneg _) hε

Premises used: Nat.cast_nonneg, mul_nonpos_of_nonneg_of_nonpos
-- 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 : α
⊢ G.IsUniform ε {a} {b} ↔ 0 < ε

Tactic:
⟨IsUniform.pos, fun hε s' hs' t' ht' hs ht ↦ ?_⟩

Premises used: SimpleGraph.IsUniform.pos, Iff.intro
-- 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 : α
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}) : 𝕜)| < ε
⊢ G.IsUniform ε {a} {b} ↔ 0 < ε

Tactic:
refine ⟨IsUniform.pos, fun hε s' hs' t' ht' hs 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 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : (↑(card (α := α) {a}) : 𝕜) * ε ≤ (↑(#s') : 𝕜)
ht : (↑(card (α := α) {b}) : 𝕜) * ε ≤ (↑(#t') : 𝕜)
⊢ ε ≤ (↑(#s') : 𝕜)

Tactic:
rw [card_singleton, Nat.cast_one, one_mul] at hs ht

Premises used: Nat.cast_one, one_mul, Finset.card_singleton
-- 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 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : (↑(card (α := α) {a}) : 𝕜) * ε ≤ (↑(#s') : 𝕜)
ht : (↑(card (α := α) {b}) : 𝕜) * ε ≤ (↑(#t') : 𝕜)
hs₁ : ε ≤ (↑(#s') : 𝕜)
⊢ ε ≤ (↑(#t') : 𝕜)

Tactic:
rw [card_singleton, Nat.cast_one, one_mul] at hs ht

Premises used: Nat.cast_one, one_mul, Finset.card_singleton
-- 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 < ε
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}) : 𝕜)| < ε
inr :
  ∀ (hs' : Subset (α := Finset α) {a} {a}) (hs : ε ≤ (↑(card (α := α) {a}) : 𝕜)),
    |HSub.hSub (α := 𝕜) (↑(G.edgeDensity {a} t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε
⊢ |HSub.hSub (α := 𝕜) (↑(G.edgeDensity s' t') : 𝕜) (↑(G.edgeDensity {a} {b}) : 𝕜)| < ε

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

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

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

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

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

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

Premises used: False.elim, LT.lt.not_ge