diff --git a/tests/proofmode.v b/tests/proofmode.v
index fe6b8969ac8d5844a71cc8a415e37140eea87183..1100315a65044ae1b0059eaec0a31f866e87a5b7 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -12,6 +12,13 @@ Proof. eauto 6. Qed.
 Lemma test_eauto_isplit_biwand P : (P ∗-∗ P)%I.
 Proof. eauto. Qed.
 
+Fixpoint test_fixpoint (n : nat) {struct n} : True → emp ⊢@{PROP} ⌜ (n + 0)%nat = n ⌝%I.
+Proof.
+  case: n => [|n] /=; first (iIntros (_) "_ !%"; reflexivity).
+  iIntros (_) "_".
+  by iDestruct (test_fixpoint with "[//]") as %->.
+Qed.
+
 Check "demo_0".
 Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
 Proof.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 62c1402606a8fff084c31f2c905e61cbe76d8bca..3018f180b49b5abe85096bb7e2d9612a04be2a46 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -453,18 +453,26 @@ Proof.
 Qed.
 
 Definition IntoEmpValid (φ : Type) (P : PROP) := φ → bi_emp_valid P.
+(** These lemmas are [Defined] because the guardedness checker must see
+through them. See https://gitlab.mpi-sws.org/iris/iris/issues/274. For the
+same reason, their bodies use as little automation as possible. *)
 Lemma into_emp_valid_here φ P : AsEmpValid φ P → IntoEmpValid φ P.
-Proof. by intros [??]. Qed.
+Proof. by intros [??]. Defined.
 Lemma into_emp_valid_impl (φ ψ : Type) P :
   φ → IntoEmpValid ψ P → IntoEmpValid (φ → ψ) P.
-Proof. rewrite /IntoEmpValid; auto. Qed.
+Proof. rewrite /IntoEmpValid => Hφ Hi1 Hi2. apply Hi1, Hi2, Hφ. Defined.
 Lemma into_emp_valid_forall {A} (φ : A → Type) P x :
   IntoEmpValid (φ x) P → IntoEmpValid (∀ x : A, φ x) P.
-Proof. rewrite /IntoEmpValid; auto. Qed.
-
-Lemma tac_pose_proof Δ j (φ : Prop) P Q :
-  φ →
-  IntoEmpValid φ P →
+Proof. rewrite /IntoEmpValid => Hi1 Hi2. apply Hi1, Hi2. Defined.
+Lemma into_emp_valid_proj φ P : IntoEmpValid φ P → φ → bi_emp_valid P.
+Proof. intros HP. apply HP. Defined.
+
+(** When called by the proof mode, the proof of [P] is produced by calling
+[into_emp_valid_proj]. That call must be transparent to the guardedness
+checker, per https://gitlab.mpi-sws.org/iris/iris/issues/274; hence, it must
+be done _outside_ [tac_pose_proof], so the latter can remain opaque. *)
+Lemma tac_pose_proof Δ j P Q :
+  P →
   match envs_app true (Esnoc Enil j P) Δ with
   | None => False
   | Some Δ' => envs_entails Δ' Q
@@ -472,8 +480,8 @@ Lemma tac_pose_proof Δ j (φ : Prop) P Q :
   envs_entails Δ Q.
 Proof.
   destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
-  rewrite envs_entails_eq => ? HP <-. rewrite envs_app_singleton_sound //=.
-  by rewrite -HP //= intuitionistically_emp emp_wand.
+  rewrite envs_entails_eq => HP <-. rewrite envs_app_singleton_sound //=.
+  by rewrite -HP /= intuitionistically_emp emp_wand.
 Qed.
 
 Lemma tac_pose_proof_hyp Δ i j Q :
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 915b812d0c9f43e916734946815f65064394d27a..786f912f5eef966ea92676e08d9013979f3b1c94 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -777,7 +777,7 @@ Ltac iIntoEmpValid :=
 
 Tactic Notation "iPoseProofCoreLem" open_constr(lem) "as" tactic3(tac) :=
   let Hnew := iFresh in
-  notypeclasses refine (tac_pose_proof _ Hnew _ _ _ lem _ _);
+  notypeclasses refine (tac_pose_proof _ Hnew _ _ (into_emp_valid_proj _ _ _ lem) _);
     [iIntoEmpValid
     |pm_reduce;
      lazymatch goal with