diff --git a/Mathlib/Order/Normal.lean b/Mathlib/Order/Normal.lean
index 90effecb5ddf0..dd6c82ba1c592 100644
--- a/Mathlib/Order/Normal.lean
+++ b/Mathlib/Order/Normal.lean
@@ -3,6 +3,7 @@ Copyright (c) 2025 Violeta Hernández Palacios. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Violeta Hernández Palacios
 -/
+import Mathlib.Order.SuccPred.CompleteLinearOrder
 import Mathlib.Order.SuccPred.InitialSeg
 
 /-!
@@ -21,7 +22,7 @@ TODO: replace `Ordinal.IsNormal` by this more general notion.
 
 open Order Set
 
-variable {α β : Type*} {a b : α} [LinearOrder α] [LinearOrder β]
+variable {α β γ : Type*} {a b : α} [LinearOrder α] [LinearOrder β] [LinearOrder γ]
 
 /-- A normal function between well-orders is a strictly monotonic continuous function. -/
 structure IsNormal (f : α → β) : Prop where
@@ -32,9 +33,7 @@ structure IsNormal (f : α → β) : Prop where
     f a ∈ lowerBounds (upperBounds (f '' Iio a))
 
 namespace IsNormal
-variable {f : α → β}
-
---theorem of_
+variable {f : α → β} {g : β → γ}
 
 theorem of_succ_lt [SuccOrder α] [WellFoundedLT α]
     (hs : ∀ a, f a < f (succ a)) (hl : ∀ {a}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)) :
@@ -76,28 +75,51 @@ theorem le_iff_forall_le (hf : IsNormal f) (ha : IsSuccLimit a) {b : β} :
     f a ≤ b ↔ ∀ a' < a, f a' ≤ b := by
   simpa [mem_upperBounds] using isLUB_le_iff (hf.isLUB_of_isSuccLimit ha)
 
-theorem lf_iff_exists_lt (hf : IsNormal f) (ha : IsSuccLimit a) {b : β} :
+theorem lt_iff_exists_lt (hf : IsNormal f) (ha : IsSuccLimit a) {b : β} :
     b < f a ↔ ∃ a' < a, b < f a' := by
   simpa [mem_upperBounds] using lt_isLUB_iff (hf.isLUB_of_isSuccLimit ha)
 
