internlm/Lean-Github huggingface dataset:
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
⊢ X ∩ Y ⊆ M.cl ∅
Tactic:
refine (inter_subset_inter hI.subset_cl hJ.subset_cl).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 : α
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
⊢ M.cl I ∩ M.cl J ⊆ 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
⊢ M.cl I ∩ M.cl J ⊆ M.cl ∅
Tactic:
rw [← hu.cl_inter_eq_inter_cl, hdj.inter_eq]
Proof state after:
no goals
Theorem: Matroid.skew_iff_exist_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 : α
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
Tactic:
rw [disjoint_iff_forall_ne]
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 ∅
⊢ ∀ ⦃a : α⦄, a ∈ I → ∀ ⦃b : α⦄, b ∈ J → a ≠ b
Theorem: Matroid.skew_iff_exist_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 : α
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 ∅
⊢ ∀ ⦃a : α⦄, a ∈ I → ∀ ⦃b : α⦄, b ∈ J → a ≠ b
Tactic:
rintro e heI _ heJ 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 : α
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 ∅
e : α
heI : e ∈ I
heJ : e ∈ J
⊢ False
Theorem: Matroid.skew_iff_exist_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 : α
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 ∅
e : α
heI : e ∈ I
heJ : e ∈ J
⊢ False
Tactic:
exact (hI.indep.nonloop_of_mem heI).not_loop (h ⟨hJ.subset heJ, hI.subset heI⟩)
Proof state after:
no goals
Theorem: Matroid.Skew.disjoint_of_indep_subset_left
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
hI : M.Indep I
hIX : I ⊆ X
⊢ true ≠ false
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Skew.disjoint_of_indep_subset_right
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
hJ : M.Indep J
hJY : J ⊆ Y
⊢ false ≠ true
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Skew.diff_loops_disjoint_left
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
⊢ Disjoint (X \ M.cl ∅) Y
Tactic:
rw [disjoint_iff_inter_eq_empty, ← inter_diff_right_comm, diff_eq_empty]
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.Skew X Y
⊢ X ∩ Y ⊆ M.cl ∅
Theorem: Matroid.Skew.diff_loops_disjoint_left
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
⊢ X ∩ Y ⊆ M.cl ∅
Tactic:
exact h.inter_subset_loops
Proof state after:
no goals
Theorem: Matroid.Skew.mono
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
hX : X' ⊆ X
hY : Y' ⊆ Y
⊢ (fun i => bif i then X' else Y') false ⊆ bif false then X else Y
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Skew.mono
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
hX : X' ⊆ X
hY : Y' ⊆ Y
⊢ (fun i => bif i then X' else Y') true ⊆ bif true then X else Y
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Skew.cl_skew
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 (M.cl X) (M.cl Y)
Tactic:
have h' := SkewFamily.cls_skewFamily 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.Skew X Y
h' : M.SkewFamily fun i => M.cl (bif i then X else Y)
⊢ M.Skew (M.cl X) (M.cl Y)
Theorem: Matroid.Skew.cl_skew
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
h' : M.SkewFamily fun i => M.cl (bif i then X else Y)
⊢ M.Skew (M.cl X) (M.cl Y)
Tactic:
simp_rw [Bool.cond_eq_ite, apply_ite, ← Bool.cond_eq_ite] 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.Skew X Y
h' : M.SkewFamily fun i => bif i then M.cl X else M.cl Y
⊢ M.Skew (M.cl X) (M.cl Y)
Theorem: Matroid.Skew.cl_skew
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
h' : M.SkewFamily fun i => bif i then M.cl X else M.cl Y
⊢ M.Skew (M.cl X) (M.cl Y)
Tactic:
exact h'
Proof state after:
no goals
Theorem: Matroid.skew_iff_cl_skew_left
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.Skew X Y ↔ M.Skew (M.cl X) Y
Tactic:
by_cases hY : Y ⊆ M.E
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : Y ⊆ M.E
⊢ M.Skew X Y ↔ M.Skew (M.cl X) Y

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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : ¬Y ⊆ M.E
⊢ M.Skew X Y ↔ M.Skew (M.cl X) Y
Theorem: Matroid.skew_iff_cl_skew_left
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : ¬Y ⊆ M.E
⊢ M.Skew X Y ↔ M.Skew (M.cl X) Y
Tactic:
exact iff_of_false (fun h ↦ hY <| h.subset_ground_right) (fun h ↦ hY <| h.subset_ground_right)
Proof state after:
no goals
Theorem: Matroid.skew_iff_cl_skew_left
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : Y ⊆ M.E
⊢ M.Skew X Y ↔ M.Skew (M.cl X) Y
Tactic:
rw [skew_iff_cl_skew, iff_comm, skew_iff_cl_skew, cl_cl]
Proof state after:
no goals
Theorem: Matroid.skew_iff_cl_skew_right
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 : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.Skew X Y ↔ M.Skew X (M.cl Y)
Tactic:
rw [skew_comm, skew_iff_cl_skew_left, skew_comm]
Proof state after:
no goals
Theorem: Matroid.skew_iff_of_loopEquiv
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 : α
hX : M.LoopEquiv X X'
hY : M.LoopEquiv Y Y'
⊢ M.Skew X Y ↔ M.Skew X' Y'
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
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 : α
hX : M.LoopEquiv X X'
hY : M.LoopEquiv Y Y'
h : M.Skew X Y
⊢ M.Skew X' Y'

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 : α
hX : M.LoopEquiv X X'
hY : M.LoopEquiv Y Y'
h : M.Skew X' Y'
⊢ M.Skew X Y
Theorem: Matroid.skew_iff_of_loopEquiv
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 : α
hX : M.LoopEquiv X X'
hY : M.LoopEquiv Y Y'
h : M.Skew X' Y'
⊢ M.Skew X Y
Tactic:
rwa [skew_iff_cl_skew hX.symm.subset_ground hY.symm.subset_ground, hX.cl_eq_cl, hY.cl_eq_cl,
    ← skew_iff_cl_skew]
