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

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

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