Theorem: Matroid.strictMinor_iff_minor_contract_or_delete (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₂ : Matroid α
⊢ N <m M ↔ ∃ e ∈ M.E, N ≤m M ／ e ∨ N ≤m M ＼ e
Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
State after:
case refine_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
h : N <m M
⊢ ∃ e ∈ M.E, N ≤m M ／ e ∨ N ≤m M ＼ e

case refine_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ e ∈ M.E, N ≤m M ／ e ∨ N ≤m M ＼ e) → N <m M

State before:
case refine_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ e ∈ M.E, N ≤m M ／ e ∨ N ≤m M ＼ e) → N <m M
Tactic:
rintro ⟨e, he, (hc | hd)⟩
State after:
case refine_2.intro.intro.inl
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
e : α
he : e ∈ M.E
hc : N ≤m M ／ e
⊢ N <m M

case refine_2.intro.intro.inr
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
e : α
he : e ∈ M.E
hd : N ≤m M ＼ e
⊢ N <m M

State before:
case refine_2.intro.intro.inr
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
e : α
he : e ∈ M.E
hd : N ≤m M ＼ e
⊢ N <m M
Tactic:
exact hd.trans_strictMinor (deleteElem_strictMinor he)
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 : Set α
M₀ M₁ M₂ : Matroid α
h : N <m M
⊢ ∃ e ∈ M.E, N ≤m M ／ e ∨ N ≤m M ＼ e
Tactic:
obtain ⟨C, D, hC, hD, hCD, ⟨e,(heC | heD)⟩, rfl⟩ :=
  strictMinor_iff_exists_eq_contract_delete.1 h
State after:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inl
α : Type u_1
M M' : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heC : e ∈ C
h : M ／ C ＼ D <m M
⊢ ∃ e ∈ M.E, M ／ C ＼ D ≤m M ／ e ∨ M ／ C ＼ D ≤m M ＼ e

case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M M' : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ ∃ e ∈ M.E, M ／ C ＼ D ≤m M ／ e ∨ M ／ C ＼ D ≤m M ＼ e

State before:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M M' : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ ∃ e ∈ M.E, M ／ C ＼ D ≤m M ／ e ∨ M ／ C ＼ D ≤m M ＼ e
Tactic:
refine ⟨e, hD heD, Or.inr ?_⟩
State after:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M M' : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ M ／ C ＼ D ≤m M ＼ e

State before:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M M' : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ M ／ C ＼ D ≤m M ＼ e
Tactic:
rw [contract_delete_comm _ hCD, ← insert_eq_of_mem heD, ← singleton_union, ← delete_delete]
State after:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M M' : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ M ＼ {e} ＼ D ／ C ≤m M ＼ e

State before:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M M' : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ M ＼ {e} ＼ D ／ C ≤m M ＼ e
Tactic:
apply delete_contract_minor
State after:
no goals

State before:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inl
α : Type u_1
M M' : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heC : e ∈ C
h : M ／ C ＼ D <m M
⊢ ∃ e ∈ M.E, M ／ C ＼ D ≤m M ／ e ∨ M ／ C ＼ D ≤m M ＼ e
Tactic:
refine ⟨e, hC heC, Or.inl ?_⟩
State after:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inl
α : Type u_1
M M' : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heC : e ∈ C
h : M ／ C ＼ D <m M
⊢ M ／ C ＼ D ≤m M ／ e

State before:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inl
α : Type u_1
M M' : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heC : e ∈ C
h : M ／ C ＼ D <m M
⊢ M ／ C ＼ D ≤m M ／ e
Tactic:
rw [← insert_eq_of_mem heC, ← singleton_union, ← contract_contract, contract_elem ]
State after:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inl
α : Type u_1
M M' : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heC : e ∈ C
h : M ／ C ＼ D <m M
⊢ M ／ {e} ／ C ＼ D ≤m M ／ {e}

State before:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inl
α : Type u_1
M M' : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
heC : e ∈ C
h : M ／ C ＼ D <m M
⊢ M ／ {e} ／ C ＼ D ≤m M ／ {e}
Tactic:
apply contract_delete_minor
State after:
no goals

State before:
case refine_2.intro.intro.inl
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
e : α
he : e ∈ M.E
hc : N ≤m M ／ e
⊢ N <m M
Tactic:
exact hc.trans_strictMinor (contractElem_strictMinor he)
State after:
no goals