Theorem: Matroid.Flat.inter (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 : α
hF₁ : M.Flat F₁
hF₂ : M.Flat F₂
⊢ M.Flat (F₁ ∩ F₂)
Tactic:
rw [inter_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 : α
hF₁ : M.Flat F₁
hF₂ : M.Flat F₂
⊢ M.Flat (⋂ b, bif b then F₁ else F₂)

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 : α
hF₁ : M.Flat F₁
hF₂ : M.Flat F₂
⊢ M.Flat (⋂ b, bif b then F₁ else F₂)
Tactic:
apply Flat.iInter
State after:
case hFs
α : 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 : α
hF₁ : M.Flat F₁
hF₂ : M.Flat F₂
⊢ ∀ (i : Bool), M.Flat (bif i then F₁ else F₂)

State before:
case hFs
α : 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 : α
hF₁ : M.Flat F₁
hF₂ : M.Flat F₂
⊢ ∀ (i : Bool), M.Flat (bif i then F₁ else F₂)
Tactic:
simp [hF₁, hF₂]
State after:
no goals