Theorem: Matroid.IsSimplification.repFun_apply_mem_ground (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
he : M.Nonloop e
⊢ h.repFun e ∈ N.E
Tactic:
rw [← congr_arg Matroid.E h.image_restrict_repFun, restrict_ground_eq]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
he : M.Nonloop e
⊢ h.repFun e ∈ ⇑h.repFun '' {e | M.Nonloop e}

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
x y : α
h : N.IsSimplification M
he : M.Nonloop e
⊢ h.repFun e ∈ ⇑h.repFun '' {e | M.Nonloop e}
Tactic:
exact mem_image_of_mem h.repFun he
State after:
no goals