case refine'_1
𝕜 : Type u_1
𝕜₂ : Type ?u.2121574
𝕜₃ : Type ?u.2121577
E : Type u_2
Eₗ : Type ?u.2121583
F : Type ?u.2121586
Fₗ : Type ?u.2121589
G : Type ?u.2121592
Gₗ : Type ?u.2121595
𝓕 : Type ?u.2121598
inst✝²² : SeminormedAddCommGroup E
inst✝²¹ : SeminormedAddCommGroup Eₗ
inst✝²⁰ : SeminormedAddCommGroup F
inst✝¹⁹ : SeminormedAddCommGroup Fₗ
inst✝¹⁸ : SeminormedAddCommGroup G
inst✝¹⁷ : SeminormedAddCommGroup Gₗ
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜 Eₗ
inst✝¹¹ : NormedSpace 𝕜₂ F
inst✝¹⁰ : NormedSpace 𝕜 Fₗ
inst✝⁹ : NormedSpace 𝕜₃ G
inst✝⁸ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁶ : RingHomIsometric σ₂₃
inst✝⁵ : RingHomIsometric σ₁₃
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type ?u.2124098
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
x✝ : E
x : 𝕜
⊢ ‖↑(toSpanSingleton 𝕜 x✝) x‖ ≤ ‖x✝‖ * ‖x‖

