case refine'_1
o : Ordinal
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
ho₀ : o = 0
⊢ False

case refine'_2
o : Ordinal
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
⊢ succ a < o
o : Ordinal
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
⊢ IsLimit o
refine' ⟨fun ho₀ => _, fun a hao => _⟩
case refine'_1
o : Ordinal
ho₁ : 1 < 0
ho : Principal (fun x x_1 => x + x_1) o
ho₀ : o = 0
⊢ False
case refine'_1
o : Ordinal
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
ho₀ : o = 0
⊢ False
rw [ho₀] at ho₁
no goals
case refine'_1
o : Ordinal
ho₁ : 1 < 0
ho : Principal (fun x x_1 => x + x_1) o
ho₀ : o = 0
⊢ False
exact not_lt_of_gt zero_lt_one ho₁
case refine'_2.inl
o : Ordinal
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
ha : a = 0
⊢ succ a < o

case refine'_2.inr
o : Ordinal
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
ha : a ≠ 0
⊢ succ a < o
case refine'_2
o : Ordinal
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
⊢ succ a < o
cases' eq_or_ne a 0 with ha ha
case refine'_2.inl
o : Ordinal
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
ha : a = 0
⊢ 1 < o
case refine'_2.inl
o : Ordinal
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
ha : a = 0
⊢ succ a < o
rw [ha, succ_zero]
no goals
case refine'_2.inl
o : Ordinal
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
ha : a = 0
⊢ 1 < o
exact ho₁
case refine'_2.inr
o : Ordinal
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
ha : a ≠ 0
⊢ succ a ≤ (fun x x_1 => x + x_1) a a
case refine'_2.inr
o : Ordinal
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
ha : a ≠ 0
⊢ succ a < o
refine' lt_of_le_of_lt _ (ho hao hao)
no goals
case refine'_2.inr
o : Ordinal
ho₁ : 1 < o
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
ha : a ≠ 0
⊢ succ a ≤ (fun x x_1 => x + x_1) a a
rwa [← add_one_eq_succ, add_le_add_iff_left, one_le_iff_ne_zero]