awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : CStarMatrix m m A
⊢ AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (star M) =
    star (AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M)
have h : ∀ (i j : n),
  AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) (star M) i j =
    star (AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) 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 : 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)) (star M) i j =
    star (AddHom.toFun (LinearMap.toAddHom (↑(reindexₗ R A e e) : CStarMatrix m m A →ₗ[R] CStarMatrix n n A)) M) i j
have h : Eq.{u_8 + 1} (α := A)
  (AddHom.toFun
    (LinearMap.toAddHom
      (↑(let __src : Matrix m m A ≃ Matrix n n A := Matrix.reindex e e;
          { toFun := __src.toFun, map_add' := sorry, map_smul' := sorry, invFun := __src.invFun, left_inv := sorry,
            right_inv := sorry }) :
        CStarMatrix m m A →ₗ[R] CStarMatrix n n A))
    (star M) i j)
  (star
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(let __src : Matrix m m A ≃ Matrix n n A := Matrix.reindex e e;
            { toFun := __src.toFun, map_add' := sorry, map_smul' := sorry, invFun := __src.invFun, left_inv := sorry,
              right_inv := sorry }) :
          CStarMatrix m m A →ₗ[R] CStarMatrix n n A))
      M)
    i j)
Tactic: unfold reindexₗ
-- 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 : CStarMatrix m m A
i j : n
⊢ Eq.{u_8 + 1} (α := A)
    (AddHom.toFun
      (LinearMap.toAddHom
        (↑(let __src : Matrix m m A ≃ Matrix n n A := Matrix.reindex e e;
            { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
              right_inv := ⋯ }) :
          CStarMatrix m m A →ₗ[R] CStarMatrix n n A))
      (star M) i j)
    (star
      (AddHom.toFun
        (LinearMap.toAddHom
          (↑(let __src : Matrix m m A ≃ Matrix n n A := Matrix.reindex e e;
              { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
                right_inv := ⋯ }) :
            CStarMatrix m m A →ₗ[R] CStarMatrix n n A))
        M)
      i j)
