Theorem: Matroid.IsSimplification.of_restriction (Matroid/Simple.lean)

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

State before:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
⊢ N.IsSimplification (M ↾ R)
Tactic:
rw [isSimplification_iff] at h ⊢
State after:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
⊢ N.Loopless ∧ N ≤r M ↾ R ∧ ∀ ⦃e : α⦄, (M ↾ R).Nonloop e → ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f

State before:
case intro.intro
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
⊢ N.Loopless ∧ N ≤r M ↾ R ∧ ∀ ⦃e : α⦄, (M ↾ R).Nonloop e → ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f
Tactic:
refine ⟨h.1, hNM', fun e he ↦ ?_⟩
State after:
case intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
⊢ ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f

State before:
case intro.intro
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
⊢ ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f
Tactic:
obtain ⟨f, hf, hf'⟩ := h.2.2 (he.of_restriction hM'M)
State after:
case intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
f : α
hf : f ∈ N.E ∧ M.Parallel e f
hf' : ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f
⊢ ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f

State before:
case intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
f : α
hf : f ∈ N.E ∧ M.Parallel e f
hf' : ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f
⊢ ∃! f, f ∈ N.E ∧ (M ↾ R).Parallel e f
Tactic:
simp only [restrict_parallel_iff]
State after:
case intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
f : α
hf : f ∈ N.E ∧ M.Parallel e f
hf' : ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f
⊢ ∃! f, f ∈ N.E ∧ M.Parallel e f ∧ e ∈ R ∧ f ∈ R

State before:
case intro.intro.intro.intro
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
f : α
hf : f ∈ N.E ∧ M.Parallel e f
hf' : ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f
⊢ ∃! f, f ∈ N.E ∧ M.Parallel e f ∧ e ∈ R ∧ f ∈ R
Tactic:
exact ⟨f, ⟨hf.1, hf.2, he.mem_ground, hNM'.subset hf.1⟩, by tauto⟩
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
x y : α
h : N.Loopless ∧ N ≤r M ∧ ∀ ⦃e : α⦄, M.Nonloop e → ∃! f, f ∈ N.E ∧ M.Parallel e f
R : Set α
hR : R ⊆ M.E
hNM' : N ≤r M ↾ R
hM'M : M ↾ R ≤r M
e : α
he : (M ↾ R).Nonloop e
f : α
hf : f ∈ N.E ∧ M.Parallel e f
hf' : ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f) y → y = f
⊢ ∀ (y : α), (fun f => f ∈ N.E ∧ M.Parallel e f ∧ e ∈ R ∧ f ∈ R) y → y = f
Tactic:
tauto
State after:
no goals