Theorem: Matroid.modularPair_iff_exists_basis_basis (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 : α
⊢ M.ModularPair X Y ↔ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Tactic:
rw [modularPair_iff]
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 : α
⊢ (∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y) ↔ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)

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 : α
⊢ (∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y) ↔ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Tactic:
refine ⟨fun ⟨I,hI,hIX,hIY⟩ ↦ ⟨_, _, hIX, hIY, hI.subset (by simp)⟩,
  fun ⟨I,J,hI,hJ,hi⟩ ↦ ⟨_,hi, ?_⟩⟩
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 : α
x✝ : ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hi : M.Indep (I ∪ J)
⊢ M.Basis (X ∩ (I ∪ J)) X ∧ M.Basis (Y ∩ (I ∪ J)) Y

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 : α
x✝ : ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hi : M.Indep (I ∪ J)
⊢ M.Basis (X ∩ (I ∪ J)) X ∧ M.Basis (Y ∩ (I ∪ J)) Y
Tactic:
simp_rw [hi.inter_basis_cl_iff_subset_cl_inter]
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 : α
x✝ : ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hi : M.Indep (I ∪ J)
⊢ X ⊆ M.cl (X ∩ (I ∪ J)) ∧ Y ⊆ M.cl (Y ∩ (I ∪ J))

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 : α
x✝ : ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hi : M.Indep (I ∪ J)
⊢ X ⊆ M.cl (X ∩ (I ∪ J)) ∧ Y ⊆ M.cl (Y ∩ (I ∪ J))
Tactic:
use hI.subset_cl.trans (M.cl_subset_cl (subset_inter hI.subset subset_union_left))
State after:
case right
ι : 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 : α
x✝ : ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hi : M.Indep (I ∪ J)
⊢ Y ⊆ M.cl (Y ∩ (I ∪ J))

State before:
case right
ι : 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 : α
x✝ : ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
I J : Set α
hI : M.Basis I X
hJ : M.Basis J Y
hi : M.Indep (I ∪ J)
⊢ Y ⊆ M.cl (Y ∩ (I ∪ J))
Tactic:
exact hJ.subset_cl.trans (M.cl_subset_cl (subset_inter hJ.subset subset_union_right))
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 : α
x✝ : ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I : Set α
hI : M.Indep I
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ X ∩ I ∪ Y ∩ I ⊆ I
Tactic:
simp
State after:
no goals