funext _
α : Type u_3
β : Type u_4
γ : Type ?u.895
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type ?u.907)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
y : β
⊢ (isomorph tag fun x => y) = fun x => (IsomorphicType.equiv tag) y
case h
α : Type u_3
β : Type u_4
γ : Type ?u.895
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type ?u.907)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
y : β
x✝ : α'
⊢ isomorph tag (fun x => y) x✝ = (IsomorphicType.equiv tag) y