awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 + 1))⁻¹ = (A ^ -[n+1])⁻¹
rw₁ : (A⁻¹ ^ (n + 1))⁻¹ = (A ^ (n + 1))⁻¹⁻¹
rw₂ rw₃ : (A ^ (n + 1))⁻¹⁻¹ = (A ^ (n + 1))⁻¹⁻¹
⊢ A⁻¹ ^ -[n+1] = (A ^ -[n+1])⁻¹

Tactic:
rw [zpow_negSucc, zpow_negSucc, inv_pow']

Premises used: zpow_negSucc, Matrix.inv_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
⊢ DivInvMonoid.zpow -[0+1] A = (DivInvMonoid.zpow (↑(Nat.succ 0) : ℤ) A)⁻¹

Tactic:
DivInvMonoid.zpow_neg' 0 A

Premises used: DivInvMonoid.zpow_neg', 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
h : A = DivInvMonoid.zpow (↑(Nat.succ 0) : ℤ) A
⊢ HPow.hPow (β := ℤ) A (-1) = A⁻¹

Tactic:
convert! DivInvMonoid.zpow_neg' 0 A

Premises used: DivInvMonoid.zpow_neg', 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
⊢ A = DivInvMonoid.zpow (↑(Nat.succ 0) : ℤ) A

Tactic:
simp only [zpow_one, Int.ofNat_zero, Int.natCast_succ, zpow_eq_pow, zero_add]

Premises used: zpow_one, zero_add, Int.ofNat_zero, Int.natCast_succ, zpow_eq_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
n : ℕ
zero : HPow.hPow (β := ℤ) A (-(↑0 : ℤ)) = (HPow.hPow (β := ℕ) A 0)⁻¹
succ : ∀ (n : ℕ), HPow.hPow (β := ℤ) A (-(↑(n + 1) : ℤ)) = (A ^ (n + 1))⁻¹
⊢ HPow.hPow (β := ℤ) A (-(↑n : ℤ)) = (A ^ n)⁻¹

Tactic:
cases n
-- 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 : ℕ
⊢ HPow.hPow (β := ℤ) A (-(↑(n + 1) : ℤ)) = (A ^ (n + 1))⁻¹

Tactic:
DivInvMonoid.zpow_neg' _ _

Premises used: npowRec, DivInvMonoid.zpow_neg', zpowRec, Int.neg, Int.negOfNat
-- 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 : ℕ
⊢ HPow.hPow (β := ℤ) A (-(↑(n + 1) : ℤ)) = (A ^ (n + 1))⁻¹

Tactic:
exact DivInvMonoid.zpow_neg' _ _

Premises used: DivInvMonoid.zpow_neg'
-- 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
h : IsUnit A.det
n : ℤ
ofNat : ∀ (n : ℕ), IsUnit (A ^ Int.ofNat n).det
negSucc : ∀ (n : ℕ), IsUnit (A ^ -[n+1]).det
⊢ IsUnit (A ^ n).det

Tactic:
rcases n with n | n
-- 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
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A ^ ofNat n).det

Tactic:
simpa using h.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
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A ^ -[n+1]).det

Tactic:
simpa using h.pow n.succ

Premises used: IsUnit.pow, Nat.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
⊢ IsUnit (HPow.hPow (β := ℤ) A 0).det ↔ IsUnit A.det ∨ Eq (α := ℤ) 0 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
z : ℕ
h : IsUnit (HPow.hPow (β := ℤ) A (↑z : ℤ)).det ↔ IsUnit A.det ∨ Eq (α := ℤ) (↑z : ℤ) 0
succ : IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 0
⊢ IsUnit (A ^ HAdd.hAdd (α := ℤ) (↑z : ℤ) 1).det ↔ IsUnit A.det ∨ HAdd.hAdd (α := ℤ) (↑z : ℤ) 1 = 0

Tactic:
rw [← Int.natCast_succ, zpow_natCast, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero,
      Int.ofNat_inj]

Premises used: zpow_natCast, Int.ofNat_inj, Int.ofNat_zero, isUnit_pow_succ_iff, Int.natCast_succ, Matrix.det_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
z : ℕ
h : IsUnit (HPow.hPow (β := ℤ) A (↑z : ℤ)).det ↔ IsUnit A.det ∨ Eq (α := ℤ) (↑z : ℤ) 0
⊢ IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 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
z : ℕ
h : IsUnit (HPow.hPow (β := ℤ) A (-(↑z : ℤ))).det ↔ IsUnit A.det ∨ Eq (α := ℤ) (-(↑z : ℤ)) 0
pred : IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 0
⊢ IsUnit (A ^ HSub.hSub (α := ℤ) (-(↑z : ℤ)) 1).det ↔ IsUnit A.det ∨ HSub.hSub (α := ℤ) (-(↑z : ℤ)) 1 = 0

