awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : R₁ × R₂
inl :
  ∀ (h : ‖x.1‖ ≤ ‖x.2‖),
    HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.1‖ 2 ∨
      HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.2‖ 2
⊢ HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.1‖ 2 ∨
    HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.2‖ 2
have inr : ∀ (h : ‖x.2‖ ≤ ‖x.1‖),
  HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.1‖ 2 ∨
    HPow.hPow (β := ℕ) (max ‖x.1‖ ‖x.2‖) 2 ≤ HPow.hPow (β := ℕ) ‖x.2‖ 2
Tactic: rcases le_total ‖x.fst‖ ‖x.snd‖ with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : (i : ι) → R i
⊢ ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖
have refine : ‖x⋆ * x‖ = ‖x‖ * ‖x‖
Tactic: refine le_of_eq (Eq.symm ?_)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : (i : ι) → R i
⊢ ‖x⋆ * x‖ = ‖x‖ * ‖x‖
have simp : (↑(Finset.sup Finset.univ fun (b : ι) ↦ HPow.hPow (β := ℕ) ‖x b‖₊ 2) : ℝ) =
  HPow.hPow (β := ℕ) (↑(Finset.sup Finset.univ fun (b : ι) ↦ ‖x b‖₊) : ℝ) 2
Tactic: simp only [norm, Pi.mul_apply, Pi.star_apply, nnnorm_star_mul_self, ← sq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst : NonUnitalNormedRing R₁
inst_1 : StarRing R₁
inst_2 : CStarRing R₁
inst_3 : NonUnitalNormedRing R₂
inst_4 : StarRing R₂
inst_5 : CStarRing R₂
inst_6 : (i : ι) → NonUnitalNormedRing (R i)
inst_7 : (i : ι) → StarRing (R i)
inst_8 : Fintype ι
inst_9 : ∀ (i : ι), CStarRing.{u_7} (R i)
x : (i : ι) → R i
⊢ (↑(Finset.sup Finset.univ fun (b : ι) ↦ HPow.hPow (β := ℕ) ‖x b‖₊ 2) : ℝ) =
    HPow.hPow (β := ℕ) (↑(Finset.sup Finset.univ fun (b : ι) ↦ ‖x b‖₊) : ℝ) 2
have norm_cast : (Finset.sup Finset.univ fun (b : ι) ↦ HPow.hPow (β := ℕ) ‖x b‖₊ 2) =
  HPow.hPow (α := NNReal) (β := ℕ) (Finset.sup Finset.univ fun (b : ι) ↦ ‖x b‖₊) 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (hypothesis)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
⊢ norm.{u_2} (E := E) 1 = 1
have this : 0 < norm.{u_2} (E := E) 1
Tactic: have : 0 < ‖(1 : E)‖ := norm_pos_iff.mpr one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
this : 0 < norm.{u_2} (E := E) 1
⊢ norm.{u_2} (E := E) 1 = 1
have rw : norm.{u_2} (E := E) 1 * norm.{u_2} (E := E) 1 = 1 * norm.{u_2} (E := E) 1
Tactic: rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
this : 0 < norm.{u_2} (E := E) 1
rw : norm.{u_2} (E := E) 1 * norm.{u_2} (E := E) 1 = 1 * norm.{u_2} (E := E) 1
⊢ norm.{u_2} (E := E) 1 = 1
have rw₁ : ‖HMul.hMul (α := E) 1⋆ 1‖ = 1 * norm.{u_2} (E := E) 1
Tactic: rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
this : 0 < norm.{u_2} (E := E) 1
rw : norm.{u_2} (E := E) 1 * norm.{u_2} (E := E) 1 = 1 * norm.{u_2} (E := E) 1
rw₁ : ‖HMul.hMul (α := E) 1⋆ 1‖ = 1 * norm.{u_2} (E := E) 1
⊢ norm.{u_2} (E := E) 1 = 1
have rw₂ : norm.{u_2} (E := E) 1⋆ = 1 * norm.{u_2} (E := E) 1
Tactic: rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
this : 0 < norm.{u_2} (E := E) 1
rw : norm.{u_2} (E := E) 1 * norm.{u_2} (E := E) 1 = 1 * norm.{u_2} (E := E) 1
rw₁ : ‖HMul.hMul (α := E) 1⋆ 1‖ = 1 * norm.{u_2} (E := E) 1
rw₂ : norm.{u_2} (E := E) 1⋆ = 1 * norm.{u_2} (E := E) 1
⊢ norm.{u_2} (E := E) 1 = 1
have rw₃ : norm.{u_2} (E := E) 1 = 1 * norm.{u_2} (E := E) 1
Tactic: rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
this : 0 < norm.{u_2} (E := E) 1
rw : norm.{u_2} (E := E) 1 * norm.{u_2} (E := E) 1 = 1 * norm.{u_2} (E := E) 1
rw₁ : ‖HMul.hMul (α := E) 1⋆ 1‖ = 1 * norm.{u_2} (E := E) 1
rw₂ : norm.{u_2} (E := E) 1⋆ = 1 * norm.{u_2} (E := E) 1
rw₃ : norm.{u_2} (E := E) 1 = 1 * norm.{u_2} (E := E) 1
⊢ norm.{u_2} (E := E) 1 = 1
have rw₄ : norm.{u_2} (E := E) 1 = norm.{u_2} (E := E) 1
Tactic: rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
U : ↥(unitary E)
⊢ ‖(↑U : E)‖ = 1
have rw : HPow.hPow (β := ℕ) ‖(↑U : E)‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) zero_le_one, one_pow 2, sq, ← CStarRing.norm_star_mul_self,
    Unitary.coe_star_mul_self, CStarRing.norm_one]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
