Theorem: SciLean.isomorphicType_equiv_id (SciLean/Core/Objects/IsomorphicType/RealToFloat.lean)

State before:
α✝ : Type ?u.9726
α' : Type ?u.9729
β : Type ?u.9732
β' : Type ?u.9735
γ : Type ?u.9738
γ' : Type ?u.9741
inst✝² : IsomorphicType `RealToFloat α✝ α'
inst✝¹ : IsomorphicType `RealToFloat β β'
inst✝ : IsomorphicType `RealToFloat γ γ'
α : Type u_1
a : α
⊢ (IsomorphicType.equiv `RealToFloat) a = a
Tactic:
rfl
State after:
no goals