Theorem: Matroid.comapOn_preimage_eq (Matroid/Map.lean)

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
⊢ N.comapOn (f ⁻¹' N.E) f = N.comap f
Tactic:
rw [comapOn, restrict_eq_self_iff]
State after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
⊢ f ⁻¹' N.E = (N.comap f).E

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
⊢ f ⁻¹' N.E = (N.comap f).E
Tactic:
rfl
State after:
no goals