Theorem: Matroid.SkewFamily.skew_compl (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.SkewFamily Xs
A : Set ι
⊢ M.Skew (⋃ i ∈ A, Xs i) (⋃ i ∈ Aᶜ, Xs i)
Tactic:
rw [skew_iff_modularPair_inter_subset_loops]
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.SkewFamily Xs
A : Set ι
⊢ M.ModularPair (⋃ i ∈ A, Xs i) (⋃ i ∈ Aᶜ, Xs i) ∧ (⋃ i ∈ A, Xs i) ∩ ⋃ i ∈ Aᶜ, Xs i ⊆ M.cl ∅

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.SkewFamily Xs
A : Set ι
⊢ M.ModularPair (⋃ i ∈ A, Xs i) (⋃ i ∈ Aᶜ, Xs i) ∧ (⋃ i ∈ A, Xs i) ∩ ⋃ i ∈ Aᶜ, Xs i ⊆ M.cl ∅
Tactic:
refine ⟨h.modularFamily.modularPair_compl_biUnion A, ?_⟩
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.SkewFamily Xs
A : Set ι
⊢ (⋃ i ∈ A, Xs i) ∩ ⋃ i ∈ Aᶜ, Xs i ⊆ M.cl ∅

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.SkewFamily Xs
A : Set ι
⊢ (⋃ i ∈ A, Xs i) ∩ ⋃ i ∈ Aᶜ, Xs i ⊆ M.cl ∅
Tactic:
rintro e ⟨⟨_,⟨i,hi,rfl⟩,hi'⟩ ,⟨_,⟨j,hj,rfl⟩,hj'⟩⟩
State after:
case intro.intro.intro.intro.refl.intro.intro.intro.refl
ι : 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.SkewFamily Xs
A : Set ι
e : α
i : ι
hi' : e ∈ (fun i => ⋃ (_ : i ∈ A), Xs i) i
j : ι
hj' : e ∈ (fun i => ⋃ (_ : i ∈ Aᶜ), Xs i) j
⊢ e ∈ M.cl ∅

State before:
case intro.intro.intro.intro.refl.intro.intro.intro.refl
ι : 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.SkewFamily Xs
A : Set ι
e : α
i : ι
hi' : e ∈ (fun i => ⋃ (_ : i ∈ A), Xs i) i
j : ι
hj' : e ∈ (fun i => ⋃ (_ : i ∈ Aᶜ), Xs i) j
⊢ e ∈ M.cl ∅
Tactic:
simp only [mem_iUnion, exists_prop] at hi' hj'
State after:
case intro.intro.intro.intro.refl.intro.intro.intro.refl
ι : 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.SkewFamily Xs
A : Set ι
e : α
i j : ι
hi' : i ∈ A ∧ e ∈ Xs i
hj' : j ∈ Aᶜ ∧ e ∈ Xs j
⊢ e ∈ M.cl ∅

State before:
case intro.intro.intro.intro.refl.intro.intro.intro.refl
ι : 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.SkewFamily Xs
A : Set ι
e : α
i j : ι
hi' : i ∈ A ∧ e ∈ Xs i
hj' : j ∈ Aᶜ ∧ e ∈ Xs j
⊢ e ∈ M.cl ∅
Tactic:
exact h.loop_of_mem_inter (show i ≠ j from fun hij ↦ hj'.1 <| hij ▸ hi'.1) ⟨hi'.2, hj'.2⟩
State after:
no goals