awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
s₁ s₂ : Finset α
hs_1 : (s₁, s₂) ∈ P.parts.offDiag
hs : (s₁, s₂).1 ∈ P.parts ∧ (s₁, s₂).2 ∈ P.parts ∧ (s₁, s₂).1 ≠ (s₁, s₂).2
h :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (s₁, s₂) hs_1 ∈
    (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag)
t₁ t₂ : Finset α
ht_1 : (t₁, t₂) ∈ P.parts.offDiag
ht : (t₁, t₂).1 ∈ P.parts ∧ (t₁, t₂).2 ∈ P.parts ∧ (t₁, t₂).1 ≠ (t₁, t₂).2
h_1 :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (t₁, t₂) ht_1 ∈
    (↑P.parts.offDiag.attach : Set ↥P.parts.offDiag)
hst :
  Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (s₁, s₂) hs_1 ≠
    Subtype.mk (p := fun (x : Finset α × Finset α) ↦ x ∈ P.parts.offDiag) (t₁, t₂) ht_1
u v : Finset α
huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts
a : α
ha : a ∈ (u, v).1
b : α
hb : b ∈ (u, v).2
⊢ False

Tactic:
exact hst <| Subtype.ext <| Prod.ext
    (P.disjoint.elim_finset hs.1 ht.1 a (Finpartition.le _ huv₁.1 ha) <|
      Finpartition.le _ huv₂.1 ha) <|
        P.disjoint.elim_finset hs.2.1 ht.2.1 b (Finpartition.le _ huv₁.2 hb) <|
          Finpartition.le _ huv₂.2 hb

Premises used: Finpartition.disjoint, And.right, And.left, Prod.ext, Finpartition.le, Set.PairwiseDisjoint.elim_finset, Subtype.ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
rw :
  (HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2) : ℝ) 2 -
        HPow.hPow (β := ℕ) ε 5 / 25 +
      if G.IsUniform ε (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2 then 0
      else HPow.hPow (β := ℕ) ε 4 / 3) ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2) : ℝ) 2 +
      ((if G.IsUniform ε (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2 then 0
        else HPow.hPow (β := ℕ) ε 4 / 3) -
        HPow.hPow (β := ℕ) ε 5 / 25) ≤
    (∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
rw [distinctPairs, ← add_sub_assoc, add_sub_right_comm]

Premises used: add_sub_assoc, add_sub_right_comm, _private.0.SzemerediRegularity.distinctPairs
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
pos :
  ∀ (h : G.IsUniform ε (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2),
    HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2) : ℝ) 2 -
          HPow.hPow (β := ℕ) ε 5 / 25 +
        0 ≤
      (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts,
          HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
        HPow.hPow (α := ℝ) 16 #P.parts
neg :
  ∀ (h : ¬G.IsUniform ε (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2),
    HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2) : ℝ) 2 -
          HPow.hPow (β := ℕ) ε 5 / 25 +
        HPow.hPow (β := ℕ) ε 4 / 3 ≤
      (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts,
          HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
        HPow.hPow (α := ℝ) 16 #P.parts
⊢ (HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2) : ℝ) 2 -
        HPow.hPow (β := ℕ) ε 5 / 25 +
      if G.IsUniform ε (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2 then 0
      else HPow.hPow (β := ℕ) ε 4 / 3) ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
split_ifs with h
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
h : G.IsUniform ε (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2
pos :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2) : ℝ) 2 -
      HPow.hPow (β := ℕ) ε 5 / 25 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2) : ℝ) 2 -
        HPow.hPow (β := ℕ) ε 5 / 25 +
      0 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
h : G.IsUniform ε (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2) : ℝ) 2 -
      HPow.hPow (β := ℕ) ε 5 / 25 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
edgeDensity_chunk_uniform hPα hPε _ _

Premises used: SzemerediRegularity.edgeDensity_chunk_uniform
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
h : G.IsUniform ε (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2) : ℝ) 2 -
      HPow.hPow (β := ℕ) ε 5 / 25 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
