-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem deleteFar_iff [Fintype (Sym2 V)] :
    G.DeleteFar p r ↔ ∀ ⦃H : SimpleGraph _⦄ [DecidableRel H.Adj],
      H ≤ G → p H → r ≤ #G.edgeFinset - #H.edgeFinset

Proof state:
case refine_2
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
s : Finset (Sym2 V)
hs : s ⊆ G.edgeFinset
hG : p (G.deleteEdges ↑s)
⊢ r ≤ ↑(#s)

Tactic:
simpa [card_sdiff hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub,
  card_le_card hs] using h (G.deleteEdges_le s) hG

Result:
no goals

Proof state:
case refine_1
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : G.DeleteFar p r
H : SimpleGraph V
x✝ : DecidableRel H.Adj
hHG : H ≤ G
hH : p H
this : p (G.deleteEdges ↑(G.edgeFinset \ H.edgeFinset)) → r ≤ ↑(#(G.edgeFinset \ H.edgeFinset))
⊢ r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
simp only [deleteEdges_sdiff_eq_of_le hHG, edgeFinset_mono hHG, card_sdiff,
  card_le_card, coe_sdiff, coe_edgeFinset, Nat.cast_sub] at this

Result:
case refine_1
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : G.DeleteFar p r
H : SimpleGraph V
x✝ : DecidableRel H.Adj
hHG : H ≤ G
hH : p H
this : p H → r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
⊢ r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Proof state:
case refine_1
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : G.DeleteFar p r
H : SimpleGraph V
x✝ : DecidableRel H.Adj
hHG : H ≤ G
hH : p H
this : p H → r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
⊢ r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
exact this hH

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
⊢ G.DeleteFar p r ↔
    ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
refine ⟨fun h H _ hHG hH ↦ ?_, fun h s hs hG ↦ ?_⟩

Result:
case refine_1
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : G.DeleteFar p r
H : SimpleGraph V
x✝ : DecidableRel H.Adj
hHG : H ≤ G
hH : p H
⊢ r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

case refine_2
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
s : Finset (Sym2 V)
hs : s ⊆ G.edgeFinset
hG : p (G.deleteEdges ↑s)
⊢ r ≤ ↑(#s)

Proof state:
case refine_1
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : G.DeleteFar p r
H : SimpleGraph V
x✝ : DecidableRel H.Adj
hHG : H ≤ G
hH : p H
⊢ r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
have := h (sdiff_subset (t := H.edgeFinset))

Result:
case refine_1
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : G.DeleteFar p r
H : SimpleGraph V
x✝ : DecidableRel H.Adj
hHG : H ≤ G
hH : p H
this : p (G.deleteEdges ↑(G.edgeFinset \ H.edgeFinset)) → r ≤ ↑(#(G.edgeFinset \ H.edgeFinset))
⊢ r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Proof state:
case refine_2
V : Type u_1
G : SimpleGraph V
𝕜 : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : Fintype ↑G.edgeSet
p : SimpleGraph V → Prop
r : 𝕜
inst✝ : Fintype (Sym2 V)
h : ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)
s : Finset (Sym2 V)
hs : s ⊆ G.edgeFinset
hG : p (G.deleteEdges ↑s)
⊢ r ≤ ↑(#s)

Tactic:
classical
simpa [card_sdiff hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub,
  card_le_card hs] using h (G.deleteEdges_le s) hG

Result:
no goals