-- 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:
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))

Tactic:
have : z = b := by omega

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

Tactic:
rw [inductionOn'_self]

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

Proof state:
case intro.succ
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]
⊢ HEq (Hp (b + -[n+1]) ⋯ (inductionOn'.neg b H0 Hp n)) (Hp (b + -[n+1]) hz ((b + -[n+1]).inductionOn' b H0 Hs Hp))

Tactic:
congr

Result:
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]
⊢ inductionOn'.neg b H0 Hp n = (b + -[n+1]).inductionOn' b H0 Hs Hp

Proof state:
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))

Tactic:
rw [hn]

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

Tactic:
exact heq_of_eq rfl

Result:
no goals

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 - b < 0

Tactic:
omega

Result:
no goals

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 = -1
this : z = b
⊢ 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:
subst this

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

Tactic:
omega

Result:
no goals

Proof state:
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] - b = -[n+1]

Tactic:
omega

Result:
no goals

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:
omega

Result:
no goals

Proof state:
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 -[n+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:
obtain _|n := n

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 = -[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))

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))

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]
⊢ inductionOn'.neg b H0 Hp n = (b + -[n+1]).inductionOn' b H0 Hs Hp

Tactic:
symm

Result:
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

Proof state:
case intro.succ
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]
⊢ HEq
    (match -[n + 1+1] with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hp (b + -[n+1]) hz ((b + -[n+1]).inductionOn' b H0 Hs Hp))

Tactic:
refine (cast_heq _ _).trans ?_

Result:
case intro.succ
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]
⊢ HEq (Hp (b + -[n+1]) ⋯ (inductionOn'.neg b H0 Hp n)) (Hp (b + -[n+1]) hz ((b + -[n+1]).inductionOn' b H0 Hs Hp))

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]
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))

Tactic:
subst this

Result:
case intro.succ
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]
⊢ HEq
    (match -[n + 1+1] with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hp (b + -[n+1]) hz ((b + -[n+1]).inductionOn' b H0 Hs Hp))