funext x'
α : Type u_4
β : Type u_5
γ : Type u_6
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type u_3)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β → γ
⊢ (isomorph tag fun x y => f x y) = fun x' => isomorph tag (f ((IsomorphicType.equiv tag).symm x'))
case h
α : Type u_4
β : Type u_5
γ : Type u_6
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type u_3)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β → γ
x' : α'
⊢ isomorph tag (fun x y => f x y) x' = isomorph tag (f ((IsomorphicType.equiv tag).symm x'))