-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : 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
have have₁ have₂ :
  ∀ (h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε),
    (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
      (↑(#({x ∈ s ×ˢ t ×ˢ u |
              match (motive := α × α × α → Prop) x with
              | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})) :
        ℝ)
have₃ have₄ :
  ∀ (h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε) (h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε),
    (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
      (↑(#({x ∈ s ×ˢ t ×ˢ u |
              match (motive := α × α × α → Prop) x with
              | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})) :
        ℝ)
have₅ :
  ∀ (h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε) (h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε),
    let X' := s \ (G.badVertices ε s t ∪ G.badVertices ε s u);
    ∀
      (this :
        (X'.biUnion fun (x : α) ↦
            image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
          {x ∈ s ×ˢ t ×ˢ u |
            match (motive := α × α × α → Prop) x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}),
      (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
        (↑(#({x ∈ s ×ˢ t ×ˢ u |
                match (motive := α × α × α → Prop) x with
                | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})) :
          ℝ)
have₆ :
  ∀ (h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε) (h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε),
    let X' := s \ (G.badVertices ε s t ∪ G.badVertices ε s u);
    ∀
      (this :
        (X'.biUnion fun (x : α) ↦
            image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
          {x ∈ s ×ˢ t ×ˢ u |
            match (motive := α × α × α → Prop) x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}),
      (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
        (↑(Finset.card (α := α × α × α)
              (X'.biUnion fun (x : α) ↦
                image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y})))) :
          ℝ)
have₇ :
  ∀ (h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε) (h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε),
    let X' := s \ (G.badVertices ε s t ∪ G.badVertices ε s u);
    ∀
      (this :
        (X'.biUnion fun (x : α) ↦
            image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
          {x ∈ s ×ˢ t ×ˢ u |
            match (motive := α × α × α → Prop) x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}),
      (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
        ∑ x ∈ X',
          (↑(Finset.card (α := α × α × α)
                (image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y})))) :
            ℝ)
have₈ have₉ :
  ∀ (h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε) (h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε),
    let X' := s \ (G.badVertices ε s t ∪ G.badVertices ε s u);
    ∀
      (this :
        (X'.biUnion fun (x : α) ↦
            image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
          {x ∈ s ×ˢ t ×ˢ u |
            match (motive := α × α × α → Prop) x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}),
      (↑X' : Set α).PairwiseDisjoint (α := Finset (α × α × α)) fun (x : α) ↦
        image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))
have₁₀ :
  ∀ (h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε) (h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε),
    let X' := s \ (G.badVertices ε s t ∪ G.badVertices ε s u);
    ∀
      (this :
        (X'.biUnion fun (x : α) ↦
            image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
          {x ∈ s ×ˢ t ×ˢ u |
            match (motive := α × α × α → Prop) x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})
      ⦃a : α⦄,
      a ∈ (↑X' : Set α) →
        ∀ ⦃b : α⦄,
          b ∈ (↑X' : Set α) →
            ∀ (t_1 : a ≠ b),
              Function.onFun (β := Finset (α × α × α)) Disjoint
                (fun (x : α) ↦
                  image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y})))
                a b
have₁₁ :
  ∀ (h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε) (h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε),
    let X' := s \ (G.badVertices ε s t ∪ G.badVertices ε s u);
    ∀
      (this :
        (X'.biUnion fun (x : α) ↦
            image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
          {x ∈ s ×ˢ t ×ˢ u |
            match (motive := α × α × α → Prop) x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})
      ⦃a : α⦄,
      a ∈ (↑X' : Set α) →
        ∀ ⦃b : α⦄,
          b ∈ (↑X' : Set α) →
            ∀ (t_1 : a ≠ b) ⦃a_3 : α × α × α⦄,
              Membership.mem (γ := Finset (α × α × α))
                  (image (fun (x : α × α) ↦ (a, x)) (G.interedges ({y ∈ t | G.Adj a y}) ({y ∈ u | G.Adj a y}))) a_3 →
                a_3 ∉ image (fun (x : α × α) ↦ (b, x)) (G.interedges ({y ∈ t | G.Adj b y}) ({y ∈ u | G.Adj b y}))
have₁₂ :
  ∀ (h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε) (h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε),
    let X' := s \ (G.badVertices ε s t ∪ G.badVertices ε s u);
    ∀
      (this :
        (X'.biUnion fun (x : α) ↦
            image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
          {x ∈ s ×ˢ t ×ˢ u |
            match (motive := α × α × α → Prop) x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})
      ⦃a : α⦄,
      a ∈ (↑X' : Set α) →
        ∀ ⦃b : α⦄,
          b ∈ (↑X' : Set α) →
            ∀ (t_1 : a ≠ b) (a_3 a_4 b_1 a_5 b_2 : α),
              (a_5, b_2) ∈ G.interedges ({y ∈ t | G.Adj a y}) ({y ∈ u | G.Adj a y}) →
                a = a_3 →
                  a_5 = a_4 →
                    b_2 = b_1 →
                      ∀ (a b_3 : α),
                        (a, b_3) ∈ G.interedges ({y ∈ t | G.Adj b y}) ({y ∈ u | G.Adj b y}) →
                          b = a_3 → a = a_4 → ¬b_3 = b_1
⊢ (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
    (↑(#({x ∈ s ×ˢ t ×ˢ u |
            match (motive := α × α × α → Prop) x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})) :
      ℝ)

Tactic:
classical
  have h₁ : #(badVertices G ε s t) ≤ #s * ε := G.card_badVertices_le dst hst
  have h₂ : #(badVertices G ε s u) ≤ #s * ε := G.card_badVertices_le dsu usu
  let X' := s \ (badVertices G ε s t ∪ badVertices G ε s u)
  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 _
  refine le_trans ?_ (Nat.cast_le.2 <| card_le_card this)
  rw [card_biUnion, Nat.cast_sum]
  · apply le_trans _ (card_nsmul_le_sum X' _ _ <| G.good_vertices_triangle_card dst dsu dtu utu)
    rw [nsmul_eq_mul]
    have := hst.pos.le
    suffices hX' : (1 - 2 * ε) * #s ≤ #X' by
      exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)
    have i : badVertices G ε s t ∪ badVertices G ε s u ⊆ s :=
      union_subset (filter_subset _ _) (filter_subset _ _)
    rw [sub_mul, one_mul, card_sdiff_of_subset i, Nat.cast_sub (card_le_card i),
      sub_le_sub_iff_left, mul_assoc, mul_comm ε, two_mul]
    refine (Nat.cast_le.2 <| card_union_le _ _).trans ?_
    rw [Nat.cast_add]
    gcongr
  rintro a _ b _ t
  rw [Function.onFun, Finset.disjoint_left]
  simp only [Prod.forall, mem_image, not_exists, Prod.mk_inj,
    exists_imp, and_imp, not_and]
  aesop

Premises used: Iff.mpr, Function.onFun, Finset.mem_image, and_imp, mul_assoc, Prod.mk_inj, two_mul, not_exists, Finset.card_biUnion, sub_le_sub_iff_left, Finset.card_union_le, sub_mul, Nat.cast_add, Nat.cast_sum, mul_comm, nsmul_eq_mul, Prod.forall, Nat.cast_le, LE.le.trans, Finset.disjoint_left, exists_imp, not_and, one_mul