using Jason's first definition

Patrick Nicodemus · Patrick Nicodemus · commit a779b6556289 · 2025-03-08T11:48:41.000-05:00
diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v
@@ -248,7 +248,7 @@ Section AbelGroup.
     intros x y z; cbn beta.
     lhs nrapply ap.
     2: rhs nrapply ap.
-    1,3: lhs rapply inverse_sg_op; nrapply (ap (.* _)); rapply inverse_sg_op.
+    1,3: lhs tapply inverse_sg_op; nrapply (ap (.* _)); tapply inverse_sg_op.
     change (abel_in z^ * abel_in y^ * abel_in x^
       = abel_in y^ * abel_in z^ * abel_in x^).
     apply (ap (.* _)).
diff --git a/theories/Algebra/AbGroups/TensorProduct.v b/theories/Algebra/AbGroups/TensorProduct.v
@@ -251,7 +251,7 @@ Definition ab_tensor_prod_ind_hprop_triple {A B C : AbGroup}
 Proof.
   rapply (ab_tensor_prod_ind_hprop P).
   - intros a.
-    rapply (ab_tensor_prod_ind_hprop (fun x => P (tensor _ x))).
+    rapply (ab_tensor_prod_ind_hprop (fun x => P (tensor _ x))); cbv beta.
     + nrapply Hin.
     + intros x y Hx Hy.
       rewrite tensor_dist_l.
@@ -781,15 +781,15 @@ Proof.
   - snrapply ab_tensor_prod_ind_homotopy.
     intros x.
     change (f $o g $o grp_homo_tensor_l x $== grp_homo_tensor_l x).
-    rapply Abel_ind_hprop.
+    rapply Abel_ind_hprop; cbv beta.
     change (@abel_in ?G) with (grp_homo_map (@abel_unit G)).
     repeat change (cat_comp (A:=AbGroup) ?f ?g) with (cat_comp (A:=Group) f g).
     change (forall y, grp_homo_map ?f (abel_unit y) = grp_homo_map ?g (abel_unit y))
       with (cat_comp (A:=Group) f abel_unit $== cat_comp (A:=Group) g abel_unit).
     rapply FreeGroup_ind_homotopy.
     intros y; revert x.
     change (f $o g $o grp_homo_tensor_r (freeabgroup_in y) $== grp_homo_tensor_r (freeabgroup_in y)).
-    rapply Abel_ind_hprop.
+    rapply Abel_ind_hprop; cbv beta.
     change (@abel_in ?G) with (grp_homo_map (@abel_unit G)).
     repeat change (cat_comp (A:=AbGroup) ?f ?g) with (cat_comp (A:=Group) f g).
     change (forall y, grp_homo_map ?f (abel_unit y) = grp_homo_map ?g (abel_unit y))
diff --git a/theories/Algebra/AbSES/Core.v b/theories/Algebra/AbSES/Core.v
@@ -713,8 +713,6 @@ Lemma abses_from_surjection {E B : AbGroup@{u}} (p : E $-> B) `{IsSurjection p}
   : AbSES B (ab_kernel p).
 Proof.
   srapply (Build_AbSES E _ p).
-  1: exact (subgroup_incl _).
-  1: exact _.
   snrapply Build_IsExact.
   - apply phomotopy_homotopy_hset.
     intros [e q]; cbn.
@@ -734,7 +732,7 @@ Proof.
     refine (ap _ p^ @ _).
     tapply cx_isexact.
   - apply isequiv_surj_emb.
-    1: rapply cancelR_conn_map.
+    1: tapply cancelR_conn_map.
     apply isembedding_isinj_hset.
     srapply Quotient_ind2_hprop; intros x y.
     intro p.
diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
@@ -1122,7 +1122,7 @@ Proof.
   snrapply subgroup_image_rec.
   intros x Jx.
   change (subgroup_image f J ((grp_conj y $o f) x)).
-  revert y; rapply (conn_map_elim (Tr (-1)) f); intros y.
+  revert y; rapply (conn_map_elim (Tr (-1)) f); intros y; cbv beta.
   rewrite <- grp_homo_conj.
   nrapply subgroup_image_in.
   by rapply isnormal_conj.
diff --git a/theories/Algebra/Rings/CRing.v b/theories/Algebra/Rings/CRing.v
@@ -29,7 +29,7 @@ Definition Build_CRing' (R : AbGroup) `(!One R, !Mult R)
   : CRing.
 Proof.
   snrapply Build_CRing.
-  - rapply (Build_Ring R); only 1,2,4: exact _.
+  - rapply (Build_Ring R).
     + intros x y z.
       lhs nrapply comm.
       lhs rapply dist_l.
