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

Goal state before:
pp: case calc_2
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ε * ↑(∑ x ∈ P.parts.offDiag, #x.1 * #x.2) ≤ ε * ↑((#A + #P.parts) ^ 2)

Tactic:
gcongr

Goal state after:
case a
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∑ x ∈ P.parts.offDiag, #x.1 * #x.2 ≤ (#A + #P.parts) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ (#P.parts * (#A / #P.parts) + #P.parts) ^ 2 ≤ (#A + #P.parts) ^ 2

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ #P.parts * (#A / #P.parts) ≤ #A
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ε * (↑(#A) + ↑(#P.parts)) ^ 2 ≤ ε * (↑(#A) + ↑(#A)) ^ 2

Tactic:
gcongr

Goal state after:
case a
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ #P.parts ≤ #A
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:

Tactic:
_ ≤ _ := hP.card_interedges_sparsePairs_le' hε
    _ ≤ ε * (#A + #A) ^ 2 := by gcongr; exact P.card_parts_le_card
    _ = _ := by ring

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: i j : ℕ
hj : 0 < j
this : j * (j - 1) < j ^ 2
⊢ (j * (i / j) + j) ^ 2 ≤ (i + j) ^ 2

Tactic:
gcongr

Goal state after:
case h₁
i j : ℕ
hj : 0 < j
this : j * (j - 1) < j ^ 2
⊢ j * (i / j) ≤ i
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) + ↑(#P.parts) ≤ ↑(#A) + ↑(#A)

Tactic:
gcongr

Goal state after:
case a
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ #P.parts ≤ #A
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case calc_2
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ↑(#P.parts * (#P.parts - 1)) * ↑(#A / #P.parts + 1) ^ 2 * ε < (↑(#A) + ↑(#P.parts)) ^ 2 * ε

Tactic:
gcongr

Goal state after:
case hbc
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ↑(#P.parts * (#P.parts - 1)) * ↑(#A / #P.parts + 1) ^ 2 < (↑(#A) + ↑(#P.parts)) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ε * (↑(#A) + ↑(#P.parts)) ^ 2 ≤ ε * (↑(#A) + ↑(#A)) ^ 2

Tactic:
gcongr

Goal state after:
case a
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ #P.parts ≤ #A
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
⊢ #P.parts * 4 ^ #P.parts ≤ #P.parts * 16 ^ #P.parts

Tactic:
gcongr

Goal state after:
case hab
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
⊢ 4 ≤ 16
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
⊢ l ≤ #univ ∧ #univ ≤ bound ε l ∧ ⊥.IsUniform G ε

Tactic:
card_univ

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
⊢ l ≤ Fintype.card α ∧ Fintype.card α ≤ bound ε l ∧ ⊥.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⌋₊] t * 4 ^ stepBound^[⌊4 / ε ^ 5⌋₊] t ≤
    stepBound^[⌊4 / ε ^ 5⌋₊] (initialBound ε l) * 16 ^ stepBound^[⌊4 / ε ^ 5⌋₊] (initialBound ε l)

Tactic:
gcongr

Goal state after:
case hab
α : 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 : ℕ := ⋯
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)
⊢ 4 ≤ 16
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: α : 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)
⊢ ε ^ 5 / 4 * (4 / ε ^ 5) < ε ^ 5 / 4 * (↑⌊4 / ε ^ 5⌋₊ + 1)

Tactic:
gcongr

Goal state after:
case hbc
α : 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 : ℕ := ⋯
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)
⊢ 4 / ε ^ 5 < ↑⌊4 / ε ^ 5⌋₊ + 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) /
      ↑(#(increment hP G ε).parts) ^ 2 ≤
    (∑ uv ∈ (increment hP G ε).parts.offDiag, ↑(G.edgeDensity uv.1 uv.2) ^ 2) / ↑(#(increment hP G ε).parts) ^ 2

Tactic:
gcongr

Goal state after:
case hab
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2 ≤
    ∑ uv ∈ (increment hP G ε).parts.offDiag, ↑(G.edgeDensity uv.1 uv.2) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑(#P.parts) ^ 2 * (ε ^ 5 / 4)) / ↑(#P.parts) ^ 2 ≤
    (∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts) /
      ↑(#P.parts) ^ 2

Tactic:
gcongr

Goal state after:
case hab
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑(#P.parts) ^ 2 * (ε ^ 5 / 4) ≤
    ∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
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 + ε ^ 5 / 4 ≤ ↑(P.energy G) + ε ^ 5 / 4

Tactic:
gcongr

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set (Sym2 V)
G' : SimpleGraph V
⊢ G.deleteEdges s ≤ G' ↔ G ≤ fromEdgeSet s ⊔ G'

Tactic:
rw [deleteEdges, sdiff_le_iff]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: case hab
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑(#P.parts) ^ 2 * (ε ^ 5 / 4) ≤
    ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 +
      (↑(#(P.nonUniforms G ε)) * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25))

Tactic:
gcongr

Goal state after:
case h₂
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ↑(#P.parts) ^ 2 * (ε ^ 5 / 4) ≤ ↑(#(P.nonUniforms G ε)) * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx : x ∈ G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id
⊢ x ∈
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id

Tactic:
rw [← biUnion_filter_atomise hX (G.nonuniformWitness_subset h₂), star, mem_sdiff,
      mem_biUnion] at hx

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx :
  (∃ a ∈ {u ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | u ⊆ G.nonuniformWitness ε U V ∧ u.Nonempty}, x ∈ id a) ∧
    x ∉ {A ∈ (chunk hP G ε hU).parts | A ⊆ G.nonuniformWitness ε U V}.biUnion id
⊢ x ∈
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ↑(#P.parts.offDiag) * ε * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25) ≤
    ↑(#(P.nonUniforms G ε)) * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25)

Tactic:
gcongr

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inr.calc_1
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ #G.edgeFinset - #univ = #G.edgeFinset - Fintype.card { G' // Nonempty (H ≃g G'.coe) }

Tactic:
card_univ

Goal state after:
case inr.calc_1
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ #G.edgeFinset - Fintype.card { G' // Nonempty (H ≃g G'.coe) } =
    #G.edgeFinset - Fintype.card { G' // Nonempty (H ≃g G'.coe) }
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : ↑s = H.neighborSet v
t : Finset V
ht : ↑t = G.neighborSet v
h : ↑↑t ≃ ↑↑s
⊢ s ⊆ t

Tactic:
rw [← Finset.coe_subset, hs, ht]

Goal state after:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
s : Finset V
hs : ↑s = H.neighborSet v
t : Finset V
ht : ↑t = G.neighborSet v
h : ↑↑t ≃ ↑↑s
⊢ H.neighborSet v ⊆ G.neighborSet v
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (G.subgraphOfAdj hvw)).verts ↔ x✝ ∈ (G'.subgraphOfAdj ⋯).verts

Tactic:
grind [Subgraph.map_verts, subgraphOfAdj_verts, Relation.Map, Subgraph.map_adj,
    subgraphOfAdj_adj]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝¹ x✝ : W
⊢ (Subgraph.map f (G.subgraphOfAdj hvw)).Adj x✝¹ x✝ ↔ (G'.subgraphOfAdj ⋯).Adj x✝¹ x✝

Tactic:
grind [Subgraph.map_verts, subgraphOfAdj_verts, Relation.Map, Subgraph.map_adj,
    subgraphOfAdj_adj]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
⊢ (1 - ε / 10) * ↑(#(G.nonuniformWitness ε U V)) ≤
    (1 - 2 ^ #P.parts * ↑m / (↑(#U) * ε)) * ↑(#(G.nonuniformWitness ε U V))

Tactic:
gcongr

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this✝ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
⊢ 0 < ↑(#U) * ε

Tactic:
have := Finset.card_pos.mpr (P.nonempty_of_mem_parts hU)

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this✝¹ : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
this✝ : 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2
this : 0 < #U
⊢ 0 < ↑(#U) * ε
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : n ≤ p.length
⊢ p.getVert n = p.support.getD n v

pp: case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : ¬n ≤ p.length
⊢ p.getVert n = p.support.getD n v

Tactic:
· simp [← getVert_eq_support_getElem? p h]

Goal state after:
case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : ¬n ≤ p.length
⊢ p.getVert n = p.support.getD n v
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#𝒜) * ↑m * ↑(#s) ≤ ↑(#(𝒜.sup id)) * (↑m + 1)

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#𝒜) * ↑m ≤ ↑(#(𝒜.sup id))

case h₂
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#s) ≤ ↑m + 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#(𝒜.biUnion id)) * ↑m ≤ ↑(#𝒜) * (↑m + 1) * ↑(#s)

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#(𝒜.biUnion id)) ≤ ↑(#𝒜) * (↑m + 1)

case a
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ m ≤ #s
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w : V
p✝ : G.Walk u v
H : SimpleGraph V
s s' : Set V
e : Sym2 V
p : G.Walk v w
hp : e ∉ p.edges
x✝ : Sym2 V
⊢ x✝ ∈ p.edges → x✝ ∉ {e}

Tactic:
by contrapose; simp +contextual [hp]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 1 + ε ^ 5 * (50⁻¹ + ε ^ 5 / 10000) ≤ 1 + ε ^ 5 * (50⁻¹ + 1 ^ 5 / 10000)

Tactic:
gcongr

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 1 + ε ^ 5 * (50⁻¹ + 1 ^ 5 / 10000) ≤ 1 + ε ^ 5 * 49⁻¹

Tactic:
gcongr

Goal state after:
case hbc
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 50⁻¹ + 1 ^ 5 / 10000 ≤ 49⁻¹