case refine'_1
op : Ordinal → Ordinal → Ordinal
h : Principal op 1
⊢ op 0 0 = 0

case refine'_2
op : Ordinal → Ordinal → Ordinal
h : op 0 0 = 0
a b : Ordinal
ha : a < 1
hb : b < 1
⊢ op a b < 1
op : Ordinal → Ordinal → Ordinal
⊢ Principal op 1 ↔ op 0 0 = 0
refine' ⟨fun h => _, fun h a b ha hb => _⟩
case refine'_1
op : Ordinal → Ordinal → Ordinal
h : Principal op 1
⊢ op 0 0 < 1
case refine'_1
op : Ordinal → Ordinal → Ordinal
h : Principal op 1
⊢ op 0 0 = 0
rw [← lt_one_iff_zero]
no goals
case refine'_1
op : Ordinal → Ordinal → Ordinal
h : Principal op 1
⊢ op 0 0 < 1
exact h zero_lt_one zero_lt_one
no goals
case refine'_2
op : Ordinal → Ordinal → Ordinal
h : op 0 0 = 0
a b : Ordinal
ha : a < 1
hb : b < 1
⊢ op a b < 1
rwa [lt_one_iff_zero, ha, hb] at *