Theorem: Partial.mapIdx_ids (ReactorModel/Extensions.lean)

State before:
α : Type u_1
β : Type u_2
g : α → β
f : α ⇀ β
⊢ ids (mapIdx g f) = ids f
Tactic:
simp [mapIdx, mem_iff, ids]
State after:
no goals