[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x : Unitization 𝕜 A
⊢ (fst x + 0, ↑↑(↑lift (NonUnitalAlgHom.Lmul 𝕜 A)) x) =
    (fst x, ↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x))
[PROOFSTEP]
rw [add_zero]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x : Unitization 𝕜 A
⊢ (fst x, ↑↑(↑lift (NonUnitalAlgHom.Lmul 𝕜 A)) x) = (fst x, ↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x))
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
⊢ Function.Injective ↑(splitMul 𝕜 A)
[PROOFSTEP]
rw [injective_iff_map_eq_zero]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
⊢ ∀ (a : Unitization 𝕜 A), ↑(splitMul 𝕜 A) a = 0 → a = 0
[PROOFSTEP]
intro x hx
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
x : Unitization 𝕜 A
hx : ↑(splitMul 𝕜 A) x = 0
⊢ x = 0
[PROOFSTEP]
induction x using Unitization.ind
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : ↑(splitMul 𝕜 A) (inl r✝ + ↑a✝) = 0
⊢ inl r✝ + ↑a✝ = 0
[PROOFSTEP]
rw [map_add] at hx 
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : ↑(splitMul 𝕜 A) (inl r✝) + ↑(splitMul 𝕜 A) ↑a✝ = 0
⊢ inl r✝ + ↑a✝ = 0
[PROOFSTEP]
simp only [splitMul_apply, fst_inl, snd_inl, map_zero, add_zero, fst_inr, snd_inr, zero_add, Prod.mk_add_mk,
  Prod.mk_eq_zero] at hx 
[GOAL]
case h
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
r✝ : 𝕜
a✝ : A
hx : r✝ = 0 ∧ ↑(algebraMap 𝕜 (A →L[𝕜] A)) r✝ + ↑(mul 𝕜 A) a✝ = 0
⊢ inl r✝ + ↑a✝ = 0
[PROOFSTEP]
obtain ⟨rfl, hx⟩ := hx
[GOAL]
case h.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
a✝ : A
hx : ↑(algebraMap 𝕜 (A →L[𝕜] A)) 0 + ↑(mul 𝕜 A) a✝ = 0
⊢ inl 0 + ↑a✝ = 0
[PROOFSTEP]
simp only [map_zero, zero_add, inl_zero] at hx ⊢
[GOAL]
case h.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
a✝ : A
hx : ↑(mul 𝕜 A) a✝ = 0
⊢ ↑a✝ = 0
[PROOFSTEP]
rw [← map_zero (mul 𝕜 A)] at hx 
[GOAL]
case h.intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
h : Function.Injective ↑(mul 𝕜 A)
a✝ : A
hx : ↑(mul 𝕜 A) a✝ = ↑(mul 𝕜 A) 0
⊢ ↑a✝ = 0
[PROOFSTEP]
rw [h hx, inr_zero]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖x‖ = ‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖
[PROOFSTEP]
rw [norm_def, splitMul_apply, Prod.norm_def, sup_eq_max]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ LipschitzWith 2 ↑(addEquiv 𝕜 A)
[PROOFSTEP]
rw [← Real.toNNReal_ofNat]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ LipschitzWith (Real.toNNReal 2) ↑(addEquiv 𝕜 A)
[PROOFSTEP]
refine AddMonoidHomClass.lipschitz_of_bound (Unitization.addEquiv 𝕜 A) 2 fun x => ?_
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖↑(addEquiv 𝕜 A) x‖ ≤ 2 * ‖x‖
[PROOFSTEP]
rw [norm_eq_sup, Prod.norm_def]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ max ‖(↑(addEquiv 𝕜 A) x).fst‖ ‖(↑(addEquiv 𝕜 A) x).snd‖ ≤
    2 * (‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖)
[PROOFSTEP]
refine' max_le ?_ ?_
[GOAL]
case refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖(↑(addEquiv 𝕜 A) x).fst‖ ≤ 2 * (‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖)
[PROOFSTEP]
rw [sup_eq_max, mul_max_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]
[GOAL]
case refine'_1
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖(↑(addEquiv 𝕜 A) x).fst‖ ≤ max (2 * ‖fst x‖) (2 * ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖)
[PROOFSTEP]
exact le_max_of_le_left ((le_add_of_nonneg_left (norm_nonneg _)).trans_eq (two_mul _).symm)
[GOAL]
case refine'_2
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖(↑(addEquiv 𝕜 A) x).snd‖ ≤ 2 * (‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖)
[PROOFSTEP]
nontriviality A
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
✝ : Nontrivial A
⊢ ‖(↑(addEquiv 𝕜 A) x).snd‖ ≤ 2 * (‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖)
[PROOFSTEP]
rw [two_mul]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
✝ : Nontrivial A
⊢ ‖(↑(addEquiv 𝕜 A) x).snd‖ ≤
    ‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖ +
      ‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖
