simp [disjoint_sdiff_right, hJ.indep]
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_1
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ (M ＼ ((M.E \ K₁) \ J)).Indep J
no goals