Tactic:
rw [← neg_add', ← Int.natCast_succ, zpow_neg_natCast, isUnit_nonsing_inv_det_iff, det_pow,
      isUnit_pow_succ_iff, neg_eq_zero, ← Int.ofNat_zero, Int.ofNat_inj]

Premises used: Matrix.isUnit_nonsing_inv_det_iff, Int.ofNat_inj, neg_eq_zero, Int.ofNat_zero, neg_add', isUnit_pow_succ_iff, Int.natCast_succ, Matrix.zpow_neg_natCast, Matrix.det_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
z : ℕ
h : IsUnit (HPow.hPow (β := ℤ) A (-(↑z : ℤ))).det ↔ IsUnit A.det ∨ Eq (α := ℤ) (-(↑z : ℤ)) 0
⊢ IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 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
z : ℤ
zero : IsUnit (HPow.hPow (β := ℤ) A 0).det ↔ IsUnit A.det ∨ Eq (α := ℤ) 0 0
succ :
  ∀ (z : ℕ),
    (IsUnit (HPow.hPow (β := ℤ) A (↑z : ℤ)).det ↔ IsUnit A.det ∨ Eq (α := ℤ) (↑z : ℤ) 0) →
      (IsUnit (A ^ HAdd.hAdd (α := ℤ) (↑z : ℤ) 1).det ↔ IsUnit A.det ∨ HAdd.hAdd (α := ℤ) (↑z : ℤ) 1 = 0)
pred :
  ∀ (z : ℕ),
    (IsUnit (HPow.hPow (β := ℤ) A (-(↑z : ℤ))).det ↔ IsUnit A.det ∨ Eq (α := ℤ) (-(↑z : ℤ)) 0) →
      (IsUnit (A ^ HSub.hSub (α := ℤ) (-(↑z : ℤ)) 1).det ↔ IsUnit A.det ∨ HSub.hSub (α := ℤ) (-(↑z : ℤ)) 1 = 0)
⊢ IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0

Tactic:
induction z with
  | zero => simp
  | succ z =>
    rw [← Int.natCast_succ, zpow_natCast, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero,
      Int.ofNat_inj]
    simp
  | pred z =>
    rw [← neg_add', ← Int.natCast_succ, zpow_neg_natCast, isUnit_nonsing_inv_det_iff, det_pow,
      isUnit_pow_succ_iff, neg_eq_zero, ← Int.ofNat_zero, Int.ofNat_inj]
    simp

Premises used: zpow_natCast, Int.pred, Matrix.isUnit_nonsing_inv_det_iff, Int.ofNat_inj, neg_eq_zero, Int.ofNat_zero, neg_add', isUnit_pow_succ_iff, Int.natCast_succ, Int.succ, Matrix.zpow_neg_natCast, Matrix.zero, Matrix.det_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
h : IsUnit A.det
n : ℕ
h₁ : IsUnit (A ^ (n + 1)).det
⊢ A ^ (- -[n+1]) = (A ^ -[n+1])⁻¹

Tactic:
rw [zpow_negSucc, neg_negSucc, zpow_natCast, nonsing_inv_nonsing_inv]

Premises used: zpow_natCast, zpow_negSucc, Int.neg_negSucc, Matrix.nonsing_inv_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
h : IsUnit A.det
n : ℕ
h₁ : IsUnit (A.det ^ (n + 1))
⊢ IsUnit (A ^ (n + 1)).det

Tactic:
rw [det_pow]

Premises used: Matrix.det_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
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A.det ^ (n + 1))

Tactic:
h.pow _

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
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A.det ^ (n + 1))

Tactic:
exact h.pow _

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
h : IsUnit A.det
n : ℤ
rw : A⁻¹ ^ n = (A ^ n)⁻¹
rw₁ rw₂ : (A ^ n)⁻¹ = (A ^ n)⁻¹
⊢ A⁻¹ ^ n = A ^ (-n)

Tactic:
rw [zpow_neg h, inv_zpow]

