[GOAL]
n : Type ?u.20
m : Type ?u.8
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type ?u.35
inst✝ : Fintype R
⊢ Fintype (Matrix m n R)
[PROOFSTEP]
unfold Matrix
[GOAL]
n : Type ?u.20
m : Type ?u.8
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type ?u.35
inst✝ : Fintype R
⊢ Fintype (m → n → R)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
⊢ vecMul (↑(LinearMap.stdBasis R (fun x => R) i) 1) M j = M i j
[PROOFSTEP]
have : (∑ i', (if i = i' then 1 else 0) * M i' j) = M i j := by
  simp_rw [boole_mul, Finset.sum_ite_eq, Finset.mem_univ, if_true]
[GOAL]
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
⊢ ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
[PROOFSTEP]
simp_rw [boole_mul, Finset.sum_ite_eq, Finset.mem_univ, if_true]
[GOAL]
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
⊢ vecMul (↑(LinearMap.stdBasis R (fun x => R) i) 1) M j = M i j
[PROOFSTEP]
simp only [vecMul, dotProduct]
[GOAL]
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
⊢ ∑ x : m, ↑(LinearMap.stdBasis R (fun x => R) i) 1 x * M x j = M i j
[PROOFSTEP]
convert this
[GOAL]
case h.e'_2.a.h.e'_5
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
x✝ : m
a✝ : x✝ ∈ Finset.univ
⊢ ↑(LinearMap.stdBasis R (fun x => R) i) 1 x✝ = if i = x✝ then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
x✝ : m
a✝ : x✝ ∈ Finset.univ
h : i = x✝
⊢ ↑(LinearMap.stdBasis R (fun x => R) i) 1 x✝ = 1
[PROOFSTEP]
simp only [stdBasis_apply]
[GOAL]
case neg
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
x✝ : m
a✝ : x✝ ∈ Finset.univ
h : ¬i = x✝
⊢ ↑(LinearMap.stdBasis R (fun x => R) i) 1 x✝ = 0
[PROOFSTEP]
simp only [stdBasis_apply]
[GOAL]
case pos
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
x✝ : m
a✝ : x✝ ∈ Finset.univ
h : i = x✝
⊢ Function.update 0 i 1 x✝ = 1
[PROOFSTEP]
rw [h, Function.update_same]
[GOAL]
case neg
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
this : ∑ i' : m, (if i = i' then 1 else 0) * M i' j = M i j
x✝ : m
a✝ : x✝ ∈ Finset.univ
h : ¬i = x✝
⊢ Function.update 0 i 1 x✝ = 0
[PROOFSTEP]
rw [Function.update_noteq (Ne.symm h), Pi.zero_apply]
[GOAL]
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f g : (m → R) →ₗ[R] n → R
⊢ (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
    (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f + (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g
[PROOFSTEP]
ext i j
[GOAL]
case a.h
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f g : (m → R) →ₗ[R] n → R
i : m
j : n
⊢ (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) i j =
    ((fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f + (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) i
      j
[PROOFSTEP]
simp only [Pi.add_apply, LinearMap.add_apply, Matrix.add_apply]
[GOAL]
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
c : Rᵐᵒᵖ
f : (m → R) →ₗ[R] n → R
⊢ AddHom.toFun
      { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
        map_add' :=
          (_ :
            ∀ (f g : (m → R) →ₗ[R] n → R),
              (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                  (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
      (c • f) =
    ↑(RingHom.id Rᵐᵒᵖ) c •
      AddHom.toFun
        { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
          map_add' :=
            (_ :
              ∀ (f g : (m → R) →ₗ[R] n → R),
                (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                  (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                    (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
        f
[PROOFSTEP]
ext i j
[GOAL]
case a.h
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
c : Rᵐᵒᵖ
f : (m → R) →ₗ[R] n → R
i : m
j : n
⊢ AddHom.toFun
      { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
        map_add' :=
          (_ :
            ∀ (f g : (m → R) →ₗ[R] n → R),
              (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                  (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
      (c • f) i j =
    (↑(RingHom.id Rᵐᵒᵖ) c •
        AddHom.toFun
          { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
            map_add' :=
              (_ :
                ∀ (f g : (m → R) →ₗ[R] n → R),
                  (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                    (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                      (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
          f)
      i j
[PROOFSTEP]
simp only [Pi.smul_apply, LinearMap.smul_apply, RingHom.id_apply, Matrix.smul_apply]
[GOAL]
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f : (m → R) →ₗ[R] n → R
⊢ vecMulLinear
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                map_add' :=
                  (_ :
                    ∀ (f g : (m → R) →ₗ[R] n → R),
                      (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                        (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                          (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) },
            map_smul' :=
              (_ :
                ∀ (c : Rᵐᵒᵖ) (f : (m → R) →ₗ[R] n → R),
                  AddHom.toFun
                      { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                        map_add' :=
                          (_ :
                            ∀ (f g : (m → R) →ₗ[R] n → R),
                              (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                                (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                                  (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
                      (c • f) =
                    ↑(RingHom.id Rᵐᵒᵖ) c •
                      AddHom.toFun
                        { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                          map_add' :=
                            (_ :
                              ∀ (f g : (m → R) →ₗ[R] n → R),
                                (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                                  (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                                    (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
                        f) }.toAddHom
        f) =
    f
[PROOFSTEP]
apply (Pi.basisFun R m).ext
[GOAL]
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f : (m → R) →ₗ[R] n → R
⊢ ∀ (i : m),
    ↑(vecMulLinear
            (AddHom.toFun
              {
                  toAddHom :=
                    { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                      map_add' :=
                        (_ :
                          ∀ (f g : (m → R) →ₗ[R] n → R),
                            (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                              (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                                (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) },
                  map_smul' :=
                    (_ :
                      ∀ (c : Rᵐᵒᵖ) (f : (m → R) →ₗ[R] n → R),
                        AddHom.toFun
                            { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                              map_add' :=
                                (_ :
                                  ∀ (f g : (m → R) →ₗ[R] n → R),
                                    (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                                      (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                                        (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
                            (c • f) =
                          ↑(RingHom.id Rᵐᵒᵖ) c •
                            AddHom.toFun
                              { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                                map_add' :=
                                  (_ :
                                    ∀ (f g : (m → R) →ₗ[R] n → R),
                                      (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                                        (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                                          (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
                              f) }.toAddHom
              f))
        (↑(Pi.basisFun R m) i) =
      ↑f (↑(Pi.basisFun R m) i)
[PROOFSTEP]
intro j
[GOAL]
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f : (m → R) →ₗ[R] n → R
j : m
⊢ ↑(vecMulLinear
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                    map_add' :=
                      (_ :
                        ∀ (f g : (m → R) →ₗ[R] n → R),
                          (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                            (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                              (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) },
                map_smul' :=
                  (_ :
                    ∀ (c : Rᵐᵒᵖ) (f : (m → R) →ₗ[R] n → R),
                      AddHom.toFun
                          { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                            map_add' :=
                              (_ :
                                ∀ (f g : (m → R) →ₗ[R] n → R),
                                  (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                                    (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                                      (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
                          (c • f) =
                        ↑(RingHom.id Rᵐᵒᵖ) c •
                          AddHom.toFun
                            { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                              map_add' :=
                                (_ :
                                  ∀ (f g : (m → R) →ₗ[R] n → R),
                                    (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                                      (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                                        (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
                            f) }.toAddHom
            f))
      (↑(Pi.basisFun R m) j) =
    ↑f (↑(Pi.basisFun R m) j)
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f : (m → R) →ₗ[R] n → R
j : m
i : n
⊢ ↑(vecMulLinear
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                    map_add' :=
                      (_ :
                        ∀ (f g : (m → R) →ₗ[R] n → R),
                          (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                            (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                              (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) },
                map_smul' :=
                  (_ :
                    ∀ (c : Rᵐᵒᵖ) (f : (m → R) →ₗ[R] n → R),
                      AddHom.toFun
                          { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                            map_add' :=
                              (_ :
                                ∀ (f g : (m → R) →ₗ[R] n → R),
                                  (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                                    (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                                      (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
                          (c • f) =
                        ↑(RingHom.id Rᵐᵒᵖ) c •
                          AddHom.toFun
                            { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                              map_add' :=
                                (_ :
                                  ∀ (f g : (m → R) →ₗ[R] n → R),
                                    (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                                      (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                                        (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
                            f) }.toAddHom
            f))
      (↑(Pi.basisFun R m) j) i =
    ↑f (↑(Pi.basisFun R m) j) i
[PROOFSTEP]
simp only [Pi.basisFun_apply, Matrix.vecMul_stdBasis, Matrix.vecMulLinear_apply]
[GOAL]
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
              map_add' :=
                (_ :
                  ∀ (f g : (m → R) →ₗ[R] n → R),
                    (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                      (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                        (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) },
          map_smul' :=
            (_ :
              ∀ (c : Rᵐᵒᵖ) (f : (m → R) →ₗ[R] n → R),
                AddHom.toFun
                    { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                      map_add' :=
                        (_ :
                          ∀ (f g : (m → R) →ₗ[R] n → R),
                            (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                              (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                                (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
                    (c • f) =
                  ↑(RingHom.id Rᵐᵒᵖ) c •
                    AddHom.toFun
                      { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                        map_add' :=
                          (_ :
                            ∀ (f g : (m → R) →ₗ[R] n → R),
                              (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                                (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                                  (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
                      f) }.toAddHom
      (vecMulLinear M) =
    M
[PROOFSTEP]
ext i j
[GOAL]
case a.h
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
              map_add' :=
                (_ :
                  ∀ (f g : (m → R) →ₗ[R] n → R),
                    (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                      (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                        (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) },
          map_smul' :=
            (_ :
              ∀ (c : Rᵐᵒᵖ) (f : (m → R) →ₗ[R] n → R),
                AddHom.toFun
                    { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                      map_add' :=
                        (_ :
                          ∀ (f g : (m → R) →ₗ[R] n → R),
                            (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                              (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                                (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
                    (c • f) =
                  ↑(RingHom.id Rᵐᵒᵖ) c •
                    AddHom.toFun
                      { toFun := fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j,
                        map_add' :=
                          (_ :
                            ∀ (f g : (m → R) →ₗ[R] n → R),
                              (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) (f + g) =
                                (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) f +
                                  (fun f i j => ↑f (↑(stdBasis R (fun x => R) i) 1) j) g) }
                      f) }.toAddHom
      (vecMulLinear M) i j =
    M i j
[PROOFSTEP]
simp only [Matrix.vecMul_stdBasis, Matrix.vecMulLinear_apply]
[GOAL]
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
⊢ ↑toLinearMapRight' 1 = LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case h.h.h
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
i✝ x✝ : m
⊢ ↑(comp (↑toLinearMapRight' 1) (single i✝)) 1 x✝ = ↑(comp LinearMap.id (single i✝)) 1 x✝
[PROOFSTEP]
simp [LinearMap.one_apply, stdBasis_apply]
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
src✝ : (fun x => (n → R) →ₗ[R] m → R) M' := ↑(LinearEquiv.symm toMatrixRight') M'
x : n → R
⊢ ↑(↑toLinearMapRight' M)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(↑toLinearMapRight' M'),
                map_add' :=
                  (_ :
                    ∀ (x y : n → R),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : n → R),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x) =
    x
[PROOFSTEP]
dsimp only
  -- porting note: needed due to non-flat structures
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
src✝ : (fun x => (n → R) →ₗ[R] m → R) M' := ↑(LinearEquiv.symm toMatrixRight') M'
x : n → R
⊢ ↑(↑toLinearMapRight' M) (↑(↑toLinearMapRight' M') x) = x
[PROOFSTEP]
rw [← Matrix.toLinearMapRight'_mul_apply, hM'M, Matrix.toLinearMapRight'_one, id_apply]
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
src✝ : (fun x => (n → R) →ₗ[R] m → R) M' := ↑(LinearEquiv.symm toMatrixRight') M'
x : m → R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(↑toLinearMapRight' M'),
              map_add' :=
                (_ :
                  ∀ (x y : n → R),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : n → R),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      (↑(↑toLinearMapRight' M) x) =
    x
[PROOFSTEP]
dsimp only
  -- porting note: needed due to non-flat structures
[GOAL]
R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
src✝ : (fun x => (n → R) →ₗ[R] m → R) M' := ↑(LinearEquiv.symm toMatrixRight') M'
x : m → R
⊢ ↑(↑toLinearMapRight' M') (↑(↑toLinearMapRight' M) x) = x
[PROOFSTEP]
rw [← Matrix.toLinearMapRight'_mul_apply, hMM', Matrix.toLinearMapRight'_one, id_apply]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ mulVecLin 1 = LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case h.h.h
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ x✝ : n
⊢ ↑(comp (mulVecLin 1) (single i✝)) 1 x✝ = ↑(comp LinearMap.id (single i✝)) 1 x✝
[PROOFSTEP]
simp [Matrix.one_apply, Pi.single_apply]
[GOAL]
R : Type u_1
inst✝¹ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix n n R
⊢ ker (mulVecLin M) = ⊥ ↔ ∀ (v : n → R), mulVec M v = 0 → v = 0
[PROOFSTEP]
simp only [Submodule.eq_bot_iff, LinearMap.mem_ker, Matrix.mulVecLin_apply]
[GOAL]
R : Type u_1
inst✝¹ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
⊢ LinearMap.range (mulVecLin M) = span R (Set.range Mᵀ)
[PROOFSTEP]
letI := Classical.decEq n
[GOAL]
R : Type u_1
inst✝¹ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
this : DecidableEq n := Classical.decEq n
⊢ LinearMap.range (mulVecLin M) = span R (Set.range Mᵀ)
[PROOFSTEP]
simp_rw [range_eq_map, ← iSup_range_stdBasis, Submodule.map_iSup, range_eq_map, ← Ideal.span_singleton_one, Ideal.span,
  Submodule.map_span, image_image, image_singleton, Matrix.mulVecLin_apply, M.mulVec_stdBasis_apply, iSup_span,
  range_eq_iUnion]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f g : (n → R) →ₗ[R] m → R
⊢ (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
    (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
      (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g
[PROOFSTEP]
ext i j
[GOAL]
case a.h
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f g : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) i j =
    ((fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
        (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g)
      i j
[PROOFSTEP]
simp only [Pi.add_apply, LinearMap.add_apply, of_apply, Matrix.add_apply]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : R
f : (n → R) →ₗ[R] m → R
⊢ AddHom.toFun
      { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
        map_add' :=
          (_ :
            ∀ (f g : (n → R) →ₗ[R] m → R),
              (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                  (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
      (c • f) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
          map_add' :=
            (_ :
              ∀ (f g : (n → R) →ₗ[R] m → R),
                (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                  (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                    (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
        f
[PROOFSTEP]
ext i j
[GOAL]
case a.h
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : R
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ AddHom.toFun
      { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
        map_add' :=
          (_ :
            ∀ (f g : (n → R) →ₗ[R] m → R),
              (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                  (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
      (c • f) i j =
    (↑(RingHom.id R) c •
        AddHom.toFun
          { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
            map_add' :=
              (_ :
                ∀ (f g : (n → R) →ₗ[R] m → R),
                  (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                    (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                      (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
          f)
      i j
[PROOFSTEP]
simp only [Pi.smul_apply, LinearMap.smul_apply, RingHom.id_apply, of_apply, Matrix.smul_apply]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
⊢ mulVecLin
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                map_add' :=
                  (_ :
                    ∀ (f g : (n → R) →ₗ[R] m → R),
                      (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                        (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                          (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) },
            map_smul' :=
              (_ :
                ∀ (c : R) (f : (n → R) →ₗ[R] m → R),
                  AddHom.toFun
                      { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                        map_add' :=
                          (_ :
                            ∀ (f g : (n → R) →ₗ[R] m → R),
                              (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                                (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                                  (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
                      (c • f) =
                    ↑(RingHom.id R) c •
                      AddHom.toFun
                        { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                          map_add' :=
                            (_ :
                              ∀ (f g : (n → R) →ₗ[R] m → R),
                                (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                                  (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                                    (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
                        f) }.toAddHom
        f) =
    f
[PROOFSTEP]
apply (Pi.basisFun R n).ext
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
⊢ ∀ (i : n),
    ↑(mulVecLin
            (AddHom.toFun
              {
                  toAddHom :=
                    { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                      map_add' :=
                        (_ :
                          ∀ (f g : (n → R) →ₗ[R] m → R),
                            (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                              (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                                (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) },
                  map_smul' :=
                    (_ :
                      ∀ (c : R) (f : (n → R) →ₗ[R] m → R),
                        AddHom.toFun
                            { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                              map_add' :=
                                (_ :
                                  ∀ (f g : (n → R) →ₗ[R] m → R),
                                    (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                                      (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                                        (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
                            (c • f) =
                          ↑(RingHom.id R) c •
                            AddHom.toFun
                              { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                                map_add' :=
                                  (_ :
                                    ∀ (f g : (n → R) →ₗ[R] m → R),
                                      (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                                        (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                                          (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
                              f) }.toAddHom
              f))
        (↑(Pi.basisFun R n) i) =
      ↑f (↑(Pi.basisFun R n) i)
[PROOFSTEP]
intro j
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
j : n
⊢ ↑(mulVecLin
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                    map_add' :=
                      (_ :
                        ∀ (f g : (n → R) →ₗ[R] m → R),
                          (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                            (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                              (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) },
                map_smul' :=
                  (_ :
                    ∀ (c : R) (f : (n → R) →ₗ[R] m → R),
                      AddHom.toFun
                          { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                            map_add' :=
                              (_ :
                                ∀ (f g : (n → R) →ₗ[R] m → R),
                                  (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                                    (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                                      (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
                          (c • f) =
                        ↑(RingHom.id R) c •
                          AddHom.toFun
                            { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                              map_add' :=
                                (_ :
                                  ∀ (f g : (n → R) →ₗ[R] m → R),
                                    (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                                      (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                                        (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
                            f) }.toAddHom
            f))
      (↑(Pi.basisFun R n) j) =
    ↑f (↑(Pi.basisFun R n) j)
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
j : n
i : m
⊢ ↑(mulVecLin
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                    map_add' :=
                      (_ :
                        ∀ (f g : (n → R) →ₗ[R] m → R),
                          (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                            (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                              (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) },
                map_smul' :=
                  (_ :
                    ∀ (c : R) (f : (n → R) →ₗ[R] m → R),
                      AddHom.toFun
                          { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                            map_add' :=
                              (_ :
                                ∀ (f g : (n → R) →ₗ[R] m → R),
                                  (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                                    (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                                      (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
                          (c • f) =
                        ↑(RingHom.id R) c •
                          AddHom.toFun
                            { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                              map_add' :=
                                (_ :
                                  ∀ (f g : (n → R) →ₗ[R] m → R),
                                    (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                                      (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                                        (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
                            f) }.toAddHom
            f))
      (↑(Pi.basisFun R n) j) i =
    ↑f (↑(Pi.basisFun R n) j) i
[PROOFSTEP]
simp only [Pi.basisFun_apply, Matrix.mulVec_stdBasis, Matrix.mulVecLin_apply, of_apply]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
              map_add' :=
                (_ :
                  ∀ (f g : (n → R) →ₗ[R] m → R),
                    (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                      (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                        (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) },
          map_smul' :=
            (_ :
              ∀ (c : R) (f : (n → R) →ₗ[R] m → R),
                AddHom.toFun
                    { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                      map_add' :=
                        (_ :
                          ∀ (f g : (n → R) →ₗ[R] m → R),
                            (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                              (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                                (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
                    (c • f) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                        map_add' :=
                          (_ :
                            ∀ (f g : (n → R) →ₗ[R] m → R),
                              (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                                (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                                  (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
                      f) }.toAddHom
      (mulVecLin M) =
    M
[PROOFSTEP]
ext i j
[GOAL]
case a.h
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
i : m
j : n
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
              map_add' :=
                (_ :
                  ∀ (f g : (n → R) →ₗ[R] m → R),
                    (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                      (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                        (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) },
          map_smul' :=
            (_ :
              ∀ (c : R) (f : (n → R) →ₗ[R] m → R),
                AddHom.toFun
                    { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                      map_add' :=
                        (_ :
                          ∀ (f g : (n → R) →ₗ[R] m → R),
                            (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                              (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                                (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
                    (c • f) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      { toFun := fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i,
                        map_add' :=
                          (_ :
                            ∀ (f g : (n → R) →ₗ[R] m → R),
                              (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) (f + g) =
                                (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) f +
                                  (fun f => ↑of fun i j => ↑f (↑(stdBasis R (fun x => R) j) 1) i) g) }
                      f) }.toAddHom
      (mulVecLin M) i j =
    M i j
[PROOFSTEP]
simp only [Matrix.mulVec_stdBasis, Matrix.mulVecLin_apply, of_apply]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ ↑toMatrix' f i j = ↑f (fun j' => if j' = j then 1 else 0) i
[PROOFSTEP]
simp only [LinearMap.toMatrix', LinearEquiv.coe_mk, of_apply]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ ↑f (↑(stdBasis R (fun x => R) j) 1) i = ↑f (fun j' => if j' = j then 1 else 0) i
[PROOFSTEP]
refine
  congr_fun ?_
    _
      -- porting note: `congr` didn't do this
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ ↑f (↑(stdBasis R (fun x => R) j) 1) = ↑f fun j' => if j' = j then 1 else 0
[PROOFSTEP]
congr
[GOAL]
case h.e_6.h
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j : n
⊢ ↑(stdBasis R (fun x => R) j) 1 = fun j' => if j' = j then 1 else 0
[PROOFSTEP]
ext j'
[GOAL]
case h.e_6.h.h
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
⊢ ↑(stdBasis R (fun x => R) j) 1 j' = if j' = j then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
h : j' = j
⊢ ↑(stdBasis R (fun x => R) j) 1 j' = 1
[PROOFSTEP]
rw [h, stdBasis_same]
[GOAL]
case neg
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] m → R
i : m
j j' : n
h : ¬j' = j
⊢ ↑(stdBasis R (fun x => R) j) 1 j' = 0
[PROOFSTEP]
apply stdBasis_ne _ _ _ _ h
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ ↑toMatrix' id = 1
[PROOFSTEP]
ext
[GOAL]
case a.h
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ x✝ : n
⊢ ↑toMatrix' id i✝ x✝ = OfNat.ofNat 1 i✝ x✝
[PROOFSTEP]
rw [Matrix.one_apply, LinearMap.toMatrix'_apply, id_apply]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix l m R
N : Matrix m n R
x : n → R
⊢ ↑(↑toLin' (M * N)) x = ↑(↑toLin' M) (↑(↑toLin' N) x)
[PROOFSTEP]
rw [Matrix.toLin'_mul, LinearMap.comp_apply]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
⊢ ↑toMatrix' (comp f g) = ↑toMatrix' f * ↑toMatrix' g
[PROOFSTEP]
suffices f.comp g = Matrix.toLin' (LinearMap.toMatrix' f * LinearMap.toMatrix' g) by
  rw [this, LinearMap.toMatrix'_toLin']
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
this : comp f g = ↑toLin' (↑toMatrix' f * ↑toMatrix' g)
⊢ ↑toMatrix' (comp f g) = ↑toMatrix' f * ↑toMatrix' g
[PROOFSTEP]
rw [this, LinearMap.toMatrix'_toLin']
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
⊢ comp f g = ↑toLin' (↑toMatrix' f * ↑toMatrix' g)
[PROOFSTEP]
rw [Matrix.toLin'_mul, Matrix.toLin'_toMatrix', Matrix.toLin'_toMatrix']
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x : R
⊢ ↑toMatrix' (↑(algebraMap R (Module.End R (n → R))) x) = ↑(scalar n) x
[PROOFSTEP]
simp [Module.algebraMap_end_eq_smul_id]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
src✝ : (fun x => (m → R) →ₗ[R] n → R) M' := ↑toLin' M'
x : m → R
⊢ ↑(↑toLin' M)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(↑toLin' M'),
                map_add' :=
                  (_ :
                    ∀ (x y : m → R),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : m → R),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x) =
    x
[PROOFSTEP]
rw [← Matrix.toLin'_mul_apply, hMM', Matrix.toLin'_one, id_apply]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
src✝ : (fun x => (m → R) →ₗ[R] n → R) M' := ↑toLin' M'
x : n → R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(↑toLin' M'),
              map_add' :=
                (_ :
                  ∀ (x y : m → R),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : m → R),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      (↑(↑toLin' M) x) =
    x
[PROOFSTEP]
simp only
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
src✝ : (fun x => (m → R) →ₗ[R] n → R) M' := ↑toLin' M'
x : n → R
⊢ ↑(↑toLin' M') (↑(↑toLin' M) x) = x
[PROOFSTEP]
rw [← Matrix.toLin'_mul_apply, hM'M, Matrix.toLin'_one, id_apply]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : (n → R) →ₗ[R] n → R
i j : n
⊢ ↑toMatrixAlgEquiv' f i j = ↑f (fun j' => if j' = j then 1 else 0) i
[PROOFSTEP]
simp [LinearMap.toMatrixAlgEquiv']
[GOAL]
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
⊢ ↑(toLin v₁ v₂) (↑(toMatrix v₁ v₂) f) = f
[PROOFSTEP]
rw [← Matrix.toLin_symm, LinearEquiv.apply_symm_apply]
[GOAL]
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
⊢ ↑(toMatrix v₁ v₂) (↑(toLin v₁ v₂) M) = M
[PROOFSTEP]
rw [← Matrix.toLin_symm, LinearEquiv.symm_apply_apply]
[GOAL]
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
⊢ ↑(toMatrix v₁ v₂) f i j = ↑(↑v₂.repr (↑f (↑v₁ j))) i
[PROOFSTEP]
rw [LinearMap.toMatrix, LinearEquiv.trans_apply, LinearMap.toMatrix'_apply, LinearEquiv.arrowCongr_apply,
  Basis.equivFun_symm_apply, Finset.sum_eq_single j, if_pos rfl, one_smul, Basis.equivFun_apply]
[GOAL]
case h₀
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
⊢ ∀ (b : n), b ∈ Finset.univ → b ≠ j → (if b = j then 1 else 0) • ↑v₁ b = 0
[PROOFSTEP]
intro j' _ hj'
[GOAL]
case h₀
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j j' : n
a✝ : j' ∈ Finset.univ
hj' : j' ≠ j
⊢ (if j' = j then 1 else 0) • ↑v₁ j' = 0
[PROOFSTEP]
rw [if_neg hj', zero_smul]
[GOAL]
case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
⊢ ¬j ∈ Finset.univ → (if j = j then 1 else 0) • ↑v₁ j = 0
[PROOFSTEP]
intro hj
[GOAL]
case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
hj : ¬j ∈ Finset.univ
⊢ (if j = j then 1 else 0) • ↑v₁ j = 0
[PROOFSTEP]
have := Finset.mem_univ j
[GOAL]
case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
hj : ¬j ∈ Finset.univ
this : j ∈ Finset.univ
⊢ (if j = j then 1 else 0) • ↑v₁ j = 0
[PROOFSTEP]
contradiction
[GOAL]
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
v : M₁
⊢ ↑(LinearEquiv.symm (Basis.equivFun v₂)) (↑(↑toLin' M) ↑(↑v₁.repr v)) = ∑ j : m, mulVec M (↑(↑v₁.repr v)) j • ↑v₂ j
[PROOFSTEP]
rw [Matrix.toLin'_apply, v₂.equivFun_symm_apply]
[GOAL]
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
i : n
⊢ ↑(↑(toLin v₁ v₂) M) (↑v₁ i) = ∑ j : m, M j i • ↑v₂ j
[PROOFSTEP]
rw [Matrix.toLin_apply, Finset.sum_congr rfl fun j _hj => ?_]
[GOAL]
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ mulVec M (↑(↑v₁.repr (↑v₁ i))) j • ↑v₂ j = M j i • ↑v₂ j
[PROOFSTEP]
rw [Basis.repr_self, Matrix.mulVec, dotProduct, Finset.sum_eq_single i, Finsupp.single_eq_same, mul_one]
[GOAL]
case h₀
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ ∀ (b : n), b ∈ Finset.univ → b ≠ i → M j b * ↑(Finsupp.single i 1) b = 0
[PROOFSTEP]
intro i' _ i'_ne
[GOAL]
case h₀
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
i' : n
a✝ : i' ∈ Finset.univ
i'_ne : i' ≠ i
⊢ M j i' * ↑(Finsupp.single i 1) i' = 0
[PROOFSTEP]
rw [Finsupp.single_eq_of_ne i'_ne.symm, mul_zero]
[GOAL]
case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
⊢ ¬i ∈ Finset.univ → M j i * ↑(Finsupp.single i 1) i = 0
[PROOFSTEP]
intros
[GOAL]
case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
a✝ : ¬i ∈ Finset.univ
⊢ M j i * ↑(Finsupp.single i 1) i = 0
[PROOFSTEP]
have := Finset.mem_univ i
[GOAL]
case h₁
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
a✝ : ¬i ∈ Finset.univ
this : i ∈ Finset.univ
⊢ M j i * ↑(Finsupp.single i 1) i = 0
[PROOFSTEP]
contradiction
[GOAL]
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
⊢ ↑(toMatrix v₁ v₁) id = 1
[PROOFSTEP]
ext i j
[GOAL]
case a.h
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
i j : n
⊢ ↑(toMatrix v₁ v₁) id i j = OfNat.ofNat 1 i j
[PROOFSTEP]
simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]
[GOAL]
R : Type u_1
inst✝⁷ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
⊢ ↑(toLin v₁ v₁) 1 = LinearMap.id
[PROOFSTEP]
rw [← LinearMap.toMatrix_id v₁, Matrix.toLin_toMatrix]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝¹ : DecidableEq M₁
inst✝ : DecidableEq M₂
f : M₁ →ₗ[R] M₂
k : m
i : n
⊢ ↑(toMatrix (Basis.reindexRange v₁) (Basis.reindexRange v₂)) f
      { val := ↑v₂ k, property := (_ : ↑v₂ k ∈ Set.range ↑v₂) }
      { val := ↑v₁ i, property := (_ : ↑v₁ i ∈ Set.range ↑v₁) } =
    ↑(toMatrix v₁ v₂) f k i
[PROOFSTEP]
simp_rw [LinearMap.toMatrix_apply, Basis.reindexRange_self, Basis.reindexRange_repr]
[GOAL]
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq m
f : M₂ →ₗ[R] M₃
g : M₁ →ₗ[R] M₂
⊢ ↑(toMatrix v₁ v₃) (comp f g) = ↑(toMatrix v₂ v₃) f * ↑(toMatrix v₁ v₂) g
[PROOFSTEP]
simp_rw [LinearMap.toMatrix, LinearEquiv.trans_apply, LinearEquiv.arrowCongr_comp _ v₂.equivFun,
  LinearMap.toMatrix'_comp]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f g : M₁ →ₗ[R] M₁
⊢ ↑(toMatrix v₁ v₁) (f * g) = ↑(toMatrix v₁ v₁) f * ↑(toMatrix v₁ v₁) g
[PROOFSTEP]
rw [LinearMap.mul_eq_comp, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
x : R
⊢ ↑(toMatrix v₁ v₁) (↑(algebraMap R (Module.End R M₁)) x) = ↑(scalar n) x
[PROOFSTEP]
simp [Module.algebraMap_end_eq_smul_id, LinearMap.toMatrix_id]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f : M₁ →ₗ[R] M₂
x : M₁
⊢ mulVec (↑(toMatrix v₁ v₂) f) ↑(↑v₁.repr x) = ↑(↑v₂.repr (↑f x))
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ mulVec (↑(toMatrix v₁ v₂) f) (↑(↑v₁.repr x)) i = ↑(↑v₂.repr (↑f x)) i
[PROOFSTEP]
rw [← Matrix.toLin'_apply, LinearMap.toMatrix, LinearEquiv.trans_apply, Matrix.toLin'_toMatrix',
  LinearEquiv.arrowCongr_apply, v₂.equivFun_apply]
[GOAL]
case h
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ ↑(↑v₂.repr (↑f (↑(LinearEquiv.symm (Basis.equivFun v₁)) ↑(↑v₁.repr x)))) i = ↑(↑v₂.repr (↑f x)) i
[PROOFSTEP]
congr
[GOAL]
case h.e_a.h.e_6.h.h.e_6.h
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ ↑(LinearEquiv.symm (Basis.equivFun v₁)) ↑(↑v₁.repr x) = x
[PROOFSTEP]
exact v₁.equivFun.symm_apply_apply x
[GOAL]
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
⊢ ↑(toMatrix b' b) ↑(Basis.equiv b' b (Equiv.refl l)) = 1
[PROOFSTEP]
ext i j
[GOAL]
case a.h
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
i j : l
⊢ ↑(toMatrix b' b) (↑(Basis.equiv b' b (Equiv.refl l))) i j = OfNat.ofNat 1 i j
[PROOFSTEP]
simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]
[GOAL]
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
⊢ ↑(toLin v₁ v₃) (A * B) = comp (↑(toLin v₂ v₃) A) (↑(toLin v₁ v₂) B)
[PROOFSTEP]
apply (LinearMap.toMatrix v₁ v₃).injective
[GOAL]
case a
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
⊢ ↑(toMatrix v₁ v₃) (↑(toLin v₁ v₃) (A * B)) = ↑(toMatrix v₁ v₃) (comp (↑(toLin v₂ v₃) A) (↑(toLin v₁ v₂) B))
[PROOFSTEP]
haveI : DecidableEq l := fun _ _ => Classical.propDecidable _
[GOAL]
case a
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
⊢ ↑(toMatrix v₁ v₃) (↑(toLin v₁ v₃) (A * B)) = ↑(toMatrix v₁ v₃) (comp (↑(toLin v₂ v₃) A) (↑(toLin v₁ v₂) B))
[PROOFSTEP]
rw [LinearMap.toMatrix_comp v₁ v₂ v₃]
[GOAL]
case a
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
⊢ ↑(toMatrix v₁ v₃) (↑(toLin v₁ v₃) (A * B)) =
    ↑(toMatrix v₂ v₃) (↑(toLin v₂ v₃) A) * ↑(toMatrix v₁ v₂) (↑(toLin v₁ v₂) B)
[PROOFSTEP]
repeat' rw [LinearMap.toMatrix_toLin]
[GOAL]
case a
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
⊢ ↑(toMatrix v₁ v₃) (↑(toLin v₁ v₃) (A * B)) =
    ↑(toMatrix v₂ v₃) (↑(toLin v₂ v₃) A) * ↑(toMatrix v₁ v₂) (↑(toLin v₁ v₂) B)
[PROOFSTEP]
rw [LinearMap.toMatrix_toLin]
[GOAL]
case a
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
⊢ A * B = ↑(toMatrix v₂ v₃) (↑(toLin v₂ v₃) A) * ↑(toMatrix v₁ v₂) (↑(toLin v₁ v₂) B)
[PROOFSTEP]
rw [LinearMap.toMatrix_toLin]
[GOAL]
case a
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
⊢ A * B = A * ↑(toMatrix v₁ v₂) (↑(toLin v₁ v₂) B)
[PROOFSTEP]
rw [LinearMap.toMatrix_toLin]
[GOAL]
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Fintype l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
x : M₁
⊢ ↑(↑(toLin v₁ v₃) (A * B)) x = ↑(↑(toLin v₂ v₃) A) (↑(↑(toLin v₁ v₂) B) x)
[PROOFSTEP]
rw [Matrix.toLin_mul v₁ v₂, LinearMap.comp_apply]
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Fintype m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
src✝ : (fun x => M₁ →ₗ[R] M₂) M := ↑(toLin v₁ v₂) M
x : M₁
⊢ ↑(↑(toLin v₂ v₁) M')
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(↑(toLin v₁ v₂) M),
                map_add' :=
                  (_ :
                    ∀ (x y : M₁),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : M₁),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x) =
    x
[PROOFSTEP]
rw [← Matrix.toLin_mul_apply, hM'M, Matrix.toLin_one, id_apply]
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Fintype m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
src✝ : (fun x => M₁ →ₗ[R] M₂) M := ↑(toLin v₁ v₂) M
x : M₂
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(↑(toLin v₁ v₂) M),
              map_add' :=
                (_ :
                  ∀ (x y : M₁),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : M₁),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      (↑(↑(toLin v₂ v₁) M') x) =
    x
[PROOFSTEP]
simp only
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Fintype m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
src✝ : (fun x => M₁ →ₗ[R] M₂) M := ↑(toLin v₁ v₂) M
x : M₂
⊢ ↑(↑(toLin v₁ v₂) M) (↑(↑(toLin v₂ v₁) M') x) = x
[PROOFSTEP]
rw [← Matrix.toLin_mul_apply, hMM', Matrix.toLin_one, id_apply]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f : M₁ →ₗ[R] M₁
⊢ ↑(toLinAlgEquiv v₁) (↑(toMatrixAlgEquiv v₁) f) = f
[PROOFSTEP]
rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.apply_symm_apply]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
M : Matrix n n R
⊢ ↑(toMatrixAlgEquiv v₁) (↑(toLinAlgEquiv v₁) M) = M
[PROOFSTEP]
rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.symm_apply_apply]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f : M₁ →ₗ[R] M₁
i j : n
⊢ ↑(toMatrixAlgEquiv v₁) f i j = ↑(↑v₁.repr (↑f (↑v₁ j))) i
[PROOFSTEP]
simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_apply]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
M : Matrix n n R
v : M₁
⊢ ↑(LinearEquiv.symm (Basis.equivFun v₁)) (↑(↑toLinAlgEquiv' M) ↑(↑v₁.repr v)) =
    ∑ j : n, mulVec M (↑(↑v₁.repr v)) j • ↑v₁ j
[PROOFSTEP]
rw [Matrix.toLinAlgEquiv'_apply, v₁.equivFun_symm_apply]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
⊢ ↑(toMatrixAlgEquiv v₁) id = 1
[PROOFSTEP]
simp_rw [LinearMap.toMatrixAlgEquiv, AlgEquiv.ofLinearEquiv_apply, LinearMap.toMatrix_id]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
⊢ ↑(toLinAlgEquiv v₁) 1 = LinearMap.id
[PROOFSTEP]
rw [← LinearMap.toMatrixAlgEquiv_id v₁, Matrix.toLinAlgEquiv_toMatrixAlgEquiv]
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Fintype m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq M₁
f : M₁ →ₗ[R] M₁
k i : n
⊢ ↑(toMatrixAlgEquiv (Basis.reindexRange v₁)) f { val := ↑v₁ k, property := (_ : ↑v₁ k ∈ Set.range ↑v₁) }
      { val := ↑v₁ i, property := (_ : ↑v₁ i ∈ Set.range ↑v₁) } =
    ↑(toMatrixAlgEquiv v₁) f k i
[PROOFSTEP]
simp_rw [LinearMap.toMatrixAlgEquiv_apply, Basis.reindexRange_self, Basis.reindexRange_repr]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f g : M₁ →ₗ[R] M₁
⊢ ↑(toMatrixAlgEquiv v₁) (comp f g) = ↑(toMatrixAlgEquiv v₁) f * ↑(toMatrixAlgEquiv v₁) g
[PROOFSTEP]
simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f g : M₁ →ₗ[R] M₁
⊢ ↑(toMatrixAlgEquiv v₁) (f * g) = ↑(toMatrixAlgEquiv v₁) f * ↑(toMatrixAlgEquiv v₁) g
[PROOFSTEP]
rw [LinearMap.mul_eq_comp, LinearMap.toMatrixAlgEquiv_comp v₁ f g]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
A B : Matrix n n R
⊢ ↑(toLinAlgEquiv v₁) (A * B) = comp (↑(toLinAlgEquiv v₁) A) (↑(toLinAlgEquiv v₁) B)
[PROOFSTEP]
convert Matrix.toLin_mul v₁ v₁ v₁ A B
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
a b c d : R
x : R × R
⊢ ↑(↑(toLin (Basis.finTwoProd R) (Basis.finTwoProd R)) (↑of ![![a, b], ![c, d]])) x =
    (a * x.fst + b * x.snd, c * x.fst + d * x.snd)
[PROOFSTEP]
simp [Matrix.toLin_apply, Matrix.mulVec, Matrix.dotProduct, (Prod.smul_mk)]
[GOAL]
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
x : R
⊢ ↑(toMatrix v₁ v₁) (DistribMulAction.toLinearMap R M₁ x) = Matrix.diagonal fun x_1 => x
[PROOFSTEP]
ext
[GOAL]
case a.h
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
x : R
i✝ x✝ : n
⊢ ↑(toMatrix v₁ v₁) (DistribMulAction.toLinearMap R M₁ x) i✝ x✝ = Matrix.diagonal (fun x_1 => x) i✝ x✝
[PROOFSTEP]
rw [LinearMap.toMatrix_apply, DistribMulAction.toLinearMap_apply, LinearEquiv.map_smul, Basis.repr_self,
  Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply, Pi.single_apply]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x : S
i j : m
⊢ ↑(toMatrix b b) (↑(lmul R S) x) i j = ↑(↑b.repr (x * ↑b j)) i
[PROOFSTEP]
simp only [LinearMap.toMatrix_apply', coe_lmul_eq_mul, LinearMap.mul_apply']
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
⊢ (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1
[PROOFSTEP]
dsimp only
  -- porting node: needed due to new-style structures
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
⊢ ↑(toMatrix b b) (↑(lmul R S) 1) = 1
[PROOFSTEP]
rw [AlgHom.map_one, LinearMap.toMatrix_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ OneHom.toFun
      { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
        map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
          map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
        x *
      OneHom.toFun
        { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
          map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
        y
[PROOFSTEP]
dsimp only
  -- porting node: needed due to new-style structures
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ ↑(toMatrix b b) (↑(lmul R S) (x * y)) = ↑(toMatrix b b) (↑(lmul R S) x) * ↑(toMatrix b b) (↑(lmul R S) y)
[PROOFSTEP]
rw [AlgHom.map_mul, LinearMap.toMatrix_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
              map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : S),
                OneHom.toFun
                    { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                      map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                        map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                        map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                      y) })
      0 =
    0
[PROOFSTEP]
dsimp only
  -- porting node: needed due to new-style structures
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
⊢ ↑(toMatrix b b) (↑(lmul R S) 0) = 0
[PROOFSTEP]
rw [AlgHom.map_zero, LinearEquiv.map_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
              map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : S),
                OneHom.toFun
                    { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                      map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                        map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                        map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                      y) })
      (x + y) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : S),
                  OneHom.toFun
                      { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                        map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                          map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                          map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                        y) })
        x +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : S),
                  OneHom.toFun
                      { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                        map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                          map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                          map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                        y) })
        y
[PROOFSTEP]
dsimp only
  -- porting node: needed due to new-style structures
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ ↑(toMatrix b b) (↑(lmul R S) (x + y)) = ↑(toMatrix b b) (↑(lmul R S) x) + ↑(toMatrix b b) (↑(lmul R S) y)
[PROOFSTEP]
rw [AlgHom.map_add, LinearEquiv.map_add]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
r : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                    map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : S),
                      OneHom.toFun
                          { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                            map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                          (x * y) =
                        OneHom.toFun
                            { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                              map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                              map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                            y) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                            map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (x y : S),
                              OneHom.toFun
                                  { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                    map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                                  (x * y) =
                                OneHom.toFun
                                    { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                      map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                                    x *
                                  OneHom.toFun
                                    { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                      map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                                    y) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : S),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                              map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : S),
                                OneHom.toFun
                                    { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                      map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                                    (x * y) =
                                  OneHom.toFun
                                      { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                        map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                                      x *
                                    OneHom.toFun
                                      { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                        map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                                      y) })
                      (x + y) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : S),
                                  OneHom.toFun
                                      { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                        map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                                      (x * y) =
                                    OneHom.toFun
                                        { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                          map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                                        x *
                                      OneHom.toFun
                                        { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                          map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                                        y) })
                        x +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : S),
                                  OneHom.toFun
                                      { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                        map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                                      (x * y) =
                                    OneHom.toFun
                                        { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                          map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                                        x *
                                      OneHom.toFun
                                        { toFun := fun x => ↑(toMatrix b b) (↑(lmul R S) x),
                                          map_one' := (_ : (fun x => ↑(toMatrix b b) (↑(lmul R S) x)) 1 = 1) }
                                        y) })
                        y) })
      (↑(algebraMap R S) r) =
    ↑(algebraMap R (Matrix m m R)) r
[PROOFSTEP]
dsimp only
  -- porting node: needed due to new-style structures
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
r : R
⊢ ↑(toMatrix b b) (↑(lmul R S) (↑(algebraMap R S) r)) = ↑(algebraMap R (Matrix m m R)) r
[PROOFSTEP]
ext
[GOAL]
case a.h
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
r : R
i✝ x✝ : m
⊢ ↑(toMatrix b b) (↑(lmul R S) (↑(algebraMap R S) r)) i✝ x✝ = ↑(algebraMap R (Matrix m m R)) r i✝ x✝
[PROOFSTEP]
rw [lmul_algebraMap, toMatrix_lsmul, algebraMap_eq_diagonal, Pi.algebraMap_def, Algebra.id.map_eq_self]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x : S
i j : m
⊢ ↑(leftMulMatrix b) x i j = ↑(↑b.repr (x * ↑b j)) i
[PROOFSTEP]
rw [leftMulMatrix_apply, toMatrix_lmul' b x i j]
[GOAL]
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x x' : S
h : ↑(leftMulMatrix b) x = ↑(leftMulMatrix b) x'
⊢ ↑(↑(lmul R S) x) 1 = ↑(↑(lmul R S) x') 1
[PROOFSTEP]
rw [(LinearMap.toMatrix b b).injective h]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : T
ik jk : m × n
⊢ ↑(leftMulMatrix (Basis.smul b c)) x ik jk = ↑(leftMulMatrix b) (↑(leftMulMatrix c) x ik.snd jk.snd) ik.fst jk.fst
[PROOFSTEP]
simp only [leftMulMatrix_apply, LinearMap.toMatrix_apply, mul_comm, Basis.smul_apply, Basis.smul_repr,
  Finsupp.smul_apply, id.smul_eq_mul, LinearEquiv.map_smul, mul_smul_comm, coe_lmul_eq_mul, LinearMap.mul_apply']
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
⊢ ↑(leftMulMatrix (Basis.smul b c)) (↑(algebraMap S T) x) = blockDiagonal fun x_1 => ↑(leftMulMatrix b) x
[PROOFSTEP]
ext ⟨i, k⟩ ⟨j, k'⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ ↑(leftMulMatrix (Basis.smul b c)) (↑(algebraMap S T) x) (i, k) (j, k') =
    blockDiagonal (fun x_1 => ↑(leftMulMatrix b) x) (i, k) (j, k')
[PROOFSTEP]
rw [smul_leftMulMatrix, AlgHom.commutes, blockDiagonal_apply, algebraMap_matrix_apply]
[GOAL]
case a.mk.h.mk
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ ↑(leftMulMatrix b) (if (i, k).snd = (j, k').snd then ↑(algebraMap S S) x else 0) (i, k).fst (j, k').fst =
    if (i, k).snd = (j, k').snd then ↑(leftMulMatrix b) x (i, k).fst (j, k').fst else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
h : (i, k).snd = (j, k').snd
⊢ ↑(leftMulMatrix b) (if (i, k).snd = (j, k').snd then ↑(algebraMap S S) x else 0) (i, k).fst (j, k').fst =
    ↑(leftMulMatrix b) x (i, k).fst (j, k').fst
[PROOFSTEP]
simp only at h 
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
h : ¬(i, k).snd = (j, k').snd
⊢ ↑(leftMulMatrix b) (if (i, k).snd = (j, k').snd then ↑(algebraMap S S) x else 0) (i, k).fst (j, k').fst = 0
[PROOFSTEP]
simp only at h 
[GOAL]
case pos
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
h : k = k'
⊢ ↑(leftMulMatrix b) (if (i, k).snd = (j, k').snd then ↑(algebraMap S S) x else 0) (i, k).fst (j, k').fst =
    ↑(leftMulMatrix b) x (i, k).fst (j, k').fst
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
h : ¬k = k'
⊢ ↑(leftMulMatrix b) (if (i, k).snd = (j, k').snd then ↑(algebraMap S S) x else 0) (i, k).fst (j, k').fst = 0
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i j : m
k : n
⊢ ↑(leftMulMatrix (Basis.smul b c)) (↑(algebraMap S T) x) (i, k) (j, k) = ↑(leftMulMatrix b) x i j
[PROOFSTEP]
rw [smul_leftMulMatrix_algebraMap, blockDiagonal_apply_eq]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Ring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i j : m
k k' : n
h : k ≠ k'
⊢ ↑(leftMulMatrix (Basis.smul b c)) (↑(algebraMap S T) x) (i, k) (j, k') = 0
[PROOFSTEP]
rw [smul_leftMulMatrix_algebraMap, blockDiagonal_apply_ne _ _ _ h]
[GOAL]
R : Type v
inst✝⁷ : CommRing R
n : Type u_1
inst✝⁶ : DecidableEq n
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M₁ ≃ₗ[R] M₂
src✝ : Module.End R M₁ ≃ₗ[R] Module.End R M₂ := conj e
f g : Module.End R M₁
⊢ Equiv.toFun
      { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (f * g) =
    Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        f *
      Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        g
[PROOFSTEP]
apply e.arrowCongr_comp
[GOAL]
R : Type v
inst✝⁷ : CommRing R
n : Type u_1
inst✝⁶ : DecidableEq n
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M₁ ≃ₗ[R] M₂
src✝ : Module.End R M₁ ≃ₗ[R] Module.End R M₂ := conj e
r : R
⊢ Equiv.toFun
      { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (↑(algebraMap R (Module.End R M₁)) r) =
    ↑(algebraMap R (Module.End R M₂)) r
[PROOFSTEP]
change e.conj (r • LinearMap.id) = r • LinearMap.id
[GOAL]
R : Type v
inst✝⁷ : CommRing R
n : Type u_1
inst✝⁶ : DecidableEq n
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
e : M₁ ≃ₗ[R] M₂
src✝ : Module.End R M₁ ≃ₗ[R] Module.End R M₂ := conj e
r : R
⊢ ↑(conj e) (r • LinearMap.id) = r • LinearMap.id
[PROOFSTEP]
rw [LinearEquiv.map_smul, LinearEquiv.conj_id]
