case refine'_1
α : Type ?u.69314
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
⊢ 1 ≤ ord (cof (succ o))

case refine'_2
α : Type ?u.69314
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
i j : Ordinal
hi : i < 1
hj : j < 1
h : i < j
⊢ (fun x x => o) i hi < (fun x x => o) j hj
α : Type ?u.69314
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
⊢ IsFundamentalSequence (succ o) 1 fun x x => o
refine' ⟨_, @fun i j hi hj h => _, blsub_const Ordinal.one_ne_zero o⟩
no goals
case refine'_1
α : Type ?u.69314
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
⊢ 1 ≤ ord (cof (succ o))
rw [cof_succ, ord_one]
case refine'_2
α : Type ?u.69314
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
i j : Ordinal
hi✝ : i < 1
hi : i = 0
hj✝ : j < 1
hj : j = 0
h : i < j
⊢ (fun x x => o) i hi✝ < (fun x x => o) j hj✝
case refine'_2
α : Type ?u.69314
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
i j : Ordinal
hi : i < 1
hj : j < 1
h : i < j
⊢ (fun x x => o) i hi < (fun x x => o) j hj
rw [lt_one_iff_zero] at hi hj
case refine'_2
α : Type ?u.69314
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
i j : Ordinal
hi✝ : i < 1
hi : i = 0
hj✝ : j < 1
hj : j = 0
h : 0 < 0
⊢ (fun x x => o) i hi✝ < (fun x x => o) j hj✝
case refine'_2
α : Type ?u.69314
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
i j : Ordinal
hi✝ : i < 1
hi : i = 0
hj✝ : j < 1
hj : j = 0
h : i < j
⊢ (fun x x => o) i hi✝ < (fun x x => o) j hj✝
rw [hi, hj] at h
no goals
case refine'_2
α : Type ?u.69314
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
i j : Ordinal
hi✝ : i < 1
hi : i = 0
hj✝ : j < 1
hj : j = 0
h : 0 < 0
⊢ (fun x x => o) i hi✝ < (fun x x => o) j hj✝
exact h.false.elim