-- Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
lemma regularityReduced_edges_card_aux [Nonempty α] (hε : 0 < ε) (hP : P.IsEquipartition)
    (hPε : P.IsUniform G (ε/8)) (hP' : 4 / ε ≤ #P.parts) :
    2 * (#G.edgeFinset - #(G.regularityReduced P (ε/8) (ε/4)).edgeFinset : ℝ)
      < 2 * ε * (card α ^ 2 : ℕ)

Proof state:
case h₂
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x =>
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x =>
    match x with
    | (U, V) => G.interedges U V
⊢ ↑(#C) ≤ 4 * (ε / 4) * ↑(Fintype.card α) ^ 2

Tactic:
exact hP.card_interedges_sparsePairs_le (G := G) (ε := ε / 4) (by positivity)

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x =>
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x =>
    match x with
    | (U, V) => G.interedges U V
⊢ 4 * (ε / 8) * ↑(Fintype.card α) ^ 2 + ε / 2 * ↑(Fintype.card α) ^ 2 + 4 * (ε / 4) * ↑(Fintype.card α) ^ 2 =
    2 * ε * ↑(Fintype.card α ^ 2)

Tactic:
norm_cast

Result:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x =>
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x =>
    match x with
    | (U, V) => G.interedges U V
⊢ 4 * (ε / 8) * ↑(Fintype.card α ^ 2) + ε / 2 * ↑(Fintype.card α ^ 2) + 4 * (ε / 4) * ↑(Fintype.card α ^ 2) =
    2 * ε * ↑(Fintype.card α ^ 2)

Proof state:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x =>
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x =>
    match x with
    | (U, V) => G.interedges U V
⊢ 2 * ↑(#G.edgeFinset) - 2 * ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    ↑(#(filter (fun x => G.Adj x.1 x.2) univ)) -
      ↑(#(filter (fun x => (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2) univ))

Tactic:
norm_cast

Result:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x =>
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x =>
    match x with
    | (U, V) => G.interedges U V
⊢ Int.subNatNat (2 * #G.edgeFinset) (2 * #(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    Int.subNatNat (#(filter (fun x => G.Adj x.1 x.2) univ))
      #(filter (fun x => (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2) univ)

Proof state:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x =>
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x =>
    match x with
    | (U, V) => G.interedges U V
⊢ 2 * (↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset)) =
    ↑(#(filter
          (fun x =>
            match x with
            | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y)
          (univ ×ˢ univ)))

Tactic:
rw [univ_product_univ, mul_sub, filter_and_not, cast_card_sdiff]

Result:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x =>
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x =>
    match x with
    | (U, V) => G.interedges U V
⊢ 2 * ↑(#G.edgeFinset) - 2 * ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) =
    ↑(#(filter (fun x => G.Adj x.1 x.2) univ)) -
      ↑(#(filter (fun x => (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2) univ))

α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x =>
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x =>
    match x with
    | (U, V) => G.interedges U V
⊢ filter (fun x => (regularityReduced P G (ε / 8) (ε / 4)).Adj x.1 x.2) univ ⊆ filter (fun x => G.Adj x.1 x.2) univ

Proof state:
case h.a
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x =>
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x =>
    match x with
    | (U, V) => G.interedges U V
⊢ filter
      (fun x =>
        match x with
        | (x, y) => G.Adj x y ∧ ¬(regularityReduced P G (ε / 8) (ε / 4)).Adj x y)
      (univ ×ˢ univ) ⊆
    A ∪ B ∪ C

Tactic:
exact unreduced_edges_subset

Result:
no goals

Proof state:
case bc.bc
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hε : 0 < ε
hP : P.IsEquipartition
hPε : P.IsUniform G (ε / 8)
hP' : 4 / ε ≤ ↑(#P.parts)
A : Finset (α × α) :=
  (P.nonUniforms G (ε / 8)).biUnion fun x =>
    match x with
    | (U, V) => U ×ˢ V
B : Finset (α × α) := P.parts.biUnion offDiag
C : Finset (α × α) :=
  (P.sparsePairs G (ε / 4)).biUnion fun x =>
    match x with
    | (U, V) => G.interedges U V
⊢ ↑(#A) < 4 * (ε / 8) * ↑(Fintype.card α) ^ 2

Tactic:
exact hP.sum_nonUniforms_lt univ_nonempty (by positivity) hPε

Result:
no goals