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 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
⊢ Y ^ n.succ * (A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate) =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
have 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
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]
-- 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 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
⊢ Y ^ n.succ * (A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate) =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
have 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
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]
-- 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 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
⊢ Y ^ n.succ * (A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate) =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
have 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
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]
-- 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 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
⊢ Y ^ n.succ * (A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate) =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
have rw₁₀ : A * HSMul.hSMul (α := R) (β := M) 1 1 = HSMul.hSMul (β := M) ((↑hy'.unit⁻¹ : R) * (Y ^ n.succ).det) 1 * 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]
-- 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 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
⊢ Y ^ n.succ * (A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate) =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
have rw₁₁ : A * HSMul.hSMul (α := R) (β := M) 1 1 = HSMul.hSMul (α := R) (β := M) 1 1 * 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]
-- 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 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
⊢ Y ^ n.succ * (A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate) =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
have rw₁₂ : A * 1 = 1 * 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]
-- 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 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
⊢ Y ^ n.succ * (A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate) =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
have rw₁₃ : A = 1 * 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]
-- 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 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
⊢ Y ^ n.succ * (A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate) =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
have rw₁₄ : A = 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]
-- 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
m : ℤ
⊢ Commute A (B ^ m)
have inl : ∀ (hB : B⁻¹ * B = 1), B * B⁻¹ = 1 → Commute A (B ^ m)
Tactic: rcases nonsing_inv_cancel_or_zero B with (⟨hB, _⟩ | hB)
-- 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
m : ℤ
inl : ∀ (hB : B⁻¹ * B = 1), B * B⁻¹ = 1 → Commute A (B ^ m)
⊢ Commute A (B ^ m)
have inr : ∀ (hB : B⁻¹ = 0), Commute A (B ^ m)
Tactic: rcases nonsing_inv_cancel_or_zero B with (⟨hB, _⟩ | hB)
-- 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
m : ℤ
hB : B⁻¹ * B = 1
right : B * B⁻¹ = 1
⊢ Commute A (B ^ m)
have inl : IsUnit B.det
Tactic: refine SemiconjBy.zpow_right ?_ ?_ 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 B : M
h : Commute A B
m : ℤ
hB : B⁻¹ = 0
⊢ Commute A (B ^ m)
have inr : ∀ (a : ℕ), Commute A (B ^ ofNat a)
Tactic: cases m
Cleared hypotheses: m
-- 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
m : ℤ
hB : B⁻¹ = 0
inr : ∀ (a : ℕ), Commute A (B ^ ofNat a)
⊢ Commute A (B ^ m)
have inr₁ : ∀ (a : ℕ), Commute A (B ^ -[a+1])
Tactic: cases m
Cleared hypotheses: m
-- 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 : ℕ
h : -HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 ≠ -1
⊢ A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * A
have inl : ∀ (h : A⁻¹ * A = 1), A * A⁻¹ = 1 → A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * A
Tactic: rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | 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 : ℕ
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
⊢ A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * A
have inr : ∀ (h : A⁻¹ = 0), A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * A
Tactic: rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | 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 : ℕ
h_1 : -HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 ≠ -1
h : A⁻¹ = 0
⊢ A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) = A ^ (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * A
have inr : HPow.hPow (β := ℤ) A (-(↑(n + 1) : ℤ)) = HPow.hPow (β := ℤ) A (-(↑(n + 2) : ℤ)) * A
Tactic: change A ^ (-((n + 1 : ℕ) : ℤ)) = A ^ (-((n + 2 : ℕ) : ℤ)) * 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 : ℕ
h_1 : -HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 ≠ -1
h : A⁻¹ = 0
⊢ HPow.hPow (β := ℤ) A (-(↑(n + 1) : ℤ)) = HPow.hPow (β := ℤ) A (-(↑(n + 2) : ℤ)) * A
have inr : (A ^ (n + 1))⁻¹ = (A ^ (n + 2))⁻¹ * A
Tactic: simp_rw [zpow_neg_natCast, ← inv_pow', h, zero_pow <| Nat.succ_ne_zero _, zero_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
n : ℕ
h_1 : -HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 ≠ -1
h : A⁻¹ = 0
inr : (A ^ (n + 1))⁻¹ = (A ^ (n + 2))⁻¹ * A
⊢ HPow.hPow (β := ℤ) A (-(↑(n + 1) : ℤ)) = HPow.hPow (β := ℤ) A (-(↑(n + 2) : ℤ)) * A
have inr₁ : A⁻¹ ^ (n + 1) = A⁻¹ ^ (n + 2) * A
Tactic: simp_rw [zpow_neg_natCast, ← inv_pow', h, zero_pow <| Nat.succ_ne_zero _, zero_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
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
⊢ HPow.hPow (β := ℤ) A (-(↑(n + 1) : ℤ)) = HPow.hPow (β := ℤ) A (-(↑(n + 2) : ℤ)) * A
have inr₂ : HPow.hPow (α := M) 0 (n + 1) = HPow.hPow (α := M) 0 (n + 2) * A
Tactic: simp_rw [zpow_neg_natCast, ← inv_pow', h, zero_pow <| Nat.succ_ne_zero _, zero_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
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
⊢ HPow.hPow (β := ℤ) A (-(↑(n + 1) : ℤ)) = HPow.hPow (β := ℤ) A (-(↑(n + 2) : ℤ)) * A
have inr₃ : 0 = 0 * A
Tactic: simp_rw [zpow_neg_natCast, ← inv_pow', h, zero_pow <| Nat.succ_ne_zero _, zero_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 ^ 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
⊢ A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) A (↑m : ℤ)) (↑n : ℤ)
have rw₁ : A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = (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
⊢ A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) A (↑m : ℤ)) (↑n : ℤ)
have rw₂ : A ^ HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ) = A ^ (m * n)
Tactic: rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast, Int.natCast_mul]