diff --git a/theories/Basics/Tactics.v b/theories/Basics/Tactics.v
@@ -322,15 +322,15 @@ Tactic Notation "snrefine" uconstr(term) := simple notypeclasses refine term; gl
 (** This tactic is weaker than [tapply], and equivalent in strength to [nrapply], i.e., it should succeed iff [nrapply] succeeds, but it solves all possible typeclasses afterward. The implementation is: try [nrefine t, t _, t _ _], ... until success; upon success, revert the last (successful) application of [nrefine] and call [refine (t _ _ _)]. *)
 (** TODO: Find a nicer implementation of this tactic. *)
 Tactic Notation "rapply" uconstr(term)
-  := do_with_holes ltac:(fun x => assert_succeeds (nrefine x); refine x) term.
+  := do_with_holes ltac:(fun x => simple notypeclasses refine x) term; try typeclasses eauto; shelve_unifiable.
 Tactic Notation "rapply'" uconstr(term)
-  := do_with_holes' ltac:(fun x => assert_succeeds (nrefine x); refine x) term.
+:= do_with_holes' ltac:(fun x => simple notypeclasses refine x) term; try typeclasses eauto; shelve_unifiable.
 
 (** See comment for [rapply]. This cannot be simplified to [snrefine x] because we don't want the [global_axiom] tactic to run here. *)
 Tactic Notation "srapply" uconstr(term)
-  := do_with_holes ltac:(fun x => assert_succeeds (simple notypeclasses refine x); srefine x) term.
+  := do_with_holes ltac:(fun x => simple notypeclasses refine x) term; try typeclasses eauto.
 Tactic Notation "srapply'" uconstr(term)
-:= do_with_holes' ltac:(fun x => assert_succeeds (simple notypeclasses refine x); srefine x) term.
+  := do_with_holes' ltac:(fun x => simple notypeclasses refine x) term; try typeclasses eauto.
 
 Tactic Notation "nrapply" uconstr(term)
   := do_with_holes ltac:(fun x => nrefine x) term.
diff --git a/theories/Classes/theory/rings.v b/theories/Classes/theory/rings.v
@@ -254,7 +254,8 @@ Section ring_props.
   Lemma negate_swap_r : forall x y, x - y = -(y - x).
   Proof.
     intros; symmetry.
-    lhs rapply groups.inverse_sg_op.
+    Set Printing All.
+    lhs tapply groups.inverse_sg_op.
     f_ap.
     apply involutive.
   Defined.
@@ -465,7 +466,7 @@ Section ringmor_props.
 
   Definition preserves_negate x : f (- x) = - f x.
   Proof.
-    rapply preserves_inverse.
+    tapply preserves_inverse.
   Defined.
 
   Lemma preserves_minus x y : f (x - y) = f x - f y.
diff --git a/theories/Colimits/Colimit_Coequalizer.v b/theories/Colimits/Colimit_Coequalizer.v
@@ -80,8 +80,7 @@ Section Coequalizer.
     : Coeq f g <~> Coequalizer f g.
   Proof.
     srapply colimit_unicity.
-    3: eapply iscoequalizer_Coeq.
-    eapply iscolimit_colimit.
+    eapply iscoequalizer_Coeq.
   Defined.
 
 End Coequalizer.
diff --git a/theories/Colimits/Colimit_Flattening.v b/theories/Colimits/Colimit_Flattening.v
@@ -224,9 +224,7 @@ Section Flattening.
   Definition flattening_lemma : Colimit (diagram_sigma E) <~> sig E'.
   Proof.
     srapply colimit_unicity.
-    3: apply iscolimit_colimit.
     rapply Build_IsColimit.
-    apply unicocone_cocone_E'.
   Defined.
 
 End Flattening.
diff --git a/theories/Colimits/Colimit_Pushout.v b/theories/Colimits/Colimit_Pushout.v
@@ -161,7 +161,8 @@ Section is_PO_pushout.
 
   Definition is_PO_pushout : is_PO f g (Pushout f g).
   Proof.
-    srapply Build_IsColimit.
+    unfold is_PO. 
+    unshelve eapply Build_IsColimit.
     - srapply Build_span_cocone.
       + exact (push o inl).
       + exact (push o inr).
@@ -201,8 +202,7 @@ Section is_PO_pushout.
   Definition equiv_pushout_PO : Pushout f g <~> PO f g.
   Proof.
     srapply colimit_unicity.
-    3: eapply is_PO_pushout.
-    eapply iscolimit_colimit.
+    eapply is_PO_pushout.
   Defined.
 
   Definition equiv_pushout_PO_beta_pglue (a : A)
diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v
@@ -151,7 +151,7 @@ Global Instance ishprop_isexact_hset `{Univalence} {F X Y : pType} `{IsHSet Y}
   : IsHProp (IsExact n i f).
 Proof.
   rapply (transport (fun A => IsHProp A) (x := { cx : IsComplex i f & IsConnMap n (cxfib cx) })).
-  2: exact _.
+  2: cbn; exact _.
   apply path_universe_uncurried; issig.
 Defined.
 
@@ -288,7 +288,6 @@ Global Instance isequiv_cxfib {O : Modality} {F X Y : pType} {i : F ->* X} {f :
   : IsEquiv (cxfib cx_isexact).
 Proof.
   rapply isequiv_conn_ino_map.
-  1: apply ex.
   rapply (cancelL_mapinO _ _ pr1).
 Defined.
 
diff --git a/theories/Modalities/Lex.v b/theories/Modalities/Lex.v
@@ -400,7 +400,7 @@ Definition lex_gen `{Univalence} (O : Modality) `{IsAccModality O}
                IsConnected O (x = y))
   : Lex O.
 Proof.
-  srapply lex_from_inO_typeO; [ exact _ | intros i ].
+  srapply lex_from_inO_typeO; intros i.
   rapply ooextendable_TypeO_from_extension; intros P; srefine (_;_).
   1:intros; exists (forall x, P x); exact _.
   assert (wc : forall y z, P y <~> P z).
diff --git a/theories/Modalities/Meet.v b/theories/Modalities/Meet.v
@@ -298,7 +298,7 @@ Section LexMeet.
     apply IHn.
     - rapply mapinO_diagonal.
       pose (O_eq_Tr n.+1).
-      rapply (mapinO_O_leq _ (Sep (Tr n.+1))).
+      rapply (mapinO_O_leq (Tr n.+2) (Sep (Tr n.+1))).
     - apply plusconnmap_diagonal; assumption.
   Defined.
 
diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v
@@ -122,7 +122,7 @@ Section Subuniverse.
   Proof.
     split.
     - exact _. (* Uses the instance mapinO_pr1 above. *)
-    - rapply functor_forall; intros a x.
+    - rapply functor_forall; intros a x. cbv beta in *.
       exact (inO_equiv_inO (hfiber pr1 a)
                            (hfiber_fibration a B)^-1%equiv).
   Defined.
diff --git a/theories/Sets/Ordinals.v b/theories/Sets/Ordinals.v
@@ -434,8 +434,6 @@ Proof.
     try exact _.
   srapply (isordinal_simulation pr1).
   - unfold lt. exact _.
-  - exact _.
-  - exact _.
   - constructor.
     + intros x y x_y. exact x_y.
     + intros b a' a'_b; cbn in *. apply tr.
diff --git a/theories/Spaces/Nat/Core.v b/theories/Spaces/Nat/Core.v
@@ -1404,7 +1404,7 @@ Proof.
   intros H.
   rewrite nat_add_comm.
   apply (nat_add_r_monotone k) in H.
-  rapply leq_trans.
+  exact (leq_trans _ H).
 Defined.
 
 Definition leq_moveL_nM {n m} k : n - k <= m -> n <= m + k.
diff --git a/theories/Spaces/Nat/Division.v b/theories/Spaces/Nat/Division.v
@@ -735,7 +735,9 @@ Proof.
   - intros q H1 H2.
     rapply nat_divides_r_gcd.
   - rapply (nat_divides_trans (nat_divides_l_gcd_l _ _)).
-  - apply nat_divides_r_gcd; rapply nat_divides_trans.
+  - apply nat_divides_r_gcd.
+    + rapply (nat_divides_trans (m:=nat_gcd n m)).
+    + rapply nat_divides_trans.
 Defined.
 
 (** If [nat_gcd n m] is [0], then [n] must also be [0]. *)
diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v
@@ -334,7 +334,7 @@ Proof.
     2: exact _. (* The second part is an equivalence, so it's an embedding. *)
     nrefine (mapinO_compose _ (functor_forall_id _)).
     1: exact _. (* The first part is an equivalence, so it's an embedding. *)
-    rapply mapinO_functor_forall_id.
+    rapply mapinO_functor_forall_id; cbv beta.
     intro y.
     apply isembedding_equiv_fun.
   - (* The composite is an equivalence because it is homotopic to the identity. *)
diff --git a/theories/WildCat/Adjoint.v b/theories/WildCat/Adjoint.v
@@ -375,10 +375,9 @@ Proof.
     nrefine (natequiv_compose (natequiv_adjunction_l adj1 _) _).
     exact (natequiv_prewhisker (A:=A^op) (B:=B^op)
       (natequiv_adjunction_l adj2 y) F). }
-  intros x.
+  intros x. cbv beta.
   rapply is1natural_comp.
-  + exact (is1natural_prewhisker G' (natequiv_adjunction_r adj1 x)).
-  + tapply is1natural_equiv_adjunction_r.
+  exact (is1natural_prewhisker G' (natequiv_adjunction_r adj1 x)).
 Defined.
 
 (** Replace the left functor in an adjunction by a naturally equivalent one. *)
@@ -409,7 +408,6 @@ Proof.
     rapply (natequiv_postwhisker _ e). }
   intros y.
   rapply is1natural_comp.
-  2: exact _.
   rapply is1natural_yoneda.
 Defined.
 
