awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : PartialOrder α
inst_1 : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : IsSuccLimit b
rw :
  (isSuccPrelimitRecOn b (motive := fun (x : α) ↦ motive x) succ fun (a : α) (ha : IsSuccPrelimit a) ↦
      if h : IsMin a then isMin a h else isSuccLimit a ⋯) =
    isSuccLimit b hb
rw₁ : (if h : IsMin b then isMin b h else isSuccLimit b ⋯) = isSuccLimit b hb
rw₂ rw₃ : isSuccLimit b ⋯ = isSuccLimit b hb
⊢ isSuccLimitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = isSuccLimit b hb

Tactic:
rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit,
    dif_neg hb.not_isMin]

Premises used: Order.isSuccPrelimitRecOn_of_isSuccPrelimit, dif_neg, Order.IsSuccLimit.not_isMin, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : ¬IsMax b
rw :
  (isSuccPrelimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) succ fun (a : α) (ha : IsSuccPrelimit a) ↦
      if h : IsMin a then isMin a h else isSuccLimit a ⋯) =
    succ b hb
rw₁ : succ b hb = succ b hb
hb₁ : ¬IsMax b
rw₂ : succ b hb = succ b hb
hb₂ : ¬IsMax b
⊢ isSuccLimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = succ b hb

Tactic:
rw [isSuccLimitRecOn, isSuccPrelimitRecOn_succ_of_not_isMax]

Premises used: Order.isSuccPrelimitRecOn_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
inst_2 : NoMaxOrder α
b : α
⊢ isSuccLimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = succ b ⋯

Tactic:
isSuccLimitRecOn_succ_of_not_isMax isMin succ isSuccLimit _

Premises used: Order.isSuccLimitRecOn_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : IsMin b
rw :
  (isSuccPrelimitRecOn b (motive := fun (x : α) ↦ motive x) succ fun (a : α) (ha : IsSuccPrelimit a) ↦
      if h : IsMin a then isMin a h else isSuccLimit a ⋯) =
    isMin b hb
rw₁ : (if h : IsMin b then isMin b h else isSuccLimit b ⋯) = isMin b hb
rw₂ rw₃ : isMin b hb = isMin b hb
⊢ isSuccLimitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = isMin b hb

Tactic:
rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]

Premises used: IsMin.isSuccPrelimit, Order.isSuccPrelimitRecOn_of_isSuccPrelimit, dif_pos
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccPrelimit b
rw :
  (isSuccPrelimit b hb fun (y : α) (x : y < b) ↦
      WellFounded.fix (C := fun (x : α) ↦ motive x) (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯
        (fun (a : α) (IH : (y : α) → y < a → motive y) ↦
          if h : IsSuccPrelimit a then isSuccPrelimit a h IH
          else
            cast ⋯
              (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) ⋯) ⋯
                (IH (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) ⋯) ⋯)))
        y) =
    isSuccPrelimit b hb fun (x : α) (x_1 : x < b) ↦
      prelimitRecOn x (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit
⊢ prelimitRecOn b (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit =
    isSuccPrelimit b hb fun (x : α) (x_1 : x < b) ↦
      prelimitRecOn x (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit

Tactic:
rw [prelimitRecOn, WellFounded.fix_eq, dif_pos hb]

Premises used: dif_pos, WellFounded.fix_eq
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccPrelimit b
⊢ (isSuccPrelimit b hb fun (y : α) (x : y < b) ↦
      WellFounded.fix (C := fun (x : α) ↦ motive x) (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯
        (fun (a : α) (IH : (y : α) → y < a → motive y) ↦
          if h : IsSuccPrelimit a then isSuccPrelimit a h IH
          else
            cast ⋯
              (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) ⋯) ⋯
                (IH (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) ⋯) ⋯)))
        y) =
    isSuccPrelimit b hb fun (x : α) (x_1 : x < b) ↦
      prelimitRecOn x (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit

Tactic:
rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
⊢ ¬IsSuccPrelimit (Order.succ b)

Tactic:
have h := mt IsSuccPrelimit.isMax hb
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
⊢ ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ∧
    Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) = Order.succ b

Tactic:
have H := Classical.choose_spec (not_isSuccPrelimit_iff_succ_eq.1 h)
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H :
  ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ∧
    Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) = Order.succ b
