chore: add #align statements for Core and Std (#1966)

Mathlib.lean

@@ -633,6 +633,7 @@ import Mathlib.Init.Algebra.Functions
 import Mathlib.Init.Algebra.Order
 import Mathlib.Init.Align
 import Mathlib.Init.CcLemmas
+import Mathlib.Init.Classes.Order
 import Mathlib.Init.Classical
 import Mathlib.Init.Control.Combinators
 import Mathlib.Init.Core
@@ -641,18 +642,25 @@ import Mathlib.Init.Data.Bool.Lemmas
 import Mathlib.Init.Data.Fin.Basic
 import Mathlib.Init.Data.Int.Basic
 import Mathlib.Init.Data.Int.Bitwise
+import Mathlib.Init.Data.Int.DivMod
+import Mathlib.Init.Data.Int.Lemmas
 import Mathlib.Init.Data.Int.Order
 import Mathlib.Init.Data.List.Basic
 import Mathlib.Init.Data.List.Instances
 import Mathlib.Init.Data.List.Lemmas
 import Mathlib.Init.Data.Nat.Basic
 import Mathlib.Init.Data.Nat.Bitwise
+import Mathlib.Init.Data.Nat.Div
 import Mathlib.Init.Data.Nat.GCD
 import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Init.Data.Nat.Notation
+import Mathlib.Init.Data.Option.Basic
+import Mathlib.Init.Data.Option.Init.Lemmas
+import Mathlib.Init.Data.Option.Lemmas
 import Mathlib.Init.Data.Ordering.Basic
 import Mathlib.Init.Data.Prod
 import Mathlib.Init.Data.Quot
+import Mathlib.Init.Data.Rat.Basic
 import Mathlib.Init.Data.Sigma.Basic
 import Mathlib.Init.Data.Subtype.Basic
 import Mathlib.Init.Function

Mathlib/Data/List/Basic.lean

@@ -18,8 +18,6 @@ import Std.Data.List.Lemmas
 # Basic properties of lists
 -/
 
-#align list.mem_cons_iff List.mem_cons
-
 open Function
 
 open Nat hiding one_pos
@@ -696,9 +694,6 @@ theorem mem_reverse' {a : α} {l : List α} : a ∈ reverse l ↔ a ∈ l :=
 
 /-! ### empty -/
 
--- Porting note: Definition from Lean3 core, so should be moved
-#align list.empty List.isEmpty
-
 -- Porting note: this does not work as desired
 -- attribute [simp] List.isEmpty
 
