rapply definition variation

theories/Algebra/AbGroups/AbHom.v

@@ -150,10 +150,10 @@ Proof.
   - exact (functor_ab_coeq a^-1$ b^-1$ (hinverse _ _ p) (hinverse _ _ q)).
   - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
       $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
-    rapply cate_isretr.
+      exact (cate_isretr _).
   - nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
       $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
-    rapply cate_issect.
+      exact (cate_issect _).
 Defined.
 
 (** ** The bifunctor [ab_hom] *)

theories/Algebra/AbGroups/TensorProduct.v

@@ -695,7 +695,7 @@ Proof.
     + rapply (fmap01 ab_tensor_prod A).
       nrapply ab_coeq_in.
     + refine (_^$ $@ fmap02 ab_tensor_prod _ _ $@ _).
-      1,3: rapply fmap01_comp.
+      1,3: exact (fmap01_comp _ _ _ _).
       nrapply ab_coeq_glue.
   - snrapply ab_tensor_prod_rec'.
     + intros a.

theories/Algebra/AbSES/Core.v

@@ -403,7 +403,7 @@ Proof.
   induction p.
   refine (ap (ap f) (eisretr _ _) @ _).
   nrefine (_ @ ap equiv_path_abses_iso _).
-  2: { rapply path_hom.
+  2: { refine (path_hom _).
        srefine (_ $@ fmap2 _ _).
        2: exact (Id E).
        2: intro x; reflexivity.
@@ -426,7 +426,7 @@ Proof.
   2: apply (abses_ap_fmap g).
   nrefine (_ @ (abses_path_data_compose_beta _ _)^).
   nrapply (ap equiv_path_abses_iso).
-  rapply path_hom.
+  refine (path_hom _).
   reflexivity.
 Defined.
 
@@ -575,7 +575,7 @@ Proof.
   apply path_sigma_hprop; cbn.
   apply grp_cancelL1.
   refine (ap (fun x => - s x) _ @ _).
-  1: rapply cx_isexact.
+  1: refine (cx_isexact  _ ).
   exact (ap _ (grp_homo_unit _) @ grp_inv_unit).
 Defined.
 
@@ -629,7 +629,7 @@ Proof.
   lhs nrapply ab_biprod_functor_beta.
   *)
   nrapply path_prod'.
-  2: rapply cx_isexact.
+  2: refine (cx_isexact _).
   (* The LHS of the remaining goal is definitionally equal to
        (grp_iso_inverse (grp_iso_cxfib (isexact_inclusion_projection E)) $o
          (projection_split_to_kernel E h $o inclusion E)) a
@@ -686,12 +686,12 @@ Lemma abses_kernel_iso `{Funext} {A E B : AbGroup} (i : A $-> E) (p : E $-> B)
 Proof.
   snrapply Build_GroupIsomorphism.
   - apply (grp_kernel_corec i).
-    rapply cx_isexact.
+    refine cx_isexact.
   - apply isequiv_surj_emb.
-    2: rapply (cancelL_mapinO _ (grp_kernel_corec _ _) _).
+    2: refine (cancelL_mapinO _ (grp_kernel_corec _ _) _ _ _).
     intros [y q].
     assert (a : Tr (-1) (hfiber i y)).
-    1: by rapply isexact_preimage.
+    1: by refine (isexact_preimage _ _ _ _ _).
     strip_truncations; destruct a as [a r].
     rapply contr_inhabited_hprop.
     refine (tr (a; _)); cbn.
@@ -732,7 +732,7 @@ Proof.
   - snrapply (quotient_abgroup_rec _ _ g).
     intros e; rapply Trunc_rec; intros [a p].
     refine (ap _ p^ @ _).
-    rapply cx_isexact.
+    refine (cx_isexact _).
   - apply isequiv_surj_emb.
     1: rapply cancelR_conn_map.
     apply isembedding_isinj_hset.

theories/Algebra/AbSES/Pullback.v

@@ -460,7 +460,7 @@ Proof.
     { refine (ap _ (abses_path_data_V p) @ _).
       apply eissect. }
     refine (ap (fun x => x $@ _) _).
-    rapply gpd_strong_1functor_V. }
+    exact (gpd_strong_1functor_V _ _). }
   refine (equiv_path_sigma_hprop _ _ oE _).
   apply equiv_path_groupisomorphism.
 Defined.

theories/Algebra/AbSES/PullbackFiberSequence.v

@@ -105,13 +105,13 @@ Proof.
       revert_opaque f; apply Trunc_rec; intros [f q0].
       (* Since [projection F f] is in the kernel of [projection E], we find a preimage in [B]. *)
       assert (b : merely (hfiber (inclusion E) (projection F f))).
-      1: { rapply isexact_preimage.
+      1: { refine (isexact_preimage _ _ _ _ _).
            exact (ap _ q0 @ q). }
       revert_opaque b; apply Trunc_rec; intros [b q1].
       (* The difference [f - b] in [F] is in the kernel of [projection F], hence lies in [A]. *)
       assert (a : merely (hfiber (inclusion F)
                                  (sg_op f (-(grp_pullback_pr1 _ _ (p^$.1 (ab_biprod_inr b))))))).
-      1: { rapply isexact_preimage.
+      1: { refine (isexact_preimage _ _ _ _ _).
            refine (grp_homo_op _ _ _ @ _).
            refine (ap (fun x => _ + x) (grp_homo_inv _ _) @ _).
            refine (ap (fun x => _ - x) (abses_pullback_inclusion_transpose_beta (inclusion E) F p b @ q1) @ _).
@@ -171,7 +171,7 @@ Proof.
   change (equiv_ptransformation_phomotopy (iscomplex_abses_pullback' _ _ (iscomplex_abses E)) U)
     with (equiv_path_abses_iso ((iscomplex_abses_pullback' _ _ (iscomplex_abses E)).1 U)).
   apply (ap equiv_path_abses_iso).
-  rapply path_hom.
+  refine (path_hom _ ).
   refine (_ $@R abses_pullback_compose' (inclusion E) (projection E) U);
     unfold trans_comp.
   refine (_ $@R abses_pullback_homotopic' (projection E $o inclusion E) grp_homo_const (iscomplex_abses E) U).
@@ -248,7 +248,7 @@ Proof.
        apply eissect. }
   refine (equiv_concat_l _ _ oE _).
   1: { refine (ap (fun x => (x $@ _).1) _).
-       rapply gpd_strong_1functor_V. }
+       exact (gpd_strong_1functor_V _ _). }
   apply equiv_path_groupisomorphism.
 Defined.
 
@@ -366,8 +366,8 @@ Lemma hfiber_cxfib'_induced_path' `{Univalence} {A B C : AbGroup} (E : AbSES C B
   : path_hfiber_cxfib' (hfiber_cxfib'_inhabited E F p) Y.
 Proof.
   exists (hfiber_cxfib'_induced_path'0 E F p Y).
-  rapply gpd_moveR_Vh.
-  rapply gpd_moveL_hM.
+  refine (gpd_moveR_Vh _).
+  refine (gpd_moveL_hM _).
   rapply gpd_moveR_Vh.
   intro x.
   srapply equiv_path_pullback_hset; split.

theories/Algebra/ooGroup.v

@@ -133,7 +133,7 @@ Proof.
   rewrite <- p.
   rewrite !loops_functor_group.
   apply ap.
-  symmetry; rapply (fmap_comp loops).
+  symmetry; exact (fmap_comp loops _ _ _).
 Qed.
 
 Definition grouphom_idmap (G : ooGroup) : ooGroupHom G G
@@ -285,13 +285,13 @@ Global Instance is0functor_group_to_oogroup : Is0Functor group_to_oogroup.
 Proof.
   snrapply Build_Is0Functor.
   intros G H f.
-  by rapply (fmap pClassifyingSpace).
+  by exact (fmap pClassifyingSpace f).
 Defined.
 
 Global Instance is1functor_group_to_oogroup : Is1Functor group_to_oogroup.
 Proof.
   snrapply Build_Is1Functor; hnf; intros.
-  1: by rapply (fmap2 pClassifyingSpace).
-  1: by rapply (fmap_id pClassifyingSpace).
-  by rapply (fmap_comp pClassifyingSpace).
+  1: by exact (fmap2 pClassifyingSpace X).
+  1: by exact (fmap_id pClassifyingSpace _).
+  by exact (fmap_comp pClassifyingSpace _ _).
 Defined.

theories/Basics/Tactics.v

@@ -320,7 +320,9 @@ Tactic Notation "snrefine" uconstr(term) := simple notypeclasses refine term; gl
 
 (** Note that the Coq standard library has a [rapply], but it is like our [rapply'] with many-holes first.  We prefer fewer-holes first, for instance so that a theorem producing an equivalence will by preference be used to produce an equivalence rather than to apply the coercion of that equivalence to a function. *)
 Tactic Notation "rapply" uconstr(term)
-  := do_with_holes ltac:(fun x => refine x) term.
+  := do_with_holes (ltac:(fun x => unshelve nrefine x; try typeclasses eauto)) term.
+  (* := do_with_holes ltac:(fun x => match goal with | [|-?G] => unify x ?G ; refine x end). *)
+  (* := do_with_holes ltac:(fun x => try (try (nrefine x || fail 2); fail); refine x) term. *)
 Tactic Notation "rapply'" uconstr(term)
   := do_with_holes' ltac:(fun x => refine x) term.
 

theories/Colimits/Coeq.v

@@ -26,8 +26,7 @@ Definition Coeq_ind {B A f g} (P : @Coeq B A f g -> Type)
   : forall w, P w.
 Proof.
   rapply GraphQuotient_ind.
-  intros a b [x [[] []]].
-  exact (cglue' x).
+  2: intros a b [x [[] []]]; exact (cglue' x).
 Defined.
 
 Lemma Coeq_ind_beta_cglue {B A f g} (P : @Coeq B A f g -> Type)
@@ -43,8 +42,7 @@ Definition Coeq_rec {B A f g} (P : Type) (coeq' : A -> P)
   : @Coeq B A f g -> P.
 Proof.
   rapply GraphQuotient_rec.
-  intros a b [x [[] []]].
-  exact (cglue' x).
+  2: intros a b [x [[] []]]; exact (cglue' x).
 Defined.
 
 Definition Coeq_rec_beta_cglue {B A f g} (P : Type) (coeq' : A -> P)

theories/Colimits/CoeqUnivProp.v

@@ -128,10 +128,7 @@ Section UnivPropNat.
 
   (** Help Coq find the same graph structure for the sigma-groupoid of [Coeq_ind_data] when precomposing with [functor_coeq]. *)
   Local Instance isgraph_Coeq_ind_data_total
-    : IsGraph (sig (Coeq_ind_data f g (P o functor_coeq h k p q))).
-  Proof.
-    rapply isgraph_total.
-  Defined.
+    : IsGraph (sig (Coeq_ind_data f g (P o functor_coeq h k p q))) := isgraph_total _.
 
   (** Given a map out of [A'] that coequalizes the parallel pair [f'] and [g'], we construct a map out of [A] that coequalizes [f] and [g]. Precomposing with [k] yields a dependent map [forall a : A, P (coeq (k a))], and [functor_coeq_beta_cglue] gives us a way to relate the paths. *)
   Definition functor_Coeq_ind_data

theories/Colimits/Colimit_Flattening.v

@@ -226,7 +226,6 @@ Section Flattening.
     srapply colimit_unicity.
     3: apply iscolimit_colimit.
     rapply Build_IsColimit.
-    apply unicocone_cocone_E'.
   Defined.
 
 End Flattening.

theories/Colimits/Sequential.v

@@ -42,8 +42,8 @@ Proof.
     intros n.
     exact (const (a n.+1)). }
   rapply contr_equiv'.
-  1: rapply equiv_functor_colimit.
-  1: rapply (equiv_sequence B A).
+  2: rapply equiv_functor_colimit.
+  2: rapply (equiv_sequence B A).
   1: reflexivity.
   { intros n e.
     exists equiv_idmap.

theories/Extensions.v

@@ -719,9 +719,9 @@ Proof.
              ExtendableAlong 1 cyl (fun x:Cyl h => DPath C' (cglue x) (u x) (v x))).
   { intros u v.
     rapply extendable_postcompose'.
-    2:{ rapply (cancelL_extendable 1 _ cyl pr_cyl).
-        - rapply extendable_equiv.
-        - exact (eh (fun x => cglue x # u (cyr x)) (v o cyr)). }
+    3:{ rapply (cancelL_extendable 1 _ cyl pr_cyl).
+        2: rapply extendable_equiv.
+        2: exact (eh (fun x => cglue x # u (cyr x)) (v o cyr)). }
     intros x; subst C'.
     refine ((dp_compose (pr_cylcoeq p q) C _)^-1 oE _).
     symmetry; srapply equiv_ds_fill_lr.

theories/HFiber.v

@@ -126,7 +126,7 @@ Definition hfiber_functor_hfiber {A B C D}
   : hfiber (functor_hfiber p b) (c;q)
     <~> hfiber (functor_hfiber (fun x => (p x)^) c) (b;q^).
 Proof.
-  rapply (equiv_functor_sigma_id _ oE _ oE (equiv_functor_sigma_id _)^-1).
+  refine (equiv_functor_sigma_id _ oE _ oE (equiv_functor_sigma_id _)^-1).
   1,3:intros; rapply equiv_path_sigma.
   refine (equiv_sigma_assoc _ _ oE _ oE (equiv_sigma_assoc _ _)^-1).
   apply equiv_functor_sigma_id; intros a; cbn.

theories/Homotopy/Bouquet.v

@@ -82,7 +82,7 @@ Section AssumeUnivalence.
     intros f.
     refine (_ @ @is1natural_equiv_pi1bouquet_rec S _ _ f grp_homo_id).
     simpl; f_ap; symmetry.
-    rapply (cat_idr_strong f).
+    exact (cat_idr_strong f).
   Defined.
 
 End AssumeUnivalence.

theories/Homotopy/EMSpace.v

@@ -62,7 +62,7 @@ Section EilenbergMacLane.
     : pTr n.+2 X <~>* pTr n.+2 (loops (psusp X)).
   Proof.
     snrapply Build_pEquiv.
-    1: rapply (fmap (pTr _) (loop_susp_unit _)).
+    1: exact (fmap (pTr _) (loop_susp_unit _)).
     nrapply O_inverts_conn_map.
     nrapply (isconnmap_pred_add n.-2).
     rewrite 2 trunc_index_add_succ.

theories/Homotopy/ExactSequence.v

@@ -48,7 +48,7 @@ Definition iscomplex_ptr (n : trunc_index) {F X Y : pType}
 Proof.
   refine ((fmap_comp (pTr n) i f)^* @* _).
   refine (_ @* ptr_functor_pconst n).
-  rapply (fmap2 (pTr _)); assumption.
+  refine (fmap2 (pTr _) _); assumption.
 Defined.
 
 (** Loop spaces preserve complexes. *)
@@ -57,7 +57,7 @@ Definition iscomplex_loops {F X Y : pType}
   : IsComplex (fmap loops i) (fmap loops f).
 Proof.
   refine ((fmap_comp loops i f)^$ $@ _ $@ fmap_zero_morphism _).
-  rapply (fmap2 loops); assumption.
+  refine (fmap2 loops _); assumption.
 Defined.
 
 Definition iscomplex_iterated_loops {F X Y : pType}
@@ -387,7 +387,7 @@ Proof.
     (isexact_purely_fiberseq (fiberseq_loops (fiberseq_isexact_purely i f)))).
   transitivity (fmap loops (pfib f) o* fmap loops (cxfib cx_isexact)).
   - refine (_ @* fmap_comp loops _ _).
-    rapply (fmap2 loops).
+    refine (fmap2 loops _).
     symmetry; apply pfib_cxfib.
   - refine (_ @* pmap_compose_assoc _ _ _).
     refine (pmap_prewhisker (fmap loops (cxfib cx_isexact)) _).

theories/Homotopy/HSpace/Core.v

@@ -151,8 +151,8 @@ Proof.
     exact (fmap loops (pmap_hspace_left_op a o* (pequiv_hspace_left_op pt)^-1*)).
   - lazy beta.
     transitivity (fmap (b:=A) loops pmap_idmap).
-    2: rapply (fmap_id loops).
-    rapply (fmap2 loops).
+    2: exact (fmap_id loops _).
+    refine (fmap2 loops _).
     nrapply peisretr.
 Defined.
 

theories/Homotopy/HomotopyGroup.v

@@ -122,8 +122,8 @@ Proof.
   apply Build_Is0Functor.
   intros X Y f.
   snrapply Build_GroupHomomorphism.
-  { rapply (fmap (Tr 0)).
-    rapply (fmap loops).
+  { refine (fmap (Tr 0) _).
+    refine (fmap loops _).
     assumption. }
   (** Note: we don't have to be careful about which paths we choose here since we are trying to inhabit a proposition. *)
   intros x y.
@@ -197,7 +197,7 @@ Definition pi_loops n X : Pi n.+1 X <~>* Pi n (loops X).
 Proof.
   destruct n.
   1: reflexivity.
-  rapply (emap (pTr 0 o loops)).
+  refine (emap (pTr 0 o loops) _).
   apply unfold_iterated_loops'.
 Defined.
 
@@ -289,7 +289,7 @@ Global Instance isequiv_pi_connmap `{Univalence} (n : nat) {X Y : pType} (f : X
   : IsEquiv (fmap (pPi n) f).
 Proof.
   (* For [n = 0] and [n] a successor, [fmap (pPi n) f] is definitionally equal to the map in the previous result as a map of types. *)
-  destruct n; rapply isequiv_pi_connmap'.
+  destruct n; exact (isequiv_pi_connmap' _ _).
 Defined.
 
 Definition pequiv_pi_connmap `{Univalence} (n : nat) {X Y : pType} (f : X ->* Y)
@@ -340,10 +340,10 @@ Proposition isembedding_pi_psect {n : nat} {X Y : pType}
   : IsEmbedding (fmap (pPi n) s).
 Proof.
   apply isembedding_isinj_hset.
-  rapply (isinj_section (r:=fmap (pPi n) r)).
+  refine (isinj_section (r:=fmap (pPi n) r) _).
   intro x.
-  lhs_V rapply (fmap_comp (pPi n) s r x).
-  lhs rapply (fmap2 (pPi n) k x).
+  lhs_V refine (fmap_comp (pPi n) s r x).
+  lhs refine (fmap2 (pPi n) k x).
   exact (fmap_id (pPi n) X x).
 Defined.
 

theories/Homotopy/Hopf.v

@@ -42,7 +42,7 @@ Proof.
       snrapply equiv_functor_sigma_id.
       intros x.
       exact (Build_Equiv _ _ (.* x) _). }
-    1,2: rapply (equiv_contr_sigma (Unit_ind (pointed_type X))).
+    1,2: exact (equiv_contr_sigma (Unit_ind (pointed_type X))).
     1,2: reflexivity. }
   reflexivity.
 Defined.
@@ -183,9 +183,9 @@ Definition pequiv_ptr_psusp_loops `{Univalence} (X : pType) (n : nat) `{IsConnec
   : pTr n.+2 (psusp (loops X)) <~>* pTr n.+2 X.
 Proof.
   snrapply Build_pEquiv.
-  1: rapply (fmap (pTr _) (loop_susp_counit _)).
+  1: exact (fmap (pTr _) (loop_susp_counit _)).
   nrapply O_inverts_conn_map.
   nrapply (isconnmap_pred_add n.-2).
   rewrite 2 trunc_index_add_succ.
-  rapply (conn_map_loop_susp_counit X).
+  exact (conn_map_loop_susp_counit X).
 Defined.

theories/Homotopy/IdentitySystems.v

@@ -76,7 +76,7 @@ Definition contr_sigma_equiv_path {A : Type} {a0 : A}
   : Contr (sig R).
 Proof.
   rapply contr_equiv'.
-  1: exact (equiv_functor_sigma_id f).
+  2: exact (equiv_functor_sigma_id f).
   apply contr_basedpaths.
 Defined.
 

theories/Homotopy/InjectiveTypes/TypeFamKanExt.v

@@ -31,14 +31,14 @@ Section UniverseStructure.
     (P : X -> Type@{w}) (j : X -> Y) (isem : IsEmbedding@{u v uv} j) (x : X)
     : Equiv@{uvw w} (LeftKanFam@{} P j (j x)) (P x).
   Proof.
-    rapply (@equiv_contr_sigma (hfiber j (j x)) _ _).
+    exact (@equiv_contr_sigma (hfiber j (j x)) _ _).
   Defined.
 
   Definition isext_equiv_rightkanfam@{} `{Funext} {X : Type@{u}} {Y : Type@{v}}
     (P : X -> Type@{w}) (j : X -> Y) (isem : IsEmbedding@{u v uv} j) (x : X)
     : Equiv@{uvw w} (RightKanFam@{} P j (j x)) (P x).
   Proof.
-    rapply (@equiv_contr_forall _ (hfiber j (j x)) _ _).
+    exact (@equiv_contr_forall _ (hfiber j (j x)) _ _).
   Defined.
 
   Definition isext_leftkanfam@{suvw | uvw < suvw} `{Univalence} {X : Type@{u}} {Y : Type@{v}}