diff --git a/Mathlib/Algebra/Divisibility/Basic.lean b/Mathlib/Algebra/Divisibility/Basic.lean
index 3003715b06b6a..3467c6fc22240 100644
--- a/Mathlib/Algebra/Divisibility/Basic.lean
+++ b/Mathlib/Algebra/Divisibility/Basic.lean
@@ -3,7 +3,6 @@ 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, Floris van Doorn, Amelia Livingston, Yury Kudryashov,
 Neil Strickland, Aaron Anderson
-Ported by: Matej Penciak
 -/
 import Mathlib.Algebra.Hom.Group
 
diff --git a/Mathlib/Algebra/Divisibility/Units.lean b/Mathlib/Algebra/Divisibility/Units.lean
index aedfeac8e69b3..11f0d52c83bcf 100644
--- a/Mathlib/Algebra/Divisibility/Units.lean
+++ b/Mathlib/Algebra/Divisibility/Units.lean
@@ -3,7 +3,6 @@ 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, Floris van Doorn, Amelia Livingston, Yury Kudryashov,
 Neil Strickland, Aaron Anderson
-Ported by: Joël Riou
 -/
 import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Group.Units
diff --git a/Mathlib/Algebra/GroupPower/Ring.lean b/Mathlib/Algebra/GroupPower/Ring.lean
index b7045145b8843..3294de249a10e 100644
--- a/Mathlib/Algebra/GroupPower/Ring.lean
+++ b/Mathlib/Algebra/GroupPower/Ring.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
-Ported by: Joël Riou
 -/
 
 import Mathlib.Algebra.GroupPower.Basic
diff --git a/Mathlib/Algebra/Hom/Commute.lean b/Mathlib/Algebra/Hom/Commute.lean
index 3bb68ff1a9bee..3d309e11a5df6 100644
--- a/Mathlib/Algebra/Hom/Commute.lean
+++ b/Mathlib/Algebra/Hom/Commute.lean
@@ -3,7 +3,6 @@ Copyright (c) 2018 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Kevin Buzzard, Scott Morrison, Johan Commelin, Chris Hughes,
   Johannes Hölzl, Yury Kudryashov
-Ported by: Frédéric Dupuis
 -/
 import Mathlib.Algebra.Hom.Group
 import Mathlib.Algebra.Group.Commute
diff --git a/Mathlib/Algebra/Hom/Equiv/Basic.lean b/Mathlib/Algebra/Hom/Equiv/Basic.lean
index 912acd9b7e9c5..000aaed876d5f 100644
--- a/Mathlib/Algebra/Hom/Equiv/Basic.lean
+++ b/Mathlib/Algebra/Hom/Equiv/Basic.lean
@@ -2,7 +2,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
-Ported by: Winston Yin
 -/
 import Mathlib.Algebra.Hom.Group
 import Mathlib.Data.FunLike.Equiv
diff --git a/Mathlib/Algebra/Hom/Equiv/TypeTags.lean b/Mathlib/Algebra/Hom/Equiv/TypeTags.lean
index 9b8d5f7298b63..75c0beb2be8db 100644
--- a/Mathlib/Algebra/Hom/Equiv/TypeTags.lean
+++ b/Mathlib/Algebra/Hom/Equiv/TypeTags.lean
@@ -2,7 +2,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
-Ported by: Frédéric Dupuis
 -/
 import Mathlib.Algebra.Hom.Equiv.Basic
 import Mathlib.Algebra.Group.TypeTags
diff --git a/Mathlib/Algebra/Hom/Equiv/Units/Basic.lean b/Mathlib/Algebra/Hom/Equiv/Units/Basic.lean
index 0bdc555cecd98..9c8b91ebc1ead 100644
--- a/Mathlib/Algebra/Hom/Equiv/Units/Basic.lean
+++ b/Mathlib/Algebra/Hom/Equiv/Units/Basic.lean
@@ -2,7 +2,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
-Ported by: Scott Morrison
 -/
 import Mathlib.Algebra.Hom.Equiv.Basic
 import Mathlib.Algebra.Hom.Units
