Theorem: HSMul.hSMul.arg_a1.IsLinearMap_rule (SciLean/Core/FunctionPropositions/IsLinearMap.lean)

State before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.177202
ι : Type ?u.177205
E : ι → Type ?u.177210
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module R X
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module R Y
inst✝³ : AddCommGroup Z
inst✝² : Module R Z
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
c : R
f : X → Y
hf : IsLinearMap R f
a : Y →ₗ[R] Y := mk' (fun z => c • z) ⋯
b : X →ₗ[R] Y := mk' f hf
⊢ ∀ (x : X), c • f x = (a ∘ₗ b) x
Tactic:
simp (config:={zetaDelta:=true})
State after:
no goals