-- Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
/-- The **Triangle Counting Lemma**. If `G` is a graph and `s`, `t`, `u` are disjoint sets of
vertices such that each pair is `ε`-uniform and `2 * ε`-dense, then `G` contains at least
`(1 - 2 * ε) * ε ^ 3 * |s| * |t| * |u|` triangles. -/
lemma triangle_counting
    (dst : 2 * ε ≤ G.edgeDensity s t) (ust : G.IsUniform ε s t) (hst : Disjoint s t)
    (dsu : 2 * ε ≤ G.edgeDensity s u) (usu : G.IsUniform ε s u) (hsu : Disjoint s u)
    (dtu : 2 * ε ≤ G.edgeDensity t u) (utu : G.IsUniform ε t u) (htu : Disjoint t u) :
    (1 - 2 * ε) * ε ^ 3 * #s * #t * #u ≤ #(G.cliqueFinset 3)

Proof state:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
ust : G.IsUniform ε s t
hst : Disjoint s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
htu : Disjoint t u
⊢ Set.InjOn
    (fun x =>
      match x with
      | (x, y, z) => {x, y, z})
    ↑(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:
rintro ⟨x₁, y₁, z₁⟩ h₁ ⟨x₂, y₂, z₂⟩ h₂ t

Result:
case refine_2.mk.mk.mk.mk
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t✝ u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)
ust : G.IsUniform ε s t✝
hst : Disjoint s t✝
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)
utu : G.IsUniform ε t✝ u
htu : Disjoint t✝ u
x₁ y₁ z₁ : α
h₁ :
  (x₁, y₁, z₁) ∈
    ↑(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₂ y₂ z₂ : α
h₂ :
  (x₂, y₂, z₂) ∈
    ↑(filter
        (fun x =>
          match x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
        (s ×ˢ t✝ ×ˢ u))
t :
  (fun x =>
        match x with
        | (x, y, z) => {x, y, z})
      (x₁, y₁, z₁) =
    (fun x =>
        match x with
        | (x, y, z) => {x, y, z})
      (x₂, y₂, z₂)
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)

Proof state:
case refine_1
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
ust : G.IsUniform ε s t
hst : Disjoint s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
htu : Disjoint t u
⊢ ∀
    a ∈
      filter
        (fun x =>
          match x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
        (s ×ˢ t ×ˢ u),
    (fun x =>
          match x with
          | (x, y, z) => {x, y, z})
        a ∈
      G.cliqueFinset 3

Tactic:
rintro ⟨x, y, z⟩

Result:
case refine_1.mk.mk
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
ust : G.IsUniform ε s t
hst : Disjoint s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
htu : Disjoint t u
x y z : α
⊢ (x, y, z) ∈
      filter
        (fun x =>
          match x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
        (s ×ˢ t ×ˢ u) →
    (fun x =>
          match x with
          | (x, y, z) => {x, y, z})
        (x, y, z) ∈
      G.cliqueFinset 3

Proof state:
case refine_2.mk.mk.mk.mk
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t✝ u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)
ust : G.IsUniform ε s t✝
hst : Disjoint s t✝
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)
utu : G.IsUniform ε t✝ u
htu : Disjoint t✝ u
x₁ y₁ z₁ : α
h₁ :
  (x₁, y₁, z₁) ∈
    ↑(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₂ y₂ z₂ : α
h₂ :
  (x₂, y₂, z₂) ∈
    ↑(filter
        (fun x =>
          match x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c)
        (s ×ˢ t✝ ×ˢ u))
t :
  (fun x =>
        match x with
        | (x, y, z) => {x, y, z})
      (x₁, y₁, z₁) =
    (fun x =>
        match x with
        | (x, y, z) => {x, y, z})
      (x₂, y₂, z₂)
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)

Tactic:
simp only [mem_coe, mem_filter, mem_product] at h₁ h₂

Result:
case refine_2.mk.mk.mk.mk
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t✝ u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t✝)
ust : G.IsUniform ε s t✝
hst : Disjoint s t✝
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t✝ u)
utu : G.IsUniform ε t✝ u
htu : Disjoint t✝ u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  (fun x =>
        match x with
        | (x, y, z) => {x, y, z})
      (x₁, y₁, z₁) =
    (fun x =>
        match x with
        | (x, y, z) => {x, y, z})
      (x₂, y₂, z₂)
h₁ : (x₁ ∈ s ∧ y₁ ∈ t✝ ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t✝ ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)

Proof state:
case refine_1.mk.mk
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
ust : G.IsUniform ε s t
hst : Disjoint s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
htu : Disjoint t u
x y z : α
⊢ x ∈ s → y ∈ t → z ∈ u → G.Adj x y → G.Adj x z → G.Adj y z → G.Adj x y ∧ G.Adj x z ∧ G.Adj y z

Tactic:
exact fun _ _ _ hxy hxz hyz ↦ ⟨hxy, hxz, hyz⟩

Result:
no goals