chore: fixing some naming issues in Data/* (#570)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib/Data/Option/Basic.lean

@@ -50,8 +50,9 @@ theorem coe_get {o : Option α} (h : o.isSome) : ((Option.get _ h : α) : Option
 theorem eq_of_mem_of_mem {a : α} {o1 o2 : Option α} (h1 : a ∈ o1) (h2 : a ∈ o2) : o1 = o2 :=
   h1.trans h2.symm
 
-theorem Mem.left_unique : Relator.LeftUnique ((· ∈ ·) : α → Option α → Prop) :=
+theorem Mem.leftUnique : Relator.LeftUnique ((· ∈ ·) : α → Option α → Prop) :=
 fun _ _ _=> mem_unique
+#align Mem.left_unique Mem.leftUnique
 
 theorem some_injective (α : Type _) : Function.Injective (@some α) := fun _ _ => some_inj.mp
 

Mathlib/Data/Prod/Basic.lean

@@ -222,17 +222,19 @@ instance {r : α → α → Prop} {s : β → β → Prop} [IsStrictOrder α r]
     | (_, _), (_, _), .right _ _,     .left  _ _ hr₂ => (irrefl _ hr₂).elim
     | (_, _), (_, _), .right _ hs₁,   .right _ hs₂   => antisymm hs₁ hs₂ ▸ rfl⟩
 
-instance is_total_left {r : α → α → Prop} {s : β → β → Prop} [IsTotal α r] :
+instance isTotal_left {r : α → α → Prop} {s : β → β → Prop} [IsTotal α r] :
     IsTotal (α × β) (Lex r s) :=
   ⟨fun ⟨a₁, _⟩ ⟨a₂, _⟩ => (IsTotal.total a₁ a₂).imp (Lex.left _ _) (Lex.left _ _)⟩
+#align is_total_left isTotal_left
 
-instance is_total_right {r : α → α → Prop} {s : β → β → Prop} [IsTrichotomous α r] [IsTotal β s] :
+instance isTotal_right {r : α → α → Prop} {s : β → β → Prop} [IsTrichotomous α r] [IsTotal β s] :
     IsTotal (α × β) (Lex r s) :=
   ⟨fun ⟨i, a⟩ ⟨j, b⟩ => by
     obtain hij | rfl | hji := trichotomous_of r i j
     · exact Or.inl (.left _ _ hij)
     · exact (total_of s a b).imp (.right _) (.right _)
     · exact Or.inr (.left _ _ hji) ⟩
+#align is_total_right isTotal_right
 
 end Prod
 

Mathlib/Data/Quot.lean

@@ -90,9 +90,10 @@ theorem lift_mk (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a
   rfl
 #align quot.lift_beta Quot.lift_mk
 
-theorem lift_on_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
+theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
   Quot.liftOn (Quot.mk r a) f h = f a :=
   rfl
+#align quot.lift_on_mk Quot.liftOn_mk
 
 /-- Descends a function `f : α → β → γ` to quotients of `α` and `β`. -/
 -- porting note: removed `@[elab_as_elim]`, gave "unexpected resulting type γ"
@@ -116,10 +117,11 @@ protected def liftOn₂ (p : Quot r) (q : Quot s) (f : α → β → γ)
   Quot.lift₂ f hr hs p q
 
 @[simp]
-theorem lift_on₂_mk (a : α) (b : β) (f : α → β → γ) (hr : ∀ a b₁ b₂, s b₁ b₂ → f a b₁ = f a b₂)
+theorem liftOn₂_mk (a : α) (b : β) (f : α → β → γ) (hr : ∀ a b₁ b₂, s b₁ b₂ → f a b₁ = f a b₂)
     (hs : ∀ a₁ a₂ b, r a₁ a₂ → f a₁ b = f a₂ b) :
     Quot.liftOn₂ (Quot.mk r a) (Quot.mk s b) f hr hs = f a b :=
   rfl
+#align quot.lift_on₂_mk Quot.liftOn₂_mk
 
 variable {t : γ → γ → Prop}
 
@@ -284,15 +286,17 @@ theorem Quotient.lift₂_mk {α : Sort _} {β : Sort _} {γ : Sort _} [Setoid α
     Quotient.lift₂ f h (Quotient.mk _ a) (Quotient.mk _ b) = f a b :=
   rfl
 
-theorem Quotient.lift_on_mk [s : Setoid α] (f : α → β) (h : ∀ a b : α, a ≈ b → f a = f b) (x : α) :
+theorem Quotient.liftOn_mk [s : Setoid α] (f : α → β) (h : ∀ a b : α, a ≈ b → f a = f b) (x : α) :
     Quotient.liftOn (Quotient.mk s x) f h = f x :=
   rfl
+#align Quotient.lift_on_mk Quotient.liftOn_mk
 
 @[simp]
-theorem Quotient.lift_on₂_mk {α : Sort _} {β : Sort _} [Setoid α] (f : α → α → β)
+theorem Quotient.liftOn₂_mk {α : Sort _} {β : Sort _} [Setoid α] (f : α → α → β)
     (h : ∀ a₁ a₂ b₁ b₂ : α, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) (x y : α) :
     Quotient.liftOn₂ (Quotient.mk _ x) (Quotient.mk _ y) f h = f x y :=
   rfl
+#align Quotient.lift_on₂_mk Quotient.liftOn₂_mk
 
 /-- `quot.mk r` is a surjective function. -/
 theorem surjective_quot_mk (r : α → α → Prop) : Function.Surjective (Quot.mk r) :=
@@ -617,10 +621,11 @@ protected def hrecOn' {φ : Quotient s₁ → Sort _} (qa : Quotient s₁) (f :
   Quot.hrecOn qa f c
 
 @[simp]
-theorem hrec_on'_mk'' {φ : Quotient s₁ → Sort _} (f : ∀ a, φ (Quotient.mk'' a))
+theorem hrecOn'_mk'' {φ : Quotient s₁ → Sort _} (f : ∀ a, φ (Quotient.mk'' a))
     (c : ∀ a₁ a₂, a₁ ≈ a₂ → HEq (f a₁) (f a₂))
     (x : α) : (Quotient.mk'' x).hrecOn' f c = f x :=
   rfl
+#align quotient.hrec_on'_mk'' Quotient.hrecOn'_mk''
 
 /-- Recursion on two `Quotient` arguments `a` and `b`, result type depends on `⟦a⟧` and `⟦b⟧`. -/
 protected def hrecOn₂' {φ : Quotient s₁ → Quotient s₂ → Sort _} (qa : Quotient s₁)
@@ -630,11 +635,12 @@ protected def hrecOn₂' {φ : Quotient s₁ → Quotient s₂ → Sort _} (qa :
   Quotient.hrecOn₂ qa qb f c
 
 @[simp]
-theorem hrec_on₂'_mk'' {φ : Quotient s₁ → Quotient s₂ → Sort _}
+theorem hrecOn₂'_mk'' {φ : Quotient s₁ → Quotient s₂ → Sort _}
     (f : ∀ a b, φ (Quotient.mk'' a) (Quotient.mk'' b))
     (c : ∀ a₁ b₁ a₂ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → HEq (f a₁ b₁) (f a₂ b₂)) (x : α) (qb : Quotient s₂) :
     (Quotient.mk'' x).hrecOn₂' qb f c = qb.hrecOn' (f x) fun _ _ => c _ _ _ _ (Setoid.refl _) :=
   rfl
+#align quotient.hrec_on₂'_mk'' Quotient.hrecOn₂'_mk''
 
 /-- Map a function `f : α → β` that sends equivalent elements to equivalent elements
 to a function `quotient sa → quotient sb`. Useful to define unary operations on quotients. -/
@@ -688,13 +694,15 @@ protected theorem mk''_eq_mk (x : α) : Quotient.mk'' x = Quotient.mk s x :=
   rfl
 
 @[simp]
-protected theorem lift_on'_mk (x : α) (f : α → β) (h) : (Quotient.mk s x).liftOn' f h = f x :=
+protected theorem liftOn'_mk (x : α) (f : α → β) (h) : (Quotient.mk s x).liftOn' f h = f x :=
   rfl
+#align quotient.lift_on'_mk Quotient.liftOn'_mk
 
 @[simp]
-protected theorem lift_on₂'_mk [t : Setoid β] (f : α → β → γ) (h) (a : α) (b : β) :
+protected theorem liftOn₂'_mk [t : Setoid β] (f : α → β → γ) (h) (a : α) (b : β) :
     Quotient.liftOn₂' (Quotient.mk s a) (Quotient.mk t b) f h = f a b :=
   Quotient.liftOn₂'_mk'' _ _ _ _
+#align quotient.lift_on₂'_mk Quotient.liftOn₂'_mk
 
 @[simp]
 theorem map'_mk [t : Setoid β] (f : α → β) (h) (x : α) :

Mathlib/Data/Sigma/Basic.lean

@@ -144,20 +144,24 @@ def Prod.toSigma {α β} (p : α × β) : Σ_ : α, β :=
   ⟨p.1, p.2⟩
 
 @[simp]
-theorem Prod.fst_comp_to_sigma {α β} : Sigma.fst ∘ @Prod.toSigma α β = Prod.fst :=
+theorem Prod.fst_comp_toSigma {α β} : Sigma.fst ∘ @Prod.toSigma α β = Prod.fst :=
   rfl
+#align prod.fst_comp_to_sigma Prod.fst_comp_toSigma
 
 @[simp]
-theorem Prod.fst_to_sigma {α β} (x : α × β) : (Prod.toSigma x).fst = x.fst :=
+theorem Prod.fst_toSigma {α β} (x : α × β) : (Prod.toSigma x).fst = x.fst :=
   rfl
+#align prod.fst_to_sigma Prod.fst_toSigma
 
 @[simp]
-theorem Prod.snd_to_sigma {α β} (x : α × β) : (Prod.toSigma x).snd = x.snd :=
+theorem Prod.snd_toSigma {α β} (x : α × β) : (Prod.toSigma x).snd = x.snd :=
   rfl
+#align prod.snd_to_sigma Prod.snd_toSigma
 
 @[simp]
-theorem Prod.to_sigma_mk {α β} (x : α) (y : β) : (x, y).toSigma = ⟨x, y⟩ :=
+theorem Prod.toSigma_mk {α β} (x : α) (y : β) : (x, y).toSigma = ⟨x, y⟩ :=
   rfl
+#align prod.to_sigma_mk Prod.toSigma_mk
 
 -- Porting note: the meta instance `has_reflect (Σa, β a)` was removed here.