-- Mathlib/Data/Int/Init.lean
lemma inductionOn'_sub_one (hz : z ≤ b) :
    (z - 1).inductionOn' b H0 Hs Hp = Hp z hz (z.inductionOn' b H0 Hs Hp)

Proof state:
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
hz : z ≤ b
⊢ (z - 1).inductionOn' b H0 Hs Hp = Hp z hz (z.inductionOn' b H0 Hs Hp)

Tactic:
apply cast_eq_iff_heq.mpr

Result:
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
hz : z ≤ b
⊢ HEq
    (match z - 1 - b with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hp z hz (z.inductionOn' b H0 Hs Hp))

Proof state:
case intro.zero
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
hz : z ≤ b
hn : z - 1 - b = -[0+1]
⊢ HEq
    (match -[0+1] with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hp z hz (z.inductionOn' b H0 Hs Hp))

Tactic:
change _ = -1 at hn

Result:
case intro.zero
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
hz : z ≤ b
hn : z - 1 - b = -1
⊢ HEq
    (match -[0+1] with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hp z hz (z.inductionOn' b H0 Hs Hp))

Proof state:
case intro.succ.h.e_a
C : ℤ → Sort u_1
b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
n : ℕ
hz : b + -[n+1] ≤ b
hn : b + -[n+1] - 1 - b = -[n + 1+1]
⊢ (b + -[n+1]).inductionOn' b H0 Hs Hp = inductionOn'.neg b H0 Hp n

Tactic:
rw [Int.inductionOn', cast_eq_iff_heq, show b + -[n+1] - b = -[n+1] by omega]

Result:
no goals

Proof state:
case intro.succ
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
hz : z ≤ b
n : ℕ
hn : z - 1 - b = -[n + 1+1]
⊢ HEq
    (match -[n + 1+1] with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hp z hz (z.inductionOn' b H0 Hs Hp))

Tactic:
have : z = b + -[n+1] := by rw [Int.negSucc_eq] at hn ⊢; omega

Result:
case intro.succ
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
hz : z ≤ b
n : ℕ
hn : z - 1 - b = -[n + 1+1]
this : z = b + -[n+1]
⊢ HEq
    (match -[n + 1+1] with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hp z hz (z.inductionOn' b H0 Hs Hp))

Proof state:
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
hz : z ≤ b
⊢ HEq
    (match z - 1 - b with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hp z hz (z.inductionOn' b H0 Hs Hp))

Tactic:
obtain ⟨n, hn⟩ := Int.eq_negSucc_of_lt_zero (show z - 1 - b < 0 by omega)

Result:
case intro
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
hz : z ≤ b
n : ℕ
hn : z - 1 - b = -[n+1]
⊢ HEq
    (match z - 1 - b with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hp z hz (z.inductionOn' b H0 Hs Hp))

Proof state:
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
hz : z ≤ b
n : ℕ
hn : z - 1 - b = -[n + 1+1]
⊢ z = b + -[n+1]

Tactic:
rw [Int.negSucc_eq] at hn ⊢

Result:
C : ℤ → Sort u_1
z b : ℤ
H0 : C b
Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)
Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)
hz : z ≤ b
n : ℕ
hn : z - 1 - b = -(↑(n + 1) + 1)
⊢ z = b + -(↑n + 1)