Theorem: Matroid.Flat.iInter (Matroid/Flat.lean)

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
⊢ M.Flat (⋂ i, Fs i)
Tactic:
refine' ⟨fun I X hI hIX ↦ subset_iInter fun i ↦ _,
  (iInter_subset _ (Classical.arbitrary _)).trans (hFs _).subset_ground⟩
State after:
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
⊢ X ⊆ Fs i

State before:
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
⊢ X ⊆ Fs i
Tactic:
obtain ⟨J, hIJ, hJ⟩ := hI.indep.subset_basis_of_subset (hI.subset.trans (iInter_subset _ i))
State after:
case intro.intro
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
J : Set α
hIJ : M.Basis J (Fs i)
hJ : I ⊆ J
⊢ X ⊆ Fs i

State before:
case intro.intro
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
J : Set α
hIJ : M.Basis J (Fs i)
hJ : I ⊆ J
⊢ X ⊆ Fs i
Tactic:
refine' subset_union_right.trans ((hFs i).1 (X := Fs i ∪ X) hIJ _)
State after:
case intro.intro
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
J : Set α
hIJ : M.Basis J (Fs i)
hJ : I ⊆ J
⊢ M.Basis J (Fs i ∪ X)

State before:
case intro.intro
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
J : Set α
hIJ : M.Basis J (Fs i)
hJ : I ⊆ J
⊢ M.Basis J (Fs i ∪ X)
Tactic:
convert hIJ.basis_union (hIX.basis_union_of_subset hIJ.indep hJ) using 1
State after:
case h.e'_4
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
J : Set α
hIJ : M.Basis J (Fs i)
hJ : I ⊆ J
⊢ Fs i ∪ X = Fs i ∪ (J ∪ X)

State before:
case h.e'_4
α : Type u_1
M : Matroid α
I✝ F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.Flat (Fs i)
I X : Set α
hI : M.Basis I (⋂ i, Fs i)
hIX : M.Basis I X
i : ι
J : Set α
hIJ : M.Basis J (Fs i)
hJ : I ⊆ J
⊢ Fs i ∪ X = Fs i ∪ (J ∪ X)
Tactic:
rw [← union_assoc, union_eq_self_of_subset_right hIJ.subset]
State after:
no goals