-- Mathlib/Data/Matroid/Basic.lean
theorem isBase_compl_iff_maximal_disjoint_isBase (hB : B ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
⊢ M.IsBase (M.E \ B) ↔ Maximal (fun I => I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) B

Tactic:
simp_rw [maximal_iff, and_iff_right hB, and_imp, forall_exists_index]

Result:
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
⊢ M.IsBase (M.E \ B) ↔
    (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y

Proof state:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ I ≤ B

Tactic:
rw [hB'.eq_of_subset_isBase h, ← subset_compl_iff_disjoint_right, diff_eq, compl_inter,
  compl_compl] at hIB'

Result:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : I ⊆ M.Eᶜ ∪ B
⊢ I ≤ B

case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ B' ⊆ M.E \ B

Proof state:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : I ⊆ M.Eᶜ ∪ B
⊢ I ≤ B

Tactic:
exact fun e he ↦ (hIB' he).elim (fun h' ↦ (h' (hI he)).elim) id

Result:
no goals

Proof state:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ B' ⊆ M.E \ B

Tactic:
rw [subset_diff, and_iff_right hB'.subset_ground, disjoint_comm]

Result:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ Disjoint B B'

Proof state:
case refine_2
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
x✝ :
  (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y
⊢ M.IsBase (M.E \ (M.E \ B'))

Tactic:
simpa [hB'.subset_ground]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
x✝ :
  (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y
⊢ M.IsBase (M.E \ B)

Tactic:
rw [h diff_subset B' ⟨hB', disjoint_sdiff_left⟩]

Result:
case refine_2
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
x✝ :
  (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y
⊢ M.IsBase (M.E \ (M.E \ B'))

case refine_2
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
x✝ :
  (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y
⊢ B ≤ M.E \ B'

Proof state:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ Disjoint B B'

Tactic:
exact disjoint_of_subset_left hBI hIB'

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
⊢ M.IsBase (M.E \ B) ↔
    (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y

Tactic:
refine ⟨fun h ↦ ⟨⟨_, h, disjoint_sdiff_right⟩,
  fun I hI B' ⟨hB', hIB'⟩ hBI ↦ hBI.antisymm ?_⟩, fun ⟨⟨B', hB', hBB'⟩,h⟩ ↦ ?_⟩

Result:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ≤ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ I ≤ B

case refine_2
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
x✝ :
  (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y
⊢ M.IsBase (M.E \ B)

Proof state:
case refine_2
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
x✝ :
  (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ≤ y → B = y
⊢ B ≤ M.E \ B'

Tactic:
simp [subset_diff, hB, hBB']

Result:
no goals