chore: partial forward port of 14324 (#5954)

This doesn't yet forward port the changes to Mathlib/SetTheory/Ordinal/NaturalOps.lean.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Floris van Doorn, Violeta Hernández Palacios
 
 ! This file was ported from Lean 3 source module set_theory.ordinal.arithmetic
-! leanprover-community/mathlib commit e08a42b2dd544cf11eba72e5fc7bf199d4349925
+! leanprover-community/mathlib commit 31b269b60935483943542d547a6dd83a66b37dc7
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1999,6 +1999,21 @@ theorem IsNormal.eq_iff_zero_and_succ {f g : Ordinal.{u} → Ordinal.{u}} (hf :
       exact H b hb⟩
 #align ordinal.is_normal.eq_iff_zero_and_succ Ordinal.IsNormal.eq_iff_zero_and_succ
 
+/-- A two-argument version of `Ordinal.blsub`.
+We don't develop a full API for this, since it's only used in a handful of existence results. -/
+def blsub₂ (o₁ o₂ : Ordinal) (op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) :
+    Ordinal :=
+  lsub (fun x : o₁.out.α × o₂.out.α => op (typein_lt_self x.1) (typein_lt_self x.2))
+#align ordinal.blsub₂ Ordinal.blsub₂
+
+theorem lt_blsub₂ {o₁ o₂ : Ordinal}
+    (op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) {a b : Ordinal}
+    (ha : a < o₁) (hb : b < o₂) : op ha hb < blsub₂ o₁ o₂ op := by
+  convert lt_lsub _ (Prod.mk (enum (· < · ) a (by rwa [type_lt]))
+    (enum (· < · ) b (by rwa [type_lt])))
+  simp only [typein_enum]
+#align ordinal.lt_blsub₂ Ordinal.lt_blsub₂
+
 /-! ### Minimum excluded ordinals -/
 
 

Mathlib/SetTheory/Ordinal/NaturalOps.lean

@@ -9,6 +9,7 @@ Authors: Violeta Hernández Palacios
 ! if you have ported upstream changes.
 -/
 import Mathlib.SetTheory.Ordinal.Arithmetic
+import Mathlib.Tactic.Abel
 
 /-!
 # Natural operations on ordinals
@@ -39,7 +40,6 @@ between both types, we attempt to prove and state most results on `Ordinal`.
 
 # Todo
 
-- Define natural multiplication and provide a basic API.
 - Prove the characterizations of natural addition and multiplication in terms of the Cantor normal
   form.
 -/
@@ -51,6 +51,8 @@ open Function Order
 
 noncomputable section
 
+/-! ### Basic casts between `ordinal` and `nat_ordinal` -/
+
 /-- A type synonym for ordinals with natural addition and multiplication. -/
 def NatOrdinal : Type _ :=
   -- porting note: used to derive LinearOrder & SuccOrder but need to manually define
@@ -73,10 +75,10 @@ def NatOrdinal.toOrdinal : NatOrdinal ≃o Ordinal :=
   OrderIso.refl _
 #align nat_ordinal.to_ordinal NatOrdinal.toOrdinal
 
-open Ordinal
-
 namespace NatOrdinal
 
+open Ordinal
+
 variable {a b c : NatOrdinal.{u}}
 
 @[simp]

Mathlib/SetTheory/Ordinal/Principal.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Violeta Hernández Palacios
 
 ! This file was ported from Lean 3 source module set_theory.ordinal.principal
-! leanprover-community/mathlib commit 9b2660e1b25419042c8da10bf411aa3c67f14383
+! leanprover-community/mathlib commit 31b269b60935483943542d547a6dd83a66b37dc7
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -91,35 +91,21 @@ theorem nfp_le_of_principal {op : Ordinal → Ordinal → Ordinal} {a o : Ordina
 
 /-! ### Principal ordinals are unbounded -/
 
-
-/-- The least strict upper bound of `op` applied to all pairs of ordinals less than `o`. This is
-essentially a two-argument version of `Ordinal.blsub`. -/
-def blsub₂ (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) : Ordinal :=
-  lsub fun x : o.out.α × o.out.α => op (typein LT.lt x.1) (typein LT.lt x.2)
-#align ordinal.blsub₂ Ordinal.blsub₂
-
-theorem lt_blsub₂ (op : Ordinal.{u} → Ordinal.{u} → Ordinal.{max u v})
-  {o a b : Ordinal.{u}} (ha : a < o)
-    (hb : b < o) : op a b < blsub₂.{u, v} op o := by
-  convert lt_lsub.{v, u}
-      (fun x : (Quotient.out.{u+2} o).α × (Quotient.out.{u+2} o).α =>
-        op (typein.{u} LT.lt x.fst) (typein.{u} LT.lt x.snd))
-      (Prod.mk.{u, u} (enum.{u} LT.lt a (by rwa [type_lt])) (enum.{u} LT.lt b (by rwa [type_lt])))
-  <;> simp only [typein_enum]
-#align ordinal.lt_blsub₂ Ordinal.lt_blsub₂
-
 theorem principal_nfp_blsub₂ (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) :
-    Principal op (nfp (blsub₂.{u, u} op) o) := fun a b ha hb => by
+    Principal op (nfp (fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b)) o) :=
+  fun a b ha hb => by
   rw [lt_nfp] at *
   cases' ha with m hm
   cases' hb with n hn
-  cases' le_total ((blsub₂.{u, u} op)^[m] o) ((blsub₂.{u, u} op)^[n] o) with h h
+  cases' le_total
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[m] o)
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[n] o) with h h
   · use n + 1
     rw [Function.iterate_succ']
-    exact lt_blsub₂ op (hm.trans_le h) hn
+    exact lt_blsub₂ (@fun a _ b _ => op a b) (hm.trans_le h) hn
   · use m + 1
     rw [Function.iterate_succ']
-    exact lt_blsub₂ op hm (hn.trans_le h)
+    exact lt_blsub₂ (@fun a _ b _ => op a b) hm (hn.trans_le h)
 #align ordinal.principal_nfp_blsub₂ Ordinal.principal_nfp_blsub₂
 
 theorem unbounded_principal (op : Ordinal → Ordinal → Ordinal) :