awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst_3 : Fintype α
inst_4 : DecidableRel G.Adj
inst_5 : Nonempty α
hε : G.FarFromTriangleFree ε
ε₁ : ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2 ≤ (↑(#G.edgeFinset) : 𝕜)
⊢ ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2 <
    2⁻¹ * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2
have ε₂ : LE.le.{u_3} (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑((Fintype.card α).choose 2) : 𝕜)
Tactic: calc
        ε * Fintype.card α ^ 2
    _ ≤ #G.edgeFinset := by simpa using hε.le_card_edgeFinset (by simp)
    _ ≤ (Fintype.card α).choose 2 := by gcongr; exact card_edgeFinset_le_card_choose_two
    _ < 2⁻¹ * Fintype.card α ^ 2 := by
      simpa [← div_eq_inv_mul] using Nat.choose_lt_pow_div (by positivity) le_rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst_3 : Fintype α
inst_4 : DecidableRel G.Adj
inst_5 : Nonempty α
hε : G.FarFromTriangleFree ε
ε₁ : ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2 ≤ (↑(#G.edgeFinset) : 𝕜)
ε₂ : LE.le.{u_3} (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑((Fintype.card α).choose 2) : 𝕜)
⊢ ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2 <
    2⁻¹ * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2
have ε₃ : (↑((Fintype.card α).choose 2) : 𝕜) < 2⁻¹ * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2
Tactic: calc
        ε * Fintype.card α ^ 2
    _ ≤ #G.edgeFinset := by simpa using hε.le_card_edgeFinset (by simp)
    _ ≤ (Fintype.card α).choose 2 := by gcongr; exact card_edgeFinset_le_card_choose_two
    _ < 2⁻¹ * Fintype.card α ^ 2 := by
      simpa [← div_eq_inv_mul] using Nat.choose_lt_pow_div (by positivity) le_rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst_3 : Fintype α
inst_4 : DecidableRel G.Adj
inst_5 : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
⊢ ε ≤ 0
have this : (fun (H : SimpleGraph α) ↦ H.CliqueFree 3) (G.deleteEdges (↑∅ : Set (Sym2 α))) →
  ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(Finset.card.{u_1} (α := Sym2 α) ∅) : 𝕜)
Tactic: have := h₀ (empty_subset _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst_3 : Fintype α
inst_4 : DecidableRel G.Adj
inst_5 : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
this :
  (fun (H : SimpleGraph α) ↦ H.CliqueFree 3) (G.deleteEdges (↑∅ : Set (Sym2 α))) →
    ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(Finset.card.{u_1} (α := Sym2 α) ∅) : 𝕜)
⊢ ε ≤ 0
have this₁ : (fun (H : SimpleGraph α) ↦ H.CliqueFree 3) G → ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ 0
Tactic: rw [coe_empty, Finset.card_empty, cast_zero, deleteEdges_empty] 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 : Finset α
⊢ (↑(#(Rel.interedges G.Adj (G.badVertices ε s t) t)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)
have refine : (↑(∑ a ∈ G.badVertices ε s t, #(map { toFun := fun (x : α) ↦ (a, x), inj' := sorry : α ↪ α × α } ({y ∈ t | G.Adj a y}))) :
    ℝ) ≤
  HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)
Tactic: refine (Nat.cast_le.2 <| (card_le_card <| subset_of_eq (Rel.interedges_eq_biUnion _)).trans
    card_biUnion_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 : Finset α
⊢ (↑(∑ 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) : ℝ) - ε)
have simp_rw : ∑ x ∈ G.badVertices ε s t, (↑(#({y ∈ t | G.Adj x y})) : ℝ) ≤
  #(G.badVertices ε s t) • (((↑(G.edgeDensity s t) : ℝ) - ε) * (↑(#t) : ℝ))
Tactic: simp_rw [Nat.cast_sum, card_map, ← nsmul_eq_mul, smul_mul_assoc, mul_comm (#t : ℝ)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ (↑(#(Rel.interedges G.Adj (G.badVertices ε s t) t)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)
have refine : (↑(∑ a ∈ G.badVertices ε s t, #(map { toFun := fun (x : α) ↦ (a, x), inj' := sorry : α ↪ α × α } ({y ∈ t | G.Adj a y}))) :
    ℝ) ≤
  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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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) : ℝ) - ε)
⊢ (↑(#(Rel.interedges G.Adj (G.badVertices ε s t) t)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)
have refine₁ : ∑ x ∈ G.badVertices ε s t, (↑(#({y ∈ t | G.Adj x y})) : ℝ) ≤
  #(G.badVertices ε s t) • (((↑(G.edgeDensity s t) : ℝ) - ε) * (↑(#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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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) : ℝ) - ε
have push_cast : (↑(#(G.interedges (G.badVertices ε s t) t)) : ℝ) / HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ) ≤
  (↑(G.edgeDensity s t) : ℝ) - ε
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
hε : 0 ≤ ε
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
⊢ ε ≤ (↑(G.edgeDensity s t) : ℝ)
have linarith : (↑(G.edgeDensity s t) : ℝ) < ε → 0 - ε + (2 * ε - (↑(G.edgeDensity s t) : ℝ)) + ((↑(G.edgeDensity s t) : ℝ) - ε) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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) : ℝ) - ε
have refine : (↑(#(G.interedges (G.badVertices ε s t) t)) : ℝ) ≤
  ((↑(G.edgeDensity s t) : ℝ) - ε) * HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ)
Tactic: refine div_le_of_le_mul₀ (by positivity) (sub_nonneg_of_le <| by linarith) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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)) : ℝ) ≤
    ((↑(G.edgeDensity s t) : ℝ) - ε) * HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ)
have rw : (↑(#(G.interedges (G.badVertices ε s t) t)) : ℝ) ≤
  HMul.hMul (α := ℝ) (↑(#(G.badVertices ε s t)) : ℝ) (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ (↑(G.edgeDensity s t) : ℝ)
hst : G.IsUniform ε s t
⊢ (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε
have hε : ε ≤ 1
Tactic: have hε : ε ≤ 1 := (le_mul_of_one_le_left hst.pos.le (by simp)).trans
    (dst.trans <| mod_cast edgeDensity_le_one _ _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (goal)
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
⊢ (↑(#(G.badVertices ε s t)) : ℝ) ≤ (↑(#s) : ℝ) * ε
have by_contra! : ∀ (h : (↑(#s) : ℝ) * ε < (↑(#(G.badVertices ε s t)) : ℝ)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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)) : ℝ)
⊢ False
have this : |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ε)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Counting (hypothesis)
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) : ℝ)| < ε
⊢ False
have 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) : ℝ) < ε
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 : 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) : ℝ) < ε
⊢ False
have 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
Tactic: linarith [G.edgeDensity_badVertices_le hst.pos.le dst]
-- 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 α
x 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}
have 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
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]
-- 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 : α
hx : x ∈ s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
⊢ 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 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})) : ℝ))
Tactic: simp only [mem_sdiff, badVertices, mem_union, not_or, mem_filter, not_and_or, not_lt] at hx
Cleared hypotheses: hx
-- 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 : α
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})) : ℝ))
⊢ 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 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})) : ℝ)
Tactic: rw [← or_and_left, and_or_left] at hx
Cleared hypotheses: hx
-- 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 : α
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})) : ℝ)
⊢ 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 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})) : ℝ)
Tactic: simp only [false_or, and_not_self, mul_comm (_ - _)] at hx
Cleared hypotheses: hx
-- 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 : α
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})) : ℝ)
⊢ 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 hxY : (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε) ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
Tactic: obtain ⟨-, hxY, hsu⟩ := hx
Cleared hypotheses: hx
-- 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 : α
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})) : ℝ)
⊢ 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 hsu : (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε) ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
Tactic: obtain ⟨-, hxY, hsu⟩ := hx
Cleared hypotheses: hx
-- 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})) : ℝ)
⊢ (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
have refine : (↑(#t) : ℝ) * ε ≤ (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)
Tactic: refine le_trans ?_ hxY
-- 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})) : ℝ)
⊢ (↑(#t) : ℝ) * ε ≤ (↑(#t) : ℝ) * ((↑(G.edgeDensity s t) : ℝ) - ε)
have hbc : ε ≤ (↑(G.edgeDensity s t) : ℝ) - ε
Tactic: gcongr
-- 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})) : ℝ)
⊢ ε ≤ (↑(G.edgeDensity s t) : ℝ) - ε
have linarith : (↑(G.edgeDensity s t) : ℝ) - ε < ε → 2 * ε - (↑(G.edgeDensity s t) : ℝ) + ((↑(G.edgeDensity s t) : ℝ) - ε - ε) = 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})) : ℝ)
⊢ 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 hY : (↑(#t) : ℝ) * ε ≤ (↑(#({y ∈ t | G.Adj x y})) : ℝ)
Tactic: have hY : #t * ε ≤ #{y ∈ t | G.Adj x y} := by
    refine le_trans ?_ hxY; gcongr; linarith
-- 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})) : ℝ)
⊢ (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
have refine : (↑(#u) : ℝ) * ε ≤ (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε)
Tactic: refine le_trans ?_ hsu
-- 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})) : ℝ)
⊢ (↑(#u) : ℝ) * ε ≤ (↑(#u) : ℝ) * ((↑(G.edgeDensity s u) : ℝ) - ε)
have hbc : ε ≤ (↑(G.edgeDensity s u) : ℝ) - ε
Tactic: gcongr
-- 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})) : ℝ)
⊢ ε ≤ (↑(G.edgeDensity s u) : ℝ) - ε
have linarith : (↑(G.edgeDensity s u) : ℝ) - ε < ε → 2 * ε - (↑(G.edgeDensity s u) : ℝ) + ((↑(G.edgeDensity s u) : ℝ) - ε - ε) = 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})) : ℝ)
⊢ 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 hZ : (↑(#u) : ℝ) * ε ≤ (↑(#({y ∈ u | G.Adj x y})) : ℝ)
Tactic: have hZ : #u * ε ≤ #{y ∈ u | G.Adj x y} := by
    refine le_trans ?_ hsu; gcongr; linarith