-- 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 ≤ ε
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤ ↑(#X') * (ε ^ 3 * ↑(#t) * ↑(#u))

Tactic:
suffices hX' : (1 - 2 * ε) * #s ≤ #X' by
  exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)

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 ≤ ε
⊢ (1 - 2 * ε) * ↑(#s) ≤ ↑(#X')

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:
refine (Nat.cast_le.2 <| card_union_le _ _).trans ?_

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) * ε
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)))

Tactic:
let X' := s \ (badVertices G ε s t ∪ badVertices G ε s u)

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)
⊢ (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)
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:
exact add_le_add h₁ h₂

Result:
no goals

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

Tactic:
aesop

Result:
no goals