-- Mathlib/Data/Int/Basic.lean
lemma inductionOn'_add_one (hz : b ≤ z) :
    (z + 1).inductionOn' b H0 Hs Hp = Hs 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 : b ≤ z
⊢ (z + 1).inductionOn' b H0 Hs Hp = Hs 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 : b ≤ z
⊢ HEq
    (match z + 1 - b with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hs 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 : b ≤ z
⊢ HEq
    (match z + 1 - b with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hs z hz (z.inductionOn' b H0 Hs Hp))

Tactic:
lift z - b to ℕ using Int.sub_nonneg.mpr hz with zb hzb

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 : b ≤ z
zb : ℕ
hzb : ↑zb = z - b
⊢ HEq
    (match z + 1 - b with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hs z hz (z.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 : b ≤ z
zb : ℕ
hzb : ↑zb = z - b
⊢ HEq
    (match ↑zb + 1 with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hs z hz (z.inductionOn' b H0 Hs Hp))

Tactic:
have : b + zb = z := 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 : b ≤ z
zb : ℕ
hzb : ↑zb = z - b
this : b + ↑zb = z
⊢ HEq
    (match ↑zb + 1 with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hs z hz (z.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 : b ≤ z
zb : ℕ
hzb : ↑zb = z - b
this : b + ↑zb = z
⊢ HEq
    (match ↑zb + 1 with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hs z hz (z.inductionOn' b H0 Hs Hp))

Tactic:
subst this

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

Tactic:
omega

Result:
no goals

Proof state:
case h.e'_4.h.e'_3
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)
zb : ℕ
hz : b ≤ b + ↑zb
hzb : ↑zb = b + ↑zb - b
⊢ (b + ↑zb).inductionOn' b H0 Hs Hp = inductionOn'.pos b H0 Hs zb

Tactic:
rw [Int.inductionOn', cast_eq_iff_heq, ← hzb]

Result:
no goals

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

Tactic:
convert cast_heq _ _

Result:
case h.e'_4.h.e'_3
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)
zb : ℕ
hz : b ≤ b + ↑zb
hzb : ↑zb = b + ↑zb - b
⊢ (b + ↑zb).inductionOn' b H0 Hs Hp = inductionOn'.pos b H0 Hs zb

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 : b ≤ z
zb : ℕ
hzb : ↑zb = z - b
⊢ HEq
    (match z + 1 - b with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hs z hz (z.inductionOn' b H0 Hs Hp))

Tactic:
rw [show z + 1 - b = zb + 1 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 : b ≤ z
zb : ℕ
hzb : ↑zb = z - b
⊢ HEq
    (match ↑zb + 1 with
    | ofNat n => inductionOn'.pos b H0 Hs n
    | -[n+1] => inductionOn'.neg b H0 Hp n)
    (Hs 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 : b ≤ z
zb : ℕ
hzb : ↑zb = z - b
⊢ b + ↑zb = z

Tactic:
omega

Result:
no goals