[GOAL]
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
⊢ Equiv.toFun
      { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
        invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
        left_inv :=
          (_ :
            ∀ (A : Matrix n n (DualNumber R)),
              (fun d => ↑of fun i j => (fst d i j, snd d i j))
                  ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                A),
        right_inv :=
          (_ :
            ∀ (d : DualNumber (Matrix n n R)),
              (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                  ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                d) }
      (A * B) =
    Equiv.toFun
        { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
          invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
          left_inv :=
            (_ :
              ∀ (A : Matrix n n (DualNumber R)),
                (fun d => ↑of fun i j => (fst d i j, snd d i j))
                    ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                  A),
          right_inv :=
            (_ :
              ∀ (d : DualNumber (Matrix n n R)),
                (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                    ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                  d) }
        A *
      Equiv.toFun
        { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
          invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
          left_inv :=
            (_ :
              ∀ (A : Matrix n n (DualNumber R)),
                (fun d => ↑of fun i j => (fst d i j, snd d i j))
                    ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                  A),
          right_inv :=
            (_ :
              ∀ (d : DualNumber (Matrix n n R)),
                (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                    ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                  d) }
        B
[PROOFSTEP]
ext
[GOAL]
case h1.a.h
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ x✝ : n
⊢ fst
      (Equiv.toFun
        { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
          invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
          left_inv :=
            (_ :
              ∀ (A : Matrix n n (DualNumber R)),
                (fun d => ↑of fun i j => (fst d i j, snd d i j))
                    ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                  A),
          right_inv :=
            (_ :
              ∀ (d : DualNumber (Matrix n n R)),
                (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                    ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                  d) }
        (A * B))
      i✝ x✝ =
    fst
      (Equiv.toFun
          { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
            invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
            left_inv :=
              (_ :
                ∀ (A : Matrix n n (DualNumber R)),
                  (fun d => ↑of fun i j => (fst d i j, snd d i j))
                      ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                    A),
            right_inv :=
              (_ :
                ∀ (d : DualNumber (Matrix n n R)),
                  (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                      ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                    d) }
          A *
        Equiv.toFun
          { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
            invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
            left_inv :=
              (_ :
                ∀ (A : Matrix n n (DualNumber R)),
                  (fun d => ↑of fun i j => (fst d i j, snd d i j))
                      ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                    A),
            right_inv :=
              (_ :
                ∀ (d : DualNumber (Matrix n n R)),
                  (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                      ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                    d) }
          B)
      i✝ x✝
[PROOFSTEP]
dsimp [mul_apply]
[GOAL]
case h1.a.h
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ x✝ : n
⊢ fst (Finset.sum Finset.univ fun j => A i✝ j * B j x✝) = Finset.sum Finset.univ fun j => fst (A i✝ j) * fst (B j x✝)
[PROOFSTEP]
simp_rw [fst_sum]
[GOAL]
case h1.a.h
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ x✝ : n
⊢ (Finset.sum Finset.univ fun i => fst (A i✝ i * B i x✝)) = Finset.sum Finset.univ fun j => fst (A i✝ j) * fst (B j x✝)
[PROOFSTEP]
rfl
[GOAL]
case h2.a.h
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ x✝ : n
⊢ snd
      (Equiv.toFun
        { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
          invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
          left_inv :=
            (_ :
              ∀ (A : Matrix n n (DualNumber R)),
                (fun d => ↑of fun i j => (fst d i j, snd d i j))
                    ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                  A),
          right_inv :=
            (_ :
              ∀ (d : DualNumber (Matrix n n R)),
                (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                    ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                  d) }
        (A * B))
      i✝ x✝ =
    snd
      (Equiv.toFun
          { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
            invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
            left_inv :=
              (_ :
                ∀ (A : Matrix n n (DualNumber R)),
                  (fun d => ↑of fun i j => (fst d i j, snd d i j))
                      ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                    A),
            right_inv :=
              (_ :
                ∀ (d : DualNumber (Matrix n n R)),
                  (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                      ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                    d) }
          A *
        Equiv.toFun
          { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
            invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
            left_inv :=
              (_ :
                ∀ (A : Matrix n n (DualNumber R)),
                  (fun d => ↑of fun i j => (fst d i j, snd d i j))
                      ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                    A),
            right_inv :=
              (_ :
                ∀ (d : DualNumber (Matrix n n R)),
                  (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                      ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                    d) }
          B)
      i✝ x✝
[PROOFSTEP]
simp_rw [snd_mul, smul_eq_mul, op_smul_eq_mul]
[GOAL]
case h2.a.h
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ x✝ : n
⊢ snd (↑of fun i j => fst ((A * B) i j), ↑of fun i j => snd ((A * B) i j)) i✝ x✝ =
    (fst (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)) *
          snd (↑of fun i j => fst (B i j), ↑of fun i j => snd (B i j)) +
        snd (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)) *
          fst (↑of fun i j => fst (B i j), ↑of fun i j => snd (B i j)))
      i✝ x✝
[PROOFSTEP]
simp [mul_apply, snd_sum, snd_mul]
[GOAL]
case h2.a.h
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ x✝ : n
⊢ (Finset.sum Finset.univ fun x => fst (A i✝ x) * snd (B x x✝) + snd (A i✝ x) * fst (B x x✝)) =
    (Finset.sum Finset.univ fun x => fst (A i✝ x) * snd (B x x✝)) +
      Finset.sum Finset.univ fun x => snd (A i✝ x) * fst (B x x✝)
[PROOFSTEP]
rw [← Finset.sum_add_distrib]
[GOAL]
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ Equiv.toFun
      { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
        invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
        left_inv :=
          (_ :
            ∀ (A : Matrix n n (DualNumber R)),
              (fun d => ↑of fun i j => (fst d i j, snd d i j))
                  ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                A),
        right_inv :=
          (_ :
            ∀ (d : DualNumber (Matrix n n R)),
              (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                  ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                d) }
      (↑(algebraMap R (Matrix n n (DualNumber R))) r) =
    ↑(algebraMap R (DualNumber (Matrix n n R))) r
[PROOFSTEP]
simp_rw [algebraMap_eq_inl', algebraMap_eq_diagonal, Pi.algebraMap_def, Algebra.id.map_eq_self, algebraMap_eq_inl, ←
  diagonal_map (inl_zero R), map_apply, fst_inl, snd_inl]
[GOAL]
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (↑of fun i j => diagonal (fun m => r) i j, ↑of fun i j => 0) = inl (diagonal fun m => r)
[PROOFSTEP]
rfl
