feat: align init.{core, logic}

Mathlib.lean

@@ -45,14 +45,15 @@ import Mathlib.Data.UnionFind
 import Mathlib.Init.Algebra.Classes
 import Mathlib.Init.Algebra.Functions
 import Mathlib.Init.Algebra.Order
+import Mathlib.Init.Core
 import Mathlib.Init.Data.Int.Basic
 import Mathlib.Init.Data.Int.Notation
 import Mathlib.Init.Data.Nat.Basic
 import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Init.Function
 import Mathlib.Init.Logic
 import Mathlib.Init.Set
-import Mathlib.Init.Zero
+import Mathlib.Init.ZeroOne
 import Mathlib.Lean.Exception
 import Mathlib.Lean.Expr
 import Mathlib.Lean.Expr.Basic

Mathlib/Algebra/Group/Defs.lean

@@ -3,10 +3,11 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 -/
-import Mathlib.Init.Zero
-import Mathlib.Init.Data.Int.Notation
 import Mathlib.Tactic.Spread
 import Mathlib.Tactic.ToAdditive
+import Mathlib.Init.ZeroOne
+import Mathlib.Init.Data.Int.Notation
+import Mathlib.Data.List.Basic
 
 /-!
 # Typeclasses for (semi)groups and monoids
@@ -77,23 +78,12 @@ universe u
 
 variable {G : Type _}
 
-@[to_additive Zero]
-class One (α : Type u) where
-  one : α
-
-@[to_additive Zero.toOfNat0]
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-@[to_additive Zero.ofOfNat0]
-instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
-  one := 1
-
 /-- Class of types that have an inversion operation. -/
 @[to_additive Neg]
 class Inv (α : Type u) where
   /-- Invert an element of α. -/
   inv : α → α
+#align has_inv Inv
 
 @[inherit_doc]
 postfix:max "⁻¹" => Inv.inv

Mathlib/Data/List/Basic.lean

@@ -218,7 +218,7 @@ theorem product_spec (xs : List α) (ys : List β) (x : α) (y : β) :
   to apply `f`. -/
 @[simp]
 def pmap {p : α → Prop} (f : ∀ a, p a → β) : ∀ l : List α, (∀ a ∈ l, p a) → List β
-  | [], H => []
+  | [], _ => []
   | a :: l, H => f a (forall_mem_cons.1 H).1 :: pmap f l (forall_mem_cons.1 H).2
 
 /-- "Attach" the proof that the elements of `l` are in `l` to produce a new list

Mathlib/Data/List/Pairwise.lean

@@ -13,13 +13,13 @@ namespace List
 
 variable {α β : Type _} {R S T : α → α → Prop} {a : α} {l : List α}
 
-theorem pairwise_append_comm (s : symmetric R) {l₁ l₂ : List α} :
+theorem pairwise_append_comm (s : Symmetric R) {l₁ l₂ : List α} :
     Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁) := by
   have : ∀ l₁ l₂ : List α, (∀ x : α, x ∈ l₁ → ∀ y : α, y ∈ l₂ → R x y) →
     ∀ x : α, x ∈ l₂ → ∀ y : α, y ∈ l₁ → R x y := fun l₁ l₂ a x xm y ym => s (a y ym x xm)
-  simp only [pairwise_append, And.left_comm] <;> rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]
+  simp only [pairwise_append, and_left_comm] <;> rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]
 
-theorem pairwise_middle (s : symmetric R) {a : α} {l₁ l₂ : List α} :
+theorem pairwise_middle (s : Symmetric R) {a : α} {l₁ l₂ : List α} :
     Pairwise R (l₁ ++ a :: l₂) ↔ Pairwise R (a :: (l₁ ++ l₂)) :=
   show Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂) by
     rw [← append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]

Mathlib/Data/List/Perm.lean

@@ -147,7 +147,7 @@ theorem Perm.eq_nil {l : List α} (p : l ~ []) : l = [] := eq_nil_of_length_eq_z
 
 theorem Perm.nil_eq {l : List α} (p : [] ~ l) : [] = l := p.symm.eq_nil.symm
 
