mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy✝ : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
hV : U ∈ P.parts
hy : y ∈ U
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

pp: case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy✝ : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
·

Goal state after:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy✝ : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
hV : U ∈ P.parts
hy : y ∈ U
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case pos
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy✝ : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
h₂ : G.IsUniform (ε / 8) U V
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

pp: case neg
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy✝ : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
h₂ : ¬G.IsUniform (ε / 8) U V
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
·

Goal state after:
case pos
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy✝ : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
h₂ : G.IsUniform (ε / 8) U V
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case neg
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy✝ : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
h₂ : ¬G.IsUniform (ε / 8) U V
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
·

Goal state after:
case neg
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy✝ : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
h₂ : ¬G.IsUniform (ε / 8) U V
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

pp: case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : 1 ≤ ε
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

pp: case inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : 1 ≤ ε
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t ≤ bound ε l

pp: case refine_2
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
hPenergy : ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ 1 < 1

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t ≤ bound ε l
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
huniform : P.IsUniform G ε
⊢ ∃ P,
    P.IsEquipartition ∧
      t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i + 1] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(i + 1) ≤ ↑(P.energy G))

pp: case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
huniform : ¬P.IsUniform G ε
⊢ ∃ P,
    P.IsEquipartition ∧
      t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i + 1] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(i + 1) ≤ ↑(P.energy G))

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
huniform : P.IsUniform G ε
⊢ ∃ P,
    P.IsEquipartition ∧
      t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i + 1] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(i + 1) ≤ ↑(P.energy G))
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
h : G.IsUniform ε (↑x).1 (↑x).2
⊢ ↑(G.edgeDensity (↑x).1 (↑x).2) ^ 2 - ε ^ 5 / 25 + 0 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts

pp: case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
h : ¬G.IsUniform ε (↑x).1 (↑x).2
⊢ ↑(G.edgeDensity (↑x).1 (↑x).2) ^ 2 - ε ^ 5 / 25 + ε ^ 4 / 3 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
h : G.IsUniform ε (↑x).1 (↑x).2
⊢ ↑(G.edgeDensity (↑x).1 (↑x).2) ^ 2 - ε ^ 5 / 25 + 0 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
h : ¬G.IsUniform ε (↑x).1 (↑x).2
⊢ ↑(G.edgeDensity (↑x).1 (↑x).2) ^ 2 - ε ^ 5 / 25 + ε ^ 4 / 3 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
h : ¬G.IsUniform ε (↑x).1 (↑x).2
⊢ ↑(G.edgeDensity (↑x).1 (↑x).2) ^ 2 - ε ^ 5 / 25 + ε ^ 4 / 3 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ t ≤ #(increment hP₁ G ε).parts

pp: case neg.refine_2
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ #(increment hP₁ G ε).parts ≤ stepBound^[i + 1] t

pp: case neg.refine_3
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ ε ^ 5 / 4 * ↑(i + 1) ≤ ↑(P.energy G) + ε ^ 5 / 4

Tactic:
·

Goal state after:
case neg.refine_1
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ t ≤ #(increment hP₁ G ε).parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case neg.refine_2.refine_1
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
⊢ #(u \ {y ∈ insert t R.parts | y ⊆ u}.biUnion id) ≤ m

Tactic:
simp only [filter_insert, if_pos htu, biUnion_insert, id]

Goal state after:
case neg.refine_2.refine_1
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
⊢ #(u \ (t ∪ {y ∈ R.parts | y ⊆ u}.biUnion id)) ≤ m
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ #(increment hP₁ G ε).parts ≤ stepBound^[i + 1] t

pp: case neg.refine_3
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ ε ^ 5 / 4 * ↑(i + 1) ≤ ↑(P.energy G) + ε ^ 5 / 4

Tactic:
·

Goal state after:
case neg.refine_2
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[i] t
huniform : ¬P.IsUniform G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G)
hεl' : 100 ≤ 4 ^ #P.parts * ε ^ 5
hi : ↑i ≤ 4 / ε ^ 5
hsize : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ #(increment hP₁ G ε).parts ≤ stepBound^[i + 1] t