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

State before:
α : Type u_3
β : Type u_2
γ : Type ?u.587
α' : outParam (Type u_4)
β' : outParam (Type u_1)
γ' : outParam (Type ?u.599)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β
x : α
⊢ (IsomorphicType.equiv tag) (f x) = isomorph tag f ((IsomorphicType.equiv tag) x)
Tactic:
simp[IsomorphicType.equiv, isomorph]
State after:
no goals