Theorem: SciLean.decompose_has_unique_solution (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)
⊢ HasUniqueSolution P ↔ HasUniqueSolution fun ys => Q₂ ys (solve zs, Q₁ ys zs)
Tactic:
sorry_proof
State after:
no goals