case h
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : A
⊢ ↑(mulLeft R 1) x✝ = ↑id x✝
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ mulLeft R 1 = id
ext
no goals
case h
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : A
⊢ ↑(mulLeft R 1) x✝ = ↑id x✝
simp only [LinearMap.id_coe, one_mul, id.def, mulLeft_apply]