Theorem: Matroid.ModularCut.iInter_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
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
⊢ ⋂ i, Fs i ∈ U
Tactic:
have hwin := U.sInter_mem (Fs := range Fs) (range_nonempty Fs) ?_ ?_
State after:
case refine_3
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
hwin : ⋂₀ range Fs ∈ U
⊢ ⋂ i, Fs i ∈ U

case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
⊢ range Fs ⊆ ↑U

case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
⊢ M.ModularFamily fun F => ↑F

State before:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
⊢ M.ModularFamily fun F => ↑F
Tactic:
obtain ⟨B, hB, hB'⟩ := hFs_mod
State after:
case refine_2.intro.intro
α : Type u_1
M : Matroid α
I J B✝ F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
B : Set α
hB : M.Base B
hB' : ∀ (i : ι), M.Basis (Fs i ∩ B) (Fs i)
⊢ M.ModularFamily fun F => ↑F

State before:
case refine_2.intro.intro
α : Type u_1
M : Matroid α
I J B✝ F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
B : Set α
hB : M.Base B
hB' : ∀ (i : ι), M.Basis (Fs i ∩ B) (Fs i)
⊢ M.ModularFamily fun F => ↑F
Tactic:
exact ⟨B, hB, by simpa⟩
State after:
no goals

State before:
case refine_3
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
hwin : ⋂₀ range Fs ∈ U
⊢ ⋂ i, Fs i ∈ U
Tactic:
simpa using hwin
State after:
no goals

State before:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
⊢ range Fs ⊆ ↑U
Tactic:
rintro _ ⟨i, hi, rfl⟩
State after:
case refine_1.intro.refl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
i : ι
⊢ Fs i ∈ ↑U

State before:
case refine_1.intro.refl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
i : ι
⊢ Fs i ∈ ↑U
Tactic:
exact hFs i
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I J B✝ F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
B : Set α
hB : M.Base B
hB' : ∀ (i : ι), M.Basis (Fs i ∩ B) (Fs i)
⊢ ∀ (i : ↑(range Fs)), M.Basis ((fun F => ↑F) i ∩ B) ((fun F => ↑F) i)
Tactic:
simpa
State after:
no goals