Theorem: Matroid.Indep.modularFamily_of_subsets (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 : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
⊢ M.ModularFamily Js
Tactic:
refine hI.modularFamily (fun i ↦ ?_)
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 : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
i : ι
⊢ M.Basis (Js i ∩ I) (Js 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 : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
i : ι
⊢ M.Basis (Js i ∩ I) (Js i)
Tactic:
have hJI : Js i ⊆ I := (subset_iUnion _ i).trans hJs
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 : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
i : ι
hJI : Js i ⊆ I
⊢ M.Basis (Js i ∩ I) (Js 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 : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
i : ι
hJI : Js i ⊆ I
⊢ M.Basis (Js i ∩ I) (Js i)
Tactic:
rw [inter_eq_self_of_subset_left hJI]
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 : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
i : ι
hJI : Js i ⊆ I
⊢ M.Basis (Js i) (Js 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 : α
hI : M.Indep I
hJs : ⋃ i, Js i ⊆ I
i : ι
hJI : Js i ⊆ I
⊢ M.Basis (Js i) (Js i)
Tactic:
exact (hI.subset hJI).basis_self
State after:
no goals