awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : t ∈ tris) → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂
t : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯ ∨ fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯
i : ((↑t₁ : Set α) ∩ (↑t₂ : Set α)).Subsingleton
inl : ∀ (t : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯), False
inr : ∀ (t : fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯), False
⊢ False

Tactic:
obtain t | t := t
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : t ∈ tris) → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂
i : ((↑t₁ : Set α) ∩ (↑t₂ : Set α)).Subsingleton
t : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯
⊢ False

Tactic:
hfne _ (i ⟨hfx ht₁, t.1.symm ▸ hfx ht₂⟩ ⟨hfy ht₁, t.2.symm ▸ hfy ht₂⟩)

Premises used: Eq.rec, And.right, And.left, And.intro, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : t ∈ tris) → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂
i : ((↑t₁ : Set α) ∩ (↑t₂ : Set α)).Subsingleton
t : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯
⊢ False

Tactic:
exact hfne _ (i ⟨hfx ht₁, t.1.symm ▸ hfx ht₂⟩ ⟨hfy ht₁, t.2.symm ▸ hfy ht₂⟩)

Premises used: Eq.rec, And.right, And.left, And.intro, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : t ∈ tris) → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂
i : ((↑t₁ : Set α) ∩ (↑t₂ : Set α)).Subsingleton
t : fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯
⊢ False

Tactic:
hfne _ (i ⟨hfx ht₁, t.1.symm ▸ hfy ht₂⟩ ⟨hfy ht₁, t.2.symm ▸ hfx ht₂⟩)

Premises used: Eq.rec, And.right, And.left, And.intro, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : t ∈ tris) → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂
i : ((↑t₁ : Set α) ∩ (↑t₂ : Set α)).Subsingleton
t : fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯
⊢ False

Tactic:
exact hfne _ (i ⟨hfx ht₁, t.1.symm ▸ hfy ht₂⟩ ⟨hfy ht₁, t.2.symm ▸ hfx ht₂⟩)

Premises used: Eq.rec, And.right, And.left, And.intro, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
tris_big : ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(#tris) : 𝕜)
rw :
  ∀ ⦃H : SimpleGraph α⦄ [inst_6 : DecidableRel H.Adj],
    H ≤ G →
      H.CliqueFree 3 →
        ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤
          HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
⊢ G.FarFromTriangleFree ε

Tactic:
rw [farFromTriangleFree_iff]

Premises used: SimpleGraph.farFromTriangleFree_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
tris_big : ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(#tris) : 𝕜)
H : SimpleGraph α
_ :
  ∀ [inst_6 : DecidableRel H.Adj],
    H ≤ G →
      H.CliqueFree 3 →
        ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤
          HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)
⊢ ∀ [inst_6 : DecidableRel H.Adj],
    H ≤ G →
      H.CliqueFree 3 →
        ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤
          HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
tris_big : ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(#tris) : 𝕜)
H : SimpleGraph α
inst_6 : DecidableRel H.Adj
hG : H ≤ G
hH : H.CliqueFree 3
rw : ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(#G.edgeFinset - #H.edgeFinset) : 𝕜)
⊢ ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)

Tactic:
rw [← Nat.cast_sub (card_le_card <| edgeFinset_mono hG)]

Premises used: SimpleGraph.edgeFinset_mono, Nat.cast_sub, Finset.card_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
tris_big : ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(#tris) : 𝕜)
H : SimpleGraph α
inst_6 : DecidableRel H.Adj
hG : H ≤ G
hH : H.CliqueFree 3
⊢ ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(#G.edgeFinset - #H.edgeFinset) : 𝕜)

Tactic:
tris_big.trans
    (Nat.cast_le.2 <| farFromTriangleFree_of_disjoint_triangles_aux htris pd hG hH)

Premises used: Iff.mpr, Nat.cast_le, LE.le.trans, _private.0.SimpleGraph.farFromTriangleFree_of_disjoint_triangles_aux
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
tris_big : ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(#tris) : 𝕜)
H : SimpleGraph α
inst_6 : DecidableRel H.Adj
hG : H ≤ G
hH : H.CliqueFree 3
⊢ ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(#G.edgeFinset - #H.edgeFinset) : 𝕜)

Tactic:
exact tris_big.trans
    (Nat.cast_le.2 <| farFromTriangleFree_of_disjoint_triangles_aux htris pd hG hH)

Premises used: Iff.mpr, Nat.cast_le, LE.le.trans, _private.0.SimpleGraph.farFromTriangleFree_of_disjoint_triangles_aux
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 : DecidableEq α
hG : G.EdgeDisjointTriangles
tris_big : ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ (↑(#(G.cliqueFinset 3)) : 𝕜)
⊢ (↑(G.cliqueFinset 3) : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton

Tactic:
simpa using hG
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 ε
⊢ 0 ≤ HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 ε
refine :
  ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2 <
    2⁻¹ * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2
⊢ ε < 2⁻¹

Tactic:
refine lt_of_mul_lt_mul_right (α := 𝕜) (a := Fintype.card α ^ 2) ?_ (by positivity)

Premises used: lt_of_mul_lt_mul_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 ε
⊢ CliqueFree.{u_1} (α := α) ⊥ 3

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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) : 𝕜)

Tactic:
simpa using hε.le_card_edgeFinset (by simp)

Premises used: SimpleGraph.DeleteFar.le_card_edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 ε
a : #G.edgeFinset ≤ (Fintype.card α).choose 2
⊢ LE.le.{u_3} (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑((Fintype.card α).choose 2) : 𝕜)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 ε
⊢ #G.edgeFinset ≤ (Fintype.card α).choose 2

Tactic:
card_edgeFinset_le_card_choose_two

Premises used: SimpleGraph.card_edgeFinset_le_card_choose_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 ε
⊢ #G.edgeFinset ≤ (Fintype.card α).choose 2

Tactic:
exact card_edgeFinset_le_card_choose_two

Premises used: SimpleGraph.card_edgeFinset_le_card_choose_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 ε
⊢ Fintype.card α ≠ 0

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 ε
⊢ (↑((Fintype.card α).choose 2) : 𝕜) < 2⁻¹ * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2

Tactic:
simpa [← div_eq_inv_mul] using Nat.choose_lt_pow_div (by positivity) le_rfl

Premises used: le_rfl, Nat.choose_lt_pow_div, div_eq_inv_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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) : 𝕜)
ε₃ : (↑((Fintype.card α).choose 2) : 𝕜) < 2⁻¹ * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 2
⊢ ε * HPow.hPow (α := 𝕜) (β := ℕ) (↑(Fintype.card α) : 𝕜) 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

Premises used: Nat.choose, Fintype.card, SimpleGraph.edgeFinset, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 α
hG : G.FarFromTriangleFree ε
⊢ ε < 1

Tactic:
hG.lt_half.trans two_inv_lt_one

Premises used: two_inv_lt_one, SimpleGraph.FarFromTriangleFree.lt_half, LT.lt.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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
⊢ (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 _)
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 α) ∅) : 𝕜)
⊢ (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

Premises used: Finset.coe_empty, SimpleGraph.deleteEdges_empty, Finset.card_empty, Nat.cast_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 → ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ 0
⊢ ε ≤ 0

Tactic:
nonpos_of_mul_nonpos_left (this h₁) (cast_pos.2 <| sq_pos_of_pos Fintype.card_pos)

Premises used: Iff.mpr, Nat.cast_pos, sq_pos_of_pos, nonpos_of_mul_nonpos_left, Fintype.card_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 → ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ 0
⊢ ε ≤ 0

Tactic:
exact nonpos_of_mul_nonpos_left (this h₁) (cast_pos.2 <| sq_pos_of_pos Fintype.card_pos)

Premises used: Iff.mpr, Nat.cast_pos, sq_pos_of_pos, nonpos_of_mul_nonpos_left, Fintype.card_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 α
hG : G.CliqueFree 3
hε : 0 < ε
⊢ ¬G.FarFromTriangleFree ε

Tactic:
fun h => (h.nonpos hG).not_gt hε

Premises used: SimpleGraph.FarFromTriangleFree.nonpos, LE.le.not_gt, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 α
hG : G.FarFromTriangleFree ε
hε : 0 < ε
⊢ ¬G.CliqueFree 3

Tactic:
fun h => (hG.nonpos h).not_gt hε

Premises used: SimpleGraph.FarFromTriangleFree.nonpos, LE.le.not_gt, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
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 α
inst_6 : DecidableEq α
hG : G.FarFromTriangleFree ε
hε : 0 < ε
⊢ (G.cliqueFinset 3).Nonempty

Tactic:
nonempty_of_ne_empty <| cliqueFinset_eq_empty_iff.not.2 <| hG.not_cliqueFree hε

Premises used: Iff.mpr, SimpleGraph.cliqueFinset_eq_empty_iff, SimpleGraph.FarFromTriangleFree.not_cliqueFree, Iff.not, Finset.nonempty_of_ne_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
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) : ℝ) - ε)

