Theorem: Function.Bijective.HMul.hMul.arg_a0.Bijective_rule_field (SciLean/Core/FunctionPropositions/Bijective.lean)

State before:
X✝ : Type ?u.4430
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.4436
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.4442
inst✝⁶ : Nonempty Z✝
X : Type u_2
inst✝⁵ : Nonempty X
X₁ : Type ?u.4454
inst✝⁴ : Nonempty X₁
X₂ : Type ?u.4460
inst✝³ : Nonempty X₂
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.4472
inst✝¹ : Nonempty Z
inst✝ : Field Y
f : X → Y
y : Y
hf : Bijective f
hy : y ≠ 0
⊢ Bijective fun x => f x * y
Tactic:
sorry_proof
State after:
no goals