chore(*): replace exact calc by calc (#10137)

This PR is the result of a sed script that replaces

* `exact calc` by `calc`
* `refine calc` by `calc`

src/analysis/inner_product_space/projection.lean

@@ -139,7 +139,7 @@ begin
     rw dist_eq_norm,
     apply nonneg_le_nonneg_of_sq_le_sq, { exact sqrt_nonneg _ },
     rw mul_self_sqrt,
-    exact calc
+    calc
       ∥wp - wq∥ * ∥wp - wq∥ = 2 * (∥a∥*∥a∥ + ∥b∥*∥b∥) -
         4 * ∥u - half • (wq+wp)∥ * ∥u - half • (wq+wp)∥ : by { rw ← this, simp }
       ... ≤ 2 * (∥a∥ * ∥a∥ + ∥b∥ * ∥b∥) - 4 * δ * δ : sub_le_sub_left eq₁ _
@@ -246,7 +246,7 @@ begin
   { apply le_cinfi, assume w,
     apply nonneg_le_nonneg_of_sq_le_sq (norm_nonneg _),
     have := h w w.2,
-    exact calc
+    calc
       ∥u - v∥ * ∥u - v∥ ≤ ∥u - v∥ * ∥u - v∥ - 2 * inner (u - v) ((w:F) - v) : by linarith
       ... ≤ ∥u - v∥^2 - 2 * inner (u - v) ((w:F) - v) + ∥(w:F) - v∥^2 :
         by { rw sq, refine le_add_of_nonneg_right _, exact sq_nonneg _ }

src/data/complex/exponential.lean

@@ -51,7 +51,7 @@ begin
   assume j hj,
   have hfij : f j ≤ f i := forall_ge_le_of_forall_le_succ f hnm hi.1 hj,
   rw [abs_of_nonpos (sub_nonpos.2 hfij), neg_sub, sub_lt_iff_lt_add'],
-  exact calc f i ≤ a - (nat.pred l) • ε : hi.2
+  calc f i ≤ a - (nat.pred l) • ε : hi.2
     ... = a - l • ε + ε :
       by conv {to_rhs, rw [← nat.succ_pred_eq_of_pos (nat.pos_of_ne_zero hl0), succ_nsmul',
         sub_add, add_sub_cancel] }
@@ -287,7 +287,7 @@ begin
   refine add_lt_add (lt_of_le_of_lt hsumlesum
     (by rw [← sum_mul, mul_comm]; exact (mul_lt_mul_left hPε0).mpr hsumltP)) _,
   rw sum_range_sub_sum_range (le_of_lt hNMK),
-  exact calc ∑ i in (range K).filter (λ k, max N M + 1 ≤ k),
+  calc ∑ i in (range K).filter (λ k, max N M + 1 ≤ k),
       abv (a i) * abv (∑ k in range (K - i), b k - ∑ k in range K, b k)
       ≤ ∑ i in (range K).filter (λ k, max N M + 1 ≤ k), abv (a i) * (2 * Q) :
     sum_le_sum (λ n hn, begin
@@ -1254,7 +1254,7 @@ begin
   show abs (∑ m in range j, x ^ m / m! - ∑ m in range n, x ^ m / m!)
     ≤ abs x ^ n * (n.succ * (n! * n)⁻¹),
   rw sum_range_sub_sum_range hj,
-  exact calc abs (∑ m in (range j).filter (λ k, n ≤ k), (x ^ m / m! : ℂ))
+  calc abs (∑ m in (range j).filter (λ k, n ≤ k), (x ^ m / m! : ℂ))
       = abs (∑ m in (range j).filter (λ k, n ≤ k), (x ^ n * (x ^ (m - n) / m!) : ℂ)) :
     begin
       refine congr_arg abs (sum_congr rfl (λ m hm, _)),

src/data/nat/log.lean

@@ -144,7 +144,7 @@ lemma log_le_log_of_left_ge {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : log b n
 begin
   cases n, { simp },
   rw ← pow_le_iff_le_log hc (zero_lt_succ n),
-  exact calc
+  calc
     c ^ log b n.succ ≤ b ^ log b n.succ : pow_le_pow_of_le_left
                                             (le_of_lt $ zero_lt_one.trans hc) hb _
                  ... ≤ n.succ           : pow_log_le_self (lt_of_lt_of_le hc hb)
@@ -257,7 +257,7 @@ lemma clog_le_clog_of_left_ge {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : clog b
 begin
   cases n, { simp },
   rw ← le_pow_iff_clog_le (lt_of_lt_of_le hc hb),
-  exact calc
+  calc
     n.succ ≤ c ^ clog c n.succ : le_pow_clog hc _
        ... ≤ b ^ clog c n.succ : pow_le_pow_of_le_left (le_of_lt $ zero_lt_one.trans hc) hb _
 end

src/group_theory/group_action/basic.lean

@@ -151,7 +151,7 @@ begin
   { exact λ h, ⟨⟨a, mem_orbit_self _⟩, λ ⟨b, ⟨x, hx⟩⟩, subtype.eq $ by simp [h x, hx.symm]⟩ },
   { assume h x,
     rcases h with ⟨⟨z, hz⟩, hz₁⟩,
-    exact calc x • a = z : subtype.mk.inj (hz₁ ⟨x • a, mem_orbit _ _⟩)
+    calc x • a = z : subtype.mk.inj (hz₁ ⟨x • a, mem_orbit _ _⟩)
       ... = a : (subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _⟩)).symm }
 end
 

src/order/filter/pointwise.lean

@@ -82,12 +82,12 @@ begin
   ext s, split,
   { rintros ⟨a, b, ⟨a₁, a₂, ha₁, ha₂, a₁a₂⟩, hb, ab⟩,
     refine ⟨a₁, a₂ * b, ha₁, mul_mem_mul ha₂ hb, _⟩, rw [← mul_assoc],
-    exact calc
+    calc
       a₁ * a₂ * b ⊆ a * b : mul_subset_mul a₁a₂ (subset.refl _)
       ...         ⊆ s     : ab },
   { rintros ⟨a, b, ha, ⟨b₁, b₂, hb₁, hb₂, b₁b₂⟩, ab⟩,
     refine ⟨a * b₁, b₂, mul_mem_mul ha hb₁, hb₂, _⟩, rw [mul_assoc],
-    exact calc
+    calc
       a * (b₁ * b₂) ⊆ a * b : mul_subset_mul (subset.refl _) b₁b₂
       ...           ⊆ s     : ab }
 end

src/set_theory/ordinal_notation.lean

@@ -734,7 +734,7 @@ begin
       simpa using (add_lt_add_iff_left (repr a0)).2 e0 },
     { refine lt_of_lt_of_le Rl (power_le_power_right omega_pos $
         mul_le_mul_left _ $ succ_le_succ.2 $ nat_cast_le.2 $ le_of_lt k.lt_succ_self) } },
-  refine calc
+  calc
         ω0 ^ k.succ * α' + R'
       = ω0 ^ succ k * α' + (ω0 ^ k * α' * m + R) : by rw [nat_cast_succ, RR, ← mul_assoc]
   ... = (ω0 ^ k * α' + R) * α' + (ω0 ^ k * α' + R) * m : _

src/topology/continuous_function/bounded.lean

@@ -339,7 +339,7 @@ begin
   /- If two functions have the same approximation, then they are within distance ε -/
   refine lt_of_le_of_lt ((dist_le $ le_of_lt ε₁0).2 (λ x, _)) εε₁,
   obtain ⟨x', x'tα, hx'⟩ : ∃x' ∈ tα, x ∈ U x' := mem_bUnion_iff.1 (htα (mem_univ x)),
-  refine calc dist (f x) (g x)
+  calc dist (f x) (g x)
       ≤ dist (f x) (f x') + dist (g x) (g x') + dist (f x') (g x') : dist_triangle4_right _ _ _ _
   ... ≤ ε₂ + ε₂ + ε₁/2 : le_of_lt (add_lt_add (add_lt_add _ _) _)
   ... = ε₁ : by rw [add_halves, add_halves],