Theorem: IMOSL.Extra.IntLinearSolver (IMOSLLean4/Extra/IntLinearSolver.lean)

State before:
G : Type u_1
g : G
inst✝ : AddGroup G
f : ℤ → G
h : ∀ (n : ℤ), f (n + 1) = g + f n
n : ℤ
⊢ f 0 = 0 • g + f 0
Tactic:
rw [zero_zsmul, zero_add]
State after:
no goals

State before:
G : Type u_1
g : G
inst✝ : AddGroup G
f : ℤ → G
h : ∀ (n : ℤ), f (n + 1) = g + f n
n k : ℤ
x✝ : 0 ≤ k
h1 : f k = k • g + f 0
⊢ f (k + 1) = (k + 1) • g + f 0
Tactic:
rw [h, h1, ← add_assoc, add_comm, one_add_zsmul]
State after:
no goals

State before:
G : Type u_1
g : G
inst✝ : AddGroup G
f : ℤ → G
h : ∀ (n : ℤ), f (n + 1) = g + f n
n k : ℤ
x✝ : k ≤ 0
h1 : f k = k • g + f 0
⊢ f (k - 1) = (k - 1) • g + f 0
Tactic:
rwa [← add_right_inj g, ← h, sub_add_cancel,
  ← add_assoc, ← one_add_zsmul, add_sub_cancel]
State after:
no goals