chore: add missing #align statements (#1902)

This PR is the result of a slight variant on the following "algorithm"

* take all mathlib 3 names, remove `_` and make all uppercase letters into lowercase
* take all mathlib 4 names, remove `_` and make all uppercase letters into lowercase
* look for matches, and create pairs `(original_lean3_name, OriginalLean4Name)`
* for pairs that do not have an align statement:
  - use Lean 4 to lookup the file + position of the Lean 4 name
  - add an `#align` statement just before the next empty line
* manually fix some tiny mistakes (e.g., empty lines in proofs might cause the `#align` statement to have been inserted too early)

Mathlib/Algebra/BigOperators/Pi.lean

@@ -70,7 +70,7 @@ theorem prod_mk_prod {α β γ : Type _} [CommMonoid α] [CommMonoid β] (s : Fi
   haveI := Classical.decEq γ
   Finset.induction_on s rfl (by simp (config := { contextual := true }) [Prod.ext_iff])
 #align prod_mk_prod prod_mk_prod
-#align sum_mk_sum prod_mk_sum
+#align prod_mk_sum prod_mk_sum
 
 section Single
 

Mathlib/Algebra/BigOperators/Ring.lean

@@ -257,6 +257,7 @@ theorem prod_powerset_insert [DecidableEq α] [CommMonoid β] {s : Finset α} {x
     rw [← H₃₂]
     exact ne_insert_of_not_mem _ _ (not_mem_of_mem_powerset_of_not_mem h₁ h)
 #align finset.prod_powerset_insert Finset.prod_powerset_insert
+#align finset.sum_powerset_insert Finset.sum_powerset_insert
 
 /-- A product over `powerset s` is equal to the double product over sets of subsets of `s` with
 `card s = k`, for `k = 1, ..., card s`. -/
@@ -267,6 +268,7 @@ theorem prod_powerset [CommMonoid β] (s : Finset α) (f : Finset α → β) :
     (∏ t in powerset s, f t) = ∏ j in range (card s + 1), ∏ t in powersetLen j s, f t := by
   rw [powerset_card_disjUnionᵢ, prod_disjUnionᵢ]
 #align finset.prod_powerset Finset.prod_powerset
+#align finset.sum_powerset Finset.sum_powerset
 
 theorem sum_range_succ_mul_sum_range_succ [NonUnitalNonAssocSemiring β] (n k : ℕ) (f g : ℕ → β) :
     ((∑ i in range (n + 1), f i) * ∑ i in range (k + 1), g i) =

Mathlib/Algebra/CharZero/Lemmas.lean

@@ -34,6 +34,7 @@ variable {R : Type _} [AddMonoidWithOne R] [CharZero R]
 def castEmbedding : ℕ ↪ R :=
   ⟨Nat.cast, cast_injective⟩
 #align nat.cast_embedding Nat.castEmbedding
+#align nat.cast_embedding_apply Nat.castEmbedding_apply
 
 @[simp]
 theorem cast_pow_eq_one {R : Type _} [Semiring R] [CharZero R] (q : ℕ) (n : ℕ) (hn : n ≠ 0) :

Mathlib/Algebra/CovariantAndContravariant.lean

@@ -81,13 +81,15 @@ action of a Type on another one and a relation on the acted-upon Type.
 See the `CovariantClass` doc-string for its meaning. -/
 def Covariant : Prop :=
   ∀ (m) {n₁ n₂}, r n₁ n₂ → r (μ m n₁) (μ m n₂)
+#align covariant Covariant
 
 /-- `Contravariant` is useful to formulate succintly statements about the interactions between an
 action of a Type on another one and a relation on the acted-upon Type.
 
 See the `ContravariantClass` doc-string for its meaning. -/
 def Contravariant : Prop :=
   ∀ (m) {n₁ n₂}, r (μ m n₁) (μ m n₂) → r n₁ n₂
+#align contravariant Contravariant
 
 /-- Given an action `μ` of a Type `M` on a Type `N` and a relation `r` on `N`, informally, the
 `CovariantClass` says that "the action `μ` preserves the relation `r`."
@@ -104,6 +106,7 @@ class CovariantClass : Prop where
   /-- For all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the pair
   `(n₁, n₂)`, then, the relation `r` also holds for the pair `(μ m n₁, μ m n₂)` -/
   protected elim : Covariant M N μ r
+#align covariant_class CovariantClass
 
 /-- Given an action `μ` of a Type `M` on a Type `N` and a relation `r` on `N`, informally, the
 `ContravariantClass` says that "if the result of the action `μ` on a pair satisfies the
@@ -122,20 +125,24 @@ class ContravariantClass : Prop where
   pair `(μ m n₁, μ m n₂)` obtained from `(n₁, n₂)` by acting upon it by `m`, then, the relation
   `r` also holds for the pair `(n₁, n₂)`. -/
   protected elim : Contravariant M N μ r
+#align contravariant_class ContravariantClass
 
 theorem rel_iff_cov [CovariantClass M N μ r] [ContravariantClass M N μ r] (m : M) {a b : N} :
     r (μ m a) (μ m b) ↔ r a b :=
   ⟨ContravariantClass.elim _, CovariantClass.elim _⟩
+#align rel_iff_cov rel_iff_cov
 
 section flip
 
 variable {M N μ r}
 
 theorem Covariant.flip (h : Covariant M N μ r) : Covariant M N μ (flip r) :=
   fun a _ _ hbc ↦ h a hbc
+#align covariant.flip Covariant.flip
 
 theorem Contravariant.flip (h : Contravariant M N μ r) : Contravariant M N μ (flip r) :=
   fun a _ _ hbc ↦ h a hbc
+#align contravariant.flip Contravariant.flip
 
 end flip
 
@@ -145,6 +152,7 @@ variable {M N μ r} [CovariantClass M N μ r]
 
 theorem act_rel_act_of_rel (m : M) {a b : N} (ab : r a b) : r (μ m a) (μ m b) :=
   CovariantClass.elim _ ab
+#align act_rel_act_of_rel act_rel_act_of_rel
 
 @[to_additive]
 theorem Group.covariant_iff_contravariant [Group N] :
@@ -154,6 +162,8 @@ theorem Group.covariant_iff_contravariant [Group N] :
     exact h a⁻¹ bc
   · rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc
     exact h a⁻¹ bc
+#align group.covariant_iff_contravariant Group.covariant_iff_contravariant
+#align add_group.covariant_iff_contravariant AddGroup.covariant_iff_contravariant
 
 @[to_additive]
 instance (priority := 100) Group.covconv [Group N] [CovariantClass N N (· * ·) r] :
@@ -168,6 +178,8 @@ theorem Group.covariant_swap_iff_contravariant_swap [Group N] :
     exact h a⁻¹ bc
   · rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc
     exact h a⁻¹ bc
+#align group.covariant_swap_iff_contravariant_swap Group.covariant_swap_iff_contravariant_swap
+#align add_group.covariant_swap_iff_contravariant_swap AddGroup.covariant_swap_iff_contravariant_swap
 
 
 @[to_additive]
@@ -183,9 +195,11 @@ variable [IsTrans N r] (m n : M) {a b c d : N}
 --  Lemmas with 3 elements.
 theorem act_rel_of_rel_of_act_rel (ab : r a b) (rl : r (μ m b) c) : r (μ m a) c :=
   _root_.trans (act_rel_act_of_rel m ab) rl
+#align act_rel_of_rel_of_act_rel act_rel_of_rel_of_act_rel
 
 theorem rel_act_of_rel_of_rel_act (ab : r a b) (rr : r c (μ m a)) : r c (μ m b) :=
   _root_.trans rr (act_rel_act_of_rel _ ab)
+#align rel_act_of_rel_of_rel_act rel_act_of_rel_of_rel_act
 
 end Trans
 
@@ -199,6 +213,7 @@ variable {M N μ r} {mu : N → N → N} [IsTrans N r] [i : CovariantClass N N m
 
 theorem act_rel_act_of_rel_of_rel (ab : r a b) (cd : r c d) : r (mu a c) (mu b d) :=
   _root_.trans (@act_rel_act_of_rel _ _ (swap mu) r _ c _ _ ab) (act_rel_act_of_rel b cd)
+#align act_rel_act_of_rel_of_rel act_rel_act_of_rel_of_rel
 
 end MEqN
 
@@ -208,6 +223,7 @@ variable {M N μ r} [ContravariantClass M N μ r]
 
 theorem rel_of_act_rel_act (m : M) {a b : N} (ab : r (μ m a) (μ m b)) : r a b :=
   ContravariantClass.elim _ ab
+#align rel_of_act_rel_act rel_of_act_rel_act
 
 section Trans
 
@@ -217,10 +233,12 @@ variable [IsTrans N r] (m n : M) {a b c d : N}
 theorem act_rel_of_act_rel_of_rel_act_rel (ab : r (μ m a) b) (rl : r (μ m b) (μ m c)) :
     r (μ m a) c :=
   _root_.trans ab (rel_of_act_rel_act m rl)
+#align act_rel_of_act_rel_of_rel_act_rel act_rel_of_act_rel_of_rel_act_rel
 
 theorem rel_act_of_act_rel_act_of_rel_act (ab : r (μ m a) (μ m b)) (rr : r b (μ m c)) :
     r a (μ m c) :=
   _root_.trans (rel_of_act_rel_act m ab) rr
+#align rel_act_of_act_rel_act_of_rel_act rel_act_of_act_rel_act_of_rel_act
 
 end Trans
 
@@ -235,28 +253,33 @@ variable {f : N → α}
 /-- The partial application of a constant to a covariant operator is monotone. -/
 theorem Covariant.monotone_of_const [CovariantClass M N μ (· ≤ ·)] (m : M) : Monotone (μ m) :=
   fun _ _ ha ↦ CovariantClass.elim m ha
+#align covariant.monotone_of_const Covariant.monotone_of_const
 
 /-- A monotone function remains monotone when composed with the partial application
 of a covariant operator. E.g., `∀ (m : ℕ), Monotone f → Monotone (λ n, f (m + n))`. -/
 theorem Monotone.covariant_of_const [CovariantClass M N μ (· ≤ ·)] (hf : Monotone f) (m : M) :
     Monotone fun n ↦ f (μ m n) :=
   fun _ _ x ↦ hf (Covariant.monotone_of_const m x)
+#align monotone.covariant_of_const Monotone.covariant_of_const
 
 /-- Same as `Monotone.covariant_of_const`, but with the constant on the other side of
 the operator.  E.g., `∀ (m : ℕ), monotone f → monotone (λ n, f (n + m))`. -/
 theorem Monotone.covariant_of_const' {μ : N → N → N} [CovariantClass N N (swap μ) (· ≤ ·)]
     (hf : Monotone f) (m : N) : Monotone fun n ↦ f (μ n m) :=
   fun _ _ x ↦ hf (@Covariant.monotone_of_const _ _ (swap μ) _ _ m _ _ x)
+#align monotone.covariant_of_const' Monotone.covariant_of_const'
 
 /-- Dual of `Monotone.covariant_of_const` -/
 theorem Antitone.covariant_of_const [CovariantClass M N μ (· ≤ ·)] (hf : Antitone f) (m : M) :
     Antitone fun n ↦ f (μ m n) :=
   hf.comp_monotone <| Covariant.monotone_of_const m
+#align antitone.covariant_of_const Antitone.covariant_of_const
 
 /-- Dual of `Monotone.covariant_of_const'` -/
 theorem Antitone.covariant_of_const' {μ : N → N → N} [CovariantClass N N (swap μ) (· ≤ ·)]
     (hf : Antitone f) (m : N) : Antitone fun n ↦ f (μ n m) :=
   hf.comp_monotone <| @Covariant.monotone_of_const _ _ (swap μ) _ _ m
+#align antitone.covariant_of_const' Antitone.covariant_of_const'
 
 end Monotone
 
@@ -266,21 +289,25 @@ theorem covariant_le_of_covariant_lt [PartialOrder N] :
   rcases le_iff_eq_or_lt.mp bc with (rfl | bc)
   · exact rfl.le
   · exact (h _ bc).le
+#align covariant_le_of_covariant_lt covariant_le_of_covariant_lt
 
 theorem contravariant_lt_of_contravariant_le [PartialOrder N] :
     Contravariant M N μ (· ≤ ·) → Contravariant M N μ (· < ·) := by
   refine fun h a b c bc ↦ lt_iff_le_and_ne.mpr ⟨h a bc.le, ?_⟩
   rintro rfl; exact lt_irrefl _ bc
+#align contravariant_lt_of_contravariant_le contravariant_lt_of_contravariant_le
 
 theorem covariant_le_iff_contravariant_lt [LinearOrder N] :
     Covariant M N μ (· ≤ ·) ↔ Contravariant M N μ (· < ·) :=
   ⟨fun h _ _ _ bc ↦ not_le.mp fun k ↦ not_le.mpr bc (h _ k),
    fun h _ _ _ bc ↦ not_lt.mp fun k ↦ not_lt.mpr bc (h _ k)⟩
+#align covariant_le_iff_contravariant_lt covariant_le_iff_contravariant_lt
 
 theorem covariant_lt_iff_contravariant_le [LinearOrder N] :
     Covariant M N μ (· < ·) ↔ Contravariant M N μ (· ≤ ·) :=
   ⟨fun h _ _ _ bc ↦ not_lt.mp fun k ↦ not_lt.mpr bc (h _ k),
    fun h _ _ _ bc ↦ not_le.mp fun k ↦ not_le.mpr bc (h _ k)⟩
+#align covariant_lt_iff_contravariant_le covariant_lt_iff_contravariant_le
 
 -- Porting note: `covariant_flip_mul_iff` used to use the `IsSymmOp` typeclass from Lean 3 core.
 -- To avoid it, we prove the relevant lemma here.
@@ -291,10 +318,14 @@ lemma flip_mul [CommSemigroup N] : (flip (· * ·) : N → N → N) = (· * ·)
 @[to_additive]
 theorem covariant_flip_mul_iff [CommSemigroup N] :
     Covariant N N (flip (· * ·)) r ↔ Covariant N N (· * ·) r := by rw [flip_mul]
+#align covariant_flip_mul_iff covariant_flip_mul_iff
+#align covariant_flip_add_iff covariant_flip_add_iff
 
 @[to_additive]
 theorem contravariant_flip_mul_iff [CommSemigroup N] :
     Contravariant N N (flip (· * ·)) r ↔ Contravariant N N (· * ·) r := by rw [flip_mul]
+#align contravariant_flip_mul_iff contravariant_flip_mul_iff
+#align contravariant_flip_add_iff contravariant_flip_add_iff
 
 @[to_additive]
 instance contravariant_mul_lt_of_covariant_mul_le [Mul N] [LinearOrder N]

Mathlib/Algebra/Divisibility/Basic.lean

@@ -53,6 +53,7 @@ theorem Dvd.intro (c : α) (h : a * c = b) : a ∣ b :=
 #align dvd.intro Dvd.intro
 
 alias Dvd.intro ← dvd_of_mul_right_eq
+#align dvd_of_mul_right_eq dvd_of_mul_right_eq
 
 theorem exists_eq_mul_right_of_dvd (h : a ∣ b) : ∃ c, b = a * c :=
   h
@@ -140,6 +141,7 @@ theorem Dvd.intro_left (c : α) (h : c * a = b) : a ∣ b :=
 #align dvd.intro_left Dvd.intro_left
 
 alias Dvd.intro_left ← dvd_of_mul_left_eq
+#align dvd_of_mul_left_eq dvd_of_mul_left_eq
 
 theorem exists_eq_mul_left_of_dvd (h : a ∣ b) : ∃ c, b = c * a :=
   Dvd.elim h fun c => fun H1 : b = a * c => Exists.intro c (Eq.trans H1 (mul_comm a c))

Mathlib/Algebra/Divisibility/Units.lean

@@ -29,12 +29,14 @@ variable [Monoid α] {a b : α} {u : αˣ}
     divide any element of the monoid. -/
 theorem coe_dvd : ↑u ∣ a :=
   ⟨↑u⁻¹ * a, by simp⟩
+#align units.coe_dvd Units.coe_dvd
 
 /-- In a monoid, an element `a` divides an element `b` iff `a` divides all
     associates of `b`. -/
 theorem dvd_mul_right : a ∣ b * u ↔ a ∣ b :=
   Iff.intro (fun ⟨c, Eq⟩ ↦ ⟨c * ↑u⁻¹, by rw [← mul_assoc, ← Eq, Units.mul_inv_cancel_right]⟩)
     fun ⟨c, Eq⟩ ↦ Eq.symm ▸ (_root_.dvd_mul_right _ _).mul_right _
+#align units.dvd_mul_right Units.dvd_mul_right
 
 /-- In a monoid, an element `a` divides an element `b` iff all associates of `a` divide `b`. -/
 theorem mul_right_dvd : a * u ∣ b ↔ a ∣ b :=
@@ -77,17 +79,20 @@ variable [Monoid α] {a b u : α} (hu : IsUnit u)
 theorem dvd : u ∣ a := by
   rcases hu with ⟨u, rfl⟩
   apply Units.coe_dvd
+#align is_unit.dvd IsUnit.dvd
 
 @[simp]
 theorem dvd_mul_right : a ∣ b * u ↔ a ∣ b := by
   rcases hu with ⟨u, rfl⟩
   apply Units.dvd_mul_right
+#align is_unit.dvd_mul_right IsUnit.dvd_mul_right
 
 /-- In a monoid, an element a divides an element b iff all associates of `a` divide `b`.-/
 @[simp]
 theorem mul_right_dvd : a * u ∣ b ↔ a ∣ b := by
   rcases hu with ⟨u, rfl⟩
   apply Units.mul_right_dvd
+#align is_unit.mul_right_dvd IsUnit.mul_right_dvd
 
 end Monoid
 
@@ -101,13 +106,15 @@ variable [CommMonoid α] (a b u : α) (hu : IsUnit u)
 theorem dvd_mul_left : a ∣ u * b ↔ a ∣ b := by
   rcases hu with ⟨u, rfl⟩
   apply Units.dvd_mul_left
+#align is_unit.dvd_mul_left IsUnit.dvd_mul_left
 
 /-- In a commutative monoid, an element `a` divides an element `b` iff all
   left associates of `a` divide `b`.-/
 @[simp]
 theorem mul_left_dvd : u * a ∣ b ↔ a ∣ b := by
   rcases hu with ⟨u, rfl⟩
   apply Units.mul_left_dvd
+#align is_unit.mul_left_dvd IsUnit.mul_left_dvd
 
 end CommMonoid