rw [← insert_diff_singleton_comm hne, hi.insert_indep_iff_of_not_mem, mem_diff,
  and_iff_right ((M.cl_subset_ground _) he.1)]
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ e ∉ M.cl (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})

case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ e ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f}