-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
lemma IsEquipartition.card_biUnion_offDiag_le' (hP : P.IsEquipartition) :
    (#(P.parts.biUnion offDiag) : 𝕜) ≤ #A * (#A + #P.parts) / #P.parts

Proof state:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts = ∅
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)

Tactic:
simp [h]

Result:
no goals

Proof state:
case inr.calc_1
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#A / #P.parts + 1) ≤ ↑(#A) / ↑(#P.parts) + 1

Tactic:
simpa using Nat.cast_div_le

Result:
no goals

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

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)

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

Result:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts = ∅
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)

case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : 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)
⊢ #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)

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

Result:
no goals

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

Tactic:
positivity

Result:
no goals

Proof state:
case inr.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
⊢ #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

Result:
case inr.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
⊢ (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1)

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#P.parts) * (↑(#A / #P.parts) * ↑(#A / #P.parts + 1)) = ↑(#P.parts) * ↑(#A / #P.parts) * ↑(#A / #P.parts + 1)

Tactic:
rw [mul_assoc]

Result:
no goals

Proof state:
case inr.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
⊢ (#U - 1) * #U ≤ #A / #P.parts * (#A / #P.parts + 1)

Tactic:
have := hP.card_part_le_average_add_one hU

Result:
case inr.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : 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)

Proof state:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ↑(#A) * (↑(#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]

Result:
case inr.calc_1
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#A / #P.parts + 1) ≤ ↑(#A) / ↑(#P.parts) + 1

case inr.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
⊢ #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#A) * (↑(#A) / ↑(#P.parts) + 1) = ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts)

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

Result:
no goals

Proof state:
case inr.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : 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, card_univ, le_rfl]

Result:
no goals

Proof state:
case inr.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : 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:
refine Nat.mul_le_mul ((Nat.sub_le_sub_right this 1).trans ?_) this

Result:
case inr.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
inst✝ : 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