diff --git a/Mathlib/Algebra/Hom/Group.lean b/Mathlib/Algebra/Hom/Group.lean
index db69f51796461..78304deb72c21 100644
--- a/Mathlib/Algebra/Hom/Group.lean
+++ b/Mathlib/Algebra/Hom/Group.lean
@@ -3,7 +3,6 @@ Copyright (c) 2018 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Kevin Buzzard, Scott Morrison, Johan Commelin, Chris Hughes,
   Johannes Hölzl, Yury Kudryashov
-Ported by: Winston Yin
 -/
 import Mathlib.Init.CCLemmas
 import Mathlib.Algebra.NeZero
diff --git a/Mathlib/Algebra/Hom/Ring.lean b/Mathlib/Algebra/Hom/Ring.lean
index e6945aadf9b32..6d4e0d0fcec98 100644
--- a/Mathlib/Algebra/Hom/Ring.lean
+++ b/Mathlib/Algebra/Hom/Ring.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2019 Amelia Livingston. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Amelia Livingston, Jireh Loreaux
-Ported by: Winston Yin
 -/
 import Mathlib.Algebra.GroupWithZero.InjSurj
 import Mathlib.Algebra.Ring.Basic
diff --git a/Mathlib/Algebra/Hom/Units.lean b/Mathlib/Algebra/Hom/Units.lean
index 842511923300d..d9389cf968d11 100644
--- a/Mathlib/Algebra/Hom/Units.lean
+++ b/Mathlib/Algebra/Hom/Units.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2018 Johan Commelin All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Chris Hughes, Kevin Buzzard
-Ported by: Winston Yin
 -/
 import Mathlib.Algebra.Hom.Group
 import Mathlib.Algebra.Group.Units
diff --git a/Mathlib/Algebra/Order/Field/Canonical/Defs.lean b/Mathlib/Algebra/Order/Field/Canonical/Defs.lean
index 3fc0c8be6bb0c..621a7e2e48122 100644
--- a/Mathlib/Algebra/Order/Field/Canonical/Defs.lean
+++ b/Mathlib/Algebra/Order/Field/Canonical/Defs.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
-Ported by: Rémy Degenne
 -/
 import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.Order.Ring.Canonical
diff --git a/Mathlib/Algebra/Order/Field/Defs.lean b/Mathlib/Algebra/Order/Field/Defs.lean
index b557d38e9de78..d928933c28547 100644
--- a/Mathlib/Algebra/Order/Field/Defs.lean
+++ b/Mathlib/Algebra/Order/Field/Defs.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Mario Carneiro, Floris van Doorn
-Ported by: Scott Morrison
 -/
 import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.Order.Ring.Defs
diff --git a/Mathlib/Algebra/Order/Group/OrderIso.lean b/Mathlib/Algebra/Order/Group/OrderIso.lean
index 202c9a9c4a484..317978217cad5 100644
--- a/Mathlib/Algebra/Order/Group/OrderIso.lean
+++ b/Mathlib/Algebra/Order/Group/OrderIso.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
-Ported by: Scott Morrison
 -/
 import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Hom.Equiv.Units.Basic
diff --git a/Mathlib/Algebra/Order/Hom/Monoid.lean b/Mathlib/Algebra/Order/Hom/Monoid.lean
index c94629b633931..2a3d9caee0569 100644
--- a/Mathlib/Algebra/Order/Hom/Monoid.lean
+++ b/Mathlib/Algebra/Order/Hom/Monoid.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
-Ported by: Frédéric Dupuis
 -/
 import Mathlib.Data.Pi.Algebra
 import Mathlib.Algebra.Hom.Group
diff --git a/Mathlib/Algebra/Order/Monoid/Prod.lean b/Mathlib/Algebra/Order/Monoid/Prod.lean
index 0eb2466d21724..49634a9d08025 100644
--- a/Mathlib/Algebra/Order/Monoid/Prod.lean
+++ b/Mathlib/Algebra/Order/Monoid/Prod.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
-Ported by: Joël Riou
 -/
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Order.Monoid.Cancel.Defs
diff --git a/Mathlib/Algebra/Order/Monoid/WithTop.lean b/Mathlib/Algebra/Order/Monoid/WithTop.lean
index 12b0c24e05ba0..f3d1961709c53 100644
--- a/Mathlib/Algebra/Order/Monoid/WithTop.lean
+++ b/Mathlib/Algebra/Order/Monoid/WithTop.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
-Ported by: Jon Eugster
 -/
 import Mathlib.Algebra.Hom.Group
 import Mathlib.Algebra.Order.Monoid.OrderDual
