-- 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)
a : α
a✝¹ : a ∈ X'
b : α
a✝ : b ∈ X'
t : a ≠ b
⊢ Disjoint (image (fun x => (a, x)) (G.interedges (filter (fun y => G.Adj a y) t✝) (filter (fun y => G.Adj a y) u)))
    (image (fun x => (b, x)) (G.interedges (filter (fun y => G.Adj b y) t✝) (filter (fun y => G.Adj b y) u)))

Tactic:
rw [disjoint_left]

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

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)
⊢ ∀ x ∈ X',
    ∀ y ∈ X',
      x ≠ y →
        Disjoint
          (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)))
          (image (fun x => (y, x))
            (G.interedges (filter (fun y_1 => G.Adj y y_1) t) (filter (fun y_1 => G.Adj y y_1) u)))

Tactic:
rintro a _ b _ t

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
⊢ Disjoint (image (fun x => (a, x)) (G.interedges (filter (fun y => G.Adj a y) t✝) (filter (fun y => G.Adj a y) u)))
    (image (fun x => (b, x)) (G.interedges (filter (fun y => G.Adj b y) t✝) (filter (fun y => G.Adj b y) 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) ≤
    ↑(#(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:
refine le_trans ?_ (Nat.cast_le.2 <| card_le_card this)

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'.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))))