awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
⊢ ε ≤
    (↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
              (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
            G.edgeDensity s t| :
      𝕜)
have inr : ε ≤ (↑|G.edgeDensity (G.nonuniformWitnesses ε t s).1 (G.nonuniformWitnesses ε t s).2 - G.edgeDensity t s| : 𝕜)
Tactic: rw [if_neg (asymm gt), if_pos gt, edgeDensity_comm, edgeDensity_comm _ s]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
u v : Finset α
ε : 𝕜
⊢ (u, v) ∈ P.sparsePairs G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
have rw : (u, v) ∈
    {x ∈ P.parts.offDiag |
      match (motive := Finset α × Finset α → Prop) x with
      | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε} ↔
  u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
Tactic: rw [sparsePairs, mem_filter, mem_offDiag, and_assoc, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
u v : Finset α
ε : 𝕜
rw :
  (u, v) ∈
      {x ∈ P.parts.offDiag |
        match (motive := Finset α × Finset α → Prop) x with
        | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε} ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
⊢ (u, v) ∈ P.sparsePairs G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
have rw₁ : ((u, v) ∈ P.parts.offDiag ∧
    match (motive := Finset α × Finset α → Prop) (u, v) with
    | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
  u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
Tactic: rw [sparsePairs, mem_filter, mem_offDiag, and_assoc, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
u v : Finset α
ε : 𝕜
rw :
  (u, v) ∈
      {x ∈ P.parts.offDiag |
        match (motive := Finset α × Finset α → Prop) x with
        | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε} ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
rw₁ :
  ((u, v) ∈ P.parts.offDiag ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
⊢ (u, v) ∈ P.sparsePairs G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
have rw₂ : (((u, v).1 ∈ P.parts ∧ (u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
    match (motive := Finset α × Finset α → Prop) (u, v) with
    | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
  u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
Tactic: rw [sparsePairs, mem_filter, mem_offDiag, and_assoc, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
u v : Finset α
ε : 𝕜
rw :
  (u, v) ∈
      {x ∈ P.parts.offDiag |
        match (motive := Finset α × Finset α → Prop) x with
        | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε} ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
rw₁ :
  ((u, v) ∈ P.parts.offDiag ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
rw₂ :
  (((u, v).1 ∈ P.parts ∧ (u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
⊢ (u, v) ∈ P.sparsePairs G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
have rw₃ : ((u, v).1 ∈ P.parts ∧
    ((u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
  u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
Tactic: rw [sparsePairs, mem_filter, mem_offDiag, and_assoc, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
u v : Finset α
ε : 𝕜
rw :
  (u, v) ∈
      {x ∈ P.parts.offDiag |
        match (motive := Finset α × Finset α → Prop) x with
        | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε} ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
rw₁ :
  ((u, v) ∈ P.parts.offDiag ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
rw₂ :
  (((u, v).1 ∈ P.parts ∧ (u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
rw₃ :
  ((u, v).1 ∈ P.parts ∧
      ((u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
        match (motive := Finset α × Finset α → Prop) (u, v) with
        | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
⊢ (u, v) ∈ P.sparsePairs G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
have rw₄ : ((u, v).1 ∈ P.parts ∧
    (u, v).2 ∈ P.parts ∧
      (u, v).1 ≠ (u, v).2 ∧
        match (motive := Finset α × Finset α → Prop) (u, v) with
        | (u, v) => (↑(G.edgeDensity u v) : 𝕜) < ε) ↔
  u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ (↑(G.edgeDensity u v) : 𝕜) < ε
Tactic: rw [sparsePairs, mem_filter, mem_offDiag, and_assoc, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
u v : Finset α
⊢ (u, v) ∈ P.nonUniforms G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
have rw : (u, v) ∈
    {x ∈ P.parts.offDiag |
      match (motive := Finset α × Finset α → Prop) x with
      | (u, v) => ¬G.IsUniform ε u v} ↔
  u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
Tactic: rw [nonUniforms, mem_filter, mem_offDiag, and_assoc, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
u v : Finset α
rw :
  (u, v) ∈
      {x ∈ P.parts.offDiag |
        match (motive := Finset α × Finset α → Prop) x with
        | (u, v) => ¬G.IsUniform ε u v} ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
⊢ (u, v) ∈ P.nonUniforms G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
have rw₁ : ((u, v) ∈ P.parts.offDiag ∧
    match (motive := Finset α × Finset α → Prop) (u, v) with
    | (u, v) => ¬G.IsUniform ε u v) ↔
  u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
Tactic: rw [nonUniforms, mem_filter, mem_offDiag, and_assoc, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
u v : Finset α
rw :
  (u, v) ∈
      {x ∈ P.parts.offDiag |
        match (motive := Finset α × Finset α → Prop) x with
        | (u, v) => ¬G.IsUniform ε u v} ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
rw₁ :
  ((u, v) ∈ P.parts.offDiag ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => ¬G.IsUniform ε u v) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
⊢ (u, v) ∈ P.nonUniforms G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
have rw₂ : (((u, v).1 ∈ P.parts ∧ (u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
    match (motive := Finset α × Finset α → Prop) (u, v) with
    | (u, v) => ¬G.IsUniform ε u v) ↔
  u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
Tactic: rw [nonUniforms, mem_filter, mem_offDiag, and_assoc, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
u v : Finset α
rw :
  (u, v) ∈
      {x ∈ P.parts.offDiag |
        match (motive := Finset α × Finset α → Prop) x with
        | (u, v) => ¬G.IsUniform ε u v} ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
rw₁ :
  ((u, v) ∈ P.parts.offDiag ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => ¬G.IsUniform ε u v) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
rw₂ :
  (((u, v).1 ∈ P.parts ∧ (u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => ¬G.IsUniform ε u v) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
⊢ (u, v) ∈ P.nonUniforms G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
have rw₃ : ((u, v).1 ∈ P.parts ∧
    ((u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => ¬G.IsUniform ε u v) ↔
  u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
Tactic: rw [nonUniforms, mem_filter, mem_offDiag, and_assoc, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_3 : DecidableRel G.Adj
ε : 𝕜
u v : Finset α
rw :
  (u, v) ∈
      {x ∈ P.parts.offDiag |
        match (motive := Finset α × Finset α → Prop) x with
        | (u, v) => ¬G.IsUniform ε u v} ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
rw₁ :
  ((u, v) ∈ P.parts.offDiag ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => ¬G.IsUniform ε u v) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
rw₂ :
  (((u, v).1 ∈ P.parts ∧ (u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
      match (motive := Finset α × Finset α → Prop) (u, v) with
      | (u, v) => ¬G.IsUniform ε u v) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
rw₃ :
  ((u, v).1 ∈ P.parts ∧
      ((u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
        match (motive := Finset α × Finset α → Prop) (u, v) with
        | (u, v) => ¬G.IsUniform ε u v) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
⊢ (u, v) ∈ P.nonUniforms G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
have rw₄ : ((u, v).1 ∈ P.parts ∧
    (u, v).2 ∈ P.parts ∧
      (u, v).1 ≠ (u, v).2 ∧
        match (motive := Finset α × Finset α → Prop) (u, v) with
        | (u, v) => ¬G.IsUniform ε u v) ↔
  u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
Tactic: rw [nonUniforms, mem_filter, mem_offDiag, and_assoc, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ nonUniforms (A := A) ⊥ G ε = ∅
have rw : ∀ (x : Finset α × Finset α), x ∉ nonUniforms (A := A) ⊥ G ε
Tactic: rw [eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ (u, v) ∉ nonUniforms (A := A) ⊥ G ε
have simp : ∀ (x : α),
  x ∈ A ∧ ({ toFun := singleton, inj' := sorry : α ↪ Finset α } : (a : α) → Finset α) x = u →
    ∀ (x : α),
      x ∈ A ∧ ({ toFun := singleton, inj' := sorry : α ↪ Finset α } : (a : α) → Finset α) x = v → u ≠ v → G.IsUniform ε u v
Tactic: simp only [mk_mem_nonUniforms, parts_bot, mem_map, not_and,
    Classical.not_not, exists_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ IsUniform (A := A) ⊥ G ε
have rw : 0 ≤ (↑(#A * (#A - 1)) : 𝕜) * ε
Tactic: rw [Finpartition.IsUniform, Finpartition.card_bot, nonUniforms_bot _ hε, Finset.card_empty,
    Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
⊢ IsUniform.{u_1, u_2} (𝕜 := 𝕜) P G 1
have rw : #(nonUniforms.{u_1, u_2} (𝕜 := 𝕜) P G 1) ≤ #P.parts * (#P.parts - 1)
Tactic: rw [IsUniform, mul_one, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
⊢ #(nonUniforms.{u_1, u_2} (𝕜 := 𝕜) P G 1) ≤ #P.parts * (#P.parts - 1)
have refine : #P.parts.offDiag ≤ #P.parts * (#P.parts - 1)
Tactic: refine (card_filter_le _
    (fun uv => ¬SimpleGraph.IsUniform G 1 (Prod.fst uv) (Prod.snd uv))).trans ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
⊢ #P.parts.offDiag ≤ #P.parts * (#P.parts - 1)
have rw : #P.parts * #P.parts - #P.parts ≤ #P.parts * (#P.parts - 1)
Tactic: rw [offDiag_card, Nat.mul_sub_left_distrib, mul_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
rw : #P.parts * #P.parts - #P.parts ≤ #P.parts * (#P.parts - 1)
⊢ #P.parts.offDiag ≤ #P.parts * (#P.parts - 1)
have rw₁ : #P.parts * #P.parts - #P.parts ≤ #P.parts * #P.parts - #P.parts * 1
Tactic: rw [offDiag_card, Nat.mul_sub_left_distrib, mul_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
rw : #P.parts * #P.parts - #P.parts ≤ #P.parts * (#P.parts - 1)
rw₁ : #P.parts * #P.parts - #P.parts ≤ #P.parts * #P.parts - #P.parts * 1
⊢ #P.parts.offDiag ≤ #P.parts * (#P.parts - 1)
have rw₂ : #P.parts * #P.parts - #P.parts ≤ #P.parts * #P.parts - #P.parts
Tactic: rw [offDiag_card, Nat.mul_sub_left_distrib, mul_one]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε ε' : 𝕜
hP : P.IsUniform G ε
h : ε ≤ ε'
⊢ (↑(#P.parts * (#P.parts - 1)) : 𝕜) * ε ≤ (↑(#P.parts * (#P.parts - 1)) : 𝕜) * ε'
have ha : LE.le.{u_2} (α := 𝕜) 0 (↑(#P.parts * (#P.parts - 1)) : 𝕜)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ LE.le.{u_2} (α := 𝕜) (∑ UV ∈ P.sparsePairs G ε, ε * HMul.hMul (α := 𝕜) (↑(#UV.1) : 𝕜) (↑(#UV.2) : 𝕜))
    (∑ UV ∈ P.parts.offDiag, ε * HMul.hMul (α := 𝕜) (↑(#UV.1) : 𝕜) (↑(#UV.2) : 𝕜))
have h : P.sparsePairs G ε ⊆ P.parts.offDiag
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ (↑(card (α := α × α)
          ((P.sparsePairs G ε).biUnion fun (x : Finset α × Finset α) ↦
            match (motive := Finset α × Finset α → Finset (α × α)) x with
            | (U, V) => G.interedges U V)) :
      𝕜) ≤
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2
have calc_1 : LE.le.{u_2} (α := 𝕜) (∑ UV ∈ P.sparsePairs G ε, (↑(#(G.interedges UV.1 UV.2)) : 𝕜))
  (∑ UV ∈ P.sparsePairs G ε, ε * HMul.hMul (α := 𝕜) (↑(#UV.1) : 𝕜) (↑(#UV.2) : 𝕜))
Tactic: calc
    _ ≤ ∑ UV ∈ P.sparsePairs G ε, (#(G.interedges UV.1 UV.2) : 𝕜) := mod_cast card_biUnion_le
    _ ≤ ∑ UV ∈ P.sparsePairs G ε, ε * (#UV.1 * #UV.2) := ?_
    _ ≤ ∑ UV ∈ P.parts.offDiag, ε * (#UV.1 * #UV.2) := by gcongr; apply filter_subset
    _ = ε * ∑ UV ∈ P.parts.offDiag, (#UV.1 * #UV.2 : 𝕜) := (mul_sum _ _ _).symm
    _ ≤ _ := ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
calc_1 :
  LE.le.{u_2} (α := 𝕜) (∑ UV ∈ P.sparsePairs G ε, (↑(#(G.interedges UV.1 UV.2)) : 𝕜))
    (∑ UV ∈ P.sparsePairs G ε, ε * HMul.hMul (α := 𝕜) (↑(#UV.1) : 𝕜) (↑(#UV.2) : 𝕜))
⊢ (↑(card (α := α × α)
          ((P.sparsePairs G ε).biUnion fun (x : Finset α × Finset α) ↦
            match (motive := Finset α × Finset α → Finset (α × α)) x with
            | (U, V) => G.interedges U V)) :
      𝕜) ≤
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2
have calc_2 : ε * ∑ UV ∈ P.parts.offDiag, HMul.hMul (α := 𝕜) (↑(#UV.1) : 𝕜) (↑(#UV.2) : 𝕜) ≤
  ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2
Tactic: calc
    _ ≤ ∑ UV ∈ P.sparsePairs G ε, (#(G.interedges UV.1 UV.2) : 𝕜) := mod_cast card_biUnion_le
    _ ≤ ∑ UV ∈ P.sparsePairs G ε, ε * (#UV.1 * #UV.2) := ?_
    _ ≤ ∑ UV ∈ P.parts.offDiag, ε * (#UV.1 * #UV.2) := by gcongr; apply filter_subset
    _ = ε * ∑ UV ∈ P.parts.offDiag, (#UV.1 * #UV.2 : 𝕜) := (mul_sum _ _ _).symm
    _ ≤ _ := ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ LE.le.{u_2} (α := 𝕜) (∑ UV ∈ P.sparsePairs G ε, (↑(#(G.interedges UV.1 UV.2)) : 𝕜))
    (∑ UV ∈ P.sparsePairs G ε, ε * HMul.hMul (α := 𝕜) (↑(#UV.1) : 𝕜) (↑(#UV.2) : 𝕜))
have calc_1 : ∀ (U V : Finset α) (hUV : (U, V) ∈ P.sparsePairs G ε),
  (↑(#(G.interedges (U, V).1 (U, V).2)) : 𝕜) ≤ ε * HMul.hMul (α := 𝕜) (↑(#(U, V).1) : 𝕜) (↑(#(U, V).2) : 𝕜)
Tactic: gcongr with ⟨U, V⟩ hUV
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
U V : Finset α
hUV : (U, V) ∈ P.sparsePairs G ε
⊢ (↑(#(G.interedges (U, V).1 (U, V).2)) : 𝕜) ≤ ε * HMul.hMul (α := 𝕜) (↑(#(U, V).1) : 𝕜) (↑(#(U, V).2) : 𝕜)
have hUV₁ : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V ∧ (↑(#(G.interedges U V)) : 𝕜) / HMul.hMul (α := 𝕜) (↑(#U) : 𝕜) (↑(#V) : 𝕜) < ε
Tactic: simp only [mk_mem_sparsePairs, ne_eq, ← card_interedges_div_card, Rat.cast_div,
      Rat.cast_natCast, Rat.cast_mul] at hUV
Cleared hypotheses: hUV
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
U V : Finset α
hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V ∧ (↑(#(G.interedges U V)) : 𝕜) / HMul.hMul (α := 𝕜) (↑(#U) : 𝕜) (↑(#V) : 𝕜) < ε
⊢ (↑(#(G.interedges (U, V).1 (U, V).2)) : 𝕜) ≤ ε * HMul.hMul (α := 𝕜) (↑(#(U, V).1) : 𝕜) (↑(#(U, V).2) : 𝕜)
have calc_1 : 0 < HMul.hMul (α := 𝕜) (↑(#U) : 𝕜) (↑(#V) : 𝕜)
Tactic: refine ((div_lt_iff₀ ?_).1 hUV.2.2.2).le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ε * ∑ UV ∈ P.parts.offDiag, HMul.hMul (α := 𝕜) (↑(#UV.1) : 𝕜) (↑(#UV.2) : 𝕜) ≤
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2
have calc_2 : ε * (↑(∑ x ∈ P.parts.offDiag, #x.1 * #x.2) : 𝕜) ≤ ε * (↑(HPow.hPow (β := ℕ) (#A + #P.parts) 2) : 𝕜)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ε * (↑(∑ x ∈ P.parts.offDiag, #x.1 * #x.2) : 𝕜) ≤ ε * (↑(HPow.hPow (β := ℕ) (#A + #P.parts) 2) : 𝕜)
have calc_2 : ∑ x ∈ P.parts.offDiag, #x.1 * #x.2 ≤ HPow.hPow (β := ℕ) (#A + #P.parts) 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ HPow.hPow (β := ℕ) (#P.parts * (#A / #P.parts) + #P.parts) 2 ≤ HPow.hPow (β := ℕ) (#A + #P.parts) 2
have hab : #P.parts * (#A / #P.parts) ≤ #A
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst_4 : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∑ x ∈ P.parts.offDiag, #x.1 * #x.2 ≤ HPow.hPow (β := ℕ) (#A + #P.parts) 2
have calc_2 : ∀ x ∈ P.parts.offDiag, (fun (i : Finset α × Finset α) ↦ #i.1 * #i.2) x ≤ HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2
Tactic: calc
    (_ : ℕ) ≤ _ := sum_le_card_nsmul P.parts.offDiag (fun i ↦ #i.1 * #i.2)
            ((#A / #P.parts + 1) ^ 2 : ℕ) ?_
    _ ≤ (#P.parts * (#A / #P.parts) + #P.parts) ^ 2 := ?_
    _ ≤ _ := by gcongr; apply Nat.mul_div_le