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
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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)

Tactic:
rw [Finpartition.IsUniform, not_le, mul_tsub, mul_one, ← offDiag_card] at hPG

Premises used: not_le, Finset.offDiag_card, Finpartition.IsUniform, mul_one, mul_tsub
-- 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
hPG₁ : (↑(#P.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
⊢ 0 ≤ ε

Tactic:
rw [Finpartition.IsUniform, not_le, mul_tsub, mul_one, ← offDiag_card] at hPG

Premises used: not_le, Finset.offDiag_card, Finpartition.IsUniform, mul_one, mul_tsub
-- 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
hPG₁ : (↑(#P.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₂ : 0 ≤ ε
⊢ ε ≤ 1

Tactic:
rw [Finpartition.IsUniform, not_le, mul_tsub, mul_one, ← offDiag_card] at hPG

Premises used: not_le, Finset.offDiag_card, Finpartition.IsUniform, mul_one, mul_tsub
-- 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.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))

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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ Eq (α := ℝ)
    (∑ 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)))
    (∑ x ∈ P.parts.offDiag.attach,
      (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)))

Tactic:
(sum_attach ..).symm

Premises used: Finset.sum_attach, Eq.symm
-- 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ LE.le (α := ℝ)
    (∑ x ∈ P.parts.offDiag.attach,
      (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 ∈ P.parts.offDiag.attach,
      (∑ i ∈ distinctPairs hP G ε i, HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2) /
        HPow.hPow (α := ℝ) 16 #P.parts)

Tactic:
sum_le_sum fun i _ ↦ le_sum_distinctPairs_edgeDensity_sq i hε₁ hPα hPε

Premises used: SzemerediRegularity.le_sum_distinctPairs_edgeDensity_sq, Finset.sum_le_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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms 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, 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 +
      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:
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ε

Premises used: SzemerediRegularity.le_sum_distinctPairs_edgeDensity_sq, HMul.hMul, HSub.hSub, Finset.sum_attach, HDiv.hDiv, Finpartition.parts, Finset.offDiag, Nat.cast, HPow.hPow, Finset.card, Finpartition.nonUniforms, Finset.sum_le_sum, OfNat.ofNat, Eq.symm
-- 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
hab :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4) ≤
    (↑(#(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 +
      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:
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.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)

Tactic:
ring
-- 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
h₁ : 6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≤ (↑(#P.parts.offDiag) : ℝ)
h₂ : 7 / 24 ≤ 22 / 75
⊢ 6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * HPow.hPow (β := ℕ) ε 5 * (7 / 24) ≤
    (↑(#P.parts.offDiag) : ℝ) * HPow.hPow (β := ℕ) ε 5 * (22 / 75)

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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ LT.lt (α := ℝ) 0 7

Tactic:
simp
-- 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
h₁ : 6 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≤ HMul.hMul (α := ℝ) (↑(#P.parts * #P.parts - #P.parts) : ℝ) 7
⊢ 6 / 7 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≤ (↑(#P.parts.offDiag) : ℝ)

Tactic:
rw [← mul_div_right_comm, div_le_iff₀ (by simp), offDiag_card]

Premises used: div_le_iff₀, Finset.offDiag_card, mul_div_right_comm
-- 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
h₁ : 6 * HPow.hPow (β := ℕ) (#P.parts) 2 ≤ (#P.parts * #P.parts - #P.parts) * 7
⊢ 6 * HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 ≤ HMul.hMul (α := ℝ) (↑(#P.parts * #P.parts - #P.parts) : ℝ) 7

Tactic:
norm_cast
-- 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
h₁ : 6 * HPow.hPow (β := ℕ) (#P.parts) 2 ≤ #P.parts * #P.parts * 7 - #P.parts * 7
⊢ 6 * HPow.hPow (β := ℕ) (#P.parts) 2 ≤ (#P.parts * #P.parts - #P.parts) * 7

Tactic:
rw [tsub_mul]

Premises used: tsub_mul
-- 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 6 * HPow.hPow (β := ℕ) (#P.parts) 2 ≤ #P.parts * #P.parts * 7 - #P.parts * 7

Tactic:
le_tsub_of_add_le_left ?_

Premises used: le_tsub_of_add_le_left
-- 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
h₁ : #P.parts * 7 + 6 * HPow.hPow (β := ℕ) (#P.parts) 2 ≤ #P.parts * #P.parts * 7
⊢ 6 * HPow.hPow (β := ℕ) (#P.parts) 2 ≤ #P.parts * #P.parts * 7 - #P.parts * 7

Tactic:
refine le_tsub_of_add_le_left ?_

Premises used: le_tsub_of_add_le_left
-- 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
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
⊢ #P.parts * 7 + 6 * HPow.hPow (β := ℕ) (#P.parts) 2 ≤ #P.parts * #P.parts * 7

Tactic:
nlinarith
-- 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 7 / 24 ≤ 22 / 75

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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (↑(#P.parts.offDiag) : ℝ) * HPow.hPow (β := ℕ) ε 5 * (22 / 75) =
    (↑(#P.parts.offDiag) : ℝ) * ε * (HPow.hPow (β := ℕ) ε 4 / 3) -
      (↑(#P.parts.offDiag) : ℝ) * (HPow.hPow (β := ℕ) ε 5 / 25)

Tactic:
ring
-- 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.parts.offDiag) : ℝ) * ε < (↑(#(P.nonUniforms G ε)) : ℝ)
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
h : 0 ≤ HPow.hPow (β := ℕ) ε 4 / 3
⊢ (↑(#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:
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.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)
_₃ :
  (↑(#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)
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(#P.parts) : ℝ) 2 * (HPow.hPow (β := ℕ) ε 5 / 4) ≤
    (↑(#(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

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Finpartition.parts, Finset.offDiag, Nat.cast, HPow.hPow, Finset.card, Finpartition.nonUniforms, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
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 ε
inr :
  ∀ (hα : bound ε l ≤ Fintype.card α),
    ∃ (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 ε

Tactic:
obtain hα | hα := le_total (card α) (bound ε l)

Premises used: SzemerediRegularity.bound, Fintype.card, le_total
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
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 ε

Tactic:
⟨⊥, bot_isEquipartition _, ?_⟩

Premises used: Bot.bot, And.intro, Exists.intro, Finpartition.bot_isEquipartition
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
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
inl :
  l ≤ Finset.card.{u_1} (α := Finset α) (parts (a := univ) ⊥) ∧
    Finset.card.{u_1} (α := Finset α) (parts (a := univ) ⊥) ≤ bound ε l ∧ IsUniform (A := univ) ⊥ G ε
⊢ ∃ (P : Finpartition (α := Finset α) univ), P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

Tactic:
refine ⟨⊥, bot_isEquipartition _, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
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
inl : l ≤ Fintype.card α ∧ Fintype.card α ≤ bound ε l ∧ IsUniform (A := univ) ⊥ G ε
⊢ l ≤ Finset.card.{u_1} (α := Finset α) (parts (a := univ) ⊥) ∧
    Finset.card.{u_1} (α := Finset α) (parts (a := univ) ⊥) ≤ bound ε l ∧ IsUniform (A := univ) ⊥ G ε

Tactic:
rw [card_bot, card_univ]

Premises used: Finset.card_univ, Finpartition.card_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
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 ≤ Fintype.card α ∧ Fintype.card α ≤ bound ε l ∧ IsUniform (A := univ) ⊥ G ε

Tactic:
⟨hl, hα, bot_isUniform _ hε⟩

Premises used: Finpartition.bot_isUniform, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
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 ≤ Fintype.card α ∧ Fintype.card α ≤ bound ε l ∧ IsUniform (A := univ) ⊥ G ε

Tactic:
exact ⟨hl, hα, bot_isUniform _ hε⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
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
rwa rwa₁ rwa₂ rwa₃ : bound ε l ≤ Fintype.card α
⊢ bound ε l ≤ Finset.card.{u_1} (α := α) univ

Tactic:
rwa [Finset.card_univ]

Premises used: Finset.card_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
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
⊢ t ≤ Finset.card.{u_1} (α := α) univ

Tactic:
have htα : t ≤ #(univ : Finset α) :=
    (initialBound_le_bound _ _).trans (by rwa [Finset.card_univ])