Theorem: PartialEquiv.insert_apply_mem (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
i : α
hi : i ∈ e.source
⊢ ↑(e.insert ha hb) i = ↑e i
Tactic:
rw [insert_apply, update_apply, if_neg]
State after:
case hnc
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
e : PartialEquiv α β
ha : a ∉ e.source
hb : b ∉ e.target
i : α
hi : i ∈ e.source
⊢ ¬i = a

State before:
case hnc
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
e : PartialEquiv α β
ha : a ∉ e.source
hb : b ∉ e.target
i : α
hi : i ∈ e.source
⊢ ¬i = a
Tactic:
exact fun h ↦ ha <| h ▸ hi
State after:
no goals