no goals
𝕜 : Type u_2
inst✝⁴ : IsROrC 𝕜
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
x : F
⊢ ↑re (↑(extendTo𝕜' fr) x) = ↑fr x
simp only [extendTo𝕜'_apply, map_sub, MulZeroClass.zero_mul, MulZeroClass.mul_zero, sub_zero,
  isROrC_simps]