awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : AddMonoid α
inst_1 : StarAddMonoid α
x x_1 : WithConv (Matrix m n α)
⊢ star (x + x_1) = star x + star x_1

Tactic:
simp [Matrix.map_add]

Premises used: Matrix.map_add
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : Mul α
inst_1 : StarMul α
x x_1 : WithConv (Matrix m n α)
h : ∀ (i : m) (j : n), (star (x * x_1)).ofConv i j = (star x_1 * star x).ofConv i j
⊢ star (x * x_1) = star x_1 * star x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : Mul α
inst_1 : StarMul α
x x_1 : WithConv (Matrix m n α)
i : m
j : n
⊢ (star (x * x_1)).ofConv i j = (star x_1 * star x).ofConv i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
⊢ ∀ (r s : WithConv (Matrix m n α)), star (r + s) = star r + star s

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid β
inst_1 : MulAction β α
inst_2 : Mul α
inst_3 : SMulCommClass β α α
⊢ ∀ (m_1 : β) (n_1 a : WithConv (Matrix m n α)), m_1 • n_1 • a = n_1 • m_1 • a

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid β
inst_1 : MulAction β α
inst_2 : Mul α
inst_3 : IsScalarTower β α α
⊢ ∀ (x : β) (y z : WithConv (Matrix m n α)), (x • y) • z = x • y • z

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Semiring α
inst_1 : IsLeftCancelMulZero α
inst_2 : StarRing α
f : WithConv (Matrix m n α)
hf : IsIdempotentElem f
⊢ ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1

Tactic:
simp_rw [IsIdempotentElem, WithConv.ext_iff, ← Matrix.ext_iff, convMul_def, hadamard_apply,
    ← isIdempotentElem_iff, IsIdempotentElem.iff_eq_zero_or_one] at hf

Premises used: Matrix.hadamard_apply, IsIdempotentElem.iff_eq_zero_or_one, IsIdempotentElem, Matrix.ext_iff, convMul_def, WithConv.ext_iff, isIdempotentElem_iff
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Semiring α
inst_1 : IsLeftCancelMulZero α
inst_2 : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
rw : (star f).ofConv = f.ofConv
⊢ IsSelfAdjoint f

Tactic:
rw [IsSelfAdjoint, WithConv.ext_iff]

Premises used: IsSelfAdjoint, WithConv.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Semiring α
inst_1 : IsLeftCancelMulZero α
inst_2 : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
a : ∀ (i : m) (j : n), (star f).ofConv i j = f.ofConv i j
⊢ (star f).ofConv = f.ofConv

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Semiring α
inst_1 : IsLeftCancelMulZero α
inst_2 : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
i : m
j : n
a : ∀ (h : f.ofConv i j = 0), (star f).ofConv i j = f.ofConv i j
a₁ : ∀ (h : f.ofConv i j = 1), (star f).ofConv i j = f.ofConv i j
⊢ (star f).ofConv i j = f.ofConv i j