exact edgeDensity_chunk_uniform hPα hPε _ _

Premises used: SzemerediRegularity.edgeDensity_chunk_uniform
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
h : ¬G.IsUniform ε (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2) : ℝ) 2 -
        HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (β := ℕ) ε 4 / 3 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
edgeDensity_chunk_not_uniform hPα hPε hε₁ (mem_offDiag.1 x.2).2.2 h

Premises used: And.right, Iff.mp, Finset.mem_offDiag, SzemerediRegularity.edgeDensity_chunk_not_uniform, Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
h : ¬G.IsUniform ε (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2) : ℝ) 2 -
        HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (β := ℕ) ε 4 / 3 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
exact edgeDensity_chunk_not_uniform hPα hPε hε₁ (mem_offDiag.1 x.2).2.2 h

Premises used: And.right, Iff.mp, Finset.mem_offDiag, SzemerediRegularity.edgeDensity_chunk_not_uniform, Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
ha : HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≠ 0
⊢ (↑(P.energy G) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 4 =
    (∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
        HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4)) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2

Tactic:
rw [coe_energy, add_div, mul_div_cancel_left₀]

Premises used: mul_div_cancel_left₀, Finpartition.coe_energy, add_div
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
        HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4)) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≤
    (∑ x ∈ P.parts.offDiag.attach,
        (∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
          HPow.hPow (α := ℝ) 16 #P.parts) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2

Tactic:
?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
rw :
  (∑ i ∈ P.parts.offDiag.attach,
          ∑ i ∈ distinctPairs hP G ε i, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
        HPow.hPow (α := ℝ) 16 #P.parts /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 =
    (∑ x ∈ P.parts.offDiag.attach,
          ∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
        HPow.hPow (α := ℝ) (β := ℕ) 4 2 ^ #P.parts /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2
⊢ (∑ x ∈ P.parts.offDiag.attach,
        (∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
          HPow.hPow (α := ℝ) 16 #P.parts) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 =
    (∑ x ∈ P.parts.offDiag.attach,
        ∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#(increment hP G ε).parts) : ℝ) 2

Tactic:
rw [card_increment hPα hPG, coe_stepBound, mul_pow, pow_right_comm,
          div_mul_eq_div_div_swap, ← sum_div]

Premises used: pow_right_comm, SzemerediRegularity.card_increment, SzemerediRegularity.coe_stepBound, div_mul_eq_div_div_swap, Finset.sum_div, mul_pow
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ i ∈ P.parts.offDiag.attach,
          ∑ i ∈ distinctPairs hP G ε i, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
        HPow.hPow (α := ℝ) 16 #P.parts /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 =
    (∑ x ∈ P.parts.offDiag.attach,
          ∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
        HPow.hPow (α := ℝ) (β := ℕ) 4 2 ^ #P.parts /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
rw :
  (∑ x ∈ P.parts.offDiag.attach,
        ∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#(increment hP G ε).parts) : ℝ) 2 ≤
    (∑ uv ∈ (increment hP G ε).parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity uv.1 uv.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#(increment hP G ε).parts) : ℝ) 2
⊢ (∑ x ∈ P.parts.offDiag.attach,
        ∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#(increment hP G ε).parts) : ℝ) 2 ≤
    (↑((increment hP G ε).energy G) : ℝ)

Tactic:
rw [coe_energy]

Premises used: Finpartition.coe_energy
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
hab :
  LE.le (α := ℝ)
    (∑ x ∈ P.parts.offDiag.attach,
      ∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2)
    (∑ uv ∈ (increment hP G ε).parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity uv.1 uv.2) : ℝ) 2)
⊢ (∑ x ∈ P.parts.offDiag.attach,
        ∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#(increment hP G ε).parts) : ℝ) 2 ≤
    (∑ uv ∈ (increment hP G ε).parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity uv.1 uv.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#(increment hP G ε).parts) : ℝ) 2

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
hab :
  LE.le (α := ℝ)
    (∑ x ∈ P.parts.offDiag.attach.biUnion (distinctPairs hP G ε),
      HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2)
    (∑ uv ∈ (increment hP G ε).parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity uv.1 uv.2) : ℝ) 2)
⊢ LE.le (α := ℝ)
    (∑ x ∈ P.parts.offDiag.attach,
      ∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2)
    (∑ uv ∈ (increment hP G ε).parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity uv.1 uv.2) : ℝ) 2)

Tactic:
rw [← sum_biUnion pairwiseDisjoint_distinctPairs]

Premises used: _private.0.SzemerediRegularity.pairwiseDisjoint_distinctPairs, Finset.sum_biUnion
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ LE.le (α := ℝ)
    (∑ x ∈ P.parts.offDiag.attach.biUnion (distinctPairs hP G ε),
      HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2)
    (∑ uv ∈ (increment hP G ε).parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity uv.1 uv.2) : ℝ) 2)

Tactic:
sum_le_sum_of_subset_of_nonneg distinctPairs_increment fun i _ _ ↦ sq_nonneg _

Premises used: SimpleGraph.edgeDensity, _private.0.SzemerediRegularity.distinctPairs_increment, Rat.cast, Prod.fst, sq_nonneg, Finset.sum_le_sum_of_subset_of_nonneg, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ LE.le (α := ℝ)
    (∑ x ∈ P.parts.offDiag.attach.biUnion (distinctPairs hP G ε),
      HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2)
    (∑ uv ∈ (increment hP G ε).parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity uv.1 uv.2) : ℝ) 2)

Tactic:
exact sum_le_sum_of_subset_of_nonneg distinctPairs_increment fun i _ _ ↦ sq_nonneg _

Premises used: _private.0.SzemerediRegularity.distinctPairs_increment, sq_nonneg, Finset.sum_le_sum_of_subset_of_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
_ :
  (∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
        HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4)) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≤
    (∑ x ∈ P.parts.offDiag.attach,
        (∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
          HPow.hPow (α := ℝ) 16 #P.parts) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2
⊢ (↑(P.energy G) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 4 ≤ (↑((increment hP G ε).energy G) : ℝ)

Tactic:
calc
    _ = (∑ x ∈ P.parts.offDiag, (G.edgeDensity x.1 x.2 : ℝ) ^ 2 +
          #P.parts ^ 2 * (ε ^ 5 / 4) : ℝ) / #P.parts ^ 2 := by
        rw [coe_energy, add_div, mul_div_cancel_left₀]; positivity
    _ ≤ (∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x,
          G.edgeDensity i.1 i.2 ^ 2 : ℝ) / 16 ^ #P.parts) / #P.parts ^ 2 := ?_
    _ = (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x,
          G.edgeDensity i.1 i.2 ^ 2 : ℝ) / #(increment hP G ε).parts ^ 2 := by
        rw [card_increment hPα hPG, coe_stepBound, mul_pow, pow_right_comm,
          div_mul_eq_div_div_swap, ← sum_div]; norm_num
    _ ≤ _ := by
        rw [coe_energy]
        gcongr
        rw [← sum_biUnion pairwiseDisjoint_distinctPairs]
        exact sum_le_sum_of_subset_of_nonneg distinctPairs_increment fun i _ _ ↦ sq_nonneg _

Premises used: HMul.hMul, SimpleGraph.edgeDensity, HDiv.hDiv, Rat.cast, SzemerediRegularity.increment, Finpartition.parts, Finset.offDiag, Nat.cast, Prod.fst, HPow.hPow, HAdd.hAdd, Finset.attach, Finset.card, OfNat.ofNat, _private.0.SzemerediRegularity.distinctPairs, Prod.snd, Finset.sum
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
inst_3 : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
hab :
  ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4) ≤
    ∑ x ∈ P.parts.offDiag.attach,
      (∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
        HPow.hPow (α := ℝ) 16 #P.parts
⊢ (∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
        HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4)) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≤
    (∑ x ∈ P.parts.offDiag.attach,
        (∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
          HPow.hPow (α := ℝ) 16 #P.parts) /
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2

Tactic:
gcongr