Theorem: SciLean.isomorph.ext (SciLean/Core/Objects/IsomorphicType.lean)

State before:
α : Type u_2
β : Type ?u.2581
γ : Type ?u.2584
α' : outParam (Type u_1)
β' : outParam (Type ?u.2592)
γ' : outParam (Type ?u.2596)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
a b : α
⊢ (IsomorphicType.equiv tag) a = (IsomorphicType.equiv tag) b → a = b
Tactic:
simp[IsomorphicType.equiv]
State after:
no goals