rintro rfl
case inl.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ ¬M' = M.addLoop e
case inl.refine_1
α : Type u_1
M : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ (M.addLoop e).E
⊢ False