Theorem: Matroid.Flat.iInter_inter_ground (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 α
hFs : ∀ (i : ι), M.Flat (Fs i)
⊢ M.Flat ((⋂ i, Fs i) ∩ M.E)
Tactic:
obtain (hι | hι) := isEmpty_or_nonempty ι
State after:
case inl
α : 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 α
hFs : ∀ (i : ι), M.Flat (Fs i)
hι : IsEmpty ι
⊢ M.Flat ((⋂ i, Fs i) ∩ M.E)

case inr
α : 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 α
hFs : ∀ (i : ι), M.Flat (Fs i)
hι : Nonempty ι
⊢ M.Flat ((⋂ i, Fs i) ∩ M.E)

State before:
case inr
α : 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 α
hFs : ∀ (i : ι), M.Flat (Fs i)
hι : Nonempty ι
⊢ M.Flat ((⋂ i, Fs i) ∩ M.E)
Tactic:
exact (Flat.iInter hFs).inter M.ground_flat
State after:
no goals

State before:
case inl
α : 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 α
hFs : ∀ (i : ι), M.Flat (Fs i)
hι : IsEmpty ι
⊢ M.Flat ((⋂ i, Fs i) ∩ M.E)
Tactic:
simp
State after:
no goals