Theorem: insert_symm (Matroid/ForMathlib/PartialEquiv.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
e : PartialEquiv α β
ha : a ∉ e.source
hb : b ∉ e.target
⊢ (e.insert ha hb).symm = e.symm.insert hb ha
Tactic:
ext <;> simp
State after:
no goals