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 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 :
  Y ^ n.succ * A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
rw₁ :
  A * X ^ n.succ * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
rw₂ :
  A * (X ^ n.succ * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate) =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
rw₃ :
  A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ * (X ^ n.succ).adjugate) =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
rw₄ :
  A * (↑hx'.unit⁻¹ : R) • HSMul.hSMul (β := M) (X ^ n.succ).det 1 =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
rw₅ :
  A * (↑hx'.unit⁻¹ : R) • HSMul.hSMul (β := M) (X ^ n.succ).det 1 =
    Y ^ n.succ * (↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A
rw₆ :
  A * (↑hx'.unit⁻¹ : R) • HSMul.hSMul (β := M) (X ^ n.succ).det 1 =
    (↑hy'.unit⁻¹ : R) • (Y ^ n.succ * (Y ^ n.succ).adjugate) * A
rw₇ :
  A * (↑hx'.unit⁻¹ : R) • HSMul.hSMul (β := M) (X ^ n.succ).det 1 =
    (↑hy'.unit⁻¹ : R) • HSMul.hSMul (β := M) (Y ^ n.succ).det 1 * A
rw₈ :
  A * HSMul.hSMul (β := M) ((↑hx'.unit⁻¹ : R) * (X ^ n.succ).det) 1 =
    (↑hy'.unit⁻¹ : R) • HSMul.hSMul (β := M) (Y ^ n.succ).det 1 * A
rw₉ :
  A * HSMul.hSMul (β := M) ((↑hx'.unit⁻¹ : R) * (X ^ n.succ).det) 1 =
    HSMul.hSMul (β := M) ((↑hy'.unit⁻¹ : R) * (Y ^ n.succ).det) 1 * A
rw₁₀ : A * HSMul.hSMul (α := R) (β := M) 1 1 = HSMul.hSMul (β := M) ((↑hy'.unit⁻¹ : R) * (Y ^ n.succ).det) 1 * A
rw₁₁ : A * HSMul.hSMul (α := R) (β := M) 1 1 = HSMul.hSMul (α := R) (β := M) 1 1 * A
rw₁₂ : A * 1 = 1 * A
rw₁₃ : A = 1 * A
rw₁₄ rw₁₅ : A = A
⊢ Y ^ n.succ * (A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate) =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)

Tactic:
rw [← mul_assoc, ← (h.pow_right n.succ).eq, mul_assoc, Matrix.mul_smul,
      mul_adjugate, ← Matrix.mul_assoc, Matrix.mul_smul (Y ^ _) (↑hy'.unit⁻¹ : R),
      mul_adjugate, smul_smul, smul_smul, hx'.val_inv_mul,
      hy'.val_inv_mul, one_smul, Matrix.mul_one, Matrix.one_mul]

Premises used: Units.val, Matrix.mul_smul, mul_assoc, Matrix.mul_assoc, smul_smul, SemiconjBy.eq, one_smul, SemiconjBy.pow_right, Inv.inv, HPow.hPow, IsUnit.unit, Matrix.mul_one, IsUnit.val_inv_mul, Nat.succ, Matrix.one_mul, Matrix.mul_adjugate
-- 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 B : M
h : Commute A B
m : ℤ
inl : ∀ (hB : B⁻¹ * B = 1), B * B⁻¹ = 1 → Commute A (B ^ m)
inr : ∀ (hB : B⁻¹ = 0), Commute A (B ^ m)
⊢ Commute A (B ^ m)

Tactic:
rcases nonsing_inv_cancel_or_zero B with (⟨hB, _⟩ | hB)

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 B : M
h : Commute A B
m : ℤ
hB : B⁻¹ * B = 1
right : B * B⁻¹ = 1
⊢ Commute A (B ^ m)

Tactic:
SemiconjBy.zpow_right ?_ ?_ h _

Premises used: Matrix.SemiconjBy.zpow_right, Commute
-- 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 B : M
h : Commute A B
m : ℤ
hB : B⁻¹ * B = 1
right : B * B⁻¹ = 1
inl inl₁ : IsUnit B.det
⊢ Commute A (B ^ m)

Tactic:
refine SemiconjBy.zpow_right ?_ ?_ h _

Premises used: Matrix.SemiconjBy.zpow_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 B : M
h : Commute A B
m : ℤ
hB : B⁻¹ * B = 1
right : B * B⁻¹ = 1
⊢ IsUnit B.det

Tactic:
isUnit_det_of_left_inverse hB

Premises used: 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 B : M
h : Commute A B
m : ℤ
hB : B⁻¹ * B = 1
right : B * B⁻¹ = 1
⊢ IsUnit B.det

Tactic:
exact isUnit_det_of_left_inverse hB

Premises used: 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 B : M
h : Commute A B
m : ℤ
hB : B⁻¹ = 0
inr : ∀ (a : ℕ), Commute A (B ^ ofNat a)
inr₁ : ∀ (a : ℕ), Commute A (B ^ -[a+1])
⊢ Commute A (B ^ m)

Tactic:
cases 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 B : M
h : Commute A B
hB : B⁻¹ = 0
a : ℕ
⊢ Commute A (B ^ ofNat a)

Tactic:
simpa using h.pow_right _

Premises used: Commute.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 B : M
h : Commute A B
hB : B⁻¹ = 0
a : ℕ
⊢ Commute A (B ^ -[a+1])

Tactic:
simp [← inv_pow', hB]

Premises used: 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 B : M
h : Commute A B
m : ℤ
⊢ Commute (A ^ m) B

Tactic:
(Commute.zpow_right h.symm m).symm

Premises used: Matrix.Commute.zpow_right, Commute.symm
-- 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 B : M
h : Commute A B
m n : ℤ
⊢ Commute (A ^ m) (B ^ n)

Tactic:
Commute.zpow_right (Commute.zpow_left h _) _

Premises used: Matrix.Commute.zpow_right, Matrix.Commute.zpow_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 : M
n : ℤ
⊢ Commute (A ^ n) A

Tactic:
Commute.zpow_left (Commute.refl A) _

Premises used: Matrix.Commute.zpow_left, Commute.refl
-- 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 : ℤ
⊢ Commute A (A ^ n)

Tactic:
Commute.zpow_right (Commute.refl A) _

Premises used: Matrix.Commute.zpow_right, Commute.refl
-- 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 : ℤ
⊢ Commute (A ^ m) (A ^ n)

Tactic:
Commute.zpow_zpow (Commute.refl A) _ _

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

Tactic:
simp only [pow_succ, ← Nat.cast_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
n : ℕ
h : -HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 ≠ -1
inl :
  ∀ (h : A⁻¹ * A = 1), A * A⁻¹ = 1 → A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * A
inr : ∀ (h : A⁻¹ = 0), A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * A
⊢ A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * A

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
n : ℕ
h_1 : -HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 ≠ -1
h : A⁻¹ * A = 1
right : A * A⁻¹ = 1
⊢ A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * A

Tactic:
apply zpow_add_one (isUnit_det_of_left_inverse h)

Premises used: Matrix.zpow_add_one, 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
n : ℕ
h_1 : -HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 ≠ -1
h : A⁻¹ = 0
inr : HPow.hPow (β := ℤ) A (-(↑(n + 1) : ℤ)) = HPow.hPow (β := ℤ) A (-(↑(n + 2) : ℤ)) * A
⊢ A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * A

Tactic:
change A ^ (-((n + 1 : ℕ) : ℤ)) = A ^ (-((n + 2 : ℕ) : ℤ)) * A

Premises used: Nat.cast, HAdd.hAdd, OfNat.ofNat, Neg.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
n : ℕ
h_1 : -HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 ≠ -1
h : A⁻¹ = 0
inr : (A ^ (n + 1))⁻¹ = (A ^ (n + 2))⁻¹ * A
inr₁ : A⁻¹ ^ (n + 1) = A⁻¹ ^ (n + 2) * A
inr₂ : HPow.hPow (α := M) 0 (n + 1) = HPow.hPow (α := M) 0 (n + 2) * A
inr₃ : 0 = 0 * A
⊢ HPow.hPow (β := ℤ) A (-(↑(n + 1) : ℤ)) = HPow.hPow (β := ℤ) A (-(↑(n + 2) : ℤ)) * A

Tactic:
simp_rw [zpow_neg_natCast, ← inv_pow', h, zero_pow <| Nat.succ_ne_zero _, zero_mul]

Premises used: MulZeroClass.zero_mul, Matrix.inv_pow', Nat.succ_ne_zero, Matrix.zpow_neg_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
A : M
h : IsUnit A.det
m n : ℕ
rw : A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = HPow.hPow (β := ℤ) A (↑m : ℤ) ^ n
rw₁ : A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = (A ^ m) ^ n
rw₂ : A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = A ^ (m * n)
rw₃ : A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = HPow.hPow (β := ℤ) A (↑(m * n) : ℤ)
rw₄ rw₅ : A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ)
⊢ A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) A (↑m : ℤ)) (↑n : ℤ)

Tactic:
rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast, Int.natCast_mul]

Premises used: zpow_natCast, pow_mul, Int.natCast_mul
-- 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
m n : ℕ
rw : A ^ ((↑m : ℤ) * -[n+1]) = (A ^ m) ^ -[n+1]
rw₁ : A ^ ((↑m : ℤ) * -[n+1]) = ((A ^ m) ^ (n + 1))⁻¹
rw₂ : A ^ ((↑m : ℤ) * -[n+1]) = (A ^ (m * (n + 1)))⁻¹
rw₃ : HPow.hPow (β := ℤ) A (-(↑(m * n.succ) : ℤ)) = (A ^ (m * (n + 1)))⁻¹
rw₄ rw₅ : (A ^ (m * n.succ))⁻¹ = (A ^ (m * (n + 1)))⁻¹
⊢ A ^ ((↑m : ℤ) * -[n+1]) = HPow.hPow (β := ℤ) A (↑m : ℤ) ^ -[n+1]

Tactic:
rw [zpow_natCast, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_natCast]

Premises used: zpow_natCast, zpow_negSucc, Int.ofNat_mul_negSucc, pow_mul, 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
h : IsUnit A.det
m n : ℕ
rw : A ^ (-[m+1] * (↑n : ℤ)) = (A ^ -[m+1]) ^ n
rw₁ : A ^ (-[m+1] * (↑n : ℤ)) = (A ^ (m + 1))⁻¹ ^ n
rw₂ : A ^ (-[m+1] * (↑n : ℤ)) = (A⁻¹ ^ (m + 1)) ^ n
rw₃ : A ^ (-[m+1] * (↑n : ℤ)) = A⁻¹ ^ ((m + 1) * n)
rw₄ : HPow.hPow (β := ℤ) A (-(↑(m.succ * n) : ℤ)) = A⁻¹ ^ ((m + 1) * n)
rw₅ : (A ^ (m.succ * n))⁻¹ = A⁻¹ ^ ((m + 1) * n)
rw₆ rw₇ : (A ^ (m.succ * n))⁻¹ = (A ^ ((m + 1) * n))⁻¹
⊢ A ^ (-[m+1] * (↑n : ℤ)) = HPow.hPow (β := ℤ) (A ^ -[m+1]) (↑n : ℤ)

Tactic:
rw [zpow_natCast, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_natCast,
        inv_pow']

Premises used: zpow_natCast, Int.negSucc_mul_ofNat, zpow_negSucc, pow_mul, 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
h : IsUnit A.det
m n : ℕ
h₁ : IsUnit (A ^ ((m + 1) * (n + 1))).det
⊢ A ^ (-[m+1] * -[n+1]) = (A ^ -[m+1]) ^ -[n+1]

Tactic:
rw [zpow_negSucc, zpow_negSucc, negSucc_mul_negSucc, ← Int.natCast_mul, zpow_natCast, inv_pow',
      ← pow_mul, nonsing_inv_nonsing_inv]

Premises used: zpow_natCast, zpow_negSucc, Matrix.nonsing_inv_nonsing_inv, pow_mul, Int.natCast_mul, Matrix.inv_pow', Int.negSucc_mul_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
A : M
h : IsUnit A.det
m n : ℕ
h₁ : IsUnit (A.det ^ ((m + 1) * (n + 1)))
⊢ IsUnit (A ^ ((m + 1) * (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
m n : ℕ
⊢ IsUnit (A.det ^ ((m + 1) * (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
m n : ℕ
⊢ IsUnit (A.det ^ ((m + 1) * (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
m n : ℤ
rw : A ^ (n * m) = (A ^ n) ^ m
rw₁ rw₂ : (A ^ n) ^ m = (A ^ n) ^ m
⊢ A ^ (m * n) = (A ^ n) ^ m

Tactic:
rw [mul_comm, zpow_mul _ h]

Premises used: mul_comm, Matrix.zpow_mul
-- 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
u : Mˣ
n : ℕ
rw : (↑(u ^ n) : M) = HPow.hPow (β := ℤ) (↑u : M) (↑n : ℤ)
rw₁ : (↑(u ^ n) : M) = (↑u : M) ^ n
rw₂ rw₃ : (↑u : M) ^ n = (↑u : M) ^ n
⊢ (↑(HPow.hPow (β := ℤ) u (↑n : ℤ)) : M) = HPow.hPow (β := ℤ) (↑u : M) (↑n : ℤ)

Tactic:
rw [zpow_natCast, zpow_natCast, Units.val_pow_eq_pow_val]

Premises used: zpow_natCast, Units.val_pow_eq_pow_val
-- 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
u : Mˣ
k : ℕ
rw : (↑(u ^ (k + 1))⁻¹ : M) = (↑u : M) ^ -[k+1]
rw₁ : (↑(u ^ (k + 1))⁻¹ : M) = ((↑u : M) ^ (k + 1))⁻¹
rw₂ : (↑(u⁻¹ ^ (k + 1)) : M) = ((↑u : M) ^ (k + 1))⁻¹
rw₃ : (↑u⁻¹ : M) ^ (k + 1) = ((↑u : M) ^ (k + 1))⁻¹
rw₄ : (↑u⁻¹ : M) ^ (k + 1) = (↑u : M)⁻¹ ^ (k + 1)
rw₅ rw₆ : (↑u : M)⁻¹ ^ (k + 1) = (↑u : M)⁻¹ ^ (k + 1)
⊢ (↑(u ^ -[k+1]) : M) = (↑u : M) ^ -[k+1]

Tactic:
rw [zpow_negSucc, zpow_negSucc, ← inv_pow, u⁻¹.val_pow_eq_pow_val, ← inv_pow', coe_units_inv]

Premises used: Matrix.coe_units_inv, zpow_negSucc, inv_pow, Inv.inv, Matrix.inv_pow', Units.val_pow_eq_pow_val
-- 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
inst_3 : Nonempty n'
inst_4 : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
⊢ IsUnit (A ^ z).det

Tactic:
have := ha.det_zpow z
-- 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
inst_3 : Nonempty n'
inst_4 : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
this : IsUnit (A ^ z).det
contrapose : ∀ (this : A ^ z = 0), ¬IsUnit (A ^ z).det
⊢ A ^ z ≠ 0

Tactic:
contrapose this
-- 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
inst_3 : Nonempty n'
inst_4 : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
this : A ^ z = 0
rw : ¬IsUnit.{u_2} («M» := R) 0
⊢ ¬IsUnit (A ^ z).det

Tactic:
rw [this, det_zero ‹_›]

Premises used: Matrix.det_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
inst_3 : Nonempty n'
inst_4 : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit.{u_2} («M» := R) 0

Tactic:
not_isUnit_zero

Premises used: not_isUnit_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
inst_3 : Nonempty n'
inst_4 : Nontrivial R
A : M
ha : IsUnit A.det
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit.{u_2} («M» := R) 0

Tactic:
exact not_isUnit_zero

Premises used: not_isUnit_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
ha : IsUnit A.det
z1 z2 : ℤ
rw : A ^ (z1 + -z2) = A ^ z1 / A ^ z2
rw₁ : A ^ z1 * A ^ (-z2) = A ^ z1 / A ^ z2
rw₂ : A ^ z1 * (A ^ z2)⁻¹ = A ^ z1 / A ^ z2
rw₃ rw₄ : A ^ z1 * (A ^ z2)⁻¹ = A ^ z1 * (A ^ z2)⁻¹
⊢ A ^ (z1 - z2) = A ^ z1 / A ^ z2

Tactic:
rw [sub_eq_add_neg, zpow_add ha, zpow_neg ha, div_eq_mul_inv]

Premises used: Matrix.zpow_add, sub_eq_add_neg, div_eq_mul_inv, Matrix.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 B : M
h : Commute A B
n : ℕ
⊢ HPow.hPow (β := ℤ) (A * B) (↑n : ℤ) = HPow.hPow (β := ℤ) A (↑n : ℤ) * HPow.hPow (β := ℤ) B (↑n : ℤ)

Tactic:
simp [h.mul_pow n]

Premises used: Commute.mul_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 B : M
h : Commute A B
n : ℕ
rw : ((A * B) ^ (n + 1))⁻¹ = A ^ -[n+1] * B ^ -[n+1]
rw₁ : ((A * B) ^ (n + 1))⁻¹ = (A ^ (n + 1))⁻¹ * B ^ -[n+1]
rw₂ : ((A * B) ^ (n + 1))⁻¹ = (A ^ (n + 1))⁻¹ * (B ^ (n + 1))⁻¹
rw₃ : ((A * B) ^ (n + 1))⁻¹ = (B ^ (n + 1) * A ^ (n + 1))⁻¹
rw₄ : (A ^ n.succ * B ^ n.succ)⁻¹ = (B ^ (n + 1) * A ^ (n + 1))⁻¹
rw₅ rw₆ : (B ^ n.succ * A ^ n.succ)⁻¹ = (B ^ (n + 1) * A ^ (n + 1))⁻¹
⊢ (A * B) ^ -[n+1] = A ^ -[n+1] * B ^ -[n+1]

Tactic:
rw [zpow_negSucc, zpow_negSucc, zpow_negSucc, ← mul_inv_rev,
      h.mul_pow n.succ, (h.pow_pow _ _).eq]

Premises used: zpow_negSucc, Commute.pow_pow, Matrix.mul_inv_rev, Commute.mul_pow, Nat.succ, Commute.eq
-- 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 : ℤ
A : M
h : IsUnit A.det
rw : (A ^ n)⁻¹ * A ^ n = 1
rw₁ rw₂ : Eq (α := M) 1 1
⊢ A ^ (-n) * A ^ n = 1

Tactic:
rw [zpow_neg h, nonsing_inv_mul _ (h.det_zpow _)]

Premises used: Matrix.nonsing_inv_mul, IsUnit.det_zpow, Matrix.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
n : ℕ
⊢ (1 / A) ^ n = 1 / A ^ n

Tactic:
simp only [one_div, inv_pow']

Premises used: Matrix.inv_pow', one_div
-- 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 : ℤ
⊢ (1 / A) ^ n = 1 / A ^ n

Tactic:
simp only [one_div, inv_zpow]

Premises used: one_div, 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
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, transpose_pow]

Premises used: zpow_natCast, Matrix.transpose_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 : ℕ
rw : (A ^ (n + 1))⁻¹ᵀ = Aᵀ ^ -[n+1]
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, transpose_nonsing_inv, transpose_pow]

Premises used: zpow_negSucc, Matrix.transpose_pow, Matrix.transpose_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
inst_3 : StarRing 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, conjTranspose_pow]

Premises used: zpow_natCast, Matrix.conjTranspose_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
inst_3 : StarRing R
A : M
n : ℕ
rw : (A ^ (n + 1))⁻¹ᴴ = Aᴴ ^ -[n+1]
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, conjTranspose_nonsing_inv, conjTranspose_pow]

Premises used: zpow_negSucc, Matrix.conjTranspose_nonsing_inv, Matrix.conjTranspose_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 : A.IsSymm
k : ℤ
rw : (A ^ k)ᵀ = A ^ k
rw₁ : Aᵀ ^ k = A ^ k
rw₂ rw₃ : A ^ k = A ^ k
⊢ (A ^ k).IsSymm

Tactic:
rw [IsSymm, transpose_zpow, h]

Premises used: Matrix.transpose_zpow, Matrix.IsSymm
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' f g : MultilinearMap R M₁ M₂
h :
  Eq (α := (a : (i : ι) → M₁ i) → M₂) ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁)) f)
    ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁)) g)
mk :
  ∀ (toFun : ((i : ι) → M₁ i) → M₂)
    (map_update_add' :
      ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
        toFun (update (β := M₁) m i (x + y)) = toFun (update (β := M₁) m i x) + toFun (update (β := M₁) m i y))
    (map_update_smul' :
      ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
        toFun (update (β := M₁) m i (c • x)) = c • toFun (update (β := M₁) m i x))
    (h :
      Eq (α := (a : (i : ι) → M₁ i) → M₂)
        ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁))
          (MultilinearMap.mk (M₁ := M₁) toFun map_update_add' map_update_smul'))
        ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁)) g)),
    MultilinearMap.mk (M₁ := M₁) toFun map_update_add' map_update_smul' = g
⊢ f = g

Tactic:
cases f