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 : Finset α
refine :
  (↑(∑ a ∈ G.badVertices ε s t, #(map { toFun := fun (x : α) ↦ (a, x), inj' := ⋯ : α ↪ α × α } ({y ∈ t | G.Adj a y}))) :
      ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)
refine₁ :
  ∑ x ∈ G.badVertices ε s t, (↑(#({y ∈ t | G.Adj x y})) : ℝ) ≤
    #(G.badVertices ε s t) • (((↑(G.edgeDensity s t) : ℝ) - ε) * (↑(#t) : ℝ))
⊢ (↑(#(Rel.interedges G.Adj (G.badVertices ε s t) t)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)

Tactic:
classical
  refine (Nat.cast_le.2 <| (card_le_card <| subset_of_eq (Rel.interedges_eq_biUnion _)).trans
    card_biUnion_le).trans ?_
  simp_rw [Nat.cast_sum, card_map, ← nsmul_eq_mul, smul_mul_assoc, mul_comm (#t : ℝ)]
  exact sum_le_card_nsmul _ _ _ fun x hx ↦ (mem_filter.1 hx).2.le

Premises used: Iff.mpr, Rel.interedges_eq_biUnion, Finset.card_le_card, Finset.card_map, subset_of_eq, smul_mul_assoc, Nat.cast, Finset.sum_le_card_nsmul, Nat.cast_sum, mul_comm, Finset.card, Finset.card_biUnion_le, nsmul_eq_mul, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
push_cast :
  (↑(#(G.interedges (G.badVertices ε s t) t)) : ℝ) / HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ) ≤
    (↑(G.edgeDensity s t) : ℝ) - ε
⊢ (↑((↑(#(G.interedges (G.badVertices ε s t) t)) : ℚ) /
          HMul.hMul (α := ℚ) (↑(#(G.badVertices ε s t)) : ℚ) (↑(#t) : ℚ)) :
      ℝ) ≤
    (↑(G.edgeDensity s t) : ℝ) - ε

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
⊢ 0 ≤ HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
linarith :
  (↑(G.edgeDensity s t) : ℝ) < ε → 0 - ε + (2 * ε - (↑(G.edgeDensity s t) : ℝ)) + ((↑(G.edgeDensity s t) : ℝ) - ε) = 0
⊢ ε ≤ (↑(G.edgeDensity s t) : ℝ)

Tactic:
linarith
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
refine :
  (↑(#(G.interedges (G.badVertices ε s t) t)) : ℝ) ≤
    ((↑(G.edgeDensity s t) : ℝ) - ε) * HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ)
⊢ (↑(#(G.interedges (G.badVertices ε s t) t)) : ℝ) / HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ) ≤
    (↑(G.edgeDensity s t) : ℝ) - ε

Tactic:
refine div_le_of_le_mul₀ (by positivity) (sub_nonneg_of_le <| by linarith) ?_

Premises used: div_le_of_le_mul₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
rw :
  (↑(#(G.interedges (G.badVertices ε s t) t)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)
⊢ (↑(#(G.interedges (G.badVertices ε s t) t)) : ℝ) ≤
    ((↑(G.edgeDensity s t) : ℝ) - ε) * HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
⊢ (↑(#(G.interedges (G.badVertices ε s t) t)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)

Tactic:
G.card_interedges_badVertices_le

Premises used: _private.0.SimpleGraph.card_interedges_badVertices_le, SimpleGraph.interedges
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
⊢ (↑(#(G.interedges (G.badVertices ε s t) t)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)

Tactic:
exact G.card_interedges_badVertices_le

Premises used: _private.0.SimpleGraph.card_interedges_badVertices_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
hst : G.IsUniform ε s t
⊢ LE.le (α := ℝ) 1 2

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
hst : G.IsUniform ε s t
⊢ ε ≤ 1

Tactic:
have hε : ε ≤ 1 := (le_mul_of_one_le_left hst.pos.le (by simp)).trans
    (dst.trans <| mod_cast edgeDensity_le_one _ _ _)
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
hst : G.IsUniform ε s t
hε : ε ≤ 1
by_contra! : ∀ (h : (↑(#s) : ℝ) * ε < (↑(#(G.badVertices ε s t)) : ℝ)), False
⊢ (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε

Tactic:
by_contra! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
hst : G.IsUniform ε s t
hε : ε ≤ 1
h : (↑(#s) : ℝ) * ε < (↑(#(G.badVertices ε s t)) : ℝ)
⊢ |HSub.hSub (α := ℝ) (↑(G.edgeDensity (G.badVertices ε s t) t) : ℝ) (↑(G.edgeDensity s t) : ℝ)| < ε

Tactic:
have : |(G.edgeDensity (badVertices G ε s t) t - G.edgeDensity s t : ℝ)| < ε :=
    hst (filter_subset _ _) Subset.rfl h.le (mul_le_of_le_one_right (Nat.cast_nonneg _) hε)
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
hst : G.IsUniform ε s t
hε : ε ≤ 1
h : (↑(#s) : ℝ) * ε < (↑(#(G.badVertices ε s t)) : ℝ)
this : |HSub.hSub (α := ℝ) (↑(G.edgeDensity (G.badVertices ε s t) t) : ℝ) (↑(G.edgeDensity s t) : ℝ)| < ε
⊢ HSub.hSub (α := ℝ) (↑(G.edgeDensity (G.badVertices ε s t) t) : ℝ) (↑(G.edgeDensity s t) : ℝ) < ε ∧
    HSub.hSub (α := ℝ) (↑(G.edgeDensity s t) : ℝ) (↑(G.edgeDensity (G.badVertices ε s t) t) : ℝ) < ε

Tactic:
rw [abs_sub_lt_iff] at this

Premises used: abs_sub_lt_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
hst : G.IsUniform ε s t
hε : ε ≤ 1
h : (↑(#s) : ℝ) * ε < (↑(#(G.badVertices ε s t)) : ℝ)
this :
  HSub.hSub (α := ℝ) (↑(G.edgeDensity (G.badVertices ε s t) t) : ℝ) (↑(G.edgeDensity s t) : ℝ) < ε ∧
    HSub.hSub (α := ℝ) (↑(G.edgeDensity s t) : ℝ) (↑(G.edgeDensity (G.badVertices ε s t) t) : ℝ) < ε
linarith :
  HSub.hSub (α := ℝ) (↑(G.edgeDensity s t) : ℝ) (↑(G.edgeDensity (G.badVertices ε s t) t) : ℝ) - ε +
      ((↑(G.edgeDensity (G.badVertices ε s t) t) : ℝ) - ((↑(G.edgeDensity s t) : ℝ) - ε)) =
    0
⊢ False

Tactic:
linarith [G.edgeDensity_badVertices_le hst.pos.le dst]

Premises used: SimpleGraph.IsUniform.pos, LT.lt.le, _private.0.SimpleGraph.edgeDensity_badVertices_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : DecidableEq α
x y z : α
simp :
  ∀ x_1 ∈ s,
    ¬(x_1 ∈ G.badVertices ε s t ∨ x_1 ∈ G.badVertices ε 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
⊢ Membership.mem (γ := Finset (α × α × α))
      ((s \ (G.badVertices ε s t ∪ G.badVertices ε s u)).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, y, z) →
    (x, y, z) ∈
      {x ∈ s ×ˢ t ×ˢ u |
        match (motive := α × α × α → Prop) x with
        | (x, y, z) => G.Adj x y ∧ G.Adj x z ∧ G.Adj y z}

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

Premises used: Finset.mem_image, and_imp, Prod.mk_inj, Finset.mem_sdiff, SimpleGraph.mem_interedges_iff, and_assoc, Finset.mem_filter, Finset.mem_union, exists_imp, Prod.exists, Finset.mem_product, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : 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:
⟨hx, hy, hz, xy, xz, yz⟩

Premises used: And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : 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⟩
-- 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 : α
hx : x ∈ s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
⊢ x ∈ s ∧
    (x ∉ s ∨ ((↑(G.edgeDensity s t) : ℝ) - ε) * (↑(#t) : ℝ) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)) ∧
      (x ∉ s ∨ ((↑(G.edgeDensity s u) : ℝ) - ε) * (↑(#u) : ℝ) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ))

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

Premises used: _private.0.SimpleGraph.badVertices, not_or, Finset.mem_sdiff, not_lt, not_and_or, Finset.mem_filter, Finset.mem_union
-- 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 : α
hx :
  x ∈ s ∧
    (x ∉ s ∨ ((↑(G.edgeDensity s t) : ℝ) - ε) * (↑(#t) : ℝ) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)) ∧
      (x ∉ s ∨ ((↑(G.edgeDensity s u) : ℝ) - ε) * (↑(#u) : ℝ) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ))
⊢ x ∈ s ∧ x ∉ s ∨
    x ∈ s ∧
      ((↑(G.edgeDensity s t) : ℝ) - ε) * (↑(#t) : ℝ) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ) ∧
        ((↑(G.edgeDensity s u) : ℝ) - ε) * (↑(#u) : ℝ) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)

Tactic:
rw [← or_and_left, and_or_left] at hx

Premises used: and_or_left, or_and_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 : α
hx :
  x ∈ s ∧ x ∉ s ∨
    x ∈ s ∧
      ((↑(G.edgeDensity s t) : ℝ) - ε) * (↑(#t) : ℝ) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ) ∧
        ((↑(G.edgeDensity s u) : ℝ) - ε) * (↑(#u) : ℝ) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
⊢ x ∈ s ∧
    (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ) ∧
      (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)

Tactic:
simp only [false_or, and_not_self, mul_comm (_ - _)] at hx

Premises used: HSub.hSub, false_or, and_not_self, mul_comm
-- 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 : α
hx :
  x ∈ s ∧
    (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ) ∧
      (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
⊢ (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)

Tactic:
obtain ⟨-, hxY, hsu⟩ := hx
-- 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 : α
hx :
  x ∈ s ∧
    (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ) ∧
      (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
hxY : (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
⊢ (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)

Tactic:
obtain ⟨-, hxY, hsu⟩ := hx
-- 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})) : ℝ)
⊢ (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)

Tactic:
le_trans ?_ hxY

Premises used: 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})) : ℝ)
refine : (↑(#t) : ℝ) * ε ≤ (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)
⊢ (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)

Tactic:
refine le_trans ?_ hxY

Premises used: 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})) : ℝ)
hbc : ε ≤ (↑(G.edgeDensity s t) : ℝ) - ε
⊢ (↑(#t) : ℝ) * ε ≤ (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)

Tactic:
gcongr
-- 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})) : ℝ)
linarith :
  (↑(G.edgeDensity s t) : ℝ) - ε < ε → 2 * ε - (↑(G.edgeDensity s t) : ℝ) + ((↑(G.edgeDensity s t) : ℝ) - ε - ε) = 0
⊢ ε ≤ (↑(G.edgeDensity s t) : ℝ) - ε

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})) : ℝ)
⊢ (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)

Tactic:
have hY : #t * ε ≤ #{y ∈ t | G.Adj x y} := by
    refine le_trans ?_ hxY; gcongr; 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})) : ℝ)
⊢ (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)

Tactic:
le_trans ?_ hsu

Premises used: 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})) : ℝ)
refine : (↑(#u) : ℝ) * ε ≤ (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε)
⊢ (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)

Tactic:
refine le_trans ?_ hsu

Premises used: 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})) : ℝ)
hbc : ε ≤ (↑(G.edgeDensity s u) : ℝ) - ε
⊢ (↑(#u) : ℝ) * ε ≤ (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε)

Tactic:
gcongr
-- 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})) : ℝ)
linarith :
  (↑(G.edgeDensity s u) : ℝ) - ε < ε → 2 * ε - (↑(G.edgeDensity s u) : ℝ) + ((↑(G.edgeDensity s u) : ℝ) - ε - ε) = 0
⊢ ε ≤ (↑(G.edgeDensity s u) : ℝ) - ε

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})) : ℝ)
⊢ (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)

Tactic:
have hZ : #u * ε ≤ #{y ∈ u | G.Adj x y} := by
    refine le_trans ?_ hsu; gcongr; 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})) : ℝ)
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})) :
      ℝ)
⊢ 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}))) :
      ℝ)

Tactic:
rw [card_image_of_injective _ (Prod.mk_right_injective _)]

Premises used: Finset.card_image_of_injective, Prod.mk_right_injective
-- 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})) : ℝ)
⊢ |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
-- 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 (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

Premises used: abs_sub_lt_iff