diff --git a/Mathlib/Algebra/Order/Ring/Canonical.lean b/Mathlib/Algebra/Order/Ring/Canonical.lean
index a081e238e9f7c..ae4a410de1478 100644
--- a/Mathlib/Algebra/Order/Ring/Canonical.lean
+++ b/Mathlib/Algebra/Order/Ring/Canonical.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
-Ported by: Scott Morrison
 -/
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Algebra.Order.Sub.Canonical
diff --git a/Mathlib/Algebra/Order/Ring/CharZero.lean b/Mathlib/Algebra/Order/Ring/CharZero.lean
index ff0b3f808bc93..adc07590e84e6 100644
--- a/Mathlib/Algebra/Order/Ring/CharZero.lean
+++ b/Mathlib/Algebra/Order/Ring/CharZero.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
-Ported by: Scott Morrison
 -/
 import Mathlib.Algebra.CharZero.Defs
 import Mathlib.Algebra.Order.Ring.Defs
diff --git a/Mathlib/Algebra/Order/Ring/Defs.lean b/Mathlib/Algebra/Order/Ring/Defs.lean
index 5c94ce4fe2a9c..ba0adf07198e5 100644
--- a/Mathlib/Algebra/Order/Ring/Defs.lean
+++ b/Mathlib/Algebra/Order/Ring/Defs.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Yaël Dillies
-Ported by: Scott Morrison
 -/
 import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Monoid.Cancel.Defs
diff --git a/Mathlib/Algebra/Ring/Basic.lean b/Mathlib/Algebra/Ring/Basic.lean
index 0462b08c466cb..7df28ef21a8ed 100644
--- a/Mathlib/Algebra/Ring/Basic.lean
+++ b/Mathlib/Algebra/Ring/Basic.lean
@@ -2,7 +2,6 @@
 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, Floris van Doorn, Yury Kudryashov, Neil Strickland
-Ported by: Moritz Doll
 -/
 import Mathlib.Algebra.Ring.Defs
 import Mathlib.Algebra.Hom.Group
diff --git a/Mathlib/Algebra/Ring/Divisibility.lean b/Mathlib/Algebra/Ring/Divisibility.lean
index 5b3c22994e6e2..eac4c8bcaf095 100644
--- a/Mathlib/Algebra/Ring/Divisibility.lean
+++ b/Mathlib/Algebra/Ring/Divisibility.lean
@@ -2,7 +2,6 @@
 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, Floris van Doorn, Yury Kudryashov, Neil Strickland
-Ported by: Matej Penciak
 -/
 import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Hom.Equiv.Basic
diff --git a/Mathlib/Algebra/Ring/Equiv.lean b/Mathlib/Algebra/Ring/Equiv.lean
index deda88c04b984..5c2d669e7b66f 100644
--- a/Mathlib/Algebra/Ring/Equiv.lean
+++ b/Mathlib/Algebra/Ring/Equiv.lean
@@ -2,7 +2,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
-Ported by: Anatole Dedecker
 -/
 import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.Hom.Ring
diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
index 870f1226d5ae8..37a4e12c80dfc 100644
--- a/Mathlib/CategoryTheory/Category/Basic.lean
+++ b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl, Reid Barton
-Ported by: Scott Morrison
 -/
 import Mathlib.CategoryTheory.Category.Init
 import Mathlib.Combinatorics.Quiver.Basic
