awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMaxOrder α
x : WithTop α
coe :
  ∀ (x : α),
    IsSuccLimit (↑x : WithTop α) ↔ (↑x : WithTop α) = ⊤ ∨ ∃ (y : α), (↑x : WithTop α) = (↑y : WithTop α) ∧ IsSuccLimit y
⊢ IsSuccLimit x ↔ x = ⊤ ∨ ∃ (y : α), x = (↑y : WithTop α) ∧ IsSuccLimit y
have top : IsSuccLimit.{u_1} (α := WithTop α) ⊤ ↔
  Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∨ ∃ (y : α), ⊤ = (↑y : WithTop α) ∧ IsSuccLimit y
Tactic: cases x with
  | coe x => simp [IsSuccLimit, WithTop.isSuccPrelimit_iff, WithTop.exists]
  | top => simp [IsSuccLimit, WithTop.exists]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : Preorder α
x : WithTop α
⊢ IsPredPrelimit x ↔ x = ⊤ ∨ ∃ (y : α), x = (↑y : WithTop α) ∧ IsPredLimit y
have coe : ∀ (x : α),
  IsPredPrelimit (↑x : WithTop α) ↔
    (↑x : WithTop α) = ⊤ ∨ ∃ (y : α), (↑x : WithTop α) = (↑y : WithTop α) ∧ IsPredLimit y
Tactic: cases x with
  | coe x => simp [IsPredPrelimit, IsPredLimit, WithTop.forall]
  | top => simp
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : Preorder α
x : WithTop α
coe :
  ∀ (x : α),
    IsPredPrelimit (↑x : WithTop α) ↔
      (↑x : WithTop α) = ⊤ ∨ ∃ (y : α), (↑x : WithTop α) = (↑y : WithTop α) ∧ IsPredLimit y
⊢ IsPredPrelimit x ↔ x = ⊤ ∨ ∃ (y : α), x = (↑y : WithTop α) ∧ IsPredLimit y
have top : IsPredPrelimit.{u_1} (α := WithTop α) ⊤ ↔
  Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∨ ∃ (y : α), ⊤ = (↑y : WithTop α) ∧ IsPredLimit y
