-- Mathlib/Data/Matroid/Basic.lean
theorem IsBase.eq_exchange_of_diff_eq_singleton (hB : M.IsBase B) (hB' : M.IsBase B')
    (h : B \ B' = {e}) : ∃ f ∈ B' \ B, B' = (insert f B) \ {e}

Proof state:
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f (B \ {e}))
⊢ f ≠ e

Tactic:
rintro rfl

Result:
α : Type u_1
M : Matroid α
B B' : Set α
hB : M.IsBase B
hB' : M.IsBase B'
f : α
hf : f ∈ B' \ B
h : B \ B' = {f}
hb : M.IsBase (insert f (B \ {f}))
⊢ False

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f (B \ {e}))
hne : f ≠ e
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}

Tactic:
rw [insert_diff_singleton_comm hne] at hb

Result:
case intro.intro
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f B \ {e})
hne : f ≠ e
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}

Proof state:
α : Type u_1
M : Matroid α
B B' : Set α
hB : M.IsBase B
hB' : M.IsBase B'
f : α
hf : f ∈ B' \ B
h : B \ B' = {f}
hb : M.IsBase (insert f (B \ {f}))
⊢ False

Tactic:
exact hf.2 (h.symm.subset (mem_singleton f)).1

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f B \ {e})
hne : f ≠ e
⊢ f ∈ B' ∪ {e}

Tactic:
exact Or.inl hf.1

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f (B \ {e}))
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}

Tactic:
have hne : f ≠ e := by rintro rfl; exact hf.2 (h.symm.subset (mem_singleton f)).1

Result:
case intro.intro
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f (B \ {e}))
hne : f ≠ e
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f B \ {e})
hne : f ≠ e
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}

Tactic:
refine ⟨f, hf, (hb.eq_of_subset_isBase hB' ?_).symm⟩

Result:
case intro.intro
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f B \ {e})
hne : f ≠ e
⊢ insert f B \ {e} ⊆ B'

Proof state:
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}

Tactic:
obtain ⟨f, hf, hb⟩ := hB.exchange hB' (h.symm.subset (mem_singleton e))

Result:
case intro.intro
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f (B \ {e}))
⊢ ∃ f ∈ B' \ B, B' = insert f B \ {e}

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f B \ {e})
hne : f ≠ e
⊢ insert f B \ {e} ⊆ B'

Tactic:
rw [diff_subset_iff, insert_subset_iff, union_comm, ← diff_subset_iff, h, and_iff_left rfl.subset]

Result:
case intro.intro
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f B \ {e})
hne : f ≠ e
⊢ f ∈ B' ∪ {e}