Theorem: Function.invFun.Equiv.invFun.arg_a0.invFun_rule (SciLean/Core/FunctionTransformations/InvFun.lean)

State before:
X✝ : Type ?u.10851
inst✝⁷ : Nonempty X✝
Y✝ : Type ?u.10857
inst✝⁶ : Nonempty Y✝
Z✝ : Type ?u.10863
inst✝⁵ : Nonempty Z✝
X₁ : Type ?u.10869
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.10875
inst✝³ : Nonempty X₂
X : Type u_3
inst✝² : Nonempty X
Y : Type u_1
inst✝¹ : Nonempty Y
Z : Type u_2
inst✝ : Nonempty Z
f : Y ≃ Z
g : X → Z
hf : Bijective g
⊢ (invFun fun x => f.invFun (g x)) = fun z => invFun g (f z)
Tactic:
sorry_proof
State after:
no goals