chore: Remove Init.CCLemmas (#10696)

Those lemmas were weird and unused, except the last few about transitivity of `=` and `≠`, which I moved to `Logic.Basic`

Author: YaelDillies

Mathlib.lean

@@ -2364,7 +2364,6 @@ import Mathlib.GroupTheory.Transfer
 import Mathlib.InformationTheory.Hamming
 import Mathlib.Init.Algebra.Classes
 import Mathlib.Init.Align
-import Mathlib.Init.CCLemmas
 import Mathlib.Init.Classes.Order
 import Mathlib.Init.Classical
 import Mathlib.Init.Control.Combinators

Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

@@ -3,7 +3,6 @@ Copyright (c) 2020 Kevin Kappelmann. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 -/
-import Mathlib.Init.CCLemmas
 import Mathlib.Algebra.ContinuedFractions.Computation.Basic
 import Mathlib.Algebra.ContinuedFractions.Translations
 

Mathlib/Algebra/Group/Pi/Lemmas.lean

@@ -3,7 +3,6 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
-import Mathlib.Init.CCLemmas
 import Mathlib.Algebra.Group.Hom.Instances
 import Mathlib.Data.Set.Function
 import Mathlib.Logic.Pairwise

Mathlib/Algebra/Ring/Equiv.lean

@@ -3,7 +3,6 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 -/
-import Mathlib.Init.CCLemmas
 import Mathlib.Algebra.Field.IsField
 import Mathlib.Algebra.Group.Equiv.Basic
 import Mathlib.Algebra.Group.Opposite

Mathlib/Data/Finset/Card.lean

@@ -3,7 +3,6 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad
 -/
-import Mathlib.Init.CCLemmas
 import Mathlib.Data.Finset.Image
 
 #align_import data.finset.card from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"

Mathlib/Data/List/BigOperators/Lemmas.lean

@@ -3,17 +3,16 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
-import Mathlib.Init.CCLemmas
-import Mathlib.Data.List.BigOperators.Basic
 import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.Order.Monoid.OrderDual
 import Mathlib.Algebra.Ring.Basic
-import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Algebra.Ring.Commute
+import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Data.Int.Units
+import Mathlib.Data.List.BigOperators.Basic
 
 #align_import data.list.big_operators.lemmas from "leanprover-community/mathlib"@"f694c7dead66f5d4c80f446c796a5aad14707f0e"
 

Mathlib/Init/CCLemmas.lean

@@ -529,6 +529,14 @@ theorem ball_mem_comm {α β} [Membership α β] {s : β} {p : α → α → Pro
 
 #align ne_of_apply_ne ne_of_apply_ne
 
+lemma ne_of_eq_of_ne (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c := h₁.symm ▸ h₂
+lemma ne_of_ne_of_eq (h₁ : a ≠ b) (h₂ : b = c) : a ≠ c := h₂ ▸ h₁
+
+alias Eq.trans_ne := ne_of_eq_of_ne
+alias Ne.trans_eq := ne_of_ne_of_eq
+#align eq.trans_ne Eq.trans_ne
+#align ne.trans_eq Ne.trans_eq
+
 theorem eq_equivalence : Equivalence (@Eq α) :=
   ⟨Eq.refl, @Eq.symm _, @Eq.trans _⟩
 #align eq_equivalence eq_equivalence