diff --git a/Iris/Iris/Algebra/Auth.lean b/Iris/Iris/Algebra/Auth.lean
index ff13f4b6b..01978bd4e 100644
--- a/Iris/Iris/Algebra/Auth.lean
+++ b/Iris/Iris/Algebra/Auth.lean
@@ -137,7 +137,12 @@ nonrec theorem auth_dfrac_op {dq1 dq2 : DFrac F} {a : A} :
     (●{dq1 • dq2} a) ≡ (●{dq1} a) • (●{dq2} a) :=
   auth_op_auth_eqv
 
--- TODO: auth_auth_dfrac_is_op
+@[rocq_alias auth_auth_dfrac_is_op]
+instance {dq dq1 dq2 : DFrac F} [h : IsOp merge dq dq1 dq2] :
+    IsOp io (●{dq} a : Auth F A) (●{dq1} a) (●{dq2} a) where
+  is_op := by
+    rw [h.is_op]
+    apply auth_dfrac_op
 
 @[rocq_alias auth_frag_op]
 theorem frag_op {b1 b2 : A} : (◯ (b1 • b2) : Auth F A) = ((◯ b1 : Auth F A) • ◯ b2) :=
@@ -174,7 +179,11 @@ nonrec instance {a : A} {b : A} [CoreId b] :
     CoreId ((●{.discard} a : Auth F A) • ◯ b) :=
   instCoreIdOpAuthDiscardFrag
 
--- TODO: auth_frag_is_op
+@[rocq_alias auth_frag_is_op]
+instance {a b1 b2 : A} [h : IsOp merge a b1 b2] :
+    IsOp io (◯ a : Auth F A) (◯ b1) (◯ b2) where
+  is_op := ⟨⟨⟩, h.is_op⟩
+
 -- TODO: auth_frag_sep_homomorphism
 
 /- TODO: BigOPs
diff --git a/Iris/Iris/Algebra/DFrac.lean b/Iris/Iris/Algebra/DFrac.lean
index 30fe47d6b..3d3fef2d2 100644
--- a/Iris/Iris/Algebra/DFrac.lean
+++ b/Iris/Iris/Algebra/DFrac.lean
@@ -10,6 +10,7 @@ public import Iris.Algebra.OFE
 public import Iris.Algebra.Frac
 public import Iris.Algebra.Updates
 public import Iris.Algebra.LocalUpdates
+public import Iris.Algebra.IsOp
 meta import Iris.Std.RocqPorting
 
 @[expose] public section
@@ -32,7 +33,7 @@ instance : OFE.Discrete (DFrac F) := ⟨congrArg id⟩
 
 namespace DFrac
 
-open DFrac Fraction OFE.Discrete
+open DFrac Fraction OFE.Discrete IsOp
 
 variable [UFraction F]
 
@@ -220,4 +221,12 @@ theorem DFrac.update_acquire [IsSplitFraction F] :
     rw [← add_assoc, IsSplitFraction.split_add]
     exact HP
 
