rintro I - hf -
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I C : Set α
M : Matroid α
e f : α
⊢ ∀ I ⊆ M.E,
    f ∉ I →
      f ∉ I →
        ((M.Indep (if f ∈ I then insert e (I \ {f}) else I) ∧ (f ∈ I → e ∈ I → f = e)) ∧ I ⊆ insert f M.E ↔ M.Indep I)
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f✝ x : α
I✝ C : Set α
M : Matroid α
e f : α
I : Set α
hf : f ∉ I
⊢ (M.Indep (if f ∈ I then insert e (I \ {f}) else I) ∧ (f ∈ I → e ∈ I → f = e)) ∧ I ⊆ insert f M.E ↔ M.Indep I