-- Mathlib/Data/Matroid/Dual.lean
theorem IsBase.compl_inter_isBasis_of_inter_isBasis (hB : M.IsBase B) (hBX : M.IsBasis (B ∩ X) X) :
    M✶.IsBasis ((M.E \ B) ∩ (M.E \ X)) (M.E \ X)

Proof state:
case refine_2.intro.intro
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
hi : M.Indep (insert f (B ∩ X))
⊢ False

Tactic:
exact hfb.2 (hBX.mem_of_insert_indep (Or.elim (hem.1 hfb.1) (False.elim ∘ hfb.2) id) hi).1

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ B ∩ X ⊆ B \ {e}

Tactic:
simp_rw [subset_diff, and_iff_right inter_subset_left, disjoint_singleton_right,
  mem_inter_iff, iff_false_intro he.1.2, and_false, not_false_iff]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
⊢ ∀ (B_1 : Set α), M.IsBase B_1 → (insert e (M.E \ B ∩ (M.E \ X)) ∩ B_1).Nonempty

Tactic:
refine fun B' hB' ↦ by_contra (fun hem ↦ ?_)

Result:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : ¬(insert e (M.E \ B ∩ (M.E \ X)) ∩ B').Nonempty
⊢ False

Proof state:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : ¬(insert e (M.E \ B ∩ (M.E \ X)) ∩ B').Nonempty
⊢ False

Tactic:
rw [nonempty_iff_ne_empty, not_ne_iff, ← union_singleton, diff_inter_diff,
 union_inter_distrib_right, union_empty_iff, singleton_inter_eq_empty, diff_eq,
 inter_right_comm, inter_eq_self_of_subset_right hB'.subset_ground, ← diff_eq,
 diff_eq_empty] at hem

Result:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
⊢ False

Proof state:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : e ∈ (M.E \ X) \ (M.E \ B ∩ (M.E \ X))
⊢ M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))

Tactic:
simp only [diff_inter_self_eq_diff, mem_diff, not_and, not_not, imp_iff_right he.1.1] at he

Result:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
⊢ M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))

Proof state:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ M✶.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

Tactic:
refine Indep.isBasis_of_forall_insert ?_ inter_subset_right (fun e he ↦ ?_)

Result:
case refine_1
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ M✶.Indep (M.E \ B ∩ (M.E \ X))

case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : e ∈ (M.E \ X) \ (M.E \ B ∩ (M.E \ X))
⊢ M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))

Proof state:
case refine_1
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ M✶.Indep (M.E \ B ∩ (M.E \ X))

Tactic:
rw [dual_indep_iff_exists]

Result:
case refine_1
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ ∃ B_1, M.IsBase B_1 ∧ Disjoint (M.E \ B ∩ (M.E \ X)) B_1

Proof state:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
⊢ False

Tactic:
obtain ⟨f, hfb, hBf⟩ := hB.exchange hB' ⟨he.2, hem.2⟩

Result:
case refine_2.intro.intro
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ False

Proof state:
case refine_1
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ ∃ B_1, M.IsBase B_1 ∧ Disjoint (M.E \ B ∩ (M.E \ X)) B_1

Tactic:
exact ⟨B, hB, disjoint_of_subset_left inter_subset_left disjoint_sdiff_left⟩

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ False

Tactic:
have hi : M.Indep (insert f (B ∩ X)) := by
  refine hBf.indep.subset (insert_subset_insert ?_)
  simp_rw [subset_diff, and_iff_right inter_subset_left, disjoint_singleton_right,
    mem_inter_iff, iff_false_intro he.1.2, and_false, not_false_iff]

Result:
case refine_2.intro.intro
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
hi : M.Indep (insert f (B ∩ X))
⊢ False

Proof state:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
⊢ M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))

Tactic:
simp_rw [dual_dep_iff_forall, insert_subset_iff, and_iff_right he.1.1,
  and_iff_left (inter_subset_left.trans diff_subset)]

Result:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
⊢ ∀ (B_1 : Set α), M.IsBase B_1 → (insert e (M.E \ B ∩ (M.E \ X)) ∩ B_1).Nonempty

Proof state:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ M.Indep (insert f (B ∩ X))

Tactic:
refine hBf.indep.subset (insert_subset_insert ?_)

Result:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ B ∩ X ⊆ B \ {e}