internlm/Lean-Github huggingface dataset:
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'
⊢ (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i) \ {f} ⊆ M.cl ((⋃ i, Ks i) \ {f})
Tactic:
simp only [mem_compl_iff, mem_singleton_iff, mem_union, mem_iUnion, exists_prop, not_exists,
  diff_singleton_subset_iff, union_subset_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)
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₀ ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f})) ∧ ∀ (i : ι), ¬i = i₀ → Ks i ⊆ insert 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'
⊢ Js i₀ ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f})) ∧ ∀ (i : ι), ¬i = i₀ → Ks i ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f}))
Tactic:
refine ⟨(hJs i₀).1.subset.trans ?_, fun i _ ↦ ?_⟩
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✝ : α
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'
⊢ Xs i₀ ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f}))

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✝ : α
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'
i : ι
x✝ : ¬i = i₀
⊢ Ks i ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f}))
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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✝ : α
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'
i : ι
x✝ : ¬i = i₀
⊢ Ks i ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f}))
Tactic:
refine subset_trans ?_ <|
  insert_subset_insert (M.subset_cl _ (diff_subset.trans hKs.indep.subset_ground))
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✝ : α
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'
i : ι
x✝ : ¬i = i₀
⊢ Ks i ⊆ insert f ((⋃ i, Ks i) \ {f})
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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✝ : α
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'
i : ι
x✝ : ¬i = i₀
⊢ Ks i ⊆ insert f ((⋃ i, Ks i) \ {f})
Tactic:
rw [insert_diff_singleton]
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✝ : α
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'
i : ι
x✝ : ¬i = i₀
⊢ Ks i ⊆ insert f (⋃ i, Ks i)
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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✝ : α
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'
i : ι
x✝ : ¬i = i₀
⊢ Ks i ⊆ insert f (⋃ i, Ks i)
Tactic:
exact (subset_iUnion Ks i).trans (subset_insert _ _)
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 : ι
hne : i ≠ i₀
f : α
hf : f ∈ Ks i
hfK' : f ∉ K'
⊢ f ∈ M.cl K'
Tactic:
exact hK'.subset_cl (Or.inr <| mem_biUnion hne hf)
Proof state after:
no goals
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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✝ : α
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'
⊢ Xs i₀ ⊆ insert f (M.cl ((⋃ i, Ks i) \ {f}))
Tactic:
refine (huKs i₀).subset_cl.trans (subset_trans (M.cl_subset_cl ?_) (subset_insert _ _))
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✝ : α
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'
⊢ Ks i₀ ⊆ (⋃ i, Ks i) \ {f}
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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✝ : α
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'
⊢ Ks i₀ ⊆ (⋃ i, Ks i) \ {f}
Tactic:
refine subset_diff_singleton (subset_iUnion Ks i₀) (fun hf' ↦ ?_)
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✝ : α
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'
hf' : f ∈ Ks i₀
⊢ False
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
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✝ : α
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'
hf' : f ∈ Ks i₀
⊢ False
Tactic:
exact (hdj hne).ne_of_mem hf hf' rfl
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'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
⊢ e ∈ M.cl (K' \ {e})
Tactic:
refine mem_of_mem_of_subset (hJ.subset_cl (mem_iUnion_of_mem _ hei₀)) ?_
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'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
⊢ M.cl J ⊆ M.cl (K' \ {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)
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'
⊢ M.cl J ⊆ M.cl (K' \ {e})
Tactic:
rw [cl_subset_cl_iff_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'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
⊢ J ⊆ M.cl (K' \ {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)
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'
⊢ J ⊆ M.cl (K' \ {e})
Tactic:
rintro 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'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
⊢ f ∈ M.cl (K' \ {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)
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'
f : α
hf : f ∈ J
⊢ f ∈ M.cl (K' \ {e})
Tactic:
obtain ⟨i, hfi⟩ := mem_iUnion.1 (hJ.subset hf)
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)
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'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
⊢ f ∈ M.cl (K' \ {e})
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)
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'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
⊢ f ∈ M.cl (K' \ {e})
Tactic:
obtain (rfl | hi) := eq_or_ne i₀ i
Proof state after:
case intro.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✝ : α
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'
f : α
hf : f ∈ J
hfi : f ∈ Js i₀
⊢ f ∈ M.cl (K' \ {e})

case intro.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✝ : α
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'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
hi : i₀ ≠ i
⊢ f ∈ M.cl (K' \ {e})
Theorem: Matroid.SkewFamily.iUnion_indep_subset_indep
Proof state before:
case intro.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✝ : α
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'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
hi : i₀ ≠ i
⊢ f ∈ M.cl (K' \ {e})
Tactic:
refine mem_of_mem_of_subset ((hJs i).1.subset.trans (huKs i).subset_cl hfi) (M.cl_subset_cl ?_)
Proof state after:
case intro.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✝ : α
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'
f : α
hf : f ∈ J
i : ι
hfi : f ∈ Js i
hi : i₀ ≠ i
⊢ Ks i ⊆ K' \ {e}