diff --git a/Iris/Iris/Algebra/OFE.lean b/Iris/Iris/Algebra/OFE.lean
index c8b831187..7217911df 100644
--- a/Iris/Iris/Algebra/OFE.lean
+++ b/Iris/Iris/Algebra/OFE.lean
@@ -7,6 +7,7 @@ module
 
 public import Iris.Std.Option
 public meta import Iris.Std.RocqPorting
+public meta import Iris.Std.NonExp
 
 @[expose] public section
 
@@ -62,6 +63,8 @@ instance [OFE α] {n : Nat} : Trans (OFE.Dist n) (OFE.Dist n) (OFE.Dist n : α 
 class NonExpansive [OFE α] [OFE β] (f : α → β) where
   ne : ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → f x₁ ≡{n}≡ f x₂
 
+attribute [non_exp] NonExpansive.ne
+
 instance id_ne [OFE α] : NonExpansive (@id α) := ⟨fun _ _ _ h => h⟩
 
 instance const_ne [OFE α] [OFE β] {x : α} : NonExpansive (Function.const β x) := ⟨fun _ _ _ _ => .rfl⟩
@@ -77,6 +80,8 @@ theorem NonExpansive.comp [OFE α] [OFE β] [OFE γ] {g : β → γ} {f : α →
 class NonExpansive₂ [OFE α] [OFE β] [OFE γ] (f : α → β → γ) where
   ne : ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → ∀ ⦃y₁ y₂⦄, y₁ ≡{n}≡ y₂ → f x₁ y₁ ≡{n}≡ f x₂ y₂
 
+attribute [non_exp] NonExpansive₂.ne
+
 #rocq_ignore ne_proper_2 "OFE is Leibniz; use equality"
 
 /-- Note: Not an instance, for symmetry with NonExpansive₂.ne_left, which cannot be an instance. -/
diff --git a/Iris/Iris/BI/BI.lean b/Iris/Iris/BI/BI.lean
index 172a6fc2e..18912586f 100644
--- a/Iris/Iris/BI/BI.lean
+++ b/Iris/Iris/BI/BI.lean
@@ -92,6 +92,15 @@ instance entails_preorder [BI PROP] : Std.IsPreorder PROP where
   le_refl _ := BI.entails_refl
   le_trans _ _ _ := BI.entails_trans
 
+attribute [instance] and_ne
+attribute [instance] or_ne
+attribute [instance] imp_ne
+attribute [non_exp] sForall_ne
+attribute [non_exp] sExists_ne
+attribute [instance] sep_ne
+attribute [instance] wand_ne
+attribute [instance] persistently_ne
+
 instance [BI PROP] : Std.Refl <| BIBase.Entails (PROP := PROP) where
   refl _ := BI.entails_refl
 
diff --git a/Iris/Iris/BI/BigOp/BigSepList.lean b/Iris/Iris/BI/BigOp/BigSepList.lean
index 21aed5e46..fa3694e35 100644
--- a/Iris/Iris/BI/BigOp/BigSepList.lean
+++ b/Iris/Iris/BI/BigOp/BigSepList.lean
@@ -73,7 +73,7 @@ theorem bigSepL_eq_of_forall_eq {Φ Ψ : Nat → A → PROP} {l : List A} (h : 
     ([∗list] k ↦ x ∈ l, Φ k x) = [∗list] k ↦ x ∈ l, Ψ k x :=
   bigOpL_eq_of_forall_eq h
 
-@[rocq_alias big_sepL_ne]
+@[rocq_alias big_sepL_ne, non_exp]
 theorem bigSepL_dist {Φ Ψ : Nat → A → PROP} {l : List A} {n : Nat}
     (h : ∀ {k x}, l[k]? = some x → Φ k x ≡{n}≡ Ψ k x) :
     ([∗list] k ↦ x ∈ l, Φ k x) ≡{n}≡ [∗list] k ↦ x ∈ l, Ψ k x :=
diff --git a/Iris/Iris/BI/DerivedLaws.lean b/Iris/Iris/BI/DerivedLaws.lean
index c8c02468d..69e4d4e53 100644
--- a/Iris/Iris/BI/DerivedLaws.lean
+++ b/Iris/Iris/BI/DerivedLaws.lean
@@ -165,7 +165,7 @@ theorem imp_congr_left [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : (P → Q) 
 theorem imp_congr_right [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : (P → Q) ⊣⊢ (P → Q') :=
   imp_congr .rfl h
 
-@[rocq_alias bi.forall_ne]
+@[rocq_alias bi.forall_ne, non_exp]
 theorem forall_ne [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ≡{n}≡ Ψ a) :
     iprop(∀ a, Φ a) ≡{n}≡ iprop(∀ a, Ψ a) := sForall_ne <| by
   constructor <;> rintro _ ⟨a, rfl⟩ <;> exact ⟨_, ⟨a, rfl⟩, h _⟩
@@ -190,7 +190,7 @@ theorem forall_mono [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ⊢ Ψ a) :
 theorem forall_congr [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ⊣⊢ Ψ a) : (∀ a, Φ a) ⊣⊢ ∀ a, Ψ a :=
   ⟨forall_mono fun a => (h a).1, forall_mono fun a => (h a).2⟩
 
-@[rocq_alias bi.exist_ne]
+@[rocq_alias bi.exist_ne, non_exp]
 theorem exists_ne [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ≡{n}≡ Ψ a) :
     iprop(∃ a, Φ a) ≡{n}≡ iprop(∃ a, Ψ a) := sExists_ne <| by
   constructor <;> rintro _ ⟨a, rfl⟩ <;> exact ⟨_, ⟨a, rfl⟩, h _⟩
@@ -895,7 +895,7 @@ theorem pure_wand_forall [BI PROP] {φ : Prop} {P : PROP} [Absorbing P] :
 /-! # Affine -/
 
 @[rocq_alias bi.affinely_ne]
-theorem affinely_ne [BI PROP] : OFE.NonExpansive (@affinely PROP _) where
+instance affinely_ne [BI PROP] : OFE.NonExpansive (@affinely PROP _) where
   ne _ _ _ h := and_ne.1 .rfl h
 #rocq_ignore bi.affinely_flip_mono' "Use _mono."
 #rocq_ignore bi.affinely_mono' "Use _mono."
@@ -1048,7 +1048,7 @@ theorem pure_imp_forall [BI PROP] {φ : Prop} {P : PROP} :
 /-! # Absorbing -/
 
 @[rocq_alias bi.absorbingly_ne]
-theorem absorbingly_ne [BI PROP] : OFE.NonExpansive (@absorbingly PROP _) where
+instance absorbingly_ne [BI PROP] : OFE.NonExpansive (@absorbingly PROP _) where
   ne _ _ _ h := sep_ne.1 .rfl h
 #rocq_ignore bi.absorbingly_flip_mono' "Use _mono."
 #rocq_ignore bi.absorbingly_mono' "Use _mono."
@@ -1647,8 +1647,7 @@ instance absorbingly_persistent [BI PROP] (P : PROP) [Persistent P] :
 
 /-! # The intuitionistic modality -/
 
-@[rocq_alias bi.intuitionistically_ne]
-theorem intuitionistically_ne [BI PROP] : OFE.NonExpansive (@intuitionistically PROP _) where
+instance intuitionistically_ne [BI PROP] : OFE.NonExpansive (@intuitionistically PROP _) where
   ne _ _ _ h := affinely_ne.1 (persistently_ne.1 h)
 #rocq_ignore bi.intuitionistically_flip_mono' "Use _mono."
 #rocq_ignore bi.intuitionistically_mono' "Use _mono."
@@ -1836,7 +1835,7 @@ theorem intuitionistically_into_persistently [BI PROP] {P : PROP} [BIAffine PROP
     iprop(<affine>?true P) = iprop(<affine> P) := rfl
 
 @[rocq_alias bi.affinely_if_ne]
-theorem affinelyIf_ne {p : Bool} [BI PROP] : OFE.NonExpansive (affinelyIf (PROP := PROP) p) :=
+instance affinelyIf_ne {p : Bool} [BI PROP] : OFE.NonExpansive (affinelyIf (PROP := PROP) p) :=
   match p with
   | true => affinely_ne
   | false => OFE.id_ne
@@ -1976,7 +1975,7 @@ theorem affinelyIf_and_left_right {p : Bool} [BI PROP] {P Q : PROP} :
     iprop(<absorb>?true P) = iprop(<absorb> P) := rfl
 
 @[rocq_alias bi.absorbingly_if_ne]
-theorem absorbinglyIf_ne {p : Bool} [BI PROP] : OFE.NonExpansive (absorbinglyIf (PROP := PROP) p) :=
+instance absorbinglyIf_ne {p : Bool} [BI PROP] : OFE.NonExpansive (absorbinglyIf (PROP := PROP) p) :=
   match p with
   | true => absorbingly_ne
   | false => OFE.id_ne
@@ -2119,7 +2118,7 @@ theorem affinely_if_absorbingly_if_elim [BI PROP] {p : Bool} {P : PROP} [BIPosit
     iprop(<pers>?true P) = iprop(<pers> P) := rfl
 
 @[rocq_alias bi.persistently_if_ne]
-theorem persistentlyIf_ne {p : Bool} [BI PROP] :
+instance persistentlyIf_ne {p : Bool} [BI PROP] :
     OFE.NonExpansive (persistentlyIf (PROP := PROP) p) :=
   match p with
   | true => persistently_ne
@@ -2220,7 +2219,7 @@ theorem persistentlyIf_intutitionistically {p : Bool} [BI PROP] {P : PROP} :
 @[simp] theorem intuitionisticallyIf_true [BI PROP] (P : PROP) : iprop(□?true P) = iprop(□ P) := rfl
 
 @[rocq_alias bi.intuitionistically_if_ne]
-theorem intuitionisticallyIf_ne {p : Bool} [BI PROP] :
+instance intuitionisticallyIf_ne {p : Bool} [BI PROP] :
     OFE.NonExpansive (intuitionisticallyIf (PROP := PROP) p) :=
   match p with
   | true => intuitionistically_ne
diff --git a/Iris/Iris/BI/DerivedLawsLater.lean b/Iris/Iris/BI/DerivedLawsLater.lean
index 867017d1c..c8b07a5e8 100644
--- a/Iris/Iris/BI/DerivedLawsLater.lean
+++ b/Iris/Iris/BI/DerivedLawsLater.lean
@@ -312,7 +312,7 @@ theorem loeb_alt_wand [BIAffine PROP] :
 /-! # LaterN -/
 
 @[rocq_alias bi.laterN_ne]
-theorem laterN_ne (n : Nat) : OFE.NonExpansive (BIBase.laterN (PROP:=PROP) n) where
+instance laterN_ne (n : Nat) : OFE.NonExpansive (BIBase.laterN (PROP:=PROP) n) where
   ne := by
     induction n with
     | zero => exact fun _ _ _ h => h
@@ -518,7 +518,7 @@ instance bi_laterN_sep_entails_homomorphism (n : Nat) :
 /-! # Except0 -/
 
 @[rocq_alias bi.except_0_ne]
-theorem except0_ne : OFE.NonExpansive (BIBase.except0 (PROP:=PROP)) where
+instance except0_ne : OFE.NonExpansive (BIBase.except0 (PROP:=PROP)) where
   ne _ _ _ h := or_ne.ne .rfl h
 
 @[rw_mono_rule, rocq_alias bi.except_0_mono]
diff --git a/Iris/Iris/BI/Updates.lean b/Iris/Iris/BI/Updates.lean
index 862419f61..57369f2ea 100644
--- a/Iris/Iris/BI/Updates.lean
+++ b/Iris/Iris/BI/Updates.lean
@@ -176,6 +176,8 @@ class BIFUpdate (PROP : Type _) [BI PROP] extends FUpd PROP where
     E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P
   frame_right {E1 E2 : CoPset} {P R : PROP} : (|={E1,E2}=> P) ∗ R ⊢ |={E1,E2}=> P ∗ R
 
+attribute [instance] BIFUpdate.ne
+
 #rocq_ignore BiFUpdMixin "Included in BIFUpdate typeclass."
 
 @[rocq_alias BiBUpdFUpd]
@@ -530,14 +532,14 @@ variable [BI PROP] [BIFUpdate PROP]
 
 open BIFUpdate LawfulSet
 
-theorem step_fupdN_contractive {E1 E2 : CoPset} {n : Nat} [ι : BILaterContractive PROP] :
+instance step_fupdN_contractive {E1 E2 : CoPset} {n : Nat} [ι : BILaterContractive PROP] :
     OFE.Contractive (iprop(|={E1}[E2]▷=>^[n + 1] · : PROP)) where
   distLater_dist {i x y} xy_i := by
     induction n with
     | zero => exact ne.ne (ι.distLater_dist (ne.ne <| xy_i · ·))
     | succ n IH => exact ne.ne (later_ne.ne (ne.ne IH))
 
-theorem step_fupdN_ne {E1 E2 : CoPset} {n : Nat} :
+instance step_fupdN_ne {E1 E2 : CoPset} {n : Nat} :
     OFE.NonExpansive (iprop(|={E1}[E2]▷=>^[n] · : PROP)) where
   ne {i x y} xy_i := by
     induction n with
diff --git a/Iris/Iris/Examples/IProp.lean b/Iris/Iris/Examples/IProp.lean
index 87984805c..3f02857ab 100644
--- a/Iris/Iris/Examples/IProp.lean
+++ b/Iris/Iris/Examples/IProp.lean
@@ -120,17 +120,7 @@ def wp_F (wp : Expr → (Value → IProp GF) → IProp GF) (e : Expr) (Φ : Valu
     ∃ e' s', ⌜@step _ _ Value _ (e, s) = (e', s') ⌝ ∗ ▷ |==> (@state_interp _ _ _  s' ∗ wp e' Φ))
 
 instance wp_F_contractive : Contractive (@wp_F Expr State Value _ GF _) where
-  distLater_dist {n x y HL} e Φ := by
-    refine or_ne.ne (.of_eq rfl) ?_
-    refine forall_ne (fun _ => ?_)
-    refine wand_ne.ne (.of_eq rfl) ?_
-    refine exists_ne (fun v => ?_)
-    refine exists_ne (fun _ => ?_)
-    refine sep_ne.ne (.of_eq rfl) ?_
-    refine Contractive.distLater_dist fun m Hm => ?_
-    refine BIUpdate.bupd_ne.ne ?_
-    refine sep_ne.ne (.of_eq rfl) ?_
-    exact HL m Hm v Φ
+  distLater_dist := by contractive
 
 def wp {Expr State Value : Type _} [@Ex3WP Expr State Value GF] (e : Expr) (Φ : Value → IProp GF) : IProp GF :=
   (fixpoint <| @wp_F Expr State Value _ GF _) e Φ
diff --git a/Iris/Iris/Instances/Lib/CInvariants.lean b/Iris/Iris/Instances/Lib/CInvariants.lean
index 6458fe5a5..723978e07 100644
--- a/Iris/Iris/Instances/Lib/CInvariants.lean
+++ b/Iris/Iris/Instances/Lib/CInvariants.lean
@@ -59,9 +59,7 @@ instance instTimelessExcl (γ : GName) : Timeless (excl (GF := GF) γ) :=
 @[rocq_alias cinv_contractive]
 instance instContractiveCinv (N : Namespace) (γ : GName) :
     Contractive (cinv (GF := GF) N γ) where
-  distLater_dist {n x y} H := by
-    unfold cinv
-    refine Contractive.distLater_dist fun m hm => or_ne.ne (sep_ne.ne (H _ hm) .rfl) .rfl
+  distLater_dist := by contractive
 
 @[rocq_alias cinv_ne]
 instance instNonExpansiveCinv (N : Namespace) (γ : GName) :
diff --git a/Iris/Iris/Instances/Lib/Invariants.lean b/Iris/Iris/Instances/Lib/Invariants.lean
index a44728626..f74c77c20 100644
--- a/Iris/Iris/Instances/Lib/Invariants.lean
+++ b/Iris/Iris/Instances/Lib/Invariants.lean
@@ -47,19 +47,8 @@ variable {GF : BundledGFunctors} [InvGS_gen hlc GF]
 
 @[rocq_alias inv_contractive]
 instance inv_contractive (N : Namespace) : Contractive (inv (GF := GF) N) where
-  distLater_dist {n x y} H := by
-    simp only [inv]
-    refine intuitionistically_ne.ne ?_
-    refine forall_ne (fun i => ?_)
-    refine imp_ne.ne .rfl ?_
-    refine wand_ne.ne .rfl ?_
-    refine (inferInstance : NonExpansive le_upd).ne ?_
-    refine sep_ne.ne .rfl ?_
-    refine sep_ne.ne .rfl ?_
-    refine sep_ne.ne ?_ ?_
-    · exact Contractive.distLater_dist H
-    · refine wand_ne.ne ?_ .rfl
-      exact Contractive.distLater_dist H
+  distLater_dist := by
+    contractive
 
 @[rocq_alias inv_ne]
 instance inv_ne (N : Namespace) : NonExpansive (inv (GF := GF) N) := ne_of_contractive _
diff --git a/Iris/Iris/Instances/Lib/LaterCredits.lean b/Iris/Iris/Instances/Lib/LaterCredits.lean
index 1f1847af6..965b684e4 100644
--- a/Iris/Iris/Instances/Lib/LaterCredits.lean
+++ b/Iris/Iris/Instances/Lib/LaterCredits.lean
@@ -12,6 +12,7 @@ public import Iris.Algebra.Numbers
 public import Iris.ProofMode
 public import Iris.BI.Algebra
 public import Iris.Instances.IProp
+public import Iris.ProofMode.Tactics.Contractive
 
 @[expose] public section
 
@@ -225,20 +226,7 @@ def le_upd_pre (P le_upd : IProp GF) : IProp GF :=
 
 @[rocq_alias le_upd.le_upd_pre_contractive]
 instance {P : IProp GF} : Contractive (le_upd_pre P) where
-  distLater_dist {n x y} H := by
-    simp only [le_upd_pre]
-    refine forall_ne (fun i => ?_)
-    refine wand_ne.ne .rfl ?_
-    refine UPred.bupd_ne.ne ?_
-    refine or_ne.ne .rfl ?_
-    refine or_ne.ne .rfl ?_
-    refine exists_ne (fun m => ?_)
-    refine sep_ne.ne .rfl ?_
-    refine sep_ne.ne .rfl ?_
-    refine Contractive.distLater_dist ?_
-    cases n
-    · exact distLater_zero
-    · exact distLater_succ.mpr (distLater_succ.mp H)
+  distLater_dist := by contractive
 
 #rocq_ignore le_upd.le_upd_def "`le_upd` is defined directly without `seal`/`unseal`."
 #rocq_ignore le_upd.le_upd_aux "`le_upd` is defined directly without `seal`/`unseal`."
diff --git a/Iris/Iris/Instances/Lib/Monotone.lean b/Iris/Iris/Instances/Lib/Monotone.lean
new file mode 100644
index 000000000..9276dbe62
--- /dev/null
+++ b/Iris/Iris/Instances/Lib/Monotone.lean
@@ -0,0 +1,604 @@
+/-
+Copyright (c) 2026 Oliver Soeser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Soeser
+-/
+module
+
+public import Iris.ProofMode
+
+@[expose] public section
+
+open Iris BI OFE Iris.Std
+
+class MonotonePred [BI PROP] [OFE A]
+    (F : (A → PROP) → (A → PROP)) : Prop where
+  monotone : ∀ (Φ Ψ : A → PROP),
+    ⊢ (□ ∀ x, Φ x -∗ Ψ x) -∗ ∀ x, F Φ x -∗ F Ψ x
+
+class AntitonePred [BI PROP] [OFE A]
+    (F : (A → PROP) → (A → PROP)) : Prop where
+  antitone : ∀ (Φ Ψ : A → PROP),
+    ⊢ (□ ∀ x, Φ x -∗ Ψ x) -∗ ∀ x, F Ψ x -∗ F Φ x
+
+section const
+
+instance monotone_const [BI PROP] [OFE A] : MonotonePred (λ_ : A → PROP => Ω) := by
+  constructor
+  intros
+  iintro #H1 %x H2
+  iexact H2
+
+instance monotone_const' [BI PROP] [OFE A] (y : A) : MonotonePred (λΦ : A → PROP => λ_ : A => Φ y) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  iapply H1
+  iexact H2
+
+instance antitone_const [BI PROP] [OFE A] : AntitonePred (λ_ : A → PROP => Ω) := by
+  constructor
+  intros
+  iintro #H1 %x H2
+  iexact H2
+
+end const
+
+section id
+
+instance monotone_id [BI PROP] [OFE A] : MonotonePred (λΦ : A → PROP => Φ) := by
+  constructor
+  intros
+  iintro #H %x HΦ
+  iapply H
+  iexact HΦ
+
+instance monotone_id' [BI PROP] [OFE A] (F : A → A) : MonotonePred (λΦ : A → PROP => λx : A => Φ (F x)) := by
+  constructor
+  intros
+  iintro #H %x HΦ
+  iapply H
+  iexact HΦ
+
+end id
+
+section comp
+
+instance monotone_comp [BI PROP] [OFE A] (F G : (A → PROP) → A → PROP)
+    [hf : MonotonePred F] [hg : MonotonePred G] : MonotonePred (λΦ => F (G Φ)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H %x HΦ
+  iapply hf.monotone (G Φ)
+  · imodintro
+    iapply hg.monotone
+    iexact H
+  · iexact HΦ
+
+end comp
+
+section and
+
+instance monotone_and [BI PROP] [OFE A] (F G : (A → PROP) → A → PROP)
+      [hf : MonotonePred F] [hg : MonotonePred G] :
+    MonotonePred (λΦ : A → PROP => λx : A => iprop(F Φ x ∧ G Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  isplit
+  · iapply hf.monotone Φ Ψ
+    iexact H1
+    iexact H2
+  · iapply hg.monotone Φ Ψ
+    iexact H1
+    iexact H2
+
+instance antitone_and [BI PROP] [OFE A] (F G : (A → PROP) → A → PROP)
+      [hf : AntitonePred F] [hg : AntitonePred G] :
+    AntitonePred (λΦ : A → PROP => λx : A => iprop(F Φ x ∧ G Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  isplit
+  · iapply hf.antitone Φ Ψ
+    iexact H1
+    iexact H2
+  · iapply hg.antitone Φ Ψ
+    iexact H1
+    iexact H2
+
+end and
+
+section or
+
+instance monotone_or [BI PROP] [OFE A] (F G : (A → PROP) → A → PROP)
+      [hf : MonotonePred F] [hg : MonotonePred G] :
+    MonotonePred (λΦ : A → PROP => λx : A => iprop(F Φ x ∨ G Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H %x (HF | HG)
+  · ileft
+    iapply hf.monotone Φ Ψ
+    iexact H
+    iexact HF
+  · iright
+    iapply hg.monotone Φ Ψ
+    iexact H
+    iexact HG
+
+instance antitone_or [BI PROP] [OFE A] (F G : (A → PROP) → A → PROP)
+      [hf : AntitonePred F] [hg : AntitonePred G] :
+    AntitonePred (λΦ : A → PROP => λx : A => iprop(F Φ x ∨ G Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H %x (HF | HG)
+  · ileft
+    iapply hf.antitone Φ Ψ
+    iexact H
+    iexact HF
+  · iright
+    iapply hg.antitone Φ Ψ
+    iexact H
+    iexact HG
+
+end or
+
+section sep
+
+instance monotone_sep [BI PROP] [OFE A] (F G : (A → PROP) → A → PROP)
+      [hf : MonotonePred F] [hg : MonotonePred G] :
+    MonotonePred (λΦ : A → PROP => λx : A => iprop(F Φ x ∗ G Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H %x ⟨HF, HG⟩
+  isplitl [HF]
+  · iapply hf.monotone Φ Ψ
+    iexact H
+    iexact HF
+  · iapply hg.monotone Φ Ψ
+    iexact H
+    iexact HG
+
+instance antitone_sep [BI PROP] [OFE A] (F G : (A → PROP) → A → PROP)
+      [hf : AntitonePred F] [hg : AntitonePred G] :
+    AntitonePred (λΦ : A → PROP => λx : A => iprop(F Φ x ∗ G Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H %x ⟨HF, HG⟩
+  isplitl [HF]
+  · iapply hf.antitone Φ Ψ
+    iexact H
+    iexact HF
+  · iapply hg.antitone Φ Ψ
+    iexact H
+    iexact HG
+
+end sep
+
+section wand
+
+instance monotone_wand [BI PROP] [OFE A] (F G : (A → PROP) → A → PROP)
+      [hf : AntitonePred F] [hg : MonotonePred G] :
+    MonotonePred (λΦ : A → PROP => λx : A => iprop(F Φ x -∗ G Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2 HF
+  iapply hg.monotone Φ Ψ
+  · iexact H1
+  · iapply H2
+    iapply hf.antitone Φ Ψ
+    · iexact H1
+    · iexact HF
+
+instance antitone_wand [BI PROP] [OFE A] (F G : (A → PROP) → A → PROP)
+      [hf : MonotonePred F] [hg : AntitonePred G] :
+    AntitonePred (λΦ : A → PROP => λx : A => iprop(F Φ x -∗ G Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2 HF
+  iapply hg.antitone Φ Ψ
+  · iexact H1
+  · iapply H2
+    iapply hf.monotone Φ Ψ
+    · iexact H1
+    · iexact HF
+
+end wand
+
+section pers_imp
+
+instance monotone_pers_imp [BI PROP] [OFE A] (F G : (A → PROP) → A → PROP)
+      [hf : AntitonePred F] [hg : MonotonePred G] :
+    MonotonePred (λΦ : A → PROP => λx : A => iprop(<pers> F Φ x → G Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2 #HF
+  iapply hg.monotone Φ Ψ
+  · iexact H1
+  · iapply (@intuitionistically_wand _ _ (F Φ x)).mpr $$ [H2]
+    iexact H2
+    imodintro
+    iapply hf.antitone Φ Ψ
+    · iexact H1
+    · iexact HF
+
+instance antitone_pers_imp [BI PROP] [OFE A] (F G : (A → PROP) → A → PROP)
+      [hf : MonotonePred F] [hg : AntitonePred G] :
+    AntitonePred (λΦ : A → PROP => λx : A => iprop(<pers> F Φ x → G Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2 #HF
+  iapply hg.antitone Φ Ψ
+  · iexact H1
+  · iapply (@intuitionistically_wand _ _ (F Ψ x)).mpr $$ [H2]
+    iexact H2
+    imodintro
+    iapply hf.monotone Φ Ψ
+    · iexact H1
+    · iexact HF
+
+end pers_imp
+
+section «forall»
+
+instance monotone_forall [BI PROP] [OFE A] (F : B → (A → PROP) → A → PROP)
+      [hf : ∀y, MonotonePred (F y)] :
+    MonotonePred (λΦ : A → PROP => λx : A => BI.forall (λy : B => F y Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  iintro %y
+  iapply (hf y).monotone Φ
+  · iexact H1
+  · iexact H2
+
+instance antitone_forall [BI PROP] [OFE A] (F : B → (A → PROP) → A → PROP)
+      [hf : ∀y, AntitonePred (F y)] :
+    AntitonePred (λΦ : A → PROP => λx : A => BI.forall (λy : B => F y Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  iintro %y
+  iapply (hf y).antitone Φ
+  · iexact H1
+  · iexact H2
+
+end «forall»
+
+section «exists»
+
+instance monotone_exists [BI PROP] [OFE A] (F : B → (A → PROP) → A → PROP)
+      [hf : ∀y, MonotonePred (F y)] :
+    MonotonePred (λΦ : A → PROP => λx : A => BI.exists (λy : B => F y Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x ⟨%y, H2⟩
+  iexists y
+  iapply (hf y).monotone Φ Ψ
+  iexact H1
+  iexact H2
+
+instance antitone_exists [BI PROP] [OFE A] (F : B → (A → PROP) → A → PROP)
+      [hf : ∀y, AntitonePred (F y)] :
+    AntitonePred (λΦ : A → PROP => λx : A => BI.exists (λy : B => F y Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x ⟨%y, H2⟩
+  iexists y
+  iapply (hf y).antitone Φ Ψ
+  iexact H1
+  iexact H2
+
+end «exists»
+
+section persistently
+
+instance monotone_persistently [BI PROP] [OFE A] (F : (A → PROP) → A → PROP)
+    [hf : MonotonePred F] : MonotonePred (λΦ : A → PROP => λx : A => iprop(<pers> F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x #H2
+  imodintro
+  iapply hf.monotone Φ Ψ
+  iexact H1
+  iexact H2
+
+instance antitone_persistently [BI PROP] [OFE A] (F : (A → PROP) → A → PROP)
+    [hf : AntitonePred F] : AntitonePred (λΦ : A → PROP => λx : A => iprop(<pers> F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x #H2
+  imodintro
+  iapply hf.antitone Φ Ψ
+  iexact H1
+  iexact H2
+
+end persistently
+
+section affinely
+
+instance monotone_affinely [BI PROP] [OFE A] (F : (A → PROP) → A → PROP)
+    [hf : MonotonePred F] : MonotonePred (λΦ : A → PROP => λx : A => iprop(<affine> F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  imodintro
+  iapply hf.monotone Φ Ψ
+  iexact H1
+  iexact H2
+
+instance antitone_affinely [BI PROP] [OFE A] (F : (A → PROP) → A → PROP)
+    [hf : AntitonePred F] : AntitonePred (λΦ : A → PROP => λx : A => iprop(<affine> F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  imodintro
+  iapply hf.antitone Φ Ψ
+  iexact H1
+  iexact H2
+
+end affinely
+
+section absorbingly
+
+instance monotone_absorbingly [BI PROP] [OFE A] (F : (A → PROP) → A → PROP)
+    [hf : MonotonePred F] : MonotonePred (λΦ : A → PROP => λx : A => iprop(<absorb> F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x >H2
+  imodintro
+  iapply hf.monotone Φ Ψ
+  iexact H1
+  iexact H2
+
+instance antitone_absorbingly [BI PROP] [OFE A] (F : (A → PROP) → A → PROP)
+    [hf : AntitonePred F] : AntitonePred (λΦ : A → PROP => λx : A => iprop(<absorb> F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x >H2
+  imodintro
+  iapply hf.antitone Φ Ψ
+  iexact H1
+  iexact H2
+
+end absorbingly
+
+section intuitionistically
+
+instance monotone_intuitionistically [BI PROP] [OFE A] (F : (A → PROP) → A → PROP)
+    [hf : MonotonePred F] : MonotonePred (λΦ : A → PROP => λx : A => iprop(□ F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x #H2
+  imodintro
+  iapply hf.monotone Φ Ψ
+  iexact H1
+  iexact H2
+
+instance antitone_intuitionistically [BI PROP] [OFE A] (F : (A → PROP) → A → PROP)
+    [hf : AntitonePred F] : AntitonePred (λΦ : A → PROP => λx : A => iprop(□ F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x #H2
+  imodintro
+  iapply hf.antitone Φ Ψ
+  iexact H1
+  iexact H2
+
+end intuitionistically
+
+section later
+
+instance monotone_later [BI PROP] [OFE A] (F : (A → PROP) → A → PROP)
+    [hf : MonotonePred F] : MonotonePred (λΦ : A → PROP => λx : A => iprop(▷ F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  inext
+  iapply hf.monotone Φ Ψ
+  iexact H1
+  iexact H2
+
+instance antitone_later [BI PROP] [OFE A] (F : (A → PROP) → A → PROP)
+    [hf : AntitonePred F] : AntitonePred (λΦ : A → PROP => λx : A => iprop(▷ F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  inext
+  iapply hf.antitone Φ Ψ
+  iexact H1
+  iexact H2
+
+end later
+
+section except0
+
+instance monotone_except0 [BI PROP] [OFE A] (F : (A → PROP) → A → PROP)
+    [hf : MonotonePred F] : MonotonePred (λΦ : A → PROP => λx : A => iprop(◇ F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x >H2
+  imodintro
+  iapply hf.monotone Φ Ψ
+  iexact H1
+  iexact H2
+
+instance antitone_except0 [BI PROP] [OFE A] (F : (A → PROP) → A → PROP)
+    [hf : AntitonePred F] : AntitonePred (λΦ : A → PROP => λx : A => iprop(◇ F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x >H2
+  imodintro
+  iapply hf.antitone Φ Ψ
+  iexact H1
+  iexact H2
+
+end except0
+
+section fupd
+
+instance monotone_fupd [BI PROP] [BIFUpdate PROP] [OFE A] (F : (A → PROP) → A → PROP)
+      (E1 E2 : A → CoPset) [hf : MonotonePred F] :
+    MonotonePred (λΦ : A → PROP => λx : A => fupd (E1 x) (E2 x) (F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  imod H2
+  imodintro
+  iapply hf.monotone Φ $$ H1 H2
+
+instance antitone_fupd [BI PROP] [BIFUpdate PROP] [OFE A] (F : (A → PROP) → A → PROP)
+      (E1 E2 : A → CoPset) [hf : AntitonePred F] :
+    AntitonePred (λΦ : A → PROP => λx : A => fupd (E1 x) (E2 x) (F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  imod H2
+  imodintro
+  iapply hf.antitone Φ $$ H1 H2
+
+end fupd
+
+section bupd
+
+instance monotone_bupd [BI PROP] [BIUpdate PROP] [OFE A] (F : (A → PROP) → A → PROP)
+      [hf : MonotonePred F] :
+    MonotonePred (λΦ : A → PROP => λx : A => iprop(|==> F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  imod H2
+  imodintro
+  iapply hf.monotone Φ $$ H1 H2
+
+instance antitone_bupd [BI PROP] [BIUpdate PROP] [OFE A] (F : (A → PROP) → A → PROP)
+      [hf : AntitonePred F] :
+    AntitonePred (λΦ : A → PROP => λx : A => iprop(|==> F Φ x)) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  imod H2
+  imodintro
+  iapply hf.antitone Φ $$ H1 H2
+
+end bupd
+
+section bigSepL
+
+instance monotone_bigSepL [BI PROP] [OFE A] (l : List B)
+      (F : Nat → B → (A → PROP) → A → PROP) [hf : ∀n y, MonotonePred (F n y)] :
+    MonotonePred (λΦ : A → PROP => λx : A => bigSepL (λn y => F n y Φ x) l) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  iapply BigSepL.bigSepL_impl (Φ := λn y => F n y Φ x) $$ H2
+  iintro !> %k %y #H2 H3
+  iapply (hf k y).monotone Φ $$ H1 H3
+
+instance antitone_bigSepL [BI PROP] [OFE A] (l : List B)
+      (F : Nat → B → (A → PROP) → A → PROP) [hf : ∀n y, AntitonePred (F n y)] :
+    AntitonePred (λΦ : A → PROP => λx : A => bigSepL (λn y => F n y Φ x) l) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  iapply BigSepL.bigSepL_impl (Φ := λn y => F n y Ψ x) $$ H2
+  iintro !> %k %y #H2 H3
+  iapply (hf k y).antitone Φ $$ H1 H3
+
+end bigSepL
+
+section bigSepL2
+
+instance monotone_bigSepL2 [BI PROP] [OFE A] (l1 : List B) (l2 : List C)
+      (F : Nat → B → C → (A → PROP) → A → PROP) [hf : ∀n y z, MonotonePred (F n y z)] :
+    MonotonePred (λΦ : A → PROP => λx : A => bigSepL2 (λn y z => F n y z Φ x) l1 l2) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  iapply BigSepL2.bigSepL2_impl (Φ := λn y z => F n y z Φ x) $$ H2
+  iintro !> %k %y %z #_ #_ H3
+  iapply (hf k y z).monotone Φ $$ H1 H3
+
+instance antitone_bigSepL2 [BI PROP] [OFE A] (l1 : List B) (l2 : List C)
+      (F : Nat → B → C → (A → PROP) → A → PROP) [hf : ∀n y z, AntitonePred (F n y z)] :
+    AntitonePred (λΦ : A → PROP => λx : A => bigSepL2 (λn y z => F n y z Φ x) l1 l2) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  iapply BigSepL2.bigSepL2_impl (Φ := λn y z => F n y z Ψ x) $$ H2
+  iintro !> %k %y %z #_ #_ H3
+  iapply (hf k y z).antitone Φ $$ H1 H3
+
+end bigSepL2
+
+section bigSepM
+
+instance monotone_bigSepM [BI PROP] [OFE A] [LawfulFiniteMap M K]
+      (m : M V) (F : K → V → (A → PROP) → A → PROP) [hf : ∀k v, MonotonePred (F k v)] :
+    MonotonePred (λΦ : A → PROP => λx : A => bigSepM (λk v => F k v Φ x) m) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  iapply BigSepM.bigSepM_impl (Φ := λk v => F k v Φ x) $$ H2
+  iintro !> %k %v #_ H3
+  iapply (hf k v).monotone Φ $$ H1 H3
+
+instance antitone_bigSepM [BI PROP] [OFE A] [LawfulFiniteMap M K]
+      (m : M V) (F : K → V → (A → PROP) → A → PROP) [hf : ∀k v, AntitonePred (F k v)] :
+    AntitonePred (λΦ : A → PROP => λx : A => bigSepM (λk v => F k v Φ x) m) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  iapply BigSepM.bigSepM_impl (Φ := λk v => F k v Ψ x) $$ H2
+  iintro !> %k %v #_ H3
+  iapply (hf k v).antitone Φ $$ H1 H3
+
+end bigSepM
+
+section bigSepS
+
+instance monotone_bigSepS [BI PROP] [OFE A] [LawfulFiniteSet S B] (X : S)
+      (F : B → (A → PROP) → A → PROP) [hf : ∀y, MonotonePred (F y)] :
+    MonotonePred (λΦ : A → PROP => λx : A => bigSepS (λy => F y Φ x) X) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  iapply BigSepS.bigSepS_impl (Φ := λy => F y Φ x) $$ H2
+  iintro !> %y #_ H3
+  iapply (hf y).monotone Φ $$ H1 H3
+
+instance antitone_bigSepS [BI PROP] [OFE A] [LawfulFiniteSet S B] (X : S)
+      (F : B → (A → PROP) → A → PROP) [hf : ∀y, AntitonePred (F y)] :
+    AntitonePred (λΦ : A → PROP => λx : A => bigSepS (λy => F y Φ x) X) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  iapply BigSepS.bigSepS_impl (Φ := λy => F y Ψ x) $$ H2
+  iintro !> %y #_ H3
+  iapply (hf y).antitone Φ $$ H1 H3
+
+end bigSepS
+
+section bigSepMS
+
+instance monotone_bigSepMS [BI PROP] [OFE A] [LawfulFiniteMultiSet MS B] (X : MS)
+      (F : B → (A → PROP) → A → PROP) [hf : ∀y, MonotonePred (F y)] :
+    MonotonePred (λΦ : A → PROP => λx : A => bigSepMS (λy => F y Φ x) X) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  iapply BigSepMS.bigSepMS_impl (Φ := λy => F y Φ x) $$ H2
+  iintro !> %y #_ H3
+  iapply (hf y).monotone Φ $$ H1 H3
+
+instance antitone_bigSepMS [BI PROP] [OFE A] [LawfulFiniteMultiSet MS B] (X : MS)
+      (F : B → (A → PROP) → A → PROP) [hf : ∀y, AntitonePred (F y)] :
+    AntitonePred (λΦ : A → PROP => λx : A => bigSepMS (λy => F y Φ x) X) := by
+  constructor
+  intros Φ Ψ
+  iintro #H1 %x H2
+  iapply BigSepMS.bigSepMS_impl (Φ := λy => F y Ψ x) $$ H2
+  iintro !> %y #_ H3
+  iapply (hf y).antitone Φ $$ H1 H3
+
+end bigSepMS
diff --git a/Iris/Iris/Instances/Lib/NaInvariants.lean b/Iris/Iris/Instances/Lib/NaInvariants.lean
index f3ff10010..fd750b613 100644
--- a/Iris/Iris/Instances/Lib/NaInvariants.lean
+++ b/Iris/Iris/Instances/Lib/NaInvariants.lean
@@ -65,10 +65,7 @@ instance instTimeless_own (p : NaInvPoolName) (E : CoPset) : Timeless (own (GF :
 @[rocq_alias na_inv_contractive]
 instance instContractive_inv (p : NaInvPoolName) (N : Namespace) :
     Contractive (inv (GF := GF) p N) where
-  distLater_dist {n x y} H := by
-    refine exists_ne fun i => and_ne.ne .rfl ?_
-    refine Contractive.distLater_dist fun m hm => ?_
-    exact or_ne.ne (sep_ne.ne (H _ hm) .rfl) .rfl
+  distLater_dist := by contractive
 
 @[rocq_alias na_inv_ne]
 instance instNonExpansive_inv (p : NaInvPoolName) (N : Namespace) : NonExpansive (inv (GF := GF) p N) :=
diff --git a/Iris/Iris/Instances/Lib/WSat.lean b/Iris/Iris/Instances/Lib/WSat.lean
index e93f80c16..0d030c7e5 100644
--- a/Iris/Iris/Instances/Lib/WSat.lean
+++ b/Iris/Iris/Instances/Lib/WSat.lean
@@ -89,12 +89,7 @@ def wsat : IProp GF := iprop(
 
 @[rocq_alias ownI_contractive]
 instance (i : Pos) : Contractive (ownI (W := W) i) where
-  distLater_dist h := by
-    unfold ownI
-    refine NonExpansive.ne ?_
-    refine NonExpansive.ne ?_
-    refine NonExpansive.ne ?_
-    exact Contractive.distLater_dist h
+  distLater_dist := by contractive
 
 @[rocq_alias ownI_persistent]
 instance (i : Pos) (P : IProp GF) : Persistent (ownI (W := W) i P) := by
diff --git a/Iris/Iris/ProgramLogic/TotalWeakestPre.lean b/Iris/Iris/ProgramLogic/TotalWeakestPre.lean
new file mode 100644
index 000000000..6f3496330
--- /dev/null
+++ b/Iris/Iris/ProgramLogic/TotalWeakestPre.lean
@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Fernando Leal, Oliver Soeser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+module
+
+public import Iris.ProgramLogic.WeakestPre
+public import Iris.ProofMode.Tactics.Monotone
+public import Iris.BI.Lib.Fixpoint
+
+namespace Iris
+
+open ProgramLogic Language.Notation Std
+
+@[expose] public section
+
+export StateInterp (stateInterp)
+
+variable {hlc : outParam HasLC} {Expr State Obs Val}
+variable [Λ : Language Expr State Obs Val]
+variable {GF : BundledGFunctors} [ι : IrisGS_gen hlc Expr GF]
+
+abbrev Stuckness.MaybeReducibleNoObs : Stuckness → Expr × State → Prop
+| .NotStuck, (e₁, σ₁) => PrimStep.ReducibleNoObs (e₁, σ₁)
+| _, _ => True
+
+@[rocq_alias twp_pre]
+def twp.pre (s : Stuckness) (wp : CoPset -> Expr -> (Val -> IProp GF) -> IProp GF) (E : CoPset)
+    (e₁ : Expr) (Φ : Val -> IProp GF) : IProp GF :=
+  match toVal e₁ with
+  | some v => iprop(|={E}=> Φ v)
+  | none => iprop(∀ (σ₁ : State) (ns : Nat) (obs' : List Obs) (nt : Nat),
+    stateInterp σ₁ ns obs' nt ={E,∅}=∗
+    ⌜s.MaybeReducibleNoObs (e₁, σ₁)⌝ ∗
+    ∀ obs e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<obs>-> (e₂, σ₂, eₜ)⌝ ={E,∅}=∗
+      ⌜obs = []⌝ ∗ stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗
+      wp E e₂ Φ ∗ [∗list] e' ∈ eₜ, wp ⊤ e' ι.forkPost)
+
+open Function in
+@[rocq_alias twp_pre']
+def twp.pre' (s : Stuckness) (wp : (CoPset × Expr) × (Val -> IProp GF) -> IProp GF) :=
+    uncurry <| uncurry <| @twp.pre hlc Expr State Obs Val Λ GF ι s (curry <| curry wp)
+
+instance twp.pre_mono' [OFE Expr] [OFE CoPset] [OFE.Discrete Expr] [OFE.Discrete CoPset]
+    (s : Stuckness) : BIMonoPred (@twp.pre' hlc Expr State Obs Val Λ GF ι s) where
+  mono_pred := by monotone
+  mono_pred_ne := by nonexp
+
+def twp.def [OFE Expr] [OFE CoPset] (s : Stuckness) (E : CoPset)
+    (e : Expr) (Φ : Val → IProp GF) := bi_least_fixpoint (twp.pre' s) ((E, e), Φ)
diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean
index 1e34f6685..7f62c82e4 100644
--- a/Iris/Iris/ProgramLogic/WeakestPre.lean
+++ b/Iris/Iris/ProgramLogic/WeakestPre.lean
@@ -84,35 +84,7 @@ def wp.pre (s : Stuckness) (wp : CoPset -> Expr -> (Val -> IProp GF) -> IProp GF
 
 @[rocq_alias wp_pre_contractive]
 instance wp.pre.contractive s : OFE.Contractive (wp.pre s (ι := ι)) where
-  distLater_dist := by
-    intros n wp wp' Hwp E e₁ Φ
-    unfold pre
-    cases toVal e₁
-    case some _ =>
-      exact .rfl
-    case none =>
-      refine BI.forall_ne (fun σ₁ => ?_)
-      refine BI.forall_ne (fun ns => ?_)
-      refine BI.forall_ne (fun obs => ?_)
-      refine BI.forall_ne (fun obs' => ?_)
-      refine BI.forall_ne (fun nt => ?_)
-      refine BI.wand_ne.ne .rfl ?_
-      refine BIFUpdate.ne.ne ?_
-      refine BI.sep_ne.ne .rfl ?_
-      refine BI.forall_ne (fun e₂  => ?_)
-      refine BI.forall_ne (fun σ₂ => ?_)
-      refine BI.forall_ne (fun eₜ => ?_)
-      refine BI.wand_ne.ne .rfl ?_
-      refine BI.wand_ne.ne .rfl ?_
-      refine BIFUpdate.ne.ne ?_
-      refine OFE.Contractive.distLater_dist fun m m_n => ?_
-      refine BIFUpdate.ne.ne ?_
-      refine step_fupdN_ne.ne ?_
-      refine BIFUpdate.ne.ne ?_
-      refine BI.sep_ne.ne .rfl ?_
-      refine BI.sep_ne.ne ?_ ?_
-      · exact Hwp m m_n _ _ _
-      · exact BI.BigSepL.bigSepL_dist <| fun _ => Hwp m m_n _ _ _
+  distLater_dist := by contractive
 
 @[rocq_alias wp_def]
 instance wp.def : Wp (IProp GF) (Expr) (Val) Stuckness where
@@ -168,25 +140,7 @@ theorem wp_contractive (s : Stuckness) E (e : Expr) (h : toVal e = none) :
   distLater_dist {n Φ₁ Φ₂} HΦ := by
     simp only [wp_unfold.to_eq]
     simp only [wp.pre, h]
-    refine BI.forall_ne fun σ₁ => ?_
-    refine BI.forall_ne fun ns => ?_
-    refine BI.forall_ne fun obs => ?_
-    refine BI.forall_ne fun obs' => ?_
-    refine BI.forall_ne fun nt => ?_
-    refine BI.wand_ne.ne .rfl ?_
-    refine BIFUpdate.ne.ne ?_
-    refine BI.sep_ne.ne .rfl ?_
-    refine BI.forall_ne fun e₂  => ?_
-    refine BI.forall_ne fun σ₂ => ?_
-    refine BI.forall_ne fun eₜ => ?_
-    refine BI.wand_ne.ne .rfl ?_
-    refine BI.wand_ne.ne .rfl ?_
-    refine step_fupdN_contractive.distLater_dist fun m n_m => ?_
-    refine BIFUpdate.ne.ne ?_
-    refine BI.sep_ne.ne .rfl ?_
-    refine BI.sep_ne.ne ?_ .rfl
-    refine wp_ne.ne ?_
-    exact HΦ m n_m
+    contractive
 
 @[rocq_alias wp_value_fupd']
 theorem wp_value_fupd' {s : Stuckness} {E} {Φ : Val → IProp GF} {v : Val} :
diff --git a/Iris/Iris/ProofMode/Tactics.lean b/Iris/Iris/ProofMode/Tactics.lean
index 12556fbe9..2f2b321dc 100644
--- a/Iris/Iris/ProofMode/Tactics.lean
+++ b/Iris/Iris/ProofMode/Tactics.lean
@@ -8,6 +8,7 @@ public meta import Iris.ProofMode.Tactics.Basic
 public meta import Iris.ProofMode.Tactics.Cases
 public meta import Iris.ProofMode.Tactics.Clear
 public meta import Iris.ProofMode.Tactics.Combine
+public meta import Iris.ProofMode.Tactics.Contractive
 public meta import Iris.ProofMode.Tactics.Eval
 public meta import Iris.ProofMode.Tactics.Exact
 public meta import Iris.ProofMode.Tactics.ExFalso
diff --git a/Iris/Iris/ProofMode/Tactics/Contractive.lean b/Iris/Iris/ProofMode/Tactics/Contractive.lean
new file mode 100644
index 000000000..f94749d8c
--- /dev/null
+++ b/Iris/Iris/ProofMode/Tactics/Contractive.lean
@@ -0,0 +1,237 @@
+/-
+Copyright (c) 2026 Oliver Soeser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Soeser
+-/
+module
+
+public meta import Iris.Algebra.OFE
+meta import Lean.Meta.Tactic.Split
+
+namespace Iris
+
+open Lean Elab Tactic Meta Term Iris.Std
+
+meta def nonexpLemmas : MetaM (Array Name) := do
+  let env ← getEnv
+  return (nonexpExt.getState env).reverse
+
+/-- Does `e` use the pointwise (`∀`) OFE instance? -/
+meta def distIsForall (e : Expr) : MetaM Bool := do
+  let some inst := e.getAppArgs[1]? | return false
+  return inst.getAppFn.getLambdaBody.getAppFn.isConstOf ``OFE.instForallOfOFEFun
+
+/-- Applying a hypothesis of a given type. -/
+meta def applyHypStep (type : Name) (goal : MVarId) : TermElabM (Option (List MVarId)) :=
+  goal.withContext do
+    for decl? in (← getLCtx).decls do
+      if let some decl := decl? then
+        if decl.type.isAppOf type then try
+            match ← goal.apply decl.toExpr with
+            | [] => return some []
+            | head :: tail =>
+              head.assumption
+              return some tail
+          catch _ => continue
+    return none
+
+meta def distLaterStep (goal : MVarId) : TermElabM (Option (List MVarId)) :=
+  applyHypStep ``OFE.DistLater goal
+
+meta def distCarrier (h : Expr) : MetaM (Option Expr) := do
+  return (← instantiateMVars (← inferType h)).getAppArgs[0]?
+
+meta partial def distProjections (h : Expr) : MetaM (Array Expr) := do
+  let some A ← distCarrier h | return #[h]
+  if A.isAppOfArity ``Prod 2 then
+    let hf ← mkAppM ``OFE.dist_fst #[h]
+    let hs ← mkAppM ``OFE.dist_snd #[h]
+    return #[h] ++ (← distProjections hf) ++ (← distProjections hs)
+  else
+    return #[h]
+
+meta def distStep (goal : MVarId) : TermElabM (Option (List MVarId)) :=
+  goal.withContext do
+    for decl? in (← getLCtx).decls do
+      if let some decl := decl? then
+        if decl.type.isAppOf ``OFE.Dist then
+          for cand in ← distProjections decl.toExpr do try
+              match ← goal.apply cand with
+              | [] => return some []
+              | head :: tail =>
+                head.assumption
+                return some tail
+            catch _ => continue
+    return none
+
+meta partial def discreteEqs (h : Expr) : MetaM (Array Expr) := do
+  try
+    return #[← mkAppM ``OFE.Discrete.discrete #[h]]
+  catch _ =>
+    let some A ← distCarrier h | return #[]
+    if A.isAppOfArity ``Prod 2 then
+      let hf ← mkAppM ``OFE.dist_fst #[h]
+      let hs ← mkAppM ``OFE.dist_snd #[h]
+      return (← discreteEqs hf) ++ (← discreteEqs hs)
+    else
+      return #[]
+
+meta def discreteAlignStep (goal : MVarId) : TermElabM (Option (List MVarId)) :=
+  goal.withContext do
+    let mut eqs : Array Expr := #[]
+    for decl? in (← getLCtx).decls do
+      if let some decl := decl? then
+        if decl.type.isAppOf ``OFE.Dist then
+          eqs := eqs ++ (← discreteEqs decl.toExpr)
+    if eqs.isEmpty then return none
+    try
+      let eqStxs ← eqs.mapM exprToSyntax
+      let goals ← Elab.Tactic.run goal <| evalTactic <| ← `(tactic|simp only [$[$eqStxs:term],*])
+      return some goals
+    catch _ => return none
+
+meta def splitMatchStep (goal : MVarId) : TermElabM (Option (List MVarId)) := do
+  try
+    let goals ← Elab.Tactic.run goal <| evalTactic <| ← `(tactic|split <;> try simp_all)
+    return some goals
+  catch _ => return none
+
+meta def isPrimitive (fn : Name) : MetaM Bool := do
+  return (`Iris.BI.BIBase).isPrefixOf fn || (← getProjectionFnInfo? fn).any (·.fromClass)
+
+meta def unfoldHeadStep (goal : MVarId) : TermElabM (Option (List MVarId)) :=
+  goal.withContext do
+    let some fnArg := (← instantiateMVars (← goal.getType)).getAppArgs[3]? | return none
+    let .const fn _ := fnArg.getAppFn | return none
+    if ← isPrimitive fn then return none
+    try
+      let goals ← Elab.Tactic.run goal <| evalTactic <| ← `(tactic|unfold $(mkIdent fn))
+      return some goals
+    catch _ => return none
+
+meta def distInstanceStep (goal : MVarId) : TermElabM (Option (List MVarId)) := do try
+    match ← goal.applyConst ``OFE.Contractive.distLater_dist with
+    | [] => return some []
+    | head :: tail =>
+      let (_, head) ← head.introN 2
+      return some (head :: tail)
+  catch _ => return none
+
+meta def nonexpStep (goal : MVarId) : TermElabM (Option (List MVarId)) := do
+  for neLem in ← nonexpLemmas do try
+      let goals ← Elab.Tactic.run goal <| evalTactic <| ← `(tactic|apply $(mkIdent neLem))
+      match goals with
+      | [] => return some []
+      | head :: tail =>
+        let (_, head) ← head.intros
+        return some (head :: tail)
+    catch _ => continue
+  return none
+
+meta def tryUnfoldFn : TacticM Unit := do
+  let _ ← observing? do
+    let some fnArg := (← getMainTarget).getAppArgs[3]? | return
+    match fnArg.getAppFn with
+    | .const fn _ =>
+      -- don't unfold primitives
+      if not <| (`Iris.BI.BIBase).isPrefixOf fn then
+        evalTactic <| ← `(tactic|unfold $(mkIdent fn); try split)
+    | _ => return
+
+meta def makeMainGoal (goal : MVarId) : TacticM Unit := do
+  let goals ← getGoals
+  let goals := goal :: goals.erase goal
+  setGoals goals
+
+meta def tryStep (recurse : MVarId → TacticM Unit)
+    (step : MVarId → TermElabM (Option (List MVarId))) (goal : MVarId) : TacticM Bool := do
+  match ← step goal with
+  | some newGoals =>
+    replaceMainGoal newGoals
+    discard <| newGoals.mapM recurse
+    return true
+  | none => return false
+
+meta def simpThenRecurse (k : MVarId → TacticM Unit) : TacticM Bool := do
+  if let some _ ← observing? (evalTactic <| ← `(tactic|simp [Function.uncurry, Function.curry])) then
+    if let some newGoal ← observing? getMainGoal then
+      k newGoal
+    return true
+  return false
+
+meta partial def contractiveMain (goal : MVarId) (guarded : Bool) : TacticM Unit := do
+  if ← goal.isAssigned then return
+  makeMainGoal goal
+
+  -- simplification step (includes application of Dist.rfl)
+  if ← simpThenRecurse (contractiveMain · guarded) then return
+
+  -- uses an OFE.Contractive instance
+  if not guarded then
+    if ← tryStep (contractiveMain · true) distInstanceStep goal then return
+
+  -- applies an OFE.DistLater hypothesis
+  if ← tryStep (contractiveMain · guarded) distLaterStep goal then return
+
+  -- applies a non-expansive lemma
+  if ← tryStep (contractiveMain · guarded) nonexpStep goal then return
+
+  throwError "tactic 'contractive' failed"
+
+meta partial def nonexpMain (goal : MVarId) : TacticM Unit := do
+  if ← goal.isAssigned then return
+  makeMainGoal goal
+
+  -- simplification step (includes application of Dist.rfl)
+  if ← simpThenRecurse nonexpMain then return
+
+  -- deal with uncurried functions
+  if ← tryStep nonexpMain discreteAlignStep goal then return
+
+  -- split goal by cases
+  if ← tryStep nonexpMain splitMatchStep goal then return
+
+  -- applies an OFE.Dist hypothesis
+  if ← tryStep nonexpMain distStep goal then return
+
+  -- applies a non-expansive lemma
+  if ← tryStep nonexpMain nonexpStep goal then return
+
+  -- unfolds further if needed
+  if ← tryStep nonexpMain unfoldHeadStep goal then return
+
+  throwError "tactic 'nonexp' failed"
+
+meta def contractiveSetup : TacticM Unit := do
+  evalTactic <| ← `(tactic|intros)
+
+  while ← distIsForall <| ← getMainTarget do
+    evalTactic <| ← `(tactic|intro)
+
+  tryUnfoldFn
+
+meta def isNonExpansiveGoal : TacticM Bool := do
+  let target ← getMainTarget
+  return target.isAppOf ``OFE.NonExpansive || target.isAppOf ``OFE.NonExpansive₂
+
+meta def nonexpSetup : TacticM Unit := do
+  evalTactic <| ← `(tactic|intros)
+
+  while ← isNonExpansiveGoal do
+    evalTactic <| ← `(tactic|constructor)
+    evalTactic <| ← `(tactic|intros)
+
+  while ← distIsForall <| ← getMainTarget do
+    evalTactic <| ← `(tactic|intro)
+
+  tryUnfoldFn
+
+elab "contractive" : tactic => do
+  contractiveSetup
+  contractiveMain (← getMainGoal) false
+
+elab "nonexp" : tactic => do
+  nonexpSetup
+  nonexpMain (← getMainGoal)
+
+end Iris
diff --git a/Iris/Iris/ProofMode/Tactics/Monotone.lean b/Iris/Iris/ProofMode/Tactics/Monotone.lean
new file mode 100644
index 000000000..01dad4dbe
--- /dev/null
+++ b/Iris/Iris/ProofMode/Tactics/Monotone.lean
@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026 Oliver Soeser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Soeser
+-/
+module
+
+public meta import Iris.Instances.Lib.Monotone
+public meta import Iris.ProofMode
+meta import Lean.Meta.Tactic.Split
+meta import Lean.Meta.Tactic.Repeat
+
+namespace Iris
+
+open Lean Elab Tactic Meta Iris.Std ProofMode Term Macro
+
+meta partial def etaExpand (e : Expr) : TacticM Unit := do
+  let ty ← whnf (← instantiateMVars (← inferType e))
+  if ty.isAppOf ``Prod then
+    let stx ← exprToSyntax e
+    evalTactic (← `(tactic| rw [← Prod.eta $stx]))
+    etaExpand (← mkAppM ``Prod.fst #[e])
+    etaExpand (← mkAppM ``Prod.snd #[e])
+
+/-- The RHS of the goal's entailment. -/
+meta def goalRHS? (goal : MVarId) : MetaM (Option Expr) := goal.withContext do
+  let target ← instantiateMVars (← goal.getType)
+  target.withApp fun _ args => pure args[3]?
+
+/-- If the goal contains a pattern match, case on the discriminant. -/
+meta def splitStep (xType : Expr) (name : Name) (goal : MVarId) : TacticM (List MVarId) := do
+  let some wandGoal ← goalRHS? goal | throwError "monotone: no match to split"
+
+  -- find discriminants
+  let some e ← findSplit? wandGoal .match | throwError "monotone: no match to split"
+  let some app ← matchMatcherApp? e | throwError "monotone: no match to split"
+  if app.discrs.isEmpty then throwError "monotone: no match to split"
+  let stxs ← goal.withContext (app.discrs.mapM exprToSyntax : TermElabM (Array Term))
+
+  let goals ← Elab.Tactic.run goal <| evalTactic <| ← `(tactic| cases $[$stxs:term],*)
+  let goals ← (goals.mapM Split.simpMatchTarget : MetaM (List MVarId))
+
+  -- keep `x` available for use by `irevert` by renaming
+  goals.mapM fun g => g.withContext do
+    for decl in (← getLCtx) do
+      if !decl.isImplementationDetail && (← isDefEq decl.type xType) then
+        return ← g.rename decl.fvarId name
+    return g
+
+/-- Check if `fn` is a primitive connective that can be dealt with by typeclass search. -/
+meta def isPrimitiveConnective (fn : Name) : MetaM Bool := do
+  return (`Iris.BI.BIBase).isPrefixOf fn || (← getProjectionFnInfo? fn).any (·.fromClass)
+
+meta def unfoldStep (goal : MVarId) : TacticM (List MVarId) := do
+  let some wandGoal ← goalRHS? goal | throwError "monotone: nothing to unfold"
+  let some fn := wandGoal.withApp fun _ args => (args[2]?.map (·.getAppFn)).bind (·.constName?)
+    | throwError "monotone: nothing to unfold"
+  if ← isPrimitiveConnective fn then
+    throwError "monotone: {fn} is a primitive connective"
+  run goal <| evalTactic <| ← `(tactic|unfold $(mkIdent fn); try simp)
+
+/-- Split if possible, otherwise unfold the goal -/
+meta def monotoneStep (xType : Expr) (name : Name) (goal : MVarId) : TacticM (List MVarId) := do
+  if let some goals ← observing? (splitStep xType name goal) then
+    return goals
+  else
+    unfoldStep goal
+
+elab "monotone" : tactic => do
+  let H ← `(icasesPat| H)
+  let H' ← `(selPat| H)
+  let x ← `(ident| x)
+
+  -- introduce hypotheses
+  evalTactic <| ← `(tactic|intros; iintro #$H %$x)
+
+  let xType ← withMainContext <| inferType (mkFVar (← getFVarId x))
+
+  -- eta-expand the argument
+  withMainContext do
+    let e := mkFVar (← getFVarId x)
+    etaExpand e
+
+  -- unfold and split as much as possible
+  let newGoals ← repeat' (monotoneStep xType x.getId) [← getMainGoal]
+  setGoals newGoals
+
+  -- get the goal in the right form and use typeclass search
+  evalTactic <| ← `(tactic|all_goals (irevert $H' %$x; apply MonotonePred.monotone))
diff --git a/Iris/Iris/Std/NonExp.lean b/Iris/Iris/Std/NonExp.lean
new file mode 100644
index 000000000..ddf188f13
--- /dev/null
+++ b/Iris/Iris/Std/NonExp.lean
@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2026 Oliver Soeser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Soeser
+-/
+module
+
+public meta import Lean.Meta
+
+public meta section
+
+namespace Iris.Std
+open Lean Meta
+
+meta initialize nonexpExt :
+    SimpleScopedEnvExtension Name (Array Name) ←
+  registerSimpleScopedEnvExtension {
+    addEntry := λ arr n => arr.push n
+    initial := #[]
+  }
+
+meta initialize registerBuiltinAttribute {
+  name := `non_exp
+  descr := "Non-expansiveness lemmas to be used by the non-expansiveness and contractiveness solvers"
+  add := λ decl _ kind => nonexpExt.add decl kind
+}
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 1303d235d..fea7b6d22 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -18,6 +18,8 @@ public import Iris.Instances.Lib.CInvariants
 public import Iris.Instances.Lib.NaInvariants
 public import Iris.ProgramLogic.Language
 public import Iris.ProgramLogic.WeakestPre
+public import Iris.Instances.Lib.Monotone
+public meta import Iris.ProofMode.Tactics.Monotone
 
 @[expose] public section
 
@@ -2789,8 +2791,7 @@ example (P Q : PROP) :
   iintro #HPQ HQ !>
   inext
   irewrite [HPQ] at HQ
-  · exact ⟨fun _ _ _ h => affinely_ne.ne h⟩
-  · iexact HQ
+  iexact HQ
 
 /- Tests `irewrite` under affine and later backwards. -/
 example (P Q : PROP) :
@@ -2798,8 +2799,7 @@ example (P Q : PROP) :
   iintro #HPQ HQ !>
   inext
   irewrite [←HPQ] at HQ
-  · exact ⟨fun _ _ _ h => affinely_ne.ne h⟩
-  · iexact HQ
+  iexact HQ
 
 /- Tests `irewrite` with no matching target. -/
 /--
@@ -4195,3 +4195,87 @@ example [BI PROP] {P : PROP} {m n : Nat} {T : Nat → Prop}
   | succ n IH => itrivial
 
 end iinduction
+
+section contractive
+
+open OFE
+
+variable [OFE α] [BI PROP] [BILaterContractive PROP]
+
+/- Identity is non-expansive. -/
+example : NonExpansive (fun x : α => x) where
+  ne := by nonexp
+
+/- Constant functions are non-expansive. -/
+example (y : α) : NonExpansive (fun _ : α => y) where
+  ne := by nonexp
+
+/- A non-expansive function with every occurrence of `x` guarded by ▷. -/
+example (f : PROP → PROP) [NonExpansive f] : Contractive (fun x => iprop(▷ (f x))) where
+  distLater_dist := by contractive
+
+/- A non-expansive function remains contractive under additional ▷s. -/
+example (f : PROP → PROP) [NonExpansive f] : Contractive (fun x => iprop(▷ ▷ (f x))) where
+  distLater_dist := by contractive
+
+/- A contractive function is also non-expansive. -/
+example (f : α → α) [Contractive f] : NonExpansive f where
+  ne := by nonexp
+
+/- Fails because `x` occurs outside a ▷. -/
+/-- error: tactic 'contractive' failed -/
+#guard_msgs in
+example : Contractive (fun x : α => x) where
+  distLater_dist := by
+    contractive
+
+/- Fails because one occurrence of `x` is unguarded. -/
+/-- error: tactic 'contractive' failed -/
+#guard_msgs in
+example (f : α → α) [Contractive f] : Contractive (fun x => (f x, x)) where
+  distLater_dist := by
+    contractive
+
+end contractive
+
+section monotone
+open OFE
+
+variable [BI PROP] [OFE α]
+
+/-- Tests `monotone` closing a goal already in the right form. -/
+example : MonotonePred (PROP := PROP) (A := α) (fun Φ x => iprop(Φ x ∗ Φ x)) where
+  monotone := by monotone
+
+private def wrap0 (wp : α → PROP) (x : α) : PROP := iprop(wp x ∗ wp x)
+private def wrap1 (wp : α → PROP) : α → PROP := wrap0 wp
+private def wrap2 (wp : α → PROP) : α → PROP := wrap1 wp
+
+/-- Tests `monotone` unfolding. -/
+example : MonotonePred (PROP := PROP) (A := α) wrap2 where
+  monotone := by monotone
+
+private def stepPre (wp : α × Option α → PROP) (x : α × Option α) : PROP :=
+  match x.2 with
+  | none => iprop(wp (x.1, none) ∨ wp (x.1, none))
+  | some _ => iprop(wp (x.1, none) ∗ wp (x.1, none))
+
+/-- Tests `monotone` on matches on projections. -/
+example : MonotonePred (PROP := PROP) (A := α × Option α) stepPre where
+  monotone := by monotone
+
+/-- Tests `monotone` directly on a bare entailment goal of right shape. -/
+example (Φ Ψ : α × Option α → PROP) :
+    ⊢ (□ ∀ x, Φ x -∗ Ψ x) -∗ ∀ x, stepPre Φ x -∗ stepPre Ψ x := by
+  monotone
+
+private def choicePre (wp : α × (α ⊕ α) → PROP) (x : α × (α ⊕ α)) : PROP :=
+  match x.2 with
+  | .inl a => iprop(wp (x.1, .inr a) ∨ wp (x.1, .inr a))
+  | .inr a => iprop(wp (x.1, .inl a) ∨ wp (x.1, .inl a))
+
+/-- Tests `monotone` on a non-`Option` type match. -/
+example : MonotonePred (PROP := PROP) (A := α × (α ⊕ α)) choicePre where
+  monotone := by monotone
+
+end monotone