internlm/Lean-Github huggingface dataset:
Theorem: Matroid.skewFamily_iff_exist_bases
Proof state before:
case intro.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 : α
h : M.SkewFamily Xs
B : Set α
hB : M.ModularBase B Xs
⊢ Pairwise (Disjoint on fun i => Xs i ∩ B)
Tactic:
exact h.pairwise_disjoint_of_indep_subsets (fun i ↦ inter_subset_left)
  (fun i ↦ hB.indep.inter_left _)
Proof state after:
no goals
Theorem: Matroid.Indep.skewFamily_iff_pairwise_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 : α
hI : M.Indep (⋃ i, Is i)
⊢ M.SkewFamily Is ↔ Pairwise (Disjoint on Is)
Tactic:
refine ⟨fun h ↦ h.pairwise_disjoint_of_indep_subsets
  (fun _ ↦ Subset.rfl) (fun i ↦ hI.subset (subset_iUnion _ _)),
  fun h ↦ hI.skewFamily_of_disjoint_bases ?_ (fun i ↦ (hI.subset (subset_iUnion _ _)).basis_self)⟩
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 : α
hI : M.Indep (⋃ i, Is i)
h : Pairwise (Disjoint on Is)
⊢ Pairwise (Disjoint on fun i => Is i)
Theorem: Matroid.Indep.skewFamily_iff_pairwise_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 : α
hI : M.Indep (⋃ i, Is i)
h : Pairwise (Disjoint on Is)
⊢ Pairwise (Disjoint on fun i => Is i)
Tactic:
exact h
Proof state after:
no goals
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
⊢ M.Indep (⋃ i, Is i)
Tactic:
choose Js hJs using fun i ↦ (hIs i).subset_basis_of_subset (hIX 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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
⊢ M.Indep (⋃ i, Is i)
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
⊢ M.Indep (⋃ i, Is i)
Tactic:
refine Indep.subset ?_ <| iUnion_mono (fun i ↦ (hJs i).2)
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
⊢ M.Indep (⋃ i, Js i)
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
⊢ M.Indep (⋃ i, Js i)
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis _ (iUnion_subset (fun i ↦ (hJs i).1.indep.subset_ground))
Proof state after:
case 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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
⊢ M.Indep (⋃ i, Js i)
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
Proof state before:
case 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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
⊢ M.Indep (⋃ i, Js i)
Tactic:
by_contra hcon
Proof state after:
case 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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
⊢ False
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
Proof state before:
case 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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
⊢ False
Tactic:
have ex_i : ∃ i e, e ∈ (Js i) \ J := by
  by_contra! h'
  rw [← hJ.subset.antisymm (iUnion_subset fun i e he ↦ by_contra fun heJ ↦ h' i e ⟨he, heJ⟩)]
    at hcon
  exact hcon hJ.indep
Proof state after:
case 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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
ex_i : ∃ i e, e ∈ Js i \ J
⊢ False
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
Proof state before:
case 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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
ex_i : ∃ i e, e ∈ Js i \ J
⊢ False
Tactic:
obtain ⟨i₀, e, hei₀, heJ⟩ := ex_i
Proof state after:
case 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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
⊢ False
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
Proof state before:
case 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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
⊢ False
Tactic:
obtain ⟨Ks, hdj, hKs, huKs⟩ := skewFamily_iff_exist_bases.1 h
Proof state after:
case intro.intro.intro.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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ False
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
Proof state before:
case intro.intro.intro.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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ False
Tactic:
have hssE : Js i₀ ∪ (⋃ i ∈ ({i₀}ᶜ : Set ι), Ks i) ⊆ M.E := by
  refine union_subset (hJs i₀).1.indep.subset_ground ?_
  simp only [mem_compl_iff, mem_singleton_iff, iUnion_subset_iff]
  exact fun i _ ↦ (huKs i).indep.subset_ground
Proof state after:
case intro.intro.intro.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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
⊢ False
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
Proof state before:
case intro.intro.intro.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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
⊢ False
Tactic:
obtain ⟨K', hK', hss⟩ := (hJs i₀).1.indep.subset_basis_of_subset subset_union_left hssE
Proof state after:
case intro.intro.intro.intro.intro.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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
⊢ False
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
Proof state before:
case intro.intro.intro.intro.intro.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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
he' : e ∈ M.cl (K' \ {e})
⊢ False
Tactic:
exact hK'.indep.not_mem_cl_diff_of_mem (hss hei₀) he'
Proof state after:
no goals
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
⊢ ∃ i e, e ∈ Js i \ J
Tactic:
by_contra! 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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
h' : ∀ (i : ι) (e : α), e ∉ Js i \ J
⊢ False
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
h' : ∀ (i : ι) (e : α), e ∉ Js i \ J
⊢ False
Tactic:
rw [← hJ.subset.antisymm (iUnion_subset fun i e he ↦ by_contra fun heJ ↦ h' i e ⟨he, heJ⟩)]
  at 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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep J
h' : ∀ (i : ι) (e : α), e ∉ Js i \ J
⊢ False
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep J
h' : ∀ (i : ι) (e : α), e ∉ Js i \ J
⊢ False
Tactic:
exact hcon hJ.indep
Proof state after:
no goals
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
Tactic:
refine union_subset (hJs i₀).1.indep.subset_ground ?_
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
Tactic:
simp only [mem_compl_iff, mem_singleton_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 : α
h : M.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ ∀ (i : ι), ¬i = i₀ → Ks i ⊆ M.E
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
⊢ ∀ (i : ι), ¬i = i₀ → Ks i ⊆ M.E
Tactic:
exact fun i _ ↦ (huKs i).indep.subset_ground
Proof state after:
no goals
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
⊢ ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
Tactic:
intro i hne f hf
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
⊢ f ∈ K'
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
⊢ f ∈ K'
Tactic:
by_contra hfK'
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
⊢ False
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
⊢ False
Tactic:
apply hKs.indep.not_mem_cl_diff_of_mem (mem_iUnion.2 ⟨i,hf⟩)
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
⊢ f ∈ M.cl ((⋃ i, Ks i) \ {f})
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
⊢ f ∈ M.cl ((⋃ i, Ks i) \ {f})
Tactic:
have hcl : f ∈ M.cl K' := by
  exact hK'.subset_cl (Or.inr <| mem_biUnion hne hf)
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
⊢ f ∈ M.cl ((⋃ i, Ks i) \ {f})
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
⊢ f ∈ M.cl ((⋃ i, Ks i) \ {f})
Tactic:
refine mem_of_mem_of_subset
  (M.cl_subset_cl (subset_diff_singleton hK'.subset hfK') hcl) (M.cl_subset_cl_of_subset_cl ?_)
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.SkewFamily Xs
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
i : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
hcl : f ∈ M.cl K'
⊢ (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i) \ {f} ⊆ M.cl ((⋃ i, Ks i) \ {f})