awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ False
have obtain : ∀ (b : α) (hb : b ∈ (u, v).2), False
Tactic: obtain ⟨b, hb⟩ := Finpartition.nonempty_of_mem_parts _ huv₁.2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ 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
have 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 ε sorry).parts ×ˢ (chunk hP G ε sorry).parts,
      HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
    HPow.hPow (α := ℝ) 16 #P.parts
Tactic: rw [distinctPairs, ← add_sub_assoc, add_sub_right_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ (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
have 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 ε sorry).parts ×ˢ (chunk hP G ε sorry).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ (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
have 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 ε sorry).parts ×ˢ (chunk hP G ε sorry).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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 +
      0 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts
have pos : HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity (↑x : Finset α × Finset α).1 (↑x : Finset α × Finset α).2) : ℝ) 2 -
    HPow.hPow (β := ℕ) ε 5 / 25 ≤
  (∑ i ∈ (chunk hP G ε sorry).parts ×ˢ (chunk hP G ε sorry).parts,
      HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
    HPow.hPow (α := ℝ) 16 #P.parts
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ (↑(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
have ha : HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≠ 0
Tactic: rw [coe_energy, add_div, mul_div_cancel_left₀]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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.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
have 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
Tactic: rw [card_increment hPα hPG, coe_stepBound, mul_pow, pow_right_comm,
          div_mul_eq_div_div_swap, ← sum_div]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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.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) : ℝ)
have 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
Tactic: rw [coe_energy]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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.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
have 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)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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,
      ∑ 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)
have 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)
Tactic: rw [← sum_biUnion pairwiseDisjoint_distinctPairs]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
⊢ (↑(P.energy G) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 4 ≤ (↑((increment hP G ε).energy G) : ℝ)
have _ : (∑ 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: 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 _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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
have 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
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (hypothesis)
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) ≤
    ∑ x ∈ P.parts.offDiag.attach,
      (∑ i ∈ distinctPairs hP G ε x, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
        HPow.hPow (α := ℝ) 16 #P.parts
have hPG₁ : (↑(#P.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
Tactic: rw [Finpartition.IsUniform, not_le, mul_tsub, mul_one, ← offDiag_card] at hPG
Cleared hypotheses: hPG, hε₀, hε₁
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
        (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
    ∑ x ∈ P.parts.offDiag,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
        ((if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3) - HPow.hPow (β := ℕ) ε 5 / 25))
have rw : ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
    ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
  HAdd.hAdd (α := ℝ) (∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2)
    (∑ x ∈ P.parts.offDiag,
      ((if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3) - HPow.hPow (β := ℕ) ε 5 / 25))
Tactic: rw [sum_add_distrib, sum_sub_distrib, sum_const, nsmul_eq_mul, sum_ite, sum_const_zero,
          zero_add, sum_const, nsmul_eq_mul, ← Finpartition.nonUniforms, ← add_sub_assoc,
          add_sub_right_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
rw :
  ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
        (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
    HAdd.hAdd (α := ℝ) (∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2)
      (∑ x ∈ P.parts.offDiag,
        ((if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3) - HPow.hPow (β := ℕ) ε 5 / 25))
⊢ ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
        (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
    ∑ x ∈ P.parts.offDiag,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
        ((if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3) - HPow.hPow (β := ℕ) ε 5 / 25))
have rw₁ : ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
    ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
  ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
    HSub.hSub (α := ℝ) (∑ x ∈ P.parts.offDiag, if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3)
      (∑ x ∈ P.parts.offDiag, HPow.hPow (β := ℕ) ε 5 / 25)
Tactic: rw [sum_add_distrib, sum_sub_distrib, sum_const, nsmul_eq_mul, sum_ite, sum_const_zero,
          zero_add, sum_const, nsmul_eq_mul, ← Finpartition.nonUniforms, ← add_sub_assoc,
          add_sub_right_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Increment (goal)
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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
rw :
  ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
        (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
    HAdd.hAdd (α := ℝ) (∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2)
      (∑ x ∈ P.parts.offDiag,
        ((if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3) - HPow.hPow (β := ℕ) ε 5 / 25))
rw₁ :
  ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
        (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
    ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      HSub.hSub (α := ℝ) (∑ x ∈ P.parts.offDiag, if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3)
        (∑ x ∈ P.parts.offDiag, HPow.hPow (β := ℕ) ε 5 / 25)
⊢ ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
      ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
        (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
    ∑ x ∈ P.parts.offDiag,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
        ((if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3) - HPow.hPow (β := ℕ) ε 5 / 25))
have rw₂ : ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
    ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)) =
  ∑ x ∈ P.parts.offDiag, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
    ((∑ x ∈ P.parts.offDiag, if G.IsUniform ε x.1 x.2 then 0 else HPow.hPow (β := ℕ) ε 4 / 3) -
      #P.parts.offDiag • (HPow.hPow (β := ℕ) ε 5 / 25))
Tactic: rw [sum_add_distrib, sum_sub_distrib, sum_const, nsmul_eq_mul, sum_ite, sum_const_zero,
          zero_add, sum_const, nsmul_eq_mul, ← Finpartition.nonUniforms, ← add_sub_assoc,
          add_sub_right_comm]