case zero
𝕜 : Type ?u.92251
E : Type u_1
α : Type ?u.92257
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
⊢ ‖x ^ 2 ^ Nat.zero‖₊ = ‖x‖₊ ^ 2 ^ Nat.zero

case succ
𝕜 : Type ?u.92251
E : Type u_1
α : Type ?u.92257
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ Nat.succ k‖₊ = ‖x‖₊ ^ 2 ^ Nat.succ k
𝕜 : Type ?u.92251
E : Type u_1
α : Type ?u.92257
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
n : ℕ
⊢ ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n
induction' n with k hk
no goals
case zero
𝕜 : Type ?u.92251
E : Type u_1
α : Type ?u.92257
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
⊢ ‖x ^ 2 ^ Nat.zero‖₊ = ‖x‖₊ ^ 2 ^ Nat.zero
simp only [pow_zero, pow_one, Nat.zero_eq]
case succ
𝕜 : Type ?u.92251
E : Type u_1
α : Type ?u.92257
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ k * x ^ 2 ^ k‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)
case succ
𝕜 : Type ?u.92251
E : Type u_1
α : Type ?u.92257
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ Nat.succ k‖₊ = ‖x‖₊ ^ 2 ^ Nat.succ k
rw [pow_succ, pow_mul', sq]
case succ
𝕜 : Type ?u.92251
E : Type u_1
α : Type ?u.92257
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x⋆ ^ 2 ^ k * x ^ 2 ^ k‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)
case succ
𝕜 : Type ?u.92251
E : Type u_1
α : Type ?u.92257
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ k * x ^ 2 ^ k‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)
nth_rw 1 [← selfAdjoint.mem_iff.mp hx]
no goals
case succ
𝕜 : Type ?u.92251
E : Type u_1
α : Type ?u.92257
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CstarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x⋆ ^ 2 ^ k * x ^ 2 ^ k‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)
rw [← star_pow, CstarRing.nnnorm_star_mul_self, ← sq, hk, pow_mul']