Theorem: SciLean.isomorph.comp_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 => f (g x)) = fun x => isomorph tag f (isomorph tag g x)
Tactic:
funext _
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 => f (g x)) x✝ = isomorph tag f (isomorph tag g x✝)

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 => f (g x)) x✝ = isomorph tag f (isomorph tag g x✝)
Tactic:
unfold isomorph
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✝ : α'
⊢ (IsomorphicType.equiv tag) ((fun x => f (g x)) ((IsomorphicType.equiv tag).symm x✝)) =
    (IsomorphicType.equiv tag)
      (f ((IsomorphicType.equiv tag).symm ((IsomorphicType.equiv tag) (g ((IsomorphicType.equiv tag).symm x✝)))))

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✝ : α'
⊢ (IsomorphicType.equiv tag) ((fun x => f (g x)) ((IsomorphicType.equiv tag).symm x✝)) =
    (IsomorphicType.equiv tag)
      (f ((IsomorphicType.equiv tag).symm ((IsomorphicType.equiv tag) (g ((IsomorphicType.equiv tag).symm x✝)))))
Tactic:
simp
State after:
no goals