Theorem: SimpleGraph.delFedges_is_sdiff (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 α
inst✝ : DecidableRel H.Adj
⊢ delFedges G (edgeFinset H) = G \ H
Tactic:
ext u v
State after:
case Adj.h.h.a
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
inst✝ : DecidableRel H.Adj
u v : α
⊢ Adj (delFedges G (edgeFinset H)) u v ↔ Adj (G \ H) u v

State before:
case Adj.h.h.a
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
inst✝ : DecidableRel H.Adj
u v : α
⊢ Adj (delFedges G (edgeFinset H)) u v ↔ Adj (G \ H) u v
Tactic:
simp only [delFedges, sdiff_adj, Set.coe_toFinset,  Sym2.toRel_prop, mem_edgeSet]
State after:
case Adj.h.h.a
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
inst✝ : DecidableRel H.Adj
u v : α
⊢ Adj G u v \ Adj H u v ↔ Adj G u v ∧ ¬Adj H u v

State before:
case Adj.h.h.a
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
inst✝ : DecidableRel H.Adj
u v : α
⊢ Adj G u v \ Adj H u v ↔ Adj G u v ∧ ¬Adj H u v
Tactic:
rfl
State after:
no goals