case refine'_1
α : Type ?u.322882
β : Type ?u.322885
γ : Type ?u.322888
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : succ (sup f) ≤ lsub f
⊢ ∃ i, f i = sup f

case refine'_2
α : Type ?u.322882
β : Type ?u.322885
γ : Type ?u.322888
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
⊢ (∃ i, f i = sup f) → succ (sup f) ≤ lsub f
α : Type ?u.322882
β : Type ?u.322885
γ : Type ?u.322888
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
⊢ succ (sup f) ≤ lsub f ↔ ∃ i, f i = sup f
refine' ⟨fun h => _, _⟩
case refine'_2.intro
α : Type ?u.322882
β : Type ?u.322885
γ : Type ?u.322888
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
w✝ : ι
hf : f w✝ = sup f
⊢ succ (sup f) ≤ lsub f
case refine'_2
α : Type ?u.322882
β : Type ?u.322885
γ : Type ?u.322888
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
⊢ (∃ i, f i = sup f) → succ (sup f) ≤ lsub f
rintro ⟨_, hf⟩
case refine'_2.intro
α : Type ?u.322882
β : Type ?u.322885
γ : Type ?u.322888
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
w✝ : ι
hf : f w✝ = sup f
⊢ f w✝ < lsub f
case refine'_2.intro
α : Type ?u.322882
β : Type ?u.322885
γ : Type ?u.322888
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
w✝ : ι
hf : f w✝ = sup f
⊢ succ (sup f) ≤ lsub f
rw [succ_le_iff, ← hf]
no goals
case refine'_2.intro
α : Type ?u.322882
β : Type ?u.322885
γ : Type ?u.322888
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
w✝ : ι
hf : f w✝ = sup f
⊢ f w✝ < lsub f
exact lt_lsub _ _
case refine'_1
α : Type ?u.322882
β : Type ?u.322885
γ : Type ?u.322888
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : succ (sup f) ≤ lsub f
hf : ∀ (i : ι), f i ≠ sup f
⊢ False
case refine'_1
α : Type ?u.322882
β : Type ?u.322885
γ : Type ?u.322888
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : succ (sup f) ≤ lsub f
⊢ ∃ i, f i = sup f
by_contra' hf
no goals
case refine'_1
α : Type ?u.322882
β : Type ?u.322885
γ : Type ?u.322888
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : succ (sup f) ≤ lsub f
hf : ∀ (i : ι), f i ≠ sup f
⊢ False
exact (succ_le_iff.1 h).ne ((sup_le_lsub f).antisymm (lsub_le (ne_sup_iff_lt_sup.1 hf)))