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
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)
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))
⊢ ∑ 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]
-- 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 +
      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 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, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2 +
    ((↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25))
Tactic: calc
    _ ≤ ∑ x ∈ P.parts.offDiag, (edgeDensity G x.1 x.2 : ℝ) ^ 2 +
        (#(nonUniforms P G ε) * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := ?_
    _ = ∑ x ∈ P.parts.offDiag, ((G.edgeDensity x.1 x.2 : ℝ) ^ 2 +
        ((if G.IsUniform ε x.1 x.2 then (0 : ℝ) else ε ^ 4 / 3) - ε ^ 5 / 25) : ℝ) := by
        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]
    _ = _ := (sum_attach ..).symm
    _ ≤ _ := sum_le_sum fun i _ ↦ le_sum_distinctPairs_edgeDensity_sq i hε₁ hPα hPε
-- 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 +
      HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4) ≤
    ∑ 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))
have hab : HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4) ≤
  (↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
    (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)
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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * HPow.hPow (β := ℕ) ε 5 * (7 / 24) ≤
    (↑(#P.parts.offDiag) : ℝ) * HPow.hPow (β := ℕ) ε 5 * (22 / 75)
have h₁ : 6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≤ (↑(#P.parts.offDiag) : ℝ)
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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
h₁ : 6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≤ (↑(#P.parts.offDiag) : ℝ)
⊢ 6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * HPow.hPow (β := ℕ) ε 5 * (7 / 24) ≤
    (↑(#P.parts.offDiag) : ℝ) * HPow.hPow (β := ℕ) ε 5 * (22 / 75)
have h₂ : 7 / 24 ≤ 22 / 75
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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≤ (↑(#P.parts.offDiag) : ℝ)
have h₁ : 6 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≤ HMul.hMul (α := ℝ) (↑(#P.parts * #P.parts - #P.parts) : ℝ) 7
Tactic: rw [← mul_div_right_comm, div_le_iff₀ (by simp), offDiag_card]
-- 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
⊢ 6 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≤ HMul.hMul (α := ℝ) (↑(#P.parts * #P.parts - #P.parts) : ℝ) 7
have h₁ : 6 * HPow.hPow (β := ℕ) (#P.parts) 2 ≤ (#P.parts * #P.parts - #P.parts) * 7
Tactic: norm_cast
-- 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
⊢ 6 * HPow.hPow (β := ℕ) (#P.parts) 2 ≤ (#P.parts * #P.parts - #P.parts) * 7
have h₁ : 6 * HPow.hPow (β := ℕ) (#P.parts) 2 ≤ #P.parts * #P.parts * 7 - #P.parts * 7
Tactic: rw [tsub_mul]
-- 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
⊢ 6 * HPow.hPow (β := ℕ) (#P.parts) 2 ≤ #P.parts * #P.parts * 7 - #P.parts * 7
have h₁ : #P.parts * 7 + 6 * HPow.hPow (β := ℕ) (#P.parts) 2 ≤ #P.parts * #P.parts * 7
Tactic: refine le_tsub_of_add_le_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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ #P.parts * 7 + 6 * HPow.hPow (β := ℕ) (#P.parts) 2 ≤ #P.parts * #P.parts * 7
have nlinarith : #P.parts * #P.parts * 7 < #P.parts * 7 + 6 * HPow.hPow (β := ℕ) (#P.parts) 2 →
  -1 +
        (HMul.hMul (α := ℤ) (↑(#P.parts) : ℤ) (↑(#P.parts) : ℤ) * 7 + 1 -
          (HMul.hMul (α := ℤ) (↑(#P.parts) : ℤ) 7 + 6 * HPow.hPow (α := ℤ) (β := ℕ) (↑(#P.parts) : ℤ) 2)) +
      (0 - HSub.hSub (α := ℤ) 0 (↑(#P.parts) : ℤ) * HSub.hSub (α := ℤ) 7 (↑(#P.parts) : ℤ)) =
    0
Tactic: nlinarith
-- 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
⊢ (↑(#P.parts.offDiag) : ℝ) * ε * (HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25) ≤
    (↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)
have h : 0 ≤ HPow.hPow (β := ℕ) ε 4 / 3
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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4) ≤
    (↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)
have _ : HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4) =
  6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * HPow.hPow (β := ℕ) ε 5 * (7 / 24)
Tactic: calc
    _ = (6 / 7 * #P.parts ^ 2) * ε ^ 5 * (7 / 24) := by ring
    _ ≤ #P.parts.offDiag * ε ^ 5 * (22 / 75) := by
        gcongr ?_ * _ * ?_
        · rw [← mul_div_right_comm, div_le_iff₀ (by simp), offDiag_card]
          norm_cast
          rw [tsub_mul]
          refine le_tsub_of_add_le_left ?_
          nlinarith
        · norm_num
    _ = (#P.parts.offDiag * ε * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := by ring
    _ ≤ (#(nonUniforms P G ε) * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := by 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
_ :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4) =
    6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * HPow.hPow (β := ℕ) ε 5 * (7 / 24)
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4) ≤
    (↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)
have _₁ : 6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * HPow.hPow (β := ℕ) ε 5 * (7 / 24) ≤
  (↑(#P.parts.offDiag) : ℝ) * HPow.hPow (β := ℕ) ε 5 * (22 / 75)
Tactic: calc
    _ = (6 / 7 * #P.parts ^ 2) * ε ^ 5 * (7 / 24) := by ring
    _ ≤ #P.parts.offDiag * ε ^ 5 * (22 / 75) := by
        gcongr ?_ * _ * ?_
        · rw [← mul_div_right_comm, div_le_iff₀ (by simp), offDiag_card]
          norm_cast
          rw [tsub_mul]
          refine le_tsub_of_add_le_left ?_
          nlinarith
        · norm_num
    _ = (#P.parts.offDiag * ε * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := by ring
    _ ≤ (#(nonUniforms P G ε) * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := by 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
_ :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4) =
    6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * HPow.hPow (β := ℕ) ε 5 * (7 / 24)
_₁ :
  6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * HPow.hPow (β := ℕ) ε 5 * (7 / 24) ≤
    (↑(#P.parts.offDiag) : ℝ) * HPow.hPow (β := ℕ) ε 5 * (22 / 75)
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4) ≤
    (↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)
have _₂ : (↑(#P.parts.offDiag) : ℝ) * HPow.hPow (β := ℕ) ε 5 * (22 / 75) =
  (↑(#P.parts.offDiag) : ℝ) * ε * (HPow.hPow (β := ℕ) ε 4 / 3) -
    (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)
Tactic: calc
    _ = (6 / 7 * #P.parts ^ 2) * ε ^ 5 * (7 / 24) := by ring
    _ ≤ #P.parts.offDiag * ε ^ 5 * (22 / 75) := by
        gcongr ?_ * _ * ?_
        · rw [← mul_div_right_comm, div_le_iff₀ (by simp), offDiag_card]
          norm_cast
          rw [tsub_mul]
          refine le_tsub_of_add_le_left ?_
          nlinarith
        · norm_num
    _ = (#P.parts.offDiag * ε * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := by ring
    _ ≤ (#(nonUniforms P G ε) * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := by 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
_ :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4) =
    6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * HPow.hPow (β := ℕ) ε 5 * (7 / 24)
_₁ :
  6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * HPow.hPow (β := ℕ) ε 5 * (7 / 24) ≤
    (↑(#P.parts.offDiag) : ℝ) * HPow.hPow (β := ℕ) ε 5 * (22 / 75)
_₂ :
  (↑(#P.parts.offDiag) : ℝ) * HPow.hPow (β := ℕ) ε 5 * (22 / 75) =
    (↑(#P.parts.offDiag) : ℝ) * ε * (HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4) ≤
    (↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)
have _₃ : (↑(#P.parts.offDiag) : ℝ) * ε * (HPow.hPow (β := ℕ) ε 4 / 3) -
    (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25) ≤
  (↑(#(P.nonUniforms G ε)) : ℝ) * (HPow.hPow (β := ℕ) ε 4 / 3) -
    (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)
Tactic: calc
    _ = (6 / 7 * #P.parts ^ 2) * ε ^ 5 * (7 / 24) := by ring
    _ ≤ #P.parts.offDiag * ε ^ 5 * (22 / 75) := by
        gcongr ?_ * _ * ?_
        · rw [← mul_div_right_comm, div_le_iff₀ (by simp), offDiag_card]
          norm_cast
          rw [tsub_mul]
          refine le_tsub_of_add_le_left ?_
          nlinarith
        · norm_num
    _ = (#P.parts.offDiag * ε * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := by ring
    _ ≤ (#(nonUniforms P G ε) * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := by gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
have inl : ∀ (hα : Fintype.card α ≤ bound ε l),
  ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
Tactic: obtain hα | hα := le_total (card α) (bound ε l)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
inl :
  ∀ (hα : Fintype.card α ≤ bound ε l),
    ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
have inr : ∀ (hα : bound ε l ≤ Fintype.card α),
  ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
Tactic: obtain hα | hα := le_total (card α) (bound ε l)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
have inl : l ≤ Finset.card.{u_1} (α := Finset α) (parts (a := univ) ⊥) ∧
  Finset.card.{u_1} (α := Finset α) (parts (a := univ) ⊥) ≤ bound ε l ∧ IsUniform (A := univ) ⊥ G ε
Tactic: refine ⟨⊥, bot_isEquipartition _, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ l ≤ Finset.card.{u_1} (α := Finset α) (parts (a := univ) ⊥) ∧
    Finset.card.{u_1} (α := Finset α) (parts (a := univ) ⊥) ≤ bound ε l ∧ IsUniform (A := univ) ⊥ G ε
have inl : l ≤ Fintype.card α ∧ Fintype.card α ≤ bound ε l ∧ IsUniform (A := univ) ⊥ G ε
Tactic: rw [card_bot, card_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
have htα : t ≤ Finset.card.{u_1} (α := α) univ
Tactic: have htα : t ≤ #(univ : Finset α) :=
    (initialBound_le_bound _ _).trans (by rwa [Finset.card_univ])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card.{u_1} (α := α) univ
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
have inr : ∀ (dum : Finpartition (α := Finset α) univ) (hdum₁ : dum.IsEquipartition) (hdum₂ : #dum.parts = initialBound ε l),
  ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
Tactic: obtain ⟨dum, hdum₁, hdum₂⟩ :=
    exists_equipartition_card_eq (univ : Finset α) (initialBound_pos _ _).ne' htα
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card.{u_1} (α := α) univ
dum : Finpartition (α := Finset α) univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
have inr : ∀ (hε₁ : 1 ≤ ε),
  ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
Tactic: obtain hε₁ | hε₁ := le_total 1 ε