case refine'_1
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : sup f = lsub f
⊢ ∀ (a : Ordinal), a < lsub f → succ a < lsub f

case refine'_2
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
⊢ f i < sup f
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
⊢ sup f = lsub f ↔ ∀ (a : Ordinal), a < lsub f → succ a < lsub f
refine' ⟨fun h => _, fun hf => le_antisymm (sup_le_lsub f) (lsub_le fun i => _)⟩
case refine'_2
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
hle : sup f ≤ f i
⊢ False
case refine'_2
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
⊢ f i < sup f
by_contra' hle
case refine'_2
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
⊢ False
case refine'_2
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
hle : sup f ≤ f i
⊢ False
have heq := (sup_succ_eq_lsub f).2 ⟨i, le_antisymm (le_sup _ _) hle⟩
case refine'_2
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
this : succ (sup f) < lsub f
⊢ False
case refine'_2
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
⊢ False
have :=
  hf _
    (by
      rw [← heq]
      exact lt_succ (sup f))
case refine'_2
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
this : lsub f < lsub f
⊢ False
case refine'_2
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
this : succ (sup f) < lsub f
⊢ False
rw [heq] at this
no goals
case refine'_2
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
this : lsub f < lsub f
⊢ False
exact this.false
case refine'_1
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : sup f = lsub f
⊢ ∀ (a : Ordinal), a < sup f → succ a < sup f
case refine'_1
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : sup f = lsub f
⊢ ∀ (a : Ordinal), a < lsub f → succ a < lsub f
rw [← h]
no goals
case refine'_1
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
h : sup f = lsub f
⊢ ∀ (a : Ordinal), a < sup f → succ a < sup f
exact fun a => sup_not_succ_of_ne_sup fun i => (lsub_le_iff.1 (le_of_eq h.symm) i).ne
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
⊢ ?m.325906 < succ (sup f)

α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
⊢ Ordinal
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
⊢ ?m.325906 < lsub f
rw [← heq]
no goals
α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
⊢ ?m.325906 < succ (sup f)

α : Type ?u.324464
β : Type ?u.324467
γ : Type ?u.324470
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (a : Ordinal), a < lsub f → succ a < lsub f
i : ι
hle : sup f ≤ f i
heq : succ (sup f) = lsub f
⊢ Ordinal
exact lt_succ (sup f)