U : ↥(unitary E)
rw : HPow.hPow (β := ℕ) ‖(↑U : E)‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
⊢ ‖(↑U : E)‖ = 1
have rw₁ : HPow.hPow (β := ℕ) ‖(↑U : E)‖ 2 = 1
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) zero_le_one, one_pow 2, sq, ← CStarRing.norm_star_mul_self,
    Unitary.coe_star_mul_self, CStarRing.norm_one]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
U : ↥(unitary E)
rw : HPow.hPow (β := ℕ) ‖(↑U : E)‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
rw₁ : HPow.hPow (β := ℕ) ‖(↑U : E)‖ 2 = 1
⊢ ‖(↑U : E)‖ = 1
have rw₂ : ‖(↑U : E)‖ * ‖(↑U : E)‖ = 1
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) zero_le_one, one_pow 2, sq, ← CStarRing.norm_star_mul_self,
    Unitary.coe_star_mul_self, CStarRing.norm_one]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
U : ↥(unitary E)
rw : HPow.hPow (β := ℕ) ‖(↑U : E)‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
rw₁ : HPow.hPow (β := ℕ) ‖(↑U : E)‖ 2 = 1
rw₂ : ‖(↑U : E)‖ * ‖(↑U : E)‖ = 1
⊢ ‖(↑U : E)‖ = 1
have rw₃ : ‖(↑U : E)⋆ * (↑U : E)‖ = 1
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) zero_le_one, one_pow 2, sq, ← CStarRing.norm_star_mul_self,
    Unitary.coe_star_mul_self, CStarRing.norm_one]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
U : ↥(unitary E)
rw : HPow.hPow (β := ℕ) ‖(↑U : E)‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
rw₁ : HPow.hPow (β := ℕ) ‖(↑U : E)‖ 2 = 1
rw₂ : ‖(↑U : E)‖ * ‖(↑U : E)‖ = 1
rw₃ : ‖(↑U : E)⋆ * (↑U : E)‖ = 1
⊢ ‖(↑U : E)‖ = 1
have rw₄ : norm.{u_2} (E := E) 1 = 1
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) zero_le_one, one_pow 2, sq, ← CStarRing.norm_star_mul_self,
    Unitary.coe_star_mul_self, CStarRing.norm_one]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
inst_3 : Nontrivial E
U : ↥(unitary E)
rw : HPow.hPow (β := ℕ) ‖(↑U : E)‖ 2 = HPow.hPow (α := ℝ) (β := ℕ) 1 2
rw₁ : HPow.hPow (β := ℕ) ‖(↑U : E)‖ 2 = 1
rw₂ : ‖(↑U : E)‖ * ‖(↑U : E)‖ = 1
rw₃ : ‖(↑U : E)⋆ * (↑U : E)‖ = 1
rw₄ : norm.{u_2} (E := E) 1 = 1
⊢ ‖(↑U : E)‖ = 1
have rw₅ : Eq (α := ℝ) 1 1
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) zero_le_one, one_pow 2, sq, ← CStarRing.norm_star_mul_self,
    Unitary.coe_star_mul_self, CStarRing.norm_one]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