Proof state after:
no goals
Theorem: Matroid.skew_iff_of_loopEquiv
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 : α
hX : M.LoopEquiv X X'
hY : M.LoopEquiv Y Y'
h : M.Skew X Y
⊢ M.Skew X' Y'
Tactic:
rwa [skew_iff_cl_skew hX.subset_ground hY.subset_ground, ← hX.cl_eq_cl, ← hY.cl_eq_cl,
  ← skew_iff_cl_skew]
Proof state after:
no goals
Theorem: Matroid.Skew.union_indep_of_indep_subsets
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
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ M.Indep (I ∪ J)
Tactic:
rw [union_eq_iUnion]
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.Skew X Y
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ M.Indep (⋃ b, bif b then I else J)
Theorem: Matroid.Skew.union_indep_of_indep_subsets
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
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ M.Indep (⋃ b, bif b then I else J)
Tactic:
exact SkewFamily.iUnion_indep_subset_indep h (Is := fun i ↦ bif i then I else J)
  (Bool.rec (by simpa) (by simpa)) (Bool.rec (by simpa) (by simpa))
Proof state after:
no goals
Theorem: Matroid.Skew.union_indep_of_indep_subsets
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
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ (fun i => bif i then I else J) false ⊆ bif false then X else Y
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Skew.union_indep_of_indep_subsets
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
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ (fun i => bif i then I else J) true ⊆ bif true then X else Y
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Skew.union_indep_of_indep_subsets
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
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ M.Indep ((fun i => bif i then I else J) false)
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Skew.union_indep_of_indep_subsets
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
hI : M.Indep I
hIX : I ⊆ X
hJ : M.Indep J
hJY : J ⊆ Y
⊢ M.Indep ((fun i => bif i then I else J) true)
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Skew.union_basis_union
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
hI : M.Basis I X
hJ : M.Basis J Y
⊢ M.Basis (I ∪ J) (X ∪ Y)
Tactic:
rw [union_eq_iUnion, union_eq_iUnion]
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.Skew X Y
hI : M.Basis I X
hJ : M.Basis J Y
⊢ M.Basis (⋃ b, bif b then I else J) (⋃ b, bif b then X else Y)
Theorem: Matroid.Skew.union_basis_union
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
hI : M.Basis I X
hJ : M.Basis J Y
⊢ M.Basis (⋃ b, bif b then I else J) (⋃ b, bif b then X else Y)
Tactic:
exact SkewFamily.iUnion_basis_iUnion h (Bool.rec (by simpa) (by simpa))
Proof state after:
no goals
Theorem: Matroid.Skew.union_basis_union
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
hI : M.Basis I X
hJ : M.Basis J Y
⊢ M.Basis (bif false then I else J) (bif false then X else Y)
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Skew.union_basis_union
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
hI : M.Basis I X
hJ : M.Basis J Y
⊢ M.Basis (bif true then I else J) (bif true then X else Y)
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Indep.skew_iff_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 : α
h : M.Indep (I ∪ J)
⊢ M.Skew I J ↔ Disjoint I J
Tactic:
rw [← pairwise_disjoint_on_bool, Skew, Indep.skewFamily_iff_pairwise_disjoint]
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.Indep (I ∪ J)
⊢ M.Indep (⋃ i, bif i then I else J)
Theorem: Matroid.Indep.skew_iff_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 : α
h : M.Indep (I ∪ J)
⊢ M.Indep (⋃ i, bif i then I else J)
Tactic:
rwa [union_eq_iUnion] at h
Proof state after:
no goals
Theorem: Matroid.Indep.skew_iff_disjoint_union_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 : α
hI : M.Indep I
hJ : M.Indep J
⊢ M.Skew I J ↔ Disjoint I J ∧ M.Indep (I ∪ J)
Tactic:
refine ⟨fun h ↦ ⟨h.disjoint_of_indep_left hI, ?_⟩, fun h ↦ h.2.skew_iff_disjoint.2 h.1⟩
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
hJ : M.Indep J
h : M.Skew I J
⊢ M.Indep (I ∪ J)
Theorem: Matroid.Indep.skew_iff_disjoint_union_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 : α
hI : M.Indep I
hJ : M.Indep J
h : M.Skew I J
⊢ M.Indep (I ∪ J)
Tactic:
exact h.union_indep_of_indep_subsets hI Subset.rfl hJ Subset.rfl
Proof state after:
no goals
Theorem: Matroid.Indep.subset_skew_diff
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.Indep I
hJI : J ⊆ I
⊢ M.Skew J (I \ J)
Tactic:
rw [Indep.skew_iff_disjoint]
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.Indep I
hJI : J ⊆ I
⊢ Disjoint J (I \ J)

