no goals
R : Type u_1
A : Type u_2
B : Type ?u.109263
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
r : R
x : ℍ[R,c₁,c₂]
⊢ lift q (r • x) = r • lift q x
simp [lift, mul_smul, ← Algebra.smul_def]