[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
⊢ Monoid M
[PROOFSTEP]
infer_instance
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
src✝ : Monoid M :=
  let_fun this := inferInstance;
  this
⊢ Inv M
[PROOFSTEP]
infer_instance
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A⁻¹ ^ n = (A ^ n)⁻¹
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A⁻¹ ^ Nat.zero = (A ^ Nat.zero)⁻¹
[PROOFSTEP]
simp
[GOAL]
case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
ih : A⁻¹ ^ n = (A ^ n)⁻¹
⊢ A⁻¹ ^ Nat.succ n = (A ^ Nat.succ n)⁻¹
[PROOFSTEP]
rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
ha : IsUnit (det A)
h : n ≤ m
⊢ A ^ (m - n) = A ^ m * (A ^ n)⁻¹
[PROOFSTEP]
rw [← tsub_add_cancel_of_le h, pow_add, Matrix.mul_assoc, mul_nonsing_inv, tsub_add_cancel_of_le h, Matrix.mul_one]
[GOAL]
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
ha : IsUnit (det A)
h : n ≤ m
⊢ IsUnit (det (A ^ n))
[PROOFSTEP]
simpa using ha.pow n
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
⊢ A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
[PROOFSTEP]
induction' n with n IH generalizing m
[GOAL]
case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ m : ℕ
⊢ A⁻¹ ^ m * A ^ Nat.zero = A ^ Nat.zero * A⁻¹ ^ m
[PROOFSTEP]
simp
[GOAL]
case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
⊢ A⁻¹ ^ m * A ^ Nat.succ n = A ^ Nat.succ n * A⁻¹ ^ m
[PROOFSTEP]
cases' m with m m
[GOAL]
case succ.zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
⊢ A⁻¹ ^ Nat.zero * A ^ Nat.succ n = A ^ Nat.succ n * A⁻¹ ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ.succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
⊢ A⁻¹ ^ Nat.succ m * A ^ Nat.succ n = A ^ Nat.succ n * A⁻¹ ^ Nat.succ m
[PROOFSTEP]
rcases nonsing_inv_cancel_or_zero A with (⟨h, h'⟩ | h)
[GOAL]
case succ.succ.inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A⁻¹ ^ Nat.succ m * A ^ Nat.succ n = A ^ Nat.succ n * A⁻¹ ^ Nat.succ m
[PROOFSTEP]
simp only [Nat.succ_eq_add_one]
[GOAL]
case succ.succ.inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A ^ (n + 1) * A⁻¹ ^ (m + 1)
[PROOFSTEP]
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, Matrix.one_mul, IH m]
  _ = A ^ n * (A * A⁻¹) * A⁻¹ ^ m := by simp only [h', Matrix.mul_one, Matrix.one_mul]
  _ = A ^ (n + 1) * A⁻¹ ^ (m + 1) := by simp only [pow_succ' A, pow_succ A⁻¹, Matrix.mul_assoc]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A⁻¹ ^ (m + 1) * A ^ (n + 1) = A⁻¹ ^ m * (A⁻¹ * A) * A ^ n
[PROOFSTEP]
simp only [pow_succ' A⁻¹, pow_succ A, Matrix.mul_assoc]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A⁻¹ ^ m * (A⁻¹ * A) * A ^ n = A ^ n * A⁻¹ ^ m
[PROOFSTEP]
simp only [h, Matrix.mul_one, Matrix.one_mul, IH m]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A ^ n * A⁻¹ ^ m = A ^ n * (A * A⁻¹) * A⁻¹ ^ m
[PROOFSTEP]
simp only [h', Matrix.mul_one, Matrix.one_mul]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ * A = 1
h' : A * A⁻¹ = 1
⊢ A ^ n * (A * A⁻¹) * A⁻¹ ^ m = A ^ (n + 1) * A⁻¹ ^ (m + 1)
[PROOFSTEP]
simp only [pow_succ' A, pow_succ A⁻¹, Matrix.mul_assoc]
[GOAL]
case succ.succ.inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m✝ n : ℕ
IH : ∀ (m : ℕ), A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m
m : ℕ
h : A⁻¹ = 0
⊢ A⁻¹ ^ Nat.succ m * A ^ Nat.succ n = A ^ Nat.succ n * A⁻¹ ^ Nat.succ m
[PROOFSTEP]
simp [h]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
⊢ 1 ^ ↑n = 1
[PROOFSTEP]
rw [zpow_ofNat, one_pow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
⊢ 1 ^ -[n+1] = 1
[PROOFSTEP]
rw [zpow_negSucc, one_pow, inv_one]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : ↑n ≠ 0
⊢ 0 ^ ↑n = 0
[PROOFSTEP]
rw [zpow_ofNat, zero_pow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : ↑n ≠ 0
⊢ 0 < n
[PROOFSTEP]
refine' lt_of_le_of_ne n.zero_le (Ne.symm _)
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0
[PROOFSTEP]
simpa using h
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
x✝ : -[n+1] ≠ 0
⊢ 0 ^ -[n+1] = 0
[PROOFSTEP]
simp [zero_pow n.zero_lt_succ]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
h : n = 0
⊢ 0 ^ n = 1
[PROOFSTEP]
rw [h, zpow_zero]
[GOAL]
case neg
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0
[PROOFSTEP]
rw [zero_zpow _ h]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A⁻¹ ^ ↑n = (A ^ ↑n)⁻¹
[PROOFSTEP]
rw [zpow_ofNat, zpow_ofNat, inv_pow']
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A⁻¹ ^ -[n+1] = (A ^ -[n+1])⁻¹
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, inv_pow']
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A ^ (-1) = A⁻¹
[PROOFSTEP]
convert DivInvMonoid.zpow_neg' 0 A
[GOAL]
case h.e'_3.h.e'_3
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A = DivInvMonoid.zpow (↑(Nat.succ 0)) A
[PROOFSTEP]
simp only [zpow_one, Int.ofNat_zero, Int.ofNat_succ, zpow_eq_pow, zero_add]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A ^ (-↑n) = (A ^ n)⁻¹
[PROOFSTEP]
cases n
[GOAL]
case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A ^ (-↑Nat.zero) = (A ^ Nat.zero)⁻¹
[PROOFSTEP]
simp
[GOAL]
case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n✝ : ℕ
⊢ A ^ (-↑(Nat.succ n✝)) = (A ^ Nat.succ n✝)⁻¹
[PROOFSTEP]
exact DivInvMonoid.zpow_neg' _ _
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℤ
⊢ IsUnit (det (A ^ n))
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ IsUnit (det (A ^ ofNat n))
[PROOFSTEP]
simpa using h.pow n
[GOAL]
case negSucc
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ IsUnit (det (A ^ -[n+1]))
[PROOFSTEP]
simpa using h.pow n.succ
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℤ
⊢ IsUnit (det (A ^ z)) ↔ IsUnit (det A) ∨ z = 0
[PROOFSTEP]
induction' z using Int.induction_on with z _ z _
[GOAL]
case hz
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ IsUnit (det (A ^ 0)) ↔ IsUnit (det A) ∨ 0 = 0
[PROOFSTEP]
simp
[GOAL]
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ ↑z)) ↔ IsUnit (det A) ∨ ↑z = 0
⊢ IsUnit (det (A ^ (↑z + 1))) ↔ IsUnit (det A) ∨ ↑z + 1 = 0
[PROOFSTEP]
rw [← Int.ofNat_succ, zpow_ofNat, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero, Int.ofNat_inj]
[GOAL]
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ ↑z)) ↔ IsUnit (det A) ∨ ↑z = 0
⊢ IsUnit (det A) ↔ IsUnit (det A) ∨ Nat.succ z = 0
[PROOFSTEP]
simp
[GOAL]
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ (-↑z))) ↔ IsUnit (det A) ∨ -↑z = 0
⊢ IsUnit (det (A ^ (-↑z - 1))) ↔ IsUnit (det A) ∨ -↑z - 1 = 0
[PROOFSTEP]
rw [← neg_add', ← Int.ofNat_succ, zpow_neg_coe_nat, isUnit_nonsing_inv_det_iff, det_pow, isUnit_pow_succ_iff,
  neg_eq_zero, ← Int.ofNat_zero, Int.ofNat_inj]
[GOAL]
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
z : ℕ
a✝ : IsUnit (det (A ^ (-↑z))) ↔ IsUnit (det A) ∨ -↑z = 0
⊢ IsUnit (det A) ↔ IsUnit (det A) ∨ Nat.succ z = 0
[PROOFSTEP]
simp
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ A ^ (- -[n+1]) = (A ^ -[n+1])⁻¹
[PROOFSTEP]
rw [zpow_negSucc, neg_negSucc, zpow_ofNat, nonsing_inv_nonsing_inv]
[GOAL]
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ IsUnit (det (A ^ (n + 1)))
[PROOFSTEP]
rw [det_pow]
[GOAL]
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ IsUnit (det A ^ (n + 1))
[PROOFSTEP]
exact h.pow _
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℤ
⊢ A⁻¹ ^ n = A ^ (-n)
[PROOFSTEP]
rw [zpow_neg h, inv_zpow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ A ^ (↑n + 1) = A ^ ↑n * A
[PROOFSTEP]
simp only [← Nat.cast_succ, pow_succ', zpow_ofNat]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ A ^ (-(↑n + 1) + 1) = (A ^ n)⁻¹
[PROOFSTEP]
rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_ofNat]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ (A ^ n)⁻¹ = (A * A ^ n)⁻¹ * A
[PROOFSTEP]
rw [mul_inv_rev, Matrix.mul_assoc, nonsing_inv_mul _ h, Matrix.mul_one]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℕ
⊢ (A * A ^ n)⁻¹ * A = A ^ (-(↑n + 1)) * A
[PROOFSTEP]
rw [zpow_neg h, ← Int.ofNat_succ, zpow_ofNat, pow_succ]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℤ
⊢ A ^ (n - 1) = A ^ (n - 1) * A * A⁻¹
[PROOFSTEP]
rw [mul_assoc, mul_nonsing_inv _ h, mul_one]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
n : ℤ
⊢ A ^ (n - 1) * A * A⁻¹ = A ^ n * A⁻¹
[PROOFSTEP]
rw [← zpow_add_one h, sub_add_cancel]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit (det A)
m n : ℤ
⊢ A ^ (m + n) = A ^ m * A ^ n
[PROOFSTEP]
induction n using Int.induction_on with
| hz => simp
| hp n ihn => simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
| hn n ihn => rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit (det A)
m n : ℤ
⊢ A ^ (m + n) = A ^ m * A ^ n
[PROOFSTEP]
induction n using Int.induction_on with
| hz => simp
| hp n ihn => simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
| hn n ihn => rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
[GOAL]
case hz
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit (det A)
m : ℤ
⊢ A ^ (m + 0) = A ^ m * A ^ 0
[PROOFSTEP]

| hz => simp
[GOAL]
case hz
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit (det A)
m : ℤ
⊢ A ^ (m + 0) = A ^ m * A ^ 0
[PROOFSTEP]
simp
[GOAL]
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit (det A)
m : ℤ
n : ℕ
ihn : A ^ (m + ↑n) = A ^ m * A ^ ↑n
⊢ A ^ (m + (↑n + 1)) = A ^ m * A ^ (↑n + 1)
[PROOFSTEP]

| hp n ihn => simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
[GOAL]
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit (det A)
m : ℤ
n : ℕ
ihn : A ^ (m + ↑n) = A ^ m * A ^ ↑n
⊢ A ^ (m + (↑n + 1)) = A ^ m * A ^ (↑n + 1)
[PROOFSTEP]
simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
[GOAL]
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit (det A)
m : ℤ
n : ℕ
ihn : A ^ (m + -↑n) = A ^ m * A ^ (-↑n)
⊢ A ^ (m + (-↑n - 1)) = A ^ m * A ^ (-↑n - 1)
[PROOFSTEP]

| hn n ihn => rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
[GOAL]
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit (det A)
m : ℤ
n : ℕ
ihn : A ^ (m + -↑n) = A ^ m * A ^ (-↑n)
⊢ A ^ (m + (-↑n - 1)) = A ^ m * A ^ (-↑n - 1)
[PROOFSTEP]
rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
⊢ A ^ (m + n) = A ^ m * A ^ n
[PROOFSTEP]
rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | h)
[GOAL]
case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ * A = 1
right✝ : A * A⁻¹ = 1
⊢ A ^ (m + n) = A ^ m * A ^ n
[PROOFSTEP]
exact zpow_add (isUnit_det_of_left_inverse h) m n
[GOAL]
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ = 0
⊢ A ^ (m + n) = A ^ m * A ^ n
[PROOFSTEP]
obtain ⟨k, rfl⟩ := exists_eq_neg_ofNat hm
[GOAL]
case inr.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
hn : n ≤ 0
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
⊢ A ^ (-↑k + n) = A ^ (-↑k) * A ^ n
[PROOFSTEP]
obtain ⟨l, rfl⟩ := exists_eq_neg_ofNat hn
[GOAL]
case inr.intro.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
l : ℕ
hn : -↑l ≤ 0
⊢ A ^ (-↑k + -↑l) = A ^ (-↑k) * A ^ (-↑l)
[PROOFSTEP]
simp_rw [← neg_add, ← Int.ofNat_add, zpow_neg_coe_nat, ← inv_pow', h, pow_add]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : 0 ≤ m
hn : 0 ≤ n
⊢ A ^ (m + n) = A ^ m * A ^ n
[PROOFSTEP]
obtain ⟨k, rfl⟩ := eq_ofNat_of_zero_le hm
[GOAL]
case intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
hn : 0 ≤ n
k : ℕ
hm : 0 ≤ ↑k
⊢ A ^ (↑k + n) = A ^ ↑k * A ^ n
[PROOFSTEP]
obtain ⟨l, rfl⟩ := eq_ofNat_of_zero_le hn
[GOAL]
case intro.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
k : ℕ
hm : 0 ≤ ↑k
l : ℕ
hn : 0 ≤ ↑l
⊢ A ^ (↑k + ↑l) = A ^ ↑k * A ^ ↑l
[PROOFSTEP]
rw [← Int.ofNat_add, zpow_ofNat, zpow_ofNat, zpow_ofNat, pow_add]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
i : ℤ
⊢ A ^ (1 + i) = A * A ^ i
[PROOFSTEP]
rw [zpow_add h, zpow_one]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
⊢ SemiconjBy A (X ^ ↑n) (Y ^ ↑n)
[PROOFSTEP]
simp [h.pow_right n]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
[PROOFSTEP]
have hx' : IsUnit (X ^ n.succ).det := by
  rw [det_pow]
  exact hx.pow n.succ
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (det (X ^ Nat.succ n))
[PROOFSTEP]
rw [det_pow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (det X ^ Nat.succ n)
[PROOFSTEP]
exact hx.pow n.succ
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
[PROOFSTEP]
have hy' : IsUnit (Y ^ n.succ).det := by
  rw [det_pow]
  exact hy.pow n.succ
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
⊢ IsUnit (det (Y ^ Nat.succ n))
[PROOFSTEP]
rw [det_pow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
⊢ IsUnit (det Y ^ Nat.succ n)
[PROOFSTEP]
exact hy.pow n.succ
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, nonsing_inv_apply _ hx', nonsing_inv_apply _ hy', SemiconjBy]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ A * ↑(IsUnit.unit hx')⁻¹ • adjugate (X ^ Nat.succ n) = ↑(IsUnit.unit hy')⁻¹ • adjugate (Y ^ Nat.succ n) * A
[PROOFSTEP]
refine' (isRegular_of_isLeftRegular_det hy'.isRegular.left).left _
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ (fun x => Y ^ Nat.succ n * x) (A * ↑(IsUnit.unit hx')⁻¹ • adjugate (X ^ Nat.succ n)) =
    (fun x => Y ^ Nat.succ n * x) (↑(IsUnit.unit hy')⁻¹ • adjugate (Y ^ Nat.succ n) * A)
[PROOFSTEP]
dsimp only
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ Y ^ Nat.succ n * (A * ↑(IsUnit.unit hx')⁻¹ • adjugate (X ^ Nat.succ n)) =
    Y ^ Nat.succ n * (↑(IsUnit.unit hy')⁻¹ • adjugate (Y ^ Nat.succ n) * A)
[PROOFSTEP]
rw [← mul_assoc, ← (h.pow_right n.succ).eq, mul_assoc, mul_smul, mul_adjugate, ← Matrix.mul_assoc,
  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]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
⊢ Commute A (B ^ m)
[PROOFSTEP]
rcases nonsing_inv_cancel_or_zero B with (⟨hB, _⟩ | hB)
[GOAL]
case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ * B = 1
right✝ : B * B⁻¹ = 1
⊢ Commute A (B ^ m)
[PROOFSTEP]
refine' SemiconjBy.zpow_right _ _ h _
[GOAL]
case inl.intro.refine'_1
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ * B = 1
right✝ : B * B⁻¹ = 1
⊢ IsUnit (det B)
[PROOFSTEP]
exact isUnit_det_of_left_inverse hB
[GOAL]
case inl.intro.refine'_2
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ * B = 1
right✝ : B * B⁻¹ = 1
⊢ IsUnit (det B)
[PROOFSTEP]
exact isUnit_det_of_left_inverse hB
[GOAL]
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ = 0
⊢ Commute A (B ^ m)
[PROOFSTEP]
cases m
[GOAL]
case inr.ofNat
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ ofNat a✝)
[PROOFSTEP]
simpa using h.pow_right _
[GOAL]
case inr.negSucc
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ -[a✝+1])
[PROOFSTEP]
simp [← inv_pow', hB]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
⊢ A ^ bit0 n = A ^ n * A ^ n
[PROOFSTEP]
cases' le_total 0 n with nonneg nonpos
[GOAL]
case inl
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
nonneg : 0 ≤ n
⊢ A ^ bit0 n = A ^ n * A ^ n
[PROOFSTEP]
exact zpow_add_of_nonneg nonneg nonneg
[GOAL]
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
nonpos : n ≤ 0
⊢ A ^ bit0 n = A ^ n * A ^ n
[PROOFSTEP]
exact zpow_add_of_nonpos nonpos nonpos
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : ↑n ≠ -1
⊢ A ^ (↑n + 1) = A ^ ↑n * A
[PROOFSTEP]
simp only [pow_succ', ← Nat.cast_succ, zpow_ofNat]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
⊢ A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A
[PROOFSTEP]
rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | h)
[GOAL]
case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ * A = 1
right✝ : A * A⁻¹ = 1
⊢ A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A
[PROOFSTEP]
apply zpow_add_one (isUnit_det_of_left_inverse h)
[GOAL]
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ A ^ (-(↑n + 2) + 1) = A ^ (-(↑n + 2)) * A
[PROOFSTEP]
show A ^ (-((n + 1 : ℕ) : ℤ)) = A ^ (-((n + 2 : ℕ) : ℤ)) * A
[GOAL]
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
x✝ : -(↑n + 2) ≠ -1
h : A⁻¹ = 0
⊢ A ^ (-↑(n + 1)) = A ^ (-↑(n + 2)) * A
[PROOFSTEP]
simp_rw [zpow_neg_coe_nat, ← inv_pow', h, zero_pow Nat.succ_pos', zero_mul]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
⊢ A ^ bit1 n = A ^ n * A ^ n * A
[PROOFSTEP]
rw [bit1, zpow_add_one_of_ne_neg_one, zpow_bit0]
[GOAL]
case a
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
⊢ bit0 n ≠ -1
[PROOFSTEP]
intro h
[GOAL]
case a
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
h : bit0 n = -1
⊢ False
[PROOFSTEP]
simpa using congr_arg bodd h
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ A ^ (↑m * ↑n) = (A ^ ↑m) ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat, zpow_ofNat, ← pow_mul, ← zpow_ofNat, Int.ofNat_mul]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ A ^ (↑m * -[n+1]) = (A ^ ↑m) ^ -[n+1]
[PROOFSTEP]
rw [zpow_ofNat, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_coe_nat]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ A ^ (-[m+1] * ↑n) = (A ^ -[m+1]) ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_coe_nat, inv_pow']
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ A ^ (-[m+1] * -[n+1]) = (A ^ -[m+1]) ^ -[n+1]
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, negSucc_mul_negSucc, ← Int.ofNat_mul, zpow_ofNat, inv_pow', ← pow_mul,
  nonsing_inv_nonsing_inv]
[GOAL]
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ IsUnit (det (A ^ ((m + 1) * (n + 1))))
[PROOFSTEP]
rw [det_pow]
[GOAL]
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℕ
⊢ IsUnit (det A ^ ((m + 1) * (n + 1)))
[PROOFSTEP]
exact h.pow _
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit (det A)
m n : ℤ
⊢ A ^ (m * n) = (A ^ n) ^ m
[PROOFSTEP]
rw [mul_comm, zpow_mul _ h]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
u : Mˣ
n : ℕ
⊢ ↑(u ^ ↑n) = ↑u ^ ↑n
[PROOFSTEP]
rw [_root_.zpow_coe_nat, zpow_ofNat, Units.val_pow_eq_pow_val]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
u : Mˣ
k : ℕ
⊢ ↑(u ^ -[k+1]) = ↑u ^ -[k+1]
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, ← inv_pow, u⁻¹.val_pow_eq_pow_val, ← inv_pow', coe_units_inv]
[GOAL]
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
⊢ A ^ z ≠ 0
[PROOFSTEP]
have := ha.det_zpow z
[GOAL]
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
this : IsUnit (det (A ^ z))
⊢ A ^ z ≠ 0
[PROOFSTEP]
contrapose! this
[GOAL]
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit (det (A ^ z))
[PROOFSTEP]
rw [this, det_zero ‹_›]
[GOAL]
n' : Type u_1
inst✝⁴ : DecidableEq n'
inst✝³ : Fintype n'
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Nonempty n'
inst✝ : Nontrivial R
A : M
ha : IsUnit (det A)
z : ℤ
this : A ^ z = 0
⊢ ¬IsUnit 0
[PROOFSTEP]
exact not_isUnit_zero
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit (det A)
z1 z2 : ℤ
⊢ A ^ (z1 - z2) = A ^ z1 / A ^ z2
[PROOFSTEP]
rw [sub_eq_add_neg, zpow_add ha, zpow_neg ha, div_eq_mul_inv]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
n : ℕ
⊢ (A * B) ^ ↑n = A ^ ↑n * B ^ ↑n
[PROOFSTEP]
simp [h.mul_pow n]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
n : ℕ
⊢ (A * B) ^ -[n+1] = A ^ -[n+1] * B ^ -[n+1]
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, zpow_negSucc, ← mul_inv_rev, h.mul_pow n.succ, (h.pow_pow _ _).eq]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
⊢ A ^ bit1 n = (A * A) ^ n * A
[PROOFSTEP]
rw [zpow_bit1, Commute.mul_zpow (Commute.refl A)]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
A : M
h : IsUnit (det A)
⊢ A ^ (-n) * A ^ n = 1
[PROOFSTEP]
rw [zpow_neg h, nonsing_inv_mul _ (h.det_zpow _)]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (1 / A) ^ n = 1 / A ^ n
[PROOFSTEP]
simp only [one_div, inv_pow']
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
⊢ (1 / A) ^ n = 1 / A ^ n
[PROOFSTEP]
simp only [one_div, inv_zpow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (A ^ ↑n)ᵀ = Aᵀ ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat, zpow_ofNat, transpose_pow]
[GOAL]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (A ^ -[n+1])ᵀ = Aᵀ ^ -[n+1]
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, transpose_nonsing_inv, transpose_pow]
[GOAL]
n' : Type u_1
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ (A ^ ↑n)ᴴ = Aᴴ ^ ↑n
[PROOFSTEP]
rw [zpow_ofNat, zpow_ofNat, conjTranspose_pow]
[GOAL]
n' : Type u_1
inst✝³ : DecidableEq n'
inst✝² : Fintype n'
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
A : M
n : ℕ
⊢ (A ^ -[n+1])ᴴ = Aᴴ ^ -[n+1]
[PROOFSTEP]
rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow]


[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ natDegree (det (X • Matrix.map A ↑C + Matrix.map B ↑C)) ≤ Fintype.card n
[PROOFSTEP]
rw [det_apply]
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ natDegree (∑ σ : Equiv.Perm n, ↑sign σ • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑σ i) i) ≤ Fintype.card n
[PROOFSTEP]
refine' (natDegree_sum_le _ _).trans _
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ Finset.fold max 0 (natDegree ∘ fun σ => ↑sign σ • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑σ i) i)
      Finset.univ ≤
    Fintype.card n
[PROOFSTEP]
refine' Multiset.max_nat_le_of_forall_le _ _ _
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ (x : ℕ),
    x ∈
        Multiset.map (natDegree ∘ fun σ => ↑sign σ • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑σ i) i)
          Finset.univ.val →
      x ≤ Fintype.card n
[PROOFSTEP]
simp only [forall_apply_eq_imp_iff', true_and_iff, Function.comp_apply, Multiset.map_map, Multiset.mem_map, exists_imp,
  Finset.mem_univ_val]
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ (a : Equiv.Perm n), natDegree (↑sign a • ∏ x : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑a x) x) ≤ Fintype.card n
[PROOFSTEP]
intro g
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ natDegree (↑sign g • ∏ x : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) ≤ Fintype.card n
[PROOFSTEP]
calc
  natDegree (sign g • ∏ i : n, (X • A.map C + B.map C) (g i) i) ≤
      natDegree (∏ i : n, (X • A.map C + B.map C) (g i) i) :=
    by
    cases' Int.units_eq_one_or (sign g) with sg sg
    · rw [sg, one_smul]
    · rw [sg, Units.neg_smul, one_smul, natDegree_neg]
  _ ≤ ∑ i : n, natDegree (((X : α[X]) • A.map C + B.map C) (g i) i) :=
    (natDegree_prod_le (Finset.univ : Finset n) fun i : n => (X • A.map C + B.map C) (g i) i)
  _ ≤ Finset.univ.card • 1 := (Finset.sum_le_card_nsmul _ _ 1 fun (i : n) _ => ?_)
  _ ≤ Fintype.card n := by simp [mul_one, Algebra.id.smul_eq_mul, Finset.card_univ]
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ natDegree (↑sign g • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) ≤
    natDegree (∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i)
[PROOFSTEP]
cases' Int.units_eq_one_or (sign g) with sg sg
[GOAL]
case inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
sg : ↑sign g = 1
⊢ natDegree (↑sign g • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) ≤
    natDegree (∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i)
[PROOFSTEP]
rw [sg, one_smul]
[GOAL]
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
sg : ↑sign g = -1
⊢ natDegree (↑sign g • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) ≤
    natDegree (∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i)
[PROOFSTEP]
rw [sg, Units.neg_smul, one_smul, natDegree_neg]
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ Finset.card Finset.univ • 1 ≤ Fintype.card n
[PROOFSTEP]
simp [mul_one, Algebra.id.smul_eq_mul, Finset.card_univ]
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
i : n
x✝ : i ∈ Finset.univ
⊢ natDegree ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) ≤ 1
[PROOFSTEP]
calc
  natDegree (((X : α[X]) • A.map C + B.map C) (g i) i) = natDegree ((X : α[X]) * C (A (g i) i) + C (B (g i) i)) := by
    simp
  _ ≤ max (natDegree ((X : α[X]) * C (A (g i) i))) (natDegree (C (B (g i) i))) := (natDegree_add_le _ _)
  _ = natDegree ((X : α[X]) * C (A (g i) i)) := (max_eq_left ((natDegree_C _).le.trans (zero_le _)))
  _ ≤ natDegree (X : α[X]) := (natDegree_mul_C_le _ _)
  _ ≤ 1 := natDegree_X_le
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
i : n
x✝ : i ∈ Finset.univ
⊢ natDegree ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) = natDegree (X * ↑C (A (↑g i) i) + ↑C (B (↑g i) i))
[PROOFSTEP]
simp
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ coeff (det (X • Matrix.map A ↑C + Matrix.map B ↑C)) 0 = det B
[PROOFSTEP]
rw [det_apply, finset_sum_coeff, det_apply]
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∑ b : Equiv.Perm n, coeff (↑sign b • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑b i) i) 0 =
    ∑ σ : Equiv.Perm n, ↑sign σ • ∏ i : n, B (↑σ i) i
[PROOFSTEP]
refine' Finset.sum_congr rfl _
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ (x : Equiv.Perm n),
    x ∈ Finset.univ →
      coeff (↑sign x • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑x i) i) 0 = ↑sign x • ∏ i : n, B (↑x i) i
