-- Mathlib/Order/SuccPred/Limit.lean
theorem isSuccPrelimitRecOn_succ_of_not_isMax (hb : ¬ IsMax b) :
    isSuccPrelimitRecOn (succ b) hs hl = hs b hb

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccPrelimit a → C a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ succ (Classical.choose ⋯) = succ b
⊢ isSuccPrelimitRecOn (succ b) hs hl = hs b hb

Tactic:
rw [isSuccPrelimitRecOn, dif_neg hb', cast_eq_iff_heq]

Result:
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccPrelimit a → C a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ succ (Classical.choose ⋯) = succ b
⊢ HEq (hs (Classical.choose ⋯) ⋯) (hs b hb)

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccPrelimit a → C a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (succ b)
⊢ isSuccPrelimitRecOn (succ b) hs hl = hs b hb

Tactic:
have H := Classical.choose_spec (not_isSuccPrelimit_iff.1 hb')

Result:
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccPrelimit a → C a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ succ (Classical.choose ⋯) = succ b
⊢ isSuccPrelimitRecOn (succ b) hs hl = hs b hb

Proof state:
case e_1
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccPrelimit a → C a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ succ (Classical.choose ⋯) = succ b
⊢ Classical.choose ⋯ = b

case e_2
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccPrelimit a → C a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ succ (Classical.choose ⋯) = succ b
⊢ HEq ⋯ hb

Tactic:
exacts [(succ_eq_succ_iff_of_not_isMax H.1 hb).1 H.2, proof_irrel_heq _ _]

Result:
no goals

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccPrelimit a → C a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ succ (Classical.choose ⋯) = succ b
⊢ HEq (hs (Classical.choose ⋯) ⋯) (hs b hb)

Tactic:
congr

Result:
case e_1
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccPrelimit a → C a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ succ (Classical.choose ⋯) = succ b
⊢ Classical.choose ⋯ = b

case e_2
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccPrelimit a → C a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ succ (Classical.choose ⋯) = succ b
⊢ HEq ⋯ hb

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccPrelimit a → C a
hb : ¬IsMax b
⊢ isSuccPrelimitRecOn (succ b) hs hl = hs b hb

Tactic:
have hb' := not_isSuccPrelimit_succ_of_not_isMax hb

Result:
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccPrelimit a → C a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (succ b)
⊢ isSuccPrelimitRecOn (succ b) hs hl = hs b hb