Premises used: Matrix.zpow_neg, Matrix.inv_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
h : IsUnit A.det
n : ℕ
⊢ A ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HPow.hPow (β := ℤ) A (↑n : ℤ) * A

Tactic:
simp only [← Nat.cast_succ, pow_succ, zpow_natCast]

Premises used: zpow_natCast, Nat.cast_succ, 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
h : IsUnit A.det
n : ℕ
rw : A ^ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (-1) + 1) = (A ^ n)⁻¹
rw₁ : HPow.hPow (β := ℤ) A (-(↑n : ℤ)) = (A ^ n)⁻¹
rw₂ : (HPow.hPow (β := ℤ) A (↑n : ℤ))⁻¹ = (A ^ n)⁻¹
rw₃ rw₄ : (A ^ n)⁻¹ = (A ^ n)⁻¹
⊢ A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) = (A ^ n)⁻¹

Tactic:
rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_natCast]

Premises used: zpow_natCast, neg_add, Matrix.zpow_neg, neg_add_cancel_right
-- 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
h : IsUnit A.det
n : ℕ
rw : (A ^ n)⁻¹ = (A ^ n)⁻¹ * A⁻¹ * A
rw₁ : (A ^ n)⁻¹ = (A ^ n)⁻¹ * (A⁻¹ * A)
rw₂ : (A ^ n)⁻¹ = (A ^ n)⁻¹ * 1
rw₃ rw₄ : (A ^ n)⁻¹ = (A ^ n)⁻¹
⊢ (A ^ n)⁻¹ = (A * A ^ n)⁻¹ * A

Tactic:
rw [mul_inv_rev, Matrix.mul_assoc, nonsing_inv_mul _ h, Matrix.mul_one]

Premises used: Matrix.mul_assoc, Matrix.nonsing_inv_mul, Matrix.mul_inv_rev, 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
h : IsUnit A.det
n : ℕ
rw : (A * A ^ n)⁻¹ * A = (A ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)⁻¹ * A
rw₁ : (A * A ^ n)⁻¹ * A = (HPow.hPow (β := ℤ) A (↑n.succ : ℤ))⁻¹ * A
rw₂ : (A * A ^ n)⁻¹ * A = (A ^ n.succ)⁻¹ * A
rw₃ rw₄ : (A * A ^ n)⁻¹ * A = (A * A ^ n)⁻¹ * A
⊢ (A * A ^ n)⁻¹ * A = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * A

Tactic:
rw [zpow_neg h, ← Int.natCast_succ, zpow_natCast, pow_succ']

Premises used: zpow_natCast, Int.natCast_succ, Matrix.zpow_neg, 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
h : IsUnit A.det
n : ℤ
rw : A ^ (n - 1) = A ^ (n - 1) * (A * A⁻¹)
rw₁ : A ^ (n - 1) = A ^ (n - 1) * 1
rw₂ rw₃ : A ^ (n - 1) = A ^ (n - 1)
⊢ A ^ (n - 1) = A ^ (n - 1) * A * A⁻¹

Tactic:
rw [mul_assoc, mul_nonsing_inv _ h, mul_one]

Premises used: mul_assoc, 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
h : IsUnit A.det
n : ℤ
rw : A ^ (n - 1 + 1) * A⁻¹ = A ^ n * A⁻¹
rw₁ rw₂ : A ^ n * A⁻¹ = A ^ n * A⁻¹
⊢ A ^ (n - 1) * A * A⁻¹ = A ^ n * A⁻¹

Tactic:
rw [← zpow_add_one h, sub_add_cancel]

Premises used: Matrix.zpow_add_one, sub_add_cancel
-- 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
ha : IsUnit A.det
m : ℤ
⊢ A ^ (m + 0) = A ^ m * 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
ha : IsUnit A.det
m : ℤ
n : ℕ
ihn : A ^ (m + (↑n : ℤ)) = A ^ m * HPow.hPow (β := ℤ) A (↑n : ℤ)
⊢ A ^ (m + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = A ^ m * A ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1

Tactic:
simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]

Premises used: add_assoc, mul_assoc, Matrix.zpow_add_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
ha : IsUnit A.det
m : ℤ
n : ℕ
ihn : A ^ (m + -(↑n : ℤ)) = A ^ m * HPow.hPow (β := ℤ) A (-(↑n : ℤ))
pred : A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ m * (HPow.hPow (β := ℤ) A (-(↑n : ℤ)) * A⁻¹)
pred₁ : A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ m * HPow.hPow (β := ℤ) A (-(↑n : ℤ)) * A⁻¹
pred₂ : A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ (m + -(↑n : ℤ)) * A⁻¹
pred₃ : A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ (m + -(↑n : ℤ) - 1)
pred₄ pred₅ : A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ m * A ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1

Tactic:
rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]