[PROOFSTEP]
rintro g -
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ coeff (↑sign g • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) 0 = ↑sign g • ∏ i : n, B (↑g i) i
[PROOFSTEP]
convert coeff_smul (R := α) (sign g) _ 0
[GOAL]
case h.e'_3.h.e'_6
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ i : n, B (↑g i) i = coeff (∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) 0
[PROOFSTEP]
rw [coeff_zero_prod]
[GOAL]
case h.e'_3.h.e'_6
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ i : n, B (↑g i) i = ∏ i : n, coeff ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) 0
[PROOFSTEP]
refine' Finset.prod_congr rfl _
[GOAL]
case h.e'_3.h.e'_6
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∀ (x : n), x ∈ Finset.univ → B (↑g x) x = coeff ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) 0
[PROOFSTEP]
simp
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ coeff (det (X • Matrix.map A ↑C + Matrix.map B ↑C)) (Fintype.card n) = det A
[PROOFSTEP]
rw [det_apply, det_apply, finset_sum_coeff]
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∑ b : Equiv.Perm n, coeff (↑sign b • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑b i) i) (Fintype.card n) =
    ∑ σ : Equiv.Perm n, ↑sign σ • ∏ i : n, A (↑σ i) i
[PROOFSTEP]
refine' Finset.sum_congr rfl _
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ (x : Equiv.Perm n),
    x ∈ Finset.univ →
      coeff (↑sign x • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑x i) i) (Fintype.card n) =
        ↑sign x • ∏ i : n, A (↑x i) i
