Theorem: Matroid.ModularCut.inter_mem (Matroid/Extension.lean)

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ F ∩ F' ∈ U
Tactic:
rw [inter_eq_iInter]
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ (⋂ b, bif b then F else F') ∈ U

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ (⋂ b, bif b then F else F') ∈ U
Tactic:
apply U.iInter_mem
State after:
case hFs
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ ∀ (i : Bool), (bif i then F else F') ∈ U

case hFs_mod
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ M.ModularFamily fun i => bif i then F else F'

State before:
case hFs_mod
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ M.ModularFamily fun i => bif i then F else F'
Tactic:
exact h
State after:
no goals

State before:
case hFs
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ ∀ (i : Bool), (bif i then F else F') ∈ U
Tactic:
simp [hF, hF']
State after:
no goals