Theorem: Matroid.IsSimplification.repFun_injOn (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
⊢ InjOn (⇑h.repFun) N.E
Tactic:
apply Simple.repFun_injOn
State after:
case h
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ (M ↾ N.E).Simple

State before:
case h
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ (M ↾ N.E).Simple
Tactic:
rw [h.restriction.eq_restrict]
State after:
case h
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ N.Simple

State before:
case h
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
⊢ N.Simple
Tactic:
exact h.simple
State after:
no goals