-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
lemma IsEquipartition.sum_nonUniforms_lt (hA : A.Nonempty) (hε : 0 < ε) (hP : P.IsEquipartition)
    (hG : P.IsUniform G ε) :
    #((P.nonUniforms G ε).biUnion fun (U, V) ↦ U ×ˢ V) < 4 * ε * #A ^ 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.nonUniforms G ε).biUnion fun x =>
        match x with
        | (U, V) => U ×ˢ V) ≤
    ∑ x ∈ P.nonUniforms G ε, #x.1 * #x.2

Tactic:
simp_rw [← card_product]

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.nonUniforms G ε).biUnion fun x => x.1 ×ˢ x.2) ≤ ∑ x ∈ P.nonUniforms G ε, #(x.1 ×ˢ x.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 ε
⊢ ε * (↑(#A) + ↑(#P.parts)) ^ 2 ≤ ε * (↑(#A) + ↑(#A)) ^ 2

Tactic:
gcongr

Result:
case h.hab.bc.h
α : 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 ≤ #A

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.nonUniforms G ε).biUnion fun x =>
          match x with
          | (U, V) => U ×ˢ V)) ≤
    ∑ i ∈ P.nonUniforms G ε, ↑(#i.1) * ↑(#i.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.nonUniforms G ε).biUnion fun x =>
        match x with
        | (U, V) => U ×ˢ V) ≤
    ∑ x ∈ P.nonUniforms G ε, #x.1 * #x.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 ε
⊢ ε * (↑(#A) + ↑(#A)) ^ 2 = 4 * ε * ↑(#A) ^ 2

Tactic:
ring

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 ε
⊢ #((P.nonUniforms G ε).biUnion fun x => x.1 ×ˢ x.2) ≤ ∑ x ∈ P.nonUniforms G ε, #(x.1 ×ˢ x.2)

Tactic:
exact card_biUnion_le

Result:
no goals

Proof state:
case h.hab.bc.h
α : 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 ≤ #A

Tactic:
exact 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
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ↑(#((P.nonUniforms G ε).biUnion fun x =>
          match x with
          | (U, V) => U ×ˢ V)) <
    4 * ε * ↑(#A) ^ 2

Tactic:
calc
  _ ≤ ∑ i ∈ P.nonUniforms G ε, (#i.1 * #i.2 : 𝕜) := by
      norm_cast; simp_rw [← card_product]; exact card_biUnion_le
  _ < _ := hP.sum_nonUniforms_lt' hA hε hG
  _ ≤ ε * (#A + #A) ^ 2 := by gcongr; exact P.card_parts_le_card
  _ = _ := by ring

Result:
no goals