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

State before:
α : 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
⊢ IsFar G H s → IsFar G H t
Tactic:
intro h1
State after:
α : 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

State before:
α : 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
Tactic:
obtain ⟨S, hS1, hS2⟩ := h1
State after:
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

State before:
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
Tactic:
exact ⟨S, hS1, hS2.trans h⟩
State after:
no goals