refine ⟨fun ⟨hE, hi⟩ ↦ ⟨?_, ?_, ?_⟩, fun ⟨hi, hE, h⟩ ↦ ⟨?_, fun I hIss ↦ ?_⟩⟩
case inr
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
⊢ (M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I) ↔
    ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
case inr.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ¬M'.Indep {e}

case inr.refine_2
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ M'.E \ {e} = M.E

case inr.refine_3
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)

case inr.refine_4
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
⊢ M'.E = insert e M.E

case inr.refine_5
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
I : Set α
hIss : I ⊆ M'.E
⊢ M'.Indep I ↔ M.Indep I