-theorem Perm.pairwise_iff {R : α → α → Prop} (S : symmetric R) :
+theorem Perm.pairwise_iff {R : α → α → Prop} (S : Symmetric R) :
     ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → (Pairwise R l₁ ↔ Pairwise R l₂) := by
   suffices ∀ {l₁ l₂}, l₁ ~ l₂ → Pairwise R l₁ → Pairwise R l₂ from
     fun l₁ l₂ p => ⟨this p, this p.symm⟩

Mathlib/Data/String/Defs.lean

@@ -1,4 +1,4 @@
-import Mathlib.Data.List.Basic
+import Std.Data.List.Basic
 
 namespace String
 
@@ -9,10 +9,10 @@ def leftpad (n : Nat) (c : Char) (s : String) : String :=
 
 def replicate (n : Nat) (c : Char) : String := ⟨List.replicate n c⟩
 
-def isPrefix : String -> String -> Prop
+def isPrefix : String → String → Prop
 | ⟨d1⟩, ⟨d2⟩ => List.isPrefix d1 d2
 
-def isSuffix : String -> String -> Prop
+def isSuffix : String → String → Prop
 | ⟨d1⟩, ⟨d2⟩ => List.isSuffix d1 d2
 
 /-- `string.mapTokens c f s` tokenizes `s : string` on `c : char`, maps `f` over each token, and

Mathlib/Init/Algebra/Classes.lean

@@ -362,10 +362,10 @@ theorem is_strict_weak_order_of_is_total_preorder {α : Type u} {le : α → α
       Iff.mpr (h _ _) nca,
     irrefl := fun a hlt => absurd (refl_of le a) (Iff.mp (h _ _) hlt),
     incomp_trans := fun a b c ⟨nab, nba⟩ ⟨nbc, ncb⟩ =>
-      have hba : le b a := Decidable.of_not_not (Iff.mp (not_iff_not_of_iff (h _ _)) nab)
-      have hab : le a b := Decidable.of_not_not (Iff.mp (not_iff_not_of_iff (h _ _)) nba)
-      have hcb : le c b := Decidable.of_not_not (Iff.mp (not_iff_not_of_iff (h _ _)) nbc)
-      have hbc : le b c := Decidable.of_not_not (Iff.mp (not_iff_not_of_iff (h _ _)) ncb)
+      have hba : le b a := Decidable.of_not_not (Iff.mp (not_congr (h _ _)) nab)
+      have hab : le a b := Decidable.of_not_not (Iff.mp (not_congr (h _ _)) nba)
+      have hcb : le c b := Decidable.of_not_not (Iff.mp (not_congr (h _ _)) nbc)
+      have hbc : le b c := Decidable.of_not_not (Iff.mp (not_congr (h _ _)) ncb)
       have hac : le a c := trans_of le hab hbc
       have hca : le c a := trans_of le hcb hba
       And.intro (fun n => absurd hca (Iff.mp (h _ _) n)) fun n => absurd hac (Iff.mp (h _ _) n) }

Mathlib/Init/Algebra/Functions.lean

@@ -58,7 +58,7 @@ by apply eq_min
    . intros d h₁ h₂; apply le_min; apply le_min h₁; apply le_trans h₂; apply min_le_left;
      apply le_trans h₂; apply min_le_right
 
-lemma min_left_comm : @left_commutative α α min :=
+lemma min_left_comm : @LeftCommutative α α min :=
 left_comm min (@min_comm α _) (@min_assoc α _)
 
 @[simp]

Mathlib/Init/Core.lean

