internlm/Lean-Github huggingface dataset:
Theorem: Matroid.modularSet_iff_cl
Proof state before:
case refine_1.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 : α
M : Matroid α
X : Set α
h : ∀ ⦃F : Set α⦄, M.Flat F → ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
F : Set α
hF : M.Flat F
I : Set α
hI : M.Indep I
hI' : M.Basis (X ∩ I) X ∧ M.Basis (F ∩ I) F
⊢ X ⊆ M.cl (X ∩ I) ∧ F ⊆ M.cl (F ∩ I)
Tactic:
rwa [← hI.inter_basis_cl_iff_subset_cl_inter, ← hI.inter_basis_cl_iff_subset_cl_inter]
Proof state after:
no goals
Theorem: Matroid.modularSet_singleton
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 : Matroid α
he : e ∈ M.E
⊢ M.ModularSet {e}
Tactic:
refine modularSet_def.2 fun 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 : α
M : Matroid α
he : e ∈ M.E
F : Set α
hF : M.Flat F
⊢ M.ModularPair {e} F
Theorem: Matroid.modularSet_singleton
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 : Matroid α
he : e ∈ M.E
F : Set α
hF : M.Flat F
⊢ M.ModularPair {e} F
Tactic:
by_cases heF : {e} ⊆ F
Proof state after:
case pos
ι : 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 : Matroid α
he : e ∈ M.E
F : Set α
hF : M.Flat F
heF : {e} ⊆ F
⊢ M.ModularPair {e} F

case neg
ι : 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 : Matroid α
he : e ∈ M.E
F : Set α
hF : M.Flat F
heF : ¬{e} ⊆ F
⊢ M.ModularPair {e} F
Theorem: Matroid.modularSet_singleton
Proof state before:
case neg
ι : 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 : Matroid α
he : e ∈ M.E
F : Set α
hF : M.Flat F
heF : ¬{e} ⊆ F
⊢ M.ModularPair {e} F
Tactic:
rw [singleton_subset_iff, ← hF.cl] at heF
Proof state after:
case neg
ι : 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 : Matroid α
he : e ∈ M.E
F : Set α
hF : M.Flat F
heF : e ∉ M.cl F
⊢ M.ModularPair {e} F
Theorem: Matroid.modularSet_singleton
Proof state before:
case neg
ι : 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 : Matroid α
he : e ∈ M.E
F : Set α
hF : M.Flat F
heF : e ∉ M.cl F
⊢ M.ModularPair {e} F
Tactic:
exact modularPair_singleton he hF.subset_ground heF
Proof state after:
no goals
Theorem: Matroid.modularSet_singleton
Proof state before:
case pos
ι : 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 : Matroid α
he : e ∈ M.E
F : Set α
hF : M.Flat F
heF : {e} ⊆ F
⊢ M.ModularPair {e} F
Tactic:
apply modularPair_of_subset heF hF.subset_ground
Proof state after:
no goals
Theorem: Matroid.ModularSet.Flat
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.Simple
hF : M.ModularSet F
⊢ M.Flat F
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 : α
inst✝ : M.Simple
hF : M.ModularSet F
h : ¬M.Flat F
⊢ False
Theorem: Matroid.ModularSet.Flat
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.Simple
hF : M.ModularSet F
h : ¬M.Flat F
⊢ False
Tactic:
obtain ⟨e, heF, he⟩ := exists_mem_cl_not_mem_of_not_flat h
Proof state after:
case 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 : α
inst✝ : M.Simple
hF : M.ModularSet F
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
⊢ False
Theorem: Matroid.ModularSet.Flat
Proof state before:
case 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 : α
inst✝ : M.Simple
hF : M.ModularSet F
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
⊢ False
Tactic:
rw [modularSet_iff] at hF
Proof state after:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
⊢ False
Theorem: Matroid.ModularSet.Flat
Proof state before:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
⊢ False
Tactic:
obtain ⟨I, hI, hIF, hIe⟩ := hF (M.cl_flat {e})
Proof state after:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
⊢ False
Theorem: Matroid.ModularSet.Flat
Proof state before:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
⊢ False
Tactic:
have heM := M.cl_subset_ground F heF
Proof state after:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
⊢ False
Theorem: Matroid.ModularSet.Flat
Proof state before:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
⊢ False
Tactic:
have heI : e ∈ I := by
  rw [hI.inter_basis_cl_iff_subset_cl_inter, cl_singleton_eq,
    cl_eq_self_of_subset_singleton heM inter_subset_left] at hIe
  simpa using hIe
