obtain ⟨S, hS1, hS2⟩ := h1
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝¹ : DecidableRel G✝.Adj
inst✝ : DecidableRel H✝.Adj
s t : ℕ
G H : SimpleGraph α
h : s ≤ t
h1 : IsFar G H s
⊢ IsFar G H t
case intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝¹ : DecidableRel G✝.Adj
inst✝ : DecidableRel H✝.Adj
s t : ℕ
G H : SimpleGraph α
h : s ≤ t
S : Finset (Sym2 α)
hS1 : delFedges G S ≤ H
hS2 : card S ≤ s
⊢ IsFar G H t