fix(*): fix things from change tendsto_congr -> tendsto.congr'

src/analysis/normed_space/deriv.lean

@@ -49,7 +49,7 @@ theorem has_fderiv_at_filter_equiv_aux {f : E → F} {f' : E → F} {x : E} {L :
   tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - f' (x' - x)∥) L (nhds 0) :=
 begin
   have f'0 : f' 0 = 0 := (bf'.to_linear_map _).map_zero,
-  rw [tendsto_iff_norm_tendsto_zero], refine tendsto_congr (λ x', _),
+  rw [tendsto_iff_norm_tendsto_zero], refine tendsto.congr'r (λ x', _),
   have : ∥x' + -x∥⁻¹ ≥ 0, from inv_nonneg.mpr (norm_nonneg _),
   simp [norm_smul, real.norm_eq_abs, abs_of_nonneg this]
 end
@@ -68,7 +68,7 @@ and.congr_right_iff.mpr $
   begin
     rw has_fderiv_at_filter_equiv_aux bf',
     rw [←is_littleo_norm_left, ←is_littleo_norm_right, is_littleo_iff_tendsto h],
-    exact tendsto_congr (λ x', mul_comm _ _)
+    exact tendsto.congr'r (λ x', mul_comm _ _)
   end
 
 theorem has_fderiv_at_within_iff_tendsto {f : E → F} {f' : E → F} {x : E} {s : set E} :

src/analysis/specific_limits.lean

@@ -59,7 +59,7 @@ by_cases
     have tendsto (λn, (r⁻¹ ^ n)⁻¹) at_top (nhds 0),
       from (tendsto_pow_at_top_at_top_of_gt_1 $ one_lt_inv (lt_of_le_of_ne h₁ this.symm) h₂).comp
         tendsto_inverse_at_top_nhds_0,
-    tendsto_cong this $ univ_mem_sets' $ by simp *)
+    tendsto.congr' (univ_mem_sets' $ by simp *) this)
 
 lemma tendsto_pow_at_top_at_top_of_gt_1_nat {k : ℕ} (h : 1 < k) :
   tendsto (λn:ℕ, k ^ n) at_top at_top :=

src/data/padics/hensel.lean

@@ -335,9 +335,10 @@ squeeze_zero (λ _, norm_nonneg _) newton_seq_norm_le bound'_sq
 
 private lemma newton_seq_dist_tendsto :
   tendsto (λ n, ∥newton_cau_seq n - a∥) at_top (nhds (∥F.eval a∥ / ∥F.derivative.eval a∥)) :=
-tendsto_cong (tendsto_const_nhds) $
-  suffices ∃ k, ∀ n ≥ k,  ∥F.eval a∥ / ∥F.derivative.eval a∥ = ∥newton_cau_seq n - a∥, by simpa,
-  ⟨1, λ _ hx, (newton_seq_dist_to_a _ hx).symm⟩
+tendsto.congr'
+  (suffices ∃ k, ∀ n ≥ k,  ∥F.eval a∥ / ∥F.derivative.eval a∥ = ∥newton_cau_seq n - a∥, by simpa,
+    ⟨1, λ _ hx, (newton_seq_dist_to_a _ hx).symm⟩)
+  (tendsto_const_nhds)
 
 private lemma newton_seq_dist_tendsto' :
   tendsto (λ n, ∥newton_cau_seq n - a∥) at_top (nhds ∥soln - a∥) :=

src/order/filter/basic.lean

@@ -1111,13 +1111,13 @@ lemma tendsto.congr' {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter 
   (hl : {x | f₁ x = f₂ x} ∈ l₁.sets) (h : tendsto f₁ l₁ l₂) : tendsto f₂ l₁ l₂ :=
 by rwa [tendsto, ←map_cong hl]
 
-theorem tendsto_congr {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β}
+theorem tendsto.congr'r {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β}
   (h : ∀ x, f₁ x = f₂ x) : tendsto f₁ l₁ l₂ ↔ tendsto f₂ l₁ l₂ :=
 iff_of_eq (by congr'; exact funext h)
 
 theorem tendsto.congr {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β}
   (h : ∀ x, f₁ x = f₂ x) : tendsto f₁ l₁ l₂ → tendsto f₂ l₁ l₂ :=
-(tendsto_congr h).1
+(tendsto.congr'r h).1
 
 lemma tendsto_id' {x y : filter α} : x ≤ y → tendsto id x y :=
 by simp only [tendsto, map_id, forall_true_iff] {contextual := tt}

src/topology/algebra/infinite_sum.lean

@@ -76,8 +76,9 @@ lemma has_sum_sum {f : γ → β → α} {s : finset γ} (hf : ∀i∈s, has_sum
 has_sum_spec $ is_sum_sum $ assume i hi, is_sum_tsum $ hf i hi
 
 lemma is_sum_sum_of_ne_finset_zero (hf : ∀b∉s, f b = 0) : is_sum f (s.sum f) :=
-tendsto_infi' s $ tendsto_cong tendsto_const_nhds $
-  assume t (ht : s ⊆ t), show s.sum f = t.sum f, from sum_subset ht $ assume x _, hf _
+tendsto_infi' s $ tendsto.congr'
+  (assume t (ht : s ⊆ t), show s.sum f = t.sum f, from sum_subset ht $ assume x _, hf _)
+  tendsto_const_nhds
 
 lemma has_sum_sum_of_ne_finset_zero (hf : ∀b∉s, f b = 0) : has_sum f :=
 has_sum_spec $ is_sum_sum_of_ne_finset_zero hf

src/topology/instances/ennreal.lean

@@ -273,8 +273,8 @@ begin
   { simp [@nhds_coe a, tendsto_map'_iff, (∘), tendsto_coe, coe_sub.symm],
     exact nnreal.tendsto_sub tendsto_const_nhds tendsto_id },
   simp,
-  exact (tendsto_cong tendsto_const_nhds $ mem_sets_of_superset (lt_mem_nhds $ @coe_lt_top r) $
-    by simp [le_of_lt] {contextual := tt})
+  exact (tendsto.congr' (mem_sets_of_superset (lt_mem_nhds $ @coe_lt_top r) $
+    by simp [le_of_lt] {contextual := tt})) tendsto_const_nhds
 end
 
 lemma sub_supr {ι : Sort*} [hι : nonempty ι] {b : ι → ennreal} (hr : a < ⊤) :