-- Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
/-- The **Triangle Counting Lemma**. If `G` is a graph and `s`, `t`, `u` are sets of vertices such
that each pair is `ε`-uniform and `2 * ε`-dense, then a proportion of at least
`(1 - 2 * ε) * ε ^ 3` of the triples `(a, b, c) ∈ s × t × u` are triangles. -/
lemma triangle_counting'
    (dst : 2 * ε ≤ G.edgeDensity s t) (hst : G.IsUniform ε s t)
    (dsu : 2 * ε ≤ G.edgeDensity s u) (usu : G.IsUniform ε s u)
    (dtu : 2 * ε ≤ G.edgeDensity t u) (utu : G.IsUniform ε t u) :
    (1 - 2 * ε) * ε ^ 3 * #s * #t * #u ≤
      #((s ×ˢ t ×ˢ u).filter fun (a, b, c) ↦ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(SimpleGraph.badVertices G ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(SimpleGraph.badVertices G ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u)
this✝ :
  (X'.biUnion fun x =>
      image (fun x_1 => (x, x_1)) (G.interedges (filter (fun y => G.Adj x y) t) (filter (fun y => G.Adj x y) u))) ⊆
    filter
      (fun x =>
        match x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
      (s ×ˢ t ×ˢ u)
this : 0 ≤ ε
i : SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u ⊆ s
⊢ ↑(#(SimpleGraph.badVertices G ε s t) + #(SimpleGraph.badVertices G ε s u)) ≤ ↑(#s) * ε + ↑(#s) * ε

Tactic:
rw [Nat.cast_add]

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(SimpleGraph.badVertices G ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(SimpleGraph.badVertices G ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u)
this✝ :
  (X'.biUnion fun x =>
      image (fun x_1 => (x, x_1)) (G.interedges (filter (fun y => G.Adj x y) t) (filter (fun y => G.Adj x y) u))) ⊆
    filter
      (fun x =>
        match x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
      (s ×ˢ t ×ˢ u)
this : 0 ≤ ε
i : SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u ⊆ s
⊢ ↑(#(SimpleGraph.badVertices G ε s t)) + ↑(#(SimpleGraph.badVertices G ε s u)) ≤ ↑(#s) * ε + ↑(#s) * ε

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(SimpleGraph.badVertices G ε s t)) ≤ ↑(#s) * ε
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤
    ↑(#(filter
          (fun x =>
            match x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
          (s ×ˢ t ×ˢ u)))

Tactic:
have h₂ : #(badVertices G ε s u) ≤ #s * ε := G.card_badVertices_le dsu usu

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(SimpleGraph.badVertices G ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(SimpleGraph.badVertices G ε s u)) ≤ ↑(#s) * ε
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤
    ↑(#(filter
          (fun x =>
            match x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
          (s ×ˢ t ×ˢ u)))

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(SimpleGraph.badVertices G ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(SimpleGraph.badVertices G ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u)
this :
  (X'.biUnion fun x =>
      image (fun x_1 => (x, x_1)) (G.interedges (filter (fun y => G.Adj x y) t) (filter (fun y => G.Adj x y) u))) ⊆
    filter
      (fun x =>
        match x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
      (s ×ˢ t ×ˢ u)
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤
    ∑ x ∈ X',
      ↑(#(image (fun x_1 => (x, x_1)) (G.interedges (filter (fun y => G.Adj x y) t) (filter (fun y => G.Adj x y) u))))

Tactic:
apply le_trans _ (card_nsmul_le_sum X' _ _ <| G.good_vertices_triangle_card dst dsu dtu utu)

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(SimpleGraph.badVertices G ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(SimpleGraph.badVertices G ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u)
this :
  (X'.biUnion fun x =>
      image (fun x_1 => (x, x_1)) (G.interedges (filter (fun y => G.Adj x y) t) (filter (fun y => G.Adj x y) u))) ⊆
    filter
      (fun x =>
        match x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
      (s ×ˢ t ×ˢ u)
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤ #X' • (ε ^ 3 * ↑(#t) * ↑(#u))

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t✝ u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)
hst : G.IsUniform ε s t✝
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)
utu : G.IsUniform ε t✝ u
h₁ : ↑(#(SimpleGraph.badVertices G ε s t✝)) ≤ ↑(#s) * ε
h₂ : ↑(#(SimpleGraph.badVertices G ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (SimpleGraph.badVertices G ε s t✝ ∪ SimpleGraph.badVertices G ε s u)
this :
  (X'.biUnion fun x =>
      image (fun x_1 => (x, x_1)) (G.interedges (filter (fun y => G.Adj x y) t✝) (filter (fun y => G.Adj x y) u))) ⊆
    filter
      (fun x =>
        match x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
      (s ×ˢ t✝ ×ˢ u)
a : α
a✝¹ : a ∈ X'
b : α
a✝ : b ∈ X'
t : a ≠ b
⊢ ∀ ⦃a_1 : α × α × α⦄,
    a_1 ∈ image (fun x => (a, x)) (G.interedges (filter (fun y => G.Adj a y) t✝) (filter (fun y => G.Adj a y) u)) →
      a_1 ∉ image (fun x => (b, x)) (G.interedges (filter (fun y => G.Adj b y) t✝) (filter (fun y => G.Adj b y) u))

Tactic:
simp only [Prod.forall, mem_image, not_exists, exists_prop, mem_filter, Prod.mk.inj_iff,
  exists_imp, and_imp, not_and, mem_product, or_assoc]

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t✝ u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)
hst : G.IsUniform ε s t✝
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)
utu : G.IsUniform ε t✝ u
h₁ : ↑(#(SimpleGraph.badVertices G ε s t✝)) ≤ ↑(#s) * ε
h₂ : ↑(#(SimpleGraph.badVertices G ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (SimpleGraph.badVertices G ε s t✝ ∪ SimpleGraph.badVertices G ε s u)
this :
  (X'.biUnion fun x =>
      image (fun x_1 => (x, x_1)) (G.interedges (filter (fun y => G.Adj x y) t✝) (filter (fun y => G.Adj x y) u))) ⊆
    filter
      (fun x =>
        match x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
      (s ×ˢ t✝ ×ˢ u)
a : α
a✝¹ : a ∈ X'
b : α
a✝ : b ∈ X'
t : a ≠ b
⊢ ∀ (a_1 a_2 b_1 a_3 b_2 : α),
    (a_3, b_2) ∈ G.interedges (filter (fun y => G.Adj a y) t✝) (filter (fun y => G.Adj a y) u) →
      a = a_1 →
        a_3 = a_2 →
          b_2 = b_1 →
            ∀ (a b_3 : α),
              (a, b_3) ∈ G.interedges (filter (fun y => G.Adj b y) t✝) (filter (fun y => G.Adj b y) u) →
                b = a_1 → a = a_2 → ¬b_3 = b_1