diff --git a/Iris/Iris/Algebra/CMRA.lean b/Iris/Iris/Algebra/CMRA.lean
index 1ae38c0fd..a6e4180b9 100644
--- a/Iris/Iris/Algebra/CMRA.lean
+++ b/Iris/Iris/Algebra/CMRA.lean
@@ -761,8 +761,8 @@ theorem discrete_inc_l {x y : α} [HD : DiscreteE x] (Hv : ✓{0} y) (Hle : x 
 theorem discrete_inc_r {x y : α} [HD : DiscreteE y] : x ≼{0} y → x ≼ y
   | ⟨z, hz⟩ => ⟨z, HD.discrete hz⟩
 
-@[reducible, rocq_alias cmra_op_discrete]
-def discrete_op {x y : α} (Hv : ✓{0} x • y) [Hx : DiscreteE x] [Hy : DiscreteE y] :
+@[rocq_alias cmra_op_discrete]
+theorem discrete_op {x y : α} (Hv : ✓{0} x • y) [Hx : DiscreteE x] [Hy : DiscreteE y] :
     DiscreteE (x • y) where
   discrete h :=
     let ⟨_w, _t, wt, wx, ty⟩ := extend ((Dist.validN h).mp Hv) h.symm
diff --git a/Iris/Iris/Algebra/Heap.lean b/Iris/Iris/Algebra/Heap.lean
index 61eb5bce1..23d064480 100644
--- a/Iris/Iris/Algebra/Heap.lean
+++ b/Iris/Iris/Algebra/Heap.lean
@@ -583,7 +583,7 @@ instance [OFE α] [OFE β] {f : α → β} [hne : OFE.NonExpansive f] : OFE.NonE
     cases get? m1 k <;> cases get? m2 k <;> simp
     apply OFE.NonExpansive.ne
 
-def map_id [OFE α] (a : H α):
+theorem map_id [OFE α] (a : H α) :
     PartialMap.map H id a ≡ a := by
   intro n x
   simp [PartialMap.map, get?_bindAlter, Option.bind]
@@ -593,19 +593,19 @@ def mapO [OFE α] [OFE β] (f : α -n> β) : OFE.Hom (H α) (H β) where
   f := map H f
   ne := inferInstance
 
-def map_ext [OFE α] [OFE β] {f g : α -> β} (heq : f ≡ g) : map H f m ≡ map H g m := by
+theorem map_ext [OFE α] [OFE β] {f g : α -> β} (heq : f ≡ g) : map H f m ≡ map H g m := by
   intro n k
   simp [map, get?_bindAlter, Option.bind]
   cases get? m k <;> simp
   exact heq _ _
 
-def map_ne [OFE α] [OFE β] (f g : α -> β) {heq : f ≡{n}≡ g} : map H f m ≡{n}≡ map H g m := by
+theorem map_ne [OFE α] [OFE β] (f g : α -> β) {heq : f ≡{n}≡ g} : map H f m ≡{n}≡ map H g m := by
   simp [OFE.Dist, Option.Forall₂, map, get?_bindAlter]
   intro k
   cases get? m k <;> simp
   exact heq _
 
-def map_compose [OFE α] [OFE β] [OFE γ] (f : α -> β) (g : β -> γ) m :
+theorem map_compose [OFE α] [OFE β] [OFE γ] (f : α -> β) (g : β -> γ) m :
     map H (g.comp f) m ≡ map H g (map H f m) := by
   intro n k
   simp [map, get?_bindAlter]
diff --git a/Iris/Iris/Algebra/IProp.lean b/Iris/Iris/Algebra/IProp.lean
index 1f1b12c83..368000934 100644
--- a/Iris/Iris/Algebra/IProp.lean
+++ b/Iris/Iris/Algebra/IProp.lean
@@ -20,9 +20,11 @@ open COFE
 
 abbrev GType := Nat
 
+set_option linter.checkUnivs false in
 @[rocq_alias gFunctor]
 abbrev GFunctor := Σ F : OFunctorPre, RFunctorContractive F
 
+set_option linter.checkUnivs false in
 @[rocq_alias gFunctors]
 def BundledGFunctors := GType → GFunctor
 
diff --git a/Iris/Iris/Algebra/OFE.lean b/Iris/Iris/Algebra/OFE.lean
index 5d8c35b5e..9ba43b307 100644
--- a/Iris/Iris/Algebra/OFE.lean
+++ b/Iris/Iris/Algebra/OFE.lean
@@ -991,7 +991,7 @@ theorem chain_none_const [OFE V] {c : Chain (Option V)} (H : c n = none) :
     exact (Hc Hnk).symm
 
 /-- If a chain of Option is ever some, it is the lift a chain by some. -/
-def chain_option_some [OFE V] {c : Chain (Option V)} (H : c n = some v) :
+theorem chain_option_some [OFE V] {c : Chain (Option V)} (H : c n = some v) :
     ∃ c' : Chain V, c = Chain.map ⟨some, OFE.Option.some.ne⟩ c' := by
   have HVc (k) : ∃ v', c k = some v' := by
     rcases h : c.chain k with (_|v')
@@ -1158,6 +1158,7 @@ instance {P : α → Type _} [∀ x, OFE (P x)] [∀ x, IsCOFE (P x)] : IsCOFE (
     exact hequiv
 #rocq_ignore sigT_compl "Local Compl definition; folded into Lean's IsCOFE instance."
 
+set_option linter.checkUnivs false in
 abbrev OFunctorPre := ∀ α β [COFE α] [COFE β], Type _
 #rocq_ignore oFunctor_apply "Definition for application of an `oFunctor`; subsumed by `OFunctorPre` in Lean."
 
diff --git a/Iris/Iris/Algebra/UPred.lean b/Iris/Iris/Algebra/UPred.lean
index 6c67f4ff1..3e390dabe 100644
--- a/Iris/Iris/Algebra/UPred.lean
+++ b/Iris/Iris/Algebra/UPred.lean
@@ -45,7 +45,7 @@ def UPred.holds_unpacked {M : Type _} [UCMRA M] (P : UPred M) (n : Nat) (x : M)
     Prop :=
   P.holds n ⟨x, Hx⟩
 
-def UPred.mono_unpacked {M : Type _} [UCMRA M] (P : UPred M) {n1 n2 : Nat} {x1 x2 : M}
+theorem UPred.mono_unpacked {M : Type _} [UCMRA M] (P : UPred M) {n1 n2 : Nat} {x1 x2 : M}
     (Hx1 : ✓{n1} x1) (Hx2 : ✓{n2} x2) (HP : P.holds_unpacked n1 x1 Hx1) (Hxle : x1 ≼{n2} x2)
     (Hle : n2 ≤ n1) : P.holds_unpacked n2 x2 Hx2 :=
   P.mono HP Hxle Hle
diff --git a/Iris/Iris/BI/BigOp/BigOp.lean b/Iris/Iris/BI/BigOp/BigOp.lean
index 7f88c4dc3..d3aad25bf 100644
--- a/Iris/Iris/BI/BigOp/BigOp.lean
+++ b/Iris/Iris/BI/BigOp/BigOp.lean
@@ -39,7 +39,7 @@ instance orMonoidOps [BI PROP] : MonoidOps (or (PROP := PROP)) iprop(False) wher
 /-! ## Homomorphism helpers for OFE equivalence -/
 
 /-- Build a `MonoidHomomorphism` for OFE equivalence from just the essential fields. -/
-@[reducible, expose] def MonoidHomomorphism.ofEquiv [OFE PROP] {op₁ op₂ : PROP → PROP → PROP}
+theorem MonoidHomomorphism.ofEquiv [OFE PROP] {op₁ op₂ : PROP → PROP → PROP}
     {u₁ u₂ : PROP} [MonoidOps op₁ u₁] [MonoidOps op₂ u₂] {f : PROP → PROP}
     (hne : NonExpansive f) (hop : ∀ {x y}, f (op₁ x y) ≡ op₂ (f x) (f y))
     (hunit : f u₁ ≡ u₂) : MonoidHomomorphism op₁ op₂ u₁ u₂ (· ≡ ·) f where
@@ -51,7 +51,7 @@ instance orMonoidOps [BI PROP] : MonoidOps (or (PROP := PROP)) iprop(False) wher
   map_unit := hunit
 
 /-- Build a `WeakMonoidHomomorphism` for OFE equivalence from just the essential fields. -/
-@[reducible, expose] def WeakMonoidHomomorphism.ofEquiv [OFE PROP] {op₁ op₂ : PROP → PROP → PROP}
+theorem WeakMonoidHomomorphism.ofEquiv [OFE PROP] {op₁ op₂ : PROP → PROP → PROP}
     {u₁ u₂ : PROP} [MonoidOps op₁ u₁] [MonoidOps op₂ u₂] {f : PROP → PROP}
     (hne : NonExpansive f) (hop : ∀ {x y}, f (op₁ x y) ≡ op₂ (f x) (f y)) :
     WeakMonoidHomomorphism op₁ op₂ u₁ u₂ (· ≡ ·) f where
diff --git a/Iris/Iris/BI/Embedding.lean b/Iris/Iris/BI/Embedding.lean
index c08177b73..bee649f74 100644
--- a/Iris/Iris/BI/Embedding.lean
+++ b/Iris/Iris/BI/Embedding.lean
@@ -318,7 +318,7 @@ instance embed_timeless [BiEmbedLater PROP1 PROP2] (P : PROP1) [Timeless P] :
 
 /-- Cross-type `MonoidHomomorphism` for `⎡·⎤` w.r.t. OFE equivalence (mirrors
 `MonoidHomomorphism.ofEquiv`, which is single-type). -/
-@[reducible] def mkEmbedHom {op₁ : PROP1 → PROP1 → PROP1} {op₂ : PROP2 → PROP2 → PROP2}
+theorem mkEmbedHom {op₁ : PROP1 → PROP1 → PROP1} {op₂ : PROP2 → PROP2 → PROP2}
     {u₁ : PROP1} {u₂ : PROP2} [MonoidOps op₁ u₁] [MonoidOps op₂ u₂]
     (hop : ∀ {x y}, (embed (op₁ x y) : PROP2) ≡ op₂ (embed x) (embed y))
     (hunit : (embed u₁ : PROP2) ≡ u₂) :
@@ -514,8 +514,8 @@ def embedBiEmbed : BiEmbed PA PC :=
   }
 
 /-- `BiEmbedEmp` transfers along composition. -/
-@[reducible, rocq_alias embed_embed_emp]
-def embed_embed_emp [BiEmbedEmp PA PB] [BiEmbedEmp PB PC] :
+@[rocq_alias embed_embed_emp]
+theorem embed_embed_emp [BiEmbedEmp PA PB] [BiEmbedEmp PB PC] :
     @BiEmbedEmp PA PC _ _ (embedBiEmbed PB) :=
   letI : BiEmbed PA PC := embedBiEmbed PB
   { embed_emp_1 := (embed_mono (PROP1 := PB) (PROP2 := PC)
@@ -523,8 +523,8 @@ def embed_embed_emp [BiEmbedEmp PA PB] [BiEmbedEmp PB PC] :
       (BiEmbedEmp.embed_emp_1 (PROP1 := PB) (PROP2 := PC)) }
 
 /-- `BiEmbedLater` transfers along composition. -/
-@[reducible, rocq_alias embed_embed_later]
-def embed_embed_later [BiEmbedLater PA PB] [BiEmbedLater PB PC] :
+@[rocq_alias embed_embed_later]
+theorem embed_embed_later [BiEmbedLater PA PB] [BiEmbedLater PB PC] :
     @BiEmbedLater PA PC _ _ (embedBiEmbed PB) :=
   letI : BiEmbed PA PC := embedBiEmbed PB
   { embed_later := fun P => (embed_congr (PROP1 := PB) (PROP2 := PC)
@@ -532,8 +532,8 @@ def embed_embed_later [BiEmbedLater PA PB] [BiEmbedLater PB PC] :
       (BiEmbedLater.embed_later (PROP1 := PB) (PROP2 := PC) (embed (A := PA) (B := PB) P)) }
 
 /-- `BiEmbedBUpd` transfers along composition. -/
-@[reducible, rocq_alias embed_embed_bupd]
-def embed_embed_bupd [BIUpdate PA] [BIUpdate PB] [BIUpdate PC]
+@[rocq_alias embed_embed_bupd]
+theorem embed_embed_bupd [BIUpdate PA] [BIUpdate PB] [BIUpdate PC]
     [BiEmbedBUpd PA PB] [BiEmbedBUpd PB PC] :
     @BiEmbedBUpd PA PC _ _ (embedBiEmbed PB) _ _ :=
   letI : BiEmbed PA PC := embedBiEmbed PB
@@ -542,8 +542,8 @@ def embed_embed_bupd [BIUpdate PA] [BIUpdate PB] [BIUpdate PC]
       (BiEmbedBUpd.embed_bupd (PROP1 := PB) (PROP2 := PC) (embed (A := PA) (B := PB) P)) }
 
 /-- `BiEmbedFUpd` transfers along composition. -/
-@[reducible, rocq_alias embed_embed_fupd]
-def embed_embed_fupd [BIFUpdate PA] [BIFUpdate PB] [BIFUpdate PC]
+@[rocq_alias embed_embed_fupd]
+theorem embed_embed_fupd [BIFUpdate PA] [BIFUpdate PB] [BIFUpdate PC]
     [BiEmbedFUpd PA PB] [BiEmbedFUpd PB PC] :
     @BiEmbedFUpd PA PC _ _ (embedBiEmbed PB) _ _ :=
   letI : BiEmbed PA PC := embedBiEmbed PB
@@ -559,8 +559,8 @@ section
 variable {QA QB QC : Type _} [Sbi QA] [Sbi QB] [Sbi QC]
   [BiEmbed QA QB] [BiEmbed QB QC] [BiEmbedSbi QA QB] [BiEmbedSbi QB QC]
 
-@[reducible, rocq_alias embed_embed_sbi]
-def embed_embed_sbi : @BiEmbedSbi QA QC _ _ (embedBiEmbed QB) _ _ :=
+@[rocq_alias embed_embed_sbi]
+theorem embed_embed_sbi : @BiEmbedSbi QA QC _ _ (embedBiEmbed QB) _ _ :=
   letI : BiEmbed QA QC := embedBiEmbed QB
   { embed_si_emp_valid := fun P =>
       (BiEmbedSbi.embed_si_emp_valid (PROP1 := QB) (PROP2 := QC) (embed (A := QA) (B := QB) P)).trans
diff --git a/Iris/Iris/BI/MonPred.lean b/Iris/Iris/BI/MonPred.lean
index 67e825cdb..a48d9d63b 100644
--- a/Iris/Iris/BI/MonPred.lean
+++ b/Iris/Iris/BI/MonPred.lean
@@ -1249,7 +1249,7 @@ section BigOp
 open Iris.Algebra Iris.Algebra.BigOpL Iris.Algebra.BigOpM
 open Iris.BI.BigSepL Iris.BI.BigSepM Iris.BI.BigSepS
 
-@[reducible] def monPred_at_hom {op₁ : MonPred I PROP → MonPred I PROP → MonPred I PROP}
+theorem monPred_at_hom {op₁ : MonPred I PROP → MonPred I PROP → MonPred I PROP}
     {op₂ : PROP → PROP → PROP} {u₁ : MonPred I PROP} {u₂ : PROP}
     [MonoidOps op₁ u₁] [MonoidOps op₂ u₂] (i : I.car)
     (hop : ∀ {x y}, (op₁ x y).monPred_at i ≡ op₂ (x.monPred_at i) (y.monPred_at i))
@@ -1337,8 +1337,8 @@ instance monPred_objectively_monoid_sep_entails_homomorphism :
   map_op := fun {x y} => monPred_objectively_sep_2 x y
   map_unit := monPred_objectively_emp.mpr
 
-@[reducible, rocq_alias monPred_objectively_monoid_sep_homomorphism]
-def monPred_objectively_monoid_sep_homomorphism {bot : I.car} [BiIndexBottom I bot] :
+@[rocq_alias monPred_objectively_monoid_sep_homomorphism]
+theorem monPred_objectively_monoid_sep_homomorphism {bot : I.car} [BiIndexBottom I bot] :
     MonoidHomomorphism (BIBase.sep (PROP := MonPred I PROP)) BIBase.sep BIBase.emp BIBase.emp
       (· ≡ ·) MonPred.objectively :=
   MonoidHomomorphism.ofEquiv monPred_objectively_ne
@@ -1560,8 +1560,8 @@ instance monPred_subjectively_plain (P : MonPred I PROP) [Plain P] :
 
 /-! ### `SbiEmpValidExist` for `MonPred` -/
 
-@[reducible, rocq_alias monPred_sbi_emp_valid_exist]
-def monPred_sbi_emp_valid_exist {bot : I.car} [BiIndexBottom I bot] [SbiEmpValidExist PROP] :
+@[rocq_alias monPred_sbi_emp_valid_exist]
+theorem monPred_sbi_emp_valid_exist {bot : I.car} [BiIndexBottom I bot] [SbiEmpValidExist PROP] :
     SbiEmpValidExist (MonPred I PROP) where
   siEmpValid_sExists_1 Ψ := by
     refine (siEmpValid_mono (forall_elim bot)).trans ?_
diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean
index 4816c965e..2d0cab892 100644
--- a/Iris/Iris/Instances/IProp/Instance.lean
+++ b/Iris/Iris/Instances/IProp/Instance.lean
@@ -26,7 +26,7 @@ abbrev BundledGFunctors.api (FF : BundledGFunctors) (τ : GType) (T : Type _) [C
   FF τ |>.fst |>.ap T
 
 /-- Transport an OFunctorPre application along equality of the OFunctorPre.  -/
-def transpAp {F1 F2 : OFunctorPre} (H : F1 = F2) {T} [COFE T] : F1.ap T = F2.ap T :=
+theorem transpAp {F1 F2 : OFunctorPre} (H : F1 = F2) {T} [COFE T] : F1.ap T = F2.ap T :=
   congrArg (OFunctorPre.ap · T) H
 
 section TranspAp
@@ -71,10 +71,10 @@ open OFE
 
 variable [I : RFunctorContractive F]
 
-def ElemG.transpMap (E : ElemG GF F) T [OFE T] : (GF E.τ).fst = F :=
+theorem ElemG.transpMap (E : ElemG GF F) T [OFE T] : (GF E.τ).fst = F :=
   Sigma.mk.inj E.transp |>.1
 
-def ElemG.transpClass (E : ElemG GF F) T [OFE T] : (GF E.τ).snd ≍ I :=
+theorem ElemG.transpClass (E : ElemG GF F) T [OFE T] : (GF E.τ).snd ≍ I :=
   Sigma.mk.inj E.transp |>.2
 
 def ElemG.bundle (E : ElemG GF F) [COFE T] : F.ap T → GF.api E.τ T :=
diff --git a/Iris/Iris/ProgramLogic/EctxLanguage.lean b/Iris/Iris/ProgramLogic/EctxLanguage.lean
index 79eea6b56..6964c1f6d 100644
--- a/Iris/Iris/ProgramLogic/EctxLanguage.lean
+++ b/Iris/Iris/ProgramLogic/EctxLanguage.lean
@@ -307,8 +307,8 @@ theorem primStep_stuck_of_baseStep_stuck :
     BaseStep.Stuck (e, σ) → SubredexesAreValues e → PrimStep.Stuck (e, σ) :=
   fun ⟨toVal_none, irr⟩ hsr => ⟨toVal_none, primStep_irreducible_of_baseStep_irreducible irr hsr⟩
 
-@[rocq_alias ectx_language_atomic, implicit_reducible]
-def Atomic.ofBaseAtomic (a : Language.Atomicity) :
+@[rocq_alias ectx_language_atomic]
+theorem Atomic.ofBaseAtomic (a : Language.Atomicity) :
     BaseAtomic a e →
     SubredexesAreValues e →
     Language.Atomic a e := fun _ _ => ⟨by grind [BaseAtomic]⟩
diff --git a/Iris/Iris/ProgramLogic/Language.lean b/Iris/Iris/ProgramLogic/Language.lean
index 896b146cd..0e2a17858 100644
--- a/Iris/Iris/ProgramLogic/Language.lean
+++ b/Iris/Iris/ProgramLogic/Language.lean
@@ -125,7 +125,7 @@ end Notation
 
 open Notation
 
-def Step.of_primStep {e σ} {obs : List Obs} {e'} {σ' : State} {eₜ}
+theorem Step.of_primStep {e σ} {obs : List Obs} {e'} {σ' : State} {eₜ}
     (H : (e, σ) -<obs>-> (e', σ', eₜ)) {t₁ t₂: List Expr} :
     Step (t₁ ++ e :: t₂, σ) obs (t₁ ++ e' :: t₂ ++ eₜ, σ') :=
   atomic H ..
diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean
index 6ad568c26..958c75c39 100644
--- a/Iris/Iris/ProgramLogic/WeakestPre.lean
+++ b/Iris/Iris/ProgramLogic/WeakestPre.lean
@@ -431,7 +431,7 @@ theorem wp_bind (K : Expr → Expr) [κ : Language.Context K] {s : Stuckness} {E
     WP e @ s ; E {{v, WP (K (↑v : Val)) @ s ; E {{ Φ }} }} ⊢ WP (K e) @ s ; E {{ Φ }} := (wp_bind_iff K).1
 
 @[rocq_alias wp_bind_inv]
-def wp_bind_inv (K : Expr → Expr) [κ : Language.Context K] {s : Stuckness} {E : CoPset} {e : Expr}
+theorem wp_bind_inv (K : Expr → Expr) [κ : Language.Context K] {s : Stuckness} {E : CoPset} {e : Expr}
     {Φ : Val → IProp GF} :
    WP (K e) @ s ; E {{ Φ }} ⊢ WP e @ s ; E {{v, WP (K (↑v : Val)) @ s ; E {{ Φ }} }}  := (wp_bind_iff K).2
 
diff --git a/Iris/Iris/ProofMode/Tactics/Combine.lean b/Iris/Iris/ProofMode/Tactics/Combine.lean
index 1b5cca40b..dd2d8e25a 100644
--- a/Iris/Iris/ProofMode/Tactics/Combine.lean
+++ b/Iris/Iris/ProofMode/Tactics/Combine.lean
@@ -136,6 +136,7 @@ private def CombineState.combineProofModeHyp {u prop bi origE goal} :
     -- Type class instance search for the `as` syntax
     let newOutAs ← mkFreshExprMVarQ q($prop)
     let instAs ← ProofModeM.synthInstanceQ q(CombineSepAs $out2 $outAs $newOutAs)
+    have : ($(conj p1 p2)) =Q ($p1 && $p2) := ⟨⟩
     let newPfAs := q(combine_as_step $instAs $pfAs $(pf2).mp)
 
     match outGives, pfGives with
@@ -246,9 +247,9 @@ elab "icombine " patSels:(colGt ppSpace selPat)*
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
     let hs ← iCombineParseSelPats hyps patSels
-    let st ← iCombineCore hs hyps goal
+    let {outGives, pfGives, ..} ← iCombineCore hs hyps goal
 
-    match st.outGives, st.pfGives with
+    match outGives, pfGives with
     | some outGives, pfGives =>
       let pf ← iCasesCore _ hyps goal pat q(true) outGives addBIGoal
       mvar.assign q($(pfGives).trans $pf)
@@ -275,9 +276,9 @@ elab "icombine " patSels:(colGt ppSpace selPat)*
 
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
     let hs ← iCombineParseSelPats hyps patSels
-    let st ← iCombineCore hs hyps goal
+    let st@{outGives, pfGives, ..} ← iCombineCore hs hyps goal
 
-    match st.outGives, st.pfGives with
+    match outGives, pfGives with
     | some outGives, pfGives =>
       let pf ← iCasesCore _ st.newHyps goal (.conjunction [pat1, .intuitionistic pat2])
         q($st.p) q(iprop($st.outAs ∗ □ $outGives)) addBIGoal
diff --git a/Iris/Iris/Std/List.lean b/Iris/Iris/Std/List.lean
index 2cf681e76..ca9988f6b 100644
--- a/Iris/Iris/Std/List.lean
+++ b/Iris/Iris/Std/List.lean
@@ -42,8 +42,7 @@ theorem nodup_map_of_injective {B : Type _} {f : A → B} {l : List A}
     cases hinj heq.symm
     exact hnodup.1 hy
 
-@[expose, match_pattern]
-def Forall₂.append {l₁ l₁' l₂ l₂'} : List.Forall₂ R l₁ l₂ → List.Forall₂ R l₁' l₂' → List.Forall₂ R (l₁ ++ l₁') (l₂ ++ l₂')
+theorem Forall₂.append {l₁ l₁' l₂ l₂'} : List.Forall₂ R l₁ l₂ → List.Forall₂ R l₁' l₂' → List.Forall₂ R (l₁ ++ l₁') (l₂ ++ l₂')
   | .nil, h => h
   | .cons step rest, h => .cons step (append rest h)
 
diff --git a/Iris/Iris/Std/PartialMap.lean b/Iris/Iris/Std/PartialMap.lean
index 221a25664..a6033e573 100644
--- a/Iris/Iris/Std/PartialMap.lean
+++ b/Iris/Iris/Std/PartialMap.lean
@@ -149,6 +149,7 @@ def difference (m₁ m₂ : M V) : M V :=
 def zipWith (f : V → V' → V'') (m₁ : M V) (m₂ : M V') : M V'' :=
   bindAlter (fun k v => (get? m₂ k).bind fun v' => some <| f v v') m₁
 
+set_option linter.checkUnivs false in
 def zip (m₁ : M V) (m₂ : M V') : M (V × V') :=
   zipWith (fun x y => (x, y)) m₁ m₂
 
@@ -167,7 +168,7 @@ theorem equiv.trans : ∀ {a b c : M V}, equiv a b → equiv b c → equiv a c :
 /-- Pointwise equivalence is transitive. -/
 instance instEquivTrans : Trans equiv (@equiv K V M _) equiv := ⟨equiv.trans⟩
 
-@[simp] def equiv.symm :  ∀  (a b : M V), equiv a b → equiv b a :=
+@[simp] theorem equiv.symm :  ∀  (a b : M V), equiv a b → equiv b a :=
   fun _ _ h k => (h k).symm
 
 instance instEquivSymm : Std.Symm (@equiv K V M _) := ⟨equiv.symm⟩
diff --git a/Iris/Iris/Std/Positives.lean b/Iris/Iris/Std/Positives.lean
index 842c6d78e..490b4572c 100644
--- a/Iris/Iris/Std/Positives.lean
+++ b/Iris/Iris/Std/Positives.lean
@@ -349,7 +349,7 @@ theorem flatten_suffix (l k : List Pos) : l <:+ k -> ∃ q, flatten k = q ++ fla
   rintro ⟨l', rfl⟩
   exact ⟨_, flatten_app⟩
 
-def app_inj (p : Pos) : (· ++ p).Injective :=
+theorem app_inj (p : Pos) : (· ++ p).Injective :=
   fun a a' Heq => by induction p <;> simp_all [HAppend.hAppend, app]
 
 theorem reverse_involutive p : reverse (reverse p) = p := by
@@ -358,7 +358,7 @@ theorem reverse_involutive p : reverse (reverse p) = p := by
   | xO p IH => rewrite [reverse_x0, reverse_app, IH]; rfl
   | xH => rfl
 
-def rev_inj : reverse.Injective :=
+theorem rev_inj : reverse.Injective :=
   fun p q Heq => by
     rewrite [<- reverse_involutive p, <- reverse_involutive q]
     simp [Heq]
@@ -410,10 +410,10 @@ class Countable (A : Type) where
   decode : Pos -> Option A
   decode_encode x : decode (encode x) = some x
 
-def some_inj {A} : (@some A).Injective :=
+theorem some_inj {A} : (@some A).Injective :=
   fun _ _ => by rintro ⟨⟩; rfl
 
-def encode_inj [c : Countable A] : c.encode.Injective :=
+theorem encode_inj [c : Countable A] : c.encode.Injective :=
   fun x _ Hxy => by
     apply some_inj
     rewrite [<- c.decode_encode x, Hxy, c.decode_encode]
diff --git a/Iris/Iris/Std/Prod.lean b/Iris/Iris/Std/Prod.lean
index 5a9729e01..7890e4d42 100644
--- a/Iris/Iris/Std/Prod.lean
+++ b/Iris/Iris/Std/Prod.lean
@@ -9,6 +9,7 @@ module
 
 namespace Prod
 
+set_option linter.checkUnivs false in
 /-- Apply `f` to all elements of a tuple. All elements of the tuple must have the same type `α`. -/
 def mapAllM [Monad M] (f : α → M β) : α × α → M (β × β)
   | (x, y) => do return (← f x, ← f y)
diff --git a/Iris/lake-manifest.json b/Iris/lake-manifest.json
index 578cea943..8f17b358d 100644
--- a/Iris/lake-manifest.json
+++ b/Iris/lake-manifest.json
@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
+   "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0",
+   "inputRev": "v4.32.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
+   "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0",
+   "inputRev": "v4.32.0",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "iris",
diff --git a/Iris/lakefile.toml b/Iris/lakefile.toml
index c04dddd89..62ceb86ea 100644
--- a/Iris/lakefile.toml
+++ b/Iris/lakefile.toml
@@ -4,12 +4,12 @@ defaultTargets = ["Iris", "IrisTest"]
 [[require]]
 name = "Qq"
 scope = "leanprover-community"
-rev = "v4.31.0"
+rev = "v4.32.0"
 
 [[require]]
 name = "batteries"
 scope = "leanprover-community"
-rev = "v4.31.0"
+rev = "v4.32.0"
 
 [[lean_lib]]
 name = "Iris"
diff --git a/Iris/lean-toolchain b/Iris/lean-toolchain
index 18640c8b0..2544c30c5 100644
--- a/Iris/lean-toolchain
+++ b/Iris/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.31.0
+leanprover/lean4:v4.32.0
\ No newline at end of file