case refine'_2
𝕜 : Type u_1
𝕜₂ : Type ?u.2121574
𝕜₃ : Type ?u.2121577
E : Type u_2
Eₗ : Type ?u.2121583
F : Type ?u.2121586
Fₗ : Type ?u.2121589
G : Type ?u.2121592
Gₗ : Type ?u.2121595
𝓕 : Type ?u.2121598
inst✝²² : SeminormedAddCommGroup E
inst✝²¹ : SeminormedAddCommGroup Eₗ
inst✝²⁰ : SeminormedAddCommGroup F
inst✝¹⁹ : SeminormedAddCommGroup Fₗ
inst✝¹⁸ : SeminormedAddCommGroup G
inst✝¹⁷ : SeminormedAddCommGroup Gₗ
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜 Eₗ
inst✝¹¹ : NormedSpace 𝕜₂ F
inst✝¹⁰ : NormedSpace 𝕜 Fₗ
inst✝⁹ : NormedSpace 𝕜₃ G
inst✝⁸ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁶ : RingHomIsometric σ₂₃
inst✝⁵ : RingHomIsometric σ₁₃
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type ?u.2124098
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
x : E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x_1 : 𝕜), ‖↑(toSpanSingleton 𝕜 x) x_1‖ ≤ N * ‖x_1‖
⊢ ‖x‖ ≤ N
𝕜 : Type u_1
𝕜₂ : Type ?u.2121574
𝕜₃ : Type ?u.2121577
E : Type u_2
Eₗ : Type ?u.2121583
F : Type ?u.2121586
Fₗ : Type ?u.2121589
G : Type ?u.2121592
Gₗ : Type ?u.2121595
𝓕 : Type ?u.2121598
inst✝²² : SeminormedAddCommGroup E
inst✝²¹ : SeminormedAddCommGroup Eₗ
inst✝²⁰ : SeminormedAddCommGroup F
inst✝¹⁹ : SeminormedAddCommGroup Fₗ
inst✝¹⁸ : SeminormedAddCommGroup G
inst✝¹⁷ : SeminormedAddCommGroup Gₗ
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜 Eₗ
inst✝¹¹ : NormedSpace 𝕜₂ F
inst✝¹⁰ : NormedSpace 𝕜 Fₗ
inst✝⁹ : NormedSpace 𝕜₃ G
inst✝⁸ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁶ : RingHomIsometric σ₂₃
inst✝⁵ : RingHomIsometric σ₁₃
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type ?u.2124098
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
x : E
⊢ ‖toSpanSingleton 𝕜 x‖ = ‖x‖
refine' op_norm_eq_of_bounds (norm_nonneg _) (fun x => _) fun N _ h => _
no goals
case refine'_1
𝕜 : Type u_1
𝕜₂ : Type ?u.2121574
𝕜₃ : Type ?u.2121577
E : Type u_2
Eₗ : Type ?u.2121583
F : Type ?u.2121586
Fₗ : Type ?u.2121589
G : Type ?u.2121592
Gₗ : Type ?u.2121595
𝓕 : Type ?u.2121598
inst✝²² : SeminormedAddCommGroup E
inst✝²¹ : SeminormedAddCommGroup Eₗ
inst✝²⁰ : SeminormedAddCommGroup F
inst✝¹⁹ : SeminormedAddCommGroup Fₗ
inst✝¹⁸ : SeminormedAddCommGroup G
inst✝¹⁷ : SeminormedAddCommGroup Gₗ
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜 Eₗ
inst✝¹¹ : NormedSpace 𝕜₂ F
inst✝¹⁰ : NormedSpace 𝕜 Fₗ
inst✝⁹ : NormedSpace 𝕜₃ G
inst✝⁸ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁶ : RingHomIsometric σ₂₃
inst✝⁵ : RingHomIsometric σ₁₃
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type ?u.2124098
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
x✝ : E
x : 𝕜
⊢ ‖↑(toSpanSingleton 𝕜 x✝) x‖ ≤ ‖x✝‖ * ‖x‖
rw [toSpanSingleton_apply, norm_smul, mul_comm]
case refine'_2
𝕜 : Type u_1
𝕜₂ : Type ?u.2121574
𝕜₃ : Type ?u.2121577
E : Type u_2
Eₗ : Type ?u.2121583
F : Type ?u.2121586
Fₗ : Type ?u.2121589
G : Type ?u.2121592
Gₗ : Type ?u.2121595
𝓕 : Type ?u.2121598
inst✝²² : SeminormedAddCommGroup E
inst✝²¹ : SeminormedAddCommGroup Eₗ
inst✝²⁰ : SeminormedAddCommGroup F
inst✝¹⁹ : SeminormedAddCommGroup Fₗ
inst✝¹⁸ : SeminormedAddCommGroup G
inst✝¹⁷ : SeminormedAddCommGroup Gₗ
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜 Eₗ
inst✝¹¹ : NormedSpace 𝕜₂ F
inst✝¹⁰ : NormedSpace 𝕜 Fₗ
inst✝⁹ : NormedSpace 𝕜₃ G
inst✝⁸ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁶ : RingHomIsometric σ₂₃
inst✝⁵ : RingHomIsometric σ₁₃
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type ?u.2124098
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
x : E
N : ℝ
x✝ : N ≥ 0
h : ‖↑(toSpanSingleton 𝕜 x) 1‖ ≤ N * ‖1‖
⊢ ‖x‖ ≤ N
case refine'_2
𝕜 : Type u_1
𝕜₂ : Type ?u.2121574
𝕜₃ : Type ?u.2121577
E : Type u_2
Eₗ : Type ?u.2121583
F : Type ?u.2121586
Fₗ : Type ?u.2121589
G : Type ?u.2121592
Gₗ : Type ?u.2121595
𝓕 : Type ?u.2121598
inst✝²² : SeminormedAddCommGroup E
inst✝²¹ : SeminormedAddCommGroup Eₗ
inst✝²⁰ : SeminormedAddCommGroup F
inst✝¹⁹ : SeminormedAddCommGroup Fₗ
inst✝¹⁸ : SeminormedAddCommGroup G
inst✝¹⁷ : SeminormedAddCommGroup Gₗ
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜 Eₗ
inst✝¹¹ : NormedSpace 𝕜₂ F
inst✝¹⁰ : NormedSpace 𝕜 Fₗ
inst✝⁹ : NormedSpace 𝕜₃ G
inst✝⁸ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁶ : RingHomIsometric σ₂₃
inst✝⁵ : RingHomIsometric σ₁₃
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type ?u.2124098
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
x : E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x_1 : 𝕜), ‖↑(toSpanSingleton 𝕜 x) x_1‖ ≤ N * ‖x_1‖
⊢ ‖x‖ ≤ N
specialize h 1
case refine'_2
𝕜 : Type u_1
𝕜₂ : Type ?u.2121574
𝕜₃ : Type ?u.2121577
E : Type u_2
Eₗ : Type ?u.2121583
F : Type ?u.2121586
Fₗ : Type ?u.2121589
G : Type ?u.2121592
Gₗ : Type ?u.2121595
𝓕 : Type ?u.2121598
inst✝²² : SeminormedAddCommGroup E
inst✝²¹ : SeminormedAddCommGroup Eₗ
inst✝²⁰ : SeminormedAddCommGroup F
inst✝¹⁹ : SeminormedAddCommGroup Fₗ
inst✝¹⁸ : SeminormedAddCommGroup G
inst✝¹⁷ : SeminormedAddCommGroup Gₗ
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜 Eₗ
inst✝¹¹ : NormedSpace 𝕜₂ F
inst✝¹⁰ : NormedSpace 𝕜 Fₗ
inst✝⁹ : NormedSpace 𝕜₃ G
inst✝⁸ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁶ : RingHomIsometric σ₂₃
inst✝⁵ : RingHomIsometric σ₁₃
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type ?u.2124098
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
x : E
N : ℝ
x✝ : N ≥ 0
h : ‖x‖ * ‖1‖ ≤ N * ‖1‖
⊢ ‖x‖ ≤ N
case refine'_2
𝕜 : Type u_1
𝕜₂ : Type ?u.2121574
𝕜₃ : Type ?u.2121577
E : Type u_2
Eₗ : Type ?u.2121583
F : Type ?u.2121586
Fₗ : Type ?u.2121589
G : Type ?u.2121592
Gₗ : Type ?u.2121595
𝓕 : Type ?u.2121598
inst✝²² : SeminormedAddCommGroup E
inst✝²¹ : SeminormedAddCommGroup Eₗ
inst✝²⁰ : SeminormedAddCommGroup F
inst✝¹⁹ : SeminormedAddCommGroup Fₗ
inst✝¹⁸ : SeminormedAddCommGroup G
inst✝¹⁷ : SeminormedAddCommGroup Gₗ
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜 Eₗ
inst✝¹¹ : NormedSpace 𝕜₂ F
inst✝¹⁰ : NormedSpace 𝕜 Fₗ
inst✝⁹ : NormedSpace 𝕜₃ G
inst✝⁸ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁶ : RingHomIsometric σ₂₃
inst✝⁵ : RingHomIsometric σ₁₃
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type ?u.2124098
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
x : E
N : ℝ
x✝ : N ≥ 0
h : ‖↑(toSpanSingleton 𝕜 x) 1‖ ≤ N * ‖1‖
⊢ ‖x‖ ≤ N
rw [toSpanSingleton_apply, norm_smul, mul_comm] at h
no goals
case refine'_2
𝕜 : Type u_1
𝕜₂ : Type ?u.2121574
𝕜₃ : Type ?u.2121577
E : Type u_2
Eₗ : Type ?u.2121583
F : Type ?u.2121586
Fₗ : Type ?u.2121589
G : Type ?u.2121592
Gₗ : Type ?u.2121595
𝓕 : Type ?u.2121598
inst✝²² : SeminormedAddCommGroup E
inst✝²¹ : SeminormedAddCommGroup Eₗ
inst✝²⁰ : SeminormedAddCommGroup F
inst✝¹⁹ : SeminormedAddCommGroup Fₗ
inst✝¹⁸ : SeminormedAddCommGroup G
inst✝¹⁷ : SeminormedAddCommGroup Gₗ
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜 Eₗ
inst✝¹¹ : NormedSpace 𝕜₂ F
inst✝¹⁰ : NormedSpace 𝕜 Fₗ
inst✝⁹ : NormedSpace 𝕜₃ G
inst✝⁸ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁶ : RingHomIsometric σ₂₃
inst✝⁵ : RingHomIsometric σ₁₃
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type ?u.2124098
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
x : E
N : ℝ
x✝ : N ≥ 0
h : ‖x‖ * ‖1‖ ≤ N * ‖1‖
⊢ ‖x‖ ≤ N
exact (mul_le_mul_right (by simp)).mp h
no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.2121574
𝕜₃ : Type ?u.2121577
E : Type u_2
Eₗ : Type ?u.2121583
F : Type ?u.2121586
Fₗ : Type ?u.2121589
G : Type ?u.2121592
Gₗ : Type ?u.2121595
𝓕 : Type ?u.2121598
inst✝²² : SeminormedAddCommGroup E
inst✝²¹ : SeminormedAddCommGroup Eₗ
inst✝²⁰ : SeminormedAddCommGroup F
inst✝¹⁹ : SeminormedAddCommGroup Fₗ
inst✝¹⁸ : SeminormedAddCommGroup G
inst✝¹⁷ : SeminormedAddCommGroup Gₗ
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜 Eₗ
inst✝¹¹ : NormedSpace 𝕜₂ F
inst✝¹⁰ : NormedSpace 𝕜 Fₗ
inst✝⁹ : NormedSpace 𝕜₃ G
inst✝⁸ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁶ : RingHomIsometric σ₂₃
inst✝⁵ : RingHomIsometric σ₁₃
inst✝⁴ : RingHomIsometric σ₁₂
𝕜' : Type ?u.2124098
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
x : E
N : ℝ
x✝ : N ≥ 0
h : ‖x‖ * ‖1‖ ≤ N * ‖1‖
⊢ 0 < ‖1‖
simp