Theorem: SciLean.decomposeSolution (SciLean/Util/SolveFun.lean)

State before:
Xs : Type u_1
Ys : Type u_2
Zs : Type u_3
inst✝² : Nonempty Xs
inst✝¹ : Nonempty Ys
inst✝ : Nonempty Zs
f : Ys → Zs → Xs
hf : Function.Bijective (uncurryN 2 f)
P : Xs → Prop
Q₁ Q₂ : Ys → Zs → Prop
equiv : ∀ (ys : Ys) (zs : Zs), Q₁ ys zs ∧ Q₂ ys zs ↔ P (f ys zs)
unique : ∀ (ys : Ys), HasUniqueSolution (Q₁ ys)
⊢ (solve xs, P xs) =
    let zs' := fun ys => solve zs, Q₁ ys zs;
    let ys := solve ys, Q₂ ys (zs' ys);
    let zs := zs' ys;
    f ys zs
Tactic:
sorry_proof
State after:
no goals