From ea43ebd54a0848bf99b9a080daaf31e4025d2552 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Sat, 27 Jul 2024 17:37:17 +1000
Subject: [PATCH] chore: cleanups for Mathlib.Init (#4852)

It is convenient to adjust some attributes here, to allow easier cleanup
in `Mathlib.Init`.
---
 src/Init/Core.lean         | 22 ++++++++++++++--------
 src/Init/Data/Nat/Gcd.lean |  3 +++
 src/Init/Prelude.lean      |  2 +-
 3 files changed, 18 insertions(+), 9 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 7852398300..1a3b97213b 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -474,6 +474,8 @@ class LawfulSingleton (α : Type u) (β : Type v) [EmptyCollection β] [Insert 
   insert_emptyc_eq (x : α) : (insert x ∅ : β) = singleton x
 export LawfulSingleton (insert_emptyc_eq)
 
+attribute [simp] insert_emptyc_eq
+
 /-- Type class used to implement the notation `{ a ∈ c | p a }` -/
 class Sep (α : outParam <| Type u) (γ : Type v) where
   /-- Computes `{ a ∈ c | p a }`. -/
@@ -701,7 +703,7 @@ theorem Ne.elim (h : a ≠ b) : a = b → False := h
 
 theorem Ne.irrefl (h : a ≠ a) : False := h rfl
 
-theorem Ne.symm (h : a ≠ b) : b ≠ a := fun h₁ => h (h₁.symm)
+@[symm] theorem Ne.symm (h : a ≠ b) : b ≠ a := fun h₁ => h (h₁.symm)
 
 theorem ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨Ne.symm, Ne.symm⟩
 
@@ -754,7 +756,7 @@ noncomputable def HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (
 theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : HEq a b) (h₂ : p α a) : p β b :=
   HEq.ndrecOn h₁ h₂
 
-theorem HEq.symm (h : HEq a b) : HEq b a :=
+@[symm] theorem HEq.symm (h : HEq a b) : HEq b a :=
   h.rec (HEq.refl a)
 
 theorem heq_of_eq (h : a = a') : HEq a a' :=
@@ -810,15 +812,15 @@ instance : Trans Iff Iff Iff where
 theorem Eq.comm {a b : α} : a = b ↔ b = a := Iff.intro Eq.symm Eq.symm
 theorem eq_comm {a b : α} : a = b ↔ b = a := Eq.comm
 
-theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp
+@[symm] theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp
 theorem Iff.comm: (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm
 theorem iff_comm : (a ↔ b) ↔ (b ↔ a) := Iff.comm
 
-theorem And.symm : a ∧ b → b ∧ a := fun ⟨ha, hb⟩ => ⟨hb, ha⟩
+@[symm] theorem And.symm : a ∧ b → b ∧ a := fun ⟨ha, hb⟩ => ⟨hb, ha⟩
 theorem And.comm : a ∧ b ↔ b ∧ a := Iff.intro And.symm And.symm
 theorem and_comm : a ∧ b ↔ b ∧ a := And.comm
 
-theorem Or.symm : a ∨ b → b ∨ a := .rec .inr .inl
+@[symm] theorem Or.symm : a ∨ b → b ∨ a := .rec .inr .inl
 theorem Or.comm : a ∨ b ↔ b ∨ a := Iff.intro Or.symm Or.symm
 theorem or_comm : a ∨ b ↔ b ∨ a := Or.comm
 
@@ -1201,9 +1203,13 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
 
 /-! # Dependent products -/
 
-theorem ex_of_PSigma {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
+theorem PSigma.exists {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
   | ⟨x, hx⟩ => ⟨x, hx⟩
 
+@[deprecated PSigma.exists (since := "2024-07-27")]
+theorem ex_of_PSigma {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x) :=
+  PSigma.exists
+
 protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂}
     (h₁ : a₁ = a₂) (h₂ : Eq.ndrec b₁ h₁ = b₂) : PSigma.mk a₁ b₁ = PSigma.mk a₂ b₂ := by
   subst h₁
@@ -1545,7 +1551,7 @@ protected abbrev rec
     (q : Quot r) : motive q :=
   Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((lift (Quot.indep f) (Quot.indepCoherent f h) q).2)
 
-@[inherit_doc Quot.rec] protected abbrev recOn
+@[inherit_doc Quot.rec, elab_as_elim] protected abbrev recOn
     (q : Quot r)
     (f : (a : α) → motive (Quot.mk r a))
     (h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
@@ -1556,7 +1562,7 @@ protected abbrev rec
 Dependent induction principle for a quotient, when the target type is a `Subsingleton`.
 In this case the quotient's side condition is trivial so any function can be lifted.
 -/
-protected abbrev recOnSubsingleton
+@[elab_as_elim] protected abbrev recOnSubsingleton
     [h : (a : α) → Subsingleton (motive (Quot.mk r a))]
     (q : Quot r)
     (f : (a : α) → motive (Quot.mk r a))
diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean
index 9402b474a1..9aa3e558c6 100644
--- a/src/Init/Data/Nat/Gcd.lean
+++ b/src/Init/Data/Nat/Gcd.lean
@@ -46,6 +46,9 @@ theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) := by
 theorem gcd_add_one (x y : Nat) : gcd (x + 1) y = gcd (y % (x + 1)) (x + 1) := by
   rw [gcd]; rfl
 
+theorem gcd_def (x y : Nat) : gcd x y = if x = 0 then y else gcd (y % x) x := by
+  cases x <;> simp [Nat.gcd_add_one]
+
 @[simp] theorem gcd_one_left (n : Nat) : gcd 1 n = 1 := by
   rw [gcd_succ, mod_one]
   rfl
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 64726988b6..54fbcd3d5d 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -320,7 +320,7 @@ Because this is in the `Eq` namespace, if you have a variable `h : a = b`,
 
 For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
-theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a :=
+@[symm] theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a :=
   h ▸ rfl
 
 /--