internlm/Lean-Github huggingface dataset:
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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)
Proof state after:
no goals
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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]
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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]
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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⟩
Proof state after:
no goals
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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 ?_
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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 ?_
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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]
Proof state after:
no goals
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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)]
Proof state after:
no goals
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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]
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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)⟩
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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]
Proof state after:
no goals
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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
Proof state after:
no goals
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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]
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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)
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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'
Proof 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
Theorem: Matroid.skewFamily_iff_forall_circuit
Proof 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')
Proof state after:
no goals
Theorem: Matroid.skew_iff_modularPair_inter_subset_loops
Proof 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 : α
⊢ M.Skew X Y ↔ M.ModularPair X Y ∧ X ∩ Y ⊆ M.cl ∅
Tactic:
rw [Skew, SkewFamily, ModularPair, and_congr_right_iff]
Proof 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 : α
⊢ (M.ModularFamily fun i => bif i then X else Y) →
    ((∀ ⦃i j : Bool⦄, i ≠ j → ((bif i then X else Y) ∩ bif j then X else Y) ⊆ M.cl ∅) ↔ X ∩ Y ⊆ M.cl ∅)
Theorem: Matroid.skew_iff_modularPair_inter_subset_loops
Proof 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 : α
⊢ (M.ModularFamily fun i => bif i then X else Y) →
    ((∀ ⦃i j : Bool⦄, i ≠ j → ((bif i then X else Y) ∩ bif j then X else Y) ⊆ M.cl ∅) ↔ X ∩ Y ⊆ M.cl ∅)
Tactic:
simp [inter_comm X Y]
Proof state after:
no goals
Theorem: Matroid.Skew.disjoint
Proof 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✝ : M.Loopless
h : M.Skew X Y
⊢ Disjoint X Y
Tactic:
rw [disjoint_iff_inter_eq_empty, ← subset_empty_iff]
Proof 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 : α
inst✝ : M.Loopless
h : M.Skew X Y
⊢ X ∩ Y ⊆ ∅
Theorem: Matroid.Skew.disjoint
Proof 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✝ : M.Loopless
h : M.Skew X Y
⊢ X ∩ Y ⊆ ∅
Tactic:
simpa using h.inter_subset_loops
Proof state after:
no goals
Theorem: Matroid.Skew.symm
Proof 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
⊢ M.Skew Y X
Tactic:
rw [skew_iff_modularPair_inter_subset_loops] at h ⊢
Proof 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.ModularPair X Y ∧ X ∩ Y ⊆ M.cl ∅
⊢ M.ModularPair Y X ∧ Y ∩ X ⊆ M.cl ∅
Theorem: Matroid.Skew.symm
Proof 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.ModularPair X Y ∧ X ∩ Y ⊆ M.cl ∅
⊢ M.ModularPair Y X ∧ Y ∩ X ⊆ M.cl ∅
Tactic:
rwa [inter_comm, ModularPair.comm]
Proof state after:
no goals
Theorem: Matroid.skew_iff_exist_bases
Proof 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 : α
X Y : Set α
⊢ M.Skew X Y ↔ ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Tactic:
change (M.ModularPair X Y ∧ _) ↔ _
Proof 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 : α
X Y : Set α
⊢ (M.ModularPair X Y ∧
      ∀ ⦃i j : Bool⦄, i ≠ j → (fun i => bif i then X else Y) i ∩ (fun i => bif i then X else Y) j ⊆ M.cl ∅) ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Theorem: Matroid.skew_iff_exist_bases
Proof 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 : α
X Y : Set α
⊢ (M.ModularPair X Y ∧
      ∀ ⦃i j : Bool⦄, i ≠ j → (fun i => bif i then X else Y) i ∩ (fun i => bif i then X else Y) j ⊆ M.cl ∅) ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Tactic:
rw [modularPair_iff_exists_basis_basis]
Proof 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 : α
X Y : Set α
⊢ ((∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)) ∧
      ∀ ⦃i j : Bool⦄, i ≠ j → (fun i => bif i then X else Y) i ∩ (fun i => bif i then X else Y) j ⊆ M.cl ∅) ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Theorem: Matroid.skew_iff_exist_bases
Proof 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 : α
X Y : Set α
⊢ ((∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)) ∧
      ∀ ⦃i j : Bool⦄, i ≠ j → (fun i => bif i then X else Y) i ∩ (fun i => bif i then X else Y) j ⊆ M.cl ∅) ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Tactic:
simp only [exists_and_left, ne_eq, Bool.forall_bool, Bool.not_eq_false, cond_false,
  Bool.not_eq_true, cond_true, inter_self, IsEmpty.forall_iff, forall_true_left, true_and,
  and_true]
Proof 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 : α
X Y : Set α
⊢ (∃ I, M.Basis I X ∧ ∃ x, M.Basis x Y ∧ M.Indep (I ∪ x)) ∧ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅ ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Theorem: Matroid.skew_iff_exist_bases
Proof 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 : α
X Y : Set α
⊢ (∃ I, M.Basis I X ∧ ∃ x, M.Basis x Y ∧ M.Indep (I ∪ x)) ∧ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅ ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Tactic:
refine ⟨fun ⟨⟨I, hI, J, hJ, hIJ⟩, h, _⟩ ↦ ⟨I, J, hIJ, ?_, hI, hJ⟩,
  fun ⟨I, J, hu, hdj, hI, hJ⟩ ↦ ⟨⟨I,hI,J,hJ,hu⟩  , ?_⟩ ⟩
Proof 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 : α
X Y : Set α
x✝ : (∃ I, M.Basis I X ∧ ∃ x, M.Basis x Y ∧ M.Indep (I ∪ x)) ∧ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J Y
hIJ : M.Indep (I ∪ J)
h : Y ∩ X ⊆ M.cl ∅
right✝ : X ∩ Y ⊆ M.cl ∅
⊢ Disjoint I J

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 : α
X Y : Set α
x✝ : ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
I J : Set α
hu : M.Indep (I ∪ J)
hdj : Disjoint I J
hI : M.Basis I X
hJ : M.Basis J Y
⊢ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅
Theorem: Matroid.skew_iff_exist_bases
Proof 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 : α
X Y : Set α
x✝ : ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
I J : Set α
hu : M.Indep (I ∪ J)
hdj : Disjoint I J
hI : M.Basis I X
hJ : M.Basis J Y
⊢ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅
Tactic:
rw [inter_comm, and_self]
Proof 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 : α
X Y : Set α
x✝ : ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
I J : Set α
hu : M.Indep (I ∪ J)
hdj : Disjoint I J
hI : M.Basis I X
hJ : M.Basis J Y
⊢ X ∩ Y ⊆ M.cl ∅