Theorem: Matroid.Simple.exists_restriction_isSimplification_of_restriction (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
hN : N.Simple
h : N ≤r M
⊢ ∃ M', M'.IsSimplification M ∧ N ≤r M'
Tactic:
obtain ⟨R, -, rfl⟩ := h.exists_eq_restrict
State after:
case intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
⊢ ∃ M', M'.IsSimplification M ∧ M ↾ R ≤r M'

State before:
case intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
⊢ ∃ M', M'.IsSimplification M ∧ M ↾ R ≤r M'
Tactic:
obtain ⟨M', hM', hRM'⟩ := hN.exists_subset_isSimplification
State after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
M' : Matroid α
hM' : M'.IsSimplification M
hRM' : R ⊆ M'.E
⊢ ∃ M', M'.IsSimplification M ∧ M ↾ R ≤r M'

State before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
M' : Matroid α
hM' : M'.IsSimplification M
hRM' : R ⊆ M'.E
⊢ ∃ M', M'.IsSimplification M ∧ M ↾ R ≤r M'
Tactic:
refine ⟨M', hM', ?_⟩
State after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
M' : Matroid α
hM' : M'.IsSimplification M
hRM' : R ⊆ M'.E
⊢ M ↾ R ≤r M'

State before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
M' : Matroid α
hM' : M'.IsSimplification M
hRM' : R ⊆ M'.E
⊢ M ↾ R ≤r M'
Tactic:
obtain ⟨R', -, rfl⟩ := hM'.restriction.exists_eq_restrict
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
R' : Set α
hM' : (M ↾ R').IsSimplification M
hRM' : R ⊆ (M ↾ R').E
⊢ M ↾ R ≤r M ↾ R'

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
R' : Set α
hM' : (M ↾ R').IsSimplification M
hRM' : R ⊆ (M ↾ R').E
⊢ M ↾ R ≤r M ↾ R'
Tactic:
exact ⟨R, hRM', by rw [restrict_restrict_eq _ (show R ⊆ R' from hRM')]⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
e f g : α
I X P D : Set α
x y : α
R : Set α
hN : (M ↾ R).Simple
h : M ↾ R ≤r M
R' : Set α
hM' : (M ↾ R').IsSimplification M
hRM' : R ⊆ (M ↾ R').E
⊢ M ↾ R = M ↾ R' ↾ R
Tactic:
rw [restrict_restrict_eq _ (show R ⊆ R' from hRM')]
State after:
no goals