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

State before:
α : Type u_3
β : Type u_4
γ : Type ?u.13084
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type ?u.13096)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
x : α
⊢ (isomorph tag fun f => f x) = fun f => f ((IsomorphicType.equiv tag) x)
Tactic:
funext _
State after:
case h
α : Type u_3
β : Type u_4
γ : Type ?u.13084
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type ?u.13096)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
x : α
x✝ : α' → β'
⊢ isomorph tag (fun f => f x) x✝ = x✝ ((IsomorphicType.equiv tag) x)

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