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

Tactic:
have := hst.pos.le

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

Tactic:
exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)

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)
⊢ (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 : X'.biUnion _ ⊆ (s ×ˢ t ×ˢ u).filter fun (a, b, c) ↦ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c :=
  triangle_split_helper _

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

Tactic:
ring

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)
this : 0 ≤ ε
i : SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u ⊆ s
⊢ (1 - 2 * ε) * ↑(#s) ≤ ↑(#X')

Tactic:
rw [sub_mul, one_mul, card_sdiff i, Nat.cast_sub (card_le_card i), sub_le_sub_iff_left,
  mul_assoc, mul_comm ε, two_mul]

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