@@ -0,0 +1,137 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Mario Carneiro
+
+notation, basic datatypes and type classes
+-/
+import Mathlib.Mathport.Rename
+import Std.Classes.SetNotation
+
+/-! ### alignments from lean 3 `init.core` -/
+
+#align id id -- align this first so idDelta doesn't take priority
+#align idDelta id
+
+#align opt_param optParam
+#align out_param outParam
+
+#align idRhs id
+#align punit PUnit
+#align punit.star PUnit.unit
+#align unit.star Unit.unit
+
+#align thunk Thunk'
+
+-- Note: we do not currently auto-align constants.
+#align quot Quot
+#align quot.mk Quot.mk
+#align quot.lift Quot.lift
+#align quot.ind Quot.ind
+
+#align heq HEq
+#align pprod PProd
+
+#align and.left And.left
+#align and.right And.right
+#align and.elim_left And.left
+#align and.elim_right And.right
+
+-- TODO
+-- attribute [refl] Eq.refl
+-- attribute [elab_as_elim, subst] Eq.subst
+-- attribute [trans] Eq.trans
+-- attribute [symm] Eq.symm
+
+def Prod.mk.injArrow {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} :
+    (x₁, y₁) = (x₂, y₂) → ∀ ⦃P : Sort w⦄, (x₁ = x₂ → y₁ = y₂ → P) → P :=
+  fun h₁ _ h₂ => Prod.noConfusion h₁ h₂
+
+def PProd.mk.injArrow {α : Type u} {β : Type v} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} :
+    (x₁, y₁) = (x₂, y₂) → ∀ ⦃P : Sort w⦄, (x₁ = x₂ → y₁ = y₂ → P) → P :=
+  fun h₁ _ h₂ => Prod.noConfusion h₁ h₂
+
+#align psum PSum
+#align or.intro_right Or.intro_rightₓ -- reorder implicits
+#align psigma PSigma
+
+#align bool.ff Bool.false
+#align bool.tt Bool.true
+
+-- attribute [pp_using_anonymous_constructor] Sigma PSigma Subtype PProd And
+
+-- Generic 'has'-stripping
+-- Note: we don't currently strip automatically for various reasons.
+#align has_add Add
+#align has_mul Mul
+#align has_neg Neg
+#align has_sub Sub
+#align has_div Div
+#align has_dvd Dvd
+#align has_mod Mod
+#align has_le LE
+#align has_le.le LE.le
+#align has_lt LT
+#align has_lt.lt LT.lt
+#align has_append Append
+#align has_andthen AndThen'
+
+@[deprecated AndThen]
+class AndThen' (α : Type u) (β : Type v) (σ : outParam <| Type w) where
+  andthen : α → β → σ
+
+#align has_union Union
+#align has_equiv HasEquivₓ -- universe levels don't match
+#align has_inter Inter
+#align has_sdiff Sdiff
+
+#align has_subset HasSubset
+#align has_subset.subset HasSubset.Subset
+#align has_ssubset HasSSubset
+#align has_ssubset.ssubset HasSSubset.SSubset
+#align has_emptyc EmptyCollection
+#align has_emptyc.emptyc EmptyCollection.emptyCollection
+#align has_insert Insert
+#align has_singleton Singleton
+#align has_sep Sep
+#align has_mem Membership
+#align has_pow Pow
+
+#align gt GT.gt
+#align ge GE.ge
+
+#align is_lawful_singleton LawfulSingleton
+
+attribute [simp] insert_emptyc_eq
+
+@[deprecated] def Std.Priority.default : Nat := 1000
+@[deprecated] def Std.Priority.max : Nat := 4294967295
+@[deprecated] protected def Nat.prio := Std.Priority.default + 100
+@[deprecated] def Std.Prec.max : Nat := 1024
+@[deprecated] def Std.Prec.arrow : Nat := 25
+@[deprecated] def Std.Prec.maxPlus : Nat := Std.Prec.max + 10
+
+#align has_sizeof SizeOf
+#align has_sizeof.sizeof SizeOf.sizeOf
+#align sizeof SizeOf.sizeOf
+
+#align nat_add_zero Nat.add_zero
+
+-- Combinator calculus
+namespace Combinator
+
+def I (a : α) := a
+def K (a : α) (_b : β) := a
+def S (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
+#align combinator.I Combinator.I
+#align combinator.K Combinator.K
+#align combinator.S Combinator.S
+
+end Combinator
+
+@[deprecated] inductive BinTree (α : Type u)
+  | Empty : BinTree α
+  | leaf (val : α) : BinTree α
+  | node (left right : BinTree α) : BinTree α
+
+attribute [elab_without_expected_type] BinTree.node BinTree.leaf