-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
lemma IsEquipartition.sum_nonUniforms_lt' (hA : A.Nonempty) (hε : 0 < ε) (hP : P.IsEquipartition)
    (hG : P.IsUniform G ε) :
    ∑ i ∈ P.nonUniforms G ε, (#i.1 * #i.2 : 𝕜) < ε * (#A + #P.parts) ^ 2

Proof state:
case calc_2
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ↑(#P.parts * (#P.parts - 1)) * ε * ↑(#A / #P.parts + 1) ^ 2 < ε * (↑(#A) + ↑(#P.parts)) ^ 2

Tactic:
rw [mul_right_comm _ ε, mul_comm ε]

Result:
case calc_2
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ↑(#P.parts * (#P.parts - 1)) * ↑(#A / #P.parts + 1) ^ 2 * ε < (↑(#A) + ↑(#P.parts)) ^ 2 * ε

Proof state:
case calc_1
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ∀ (a b : Finset α), a ∈ P.parts → b ∈ P.parts → a ≠ b → ¬G.IsUniform ε a b → ↑(#a) * ↑(#b) ≤ ↑(#A / #P.parts + 1) ^ 2

Tactic:
rintro U V hU hV - -

Result:
case calc_1
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
U V : Finset α
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ ↑(#U) * ↑(#V) ≤ ↑(#A / #P.parts + 1) ^ 2

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ 0 ≤ ↑(#A / #P.parts + 1) ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ∑ i ∈ P.nonUniforms G ε, ↑(#i.1) * ↑(#i.2) < ε * (↑(#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
  _ < _ := ?_

Result:
case calc_1
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ∀ x ∈ P.nonUniforms G ε, ↑(#x.1) * ↑(#x.2) ≤ ↑(#A / #P.parts + 1) ^ 2

case calc_2
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ↑(#P.parts * (#P.parts - 1)) * ε * ↑(#A / #P.parts + 1) ^ 2 < ε * (↑(#A) + ↑(#P.parts)) ^ 2

Proof state:
case calc_1
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ∀ x ∈ P.nonUniforms G ε, ↑(#x.1) * ↑(#x.2) ≤ ↑(#A / #P.parts + 1) ^ 2

Tactic:
simp only [Prod.forall, Finpartition.mk_mem_nonUniforms, and_imp]

Result:
case calc_1
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ∀ (a b : Finset α), a ∈ P.parts → b ∈ P.parts → a ≠ b → ¬G.IsUniform ε a b → ↑(#a) * ↑(#b) ≤ ↑(#A / #P.parts + 1) ^ 2

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ #P.parts * (#P.parts - 1) * (#A / #P.parts + 1) ^ 2 < (#A + #P.parts) ^ 2

Tactic:
exact aux (P.parts_nonempty hA.ne_empty).card_pos

Result:
no goals

Proof state:
case calc_2
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ↑(#P.parts * (#P.parts - 1)) * ↑(#A / #P.parts + 1) ^ 2 * ε < (↑(#A) + ↑(#P.parts)) ^ 2 * ε

Tactic:
apply mul_lt_mul_of_pos_right _ hε

Result:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ↑(#P.parts * (#P.parts - 1)) * ↑(#A / #P.parts + 1) ^ 2 < (↑(#A) + ↑(#P.parts)) ^ 2

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ↑(#P.parts * (#P.parts - 1)) * ↑(#A / #P.parts + 1) ^ 2 < (↑(#A) + ↑(#P.parts)) ^ 2

Tactic:
norm_cast

Result:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ #P.parts * (#P.parts - 1) * (#A / #P.parts + 1) ^ 2 < (#A + #P.parts) ^ 2

Proof state:
case calc_1
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
U V : Finset α
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ ↑(#U) * ↑(#V) ≤ ↑(#A / #P.parts + 1) ^ 2

Tactic:
rw [sq, ← Nat.cast_mul, ← Nat.cast_mul, Nat.cast_le]

Result:
case calc_1
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
U V : Finset α
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ #U * #V ≤ (#A / #P.parts + 1) * (#A / #P.parts + 1)

Proof state:
case calc_1
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
U V : Finset α
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ #U * #V ≤ (#A / #P.parts + 1) * (#A / #P.parts + 1)

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

Result:
no goals