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

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