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
ha : IsUnit A.det
m n : ℤ
⊢ A ^ (m + n) = A ^ m * A ^ n
have zero : A ^ (m + 0) = A ^ m * HPow.hPow (β := ℤ) A 0
Tactic: induction n with
  | zero => simp
  | succ n ihn => simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
  | pred n ihn => rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
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
ha : IsUnit A.det
m n : ℤ
zero : A ^ (m + 0) = A ^ m * HPow.hPow (β := ℤ) A 0
⊢ A ^ (m + n) = A ^ m * A ^ n
have succ : ∀ (n : ℕ) (ihn : A ^ (m + (↑n : ℤ)) = A ^ m * HPow.hPow (β := ℤ) A (↑n : ℤ)),
  A ^ (m + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = A ^ m * A ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
Tactic: induction n with
  | zero => simp
  | succ n ihn => simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
  | pred n ihn => rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
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
ha : IsUnit A.det
m n : ℤ
zero : A ^ (m + 0) = A ^ m * HPow.hPow (β := ℤ) A 0
succ :
  ∀ (n : ℕ) (ihn : A ^ (m + (↑n : ℤ)) = A ^ m * HPow.hPow (β := ℤ) A (↑n : ℤ)),
    A ^ (m + HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = A ^ m * A ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ A ^ (m + n) = A ^ m * A ^ n
have pred : ∀ (n : ℕ) (ihn : A ^ (m + -(↑n : ℤ)) = A ^ m * HPow.hPow (β := ℤ) A (-(↑n : ℤ))),
  A ^ (m + HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) = A ^ m * A ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
Tactic: induction n with
  | zero => simp
  | succ n ihn => simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
  | pred n ihn => rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
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
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
⊢ A ^ (m + n) = A ^ m * A ^ n
have inl : ∀ (h : A⁻¹ * A = 1), A * A⁻¹ = 1 → A ^ (m + n) = A ^ m * A ^ n
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
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
inl : ∀ (h : A⁻¹ * A = 1), A * A⁻¹ = 1 → A ^ (m + n) = A ^ m * A ^ n
⊢ A ^ (m + n) = A ^ m * A ^ n
have inr : ∀ (h : A⁻¹ = 0), A ^ (m + n) = A ^ m * A ^ n
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
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ = 0
⊢ A ^ (m + n) = A ^ m * A ^ n
have inr : ∀ (k : ℕ) (hm : LE.le (α := ℤ) (-(↑k : ℤ)) 0), A ^ (-(↑k : ℤ) + n) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * A ^ n
Tactic: obtain ⟨k, rfl⟩ := exists_eq_neg_ofNat hm
Cleared hypotheses: m, hm
-- 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 : ℤ
hn : n ≤ 0
h : A⁻¹ = 0
k : ℕ
hm : LE.le (α := ℤ) (-(↑k : ℤ)) 0
⊢ A ^ (-(↑k : ℤ) + n) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * A ^ n
have inr : ∀ (l : ℕ) (hn : LE.le (α := ℤ) (-(↑l : ℤ)) 0),
  A ^ HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) (-(↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
Tactic: obtain ⟨l, rfl⟩ := exists_eq_neg_ofNat hn
Cleared hypotheses: n, hn
-- 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 : A⁻¹ = 0
k : ℕ
hm : LE.le (α := ℤ) (-(↑k : ℤ)) 0
l : ℕ
hn : LE.le (α := ℤ) (-(↑l : ℤ)) 0
⊢ A ^ HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) (-(↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
have inr : A ^ (-HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
Tactic: simp_rw [← neg_add, ← Int.natCast_add, zpow_neg_natCast, ← inv_pow', h, pow_add]
-- 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 : A⁻¹ = 0
k : ℕ
hm : LE.le (α := ℤ) (-(↑k : ℤ)) 0
l : ℕ
hn : LE.le (α := ℤ) (-(↑l : ℤ)) 0
inr : A ^ (-HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
⊢ A ^ HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) (-(↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
have inr₁ : HPow.hPow (β := ℤ) A (-(↑(k + l) : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
Tactic: simp_rw [← neg_add, ← Int.natCast_add, zpow_neg_natCast, ← inv_pow', h, pow_add]
-- 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 : A⁻¹ = 0
k : ℕ
hm : LE.le (α := ℤ) (-(↑k : ℤ)) 0
l : ℕ
hn : LE.le (α := ℤ) (-(↑l : ℤ)) 0
inr : A ^ (-HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
inr₁ : HPow.hPow (β := ℤ) A (-(↑(k + l) : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
⊢ A ^ HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) (-(↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
have inr₂ : (A ^ (k + l))⁻¹ = (A ^ k)⁻¹ * (A ^ l)⁻¹
Tactic: simp_rw [← neg_add, ← Int.natCast_add, zpow_neg_natCast, ← inv_pow', h, pow_add]
-- 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 : A⁻¹ = 0
k : ℕ
hm : LE.le (α := ℤ) (-(↑k : ℤ)) 0
l : ℕ
hn : LE.le (α := ℤ) (-(↑l : ℤ)) 0
inr : A ^ (-HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
inr₁ : HPow.hPow (β := ℤ) A (-(↑(k + l) : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
inr₂ : (A ^ (k + l))⁻¹ = (A ^ k)⁻¹ * (A ^ l)⁻¹
⊢ A ^ HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) (-(↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
have inr₃ : A⁻¹ ^ (k + l) = A⁻¹ ^ k * A⁻¹ ^ l
Tactic: simp_rw [← neg_add, ← Int.natCast_add, zpow_neg_natCast, ← inv_pow', h, pow_add]
-- 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 : A⁻¹ = 0
k : ℕ
hm : LE.le (α := ℤ) (-(↑k : ℤ)) 0
l : ℕ
hn : LE.le (α := ℤ) (-(↑l : ℤ)) 0
inr : A ^ (-HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
inr₁ : HPow.hPow (β := ℤ) A (-(↑(k + l) : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
inr₂ : (A ^ (k + l))⁻¹ = (A ^ k)⁻¹ * (A ^ l)⁻¹
inr₃ : A⁻¹ ^ (k + l) = A⁻¹ ^ k * A⁻¹ ^ l
⊢ A ^ HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) (-(↑l : ℤ)) = HPow.hPow (β := ℤ) A (-(↑k : ℤ)) * HPow.hPow (β := ℤ) A (-(↑l : ℤ))
have inr₄ : HPow.hPow (α := M) 0 (k + l) = HPow.hPow (α := M) 0 k * HPow.hPow (α := M) 0 l
Tactic: simp_rw [← neg_add, ← Int.natCast_add, zpow_neg_natCast, ← inv_pow', h, pow_add]
-- 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 : ℤ
hm : 0 ≤ m
hn : 0 ≤ n
⊢ A ^ (m + n) = A ^ m * A ^ n
have obtain : ∀ (k : ℕ) (hm : LE.le (α := ℤ) 0 (↑k : ℤ)), A ^ ((↑k : ℤ) + n) = HPow.hPow (β := ℤ) A (↑k : ℤ) * A ^ n
Tactic: obtain ⟨k, rfl⟩ := eq_ofNat_of_zero_le hm
Cleared hypotheses: m, hm
-- 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 : ℤ
hn : 0 ≤ n
k : ℕ
hm : LE.le (α := ℤ) 0 (↑k : ℤ)
⊢ A ^ ((↑k : ℤ) + n) = HPow.hPow (β := ℤ) A (↑k : ℤ) * A ^ n
have obtain : ∀ (l : ℕ) (hn : LE.le (α := ℤ) 0 (↑l : ℤ)),
  A ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
Tactic: obtain ⟨l, rfl⟩ := eq_ofNat_of_zero_le hn
Cleared hypotheses: n, hn
-- 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
k : ℕ
hm : LE.le (α := ℤ) 0 (↑k : ℤ)
l : ℕ
hn : LE.le (α := ℤ) 0 (↑l : ℤ)
⊢ A ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
have rw : HPow.hPow (β := ℤ) A (↑(k + l) : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
Tactic: rw [← Int.natCast_add, zpow_natCast, zpow_natCast, zpow_natCast, pow_add]
-- 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
k : ℕ
hm : LE.le (α := ℤ) 0 (↑k : ℤ)
l : ℕ
hn : LE.le (α := ℤ) 0 (↑l : ℤ)
rw : HPow.hPow (β := ℤ) A (↑(k + l) : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
⊢ A ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
have rw₁ : A ^ (k + l) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
Tactic: rw [← Int.natCast_add, zpow_natCast, zpow_natCast, zpow_natCast, pow_add]
-- 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
k : ℕ
hm : LE.le (α := ℤ) 0 (↑k : ℤ)
l : ℕ
hn : LE.le (α := ℤ) 0 (↑l : ℤ)
rw : HPow.hPow (β := ℤ) A (↑(k + l) : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
rw₁ : A ^ (k + l) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
⊢ A ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
have rw₂ : A ^ (k + l) = A ^ k * HPow.hPow (β := ℤ) A (↑l : ℤ)
Tactic: rw [← Int.natCast_add, zpow_natCast, zpow_natCast, zpow_natCast, pow_add]
-- 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
k : ℕ
hm : LE.le (α := ℤ) 0 (↑k : ℤ)
l : ℕ
hn : LE.le (α := ℤ) 0 (↑l : ℤ)
rw : HPow.hPow (β := ℤ) A (↑(k + l) : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
rw₁ : A ^ (k + l) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
rw₂ : A ^ (k + l) = A ^ k * HPow.hPow (β := ℤ) A (↑l : ℤ)
⊢ A ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
have rw₃ : A ^ (k + l) = A ^ k * A ^ l
Tactic: rw [← Int.natCast_add, zpow_natCast, zpow_natCast, zpow_natCast, pow_add]
-- 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
k : ℕ
hm : LE.le (α := ℤ) 0 (↑k : ℤ)
l : ℕ
hn : LE.le (α := ℤ) 0 (↑l : ℤ)
rw : HPow.hPow (β := ℤ) A (↑(k + l) : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
rw₁ : A ^ (k + l) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
rw₂ : A ^ (k + l) = A ^ k * HPow.hPow (β := ℤ) A (↑l : ℤ)
rw₃ : A ^ (k + l) = A ^ k * A ^ l
⊢ A ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ) = HPow.hPow (β := ℤ) A (↑k : ℤ) * HPow.hPow (β := ℤ) A (↑l : ℤ)
have rw₄ : A ^ k * A ^ l = A ^ k * A ^ l
Tactic: rw [← Int.natCast_add, zpow_natCast, zpow_natCast, zpow_natCast, pow_add]
-- 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
i : ℤ
⊢ A ^ (1 + i) = A * A ^ i
have rw : HPow.hPow (β := ℤ) A 1 * A ^ i = A * A ^ i
Tactic: rw [zpow_add h, zpow_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
i : ℤ
rw : HPow.hPow (β := ℤ) A 1 * A ^ i = A * A ^ i
⊢ A ^ (1 + i) = A * A ^ i
have rw₁ : A * A ^ i = A * A ^ i
Tactic: rw [zpow_add h, zpow_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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (X ^ n.succ).det
have rw : IsUnit (X.det ^ n.succ)
Tactic: rw [det_pow]
-- 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
A X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
have hx' : IsUnit (X ^ n.succ).det
Tactic: have hx' : IsUnit (X ^ n.succ).det := by
      rw [det_pow]
      exact hx.pow n.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 X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
⊢ IsUnit (Y ^ n.succ).det
have rw : IsUnit (Y.det ^ n.succ)
Tactic: rw [det_pow]
-- 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
A X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (X ^ n.succ).det
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
have hy' : IsUnit (Y ^ n.succ).det
Tactic: have hy' : IsUnit (Y ^ n.succ).det := by
      rw [det_pow]
      exact hy.pow n.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 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
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
have rw : A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate = (↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A
Tactic: rw [zpow_negSucc, zpow_negSucc, nonsing_inv_apply _ hx', nonsing_inv_apply _ hy', SemiconjBy]
-- 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
⊢ A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate = (↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A
have refine : Eq (α := M) ((fun (x : M) ↦ Y ^ n.succ * x) (A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate))
  ((fun (x : M) ↦ Y ^ n.succ * x) ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A))
Tactic: refine (isRegular_of_isLeftRegular_det hy'.isRegular.left).left ?_
-- 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
⊢ Y ^ n.succ * (A * (↑hx'.unit⁻¹ : R) • (X ^ n.succ).adjugate) =
    Y ^ n.succ * ((↑hy'.unit⁻¹ : R) • (Y ^ n.succ).adjugate * A)
have rw : 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]
-- 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)
⊢ 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 * X ^ n.succ * (↑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]
-- 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)
⊢ 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 * (X ^ n.succ * (↑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]
-- 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)
⊢ 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) • (X ^ n.succ * (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]
-- 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)
⊢ 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 =
  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]
-- 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)
⊢ 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 =
  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]
-- 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
⊢ 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) • (Y ^ n.succ * (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]