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

State before:
X : Type u_5
inst✝⁴ : Nonempty X
Y : Type u_1
inst✝³ : Nonempty Y
Z : Type u_3
inst✝² : Nonempty Z
X₁ : Type u_4
inst✝¹ : Nonempty X₁
X₂ : Type u_2
inst✝ : Nonempty X₂
f : X₂ → Y → Z
g : X₁ → Y
p₁ : X → X₁
p₂ : X → X₂
hf : Bijective fun xy => f xy.1 xy.2
hg : Bijective g
hp : Bijective fun x => (p₁ x, p₂ x)
⊢ (invFun fun x =>
      let y := g (p₁ x);
      f (p₂ x) y) =
    fun z =>
    let x₂y := invFun (fun xy => f xy.1 xy.2) z;
    let x₁ := invFun g x₂y.2;
    let x := invFun (fun x => (p₁ x, p₂ x)) (x₁, x₂y.1);
    x
Tactic:
sorry_proof
State after:
no goals