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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ N ≤r M
Tactic:
obtain ⟨f, rfl⟩ := h
State after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ M ↾ ⇑f '' {e | M.Nonloop e} ≤r M

State before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ M ↾ ⇑f '' {e | M.Nonloop e} ≤r M
Tactic:
refine restrict_restriction _ _ ?_
State after:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ ⇑f '' {e | M.Nonloop e} ⊆ M.E

State before:
case intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x y : α
f : M.parallelClasses.RepFun
⊢ ⇑f '' {e | M.Nonloop e} ⊆ M.E
Tactic:
rintro _ ⟨x,hx,rfl⟩
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x✝ y : α
f : M.parallelClasses.RepFun
x : α
hx : x ∈ {e | M.Nonloop e}
⊢ f x ∈ M.E

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
e f✝ g : α
I X P D : Set α
x✝ y : α
f : M.parallelClasses.RepFun
x : α
hx : x ∈ {e | M.Nonloop e}
⊢ f x ∈ M.E
Tactic:
exact Nonloop.mem_ground <| f.apply_mem hx
State after:
no goals