ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : ∃ c, c ∈ lowerBounds (Set.Ioi i) ∧ j < c
⊢ j ≤ i
ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : j < succFn i
⊢ j ≤ i
rw [lt_isGLB_iff (succFn_spec i)] at hij
case intro.intro
ι : Type u_1
inst✝ : LinearOrder ι
j i k : ι
hk_lb : k ∈ lowerBounds (Set.Ioi i)
hk : j < k
⊢ j ≤ i
ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : ∃ c, c ∈ lowerBounds (Set.Ioi i) ∧ j < c
⊢ j ≤ i
obtain ⟨k, hk_lb, hk⟩ := hij
case intro.intro
ι : Type u_1
inst✝ : LinearOrder ι
j i k : ι
hk_lb : ∀ (x : ι), x ∈ Set.Ioi i → k ≤ x
hk : j < k
⊢ j ≤ i
case intro.intro
ι : Type u_1
inst✝ : LinearOrder ι
j i k : ι
hk_lb : k ∈ lowerBounds (Set.Ioi i)
hk : j < k
⊢ j ≤ i
rw [mem_lowerBounds] at hk_lb
no goals
case intro.intro
ι : Type u_1
inst✝ : LinearOrder ι
j i k : ι
hk_lb : ∀ (x : ι), x ∈ Set.Ioi i → k ≤ x
hk : j < k
⊢ j ≤ i
exact not_lt.mp fun hi_lt_j ↦ not_le.mpr hk (hk_lb j hi_lt_j)