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

State before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ Disjoint (edgeFinset G) (edgeFinset H) ↔ G ⊓ H = ⊥
Tactic:
rw [disjoint_iff,← edgeFinset_inj,edgeFinset_inf,inf_eq_inter,edgeFinset_bot,bot_eq_empty]
State after:
no goals