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 α
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) : ℝ) ≤
    (↑(#X') : ℝ) * (HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ))

Tactic:
exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)

Premises used: Eq.trans_le, mul_le_mul_of_nonneg_right
-- 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 ≤ ε
suffices : (1 - 2 * ε) * (↑(#s) : ℝ) ≤ (↑(#X') : ℝ)
⊢ (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤
    (↑(#X') : ℝ) * (HPow.hPow (β := ℕ) ε 3 * (↑(#t) : ℝ) * (↑(#u) : ℝ))

Tactic:
suffices hX' : (1 - 2 * ε) * #s ≤ #X' by
      exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)
-- 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 ≤ ε
⊢ G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s

Tactic:
have i : badVertices G ε s t ∪ badVertices G ε s u ⊆ s :=
      union_subset (filter_subset _ _) (filter_subset _ _)
-- 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 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
rw : (↑(#(G.badVertices ε s t ∪ G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε + (↑(#s) : ℝ) * ε
⊢ (1 - 2 * ε) * (↑(#s) : ℝ) ≤ (↑(#X') : ℝ)

Tactic:
rw [sub_mul, one_mul, card_sdiff_of_subset i, Nat.cast_sub (card_le_card i),
      sub_le_sub_iff_left, mul_assoc, mul_comm ε, two_mul]

Premises used: Nat.cast_sub, Finset.card_le_card, Finset.card_sdiff_of_subset, mul_assoc, two_mul, sub_le_sub_iff_left, sub_mul, mul_comm, one_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_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 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ (↑(#(G.badVertices ε s t ∪ G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε + (↑(#s) : ℝ) * ε

Tactic:
(Nat.cast_le.2 <| card_union_le _ _).trans ?_

Premises used: Iff.mpr, Finset.card_union_le, Nat.cast_le, 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_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 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
refine : (↑(#(G.badVertices ε s t) + #(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε + (↑(#s) : ℝ) * ε
⊢ (↑(#(G.badVertices ε s t ∪ G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε + (↑(#s) : ℝ) * ε

Tactic:
refine (Nat.cast_le.2 <| card_union_le _ _).trans ?_

Premises used: Iff.mpr, Finset.card_union_le, Nat.cast_le, 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_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 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
rw :
  HAdd.hAdd (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε + (↑(#s) : ℝ) * ε
⊢ (↑(#(G.badVertices ε s t) + #(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε + (↑(#s) : ℝ) * ε

Tactic:
rw [Nat.cast_add]

Premises used: Nat.cast_add
-- 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 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ HAdd.hAdd (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε + (↑(#s) : ℝ) * ε

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t_1 u : Finset α
dst : 2 * ε ≤ (↑(G.edgeDensity s t_1) : ℝ)
hst : G.IsUniform ε s t_1
dsu : 2 * ε ≤ (↑(G.edgeDensity s u) : ℝ)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ (↑(G.edgeDensity t_1 u) : ℝ)
utu : G.IsUniform ε t_1 u
h₁ : (↑(#(G.badVertices ε s t_1)) : ℝ) ≤ (↑(#s) : ℝ) * ε
h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε
X' : Finset α := s \ (G.badVertices ε s t_1 ∪ G.badVertices ε s u)
this :
  (X'.biUnion fun (x : α) ↦
      image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t_1 | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t_1 ×ˢ u |
      match (motive := α × α × α → Prop) x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
a : α
h : a ∈ (↑X' : Set α)
b : α
h_1 : b ∈ (↑X' : Set α)
t : a ≠ b
rw :
  ∀ ⦃a_1 : α × α × α⦄,
    Membership.mem (γ := Finset (α × α × α))
        (image (fun (x : α × α) ↦ (a, x)) (G.interedges ({y ∈ t_1 | G.Adj a y}) ({y ∈ u | G.Adj a y}))) a_1 →
      a_1 ∉ image (fun (x : α × α) ↦ (b, x)) (G.interedges ({y ∈ t_1 | G.Adj b y}) ({y ∈ u | G.Adj b y}))
⊢ Function.onFun (β := Finset (α × α × α)) Disjoint
    (fun (x : α) ↦ image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t_1 | G.Adj x y}) ({y ∈ u | G.Adj x y}))) a
    b

Tactic:
rw [Function.onFun, Finset.disjoint_left]

Premises used: Function.onFun, Finset.disjoint_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t_1 u : Finset α
dst : 2 * ε ≤ (↑(G.edgeDensity s t_1) : ℝ)
hst : G.IsUniform ε s t_1
dsu : 2 * ε ≤ (↑(G.edgeDensity s u) : ℝ)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ (↑(G.edgeDensity t_1 u) : ℝ)
utu : G.IsUniform ε t_1 u
h₁ : (↑(#(G.badVertices ε s t_1)) : ℝ) ≤ (↑(#s) : ℝ) * ε
h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε
X' : Finset α := s \ (G.badVertices ε s t_1 ∪ G.badVertices ε s u)
this :
  (X'.biUnion fun (x : α) ↦
      image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t_1 | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t_1 ×ˢ u |
      match (motive := α × α × α → Prop) x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
a : α
h : a ∈ (↑X' : Set α)
b : α
h_1 : b ∈ (↑X' : Set α)
t : a ≠ b
simp :
  ∀ (a_1 a_2 b_1 a_3 b_2 : α),
    (a_3, b_2) ∈ G.interedges ({y ∈ t_1 | G.Adj a y}) ({y ∈ u | G.Adj a y}) →
      a = a_1 →
        a_3 = a_2 →
          b_2 = b_1 →
            ∀ (a b_3 : α),
              (a, b_3) ∈ G.interedges ({y ∈ t_1 | G.Adj b y}) ({y ∈ u | G.Adj b y}) → b = a_1 → a = a_2 → ¬b_3 = b_1
⊢ ∀ ⦃a_1 : α × α × α⦄,
    Membership.mem (γ := Finset (α × α × α))
        (image (fun (x : α × α) ↦ (a, x)) (G.interedges ({y ∈ t_1 | G.Adj a y}) ({y ∈ u | G.Adj a y}))) a_1 →
      a_1 ∉ image (fun (x : α × α) ↦ (b, x)) (G.interedges ({y ∈ t_1 | G.Adj b y}) ({y ∈ u | G.Adj b y}))

Tactic:
simp only [Prod.forall, mem_image, not_exists, Prod.mk_inj,
    exists_imp, and_imp, not_and]

Premises used: Finset.mem_image, and_imp, Prod.mk_inj, not_exists, Prod.forall, exists_imp, not_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t_1 u : Finset α
dst : 2 * ε ≤ (↑(G.edgeDensity s t_1) : ℝ)
hst : G.IsUniform ε s t_1
dsu : 2 * ε ≤ (↑(G.edgeDensity s u) : ℝ)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ (↑(G.edgeDensity t_1 u) : ℝ)
utu : G.IsUniform ε t_1 u
h₁ : (↑(#(G.badVertices ε s t_1)) : ℝ) ≤ (↑(#s) : ℝ) * ε
h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε
X' : Finset α := s \ (G.badVertices ε s t_1 ∪ G.badVertices ε s u)
this :
  (X'.biUnion fun (x : α) ↦
      image (fun (x_1 : α × α) ↦ (x, x_1)) (G.interedges ({y ∈ t_1 | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t_1 ×ˢ u |
      match (motive := α × α × α → Prop) x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
a : α
h : a ∈ (↑X' : Set α)
b : α
h_1 : b ∈ (↑X' : Set α)
t : a ≠ b
⊢ ∀ (a_1 a_2 b_1 a_3 b_2 : α),
    (a_3, b_2) ∈ G.interedges ({y ∈ t_1 | G.Adj a y}) ({y ∈ u | G.Adj a y}) →
      a = a_1 →
        a_3 = a_2 →
          b_2 = b_1 →
            ∀ (a b_3 : α),
              (a, b_3) ∈ G.interedges ({y ∈ t_1 | G.Adj b y}) ({y ∈ u | G.Adj b y}) → b = a_1 → a = a_2 → ¬b_3 = b_1

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
s t u : Finset α
inst : DecidableEq α
hst : Disjoint s t
hsu : Disjoint s u
htu : Disjoint t u
x₁ x₂ y₁ y₂ z₁ z₂ : α
h : Eq (α := Finset α) {x₁, y₁, z₁} {x₂, y₂, z₂}
hx₁ : x₁ ∈ s
hx₂ : x₂ ∈ s
hy₁ : y₁ ∈ t
hy₂ : y₂ ∈ t
hz₁ : z₁ ∈ u
hz₂ : z₂ ∈ u
⊢ ((x₁ = x₂ ∨ x₁ = y₂ ∨ x₁ = z₂) ∧ (y₁ = x₂ ∨ y₁ = y₂ ∨ y₁ = z₂) ∧ (z₁ = x₂ ∨ z₁ = y₂ ∨ z₁ = z₂)) ∧
    (x₂ = x₁ ∨ x₂ = y₁ ∨ x₂ = z₁) ∧ (y₂ = x₁ ∨ y₂ = y₁ ∨ y₂ = z₁) ∧ (z₂ = x₁ ∨ z₂ = y₁ ∨ z₂ = z₁)

Tactic:
simp only [Finset.Subset.antisymm_iff, subset_iff, mem_insert, mem_singleton, forall_eq_or_imp,
    forall_eq] at h

Premises used: Finset.mem_singleton, Finset.Subset.antisymm_iff, forall_eq, Finset.mem_insert, forall_eq_or_imp, Finset.subset_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
s t u : Finset α
inst : DecidableEq α
hst : Disjoint s t
hsu : Disjoint s u
htu : Disjoint t u
x₁ x₂ y₁ y₂ z₁ z₂ : α
hx₁ : x₁ ∈ s
hx₂ : x₂ ∈ s
hy₁ : y₁ ∈ t
hy₂ : y₂ ∈ t
hz₁ : z₁ ∈ u
hz₂ : z₂ ∈ u
h :
  ((x₁ = x₂ ∨ x₁ = y₂ ∨ x₁ = z₂) ∧ (y₁ = x₂ ∨ y₁ = y₂ ∨ y₁ = z₂) ∧ (z₁ = x₂ ∨ z₁ = y₂ ∨ z₁ = z₂)) ∧
    (x₂ = x₁ ∨ x₂ = y₁ ∨ x₂ = z₁) ∧ (y₂ = x₁ ∨ y₂ = y₁ ∨ y₂ = z₁) ∧ (z₂ = x₁ ∨ z₂ = y₁ ∨ z₂ = z₁)
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)

Tactic:
grind [Finset.disjoint_left]

Premises used: Finset.disjoint_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : DecidableEq α
inst_2 : 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
apply :
  LE.le (α := ℝ)
    (↑(#({x ∈ s ×ˢ t ×ˢ u |
            match (motive := α × α × α → Prop) x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})) :
      ℝ)
    (↑(#(G.cliqueFinset 3)) : ℝ)
⊢ (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤ (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
apply (G.triangle_counting' dst ust dsu usu dtu utu).trans _

Premises used: SimpleGraph.triangle_counting', LE.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 α
inst_2 : 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
rw :
  #({x ∈ s ×ˢ t ×ˢ u |
        match (motive := α × α × α → Prop) x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) ≤
    #(G.cliqueFinset 3)
⊢ LE.le (α := ℝ)
    (↑(#({x ∈ s ×ˢ t ×ˢ u |
            match (motive := α × α × α → Prop) x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c})) :
      ℝ)
    (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
rw [Nat.cast_le]

Premises used: Nat.cast_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : DecidableEq α
inst_2 : 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 ∈ s ×ˢ t ×ˢ u |
        match (motive := α × α × α → Prop) x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) ≤
    #(G.cliqueFinset 3)

Tactic:
card_le_card_of_injOn (fun (x, y, z) ↦ {x, y, z}) ?_ ?_

Premises used: Finset, Finset.card_le_card_of_injOn, Insert.insert, _private.0.SimpleGraph.triangle_split_helper.match_1, Singleton.singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : DecidableEq α
inst_2 : 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
refine_1 :
  Set.MapsTo
    (fun (x : α × α × α) ↦
      match (motive := α × α × α → Finset α) x with
      | (x, y, z) => {x, y, z})
    (↑({x ∈ s ×ˢ t ×ˢ u |
          match (motive := α × α × α → Prop) x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) :
      Set (α × α × α))
    (↑(G.cliqueFinset 3) : Set (Finset α))
refine_2 :
  Set.InjOn (β := Finset α)
    (fun (x : α × α × α) ↦
      match (motive := α × α × α → Finset α) x with
      | (x, y, z) => {x, y, z})
    (↑({x ∈ s ×ˢ t ×ˢ u |
          match (motive := α × α × α → Prop) x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) :
      Set (α × α × α))
⊢ #({x ∈ s ×ˢ t ×ˢ u |
        match (motive := α × α × α → Prop) x with
        | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) ≤
    #(G.cliqueFinset 3)

Tactic:
refine card_le_card_of_injOn (fun (x, y, z) ↦ {x, y, z}) ?_ ?_

Premises used: Finset.card_le_card_of_injOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst_1 : DecidableEq α
inst_2 : 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) ∈
      (↑({x ∈ s ×ˢ t ×ˢ u |
            match (motive := α × α × α → Prop) x with
            | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) :
        Set (α × α × α)) →
    (fun (x : α × α × α) ↦
          (match (motive := α × α × α → Finset α) x with
            | (x, y, z) => {x, y, z} :
            Finset α))
        (x, y, z) ∈
      (↑(G.cliqueFinset 3) : Set (Finset α))

Tactic:
simp +contextual [is3Clique_triple_iff]

Premises used: SimpleGraph.is3Clique_triple_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t_1 u : Finset α
inst_1 : DecidableEq α
inst_2 : Fintype α
dst : 2 * ε ≤ (↑(G.edgeDensity s t_1) : ℝ)
ust : G.IsUniform ε s t_1
hst : Disjoint s t_1
dsu : 2 * ε ≤ (↑(G.edgeDensity s u) : ℝ)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ (↑(G.edgeDensity t_1 u) : ℝ)
utu : G.IsUniform ε t_1 u
htu : Disjoint t_1 u
x₁ y₁ z₁ : α
h₁ :
  (x₁, y₁, z₁) ∈
    (↑({x ∈ s ×ˢ t_1 ×ˢ u |
          match (motive := α × α × α → Prop) x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) :
      Set (α × α × α))
x₂ y₂ z₂ : α
h₂ :
  (x₂, y₂, z₂) ∈
    (↑({x ∈ s ×ˢ t_1 ×ˢ u |
          match (motive := α × α × α → Prop) x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) :
      Set (α × α × α))
t :
  Eq.{u_1 + 1} (α := Finset α)
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₁, y₁, z₁))
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₂, y₂, z₂))
⊢ (x₁ ∈ s ∧ y₁ ∈ t_1 ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁

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

Premises used: Finset.mem_filter, Finset.mem_product, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t_1 u : Finset α
inst_1 : DecidableEq α
inst_2 : Fintype α
dst : 2 * ε ≤ (↑(G.edgeDensity s t_1) : ℝ)
ust : G.IsUniform ε s t_1
hst : Disjoint s t_1
dsu : 2 * ε ≤ (↑(G.edgeDensity s u) : ℝ)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ (↑(G.edgeDensity t_1 u) : ℝ)
utu : G.IsUniform ε t_1 u
htu : Disjoint t_1 u
x₁ y₁ z₁ : α
h₁ :
  (x₁, y₁, z₁) ∈
    (↑({x ∈ s ×ˢ t_1 ×ˢ u |
          match (motive := α × α × α → Prop) x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) :
      Set (α × α × α))
x₂ y₂ z₂ : α
h₂ :
  (x₂, y₂, z₂) ∈
    (↑({x ∈ s ×ˢ t_1 ×ˢ u |
          match (motive := α × α × α → Prop) x with
          | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}) :
      Set (α × α × α))
t :
  Eq.{u_1 + 1} (α := Finset α)
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₁, y₁, z₁))
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₂, y₂, z₂))
h₃ : (x₁ ∈ s ∧ y₁ ∈ t_1 ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
⊢ (x₂ ∈ s ∧ y₂ ∈ t_1 ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂

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

Premises used: Finset.mem_filter, Finset.mem_product, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t_1 u : Finset α
inst_1 : DecidableEq α
inst_2 : Fintype α
dst : 2 * ε ≤ (↑(G.edgeDensity s t_1) : ℝ)
ust : G.IsUniform ε s t_1
hst : Disjoint s t_1
dsu : 2 * ε ≤ (↑(G.edgeDensity s u) : ℝ)
usu : G.IsUniform ε s u
hsu : Disjoint s u
dtu : 2 * ε ≤ (↑(G.edgeDensity t_1 u) : ℝ)
utu : G.IsUniform ε t_1 u
htu : Disjoint t_1 u
x₁ y₁ z₁ x₂ y₂ z₂ : α
t :
  Eq.{u_1 + 1} (α := Finset α)
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₁, y₁, z₁))
    ((fun (x : α × α × α) ↦
        (match (motive := α × α × α → Finset α) x with
          | (x, y, z) => {x, y, z} :
          Finset α))
      (x₂, y₂, z₂))
h₁ : (x₁ ∈ s ∧ y₁ ∈ t_1 ∧ z₁ ∈ u) ∧ G.Adj x₁ y₁ ∧ G.Adj x₁ z₁ ∧ G.Adj y₁ z₁
h₂ : (x₂ ∈ s ∧ y₂ ∈ t_1 ∧ z₂ ∈ u) ∧ G.Adj x₂ y₂ ∧ G.Adj x₂ z₂ ∧ G.Adj y₂ z₂
refine_2 : x₁ ∈ s
refine_2₁ : x₂ ∈ s
refine_2₂ : y₁ ∈ t_1
refine_2₃ : y₂ ∈ t_1
refine_2₄ : z₁ ∈ u
refine_2₅ : z₂ ∈ u
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)

Tactic:
apply triple_eq_triple_of_mem hst hsu htu t

Premises used: _private.0.SimpleGraph.triple_eq_triple_of_mem