-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
n : Type u_3
inst_3 : Fintype n
inst_4 : DecidableEq n
b : Module.Basis n R V
A : SpecialLinearGroup n R
rw :
  Eq (α := (n → R) →ₗ[R] n → R)
    (↑(↑((fun (A : SpecialLinearGroup n R) ↦
                (Subtype.mk (p := fun (u : (n → R) ≃ₗ[R] n → R) ↦
                    Eq.{u_1 + 1} (α := Rˣ)
                      (((LinearEquiv.det (R := R) (M := n → R) : ((n → R) ≃ₗ[R] n → R) →* Rˣ) :
                            (a : (n → R) ≃ₗ[R] n → R) → Rˣ)
                          u :
                        Rˣ)
                      (1 : Rˣ))
                    ((toLin' : (a : SpecialLinearGroup n R) → (n → R) ≃ₗ[R] n → R) A) ⋯ :
                  { u : (n → R) ≃ₗ[R] n → R //
                    Eq.{u_1 + 1} (α := Rˣ)
                      (((LinearEquiv.det (R := R) (M := n → R) : ((n → R) ≃ₗ[R] n → R) →* Rˣ) :
                            (a : (n → R) ≃ₗ[R] n → R) → Rˣ)
                          u :
                        Rˣ)
                      (1 : Rˣ) }))
              A) :
          (n → R) ≃ₗ[R] n → R) :
      (n → R) →ₗ[R] n → R)
    ((LinearEquiv.symm LinearMap.toMatrix' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R)
      ((fun (a : { A : Matrix n n R // A.det = 1 }) ↦ (↑a : Matrix n n R)) A))
⊢ Eq (α := Matrix n n R)
    ((fun (a : { A : Matrix n n R // A.det = 1 }) ↦ (↑a : Matrix n n R))
      ((fun (u : _root_.SpecialLinearGroup R (n → R)) ↦
          (Subtype.mk (p := fun (A : Matrix n n R) ↦ A.det = 1)
              ((LinearMap.toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R)
                (↑(↑u : (n → R) ≃ₗ[R] n → R) : (n → R) →ₗ[R] n → R))
              ⋯ :
            { A : Matrix n n R // A.det = 1 }))
        ((fun (A : SpecialLinearGroup n R) ↦
            (Subtype.mk (p := fun (u : (n → R) ≃ₗ[R] n → R) ↦
                Eq.{u_1 + 1} (α := Rˣ)
                  (((LinearEquiv.det (R := R) (M := n → R) : ((n → R) ≃ₗ[R] n → R) →* Rˣ) :
                        (a : (n → R) ≃ₗ[R] n → R) → Rˣ)
                      u :
                    Rˣ)
                  (1 : Rˣ))
                ((toLin' : (a : SpecialLinearGroup n R) → (n → R) ≃ₗ[R] n → R) A) ⋯ :
              { u : (n → R) ≃ₗ[R] n → R //
                Eq.{u_1 + 1} (α := Rˣ)
                  (((LinearEquiv.det (R := R) (M := n → R) : ((n → R) ≃ₗ[R] n → R) →* Rˣ) :
                        (a : (n → R) ≃ₗ[R] n → R) → Rˣ)
                      u :
                    Rˣ)
                  (1 : Rˣ) }))
          A)))
    ((fun (a : { A : Matrix n n R // A.det = 1 }) ↦ (↑a : Matrix n n R)) A)
have rw₁ : Eq (α := (n → R) →ₗ[R] n → R)
  (↑(↑((fun (A : SpecialLinearGroup n R) ↦
              (Subtype.mk (p := fun (u : (n → R) ≃ₗ[R] n → R) ↦
                  Eq.{u_1 + 1} (α := Rˣ)
                    (((LinearEquiv.det (R := R) (M := n → R) : ((n → R) ≃ₗ[R] n → R) →* Rˣ) :
                          (a : (n → R) ≃ₗ[R] n → R) → Rˣ)
                        u :
                      Rˣ)
                    (1 : Rˣ))
                  ((toLin' : (a : SpecialLinearGroup n R) → (n → R) ≃ₗ[R] n → R) A) sorry :
                { u : (n → R) ≃ₗ[R] n → R //
                  Eq.{u_1 + 1} (α := Rˣ)
                    (((LinearEquiv.det (R := R) (M := n → R) : ((n → R) ≃ₗ[R] n → R) →* Rˣ) :
                          (a : (n → R) ≃ₗ[R] n → R) → Rˣ)
                        u :
                      Rˣ)
                    (1 : Rˣ) }))
            A) :
        (n → R) ≃ₗ[R] n → R) :
    (n → R) →ₗ[R] n → R)
  ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R)
    ((fun (a : { A : Matrix n n R // A.det = 1 }) ↦ (↑a : Matrix n n R)) A))
Tactic: rw [← LinearEquiv.eq_symm_apply, LinearMap.toMatrix'_symm,
      Matrix.SpecialLinearGroup.toLin'_to_linearMap]