Theorem: Matroid.insert_base_of_insert_indep (Matroid/ForMathlib/MatroidBasic.lean)

State before:
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
⊢ M.Base (insert f I)
Tactic:
obtain (rfl | hef) := eq_or_ne e f
State after:
case inl
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∉ I
heI : M.Base (insert e I)
hf : e ∉ I
hfI : M.Indep (insert e I)
⊢ M.Base (insert e I)

case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.Base (insert f I)

State before:
case inl
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∉ I
heI : M.Base (insert e I)
hf : e ∉ I
hfI : M.Indep (insert e I)
⊢ M.Base (insert e I)

case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.Base (insert f I)
Tactic:
assumption
State after:
case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.Base (insert f I)

State before:
case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.Base (insert f I)
Tactic:
simpa [diff_singleton_eq_self he, hfI]
  using heI.exchange_base_of_indep (e := e) (f := f) (by simp [hef.symm, hf])
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.Base (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ f ∉ insert e I
Tactic:
simp [hef.symm, hf]
State after:
no goals