Theorem: Matroid.Indep.interBasis_biInter (Matroid/Closure.lean)

State before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ M.Basis ((⋂ i ∈ A, X i) ∩ I) (⋂ i ∈ A, X i)
Tactic:
refine (hI.inter_left _).basis_of_subset_of_subset_cl inter_subset_left ?_
State after:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ ⋂ i ∈ A, X i ⊆ M.cl ((⋂ i ∈ A, X i) ∩ I)

State before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ ⋂ i ∈ A, X i ⊆ M.cl ((⋂ i ∈ A, X i) ∩ I)
Tactic:
simp_rw [biInter_distrib_inter _ hA,
  cl_biInter_eq_biInter_cl_of_biUnion_indep hA (I := fun i ↦ (X i) ∩ I) (hI.subset (by simp)),
  subset_iInter_iff]
State after:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ ∀ i ∈ A, ⋂ i ∈ A, X i ⊆ M.cl (X i ∩ I)

State before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ ∀ i ∈ A, ⋂ i ∈ A, X i ⊆ M.cl (X i ∩ I)
Tactic:
exact fun i hiA ↦ (biInter_subset_of_mem hiA).trans (h i hiA).subset_cl
State after:
no goals

State before:
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ ⋃ i ∈ A, (fun i => X i ∩ I) i ⊆ I
Tactic:
simp
State after:
no goals