awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : 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) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hsu : (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hY : (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hZ : (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
this :
  HSub.hSub (α := ℝ) (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) (↑(G.edgeDensity t u) : ℝ) < ε ∧
    HSub.hSub (α := ℝ) (↑(G.edgeDensity t u) : ℝ) (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) < ε
linarith :
  (↑(G.edgeDensity ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y})) : ℝ) < ε →
    2 * ε - (↑(G.edgeDensity t u) : ℝ) +
          (HSub.hSub (α := ℝ) (↑(G.edgeDensity t u) : ℝ)
              (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) -
            ε) +
        ((↑(G.edgeDensity ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y})) : ℝ) - ε) =
      0
⊢ ε ≤ (↑(G.edgeDensity ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y})) : ℝ)

Tactic:
linarith
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : 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) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hsu : (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hY : (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hZ : (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
this :
  |HSub.hSub (α := ℝ) (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) (↑(G.edgeDensity t u) : ℝ)| < ε
⊢ ε ≤ (↑(G.edgeDensity ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y})) : ℝ)

Tactic:
have : ε ≤ G.edgeDensity {y ∈ t | G.Adj x y} {y ∈ u | G.Adj x y} := by
    rw [abs_sub_lt_iff] at this; linarith
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : 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) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hsu : (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hY : (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hZ : (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
this_1 :
  |HSub.hSub (α := ℝ) (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) (↑(G.edgeDensity t u) : ℝ)| < ε
this : ε ≤ (↑(G.edgeDensity ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y})) : ℝ)
⊢ ε ≤
    (↑((↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) : ℚ) /
          HMul.hMul (α := ℚ) (↑(#({y ∈ t | G.Adj x y})) : ℚ) (↑(#({y ∈ u | G.Adj x y})) : ℚ)) :
      ℝ)

Tactic:
rw [edgeDensity_def] at this

Premises used: SimpleGraph.edgeDensity_def
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : 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) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hsu : (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hY : (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hZ : (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
this_1 :
  |HSub.hSub (α := ℝ) (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) (↑(G.edgeDensity t u) : ℝ)| < ε
this :
  ε ≤
    (↑((↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) : ℚ) /
          HMul.hMul (α := ℚ) (↑(#({y ∈ t | G.Adj x y})) : ℚ) (↑(#({y ∈ u | G.Adj x y})) : ℚ)) :
      ℝ)
⊢ ε ≤
    (↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) : ℝ) /
      HMul.hMul (α := ℝ) (↑(#({y ∈ t | G.Adj x y})) : ℝ) (↑(#({y ∈ u | G.Adj x y})) : ℝ)

Tactic:
push_cast at this
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : 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) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hsu : (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hY : (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hZ : (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
this_1 :
  |HSub.hSub (α := ℝ) (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) (↑(G.edgeDensity t u) : ℝ)| < ε
this :
  ε ≤
    (↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) : ℝ) /
      HMul.hMul (α := ℝ) (↑(#({y ∈ t | G.Adj x y})) : ℝ) (↑(#({y ∈ u | G.Adj x y})) : ℝ)
⊢ 0 ≤ ε

Tactic:
have hε := utu.pos.le
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : 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) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hsu : (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hY : (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hZ : (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
this_1 :
  |HSub.hSub (α := ℝ) (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) (↑(G.edgeDensity t u) : ℝ)| < ε
this :
  ε ≤
    (↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) : ℝ) /
      HMul.hMul (α := ℝ) (↑(#({y ∈ t | G.Adj x y})) : ℝ) (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hε : 0 ≤ ε
⊢ 0 ≤ HMul.hMul (α := ℝ) (↑(#({y ∈ t | G.Adj x y})) : ℝ) (↑(#({y ∈ u | G.Adj x y})) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : 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) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hsu : (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hY : (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hZ : (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
this_1 :
  |HSub.hSub (α := ℝ) (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) (↑(G.edgeDensity t u) : ℝ)| < ε
this :
  ε ≤
    (↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) : ℝ) /
      HMul.hMul (α := ℝ) (↑(#({y ∈ t | G.Adj x y})) : ℝ) (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hε : 0 ≤ ε
refine :
  HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
    ε * HMul.hMul (α := ℝ) (↑(#({y ∈ t | G.Adj x y})) : ℝ) (↑(#({y ∈ u | G.Adj x y})) : ℝ)
⊢ HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
    (↑(#({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
            match (motive := α × α → Prop) x with
            | (y, z) => G.Adj y z})) :
      ℝ)

Tactic:
refine le_trans ?_ (mul_le_of_le_div₀ (Nat.cast_nonneg _) (by positivity) this)

Premises used: mul_le_of_le_div₀, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : 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) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hsu : (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hY : (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hZ : (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
this_1 :
  |HSub.hSub (α := ℝ) (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) (↑(G.edgeDensity t u) : ℝ)| < ε
this :
  ε ≤
    (↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) : ℝ) /
      HMul.hMul (α := ℝ) (↑(#({y ∈ t | G.Adj x y})) : ℝ) (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hε : 0 ≤ ε
⊢ 0 ≤ (↑(#u) : ℝ) * ε

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : 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) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hsu : (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hY : (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hZ : (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
this_1 :
  |HSub.hSub (α := ℝ) (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) (↑(G.edgeDensity t u) : ℝ)| < ε
this :
  ε ≤
    (↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) : ℝ) /
      HMul.hMul (α := ℝ) (↑(#({y ∈ t | G.Adj x y})) : ℝ) (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hε : 0 ≤ ε
⊢ LE.le (α := ℝ) 0 (↑(#({y ∈ t | G.Adj x y})) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : 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) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hsu : (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hY : (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hZ : (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
this_1 :
  |HSub.hSub (α := ℝ) (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) (↑(G.edgeDensity t u) : ℝ)| < ε
this :
  ε ≤
    (↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) : ℝ) /
      HMul.hMul (α := ℝ) (↑(#({y ∈ t | G.Adj x y})) : ℝ) (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hε : 0 ≤ ε
refine : HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ) = ε * ((↑(#t) : ℝ) * ε * ((↑(#u) : ℝ) * ε))
⊢ HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
    ε * HMul.hMul (α := ℝ) (↑(#({y ∈ t | G.Adj x y})) : ℝ) (↑(#({y ∈ u | G.Adj x y})) : ℝ)

Tactic:
refine Eq.trans_le ?_
    (mul_le_mul_of_nonneg_left (mul_le_mul hY hZ (by positivity) (by positivity)) hε)

Premises used: Eq.trans_le, mul_le_mul, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : 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) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hsu : (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hY : (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
hZ : (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
this_1 :
  |HSub.hSub (α := ℝ) (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) (↑(G.edgeDensity t u) : ℝ)| < ε
this :
  ε ≤
    (↑(#(G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) : ℝ) /
      HMul.hMul (α := ℝ) (↑(#({y ∈ t | G.Adj x y})) : ℝ) (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hε : 0 ≤ ε
⊢ HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ) = ε * ((↑(#t) : ℝ) * ε * ((↑(#u) : ℝ) * ε))

Tactic:
ring
-- 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
⊢ (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε

Tactic:
have h₁ : #(badVertices G ε s t) ≤ #s * ε := G.card_badVertices_le dst hst
-- 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
h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε
⊢ (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε

Tactic:
have h₂ : #(badVertices G ε s u) ≤ #s * ε := G.card_badVertices_le dsu usu
-- 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
h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε
h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε
X' : Finset α := s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
⊢ (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}

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 _
-- 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
h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε
h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε
X' : Finset α := 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})) :
      ℝ)

Tactic:
le_trans ?_ (Nat.cast_le.2 <| card_le_card this)

Premises used: Iff.mpr, Finset.card_le_card, Nat.cast_le, le_trans
-- 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
h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε
h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε
X' : Finset α := 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}
refine :
  (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})))) :
      ℝ)
⊢ (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:
refine le_trans ?_ (Nat.cast_le.2 <| card_le_card this)

Premises used: Iff.mpr, Finset.card_le_card, Nat.cast_le, le_trans
-- 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
h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε
h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε
X' : Finset α := 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}
rw :
  (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})))) :
        ℝ)
rw₁ :
  (↑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}))
⊢ (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})))) :
      ℝ)

Tactic:
rw [card_biUnion, Nat.cast_sum]

Premises used: Finset.card_biUnion, Nat.cast_sum
-- 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
h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε
h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε
X' : Finset α := 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}
apply :
  (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
    #X' • (HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ))
⊢ (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})))) :
        ℝ)

Tactic:
apply le_trans _ (card_nsmul_le_sum X' _ _ <| G.good_vertices_triangle_card dst dsu dtu utu)

Premises used: Finset.card_nsmul_le_sum, _private.0.SimpleGraph.good_vertices_triangle_card, le_trans
-- 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
h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε
h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε
X' : Finset α := 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}
rw :
  (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
    (↑(#X') : ℝ) * (HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ))
⊢ (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
    #X' • (HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ))

Tactic:
rw [nsmul_eq_mul]

Premises used: nsmul_eq_mul
-- 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
h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε
h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε
X' : Finset α := 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}
⊢ 0 ≤ ε

Tactic:
have := hst.pos.le
-- 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
h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε
h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε
X' : Finset α := s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
this_1 :
  (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}
this : 0 ≤ ε
hX' : (1 - 2 * ε) * (↑(#s) : ℝ) ≤ (↑(#X') : ℝ)
⊢ (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) =
    (1 - 2 * ε) * (↑(#s) : ℝ) * (HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ))

Tactic:
ring
-- 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
h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε
h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε
X' : Finset α := s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
this_1 :
  (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}
this : 0 ≤ ε
hX' : (1 - 2 * ε) * (↑(#s) : ℝ) ≤ (↑(#X') : ℝ)
⊢ 0 ≤ HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ)

Tactic:
positivity