awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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 * ε) * (↑(#s) : ℝ) ≤ (↑(#X') : ℝ)
have i : 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 _ _)
-- 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 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ (1 - 2 * ε) * (↑(#s) : ℝ) ≤ (↑(#X') : ℝ)
have rw : (↑(#(G.badVertices ε s t ∪ G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε + (↑(#s) : ℝ) * ε
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]
-- 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 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ (↑(#(G.badVertices ε s t ∪ G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε + (↑(#s) : ℝ) * ε
have refine : (↑(#(G.badVertices ε s t) + #(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε + (↑(#s) : ℝ) * ε
Tactic: refine (Nat.cast_le.2 <| card_union_le _ _).trans ?_
-- 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 ≤ ε
i : G.badVertices ε s t ∪ G.badVertices ε s u ⊆ s
⊢ (↑(#(G.badVertices ε s t) + #(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε + (↑(#s) : ℝ) * ε
have rw : HAdd.hAdd (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#s) : ℝ) * ε + (↑(#s) : ℝ) * ε
Tactic: rw [Nat.cast_add]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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
⊢ 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
have 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}))
Tactic: rw [Function.onFun, Finset.disjoint_left]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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 : α × α × α⦄,
    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}))
have 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
Tactic: simp only [Prod.forall, mem_image, not_exists, Prod.mk_inj,
    exists_imp, and_imp, not_and]
-- 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
⊢ (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 have : ∀ (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})) :
      ℝ)
Tactic: classical
  have h₁ : #(badVertices G ε s t) ≤ #s * ε := G.card_badVertices_le dst hst
  have h₂ : #(badVertices G ε s u) ≤ #s * ε := G.card_badVertices_le dsu usu
  let X' := s \ (badVertices G ε s t ∪ badVertices G ε s u)
  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 _
  refine le_trans ?_ (Nat.cast_le.2 <| card_le_card this)
  rw [card_biUnion, Nat.cast_sum]
  · apply le_trans _ (card_nsmul_le_sum X' _ _ <| G.good_vertices_triangle_card dst dsu dtu utu)
    rw [nsmul_eq_mul]
    have := hst.pos.le
    suffices hX' : (1 - 2 * ε) * #s ≤ #X' by
      exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)
    have i : badVertices G ε s t ∪ badVertices G ε s u ⊆ s :=
      union_subset (filter_subset _ _) (filter_subset _ _)
    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]
    refine (Nat.cast_le.2 <| card_union_le _ _).trans ?_
    rw [Nat.cast_add]
    gcongr
  rintro a _ b _ t
  rw [Function.onFun, Finset.disjoint_left]
  simp only [Prod.forall, mem_image, not_exists, Prod.mk_inj,
    exists_imp, and_imp, not_and]
  aesop
-- 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
have have₁ have₂ :
  ∀ (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})) :
        ℝ)
⊢ (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 have₃ : ∀ (h₁ : (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε) (h₂ : (↑(#(G.badVertices ε s u)) : ℝ) ≤ (↑(#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})) :
      ℝ)
Tactic: classical
  have h₁ : #(badVertices G ε s t) ≤ #s * ε := G.card_badVertices_le dst hst
  have h₂ : #(badVertices G ε s u) ≤ #s * ε := G.card_badVertices_le dsu usu
  let X' := s \ (badVertices G ε s t ∪ badVertices G ε s u)
  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 _
  refine le_trans ?_ (Nat.cast_le.2 <| card_le_card this)
  rw [card_biUnion, Nat.cast_sum]
  · apply le_trans _ (card_nsmul_le_sum X' _ _ <| G.good_vertices_triangle_card dst dsu dtu utu)
    rw [nsmul_eq_mul]
    have := hst.pos.le
    suffices hX' : (1 - 2 * ε) * #s ≤ #X' by
      exact Eq.trans_le (by ring) (mul_le_mul_of_nonneg_right hX' <| by positivity)
    have i : badVertices G ε s t ∪ badVertices G ε s u ⊆ s :=
      union_subset (filter_subset _ _) (filter_subset _ _)
    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]
    refine (Nat.cast_le.2 <| card_union_le _ _).trans ?_
    rw [Nat.cast_add]
    gcongr
  rintro a _ b _ t
  rw [Function.onFun, Finset.disjoint_left]
  simp only [Prod.forall, mem_image, not_exists, Prod.mk_inj,
    exists_imp, and_imp, not_and]
  aesop
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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₁, y₁, z₁) = (x₂, y₂, z₂)
have 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₁)
Tactic: simp only [Finset.Subset.antisymm_iff, subset_iff, mem_insert, mem_singleton, forall_eq_or_imp,
    forall_eq] at h
Cleared hypotheses: h
-- 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 α
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
⊢ (1 - 2 * ε) * HPow.hPow (β := ℕ) ε 3 * (↑(#s) : ℝ) * (↑(#t) : ℝ) * (↑(#u) : ℝ) ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
have 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)) : ℝ)
Tactic: apply (G.triangle_counting' dst ust dsu usu dtu utu).trans _
-- 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 α
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
⊢ 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)) : ℝ)
have 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)
Tactic: rw [Nat.cast_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 α
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)
have 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 α))
Tactic: refine card_le_card_of_injOn (fun (x, y, z) ↦ {x, y, z}) ?_ ?_
-- 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 α
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 α))
⊢ #({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)
have 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 (α × α × α))
Tactic: refine card_le_card_of_injOn (fun (x, y, z) ↦ {x, y, z}) ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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₁, y₁, z₁) = (x₂, y₂, z₂)
have h₃ : (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₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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₁, y₁, z₁) = (x₂, y₂, z₂)
have h₄ : (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₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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₂
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)
have refine_2 : x₁ ∈ s
Tactic: apply triple_eq_triple_of_mem hst hsu htu t
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)
have refine_2₁ : x₂ ∈ s
Tactic: apply triple_eq_triple_of_mem hst hsu htu t
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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
⊢ (x₁, y₁, z₁) = (x₂, y₂, z₂)
have refine_2₂ : y₁ ∈ t_1
Tactic: apply triple_eq_triple_of_mem hst hsu htu t