ι : 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.Indep I
hJI : J ⊆ I
⊢ M.Indep (J ∪ I \ J)
Theorem: Matroid.Indep.subset_skew_diff
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.Indep I
hJI : J ⊆ I
⊢ M.Indep (J ∪ I \ J)
Tactic:
exact h.subset (union_subset hJI diff_subset)
Proof state after:
no goals
Theorem: Matroid.Indep.subset_skew_diff
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.Indep I
hJI : J ⊆ I
⊢ Disjoint J (I \ J)
Tactic:
exact disjoint_sdiff_right
Proof state after:
no goals
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.Skew X Y ↔ M ／ X ↾ Y = M ↾ Y
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis X
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ M.Skew X Y ↔ M ／ X ↾ Y = M ↾ Y
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
⊢ M.Skew X Y ↔ M ／ X ↾ Y = M ↾ Y
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ skew_iff_exist_bases.2 ?_⟩
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M.Skew X Y
⊢ M ／ X ↾ Y = M ↾ Y

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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
⊢ ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
⊢ ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis Y
Proof state after:
case intro.refine_2.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
⊢ ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
Proof state before:
case intro.refine_2.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
⊢ ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Tactic:
have hi : (M ↾ Y).Indep J := by
  exact restrict_indep_iff.2 ⟨hJ.indep, hJ.subset⟩
Proof state after:
case intro.refine_2.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
hi : (M ↾ Y).Indep J
⊢ ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
Proof state before:
case intro.refine_2.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
hi : (M ↾ Y).Indep J
⊢ ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Tactic:
refine ⟨I, J, ?_, ?_, hI, hJ⟩
Proof state after:
case intro.refine_2.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
hi : (M ↾ Y).Indep J
⊢ M.Indep (I ∪ J)

case intro.refine_2.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
hi : (M ↾ Y).Indep J
⊢ Disjoint I J
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
Proof state before:
case intro.refine_2.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
hi : (M ↾ Y).Indep J
⊢ Disjoint I J
Tactic:
rw [← h, restrict_indep_iff, hI.contract_indep_iff] at hi
Proof state after:
case intro.refine_2.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
hi : (M.Indep (J ∪ I) ∧ Disjoint X J) ∧ J ⊆ Y
⊢ Disjoint I J
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
Proof state before:
case intro.refine_2.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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
hi : (M.Indep (J ∪ I) ∧ Disjoint X J) ∧ J ⊆ Y
⊢ Disjoint I J
Tactic:
exact hi.1.2.mono_left hI.subset
Proof state after:
no goals
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M.Skew X Y
⊢ M ／ X ↾ Y = M ↾ Y
Tactic:
refine eq_of_indep_iff_indep_forall rfl fun J (hJ : J ⊆ Y) ↦ ?_
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M.Skew X Y
J : Set α
hJ : J ⊆ Y
⊢ (M ／ X ↾ Y).Indep J ↔ (M ↾ Y).Indep J
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M.Skew X Y
J : Set α
hJ : J ⊆ Y
⊢ (M ／ X ↾ Y).Indep J ↔ (M ↾ Y).Indep J
Tactic:
simp_rw [restrict_indep_iff, hI.contract_indep_iff, and_iff_left hJ]
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M.Skew X Y
J : Set α
hJ : J ⊆ Y
⊢ M.Indep (J ∪ I) ∧ Disjoint X J ↔ M.Indep J