-- Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
/-- A subset of the triangles constructed in a weird way to make them easy to count. -/
private lemma triangle_split_helper [DecidableEq α] :
    (s \ (badVertices G ε s t ∪ badVertices G ε s u)).biUnion
      (fun x ↦ (G.interedges {y ∈ t | G.Adj x y} {y ∈ u | G.Adj x y}).image (x, ·)) ⊆
      (s ×ˢ t ×ˢ u).filter (fun (x, y, z) ↦ G.Adj x y ∧ G.Adj x z ∧ G.Adj y z)

Proof state:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
x y z : α
⊢ ∀ x_1 ∈ s,
    ¬(x_1 ∈ SimpleGraph.badVertices G ε s t ∨ x_1 ∈ SimpleGraph.badVertices G ε s u) →
      ∀ (x_2 x_3 : α),
        x_2 ∈ t →
          G.Adj x_1 x_2 →
            x_3 ∈ u →
              G.Adj x_1 x_3 →
                G.Adj x_2 x_3 → x_1 = x → x_2 = y → x_3 = z → x ∈ s ∧ y ∈ t ∧ z ∈ u ∧ G.Adj x y ∧ G.Adj x z ∧ G.Adj y z

Tactic:
rintro x hx - y z hy xy hz xz yz rfl rfl rfl

Result:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
x : α
hx : x ∈ s
y z : α
hy : y ∈ t
xy : G.Adj x y
hz : z ∈ u
xz : G.Adj x z
yz : G.Adj y z
⊢ x ∈ s ∧ y ∈ t ∧ z ∈ u ∧ G.Adj x y ∧ G.Adj x z ∧ G.Adj y z

Proof state:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
x y z : α
⊢ ((x, y, z) ∈
      (s \ (SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u)).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))) →
    (x, y, z) ∈
      filter
        (fun x =>
          match x with
          | (x, y, z) => G.Adj x y ∧ G.Adj x z ∧ G.Adj y z)
        (s ×ˢ t ×ˢ u)

Tactic:
simp only [mem_filter, mem_product, mem_biUnion, mem_sdiff, exists_prop, mem_union,
  mem_image, Prod.exists, and_assoc, exists_imp, and_imp, Prod.mk.inj_iff, mem_interedges_iff]

Result:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
x y z : α
⊢ ∀ x_1 ∈ s,
    ¬(x_1 ∈ SimpleGraph.badVertices G ε s t ∨ x_1 ∈ SimpleGraph.badVertices G ε s u) →
      ∀ (x_2 x_3 : α),
        x_2 ∈ t →
          G.Adj x_1 x_2 →
            x_3 ∈ u →
              G.Adj x_1 x_3 →
                G.Adj x_2 x_3 → x_1 = x → x_2 = y → x_3 = z → x ∈ s ∧ y ∈ t ∧ z ∈ u ∧ G.Adj x y ∧ G.Adj x z ∧ G.Adj y z

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
⊢ ((s \ (SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u)).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
        | (x, y, z) => G.Adj x y ∧ G.Adj x z ∧ G.Adj y z)
      (s ×ˢ t ×ˢ u)

Tactic:
rintro ⟨x, y, z⟩

Result:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
x y z : α
⊢ ((x, y, z) ∈
      (s \ (SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u)).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))) →
    (x, y, z) ∈
      filter
        (fun x =>
          match x with
          | (x, y, z) => G.Adj x y ∧ G.Adj x z ∧ G.Adj y z)
        (s ×ˢ t ×ˢ u)

Proof state:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
x : α
hx : x ∈ s
y z : α
hy : y ∈ t
xy : G.Adj x y
hz : z ∈ u
xz : G.Adj x z
yz : G.Adj y z
⊢ x ∈ s ∧ y ∈ t ∧ z ∈ u ∧ G.Adj x y ∧ G.Adj x z ∧ G.Adj y z

Tactic:
exact ⟨hx, hy, hz, xy, xz, yz⟩

Result:
no goals