-- 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 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 ∪ B)) ≤ ↑(#A) + ↑(#B)

Tactic:
exact mod_cast card_union_le _ _

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
⊢ 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)

Tactic:
rw [two_mul_card_edgeFinset, two_mul_card_edgeFinset]

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
⊢ ↑(#(A ∪ B)) + ↑(#C) ≤ ↑(#A) + ↑(#B) + ↑(#C)

Tactic:
gcongr

Result:
case 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 ∪ B)) ≤ ↑(#A) + ↑(#B)

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
⊢ 0 < ε / 8

Tactic:
positivity

Result:
no goals

Proof state:
case h₁.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
⊢ ↑(#B) ≤ ε / 2 * ↑(Fintype.card α) ^ 2

Tactic:
exact hP.card_biUnion_offDiag_le hε hP'

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:
ring

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
⊢ ↑(#(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:
gcongr

Result:
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

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
⊢ 2 * (↑(#G.edgeFinset) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset)) < 2 * ε * ↑(Fintype.card α ^ 2)

Tactic:
let C := (P.sparsePairs G (ε/4)).biUnion fun (U, V) ↦ G.interedges U V

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) - ↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset)) < 2 * ε * ↑(Fintype.card α ^ 2)