have h : star M ((e.symm : (a : n) → m) i) ((e.symm : (a : n) → m) j) =
  star (Matrix.submatrix M (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) i j
Tactic: dsimp only [Equiv.toFun_as_coe, Equiv.invFun_as_coe, Matrix.reindex_symm, AddHom.toFun_eq_coe,
        AddHom.coe_mk, Matrix.reindex_apply, Matrix.submatrix_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 : CStarMatrix m m A
i j : n
⊢ star M ((e.symm : (a : n) → m) i) ((e.symm : (a : n) → m) j) =
    star (Matrix.submatrix M (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m)) i j
have h : star (M ((e.symm : (a : n) → m) j) ((e.symm : (a : n) → m) i)) =
  star (Matrix.submatrix M (⇑e.symm : (a : n) → m) (⇑e.symm : (a : n) → m) j i)
Tactic: rw [star_apply, star_apply]
-- 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 : Fintype n
inst_1 : Semiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : Star A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : Star B
f : A →⋆ₙₐ[R] B
M N : CStarMatrix n n A
⊢ (mapₗ (↑f : [inst : FunLike (A →⋆ₙₐ[R] B) A B] → [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
        (a : CStarMatrix n n A) → CStarMatrix n n B)
      (M * N) =
    HMul.hMul (α := CStarMatrix n n B) (β := CStarMatrix n n B)
      ((mapₗ
              (↑f :
                [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                  [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : CStarMatrix n n A) → CStarMatrix n n B)
          M :
        CStarMatrix n n B)
      ((mapₗ
              (↑f :
                [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                  [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : CStarMatrix n n A) → CStarMatrix n n B)
          N :
        CStarMatrix n n B)
have h : ∀ (i j : n),
  (mapₗ (↑f : [inst : FunLike (A →⋆ₙₐ[R] B) A B] → [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
        (a : CStarMatrix n n A) → CStarMatrix n n B)
      (M * N) i j =
    HMul.hMul (α := CStarMatrix n n B) (β := CStarMatrix n n B)
      ((mapₗ
              (↑f :
                [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                  [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : CStarMatrix n n A) → CStarMatrix n n B)
          M :
        CStarMatrix n n B)
      ((mapₗ
              (↑f :
                [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                  [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : CStarMatrix n n A) → CStarMatrix n n B)
          N :
        CStarMatrix n n 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 : Fintype n
inst_1 : Semiring R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : Star A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : Star B
f : A →⋆ₙₐ[R] B
M : CStarMatrix n n A
⊢ Eq (α := CStarMatrix n n B)
    ((mapₗ
            (↑f :
              [inst : FunLike (A →⋆ₙₐ[R] B) A B] → [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : CStarMatrix n n A) → CStarMatrix n n B)
        (star M) :
      CStarMatrix n n B)
    (star
        ((mapₗ
              (↑f :
                [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                  [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : CStarMatrix n n A) → CStarMatrix n n B)
          M) :
      CStarMatrix n n B)
have h : ∀ (i j : n),
  Eq.{u_6 + 1} (α := B)
    ((mapₗ
            (↑f :
              [inst : FunLike (A →⋆ₙₐ[R] B) A B] → [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
          (a : CStarMatrix n n A) → CStarMatrix n n B)
        (star M) i j :
      B)
    (star
        ((mapₗ
              (↑f :
                [inst : FunLike (A →⋆ₙₐ[R] B) A B] →
                  [SemilinearMapClass (A →⋆ₙₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : CStarMatrix n n A) → CStarMatrix n n B)
          M)
        i j :
      B)
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 : Unique n
inst_1 : Semiring R
inst_2 : AddCommMonoid A
inst_3 : Mul A
inst_4 : Star A
inst_5 : Module R A
x : CStarMatrix n n A
⊢ (fun (a : A) (x y : n) ↦ a) ((fun (M : CStarMatrix n n A) ↦ M default default) x) = x
have h : ∀ (i j : n), (fun (a : A) (x y : n) ↦ a) ((fun (M : CStarMatrix n n A) ↦ M default default) x) i j = x 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 : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst : Unique n
inst_1 : Semiring R
inst_2 : AddCommMonoid A
inst_3 : Mul A
inst_4 : Star A
inst_5 : Module R A
x x_1 : A
⊢ (fun (x_2 y : n) ↦ x * x_1) = HMul.hMul (α := CStarMatrix n n A) (fun (x_2 y : n) ↦ x) fun (x y : n) ↦ x_1
have h : ∀ (i j : n),
  x * x_1 = HMul.hMul (α := CStarMatrix n n A) (β := CStarMatrix n n A) (fun (x_2 y : n) ↦ x) (fun (x y : n) ↦ x_1) 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 : Unique n
inst_1 : Semiring R
inst_2 : AddCommMonoid A
inst_3 : Mul A
inst_4 : Star A
inst_5 : Module R A
x x_1 : A
⊢ (fun (x_2 y : n) ↦ x + x_1) = HAdd.hAdd (α := CStarMatrix n n A) (fun (x_2 y : n) ↦ x) fun (x y : n) ↦ x_1
have h : ∀ (i j : n),
  x + x_1 = HAdd.hAdd (α := CStarMatrix n n A) (β := CStarMatrix n n A) (fun (x_2 y : n) ↦ x) (fun (x y : n) ↦ x_1) 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 : Unique n
inst_1 : Semiring R
inst_2 : AddCommMonoid A
inst_3 : Mul A
inst_4 : Star A
inst_5 : Module R A
x : A
⊢ Eq (α := CStarMatrix n n A) (fun (x_1 y : n) ↦ star x) (star fun (x_1 y : n) ↦ x)
have h : ∀ (i j : n), star x = star (fun (x_1 y : n) ↦ x) 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 : Unique n
inst_1 : Semiring R
inst_2 : AddCommMonoid A
inst_3 : Mul A
inst_4 : Star A
inst_5 : Module R A
x : R
x_1 : A
⊢ (fun (x_2 y : n) ↦ x • x_1) = HSMul.hSMul (β := CStarMatrix n n A) x fun (x y : n) ↦ x_1
have h : ∀ (i j : n), x • x_1 = HSMul.hSMul (β := CStarMatrix n n A) x (fun (x y : n) ↦ x_1) 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 : Fintype m
inst_1 : NonUnitalCStarAlgebra A
M₁ M₂ : CStarMatrix m n A
x : C⋆ᵐᵒᵈ(A, m → A)
i : n
⊢ Eq.{u_5 + 1} (α := A)
    (({
            toFun :=
              Function.comp (β := n → A)
                (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                      (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                  (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                ((fun (v : m → A) ↦ v ᵥ* (M₁ + M₂)) ∘
                  (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                    (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
            map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x i :
      A)
    ((HAdd.hAdd (α := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
            {
              toFun :=
                Function.comp (β := n → A)
                  (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                        (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                    (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                  ((fun (v : m → A) ↦ v ᵥ* M₁) ∘
                    (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                      (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
              map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) }
            {
              toFun :=
                Function.comp (β := n → A)
                  (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                        (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                    (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                  ((fun (v : m → A) ↦ v ᵥ* M₂) ∘
                    (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                      (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
              map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) } :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x i :
      A)
have h : ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* (M₁ + M₂)) i =
  ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁) i +
    ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂) i
Tactic: simp only [ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      WithCStarModule.equivL_apply, WithCStarModule.equivL_symm_apply,
      WithCStarModule.equiv_symm_pi_apply, ContinuousLinearMap.add_apply, WithCStarModule.add_apply]
-- 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 : Fintype m
inst_1 : NonUnitalCStarAlgebra A
M₁ M₂ : CStarMatrix m n A
x : C⋆ᵐᵒᵈ(A, m → A)
i : n
⊢ ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* (M₁ + M₂)) i =
    ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁) i +
      ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂) i
have h : ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁ +
      (WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂)
    i =
  ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁) i +
    ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂) i
Tactic: rw [Matrix.vecMul_add, Pi.add_apply]
-- 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 : Fintype m
inst_1 : NonUnitalCStarAlgebra A
M₁ M₂ : CStarMatrix m n A
x : C⋆ᵐᵒᵈ(A, m → A)
i : n
h :
  ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁ +
        (WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂)
      i =
    ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁) i +
      ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂) i
⊢ ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* (M₁ + M₂)) i =
    ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁) i +
      ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂) i
have h₁ : ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁) i +
    ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂) i =
  ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₁) i +
    ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M₂) i
Tactic: rw [Matrix.vecMul_add, Pi.add_apply]
-- 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 : Fintype m
inst_1 : NonUnitalCStarAlgebra A
c : ℂ
M : CStarMatrix m n A
⊢ {
      toFun :=
        Function.comp (β := n → A)
          (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
            (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
          ((fun (v : m → A) ↦ v ᵥ* (c • M)) ∘
            (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
              (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } =
    HSMul.hSMul (α := ℂ) (β := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
      {
        toFun :=
          Function.comp (β := n → A)
            (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                  (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
              (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
            ((fun (v : m → A) ↦ v ᵥ* M) ∘
              (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) }
have h : ∀ (x : C⋆ᵐᵒᵈ(A, m → A)) (i : n),
  Eq.{u_5 + 1} (α := A)
    (({
            toFun :=
              Function.comp (β := n → A)
                (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                      (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                  (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                ((fun (v : m → A) ↦ v ᵥ* (c • M)) ∘
                  (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                    (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
            map_add' := sorry, map_smul' := sorry, cont := sorry } :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x i :
      A)
    ((HSMul.hSMul (α := ℂ) (β := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
            {
              toFun :=
                Function.comp (β := n → A)
                  (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                        (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                    (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                  ((fun (v : m → A) ↦ v ᵥ* M) ∘
                    (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                      (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
              map_add' := sorry, map_smul' := sorry, cont := sorry : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) } :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x i :
      A)
Tactic: ext x i
-- 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 : Fintype m
inst_1 : NonUnitalCStarAlgebra A
c : ℂ
M : CStarMatrix m n A
x : C⋆ᵐᵒᵈ(A, m → A)
i : n
⊢ Eq.{u_5 + 1} (α := A)
    (({
            toFun :=
              Function.comp (β := n → A)
                (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                      (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                  (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                ((fun (v : m → A) ↦ v ᵥ* (c • M)) ∘
                  (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                    (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
            map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x i :
      A)
    ((HSMul.hSMul (α := ℂ) (β := C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
            {
              toFun :=
                Function.comp (β := n → A)
                  (⇑(ContinuousLinearEquiv.symm (WithCStarModule.equivL ℂ (A := A) (E := n → A)) :
                        (n → A) ≃L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
                    (a : n → A) → C⋆ᵐᵒᵈ(A, n → A))
                  ((fun (v : m → A) ↦ v ᵥ* M) ∘
                    (⇑(WithCStarModule.equivL ℂ (A := A) (E := m → A) : C⋆ᵐᵒᵈ(A, m → A) ≃L[ℂ] m → A) :
                      (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A)),
              map_add' := ⋯, map_smul' := ⋯, cont := ⋯ : C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A) } :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        x i :
      A)
have h : ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* (c • M)) i =
  c • ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i
Tactic: simp only [ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      WithCStarModule.equivL_apply, WithCStarModule.equivL_symm_apply,
      WithCStarModule.equiv_symm_pi_apply, ContinuousLinearMap.smul_apply,
      WithCStarModule.smul_apply, RingHom.id_apply]
-- 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 : Fintype m
inst_1 : NonUnitalCStarAlgebra A
c : ℂ
M : CStarMatrix m n A
x : C⋆ᵐᵒᵈ(A, m → A)
i : n
⊢ ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* (c • M)) i =
    c • ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i
have h : (c • (WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i =
  c • ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i
Tactic: rw [Matrix.vecMul_smul, Pi.smul_apply]
-- 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 : Fintype m
inst_1 : NonUnitalCStarAlgebra A
c : ℂ
M : CStarMatrix m n A
x : C⋆ᵐᵒᵈ(A, m → A)
i : n
h :
  (c • (WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i =
    c • ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i
⊢ ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* (c • M)) i =
    c • ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i
have h₁ : c • ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i =
  c • ((WithCStarModule.equiv A (m → A) : (a : C⋆ᵐᵒᵈ(A, m → A)) → m → A) x ᵥ* M) i
Tactic: rw [Matrix.vecMul_smul, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.CStarMatrix (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_5
inst : Fintype m
inst_1 : NonUnitalCStarAlgebra A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ(A, m → A)
⊢ Eq (α := C⋆ᵐᵒᵈ(A, n → A))
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        v :
      C⋆ᵐᵒᵈ(A, n → A))
    ((Equiv.symm (WithCStarModule.equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A)) fun (j : n) ↦
        ∑ i : m, v i * M i j :
      C⋆ᵐᵒᵈ(A, (j : n) → A))
have h : ∀ (i : n),
  Eq.{u_5 + 1} (α := A)
    ((((toCLM : (a : CStarMatrix m n A) → C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) M :
            C⋆ᵐᵒᵈ(A, m → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) :
          (a : C⋆ᵐᵒᵈ(A, m → A)) → C⋆ᵐᵒᵈ(A, n → A))
        v i :
      A)
    ((Equiv.symm (WithCStarModule.equiv A ((j : n) → A)) : (a : (j : n) → A) → C⋆ᵐᵒᵈ(A, (j : n) → A))
        (fun (j : n) ↦ ∑ i : m, v i * M i j) i :
      A)
Tactic: ext i
-- 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 : Fintype m
inst_1 : NonUnitalCStarAlgebra A
inst_2 : Fintype n
x y : CStarMatrix n n A
⊢ AddHom.toFun
      (LinearMap.toAddHom
        ((↑(MulOpposite.opLinearEquiv ℂ) :
            (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) →ₗ[ℂ] (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) ∘ₗ
          toCLM))
      (x * y) =
    HMul.hMul (α := (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ)
      (AddHom.toFun
        (LinearMap.toAddHom
          ((↑(MulOpposite.opLinearEquiv ℂ) :
              (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) →ₗ[ℂ] (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) ∘ₗ
            toCLM))
        x)
      (AddHom.toFun
        (LinearMap.toAddHom
          ((↑(MulOpposite.opLinearEquiv ℂ) :
              (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) →ₗ[ℂ] (C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))ᵐᵒᵖ) ∘ₗ
            toCLM))
        y)
have simp : (toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (x * y) =
  HMul.hMul (α := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) (β := C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
    ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) y :
      C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
    ((toCLM : (a : CStarMatrix n n A) → C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A)) x :
      C⋆ᵐᵒᵈ(A, n → A) →L[ℂ] C⋆ᵐᵒᵈ(A, n → A))
Tactic: simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.coe_comp,
        LinearEquiv.coe_coe, MulOpposite.coe_opLinearEquiv, Function.comp_apply,
        ← MulOpposite.op_mul, MulOpposite.op_inj]