Theorem: Matroid.skewFamily_iff_forall_circuit (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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
⊢ M.SkewFamily Xs ↔ ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Tactic:
refine ⟨fun h C hC hCU ↦ ?_, fun h ↦ ?_⟩
State after:
case refine_1
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
⊢ ∃ i, C ⊆ Xs i

case refine_2
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
⊢ M.SkewFamily Xs

State before:
case refine_2
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
⊢ M.SkewFamily Xs
Tactic:
choose Is hIs using fun i ↦ M.exists_basis _ (hXs i)
State after:
case refine_2
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
⊢ M.SkewFamily Xs

State before:
case refine_2
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
⊢ M.SkewFamily Xs
Tactic:
have hss := iUnion_mono (fun i ↦ (hIs i).subset)
State after:
case refine_2
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
⊢ M.SkewFamily Xs

State before:
case refine_2
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
⊢ M.SkewFamily Xs
Tactic:
have hIe : ⋃ i, Is i ⊆ M.E := by simp [fun i ↦ (hIs i).subset.trans (hXs i)]
State after:
case refine_2
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
⊢ M.SkewFamily Xs

State before:
case refine_2
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
⊢ M.SkewFamily Xs
Tactic:
refine Indep.skewFamily_of_disjoint_bases ?_ ?_ hIs
State after:
case refine_2.refine_1
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
⊢ M.Indep (⋃ i, Is i)

case refine_2.refine_2
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
⊢ Pairwise (Disjoint on fun i => Is i)

State before:
case refine_2.refine_2
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
⊢ Pairwise (Disjoint on fun i => Is i)
Tactic:
exact fun i j hne ↦ (hdj hne).mono ((hIs i).subset) ((hIs j).subset)
State after:
no goals

State before:
case refine_1
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
⊢ ∃ i, C ⊆ Xs i
Tactic:
have h : ∃ i, ¬ M.Indep (C ∩ Xs i) := by
  by_contra! hcon
  refine hC.dep.not_indep ?_
  refine (h.iUnion_indep_subset_indep (fun i ↦ inter_subset_right) hcon).subset ?_
  simp [← inter_iUnion, hCU, Subset.rfl]
State after:
case refine_1
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h✝ : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
h : ∃ i, ¬M.Indep (C ∩ Xs i)
⊢ ∃ i, C ⊆ Xs i

State before:
case refine_1
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h✝ : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
h : ∃ i, ¬M.Indep (C ∩ Xs i)
⊢ ∃ i, C ⊆ Xs i
Tactic:
obtain ⟨i, hi⟩ := h
State after:
case refine_1.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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
i : ι
hi : ¬M.Indep (C ∩ Xs i)
⊢ ∃ i, C ⊆ Xs i

State before:
case refine_1.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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
i : ι
hi : ¬M.Indep (C ∩ Xs i)
⊢ ∃ i, C ⊆ Xs i
Tactic:
rw [← hC.eq_of_not_indep_subset hi inter_subset_left]
State after:
case refine_1.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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
i : ι
hi : ¬M.Indep (C ∩ Xs i)
⊢ ∃ i_1, C ∩ Xs i ⊆ Xs i_1

State before:
case refine_1.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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
i : ι
hi : ¬M.Indep (C ∩ Xs i)
⊢ ∃ i_1, C ∩ Xs i ⊆ Xs i_1
Tactic:
exact ⟨i, inter_subset_right⟩
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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
⊢ ∃ i, ¬M.Indep (C ∩ Xs i)
Tactic:
by_contra! hcon
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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
hcon : ∀ (i : ι), M.Indep (C ∩ Xs i)
⊢ False

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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
hcon : ∀ (i : ι), M.Indep (C ∩ Xs i)
⊢ False
Tactic:
refine hC.dep.not_indep ?_
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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
hcon : ∀ (i : ι), M.Indep (C ∩ Xs i)
⊢ M.Indep C

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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
hcon : ∀ (i : ι), M.Indep (C ∩ Xs i)
⊢ M.Indep C
Tactic:
refine (h.iUnion_indep_subset_indep (fun i ↦ inter_subset_right) hcon).subset ?_
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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
hcon : ∀ (i : ι), M.Indep (C ∩ Xs i)
⊢ C ⊆ ⋃ i, C ∩ Xs i

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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : M.SkewFamily Xs
C : Set α
hC : M.Circuit C
hCU : C ⊆ ⋃ i, Xs i
hcon : ∀ (i : ι), M.Indep (C ∩ Xs i)
⊢ C ⊆ ⋃ i, C ∩ Xs i
Tactic:
simp [← inter_iUnion, hCU, Subset.rfl]
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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
⊢ ⋃ i, Is i ⊆ M.E
Tactic:
simp [fun i ↦ (hIs i).subset.trans (hXs i)]
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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
⊢ ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
Tactic:
intro i
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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
i : ι
⊢ Xs i ∩ ⋃ j, Is j = Is i

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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
i : ι
⊢ Xs i ∩ ⋃ j, Is j = Is i
Tactic:
simp only [inter_iUnion, subset_antisymm_iff, iUnion_subset_iff]
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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
i : ι
⊢ (∀ (i_1 : ι), Xs i ∩ Is i_1 ⊆ Is i) ∧ Is i ⊆ ⋃ i_1, Xs i ∩ Is i_1

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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
i : ι
⊢ (∀ (i_1 : ι), Xs i ∩ Is i_1 ⊆ Is i) ∧ Is i ⊆ ⋃ i_1, Xs i ∩ Is i_1
Tactic:
refine ⟨fun j ↦ ?_, subset_iUnion_of_subset i (subset_inter (hIs i).subset Subset.rfl)⟩
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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
i j : ι
⊢ Xs i ∩ Is j ⊆ Is i

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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
i j : ι
⊢ Xs i ∩ Is j ⊆ Is i
Tactic:
obtain (rfl | hne) := eq_or_ne i j
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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
i : ι
⊢ Xs i ∩ Is i ⊆ Is i

case inr
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
i j : ι
hne : i ≠ j
⊢ Xs i ∩ Is j ⊆ Is i

State before:
case inr
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
i j : ι
hne : i ≠ j
⊢ Xs i ∩ Is j ⊆ Is i
Tactic:
simp [((hdj hne).mono_right (hIs j).subset).inter_eq]
State after:
no goals

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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
i : ι
⊢ Xs i ∩ Is i ⊆ Is i
Tactic:
apply inter_subset_right
State after:
no goals

State before:
case refine_2.refine_1
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
⊢ M.Indep (⋃ i, Is i)
Tactic:
rw [indep_iff_forall_subset_not_circuit hIe]
State after:
case refine_2.refine_1
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
⊢ ∀ C ⊆ ⋃ i, Is i, ¬M.Circuit C

State before:
case refine_2.refine_1
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
⊢ ∀ C ⊆ ⋃ i, Is i, ¬M.Circuit C
Tactic:
intro C hCss hC
State after:
case refine_2.refine_1
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
C : Set α
hCss : C ⊆ ⋃ i, Is i
hC : M.Circuit C
⊢ False

State before:
case refine_2.refine_1
ι : 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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
C : Set α
hCss : C ⊆ ⋃ i, Is i
hC : M.Circuit C
⊢ False
Tactic:
obtain ⟨i, hI⟩ := h C hC (hCss.trans hss)
State after:
case refine_2.refine_1.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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
C : Set α
hCss : C ⊆ ⋃ i, Is i
hC : M.Circuit C
i : ι
hI : C ⊆ Xs i
⊢ False

State before:
case refine_2.refine_1.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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
C : Set α
hCss : C ⊆ ⋃ i, Is i
hC : M.Circuit C
i : ι
hI : C ⊆ Xs i
⊢ False
Tactic:
have hC' := subset_inter hI hCss
State after:
case refine_2.refine_1.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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
C : Set α
hCss : C ⊆ ⋃ i, Is i
hC : M.Circuit C
i : ι
hI : C ⊆ Xs i
hC' : C ⊆ Xs i ∩ ⋃ i, Is i
⊢ False

State before:
case refine_2.refine_1.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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
C : Set α
hCss : C ⊆ ⋃ i, Is i
hC : M.Circuit C
i : ι
hI : C ⊆ Xs i
hC' : C ⊆ Xs i ∩ ⋃ i, Is i
⊢ False
Tactic:
rw [h_inter] at hC'
State after:
case refine_2.refine_1.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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
C : Set α
hCss : C ⊆ ⋃ i, Is i
hC : M.Circuit C
i : ι
hI : C ⊆ Xs i
hC' : C ⊆ Is i
⊢ False

State before:
case refine_2.refine_1.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 : α
hXs : ∀ (i : ι), Xs i ⊆ M.E
hdj : Pairwise (Disjoint on Xs)
h : ∀ (C : Set α), M.Circuit C → C ⊆ ⋃ i, Xs i → ∃ i, C ⊆ Xs i
Is : ι → Set α
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
hss : ⋃ i, Is i ⊆ ⋃ i, Xs i
hIe : ⋃ i, Is i ⊆ M.E
h_inter : ∀ (i : ι), Xs i ∩ ⋃ j, Is j = Is i
C : Set α
hCss : C ⊆ ⋃ i, Is i
hC : M.Circuit C
i : ι
hI : C ⊆ Xs i
hC' : C ⊆ Is i
⊢ False
Tactic:
exact hC.dep.not_indep ((hIs i).indep.subset hC')
State after:
no goals