[PROOFSTEP]
simp only [Algebra.id.smul_eq_mul, Finset.mem_univ, RingHom.mapMatrix_apply, forall_true_left, map_apply, Pi.smul_apply]
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ (x : Equiv.Perm n),
    coeff (↑sign x • ∏ x_1 : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑x x_1) x_1) (Fintype.card n) =
      ↑sign x • ∏ x_1 : n, A (↑x x_1) x_1
[PROOFSTEP]
intro g
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ coeff (↑sign g • ∏ x : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) (Fintype.card n) =
    ↑sign g • ∏ x : n, A (↑g x) x
[PROOFSTEP]
convert coeff_smul (R := α) (sign g) _ _
[GOAL]
case h.e'_3.h.e'_6
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ x : n, A (↑g x) x = coeff (∏ x : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) (Fintype.card n)
[PROOFSTEP]
rw [← mul_one (Fintype.card n)]
[GOAL]
case h.e'_3.h.e'_6
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ x : n, A (↑g x) x = coeff (∏ x : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) (Fintype.card n * 1)
[PROOFSTEP]
convert (coeff_prod_of_natDegree_le (R := α) _ _ _ _).symm
[GOAL]
case h.e'_2.a
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ A (↑g x✝) x✝ = coeff ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x✝) x✝) 1
[PROOFSTEP]
simp [coeff_C]
[GOAL]
case h.e'_3.h.e'_6.convert_5
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∀ (p : n), p ∈ Finset.univ → natDegree ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g p) p) ≤ 1
[PROOFSTEP]
rintro p -
[GOAL]
case h.e'_3.h.e'_6.convert_5
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
p : n
⊢ natDegree ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g p) p) ≤ 1
[PROOFSTEP]
refine' (natDegree_add_le _ _).trans _
[GOAL]
case h.e'_3.h.e'_6.convert_5
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
p : n
⊢ max (natDegree ((X • Matrix.map A ↑C) (↑g p) p)) (natDegree (Matrix.map B (↑C) (↑g p) p)) ≤ 1
[PROOFSTEP]
simpa [Pi.smul_apply, map_apply, Algebra.id.smul_eq_mul, X_mul_C, natDegree_C, max_eq_left, zero_le'] using
  (natDegree_C_mul_le _ _).trans (natDegree_X_le (R := α))
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ leadingCoeff (det (X • 1 + Matrix.map A ↑C)) = 1
[PROOFSTEP]
cases subsingleton_or_nontrivial α
[GOAL]
case inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Subsingleton α
⊢ leadingCoeff (det (X • 1 + Matrix.map A ↑C)) = 1
[PROOFSTEP]
simp
[GOAL]
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ leadingCoeff (det (X • 1 + Matrix.map A ↑C)) = 1
[PROOFSTEP]
rw [← @det_one n, ← coeff_det_X_add_C_card _ A, leadingCoeff]
[GOAL]
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
simp only [Matrix.map_one, C_eq_zero, RingHom.map_one]
[GOAL]
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
cases' (natDegree_det_X_add_C_le 1 A).eq_or_lt with h h
[GOAL]
case inr.inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) = Fintype.card n
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
simp only [RingHom.map_one, Matrix.map_one, C_eq_zero] at h
[GOAL]
case inr.inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • 1 + Matrix.map A ↑C)) = Fintype.card n
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
rw [h]
[GOAL]
case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) < Fintype.card n
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
have H := coeff_eq_zero_of_natDegree_lt h
[GOAL]
case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) < Fintype.card n
H : coeff (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) (Fintype.card n) = 0
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
rw [coeff_det_X_add_C_card] at H
[GOAL]
case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) < Fintype.card n
H : det 1 = 0
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
simp at H