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
hP : P.IsEquipartition
inl :
  ∀ (h : P.parts = ∅),
    (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤
      (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
inr :
  ∀ (h : P.parts.Nonempty),
    (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤
      (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
⊢ (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)

Tactic:
obtain h | h := P.parts.eq_empty_or_nonempty

Premises used: Finpartition.parts, Finset.eq_empty_or_nonempty
-- 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
hP : P.IsEquipartition
h : P.parts = ∅
⊢ (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)

Tactic:
simp [h]
-- 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
hP : P.IsEquipartition
h : P.parts.Nonempty
rw rw₁ :
  (↑(#P.parts) : 𝕜) * HMul.hMul (α := 𝕜) (↑(#A / #P.parts) : 𝕜) (↑(#A / #P.parts + 1) : 𝕜) =
    (↑(#P.parts) : 𝕜) * HMul.hMul (α := 𝕜) (↑(#A / #P.parts) : 𝕜) (↑(#A / #P.parts + 1) : 𝕜)
⊢ (↑(#P.parts) : 𝕜) * HMul.hMul (α := 𝕜) (↑(#A / #P.parts) : 𝕜) (↑(#A / #P.parts + 1) : 𝕜) =
    HMul.hMul (α := 𝕜) (↑(#P.parts) : 𝕜) (↑(#A / #P.parts) : 𝕜) * (↑(#A / #P.parts + 1) : 𝕜)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- 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
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ LE.le.{u_2} (α := 𝕜) 0 (↑(#A / #P.parts + 1) : 𝕜)

Tactic:
positivity
-- 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
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ LE.le.{u_2} (α := 𝕜) 0 (↑(#A) : 𝕜)

Tactic:
positivity
-- 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
hP : P.IsEquipartition
h : P.parts.Nonempty
rw :
  (↑(#A) : 𝕜) * (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)) =
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)
rw₁ rw₂ :
  (↑(#A) : 𝕜) * (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)) =
    (↑(#A) : 𝕜) * (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜))
⊢ (↑(#A) : 𝕜) * (HDiv.hDiv (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) + 1) =
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)

Tactic:
rw [← div_add_same (mod_cast h.card_pos.ne'), mul_div_assoc]

Premises used: mul_div_assoc, div_add_same
-- 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
hP : P.IsEquipartition
h : P.parts.Nonempty
inr : (↑(#A / #P.parts + 1) : 𝕜) ≤ HDiv.hDiv (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) + 1
inr₁ : ∀ (U : Finset α) (hU : U ∈ P.parts), #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
⊢ (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤
    (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜)

Tactic:
calc
    _ ≤ (#P.parts : 𝕜) * (↑(#A / #P.parts) * ↑(#A / #P.parts + 1)) :=
        mod_cast card_biUnion_le_card_mul _ _ _ fun U hU ↦ ?_
    _ = #P.parts * ↑(#A / #P.parts) * ↑(#A / #P.parts + 1) := by rw [mul_assoc]
    _ ≤ #A * (#A / #P.parts + 1) :=
        mul_le_mul (mod_cast Nat.mul_div_le _ _) ?_ (by positivity) (by positivity)
    _ = _ := by rw [← div_add_same (mod_cast h.card_pos.ne'), mul_div_assoc]

Premises used: HMul.hMul, HDiv.hDiv, Finpartition.parts, Nat.cast, HAdd.hAdd, mul_le_mul, Finset.card_biUnion_le_card_mul, Finset.card, OfNat.ofNat
-- 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
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ (↑(#A / #P.parts + 1) : 𝕜) ≤ HDiv.hDiv (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) + 1

Tactic:
simpa using Nat.cast_div_le

Premises used: Nat.cast_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
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
this : (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1)
rwa :
  ∀ (this : #U * #U - 1 * #U ≤ #A / #P.parts * (#A / #P.parts + 1)), #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
rwa₁ : ∀ (this : #U * #U - #U ≤ #A / #P.parts * (#A / #P.parts + 1)), #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (this : #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)), #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
⊢ #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)

Tactic:
rwa [Nat.mul_sub_right_distrib, one_mul, ← offDiag_card] at this

Premises used: Finset.offDiag_card, Nat.mul_sub_right_distrib, one_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
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
inr : (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1)
⊢ #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)

Tactic:
suffices (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1) by
    rwa [Nat.mul_sub_right_distrib, one_mul, ← offDiag_card] at this
-- 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
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
⊢ #U ≤ #A / #P.parts + 1

Tactic:
have := hP.card_part_le_average_add_one hU
-- 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
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
this : #U ≤ #A / #P.parts + 1
⊢ (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1)

Tactic:
Nat.mul_le_mul ((Nat.sub_le_sub_right this 1).trans ?_) this

Premises used: Nat.sub_le_sub_right, Nat.mul_le_mul, LE.le.trans, OfNat.ofNat
-- 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
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
this : #U ≤ #A / #P.parts + 1
inr : #A / #P.parts + 1 - 1 ≤ #A / #P.parts
⊢ (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1)

Tactic:
refine Nat.mul_le_mul ((Nat.sub_le_sub_right this 1).trans ?_) this

Premises used: Nat.sub_le_sub_right, Nat.mul_le_mul, LE.le.trans, OfNat.ofNat
-- 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
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
this : #U ≤ #A / #P.parts + 1
⊢ #A / #P.parts + 1 - 1 ≤ #A / #P.parts

Tactic:
simp only [Nat.add_succ_sub_one, add_zero, le_rfl]

Premises used: le_rfl, Nat.add_succ_sub_one, add_zero
-- 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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
⊢ A = ⊥ ∨ A.Nonempty

Tactic:
A.eq_empty_or_nonempty

Premises used: Finset.eq_empty_or_nonempty
-- 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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
inl :
  ∀ {P : Finpartition (α := Finset α) ⊥} (hP : P.IsEquipartition) (hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)),
    (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(card.{u_1} (α := α) ⊥) : 𝕜) 2
inr : ∀ (hA : A.Nonempty), (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
⊢ (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2

Tactic:
obtain rfl | hA : A = ⊥ ∨ _ := A.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq α
ε : 𝕜
hε : 0 < ε
P : Finpartition (α := Finset α) ⊥
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
⊢ (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(card.{u_1} (α := α) ⊥) : 𝕜) 2

Tactic:
simp [Subsingleton.elim P ⊥]

Premises used: Bot.bot, Subsingleton.elim
-- 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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
inr :
  (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜) ≤
    ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2
⊢ (↑(#(P.parts.biUnion offDiag)) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2

Tactic:
apply hP.card_biUnion_offDiag_le'.trans

Premises used: Finpartition.IsEquipartition.card_biUnion_offDiag_le', LE.le.trans
-- 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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
inr :
  (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤
    ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)
⊢ (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) / (↑(#P.parts) : 𝕜) ≤
    ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2

Tactic:
rw [div_le_iff₀ (Nat.cast_pos.2 (P.parts_nonempty hA.ne_empty).card_pos)]

Premises used: div_le_iff₀
-- 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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
rw : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)
⊢ HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)

Tactic:
rw [two_mul]

Premises used: two_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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
bc : #P.parts ≤ #A
⊢ HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#A) : 𝕜)

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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
⊢ #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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
⊢ #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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
⊢ HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)

Tactic:
have : (#A : 𝕜) + #P.parts ≤ 2 * #A := by
    rw [two_mul]; gcongr; exact P.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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
⊢ LE.le.{u_2} (α := 𝕜) 0 (↑(#A) : 𝕜)

Tactic:
positivity
-- 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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
inr :
  (↑(#A) : 𝕜) * HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)
⊢ (↑(#A) : 𝕜) * HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤
    ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)

Tactic:
refine (mul_le_mul_of_nonneg_left this <| by positivity).trans ?_

Premises used: LE.le.trans, mul_le_mul_of_nonneg_left
-- 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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this_1 : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
this : 1 ≤ ε / 4 * (↑(#P.parts) : 𝕜)
rw :
  2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)
⊢ (↑(#A) : 𝕜) * HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)

Tactic:
rw [mul_left_comm, ← sq]

Premises used: sq, mul_left_comm
-- 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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this_1 : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
this : 1 ≤ ε / 4 * (↑(#P.parts) : 𝕜)
⊢ 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * 1 ≤
    2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (ε / 4 * (↑(#P.parts) : 𝕜))

Tactic:
mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜))

Premises used: mul_nonneg, Nat.cast, sq_nonneg, Finset.card, zero_le_two, mul_le_mul_of_nonneg_left
-- 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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this_1 : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
this : 1 ≤ ε / 4 * (↑(#P.parts) : 𝕜)
h : 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 = 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * 1
h₁ :
  ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜) =
    2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (ε / 4 * (↑(#P.parts) : 𝕜))
⊢ 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)

Tactic:
convert! mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜)) using 1

Premises used: mul_nonneg, Nat.cast, sq_nonneg, Finset.card, zero_le_two, mul_le_mul_of_nonneg_left
-- 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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this_1 : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
this : 1 ≤ ε / 4 * (↑(#P.parts) : 𝕜)
⊢ 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 = 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * 1

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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this_1 : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
this : 1 ≤ ε / 4 * (↑(#P.parts) : 𝕜)
⊢ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜) =
    2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (ε / 4 * (↑(#P.parts) : 𝕜))

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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
inr : 1 ≤ ε / 4 * (↑(#P.parts) : 𝕜)
⊢ (↑(#A) : 𝕜) * HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜) ≤ ε / 2 * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A) : 𝕜) 2 * (↑(#P.parts) : 𝕜)

Tactic:
suffices 1 ≤ ε / 4 * #P.parts by
    rw [mul_left_comm, ← sq]
    convert! mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜)) using 1
      <;> 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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
inr : 0 < ε / 4
⊢ 1 ≤ ε / 4 * (↑(#P.parts) : 𝕜)

Tactic:
rwa [← div_le_iff₀', one_div_div]

Premises used: div_le_iff₀', one_div_div
-- 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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ (↑(#P.parts) : 𝕜)
hA : A.Nonempty
this : HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜) ≤ HMul.hMul (α := 𝕜) 2 (↑(#A) : 𝕜)
⊢ 0 < ε / 4

Tactic:
positivity
-- 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
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ∑ i ∈ P.nonUniforms G ε, HMul.hMul (α := 𝕜) (↑(#i.1) : 𝕜) (↑(#i.2) : 𝕜) ≤
    #(P.nonUniforms G ε) • HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2

Tactic:
sum_le_card_nsmul _ _ _ ?_

Premises used: Finset.sum_le_card_nsmul
-- 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
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ #(P.nonUniforms G ε) • HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2 =
    (↑(#(P.nonUniforms G ε)) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2

Tactic:
nsmul_eq_mul _ _

Premises used: nsmul_eq_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
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ 0 ≤ HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2

Tactic:
positivity
-- 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
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ (↑(#P.parts * (#P.parts - 1)) : 𝕜) * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 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
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
calc_1 :
  ∀ x ∈ P.nonUniforms G ε,
    HMul.hMul (α := 𝕜) (↑(#x.1) : 𝕜) (↑(#x.2) : 𝕜) ≤ HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2
calc_2 :
  (↑(#P.parts * (#P.parts - 1)) : 𝕜) * ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#A / #P.parts + 1) : 𝕜) 2 <
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2
⊢ ∑ i ∈ P.nonUniforms G ε, HMul.hMul (α := 𝕜) (↑(#i.1) : 𝕜) (↑(#i.2) : 𝕜) <
    ε * HPow.hPow (β := ℕ) (HAdd.hAdd (α := 𝕜) (↑(#A) : 𝕜) (↑(#P.parts) : 𝕜)) 2

Tactic:
calc
    _ ≤ #(P.nonUniforms G ε) • (↑(#A / #P.parts + 1) : 𝕜) ^ 2 :=
      sum_le_card_nsmul _ _ _ ?_
    _ = _ := nsmul_eq_mul _ _
    _ ≤ _ := mul_le_mul_of_nonneg_right hG <| by positivity
    _ < _ := ?_

Premises used: HDiv.hDiv, Finpartition.parts, Nat.cast, Finset.sum_le_card_nsmul, mul_le_mul_of_nonneg_right, HAdd.hAdd, Finset.card, Finpartition.nonUniforms, nsmul_eq_mul, OfNat.ofNat