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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
⊢ ∃ N, N.IsSimplification M ∧ X ⊆ N.E
Tactic:
obtain ⟨f, hf⟩ := M.parallelClasses.exists_extend_partial_repFun'
  (fun _ _ ↦ hX.eq_of_parallel_of_mem)
State after:
case intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
f : M.parallelClasses.RepFun
hf : EqOn (⇑f) id X
⊢ ∃ N, N.IsSimplification M ∧ X ⊆ N.E

State before:
case intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
f : M.parallelClasses.RepFun
hf : EqOn (⇑f) id X
⊢ ∃ N, N.IsSimplification M ∧ X ⊆ N.E
Tactic:
refine ⟨_, ⟨f,rfl⟩, ?_⟩
State after:
case intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
f : M.parallelClasses.RepFun
hf : EqOn (⇑f) id X
⊢ X ⊆ (M ↾ ⇑f '' {e | M.Nonloop e}).E

State before:
case intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
f : M.parallelClasses.RepFun
hf : EqOn (⇑f) id X
⊢ X ⊆ (M ↾ ⇑f '' {e | M.Nonloop e}).E
Tactic:
rw [← image_id X, ← hf.image_eq]
State after:
case intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
f : M.parallelClasses.RepFun
hf : EqOn (⇑f) id X
⊢ ⇑f '' X ⊆ (M ↾ ⇑f '' {e | M.Nonloop e}).E

State before:
case intro
α : Type u_1
M N : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
hX : (M ↾ X).Simple
f : M.parallelClasses.RepFun
hf : EqOn (⇑f) id X
⊢ ⇑f '' X ⊆ (M ↾ ⇑f '' {e | M.Nonloop e}).E
Tactic:
exact image_subset f hX.subset_nonloops
State after:
no goals