α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(card P.parts * card P.parts - card P.parts) ≤ ↑(card P.parts ^ 2)
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(card (offDiag P.parts)) ≤ 1 * ↑(card P.parts ^ 2)
rw [offDiag_card, one_mul]
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ card P.parts * card P.parts - card P.parts ≤ card P.parts ^ 2
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(card P.parts * card P.parts - card P.parts) ≤ ↑(card P.parts ^ 2)
norm_cast
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ card P.parts * card P.parts - card P.parts ≤ card P.parts * card P.parts
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ card P.parts * card P.parts - card P.parts ≤ card P.parts ^ 2
rw [sq]
no goals
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ card P.parts * card P.parts - card P.parts ≤ card P.parts * card P.parts
exact tsub_le_self