awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
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)
succ₅ succ₆ :
  HPow.hPow (β := ℕ) (‖x‖₊ ^ HPow.hPow (α := ℕ) 2 k) 2 = HPow.hPow (β := ℕ) (‖x‖₊ ^ HPow.hPow (α := ℕ) 2 k) 2
⊢ ‖x ^ HPow.hPow (α := ℕ) 2 (k + 1)‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 (k + 1)

Tactic:
rw [pow_succ', pow_mul', sq, (hx.pow (2 ^ k)).nnnorm_mul_self, hk, pow_mul']

Premises used: IsSelfAdjoint.nnnorm_mul_self, sq, HPow.hPow, IsSelfAdjoint.pow, OfNat.ofNat, pow_mul', pow_succ'
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
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
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)
⊢ ‖x ^ HPow.hPow (α := ℕ) 2 n‖₊ = ‖x‖₊ ^ HPow.hPow (α := ℕ) 2 n

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']

Premises used: sq, pow_zero, pow_one, pow_mul', pow_succ'
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
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

Tactic:
congr($(hx.nnnorm_pow_two_pow n))

Premises used: congrArg, id, NNReal.toReal, IsSelfAdjoint.nnnorm_pow_two_pow
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
e : E
he : IsStarProjection e
this : ‖e‖ * (‖e‖ - 1) = 0
⊢ ‖e‖ ≤ 1