Premises used: add_sub_assoc, mul_assoc, Matrix.zpow_sub_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
ha : IsUnit A.det
m n : ℤ
zero : A ^ (m + 0) = A ^ m * HPow.hPow (β := ℤ) A 0
succ :
  ∀ (n : ℕ) (ihn : A ^ (m + (↑n : ℤ)) = A ^ m * HPow.hPow (β := ℤ) A (↑n : ℤ)),
    A ^ (m + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = A ^ m * A ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
pred :
  ∀ (n : ℕ) (ihn : A ^ (m + -(↑n : ℤ)) = A ^ m * HPow.hPow (β := ℤ) A (-(↑n : ℤ))),
    A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ m * A ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
induction n with
  | zero => simp
  | succ n ihn => simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
  | pred n ihn => rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]

Premises used: add_sub_assoc, Int.pred, add_assoc, mul_assoc, Matrix.zpow_add_one, Int.succ, Matrix.zpow_sub_one, 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
A : M
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
inl : ∀ (h : A⁻¹ * A = 1), A * A⁻¹ = 1 → A ^ (m + n) = A ^ m * A ^ n
inr : ∀ (h : A⁻¹ = 0), A ^ (m + n) = A ^ m * A ^ n
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
rcases nonsing_inv_cancel_or_zero A with (⟨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
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ * A = 1
right : A * A⁻¹ = 1
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
zpow_add (isUnit_det_of_left_inverse h) m n

Premises used: Matrix.zpow_add, Matrix.isUnit_det_of_left_inverse
-- 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 : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ * A = 1
right : A * A⁻¹ = 1
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
exact zpow_add (isUnit_det_of_left_inverse h) m n

Premises used: Matrix.zpow_add, Matrix.isUnit_det_of_left_inverse
-- 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 : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ = 0
inr : ∀ (k : ℕ) (hm : LE.le (α := ℤ) (-(↑k : ℤ)) 0), A ^ (-(↑k : ℤ) + n) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * A ^ n
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
obtain ⟨k, rfl⟩ := exists_eq_neg_ofNat hm

Premises used: Int.exists_eq_neg_ofNat, rfl
-- 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 : ℤ
hn : n ≤ 0
h : A⁻¹ = 0
k : ℕ
hm : LE.le (α := ℤ) (-(↑k : ℤ)) 0
inr :
  ∀ (l : ℕ) (hn : LE.le (α := ℤ) (-(↑l : ℤ)) 0),
    A ^ HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) (-(↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
⊢ A ^ (-(↑k : ℤ) + n) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * A ^ n

Tactic:
obtain ⟨l, rfl⟩ := exists_eq_neg_ofNat hn

Premises used: Int.exists_eq_neg_ofNat, rfl
-- 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
h : A⁻¹ = 0
k : ℕ
hm : LE.le (α := ℤ) (-(↑k : ℤ)) 0
l : ℕ
hn : LE.le (α := ℤ) (-(↑l : ℤ)) 0
inr : A ^ (-HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
inr₁ : HPow.hPow (β := ℤ) A (-(↑(k + l) : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
inr₂ : (A ^ (k + l))⁻¹ = (A ^ k)⁻¹ * (A ^ l)⁻¹
inr₃ : A⁻¹ ^ (k + l) = A⁻¹ ^ k * A⁻¹ ^ l
inr₄ : HPow.hPow (α := M) 0 (k + l) = HPow.hPow (α := M) 0 k * HPow.hPow (α := M) 0 l
⊢ A ^ HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) (-(↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))

Tactic:
simp_rw [← neg_add, ← Int.natCast_add, zpow_neg_natCast, ← inv_pow', h, pow_add]

Premises used: Int.natCast_add, pow_add, neg_add, Matrix.inv_pow', Matrix.zpow_neg_natCast
-- 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 : ℤ
hm : 0 ≤ m
hn : 0 ≤ n
obtain : ∀ (k : ℕ) (hm : LE.le (α := ℤ) 0 (↑k : ℤ)), A ^ ((↑k : ℤ) + n) = HPow.hPow (β := ℤ) A (↑k : ℤ) * A ^ n
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
obtain ⟨k, rfl⟩ := eq_ofNat_of_zero_le hm

Premises used: Int.eq_ofNat_of_zero_le, rfl
-- 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 : ℤ
hn : 0 ≤ n
k : ℕ
hm : LE.le (α := ℤ) 0 (↑k : ℤ)
obtain :
  ∀ (l : ℕ) (hn : LE.le (α := ℤ) 0 (↑l : ℤ)),
    A ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
⊢ A ^ ((↑k : ℤ) + n) = HPow.hPow (β := ℤ) A (↑k : ℤ) * A ^ n

Tactic:
obtain ⟨l, rfl⟩ := eq_ofNat_of_zero_le hn

Premises used: Int.eq_ofNat_of_zero_le, rfl
-- 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
k : ℕ
hm : LE.le (α := ℤ) 0 (↑k : ℤ)
l : ℕ
hn : LE.le (α := ℤ) 0 (↑l : ℤ)
rw : HPow.hPow (β := ℤ) A (↑(k + l) : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
rw₁ : A ^ (k + l) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
rw₂ : A ^ (k + l) = A ^ k * HPow.hPow (β := ℤ) A (↑l : ℤ)
rw₃ : A ^ (k + l) = A ^ k * A ^ l
rw₄ rw₅ : A ^ k * A ^ l = A ^ k * A ^ l
⊢ A ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)

Tactic:
rw [← Int.natCast_add, zpow_natCast, zpow_natCast, zpow_natCast, pow_add]

Premises used: zpow_natCast, Int.natCast_add, pow_add
-- 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
h : IsUnit A.det
i : ℤ
rw : HPow.hPow (β := ℤ) A 1 * A ^ i = A * A ^ i
rw₁ rw₂ : A * A ^ i = A * A ^ i
⊢ A ^ (1 + i) = A * A ^ i

Tactic:
rw [zpow_add h, zpow_one]

Premises used: Matrix.zpow_add, zpow_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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
⊢ SemiconjBy A (HPow.hPow (β := ℤ) X (↑n : ℤ)) (HPow.hPow (β := ℤ) Y (↑n : ℤ))

Tactic:
simp [h.pow_right n]

Premises used: SemiconjBy.pow_right
-- 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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
rw : IsUnit (X.det ^ n.succ)
⊢ IsUnit (X ^ n.succ).det

Tactic:
rw [det_pow]

Premises used: Matrix.det_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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (X.det ^ n.succ)

Tactic:
hx.pow n.succ

Premises used: IsUnit.pow, Nat.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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (X.det ^ n.succ)

Tactic:
exact hx.pow n.succ

Premises used: IsUnit.pow, Nat.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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (X ^ n.succ).det

Tactic:
have hx' : IsUnit (X ^ n.succ).det := by
      rw [det_pow]
      exact hx.pow n.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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
rw : IsUnit (Y.det ^ n.succ)
⊢ IsUnit (Y ^ n.succ).det

Tactic:
rw [det_pow]

Premises used: Matrix.det_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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
⊢ IsUnit (Y.det ^ n.succ)

Tactic:
hy.pow n.succ

Premises used: IsUnit.pow, Nat.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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
⊢ IsUnit (Y.det ^ n.succ)

Tactic:
exact hy.pow n.succ

Premises used: IsUnit.pow, Nat.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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
⊢ IsUnit (Y ^ n.succ).det

Tactic:
have hy' : IsUnit (Y ^ n.succ).det := by
      rw [det_pow]
      exact hy.pow n.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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
rw : A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate = (↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])

Tactic:
rw [zpow_negSucc, zpow_negSucc, nonsing_inv_apply _ hx', nonsing_inv_apply _ hy', SemiconjBy]

Premises used: zpow_negSucc, SemiconjBy, Matrix.nonsing_inv_apply
-- 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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate = (↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A

Tactic:
(isRegular_of_isLeftRegular_det hy'.isRegular.left).left ?_

Premises used: Matrix.isRegular_of_isLeftRegular_det, IsUnit.isRegular, IsRegular.left
-- 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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
refine :
  Eq (α := M) ((fun (x : M) ↦ Y ^ n.succ * x) (A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate))
    ((fun (x : M) ↦ Y ^ n.succ * x) ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A))
⊢ A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate = (↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A

Tactic:
refine (isRegular_of_isLeftRegular_det hy'.isRegular.left).left ?_

Premises used: Matrix.isRegular_of_isLeftRegular_det, IsUnit.isRegular, IsRegular.left