Theorem: Function.Bijective.Equiv.toFun.arg_a0.Bijective_rule (SciLean/Core/FunctionPropositions/Bijective.lean)

State before:
X✝ : Type ?u.7310
inst✝⁷ : Nonempty X✝
Y✝ : Type ?u.7316
inst✝⁶ : Nonempty Y✝
Z✝ : Type ?u.7322
inst✝⁵ : Nonempty Z✝
X : Type u_3
inst✝⁴ : Nonempty X
X₁ : Type ?u.7334
inst✝³ : Nonempty X₁
X₂ : Type ?u.7340
inst✝² : Nonempty X₂
Y : Type u_1
inst✝¹ : Nonempty Y
Z : Type u_2
inst✝ : Nonempty Z
f : Y ≃ Z
g : X → Y
hf : Bijective g
⊢ Bijective fun x => f (g x)
Tactic:
sorry_proof
State after:
no goals