Theorem: Matroid.Circuit.contract_circuit (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 α
hK : M.Circuit K
hC : C ⊂ K
⊢ (M ／ C).Circuit (K \ C)
Tactic:
have hCi := hK.ssubset_indep hC
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
⊢ (M ／ C).Circuit (K \ C)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
⊢ (M ／ C).Circuit (K \ C)
Tactic:
rw [circuit_iff_forall_ssubset, hCi.contract_dep_iff, and_iff_right (disjoint_sdiff_left),
  diff_union_self, union_eq_self_of_subset_right hC.subset, and_iff_right hK.dep]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
⊢ ∀ ⦃I : Set α⦄, I ⊂ K \ C → (M ／ C).Indep I

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
⊢ ∀ ⦃I : Set α⦄, I ⊂ K \ C → (M ／ C).Indep I
Tactic:
intro I hI
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : I ⊂ K \ C
⊢ (M ／ C).Indep I

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : I ⊂ K \ C
⊢ (M ／ C).Indep I
Tactic:
rw [ssubset_iff_subset_not_subset, subset_diff, diff_subset_iff, union_comm] 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 α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ (M ／ C).Indep I

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ (M ／ C).Indep I
Tactic:
rw [hCi.contract_indep_iff, and_iff_right hI.1.2]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ M.Indep (I ∪ C)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ M.Indep (I ∪ C)
Tactic:
refine hK.ssubset_indep <| (union_subset hI.1.1 hC.subset).ssubset_of_ne ?_
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ I ∪ C ≠ K

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K C C₁ C₂ : Set α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ I ∪ C ≠ K
Tactic:
rintro rfl
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z C C₁ C₂ : Set α
hCi : M.Indep C
I : Set α
hK : M.Circuit (I ∪ C)
hC : C ⊂ I ∪ C
hI : (I ⊆ I ∪ C ∧ Disjoint I C) ∧ ¬I ∪ C ⊆ I ∪ C
⊢ False

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z C C₁ C₂ : Set α
hCi : M.Indep C
I : Set α
hK : M.Circuit (I ∪ C)
hC : C ⊂ I ∪ C
hI : (I ⊆ I ∪ C ∧ Disjoint I C) ∧ ¬I ∪ C ⊆ I ∪ C
⊢ False
Tactic:
exact hI.2 Subset.rfl
State after:
no goals