Theorem: Matroid.Skew.union_indep_of_indep_subsets (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 : α
h : M.Skew X Y
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ M.Indep (I ∪ J)
Tactic:
rw [union_eq_iUnion]
State after:
ι : 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 : α
h : M.Skew X Y
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ M.Indep (⋃ b, bif b then I else J)

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 : α
h : M.Skew X Y
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ M.Indep (⋃ b, bif b then I else J)
Tactic:
exact SkewFamily.iUnion_indep_subset_indep h (Is := fun i ↦ bif i then I else J)
  (Bool.rec (by simpa) (by simpa)) (Bool.rec (by simpa) (by simpa))
State after:
no goals

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 : α
h : M.Skew X Y
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ (fun i => bif i then I else J) false ⊆ bif false then X else Y
Tactic:
simpa
State after:
no goals

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 : α
h : M.Skew X Y
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ (fun i => bif i then I else J) true ⊆ bif true then X else Y
Tactic:
simpa
State after:
no goals

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 : α
h : M.Skew X Y
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ M.Indep ((fun i => bif i then I else J) false)
Tactic:
simpa
State after:
no goals

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 : α
h : M.Skew X Y
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ M.Indep ((fun i => bif i then I else J) true)
Tactic:
simpa
State after:
no goals