Theorem: Matroid.Dep.of_contract (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 ／ C).Dep X
hC : autoParam (C ⊆ M.E) _auto✝
⊢ M.Dep (C ∪ X)
Tactic:
rw [Dep, and_iff_left (union_subset hC (h.subset_ground.trans diff_subset))]
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 ／ C).Dep X
hC : autoParam (C ⊆ M.E) _auto✝
⊢ ¬M.Indep (C ∪ 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 ／ C).Dep X
hC : autoParam (C ⊆ M.E) _auto✝
⊢ ¬M.Indep (C ∪ X)
Tactic:
intro hi
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 ／ C).Dep X
hC : autoParam (C ⊆ M.E) _auto✝
hi : M.Indep (C ∪ X)
⊢ False

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 ／ C).Dep X
hC : autoParam (C ⊆ M.E) _auto✝
hi : M.Indep (C ∪ X)
⊢ False
Tactic:
rw [Dep, (hi.subset subset_union_left).contract_indep_iff, union_comm,
  and_iff_left hi] at h
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : ¬Disjoint X C ∧ X ⊆ (M ／ C).E
hC : autoParam (C ⊆ M.E) _auto✝
hi : M.Indep (C ∪ X)
⊢ False

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : ¬Disjoint X C ∧ X ⊆ (M ／ C).E
hC : autoParam (C ⊆ M.E) _auto✝
hi : M.Indep (C ∪ X)
⊢ False
Tactic:
exact h.1 (subset_diff.1 h.2).2
State after:
no goals