grind +revert

Author: kim-em

Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean

@@ -540,7 +540,7 @@ lemma liftCochain_descCochain :
 lemma liftCochain_v_descCochain_v (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + n' = p₃)
     (q : ℤ) (hq : p₁ + m = q) :
     (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (descCochain φ α' β' h').v p₂ p₃ h₂₃ =
-      α.v p₁ q hq ≫ α'.v q p₃ (by cutsat) + β.v p₁ p₂ h₁₂ ≫ β'.v p₂ p₃ h₂₃ := by
+      α.v p₁ q hq ≫ α'.v q p₃ (by grind +revert) + β.v p₁ p₂ h₁₂ ≫ β'.v p₂ p₃ h₂₃ := by
   have eq := Cochain.congr_v (liftCochain_descCochain φ α β α' β' h h' p hp) p₁ p₃ (by cutsat)
   simpa only [Cochain.comp_v _ _ hp p₁ p₂ p₃ h₁₂ h₂₃, Cochain.add_v,
     Cochain.comp_v _ _ _ _ _ _ hq (show q + m' = p₃ by cutsat)] using eq

Mathlib/Algebra/Ring/GeomSum.lean

@@ -65,7 +65,7 @@ lemma op_geom_sum₂ (x y : R) (n : ℕ) : ∑ i ∈ range n, op y ^ (n - 1 - i)
     ∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i) := by
   rw [← sum_range_reflect]
   refine sum_congr rfl fun j j_in => ?_
-  grind
+  grind +revert
 
 lemma geom_sum₂_with_one (x : R) (n : ℕ) :
     ∑ i ∈ range n, x ^ i * 1 ^ (n - 1 - i) = ∑ i ∈ range n, x ^ i :=