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

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
⊢ prelimitRecOn (Order.succ b) hs hl = hs b hb (prelimitRecOn b hs hl)

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

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

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ cast ⋯
      (hs (Classical.choose ⋯) ⋯
        ((fun y x =>
            ⋯.fix
              (fun a IH =>
                if h : IsSuccPrelimit a then hl a h IH
                else cast ⋯ (hs (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
              y)
          (Classical.choose ⋯) ⋯)) =
    hs b hb (prelimitRecOn b hs hl)

Tactic:
have {a c : α} {ha hc} {x : ∀ a, C a} (h : a = c) :
  cast (congr_arg (C ∘ succ) h) (hs a ha (x a)) = hs c hc (x c) := by subst h; rfl

Result:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
this :
  ∀ {a c : α} {ha : ¬IsMax a} {hc : ¬IsMax c} {x : (a : α) → C a} (h : a = c), cast ⋯ (hs a ha (x a)) = hs c hc (x c)
⊢ cast ⋯
      (hs (Classical.choose ⋯) ⋯
        ((fun y x =>
            ⋯.fix
              (fun a IH =>
                if h : IsSuccPrelimit a then hl a h IH
                else cast ⋯ (hs (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
              y)
          (Classical.choose ⋯) ⋯)) =
    hs b hb (prelimitRecOn b hs hl)

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
h✝ : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
a c : α
ha : ¬IsMax a
hc : ¬IsMax c
x : (a : α) → C a
h : a = c
⊢ cast ⋯ (hs a ha (x a)) = hs c hc (x c)

Tactic:
subst h

Result:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
a : α
ha : ¬IsMax a
x : (a : α) → C a
hc : ¬IsMax a
⊢ cast ⋯ (hs a ha (x a)) = hs a hc (x a)

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

Tactic:
rw [prelimitRecOn, WellFounded.fix_eq, dif_neg h]

Result:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ cast ⋯
      (hs (Classical.choose ⋯) ⋯
        ((fun y x =>
            ⋯.fix
              (fun a IH =>
                if h : IsSuccPrelimit a then hl a h IH
                else cast ⋯ (hs (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
              y)
          (Classical.choose ⋯) ⋯)) =
    hs b hb (prelimitRecOn b hs hl)

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

Tactic:
have h := not_isSuccPrelimit_succ_of_not_isMax hb

Result:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
⊢ prelimitRecOn (Order.succ b) hs hl = hs b hb (prelimitRecOn b hs hl)

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
a : α
ha : ¬IsMax a
x : (a : α) → C a
hc : ¬IsMax a
⊢ cast ⋯ (hs a ha (x a)) = hs a hc (x a)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)
hl : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → C b) → C a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
this :
  ∀ {a c : α} {ha : ¬IsMax a} {hc : ¬IsMax c} {x : (a : α) → C a} (h : a = c), cast ⋯ (hs a ha (x a)) = hs c hc (x c)
⊢ cast ⋯
      (hs (Classical.choose ⋯) ⋯
        ((fun y x =>
            ⋯.fix
              (fun a IH =>
                if h : IsSuccPrelimit a then hl a h IH
                else cast ⋯ (hs (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
              y)
          (Classical.choose ⋯) ⋯)) =
    hs b hb (prelimitRecOn b hs hl)

Tactic:
exact this <| (succ_eq_succ_iff_of_not_isMax H.1 hb).1 H.2

Result:
no goals