+@[rocq_alias dfrac_op_own]
+theorem op_own (f f' : F) : own f • own f' = own (f + f') := rfl
+
+@[rocq_alias dfrac_is_op]
+instance isOp_dfrac_own {q q1 q2 : Frac F} [h : IsOp merge q q1 q2] :
+    IsOp io (own q.car) (own q1.car) (own q2.car) where
+  is_op := by rw [h.is_op]; rfl
+
 end DFrac
diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean
index 2ba970d54..3dfebac80 100644
--- a/Iris/Iris/Algebra/Frac.lean
+++ b/Iris/Iris/Algebra/Frac.lean
@@ -7,6 +7,7 @@ module
 
 public import Iris.Algebra.CMRA
 public import Iris.Algebra.OFE
+public import Iris.Algebra.IsOp
 
 /-!
 # The Frac CMRA
diff --git a/Iris/Iris/Algebra/IsOp.lean b/Iris/Iris/Algebra/IsOp.lean
new file mode 100644
index 000000000..67f70cda4
--- /dev/null
+++ b/Iris/Iris/Algebra/IsOp.lean
@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2026 Alvin Tang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler, Alvin Tang
+-/
+module
+
+public import Iris.Algebra.CMRA
+public import Iris.ProofMode.SynthInstanceAttr
+meta import Iris.Std.RocqPorting
+
+@[expose] public section
+
+namespace Iris
+
+open CMRA ProofMode
+
+section IsOp
+
+/--
+  A type class that allows merging `b1` and `b2` into `a` as well as
+  to split `a` into `b1` and `b2`.
+-/
+@[ipm_class, rocq_alias IsOp, rocq_alias IsOp', rocq_alias IsOp'LR]
+class IsOp [CMRA α]
+    (_ : InOut) (a : semiOutParam $ α)
+    (b1 : uncheckedInParam α) (b2 : uncheckedInParam α) where
+  is_op : a ≡ b1 • b2
+
+/--
+  Syntactic sugar for specifying whether `IsOp` is used for merging or splitting.
+-/
+macro_rules
+  | `(IsOp merge $a $b1 $b2) => `(IsOp .out $a $b1 $b2)
+  | `(IsOp split $a $b1 $b2) => `(IsOp .in $a $b1 $b2)
+
+/--
+  Merging with `•` should have the lowest priority.
+-/
+@[rocq_alias is_op_op]
+instance (priority := default - 100) isOp_op [CMRA α] (a b : α) :
+    IsOp merge (a • b) a b where
+  is_op := .rfl
+
+/--
+  Splitting with `•` should have the highest priority.
+-/
+@[rocq_alias is_op_lr_op]
+instance (priority := default + 100) isOpSplit_op [CMRA α] (a b : α) :
+    IsOp split (a • b) a b where
+  is_op := .rfl
+
+/-
+  The following type class instances were originally defined in terms of
+  both `IsOp` and `IsOp'`. The distinction between `IsOp` and `IsOp'` is no
+  longer relevant in Lean, and we use `InOut` instead.
+
+  Note that in the Rocq formulation, the assumptions use `IsOp` while
+  the conclusion use `IsOp'`. We therefore use `merge` for the assumptions
+  but allow any `InOut` value for the conclusion.
+-/
+
+@[rocq_alias is_op_pair]
+instance isOpMerge_pair [CMRA α] {io : InOut}
+    (a b1 b2 : α) (a' b1' b2' : α)
+    [h1 : IsOp merge a b1 b2] [h2 : IsOp merge a' b1' b2'] :
+    IsOp io (a, a') (b1, b1') (b2, b2') where
+  is_op := ⟨h1.is_op, h2.is_op⟩
+
+@[rocq_alias is_op_pair_core_id_l]
+instance isOpMerge_pair_core_id_l [CMRA α] [CMRA β] {io : InOut}
+    (a : α) (a' b1' b2' : β) [h1 : CoreId a] [h2 : IsOp merge a' b1' b2'] :
+    IsOp io (a, a') (a, b1') (a, b2') where
+  is_op := ⟨(op_self a).symm, h2.is_op⟩
+
+@[rocq_alias is_op_pair_core_id_r]
+instance isOpMerge_pair_core_id_r [CMRA α] [CMRA β] {io : InOut}
+    (a b1 b2 : α) (a' : β)
+    [h1 : CoreId a'] [h2 : IsOp merge a b1 b2] :
+    IsOp io (a, a') (b1, a') (b2, a') where
+  is_op := ⟨h2.is_op, (op_self a').symm⟩
+
+@[rocq_alias is_op_Some]
+instance isOpMerge_some [CMRA α] (a b1 b2 : α) {io : InOut}
+    [h : IsOp merge a b1 b2] :
+    IsOp io (some a) (some b1) (some b2) where
+  is_op := h.is_op
+
+end IsOp
+
+end Iris
diff --git a/Iris/Iris/Algebra/Lib/FracAuth.lean b/Iris/Iris/Algebra/Lib/FracAuth.lean
index d8065402d..a0668d658 100644
--- a/Iris/Iris/Algebra/Lib/FracAuth.lean
+++ b/Iris/Iris/Algebra/Lib/FracAuth.lean
@@ -6,6 +6,7 @@ Authors: Markus de Medeiros
 module
 
 public import Iris.Algebra.Auth
+public import Iris.Algebra.IsOp
 import Iris.Algebra.LocalUpdates
 meta import Iris.Std.RocqPorting
 
@@ -215,6 +216,20 @@ theorem frag_op_valid {q1 q2 : Frac F} {a b : A} :
   show ✓ (◯F{q1 + q2} (a • b)) ↔ _
   exact frag_valid
 
+/-! ## IsOp type class instances -/
+
+@[rocq_alias frac_auth_is_op]
+instance isOp_frac_auth {q q1 q2 : Frac F} {a1 a2 : A} {a : outParam A}
+    [h1 : IsOp merge q q1 q2] [h2 : IsOp merge a a1 a2] :
+    IsOp io (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2) where
+  is_op := ⟨⟨⟩, ⟨h1.is_op, h2.is_op⟩⟩
+
+@[rocq_alias frac_auth_is_op_core_id]
+instance isOp_frac_auth_core_id {q q1 q2 : Frac F} {a : A}
+    [h1 : CoreId a] [h2 : IsOp merge q q1 q2] :
+    IsOp io (◯F{q} a) (◯F{q1} a) (◯F{q2} a) where
+  is_op := ⟨⟨⟩, ⟨h2.is_op, (op_self a).symm⟩⟩
+
 /-! ## Updates -/
 
 @[rocq_alias frac_auth_update]
diff --git a/Iris/Iris/Algebra/View.lean b/Iris/Iris/Algebra/View.lean
index 93340cfb0..93bb629a9 100644
--- a/Iris/Iris/Algebra/View.lean
+++ b/Iris/Iris/Algebra/View.lean
@@ -312,6 +312,14 @@ instance : UCMRA (View F R) where
 theorem auth_op_auth_eqv : (●V{dq1 • dq2} a : View F R) ≡ (●V{dq1} a) • ●V{dq2} a :=
   ⟨⟨rfl, Agree.idemp.symm⟩, UCMRA.unit_left_id.symm⟩
 
+@[rocq_alias view_auth_dfrac_is_op]
+instance isOp_view_auth_dfrac {dq dq1 dq2 : DFrac F} {a : A}
+    [h : IsOp merge dq dq1 dq2] :
+    IsOp io (●V{dq} a : View F R) (●V{dq1} a) (●V{dq2} a) where
+  is_op := by
+    rw [h.is_op]
+    apply auth_op_auth_eqv
+
 @[rocq_alias view_frag_op]
 theorem frag_op_eq : (◯V (b1 • b2) : View F R) = ((◯V b1) • ◯V b2 : View F R) := rfl
 
@@ -349,6 +357,11 @@ instance [CMRA.CoreId b] : CMRA.CoreId ((●V{.discard} a : View F R) • ◯V b
     refine (CMRA.coreId_iff_core_eqv_self.mp (by trivial)).trans ?_
     refine UCMRA.unit_left_id.symm
 
+@[rocq_alias view_frag_is_op]
+instance {b b1 b2 : B} [h : IsOp merge b b1 b2] :
+    IsOp io (◯V b : View F R) (◯V b1) (◯V b2) where
+  is_op := NonExpansive.eqv h.is_op
+
 @[rocq_alias view_auth_dfrac_op_invN]
 theorem dist_of_validN_auth (H : ✓{n} ((●V{dq1} a1 : View F R) • ●V{dq2} a2)) : a1 ≡{n}≡ a2 := by
   rcases H with ⟨_, _, H, _⟩
diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean
index 6d1d24cfd..a1709b090 100644
--- a/Iris/Iris/Instances/IProp/Instance.lean
+++ b/Iris/Iris/Instances/IProp/Instance.lean
@@ -14,7 +14,7 @@ public meta import Iris.Std.RocqPorting
 @[expose] public section
 namespace Iris
 
-open COFE
+open COFE Std CMRA
 
 /-- Apply an OFunctor at a fixed type -/
 abbrev COFE.OFunctorPre.ap (F : OFunctorPre) (T : Type _) [OFE T] :=
@@ -752,16 +752,49 @@ theorem iOwn_unit {γ} {ε : F.ap (IProp GF)} [Hε : IsUnit ε] : ⊢ |==> iOwn
     rintro rfl
     exact BI.and_elim_r
 
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias into_sep_own]
+instance intoSep_own {γ} {a : F.ap (IProp GF)} [h : IsOp split a b1 b2] :
+    IntoSep (iOwn γ a) (iOwn γ b1) (iOwn γ b2) where
+  into_sep := (equiv_iff.mp <| NonExpansive.eqv h.is_op).mp.trans iOwn_op.mp
+
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias into_and_own]
+instance intoAnd_own {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOp split a b1 b2] :
+    IntoAnd false (iOwn γ a) (iOwn γ b1) (iOwn γ b2) where
+  into_and := (equiv_iff.mp <| NonExpansive.eqv h.is_op).mp.trans <|
+    and_intro (iOwn_mono ⟨b2, .rfl⟩) (iOwn_mono ⟨b1, CMRA.comm⟩)
+
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias from_sep_own]
+instance fromSep_own {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOp split a b1 b2] :
+    FromSep (iOwn γ a) (iOwn γ b1) (iOwn γ b2) where
+  from_sep := iOwn_op.mpr.trans (equiv_iff.mp <| NonExpansive.eqv h.is_op).mpr
+
 @[rocq_alias combine_sep_as_own]
-instance combineSepAs_iOwn {γ} {a1 a2 : F.ap (IProp GF)} :
-  -- TODO: Add IsOp premise once it is ported
-  CombineSepAs (iOwn γ a1) (iOwn γ a2) (iOwn γ (a1 • a2)) where
-  combine_sep_as := iOwn_op.mpr
+instance combineSepAs_iOwn {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOp merge a b1 b2] :
+    CombineSepAs (iOwn γ b1) (iOwn γ b2) (iOwn γ a) where
+  combine_sep_as := iOwn_op.mpr.trans (equiv_iff.mp <| NonExpansive.eqv h.is_op.symm).mp
 
 @[rocq_alias combine_sep_gives_own]
 instance combineSepGives_iOwn {γ} {a1 a2 : F.ap (IProp GF)} :
-  CombineSepGives (iOwn γ a1) (iOwn γ a2) (internalCmraValid (a1 • a2)) where
+    CombineSepGives (iOwn γ a1) (iOwn γ a2) (internalCmraValid (a1 • a2)) where
   combine_sep_gives := iOwn_cmraValid_op
 
+set_option synthInstance.checkSynthOrder false in
+@[rocq_alias from_and_own_persistent]
+instance fromAndOwn_persistent {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOp split a b1 b2]
+    [TCOr (CoreId b1) (CoreId b2)] : FromAnd (iOwn γ a) (iOwn γ b1) (iOwn γ b2) where
+  from_and := by
+    -- Infer from `CoreId b1` that `iOwn γ b1` is persistent, likewise for `b2`
+    have _ : TCOr (Persistent (iOwn γ b1)) (Persistent (iOwn γ b2)) := by
+      cases (inferInstance : TCOr (CoreId b1) (CoreId b2))
+      · infer_instance
+      · infer_instance
+    calc
+      _ ⊢ iOwn γ b1 ∗ iOwn γ b2 := persistent_and_sep_1
+      _ ⊢ iOwn γ (b1 • b2)      := iOwn_op.mpr
+      _ ⊢ iOwn γ a              := (equiv_iff.mp <| NonExpansive.eqv h.is_op).mpr
+
 end iOwn
 end Iris
diff --git a/Iris/Iris/Instances/Lib/Token.lean b/Iris/Iris/Instances/Lib/Token.lean
index 522deaa76..594d27b75 100644
--- a/Iris/Iris/Instances/Lib/Token.lean
+++ b/Iris/Iris/Instances/Lib/Token.lean
@@ -19,8 +19,6 @@ open BI CMRA Excl OFE UPred IProp Std ProofMode
 This library provides assertions that represent "unique tokens".
 The `token γ` assertion provides ownership of the token named `γ`,
 and the key lemma `token_exclusive` proves only one token exists.
-
-FIXME: missing token_combine_gives
 -/
 
 abbrev TokenF : COFE.OFunctorPre := constOF (Excl Unit)
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index 71bbf0fff..f152863ac 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -10,11 +10,12 @@ public import Iris.ProofMode
 public import Iris.Instances.IProp
 public import Iris.Instances.Lib.LaterCredits
 public import Iris.Instances.Lib.Token
+public import Iris.Algebra.CMRA
 
 @[expose] public section
 
 namespace Iris.Tests
-open Iris.BI
+open BI CMRA DFrac
 
 /- This file contains tests with various scenarios for all available tactics. -/
 
@@ -2543,20 +2544,64 @@ example [BI PROP] {P Q R : PROP} : ⊢ P -∗ Q -∗ □ R -∗ R ∗ P ∗ Q :=
   iintro HP HQ #HR
   icombine %a as HNew1
 
-/-- Tests `icombine` for combining propositions involving `iOwn` -/
+/-- Tests `icombine` for combining propositions involving `iOwn`, where
+    `a2` and `a3` can be combined as `b` instead of `a2 • a3` as
+    the former takes higher precedence. Likewise, `a1` and `b` is merged
+    as `c` instead of `a1 • b`. -/
 example {F GF} [RFunctorContractive F] [ElemG GF F] {γ}
-    {a1 a2 a3 : F.ap (IProp GF)} :
+    {a1 a2 a3 b c : F.ap (IProp GF)} [IsOp merge b a2 a3] [IsOp merge c a1 b] :
     ⊢ iOwn γ a1 -∗ iOwn γ a2 -∗ iOwn γ a3 -∗
-      iOwn γ (a1 • (a2 • a3)) ∗
-      internalCmraValid (a2 • a3) ∗ internalCmraValid (a1 • (a2 • a3)) := by
+      iOwn γ c ∗ internalCmraValid (a2 • a3) ∗ internalCmraValid (a1 • b) := by
   iintro H1 H2 H3
   icombine H1 H2 H3 as Hnew1 gives ⟨Hnew2, Hnew3⟩
   isplitl
   · iexact Hnew1
   · isplit
-    · iexact Hnew2
+    · iexact Hnew2  -- `IsOp` is irrelevant to the `gives` syntax
     · iexact Hnew3
 
+/-- Tests `icombine` for combining propositions involving `iOwn` and `IsOp`
+    instances for `DFrac` and `Frac`. -/
+example {GF α} [UFraction α] [ElemG GF (constOF (DFrac α))]
+    [ElemG GF (constOF (Frac α))] {γ}
+    {a1 a2 a3 b c : Frac α} [IsOp merge b a2 a3] [IsOp merge c a1 b] :
+    ⊢@{IProp GF}
+      iOwn (F := constOF (DFrac α)) γ (own a1.car) -∗
+      iOwn (F := constOF (DFrac α)) γ (own a2.car) -∗
+      iOwn (F := constOF (DFrac α)) γ (own a3.car) -∗
+      iOwn (F := constOF (Frac α)) γ a1 -∗
+      iOwn (F := constOF (Frac α)) γ a2 -∗
+      iOwn (F := constOF (Frac α)) γ a3 -∗
+      iOwn (F := constOF (DFrac α)) γ (own c.car) ∗ iOwn (F := constOF (Frac α)) γ c := by
+  iintro H1 H2 H3 H4 H5 H6
+  icombine H1 H2 H3 as Hnew1
+  icombine H4 H5 H6 as Hnew2
+  isplitl [Hnew1]
+  · iexact Hnew1
+  · iexact Hnew2
+
+/-- Tests `icombine` for combining propositions involving `iOwn` and `IsOp`
+    instances for the authoritative CMRA. -/
+example {GF F A} [UFraction F] [UCMRA A] [ElemG GF (constOF (Auth F A))] {γ}
+    {a1 a2 a3 b c : A} {dq' dq'' dq1 dq2 dq3 dq4 : DFrac F}
+    [IsOp merge b a2 a3] [IsOp merge c a1 b]
+    [IsOp merge dq' dq1 dq2] [IsOp merge dq'' dq3 dq4] :
+    ⊢@{IProp GF}
+      iOwn (F := constOF (Auth F A)) γ (◯ a1) -∗
+      iOwn (F := constOF (Auth F A)) γ (◯ a2) -∗
+      iOwn (F := constOF (Auth F A)) γ (◯ a3) -∗
+      iOwn (F := constOF (Auth F A)) γ (●{dq1} a1) -∗
+      iOwn (F := constOF (Auth F A)) γ (●{dq2} a1) -∗
+      iOwn (F := constOF (Auth F A)) γ (●{dq3} a1) -∗
+      iOwn (F := constOF (Auth F A)) γ (●{dq4} a1) -∗
+      iOwn (F := constOF (Auth F A)) γ ((◯ c) • ●{dq' • dq''} a1) := by
+  iintro H1 H2 H3 H4 H5 H6 H7
+  icombine H1 H2 H3 as HNew1
+  icombine H4 H5 as HNew2
+  icombine H6 H7 as HNew3
+  icombine HNew1 HNew2 HNew3 as HNew
+  iexact HNew
+
 /-- Tests `icombine` for combining propositions involving later credits. -/
 example {GF m n} [LcGS GF] :
     ⊢@{IProp GF} £ n -∗ £ 1 -∗ £ m -∗ £ 1 -∗ £ n + (1 + (m + 1)) := by
diff --git a/Iris/PORTING.md b/Iris/PORTING.md
index d3c20031d..d4bca5ed2 100644
--- a/Iris/PORTING.md
+++ b/Iris/PORTING.md
@@ -95,8 +95,8 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p
   - [x] Discrete functions
   - [x] Isomorphisms
   - [ ] Sigma 
-- [ ] `proofmode_classes.v`
-  - [ ] IsOp
+- [x] `proofmode_classes.v`
+  - [x] IsOp
 - [ ] `reservation_map.v`
   - [ ] CMRA
   - [ ] Updates