Theorem: Matroid.Basis.contract_basis_union_union (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint (J ∪ X) I
⊢ (M ／ I).Basis J X
Tactic:
rw [disjoint_union_left] at hdj
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
⊢ (M ／ I).Basis J X

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
⊢ (M ／ I).Basis J X
Tactic:
have hI := h.indep.subset subset_union_right
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
⊢ (M ／ I).Basis J X

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
⊢ (M ／ I).Basis J X
Tactic:
simp_rw [Basis, mem_maximals_setOf_iff, hI.contract_indep_iff, and_iff_right hdj.1,
  and_iff_right h.indep, contract_ground, subset_diff, and_iff_left hdj.2,
  and_iff_left (subset_union_left.trans h.subset_ground), and_imp,
  and_iff_right
    (Disjoint.subset_left_of_subset_union (subset_union_left.trans h.subset) hdj.1)]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
⊢ ∀ ⦃y : Set α⦄, Disjoint y I → M.Indep (y ∪ I) → y ⊆ X → J ⊆ y → J = y

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
⊢ ∀ ⦃y : Set α⦄, Disjoint y I → M.Indep (y ∪ I) → y ⊆ X → J ⊆ y → J = y
Tactic:
intro Y hYI hYi hYX hJY
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y✝ Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
⊢ J = Y

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y✝ Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
⊢ J = Y
Tactic:
have hu :=
  h.eq_of_subset_indep hYi (union_subset_union_left _ hJY) (union_subset_union_left _ hYX)
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y✝ Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : J ∪ I = Y ∪ I
⊢ J = Y

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y✝ Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : J ∪ I = Y ∪ I
⊢ J = Y
Tactic:
apply_fun fun x : Set α ↦ x \ I at hu
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y✝ Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : (J ∪ I) \ I = (Y ∪ I) \ I
⊢ J = Y

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y✝ Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : (J ∪ I) \ I = (Y ∪ I) \ I
⊢ J = Y
Tactic:
simp_rw [union_diff_right, hdj.1.sdiff_eq_left, hYI.sdiff_eq_left] at hu
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y✝ Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : J = Y
⊢ J = Y

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y✝ Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : J = Y
⊢ J = Y
Tactic:
exact hu
State after:
no goals