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

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
ha : a ∉ φ.source
hb : b ∉ φ.target
⊢ φ < φ.insert ha hb
Tactic:
refine ⟨⟨subset_insert _ _, fun hi ↦ φ.insert_apply_mem _ _ hi⟩, ?_⟩
State after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
ha : a ∉ φ.source
hb : b ∉ φ.target
⊢ ¬((φ.insert ha hb).source ⊆ φ.source ∧ ∀ {i : α}, i ∈ (φ.insert ha hb).source → ↑φ i = ↑(φ.insert ha hb) i)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
ha : a ∉ φ.source
hb : b ∉ φ.target
⊢ ¬((φ.insert ha hb).source ⊆ φ.source ∧ ∀ {i : α}, i ∈ (φ.insert ha hb).source → ↑φ i = ↑(φ.insert ha hb) i)
Tactic:
simp only [insert_source, not_and]
State after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
ha : a ∉ φ.source
hb : b ∉ φ.target
⊢ insert a φ.source ⊆ φ.source → ¬∀ {i : α}, i ∈ insert a φ.source → ↑φ i = ↑(φ.insert ha hb) i

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
ha : a ∉ φ.source
hb : b ∉ φ.target
⊢ insert a φ.source ⊆ φ.source → ¬∀ {i : α}, i ∈ insert a φ.source → ↑φ i = ↑(φ.insert ha hb) i
Tactic:
exact fun h ↦ (ha <| h (Or.inl rfl)).elim
State after:
no goals