awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
n m : ℕ
a :
  ∀ (f : Matrix (Fin m) (Fin n) R) (g : Matrix (Fin n) (Fin m) 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ᵐᵒᵖ) 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)
          ((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) →
        m ≤ n ↔
      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 →
        m ≤ n
⊢ ∀ (a : Matrix (Fin m) (Fin n) R),
    (∀ (a_1 : Matrix (Fin n) (Fin m) 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 :
                    Matrix (Fin m) (Fin n) Rᵐᵒᵖ)
                  ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin n) (Fin m) Rᵐᵒᵖ) a_1 :
                    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) →
          m ≤ n) ↔
      ∀ (g : Matrix (Fin m) (Fin n) R),
        HMul.hMul (β := Matrix (Fin n) (Fin m) R) g
              ((AddEquiv.toEquiv (transposeAddEquiv (Fin m) (Fin n) R) :
                    (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin n) (Fin m) R)
                  a :
                Matrix (Fin n) (Fin m) R) =
            1 →
          m ≤ n

Tactic:
refine fun f ↦ .trans (forall_congr' fun g ↦ ?_) (transposeAddEquiv ..).forall_congr_right
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
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 :
  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) →
      m ≤ n ↔
    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 →
      m ≤ n
⊢ 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ᵐᵒᵖ) 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)
        ((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) →
      m ≤ n ↔
    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 →
      m ≤ n

Tactic:
rw [← (transposeAddEquiv ..).injective.eq_iff]

Premises used: Function.Injective.eq_iff, AddEquiv.injective, Matrix.transposeAddEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
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 :
  ∀ (i j : Fin m),
    (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)
        i j =
      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)
        i j
⊢ (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:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
i j : Fin m
⊢ (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)
      i j =
    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)
      i j

Tactic:
simp [map, mul_apply]

Premises used: Matrix.mul_apply, Matrix.map
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) 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) 1 :
          Matrix (Fin m) (Fin m) R) :
      Matrix (Fin m) (Fin m) R)
    (1 : Matrix (Fin m) (Fin m) R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
simp_rw :
  (∀ (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
⊢ InvariantBasisNumber.{u_1} Rᵐᵒᵖ ↔ InvariantBasisNumber R

Tactic:
simp_rw [invariantBasisNumber_iff_matrix, ← opEquiv.mapMatrix.forall_congr_right,
    ← opEquiv.mapMatrix.symm.injective.eq_iff]

Premises used: MulOpposite.opEquiv, Equiv.mapMatrix, Function.Injective.eq_iff, invariantBasisNumber_iff_matrix, Equiv.injective, Equiv.symm, Equiv.forall_congr_right
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
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) ↔
    ∀ (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m

Tactic:
forall_comm.trans <| .trans (forall_congr' ?_) (transposeAddEquiv ..).forall_congr_right

Premises used: forall_comm, forall_congr', Iff.trans, AddEquiv.toEquiv, Equiv.forall_congr_right, Matrix.transposeAddEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
n m : ℕ
⊢ ∀ (a : Matrix (Fin m) (Fin n) R),
    (∀ (a_1 : Matrix (Fin n) (Fin m) 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_1 :
                    Matrix (Fin n) (Fin m) Rᵐᵒᵖ)
                  ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin m) (Fin n) Rᵐᵒᵖ) a :
                    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 :
                      Matrix (Fin m) (Fin n) Rᵐᵒᵖ)
                    ((Equiv.mapMatrix opEquiv : (a : Matrix (Fin n) (Fin m) R) → Matrix (Fin n) (Fin m) Rᵐᵒᵖ) a_1 :
                      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) ↔
      ∀ (g : Matrix (Fin m) (Fin n) R),
        HMul.hMul (α := Matrix (Fin n) (Fin m) R)
              ((AddEquiv.toEquiv (transposeAddEquiv (Fin m) (Fin n) R) :
                    (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin n) (Fin m) R)
                  a :
                Matrix (Fin n) (Fin m) R)
              g =
            1 →
          HMul.hMul (β := Matrix (Fin n) (Fin m) R) g
                ((AddEquiv.toEquiv (transposeAddEquiv (Fin m) (Fin n) R) :
                      (a : Matrix (Fin m) (Fin n) R) → Matrix (Fin n) (Fin m) R)
                    a :
                  Matrix (Fin n) (Fin m) R) =
              1 →
            n = m

Tactic:
fun f ↦ .trans (forall_congr' fun g ↦ ?_) (transposeAddEquiv ..).forall_congr_right

Premises used: forall_congr', Iff.trans, AddEquiv.toEquiv, Equiv.forall_congr_right, Fin, Matrix.transposeAddEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
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 :
  ∀ (i j : Fin n),
    (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)
        i j =
      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)
        i j
⊢ (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)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
i j : Fin n
⊢ (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)
      i j =
    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)
      i j

Tactic:
simp [map, mul_apply]

Premises used: Matrix.mul_apply, Matrix.map
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) 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) 1 :
          Matrix (Fin n) (Fin n) R) :
      Matrix (Fin n) (Fin n) R)
    (1 : Matrix (Fin n) (Fin n) R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
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 a₁ :
  ∀ (i j : Fin n),
    (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)
        i j =
      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)
        i j
⊢ (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)

Tactic:
iterate 2 ext; simp [map, mul_apply]; simp

Premises used: Matrix.mul_apply, Matrix.map
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
inst_1 : RankCondition R
⊢ RankCondition.{u_1} Rᵐᵒᵖ

Tactic:
MulOpposite.rankCondition_iff.mpr ‹_›

Premises used: Iff.mpr, MulOpposite.rankCondition_iff