[GOAL]
α : Type u_1
inst✝ : LT α
a : α
⊢ ¬IsSuccLimit a ↔ ∃ b, b ⋖ a
[PROOFSTEP]
simp [IsSuccLimit]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
h : IsSuccLimit (succ a)
⊢ IsMax a
[PROOFSTEP]
by_contra H
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
h : IsSuccLimit (succ a)
H : ¬IsMax a
⊢ False
[PROOFSTEP]
exact h a (covby_succ_of_not_isMax H)
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
ha : ¬IsMax a
⊢ ¬IsSuccLimit (succ a)
[PROOFSTEP]
contrapose! ha
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : SuccOrder α
ha : IsSuccLimit (succ a)
⊢ IsMax a
[PROOFSTEP]
exact ha.isMax
[GOAL]
α : Type u_1
inst✝² : Preorder α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
h : IsSuccLimit a
b : α
⊢ succ b ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
b : α
h : IsSuccLimit (succ b)
⊢ False
[PROOFSTEP]
exact not_isMax _ h.isMax
[GOAL]
α : Type u_1
inst✝³ : Preorder α
a : α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
h : IsSuccLimit a
b : α
hb : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
rcases hb.exists_succ_iterate with ⟨_ | n, rfl⟩
[GOAL]
case intro.zero
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
h : IsSuccLimit (succ^[Nat.zero] b)
hb : b ≤ succ^[Nat.zero] b
⊢ succ^[Nat.zero] b ≤ b
[PROOFSTEP]
exact le_rfl
[GOAL]
case intro.succ
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
n : ℕ
h : IsSuccLimit (succ^[Nat.succ n] b)
hb : b ≤ succ^[Nat.succ n] b
⊢ succ^[Nat.succ n] b ≤ b
[PROOFSTEP]
rw [iterate_succ_apply'] at h 
[GOAL]
case intro.succ
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
n : ℕ
h : IsSuccLimit (succ (succ^[n] b))
hb : b ≤ succ^[Nat.succ n] b
⊢ succ^[Nat.succ n] b ≤ b
[PROOFSTEP]
exact (not_isSuccLimit_succ _ h).elim
[GOAL]
α : Type u_1
inst✝⁴ : Preorder α
a : α
inst✝³ : SuccOrder α
inst✝² : IsSuccArchimedean α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ ¬IsSuccLimit a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
⊢ ¬IsSuccLimit a ↔ ∃ b, ¬IsMax b ∧ succ b = a
[PROOFSTEP]
rw [not_isSuccLimit_iff_exists_covby]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
⊢ (∃ b, b ⋖ a) ↔ ∃ b, ¬IsMax b ∧ succ b = a
[PROOFSTEP]
refine' exists_congr fun b => ⟨fun hba => ⟨hba.lt.not_isMax, (Covby.succ_eq hba)⟩, _⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
b : α
⊢ ¬IsMax b ∧ succ b = a → b ⋖ a
[PROOFSTEP]
rintro ⟨h, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b✝ : α
C : α → Sort u_2
b : α
h : ¬IsMax b
⊢ b ⋖ succ b
[PROOFSTEP]
exact covby_succ_of_not_isMax h
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
h : ¬IsSuccLimit a
⊢ a ∈ range succ
[PROOFSTEP]
cases' not_isSuccLimit_iff.1 h with b hb
[GOAL]
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
h : ¬IsSuccLimit a
b : α
hb : ¬IsMax b ∧ succ b = a
⊢ a ∈ range succ
[PROOFSTEP]
exact ⟨b, hb.2⟩
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hb : IsSuccLimit b
ha : a < b
⊢ succ a < b
[PROOFSTEP]
by_cases h : IsMax a
[GOAL]
case pos
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hb : IsSuccLimit b
ha : a < b
h : IsMax a
⊢ succ a < b
[PROOFSTEP]
rwa [h.succ_eq]
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hb : IsSuccLimit b
ha : a < b
h : ¬IsMax a
⊢ succ a < b
[PROOFSTEP]
rw [lt_iff_le_and_ne, succ_le_iff_of_not_isMax h]
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hb : IsSuccLimit b
ha : a < b
h : ¬IsMax a
⊢ a < b ∧ succ a ≠ b
[PROOFSTEP]
refine' ⟨ha, fun hab => _⟩
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hb : IsSuccLimit b
ha : a < b
h : ¬IsMax a
hab : succ a = b
⊢ False
[PROOFSTEP]
subst hab
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
C : α → Sort u_2
h : ¬IsMax a
hb : IsSuccLimit (succ a)
ha : a < succ a
⊢ False
[PROOFSTEP]
exact (h hb.isMax).elim
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
b : α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
⊢ C b
[PROOFSTEP]
by_cases hb : IsSuccLimit b
[GOAL]
case pos
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
b : α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : IsSuccLimit b
⊢ C b
[PROOFSTEP]
exact hl b hb
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
b : α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : ¬IsSuccLimit b
⊢ C b
[PROOFSTEP]
have H := Classical.choose_spec (not_isSuccLimit_iff.1 hb)
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
b : α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : ¬IsSuccLimit b
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = b)) = b
⊢ C b
[PROOFSTEP]
rw [← H.2]
[GOAL]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
b : α
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : ¬IsSuccLimit b
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = b)) = b
⊢ C (succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = b)))
[PROOFSTEP]
exact hs _ H.1
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : IsSuccLimit b
⊢ isSuccLimitRecOn b hs hl = hl b hb
[PROOFSTEP]
classical exact dif_pos hb
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : IsSuccLimit b
⊢ isSuccLimitRecOn b hs hl = hl b hb
[PROOFSTEP]
exact dif_pos hb
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
⊢ isSuccLimitRecOn (succ b) hs hl = hs b hb
[PROOFSTEP]
have hb' := not_isSuccLimit_succ_of_not_isMax hb
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
⊢ isSuccLimitRecOn (succ b) hs hl = hs b hb
[PROOFSTEP]
have H := Classical.choose_spec (not_isSuccLimit_iff.1 hb')
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ isSuccLimitRecOn (succ b) hs hl = hs b hb
[PROOFSTEP]
rw [isSuccLimitRecOn]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ (if hb : IsSuccLimit (succ b) then hl (succ b) hb
    else
      let_fun H :=
        (_ :
          ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
            succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b);
      Eq.mpr (_ : C (succ b) = C (succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))))
        (hs (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))
          (_ : ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))))) =
    hs b hb
