-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsNormal.map_iSup_of_bddAbove {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f)
    {ι : Type*} (g : ι → Ordinal.{u}) (hg : BddAbove (range g))
    [Nonempty ι] : f (⨆ i, g i) = ⨆ i, f (g i) := eq_of_forall_ge_iff fun a ↦ by
  have := bddAbove_iff_small.mp hg
  have := univLE_of_injective H.strictMono.injective
  have := Small.trans_univLE.{u, v} (range g)
  have hfg : BddAbove (range (f ∘ g)) := bddAbove_iff_small.mpr <| by
    rw [range_comp]
    exact small_image f (range g)
  change _ ↔ ⨆ i, (f ∘ g) i ≤ a
  rw [ciSup_le_iff hfg, H.le_set' _ Set.univ_nonempty g] <;> simp [ciSup_le_iff hg]

Proof state:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
this✝¹ : Small.{u, u + 1} ↑(range g)
this✝ : UnivLE.{u, v}
this : Small.{v, u + 1} ↑(range g)
⊢ Small.{v, v + 1} ↑(range (f ∘ g))

Tactic:
rw [range_comp]

Result:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
this✝¹ : Small.{u, u + 1} ↑(range g)
this✝ : UnivLE.{u, v}
this : Small.{v, u + 1} ↑(range g)
⊢ Small.{v, v + 1} ↑(f '' range g)

Proof state:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
this✝¹ : Small.{u, u + 1} ↑(range g)
this✝ : UnivLE.{u, v}
this : Small.{v, u + 1} ↑(range g)
⊢ f (⨆ i, g i) ≤ a ↔ ⨆ i, f (g i) ≤ a

Tactic:
have hfg : BddAbove (range (f ∘ g)) := bddAbove_iff_small.mpr <| by
  rw [range_comp]
  exact small_image f (range g)

Result:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
this✝¹ : Small.{u, u + 1} ↑(range g)
this✝ : UnivLE.{u, v}
this : Small.{v, u + 1} ↑(range g)
hfg : BddAbove (range (f ∘ g))
⊢ f (⨆ i, g i) ≤ a ↔ ⨆ i, f (g i) ≤ a

Proof state:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
this✝¹ : Small.{u, u + 1} ↑(range g)
this✝ : UnivLE.{u, v}
this : Small.{v, u + 1} ↑(range g)
hfg : BddAbove (range (f ∘ g))
⊢ f (⨆ i, g i) ≤ a ↔ ⨆ i, (f ∘ g) i ≤ a

Tactic:
rw [ciSup_le_iff hfg, H.le_set' _ Set.univ_nonempty g] <;> simp [ciSup_le_iff hg]

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
⊢ f (⨆ i, g i) ≤ a ↔ ⨆ i, f (g i) ≤ a

Tactic:
have := bddAbove_iff_small.mp hg

Result:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
this : Small.{u, u + 1} ↑(range g)
⊢ f (⨆ i, g i) ≤ a ↔ ⨆ i, f (g i) ≤ a

Proof state:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
this✝¹ : Small.{u, u + 1} ↑(range g)
this✝ : UnivLE.{u, v}
this : Small.{v, u + 1} ↑(range g)
hfg : BddAbove (range (f ∘ g))
⊢ f (⨆ i, g i) ≤ a ↔ ⨆ i, f (g i) ≤ a

Tactic:
change _ ↔ ⨆ i, (f ∘ g) i ≤ a

Result:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
this✝¹ : Small.{u, u + 1} ↑(range g)
this✝ : UnivLE.{u, v}
this : Small.{v, u + 1} ↑(range g)
hfg : BddAbove (range (f ∘ g))
⊢ f (⨆ i, g i) ≤ a ↔ ⨆ i, (f ∘ g) i ≤ a

Proof state:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
this✝¹ : Small.{u, u + 1} ↑(range g)
this✝ : UnivLE.{u, v}
this : Small.{v, u + 1} ↑(range g)
⊢ Small.{v, v + 1} ↑(f '' range g)

Tactic:
exact small_image f (range g)

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
this✝ : Small.{u, u + 1} ↑(range g)
this : UnivLE.{u, v}
⊢ f (⨆ i, g i) ≤ a ↔ ⨆ i, f (g i) ≤ a

Tactic:
have := Small.trans_univLE.{u, v} (range g)

Result:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
this✝¹ : Small.{u, u + 1} ↑(range g)
this✝ : UnivLE.{u, v}
this : Small.{v, u + 1} ↑(range g)
⊢ f (⨆ i, g i) ≤ a ↔ ⨆ i, f (g i) ≤ a

Proof state:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
this : Small.{u, u + 1} ↑(range g)
⊢ f (⨆ i, g i) ≤ a ↔ ⨆ i, f (g i) ≤ a

Tactic:
have := univLE_of_injective H.strictMono.injective

Result:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
ι : Type u_4
g : ι → Ordinal.{u}
hg : BddAbove (range g)
inst✝ : Nonempty ι
a : Ordinal.{v}
this✝ : Small.{u, u + 1} ↑(range g)
this : UnivLE.{u, v}
⊢ f (⨆ i, g i) ≤ a ↔ ⨆ i, f (g i) ≤ a