Theorem: Function.invFun.Prod.mk.arg_fstsnd.invFun_rule (SciLean/Core/FunctionTransformations/InvFun.lean)

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