diff --git a/Mathlib/CategoryTheory/EssentialImage.lean b/Mathlib/CategoryTheory/EssentialImage.lean
index 5443758a14899..6323941535ef5 100644
--- a/Mathlib/CategoryTheory/EssentialImage.lean
+++ b/Mathlib/CategoryTheory/EssentialImage.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
-Ported by: Joël Riou
 -/
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.FullSubcategory
diff --git a/Mathlib/CategoryTheory/Functor/Basic.lean b/Mathlib/CategoryTheory/Functor/Basic.lean
index 7de322cc42d10..087d903acce75 100644
--- a/Mathlib/CategoryTheory/Functor/Basic.lean
+++ b/Mathlib/CategoryTheory/Functor/Basic.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tim Baumann, Stephen Morgan, Scott Morrison
-Ported by: Scott Morrison
 -/
 import Mathlib.CategoryTheory.Category.Basic
 
diff --git a/Mathlib/CategoryTheory/Iso.lean b/Mathlib/CategoryTheory/Iso.lean
index 2f9972bb0b814..2edcf7b046a7b 100644
--- a/Mathlib/CategoryTheory/Iso.lean
+++ b/Mathlib/CategoryTheory/Iso.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
-Ported by: Scott Morrison
 -/
 import Mathlib.Tactic.CategoryTheory.Reassoc
 
diff --git a/Mathlib/CategoryTheory/NatTrans.lean b/Mathlib/CategoryTheory/NatTrans.lean
index f13bc49a9acab..83150c6de066c 100644
--- a/Mathlib/CategoryTheory/NatTrans.lean
+++ b/Mathlib/CategoryTheory/NatTrans.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
-Ported by: Scott Morrison
 -/
 import Mathlib.Tactic.CategoryTheory.Reassoc
 
diff --git a/Mathlib/CategoryTheory/Whiskering.lean b/Mathlib/CategoryTheory/Whiskering.lean
index 31e3fddb090c3..1a9a8b0ad2966 100644
--- a/Mathlib/CategoryTheory/Whiskering.lean
+++ b/Mathlib/CategoryTheory/Whiskering.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2018 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
-Ported by: Joël Riou
 -/
 import Mathlib.CategoryTheory.Iso
 import Mathlib.CategoryTheory.Functor.Category
diff --git a/Mathlib/Combinatorics/Quiver/Basic.lean b/Mathlib/Combinatorics/Quiver/Basic.lean
index 766b91801449c..85e50efbe59a1 100644
--- a/Mathlib/Combinatorics/Quiver/Basic.lean
+++ b/Mathlib/Combinatorics/Quiver/Basic.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2021 David Wärn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Wärn, Scott Morrison
-Ported by: Scott Morrison
 -/
 import Mathlib.Data.Opposite
 
diff --git a/Mathlib/Combinatorics/Quiver/ConnectedComponent.lean b/Mathlib/Combinatorics/Quiver/ConnectedComponent.lean
index e44b2bcadad4e..1a305382fa416 100644
--- a/Mathlib/Combinatorics/Quiver/ConnectedComponent.lean
+++ b/Mathlib/Combinatorics/Quiver/ConnectedComponent.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2021 David Wärn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Wärn
-Ported by: Joël Riou
 -/
 import Mathlib.Combinatorics.Quiver.Subquiver
 import Mathlib.Combinatorics.Quiver.Path
diff --git a/Mathlib/Combinatorics/Quiver/Path.lean b/Mathlib/Combinatorics/Quiver/Path.lean
index b24c46c575a08..59bfcffeeb631 100644
--- a/Mathlib/Combinatorics/Quiver/Path.lean
+++ b/Mathlib/Combinatorics/Quiver/Path.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2021 David Wärn,. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Wärn, Scott Morrison
-Ported by: Joël Riou
 -/
 import Mathlib.Combinatorics.Quiver.Basic
 import Mathlib.Logic.Lemmas
diff --git a/Mathlib/Combinatorics/Quiver/Subquiver.lean b/Mathlib/Combinatorics/Quiver/Subquiver.lean
index 47749420733af..6e68aeb886986 100644
--- a/Mathlib/Combinatorics/Quiver/Subquiver.lean
+++ b/Mathlib/Combinatorics/Quiver/Subquiver.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2021 David Wärn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Wärn
-Ported by: Joël Riou
 -/
 import Mathlib.Order.BoundedOrder
 import Mathlib.Combinatorics.Quiver.Basic
