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

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

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