Theorem: Matroid.Indep.union_contract_basis_union_of_basis (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 α
hI : M.Indep I
hB : (M ／ I).Basis J X
⊢ M.Basis (J ∪ I) (X ∪ I)
Tactic:
have hi := hB.indep
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : (M ／ I).Indep J
⊢ M.Basis (J ∪ I) (X ∪ I)

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

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
⊢ M.Basis (J ∪ I) (X ∪ I)
Tactic:
refine' hi.2.basis_of_maximal_subset (union_subset_union_left _ hB.subset) _ _
State after:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
⊢ ∀ ⦃J_1 : Set α⦄, M.Indep J_1 → J ∪ I ⊆ J_1 → J_1 ⊆ X ∪ I → J_1 ⊆ J ∪ I

case refine'_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
⊢ X ∪ I ⊆ M.E

State before:
case refine'_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
⊢ X ∪ I ⊆ M.E
Tactic:
exact union_subset (hB.subset_ground.trans (contract_ground_subset_ground _ _)) hI.subset_ground
State after:
no goals

State before:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
⊢ ∀ ⦃J_1 : Set α⦄, M.Indep J_1 → J ∪ I ⊆ J_1 → J_1 ⊆ X ∪ I → J_1 ⊆ J ∪ I
Tactic:
intro K hK hJIK hKXI
State after:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ∪ I ⊆ K
hKXI : K ⊆ X ∪ I
⊢ K ⊆ J ∪ I

State before:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ∪ I ⊆ K
hKXI : K ⊆ X ∪ I
⊢ K ⊆ J ∪ I
Tactic:
rw [union_subset_iff] at hJIK
State after:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
⊢ K ⊆ J ∪ I

State before:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
⊢ K ⊆ J ∪ I
Tactic:
have hK' : (M ／ I).Indep (K \ I) := hK.diff_indep_contract_of_subset hJIK.2
State after:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
hK' : (M ／ I).Indep (K \ I)
⊢ K ⊆ J ∪ I

State before:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
hK' : (M ／ I).Indep (K \ I)
⊢ K ⊆ J ∪ I
Tactic:
have hm := hB.eq_of_subset_indep hK'
State after:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
hK' : (M ／ I).Indep (K \ I)
hm : J ⊆ K \ I → K \ I ⊆ X → J = K \ I
⊢ K ⊆ J ∪ I

State before:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
hK' : (M ／ I).Indep (K \ I)
hm : J ⊆ K \ I → K \ I ⊆ X → J = K \ I
⊢ K ⊆ J ∪ I
Tactic:
rw [subset_diff, and_iff_left hi.1, diff_subset_iff, union_comm, imp_iff_right hKXI,
  imp_iff_right hJIK.1] at hm
State after:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
hK' : (M ／ I).Indep (K \ I)
hm : J = K \ I
⊢ K ⊆ J ∪ I

State before:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
hK' : (M ／ I).Indep (K \ I)
hm : J = K \ I
⊢ K ⊆ J ∪ I
Tactic:
simp [hm]
State after:
no goals