Tactic:
grind [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
e : E
he : IsStarProjection e
suffices : ‖e‖ * (‖e‖ - 1) = 0
⊢ ‖e‖ ≤ 1

Tactic:
suffices ‖e‖ * (‖e‖ - 1) = 0 by grind [sub_eq_zero]
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
E : Type u_2
inst : NonUnitalNormedRing E
inst_1 : StarRing E
inst_2 : CStarRing E
e : E
he : IsStarProjection e
⊢ ‖e‖ * (‖e‖ - 1) = 0

Tactic:
simp [mul_sub, ← CStarRing.norm_star_mul_self, he.isSelfAdjoint.star_eq, he.isIdempotentElem.eq]

Premises used: IsStarProjection.isIdempotentElem, mul_sub, CStarRing.norm_star_mul_self, IsStarProjection.isSelfAdjoint, IsIdempotentElem.eq, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : StarRing 𝕜
inst_2 : SeminormedAddCommGroup E
inst_3 : StarAddMonoid E
inst_4 : NormedStarGroup E
inst_5 : Module 𝕜 E
inst_6 : StarModule 𝕜 E
⊢ Eq.{u_2 + 1} (α := (a : E) → E) (⇑(starₗᵢ 𝕜) : (a : E) → E) star

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : StarRing 𝕜
inst_2 : SeminormedAddCommGroup E
inst_3 : StarAddMonoid E
inst_4 : NormedStarGroup E
inst_5 : Module 𝕜 E
inst_6 : StarModule 𝕜 E
x : E
⊢ (starₗᵢ 𝕜 : (a : E) → E) x = x⋆

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : StarRing 𝕜
inst_2 : SeminormedAddCommGroup E
inst_3 : StarAddMonoid E
inst_4 : NormedStarGroup E
inst_5 : Module 𝕜 E
inst_6 : StarModule 𝕜 E
⊢ Eq.{u_2 + 1} (α := E ≃L⋆[𝕜] E) (↑(starₗᵢ 𝕜) : E ≃L⋆[𝕜] E) (starL 𝕜)

Tactic:
ContinuousLinearEquiv.ext rfl

Premises used: ContinuousLinearEquiv.ext, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Basic
Goal:
𝕜_1 : Type u_1
E : Type u_2
α : Type u_3
𝕜 : Type u_4
A : Type u_5
inst : NormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : SeminormedRing A
inst_3 : StarRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : StarModule 𝕜 A
S : StarSubalgebra 𝕜 A
⊢ NormedAlgebra.{u_4, u_5} 𝕜 ↥S

Tactic:
infer_instance
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
M : Matrix m n A
i : m
⊢ (ofMatrix : (a : Matrix m n A) → CStarMatrix m n A) M i = M i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
M : CStarMatrix m n A
i : m
⊢ (Equiv.symm ofMatrix : (a : CStarMatrix m n A) → Matrix m n A) M i = M i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
M N : CStarMatrix m n A
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j

Tactic:
simp [h]
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
M₁ M₂ : CStarMatrix m n A
h : ∀ (i : m) (j : n), M₁ i j = M₂ i j
⊢ M₁ = M₂

Tactic:
ext_iff.mp h

Premises used: Iff.mp, CStarMatrix.ext_iff
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
B : Type u_6
M : CStarMatrix m n A
f : A → B
i : m
j : n
⊢ M.map f i j = f (M i j)

Tactic:
rfl

Premises used: CStarMatrix.map, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
M : CStarMatrix m n A
h : ∀ (i : m) (j : n), M.map id i j = M i j
⊢ M.map id = M

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
M : CStarMatrix m n A
i : m
j : n
⊢ M.map id i j = M i j

Tactic:
rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
M : CStarMatrix m n A
⊢ (M.map fun (x : A) ↦ x) = M

Tactic:
map_id M

Premises used: CStarMatrix.map_id
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
a : ∀ (i : m) (j : n), (M.map f).map g i j = M.map (g ∘ f) i j
⊢ (M.map f).map g = M.map (g ∘ f)

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
i : m
j : n
⊢ (M.map f).map g i j = M.map (g ∘ f) i j

Tactic:
rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
B : Type u_6
f : A → B
hf : Function.Injective f
⊢ Function.Injective (β := CStarMatrix m n B) fun (M : CStarMatrix m n A) ↦ M.map f

Tactic:
fun _ _ h =>
  ext fun i j => hf <| ext_iff.mpr h i j

Premises used: Iff.mpr, CStarMatrix.ext_iff, Function.Injective, CStarMatrix.ext
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
M : CStarMatrix m n A
i : n
j : m
⊢ M.transpose i j = M j i

Tactic:
rfl

Premises used: CStarMatrix.transpose, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Star A
M : CStarMatrix m n A
i : n
j : m
⊢ M.conjTranspose i j = star (M j i)

Tactic:
rfl

Premises used: CStarMatrix.transpose, CStarMatrix.conjTranspose, CStarMatrix.map, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
n : Type u_2
A : Type u_5
inst : Star A
M : CStarMatrix n n A
⊢ star M = M.conjTranspose

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m_1 : Type u_1
n_1 : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
n : Type u_7
m : Type u_8
inst : Finite m
inst_1 : Finite n
α : Type u_9
inst_2 : Finite α
⊢ Finite (CStarMatrix m n α)

Tactic:
inferInstanceAs <| Finite (Matrix m n α)

Premises used: _private.0.CStarMatrix.instFinite._proof_1
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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 : Subsingleton A
⊢ Subsingleton (CStarMatrix m n A)

Tactic:
inferInstanceAs <| Subsingleton (Matrix m n A)

Premises used: _private.0.CStarMatrix.instSubsingleton._proof_1
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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 : Nonempty m
inst_1 : Nonempty n
inst_2 : Nontrivial A
⊢ Nontrivial (CStarMatrix m n A)

Tactic:
inferInstanceAs <| Nontrivial (Matrix m n A)

Premises used: _private.0.CStarMatrix.instNontrivial._proof_1
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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 : SMul R A
inst_1 : SMul S A
inst_2 : SMulCommClass R S A
⊢ SMulCommClass R S (CStarMatrix m n A)

Tactic:
inferInstanceAs <| SMulCommClass R S (Matrix m n A)

Premises used: _private.0.CStarMatrix.instSMulCommClass._proof_1
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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 : SMul R S
inst_1 : SMul R A
inst_2 : SMul S A
inst_3 : IsScalarTower R S A
⊢ IsScalarTower R S (CStarMatrix m n A)

Tactic:
inferInstanceAs <| IsScalarTower R S (Matrix m n A)

Premises used: _private.0.CStarMatrix.instIsScalarTower._proof_1
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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 : SMul R A
inst_1 : SMul.{u_3, u_5} Rᵐᵒᵖ A
inst_2 : IsCentralScalar R A
⊢ IsCentralScalar R (CStarMatrix m n A)

Tactic:
inferInstanceAs <| IsCentralScalar R (Matrix m n A)

Premises used: _private.0.CStarMatrix.instIsCentralScalar._proof_1
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Zero A
i : m
j : n
⊢ Eq.{u_5 + 1} (α := A) (0 i j) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Add A
M N : CStarMatrix m n A
i : m
j : n
⊢ (M + N) i j = M i j + N i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
B : Type u_6
inst : SMul B A
r : B
M : CStarMatrix m n A
i : m
j : n
⊢ (r • M) i j = r • M i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Sub A
M N : CStarMatrix m n A
i : m
j : n
⊢ (M - N) i j = M i j - N i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Neg A
M : CStarMatrix m n A
i : m
j : n
⊢ (-M) i j = -M i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : AddMonoid A
inst_1 : StarAddMonoid A
h : ∀ (i : n) (j : m), Eq.{u_5 + 1} (α := A) (conjTranspose 0 i j) (0 i j)
⊢ Eq (α := CStarMatrix n m A) (conjTranspose 0) 0

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : AddMonoid A
inst_1 : StarAddMonoid A
i : n
j : m
⊢ Eq.{u_5 + 1} (α := A) (conjTranspose 0 i j) (0 i j)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Zero A
⊢ Eq (α := CStarMatrix m n A) ((ofMatrix : (a : Matrix m n A) → CStarMatrix m n A) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Add A
f g : Matrix m n A
⊢ HAdd.hAdd (α := CStarMatrix m n A) (β := CStarMatrix m n A)
      ((ofMatrix : (a : Matrix m n A) → CStarMatrix m n A) f : CStarMatrix m n A)
      ((ofMatrix : (a : Matrix m n A) → CStarMatrix m n A) g : CStarMatrix m n A) =
    (ofMatrix : (a : Matrix m n A) → CStarMatrix m n A) (f + g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Sub A
f g : Matrix m n A
⊢ HSub.hSub (α := CStarMatrix m n A) (β := CStarMatrix m n A)
      ((ofMatrix : (a : Matrix m n A) → CStarMatrix m n A) f : CStarMatrix m n A)
      ((ofMatrix : (a : Matrix m n A) → CStarMatrix m n A) g : CStarMatrix m n A) =
    (ofMatrix : (a : Matrix m n A) → CStarMatrix m n A) (f - g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Neg A
f : Matrix m n A
⊢ Eq (α := CStarMatrix m n A) (-(ofMatrix : (a : Matrix m n A) → CStarMatrix m n A) f : CStarMatrix m n A)
    ((ofMatrix : (a : Matrix m n A) → CStarMatrix m n A) (-f) : CStarMatrix m n A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
A : Type u_5
inst : SMul R A
r : R
f : Matrix m n A
⊢ HSMul.hSMul (β := CStarMatrix m n A) r ((ofMatrix : (a : Matrix m n A) → CStarMatrix m n A) f : CStarMatrix m n A) =
    (ofMatrix : (a : Matrix m n A) → CStarMatrix m n A) (r • f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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)
rw₁ rw₂ : star (f j i) = star (f j i)
⊢ star f i j = star (f j i)

Tactic:
rw [star_eq_conjTranspose, conjTranspose_apply]

Premises used: CStarMatrix.conjTranspose_apply, CStarMatrix.star_eq_conjTranspose
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
rw₁ rw₂ : f j i = f j i
⊢ star (f i j) = f j i

Tactic:
rw [← star_apply, IsSelfAdjoint.star_eq hf]

Premises used: CStarMatrix.star_apply, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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
⊢ (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))

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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
⊢ (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))

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
n : Type u_2
A : Type u_5
inst : DecidableEq n
inst_1 : Zero A
inst_2 : One A
i j : n
⊢ Eq.{u_5 + 1} (α := A) (1 i j) (if i = j then 1 else 0)

Tactic:
rfl

Premises used: Matrix.diagonal, rfl, ite
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
n : Type u_2
A : Type u_5
inst : DecidableEq n
inst_1 : Zero A
inst_2 : One A
i : n
⊢ Eq.{u_5 + 1} (α := A) (1 i i) 1

Tactic:
Matrix.one_apply_eq _

Premises used: Matrix.one_apply_eq
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
n : Type u_2
A : Type u_5
inst : DecidableEq n
inst_1 : Zero A
inst_2 : One A
i j : n
⊢ i ≠ j → Eq.{u_5 + 1} (α := A) (1 i j) 0

Tactic:
Matrix.one_apply_ne

Premises used: Matrix.one_apply_ne
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
n : Type u_2
A : Type u_5
inst : DecidableEq n
inst_1 : Zero A
inst_2 : One A
i j : n
⊢ j ≠ i → Eq.{u_5 + 1} (α := A) (1 i j) 0

Tactic:
Matrix.one_apply_ne'

Premises used: Matrix.one_apply_ne'
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
l : Type u_7
inst : Fintype m
inst_1 : Mul A
inst_2 : AddCommMonoid A
M : CStarMatrix l m A
N : CStarMatrix m n A
i : l
k : n
⊢ (M * N) i k = ∑ j : m, M i j * N j k

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Finset.sum, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
l : Type u_7
inst : Fintype m
inst_1 : Mul A
inst_2 : AddCommMonoid A
M : CStarMatrix l m A
N : CStarMatrix m n A
i : l
k : n
⊢ (M * N) i k = (fun (j : m) ↦ M i j) ⬝ᵥ fun (j : m) ↦ N j k

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Finset.sum, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
A : Type u_5
l : Type u_7
inst : Fintype n
inst_1 : Monoid R
inst_2 : AddCommMonoid A
inst_3 : Mul A
inst_4 : DistribMulAction R A
inst_5 : IsScalarTower R A A
a : R
M : CStarMatrix m n A
N : CStarMatrix n l A
⊢ a • M * N = a • (M * N)

Tactic:
Matrix.smul_mul a M N

Premises used: Multiset.sum, Multiset.foldr, dotProduct, CStarMatrix, Matrix.smul_mul, Finset.sum
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
A : Type u_5
l : Type u_7
inst : Fintype n
inst_1 : Monoid R
inst_2 : AddCommMonoid A
inst_3 : Mul A
inst_4 : DistribMulAction R A
inst_5 : SMulCommClass R A A
M : CStarMatrix m n A
a : R
N : CStarMatrix n l A
⊢ M * a • N = a • (M * N)

Tactic:
Matrix.mul_smul M a N

Premises used: Multiset.sum, Multiset.foldr, Matrix.mul_smul, dotProduct, CStarMatrix, Finset.sum
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
o : Type u_7
inst : Fintype n
inst_1 : NonUnitalNonAssocSemiring A
M : CStarMatrix m n A
⊢ M * 0 = 0

Tactic:
Matrix.mul_zero _

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mul_zero, CStarMatrix, Finset.sum
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
l : Type u_7
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring A
M : CStarMatrix m n A
⊢ 0 * M = 0

Tactic:
Matrix.zero_mul _

Premises used: Multiset.sum, Multiset.foldr, dotProduct, CStarMatrix, Matrix.zero_mul, Finset.sum
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
o : Type u_7
inst : Fintype n
inst_1 : NonUnitalNonAssocSemiring A
L : CStarMatrix m n A
M N : CStarMatrix n o A
⊢ L * (M + N) = L * M + L * N

Tactic:
Matrix.mul_add _ _ _

Premises used: Multiset.sum, Multiset.foldr, dotProduct, CStarMatrix, Matrix.mul_add, Finset.sum
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
l : Type u_7
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring A
L M : CStarMatrix l m A
N : CStarMatrix m n A
⊢ (L + M) * N = L * N + M * N

Tactic:
Matrix.add_mul _ _ _

Premises used: Multiset.sum, Multiset.foldr, dotProduct, CStarMatrix, Matrix.add_mul, Finset.sum
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
n : Type u_2
A : Type u_5
inst : Fintype n
inst_1 : SMul ℂ A
inst_2 : Semiring A
inst_3 : StarRing A
⊢ Eq (α := (a : Matrix n n A) → CStarMatrix n n A) (⇑ofMatrix : (a : Matrix n n A) → CStarMatrix n n A)
    (⇑ofMatrixStarAlgEquiv : (a : Matrix n n A) → CStarMatrix n n A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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
⊢ Equiv.toFun (Matrix.reindex eₘ eₙ) (M + N) =
    Equiv.toFun (Matrix.reindex eₘ eₙ) M + Equiv.toFun (Matrix.reindex eₘ eₙ) N

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
A : Type u_5
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 : CStarMatrix m n A
i : l
j : o
⊢ Eq.{u_5 + 1} (α := A) ((reindexₗ R A eₘ eₙ : (a : CStarMatrix m n A) → CStarMatrix l o A) M i j : A)
    ((Matrix.reindex eₘ eₙ : (a : Matrix m n A) → Matrix l o A) M i j : A)

Tactic:
rfl

Premises used: Matrix.submatrix, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix
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
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
⊢ 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

Tactic:
ext i j