diff --git a/Mathlib/Combinatorics/Quiver/Symmetric.lean b/Mathlib/Combinatorics/Quiver/Symmetric.lean
index f8a06fad64de5..58a4ccb8c348e 100644
--- a/Mathlib/Combinatorics/Quiver/Symmetric.lean
+++ b/Mathlib/Combinatorics/Quiver/Symmetric.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2021 David Wärn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Wärn, Antoine Labelle, Rémi Bottinelli
-Ported by: Joël Riou, Rémi Bottinelli
 -/
 import Mathlib.Combinatorics.Quiver.Path
 import Mathlib.Combinatorics.Quiver.Push
diff --git a/Mathlib/Data/Int/Cast/Lemmas.lean b/Mathlib/Data/Int/Cast/Lemmas.lean
index 14c62c2d17277..9ff2f8c042d0e 100644
--- a/Mathlib/Data/Int/Cast/Lemmas.lean
+++ b/Mathlib/Data/Int/Cast/Lemmas.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
-Ported by: Scott Morrison
 -/
 import Mathlib.Data.Int.Order.Basic
 import Mathlib.Data.Nat.Cast.Basic
diff --git a/Mathlib/Data/Int/Dvd/Basic.lean b/Mathlib/Data/Int/Dvd/Basic.lean
index 898b353bdd578..9677d3cf28eb2 100644
--- a/Mathlib/Data/Int/Dvd/Basic.lean
+++ b/Mathlib/Data/Int/Dvd/Basic.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
-Ported by: Scott Morrison
 -/
 import Mathlib.Data.Int.Order.Basic
 import Mathlib.Data.Nat.Cast.Basic
diff --git a/Mathlib/Data/Int/Order/Lemmas.lean b/Mathlib/Data/Int/Order/Lemmas.lean
index 77fc59a408f6f..a59129f08d9da 100644
--- a/Mathlib/Data/Int/Order/Lemmas.lean
+++ b/Mathlib/Data/Int/Order/Lemmas.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
-Ported by: Matej Penciak
 -/
 import Mathlib.Data.Int.Order.Basic
 import Mathlib.Algebra.GroupWithZero.Divisibility
diff --git a/Mathlib/Data/Nat/Choose/Central.lean b/Mathlib/Data/Nat/Choose/Central.lean
index 81169681c4ced..7b2bb2653d13e 100644
--- a/Mathlib/Data/Nat/Choose/Central.lean
+++ b/Mathlib/Data/Nat/Choose/Central.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2021 Patrick Stevens. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Stevens, Thomas Browning
-Ported by: Frédéric Dupuis
 -/
 import Mathlib.Data.Nat.Choose.Basic
 import Mathlib.Tactic.Linarith
diff --git a/Mathlib/Data/Nat/ForSqrt.lean b/Mathlib/Data/Nat/ForSqrt.lean
index 51c3cc67b65be..e9ba76e212e87 100644
--- a/Mathlib/Data/Nat/ForSqrt.lean
+++ b/Mathlib/Data/Nat/ForSqrt.lean
@@ -2,7 +2,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, Johannes Hölzl, Mario Carneiro
-Ported by: Kevin Buzzard, Johan Commelin, Siddhartha Gadgil, Anand Rao
 -/
 
 import Mathlib.Data.Nat.Size
diff --git a/Mathlib/Data/Nat/Log.lean b/Mathlib/Data/Nat/Log.lean
index bba440126bc86..d55ac8d3c9164 100644
--- a/Mathlib/Data/Nat/Log.lean
+++ b/Mathlib/Data/Nat/Log.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2020 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Yaël Dillies
-Ported by: Rémy Degenne
 -/
 import Mathlib.Data.Nat.Pow
 
diff --git a/Mathlib/Data/Pi/Algebra.lean b/Mathlib/Data/Pi/Algebra.lean
index ad841519fbcdd..4da8c107cdce1 100644
--- a/Mathlib/Data/Pi/Algebra.lean
+++ b/Mathlib/Data/Pi/Algebra.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2020 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Eric Wieser
-Ported by: Jon Eugster
 -/
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Data.Prod.Basic
diff --git a/Mathlib/Data/Set/Accumulate.lean b/Mathlib/Data/Set/Accumulate.lean
index c49b2e72c82ba..9dba9561cc8e0 100644
--- a/Mathlib/Data/Set/Accumulate.lean
+++ b/Mathlib/Data/Set/Accumulate.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
-Ported by: Anatole Dedecker
 -/
 import Mathlib.Data.Set.Lattice
 
diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean
index 27f75b426c8d6..4a99058b6e8db 100644
--- a/Mathlib/Data/Set/Image.lean
+++ b/Mathlib/Data/Set/Image.lean
@@ -2,7 +2,6 @@
 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
-Ported by: Winston Yin
 -/
 import Mathlib.Data.Set.Basic
 
diff --git a/Mathlib/Data/Set/Intervals/Basic.lean b/Mathlib/Data/Set/Intervals/Basic.lean
index d1174233f3054..a0e31e0b8f481 100644
--- a/Mathlib/Data/Set/Intervals/Basic.lean
+++ b/Mathlib/Data/Set/Intervals/Basic.lean
@@ -2,7 +2,6 @@
 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, Mario Carneiro, Patrick Massot, Yury Kudryashov, Rémy Degenne
-Ported by: Winston Yin, Arien Malec
 -/
 import Mathlib.Order.MinMax
 import Mathlib.Data.Set.Prod
diff --git a/Mathlib/Data/Set/Intervals/Group.lean b/Mathlib/Data/Set/Intervals/Group.lean
index dcad3ac77252a..1d16fa10f57a4 100644
--- a/Mathlib/Data/Set/Intervals/Group.lean
+++ b/Mathlib/Data/Set/Intervals/Group.lean
@@ -2,7 +2,6 @@
 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, Mario Carneiro, Patrick Massot, Yury Kudryashov, Rémy Degenne
-Ported by: Winston Yin
 -/
 import Mathlib.Data.Set.Intervals.Basic
 import Mathlib.Data.Set.Pairwise.Basic
diff --git a/Mathlib/Data/Set/Intervals/SurjOn.lean b/Mathlib/Data/Set/Intervals/SurjOn.lean
index fdfc1f6034589..43f6003ff5664 100644
--- a/Mathlib/Data/Set/Intervals/SurjOn.lean
+++ b/Mathlib/Data/Set/Intervals/SurjOn.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2020 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
-Ported by: Joël Riou
 -/
 import Mathlib.Data.Set.Intervals.Basic
 import Mathlib.Data.Set.Function
diff --git a/Mathlib/Data/Set/Opposite.lean b/Mathlib/Data/Set/Opposite.lean
index bff96804d562d..02795c2be2d0f 100644
--- a/Mathlib/Data/Set/Opposite.lean
+++ b/Mathlib/Data/Set/Opposite.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2022 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
-Ported by: Joël Riou
 -/
 import Mathlib.Data.Opposite
 import Mathlib.Data.Set.Image
diff --git a/Mathlib/Data/TwoPointing.lean b/Mathlib/Data/TwoPointing.lean
index 02b288a185d0b..de2c0206c5d4f 100644
--- a/Mathlib/Data/TwoPointing.lean
+++ b/Mathlib/Data/TwoPointing.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
-Ported by: Joël Riou
 -/
 import Mathlib.Data.Sum.Basic
 import Mathlib.Logic.Nontrivial
diff --git a/Mathlib/GroupTheory/Submonoid/Basic.lean b/Mathlib/GroupTheory/Submonoid/Basic.lean
index d46a518d1a569..b6d6b388c007f 100644
--- a/Mathlib/GroupTheory/Submonoid/Basic.lean
+++ b/Mathlib/GroupTheory/Submonoid/Basic.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, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzzard,
 Amelia Livingston, Yury Kudryashov
-Ported by: Anatole Dedecker
 -/
 import Mathlib.Algebra.Hom.Group
 import Mathlib.Algebra.Group.Units
diff --git a/Mathlib/Init/Data/Sigma/Basic.lean b/Mathlib/Init/Data/Sigma/Basic.lean
index c639f2a4960db..22228b8fb1d71 100644
--- a/Mathlib/Init/Data/Sigma/Basic.lean
+++ b/Mathlib/Init/Data/Sigma/Basic.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
-Ported by: Scott Morrison
 -/
 import Mathlib.Init.Logic
 
diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean
index 51bb00aeeeb98..62f20696ed2ab 100644
--- a/Mathlib/Logic/Equiv/Basic.lean
+++ b/Mathlib/Logic/Equiv/Basic.lean
@@ -2,7 +2,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, Mario Carneiro
-Ported by: Kevin Buzzard, Ruben Vorster, Scott Morrison, Eric Rodriguez
 -/
 import Mathlib.Data.Bool.Basic
 import Mathlib.Data.Prod.Basic
diff --git a/Mathlib/Logic/Equiv/Nat.lean b/Mathlib/Logic/Equiv/Nat.lean
index e8c5f402d5b25..a1d46634e9c78 100644
--- a/Mathlib/Logic/Equiv/Nat.lean
+++ b/Mathlib/Logic/Equiv/Nat.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
-Ported by: Anatole Dedecker
 -/
 import Mathlib.Data.Nat.Pairing
 
diff --git a/Mathlib/Order/Chain.lean b/Mathlib/Order/Chain.lean
index 368ef6da61481..607a9852709b9 100644
--- a/Mathlib/Order/Chain.lean
+++ b/Mathlib/Order/Chain.lean
@@ -2,7 +2,6 @@
 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
-Ported by: Anatole Dedecker
 -/
 import Mathlib.Data.Set.Pairwise.Basic
 import Mathlib.Data.Set.Lattice
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Group.lean b/Mathlib/Order/ConditionallyCompleteLattice/Group.lean
index d9ef00206f308..b21434644d96f 100644
--- a/Mathlib/Order/ConditionallyCompleteLattice/Group.lean
+++ b/Mathlib/Order/ConditionallyCompleteLattice/Group.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2018 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
-Ported by: Anatole Dedecker
 -/
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Algebra.Order.Group.TypeTags
diff --git a/Mathlib/Order/SymmDiff.lean b/Mathlib/Order/SymmDiff.lean
index f47a7b62862e0..99b8a56c199a5 100644
--- a/Mathlib/Order/SymmDiff.lean
+++ b/Mathlib/Order/SymmDiff.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2021 Bryan Gin-ge Chen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Topaz, Bryan Gin-ge Chen, Yaël Dillies
-Ported by: Frédéric Dupuis
 -/
 import Mathlib.Order.BooleanAlgebra
 import Mathlib.Logic.Equiv.Basic
diff --git a/Mathlib/Tactic/Lift.lean b/Mathlib/Tactic/Lift.lean
index 254d031e2a420..812739557c9a3 100644
--- a/Mathlib/Tactic/Lift.lean
+++ b/Mathlib/Tactic/Lift.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2019 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
-Ported by: Yury Kudryashov, Frédéric Dupuis
 -/
 import Mathlib.Tactic.Cases
 import Mathlib.Tactic.PermuteGoals
diff --git a/Mathlib/Tactic/Linarith/Datatypes.lean b/Mathlib/Tactic/Linarith/Datatypes.lean
index d4972d69d9de2..9beff35eebc0c 100644
--- a/Mathlib/Tactic/Linarith/Datatypes.lean
+++ b/Mathlib/Tactic/Linarith/Datatypes.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2020 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
-Ported by: Scott Morrison
 -/
 import Mathlib.Tactic.Linarith.Lemmas
 import Mathlib.Tactic.Ring
diff --git a/Mathlib/Tactic/Linarith/Elimination.lean b/Mathlib/Tactic/Linarith/Elimination.lean
index fc1b57b7694c2..c6a6104ce33fb 100644
--- a/Mathlib/Tactic/Linarith/Elimination.lean
+++ b/Mathlib/Tactic/Linarith/Elimination.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2020 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
-Ported by: Scott Morrison
 -/
 import Mathlib.Tactic.Linarith.Datatypes
 
