rintro e f he hf
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hI : M.Indep I
⊢ ∀ ⦃e f : α⦄, e ∈ I → f ∈ I → M.Indep {e, f} ∧ e ∈ I ∧ f ∈ I
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
hI : M.Indep I
e f : α
he : e ∈ I
hf : f ∈ I
⊢ M.Indep {e, f} ∧ e ∈ I ∧ f ∈ I