use insert x I
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx✝ : x ∈ X
h : x ∉ I
hx : x ∈ X \ I
⊢ ∃ t ∈ S, x ∈ t
case h
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx✝ : x ∈ X
h : x ∉ I
hx : x ∈ X \ I
⊢ insert x I ∈ S ∧ x ∈ insert x I