-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
lemma IsEquipartition.card_biUnion_offDiag_le (hε : 0 < ε) (hP : P.IsEquipartition)
    (hP' : 4 / ε ≤ #P.parts) : #(P.parts.biUnion offDiag) ≤ ε / 2 * #A ^ 2

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this✝ : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
this : 1 ≤ ε / 4 * ↑(#P.parts)
⊢ ↑(#A) * (2 * ↑(#A)) ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)

Tactic:
rw [mul_left_comm, ← sq]

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this✝ : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
this : 1 ≤ ε / 4 * ↑(#P.parts)
⊢ 2 * ↑(#A) ^ 2 ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)

Proof state:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ε / 2 * ↑(#A) ^ 2

Tactic:
apply hP.card_biUnion_offDiag_le'.trans

Result:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts) ≤ ε / 2 * ↑(#A) ^ 2

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ε / 2 * ↑(#A) ^ 2

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

Result:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
ε : 𝕜
hε : 0 < ε
P : Finpartition ⊥
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ε / 2 * ↑(#⊥) ^ 2

case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ε / 2 * ↑(#A) ^ 2

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) + ↑(#P.parts) ≤ ↑(#A) + ↑(#A)

Tactic:
exact add_le_add_left (Nat.cast_le.2 P.card_parts_le_card) _

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ 0 ≤ ↑(#A)

Tactic:
positivity

Result:
no goals

Proof state:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ ↑(#A) * (2 * ↑(#A)) ≤ ε / 2 * ↑(#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

Result:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ 1 ≤ ε / 4 * ↑(#P.parts)

Proof state:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ 1 ≤ ε / 4 * ↑(#P.parts)

Tactic:
rwa [← div_le_iff₀', one_div_div]

Result:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ 0 < ε / 4

Proof state:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) * (↑(#A) + ↑(#P.parts)) ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)

Tactic:
have : (#A : 𝕜) + #P.parts ≤ 2 * #A := by
  rw [two_mul]; exact add_le_add_left (Nat.cast_le.2 P.card_parts_le_card) _

Result:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ ↑(#A) * (↑(#A) + ↑(#P.parts)) ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)

Tactic:
rw [two_mul]

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) + ↑(#P.parts) ≤ ↑(#A) + ↑(#A)

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this✝ : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
this : 1 ≤ ε / 4 * ↑(#P.parts)
⊢ 2 * ↑(#A) ^ 2 ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)

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

Result:
no goals

Proof state:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ ↑(#A) * (↑(#A) + ↑(#P.parts)) ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)

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

Result:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ ↑(#A) * (2 * ↑(#A)) ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)

Proof state:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts) ≤ ε / 2 * ↑(#A) ^ 2

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

Result:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) * (↑(#A) + ↑(#P.parts)) ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)

Proof state:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
⊢ 0 < ε / 4

Tactic:
positivity

Result:
no goals

Proof state:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
ε : 𝕜
hε : 0 < ε
P : Finpartition ⊥
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ε / 2 * ↑(#⊥) ^ 2

Tactic:
simp [Subsingleton.elim P ⊥]

Result:
no goals