-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
lemma FarFromTriangleFree.lt_half (hG : G.FarFromTriangleFree ε) : ε < 2⁻¹

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ 2 * #⊤.edgeFinset < Fintype.card α ^ 2

Tactic:
rw [edgeFinset_top, filter_not, card_sdiff (subset_univ _), card_univ, Sym2.card]

Result:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ 2 * ((Fintype.card α + 1).choose 2 - #(filter Sym2.IsDiag univ)) < Fintype.card α ^ 2

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ 2 * #G.edgeFinset ≤ 2 * #⊤.edgeFinset

Tactic:
gcongr

Result:
case bc.a.a
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ G ≤ ⊤

Proof state:
case bc.a.a
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ G ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ Fintype.card α * (Fintype.card α + 1) - 2 * #(image Sym2.diag univ) < Fintype.card α ^ 2

Tactic:
rw [card_image_of_injective _ Sym2.diag_injective, card_univ, mul_add_one (α := ℕ), two_mul, sq,
  add_tsub_add_eq_tsub_right]

Result:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ Fintype.card α * Fintype.card α - Fintype.card α < Fintype.card α * Fintype.card α

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ 2 * #G.edgeFinset < Fintype.card α ^ 2

Tactic:
calc
  _ ≤ 2 * (⊤ : SimpleGraph α).edgeFinset.card := by gcongr; exact le_top
  _ < card α ^ 2 := ?_

Result:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ 2 * #⊤.edgeFinset < Fintype.card α ^ 2

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ Fintype.card α * Fintype.card α - Fintype.card α < Fintype.card α * Fintype.card α

Tactic:
apply tsub_lt_self <;> positivity

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ ε * ↑(Fintype.card α) ^ 2 ≤ ↑(#G.edgeFinset)

Tactic:
simpa using hG.le_card_sub_card bot_le (cliqueFree_bot (le_succ _))

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 2⁻¹ ≤ ε
⊢ False

Tactic:
refine lt_irrefl (ε * card α ^ 2) ?_

Result:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 2⁻¹ ≤ ε
⊢ ε * ↑(Fintype.card α) ^ 2 < ε * ↑(Fintype.card α) ^ 2

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
⊢ ε < 2⁻¹

Tactic:
by_contra! hε

Result:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 2⁻¹ ≤ ε
⊢ False

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ 1 ≤ ε * 2

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ ε * ↑(Fintype.card α) ^ 2 < ε * ↑(Fintype.card α) ^ 2

Tactic:
calc
  _ ≤ (#G.edgeFinset : 𝕜) := by
    simpa using hG.le_card_sub_card bot_le (cliqueFree_bot (le_succ _))
  _ ≤ ε * 2 * #G.edgeFinset := le_mul_of_one_le_left (by positivity) (by assumption)
  _ < ε * card α ^ 2 := ?_

Result:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ ε * 2 * ↑(#G.edgeFinset) < ε * ↑(Fintype.card α) ^ 2

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 2⁻¹ ≤ ε
⊢ 0 < 2⁻¹

Tactic:
norm_num

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ ε * 2 * ↑(#G.edgeFinset) < ε * ↑(Fintype.card α) ^ 2

Tactic:
rw [mul_assoc, mul_lt_mul_left hε₀]

Result:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ 2 * ↑(#G.edgeFinset) < ↑(Fintype.card α) ^ 2

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ 2 * ↑(#G.edgeFinset) < ↑(Fintype.card α) ^ 2

Tactic:
norm_cast

Result:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ 2 * #G.edgeFinset < Fintype.card α ^ 2

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 1 ≤ ε * 2
hε₀ : 0 < ε
⊢ 0 ≤ ↑(#G.edgeFinset)

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 2⁻¹ ≤ ε
⊢ ε * ↑(Fintype.card α) ^ 2 < ε * ↑(Fintype.card α) ^ 2

Tactic:
have hε₀ : 0 < ε := hε.trans_lt' (by norm_num)

Result:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
hG : G.FarFromTriangleFree ε
hε : 2⁻¹ ≤ ε
hε₀ : 0 < ε
⊢ ε * ↑(Fintype.card α) ^ 2 < ε * ↑(Fintype.card α) ^ 2