Theorem: Matroid.strictMinor_iff_exists_eq_contract_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 ↔ ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D
Tactic:
rw [strictMinor_iff_minor_ssubset, minor_def]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E ↔
    ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E ↔
    ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D
Tactic:
constructor
State after:
case mp
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E →
    ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D

case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D) →
    (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E

State before:
case mp
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E →
    ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D

case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D) →
    (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E
Tactic:
rintro ⟨⟨C, D, hC, hD, hCD, rfl⟩, hss⟩
State after:
case mp.intro.intro.intro.intro.intro.intro
α : 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
hss : (M ／ C ＼ D).E ⊂ M.E
⊢ ∃ C_1 D_1, C_1 ⊆ M.E ∧ D_1 ⊆ M.E ∧ Disjoint C_1 D_1 ∧ (C_1 ∪ D_1).Nonempty ∧ M ／ C ＼ D = M ／ C_1 ＼ D_1

case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D) →
    (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E

State before:
case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D) →
    (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E
Tactic:
rintro ⟨C, D, hC, hD, hCD, ⟨e,he⟩, rfl⟩
State after:
case mpr.intro.intro.intro.intro.intro.intro.intro
α : 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 : α
he : e ∈ C ∪ D
⊢ (∃ C_1 D_1, C_1 ⊆ M.E ∧ D_1 ⊆ M.E ∧ Disjoint C_1 D_1 ∧ M ／ C ＼ D = M ／ C_1 ＼ D_1) ∧ (M ／ C ＼ D).E ⊂ M.E

State before:
case mpr.intro.intro.intro.intro.intro.intro.intro
α : 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 : α
he : e ∈ C ∪ D
⊢ (∃ C_1 D_1, C_1 ⊆ M.E ∧ D_1 ⊆ M.E ∧ Disjoint C_1 D_1 ∧ M ／ C ＼ D = M ／ C_1 ＼ D_1) ∧ (M ／ C ＼ D).E ⊂ M.E
Tactic:
use ⟨C, D, hC, hD, hCD, rfl⟩
State after:
case right
α : 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 : α
he : e ∈ C ∪ D
⊢ (M ／ C ＼ D).E ⊂ M.E

State before:
case right
α : 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 : α
he : e ∈ C ∪ D
⊢ (M ／ C ＼ D).E ⊂ M.E
Tactic:
rw [delete_ground, contract_ground, diff_diff, ssubset_iff_subset_not_subset,
  and_iff_right diff_subset]
State after:
case right
α : 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 : α
he : e ∈ C ∪ D
⊢ ¬M.E ⊆ M.E \ (C ∪ D)

State before:
case right
α : 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 : α
he : e ∈ C ∪ D
⊢ ¬M.E ⊆ M.E \ (C ∪ D)
Tactic:
exact fun hss ↦ (hss ((union_subset hC hD) he)).2 he
State after:
no goals

State before:
case mp.intro.intro.intro.intro.intro.intro
α : 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
hss : (M ／ C ＼ D).E ⊂ M.E
⊢ ∃ C_1 D_1, C_1 ⊆ M.E ∧ D_1 ⊆ M.E ∧ Disjoint C_1 D_1 ∧ (C_1 ∪ D_1).Nonempty ∧ M ／ C ＼ D = M ／ C_1 ＼ D_1
Tactic:
refine ⟨C, D, hC, hD, hCD, ?_, rfl⟩
State after:
case mp.intro.intro.intro.intro.intro.intro
α : 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
hss : (M ／ C ＼ D).E ⊂ M.E
⊢ (C ∪ D).Nonempty

State before:
case mp.intro.intro.intro.intro.intro.intro
α : 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
hss : (M ／ C ＼ D).E ⊂ M.E
⊢ (C ∪ D).Nonempty
Tactic:
rw [nonempty_iff_ne_empty]
State after:
case mp.intro.intro.intro.intro.intro.intro
α : 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
hss : (M ／ C ＼ D).E ⊂ M.E
⊢ C ∪ D ≠ ∅

State before:
case mp.intro.intro.intro.intro.intro.intro
α : 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
hss : (M ／ C ＼ D).E ⊂ M.E
⊢ C ∪ D ≠ ∅
Tactic:
rintro hCD
State after:
case mp.intro.intro.intro.intro.intro.intro
α : 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
hss : (M ／ C ＼ D).E ⊂ M.E
hCD : C ∪ D = ∅
⊢ False

State before:
case mp.intro.intro.intro.intro.intro.intro
α : 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
hss : (M ／ C ＼ D).E ⊂ M.E
hCD : C ∪ D = ∅
⊢ False
Tactic:
rw [delete_ground, contract_ground, diff_diff, hCD, diff_empty] at hss
State after:
case mp.intro.intro.intro.intro.intro.intro
α : 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
hss : M.E ⊂ M.E
hCD : C ∪ D = ∅
⊢ False

State before:
case mp.intro.intro.intro.intro.intro.intro
α : 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
hss : M.E ⊂ M.E
hCD : C ∪ D = ∅
⊢ False
Tactic:
exact hss.ne rfl
State after:
no goals