case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a✝ : Rˣ
⊢ ↑(χ * 1) ↑a✝ = ↑χ ↑a✝
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ * 1 = χ
ext
no goals
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a✝ : Rˣ
⊢ ↑(χ * 1) ↑a✝ = ↑χ ↑a✝
simp only [mul_one, Pi.mul_apply, MulChar.coeToFun_mul, MulChar.one_apply_coe]