case hz

⊢ ↑(T ^ 0) = ↑of ![![1, 0], ![0, 1]]

case hp
n : ℕ
h : ↑(T ^ ↑n) = ↑of ![![1, ↑n], ![0, 1]]
⊢ ↑(T ^ (↑n + 1)) = ↑of ![![1, ↑n + 1], ![0, 1]]

case hn
n : ℕ
h : ↑(T ^ (-↑n)) = ↑of ![![1, -↑n], ![0, 1]]
⊢ ↑(T ^ (-↑n - 1)) = ↑of ![![1, -↑n - 1], ![0, 1]]
n : ℤ
⊢ ↑(T ^ n) = ↑of ![![1, n], ![0, 1]]
induction' n using Int.induction_on with n h n h
no goals
case hz

⊢ ↑(T ^ 0) = ↑of ![![1, 0], ![0, 1]]
rw [zpow_zero, coe_one, Matrix.one_fin_two]
case hp
n : ℕ
h : ↑(T ^ ↑n) = ↑of ![![1, ↑n], ![0, 1]]
⊢ ↑of ![![1 * 1 + ↑n * 0, 1 * 1 + ↑n * 1], ![0 * 1 + 1 * 0, 0 * 1 + 1 * 1]] = ↑of ![![1, ↑n + 1], ![0, 1]]
case hp
n : ℕ
h : ↑(T ^ ↑n) = ↑of ![![1, ↑n], ![0, 1]]
⊢ ↑(T ^ (↑n + 1)) = ↑of ![![1, ↑n + 1], ![0, 1]]
simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]
no goals
case hp
n : ℕ
h : ↑(T ^ ↑n) = ↑of ![![1, ↑n], ![0, 1]]
⊢ ↑of ![![1 * 1 + ↑n * 0, 1 * 1 + ↑n * 1], ![0 * 1 + 1 * 0, 0 * 1 + 1 * 1]] = ↑of ![![1, ↑n + 1], ![0, 1]]
ring_nf
case hn
n : ℕ
h : ↑(T ^ (-↑n)) = ↑of ![![1, -↑n], ![0, 1]]
⊢ ↑of ![![1 * 1 + -↑n * 0, 1 * -1 + -↑n * 1], ![0 * 1 + 1 * 0, 0 * -1 + 1 * 1]] = ↑of ![![1, -↑n - 1], ![0, 1]]
case hn
n : ℕ
h : ↑(T ^ (-↑n)) = ↑of ![![1, -↑n], ![0, 1]]
⊢ ↑(T ^ (-↑n - 1)) = ↑of ![![1, -↑n - 1], ![0, 1]]
simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
no goals
case hn
n : ℕ
h : ↑(T ^ (-↑n)) = ↑of ![![1, -↑n], ![0, 1]]
⊢ ↑of ![![1 * 1 + -↑n * 0, 1 * -1 + -↑n * 1], ![0 * 1 + 1 * 0, 0 * -1 + 1 * 1]] = ↑of ![![1, -↑n - 1], ![0, 1]]
ring_nf