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

State before:
X : Type u_1
inst✝⁴ : Nonempty X
Y : Type ?u.53
inst✝³ : Nonempty Y
Z : Type ?u.59
inst✝² : Nonempty Z
X₁ : Type ?u.65
inst✝¹ : Nonempty X₁
X₂ : Type ?u.71
inst✝ : Nonempty X₂
⊢ (invFun fun x => x) = fun x => x
Tactic:
sorry_proof
State after:
no goals