[Merged by Bors] - feat: tactic congr! and improvement to convert

Mathlib.lean

@@ -1124,6 +1124,7 @@ import Mathlib.Tactic.Clear!
 import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Coe
+import Mathlib.Tactic.Congr!
 import Mathlib.Tactic.Constructor
 import Mathlib.Tactic.Continuity
 import Mathlib.Tactic.Continuity.Init

Mathlib/Algebra/Associated.lean

@@ -86,7 +86,7 @@ theorem comap_prime (hinv : ∀ a, g (f a : β) = a) (hp : Prime (f p)) : Prime
               simp).imp
           _ _ <;>
       · intro h
-        convert ← map_dvd g h; funext c; rw [hinv, hinv]⟩
+        convert ← map_dvd g h using 2; rw [hinv, hinv]⟩
 #align comap_prime comap_prime
 
 theorem MulEquiv.prime_iff (e : α ≃* β) : Prime p ↔ Prime (e p) :=

Mathlib/Algebra/BigOperators/Basic.lean

@@ -402,7 +402,6 @@ theorem _root_.Equiv.Perm.prod_comp (σ : Equiv.Perm α) (s : Finset α) (f : α
 theorem _root_.Equiv.Perm.prod_comp' (σ : Equiv.Perm α) (s : Finset α) (f : α → α → β)
     (hs : { a | σ a ≠ a } ⊆ s) : (∏ x in s, f (σ x) x) = ∏ x in s, f x (σ.symm x) := by
   convert σ.prod_comp s (fun x => f x (σ.symm x)) hs
-  ext
   rw [Equiv.symm_apply_apply]
 #align equiv.perm.prod_comp' Equiv.Perm.prod_comp'
 #align equiv.perm.sum_comp' Equiv.Perm.sum_comp'

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -44,8 +44,8 @@ theorem prod_Ico_add' [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [Locall
 @[to_additive]
 theorem prod_Ico_add [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α]
     (f : α → β) (a b c : α) : (∏ x in Ico a b, f (c + x)) = ∏ x in Ico (a + c) (b + c), f x := by
-  convert prod_Ico_add' f a b c
-  simp_rw [add_comm]
+  convert prod_Ico_add' f a b c using 2
+  rw [add_comm]
 #align finset.prod_Ico_add Finset.prod_Ico_add
 #align finset.sum_Ico_add Finset.sum_Ico_add
 

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -759,7 +759,6 @@ theorem pow_right_injective {x : ℤ} (h : 1 < x.natAbs) :
   suffices Function.Injective (natAbs ∘ ((· ^ ·) x : ℕ → ℤ)) by
     exact Function.Injective.of_comp this
   convert Nat.pow_right_injective h
-  ext n
   rw [Function.comp_apply, natAbs_pow]
 #align int.pow_right_injective Int.pow_right_injective
 

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

@@ -167,9 +167,6 @@ theorem isUnit_ring_inverse {a : M₀} : IsUnit (Ring.inverse a) ↔ IsUnit a :=
   ⟨fun h => by
     cases subsingleton_or_nontrivial M₀
     · convert h
-      -- Porting note:
-      -- This is needed due to a regression in `convert` noted in https://github.com/leanprover-community/mathlib4/issues/739
-      exact Subsingleton.elim _ _
     · contrapose h
       rw [Ring.inverse_non_unit _ h]
       exact not_isUnit_zero

Mathlib/Algebra/IndicatorFunction.lean

@@ -252,7 +252,7 @@ theorem mulIndicator_inter_mulSupport (s : Set α) (f : α → M) :
 theorem comp_mulIndicator (h : M → β) (f : α → M) {s : Set α} {x : α} [DecidablePred (· ∈ s)] :
     h (s.mulIndicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x := by
   letI := Classical.decPred (· ∈ s)
-  convert s.apply_piecewise f (const α 1) (fun _ => h) (x := x)
+  convert s.apply_piecewise f (const α 1) (fun _ => h) (x := x) using 2
 #align set.comp_mul_indicator Set.comp_mulIndicator
 #align set.comp_indicator Set.comp_indicator
 

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -1857,17 +1857,13 @@ def mapEdgeSet : G.edgeSet ≃ G'.edgeSet
   left_inv := by
     rintro ⟨e, h⟩
     simp [Hom.mapEdgeSet, Sym2.map_map, RelEmbedding.toRelHom]
-    apply congr_fun
-    convert Sym2.map_id (α := V)
-    apply congr_arg -- porting note: `convert` tactic did not do enough `congr`
-    exact funext fun _ => RelIso.symm_apply_apply _ _
+    convert congr_fun Sym2.map_id e
+    exact RelIso.symm_apply_apply _ _
   right_inv := by
     rintro ⟨e, h⟩
     simp [Hom.mapEdgeSet, Sym2.map_map, RelEmbedding.toRelHom]
-    apply congr_fun
-    convert Sym2.map_id (α := W)
-    apply congr_arg -- porting note: `convert` tactic did not do enough `congr`
-    exact funext fun _ => RelIso.apply_symm_apply _ _
+    convert congr_fun Sym2.map_id e
+    exact RelIso.apply_symm_apply _ _
 #align simple_graph.iso.map_edge_set SimpleGraph.Iso.mapEdgeSet
 
 /-- A graph isomorphism induces an equivalence of neighbor sets. -/

Mathlib/Combinatorics/SimpleGraph/Coloring.lean

@@ -118,8 +118,6 @@ theorem Coloring.card_colorClasses_le [Fintype α] [Fintype C.colorClasses] :
   -- porting note: brute force instance declaration `[Fintype (Setoid.classes (Setoid.ker C))]`
   haveI : Fintype (Setoid.classes (Setoid.ker C)) := by assumption
   convert Setoid.card_classes_ker_le C
-  -- porting note: convert would have handled this already in Lean 3:
-  apply Subsingleton.elim
 #align simple_graph.coloring.card_color_classes_le SimpleGraph.Coloring.card_colorClasses_le
 
 theorem Coloring.not_adj_of_mem_colorClass {c : α} {v w : V} (hv : v ∈ C.colorClass c)

Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

@@ -2242,10 +2242,8 @@ theorem coe_finsetWalkLength_eq (n : ℕ) (u v : V) :
     ext p
     simp only [mem_neighborSet, Finset.coe_map, Embedding.coeFn_mk, Set.unionᵢ_coe_set,
       Set.mem_unionᵢ, Set.mem_image, Finset.mem_coe, Set.mem_setOf_eq]
-    -- porting note: using `apply iff_of_eq` to help `congr`
-    apply iff_of_eq; congr with w
-    apply iff_of_eq; congr with h
-    apply iff_of_eq; congr with q
+    congr!
+    rename_i w _ q
     have := Set.ext_iff.mp (ih w v) q
     simp only [Finset.mem_coe, Set.mem_setOf_eq] at this
     rw [← this]

Mathlib/Combinatorics/Young/YoungDiagram.lean

@@ -356,7 +356,7 @@ theorem mk_mem_col_iff {μ : YoungDiagram} {i j : ℕ} : (i, j) ∈ μ.col j ↔
 #align young_diagram.mk_mem_col_iff YoungDiagram.mk_mem_col_iff
 
 protected theorem exists_not_mem_col (μ : YoungDiagram) (j : ℕ) : ∃ i, (i, j) ∉ μ.cells := by
-  convert μ.transpose.exists_not_mem_row j
+  convert μ.transpose.exists_not_mem_row j using 1
   simp
 #align young_diagram.exists_not_mem_col YoungDiagram.exists_not_mem_col
 

Mathlib/Data/Dfinsupp/Basic.lean

@@ -1479,9 +1479,9 @@ theorem sigmaCurry_apply [∀ i j, Zero (δ i j)] (f : Π₀ i : Σi, _, δ i.1
     case h₁ =>
       rw [@mem_image _ _ (fun a b ↦ Classical.propDecidable (a = b))]
       refine' ⟨⟨i, j⟩, _, rfl⟩
-      convert (mem_support_toFun f _).2 h <;> apply Subsingleton.elim
+      convert (mem_support_toFun f _).2 h
     · rw [mem_preimage]
-      convert (mem_support_toFun f _).2 h <;> apply Subsingleton.elim
+      convert (mem_support_toFun f _).2 h
 #align dfinsupp.sigma_curry_apply Dfinsupp.sigmaCurry_apply
 
 @[simp]

Mathlib/Data/Fin/Tuple/Basic.lean

@@ -164,9 +164,7 @@ theorem consCases_cons {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀
 @[elab_as_elim]
 def consInduction {α : Type _} {P : ∀ {n : ℕ}, (Fin n → α) → Sort v} (h0 : P Fin.elim0)
     (h : ∀ {n} (x₀) (x : Fin n → α), P x → P (Fin.cons x₀ x)) : ∀ {n : ℕ} (x : Fin n → α), P x
-  | 0, x => by
-    convert h0
-    simp
+  | 0, x => by convert h0
   | n + 1, x => consCases (fun x₀ x ↦ h _ _ <| consInduction h0 h _) x
 #align fin.cons_induction Fin.consInductionₓ -- Porting note: universes
 

Mathlib/Data/Finite/Basic.lean

@@ -140,7 +140,7 @@ instance Function.Embedding.finite {α β : Sort _} [Finite β] : Finite (α ↪
   · -- Porting note: infer_instance fails because it applies `Finite.of_fintype` and produces a
     -- "stuck at solving universe constraint" error.
     apply Finite.of_subsingleton
-   
+
   · refine' h.elim fun f => _
     haveI : Finite α := Finite.of_injective _ f.injective
     exact Finite.of_injective _ FunLike.coe_injective

Mathlib/Data/Finset/Basic.lean

@@ -2940,11 +2940,10 @@ theorem nonempty_range_succ : (range <| n + 1).Nonempty :=
 #align finset.nonempty_range_succ Finset.nonempty_range_succ
 
 @[simp]
-theorem range_filter_eq {n m : ℕ} : (range n).filter (· = m) = if m < n then {m} else ∅ :=
-  by
-  convert filter_eq (range n) m
+theorem range_filter_eq {n m : ℕ} : (range n).filter (· = m) = if m < n then {m} else ∅ := by
+  convert filter_eq (range n) m using 2
   · ext
-    simp_rw [@eq_comm _ m]
+    rw [eq_comm]
   · simp
 #align finset.range_filter_eq Finset.range_filter_eq
 

Mathlib/Data/Finset/Lattice.lean

@@ -1451,7 +1451,6 @@ theorem max_erase_ne_self {s : Finset α} : (s.erase x).max ≠ x := by
 theorem min_erase_ne_self {s : Finset α} : (s.erase x).min ≠ x := by
   -- Porting note: old proof `convert @max_erase_ne_self αᵒᵈ _ _ _`
   convert @max_erase_ne_self αᵒᵈ _ (toDual x) (s.map toDual.toEmbedding)
-  · funext _ _; simp only [eq_iff_true_of_subsingleton]
   · ext; simp only [mem_map_equiv]; exact Iff.rfl
 #align finset.min_erase_ne_self Finset.min_erase_ne_self
 

Mathlib/Data/Finset/PiInduction.lean

@@ -47,7 +47,7 @@ theorem induction_on_pi_of_choice (r : ∀ i, α i → Finset (α i) → Prop)
   cases nonempty_fintype ι
   induction' hs : univ.sigma f using Finset.strongInductionOn with s ihs generalizing f; subst s
   cases' eq_empty_or_nonempty (univ.sigma f) with he hne
-  · convert h0
+  · convert h0 using 1
     simpa [funext_iff] using he
   · rcases sigma_nonempty.1 hne with ⟨i, -, hi⟩
     rcases H_ex i (f i) hi with ⟨x, x_mem, hr⟩
@@ -118,4 +118,3 @@ theorem induction_on_pi_min [∀ i, LinearOrder (α i)] {p : (∀ i, Finset (α
 #align finset.induction_on_pi_min Finset.induction_on_pi_min
 
 end Finset
-

Mathlib/Data/Fintype/Basic.lean

@@ -1048,9 +1048,7 @@ noncomputable def finsetEquivSet [Fintype α] : Finset α ≃ Set α
     where
   toFun := (↑)
   invFun := by classical exact fun s => s.toFinset
-  left_inv s := by
-    { classical convert Finset.toFinset_coe s
-      simp }
+  left_inv s := by convert Finset.toFinset_coe s
   right_inv s := by classical exact s.coe_toFinset
 #align fintype.finset_equiv_set Fintype.finsetEquivSet
 

Mathlib/Data/Fintype/Option.lean

@@ -98,12 +98,11 @@ theorem induction_empty_option {P : ∀ (α : Type u) [Fintype α], Prop}
     (h_empty : P PEmpty) (h_option : ∀ (α) [Fintype α], P α → P (Option α)) (α : Type u)
     [h_fintype : Fintype α] : P α := by
   obtain ⟨p⟩ :=
-    let f_empty := (fun i => by convert h_empty; simp)
+    let f_empty := fun i => by convert h_empty
     let h_option : ∀ {α : Type u} [Fintype α] [DecidableEq α],
           (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)  := by
       rintro α hα - Pα hα'
       convert h_option α (Pα _)
-      simp
     @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
       f_empty h_option α _ (Classical.decEq α)
   · exact p _

Mathlib/Data/Int/ConditionallyCompleteOrder.lean

@@ -68,7 +68,6 @@ theorem csupₛ_eq_greatest_of_bdd {s : Set ℤ} [DecidablePred (· ∈ s)] (b :
   have : s.Nonempty ∧ BddAbove s := ⟨Hinh, b, Hb⟩
   simp only [supₛ, this, and_self, dite_true]
   convert (coe_greatestOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddAbove s)) Hinh).symm
-  simp
 #align int.cSup_eq_greatest_of_bdd Int.csupₛ_eq_greatest_of_bdd
 
 @[simp]
@@ -86,7 +85,6 @@ theorem cinfₛ_eq_least_of_bdd {s : Set ℤ} [DecidablePred (· ∈ s)] (b : 
   have : s.Nonempty ∧ BddBelow s := ⟨Hinh, b, Hb⟩
   simp only [infₛ, this, and_self, dite_true]
   convert (coe_leastOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddBelow s)) Hinh).symm
-  simp
 #align int.cInf_eq_least_of_bdd Int.cinfₛ_eq_least_of_bdd
 
 @[simp]

Mathlib/Data/Int/Parity.lean

@@ -74,7 +74,6 @@ theorem even_or_odd (n : ℤ) : Even n ∨ Odd n :=
 theorem even_or_odd' (n : ℤ) : ∃ k, n = 2 * k ∨ n = 2 * k + 1 := by
   rw [exists_or]
   convert even_or_odd n
-  funext i
   rw [two_mul]
 #align int.even_or_odd' Int.even_or_odd'
 

Mathlib/Data/List/Sublists.lean

@@ -397,7 +397,7 @@ alias nodup_sublists' ↔ nodup.of_sublists' nodup.sublists'
 
 theorem nodup_sublistsLen (n : ℕ) {l : List α} (h : Nodup l) : (sublistsLen n l).Nodup := by
   have : Pairwise (. ≠ .) l.sublists' := Pairwise.imp
-    (fun h => Lex.to_ne (by convert h; funext _ _; simp[swap, eq_comm])) h.sublists'
+    (fun h => Lex.to_ne (by convert h using 3; simp [swap, eq_comm])) h.sublists'
   exact this.sublist (sublistsLen_sublist_sublists' _ _)
 
 #align list.nodup_sublists_len List.nodup_sublistsLen

Mathlib/Data/ZMod/Defs.lean

@@ -111,7 +111,7 @@ instance infinite : Infinite (ZMod 0) :=
 theorem card (n : ℕ) [Fintype (ZMod n)] : Fintype.card (ZMod n) = n := by
   cases n with
   | zero => exact (not_finite (ZMod 0)).elim
-  | succ n => convert Fintype.card_fin (n + 1); apply Subsingleton.elim
+  | succ n => convert Fintype.card_fin (n + 1)
 #align zmod.card ZMod.card
 
 /- We define each field by cases, to ensure that the eta-expanded `ZMod.commRing` is defeq to the

Mathlib/GroupTheory/NoncommPiCoprod.lean

@@ -124,7 +124,6 @@ def noncommPiCoprod : (∀ i : ι, N i) →* M
       have := @Finset.noncommProd_mul_distrib _ _ _ Finset.univ (fun i => ϕ i (f i))
         (fun i => ϕ i (g i)) ?_ ?_ ?_
       · convert this
-        ext
         exact map_mul _ _ _
       · exact fun i _ j _ hij => hcomm hij _ _
       · exact fun i _ j _ hij => hcomm hij _ _

Mathlib/LinearAlgebra/Basis.lean

@@ -825,7 +825,6 @@ theorem eq_bot_of_rank_eq_zero [NoZeroDivisors R] (b : Basis ι R M) (N : Submod
   simp only [Function.const_apply, Fin.default_eq_zero, Submodule.coe_mk, Finset.univ_unique,
     Function.comp_const, Finset.sum_singleton] at sum_eq
   convert (b.smul_eq_zero.mp sum_eq).resolve_right x_ne
-  rwa [Nat.lt_one_iff] at hi
 #align eq_bot_of_rank_eq_zero Basis.eq_bot_of_rank_eq_zero
 
 end NoZeroSMulDivisors

Mathlib/MeasureTheory/MeasurableSpace.lean

@@ -271,8 +271,8 @@ for functions between empty types. -/
 theorem measurable_const' {f : β → α} (hf : ∀ x y, f x = f y) : Measurable f := by
   nontriviality β
   inhabit β
-  convert @measurable_const α β ‹_› ‹_› (f default)
-  exact funext fun x => hf x default
+  convert @measurable_const α β ‹_› ‹_› (f default) using 2
+  apply hf
 #align measurable_const' measurable_const'
 
 theorem measurable_of_countable [Countable α] [MeasurableSingletonClass α] (f : α → β) :

Mathlib/Order/CompleteLattice.lean

@@ -664,7 +664,7 @@ theorem Equiv.supᵢ_comp {g : ι' → α} (e : ι ≃ ι') : (⨆ x, g (e x)) =
 protected theorem Function.Surjective.supᵢ_congr {g : ι' → α} (h : ι → ι') (h1 : Surjective h)
     (h2 : ∀ x, g (h x) = f x) : (⨆ x, f x) = ⨆ y, g y := by
   convert h1.supᵢ_comp g
-  exact (funext h2).symm
+  exact (h2 _).symm
 #align function.surjective.supr_congr Function.Surjective.supᵢ_congr
 
 protected theorem Equiv.supᵢ_congr {g : ι' → α} (e : ι ≃ ι') (h : ∀ x, g (e x) = f x) :

Mathlib/Order/Filter/Bases.lean

@@ -964,7 +964,6 @@ theorem map_sigma_mk_comap {π : α → Type _} {π' : β → Type _} {f : α 
     map (Sigma.mk a) (comap (g a) l) = comap (Sigma.map f g) (map (Sigma.mk (f a)) l) := by
   refine' (((basis_sets _).comap _).map _).eq_of_same_basis _
   convert ((basis_sets l).map (Sigma.mk (f a))).comap (Sigma.map f g)
-  ext1 s
   apply image_sigmaMk_preimage_sigmaMap hf
 #align filter.map_sigma_mk_comap Filter.map_sigma_mk_comap
 

Mathlib/Order/PartialSups.lean

@@ -110,7 +110,7 @@ theorem partialSups_mono : Monotone (partialSups : (ℕ → α) → ℕ →o α)
 -/
 def partialSups.gi : GaloisInsertion (partialSups : (ℕ → α) → ℕ →o α) (↑) where
   choice f h :=
-    ⟨f, by convert (partialSups f).monotone; exact (le_partialSups f).antisymm h⟩
+    ⟨f, by convert (partialSups f).monotone using 1; exact (le_partialSups f).antisymm h⟩
   gc f g := by
     refine' ⟨(le_partialSups f).trans, fun h => _⟩
     convert partialSups_mono h

Mathlib/SetTheory/Ordinal/NaturalOps.lean

@@ -287,7 +287,7 @@ theorem nadd_zero : a ♯ 0 = a := by
   induction' a using Ordinal.induction with a IH
   rw [nadd_def, blsub_zero, max_zero_right]
   convert blsub_id a
-  ext (b hb)
+  rename_i hb
   exact IH _ hb
 #align ordinal.nadd_zero Ordinal.nadd_zero