Theorem: Matroid.modularPair_of_subset (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 : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
⊢ M.ModularPair X Y
Tactic:
obtain ⟨I,J, hI, hJ, hIJ⟩ := M.exists_basis_subset_basis hXY
State after:
case intro.intro.intro.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 : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.ModularPair X Y

State before:
case intro.intro.intro.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 : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.ModularPair X Y
Tactic:
refine modularPair_iff.2 ⟨J, hJ.indep, ?_, by rwa [inter_eq_self_of_subset_right hJ.subset]⟩
State after:
case intro.intro.intro.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 : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.Basis (X ∩ J) X

State before:
case intro.intro.intro.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 : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.Basis (X ∩ J) X
Tactic:
rwa [← hI.eq_of_subset_indep (hJ.indep.inter_left X) (subset_inter hI.subset hIJ)
  inter_subset_left]
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 : α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.Basis (Y ∩ J) Y
Tactic:
rwa [inter_eq_self_of_subset_right hJ.subset]
State after:
no goals