Theorem: Matroid.Minor.exists_minor_isSimplification (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hNM : N ≤m M
hN : N.Simple
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Tactic:
obtain ⟨I, hI, hr, -⟩ := hNM.exists_contract_spanning_restrict
State after:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M

State before:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Tactic:
have hN' := hr.eq_restrict ▸
  M.contract_restrict_eq_restrict_contract _ _ (subset_diff.1 hr.subset).2.symm
State after:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M

State before:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Tactic:
have h : (M ↾ (N.E ∪ I)).Simple := by
  apply Indep.simple_of_contract_simple (I := I) _ (by rwa [← hN'])
  refine restrict_indep_iff.2 ⟨hI, subset_union_right⟩
State after:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h : (M ↾ (N.E ∪ I)).Simple
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M

State before:
case intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h : (M ↾ (N.E ∪ I)).Simple
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Tactic:
obtain ⟨M₀, hM₀, h⟩ := h.exists_restriction_isSimplification_of_restriction (M := M)
  (restrict_restriction _ _ (union_subset hNM.subset hI.subset_ground))
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h✝ : (M ↾ (N.E ∪ I)).Simple
M₀ : Matroid α
hM₀ : M₀.IsSimplification M
h : M ↾ (N.E ∪ I) ≤r M₀
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h✝ : (M ↾ (N.E ∪ I)).Simple
M₀ : Matroid α
hM₀ : M₀.IsSimplification M
h : M ↾ (N.E ∪ I) ≤r M₀
⊢ ∃ M₀, N ≤m M₀ ∧ M₀.IsSimplification M
Tactic:
refine ⟨M₀, Minor.trans ?_ h.minor, hM₀⟩
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h✝ : (M ↾ (N.E ∪ I)).Simple
M₀ : Matroid α
hM₀ : M₀.IsSimplification M
h : M ↾ (N.E ∪ I) ≤r M₀
⊢ N ≤m M ↾ (N.E ∪ I)

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h✝ : (M ↾ (N.E ∪ I)).Simple
M₀ : Matroid α
hM₀ : M₀.IsSimplification M
h : M ↾ (N.E ∪ I) ≤r M₀
⊢ N ≤m M ↾ (N.E ∪ I)
Tactic:
rw [hN']
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h✝ : (M ↾ (N.E ∪ I)).Simple
M₀ : Matroid α
hM₀ : M₀.IsSimplification M
h : M ↾ (N.E ∪ I) ≤r M₀
⊢ (M ↾ (N.E ∪ I)) ／ I ≤m M ↾ (((M ↾ (N.E ∪ I)) ／ I).E ∪ I)

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
h✝ : (M ↾ (N.E ∪ I)).Simple
M₀ : Matroid α
hM₀ : M₀.IsSimplification M
h : M ↾ (N.E ∪ I) ≤r M₀
⊢ (M ↾ (N.E ∪ I)) ／ I ≤m M ↾ (((M ↾ (N.E ∪ I)) ／ I).E ∪ I)
Tactic:
simpa using contract_minor _ _
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ (M ↾ (N.E ∪ I)).Simple
Tactic:
apply Indep.simple_of_contract_simple (I := I) _ (by rwa [← hN'])
State after:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ (M ↾ (N.E ∪ I)).Indep I

State before:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ (M ↾ (N.E ∪ I)).Indep I
Tactic:
refine restrict_indep_iff.2 ⟨hI, subset_union_right⟩
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
hNM : N ≤m M
hN : N.Simple
I : Set α
hI : M.Indep I
hr : N ≤r M ／ I
hN' : N = (M ↾ (N.E ∪ I)) ／ I
⊢ ((M ↾ (N.E ∪ I)) ／ I).Simple
Tactic:
rwa [← hN']
State after:
no goals