-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.exists_insert_of_not_isBase (hI : M.Indep I) (hI' : ¬M.IsBase I) (hB : M.IsBase B) :
    ∃ e ∈ B \ I, M.Indep (insert e I)

Proof state:
case neg.intro.intro
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∉ B
e : α
he : e ∈ B \ B'
hBase : M.IsBase (insert e (B' \ {x}))
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
exact ⟨e, ⟨he.1, not_mem_subset hIB' he.2⟩,
  indep_iff.2 ⟨_, hBase, insert_subset_insert (subset_diff_singleton hIB' hx)⟩⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
hB' : M.IsBase I
hIB' : I ⊆ I
⊢ False

Tactic:
exact hI' hB'

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∉ B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
obtain ⟨e,he, hBase⟩ := hB'.exchange hB ⟨hxB',hxB⟩

Result:
case neg.intro.intro
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∉ B
e : α
he : e ∈ B \ B'
hBase : M.IsBase (insert e (B' \ {x}))
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Proof state:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
obtain ⟨B', hB', hIB'⟩ := hI.exists_isBase_superset

Result:
case intro.intro
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Proof state:
case pos
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∈ B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
exact ⟨x, ⟨hxB, hx⟩, hB'.indep.subset (insert_subset hxB' hIB')⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
⊢ I ≠ B'

Tactic:
rintro rfl

Result:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
hB' : M.IsBase I
hIB' : I ⊆ I
⊢ False

Proof state:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
⊢ I ≠ B'

Tactic:
(rintro rfl; exact hI' hB')

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
obtain ⟨x, hxB', hx⟩ := exists_of_ssubset (hIB'.ssubset_of_ne (by (rintro rfl; exact hI' hB')))

Result:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Proof state:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
by_cases hxB : x ∈ B

Result:
case pos
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∈ B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

case neg
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∉ B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)