-- Mathlib/Order/Interval/Set/Limit.lean
lemma isSuccLimit_coe {J : Type u} [LinearOrder J] {j : J}
    (m : Set.Ici j) (hm : Order.IsSuccLimit m) :
    Order.IsSuccLimit m.1 :=
  ⟨Set.not_isMin_coe _ hm.1, fun b ↦ by
    simp only [CovBy, not_lt, not_and, not_forall, Classical.not_imp, not_le]
    intro hb
    by_cases hb' : j ≤ b
    · have := hm.2 ⟨b, hb'⟩
      rw [not_covBy_iff (by exact hb)] at this
      obtain ⟨⟨x, h₁⟩, h₂, h₃⟩ := this
      refine ⟨x, h₂, h₃⟩
    · simp only [not_le] at hb'
      refine ⟨j, hb', ?_⟩
      by_contra!
      apply hm.1
      rintro ⟨k, hk⟩ _
      exact this.trans (by simpa using hk)⟩

Proof state:
case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : ¬j ≤ b
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
simp only [not_le] at hb'

Result:
case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Proof state:
case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
refine ⟨j, hb', ?_⟩

Result:
case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
⊢ j < ↑m

Proof state:
case pos
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
have := hm.2 ⟨b, hb'⟩

Result:
case pos
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
this : ¬⟨b, hb'⟩ ⋖ m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Proof state:
case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
this : ↑m ≤ j
⊢ IsMin m

Tactic:
rintro ⟨k, hk⟩ _

Result:
case neg.mk
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
this : ↑m ≤ j
k : J
hk : k ∈ Ici j
a✝ : ⟨k, hk⟩ ≤ m
⊢ m ≤ ⟨k, hk⟩

Proof state:
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
⊢ b < ↑m → ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
intro hb

Result:
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Proof state:
case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
⊢ j < ↑m

Tactic:
by_contra!

Result:
case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
this : ↑m ≤ j
⊢ False

Proof state:
case pos.intro.mk.intro
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
x : J
h₁ : x ∈ Ici j
h₂ : ⟨b, hb'⟩ < ⟨x, h₁⟩
h₃ : ⟨x, h₁⟩ < m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
refine ⟨x, h₂, h₃⟩

Result:
no goals

Proof state:
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
by_cases hb' : j ≤ b

Result:
case pos
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : ¬j ≤ b
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Proof state:
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
this : ↑m ≤ j
k : J
hk : k ∈ Ici j
a✝ : ⟨k, hk⟩ ≤ m
⊢ j ≤ (fun a => ↑a) ⟨k, hk⟩

Tactic:
simpa using hk

Result:
no goals

Proof state:
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
this : ¬⟨b, hb'⟩ ⋖ m
⊢ ⟨b, hb'⟩ < m

Tactic:
exact hb

Result:
no goals

Proof state:
case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
this : ↑m ≤ j
⊢ False

Tactic:
apply hm.1

Result:
case neg
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
this : ↑m ≤ j
⊢ IsMin m

Proof state:
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
⊢ ¬b ⋖ ↑m

Tactic:
simp only [CovBy, not_lt, not_and, not_forall, Classical.not_imp, not_le]

Result:
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
⊢ b < ↑m → ∃ x, ∃ (_ : b < x), x < ↑m

Proof state:
case pos
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
this : ¬⟨b, hb'⟩ ⋖ m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
rw [not_covBy_iff (by exact hb)] at this

Result:
case pos
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
this : ∃ c, ⟨b, hb'⟩ < c ∧ c < m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Proof state:
case pos
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
this : ∃ c, ⟨b, hb'⟩ < c ∧ c < m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
obtain ⟨⟨x, h₁⟩, h₂, h₃⟩ := this

Result:
case pos.intro.mk.intro
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
x : J
h₁ : x ∈ Ici j
h₂ : ⟨b, hb'⟩ < ⟨x, h₁⟩
h₃ : ⟨x, h₁⟩ < m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Proof state:
case neg.mk
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
this : ↑m ≤ j
k : J
hk : k ∈ Ici j
a✝ : ⟨k, hk⟩ ≤ m
⊢ m ≤ ⟨k, hk⟩

Tactic:
exact this.trans (by simpa using hk)

Result:
no goals