Theorem: SciLean.isomorph.id_rule (SciLean/Core/FunctionTransformations/Isomorph.lean)

State before:
α : Type u_2
β : Type ?u.40
γ : Type ?u.43
α' : outParam (Type u_1)
β' : outParam (Type ?u.51)
γ' : outParam (Type ?u.55)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
⊢ (isomorph tag fun x => x) = fun x => x
Tactic:
funext _
State after:
case h
α : Type u_2
β : Type ?u.40
γ : Type ?u.43
α' : outParam (Type u_1)
β' : outParam (Type ?u.51)
γ' : outParam (Type ?u.55)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
x✝ : α'
⊢ isomorph tag (fun x => x) x✝ = x✝

State before:
case h
α : Type u_2
β : Type ?u.40
γ : Type ?u.43
α' : outParam (Type u_1)
β' : outParam (Type ?u.51)
γ' : outParam (Type ?u.55)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
x✝ : α'
⊢ isomorph tag (fun x => x) x✝ = x✝
Tactic:
simp[isomorph]
State after:
no goals