diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index ca6989c212238c1df6cce1b908666de58a2fc54e..1ad2380301cbb2264bdf97e8e0cae2e85ae08784 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -14,7 +14,7 @@ Class authG Σ (A : ucmraT) := AuthG {
 Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (authR A) ].
 
 Instance subG_authΣ Σ A : subG (authΣ A) Σ → CMRADiscrete A → authG Σ A.
-Proof. intros ?%subG_inG ?. by split. Qed.
+Proof. solve_inG. Qed.
 
 Section definitions.
   Context `{invG Σ, authG Σ A} {T : Type} (γ : gname).
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index a6b89bd5bb4aa4bc6e8c34c85f812648f52b3e4a..c19c6ccdfb0dc912c86297e7c94af3193ecaaa73 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -16,7 +16,7 @@ Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolC)) *
 
 Instance subG_stsΣ Σ :
   subG boxΣ Σ → boxG Σ.
-Proof. apply subG_inG. Qed.
+Proof. solve_inG. Qed.
 
 Section box_defs.
   Context `{invG Σ, boxG Σ} (N : namespace).
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 36fd54c23582b1bb97235803e30dc1b54d377601..00aa890dfd6ff69ce53e841c58a65f0f21626e42 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -24,7 +24,7 @@ Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors :=
 
 Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
   subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
-Proof. intros ?%subG_inG; split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section definitions.
   Context `{gen_heapG L V Σ}.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 1390c6a583b925e5b7782e610fdf5404ac4e752a..f0a672be02f9df230cad0d2ee1846cc46127d4b2 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -17,6 +17,33 @@ Arguments inG_id {_ _} _.
 Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (F (iPreProp Σ)).
 Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
 
+(** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
+Ltac solve_inG :=
+  (* Get all assumptions *)
+  intros;
+  (* Unfold the top-level xΣ *)
+  lazymatch goal with
+  | H : subG (?xΣ _) _ |- _ => try unfold xΣ in H
+  | H : subG ?xΣ _ |- _ => try unfold xΣ in H
+  end;
+  (* Take apart subG for non-"atomic" lists *)
+  repeat match goal with
+         | H : subG (gFunctors.app _ _) _ |- _ => apply subG_inv in H; destruct H
+         end;
+  (* Try to turn singleton subG into inG; but also keep the subG for typeclass
+     resolution -- to keep them, we put them onto the goal. *)
+  repeat match goal with
+         | H : subG _ _ |- _ => move:(H); (apply subG_inG in H || clear H)
+         end;
+  (* Again get all assumptions *)
+  intros;
+  (* We support two kinds of goals: Things convertible to inG;
+     and records with inG and typeclass fields. Try to solve the
+     first case. *)
+  try done;
+  (* That didn't work, now we're in for the second case. *)
+  split; (assumption || by apply _).
+
 (** * Definition of the connective [own] *)
 Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
   iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 7fc022f00844cd212375214e2b10d88a8ae20949..0ea8dbdb5a61058f06b8f8a43d781592a1bf0f86 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -10,7 +10,7 @@ Definition savedPropΣ (F : cFunctor) : gFunctors :=
   #[ GFunctor (agreeRF (â–¶ F)) ].
 
 Instance subG_savedPropΣ  {Σ F} : subG (savedPropΣ F) Σ → savedPropG Σ F.
-Proof. apply subG_inG. Qed.
+Proof. solve_inG. Qed.
 
 Definition saved_prop_own `{savedPropG Σ F}
     (γ : gname) (x : F (iProp Σ)) : iProp Σ :=
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 5390919b32bc39c3e55de70a69faf88db3d92cd5..ddedc7272a86ae7efd68e4ab18a0330bf7e23db7 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -13,7 +13,7 @@ Class stsG Σ (sts : stsT) := StsG {
 Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (stsR sts) ].
 Instance subG_stsΣ Σ sts :
   subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