Tactic: cases x with
  | coe x => simp [IsPredPrelimit, IsPredLimit, WithTop.forall]
  | top => simp
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
h : IsSuccPrelimit (succ a)
⊢ IsMax a
have by_contra : ∀ (H : ¬IsMax a), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : NoMaxOrder α
h : IsSuccPrelimit a
b : α
hb : b ≤ a
⊢ a ≤ b
have zero : ∀ (h : IsSuccPrelimit (succ^[0] b)) (hb : b ≤ succ^[0] b), succ^[0] b ≤ b
Tactic: rcases hb.exists_succ_iterate with ⟨_ | n, rfl⟩
Cleared hypotheses: a, h, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : NoMaxOrder α
h : IsSuccPrelimit a
b : α
hb : b ≤ a
zero : ∀ (h : IsSuccPrelimit (succ^[0] b)) (hb : b ≤ succ^[0] b), succ^[0] b ≤ b
⊢ a ≤ b
have succ : ∀ (n : ℕ) (h : IsSuccPrelimit (succ^[n + 1] b)) (hb : b ≤ succ^[n + 1] b), succ^[n + 1] b ≤ b
Tactic: rcases hb.exists_succ_iterate with ⟨_ | n, rfl⟩
Cleared hypotheses: a, h, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : NoMaxOrder α
b : α
n : ℕ
h : IsSuccPrelimit (succ^[n + 1] b)
hb : b ≤ succ^[n + 1] b
⊢ succ^[n + 1] b ≤ b
have h₁ : IsSuccPrelimit (succ (succ^[n] b))
Tactic: rw [iterate_succ_apply'] at h
Cleared hypotheses: h, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : OrderBot α
⊢ IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a
have rw : ¬IsMin a ∧ IsSuccPrelimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a
Tactic: rw [IsSuccLimit, isMin_iff_eq_bot]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : OrderBot α
rw : ¬IsMin a ∧ IsSuccPrelimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a
⊢ IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a
have rw₁ : ¬a = ⊥ ∧ IsSuccPrelimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a
Tactic: rw [IsSuccLimit, isMin_iff_eq_bot]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
⊢ ¬IsSuccPrelimit a ↔ ∃ (b : α), ¬IsMax b ∧ succ b = a
have rw : (∃ (b : α), b ⋖ a) ↔ ∃ (b : α), ¬IsMax b ∧ succ b = a
Tactic: rw [not_isSuccPrelimit_iff]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
⊢ (∃ (b : α), b ⋖ a) ↔ ∃ (b : α), ¬IsMax b ∧ succ b = a
have refine : ∀ (b : α), ¬IsMax b ∧ succ b = a → b ⋖ a
Tactic: refine exists_congr fun b ↦ ⟨fun hba ↦ ⟨hba.lt.not_isMax, hba.succ_eq⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
h : ¬IsSuccPrelimit a
⊢ Membership.mem (γ := Set α) (range succ) a
have obtain : ∀ (b : α) (hb : ¬IsMax b ∧ succ b = a), Membership.mem (γ := Set α) (range succ) a
Tactic: obtain ⟨b, hb⟩ := not_isSuccPrelimit_iff_succ_eq.1 h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
⊢ IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
have this : Membership.mem (γ := Set α) (range succ) a ∨ IsSuccPrelimit a
Tactic: have := mem_range_succ_or_isSuccPrelimit a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
this : Membership.mem (γ := Set α) (range succ) a ∨ IsSuccPrelimit a
⊢ IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
have inl : ∀ (this : Membership.mem (γ := Set α) (range succ) a),
  IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
this : Membership.mem (γ := Set α) (range succ) a ∨ IsSuccPrelimit a
inl :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
⊢ IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
have inr : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
this : Membership.mem (γ := Set α) (range succ) a ∨ IsSuccPrelimit a
inl :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₁ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₁ : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
⊢ IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
have inl₂ : ∀ (this : Membership.mem (γ := Set α) (range succ) a),
  ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
this : Membership.mem (γ := Set α) (range succ) a ∨ IsSuccPrelimit a
inl :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₁ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₁ : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₂ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
⊢ IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
have inr₂ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
this : Membership.mem (γ := Set α) (range succ) a ∨ IsSuccPrelimit a
inl :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₁ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₁ : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₂ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₂ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₃ inl₄ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
⊢ IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
have inl₅ : ∀ (this : Membership.mem (γ := Set α) (range succ) a), ¬IsMin a → a ∉ range succ → ¬IsMin a
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
this : Membership.mem (γ := Set α) (range succ) a ∨ IsSuccPrelimit a
inl :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₁ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₁ : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₂ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₂ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₃ inl₄ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₅ : ∀ (this : Membership.mem (γ := Set α) (range succ) a), ¬IsMin a → a ∉ range succ → ¬IsMin a
⊢ IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
have inl₆ : ∀ (this : Membership.mem (γ := Set α) (range succ) a), ¬IsMin a → a ∉ range succ → IsSuccPrelimit a
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
this : Membership.mem (γ := Set α) (range succ) a ∨ IsSuccPrelimit a
inl :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₁ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₁ : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₂ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₂ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₃ inl₄ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₅ : ∀ (this : Membership.mem (γ := Set α) (range succ) a), ¬IsMin a → a ∉ range succ → ¬IsMin a
inl₆ : ∀ (this : Membership.mem (γ := Set α) (range succ) a), ¬IsMin a → a ∉ range succ → IsSuccPrelimit a
inr₃ inr₄ :
  ∀ (this : IsSuccPrelimit a), ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
⊢ IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
have inr₅ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → a ∉ range succ → ¬IsMin a
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
this : Membership.mem (γ := Set α) (range succ) a ∨ IsSuccPrelimit a
inl :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₁ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₁ : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₂ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₂ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₃ inl₄ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₅ : ∀ (this : Membership.mem (γ := Set α) (range succ) a), ¬IsMin a → a ∉ range succ → ¬IsMin a
inl₆ : ∀ (this : Membership.mem (γ := Set α) (range succ) a), ¬IsMin a → a ∉ range succ → IsSuccPrelimit a
inr₃ inr₄ :
  ∀ (this : IsSuccPrelimit a), ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₅ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → a ∉ range succ → ¬IsMin a
⊢ IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
have inr₆ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → a ∉ range succ → IsSuccPrelimit a
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a : α
this : Membership.mem (γ := Set α) (range succ) a ∨ IsSuccPrelimit a
inl :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₁ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₁ : ∀ (this : IsSuccPrelimit a), IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₂ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₂ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₃ inl₄ :
  ∀ (this : Membership.mem (γ := Set α) (range succ) a),
    ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inl₅ : ∀ (this : Membership.mem (γ := Set α) (range succ) a), ¬IsMin a → a ∉ range succ → ¬IsMin a
inl₆ : ∀ (this : Membership.mem (γ := Set α) (range succ) a), ¬IsMin a → a ∉ range succ → IsSuccPrelimit a
inr₃ inr₄ :
  ∀ (this : IsSuccPrelimit a), ¬IsMin a → Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
inr₅ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → a ∉ range succ → ¬IsMin a
inr₆ : ∀ (this : IsSuccPrelimit a), ¬IsMin a → a ∉ range succ → IsSuccPrelimit a
⊢ IsMin a ∨ Membership.mem (γ := Set α) (range succ) a ∨ ¬IsMin a ∧ IsSuccPrelimit a
have inl₇ : ∀ (this : Membership.mem (γ := Set α) (range succ) a), ¬IsMin a → a ∉ range succ → ∀ (b : α), ¬b ⋖ a
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
⊢ succ a < b
have pos : ∀ (h : IsMax a), succ a < b
Tactic: by_cases h : IsMax a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
pos : ∀ (h : IsMax a), succ a < b
⊢ succ a < b
have neg : ∀ (h : ¬IsMax a), succ a < b
Tactic: by_cases h : IsMax a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
⊢ succ a < b
have neg : a < b ∧ succ a ≠ b
Tactic: rw [lt_iff_le_and_ne, succ_le_iff_of_not_isMax h]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
⊢ a < b ∧ succ a ≠ b
have neg : ∀ (hab : succ a = b), False
Tactic: refine ⟨ha, fun hab => ?_⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
hab : succ a = b
⊢ False
have hb₁ : IsSuccPrelimit (succ a)
Tactic: subst hab
Cleared hypotheses: b, hb, ha, hab
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
a b : α
inst : PartialOrder α
inst_1 : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
hab : succ a = b
hb₁ : IsSuccPrelimit (succ a)
⊢ False
have ha₁ : a < succ a
Tactic: subst hab
Cleared hypotheses: b, hb, ha, hab
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
⊢ ¬IsSuccPrelimit a ↔ Membership.mem (γ := Set α) (range succ) a
have simp_rw : (¬∀ (b : α), succ b ≠ a) ↔ Membership.mem (γ := Set α) (range succ) a
Tactic: simp_rw [isSuccPrelimit_iff_succ_ne, not_forall, not_ne_iff, mem_range]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
simp_rw : (¬∀ (b : α), succ b ≠ a) ↔ Membership.mem (γ := Set α) (range succ) a
⊢ ¬IsSuccPrelimit a ↔ Membership.mem (γ := Set α) (range succ) a
have simp_rw₁ : (∃ (x : α), ¬succ x ≠ a) ↔ Membership.mem (γ := Set α) (range succ) a
Tactic: simp_rw [isSuccPrelimit_iff_succ_ne, not_forall, not_ne_iff, mem_range]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
simp_rw : (¬∀ (b : α), succ b ≠ a) ↔ Membership.mem (γ := Set α) (range succ) a
simp_rw₁ : (∃ (x : α), ¬succ x ≠ a) ↔ Membership.mem (γ := Set α) (range succ) a
⊢ ¬IsSuccPrelimit a ↔ Membership.mem (γ := Set α) (range succ) a
have simp_rw₂ : (∃ (x : α), succ x = a) ↔ Membership.mem (γ := Set α) (range succ) a
Tactic: simp_rw [isSuccPrelimit_iff_succ_ne, not_forall, not_ne_iff, mem_range]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
h : IsSuccPrelimit a
b : α
hb : b ≤ a
⊢ a ≤ b
have revert : ∀ (h : IsSuccPrelimit a), a ≤ b
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
b : α
hb : b ≤ a
⊢ ∀ (h : IsSuccPrelimit a), a ≤ b
have refine : ∀ (c : α), b ≤ c → ∀ (H : ∀ (h : IsSuccPrelimit c), c ≤ b) (hc : IsSuccPrelimit (succ c)), succ c ≤ b
Tactic: refine Succ.rec (fun _ => le_rfl) (fun c _ H hc => ?_) hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
h : b ≤ c
H : ∀ (h : IsSuccPrelimit c), c ≤ b
hc : IsSuccPrelimit (succ c)
⊢ succ c ≤ b
have this : succ c = c
Tactic: have := hc.isMax.succ_eq
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
h : b ≤ c
H : ∀ (h : IsSuccPrelimit c), c ≤ b
hc : IsSuccPrelimit (succ c)
this : succ c = c
⊢ succ c ≤ b
have rw : ∀ (hc : IsSuccPrelimit c) (this : succ c = c), c ≤ b
Tactic: rw [this] at hc ⊢
Cleared hypotheses: hc, this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a b : α
inst : LinearOrder α
h : IsSuccPrelimit a
⊢ a ≤ b ↔ ∀ c < a, c ≤ b
have mpr : (∀ c < a, c ≤ b) → a ≤ b
Tactic: use fun ha c hc ↦ hc.le.trans ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a b : α
inst : LinearOrder α
h : IsSuccPrelimit a
H : ∀ c < a, c ≤ b
⊢ a ≤ b
have mpr : ∀ (ha : b < a), False
Tactic: by_contra! ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a b : α
inst : LinearOrder α
h : IsSuccPrelimit b
⊢ a < b ↔ ∃ c < b, a < c
have rw : ¬a < b ↔ ¬∃ c < b, a < c
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
⊢ False
have obtain : ∀ (c : α) (hc : c ∈ s) (hbc : b < c) (hca : c ≤ a), False
Tactic: obtain ⟨c, hc, hbc, hca⟩ := hs.exists_between hb.lt
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
c : α
hc : c ∈ s
hbc : b < c
hca : c ≤ a
⊢ False
have hc₁ : a ∈ s
Tactic: obtain rfl := (hb.ge_of_gt hbc).antisymm hca
Cleared hypotheses: c, hc, hbc, hca
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
c : α
hc : c ∈ s
hbc : b < c
hca : c ≤ a
hc₁ : a ∈ s
⊢ False
have hbc₁ : b < a
Tactic: obtain rfl := (hb.ge_of_gt hbc).antisymm hca
Cleared hypotheses: c, hc, hbc, hca
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
c : α
hc : c ∈ s
hbc : b < c
hca : c ≤ a
hc₁ : a ∈ s
hbc₁ : b < a
⊢ False
have hca₁ : a ≤ a
Tactic: obtain rfl := (hb.ge_of_gt hbc).antisymm hca
Cleared hypotheses: c, hc, hbc, hca
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
ha : a ∉ s
⊢ IsSuccLimit a
have refine : ¬IsMin a
Tactic: refine ⟨?_, hs.isSuccPrelimit_of_notMem ha⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
ha : a ∉ s
⊢ ¬IsMin a
have obtain : ∀ (b : α) (hb : b ∈ s), ¬IsMin a
Tactic: obtain ⟨b, hb⟩ := hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ∈ s
⊢ ¬IsMin a
have inl : ∀ (hs : IsLUB s b) (ha : b ∉ s), ¬IsMin b
Tactic: obtain rfl | hb := (hs.1 hb).eq_or_lt
Cleared hypotheses: a, hs, ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ∈ s
inl : ∀ (hs : IsLUB s b) (ha : b ∉ s), ¬IsMin b
⊢ ¬IsMin a
have inr : ∀ (hb : b < a), ¬IsMin a
Tactic: obtain rfl | hb := (hs.1 hb).eq_or_lt