awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
ha : IsSuccPrelimit a
⊢ IsLUB (Iio a) a
have refine : ∀ (b : α) (hb : b ∈ upperBounds (Iio a)) (c : α) (hc : c < a), c < b
Tactic: refine ⟨fun _ ↦ le_of_lt, fun b hb ↦ le_of_forall_lt fun c hc ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
ha : IsSuccPrelimit a
b : α
hb : b ∈ upperBounds (Iio a)
c : α
hc : c < a
⊢ c < b
have obtain : ∀ (d : α) (hd : d < a) (hd' : c < d), c < b
Tactic: obtain ⟨d, hd, hd'⟩ := ha.lt_iff_exists_lt.1 hc
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
⊢ IsLUB (Iio a) a ↔ IsSuccPrelimit a
have refine : ∀ (ha : IsLUB (Iio a) a) (b : α) (hb : b ⋖ a), False
Tactic: refine ⟨fun ha b hb ↦ ?_, IsSuccPrelimit.isLUB_Iio⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
ha : IsLUB (Iio a) a
b : α
hb : b ⋖ a
⊢ False
have ha₁ : IsLUB (Iic b) a
Tactic: rw [hb.Iio_eq] at ha
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
b : α
ha : IsLUB (Iic b) a
hb : b ⋖ a
⊢ False
have ha₁ : IsLUB (Iic b) b
Tactic: obtain rfl := isLUB_Iic.unique ha
Cleared hypotheses: a, ha, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
b : α
ha : IsLUB (Iic b) a
hb : b ⋖ a
ha₁ : IsLUB (Iic b) b
⊢ False
have hb₁ : b ⋖ b
Tactic: obtain rfl := isLUB_Iic.unique ha
Cleared hypotheses: a, ha, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
⊢ isSuccPrelimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit = succ b hb
have hb' : ¬IsSuccPrelimit (Order.succ b)
Tactic: have hb' := mt IsSuccPrelimit.isMax hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
⊢ isSuccPrelimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit = succ b hb
have H : ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) sorry) ∧
  Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) sorry) = Order.succ b
Tactic: have H := Classical.choose_spec (not_isSuccPrelimit_iff_succ_eq.1 hb')
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬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
⊢ isSuccPrelimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit = succ b hb
have rw : HEq (α := motive (Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) sorry)))
  (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) sorry) sorry) (succ b hb)
Tactic: rw [isSuccPrelimitRecOn, dif_neg hb', cast_eq_iff_heq]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
b : α
motive : α → Sort u_2
inst : LinearOrder α
inst_1 : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬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
⊢ HEq (α := motive (Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯)))
    (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) ⋯) ⋯) (succ b hb)
have e'_1 : Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) sorry = b
Tactic: congr!
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ isSuccLimitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = isSuccLimit b hb
have 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 sorry) =
  isSuccLimit b hb
Tactic: rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit,
    dif_neg hb.not_isMin]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ isSuccLimitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = isSuccLimit b hb
have rw₁ : (if h : IsMin b then isMin b h else isSuccLimit b sorry) = isSuccLimit b hb
Tactic: rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit,
    dif_neg hb.not_isMin]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ isSuccLimitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = isSuccLimit b hb
have rw₂ : isSuccLimit b sorry = isSuccLimit b hb
Tactic: rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit,
    dif_neg hb.not_isMin]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ isSuccLimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = succ b hb
have 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 sorry) =
  succ b hb
Tactic: rw [isSuccLimitRecOn, isSuccPrelimitRecOn_succ_of_not_isMax]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ isSuccLimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = succ b hb
have rw₁ : succ b hb = succ b hb
Tactic: rw [isSuccLimitRecOn, isSuccPrelimitRecOn_succ_of_not_isMax]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ isSuccLimitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = isMin b hb
have 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 sorry) =
  isMin b hb
