Theorem: Finset.sup_univ_equiv (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
α' : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
inst✝² : Fintype α'
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : α → β
e : α' ≃ α
⊢ (univ.sup fun i => f (e i)) = univ.sup f
Tactic:
simpa[Function.comp] using Eq.symm <| Finset.sup_image univ e f
State after:
no goals