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

State before:
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
f : Fin n → α
n' : ℕ
h : n' = n
⊢ (univ.sup fun i => f (Fin.cast h i)) = univ.sup f
Tactic:
rcases h with rfl
State after:
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n' : ℕ
f : Fin n' → α
⊢ (univ.sup fun i => f (Fin.cast ⋯ i)) = univ.sup f

State before:
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n' : ℕ
f : Fin n' → α
⊢ (univ.sup fun i => f (Fin.cast ⋯ i)) = univ.sup f
Tactic:
simp
State after:
no goals