feat(order/initial_seg): is_empty (r ≺i r) (#15803)

src/order/initial_seg.lean

@@ -205,14 +205,16 @@ theorem init_iff [is_trans β s] (f : r ≺i s) {a : α} {b : β} :
   s b (f a) ↔ ∃ a', f a' = b ∧ r a' a :=
 @initial_seg.init_iff α β r s f a b
 
-theorem irrefl (r : α → α → Prop) [is_well_order α r] (f : r ≺i r) : false :=
+theorem irrefl {r : α → α → Prop} [is_well_order α r] (f : r ≺i r) : false :=
 begin
   have := f.lt_top f.top,
   rw [show f f.top = f.top, from
       initial_seg.eq ↑f (initial_seg.refl r) f.top] at this,
   exact irrefl _ this
 end
 
+instance (r : α → α → Prop) [is_well_order α r] : is_empty (r ≺i r) := ⟨λ f, f.irrefl⟩
+
 /-- Composition of a principal segment with an initial segment, as a principal segment -/
 def lt_le (f : r ≺i s) (g : s ≼i t) : r ≺i t :=
 ⟨@rel_embedding.trans _ _ _ r s t f g, g f.top, λ a,

src/set_theory/ordinal/basic.lean

@@ -182,7 +182,7 @@ instance : partial_order ordinal :=
     λ ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨γ, t, _⟩ ⟨f⟩ ⟨g⟩, ⟨f.trans g⟩,
   lt_iff_le_not_le := λ a b, quotient.induction_on₂ a b $
     λ ⟨α, r, _⟩ ⟨β, s, _⟩, by exactI
-      ⟨λ ⟨f⟩, ⟨⟨f⟩, λ ⟨g⟩, (f.lt_le g).irrefl _⟩,
+      ⟨λ ⟨f⟩, ⟨⟨f⟩, λ ⟨g⟩, (f.lt_le g).irrefl⟩,
       λ ⟨⟨f⟩, h⟩, sum.rec_on f.lt_or_eq (λ g, ⟨g⟩)
       (λ g, (h ⟨initial_seg.of_iso g.symm⟩).elim)⟩,
   le_antisymm := λ a b,