Theorem: Matroid.FlatOf.coe_sInf' (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 : α
Fs : Set (FlatOf M)
hne : Fs.Nonempty
⊢ ↑(sInf Fs) = ⋂ F ∈ Fs, ↑F
Tactic:
simp only [coe_sInf, inter_eq_left]
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 : α
Fs : Set (FlatOf M)
hne : Fs.Nonempty
⊢ ⋂ F ∈ Fs, ↑F ⊆ M.E

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 : α
Fs : Set (FlatOf M)
hne : Fs.Nonempty
⊢ ⋂ F ∈ Fs, ↑F ⊆ M.E
Tactic:
exact (biInter_subset_of_mem hne.some_mem).trans (hne.some.coe_subset_ground)
State after:
no goals