awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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})) : ℝ)
⊢ HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
    (↑(Finset.card (α := α × α × α)
          (image (fun (x_1 : α × α) ↦ (x, x_1))
            ({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
              match (motive := α × α → Prop) x with
              | (y, z) => G.Adj y z}))) :
      ℝ)
have rw : 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: rw [card_image_of_injective _ (Prod.mk_right_injective _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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})) : ℝ)
⊢ 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})) :
      ℝ)
have this : |HSub.hSub (α := ℝ) (↑(G.edgeDensity (filter (G.Adj x) t) (filter (G.Adj x) u)) : ℝ) (↑(G.edgeDensity t u) : ℝ)| < ε
Tactic: have := utu (filter_subset (G.Adj x) _) (filter_subset (G.Adj x) _) hY hZ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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})) : ℝ)
have 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)) : ℝ) < ε
Tactic: rw [abs_sub_lt_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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)) : ℝ) < ε
⊢ ε ≤ (↑(G.edgeDensity ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y})) : ℝ)
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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) : ℝ)| < ε
⊢ 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})) :
      ℝ)
have this₁ : ε ≤ (↑(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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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})) : ℝ)
⊢ 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})) :
      ℝ)
have 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})) : ℚ)) :
    ℝ)
Tactic: rw [edgeDensity_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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})) : ℚ)) :
      ℝ)
⊢ 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})) :
      ℝ)
have 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})) : ℝ)
Tactic: push_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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})) : ℝ)
⊢ 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})) :
      ℝ)
have hε : 0 ≤ ε
Tactic: have hε := utu.pos.le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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) : ℝ) ≤
    (↑(#({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
            match (motive := α × α → Prop) x with
            | (y, z) => G.Adj y z})) :
      ℝ)
have refine : HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
  ε * HMul.hMul (α := ℝ) (↑(#({y ∈ t | G.Adj x y})) : ℝ) (↑(#({y ∈ u | G.Adj x y})) : ℝ)
Tactic: refine le_trans ?_ (mul_le_of_le_div₀ (Nat.cast_nonneg _) (by positivity) this)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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) : ℝ) ≤
    ε * HMul.hMul (α := ℝ) (↑(#({y ∈ t | G.Adj x y})) : ℝ) (↑(#({y ∈ u | G.Adj x y})) : ℝ)
have refine : HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ) = ε * ((↑(#t) : ℝ) * ε * ((↑(#u) : ℝ) * ε))
Tactic: refine Eq.trans_le ?_
    (mul_le_mul_of_nonneg_left (mul_le_mul hY hZ (by positivity) (by positivity)) hε)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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
⊢ (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) : ℝ) * ε
Tactic: have h₁ : #(badVertices G ε s t) ≤ #s * ε := G.card_badVertices_le dst hst
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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) : ℝ) * ε
⊢ (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 u)) : ℝ) ≤ (↑(#s) : ℝ) * ε
Tactic: have h₂ : #(badVertices G ε s u) ≤ #s * ε := G.card_badVertices_le dsu usu
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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)
⊢ (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 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}
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 _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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})) :
      ℝ)
have 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})))) :
    ℝ)
Tactic: refine le_trans ?_ (Nat.cast_le.2 <| card_le_card this)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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) : ℝ) ≤
    (↑(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 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})))) :
      ℝ)
Tactic: rw [card_biUnion, Nat.cast_sum]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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})))) :
        ℝ)
⊢ (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 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}))
Tactic: rw [card_biUnion, Nat.cast_sum]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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 ∈ 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 apply : (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
  #X' • (HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ))
Tactic: apply le_trans _ (card_nsmul_le_sum X' _ _ <| G.good_vertices_triangle_card dst dsu dtu utu)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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' • (HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ))
have rw : (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
  (↑(#X') : ℝ) * (HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ))
Tactic: rw [nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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') : ℝ) * (HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ))
have this₁ : 0 ≤ ε
Tactic: have := hst.pos.le
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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 ≤ ε
⊢ (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
    (↑(#X') : ℝ) * (HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ))
have suffices : (1 - 2 * ε) * (↑(#s) : ℝ) ≤ (↑(#X') : ℝ)
Tactic: suffices hX' : (1 - 2 * ε) * #s ≤ #X' by
      exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)