awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
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 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
have 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
Tactic: refine fun f ↦ .trans (forall_congr' fun g ↦ ?_) (transposeAddEquiv ..).forall_congr_right
-- 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
⊢ 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
have 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
Tactic: rw [← (transposeAddEquiv ..).injective.eq_iff]
-- 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
⊢ 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
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 (?_ = ?_ → _)
-- 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
⊢ (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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ InvariantBasisNumber.{u_1} Rᵐᵒᵖ ↔ InvariantBasisNumber R
have 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
Tactic: simp_rw [invariantBasisNumber_iff_matrix, ← opEquiv.mapMatrix.forall_congr_right,
    ← opEquiv.mapMatrix.symm.injective.eq_iff]
-- 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
⊢ (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)
have 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
Tactic: ext
-- 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
⊢ (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)
have 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
Tactic: iterate 2 ext; simp [map, mul_apply]; simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
⊢ ∃ (j : n), 0 < A i j
have by_contra : ∀ (h_row : ¬∃ (j : n), 0 < A i j), False
Tactic: by_contra h_row
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
⊢ False
have no_out : ∀ (j : n), IsEmpty (i ⟶ j)
Tactic: have no_out : ∀ j : n, IsEmpty (i ⟶ j) :=
    fun j => ⟨fun e => h_row ⟨j, e.down⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
⊢ False
have obtain : ∀ (j : n) (hij : ∃ (y : n), j ≠ y), False
Tactic: obtain ⟨j, hij⟩ := exists_pair_ne n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
⊢ False
have obtain : ∀ (p : Path i j) (hp_pos : 0 < p.length), False
Tactic: obtain ⟨p, hp_pos⟩ := h_irr.connected i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
⊢ False
have h_le : 1 ≤ p.length
Tactic: have h_le : 1 ≤ p.length := Nat.succ_le_of_lt hp_pos
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
⊢ False
have have : ∀ (v : n) (p₁ : Path i v) (p₂ : Path v j) (_hp_eq : p = p₁.comp p₂) (hp₁_len : p₁.length = 1), False
Tactic: have ⟨v, p₁, p₂, _hp_eq, hp₁_len⟩ := p.exists_eq_comp_of_le_length (n := 1) h_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₁ : Path i v
p₂ : Path v j
_hp_eq : p = p₁.comp p₂
hp₁_len : p₁.length = 1
⊢ False
have hlen_ne : p₁.length ≠ 0
Tactic: have hlen_ne : p₁.length ≠ 0 := by simp [hp₁_len]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₁ : Path i v
p₂ : Path v j
_hp_eq : p = p₁.comp p₂
hp₁_len : p₁.length = 1
hlen_ne : p₁.length ≠ 0
⊢ False
have obtain : ∀ (c : n) (p' : Path i c) (e : c ⟶ v) (_hp_eq : p = (p'.cons e).comp p₂) (hp₁_len : (p'.cons e).length = 1)
  (hlen_ne : (p'.cons e).length ≠ 0), False
Tactic: obtain ⟨c, p', e, rfl⟩ := (Quiver.Path.length_ne_zero_iff_eq_cons (p := p₁)).1 (by lia)
Cleared hypotheses: p₁, _hp_eq, hp₁_len, hlen_ne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₂ : Path v j
c : n
p' : Path i c
e : c ⟶ v
_hp_eq : p = (p'.cons e).comp p₂
hp₁_len : (p'.cons e).length = 1
hlen_ne : (p'.cons e).length ≠ 0
⊢ False
have obtain : ∀ (p' : Path i i) (e : i ⟶ v) (_hp_eq : p = (p'.cons e).comp p₂) (hp₁_len : (p'.cons e).length = 1)
  (hlen_ne : (p'.cons e).length ≠ 0), False
Tactic: obtain ⟨rfl⟩ : i = c := Quiver.Path.eq_of_length_zero p' (by simp_all)
Cleared hypotheses: c, p', e, _hp_eq, hp₁_len, hlen_ne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
i j : n
⊢ 0 < HPow.hPow (β := ℕ) A 0 i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }
have zero : ∀ (h_pos : 0 < HPow.hPow (β := ℕ) A 0 i j), Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }
Tactic: refine ⟨fun h_pos ↦ ?_, fun ⟨p, hp⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
i j : n
zero : ∀ (h_pos : 0 < HPow.hPow (β := ℕ) A 0 i j), Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }
⊢ 0 < HPow.hPow (β := ℕ) A 0 i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }
have zero₁ : Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 } →
  ∀ (p : Path i j) (hp : p.length = 0), 0 < HPow.hPow (β := ℕ) A 0 i j
Tactic: refine ⟨fun h_pos ↦ ?_, fun ⟨p, hp⟩ ↦ ?_⟩