-- Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean
theorem opNorm_lsmul [NormedField R] [NormedAlgebra 𝕜 R] [NormedSpace R E]
    [IsScalarTower 𝕜 R E] [Nontrivial E] : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ = 1

Proof state:
case refine_2.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : R), ‖(lsmul 𝕜 R) x‖ ≤ N * ‖x‖
y : E
hy : y ≠ 0
this : ‖y‖ ≤ N * ‖y‖
⊢ 1 ≤ N

Tactic:
refine le_of_mul_le_mul_right ?_ (norm_pos_iff.mpr hy)

Result:
case refine_2.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : R), ‖(lsmul 𝕜 R) x‖ ≤ N * ‖x‖
y : E
hy : y ≠ 0
this : ‖y‖ ≤ N * ‖y‖
⊢ 1 * ‖y‖ ≤ N * ‖y‖

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
x : R
⊢ ‖(lsmul 𝕜 R) x‖ ≤ ‖x‖

Tactic:
apply opNorm_lsmul_apply_le

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
x : R
⊢ ‖(lsmul 𝕜 R) x‖ ≤ 1 * ‖x‖

Tactic:
rw [one_mul]

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
x : R
⊢ ‖(lsmul 𝕜 R) x‖ ≤ ‖x‖

Proof state:
case refine_2.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : R), ‖(lsmul 𝕜 R) x‖ ≤ N * ‖x‖
y : E
hy : y ≠ 0
this : ‖((lsmul 𝕜 R) 1) y‖ ≤ N * ‖1‖ * ‖y‖
⊢ 1 ≤ N

Tactic:
simp_rw [lsmul_apply, one_smul, norm_one, mul_one] at this

Result:
case refine_2.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : R), ‖(lsmul 𝕜 R) x‖ ≤ N * ‖x‖
y : E
hy : y ≠ 0
this : ‖y‖ ≤ N * ‖y‖
⊢ 1 ≤ N

Proof state:
case refine_2.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : R), ‖(lsmul 𝕜 R) x‖ ≤ N * ‖x‖
y : E
hy : y ≠ 0
this : ‖y‖ ≤ N * ‖y‖
⊢ 1 * ‖y‖ ≤ N * ‖y‖

Tactic:
simp_rw [one_mul, this]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
⊢ ‖lsmul 𝕜 R‖ = 1

Tactic:
refine ContinuousLinearMap.opNorm_eq_of_bounds zero_le_one (fun x => ?_) fun N _ h => ?_

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
x : R
⊢ ‖(lsmul 𝕜 R) x‖ ≤ 1 * ‖x‖

case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : R), ‖(lsmul 𝕜 R) x‖ ≤ N * ‖x‖
⊢ 1 ≤ N

Proof state:
case refine_2.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : R), ‖(lsmul 𝕜 R) x‖ ≤ N * ‖x‖
y : E
hy : y ≠ 0
⊢ 1 ≤ N

Tactic:
have := le_of_opNorm_le _ (h 1) y

Result:
case refine_2.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : R), ‖(lsmul 𝕜 R) x‖ ≤ N * ‖x‖
y : E
hy : y ≠ 0
this : ‖((lsmul 𝕜 R) 1) y‖ ≤ N * ‖1‖ * ‖y‖
⊢ 1 ≤ N

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : R), ‖(lsmul 𝕜 R) x‖ ≤ N * ‖x‖
⊢ 1 ≤ N

Tactic:
obtain ⟨y, hy⟩ := exists_ne (0 : E)

Result:
case refine_2.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : NormedField R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : NormedSpace R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : R), ‖(lsmul 𝕜 R) x‖ ≤ N * ‖x‖
y : E
hy : y ≠ 0
⊢ 1 ≤ N