-Proof. intros ?%subG_inG ?. by split. Qed.
+Proof. solve_inG. Qed.
 
 Section definitions.
   Context `{stsG Σ sts} (γ : gname).
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 3d5ba129349893211b00d7daccf5dbdc03f0cf4f..9a4a1115bb788463937d2e65bf991736fdc44549 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -12,7 +12,7 @@ Class heapPreG Σ := HeapPreG {
 
 Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
-Proof. intros [? ?]%subG_inv; split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
   (∀ `{heapG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
diff --git a/theories/heap_lang/lib/barrier/proof.v b/theories/heap_lang/lib/barrier/proof.v
index 7f691d03609b83bf248a1700ff5f9ef700a2f26a..c94a47a4339e4b682fc2e0945c1ad786293be5d4 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/theories/heap_lang/lib/barrier/proof.v
@@ -8,7 +8,6 @@ From iris.heap_lang.lib.barrier Require Import protocol.
 Set Default Proof Using "Type".
 
 (** The CMRAs/functors we need. *)
-(* Not bundling heapG, as it may be shared with other users. *)
 Class barrierG Σ := BarrierG {
   barrier_stsG :> stsG Σ sts;
   barrier_savedPropG :> savedPropG Σ idCF;
@@ -16,7 +15,7 @@ Class barrierG Σ := BarrierG {
 Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ idCF].
 
 Instance subG_barrierΣ {Σ} : subG barrierΣ Σ → barrierG Σ.
-Proof. intros [? [? _]%subG_inv]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 663c55fa6765a43b1bea76c1cca9bd43a4fdf8c2..deffcca5e893a0669f8abbe4f402c07cd4b7bc11 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -17,7 +17,7 @@ Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
 Definition mcounterΣ : gFunctors := #[GFunctor (authR mnatUR)].
 
 Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ → mcounterG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section mono_proof.
   Context `{!heapG Σ, !mcounterG Σ} (N : namespace).
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 7375295f9f8384a5e482597a7daa57e98dd56975..4c9b25a6a0de1e5135e84dab6a810015a8879371 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -23,7 +23,7 @@ Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
 Definition spawnΣ : gFunctors := #[GFunctor (exclR unitC)].
 
 Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 1acd5f3c3c1293354ad86c7f46bb9f3f8b15d585..4d70eb77b30a0b99d85af9879490d0523a21a397 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -18,7 +18,7 @@ Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
 Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
 
 Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
-Proof. intros ?%subG_inG. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section proof.
   Context `{!heapG Σ, !lockG Σ} (N : namespace).
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index c9eb0b4fcdf1d409feff2a2eb8b5c556ddb2faf8..2900b73c4488b9e8489ad0eea01ae453773dd687 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -34,7 +34,7 @@ Definition tlockΣ : gFunctors :=
   #[ GFunctor (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))) ].
 
 Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
-Proof. by intros ?%subG_inG. Qed.
+Proof. solve_inG. Qed.
 
 Section proof.
   Context `{!heapG Σ, !tlockG Σ} (N : namespace).
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 47f29c45a1b87c2af5bad7f1571f5019c69e0b3f..4738711a472c50e4885f3572964da3343f22aabe 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -19,9 +19,7 @@ Class invPreG (Σ : gFunctors) : Set := WsatPreG {
 }.
 
 Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
-Proof.
-  intros [?%subG_inG [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv; by constructor.
-Qed.
+Proof. solve_inG. Qed.
 
 (* Allocation *)
 Lemma wsat_alloc `{invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 58bf6d94c19c9be4f36c9335539457ebf73714c8..6f08c2b426aa27d104d1019bb60295bb87ed2be0 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -29,7 +29,7 @@ Class ownPPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
 Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) Σ).
 
 Instance subG_ownPΣ {Λstate Σ} : subG (ownPΣ Λstate) Σ → ownPPreG' Λstate Σ.
-Proof. intros [??%subG_inG]%subG_inv; constructor; apply _. Qed.
+Proof. solve_inG. Qed.
 
 (** Ownership *)
 Definition ownP `{ownPG' Λstate Σ} (σ : Λstate) : iProp Σ :=
diff --git a/theories/tests/counter.v b/theories/tests/counter.v
index c64e145af15a72b151bd05195d46166839941f67..9206a9fcca8da6b8583539ce5724ea533db7cf34 100644
--- a/theories/tests/counter.v
+++ b/theories/tests/counter.v
@@ -75,7 +75,7 @@ End M.
 Class counterG Σ := CounterG { counter_tokG :> inG Σ M_UR }.
 Definition counterΣ : gFunctors := #[GFunctor M_UR].
 Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section proof.
 Context `{!heapG Σ, !counterG Σ}.
diff --git a/theories/tests/joining_existentials.v b/theories/tests/joining_existentials.v
index 2f5ce6df6a8d94ec2eb31bec53dcf30bc1a379af..2d846d3c775b170b8afe7b3126ab78067a10b5d6 100644
--- a/theories/tests/joining_existentials.v
+++ b/theories/tests/joining_existentials.v
@@ -17,7 +17,7 @@ Class oneShotG (Σ : gFunctors) (F : cFunctor) :=
 Definition oneShotΣ (F : cFunctor) : gFunctors :=
   #[ GFunctor (csumRF (exclRF unitC) (agreeRF (â–¶ F))) ].
 Instance subG_oneShotΣ {Σ F} : subG (oneShotΣ F) Σ → oneShotG Σ F.
-Proof. apply subG_inG. Qed.
+Proof. solve_inG. Qed.
 
 Definition client eM eW1 eW2 : expr :=
   let: "b" := newbarrier #() in
diff --git a/theories/tests/one_shot.v b/theories/tests/one_shot.v
index faa24883c61b119f9f05e7b801d4cfa9074418ed..a678c1f5c7a67fb455246124d4a5d485a95df4b0 100644
--- a/theories/tests/one_shot.v
+++ b/theories/tests/one_shot.v
@@ -27,7 +27,7 @@ Definition Shot (n : Z) : one_shotR := (Cinr (to_agree n) : one_shotR).
 Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
 Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
 Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section proof.
 Set Default Proof Using "Type*".