-- 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
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
g : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this_1 : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R :=
  MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b)
r : R
hr : r ^ Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R V) = 1
this :
  Eq (α := Matrix.{u_2, u_2, u_1} (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    (↑((MulEquiv.symm (Matrix.SpecialLinearGroup.toLin_equiv b) :
            (a : SpecialLinearGroup R V) → Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R)
          g) :
      Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
    ((Matrix.of :
        (a : Module.Free.ChooseBasisIndex R V → Module.Free.ChooseBasisIndex R V → R) →
          Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
      fun (i j : Module.Free.ChooseBasisIndex R V) ↦
      ((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
            ((fun (x : V) ↦ (((↑g : V ≃ₗ[R] V) : (a : V) → V) x : V))
              ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j)) :
          (a : Module.Free.ChooseBasisIndex R V) → R)
        i)
⊢ (∀ (i j : Module.Free.ChooseBasisIndex R V),
      Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : Module.Free.ChooseBasisIndex R V) ↦ r) i j : R)
        ((((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
                  (((↑g : V ≃ₗ[R] V) : (a : V) → V) ((b : (a : Module.Free.ChooseBasisIndex R V) → V) j : V)) :
                Finsupp.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R) :
              (a : Module.Free.ChooseBasisIndex R V) → R)
            i :
          R)) ↔
    ∀ (i j : Module.Free.ChooseBasisIndex R V),
      Eq.{u_1 + 1} (α := R)
        ((LinearMap.toMatrix b b :
              (a : V →ₗ[R] V) → Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
            (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) i j :
          R)
        ((LinearMap.toMatrix b b :
              (a : V →ₗ[R] V) → Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
            (HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) i j :
          R)
have h : ∀ (a b_1 : Module.Free.ChooseBasisIndex R V),
  Eq.{u_1 + 1} (α := R) (Matrix.diagonal (fun (x : Module.Free.ChooseBasisIndex R V) ↦ r) a b_1 : R)
      ((((b.repr : (a : V) → Module.Free.ChooseBasisIndex R V →₀ R)
                (((↑g : V ≃ₗ[R] V) : (a : V) → V) ((b : (a : Module.Free.ChooseBasisIndex R V) → V) b_1 : V)) :
              Finsupp.{u_2, u_1} (Module.Free.ChooseBasisIndex R V) R) :
            (a : Module.Free.ChooseBasisIndex R V) → R)
          a :
        R) ↔
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.toMatrix b b :
            (a : V →ₗ[R] V) → Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
          (↑(↑g : V ≃ₗ[R] V) : V →ₗ[R] V) a b_1 :
        R)
      ((LinearMap.toMatrix b b :
            (a : V →ₗ[R] V) → Matrix (Module.Free.ChooseBasisIndex R V) (Module.Free.ChooseBasisIndex R V) R)
          (HSMul.hSMul (β := V →ₗ[R] V) r LinearMap.id) a b_1 :
        R)
Tactic: apply forall₂_congr