Theorem: Function.Bijective.HSMul.hSMul.arg_a1.Bijective_rule_field (SciLean/Core/FunctionPropositions/Bijective.lean)

State before:
X✝ : Type ?u.5742
inst✝⁹ : Nonempty X✝
Y✝ : Type ?u.5748
inst✝⁸ : Nonempty Y✝
Z✝ : Type ?u.5754
inst✝⁷ : Nonempty Z✝
X : Type u_3
inst✝⁶ : Nonempty X
X₁ : Type ?u.5766
inst✝⁵ : Nonempty X₁
X₂ : Type ?u.5772
inst✝⁴ : Nonempty X₂
Y : Type u_2
inst✝³ : Nonempty Y
Z : Type ?u.5784
inst✝² : Nonempty Z
R : Type u_1
inst✝¹ : Field R
inst✝ : MulAction R Y
r : R
f : X → Y
hf : Bijective f
hr : r ≠ 0
⊢ Bijective fun x => r • f x
Tactic:
sorry_proof
State after:
no goals