-- Mathlib/Analysis/CStarAlgebra/Hom.lean
/-- A non-unital star algebra monomorphism of complex C⋆-algebras is isometric. -/
lemma norm_map (φ : F) (hφ : Function.Injective φ) (a : A) : ‖φ a‖ = ‖a‖

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a : A
this : ∀ {ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B}, Function.Injective ⇑ψ → ∀ (a : Unitization ℂ A), ‖ψ a‖ = ‖a‖
⊢ ‖φ a‖ = ‖a‖

Tactic:
simpa [norm_inr] using this (starMap_injective (φ := (φ : A →⋆ₙₐ[ℂ] B)) hφ) a

Result:
no goals

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
⊢ 0 ≤ ‖a‖

Tactic:
positivity

Result:
no goals

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
ha : IsSelfAdjoint (star a * a)
⊢ (spectralRadius ℝ (ψ (star a * a))).toReal = (spectralRadius ℝ (star a * a)).toReal

Tactic:
simp only [spectralRadius, ha.map_spectrum_real ψ hψ]

Result:
no goals

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a : A
⊢ ‖φ a‖ = ‖a‖

Tactic:
suffices ∀ {ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B} (_ : Function.Injective ψ)
    (a : Unitization ℂ A), ‖ψ a‖ = ‖a‖ by
  simpa [norm_inr] using this (starMap_injective (φ := (φ : A →⋆ₙₐ[ℂ] B)) hφ) a

Result:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a : A
⊢ ∀ {ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B}, Function.Injective ⇑ψ → ∀ (a : Unitization ℂ A), ‖ψ a‖ = ‖a‖

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
ha : IsSelfAdjoint (star a * a)
⊢ ‖ψ (star a * a)‖ = ‖star a * a‖

Tactic:
calc ‖ψ (star a * a)‖ = (spectralRadius ℝ (ψ (star a * a))).toReal :=
    ha.map ψ |>.toReal_spectralRadius_eq_norm.symm
  _ = (spectralRadius ℝ (star a * a)).toReal := by
    simp only [spectralRadius, ha.map_spectrum_real ψ hψ]
  _ = ‖star a * a‖ := ha.toReal_spectralRadius_eq_norm

Result:
no goals

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
⊢ ‖ψ a‖ = ‖a‖

Tactic:
rw [← sq_eq_sq₀ (by positivity) (by positivity)]

Result:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
⊢ ‖ψ a‖ ^ 2 = ‖a‖ ^ 2

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
⊢ ‖ψ (star a * a)‖ = ‖star a * a‖

Tactic:
have ha : IsSelfAdjoint (star a * a) := .star_mul_self a

Result:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
ha : IsSelfAdjoint (star a * a)
⊢ ‖ψ (star a * a)‖ = ‖star a * a‖

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
⊢ ‖ψ a‖ ^ 2 = ‖a‖ ^ 2

Tactic:
simp only [sq, ← CStarRing.norm_star_mul_self, ← map_star, ← map_mul]

Result:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
⊢ ‖ψ (star a * a)‖ = ‖star a * a‖

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a : A
⊢ ∀ {ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B}, Function.Injective ⇑ψ → ∀ (a : Unitization ℂ A), ‖ψ a‖ = ‖a‖

Tactic:
intro ψ hψ a

Result:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
⊢ ‖ψ a‖ = ‖a‖

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
hφ : Function.Injective ⇑φ
a✝ : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
hψ : Function.Injective ⇑ψ
a : Unitization ℂ A
⊢ 0 ≤ ‖ψ a‖

Tactic:
positivity

Result:
no goals