rw :
  cast ⋯
      (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ⋯
        ((fun (y : α) (x : y < Order.succ b) ↦
            (WellFounded.fix (C := fun (x : α) ↦ motive x) (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯
                (fun (a : α) (IH : (y : α) → y < a → motive y) ↦
                  if h : IsSuccPrelimit a then isSuccPrelimit a h IH
                  else
                    cast ⋯
                      (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) ⋯) ⋯
                        (IH (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) ⋯) ⋯)))
                y :
              motive y))
          (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ⋯)) =
    succ b hb (prelimitRecOn b (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit)
⊢ prelimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit =
    succ b hb (prelimitRecOn b (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit)

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

Premises used: dif_neg, WellFounded.fix_eq
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h_1 : ¬IsSuccPrelimit (Order.succ b)
H :
  ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ∧
    Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) = Order.succ b
a c : α
ha : ¬IsMax a
hc : ¬IsMax c
x : (a : α) → motive a
h : a = c
subst : ∀ {hc : ¬IsMax a}, cast ⋯ (succ a ha (x a)) = succ a hc (x a)
⊢ cast ⋯ (succ a ha (x a)) = succ c hc (x c)

Tactic:
subst h
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H :
  ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ∧
    Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) = Order.succ b
a : α
ha : ¬IsMax a
x : (a : α) → motive a
hc : ¬IsMax a
⊢ cast ⋯ (succ a ha (x a)) = succ a hc (x a)

Tactic:
rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H :
  ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ∧
    Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) = Order.succ b
⊢ ∀ {a c : α} {ha : ¬IsMax a} {hc : ¬IsMax c} {x : (a : α) → motive a} (h : a = c),
    cast ⋯ (succ a ha (x a)) = succ c hc (x c)

Tactic:
have {a c : α} {ha hc} {x : ∀ a, motive a} (h : a = c) :
    cast (congr_arg (motive ∘ Order.succ) h) (succ a ha (x a)) = succ c hc (x c) := by subst h; rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H :
  ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ∧
    Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) = Order.succ b
this :
  ∀ {a c : α} {ha : ¬IsMax a} {hc : ¬IsMax c} {x : (a : α) → motive a} (h : a = c),
    cast ⋯ (succ a ha (x a)) = succ c hc (x c)
⊢ cast ⋯
      (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ⋯
        ((fun (y : α) (x : y < Order.succ b) ↦
            (WellFounded.fix (C := fun (x : α) ↦ motive x) (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯
                (fun (a : α) (IH : (y : α) → y < a → motive y) ↦
                  if h : IsSuccPrelimit a then isSuccPrelimit a h IH
                  else
                    cast ⋯
                      (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) ⋯) ⋯
                        (IH (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) ⋯) ⋯)))
                y :
              motive y))
          (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ⋯)) =
    succ b hb (prelimitRecOn b (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit)

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

Premises used: And.right, And.left, Iff.mp, Order.succ_eq_succ_iff_of_not_isMax, SuccOrder.prelimitRecOn
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H :
  ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ∧
    Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) = Order.succ b
this :
  ∀ {a c : α} {ha : ¬IsMax a} {hc : ¬IsMax c} {x : (a : α) → motive a} (h : a = c),
    cast ⋯ (succ a ha (x a)) = succ c hc (x c)
