Theorem: Matroid.Flat.biInter (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
Fs : ι → Set α
s : Set ι
hs : s.Nonempty
hFs : ∀ i ∈ s, M.Flat (Fs i)
⊢ M.Flat (⋂ i ∈ s, Fs i)
Tactic:
rw [biInter_eq_iInter]
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
Fs : ι → Set α
s : Set ι
hs : s.Nonempty
hFs : ∀ i ∈ s, M.Flat (Fs i)
⊢ M.Flat (⋂ x, Fs ↑x)

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
Fs : ι → Set α
s : Set ι
hs : s.Nonempty
hFs : ∀ i ∈ s, M.Flat (Fs i)
⊢ M.Flat (⋂ x, Fs ↑x)
Tactic:
have := hs.to_subtype
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
Fs : ι → Set α
s : Set ι
hs : s.Nonempty
hFs : ∀ i ∈ s, M.Flat (Fs i)
this : Nonempty ↑s
⊢ M.Flat (⋂ x, Fs ↑x)

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
Fs : ι → Set α
s : Set ι
hs : s.Nonempty
hFs : ∀ i ∈ s, M.Flat (Fs i)
this : Nonempty ↑s
⊢ M.Flat (⋂ x, Fs ↑x)
Tactic:
apply Flat.iInter (by simpa)
State after:
no goals

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
Fs : ι → Set α
s : Set ι
hs : s.Nonempty
hFs : ∀ i ∈ s, M.Flat (Fs i)
this : Nonempty ↑s
⊢ ∀ (i : ↑s), M.Flat (Fs ↑i)
Tactic:
simpa
State after:
no goals