-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
Goal:
R : Type u_1
inst : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
a :
  (transposeAddEquiv (Fin n) (Fin n) R : (a : Matrix (Fin n) (Fin n) R) → Matrix (Fin n) (Fin n) R)
      ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin n) (Fin n) Rᵐᵒᵖ) → Matrix (Fin n) (Fin n) R)
          (HMul.hMul (α := Matrix (Fin n) (Fin m) Rᵐᵒᵖ) (β := Matrix (Fin m) (Fin n) Rᵐᵒᵖ)
            ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin n) (Fin m) Rᵐᵒᵖ) g :
              Matrix (Fin n) (Fin m) Rᵐᵒᵖ)
            ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin m) (Fin n) Rᵐᵒᵖ) f :
              Matrix (Fin m) (Fin n) Rᵐᵒᵖ)) :
        Matrix (Fin n) (Fin n) R) =
    HMul.hMul (α := Matrix (Fin n) (Fin m) R) (β := Matrix (Fin m) (Fin n) R)
      ((AddEquiv.toEquiv (transposeAddEquiv (Fin m) (Fin n) R) :
            (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin n) (Fin m) R)
          f :
        Matrix (Fin n) (Fin m) R)
      ((AddEquiv.toEquiv (transposeAddEquiv (Fin n) (Fin m) R) :
            (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin m) (Fin n) R)
          g :
        Matrix (Fin m) (Fin n) R)
a₁ :
  Eq (α := Matrix (Fin n) (Fin n) R)
    ((transposeAddEquiv (Fin n) (Fin n) R : (a : Matrix (Fin n) (Fin n) R) → Matrix (Fin n) (Fin n) R)
        ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin n) (Fin n) Rᵐᵒᵖ) → Matrix (Fin n) (Fin n) R) 1 :
          Matrix (Fin n) (Fin n) R) :
      Matrix (Fin n) (Fin n) R)
    (1 : Matrix (Fin n) (Fin n) R)
⊢ Eq (α := Matrix (Fin n) (Fin n) R)
        ((transposeAddEquiv (Fin n) (Fin n) R : (a : Matrix (Fin n) (Fin n) R) → Matrix (Fin n) (Fin n) R)
            ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin n) (Fin n) Rᵐᵒᵖ) → Matrix (Fin n) (Fin n) R)
                (HMul.hMul (α := Matrix (Fin n) (Fin m) Rᵐᵒᵖ) (β := Matrix (Fin m) (Fin n) Rᵐᵒᵖ)
                  ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin n) (Fin m) Rᵐᵒᵖ) g :
                    Matrix (Fin n) (Fin m) Rᵐᵒᵖ)
                  ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin m) (Fin n) Rᵐᵒᵖ) f :
                    Matrix (Fin m) (Fin n) Rᵐᵒᵖ)) :
              Matrix (Fin n) (Fin n) R) :
          Matrix (Fin n) (Fin n) R)
        ((transposeAddEquiv (Fin n) (Fin n) R : (a : Matrix (Fin n) (Fin n) R) → Matrix (Fin n) (Fin n) R)
            ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin n) (Fin n) Rᵐᵒᵖ) → Matrix (Fin n) (Fin n) R) 1 :
              Matrix (Fin n) (Fin n) R) :
          Matrix (Fin n) (Fin n) R) →
      Eq (α := Matrix (Fin m) (Fin m) R)
          ((transposeAddEquiv (Fin m) (Fin m) R : (a : Matrix (Fin m) (Fin m) R) → Matrix (Fin m) (Fin m) R)
              ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin m) (Fin m) Rᵐᵒᵖ) → Matrix (Fin m) (Fin m) R)
                  (HMul.hMul (α := Matrix (Fin m) (Fin n) Rᵐᵒᵖ) (β := Matrix (Fin n) (Fin m) Rᵐᵒᵖ)
                    ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin m) (Fin n) Rᵐᵒᵖ) f :
                      Matrix (Fin m) (Fin n) Rᵐᵒᵖ)
                    ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin n) (Fin m) Rᵐᵒᵖ) g :
                      Matrix (Fin n) (Fin m) Rᵐᵒᵖ)) :
                Matrix (Fin m) (Fin m) R) :
            Matrix (Fin m) (Fin m) R)
          ((transposeAddEquiv (Fin m) (Fin m) R : (a : Matrix (Fin m) (Fin m) R) → Matrix (Fin m) (Fin m) R)
              ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin m) (Fin m) Rᵐᵒᵖ) → Matrix (Fin m) (Fin m) R) 1 :
                Matrix (Fin m) (Fin m) R) :
            Matrix (Fin m) (Fin m) R) →
        n = m ↔
    HMul.hMul (α := Matrix (Fin n) (Fin m) R) (β := Matrix (Fin m) (Fin n) R)
          ((AddEquiv.toEquiv (transposeAddEquiv (Fin m) (Fin n) R) :
                (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin n) (Fin m) R)
              f :
            Matrix (Fin n) (Fin m) R)
          ((AddEquiv.toEquiv (transposeAddEquiv (Fin n) (Fin m) R) :
                (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin m) (Fin n) R)
              g :
            Matrix (Fin m) (Fin n) R) =
        1 →
      HMul.hMul (α := Matrix (Fin m) (Fin n) R) (β := Matrix (Fin n) (Fin m) R)
            ((AddEquiv.toEquiv (transposeAddEquiv (Fin n) (Fin m) R) :
                  (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin m) (Fin n) R)
                g :
              Matrix (Fin m) (Fin n) R)
            ((AddEquiv.toEquiv (transposeAddEquiv (Fin m) (Fin n) R) :
                  (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin n) (Fin m) R)
                f :
              Matrix (Fin n) (Fin m) R) =
          1 →
        n = m
have a₂ : (transposeAddEquiv (Fin m) (Fin m) R : (a : Matrix (Fin m) (Fin m) R) → Matrix (Fin m) (Fin m) R)
    ((Equiv.symm (Equiv.mapMatrix opEquiv) : (a : Matrix (Fin m) (Fin m) Rᵐᵒᵖ) → Matrix (Fin m) (Fin m) R)
        (HMul.hMul (α := Matrix (Fin m) (Fin n) Rᵐᵒᵖ) (β := Matrix (Fin n) (Fin m) Rᵐᵒᵖ)
          ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin m) (Fin n) Rᵐᵒᵖ) f :
            Matrix (Fin m) (Fin n) Rᵐᵒᵖ)
          ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin n) (Fin m) Rᵐᵒᵖ) g :
            Matrix (Fin n) (Fin m) Rᵐᵒᵖ)) :
      Matrix (Fin m) (Fin m) R) =
  HMul.hMul (α := Matrix (Fin m) (Fin n) R) (β := Matrix (Fin n) (Fin m) R)
    ((AddEquiv.toEquiv (transposeAddEquiv (Fin n) (Fin m) R) :
          (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin m) (Fin n) R)
        g :
      Matrix (Fin m) (Fin n) R)
    ((AddEquiv.toEquiv (transposeAddEquiv (Fin m) (Fin n) R) :
          (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin n) (Fin m) R)
        f :
      Matrix (Fin n) (Fin m) R)
Tactic: congrm (?_ = ?_ → ?_ = ?_ → _)