case refine'_1
α : Type ?u.354095
β : Type ?u.354098
γ : Type ?u.354101
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
h : succ (bsup o f) ≤ blsub o f
⊢ ∃ i hi, f i hi = bsup o f

case refine'_2
α : Type ?u.354095
β : Type ?u.354098
γ : Type ?u.354101
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ (∃ i hi, f i hi = bsup o f) → succ (bsup o f) ≤ blsub o f
α : Type ?u.354095
β : Type ?u.354098
γ : Type ?u.354101
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ succ (bsup o f) ≤ blsub o f ↔ ∃ i hi, f i hi = bsup o f
refine' ⟨fun h => _, _⟩
case refine'_2.intro.intro
α : Type ?u.354095
β : Type ?u.354098
γ : Type ?u.354101
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
w✝¹ : Ordinal
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = bsup o f
⊢ succ (bsup o f) ≤ blsub o f
case refine'_2
α : Type ?u.354095
β : Type ?u.354098
γ : Type ?u.354101
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ (∃ i hi, f i hi = bsup o f) → succ (bsup o f) ≤ blsub o f
rintro ⟨_, _, hf⟩
case refine'_2.intro.intro
α : Type ?u.354095
β : Type ?u.354098
γ : Type ?u.354101
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
w✝¹ : Ordinal
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = bsup o f
⊢ f w✝¹ w✝ < blsub o f
case refine'_2.intro.intro
α : Type ?u.354095
β : Type ?u.354098
γ : Type ?u.354101
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
w✝¹ : Ordinal
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = bsup o f
⊢ succ (bsup o f) ≤ blsub o f
rw [succ_le_iff, ← hf]
no goals
case refine'_2.intro.intro
α : Type ?u.354095
β : Type ?u.354098
γ : Type ?u.354101
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
w✝¹ : Ordinal
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = bsup o f
⊢ f w✝¹ w✝ < blsub o f
exact lt_blsub _ _ _
case refine'_1
α : Type ?u.354095
β : Type ?u.354098
γ : Type ?u.354101
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
h : succ (bsup o f) ≤ blsub o f
hf : ∀ (i : Ordinal) (hi : i < o), f i hi ≠ bsup o f
⊢ False
case refine'_1
α : Type ?u.354095
β : Type ?u.354098
γ : Type ?u.354101
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
h : succ (bsup o f) ≤ blsub o f
⊢ ∃ i hi, f i hi = bsup o f
by_contra' hf
no goals
case refine'_1
α : Type ?u.354095
β : Type ?u.354098
γ : Type ?u.354101
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
h : succ (bsup o f) ≤ blsub o f
hf : ∀ (i : Ordinal) (hi : i < o), f i hi ≠ bsup o f
⊢ False
exact
  ne_of_lt (succ_le_iff.1 h)
    (le_antisymm (bsup_le_blsub f) (blsub_le (lt_bsup_of_ne_bsup.1 hf)))