-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      Eq (α := 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ᵐᵒᵖ) a :
                  Matrix (Fin n) (Fin m) Rᵐᵒᵖ)
                ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin m) (Fin n) Rᵐᵒᵖ) a_1 :
                  Matrix (Fin m) (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) →
        Eq (α := 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ᵐᵒᵖ) a_1 :
                    Matrix (Fin m) (Fin n) Rᵐᵒᵖ)
                  ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin n) (Fin m) Rᵐᵒᵖ) a :
                    Matrix (Fin n) (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) →
          n = m) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m
have a : ∀ (n m : ℕ),
  (∀ (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      Eq (α := 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ᵐᵒᵖ) a :
                  Matrix (Fin n) (Fin m) Rᵐᵒᵖ)
                ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin m) (Fin n) Rᵐᵒᵖ) a_1 :
                  Matrix (Fin m) (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) →
        Eq (α := 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ᵐᵒᵖ) a_1 :
                    Matrix (Fin m) (Fin n) Rᵐᵒᵖ)
                  ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin n) (Fin m) Rᵐᵒᵖ) a :
                    Matrix (Fin n) (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) →
          n = m) ↔
    ∀ (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m
Tactic: congr! 2 with n m