Theorem: SimpleGraph.isFar_trivial (Turan4/Fedges.lean)

State before:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
⊢ card (edgeFinset G) ≤ s → IsFar G H s
Tactic:
intro h
State after:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ IsFar G H s

State before:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ IsFar G H s
Tactic:
refine ⟨G.edgeFinset, ?_, h⟩
State after:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ delFedges G (edgeFinset G) ≤ H

State before:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ delFedges G (edgeFinset G) ≤ H
Tactic:
rw [delFedges_is_sdiff,_root_.sdiff_self]
State after:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ ⊥ ≤ H

State before:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ ⊥ ≤ H
Tactic:
exact bot_le
State after:
no goals