Theorem: Profinite.finiteCoproduct.range_eq (Profinite/ExplicitLimits.lean)

State before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → Profinite
α : Type
inst✝ : Fintype α
Z : α → Profinite
a b : α
h : a = b
⊢ Set.range ↑(ι Z a) = Set.range ↑(ι Z b)
Tactic:
rw [h]
State after:
no goals