Theorem: Matroid.Indep.skewFamily_of_disjoint_bases (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, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
⊢ M.SkewFamily Xs
Tactic:
refine ⟨hI.modularFamily fun i ↦ ?_, fun i j hij ↦ ?_⟩
State after:
case refine_1
ι : 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, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i : ι
⊢ M.Basis (Xs i ∩ ⋃ i, Is i) (Xs i)

case refine_2
ι : 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, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i j : ι
hij : i ≠ j
⊢ Xs i ∩ Xs j ⊆ M.cl ∅

State before:
case refine_2
ι : 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, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i j : ι
hij : i ≠ j
⊢ Xs i ∩ Xs j ⊆ M.cl ∅
Tactic:
refine (inter_subset_inter (M.subset_cl _ (hIs i).subset_ground)
  (M.subset_cl _ (hIs j).subset_ground)).trans ?_
State after:
case refine_2
ι : 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, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i j : ι
hij : i ≠ j
⊢ M.cl (Xs i) ∩ M.cl (Xs j) ⊆ M.cl ∅

State before:
case refine_2
ι : 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, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i j : ι
hij : i ≠ j
⊢ M.cl (Xs i) ∩ M.cl (Xs j) ⊆ M.cl ∅
Tactic:
rw [← (hIs i).cl_eq_cl, ← (hIs j).cl_eq_cl, ← (hI.subset _).cl_inter_eq_inter_cl,
  Disjoint.inter_eq <| hdj hij]
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, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i j : ι
hij : i ≠ j
⊢ Is i ∪ Is j ⊆ ⋃ i, Is 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, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i j : ι
hij : i ≠ j
⊢ Is i ∪ Is j ⊆ ⋃ i, Is i
Tactic:
exact union_subset (subset_iUnion _ _) (subset_iUnion _ _)
State after:
no goals

State before:
case refine_1
ι : 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, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i : ι
⊢ M.Basis (Xs i ∩ ⋃ i, Is i) (Xs i)
Tactic:
rw [hI.inter_basis_cl_iff_subset_cl_inter]
State after:
case refine_1
ι : 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, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i : ι
⊢ Xs i ⊆ M.cl (Xs i ∩ ⋃ i, Is i)

State before:
case refine_1
ι : 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, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i : ι
⊢ Xs i ⊆ M.cl (Xs i ∩ ⋃ i, Is i)
Tactic:
exact (hIs i).subset_cl.trans (M.cl_subset_cl (subset_inter (hIs i).subset (subset_iUnion _ i)))
State after:
no goals