⊢ cast ⋯
      (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ⋯
        ((fun (y : α) (x : y < Order.succ b) ↦
            (WellFounded.fix (C := fun (x : α) ↦ motive x) (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯
                (fun (a : α) (IH : (y : α) → y < a → motive y) ↦
                  if h : IsSuccPrelimit a then isSuccPrelimit a h IH
                  else
                    cast ⋯
                      (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) ⋯) ⋯
                        (IH (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) ⋯) ⋯)))
                y :
              motive y))
          (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ⋯)) =
    succ b hb (prelimitRecOn b (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit)

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

Premises used: And.right, And.left, Iff.mp, Order.succ_eq_succ_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
inst_3 : NoMaxOrder α
b : α
⊢ prelimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit =
    succ b ⋯ (prelimitRecOn b (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit)

Tactic:
prelimitRecOn_succ_of_not_isMax _ _ _

Premises used: SuccOrder.prelimitRecOn_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsMin b
rw :
  (prelimitRecOn b (motive := fun (x : α) ↦ motive x) succ
      fun (a : α) (ha : IsSuccPrelimit a) (IH : (b : α) → b < a → motive b) ↦
      if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    isMin b hb
rw₁ :
  (if h : IsMin b then isMin b h
    else
      isSuccLimit b ⋯ fun (x : α) (x_1 : x < b) ↦
        prelimitRecOn x (motive := fun (x : α) ↦ motive x) succ
          fun (a : α) (ha : IsSuccPrelimit a) (IH : (b : α) → b < a → motive b) ↦
          if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    isMin b hb
rw₂ rw₃ : isMin b hb = isMin b hb
⊢ limitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = isMin b hb

Tactic:
rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]

Premises used: IsMin.isSuccPrelimit, SuccOrder.prelimitRecOn_of_isSuccPrelimit, dif_pos
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccLimit b
rw :
  (isSuccLimit b ⋯ fun (x : α) (x_1 : x < b) ↦
      prelimitRecOn x (motive := fun (x : α) ↦ motive x) succ
        fun (a : α) (ha : IsSuccPrelimit a) (IH : (b : α) → b < a → motive b) ↦
        if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    isSuccLimit b hb fun (x : α) (x_1 : x < b) ↦ limitRecOn x (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit
⊢ limitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit =
    isSuccLimit b hb fun (x : α) (x_1 : x < b) ↦ limitRecOn x (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit

Tactic:
rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_neg hb.not_isMin]

Premises used: SuccOrder.prelimitRecOn_of_isSuccPrelimit, dif_neg, Order.IsSuccLimit.not_isMin, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccLimit b
⊢ (isSuccLimit b ⋯ fun (x : α) (x_1 : x < b) ↦
      prelimitRecOn x (motive := fun (x : α) ↦ motive x) succ
        fun (a : α) (ha : IsSuccPrelimit a) (IH : (b : α) → b < a → motive b) ↦
        if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    isSuccLimit b hb fun (x : α) (x_1 : x < b) ↦ limitRecOn x (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit

Tactic:
rfl
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
rw :
  succ b hb
      (prelimitRecOn b (motive := fun (x : α) ↦ motive x) succ
        fun (a : α) (ha : IsSuccPrelimit a) (IH : (b : α) → b < a → motive b) ↦
        if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    succ b hb (limitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit)
hb₁ : ¬IsMax b
⊢ limitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit =
    succ b hb (limitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit)

Tactic:
rw [limitRecOn, prelimitRecOn_succ_of_not_isMax]

Premises used: SuccOrder.prelimitRecOn_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
inst_3 : NoMaxOrder α
b : α
⊢ limitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit =
    succ b ⋯ (limitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit)

Tactic:
limitRecOn_succ_of_not_isMax isMin succ isSuccLimit _

Premises used: SuccOrder.limitRecOn_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
⊢ ∃ (n : ℕ), succ^[n] i = j

Tactic:
have h_exists := exists_succ_iterate_of_le hij
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), succ^[n] i = j
⊢ ∃ (n : ℕ), succ^[n] i = j ∧ ∀ m < n, succ^[m] i ≠ j

Tactic:
⟨Nat.find h_exists, Nat.find_spec h_exists, fun m hmn ↦ Nat.find_min h_exists hmn⟩

Premises used: Nat.find_min, And.intro, Nat.find, Exists.intro, Nat.find_spec
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), succ^[n] i = j
obtain : ∀ (n : ℕ) (hn_eq : succ^[n] i = j) (hn_lt_ne : ∀ m < n, succ^[m] i ≠ j), ∃ (n : ℕ), pred^[n] j = i
⊢ ∃ (n : ℕ), pred^[n] j = i

Tactic:
obtain ⟨n, hn_eq, hn_lt_ne⟩ : ∃ n, succ^[n] i = j ∧ ∀ m < n, succ^[m] i ≠ j :=
      ⟨Nat.find h_exists, Nat.find_spec h_exists, fun m hmn ↦ Nat.find_min h_exists hmn⟩
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), succ^[n] i = j
n : ℕ
hn_eq : succ^[n] i = j
hn_lt_ne : ∀ m < n, succ^[m] i ≠ j
⊢ ∃ (n : ℕ), pred^[n] j = i

Tactic:
⟨n, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), succ^[n] i = j
n : ℕ
hn_eq : succ^[n] i = j
hn_lt_ne : ∀ m < n, succ^[m] i ≠ j
refine : pred^[n] j = i
⊢ ∃ (n : ℕ), pred^[n] j = i

Tactic:
refine ⟨n, ?_⟩
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), succ^[n] i = j
n : ℕ
hn_eq : succ^[n] i = j
hn_lt_ne : ∀ m < n, succ^[m] i ≠ j
rw : pred^[n] (succ^[n] i) = i
⊢ pred^[n] j = i

Tactic:
rw [← hn_eq]
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), succ^[n] i = j
hn_eq : succ^[0] i = j
hn_lt_ne : ∀ m < 0, succ^[m] i ≠ j
⊢ pred^[0] (succ^[0] i) = i

Tactic:
simp only [Function.iterate_zero, id]

Premises used: Function.iterate_zero, id
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), Order.succ^[n] i = j
n : ℕ
hn_eq : Order.succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, Order.succ^[m] i ≠ j
succ : ¬IsMax (Order.succ^[n + 1 - 1] i)
⊢ pred^[n + 1] (Order.succ^[n + 1] i) = i

Tactic:
rw [pred_succ_iterate_of_not_isMax]

Premises used: Order.pred_succ_iterate_of_not_isMax
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), Order.succ^[n] i = j
n : ℕ
hn_eq : Order.succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, Order.succ^[m] i ≠ j
succ : ¬IsMax (Order.succ^[n] i)
⊢ ¬IsMax (Order.succ^[n + 1 - 1] i)

Tactic:
rw [Nat.succ_sub_succ_eq_sub, tsub_zero]

Premises used: tsub_zero, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), Order.succ^[n] i = j
n : ℕ
hn_eq : Order.succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, Order.succ^[m] i ≠ j
succ : Order.succ^[n] i < Order.succ^[n.succ] i
⊢ ¬IsMax (Order.succ^[n] i)

Tactic:
suffices succ^[n] i < succ^[n.succ] i from not_isMax_of_lt this
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ succ^[n] i < succ^[n.succ] i

Tactic:
lt_of_le_of_ne ?_ ?_

Premises used: lt_of_le_of_ne
-- Module: Mathlib.Order.SuccPred.LinearLocallyFinite
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ (n : ℕ), Order.succ^[n] i = j
n : ℕ
hn_eq : Order.succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, Order.succ^[m] i ≠ j
succ : Order.succ^[n] i ≤ Order.succ^[n.succ] i
succ₁ : Order.succ^[n] i ≠ Order.succ^[n.succ] i
⊢ Order.succ^[n] i < Order.succ^[n.succ] i

Tactic:
refine lt_of_le_of_ne ?_ ?_

Premises used: lt_of_le_of_ne