case h
α : Type u_1
β : Type ?u.48925
γ : Type ?u.48928
inst✝ : Finite α
e : α ↪ α
x✝ : α
⊢ ↑(Equiv.toEmbedding (equivOfFintypeSelfEmbedding e)) x✝ = ↑e x✝
α : Type u_1
β : Type ?u.48925
γ : Type ?u.48928
inst✝ : Finite α
e : α ↪ α
⊢ Equiv.toEmbedding (equivOfFintypeSelfEmbedding e) = e
ext
no goals
case h
α : Type u_1
β : Type ?u.48925
γ : Type ?u.48928
inst✝ : Finite α
e : α ↪ α
x✝ : α
⊢ ↑(Equiv.toEmbedding (equivOfFintypeSelfEmbedding e)) x✝ = ↑e x✝
rfl