Tactic:
obtain (h | h) := hf i j
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Semiring α
inst_1 : IsLeftCancelMulZero α
inst_2 : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
i : m
j : n
h : f.ofConv i j = 0
⊢ (star f).ofConv i j = f.ofConv i j

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Semiring α
inst_1 : IsLeftCancelMulZero α
inst_2 : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), f.ofConv i j = 0 ∨ f.ofConv i j = 1
i : m
j : n
h : f.ofConv i j = 1
⊢ (star f).ofConv i j = f.ofConv i j

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
x x_1 : WithConv (Matrix m n α)
h :
  ∀ (i : n) (x_2 : m),
    Eq.{u_3 + 1} (α := α)
      (((AddHom.toFun
                  (LinearMap.toAddHom
                    (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
                  (x * x_1)).ofConv ∘ₗ
              LinearMap.single α (fun (i : n) ↦ α) i :
            (a : α) → m → α)
          1 x_2 :
        α)
      (((AddHom.toFun
                    (LinearMap.toAddHom
                      (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
                    x *
                  AddHom.toFun
                    (LinearMap.toAddHom
                      (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
                    x_1).ofConv ∘ₗ
              LinearMap.single α (fun (i : n) ↦ α) i :
            (a : α) → m → α)
          1 x_2 :
        α)
⊢ AddHom.toFun
      (LinearMap.toAddHom (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
      (x * x_1) =
    AddHom.toFun
        (LinearMap.toAddHom (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
        x *
      AddHom.toFun
        (LinearMap.toAddHom (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
        x_1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
x x_1 : WithConv (Matrix m n α)
i : n
x_2 : m
⊢ Eq.{u_3 + 1} (α := α)
    (((AddHom.toFun
                (LinearMap.toAddHom
                  (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
                (x * x_1)).ofConv ∘ₗ
            LinearMap.single α (fun (i : n) ↦ α) i :
          (a : α) → m → α)
        1 x_2 :
      α)
    (((AddHom.toFun
                  (LinearMap.toAddHom
                    (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
                  x *
                AddHom.toFun
                  (LinearMap.toAddHom
                    (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
                  x_1).ofConv ∘ₗ
            LinearMap.single α (fun (i : n) ↦ α) i :
          (a : α) → m → α)
        1 x_2 :
      α)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
x : WithConv (Matrix m n α)
⊢ AddHom.toFun
      (LinearMap.toAddHom (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
      (star x) =
    star
      (AddHom.toFun
        (LinearMap.toAddHom (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
        x)

Tactic:
Matrix.intrinsicStar_toLin' _ |>.symm

Premises used: Matrix.intrinsicStar_toLin', Matrix.map, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
x : WithConv (Matrix m n α)
⊢ AddHom.toFun
      (LinearMap.toAddHom (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
      (star x) =
    star
      (AddHom.toFun
        (LinearMap.toAddHom (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
        x)

Tactic:
exact Matrix.intrinsicStar_toLin' _ |>.symm

Premises used: Matrix.intrinsicStar_toLin', Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
x : WithConv (Matrix m n α)
⊢ AddHom.toFun
      (LinearMap.toAddHom (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
      (star x) =
    star
      (AddHom.toFun
        (LinearMap.toAddHom (↑(congrLinearEquiv toLin') : WithConv (Matrix m n α) →ₗ[α] WithConv ((n → α) →ₗ[α] m → α)))
        x)

Tactic:
classical exact Matrix.intrinsicStar_toLin' _ |>.symm

Premises used: Matrix.intrinsicStar_toLin', Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
x : WithConv (Matrix m n α)
⊢ Eq (α := WithConv ((n → α) →ₗ[α] m → α))
    ((matrixToLin'StarAlgEquiv m n α : (a : WithConv (Matrix m n α)) → WithConv ((n → α) →ₗ[α] m → α)) x :
      WithConv ((n → α) →ₗ[α] m → α))
    (toConv ((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) x.ofConv) : WithConv ((n → α) →ₗ[α] m → α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
x : WithConv ((n → α) →ₗ[α] m → α)
⊢ Eq (α := WithConv (Matrix m n α))
    ((StarAlgEquiv.symm (matrixToLin'StarAlgEquiv m n α) :
          (a : WithConv ((n → α) →ₗ[α] m → α)) → WithConv (Matrix m n α))
        x :
      WithConv (Matrix m n α))
    (toConv ((LinearMap.toMatrix' : (a : (n → α) →ₗ[α] m → α) → Matrix m n α) x.ofConv) : WithConv (Matrix m n α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
x y : Matrix m n α
h :
  ∀ (i : n) (x_1 : m),
    Eq.{u_3 + 1} (α := α)
      ((((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) (x ⊙ y) ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i :
              α →ₗ[α] m → α) :
            (a : α) → m → α)
          1 x_1 :
        α)
      (((HMul.hMul (α := WithConv ((n → α) →ₗ[α] m → α)) (β := WithConv ((n → α) →ₗ[α] m → α))
                  (toConv ((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) x) : WithConv ((n → α) →ₗ[α] m → α))
                  (toConv ((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) y) :
                    WithConv ((n → α) →ₗ[α] m → α))).ofConv ∘ₗ
              LinearMap.single α (fun (i : n) ↦ α) i :
            (a : α) → m → α)
          1 x_1 :
        α)
⊢ (toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) (x ⊙ y) =
    (HMul.hMul (α := WithConv ((n → α) →ₗ[α] m → α)) (β := WithConv ((n → α) →ₗ[α] m → α))
        (toConv ((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) x) : WithConv ((n → α) →ₗ[α] m → α))
        (toConv ((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) y) : WithConv ((n → α) →ₗ[α] m → α))).ofConv

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
x y : Matrix m n α
i : n
x_1 : m
⊢ Eq.{u_3 + 1} (α := α)
    ((((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) (x ⊙ y) ∘ₗ LinearMap.single α (fun (i : n) ↦ α) i :
            α →ₗ[α] m → α) :
          (a : α) → m → α)
        1 x_1 :
      α)
    (((HMul.hMul (α := WithConv ((n → α) →ₗ[α] m → α)) (β := WithConv ((n → α) →ₗ[α] m → α))
                (toConv ((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) x) : WithConv ((n → α) →ₗ[α] m → α))
                (toConv ((toLin' : (a : Matrix m n α) → (n → α) →ₗ[α] m → α) y) :
                  WithConv ((n → α) →ₗ[α] m → α))).ofConv ∘ₗ
            LinearMap.single α (fun (i : n) ↦ α) i :
          (a : α) → m → α)
        1 x_1 :
      α)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
n : Type u_2
α : Type u_3
inst : CommSemiring α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix n n α
rw :
  A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))
rw₁ :
  A.IsSymm ↔
    Eq (α := (n → α) →ₗ[α] n → α)
      ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (A.map star) : (n → α) →ₗ[α] n → α)
      ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A) : (n → α) →ₗ[α] n → α)
rw₂ : A.IsSymm ↔ A.map star = star A
rw₃ : A.IsSymm ↔ Aᵀᴴ = star A
rw₄ : A.IsSymm ↔ Aᵀᴴ = Aᴴ
rw₅ : A.IsSymm ↔ Aᵀ = A
rw₆ rw₇ : Aᵀ = A ↔ Aᵀ = A
⊢ A.IsSymm ↔
    Eq (α := WithConv ((n → α) →ₗ[α] n → α))
      (star (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) A)) : WithConv ((n → α) →ₗ[α] n → α))
      (toConv ((toLin' : (a : Matrix n n α) → (n → α) →ₗ[α] n → α) (star A)) : WithConv ((n → α) →ₗ[α] n → α))

Tactic:
rw [intrinsicStar_toLin', toConv_injective.eq_iff, toLin'.injective.eq_iff,
    ← transpose_conjTranspose, star_eq_conjTranspose, conjTranspose_inj, IsSymm]

Premises used: Matrix.star_eq_conjTranspose, Matrix.intrinsicStar_toLin', Function.Injective.eq_iff, Matrix.toLin', Matrix.transpose_conjTranspose, Matrix.conjTranspose_inj, Matrix.IsSymm, WithConv.toConv_injective, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
⊢ HPow.hPow (β := ℕ) A⁻¹ 0 = (HPow.hPow (β := ℕ) A 0)⁻¹

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
ih : A⁻¹ ^ n = (A ^ n)⁻¹
succ : A⁻¹ ^ (n + 1) = (A ^ n * A)⁻¹
succ₁ : A⁻¹ ^ (n + 1) = A⁻¹ * (A ^ n)⁻¹
succ₂ : A⁻¹ ^ (n + 1) = A⁻¹ * A⁻¹ ^ n
succ₃ succ₄ : A⁻¹ ^ (n + 1) = A⁻¹ ^ (n + 1)
⊢ A⁻¹ ^ (n + 1) = (A ^ (n + 1))⁻¹

Tactic:
rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']

Premises used: pow_succ, Matrix.mul_inv_rev, pow_succ'
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
zero : HPow.hPow (β := ℕ) A⁻¹ 0 = (HPow.hPow (β := ℕ) A 0)⁻¹
succ : ∀ (n : ℕ) (ih : A⁻¹ ^ n = (A ^ n)⁻¹), A⁻¹ ^ (n + 1) = (A ^ (n + 1))⁻¹
⊢ A⁻¹ ^ n = (A ^ n)⁻¹

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']

Premises used: pow_succ, Matrix.mul_inv_rev, Matrix.zero, pow_succ'
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
m n : ℕ
ha : IsUnit A.det
h : n ≤ m
h₁ : IsUnit (A ^ n).det
⊢ A ^ (m - n) = A ^ m * (A ^ n)⁻¹

Tactic:
rw [← tsub_add_cancel_of_le h, pow_add, Matrix.mul_assoc, mul_nonsing_inv,
    tsub_add_cancel_of_le h, Matrix.mul_one]

Premises used: Matrix.mul_assoc, pow_add, tsub_add_cancel_of_le, Matrix.mul_one, Matrix.mul_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
m n : ℕ
ha : IsUnit A.det
h : n ≤ m
⊢ IsUnit (A ^ n).det

Tactic:
simpa using ha.pow n

Premises used: IsUnit.pow
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
m : ℕ
⊢ A⁻¹ ^ m * HPow.hPow (β := ℕ) A 0 = HPow.hPow (β := ℕ) A 0 * A⁻¹ ^ m

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
succ : HPow.hPow (β := ℕ) A⁻¹ 0 * A ^ (n + 1) = A ^ (n + 1) * HPow.hPow (β := ℕ) A⁻¹ 0
succ₁ : ∀ (m : ℕ), A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
⊢ A⁻¹ ^ m * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ m

Tactic:
rcases m with m | m
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
⊢ HPow.hPow (β := ℕ) A⁻¹ 0 * A ^ (n + 1) = A ^ (n + 1) * HPow.hPow (β := ℕ) A⁻¹ 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
succ : ∀ (h : A⁻¹ * A = 1) (h' : A * A⁻¹ = 1), A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
succ₁ : ∀ (h : A⁻¹ = 0), A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)

Tactic:
rcases nonsing_inv_cancel_or_zero A with ⟨h, h'⟩ | h

Premises used: Matrix.nonsing_inv_cancel_or_zero
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n

Tactic:
simp only [pow_succ A⁻¹, pow_succ' A, Matrix.mul_assoc]

Premises used: pow_succ, Matrix.mul_assoc, Inv.inv, pow_succ'
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A⁻¹ ^ m * (A⁻¹ * A) * A ^ n = A ^ n * A⁻¹ ^ m

Tactic:
simp only [h, Matrix.mul_one, IH m]

Premises used: Matrix.mul_one
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A ^ n * A⁻¹ ^ m = A ^ n * (A * A⁻¹) * A⁻¹ ^ m

Tactic:
simp only [h', Matrix.mul_one]

Premises used: Matrix.mul_one
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A ^ n * (A * A⁻¹) * A⁻¹ ^ m = A ^ (n + 1) * A⁻¹ ^ (m + 1)

Tactic:
simp only [pow_succ A, pow_succ' A⁻¹, Matrix.mul_assoc]

Premises used: pow_succ, Matrix.mul_assoc, Inv.inv, pow_succ'
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
A₁ : A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n
A₂ : A⁻¹ ^ m * (A⁻¹ * A) * A ^ n = A ^ n * A⁻¹ ^ m
A₃ : A ^ n * A⁻¹ ^ m = A ^ n * (A * A⁻¹) * A⁻¹ ^ m
A₄ : A ^ n * (A * A⁻¹) * A⁻¹ ^ m = A ^ (n + 1) * A⁻¹ ^ (m + 1)
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)

Tactic:
calc
        A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n := by
          simp only [pow_succ A⁻¹, pow_succ' A, Matrix.mul_assoc]
        _ = A ^ n * A⁻¹ ^ m := by simp only [h, Matrix.mul_one, IH m]
        _ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one]
        _ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by
          simp only [pow_succ A, pow_succ' A⁻¹, Matrix.mul_assoc]

Premises used: HMul.hMul, Inv.inv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ = 0
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
m n : ℕ
zero : ∀ (m : ℕ), A⁻¹ ^ m * HPow.hPow (β := ℕ) A 0 = HPow.hPow (β := ℕ) A 0 * A⁻¹ ^ m
succ :
  ∀ (n : ℕ) (IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m) (m : ℕ), A⁻¹ ^ m * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ m
⊢ A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m

Tactic:
induction n generalizing m with
  | zero => simp
  | succ n IH =>
    rcases m with m | m
    · simp
    rcases nonsing_inv_cancel_or_zero A with ⟨h, h'⟩ | h
    · calc
        A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n := by
          simp only [pow_succ A⁻¹, pow_succ' A, Matrix.mul_assoc]
        _ = A ^ n * A⁻¹ ^ m := by simp only [h, Matrix.mul_one, IH m]
        _ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one]
        _ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by
          simp only [pow_succ A, pow_succ' A⁻¹, Matrix.mul_assoc]
    · simp [h]

Premises used: HMul.hMul, Inv.inv, Matrix.nonsing_inv_cancel_or_zero, HAdd.hAdd, OfNat.ofNat, Matrix.zero
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
n : ℕ
rw : HPow.hPow (α := M) 1 n = 1
rw₁ rw₂ : Eq (α := M) 1 1
⊢ HPow.hPow (α := M) (β := ℤ) 1 (↑n : ℤ) = 1

Tactic:
rw [zpow_natCast, one_pow]

Premises used: zpow_natCast, one_pow
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
n : ℕ
rw : (HPow.hPow (α := M) 1 (n + 1))⁻¹ = 1
rw₁ : Eq (α := M) 1⁻¹ 1
rw₂ rw₃ : Eq (α := M) 1 1
⊢ HPow.hPow (α := M) 1 -[n+1] = 1

Tactic:
rw [zpow_negSucc, one_pow, inv_one]

Premises used: one_pow, inv_one, zpow_negSucc
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : Ne (α := ℤ) (↑n : ℤ) 0
rw : n ≠ 0
⊢ HPow.hPow (α := M) (β := ℤ) 0 (↑n : ℤ) = 0

Tactic:
rw [zpow_natCast, zero_pow]

Premises used: zpow_natCast, zero_pow
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : Ne (α := ℤ) (↑n : ℤ) 0
⊢ n ≠ 0

Tactic:
mod_cast h

Premises used: congrArg, cast, Ne, Nat.cast, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : Ne (α := ℤ) (↑n : ℤ) 0
⊢ n ≠ 0

Tactic:
exact mod_cast h
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
n : ℕ
h : -[n+1] ≠ 0
⊢ HPow.hPow (α := M) 0 -[n+1] = 0

Tactic:
simp [zero_pow n.succ_ne_zero]

Premises used: Nat.succ_ne_zero, zero_pow
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
n : ℤ
pos : ∀ (h : n = 0), HPow.hPow (α := M) 0 n = 1
neg : ∀ (h : ¬n = 0), HPow.hPow (α := M) 0 n = 0
⊢ HPow.hPow (α := M) 0 n = if n = 0 then 1 else 0

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
n : ℤ
h : n = 0
pos : HPow.hPow (α := M) (β := ℤ) 0 0 = 1
pos₁ pos₂ : Eq (α := M) 1 1
⊢ HPow.hPow (α := M) 0 n = 1

Tactic:
rw [h, zpow_zero]

Premises used: zpow_zero
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
n : ℤ
h : ¬n = 0
neg neg₁ : Eq (α := M) 0 0
⊢ HPow.hPow (α := M) 0 n = 0

Tactic:
rw [zero_zpow _ h]

Premises used: Matrix.zero_zpow
-- Module: Mathlib.LinearAlgebra.Matrix.ZPow
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
rw : A⁻¹ ^ n = (HPow.hPow (β := ℤ) A (↑n : ℤ))⁻¹
rw₁ : A⁻¹ ^ n = (A ^ n)⁻¹
rw₂ rw₃ : (A ^ n)⁻¹ = (A ^ n)⁻¹
⊢ HPow.hPow (β := ℤ) A⁻¹ (↑n : ℤ) = (HPow.hPow (β := ℤ) A (↑n : ℤ))⁻¹

Tactic:
rw [zpow_natCast, zpow_natCast, inv_pow']

Premises used: zpow_natCast, Matrix.inv_pow'