awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
rw₂ rw₃ : #P.parts * #P.parts - #P.parts ≤ #P.parts * #P.parts - #P.parts
⊢ #P.parts.offDiag ≤ #P.parts * (#P.parts - 1)

Tactic:
rw [offDiag_card, Nat.mul_sub_left_distrib, mul_one]

Premises used: Nat.mul_sub_left_distrib, Finset.offDiag_card, mul_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 : ε ≤ ε'
ha : LE.le.{u_2} (α := 𝕜) 0 (↑(#P.parts * (#P.parts - 1)) : 𝕜)
⊢ (↑(#P.parts * (#P.parts - 1)) : 𝕜) * ε ≤ (↑(#P.parts * (#P.parts - 1)) : 𝕜) * ε'

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
ε : 𝕜
hP : P.parts = ∅
⊢ P.IsUniform G ε

Tactic:
simp [IsUniform, hP, nonUniforms]

Premises used: Finpartition.IsUniform, Finpartition.nonUniforms
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
ε : 𝕜
h : ¬P.IsUniform G ε
⊢ P.parts.Nonempty

Tactic:
nonempty_of_ne_empty fun h₁ => h <| isUniformOfEmpty h₁

Premises used: Finpartition.isUniformOfEmpty, Finset.nonempty_of_ne_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
ε : 𝕜
s : Finset α
⊢ #(P.nonuniformWitnesses G ε s) ≤ #({t ∈ P.parts | s ≠ t ∧ ¬G.IsUniform ε s t})

Tactic:
card_image_le

Premises used: Finset.card_image_le, Finpartition.nonuniformWitnesses
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
ht : t ∈ P.parts
hst : s ≠ t
⊢ G.nonuniformWitness ε s t ∈ P.nonuniformWitnesses G ε s

Tactic:
mem_image_of_mem _ <| mem_filter.2 ⟨ht, hst, h⟩

Premises used: Iff.mpr, Set.Mem, setOf, And.intro, Finset.mem_filter, Finset.mem_image_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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) : 𝕜))

Tactic:
?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ≤ ε
h : P.sparsePairs G ε ⊆ P.parts.offDiag
⊢ LE.le.{u_2} (α := 𝕜) (∑ UV ∈ P.sparsePairs G ε, ε * HMul.hMul (α := 𝕜) (↑(#UV.1) : 𝕜) (↑(#UV.2) : 𝕜))
    (∑ UV ∈ P.parts.offDiag, ε * HMul.hMul (α := 𝕜) (↑(#UV.1) : 𝕜) (↑(#UV.2) : 𝕜))

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ≤ ε
⊢ P.sparsePairs G ε ⊆ P.parts.offDiag

Tactic:
apply filter_subset

Premises used: Finset.filter_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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) : 𝕜) =
    ε * ∑ UV ∈ P.parts.offDiag, HMul.hMul (α := 𝕜) (↑(#UV.1) : 𝕜) (↑(#UV.2) : 𝕜)

Tactic:
(mul_sum _ _ _).symm

Premises used: Finset.mul_sum, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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

Tactic:
?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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) : 𝕜))
calc_2 :
  ε * ∑ UV ∈ P.parts.offDiag, HMul.hMul (α := 𝕜) (↑(#UV.1) : 𝕜) (↑(#UV.2) : 𝕜) ≤
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 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

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
    _ ≤ _ := ?_

Premises used: Finset.mul_sum, Finpartition.parts, Finset.offDiag, Finset.card_biUnion_le, Finpartition.sparsePairs, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 :
  ∀ (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) : 𝕜)
⊢ 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:
gcongr with ⟨U, V⟩ hUV
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ε
⊢ 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

Premises used: Rat.cast_mul, Rat.cast_div, ne_eq, Rat.cast_natCast, Finpartition.mk_mem_sparsePairs, SimpleGraph.card_interedges_div_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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) : 𝕜)

Tactic:
((div_lt_iff₀ ?_).1 hUV.2.2.2).le

Premises used: LT.lt.le, div_lt_iff₀, And.right, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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) : 𝕜) < ε
calc_1 : 0 < HMul.hMul (α := 𝕜) (↑(#U) : 𝕜) (↑(#V) : 𝕜)
⊢ (↑(#(G.interedges (U, V).1 (U, V).2)) : 𝕜) ≤ ε * HMul.hMul (α := 𝕜) (↑(#(U, V).1) : 𝕜) (↑(#(U, V).2) : 𝕜)

Tactic:
refine ((div_lt_iff₀ ?_).1 hUV.2.2.2).le

Premises used: LT.lt.le, div_lt_iff₀, And.right, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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) : 𝕜) < ε
⊢ 0 < HMul.hMul (α := 𝕜) (↑(#U) : 𝕜) (↑(#V) : 𝕜)

Tactic:
mul_pos (Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.1).card_pos)
      (Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.2.1).card_pos)

Premises used: Iff.mpr, Nat.cast_pos, Finset.Nonempty.card_pos, mul_pos, And.right, And.left, Finpartition.nonempty_of_mem_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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) : 𝕜) < ε
⊢ 0 < HMul.hMul (α := 𝕜) (↑(#U) : 𝕜) (↑(#V) : 𝕜)

Tactic:
exact mul_pos (Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.1).card_pos)
      (Nat.cast_pos.2 (P.nonempty_of_mem_parts hUV.2.1).card_pos)

Premises used: Iff.mpr, Nat.cast_pos, Finset.Nonempty.card_pos, mul_pos, And.right, And.left, Finpartition.nonempty_of_mem_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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_2 : ε * (↑(∑ x ∈ P.parts.offDiag, #x.1 * #x.2) : 𝕜) ≤ ε * (↑(HPow.hPow (β := ℕ) (#A + #P.parts) 2) : 𝕜)
⊢ ε * ∑ UV ∈ P.parts.offDiag, HMul.hMul (α := 𝕜) (↑(#UV.1) : 𝕜) (↑(#UV.2) : 𝕜) ≤
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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_2 : ∑ x ∈ P.parts.offDiag, #x.1 * #x.2 ≤ HPow.hPow (β := ℕ) (#A + #P.parts) 2
⊢ ε * (↑(∑ x ∈ P.parts.offDiag, #x.1 * #x.2) : 𝕜) ≤ ε * (↑(HPow.hPow (β := ℕ) (#A + #P.parts) 2) : 𝕜)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ≤ ε
⊢ ∑ i ∈ P.parts.offDiag, #i.1 * #i.2 ≤ #P.parts.offDiag • HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2

Tactic:
sum_le_card_nsmul P.parts.offDiag (fun i ↦ #i.1 * #i.2)
            ((#A / #P.parts + 1) ^ 2 : ℕ) ?_

Premises used: HMul.hMul, HDiv.hDiv, Finpartition.parts, Finset.offDiag, Prod.fst, Finset.sum_le_card_nsmul, HPow.hPow, HAdd.hAdd, Finset.card, OfNat.ofNat, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ≤ ε
⊢ #P.parts.offDiag • HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2 ≤
    HPow.hPow (β := ℕ) (#P.parts * (#A / #P.parts) + #P.parts) 2

Tactic:
?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ≤ ε
hab : #P.parts * (#A / #P.parts) ≤ #A
⊢ HPow.hPow (β := ℕ) (#P.parts * (#A / #P.parts) + #P.parts) 2 ≤ HPow.hPow (β := ℕ) (#A + #P.parts) 2

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ≤ ε
⊢ #P.parts * (#A / #P.parts) ≤ #A

Tactic:
apply Nat.mul_div_le

Premises used: Nat.mul_div_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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_2 :
  ∀ x ∈ P.parts.offDiag, (fun (i : Finset α × Finset α) ↦ #i.1 * #i.2) x ≤ HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2
calc_2₁ :
  #P.parts.offDiag • HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2 ≤
    HPow.hPow (β := ℕ) (#P.parts * (#A / #P.parts) + #P.parts) 2
⊢ ∑ x ∈ P.parts.offDiag, #x.1 * #x.2 ≤ HPow.hPow (β := ℕ) (#A + #P.parts) 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

Premises used: HMul.hMul, HDiv.hDiv, Finpartition.parts, Finset.offDiag, Prod.fst, Finset.sum_le_card_nsmul, HPow.hPow, HAdd.hAdd, Finset.card, OfNat.ofNat, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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_2 : ∀ (a b : Finset α), a ∈ P.parts → b ∈ P.parts → a ≠ b → #a * #b ≤ (#A / #P.parts + 1) * (#A / #P.parts + 1)
⊢ ∀ x ∈ P.parts.offDiag, (fun (i : Finset α × Finset α) ↦ #i.1 * #i.2) x ≤ HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2

Tactic:
simp only [Prod.forall, and_imp, mem_offDiag, sq]

Premises used: and_imp, sq, Prod.forall, Finset.mem_offDiag
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 α
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ #U * #V ≤ (#A / #P.parts + 1) * (#A / #P.parts + 1)

Tactic:
exact_mod_cast Nat.mul_le_mul (hP.card_part_le_average_add_one hU)
      (hP.card_part_le_average_add_one hV)

Premises used: Finpartition.IsEquipartition.card_part_le_average_add_one, Nat.mul_le_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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_2 :
  HPow.hPow (β := ℕ) (#P.parts * (#A / #P.parts) + #P.parts) 2 - #P.parts * HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2 ≤
    HPow.hPow (β := ℕ) (#P.parts * (#A / #P.parts) + #P.parts) 2
⊢ #P.parts.offDiag • HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2 ≤
    HPow.hPow (β := ℕ) (#P.parts * (#A / #P.parts) + #P.parts) 2

Tactic:
rw [smul_eq_mul, offDiag_card, Nat.mul_sub_right_distrib, ← sq, ← mul_pow, mul_add_one (α := ℕ)]

Premises used: Finset.offDiag_card, sq, Nat.mul_sub_right_distrib, smul_eq_mul, mul_add_one, mul_pow
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 - #P.parts * HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2 ≤
    HPow.hPow (β := ℕ) (#P.parts * (#A / #P.parts) + #P.parts) 2

Tactic:
Nat.sub_le _ _

Premises used: Nat.sub_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 - #P.parts * HPow.hPow (β := ℕ) (#A / #P.parts + 1) 2 ≤
    HPow.hPow (β := ℕ) (#P.parts * (#A / #P.parts) + #P.parts) 2

Tactic:
exact Nat.sub_le _ _

Premises used: Nat.sub_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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

Tactic:
hP.card_interedges_sparsePairs_le' hε

Premises used: Finpartition.IsEquipartition.card_interedges_sparsePairs_le'
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ≤ ε
hbc : #P.parts ≤ #A
⊢ ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2 ≤
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ≤ ε
⊢ #P.parts ≤ #A

Tactic:
P.card_parts_le_card

Premises used: Finpartition.card_parts_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 ≤ ε
⊢ #P.parts ≤ #A

Tactic:
exact P.card_parts_le_card

Premises used: Finpartition.card_parts_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2 =
    4 * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2

Tactic:
ring
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
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 (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2 ≤
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2
_₁ :
  ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)) 2 =
    4 * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
⊢ (↑(card (α := α × α)
          ((P.sparsePairs G ε).biUnion fun (x : Finset α × Finset α) ↦
            match (motive := Finset α × Finset α → Finset (α × α)) x with
            | (U, V) => G.interedges U V)) :
      𝕜) ≤
    4 * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2

Tactic:
calc
    _ ≤ _ := hP.card_interedges_sparsePairs_le' hε
    _ ≤ ε * (#A + #A) ^ 2 := by gcongr; exact P.card_parts_le_card
    _ = _ := by ring

Premises used: HAdd.hAdd, Finset.card, Finpartition.IsEquipartition.card_interedges_sparsePairs_le'
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
i j : ℕ
hj : 0 < j
rw : j * (j - 1) < j * j
⊢ j * (j - 1) < HPow.hPow (β := ℕ) j 2

Tactic:
rw [sq]

Premises used: sq
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
i j : ℕ
hj : 0 < j
⊢ j * (j - 1) < j * j

Tactic:
Nat.mul_lt_mul_of_pos_left (Nat.sub_lt hj zero_lt_one) hj

Premises used: Nat.mul_lt_mul_of_pos_left, Nat.sub_lt, zero_lt_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
i j : ℕ
hj : 0 < j
⊢ j * (j - 1) < j * j

Tactic:
exact Nat.mul_lt_mul_of_pos_left (Nat.sub_lt hj zero_lt_one) hj

Premises used: Nat.mul_lt_mul_of_pos_left, Nat.sub_lt, zero_lt_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
i j : ℕ
hj : 0 < j
⊢ j * (j - 1) < HPow.hPow (β := ℕ) j 2

Tactic:
have : j * (j - 1) < j ^ 2 := by
    rw [sq]; exact Nat.mul_lt_mul_of_pos_left (Nat.sub_lt hj zero_lt_one) hj
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < HPow.hPow (β := ℕ) j 2
apply : HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (i / j).succ 2 ≤ HPow.hPow (β := ℕ) (i + j) 2
⊢ j * (j - 1) * HPow.hPow (β := ℕ) (i / j + 1) 2 < HPow.hPow (β := ℕ) (i + j) 2

Tactic:
apply (Nat.mul_lt_mul_of_pos_right this <| pow_pos Nat.succ_pos' _).trans_le

Premises used: Nat.succ_pos', pow_pos, Nat.mul_lt_mul_of_pos_right, LT.lt.trans_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < HPow.hPow (β := ℕ) j 2
rw : HPow.hPow (β := ℕ) (j * (i / j) + j) 2 ≤ HPow.hPow (β := ℕ) (i + j) 2
⊢ HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (i / j).succ 2 ≤ HPow.hPow (β := ℕ) (i + j) 2

Tactic:
rw [← mul_pow, Nat.mul_succ]

Premises used: Nat.mul_succ, mul_pow
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < HPow.hPow (β := ℕ) j 2
hab : j * (i / j) ≤ i
⊢ HPow.hPow (β := ℕ) (j * (i / j) + j) 2 ≤ HPow.hPow (β := ℕ) (i + j) 2

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < HPow.hPow (β := ℕ) j 2
⊢ j * (i / j) ≤ i

Tactic:
apply Nat.mul_div_le

Premises used: Nat.mul_div_le