Theorem: Matroid.contract_restrict_eq_restrict_contract (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
⊢ M ／ C ↾ R = (M ↾ (R ∪ C)) ／ C
Tactic:
refine eq_of_indep_iff_indep_forall (by simp [h.sdiff_eq_right]) (fun I _ ↦ ?_)
State after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
Tactic:
obtain ⟨J, hJ⟩ := (M ↾ (R ∪ C)).exists_basis' C
State after:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I

State before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
Tactic:
have hJ' : M.Basis' J C := by
  have := (basis'_restrict_iff.1 hJ).1
  rwa [inter_eq_self_of_subset_left subset_union_right] at this
State after:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
hJ' : M.Basis' J C
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I

State before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
hJ' : M.Basis' J C
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
Tactic:
rw [restrict_indep_iff, hJ.contract_indep_iff, hJ'.contract_indep_iff, restrict_indep_iff,
  union_subset_iff, and_iff_left (hJ.subset.trans subset_union_right), union_comm R C,
  ← diff_subset_iff, and_assoc, and_assoc, and_congr_right_iff, and_comm, and_congr_left_iff]
State after:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
hJ' : M.Basis' J C
⊢ M.Indep (I ∪ J) → Disjoint C I → (I ⊆ R ↔ I \ C ⊆ R)

State before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
hJ' : M.Basis' J C
⊢ M.Indep (I ∪ J) → Disjoint C I → (I ⊆ R ↔ I \ C ⊆ R)
Tactic:
intro _ hd
State after:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
hJ' : M.Basis' J C
a✝ : M.Indep (I ∪ J)
hd : Disjoint C I
⊢ I ⊆ R ↔ I \ C ⊆ R

State before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
hJ' : M.Basis' J C
a✝ : M.Indep (I ∪ J)
hd : Disjoint C I
⊢ I ⊆ R ↔ I \ C ⊆ R
Tactic:
rw [hd.sdiff_eq_right]
State after:
no goals

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
⊢ (M ／ C ↾ R).E = ((M ↾ (R ∪ C)) ／ C).E
Tactic:
simp [h.sdiff_eq_right]
State after:
no goals

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
⊢ M.Basis' J C
Tactic:
have := (basis'_restrict_iff.1 hJ).1
State after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
this : M.Basis' J (C ∩ (R ∪ C))
⊢ M.Basis' J C

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
this : M.Basis' J (C ∩ (R ∪ C))
⊢ M.Basis' J C
Tactic:
rwa [inter_eq_self_of_subset_left subset_union_right] at this
State after:
no goals