intro h
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
⊢ isomorph tag f = isomorph tag g → f = g
α : Type u_4
β✝ : Type ?u.3945
γ : Type ?u.3948
α' : outParam (Type u_3)
β'✝ : outParam (Type ?u.3956)
γ' : outParam (Type ?u.3960)
tag : Name
inst✝³ : IsomorphicType tag α α'
inst✝² : IsomorphicType tag β✝ β'✝
inst✝¹ : IsomorphicType tag γ γ'
β : Type u_1
β' : Type u_2
inst✝ : IsomorphicType tag β β'
f g : α → β
h : isomorph tag f = isomorph tag g
⊢ f = g