Proof state after:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ False
Theorem: Matroid.ModularSet.Flat
Proof state before:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ False
Tactic:
apply hI.not_mem_cl_diff_of_mem heI
Proof state after:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ e ∈ M.cl (I \ {e})
Theorem: Matroid.ModularSet.Flat
Proof state before:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ e ∈ M.cl (I \ {e})
Tactic:
apply mem_of_mem_of_subset <| M.cl_subset_cl_of_subset_cl hIF.subset_cl heF
Proof state after:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ M.cl (F ∩ I) ⊆ M.cl (I \ {e})
Theorem: Matroid.ModularSet.Flat
Proof state before:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ M.cl (F ∩ I) ⊆ M.cl (I \ {e})
Tactic:
apply M.cl_subset_cl
Proof state after:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ F ∩ I ⊆ I \ {e}
Theorem: Matroid.ModularSet.Flat
Proof state before:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ F ∩ I ⊆ I \ {e}
Tactic:
rw [subset_diff, and_iff_right inter_subset_right, disjoint_singleton_right]
Proof state after:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ e ∉ F ∩ I
Theorem: Matroid.ModularSet.Flat
Proof state before:
case 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 : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ e ∉ F ∩ I
Tactic:
exact fun he' ↦ he <| inter_subset_left he'
Proof state after:
no goals
Theorem: Matroid.ModularSet.Flat
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.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
⊢ e ∈ I
Tactic:
rw [hI.inter_basis_cl_iff_subset_cl_inter, cl_singleton_eq,
  cl_eq_self_of_subset_singleton heM inter_subset_left] at hIe
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.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : {e} ⊆ {e} ∩ I
heM : e ∈ M.E
⊢ e ∈ I
Theorem: Matroid.ModularSet.Flat
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.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : {e} ⊆ {e} ∩ I
heM : e ∈ M.E
⊢ e ∈ I
Tactic:
simpa using hIe
Proof state after:
no goals
Theorem: Matroid.SkewFamily.disjoint_inter_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
hI : M.Indep I
hij : i ≠ j
⊢ Disjoint (Xs i ∩ I) (Xs j)
Tactic:
rw [disjoint_iff_forall_ne]
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
hI : M.Indep I
hij : i ≠ j
⊢ ∀ ⦃a : α⦄, a ∈ Xs i ∩ I → ∀ ⦃b : α⦄, b ∈ Xs j → a ≠ b
Theorem: Matroid.SkewFamily.disjoint_inter_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
hI : M.Indep I
hij : i ≠ j
⊢ ∀ ⦃a : α⦄, a ∈ Xs i ∩ I → ∀ ⦃b : α⦄, b ∈ Xs j → a ≠ b
Tactic:
rintro e ⟨hei, heI⟩ _ hej rfl
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
hI : M.Indep I
hij : i ≠ j
e : α
hei : e ∈ Xs i
heI : e ∈ I
hej : e ∈ Xs j
⊢ False
Theorem: Matroid.SkewFamily.disjoint_inter_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
hI : M.Indep I
hij : i ≠ j
e : α
hei : e ∈ Xs i
heI : e ∈ I
hej : e ∈ Xs j
⊢ False
Tactic:
exact (hI.nonloop_of_mem heI).not_loop <| h.loop_of_mem_inter hij ⟨hei,hej⟩
Proof state after:
no goals
Theorem: Matroid.SkewFamily.disjoint_of_indep_subset
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
hI : M.Indep I
hIX : I ⊆ Xs i
hij : i ≠ j
⊢ Disjoint I (Xs j)
Tactic:
have hdj := h.disjoint_inter_indep hI hij
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
hI : M.Indep I
hIX : I ⊆ Xs i
hij : i ≠ j
hdj : Disjoint (Xs i ∩ I) (Xs j)
⊢ Disjoint I (Xs j)
Theorem: Matroid.SkewFamily.disjoint_of_indep_subset
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
hI : M.Indep I
hIX : I ⊆ Xs i
hij : i ≠ j
hdj : Disjoint (Xs i ∩ I) (Xs j)
⊢ Disjoint I (Xs j)
Tactic:
rwa [inter_eq_self_of_subset_right hIX] at hdj
Proof state after:
no goals
Theorem: Matroid.SkewFamily.cls_skewFamily
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
⊢ M.SkewFamily fun i => M.cl (Xs i)
Tactic:
refine ⟨h.modularFamily.cls_modularFamily, fun i j hij ↦ ?_⟩
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
i j : ι
hij : i ≠ j
⊢ (fun i => M.cl (Xs i)) i ∩ (fun i => M.cl (Xs i)) j ⊆ M.cl ∅
Theorem: Matroid.SkewFamily.cls_skewFamily
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
i j : ι
hij : i ≠ j
⊢ (fun i => M.cl (Xs i)) i ∩ (fun i => M.cl (Xs i)) j ⊆ M.cl ∅
Tactic:
have := M.cl_subset_cl_of_subset_cl <| h.subset_loops_of_ne hij
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
i j : ι
hij : i ≠ j
this : M.cl (Xs i ∩ Xs j) ⊆ M.cl ∅
⊢ (fun i => M.cl (Xs i)) i ∩ (fun i => M.cl (Xs i)) j ⊆ M.cl ∅
Theorem: Matroid.SkewFamily.cls_skewFamily
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
i j : ι
hij : i ≠ j
this : M.cl (Xs i ∩ Xs j) ⊆ M.cl ∅
⊢ (fun i => M.cl (Xs i)) i ∩ (fun i => M.cl (Xs i)) j ⊆ M.cl ∅
Tactic:
rwa [← (h.modularFamily.modularPair i j).inter_cl_eq]
Proof state after:
no goals
Theorem: Matroid.Indep.skewFamily_of_disjoint_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 : α
hI : M.Indep (⋃ i, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
⊢ M.SkewFamily Xs
Tactic:
refine ⟨hI.modularFamily fun i ↦ ?_, fun i j hij ↦ ?_⟩
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 : α
hI : M.Indep (⋃ i, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i : ι
⊢ M.Basis (Xs i ∩ ⋃ i, Is i) (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 : α
hI : M.Indep (⋃ i, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i j : ι
hij : i ≠ j
⊢ Xs i ∩ Xs j ⊆ M.cl ∅
Theorem: Matroid.Indep.skewFamily_of_disjoint_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 : α
hI : M.Indep (⋃ i, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i j : ι
hij : i ≠ j
⊢ Xs i ∩ Xs j ⊆ M.cl ∅
Tactic:
refine (inter_subset_inter (M.subset_cl _ (hIs i).subset_ground)
  (M.subset_cl _ (hIs j).subset_ground)).trans ?_
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 : α
hI : M.Indep (⋃ i, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i j : ι
hij : i ≠ j
⊢ M.cl (Xs i) ∩ M.cl (Xs j) ⊆ M.cl ∅
Theorem: Matroid.Indep.skewFamily_of_disjoint_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 : α
hI : M.Indep (⋃ i, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i j : ι
hij : i ≠ j
⊢ M.cl (Xs i) ∩ M.cl (Xs j) ⊆ M.cl ∅
Tactic:
rw [← (hIs i).cl_eq_cl, ← (hIs j).cl_eq_cl, ← (hI.subset _).cl_inter_eq_inter_cl,
  Disjoint.inter_eq <| hdj hij]
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)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i j : ι
hij : i ≠ j
⊢ Is i ∪ Is j ⊆ ⋃ i, Is i
Theorem: Matroid.Indep.skewFamily_of_disjoint_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 : α
hI : M.Indep (⋃ i, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i j : ι
hij : i ≠ j
⊢ Is i ∪ Is j ⊆ ⋃ i, Is i
Tactic:
exact union_subset (subset_iUnion _ _) (subset_iUnion _ _)
Proof state after:
no goals
Theorem: Matroid.Indep.skewFamily_of_disjoint_bases
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 : α
hI : M.Indep (⋃ i, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i : ι
⊢ M.Basis (Xs i ∩ ⋃ i, Is i) (Xs i)
Tactic:
rw [hI.inter_basis_cl_iff_subset_cl_inter]
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 : α
hI : M.Indep (⋃ i, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i : ι
⊢ Xs i ⊆ M.cl (Xs i ∩ ⋃ i, Is i)
Theorem: Matroid.Indep.skewFamily_of_disjoint_bases
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 : α
hI : M.Indep (⋃ i, Is i)
hdj : Pairwise (Disjoint on Is)
hIs : ∀ (i : ι), M.Basis (Is i) (Xs i)
i : ι
⊢ Xs i ⊆ M.cl (Xs i ∩ ⋃ i, Is i)
Tactic:
exact (hIs i).subset_cl.trans (M.cl_subset_cl (subset_inter (hIs i).subset (subset_iUnion _ i)))
Proof state after:
no goals
Theorem: Matroid.skewFamily_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 : α
⊢ M.SkewFamily Xs ↔ ∃ Is, Pairwise (Disjoint on Is) ∧ M.Basis (⋃ i, Is i) (⋃ i, Xs i) ∧ ∀ (i : ι), M.Basis (Is i) (Xs i)
Tactic:
refine ⟨fun h ↦ ?_, fun ⟨Is, hdj, hIs, hb⟩ ↦ hIs.indep.skewFamily_of_disjoint_bases hdj hb⟩
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
⊢ ∃ Is, Pairwise (Disjoint on Is) ∧ M.Basis (⋃ i, Is i) (⋃ i, Xs i) ∧ ∀ (i : ι), M.Basis (Is i) (Xs i)
Theorem: Matroid.skewFamily_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 : α
h : M.SkewFamily Xs
⊢ ∃ Is, Pairwise (Disjoint on Is) ∧ M.Basis (⋃ i, Is i) (⋃ i, Xs i) ∧ ∀ (i : ι), M.Basis (Is i) (Xs i)
Tactic:
obtain ⟨B, hB⟩ := h.modularFamily
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
B : Set α
hB : M.ModularBase B Xs
⊢ ∃ Is, Pairwise (Disjoint on Is) ∧ M.Basis (⋃ i, Is i) (⋃ i, Xs i) ∧ ∀ (i : ι), M.Basis (Is i) (Xs i)
Theorem: Matroid.skewFamily_iff_exist_bases
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
B : Set α
hB : M.ModularBase B Xs
⊢ ∃ Is, Pairwise (Disjoint on Is) ∧ M.Basis (⋃ i, Is i) (⋃ i, Xs i) ∧ ∀ (i : ι), M.Basis (Is i) (Xs i)
Tactic:
refine ⟨_, ?_, ?_, hB.basis_inter⟩
Proof state after:
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)

case intro.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
B : Set α
hB : M.ModularBase B Xs
⊢ M.Basis (⋃ i, Xs i ∩ B) (⋃ i, Xs i)
Theorem: Matroid.skewFamily_iff_exist_bases
Proof state before:
case intro.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
B : Set α
hB : M.ModularBase B Xs
⊢ M.Basis (⋃ i, Xs i ∩ B) (⋃ i, Xs i)
Tactic:
rw [← iUnion_inter]
Proof state after:
case intro.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
B : Set α
hB : M.ModularBase B Xs
⊢ M.Basis ((⋃ i, Xs i) ∩ B) (⋃ i, Xs i)
Theorem: Matroid.skewFamily_iff_exist_bases
Proof state before:
case intro.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
B : Set α
hB : M.ModularBase B Xs
⊢ M.Basis ((⋃ i, Xs i) ∩ B) (⋃ i, Xs i)
Tactic:
exact hB.basis_iUnion
Proof state after:
no goals