case mk
𝕜 : Type ?u.87212
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.87224
P : Type ?u.87227
Q : Type ?u.87230
Q₂ : Type ?u.87233
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᵃ[R] W
h : Continuous f.toFun
⊢ ↑{ toAffineMap := f, cont := h } =
    ↑(contLinear { toAffineMap := f, cont := h }) + Function.const V (↑{ toAffineMap := f, cont := h } 0)
𝕜 : Type ?u.87212
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.87224
P : Type ?u.87227
Q : Type ?u.87230
Q₂ : Type ?u.87233
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[R] W
⊢ ↑f = ↑(contLinear f) + Function.const V (↑f 0)
rcases f with ⟨f, h⟩
no goals
case mk
𝕜 : Type ?u.87212
R : Type u_1
V : Type u_2
W : Type u_3
W₂ : Type ?u.87224
P : Type ?u.87227
Q : Type ?u.87230
Q₂ : Type ?u.87233
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᵃ[R] W
h : Continuous f.toFun
⊢ ↑{ toAffineMap := f, cont := h } =
    ↑(contLinear { toAffineMap := f, cont := h }) + Function.const V (↑{ toAffineMap := f, cont := h } 0)
rw [coe_mk_const_linear_eq_linear, coe_mk, f.decomp, Pi.add_apply, LinearMap.map_zero, zero_add,
  ← Function.const_def]