awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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)
⊢ A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) A (↑m : ℤ)) (↑n : ℤ)
have rw₃ : A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = HPow.hPow (β := ℤ) A (↑(m * n) : ℤ)
Tactic: rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast, Int.natCast_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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) : ℤ)
⊢ A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) A (↑m : ℤ)) (↑n : ℤ)
have rw₄ : A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ)
Tactic: rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast, Int.natCast_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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 : ℕ
⊢ A ^ ((↑m : ℤ) * -[n+1]) = HPow.hPow (β := ℤ) A (↑m : ℤ) ^ -[n+1]
have rw : A ^ ((↑m : ℤ) * -[n+1]) = (A ^ m) ^ -[n+1]
Tactic: rw [zpow_natCast, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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]
⊢ A ^ ((↑m : ℤ) * -[n+1]) = HPow.hPow (β := ℤ) A (↑m : ℤ) ^ -[n+1]
have rw₁ : A ^ ((↑m : ℤ) * -[n+1]) = ((A ^ m) ^ (n + 1))⁻¹
Tactic: rw [zpow_natCast, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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))⁻¹
⊢ A ^ ((↑m : ℤ) * -[n+1]) = HPow.hPow (β := ℤ) A (↑m : ℤ) ^ -[n+1]
have rw₂ : A ^ ((↑m : ℤ) * -[n+1]) = (A ^ (m * (n + 1)))⁻¹
Tactic: rw [zpow_natCast, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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)))⁻¹
⊢ A ^ ((↑m : ℤ) * -[n+1]) = HPow.hPow (β := ℤ) A (↑m : ℤ) ^ -[n+1]
have rw₃ : HPow.hPow (β := ℤ) A (-(↑(m * n.succ) : ℤ)) = (A ^ (m * (n + 1)))⁻¹
Tactic: rw [zpow_natCast, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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)))⁻¹
⊢ A ^ ((↑m : ℤ) * -[n+1]) = HPow.hPow (β := ℤ) A (↑m : ℤ) ^ -[n+1]
have rw₄ : (A ^ (m * n.succ))⁻¹ = (A ^ (m * (n + 1)))⁻¹
Tactic: rw [zpow_natCast, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_natCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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 : ℕ
⊢ A ^ (-[m+1] * (↑n : ℤ)) = HPow.hPow (β := ℤ) (A ^ -[m+1]) (↑n : ℤ)
have rw : A ^ (-[m+1] * (↑n : ℤ)) = (A ^ -[m+1]) ^ n
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_natCast,
        inv_pow']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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
⊢ A ^ (-[m+1] * (↑n : ℤ)) = HPow.hPow (β := ℤ) (A ^ -[m+1]) (↑n : ℤ)
have rw₁ : A ^ (-[m+1] * (↑n : ℤ)) = (A ^ (m + 1))⁻¹ ^ n
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_natCast,
        inv_pow']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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
⊢ A ^ (-[m+1] * (↑n : ℤ)) = HPow.hPow (β := ℤ) (A ^ -[m+1]) (↑n : ℤ)
have rw₂ : A ^ (-[m+1] * (↑n : ℤ)) = (A⁻¹ ^ (m + 1)) ^ n
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_natCast,
        inv_pow']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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
⊢ A ^ (-[m+1] * (↑n : ℤ)) = HPow.hPow (β := ℤ) (A ^ -[m+1]) (↑n : ℤ)
have rw₃ : A ^ (-[m+1] * (↑n : ℤ)) = A⁻¹ ^ ((m + 1) * n)
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_natCast,
        inv_pow']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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)
⊢ A ^ (-[m+1] * (↑n : ℤ)) = HPow.hPow (β := ℤ) (A ^ -[m+1]) (↑n : ℤ)
have rw₄ : HPow.hPow (β := ℤ) A (-(↑(m.succ * n) : ℤ)) = A⁻¹ ^ ((m + 1) * n)
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_natCast,
        inv_pow']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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)
⊢ A ^ (-[m+1] * (↑n : ℤ)) = HPow.hPow (β := ℤ) (A ^ -[m+1]) (↑n : ℤ)
have rw₅ : (A ^ (m.succ * n))⁻¹ = A⁻¹ ^ ((m + 1) * n)
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_natCast,
        inv_pow']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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)
⊢ A ^ (-[m+1] * (↑n : ℤ)) = HPow.hPow (β := ℤ) (A ^ -[m+1]) (↑n : ℤ)
have rw₆ : (A ^ (m.succ * n))⁻¹ = (A ^ ((m + 1) * n))⁻¹
Tactic: rw [zpow_natCast, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_natCast,
        inv_pow']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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 : ℕ
⊢ A ^ (-[m+1] * -[n+1]) = (A ^ -[m+1]) ^ -[n+1]
have h₁ : IsUnit (A ^ ((m + 1) * (n + 1))).det
Tactic: rw [zpow_negSucc, zpow_negSucc, negSucc_mul_negSucc, ← Int.natCast_mul, zpow_natCast, inv_pow',
      ← pow_mul, nonsing_inv_nonsing_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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 ^ ((m + 1) * (n + 1))).det
have h₁ : IsUnit (A.det ^ ((m + 1) * (n + 1)))
Tactic: rw [det_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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 : ℤ
⊢ A ^ (m * n) = (A ^ n) ^ m
have rw : A ^ (n * m) = (A ^ n) ^ m
Tactic: rw [mul_comm, zpow_mul _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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
⊢ A ^ (m * n) = (A ^ n) ^ m
have rw₁ : (A ^ n) ^ m = (A ^ n) ^ m
Tactic: rw [mul_comm, zpow_mul _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
u : Mˣ
n : ℕ
⊢ (↑(HPow.hPow (β := ℤ) u (↑n : ℤ)) : M) = HPow.hPow (β := ℤ) (↑u : M) (↑n : ℤ)
have rw : (↑(u ^ n) : M) = HPow.hPow (β := ℤ) (↑u : M) (↑n : ℤ)
Tactic: rw [zpow_natCast, zpow_natCast, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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 : ℤ)
⊢ (↑(HPow.hPow (β := ℤ) u (↑n : ℤ)) : M) = HPow.hPow (β := ℤ) (↑u : M) (↑n : ℤ)
have rw₁ : (↑(u ^ n) : M) = (↑u : M) ^ n
Tactic: rw [zpow_natCast, zpow_natCast, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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
⊢ (↑(HPow.hPow (β := ℤ) u (↑n : ℤ)) : M) = HPow.hPow (β := ℤ) (↑u : M) (↑n : ℤ)
have rw₂ : (↑u : M) ^ n = (↑u : M) ^ n
Tactic: rw [zpow_natCast, zpow_natCast, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
u : Mˣ
k : ℕ
⊢ (↑(u ^ -[k+1]) : M) = (↑u : M) ^ -[k+1]
have rw : (↑(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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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]
⊢ (↑(u ^ -[k+1]) : M) = (↑u : M) ^ -[k+1]
have rw₁ : (↑(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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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))⁻¹
⊢ (↑(u ^ -[k+1]) : M) = (↑u : M) ^ -[k+1]
have rw₂ : (↑(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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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))⁻¹
⊢ (↑(u ^ -[k+1]) : M) = (↑u : M) ^ -[k+1]
have rw₃ : (↑u⁻¹ : M) ^ (k + 1) = ((↑u : M) ^ (k + 1))⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, ← inv_pow, u⁻¹.val_pow_eq_pow_val, ← inv_pow', coe_units_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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))⁻¹
⊢ (↑(u ^ -[k+1]) : M) = (↑u : M) ^ -[k+1]
have rw₄ : (↑u⁻¹ : M) ^ (k + 1) = (↑u : M)⁻¹ ^ (k + 1)
Tactic: rw [zpow_negSucc, zpow_negSucc, ← inv_pow, u⁻¹.val_pow_eq_pow_val, ← inv_pow', coe_units_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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)
⊢ (↑(u ^ -[k+1]) : M) = (↑u : M) ^ -[k+1]
have rw₅ : (↑u : M)⁻¹ ^ (k + 1) = (↑u : M)⁻¹ ^ (k + 1)
Tactic: rw [zpow_negSucc, zpow_negSucc, ← inv_pow, u⁻¹.val_pow_eq_pow_val, ← inv_pow', coe_units_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (hypothesis)
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 : ℤ
⊢ A ^ z ≠ 0
have this : IsUnit (A ^ z).det
Tactic: have := ha.det_zpow z
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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
⊢ A ^ z ≠ 0
have contrapose : ∀ (this : A ^ z = 0), ¬IsUnit (A ^ z).det
Tactic: contrapose this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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 (A ^ z).det
have rw : ¬IsUnit.{u_2} («M» := R) 0
Tactic: rw [this, det_zero ‹_›]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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 : ℤ
⊢ A ^ (z1 - z2) = A ^ z1 / A ^ z2
have rw : A ^ (z1 + -z2) = A ^ z1 / A ^ z2
Tactic: rw [sub_eq_add_neg, zpow_add ha, zpow_neg ha, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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
⊢ A ^ (z1 - z2) = A ^ z1 / A ^ z2
have rw₁ : A ^ z1 * A ^ (-z2) = A ^ z1 / A ^ z2
Tactic: rw [sub_eq_add_neg, zpow_add ha, zpow_neg ha, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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
⊢ A ^ (z1 - z2) = A ^ z1 / A ^ z2
have rw₂ : A ^ z1 * (A ^ z2)⁻¹ = A ^ z1 / A ^ z2
Tactic: rw [sub_eq_add_neg, zpow_add ha, zpow_neg ha, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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
⊢ A ^ (z1 - z2) = A ^ z1 / A ^ z2
have rw₃ : A ^ z1 * (A ^ z2)⁻¹ = A ^ z1 * (A ^ z2)⁻¹
Tactic: rw [sub_eq_add_neg, zpow_add ha, zpow_neg ha, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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 : ℕ
⊢ (A * B) ^ -[n+1] = A ^ -[n+1] * B ^ -[n+1]
have rw : ((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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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]
⊢ (A * B) ^ -[n+1] = A ^ -[n+1] * B ^ -[n+1]
have rw₁ : ((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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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]
⊢ (A * B) ^ -[n+1] = A ^ -[n+1] * B ^ -[n+1]
have rw₂ : ((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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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))⁻¹
⊢ (A * B) ^ -[n+1] = A ^ -[n+1] * B ^ -[n+1]
have rw₃ : ((A * B) ^ (n + 1))⁻¹ = (B ^ (n + 1) * A ^ (n + 1))⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, zpow_negSucc, ← mul_inv_rev,
      h.mul_pow n.succ, (h.pow_pow _ _).eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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))⁻¹
⊢ (A * B) ^ -[n+1] = A ^ -[n+1] * B ^ -[n+1]
have rw₄ : (A ^ n.succ * B ^ n.succ)⁻¹ = (B ^ (n + 1) * A ^ (n + 1))⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, zpow_negSucc, ← mul_inv_rev,
      h.mul_pow n.succ, (h.pow_pow _ _).eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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))⁻¹
⊢ (A * B) ^ -[n+1] = A ^ -[n+1] * B ^ -[n+1]
have rw₅ : (B ^ n.succ * A ^ n.succ)⁻¹ = (B ^ (n + 1) * A ^ (n + 1))⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, zpow_negSucc, ← mul_inv_rev,
      h.mul_pow n.succ, (h.pow_pow _ _).eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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
⊢ A ^ (-n) * A ^ n = 1
have rw : (A ^ n)⁻¹ * A ^ n = 1
Tactic: rw [zpow_neg h, nonsing_inv_mul _ (h.det_zpow _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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
⊢ A ^ (-n) * A ^ n = 1
have rw₁ : Eq (α := M) 1 1
Tactic: rw [zpow_neg h, nonsing_inv_mul _ (h.det_zpow _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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 : ℤ))ᵀ = HPow.hPow (β := ℤ) Aᵀ (↑n : ℤ)
have rw : (A ^ n)ᵀ = HPow.hPow (β := ℤ) Aᵀ (↑n : ℤ)
Tactic: rw [zpow_natCast, zpow_natCast, transpose_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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 : ℤ)
⊢ (HPow.hPow (β := ℤ) A (↑n : ℤ))ᵀ = HPow.hPow (β := ℤ) Aᵀ (↑n : ℤ)
have rw₁ : (A ^ n)ᵀ = Aᵀ ^ n
Tactic: rw [zpow_natCast, zpow_natCast, transpose_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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
⊢ (HPow.hPow (β := ℤ) A (↑n : ℤ))ᵀ = HPow.hPow (β := ℤ) Aᵀ (↑n : ℤ)
have rw₂ : Aᵀ ^ n = Aᵀ ^ n
Tactic: rw [zpow_natCast, zpow_natCast, transpose_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
Goal:
n' : Type u_1
inst : DecidableEq n'
inst_1 : Fintype n'
R : Type u_2
inst_2 : CommRing R
A : M
n : ℕ
⊢ (A ^ -[n+1])ᵀ = Aᵀ ^ -[n+1]
have rw : (A ^ (n + 1))⁻¹ᵀ = Aᵀ ^ -[n+1]
Tactic: rw [zpow_negSucc, zpow_negSucc, transpose_nonsing_inv, transpose_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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]
⊢ (A ^ -[n+1])ᵀ = Aᵀ ^ -[n+1]
have rw₁ : (A ^ (n + 1))⁻¹ᵀ = (Aᵀ ^ (n + 1))⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, transpose_nonsing_inv, transpose_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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))⁻¹
⊢ (A ^ -[n+1])ᵀ = Aᵀ ^ -[n+1]
have rw₂ : (A ^ (n + 1))ᵀ⁻¹ = (Aᵀ ^ (n + 1))⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, transpose_nonsing_inv, transpose_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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))⁻¹
⊢ (A ^ -[n+1])ᵀ = Aᵀ ^ -[n+1]
have rw₃ : (Aᵀ ^ (n + 1))⁻¹ = (Aᵀ ^ (n + 1))⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, transpose_nonsing_inv, transpose_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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 : ℕ
⊢ (HPow.hPow (β := ℤ) A (↑n : ℤ))ᴴ = HPow.hPow (β := ℤ) Aᴴ (↑n : ℤ)
have rw : (A ^ n)ᴴ = HPow.hPow (β := ℤ) Aᴴ (↑n : ℤ)
Tactic: rw [zpow_natCast, zpow_natCast, conjTranspose_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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 : ℤ)
⊢ (HPow.hPow (β := ℤ) A (↑n : ℤ))ᴴ = HPow.hPow (β := ℤ) Aᴴ (↑n : ℤ)
have rw₁ : (A ^ n)ᴴ = Aᴴ ^ n
Tactic: rw [zpow_natCast, zpow_natCast, conjTranspose_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ZPow (goal)
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
⊢ (HPow.hPow (β := ℤ) A (↑n : ℤ))ᴴ = HPow.hPow (β := ℤ) Aᴴ (↑n : ℤ)
have rw₂ : Aᴴ ^ n = Aᴴ ^ n
Tactic: rw [zpow_natCast, zpow_natCast, conjTranspose_pow]