Theorem: Matroid.modularPair_singleton (Matroid/Modular.lean)

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
⊢ M.ModularPair {e} X
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis X
State after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
⊢ M.ModularPair {e} X

State before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
⊢ M.ModularPair {e} X
Tactic:
have hi : M.Indep (insert e I) := by
  rw [hI.indep.insert_indep_iff, hI.cl_eq_cl]
  exact Or.inl ⟨he, heX⟩
State after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
hi : M.Indep (insert e I)
⊢ M.ModularPair {e} X

State before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
hi : M.Indep (insert e I)
⊢ M.ModularPair {e} X
Tactic:
have hI' := hI.insert_basis_insert hi
State after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
hi : M.Indep (insert e I)
hI' : M.Basis (insert e I) (insert e X)
⊢ M.ModularPair {e} X

State before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
hi : M.Indep (insert e I)
hI' : M.Basis (insert e I) (insert e X)
⊢ M.ModularPair {e} X
Tactic:
rw [← singleton_union] at hI'
State after:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
hi : M.Indep (insert e I)
hI' : M.Basis ({e} ∪ I) (insert e X)
⊢ M.ModularPair {e} X

State before:
case intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
hi : M.Indep (insert e I)
hI' : M.Basis ({e} ∪ I) (insert e X)
⊢ M.ModularPair {e} X
Tactic:
exact hI'.indep.modularPair_of_union.of_basis_right hI
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
⊢ M.Indep (insert e I)
Tactic:
rw [hI.indep.insert_indep_iff, hI.cl_eq_cl]
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
⊢ e ∈ M.E \ M.cl X ∨ e ∈ I

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : e ∈ M.E
hX : X ⊆ M.E
heX : e ∉ M.cl X
I : Set α
hI : M.Basis I X
⊢ e ∈ M.E \ M.cl X ∨ e ∈ I
Tactic:
exact Or.inl ⟨he, heX⟩
State after:
no goals