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

State before:
X✝ : Type ?u.3787
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.3793
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.3799
inst✝⁶ : Nonempty Z✝
X₁ : Type ?u.3805
inst✝⁵ : Nonempty X₁
X₂ : Type ?u.3811
inst✝⁴ : Nonempty X₂
X : Type u_2
inst✝³ : Nonempty X
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.3829
inst✝¹ : Nonempty Z
inst✝ : AddGroup Y
f : X → Y
y : Y
hf : Bijective f
⊢ (invFun fun x => f x - y) = fun y' => invFun f (y' + y)
Tactic:
sorry_proof
State after:
no goals