Theorem: Function.invFun.comp_rule (SciLean/Core/FunctionTransformations/InvFun.lean)

State before:
X : Type u_3
inst✝⁴ : Nonempty X
Y : Type u_1
inst✝³ : Nonempty Y
Z : Type u_2
inst✝² : Nonempty Z
X₁ : Type ?u.169
inst✝¹ : Nonempty X₁
X₂ : Type ?u.175
inst✝ : Nonempty X₂
f : Y → Z
g : X → Y
hf : Bijective f
hg : Bijective g
⊢ (invFun fun x => f (g x)) = fun z =>
    let y := invFun f z;
    let x := invFun g y;
    x
Tactic:
sorry_proof
State after:
no goals