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
m n : ℕ
zero : ∀ (m : ℕ), A⁻¹ ^ m * HPow.hPow (β := ℕ) A 0 = HPow.hPow (β := ℕ) A 0 * A⁻¹ ^ m
⊢ A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
have succ : ∀ (n : ℕ) (IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m) (m : ℕ), A⁻¹ ^ m * A ^ (n + 1) = A ^ (n + 1) * 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]
Cleared hypotheses: m, n
-- 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 : ℕ
⊢ HPow.hPow (α := M) (β := ℤ) 1 (↑n : ℤ) = 1
have rw : HPow.hPow (α := M) 1 n = 1
Tactic: rw [zpow_natCast, one_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
n : ℕ
rw : HPow.hPow (α := M) 1 n = 1
⊢ HPow.hPow (α := M) (β := ℤ) 1 (↑n : ℤ) = 1
have rw₁ : Eq (α := M) 1 1
Tactic: rw [zpow_natCast, one_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
n : ℕ
⊢ HPow.hPow (α := M) 1 -[n+1] = 1
have rw : (HPow.hPow (α := M) 1 (n + 1))⁻¹ = 1
Tactic: rw [zpow_negSucc, one_pow, inv_one]
-- 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 : ℕ
rw : (HPow.hPow (α := M) 1 (n + 1))⁻¹ = 1
⊢ HPow.hPow (α := M) 1 -[n+1] = 1
have rw₁ : Eq (α := M) 1⁻¹ 1
Tactic: rw [zpow_negSucc, one_pow, inv_one]
-- 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 : ℕ
rw : (HPow.hPow (α := M) 1 (n + 1))⁻¹ = 1
rw₁ : Eq (α := M) 1⁻¹ 1
⊢ HPow.hPow (α := M) 1 -[n+1] = 1
have rw₂ : Eq (α := M) 1 1
Tactic: rw [zpow_negSucc, one_pow, inv_one]
-- 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 : ℕ
h : Ne (α := ℤ) (↑n : ℤ) 0
⊢ HPow.hPow (α := M) (β := ℤ) 0 (↑n : ℤ) = 0
have rw : n ≠ 0
Tactic: rw [zpow_natCast, zero_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
n : ℤ
⊢ HPow.hPow (α := M) 0 n = if n = 0 then 1 else 0
have pos : ∀ (h : n = 0), HPow.hPow (α := M) 0 n = 1
Tactic: split_ifs with 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
n : ℤ
pos : ∀ (h : n = 0), HPow.hPow (α := M) 0 n = 1
⊢ HPow.hPow (α := M) 0 n = if n = 0 then 1 else 0
have neg : ∀ (h : ¬n = 0), HPow.hPow (α := M) 0 n = 0
Tactic: split_ifs with 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
n : ℤ
h : n = 0
⊢ HPow.hPow (α := M) 0 n = 1
have pos : HPow.hPow (α := M) (β := ℤ) 0 0 = 1
Tactic: rw [h, zpow_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
n : ℤ
h : n = 0
pos : HPow.hPow (α := M) (β := ℤ) 0 0 = 1
⊢ HPow.hPow (α := M) 0 n = 1
have pos₁ : Eq (α := M) 1 1
Tactic: rw [h, zpow_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
n : ℤ
h : ¬n = 0
⊢ HPow.hPow (α := M) 0 n = 0
have neg : Eq (α := M) 0 0
Tactic: rw [zero_zpow _ 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
n : ℕ
⊢ HPow.hPow (β := ℤ) A⁻¹ (↑n : ℤ) = (HPow.hPow (β := ℤ) A (↑n : ℤ))⁻¹
have rw : A⁻¹ ^ n = (HPow.hPow (β := ℤ) A (↑n : ℤ))⁻¹
Tactic: rw [zpow_natCast, zpow_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
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, 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
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, 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
n : ℕ
⊢ A⁻¹ ^ -[n+1] = (A ^ -[n+1])⁻¹
have rw : (A⁻¹ ^ (n + 1))⁻¹ = (A ^ -[n+1])⁻¹
Tactic: rw [zpow_negSucc, zpow_negSucc, 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
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, 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
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, 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
⊢ HPow.hPow (β := ℤ) A (-1) = A⁻¹
have h : A = DivInvMonoid.zpow (↑(Nat.succ 0) : ℤ) A
Tactic: convert! DivInvMonoid.zpow_neg' 0 A
-- 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 : ℤ)) = (A ^ n)⁻¹
have zero : HPow.hPow (β := ℤ) A (-(↑0 : ℤ)) = (HPow.hPow (β := ℕ) A 0)⁻¹
Tactic: cases n
Cleared hypotheses: n
-- 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 : ℕ
zero : HPow.hPow (β := ℤ) A (-(↑0 : ℤ)) = (HPow.hPow (β := ℕ) A 0)⁻¹
⊢ HPow.hPow (β := ℤ) A (-(↑n : ℤ)) = (A ^ n)⁻¹
have succ : ∀ (n : ℕ), HPow.hPow (β := ℤ) A (-(↑(n + 1) : ℤ)) = (A ^ (n + 1))⁻¹
Tactic: cases n
Cleared hypotheses: n
-- 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
n : ℤ
⊢ IsUnit (A ^ n).det
have ofNat : ∀ (n : ℕ), IsUnit (A ^ ofNat n).det
Tactic: rcases n with n | n
Cleared hypotheses: n
-- 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
n : ℤ
ofNat : ∀ (n : ℕ), IsUnit (A ^ Int.ofNat n).det
⊢ IsUnit (A ^ n).det
have negSucc : ∀ (n : ℕ), IsUnit (A ^ -[n+1]).det
Tactic: rcases n with n | n
Cleared hypotheses: n
-- 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
z : ℕ
h : 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
have succ : IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 0
Tactic: rw [← Int.natCast_succ, zpow_natCast, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero,
      Int.ofNat_inj]
-- 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
z : ℕ
h : 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
have pred : IsUnit A.det ↔ IsUnit A.det ∨ z.succ = 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]
-- 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
z : ℤ
⊢ IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0
have zero : IsUnit (HPow.hPow (β := ℤ) A 0).det ↔ IsUnit A.det ∨ Eq (α := ℤ) 0 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
Cleared hypotheses: 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
A : M
z : ℤ
zero : IsUnit (HPow.hPow (β := ℤ) A 0).det ↔ IsUnit A.det ∨ Eq (α := ℤ) 0 0
⊢ IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0
have 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)
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
Cleared hypotheses: 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
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)
⊢ IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0
have 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)
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
Cleared hypotheses: 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
A : M
h : IsUnit A.det
n : ℕ
⊢ A ^ (- -[n+1]) = (A ^ -[n+1])⁻¹
have h₁ : IsUnit (A ^ (n + 1)).det
Tactic: rw [zpow_negSucc, neg_negSucc, zpow_natCast, 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
n : ℕ
⊢ IsUnit (A ^ (n + 1)).det
have h₁ : IsUnit (A.det ^ (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
n : ℤ
⊢ A⁻¹ ^ n = A ^ (-n)
have rw : A⁻¹ ^ n = (A ^ n)⁻¹
Tactic: rw [zpow_neg h, inv_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
h : IsUnit A.det
n : ℤ
rw : A⁻¹ ^ n = (A ^ n)⁻¹
⊢ A⁻¹ ^ n = A ^ (-n)
have rw₁ : (A ^ n)⁻¹ = (A ^ n)⁻¹
Tactic: rw [zpow_neg h, inv_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
h : IsUnit A.det
n : ℕ
⊢ A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) = (A ^ n)⁻¹
have rw : A ^ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (-1) + 1) = (A ^ n)⁻¹
Tactic: rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_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
n : ℕ
rw : A ^ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (-1) + 1) = (A ^ n)⁻¹
⊢ A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) = (A ^ n)⁻¹
have rw₁ : HPow.hPow (β := ℤ) A (-(↑n : ℤ)) = (A ^ n)⁻¹
Tactic: rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_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
n : ℕ
rw : A ^ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (-1) + 1) = (A ^ n)⁻¹
rw₁ : HPow.hPow (β := ℤ) A (-(↑n : ℤ)) = (A ^ n)⁻¹
⊢ A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) = (A ^ n)⁻¹
have rw₂ : (HPow.hPow (β := ℤ) A (↑n : ℤ))⁻¹ = (A ^ n)⁻¹
Tactic: rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_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
n : ℕ
rw : A ^ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (-1) + 1) = (A ^ n)⁻¹
rw₁ : HPow.hPow (β := ℤ) A (-(↑n : ℤ)) = (A ^ n)⁻¹
rw₂ : (HPow.hPow (β := ℤ) A (↑n : ℤ))⁻¹ = (A ^ n)⁻¹
⊢ A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) = (A ^ n)⁻¹
have rw₃ : (A ^ n)⁻¹ = (A ^ n)⁻¹
Tactic: rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_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
n : ℕ
⊢ (A ^ n)⁻¹ = (A * A ^ n)⁻¹ * A
have rw : (A ^ n)⁻¹ = (A ^ n)⁻¹ * A⁻¹ * A
Tactic: rw [mul_inv_rev, Matrix.mul_assoc, nonsing_inv_mul _ h, Matrix.mul_one]
-- 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
n : ℕ
rw : (A ^ n)⁻¹ = (A ^ n)⁻¹ * A⁻¹ * A
⊢ (A ^ n)⁻¹ = (A * A ^ n)⁻¹ * A
have rw₁ : (A ^ n)⁻¹ = (A ^ n)⁻¹ * (A⁻¹ * A)
Tactic: rw [mul_inv_rev, Matrix.mul_assoc, nonsing_inv_mul _ h, Matrix.mul_one]
-- 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
n : ℕ
rw : (A ^ n)⁻¹ = (A ^ n)⁻¹ * A⁻¹ * A
rw₁ : (A ^ n)⁻¹ = (A ^ n)⁻¹ * (A⁻¹ * A)
⊢ (A ^ n)⁻¹ = (A * A ^ n)⁻¹ * A
have rw₂ : (A ^ n)⁻¹ = (A ^ n)⁻¹ * 1
Tactic: rw [mul_inv_rev, Matrix.mul_assoc, nonsing_inv_mul _ h, Matrix.mul_one]
-- 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
n : ℕ
rw : (A ^ n)⁻¹ = (A ^ n)⁻¹ * A⁻¹ * A
rw₁ : (A ^ n)⁻¹ = (A ^ n)⁻¹ * (A⁻¹ * A)
rw₂ : (A ^ n)⁻¹ = (A ^ n)⁻¹ * 1
⊢ (A ^ n)⁻¹ = (A * A ^ n)⁻¹ * A
have rw₃ : (A ^ n)⁻¹ = (A ^ n)⁻¹
Tactic: rw [mul_inv_rev, Matrix.mul_assoc, nonsing_inv_mul _ h, Matrix.mul_one]
-- 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
n : ℕ
⊢ (A * A ^ n)⁻¹ * A = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * A
have rw : (A * A ^ n)⁻¹ * A = (A ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)⁻¹ * A
Tactic: rw [zpow_neg h, ← Int.natCast_succ, zpow_natCast, pow_succ']
-- 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
n : ℕ
rw : (A * A ^ n)⁻¹ * A = (A ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)⁻¹ * A
⊢ (A * A ^ n)⁻¹ * A = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * A
have rw₁ : (A * A ^ n)⁻¹ * A = (HPow.hPow (β := ℤ) A (↑n.succ : ℤ))⁻¹ * A
Tactic: rw [zpow_neg h, ← Int.natCast_succ, zpow_natCast, pow_succ']
-- 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
n : ℕ
rw : (A * A ^ n)⁻¹ * A = (A ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)⁻¹ * A
rw₁ : (A * A ^ n)⁻¹ * A = (HPow.hPow (β := ℤ) A (↑n.succ : ℤ))⁻¹ * A
⊢ (A * A ^ n)⁻¹ * A = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * A
have rw₂ : (A * A ^ n)⁻¹ * A = (A ^ n.succ)⁻¹ * A
Tactic: rw [zpow_neg h, ← Int.natCast_succ, zpow_natCast, pow_succ']
-- 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
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
⊢ (A * A ^ n)⁻¹ * A = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * A
have rw₃ : (A * A ^ n)⁻¹ * A = (A * A ^ n)⁻¹ * A
Tactic: rw [zpow_neg h, ← Int.natCast_succ, zpow_natCast, pow_succ']
-- 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
n : ℤ
⊢ A ^ (n - 1) = A ^ (n - 1) * A * A⁻¹
have rw : A ^ (n - 1) = A ^ (n - 1) * (A * A⁻¹)
Tactic: rw [mul_assoc, mul_nonsing_inv _ h, mul_one]
-- 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
n : ℤ
rw : A ^ (n - 1) = A ^ (n - 1) * (A * A⁻¹)
⊢ A ^ (n - 1) = A ^ (n - 1) * A * A⁻¹
have rw₁ : A ^ (n - 1) = A ^ (n - 1) * 1
Tactic: rw [mul_assoc, mul_nonsing_inv _ h, mul_one]
-- 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
n : ℤ
rw : A ^ (n - 1) = A ^ (n - 1) * (A * A⁻¹)
rw₁ : A ^ (n - 1) = A ^ (n - 1) * 1
⊢ A ^ (n - 1) = A ^ (n - 1) * A * A⁻¹
have rw₂ : A ^ (n - 1) = A ^ (n - 1)
Tactic: rw [mul_assoc, mul_nonsing_inv _ h, mul_one]
-- 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
n : ℤ
⊢ A ^ (n - 1) * A * A⁻¹ = A ^ n * A⁻¹
have rw : A ^ (n - 1 + 1) * A⁻¹ = A ^ n * A⁻¹
Tactic: rw [← zpow_add_one h, sub_add_cancel]
-- 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
n : ℤ
rw : A ^ (n - 1 + 1) * A⁻¹ = A ^ n * A⁻¹
⊢ A ^ (n - 1) * A * A⁻¹ = A ^ n * A⁻¹
have rw₁ : A ^ n * A⁻¹ = A ^ n * A⁻¹
Tactic: rw [← zpow_add_one h, sub_add_cancel]
-- 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
m : ℤ
n : ℕ
ihn : A ^ (m + -(↑n : ℤ)) = A ^ m * HPow.hPow (β := ℤ) A (-(↑n : ℤ))
⊢ A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ m * A ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred : A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ m * (HPow.hPow (β := ℤ) A (-(↑n : ℤ)) * A⁻¹)
Tactic: rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
-- 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
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⁻¹)
⊢ A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ m * A ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred₁ : A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ m * HPow.hPow (β := ℤ) A (-(↑n : ℤ)) * A⁻¹
Tactic: rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
-- 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
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⁻¹
⊢ A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ m * A ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred₂ : A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ (m + -(↑n : ℤ)) * A⁻¹
Tactic: rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
-- 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
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⁻¹
⊢ A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ m * A ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred₃ : A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ (m + -(↑n : ℤ) - 1)
Tactic: rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
-- 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
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)
⊢ A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ m * A ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
have pred₄ : A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]