Tactic: rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ isSuccLimitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = isMin b hb
have rw₁ : (if h : IsMin b then isMin b h else isSuccLimit b sorry) = isMin b hb
Tactic: rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ isSuccLimitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = isMin b hb
have rw₂ : isMin b hb = isMin b hb
Tactic: rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ 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
have rw : (isSuccPrelimit b hb fun (y : α) (x : y < b) ↦
    WellFounded.fix (C := fun (x : α) ↦ motive x) (r := fun (x1 x2 : α) ↦ x1 < x2) sorry
      (fun (a : α) (IH : (y : α) → y < a → motive y) ↦
        if h : IsSuccPrelimit a then isSuccPrelimit a h IH
        else
          cast sorry
            (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) sorry) sorry
              (IH (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) sorry) sorry)))
      y) =
  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]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
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
⊢ prelimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit =
    succ b hb (prelimitRecOn b (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit)
have h : ¬IsSuccPrelimit (Order.succ b)
Tactic: have h := mt IsSuccPrelimit.isMax hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
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)
⊢ prelimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit =
    succ b hb (prelimitRecOn b (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit)
have H : ¬IsMax (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) sorry) ∧
  Order.succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) sorry) = Order.succ b
Tactic: have H := Classical.choose_spec (not_isSuccPrelimit_iff_succ_eq.1 h)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ prelimitRecOn (Order.succ b) (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit =
    succ b hb (prelimitRecOn b (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit)
have rw : cast sorry
    (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) sorry) sorry
      ((fun (y : α) (x : y < Order.succ b) ↦
          (WellFounded.fix (C := fun (x : α) ↦ motive x) (r := fun (x1 x2 : α) ↦ x1 < x2) sorry
              (fun (a : α) (IH : (y : α) → y < a → motive y) ↦
                if h : IsSuccPrelimit a then isSuccPrelimit a h IH
                else
                  cast sorry
                    (succ (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) sorry) sorry
                      (IH (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = a) sorry) sorry)))
              y :
            motive y))
        (Classical.choose (p := fun (x : α) ↦ ¬IsMax x ∧ Order.succ x = Order.succ b) sorry) sorry)) =
  succ b hb (prelimitRecOn b (motive := fun (x : α) ↦ motive x) succ isSuccPrelimit)
Tactic: rw [prelimitRecOn, WellFounded.fix_eq, dif_neg h]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ cast ⋯ (succ a ha (x a)) = succ c hc (x c)
have subst : ∀ {hc : ¬IsMax a}, cast sorry (succ a ha (x a)) = succ a hc (x a)
Tactic: subst h
Cleared hypotheses: c, hc, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
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
⊢ 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)
have this : ∀ {a c : α} {ha : ¬IsMax a} {hc : ¬IsMax c} {x : (a : α) → motive a} (h : a = c),
  cast sorry (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
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ limitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = isMin b hb
have 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 sorry IH) =
  isMin b hb
Tactic: rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ limitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = isMin b hb
have rw₁ : (if h : IsMin b then isMin b h
  else
    isSuccLimit b sorry 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 sorry IH) =
  isMin b hb
Tactic: rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ limitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit = isMin b hb
have rw₂ : isMin b hb = isMin b hb
Tactic: rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_pos hb]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ 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
have rw : (isSuccLimit b sorry 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 sorry IH) =
  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]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
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
⊢ 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)
have 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 sorry IH) =
  succ b hb (limitRecOn b (motive := fun (x : α) ↦ motive x) isMin succ isSuccLimit)
Tactic: rw [limitRecOn, prelimitRecOn_succ_of_not_isMax]
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : SuccOrder ι
inst_2 : PredOrder ι
inst_3 : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
⊢ ∃ (n : ℕ), pred^[n] j = i
have h_exists : ∃ (n : ℕ), succ^[n] i = j
Tactic: have h_exists := exists_succ_iterate_of_le hij
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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 : ℕ), pred^[n] j = i
have obtain : ∀ (n : ℕ) (hn_eq : succ^[n] i = j) (hn_lt_ne : ∀ m < n, succ^[m] i ≠ j), ∃ (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⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
have refine : pred^[n] j = i
Tactic: refine ⟨n, ?_⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.LinearLocallyFinite (goal)
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
⊢ pred^[n] j = i
have rw : pred^[n] (succ^[n] i) = i
Tactic: rw [← hn_eq]