+theorem map_isLUB (hf : IsNormal f) {s : Set α} (hs : s.Nonempty) (hs' : IsLUB s a) :
+    IsLUB (f '' s) (f a) := by
+  constructor
+  · simp_rw [mem_upperBounds, forall_mem_image, hf.le_iff_le]
+    exact hs'.1
+  · intro b hb
+    by_cases ha : a ∈ s
+    · simp_rw [mem_upperBounds, forall_mem_image] at hb
+      exact hb ha
+    · have := IsLUB.mem_of_not_isSuccPrelimit
+
+#exit
+theorem map_isSuccLimit (hf : IsNormal f) (ha : IsSuccLimit a) : IsSuccLimit (f a) := by
+  refine ⟨?_, fun b hb ↦ ?_⟩
+  · obtain ⟨b, hb⟩ := not_isMin_iff.1 ha.not_isMin
+    exact not_isMin_iff.2 ⟨_, hf.strictMono hb⟩
+  · obtain ⟨c, hc, hc'⟩ := (hf.lt_iff_exists_lt ha).1 hb.lt
+    have hc' := hb.ge_of_gt hc'
+    rw [hf.le_iff_le] at hc'
+    exact hc.not_le hc'
+
 theorem _root_.InitialSeg.isNormal (f : α ≤i β) : IsNormal f where
   strictMono := f.strictMono
   mem_lowerBounds_upperBounds := by
-    intro a ha b hb
-    apply le_of_forall_lt
-    intro c hc
-    obtain ⟨c, rfl⟩ := f.mem_range_of_le hc.le
-    rw [f.lt_iff_lt] at hc
-    have := hb (mem_image_of_mem f hc)
-    simp only [mem_upperBounds] at hb
-
-    have := hb hc
-
-protected theorem id : IsNormal (@id α) where
-  strictMono := strictMono_id
-  isLUB_of_isSuccLimit := by
     intro a ha
-    simp
-    refine isLUB_Iio
+    rw [f.image_Iio]
+    exact (f.map_isSuccLimit ha).isLUB_Iio.2
+
+theorem _root_.PrincipalSeg.isNormal (f : α <i β) : IsNormal f :=
+  (f : α ≤i β).isNormal
+
+protected theorem id : IsNormal (@id α) :=
+  (InitialSeg.refl _).isNormal
+
+theorem trans (hg : IsNormal g) (hf : IsNormal f) : IsNormal (g ∘ f) where
+  strictMono := hg.strictMono.comp hf.strictMono
+  mem_lowerBounds_upperBounds := by
+    intro a ha b hb
+    simp_rw [Function.comp_apply, mem_upperBounds, forall_mem_image] at hb
+    simpa [hg.le_iff_forall_le (hf.map_isSuccLimit ha), hf.lt_iff_exists_lt ha] using
+      fun c d hd hc ↦ (hg.strictMono hc).le.trans (hb hd)
+
 
 end IsNormal
diff --git a/Mathlib/Order/SuccPred/CompleteLinearOrder.lean b/Mathlib/Order/SuccPred/CompleteLinearOrder.lean
index 315082f3d46be..70a3762c25e7c 100644
--- a/Mathlib/Order/SuccPred/CompleteLinearOrder.lean
+++ b/Mathlib/Order/SuccPred/CompleteLinearOrder.lean
@@ -123,17 +123,17 @@ lemma exists_eq_ciSup_of_not_isSuccPrelimit'
 @[deprecated exists_eq_ciSup_of_not_isSuccPrelimit' (since := "2024-09-05")]
 alias exists_eq_ciSup_of_not_isSuccLimit' := exists_eq_ciSup_of_not_isSuccPrelimit'
 
-lemma IsLUB.mem_of_not_isSuccPrelimit (hs : IsLUB s x) (hx : ¬ IsSuccPrelimit x) : x ∈ s := by
-  obtain rfl | hs' := s.eq_empty_or_nonempty
-  · simp [show x = ⊥ by simpa using hs, isSuccPrelimit_bot] at hx
-  · exact hs.mem_of_nonempty_of_not_isSuccPrelimit hs' hx
+@[deprecated IsLUB.isSuccPrelimit_of_not_mem (since := "2025-01-05")]
+lemma IsLUB.mem_of_not_isSuccPrelimit (hs : IsLUB s x) (hx : ¬ IsSuccPrelimit x) : x ∈ s :=
+  hx.imp_symm hs.isSuccPrelimit_of_not_mem
 
 @[deprecated IsLUB.mem_of_not_isSuccPrelimit (since := "2024-09-05")]
 alias IsLUB.mem_of_not_isSuccLimit := IsLUB.mem_of_not_isSuccPrelimit
 
+@[deprecated IsLUB.isSuccPrelimit_of_not_mem (since := "2025-01-05")]
 lemma IsLUB.exists_of_not_isSuccPrelimit (hf : IsLUB (range f) x) (hx : ¬ IsSuccPrelimit x) :
     ∃ i, f i = x :=
-  hf.mem_of_not_isSuccPrelimit hx
+  hx.imp_symm hf.isSuccPrelimit_of_not_mem
 
 @[deprecated IsLUB.exists_of_not_isSuccPrelimit (since := "2024-09-05")]
 alias IsLUB.exists_of_not_isSuccLimit := IsLUB.exists_of_not_isSuccPrelimit
@@ -196,15 +196,17 @@ lemma exists_eq_iInf_of_not_isPredPrelimit (hf : ¬ IsPredPrelimit (⨅ i, f i))
 @[deprecated exists_eq_iInf_of_not_isPredPrelimit (since := "2024-09-05")]
 alias exists_eq_iInf_of_not_isPredLimit := exists_eq_iInf_of_not_isPredPrelimit
 
+@[deprecated IsGLB.isPredPrelimit_of_not_mem (since := "2025-01-05")]
 lemma IsGLB.mem_of_not_isPredPrelimit (hs : IsGLB s x) (hx : ¬ IsPredPrelimit x) : x ∈ s :=
-  hs.sInf_eq ▸ sInf_mem_of_not_isPredPrelimit (hs.sInf_eq ▸ hx)
+  hx.imp_symm hs.isPredPrelimit_of_not_mem
 
 @[deprecated IsGLB.mem_of_not_isPredPrelimit (since := "2024-09-05")]
 alias IsGLB.mem_of_not_isPredLimit := IsGLB.mem_of_not_isPredPrelimit
 
+@[deprecated IsGLB.isPredPrelimit_of_not_mem (since := "2025-01-05")]
 lemma IsGLB.exists_of_not_isPredPrelimit (hf : IsGLB (range f) x) (hx : ¬ IsPredPrelimit x) :
     ∃ i, f i = x :=
-  hf.mem_of_not_isPredPrelimit hx
+  hx.imp_symm hf.isPredPrelimit_of_not_mem
 
 @[deprecated IsGLB.exists_of_not_isPredPrelimit (since := "2024-09-05")]
 alias IsGLB.exists_of_not_isPredLimit := IsGLB.exists_of_not_isPredPrelimit
diff --git a/Mathlib/Order/SuccPred/Limit.lean b/Mathlib/Order/SuccPred/Limit.lean
index a5bf5787c8387..aa87d9363f44a 100644
--- a/Mathlib/Order/SuccPred/Limit.lean
+++ b/Mathlib/Order/SuccPred/Limit.lean
@@ -338,6 +338,13 @@ theorem isLUB_Iio_iff_isSuccPrelimit : IsLUB (Iio a) a ↔ IsSuccPrelimit a := b
   obtain rfl := isLUB_Iic.unique ha
   cases hb.lt.false
 
+lemma _root_.IsLUB.isSuccPrelimit_of_not_mem {s : Set α} (hs : IsLUB s a) (hx : a ∉ s) :
+    IsSuccPrelimit a := by
+  intro b hb
+  obtain ⟨c, hc, hbc, hca⟩ := hs.exists_between hb.lt
+  obtain rfl := (hb.ge_of_gt hbc).antisymm hca
+  contradiction
+
 variable [SuccOrder α]
 
 theorem IsSuccPrelimit.le_succ_iff (hb : IsSuccPrelimit b) : b ≤ succ a ↔ b ≤ a :=
@@ -643,6 +650,10 @@ theorem IsPredLimit.isGLB_Ioi (ha : IsPredLimit a) : IsGLB (Ioi a) a :=
 theorem isGLB_Ioi_iff_isPredPrelimit : IsGLB (Ioi a) a ↔ IsPredPrelimit a := by
   simpa using isLUB_Iio_iff_isSuccPrelimit (a := toDual a)
 
+lemma _root_.IsGLB.isPredPrelimit_of_not_mem {s : Set α} (hs : IsGLB s a) (hx : a ∉ s) :
+    IsPredPrelimit a := by
+  simpa using (IsGLB.dual hs).isSuccPrelimit_of_not_mem hx
+
 variable [PredOrder α]
 
 theorem IsPredPrelimit.pred_le_iff (hb : IsPredPrelimit b) : pred a ≤ b ↔ a ≤ b :=
diff --git a/Mathlib/Order/UpperLower/Basic.lean b/Mathlib/Order/UpperLower/Basic.lean
index 83d0d3803a83b..511b9090e9774 100644
--- a/Mathlib/Order/UpperLower/Basic.lean
+++ b/Mathlib/Order/UpperLower/Basic.lean
@@ -7,6 +7,7 @@ import Mathlib.Data.SetLike.Basic
 import Mathlib.Data.Set.Lattice
 import Mathlib.Order.Interval.Set.OrdConnected
 import Mathlib.Order.Interval.Set.OrderIso
+import Mathlib.Order.InitialSeg
 
 /-!
 # Up-sets and down-sets
@@ -349,6 +350,14 @@ theorem isUpperSet_iff_Ioi_subset : IsUpperSet s ↔ ∀ ⦃a⦄, a ∈ s → Io
 theorem isLowerSet_iff_Iio_subset : IsLowerSet s ↔ ∀ ⦃a⦄, a ∈ s → Iio a ⊆ s := by
   simp [isLowerSet_iff_forall_lt, subset_def, @forall_swap (_ ∈ s)]
 
+theorem InitialSeg.image_Iio [PartialOrder β] (f : α ≤i β) (a : α) :
+    f '' Set.Iio a = Set.Iio (f a) :=
+  f.toOrderEmbedding.image_Iio f.isLowerSet_range a
+
+theorem PrincipalSeg.image_Iio [PartialOrder β] (f : α <i β) (a : α) :
+    f '' Set.Iio a = Set.Iio (f a) :=
+  (f : α ≤i β).image_Iio a
+
 end PartialOrder
 
 /-! ### Upper/lower sets and Fibrations -/