case refine'_1
o : Ordinal
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
⊢ a + o = o

case refine'_2
o : Ordinal
h : ∀ (a : Ordinal), a < o → a + o = o
a b : Ordinal
hao : a < o
hbo : b < o
⊢ (fun x x_1 => x + x_1) a b < o
o : Ordinal
⊢ Principal (fun x x_1 => x + x_1) o ↔ ∀ (a : Ordinal), a < o → a + o = o
refine' ⟨fun ho a hao => _, fun h a b hao hbo => _⟩
case refine'_1.inl
o : Ordinal
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
ho₁ : 1 < o
⊢ a + o = o

case refine'_1.inr
o : Ordinal
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
ho₁ : o ≤ 1
⊢ a + o = o
case refine'_1
o : Ordinal
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
⊢ a + o = o
cases' lt_or_le 1 o with ho₁ ho₁
no goals
case refine'_1.inl
o : Ordinal
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
ho₁ : 1 < o
⊢ a + o = o
exact op_eq_self_of_principal hao (add_isNormal a) ho (principal_add_isLimit ho₁ ho)
case refine'_1.inr.inl
a : Ordinal
ho : Principal (fun x x_1 => x + x_1) 0
hao : a < 0
ho₁ : 0 ≤ 1
⊢ a + 0 = 0

case refine'_1.inr.inr
a : Ordinal
ho : Principal (fun x x_1 => x + x_1) 1
hao : a < 1
ho₁ : 1 ≤ 1
⊢ a + 1 = 1
case refine'_1.inr
o : Ordinal
ho : Principal (fun x x_1 => x + x_1) o
a : Ordinal
hao : a < o
ho₁ : o ≤ 1
⊢ a + o = o
rcases le_one_iff.1 ho₁ with (rfl | rfl)
no goals
case refine'_1.inr.inl
a : Ordinal
ho : Principal (fun x x_1 => x + x_1) 0
hao : a < 0
ho₁ : 0 ≤ 1
⊢ a + 0 = 0
exact (Ordinal.not_lt_zero a hao).elim
case refine'_1.inr.inr
a : Ordinal
ho : Principal (fun x x_1 => x + x_1) 1
hao : a = 0
ho₁ : 1 ≤ 1
⊢ a + 1 = 1
case refine'_1.inr.inr
a : Ordinal
ho : Principal (fun x x_1 => x + x_1) 1
hao : a < 1
ho₁ : 1 ≤ 1
⊢ a + 1 = 1
rw [lt_one_iff_zero] at hao
no goals
case refine'_1.inr.inr
a : Ordinal
ho : Principal (fun x x_1 => x + x_1) 1
hao : a = 0
ho₁ : 1 ≤ 1
⊢ a + 1 = 1
rw [hao, zero_add]
case refine'_2
o : Ordinal
h : ∀ (a : Ordinal), a < o → a + o = o
a b : Ordinal
hao : a < o
hbo : b < o
⊢ (fun x x_1 => x + x_1) a b < a + o
case refine'_2
o : Ordinal
h : ∀ (a : Ordinal), a < o → a + o = o
a b : Ordinal
hao : a < o
hbo : b < o
⊢ (fun x x_1 => x + x_1) a b < o
rw [← h a hao]
no goals
case refine'_2
o : Ordinal
h : ∀ (a : Ordinal), a < o → a + o = o
a b : Ordinal
hao : a < o
hbo : b < o
⊢ (fun x x_1 => x + x_1) a b < a + o
exact (add_isNormal a).strictMono hbo