Theorem: Function.Bijective.Prod.mk.arg_fstsnd.Bijective_rule_simple' (SciLean/Core/FunctionPropositions/Bijective.lean)

State before:
X✝ : Type ?u.475
inst✝⁷ : Nonempty X✝
Y✝ : Type ?u.481
inst✝⁶ : Nonempty Y✝
Z✝ : Type ?u.487
inst✝⁵ : Nonempty Z✝
X : Type u_1
inst✝⁴ : Nonempty X
X₁ : Type ?u.499
inst✝³ : Nonempty X₁
X₂ : Type ?u.505
inst✝² : Nonempty X₂
Y : Type u_2
inst✝¹ : Nonempty Y
Z : Type ?u.517
inst✝ : Nonempty Z
⊢ Bijective fun xy => (xy.2, xy.1)
Tactic:
sorry_proof
State after:
no goals