diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5ba909bf2fde70140e246dafdbfcd4f5e99d1853..905b35a3d8434083a3aa9928810b970cec7be8d1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -72,6 +72,11 @@ lemma.
   persistence modality no longer appears at all. This is a step towards using
   the proofmode in logics without a persistence modality.
   The lemma `of_envs_alt` shows equivalence with the old version.
+* Adjust `IntoWand` instances for non-affine BIs: in many cases where
+  `iSpecialize`/`iApply` of an implication previously failed, it will now
+  instead add an `<affine>` modality to the newly generated goal. In some rare
+  cases it might stop working or add an `<affine>` modality where previously
+  none was added.
 
 **Changes in `base_logic`:**
 
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index ba106a831c04c221c006780e17be5e5c5222a311..9d6f219821050af1cd4f09a829fa2c14873c5b82 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -1437,6 +1437,13 @@ Qed.
 Lemma persistent_and_sep_assoc P `{!Persistent P, !Absorbing P} Q R :
   P ∧ (Q ∗ R) ⊣⊢ (P ∧ Q) ∗ R.
 Proof. by rewrite -(persistent_persistently P) persistently_and_sep_assoc. Qed.
+Lemma persistent_impl_wand_affinely P `{!Persistent P, !Absorbing P} Q :
+  (P → Q) ⊣⊢ (<affine> P -∗ Q).
+Proof.
+  apply (anti_symm _).
+  - apply wand_intro_l. rewrite -persistent_and_affinely_sep_l impl_elim_r //.
+  - apply impl_intro_l. rewrite persistent_and_affinely_sep_l wand_elim_r //.
+Qed.
 
 Lemma impl_wand_2 P `{!Persistent P} Q : (P -∗ Q) ⊢ P → Q.
 Proof. apply impl_intro_l. by rewrite persistent_and_sep_1 wand_elim_r. Qed.
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 46f933bb3a23f11cd4c497cc1780ea79b18bbef4..0d431a8549bb4b61a92c7eaa30fe2ea40c420ce9 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -1,5 +1,5 @@
 From iris.bi Require Import telescopes.
-From iris.proofmode Require Import base modality_instances classes.
+From iris.proofmode Require Import base modality_instances classes classes_make.
 From iris.proofmode Require Import ltac_tactics.
 From iris.prelude Require Import options.
 Import bi.
@@ -431,30 +431,49 @@ Global Instance into_wand_wand p q P Q P' :
 Proof.
   rewrite /FromAssumption /IntoWand=> HP. by rewrite HP intuitionistically_if_elim.
 Qed.
-Global Instance into_wand_impl_false_false P Q P' :
-  Absorbing P' → Absorbing (P' → Q) →
-  FromAssumption false P P' → IntoWand false false (P' → Q) P Q.
-Proof.
-  rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
-  by rewrite sep_and impl_elim_l.
+(** Implication instances
+  For non-affine BIs, generally we assume [P → ...] is written in cases where
+  that would be equivalent to [<affine> P -∗ ...], i.e., [P] is absorbing and
+  persistent and an affinely modality is added when proving the premise. If the
+  implication itself or the premise are taken from the persistent context,
+  things become a bit easier and we can drop some of these requirements. We also
+  support arbitrary implications for affine BIs via [BiAffine]. *)
+Global Instance into_wand_impl_false_false P Q P' P'' :
+  Absorbing P →
+  (* Cheap check comes first *)
+  TCOr (BiAffine PROP) (Persistent P) →
+  MakeAffinely P P' →
+  FromAssumption false P'' P' →
+  IntoWand false false (P → Q) P'' Q.
+Proof.
+  rewrite /MakeAffinely /IntoWand /FromAssumption /= => ? Hpers <- ->.
+  apply wand_intro_l. destruct Hpers.
+  - rewrite impl_wand_1 affinely_elim wand_elim_r //.
+  - rewrite persistent_impl_wand_affinely wand_elim_r //.
 Qed.
 Global Instance into_wand_impl_false_true P Q P' :
-  Absorbing P' → FromAssumption true P P' →
+  Absorbing P' →
+  FromAssumption true P P' →
   IntoWand false true (P' → Q) P Q.
 Proof.
   rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
+  rewrite -(persistently_elim P').
+  rewrite persistent_impl_wand_affinely.
   rewrite -(intuitionistically_idemp P) HP.
-  by rewrite -persistently_and_intuitionistically_sep_l persistently_elim impl_elim_r.
+  apply wand_elim_r.
 Qed.
-Global Instance into_wand_impl_true_false P Q P' :
-  Affine P' → FromAssumption false P P' →
-  IntoWand true false (P' → Q) P Q.
+Global Instance into_wand_impl_true_false P Q P' P'' :
+  MakeAffinely P P' →
+  FromAssumption false P'' P' →
+  IntoWand true false (P → Q) P'' Q.
 Proof.
-  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
-  rewrite HP sep_and intuitionistically_elim impl_elim_l //.
+  rewrite /MakeAffinely /IntoWand /FromAssumption /= => <- ->.
+  apply wand_intro_r.
+  rewrite sep_and intuitionistically_elim affinely_elim impl_elim_l //.
 Qed.
 Global Instance into_wand_impl_true_true P Q P' :
-  FromAssumption true P P' → IntoWand true true (P' → Q) P Q.
+  FromAssumption true P P' →
+  IntoWand true true (P' → Q) P Q.
 Proof.
   rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
   rewrite sep_and [(□ (_ → _))%I]intuitionistically_elim impl_elim_r //.
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 5b428e53b2075935c8c53176e46af65c67ba3346..10bed36c02b55335abeb44cc5eaf843405284375 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -95,14 +95,14 @@ Qed.
 
 Lemma tac_assumption_coq Δ P Q :
   (⊢ P) →
-  FromAssumption true P Q →
+  FromAssumption false P Q →
   (if env_spatial_is_nil Δ then TCTrue
    else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ))) →
   envs_entails Δ Q.
 Proof.
   rewrite /FromAssumption /bi_emp_valid /= => HP HPQ H.
   rewrite envs_entails_unseal -(left_id emp%I bi_sep (of_envs Δ)).
-  rewrite -bi.intuitionistically_emp HP HPQ.
+  rewrite HP HPQ.
   destruct (env_spatial_is_nil _) eqn:?.
   - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
   - destruct H; by rewrite sep_elim_l.
@@ -381,7 +381,7 @@ Qed.
 
 Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
   envs_lookup j Δ = Some (q, R) →
-  IntoWand q true R P1 P2 →
+  IntoWand q false R P1 P2 →
   FromPure a P1 φ →
   φ →
   match envs_simple_replace j q (Esnoc Enil j P2) Δ with
@@ -392,10 +392,10 @@ Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
 Proof.
   destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done.
   rewrite envs_entails_unseal=> ?????. rewrite envs_simple_replace_singleton_sound //=.
-  rewrite -intuitionistically_if_idemp (into_wand q true) /=.
+  rewrite -intuitionistically_if_idemp (into_wand q false) /=.
   rewrite -(from_pure a P1) pure_True //.
   rewrite -affinely_affinely_if affinely_True_emp.
-  by rewrite intuitionistically_emp left_id wand_elim_r.
+  by rewrite left_id wand_elim_r.
 Qed.
 
 Lemma tac_specialize_assert_intuitionistic Δ j q P1 P1' P2 R Q :
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index e574cb04d3cf27081f09b64642bfbfc8d3414afb..b8afdcb42905703f06098b5cefa098a6dbbb6f7d 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -288,7 +288,7 @@ Tactic Notation "iAssumptionCoq" :=
   let Hass := fresh in
   match goal with
   | H : ⊢ ?P |- envs_entails _ ?Q =>
-     pose proof (_ : FromAssumption true P Q) as Hass;
+     pose proof (_ : FromAssumption false P Q) as Hass;
      notypeclasses refine (tac_assumption_coq _ P _ H _ _);
        [exact Hass
        |pm_reduce; iSolveTC ||
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 2107e27c68f51b50a19a5d930abc4dd72b0a08dd..749eb5b9724b4f32b92e656613d6ea16ea9c9c2d 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -143,6 +143,50 @@ The command has indeed failed with message:
 Tactic failure: iSpecialize: cannot solve P using done.
 The command has indeed failed with message:
 Tactic failure: iSpecialize: Q not persistent.
+"test_iSpecialize_impl_pure"
+     : string
+1 goal
+  
+  PROP : bi
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  --------------------------------------∗
+  <affine> ⌜φ⌝
+1 goal
+  
+  PROP : bi
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  "H1" : P
+  --------------------------------------â–¡
+  <affine> ⌜φ⌝
+"test_iSpecialize_impl_pure_affine"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  --------------------------------------∗
+  ⌜φ⌝
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  "H1" : P
+  --------------------------------------â–¡
+  ⌜φ⌝
 "test_iAssert_intuitionistic"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index d98cccf87be3558a3a7d96f7930fac01ffb34386..3fe9aed5fe185a7771b32a1214ca2e7e5d19fffa 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -328,6 +328,27 @@ Proof. iIntros "[H1 H2]". by iSplitL. Qed.
 Lemma test_iApply_evar P Q R : (∀ Q, Q -∗ P) -∗ R -∗ P.
 Proof. iIntros "H1 H2". iApply "H1". iExact "H2". Qed.
 
+Lemma test_iApply_1 (P Q : PROP) :
+  (▷ P -∗ Q) -∗ P -∗ Q.
+Proof.
+  iIntros "H HP".
+  iApply ("H" with "HP").
+Qed.
+
+Lemma test_iApply_2 `{!BiAffine PROP} (P Q : PROP) :
+  (▷ P → Q) -∗ P -∗ Q.
+Proof.
+  iIntros "H HP".
+  iApply ("H" with "HP").
+Qed.
+
+Lemma test_iApply_3 `{!BiAffine PROP} (P Q : PROP) :
+  (P → Q) -∗ <pers> P -∗ Q.
+Proof.
+  iIntros "H HP".
+  iApply ("H" with "HP").
+Qed.
+
 Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P -∗ Q -∗ R -∗ Q.
 Proof. iIntros "H1 H2 H3". iAssumption. Qed.
 
@@ -427,6 +448,38 @@ Proof.
   by iFrame "#".
 Qed.
 
+Check "test_iSpecialize_impl_pure".
+Lemma test_iSpecialize_impl_pure (φ : Prop) P Q :
+  φ → □ (⌜φ⌝ → P) -∗ (⌜φ⌝ → Q) -∗ P ∗ Q.
+Proof.
+  iIntros (?) "#H1 H2".
+  (* Adds an affine modality *)
+  iSpecialize ("H1" with "[]"). { Show. done. }
+  iSpecialize ("H2" with "[]"). { Show. done. }
+Restart.
+  iIntros (?) "#H1 H2".
+  (* Solving it directly as a pure goal also works. *)
+  iSpecialize ("H1" with "[% //]").
+  iSpecialize ("H2" with "[% //]").
+  by iFrame.
+Abort.
+
+Check "test_iSpecialize_impl_pure_affine".
+Lemma test_iSpecialize_impl_pure_affine `{!BiAffine PROP} (φ : Prop) P Q :
+  φ → □ (⌜φ⌝ → P) -∗ (⌜φ⌝ → Q) -∗ P ∗ Q.
+Proof.
+  iIntros (?) "#H1 H2".
+  (* Does not add an affine modality *)
+  iSpecialize ("H1" with "[]"). { Show. done. }
+  iSpecialize ("H2" with "[]"). { Show. done. }
+Restart.
+  iIntros (?) "#H1 H2".
+  (* Solving it directly as a pure goal also works. *)
+  iSpecialize ("H1" with "[% //]").
+  iSpecialize ("H2" with "[% //]").
+  by iFrame.
+Abort.
+
 Check "test_iAssert_intuitionistic".
 Lemma test_iAssert_intuitionistic `{!BiBUpd PROP} P :
   □ P -∗ □ |==> P.