Theorem: Prod.mk.isomorph_rule (SciLean/Core/FunctionTransformations/Isomorph.lean)

State before:
α : Type u_4
β : Type u_6
γ : Type u_5
α' : outParam (Type u_1)
β' : outParam (Type u_2)
γ' : outParam (Type u_3)
tag : Name
inst✝² : IsomorphicType tag α α'
inst✝¹ : IsomorphicType tag β β'
inst✝ : IsomorphicType tag γ γ'
f : α → β
g : α → γ
⊢ (isomorph tag fun x => (f x, g x)) = fun x' =>
    let y' := isomorph tag f x';
    let z' := isomorph tag g x';
    (y', z')
Tactic:
rfl
State after:
no goals