chore: remove 'Ported by' headers (#6018)

Briefly during the port we were adding "Ported by" headers, but only ~60 / 3000 files ended up with such a header. I propose deleting them. We could consider adding these uniformly via a script, as part of the great history rewrite...? Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Jul 24, 2023 · e8318a8 · e8318a8
1 parent 549500f
commit e8318a8
Show file tree

Hide file tree

Showing 66 changed files with 0 additions and 66 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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