diff --git a/Mathlib/Tactic/Linarith/Frontend.lean b/Mathlib/Tactic/Linarith/Frontend.lean
index 9ec111cda6353..572c435c6d924 100644
--- a/Mathlib/Tactic/Linarith/Frontend.lean
+++ b/Mathlib/Tactic/Linarith/Frontend.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
-Ported by: Scott Morrison
 -/
 import Mathlib.Control.Basic
 import Mathlib.Data.HashMap
diff --git a/Mathlib/Tactic/Linarith/Lemmas.lean b/Mathlib/Tactic/Linarith/Lemmas.lean
index d0d5e81f6fe87..58a07f3f1a6f2 100644
--- a/Mathlib/Tactic/Linarith/Lemmas.lean
+++ b/Mathlib/Tactic/Linarith/Lemmas.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2020 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
-Ported by: Scott Morrison
 -/
 import Std.Tactic.Simpa
 import Std.Tactic.Lint.Basic
diff --git a/Mathlib/Tactic/Linarith/Parsing.lean b/Mathlib/Tactic/Linarith/Parsing.lean
index cff32c1c5f7c6..6cc6488de1b86 100644
--- a/Mathlib/Tactic/Linarith/Parsing.lean
+++ b/Mathlib/Tactic/Linarith/Parsing.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2020 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
-Ported by: Scott Morrison
 -/
 
 import Std.Data.RBMap.Basic
diff --git a/Mathlib/Tactic/Linarith/Preprocessing.lean b/Mathlib/Tactic/Linarith/Preprocessing.lean
index 69c7c63de6586..a4b3a051aacc1 100644
--- a/Mathlib/Tactic/Linarith/Preprocessing.lean
+++ b/Mathlib/Tactic/Linarith/Preprocessing.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2020 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
-Ported by: Scott Morrison
 -/
 import Mathlib.Tactic.Linarith.Datatypes
 import Mathlib.Tactic.Zify
diff --git a/Mathlib/Tactic/Linarith/Verification.lean b/Mathlib/Tactic/Linarith/Verification.lean
index 9a851564a5aa7..b6f9863763d82 100644
--- a/Mathlib/Tactic/Linarith/Verification.lean
+++ b/Mathlib/Tactic/Linarith/Verification.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2020 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
-Ported by: Scott Morrison
 -/
 
 import Mathlib.Tactic.Linarith.Elimination
diff --git a/Mathlib/Tactic/Monotonicity/Basic.lean b/Mathlib/Tactic/Monotonicity/Basic.lean
index 3eee1115c2930..3127d1e9fcaf0 100644
--- a/Mathlib/Tactic/Monotonicity/Basic.lean
+++ b/Mathlib/Tactic/Monotonicity/Basic.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
-Ported by: Heather Macbeth
 -/
 import Mathlib.Tactic.Monotonicity.Attr
 import Mathlib.Tactic.SolveByElim
diff --git a/Mathlib/Tactic/Monotonicity/Lemmas.lean b/Mathlib/Tactic/Monotonicity/Lemmas.lean
index fc7c7c81abc89..50d39ac7fccf1 100644
--- a/Mathlib/Tactic/Monotonicity/Lemmas.lean
+++ b/Mathlib/Tactic/Monotonicity/Lemmas.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
-Ported by: Heather Macbeth
 -/
 import Mathlib.Algebra.Order.Group.Abs
 import Mathlib.Algebra.Order.Ring.Defs
diff --git a/Mathlib/Tactic/RestateAxiom.lean b/Mathlib/Tactic/RestateAxiom.lean
index b830c1190536e..b124e8d5e7de2 100644
--- a/Mathlib/Tactic/RestateAxiom.lean
+++ b/Mathlib/Tactic/RestateAxiom.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
-Ported by: E.W.Ayers
 -/
 import Lean
 import Lean.Data
diff --git a/Mathlib/Tactic/ToAdditive.lean b/Mathlib/Tactic/ToAdditive.lean
index 1acae4191cbcf..bfbdb82c00943 100644
--- a/Mathlib/Tactic/ToAdditive.lean
+++ b/Mathlib/Tactic/ToAdditive.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Yury Kudryashov, Floris van Doorn, Jon Eugster
-Ported by: E.W.Ayers
 -/
 import Mathlib.Init.Data.Nat.Notation
 import Mathlib.Data.String.Defs