[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[{a}ᶜ] a) (norm ∘ f)
⊢ f =o[𝓝[{a}ᶜ] a] fun x => (x - a)⁻¹
[PROOFSTEP]
refine' (h.isBigO_const (one_ne_zero' ℝ)).trans_isLittleO (isLittleO_const_left.2 <| Or.inr _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[{a}ᶜ] a) (norm ∘ f)
⊢ Tendsto (norm ∘ fun x => (x - a)⁻¹) (𝓝[{a}ᶜ] a) atTop
[PROOFSTEP]
simp only [(· ∘ ·), norm_inv]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[{a}ᶜ] a) (norm ∘ f)
⊢ Tendsto (fun x => ‖x - a‖⁻¹) (𝓝[{a}ᶜ] a) atTop
[PROOFSTEP]
exact (tendsto_norm_sub_self_punctured_nhds a).inv_tendsto_zero
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ (fun x => x ^ p / x ^ q) =ᶠ[atTop] fun x => x ^ (↑p - ↑q)
[PROOFSTEP]
apply (eventually_gt_atTop (0 : 𝕜)).mono fun x hx => _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ ∀ (x : 𝕜), 0 < x → (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
[PROOFSTEP]
intro x hx
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
x : 𝕜
hx : 0 < x
⊢ (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
[PROOFSTEP]
simp [zpow_sub₀ hx.ne']
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ (fun x => x ^ p / x ^ q) =ᶠ[atBot] fun x => x ^ (↑p - ↑q)
[PROOFSTEP]
apply (eventually_lt_atBot (0 : 𝕜)).mono fun x hx => _
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ ∀ (x : 𝕜), x < 0 → (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
[PROOFSTEP]
intro x hx
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
x : 𝕜
hx : x < 0
⊢ (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
[PROOFSTEP]
simp [zpow_sub₀ hx.ne]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℤ
hn : 0 < n
⊢ Tendsto (fun x => x ^ n) atTop atTop
[PROOFSTEP]
lift n to ℕ using hn.le
[GOAL]
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
hn : 0 < ↑n
⊢ Tendsto (fun x => x ^ ↑n) atTop atTop
[PROOFSTEP]
simp only [zpow_ofNat]
[GOAL]
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
hn : 0 < ↑n
⊢ Tendsto (fun x => x ^ n) atTop atTop
[PROOFSTEP]
exact tendsto_pow_atTop (Nat.cast_pos.mp hn).ne'
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x => x ^ p / x ^ q) atTop atTop
[PROOFSTEP]
rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]
[GOAL]
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (fun x => x ^ (↑p - ↑q)) atTop atTop
[PROOFSTEP]
apply tendsto_zpow_atTop_atTop
[GOAL]
case hn
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
hpq : q < p
⊢ 0 < ↑p - ↑q
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ Tendsto (fun x => x ^ p / x ^ q) atTop (𝓝 0)
[PROOFSTEP]
rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]
[GOAL]
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ Tendsto (fun x => x ^ (↑p - ↑q)) atTop (𝓝 0)
[PROOFSTEP]
apply tendsto_zpow_atTop_zero
[GOAL]
case hn
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ ↑p - ↑q < 0
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ (fun x => x ^ p) =o[atTop] fun x => x ^ q
[PROOFSTEP]
refine' (isLittleO_iff_tendsto' _).mpr (tendsto_pow_div_pow_atTop_zero hpq)
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ ∀ᶠ (x : 𝕜) in atTop, x ^ q = 0 → x ^ p = 0
[PROOFSTEP]
exact (eventually_gt_atTop 0).mono fun x hx hxq => (pow_ne_zero q hx.ne' hxq).elim
[GOAL]
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
⊢ Tendsto (fun x => ‖v x‖) l atTop
[PROOFSTEP]
rcases huv.exists_pos with ⟨c, hc, hcuv⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : 0 < c
hcuv : IsBigOWith c l u v
⊢ Tendsto (fun x => ‖v x‖) l atTop
[PROOFSTEP]
rw [IsBigOWith] at hcuv
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : 0 < c
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
⊢ Tendsto (fun x => ‖v x‖) l atTop
[PROOFSTEP]
convert Tendsto.atTop_div_const hc (tendsto_atTop_mono' l hcuv hu)
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : 0 < c
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
x✝ : α
⊢ ‖v x✝‖ = c * ‖v x✝‖ / c
[PROOFSTEP]
rw [mul_div_cancel_left _ hc.ne.symm]
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ∑ i in range n, g i
[PROOFSTEP]
have A : ∀ i, ‖g i‖ = g i := fun i => Real.norm_of_nonneg (hg i)
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ∑ i in range n, g i
[PROOFSTEP]
have B : ∀ n, ‖∑ i in range n, g i‖ = ∑ i in range n, g i := fun n => by rwa [Real.norm_eq_abs, abs_sum_of_nonneg']
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
n : ℕ
⊢ ‖∑ i in range n, g i‖ = ∑ i in range n, g i
[PROOFSTEP]
rwa [Real.norm_eq_abs, abs_sum_of_nonneg']
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ∑ i in range n, g i
[PROOFSTEP]
apply isLittleO_iff.2 fun ε εpos => _
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
⊢ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (x : ℕ) in atTop, ‖∑ i in range x, f i‖ ≤ ε * ‖∑ i in range x, g i‖
[PROOFSTEP]
intro ε εpos
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (x : ℕ) in atTop, ‖∑ i in range x, f i‖ ≤ ε * ‖∑ i in range x, g i‖
[PROOFSTEP]
obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ b : ℕ, N ≤ b → ‖f b‖ ≤ ε / 2 * g b := by
  simpa only [A, eventually_atTop] using isLittleO_iff.mp h (half_pos εpos)
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
⊢ ∃ N, ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
[PROOFSTEP]
simpa only [A, eventually_atTop] using isLittleO_iff.mp h (half_pos εpos)
[GOAL]
case intro
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
⊢ ∀ᶠ (x : ℕ) in atTop, ‖∑ i in range x, f i‖ ≤ ε * ‖∑ i in range x, g i‖
[PROOFSTEP]
have : (fun _ : ℕ => ∑ i in range N, f i) =o[atTop] fun n : ℕ => ∑ i in range n, g i :=
  by
  apply isLittleO_const_left.2
  exact Or.inr (h'g.congr fun n => (B n).symm)
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
⊢ (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
[PROOFSTEP]
apply isLittleO_const_left.2
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
⊢ ∑ i in range N, f i = 0 ∨ Tendsto (norm ∘ fun n => ∑ i in range n, g i) atTop atTop
[PROOFSTEP]
exact Or.inr (h'g.congr fun n => (B n).symm)
[GOAL]
case intro
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
⊢ ∀ᶠ (x : ℕ) in atTop, ‖∑ i in range x, f i‖ ≤ ε * ‖∑ i in range x, g i‖
[PROOFSTEP]
filter_upwards [isLittleO_iff.1 this (half_pos εpos), Ici_mem_atTop N] with n hn Nn
[GOAL]
case h
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i in range n, f i‖ ≤ ε * ‖∑ i in range n, g i‖
[PROOFSTEP]
calc
  ‖∑ i in range n, f i‖ = ‖(∑ i in range N, f i) + ∑ i in Ico N n, f i‖ := by rw [sum_range_add_sum_Ico _ Nn]
  _ ≤ ‖∑ i in range N, f i‖ + ‖∑ i in Ico N n, f i‖ := (norm_add_le _ _)
  _ ≤ ‖∑ i in range N, f i‖ + ∑ i in Ico N n, ε / 2 * g i :=
    (add_le_add le_rfl (norm_sum_le_of_le _ fun i hi => hN _ (mem_Ico.1 hi).1))
  _ ≤ ‖∑ i in range N, f i‖ + ∑ i in range n, ε / 2 * g i :=
    by
    gcongr
    apply sum_le_sum_of_subset_of_nonneg
    · rw [range_eq_Ico]
      exact Ico_subset_Ico (zero_le _) le_rfl
    · intro i _ _
      exact mul_nonneg (half_pos εpos).le (hg i)
  _ ≤ ε / 2 * ‖∑ i in range n, g i‖ + ε / 2 * ∑ i in range n, g i := by rw [← mul_sum]; gcongr
  _ = ε * ‖∑ i in range n, g i‖ := by
    simp only [B]
    ring
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i in range n, f i‖ = ‖∑ i in range N, f i + ∑ i in Ico N n, f i‖
[PROOFSTEP]
rw [sum_range_add_sum_Ico _ Nn]
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i in range N, f i‖ + ∑ i in Ico N n, ε / 2 * g i ≤ ‖∑ i in range N, f i‖ + ∑ i in range n, ε / 2 * g i
[PROOFSTEP]
gcongr
[GOAL]
case bc
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ∑ i in Ico N n, ε / 2 * g i ≤ ∑ i in range n, ε / 2 * g i
[PROOFSTEP]
apply sum_le_sum_of_subset_of_nonneg
[GOAL]
case bc.h
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ Ico N n ⊆ range n
[PROOFSTEP]
rw [range_eq_Ico]
[GOAL]
case bc.h
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ Ico N n ⊆ Ico 0 n
[PROOFSTEP]
exact Ico_subset_Ico (zero_le _) le_rfl
[GOAL]
case bc.hf
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ∀ (i : ℕ), i ∈ range n → ¬i ∈ Ico N n → 0 ≤ ε / 2 * g i
[PROOFSTEP]
intro i _ _
[GOAL]
case bc.hf
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
i : ℕ
a✝¹ : i ∈ range n
a✝ : ¬i ∈ Ico N n
⊢ 0 ≤ ε / 2 * g i
[PROOFSTEP]
exact mul_nonneg (half_pos εpos).le (hg i)
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i in range N, f i‖ + ∑ i in range n, ε / 2 * g i ≤ ε / 2 * ‖∑ i in range n, g i‖ + ε / 2 * ∑ i in range n, g i
[PROOFSTEP]
rw [← mul_sum]
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i in range N, f i‖ + ε / 2 * ∑ x in range n, g x ≤ ε / 2 * ‖∑ i in range n, g i‖ + ε / 2 * ∑ i in range n, g i
[PROOFSTEP]
gcongr
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ε / 2 * ‖∑ i in range n, g i‖ + ε / 2 * ∑ i in range n, g i = ε * ‖∑ i in range n, g i‖
[PROOFSTEP]
simp only [B]
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n => ∑ i in range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i in range n, g i‖ = ∑ i in range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x => ∑ i in range N, f i) =o[atTop] fun n => ∑ i in range n, g i
n : ℕ
hn : ‖∑ i in range N, f i‖ ≤ ε / 2 * ‖∑ i in range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ε / 2 * ∑ i in range n, g i + ε / 2 * ∑ i in range n, g i = ε * ∑ i in range n, g i
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
[PROOFSTEP]
have := ((isLittleO_one_iff ℝ).2 h).sum_range fun i => zero_le_one
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this :
  Tendsto (fun n => ∑ i in range n, 1) atTop atTop → (fun n => ∑ i in range n, f i) =o[atTop] fun n => ∑ i in range n, 1
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
[PROOFSTEP]
simp only [sum_const, card_range, Nat.smul_one_eq_coe] at this
[GOAL]
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this : Tendsto (fun n => ↑n) atTop atTop → (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
[PROOFSTEP]
exact this tendsto_nat_cast_atTop_atTop
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
⊢ Tendsto (fun n => (↑n)⁻¹ • ∑ i in range n, u i) atTop (𝓝 l)
[PROOFSTEP]
rw [← tendsto_sub_nhds_zero_iff, ← isLittleO_one_iff ℝ]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
⊢ (fun n => (↑n)⁻¹ • ∑ i in range n, u i - l) =o[atTop] fun _x => 1
[PROOFSTEP]
have := Asymptotics.isLittleO_sum_range_of_tendsto_zero (tendsto_sub_nhds_zero_iff.2 h)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
⊢ (fun n => (↑n)⁻¹ • ∑ i in range n, u i - l) =o[atTop] fun _x => 1
[PROOFSTEP]
apply ((isBigO_refl (fun n : ℕ => (n : ℝ)⁻¹) atTop).smul_isLittleO this).congr' _ _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
⊢ (fun x => (↑x)⁻¹ • ∑ i in range x, (u i - l)) =ᶠ[atTop] fun n => (↑n)⁻¹ • ∑ i in range n, u i - l
[PROOFSTEP]
filter_upwards [Ici_mem_atTop 1] with n npos
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
⊢ (↑n)⁻¹ • ∑ i in range n, (u i - l) = (↑n)⁻¹ • ∑ i in range n, u i - l
[PROOFSTEP]
have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
nposℝ : 0 < ↑n
⊢ (↑n)⁻¹ • ∑ i in range n, (u i - l) = (↑n)⁻¹ • ∑ i in range n, u i - l
[PROOFSTEP]
simp only [smul_sub, sum_sub_distrib, sum_const, card_range, sub_right_inj]
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
nposℝ : 0 < ↑n
⊢ (↑n)⁻¹ • n • l = l
[PROOFSTEP]
rw [nsmul_eq_smul_cast ℝ, smul_smul, inv_mul_cancel nposℝ.ne', one_smul]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
⊢ (fun x => (↑x)⁻¹ • ↑x) =ᶠ[atTop] fun _x => 1
[PROOFSTEP]
filter_upwards [Ici_mem_atTop 1] with n npos
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
⊢ (↑n)⁻¹ • ↑n = 1
[PROOFSTEP]
have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n => ∑ i in range n, (u i - l)) =o[atTop] fun n => ↑n
n : ℕ
npos : n ∈ Set.Ici 1
nposℝ : 0 < ↑n
⊢ (↑n)⁻¹ • ↑n = 1
[PROOFSTEP]
rw [Algebra.id.smul_eq_mul, inv_mul_cancel nposℝ.ne']


[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
src✝ : V →ₗ[R] W := f.linear
⊢ Continuous
    {
          toAddHom :=
            { toFun := ↑f.linear,
              map_add' :=
                (_ :
                  ∀ (x y : V),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : V),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom.toFun
[PROOFSTEP]
rw [AffineMap.continuous_linear_iff]
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
src✝ : V →ₗ[R] W := f.linear
⊢ Continuous ↑f.toAffineMap
[PROOFSTEP]
exact f.cont
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
⊢ ↑(contLinear f) = f.linear
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
x✝ : V
⊢ ↑↑(contLinear f) x✝ = ↑f.linear x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
⊢ contLinear f = 0 ↔ ∃ q, f = const R P q
[PROOFSTEP]
have h₁ : f.contLinear = 0 ↔ (f : P →ᵃ[R] Q).linear = 0 :=
  by
  refine' ⟨fun h => _, fun h => _⟩ <;> ext
  · rw [← coe_contLinear_eq_linear, h]; rfl
  · rw [← coe_linear_eq_coe_contLinear, h]; rfl
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
⊢ contLinear f = 0 ↔ f.linear = 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h : contLinear f = 0
⊢ f.linear = 0
[PROOFSTEP]
ext
[GOAL]
case refine'_2
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h : f.linear = 0
⊢ contLinear f = 0
[PROOFSTEP]
ext
[GOAL]
case refine'_1.h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h : contLinear f = 0
x✝ : V
⊢ ↑f.linear x✝ = ↑0 x✝
[PROOFSTEP]
rw [← coe_contLinear_eq_linear, h]
[GOAL]
case refine'_1.h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h : contLinear f = 0
x✝ : V
⊢ ↑↑0 x✝ = ↑0 x✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h : f.linear = 0
x✝ : V
⊢ ↑(contLinear f) x✝ = ↑0 x✝
[PROOFSTEP]
rw [← coe_linear_eq_coe_contLinear, h]
[GOAL]
case refine'_2.h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h : f.linear = 0
x✝ : V
⊢ ↑0 x✝ = ↑0 x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
⊢ contLinear f = 0 ↔ ∃ q, f = const R P q
[PROOFSTEP]
have h₂ : ∀ q : Q, f = const R P q ↔ (f : P →ᵃ[R] Q) = AffineMap.const R P q :=
  by
  intro q
  refine' ⟨fun h => _, fun h => _⟩ <;> ext
  · rw [h]; rfl
  · rw [← coe_to_affineMap, h]; rfl
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
⊢ ∀ (q : Q), f = const R P q ↔ f.toAffineMap = AffineMap.const R P q
[PROOFSTEP]
intro q
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
⊢ f = const R P q ↔ f.toAffineMap = AffineMap.const R P q
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f = const R P q
⊢ f.toAffineMap = AffineMap.const R P q
[PROOFSTEP]
ext
[GOAL]
case refine'_2
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f.toAffineMap = AffineMap.const R P q
⊢ f = const R P q
[PROOFSTEP]
ext
[GOAL]
case refine'_1.h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑f.toAffineMap p✝ = ↑(AffineMap.const R P q) p✝
[PROOFSTEP]
rw [h]
[GOAL]
case refine'_1.h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑(const R P q).toAffineMap p✝ = ↑(AffineMap.const R P q) p✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f.toAffineMap = AffineMap.const R P q
x✝ : P
⊢ ↑f x✝ = ↑(const R P q) x✝
[PROOFSTEP]
rw [← coe_to_affineMap, h]
[GOAL]
case refine'_2.h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
q : Q
h : f.toAffineMap = AffineMap.const R P q
x✝ : P
⊢ ↑(AffineMap.const R P q) x✝ = ↑(const R P q) x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
h₂ : ∀ (q : Q), f = const R P q ↔ f.toAffineMap = AffineMap.const R P q
⊢ contLinear f = 0 ↔ ∃ q, f = const R P q
[PROOFSTEP]
simp_rw [h₁, h₂]
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 : P →A[R] Q
h₁ : contLinear f = 0 ↔ f.linear = 0
h₂ : ∀ (q : Q), f = const R P q ↔ f.toAffineMap = AffineMap.const R P q
⊢ f.linear = 0 ↔ ∃ q, f.toAffineMap = AffineMap.const R P q
[PROOFSTEP]
exact (f : P →ᵃ[R] Q).linear_eq_zero_iff_exists_const
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 →L[R] W
⊢ contLinear (ContinuousLinearMap.toContinuousAffineMap f) = f
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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 →L[R] W
x✝ : V
⊢ ↑(contLinear (ContinuousLinearMap.toContinuousAffineMap f)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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)
[PROOFSTEP]
rcases f with ⟨f, h⟩
[GOAL]
case mk
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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)
[PROOFSTEP]
rw [coe_mk_const_linear_eq_linear, coe_mk, f.decomp, Pi.add_apply, LinearMap.map_zero, zero_add, ← Function.const_def]
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
h : ↑f 0 = 0
⊢ ‖f‖ = max ‖↑f 0‖ ‖contLinear f‖
[PROOFSTEP]
rw [norm_def]
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
h : ↑f 0 = 0
⊢ max ‖↑f 0‖ ‖contLinear f‖ = max 0 ‖contLinear f‖
[PROOFSTEP]
rw [h, norm_zero]
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
⊢ (fun f => max ‖↑f 0‖ ‖contLinear f‖) 0 = 0
[PROOFSTEP]
simp [(ContinuousAffineMap.zero_apply)]
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f g : V →A[𝕜] W
⊢ (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
    (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g
[PROOFSTEP]
simp only [coe_add, max_le_iff]
  -- Porting note: previously `Pi.add_apply, add_contLinear, ` in the previous `simp only`
          -- suffices, but now they don't fire.
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f g : V →A[𝕜] W
⊢ ‖(↑f + ↑g) 0‖ ≤ max ‖↑f 0‖ ‖contLinear f‖ + max ‖↑g 0‖ ‖contLinear g‖ ∧
    ‖contLinear (f + g)‖ ≤ max ‖↑f 0‖ ‖contLinear f‖ + max ‖↑g 0‖ ‖contLinear g‖
[PROOFSTEP]
rw [add_contLinear]
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f g : V →A[𝕜] W
⊢ ‖(↑f + ↑g) 0‖ ≤ max ‖↑f 0‖ ‖contLinear f‖ + max ‖↑g 0‖ ‖contLinear g‖ ∧
    ‖contLinear f + contLinear g‖ ≤ max ‖↑f 0‖ ‖contLinear f‖ + max ‖↑g 0‖ ‖contLinear g‖
[PROOFSTEP]
exact
  ⟨(norm_add_le _ _).trans (add_le_add (le_max_left _ _) (le_max_left _ _)),
    (norm_add_le _ _).trans (add_le_add (le_max_right _ _) (le_max_right _ _))⟩
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f : V →A[𝕜] W
⊢ (fun f => max ‖↑f 0‖ ‖contLinear f‖) (-f) = (fun f => max ‖↑f 0‖ ‖contLinear f‖) f
[PROOFSTEP]
simp [(ContinuousAffineMap.neg_apply)]
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f : V →A[𝕜] W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      f =
    0
⊢ f = 0
[PROOFSTEP]
rcases max_eq_iff.mp h₀ with (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
[GOAL]
case inl.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f : V →A[𝕜] W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      f =
    0
h₁ : ‖↑f 0‖ = 0
h₂ : ‖contLinear f‖ ≤ ‖↑f 0‖
⊢ f = 0
[PROOFSTEP]
rw [h₁] at h₂
[GOAL]
case inr.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f : V →A[𝕜] W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      f =
    0
h₁ : ‖contLinear f‖ = 0
h₂ : ‖↑f 0‖ ≤ ‖contLinear f‖
⊢ f = 0
[PROOFSTEP]
rw [h₁] at h₂
[GOAL]
case inl.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f : V →A[𝕜] W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      f =
    0
h₁ : ‖↑f 0‖ = 0
h₂ : ‖contLinear f‖ ≤ 0
⊢ f = 0
[PROOFSTEP]
rw [norm_le_zero_iff, contLinear_eq_zero_iff_exists_const] at h₂
[GOAL]
case inl.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f : V →A[𝕜] W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      f =
    0
h₁ : ‖↑f 0‖ = 0
h₂ : ∃ q, f = const 𝕜 V q
⊢ f = 0
[PROOFSTEP]
obtain ⟨q, rfl⟩ := h₂
[GOAL]
case inl.intro.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
q : W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      (const 𝕜 V q) =
    0
h₁ : ‖↑(const 𝕜 V q) 0‖ = 0
⊢ const 𝕜 V q = 0
[PROOFSTEP]
simp only [norm_eq_zero] at h₁
[GOAL]
case inl.intro.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
q : W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      (const 𝕜 V q) =
    0
h₁ : ↑(const 𝕜 V q) 0 = 0
⊢ const 𝕜 V q = 0
[PROOFSTEP]
rw [coe_const, Function.const_apply] at h₁
[GOAL]
case inl.intro.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
q : W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      (const 𝕜 V q) =
    0
h₁ : q = 0
⊢ const 𝕜 V q = 0
[PROOFSTEP]
rw [h₁]
[GOAL]
case inl.intro.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
q : W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      (const 𝕜 V q) =
    0
h₁ : q = 0
⊢ const 𝕜 V 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case inr.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f : V →A[𝕜] W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      f =
    0
h₁ : ‖contLinear f‖ = 0
h₂ : ‖↑f 0‖ ≤ 0
⊢ f = 0
[PROOFSTEP]
rw [norm_eq_zero', contLinear_eq_zero_iff_exists_const] at h₁
[GOAL]
case inr.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f : V →A[𝕜] W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      f =
    0
h₁ : ∃ q, f = const 𝕜 V q
h₂ : ‖↑f 0‖ ≤ 0
⊢ f = 0
[PROOFSTEP]
obtain ⟨q, rfl⟩ := h₁
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
q : W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      (const 𝕜 V q) =
    0
h₂ : ‖↑(const 𝕜 V q) 0‖ ≤ 0
⊢ const 𝕜 V q = 0
[PROOFSTEP]
simp only [norm_le_zero_iff] at h₂
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
q : W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      (const 𝕜 V q) =
    0
h₂ : ↑(const 𝕜 V q) 0 = 0
⊢ const 𝕜 V q = 0
[PROOFSTEP]
rw [coe_const, Function.const_apply] at h₂
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
q : W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      (const 𝕜 V q) =
    0
h₂ : q = 0
⊢ const 𝕜 V q = 0
[PROOFSTEP]
rw [h₂]
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
q : W
h₀ :
  AddGroupSeminorm.toFun
      { toFun := fun f => max ‖↑f 0‖ ‖contLinear f‖, map_zero' := (_ : max ‖↑0 0‖ ‖0‖ = 0),
        add_le' :=
          (_ :
            ∀ (f g : V →A[𝕜] W),
              (fun f => max ‖↑f 0‖ ‖contLinear f‖) (f + g) ≤
                (fun f => max ‖↑f 0‖ ‖contLinear f‖) f + (fun f => max ‖↑f 0‖ ‖contLinear f‖) g),
        neg' := (_ : ∀ (f : V →A[𝕜] W), max ‖↑(-f) 0‖ ‖-contLinear f‖ = max ‖↑f 0‖ ‖contLinear f‖) }
      (const 𝕜 V q) =
    0
h₂ : q = 0
⊢ const 𝕜 V 0 = 0
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
t : 𝕜
f : V →A[𝕜] W
⊢ ‖t • f‖ ≤ ‖t‖ * ‖f‖
[PROOFSTEP]
simp only [norm_def, (smul_contLinear), norm_smul]
  -- Porting note: previously all these rewrites were in the `simp only`,
      -- but now they don't fire.
      -- (in fact, `norm_smul` fires, but only once rather than twice!)
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
t : 𝕜
f : V →A[𝕜] W
⊢ max ‖↑(t • f) 0‖ (‖t‖ * ‖contLinear f‖) ≤ ‖t‖ * max ‖↑f 0‖ ‖contLinear f‖
[PROOFSTEP]
rw [coe_smul, Pi.smul_apply, norm_smul, ← mul_max_of_nonneg _ _ (norm_nonneg t)]
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖comp f g‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖
[PROOFSTEP]
rw [norm_def, max_le_iff]
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖↑(comp f g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖ ∧ ‖contLinear (comp f g)‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖
[PROOFSTEP]
constructor
[GOAL]
case left
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖↑(comp f g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖
[PROOFSTEP]
calc
  ‖f.comp g 0‖ = ‖f (g 0)‖ := by simp
  _ = ‖f.contLinear (g 0) + f 0‖ := by rw [f.decomp]; simp
  _ ≤ ‖f.contLinear‖ * ‖g 0‖ + ‖f 0‖ := ((norm_add_le _ _).trans (add_le_add_right (f.contLinear.le_op_norm _) _))
  _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ :=
    add_le_add_right (mul_le_mul f.norm_contLinear_le g.norm_image_zero_le (norm_nonneg _) (norm_nonneg _)) _
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖↑(comp f g) 0‖ = ‖↑f (↑g 0)‖
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖↑f (↑g 0)‖ = ‖↑(contLinear f) (↑g 0) + ↑f 0‖
[PROOFSTEP]
rw [f.decomp]
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖(↑(contLinear f) + Function.const V (↑f 0)) (↑g 0)‖ =
    ‖↑(contLinear f) (↑g 0) + (↑(contLinear f) + Function.const V (↑f 0)) 0‖
[PROOFSTEP]
simp
[GOAL]
case right
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖contLinear (comp f g)‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖
[PROOFSTEP]
calc
  ‖(f.comp g).contLinear‖ ≤ ‖f.contLinear‖ * ‖g.contLinear‖ :=
    (g.comp_contLinear f).symm ▸ f.contLinear.op_norm_comp_le _
  _ ≤ ‖f‖ * ‖g‖ := (mul_le_mul f.norm_contLinear_le g.norm_contLinear_le (norm_nonneg _) (norm_nonneg _))
  _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by rw [le_add_iff_nonneg_right]; apply norm_nonneg
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖f‖ * ‖g‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖
[PROOFSTEP]
rw [le_add_iff_nonneg_right]
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
g : W₂ →A[𝕜] V
⊢ 0 ≤ ‖↑f 0‖
[PROOFSTEP]
apply norm_nonneg
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f : V →A[𝕜] W
⊢ (fun p => ContinuousLinearMap.toContinuousAffineMap p.snd + const 𝕜 V p.fst)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f => (↑f 0, contLinear f),
                map_add' :=
                  (_ :
                    ∀ (x x_1 : V →A[𝕜] W),
                      (fun f => (↑f 0, contLinear f)) (x + x_1) = (fun f => (↑f 0, contLinear f)) (x + x_1)) },
            map_smul' :=
              (_ :
                ∀ (x : 𝕜) (x_1 : V →A[𝕜] W),
                  AddHom.toFun
                      { toFun := fun f => (↑f 0, contLinear f),
                        map_add' :=
                          (_ :
                            ∀ (x x_2 : V →A[𝕜] W),
                              (fun f => (↑f 0, contLinear f)) (x + x_2) = (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                      (x • x_1) =
                    AddHom.toFun
                      { toFun := fun f => (↑f 0, contLinear f),
                        map_add' :=
                          (_ :
                            ∀ (x x_2 : V →A[𝕜] W),
                              (fun f => (↑f 0, contLinear f)) (x + x_2) = (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                      (x • x_1)) }.toAddHom
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f : V →A[𝕜] W
x✝ : V
⊢ ↑((fun p => ContinuousLinearMap.toContinuousAffineMap p.snd + const 𝕜 V p.fst)
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => (↑f 0, contLinear f),
                    map_add' :=
                      (_ :
                        ∀ (x x_1 : V →A[𝕜] W),
                          (fun f => (↑f 0, contLinear f)) (x + x_1) = (fun f => (↑f 0, contLinear f)) (x + x_1)) },
                map_smul' :=
                  (_ :
                    ∀ (x : 𝕜) (x_1 : V →A[𝕜] W),
                      AddHom.toFun
                          { toFun := fun f => (↑f 0, contLinear f),
                            map_add' :=
                              (_ :
                                ∀ (x x_2 : V →A[𝕜] W),
                                  (fun f => (↑f 0, contLinear f)) (x + x_2) =
                                    (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                          (x • x_1) =
                        AddHom.toFun
                          { toFun := fun f => (↑f 0, contLinear f),
                            map_add' :=
                              (_ :
                                ∀ (x x_2 : V →A[𝕜] W),
                                  (fun f => (↑f 0, contLinear f)) (x + x_2) =
                                    (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                          (x • x_1)) }.toAddHom
            f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
rw [f.decomp]
  -- Porting note: previously `simp` closed the goal, but now we need to rewrite:
[GOAL]
case h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f : V →A[𝕜] W
x✝ : V
⊢ ↑((fun p => ContinuousLinearMap.toContinuousAffineMap p.snd + const 𝕜 V p.fst)
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => (↑f 0, contLinear f),
                    map_add' :=
                      (_ :
                        ∀ (x x_1 : V →A[𝕜] W),
                          (fun f => (↑f 0, contLinear f)) (x + x_1) = (fun f => (↑f 0, contLinear f)) (x + x_1)) },
                map_smul' :=
                  (_ :
                    ∀ (x : 𝕜) (x_1 : V →A[𝕜] W),
                      AddHom.toFun
                          { toFun := fun f => (↑f 0, contLinear f),
                            map_add' :=
                              (_ :
                                ∀ (x x_2 : V →A[𝕜] W),
                                  (fun f => (↑f 0, contLinear f)) (x + x_2) =
                                    (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                          (x • x_1) =
                        AddHom.toFun
                          { toFun := fun f => (↑f 0, contLinear f),
                            map_add' :=
                              (_ :
                                ∀ (x x_2 : V →A[𝕜] W),
                                  (fun f => (↑f 0, contLinear f)) (x + x_2) =
                                    (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                          (x • x_1)) }.toAddHom
            f))
      x✝ =
    (↑(contLinear f) + Function.const V (↑f 0)) x✝
[PROOFSTEP]
simp only [coe_add, ContinuousLinearMap.coe_toContinuousAffineMap, Pi.add_apply]
[GOAL]
case h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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✝ f : V →A[𝕜] W
x✝ : V
⊢ ↑(contLinear f) x✝ + ↑(const 𝕜 V (↑f 0)) x✝ = ↑(contLinear f) x✝ + Function.const V (↑f 0) x✝
[PROOFSTEP]
rw [ContinuousAffineMap.coe_const, Function.const_apply]
[GOAL]
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
⊢ Function.RightInverse (fun p => ContinuousLinearMap.toContinuousAffineMap p.snd + const 𝕜 V p.fst)
    {
          toAddHom :=
            { toFun := fun f => (↑f 0, contLinear f),
              map_add' :=
                (_ :
                  ∀ (x x_1 : V →A[𝕜] W),
                    (fun f => (↑f 0, contLinear f)) (x + x_1) = (fun f => (↑f 0, contLinear f)) (x + x_1)) },
          map_smul' :=
            (_ :
              ∀ (x : 𝕜) (x_1 : V →A[𝕜] W),
                AddHom.toFun
                    { toFun := fun f => (↑f 0, contLinear f),
                      map_add' :=
                        (_ :
                          ∀ (x x_2 : V →A[𝕜] W),
                            (fun f => (↑f 0, contLinear f)) (x + x_2) = (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                    (x • x_1) =
                  AddHom.toFun
                    { toFun := fun f => (↑f 0, contLinear f),
                      map_add' :=
                        (_ :
                          ∀ (x x_2 : V →A[𝕜] W),
                            (fun f => (↑f 0, contLinear f)) (x + x_2) = (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                    (x • x_1)) }.toAddHom.toFun
[PROOFSTEP]
rintro ⟨v, f⟩
[GOAL]
case mk
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
v : W
f : V →L[𝕜] W
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f => (↑f 0, contLinear f),
              map_add' :=
                (_ :
                  ∀ (x x_1 : V →A[𝕜] W),
                    (fun f => (↑f 0, contLinear f)) (x + x_1) = (fun f => (↑f 0, contLinear f)) (x + x_1)) },
          map_smul' :=
            (_ :
              ∀ (x : 𝕜) (x_1 : V →A[𝕜] W),
                AddHom.toFun
                    { toFun := fun f => (↑f 0, contLinear f),
                      map_add' :=
                        (_ :
                          ∀ (x x_2 : V →A[𝕜] W),
                            (fun f => (↑f 0, contLinear f)) (x + x_2) = (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                    (x • x_1) =
                  AddHom.toFun
                    { toFun := fun f => (↑f 0, contLinear f),
                      map_add' :=
                        (_ :
                          ∀ (x x_2 : V →A[𝕜] W),
                            (fun f => (↑f 0, contLinear f)) (x + x_2) = (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                    (x • x_1)) }.toAddHom
      ((fun p => ContinuousLinearMap.toContinuousAffineMap p.snd + const 𝕜 V p.fst) (v, f)) =
    (v, f)
[PROOFSTEP]
ext
[GOAL]
case mk.h₁
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
v : W
f : V →L[𝕜] W
⊢ (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f => (↑f 0, contLinear f),
                map_add' :=
                  (_ :
                    ∀ (x x_1 : V →A[𝕜] W),
                      (fun f => (↑f 0, contLinear f)) (x + x_1) = (fun f => (↑f 0, contLinear f)) (x + x_1)) },
            map_smul' :=
              (_ :
                ∀ (x : 𝕜) (x_1 : V →A[𝕜] W),
                  AddHom.toFun
                      { toFun := fun f => (↑f 0, contLinear f),
                        map_add' :=
                          (_ :
                            ∀ (x x_2 : V →A[𝕜] W),
                              (fun f => (↑f 0, contLinear f)) (x + x_2) = (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                      (x • x_1) =
                    AddHom.toFun
                      { toFun := fun f => (↑f 0, contLinear f),
                        map_add' :=
                          (_ :
                            ∀ (x x_2 : V →A[𝕜] W),
                              (fun f => (↑f 0, contLinear f)) (x + x_2) = (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                      (x • x_1)) }.toAddHom
        ((fun p => ContinuousLinearMap.toContinuousAffineMap p.snd + const 𝕜 V p.fst) (v, f))).fst =
    (v, f).fst
[PROOFSTEP]
simp
[GOAL]
case mk.h₂.h
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
W₂ : Type u_5
P : Type u_6
Q : Type u_7
Q₂ : Type u_8
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[𝕜] W
v : W
f : V →L[𝕜] W
x✝ : V
⊢ ↑(AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => (↑f 0, contLinear f),
                    map_add' :=
                      (_ :
                        ∀ (x x_1 : V →A[𝕜] W),
                          (fun f => (↑f 0, contLinear f)) (x + x_1) = (fun f => (↑f 0, contLinear f)) (x + x_1)) },
                map_smul' :=
                  (_ :
                    ∀ (x : 𝕜) (x_1 : V →A[𝕜] W),
                      AddHom.toFun
                          { toFun := fun f => (↑f 0, contLinear f),
                            map_add' :=
                              (_ :
                                ∀ (x x_2 : V →A[𝕜] W),
                                  (fun f => (↑f 0, contLinear f)) (x + x_2) =
                                    (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                          (x • x_1) =
                        AddHom.toFun
                          { toFun := fun f => (↑f 0, contLinear f),
                            map_add' :=
                              (_ :
                                ∀ (x x_2 : V →A[𝕜] W),
                                  (fun f => (↑f 0, contLinear f)) (x + x_2) =
                                    (fun f => (↑f 0, contLinear f)) (x + x_2)) }
                          (x • x_1)) }.toAddHom
            ((fun p => ContinuousLinearMap.toContinuousAffineMap p.snd + const 𝕜 V p.fst) (v, f))).snd
      x✝ =
    ↑(v, f).snd x✝
[PROOFSTEP]
simp