Tactic:
(Nat.cast_le.2 <| (card_le_card <| subset_of_eq (Rel.interedges_eq_biUnion _)).trans
    card_biUnion_le).trans ?_

Premises used: Iff.mpr, Rel.interedges_eq_biUnion, Finset.card_le_card, subset_of_eq, Finset.card_biUnion_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 : 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) : ℝ) - ε)

Tactic:
refine (Nat.cast_le.2 <| (card_le_card <| subset_of_eq (Rel.interedges_eq_biUnion _)).trans
    card_biUnion_le).trans ?_

Premises used: Iff.mpr, Rel.interedges_eq_biUnion, Finset.card_le_card, subset_of_eq, Finset.card_biUnion_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 : Finset α
simp_rw :
  ∑ x ∈ G.badVertices ε s t, (↑(#({y ∈ t | G.Adj x y})) : ℝ) ≤
    #(G.badVertices ε s t) • (((↑(G.edgeDensity s t) : ℝ) - ε) * (↑(#t) : ℝ))
⊢ (↑(∑ 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) : ℝ) - ε)

Tactic:
simp_rw [Nat.cast_sum, card_map, ← nsmul_eq_mul, smul_mul_assoc, mul_comm (#t : ℝ)]

Premises used: Finset.card_map, smul_mul_assoc, Nat.cast, Nat.cast_sum, mul_comm, Finset.card, nsmul_eq_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ∑ x ∈ G.badVertices ε s t, (↑(#({y ∈ t | G.Adj x y})) : ℝ) ≤
    #(G.badVertices ε s t) • (((↑(G.edgeDensity s t) : ℝ) - ε) * (↑(#t) : ℝ))

Tactic:
sum_le_card_nsmul _ _ _ fun x hx ↦ (mem_filter.1 hx).2.le

Premises used: LT.lt.le, Finset.sum_le_card_nsmul, And.right, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableRel G.Adj
ε : ℝ
s t : Finset α
⊢ ∑ x ∈ G.badVertices ε s t, (↑(#({y ∈ t | G.Adj x y})) : ℝ) ≤
    #(G.badVertices ε s t) • (((↑(G.edgeDensity s t) : ℝ) - ε) * (↑(#t) : ℝ))

Tactic:
exact sum_le_card_nsmul _ _ _ fun x hx ↦ (mem_filter.1 hx).2.le

Premises used: Finset.sum_le_card_nsmul