@@ -1064,8 +1059,6 @@ def bidirectionalRecOn {C : List α → Sort _} (l : List α) (H0 : C []) (H1 :
 
 attribute [refl] List.Sublist.refl
 
-#align list.sublist.cons2 List.Sublist.cons₂
-
 #align list.nil_sublist List.nil_sublist
 #align list.sublist.refl List.Sublist.refl
 #align list.sublist.trans List.Sublist.trans

Mathlib/Data/Nat/Sqrt.lean

@@ -27,6 +27,7 @@ See [Wikipedia, *Methods of computing square roots*]
 
 namespace Nat
 
+#align nat.sqrt Nat.sqrt
 -- Porting note: the implementation òf `Nat.sqrt` in `Std` no longer needs `sqrt_aux`.
 #noalign nat.sqrt_aux_dec
 #noalign nat.sqrt_aux

Mathlib/Init/Classes/Order.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2023 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import Std.Classes.Order
+import Mathlib.Mathport.Rename
+
+/-!
+# Align statements for declarations from Std
+-/
+
+#align ordering.swap_inj Ordering.swap_inj

Mathlib/Init/Core.lean

@@ -140,3 +140,6 @@ end Combinator
   | node (left right : BinTree α) : BinTree α
 
 attribute [elab_without_expected_type] BinTree.node BinTree.leaf
+
+#align function.const_apply Function.const_apply
+#align function.comp_apply Function.comp_apply

Mathlib/Init/Data/Int/Basic.lean

@@ -133,3 +133,5 @@ def natMod (m n : ℤ) : ℕ := (m.emod n).toNat
 #align int.nat_mod Int.natMod
 
 #align int.sign_mul_nat_abs Int.sign_mul_natAbs
+
+#align int.to_nat' Int.toNat'

Mathlib/Init/Data/Int/DivMod.lean

@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2023 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import Std.Data.Int.DivMod
+import Mathlib.Mathport.Rename
+
+/-!
+# Align statements for declarations from Std
+-/
+
+#align int.zero_div Int.zero_div
+#align int.div_zero Int.div_zero
+#align int.mul_sign Int.mul_sign

Mathlib/Init/Data/Int/Lemmas.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2023 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import Std.Data.Int.Lemmas
+import Mathlib.Mathport.Rename
+
+/-!
+# Align statements for declarations from Std
+-/
+
+#align int.default_eq_zero Int.default_eq_zero
+#align int.add_def Int.add_def
+#align int.mul_def Int.mul_def
+#align int.add_neg_one Int.add_neg_one
+#align int.sign_neg Int.sign_neg
+#align int.sign_mul Int.sign_mul
+#align int.add_one_le_iff Int.add_one_le_iff

Mathlib/Init/Data/List/Basic.lean

@@ -80,3 +80,6 @@ theorem le_eq_not_gt [LT α] : ∀ l₁ l₂ : List α, (l₁ ≤ l₂) = ¬l₂
 #align list.le_eq_not_gt List.le_eq_not_gt
 
 end List
+
+#align list.replicate List.replicate
+#align list.length_replicate List.length_replicate

Mathlib/Init/Data/List/Lemmas.lean

@@ -83,3 +83,7 @@ theorem length_mapAccumr₂ :
 end MapAccumr₂
 
 end List
+
+#align list.length_zip_with List.length_zipWith
+#align list.mem_replicate List.mem_replicate
+#align list.eq_of_mem_replicate List.eq_of_mem_replicate

Mathlib/Init/Data/Nat/Basic.lean

@@ -59,3 +59,4 @@ protected theorem bit1_ne_zero (n : ℕ) : bit1 n ≠ 0 :=
 #align nat.bit1_ne_zero Nat.bit1_ne_zero
 
 end Nat
+

Mathlib/Init/Data/Nat/Div.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2023 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import Init.Data.Nat.Div
+import Mathlib.Mathport.Rename
+
+/-!
+# Align statements for declarations from Core
+-/
+
+#align nat.div_add_mod Nat.div_add_mod

Mathlib/Init/Data/Nat/GCD.lean

@@ -41,3 +41,94 @@ theorem gcd_def (x y : ℕ) : gcd x y = if x = 0 then y else gcd (y % x) x := by
 #align nat.coprime Nat.coprime
 
 end Nat
+
+#align nat.gcd_dvd Nat.gcd_dvd
+#align nat.gcd_dvd_left Nat.gcd_dvd_left
+#align nat.gcd_dvd_right Nat.gcd_dvd_right
+#align nat.gcd_le_left Nat.gcd_le_left
+#align nat.gcd_le_right Nat.gcd_le_right
+#align nat.dvd_gcd Nat.dvd_gcd
+#align nat.dvd_gcd_iff Nat.dvd_gcd_iff
+#align nat.gcd_comm Nat.gcd_comm
+#align nat.gcd_eq_left_iff_dvd Nat.gcd_eq_left_iff_dvd
+#align nat.gcd_eq_right_iff_dvd Nat.gcd_eq_right_iff_dvd
+#align nat.gcd_assoc Nat.gcd_assoc
+#align nat.gcd_one_right Nat.gcd_one_right
+#align nat.gcd_mul_left Nat.gcd_mul_left
+#align nat.gcd_mul_right Nat.gcd_mul_right
+#align nat.gcd_pos_of_pos_left Nat.gcd_pos_of_pos_left
+#align nat.gcd_pos_of_pos_right Nat.gcd_pos_of_pos_right
+#align nat.eq_zero_of_gcd_eq_zero_left Nat.eq_zero_of_gcd_eq_zero_left
+#align nat.eq_zero_of_gcd_eq_zero_right Nat.eq_zero_of_gcd_eq_zero_right
+#align nat.gcd_div Nat.gcd_div
+#align nat.gcd_dvd_gcd_of_dvd_left Nat.gcd_dvd_gcd_of_dvd_left
+#align nat.gcd_dvd_gcd_of_dvd_right Nat.gcd_dvd_gcd_of_dvd_right
+#align nat.gcd_dvd_gcd_mul_left Nat.gcd_dvd_gcd_mul_left
+#align nat.gcd_dvd_gcd_mul_right Nat.gcd_dvd_gcd_mul_right
+#align nat.gcd_dvd_gcd_mul_left_right Nat.gcd_dvd_gcd_mul_left_right
+#align nat.gcd_dvd_gcd_mul_right_right Nat.gcd_dvd_gcd_mul_right_right
+#align nat.gcd_eq_left Nat.gcd_eq_left
+#align nat.gcd_eq_right Nat.gcd_eq_right
+#align nat.gcd_mul_left_left Nat.gcd_mul_left_left
+#align nat.gcd_mul_left_right Nat.gcd_mul_left_right
+#align nat.gcd_mul_right_left Nat.gcd_mul_right_left
+#align nat.gcd_mul_right_right Nat.gcd_mul_right_right
+#align nat.gcd_gcd_self_right_left Nat.gcd_gcd_self_right_left
+#align nat.gcd_gcd_self_right_right Nat.gcd_gcd_self_right_right
+#align nat.gcd_gcd_self_left_right Nat.gcd_gcd_self_left_right
+#align nat.gcd_gcd_self_left_left Nat.gcd_gcd_self_left_left
+#align nat.gcd_eq_zero_iff Nat.gcd_eq_zero_iff
+#align nat.lcm_comm Nat.lcm_comm
+#align nat.lcm_zero_left Nat.lcm_zero_left
+#align nat.lcm_zero_right Nat.lcm_zero_right
+#align nat.lcm_one_left Nat.lcm_one_left
+#align nat.lcm_one_right Nat.lcm_one_right
+#align nat.lcm_self Nat.lcm_self
+#align nat.dvd_lcm_left Nat.dvd_lcm_left
+#align nat.dvd_lcm_right Nat.dvd_lcm_right
+#align nat.gcd_mul_lcm Nat.gcd_mul_lcm
+#align nat.lcm_dvd Nat.lcm_dvd
+#align nat.lcm_assoc Nat.lcm_assoc
+#align nat.lcm_ne_zero Nat.lcm_ne_zero
+#align nat.coprime_iff_gcd_eq_one Nat.coprime_iff_gcd_eq_one
+#align nat.coprime.gcd_eq_one Nat.coprime.gcd_eq_one
+#align nat.coprime.symm Nat.coprime.symm
+#align nat.coprime_comm Nat.coprime_comm
+#align nat.coprime.dvd_of_dvd_mul_right Nat.coprime.dvd_of_dvd_mul_right
+#align nat.coprime.dvd_of_dvd_mul_left Nat.coprime.dvd_of_dvd_mul_left
+#align nat.coprime.gcd_mul_left_cancel Nat.coprime.gcd_mul_left_cancel
+#align nat.coprime.gcd_mul_right_cancel Nat.coprime.gcd_mul_right_cancel
+#align nat.coprime.gcd_mul_left_cancel_right Nat.coprime.gcd_mul_left_cancel_right
+#align nat.coprime.gcd_mul_right_cancel_right Nat.coprime.gcd_mul_right_cancel_right
+#align nat.coprime_div_gcd_div_gcd Nat.coprime_div_gcd_div_gcd
+#align nat.not_coprime_of_dvd_of_dvd Nat.not_coprime_of_dvd_of_dvd
+#align nat.exists_coprime Nat.exists_coprime
+#align nat.exists_coprime' Nat.exists_coprime'
+#align nat.coprime.mul Nat.coprime.mul
+#align nat.coprime.mul_right Nat.coprime.mul_right
+#align nat.coprime.coprime_dvd_left Nat.coprime.coprime_dvd_left
+#align nat.coprime.coprime_dvd_right Nat.coprime.coprime_dvd_right
+#align nat.coprime.coprime_mul_left Nat.coprime.coprime_mul_left
+#align nat.coprime.coprime_mul_right Nat.coprime.coprime_mul_right
+#align nat.coprime.coprime_mul_left_right Nat.coprime.coprime_mul_left_right
+#align nat.coprime.coprime_mul_right_right Nat.coprime.coprime_mul_right_right
+#align nat.coprime.coprime_div_left Nat.coprime.coprime_div_left
+#align nat.coprime.coprime_div_right Nat.coprime.coprime_div_right
+#align nat.coprime_mul_iff_left Nat.coprime_mul_iff_left
+#align nat.coprime_mul_iff_right Nat.coprime_mul_iff_right
+#align nat.coprime.gcd_left Nat.coprime.gcd_left
+#align nat.coprime.gcd_right Nat.coprime.gcd_right
+#align nat.coprime.gcd_both Nat.coprime.gcd_both
+#align nat.coprime.mul_dvd_of_dvd_of_dvd Nat.coprime.mul_dvd_of_dvd_of_dvd
+#align nat.coprime_zero_left Nat.coprime_zero_left
+#align nat.coprime_zero_right Nat.coprime_zero_right
+#align nat.coprime_one_left Nat.coprime_one_left
+#align nat.coprime_one_right Nat.coprime_one_right
+#align nat.coprime_self Nat.coprime_self
+#align nat.coprime.pow_left Nat.coprime.pow_left
+#align nat.coprime.pow_right Nat.coprime.pow_right
+#align nat.coprime.pow Nat.coprime.pow
+#align nat.coprime.eq_one_of_dvd Nat.coprime.eq_one_of_dvd
+#align nat.gcd_mul_dvd_mul_gcd Nat.gcd_mul_dvd_mul_gcd
+#align nat.coprime.gcd_mul Nat.coprime.gcd_mul
+#align nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul

Mathlib/Init/Data/Nat/Lemmas.lean

@@ -372,3 +372,5 @@ lemma repr_length (n e : Nat) : 0 < e → n < 10 ^ e → (Nat.repr n).length <=
       exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0
 
 end Nat
+
+#align nat.succ_le_succ_iff Nat.succ_le_succ_iff

Mathlib/Init/Data/Option/Basic.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2023 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import Std.Data.Option.Basic
+import Mathlib.Mathport.Rename
+
+/-!
+# Align statements for declarations from Std
+-/
+
+#align option.mem_def Option.mem_def
+#align option.is_none_iff_eq_none Option.isNone_iff_eq_none
+#align option.some_inj Option.some_inj
+#align option.decidable_eq_none Option.decidable_eq_none
+#align option.guard Option.guard
+#align option.to_list Option.toList
+#align option.rel Option.Rel
+#align option.pbind Option.pbind
+#align option.pmap Option.pmap
+#align option.join Option.join
+
+#align option.filter Option.filter

Mathlib/Init/Data/Option/Init/Lemmas.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2023 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import Std.Data.Option.Init.Lemmas
+import Mathlib.Mathport.Rename
+
+/-!
+# Align statements for declarations from Std
+-/
+
+#align option.map_none' Option.map_none'
+#align option.map_some' Option.map_some'
+#align option.none_bind Option.none_bind
+#align option.some_bind Option.some_bind

Mathlib/Init/Data/Option/Lemmas.lean

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2023 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import Std.Data.Option.Lemmas
+import Mathlib.Mathport.Rename
+
+/-!
+# Align statements for declarations from Std
+-/
+
+#align option.mem_iff Option.mem_iff
+#align option.some_ne_none Option.some_ne_none
+#align option.forall Option.forall
+#align option.exists Option.exists
+#align option.get_mem Option.get_mem
+#align option.get_of_mem Option.get_of_mem
+#align option.not_mem_none Option.not_mem_none
+#align option.some_get Option.some_get
+#align option.get_some Option.get_some
+#align option.mem_unique Option.mem_unique
+#align option.ext Option.ext
+#align option.eq_none_iff_forall_not_mem Option.eq_none_iff_forall_not_mem
+#align option.eq_some_iff_get_eq Option.eq_some_iff_get_eq
+#align option.ne_none_iff_exists Option.ne_none_iff_exists
+#align option.ne_none_iff_exists' Option.ne_none_iff_exists'
+#align option.bex_ne_none Option.bex_ne_none
+#align option.ball_ne_none Option.ball_ne_none
+#align option.bind_some Option.bind_some
+#align option.bind_eq_some Option.bind_eq_some
+#align option.bind_eq_none Option.bind_eq_none
+#align option.bind_comm Option.bind_comm
+#align option.bind_assoc Option.bind_assoc
+#align option.join_eq_some Option.join_eq_some
+#align option.join_ne_none Option.join_ne_none
+#align option.join_ne_none' Option.join_ne_none'
+#align option.join_eq_none Option.join_eq_none
+#align option.bind_id_eq_join Option.bind_id_eq_join
+#align option.map_eq_map Option.map_eq_map
+#align option.map_none Option.map_none
+#align option.map_some Option.map_some
+#align option.map_eq_some' Option.map_eq_some'
+#align option.map_eq_some Option.map_eq_some
+#align option.map_eq_none' Option.map_eq_none'
+#align option.map_eq_none Option.map_eq_none
+#align option.map_congr Option.map_congr
+#align option.map_map Option.map_map
+#align option.comp_map Option.comp_map
+#align option.map_comp_map Option.map_comp_map
+#align option.mem_map_of_mem Option.mem_map_of_mem
+#align option.bind_map_comm Option.bind_map_comm
+#align option.join_map_eq_map_join Option.join_map_eq_map_join
+#align option.join_join Option.join_join
+#align option.mem_of_mem_join Option.mem_of_mem_join
+#align option.guard_eq_some Option.guard_eq_some
+#align option.choice Option.choice
+#align option.choice_eq Option.choice_eq
+#align option.to_list_some Option.to_list_some
+#align option.to_list_none Option.to_list_none

Mathlib/Init/Data/Rat/Basic.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2023 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import Std.Data.Rat.Basic
+import Mathlib.Mathport.Rename
+
+/-!
+# Align statements for declarations from Std
+-/
+
+#align rat.ext Rat.ext
+#align rat Rat
+#align rat.ext_iff Rat.ext_iff
+#align rat.floor Rat.floor