-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sup_le_sup {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop)
    [IsWellOrder ι r] [IsWellOrder ι' r'] {o} (ho : type r = o) (ho' : type r' = o)
    (f : ∀ a < o, Ordinal.{max u v}) :
    sup.{_, v} (familyOfBFamily' r ho f) ≤ sup.{_, v} (familyOfBFamily' r' ho' f) :=
  sup_le fun i => by
    obtain ⟨j, hj⟩ := typein_surj r' (by rw [ho', ← ho]; exact typein_lt_type r i)
    simp_rw [familyOfBFamily', ← hj]
    apply le_sup

Proof state:
case intro
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
i : ι
j : ι'
hj : (typein r').toRelEmbedding j = (typein r).toRelEmbedding i
⊢ f ((typein r').toRelEmbedding j) ⋯ ≤ sup (familyOfBFamily' r' ho' f)

Tactic:
apply le_sup

Result:
no goals

Proof state:
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
i : ι
⊢ ?m.221963 < type r'

Tactic:
rw [ho', ← ho]

Result:
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
i : ι
⊢ ?m.221963 < type r

Proof state:
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
i : ι
⊢ ?m.221963 < type r

Tactic:
exact typein_lt_type r i

Result:
no goals

Proof state:
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
i : ι
⊢ familyOfBFamily' r ho f i ≤ sup (familyOfBFamily' r' ho' f)

Tactic:
obtain ⟨j, hj⟩ := typein_surj r' (by rw [ho', ← ho]; exact typein_lt_type r i)

Result:
case intro
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
i : ι
j : ι'
hj : (typein r').toRelEmbedding j = (typein r).toRelEmbedding i
⊢ familyOfBFamily' r ho f i ≤ sup (familyOfBFamily' r' ho' f)

Proof state:
case intro
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
i : ι
j : ι'
hj : (typein r').toRelEmbedding j = (typein r).toRelEmbedding i
⊢ familyOfBFamily' r ho f i ≤ sup (familyOfBFamily' r' ho' f)

Tactic:
simp_rw [familyOfBFamily', ← hj]

Result:
case intro
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
i : ι
j : ι'
hj : (typein r').toRelEmbedding j = (typein r).toRelEmbedding i
⊢ f ((typein r').toRelEmbedding j) ⋯ ≤ sup (familyOfBFamily' r' ho' f)