[PROOFSTEP]
simp only [cast_eq_iff_heq, hb', not_false_iff, eq_mpr_eq_cast, dif_neg]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ HEq
    (hs (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))
      (_ : ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))))
    (hs b hb)
[PROOFSTEP]
congr 1
[GOAL]
case e_1
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b) = b
[PROOFSTEP]
first
| exact (succ_eq_succ_iff_of_not_isMax H.left hb).mp H.right
| exact proof_irrel_heq H.left hb
[GOAL]
case e_1
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b) = b
[PROOFSTEP]
exact (succ_eq_succ_iff_of_not_isMax H.left hb).mp H.right
[GOAL]
case e_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ HEq (_ : ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))) hb
[PROOFSTEP]
first
| exact (succ_eq_succ_iff_of_not_isMax H.left hb).mp H.right
| exact proof_irrel_heq H.left hb
[GOAL]
case e_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ HEq (_ : ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))) hb
[PROOFSTEP]
exact (succ_eq_succ_iff_of_not_isMax H.left hb).mp H.right
[GOAL]
case e_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort u_2
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
b : α
hb : ¬IsMax b
hb' : ¬IsSuccLimit (succ b)
H :
  ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) ∧
    succ (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b)) = succ b
⊢ HEq (_ : ¬IsMax (Classical.choose (_ : ∃ b_1, ¬IsMax b_1 ∧ succ b_1 = succ b))) hb
[PROOFSTEP]
exact proof_irrel_heq H.left hb
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
C : α → Sort u_2
inst✝ : NoMaxOrder α
⊢ ¬IsSuccLimit a ↔ a ∈ range succ
[PROOFSTEP]
simp_rw [isSuccLimit_iff_succ_ne, not_forall, not_ne_iff]
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b : α
C : α → Sort u_2
inst✝ : NoMaxOrder α
⊢ (∃ x, succ x = a) ↔ a ∈ range succ
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort u_2
inst✝ : IsSuccArchimedean α
h : IsSuccLimit a
b : α
hb : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
revert h
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort u_2
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
⊢ IsSuccLimit a → a ≤ b
[PROOFSTEP]
refine' Succ.rec (fun _ => le_rfl) (fun c _ H hc => _) hb
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort u_2
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccLimit c → c ≤ b
hc : IsSuccLimit (succ c)
⊢ succ c ≤ b
[PROOFSTEP]
have := hc.isMax.succ_eq
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort u_2
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccLimit c → c ≤ b
hc : IsSuccLimit (succ c)
this : succ c = c
⊢ succ c ≤ b
[PROOFSTEP]
rw [this] at hc ⊢
[GOAL]
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a b✝ : α
C : α → Sort u_2
inst✝ : IsSuccArchimedean α
b : α
hb : b ≤ a
c : α
x✝ : b ≤ c
H : IsSuccLimit c → c ≤ b
hc : IsSuccLimit c
this : succ c = c
⊢ c ≤ b
[PROOFSTEP]
exact H hc
[GOAL]
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
a b : α
C : α → Sort u_2
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMinOrder α
⊢ ¬IsSuccLimit a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : LT α
a✝ a : α
⊢ ¬IsPredLimit a ↔ ∃ b, a ⋖ b
[PROOFSTEP]
simp [IsPredLimit]
[GOAL]
α : Type u_1
inst✝ : LT α
a : α
⊢ IsSuccLimit (↑toDual a) ↔ IsPredLimit a
[PROOFSTEP]
simp [IsSuccLimit, IsPredLimit]
[GOAL]
α : Type u_1
inst✝ : LT α
a : α
⊢ IsPredLimit (↑toDual a) ↔ IsSuccLimit a
[PROOFSTEP]
simp [IsSuccLimit, IsPredLimit]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : PredOrder α
h : IsPredLimit (pred a)
⊢ IsMin a
[PROOFSTEP]
by_contra H
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : PredOrder α
h : IsPredLimit (pred a)
H : ¬IsMin a
⊢ False
[PROOFSTEP]
exact h a (pred_covby_of_not_isMin H)
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : PredOrder α
ha : ¬IsMin a
⊢ ¬IsPredLimit (pred a)
[PROOFSTEP]
contrapose! ha
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
a : α
inst✝ : PredOrder α
ha : IsPredLimit (pred a)
⊢ IsMin a
[PROOFSTEP]
exact ha.isMin
[GOAL]
α : Type u_1
inst✝² : Preorder α
a : α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
h : IsPredLimit a
b : α
⊢ pred b ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝² : Preorder α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
b : α
h : IsPredLimit (pred b)
⊢ False
[PROOFSTEP]
exact not_isMin _ h.isMin
[GOAL]
α : Type u_1
inst✝⁴ : Preorder α
a : α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ ¬IsPredLimit a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
C : α → Sort u_2
⊢ ¬IsPredLimit a ↔ ∃ b, ¬IsMin b ∧ pred b = a
[PROOFSTEP]
rw [← isSuccLimit_toDual_iff]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
C : α → Sort u_2
⊢ ¬IsSuccLimit (↑toDual a) ↔ ∃ b, ¬IsMin b ∧ pred b = a
[PROOFSTEP]
exact not_isSuccLimit_iff
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
C : α → Sort u_2
h : ¬IsPredLimit a
⊢ a ∈ range pred
[PROOFSTEP]
cases' not_isPredLimit_iff.1 h with b hb
[GOAL]
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b✝ : α
C : α → Sort u_2
h : ¬IsPredLimit a
b : α
hb : ¬IsMin b ∧ pred b = a
⊢ a ∈ range pred
[PROOFSTEP]
exact ⟨b, hb.2⟩
[GOAL]
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : PredOrder α
a b : α
C : α → Sort u_2
inst✝¹ : IsPredArchimedean α
inst✝ : NoMaxOrder α
⊢ ¬IsPredLimit a
[PROOFSTEP]
simp
