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

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
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
induction' n with n IH generalizing m
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

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
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
cases' m with m m
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

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
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
rcases nonsing_inv_cancel_or_zero A with (⟨h, h'⟩ | h)
no goals
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
simp
no goals
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
simp
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)
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
simp only [Nat.succ_eq_add_one]
no goals
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)
calc
  A⁻¹ ^ (m + 1) ⬝ A ^ (n + 1) = A⁻¹ ^ m ⬝ (A⁻¹ ⬝ A) ⬝ A ^ n := by
   simp only [pow_succ' A⁻¹, pow_succ A, mul_eq_mul, 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⁻¹, mul_eq_mul, Matrix.mul_assoc]
no goals
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
simp only [pow_succ' A⁻¹, pow_succ A, mul_eq_mul, Matrix.mul_assoc]
no goals
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
simp only [h, Matrix.mul_one, Matrix.one_mul, IH m]
no goals
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
simp only [h', Matrix.mul_one, Matrix.one_mul]
no goals
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)
simp only [pow_succ' A, pow_succ A⁻¹, mul_eq_mul, Matrix.mul_assoc]
no goals
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
simp [h]