U : ↥(unitary E)
A : E
⊢ ‖(↑U : E) * A‖ = ‖A‖
have rw : HPow.hPow (β := ℕ) ‖(↑U : E) * A‖ 2 = HPow.hPow (β := ℕ) ‖A‖ 2
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ HPow.hPow (α := ℕ) 2 k‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 k
⊢ ‖x ^ HPow.hPow (α := ℕ) 2 (k + 1)‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 (k + 1)
have succ : ‖x ^ (2 * HPow.hPow (α := ℕ) 2 k)‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
Tactic: rw [pow_succ', pow_mul', sq, (hx.pow (2 ^ k)).nnnorm_mul_self, hk, pow_mul']
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ HPow.hPow (α := ℕ) 2 k‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 k
succ : ‖x ^ (2 * HPow.hPow (α := ℕ) 2 k)‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
⊢ ‖x ^ HPow.hPow (α := ℕ) 2 (k + 1)‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 (k + 1)
have succ₁ : ‖HPow.hPow (β := ℕ) (x ^ HPow.hPow (α := ℕ) 2 k) 2‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
Tactic: rw [pow_succ', pow_mul', sq, (hx.pow (2 ^ k)).nnnorm_mul_self, hk, pow_mul']
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ HPow.hPow (α := ℕ) 2 k‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 k
succ : ‖x ^ (2 * HPow.hPow (α := ℕ) 2 k)‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
succ₁ : ‖HPow.hPow (β := ℕ) (x ^ HPow.hPow (α := ℕ) 2 k) 2‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
⊢ ‖x ^ HPow.hPow (α := ℕ) 2 (k + 1)‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 (k + 1)
have succ₂ : ‖x ^ HPow.hPow (α := ℕ) 2 k * x ^ HPow.hPow (α := ℕ) 2 k‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
Tactic: rw [pow_succ', pow_mul', sq, (hx.pow (2 ^ k)).nnnorm_mul_self, hk, pow_mul']
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ HPow.hPow (α := ℕ) 2 k‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 k
succ : ‖x ^ (2 * HPow.hPow (α := ℕ) 2 k)‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
succ₁ : ‖HPow.hPow (β := ℕ) (x ^ HPow.hPow (α := ℕ) 2 k) 2‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
succ₂ : ‖x ^ HPow.hPow (α := ℕ) 2 k * x ^ HPow.hPow (α := ℕ) 2 k‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
⊢ ‖x ^ HPow.hPow (α := ℕ) 2 (k + 1)‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 (k + 1)
have succ₃ : HPow.hPow (β := ℕ) ‖x ^ HPow.hPow (α := ℕ) 2 k‖₊ 2 = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
Tactic: rw [pow_succ', pow_mul', sq, (hx.pow (2 ^ k)).nnnorm_mul_self, hk, pow_mul']
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ HPow.hPow (α := ℕ) 2 k‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 k
succ : ‖x ^ (2 * HPow.hPow (α := ℕ) 2 k)‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
succ₁ : ‖HPow.hPow (β := ℕ) (x ^ HPow.hPow (α := ℕ) 2 k) 2‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
succ₂ : ‖x ^ HPow.hPow (α := ℕ) 2 k * x ^ HPow.hPow (α := ℕ) 2 k‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
succ₃ : HPow.hPow (β := ℕ) ‖x ^ HPow.hPow (α := ℕ) 2 k‖₊ 2 = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
⊢ ‖x ^ HPow.hPow (α := ℕ) 2 (k + 1)‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 (k + 1)
have succ₄ : HPow.hPow (β := ℕ) (‖x‖₊ ^ HPow.hPow (α := ℕ) 2 k) 2 = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
Tactic: rw [pow_succ', pow_mul', sq, (hx.pow (2 ^ k)).nnnorm_mul_self, hk, pow_mul']
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ HPow.hPow (α := ℕ) 2 k‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 k
succ : ‖x ^ (2 * HPow.hPow (α := ℕ) 2 k)‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
succ₁ : ‖HPow.hPow (β := ℕ) (x ^ HPow.hPow (α := ℕ) 2 k) 2‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
succ₂ : ‖x ^ HPow.hPow (α := ℕ) 2 k * x ^ HPow.hPow (α := ℕ) 2 k‖₊ = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
succ₃ : HPow.hPow (β := ℕ) ‖x ^ HPow.hPow (α := ℕ) 2 k‖₊ 2 = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
succ₄ : HPow.hPow (β := ℕ) (‖x‖₊ ^ HPow.hPow (α := ℕ) 2 k) 2 = ‖x‖₊ ^ (2 * HPow.hPow (α := ℕ) 2 k)
⊢ ‖x ^ HPow.hPow (α := ℕ) 2 (k + 1)‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 (k + 1)
have succ₅ : HPow.hPow (β := ℕ) (‖x‖₊ ^ HPow.hPow (α := ℕ) 2 k) 2 = HPow.hPow (β := ℕ) (‖x‖₊ ^ HPow.hPow (α := ℕ) 2 k) 2
Tactic: rw [pow_succ', pow_mul', sq, (hx.pow (2 ^ k)).nnnorm_mul_self, hk, pow_mul']
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : IsSelfAdjoint x
n : ℕ
⊢ ‖x ^ HPow.hPow (α := ℕ) 2 n‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 n
have zero : ‖x ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0
Tactic: induction n with
  | zero => simp only [pow_zero, pow_one]
  | succ k hk =>
    rw [pow_succ', pow_mul', sq, (hx.pow (2 ^ k)).nnnorm_mul_self, hk, pow_mul']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
x : E
hx : IsSelfAdjoint x
n : ℕ
zero : ‖x ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0
⊢ ‖x ^ HPow.hPow (α := ℕ) 2 n‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 n
have succ : ∀ (k : ℕ) (hk : ‖x ^ HPow.hPow (α := ℕ) 2 k‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 k),
  ‖x ^ HPow.hPow (α := ℕ) 2 (k + 1)‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 (k + 1)
Tactic: induction n with
  | zero => simp only [pow_zero, pow_one]
  | succ k hk =>
    rw [pow_succ', pow_mul', sq, (hx.pow (2 ^ k)).nnnorm_mul_self, hk, pow_mul']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Basic (goal)
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
e : E
he : IsStarProjection e
⊢ ‖e‖ ≤ 1
have suffices : ‖e‖ * (‖e‖ - 1) = 0
Tactic: suffices ‖e‖ * (‖e‖ - 1) = 0 by grind [sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
M : CStarMatrix m n A
⊢ M.map id = M
have h : ∀ (i : m) (j : n), M.map id i j = M i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
B : Type u_6
C : Type u_7
M : Matrix m n A
f : A → B
g : B → C
⊢ (M.map f).map g = M.map (g ∘ f)
have a : ∀ (i : m) (j : n), (M.map f).map g i j = M.map (g ∘ f) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : AddMonoid A
inst_1 : StarAddMonoid A
⊢ Eq (α := CStarMatrix n m A) (conjTranspose 0) 0
have h : ∀ (i : n) (j : m), Eq.{u_5 + 1} (α := A) (conjTranspose 0 i j) (0 i j)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
n : Type u_2
A : Type u_5
inst : Star A
f : CStarMatrix n n A
i j : n
⊢ star f i j = star (f j i)
have rw : f.conjTranspose i j = star (f j i)
Tactic: rw [star_eq_conjTranspose, conjTranspose_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
n : Type u_2
A : Type u_5
inst : Star A
f : CStarMatrix n n A
i j : n
rw : f.conjTranspose i j = star (f j i)
⊢ star f i j = star (f j i)
have rw₁ : star (f j i) = star (f j i)
Tactic: rw [star_eq_conjTranspose, conjTranspose_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
n : Type u_2
A : Type u_5
inst : Star A
f : CStarMatrix n n A
hf : IsSelfAdjoint f
i j : n
⊢ star (f i j) = f j i
have rw : star f j i = f j i
Tactic: rw [← star_apply, IsSelfAdjoint.star_eq hf]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
n : Type u_2
A : Type u_5
inst : Star A
f : CStarMatrix n n A
hf : IsSelfAdjoint f
i j : n
rw : star f j i = f j i
⊢ star (f i j) = f j i
have rw₁ : f j i = f j i
Tactic: rw [← star_apply, IsSelfAdjoint.star_eq hf]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Module R A
inst_5 : Module S B
f : A →ₛₗ[σ] B
M N : CStarMatrix m n A
⊢ (M + N).map (⇑f : (a : A) → B) =
    HAdd.hAdd (α := CStarMatrix m n B) (M.map (⇑f : (a : A) → B)) (N.map (⇑f : (a : A) → B))
have h : ∀ (i : m) (j : n),
  (M + N).map (⇑f : (a : A) → B) i j =
    HAdd.hAdd (α := CStarMatrix m n B) (β := CStarMatrix m n B) (M.map (⇑f : (a : A) → B)) (N.map (⇑f : (a : A) → B)) i
      j
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Module R A
inst_5 : Module S B
f : A →ₛₗ[σ] B
r : R
M : CStarMatrix m n A
⊢ (r • M).map (⇑f : (a : A) → B) =
    HSMul.hSMul (α := S) (β := CStarMatrix m n B) ((σ : (a : R) → S) r : S) (M.map (⇑f : (a : A) → B))
have h : ∀ (i : m) (j : n),
  (r • M).map (⇑f : (a : A) → B) i j =
    HSMul.hSMul (α := S) (β := CStarMatrix m n B) ((σ : (a : R) → S) r : S) (M.map (⇑f : (a : A) → B)) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
l : Type u_7
o : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
eₘ : m ≃ l
eₙ : n ≃ o
M N : CStarMatrix m n A
⊢ Equiv.toFun (Matrix.reindex eₘ eₙ) (M + N) =
    Equiv.toFun (Matrix.reindex eₘ eₙ) M + Equiv.toFun (Matrix.reindex eₘ eₙ) N
have h : ∀ (i : l) (j : o),
  Equiv.toFun (Matrix.reindex eₘ eₙ) (M + N) i j =
    (Equiv.toFun (Matrix.reindex eₘ eₙ) M + Equiv.toFun (Matrix.reindex eₘ eₙ) N) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
l : Type u_7
o : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
eₘ : m ≃ l
eₙ : n ≃ o
r : R
M : CStarMatrix m n A
⊢ Equiv.toFun (Matrix.reindex eₘ eₙ) (r • M) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (Equiv.toFun (Matrix.reindex eₘ eₙ) M)
have h : ∀ (i : l) (j : o),
  Equiv.toFun (Matrix.reindex eₘ eₙ) (r • M) i j =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (Equiv.toFun (Matrix.reindex eₘ eₙ) M) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
R_1 : Type u_3
S : Type u_4
A_1 : Type u_5
B : Type u_6
R : Type u_7
A : Type u_8
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
e : m ≃ n
M N : CStarMatrix m m A
⊢ AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (M * N) =
    AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M *
      AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) N
have h : ∀ (i j : n),
  AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (M * N) i j =
    (AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M *
        AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) N)
      i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
R_1 : Type u_3
S : Type u_4
A_1 : Type u_5
B : Type u_6
R : Type u_7
A : Type u_8
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
e : m ≃ n
M N : CStarMatrix m m A
i j : n
⊢ AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (M * N) i j =
    (AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M *
        AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) N)
      i j
have h : AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (M * N) i j =
  ∑ j_1 : n,
    AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M i j_1 *
      AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) N j_1 j
Tactic: simp only [mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
R_1 : Type u_3
S : Type u_4
A_1 : Type u_5
B : Type u_6
R : Type u_7
A : Type u_8
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Mul A
inst_5 : Module R A
inst_6 : Star A
e : m ≃ n
M N : CStarMatrix m m A
i j : n
⊢ AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (M * N) i j =
    ∑ j_1 : n,
      AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M i j_1 *
        AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) N j_1 j
have h : ∀ (x : m),
  HMul.hMul (α := A)
      ((fun (j : m) ↦
          ((Equiv.symm ofMatrix : (a : CStarMatrix m m A) → Matrix m m A) M ((e.symm : (a : n) → m) i) j : A))
        x)
      ((fun (j_1 : m) ↦
          ((Equiv.symm ofMatrix : (a : CStarMatrix m m A) → Matrix m m A) N j_1 ((e.symm : (a : n) → m) j) : A))
        x) =
    AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M i
        ((e : (a : m) → n) x) *
      AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) N
        ((e : (a : m) → n) x) j
Tactic: refine Fintype.sum_equiv e _ _ ?_