[PROOFSTEP]
calc
  ‖x.snd‖ = ‖mul 𝕜 A x.snd‖ := .symm <| (isometry_mul 𝕜 A).norm_map_of_map_zero (map_zero _) _
  _ ≤ ‖algebraMap 𝕜 _ x.fst + mul 𝕜 A x.snd‖ + ‖x.fst‖ := by
    simpa only [add_comm _ (mul 𝕜 A x.snd), norm_algebraMap'] using
      norm_le_add_norm_add (mul 𝕜 A x.snd) (algebraMap 𝕜 _ x.fst)
  _ ≤ _ := add_le_add le_sup_right le_sup_left
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
✝ : Nontrivial A
⊢ ‖↑(mul 𝕜 A) (snd x)‖ ≤ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖ + ‖fst x‖
[PROOFSTEP]
simpa only [add_comm _ (mul 𝕜 A x.snd), norm_algebraMap'] using
  norm_le_add_norm_add (mul 𝕜 A x.snd) (algebraMap 𝕜 _ x.fst)
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ AntilipschitzWith 2 ↑(addEquiv 𝕜 A)
[PROOFSTEP]
refine AddMonoidHomClass.antilipschitz_of_bound (addEquiv 𝕜 A) fun x => ?_
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖x‖ ≤ ↑2 * ‖↑(addEquiv 𝕜 A) x‖
[PROOFSTEP]
rw [norm_eq_sup, Prod.norm_def, NNReal.coe_two]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖fst x‖ ⊔ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖ ≤
    2 * max ‖(↑(addEquiv 𝕜 A) x).fst‖ ‖(↑(addEquiv 𝕜 A) x).snd‖
[PROOFSTEP]
refine max_le ?_ ?_
[GOAL]
case refine_1
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖fst x‖ ≤ 2 * max ‖(↑(addEquiv 𝕜 A) x).fst‖ ‖(↑(addEquiv 𝕜 A) x).snd‖
[PROOFSTEP]
rw [mul_max_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]
[GOAL]
case refine_1
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖fst x‖ ≤ max (2 * ‖(↑(addEquiv 𝕜 A) x).fst‖) (2 * ‖(↑(addEquiv 𝕜 A) x).snd‖)
[PROOFSTEP]
exact le_max_of_le_left ((le_add_of_nonneg_left (norm_nonneg _)).trans_eq (two_mul _).symm)
[GOAL]
case refine_2
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
⊢ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖ ≤
    2 * max ‖(↑(addEquiv 𝕜 A) x).fst‖ ‖(↑(addEquiv 𝕜 A) x).snd‖
[PROOFSTEP]
nontriviality A
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
✝ : Nontrivial A
⊢ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x) + ↑(mul 𝕜 A) (snd x)‖ ≤
    2 * max ‖(↑(addEquiv 𝕜 A) x).fst‖ ‖(↑(addEquiv 𝕜 A) x).snd‖
[PROOFSTEP]
calc
  ‖algebraMap 𝕜 _ x.fst + mul 𝕜 A x.snd‖ ≤ ‖algebraMap 𝕜 _ x.fst‖ + ‖mul 𝕜 A x.snd‖ := norm_add_le _ _
  _ = ‖x.fst‖ + ‖x.snd‖ := by
    rw [norm_algebraMap', (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 A)).mp (isometry_mul 𝕜 A)]
  _ ≤ _ := (add_le_add (le_max_left _ _) (le_max_right _ _)).trans_eq (two_mul _).symm
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : Unitization 𝕜 A
✝ : Nontrivial A
⊢ ‖↑(algebraMap 𝕜 (A →L[𝕜] A)) (fst x)‖ + ‖↑(mul 𝕜 A) (snd x)‖ = ‖fst x‖ + ‖snd x‖
[PROOFSTEP]
rw [norm_algebraMap', (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 A)).mp (isometry_mul 𝕜 A)]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ 𝓤 (Unitization 𝕜 A) = 𝓤 (Unitization 𝕜 A)
[PROOFSTEP]
have key : UniformInducing (addEquiv 𝕜 A) :=
  antilipschitzWith_addEquiv.uniformInducing lipschitzWith_addEquiv.uniformContinuous
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
key : UniformInducing ↑(addEquiv 𝕜 A)
⊢ 𝓤 (Unitization 𝕜 A) = 𝓤 (Unitization 𝕜 A)
[PROOFSTEP]
rw [← key.comap_uniformity]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
key : UniformInducing ↑(addEquiv 𝕜 A)
⊢ 𝓤 (Unitization 𝕜 A) = comap (fun x => (↑(addEquiv 𝕜 A) x.fst, ↑(addEquiv 𝕜 A) x.snd)) (𝓤 (𝕜 × A))
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
k : 𝕜
x : Unitization 𝕜 A
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖
[PROOFSTEP]
rw [norm_def, map_smul, norm_smul, ← norm_def]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ ‖1‖ = 1
[PROOFSTEP]
simpa only [norm_eq_sup, fst_one, norm_one, snd_one, map_one, map_zero, add_zero, ge_iff_le, sup_eq_left] using
  op_norm_le_bound _ zero_le_one fun x => by simp
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : A
⊢ ‖↑1 x‖ ≤ 1 * ‖x‖
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
a : A
⊢ ‖↑a‖ = ‖a‖
[PROOFSTEP]
simp [norm_eq_sup]
