[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝¹ : Fintype α
inst✝ : LinearOrderedField 𝕜
G H : SimpleGraph α
ε δ : 𝕜
n : ℕ
s : Finset α
hε : FarFromTriangleFree G ε
h : δ ≤ ε
⊢ δ * ↑(Fintype.card α ^ 2) ≤ ε * ↑(Fintype.card α ^ 2)
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : Fintype α
inst✝¹ : LinearOrderedField 𝕜
G H : SimpleGraph α
ε δ : 𝕜
n : ℕ
s : Finset α
inst✝ : Nonempty α
h₀ : FarFromTriangleFree G ε
h₁ : CliqueFree G 3
⊢ ε ≤ 0
[PROOFSTEP]
have := h₀ (empty_subset _)
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : Fintype α
inst✝¹ : LinearOrderedField 𝕜
G H : SimpleGraph α
ε δ : 𝕜
n : ℕ
s : Finset α
inst✝ : Nonempty α
h₀ : FarFromTriangleFree G ε
h₁ : CliqueFree G 3
this : (fun H => CliqueFree H 3) (deleteEdges G ↑∅) → ε * ↑(Fintype.card α ^ 2) ≤ ↑(Finset.card ∅)
⊢ ε ≤ 0
[PROOFSTEP]
rw [coe_empty, Finset.card_empty, cast_zero, deleteEdges_empty_eq] at this 
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝² : Fintype α
inst✝¹ : LinearOrderedField 𝕜
G H : SimpleGraph α
ε δ : 𝕜
n : ℕ
s : Finset α
inst✝ : Nonempty α
h₀ : FarFromTriangleFree G ε
h₁ : CliqueFree G 3
this : (fun H => CliqueFree H 3) G → ε * ↑(Fintype.card α ^ 2) ≤ 0
⊢ ε ≤ 0
[PROOFSTEP]
exact nonpos_of_mul_nonpos_left (this h₁) (cast_pos.2 <| sq_pos_of_pos Fintype.card_pos)
