no goals
k : Type u₁
G : Type u₂
R : Type ?u.2675847
inst✝⁵ : CommSemiring k
inst✝⁴ : AddMonoid G
A : Type u₃
inst✝³ : Semiring A
inst✝² : Algebra k A
B : Type ?u.2675884
inst✝¹ : Semiring B
inst✝ : Algebra k B
F : Multiplicative G →* A
x : Multiplicative G
⊢ ↑(↑(lift k G A) F) (↑(of k G) x) = ↑F x
rw [of_apply, ← lift_symm_apply, Equiv.symm_apply_apply]