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

State before:
X✝ : Type ?u.593
inst✝⁷ : Nonempty X✝
Y✝ : Type ?u.599
inst✝⁶ : Nonempty Y✝
Z✝ : Type ?u.605
inst✝⁵ : Nonempty Z✝
X : Type u_5
inst✝⁴ : Nonempty X
X₁ : Type u_1
inst✝³ : Nonempty X₁
X₂ : Type u_3
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)
⊢ Bijective fun x => (f (p₁ x), g (p₂ x))
Tactic:
sorry_proof
State after:
no goals