Theorem: Matroid.modularFamily_iff_of_subsingleton (Matroid/Modular.lean)

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : Subsingleton ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E
Tactic:
obtain (h | ⟨⟨i⟩⟩) := isEmpty_or_nonempty ι
State after:
case inl
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : Subsingleton ι
h : IsEmpty ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E

case inr.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E

State before:
case inl
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : Subsingleton ι
h : IsEmpty ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E

case inr.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E
Tactic:
simp
State after:
case inr.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E

State before:
case inr.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
⊢ M.ModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E
Tactic:
refine ⟨fun h ↦ h.subset_ground_of_mem, fun h ↦ ?_⟩
State after:
case inr.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
⊢ M.ModularFamily Xs

State before:
case inr.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
⊢ M.ModularFamily Xs
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (Xs i)
State after:
case inr.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
I : Set α
hI : M.Basis I (Xs i)
⊢ M.ModularFamily Xs

State before:
case inr.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
I : Set α
hI : M.Basis I (Xs i)
⊢ M.ModularFamily Xs
Tactic:
obtain ⟨B, hB, hIB⟩ := hI.indep.exists_base_superset
State after:
case inr.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
I : Set α
hI : M.Basis I (Xs i)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ M.ModularFamily Xs

State before:
case inr.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
I : Set α
hI : M.Basis I (Xs i)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ M.ModularFamily Xs
Tactic:
refine ⟨B, hB, fun j ↦ ?_⟩
State after:
case inr.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j✝ : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
I : Set α
hI : M.Basis I (Xs i)
B : Set α
hB : M.Base B
hIB : I ⊆ B
j : ι
⊢ M.Basis (Xs j ∩ B) (Xs j)

State before:
case inr.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B✝ I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j✝ : ι
e f : α
inst✝ : Subsingleton ι
i : ι
h : ∀ (i : ι), Xs i ⊆ M.E
I : Set α
hI : M.Basis I (Xs i)
B : Set α
hB : M.Base B
hIB : I ⊆ B
j : ι
⊢ M.Basis (Xs j ∩ B) (Xs j)
Tactic:
rwa [Subsingleton.elim j i, inter_comm, hI.inter_eq_of_subset_indep hIB hB.indep]
State after:
no goals