-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
lemma IsEquipartition.card_interedges_sparsePairs_le' (hP : P.IsEquipartition)
    (hε : 0 ≤ ε) :
    #((P.sparsePairs G ε).biUnion fun (U, V) ↦ G.interedges U V) ≤ ε * (#A + #P.parts) ^ 2

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

Tactic:
rintro U V hU hV -

Result:
case calc_2.calc_1
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : 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)

Proof state:
case calc_1.h.mk
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : 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)) ≤ ε * (↑(#(U, V).1) * ↑(#(U, V).2))

Tactic:
simp [mk_mem_sparsePairs, ← card_interedges_div_card] at hUV

Result:
case calc_1.h.mk
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
U V : Finset α
hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V ∧ ↑(#(G.interedges U V)) / (↑(#U) * ↑(#V)) < ε
⊢ ↑(#(G.interedges (U, V).1 (U, V).2)) ≤ ε * (↑(#(U, V).1) * ↑(#(U, V).2))

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
i : Finset α × Finset α
x✝¹ : i ∈ P.parts.offDiag
x✝ : i ∉ P.sparsePairs G ε
⊢ 0 ≤ ε * (↑(#i.1) * ↑(#i.2))

Tactic:
positivity

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
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∑ x ∈ P.parts.offDiag, #x.1 * #x.2 ≤ (#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 := ?_
  _ ≤ _ := Nat.pow_le_pow_of_le_left (add_le_add_right (Nat.mul_div_le _ _) _) _

Result:
case calc_2.calc_1
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∀ x ∈ P.parts.offDiag, (fun i => #i.1 * #i.2) x ≤ (#A / #P.parts + 1) ^ 2

case calc_2.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ #P.parts.offDiag • (#A / #P.parts + 1) ^ 2 ≤ (#P.parts * (#A / #P.parts) + #P.parts) ^ 2

Proof state:
case calc_1.h.mk
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
U V : Finset α
hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V ∧ ↑(#(G.interedges U V)) / (↑(#U) * ↑(#V)) < ε
⊢ ↑(#(G.interedges (U, V).1 (U, V).2)) ≤ ε * (↑(#(U, V).1) * ↑(#(U, V).2))

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

Result:
case calc_1.h.mk
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
U V : Finset α
hUV : U ∈ P.parts ∧ V ∈ P.parts ∧ ¬U = V ∧ ↑(#(G.interedges U V)) / (↑(#U) * ↑(#V)) < ε
⊢ 0 < ↑(#U) * ↑(#V)

Proof state:
case calc_2.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ #P.parts.offDiag • (#A / #P.parts + 1) ^ 2 ≤ (#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 (α := ℕ)]

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

Proof state:
case calc_2.calc_1
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : 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)

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
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ↑(#((P.sparsePairs G ε).biUnion fun x =>
          match x with
          | (U, V) => G.interedges U V)) ≤
    ε * (↑(#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) := ?_
  _ ≤ _ := sum_le_sum_of_subset_of_nonneg (filter_subset _ _) fun i _ _ ↦ by positivity
  _ = _ := (mul_sum _ _ _).symm
  _ ≤ _ := mul_le_mul_of_nonneg_left ?_ hε

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
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∑ UV ∈ P.sparsePairs G ε, ↑(#(G.interedges UV.1 UV.2)) ≤ ∑ UV ∈ P.sparsePairs G ε, ε * (↑(#UV.1) * ↑(#UV.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
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∑ i ∈ P.parts.offDiag, ↑(#i.1) * ↑(#i.2) ≤ (↑(#A) + ↑(#P.parts)) ^ 2

Proof state:
case calc_2.calc_1
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∀ x ∈ P.parts.offDiag, (fun i => #i.1 * #i.2) x ≤ (#A / #P.parts + 1) ^ 2

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

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

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
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∑ i ∈ P.parts.offDiag, ↑(#i.1) * ↑(#i.2) ≤ (↑(#A) + ↑(#P.parts)) ^ 2

Tactic:
norm_cast

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
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∑ x ∈ P.parts.offDiag, #x.1 * #x.2 ≤ (#A + #P.parts) ^ 2