Theorem: Matroid.skew_iff_contract_restrict_eq_restrict (Matroid/Modular.lean)

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
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

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 ?_⟩
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

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
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

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⟩
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

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⟩
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

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
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

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
State after:
no goals

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) ↦ ?_
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

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]
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

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.Indep (J ∪ I) ∧ Disjoint X J ↔ M.Indep J
Tactic:
refine ⟨fun h ↦ h.1.subset subset_union_left,
  fun hJi ↦ ⟨?_, h.disjoint_of_indep_subset_right hJi hJ⟩⟩
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
hJi : M.Indep J
⊢ M.Indep (J ∪ I)

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
hJi : M.Indep J
⊢ M.Indep (J ∪ I)
Tactic:
exact h.symm.union_indep_of_indep_subsets hJi hJ hI.indep hI.subset
State after:
no goals

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✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
⊢ (M ↾ Y).Indep J
Tactic:
exact restrict_indep_iff.2 ⟨hJ.indep, hJ.subset⟩
State after:
no goals

State before:
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)
Tactic:
rw [← h, restrict_indep_iff, hI.contract_eq_contract_delete, delete_indep_iff,
  hI.indep.contract_indep_iff, union_comm] at hi
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 : ((Disjoint J I ∧ M.Indep (I ∪ J)) ∧ Disjoint J (X \ I)) ∧ J ⊆ Y
⊢ M.Indep (I ∪ J)

State before:
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 : ((Disjoint J I ∧ M.Indep (I ∪ J)) ∧ Disjoint J (X \ I)) ∧ J ⊆ Y
⊢ M.Indep (I ∪ J)
Tactic:
exact hi.1.1.2
State after:
no goals