-- Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean
private lemma good_vertices_triangle_card [DecidableEq α] (dst : 2 * ε ≤ G.edgeDensity s t)
    (dsu : 2 * ε ≤ G.edgeDensity s u) (dtu : 2 * ε ≤ G.edgeDensity t u) (utu : G.IsUniform ε t u)
    (x : α) (hx : x ∈ s \ (badVertices G ε s t ∪ badVertices G ε s u)) :
    ε ^ 3 * #t * #u ≤ #((({y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y}).filter
        fun (y, z) ↦ G.Adj y z).image (x, ·))

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hx :
  x ∈ s ∧
    ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t)) ∧
      ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) u))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(image (fun x_1 => (x, x_1))
          (filter
            (fun x =>
              match x with
              | (y, z) => G.Adj y z)
            (filter (fun y => G.Adj x y) t ×ˢ filter (fun y => G.Adj x y) u))))

Tactic:
obtain ⟨-, hxY, hsu⟩ := hx

Result:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) u))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(image (fun x_1 => (x, x_1))
          (filter
            (fun x =>
              match x with
              | (y, z) => G.Adj y z)
            (filter (fun y => G.Adj x y) t ×ˢ filter (fun y => G.Adj x y) u))))

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hx : x ∈ s \ (SimpleGraph.badVertices G ε s t ∪ SimpleGraph.badVertices G ε s u)
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(image (fun x_1 => (x, x_1))
          (filter
            (fun x =>
              match x with
              | (y, z) => G.Adj y z)
            (filter (fun y => G.Adj x y) t ×ˢ filter (fun y => G.Adj x y) u))))

Tactic:
simp only [mem_sdiff, badVertices, mem_union, not_or, mem_filter, not_and_or, not_lt] at hx

Result:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hx :
  x ∈ s ∧
    (x ∉ s ∨ (↑(G.edgeDensity s t) - ε) * ↑(#t) ≤ ↑(#(filter (fun y => G.Adj x y) t))) ∧
      (x ∉ s ∨ (↑(G.edgeDensity s u) - ε) * ↑(#u) ≤ ↑(#(filter (fun y => G.Adj x y) u)))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(image (fun x_1 => (x, x_1))
          (filter
            (fun x =>
              match x with
              | (y, z) => G.Adj y z)
            (filter (fun y => G.Adj x y) t ×ˢ filter (fun y => G.Adj x y) u))))

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) u))
hY : ↑(#t) * ε ≤ ↑(#(filter (fun y => G.Adj x y) t))
hZ : ↑(#u) * ε ≤ ↑(#(filter (fun y => G.Adj x y) u))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this :
  ε ≤
    ↑(#(G.interedges (filter (fun y => G.Adj x y) t) (filter (fun y => G.Adj x y) u))) /
      (↑(#(filter (fun y => G.Adj x y) t)) * ↑(#(filter (fun y => G.Adj x y) u)))
hε : 0 ≤ ε
⊢ 0 ≤ ↑(#(filter (fun y => G.Adj x y) t)) * ↑(#(filter (fun y => G.Adj x y) u))

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) u))
hY : ↑(#t) * ε ≤ ↑(#(filter (fun y => G.Adj x y) t))
hZ : ↑(#u) * ε ≤ ↑(#(filter (fun y => G.Adj x y) u))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this :
  ε ≤
    ↑(#(G.interedges (filter (fun y => G.Adj x y) t) (filter (fun y => G.Adj x y) u))) /
      (↑(#(filter (fun y => G.Adj x y) t)) * ↑(#(filter (fun y => G.Adj x y) u)))
hε : 0 ≤ ε
⊢ 0 ≤ ↑(#u) * ε

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hxY : ↑(#t) * (↑(G.edgeDensity s t) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) t))
hsu : ↑(#u) * (↑(G.edgeDensity s u) - ε) ≤ ↑(#(filter (fun y => G.Adj x y) u))
hY : ↑(#t) * ε ≤ ↑(#(filter (fun y => G.Adj x y) t))
hZ : ↑(#u) * ε ≤ ↑(#(filter (fun y => G.Adj x y) u))
this✝ : |↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) - ↑(G.edgeDensity t u)| < ε
this :
  ε ≤
    ↑(#(G.interedges (filter (fun y => G.Adj x y) t) (filter (fun y => G.Adj x y) u))) /
      (↑(#(filter (fun y => G.Adj x y) t)) * ↑(#(filter (fun y => G.Adj x y) u)))
hε : 0 ≤ ε
⊢ 0 ≤ ↑(#(filter (fun y => G.Adj x y) t))

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hx :
  x ∈ s ∧
    (x ∉ s ∨ (↑(G.edgeDensity s t) - ε) * ↑(#t) ≤ ↑(#(filter (fun y => G.Adj x y) t))) ∧
      (x ∉ s ∨ (↑(G.edgeDensity s u) - ε) * ↑(#u) ≤ ↑(#(filter (fun y => G.Adj x y) u)))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(image (fun x_1 => (x, x_1))
          (filter
            (fun x =>
              match x with
              | (y, z) => G.Adj y z)
            (filter (fun y => G.Adj x y) t ×ˢ filter (fun y => G.Adj x y) u))))

Tactic:
rw [← or_and_left, and_or_left] at hx

Result:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hx :
  x ∈ s ∧ x ∉ s ∨
    x ∈ s ∧
      (↑(G.edgeDensity s t) - ε) * ↑(#t) ≤ ↑(#(filter (fun y => G.Adj x y) t)) ∧
        (↑(G.edgeDensity s u) - ε) * ↑(#u) ≤ ↑(#(filter (fun y => G.Adj x y) u))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(image (fun x_1 => (x, x_1))
          (filter
            (fun x =>
              match x with
              | (y, z) => G.Adj y z)
            (filter (fun y => G.Adj x y) t ×ˢ filter (fun y => G.Adj x y) u))))