Trigger CI for leanprover/lean4#3183

.github/workflows/bors.yml

@@ -256,6 +256,11 @@ jobs:
           lake exe graph
           rm import_graph.dot
 
+      - name: verify `lake exe shake` works
+        # Later, we may want to make output from `shake` a CI error?
+        run: |
+          lake exe shake
+
       - name: test mathlib
         id: test
         run: |

.github/workflows/build.yml

@@ -263,6 +263,11 @@ jobs:
           lake exe graph
           rm import_graph.dot
 
+      - name: verify `lake exe shake` works
+        # Later, we may want to make output from `shake` a CI error?
+        run: |
+          lake exe shake
+
       - name: test mathlib
         id: test
         run: |

.github/workflows/build.yml.in

@@ -242,6 +242,11 @@ jobs:
           lake exe graph
           rm import_graph.dot
 
+      - name: verify `lake exe shake` works
+        # Later, we may want to make output from `shake` a CI error?
+        run: |
+          lake exe shake
+
       - name: test mathlib
         id: test
         run: |

.github/workflows/build_fork.yml

@@ -260,6 +260,11 @@ jobs:
           lake exe graph
           rm import_graph.dot
 
+      - name: verify `lake exe shake` works
+        # Later, we may want to make output from `shake` a CI error?
+        run: |
+          lake exe shake
+
       - name: test mathlib
         id: test
         run: |

Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -6,6 +6,7 @@ Authors: Kevin Kappelmann
 import Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
 import Mathlib.Data.Nat.Fib.Basic
 import Mathlib.Tactic.Monotonicity
+import Mathlib.Algebra.GroupPower.Order
 import Std.Tactic.SolveByElim
 
 #align_import algebra.continued_fractions.computation.approximations from "leanprover-community/mathlib"@"a7e36e48519ab281320c4d192da6a7b348ce40ad"

Mathlib/Algebra/Group/Defs.lean

@@ -7,6 +7,7 @@ import Mathlib.Init.ZeroOne
 import Mathlib.Init.Data.Int.Basic
 import Mathlib.Logic.Function.Basic
 import Mathlib.Tactic.Basic
+import Mathlib.Init.ZeroOne
 
 #align_import algebra.group.defs from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
 

Mathlib/Algebra/Order/Field/Pi.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Order.Field.Basic
-import Mathlib.Data.Fintype.Lattice
+import Mathlib.Data.Finset.Lattice
+import Mathlib.Data.Fintype.Card
 
 #align_import algebra.order.field.pi from "leanprover-community/mathlib"@"509de852e1de55e1efa8eacfa11df0823f26f226"
 

Mathlib/Algebra/Order/Floor.lean

@@ -12,6 +12,7 @@ import Mathlib.Init.Meta.WellFoundedTactics
 import Mathlib.Tactic.Abel
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Positivity
+import Mathlib.Init.Data.Nat.Lemmas
 
 #align_import algebra.order.floor from "leanprover-community/mathlib"@"afdb43429311b885a7988ea15d0bac2aac80f69c"
 

Mathlib/Algebra/Order/Sub/Prod.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Mathlib.Algebra.Group.Prod
-import Mathlib.Algebra.Order.Sub.Basic
+import Mathlib.Algebra.Order.Sub.Defs
 
 /-!
 # Products of `OrderedSub` types.

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -6,6 +6,7 @@ Authors: Yury Kudryashov
 import Mathlib.Analysis.BoxIntegral.Partition.Filter
 import Mathlib.Analysis.BoxIntegral.Partition.Measure
 import Mathlib.Topology.UniformSpace.Compact
+import Mathlib.Init.Data.Bool.Lemmas
 
 #align_import analysis.box_integral.basic from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 

Mathlib/Analysis/SpecificLimits/IsROrC.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Généreux, Patrick Massot
 -/
 import Mathlib.Analysis.SpecificLimits.Basic
-import Mathlib.Analysis.Complex.ReImTopology
+import Mathlib.Data.IsROrC.Basic
 
 /-!
 # A collection of specific limit computations for `IsROrC`

Mathlib/CategoryTheory/Abelian/Projective.lean

@@ -5,6 +5,7 @@ Authors: Jakob von Raumer
 -/
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
+import Mathlib.Algebra.Category.ModuleCat.EpiMono
 
 /-!
 # Projective objects in abelian categories

Mathlib/CategoryTheory/Preadditive/Yoneda/Projective.lean

@@ -6,7 +6,6 @@ Authors: Markus Himmel, Scott Morrison
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
 import Mathlib.CategoryTheory.Preadditive.Projective
 import Mathlib.Algebra.Category.GroupCat.EpiMono
-import Mathlib.Algebra.Category.ModuleCat.EpiMono
 
 #align_import category_theory.preadditive.yoneda.projective from "leanprover-community/mathlib"@"f8d8465c3c392a93b9ed226956e26dee00975946"
 

Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

@@ -7,6 +7,7 @@ import Mathlib.Combinatorics.DoubleCounting
 import Mathlib.Data.Finset.Pointwise
 import Mathlib.Data.Rat.NNRat
 import Mathlib.Tactic.GCongr
+import Mathlib.Algebra.GroupPower.Order
 
 #align_import combinatorics.additive.pluennecke_ruzsa from "leanprover-community/mathlib"@"4aab2abced69a9e579b1e6dc2856ed3db48e2cbd"
 

Mathlib/Computability/Ackermann.lean

@@ -6,6 +6,7 @@ Authors: Violeta Hernández Palacios
 import Mathlib.Computability.Primrec
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Linarith
+import Mathlib.Algebra.GroupPower.Order
 
 #align_import computability.ackermann from "leanprover-community/mathlib"@"9b2660e1b25419042c8da10bf411aa3c67f14383"
 

Mathlib/Control/Monad/Basic.lean

@@ -3,9 +3,7 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
-import Mathlib.Init.Control.Lawful
 import Mathlib.Logic.Equiv.Defs
-import Mathlib.Tactic.Common
 
 #align_import control.monad.basic from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"
 
@@ -40,7 +38,7 @@ functor, applicative, monad, simp
 
 set_option autoImplicit true
 
-attribute [ext] ReaderT.ext StateT.ext ExceptT.ext OptionT.ext
+attribute [ext] ReaderT.ext StateT.ext ExceptT.ext
 
 @[monad_norm]
 theorem map_eq_bind_pure_comp (m : Type u → Type v) [Monad m] [LawfulMonad m]

Mathlib/Data/Array/Basic.lean

@@ -1,5 +1,4 @@
-import Std.Tactic.HaveI
-import Mathlib.Data.List.Basic
+import Std.Tactic.Alias
 
 attribute [simp] Array.toArrayAux_eq
 

Mathlib/Data/Finset/Pointwise/Interval.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Data.Finset.Pointwise
-import Mathlib.Data.Finset.Interval
 import Mathlib.Data.Set.Pointwise.Interval
 
 

Mathlib/Data/Fintype/Small.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Mathlib.Data.Fintype.Card
-import Mathlib.Logic.Small.Basic
+import Mathlib.Logic.Small.Defs
 
 #align_import data.fintype.small from "leanprover-community/mathlib"@"1126441d6bccf98c81214a0780c73d499f6721fe"
 

Mathlib/Data/Nat/Choose/Bounds.lean

@@ -3,9 +3,10 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Eric Rodriguez
 -/
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Data.Nat.Choose.Basic
+import Mathlib.Algebra.Order.Ring.CharZero
+import Mathlib.Data.Nat.Cast.Order
 
 #align_import data.nat.choose.bounds from "leanprover-community/mathlib"@"550b58538991c8977703fdeb7c9d51a5aa27df11"
 

Mathlib/Data/Nat/Factorization/Basic.lean

@@ -9,6 +9,7 @@ import Mathlib.Data.Nat.PrimeFin
 import Mathlib.NumberTheory.Padics.PadicVal
 import Mathlib.Data.Nat.Interval
 import Mathlib.Tactic.IntervalCases
+import Mathlib.Algebra.GroupPower.Order
 
 #align_import data.nat.factorization.basic from "leanprover-community/mathlib"@"f694c7dead66f5d4c80f446c796a5aad14707f0e"
 

Mathlib/Data/Num/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.Mathport.Rename
 import Mathlib.Init.Data.Nat.Bitwise
 import Mathlib.Init.Data.Int.Basic
 import Lean.Linter.Deprecated
+import Mathlib.Init.ZeroOne
 
 #align_import data.num.basic from "leanprover-community/mathlib"@"c4658a649d216f57e99621708b09dcb3dcccbd23"
 /-!

Mathlib/Data/Polynomial/Degree/CardPowDegree.lean

@@ -5,6 +5,7 @@ Authors: Anne Baanen
 -/
 import Mathlib.Algebra.Order.EuclideanAbsoluteValue
 import Mathlib.Data.Polynomial.FieldDivision
+import Mathlib.Algebra.GroupPower.Order
 
 #align_import data.polynomial.degree.card_pow_degree from "leanprover-community/mathlib"@"85d9f2189d9489f9983c0d01536575b0233bd305"
 

Mathlib/Data/Real/ENNReal.lean

@@ -7,6 +7,7 @@ import Mathlib.Data.Real.NNReal
 import Mathlib.Algebra.Order.Sub.WithTop
 import Mathlib.Data.Set.Intervals.WithBotTop
 import Mathlib.Tactic.GCongr.Core
+import Mathlib.Algebra.GroupPower.Order
 
 #align_import data.real.ennreal from "leanprover-community/mathlib"@"c14c8fcde993801fca8946b0d80131a1a81d1520"
 

Mathlib/Data/Set/Basic.lean

@@ -8,6 +8,7 @@ import Mathlib.Logic.Function.Iterate
 import Mathlib.Tactic.Tauto
 import Mathlib.Tactic.ByContra
 import Mathlib.Util.Delaborators
+import Mathlib.Init.ZeroOne
 
 #align_import data.set.basic from "leanprover-community/mathlib"@"001ffdc42920050657fd45bd2b8bfbec8eaaeb29"
 

Mathlib/Data/UnionFind.lean

@@ -3,9 +3,7 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Tactic.Basic
-import Std.Tactic.Simpa
-import Mathlib.Data.Array.Basic
+import Mathlib.Init.Data.Nat.Lemmas
 
 set_option autoImplicit true
 

Mathlib/Init/Control/Lawful.lean

@@ -189,7 +189,7 @@ namespace OptionT
 
 variable {α β : Type u} {m : Type u → Type v} (x : OptionT m α)
 
-theorem ext {x x' : OptionT m α} (h : x.run = x'.run) : x = x' :=
+@[ext] theorem ext {x x' : OptionT m α} (h : x.run = x'.run) : x = x' :=
   h
 #align option_t.ext OptionTₓ.ext
 

Mathlib/Init/Data/Int/Basic.lean

@@ -7,7 +7,6 @@ The integers, with addition, multiplication, and subtraction.
 -/
 import Mathlib.Mathport.Rename
 import Mathlib.Init.Data.Nat.Notation
-import Mathlib.Init.ZeroOne
 import Std.Data.Int.Lemmas
 
 open Nat

Mathlib/Init/Data/Int/Bitwise.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 
 import Mathlib.Init.Data.Int.Basic
 import Mathlib.Init.Data.Nat.Bitwise
+import Mathlib.Init.ZeroOne
 
 #align_import init.data.int.bitwise from "leanprover-community/lean"@"855e5b74e3a52a40552e8f067169d747d48743fd"
 

Mathlib/Init/Data/Int/CompLemmas.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 
 import Mathlib.Init.Data.Int.Order
+import Mathlib.Init.ZeroOne
 
 #align_import init.data.int.comp_lemmas from "leanprover-community/lean"@"4a03bdeb31b3688c31d02d7ff8e0ff2e5d6174db"
 

Mathlib/Init/Data/Nat/GCD.lean

@@ -5,8 +5,9 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 
 -/
 
-import Mathlib.Init.Data.Nat.Lemmas
-import Mathlib.Init.Meta.WellFoundedTactics
+import Std.Data.Nat.Gcd
+import Mathlib.Init.Data.Nat.Notation
+import Mathlib.Mathport.Rename
 
 #align_import init.data.nat.gcd from "leanprover-community/lean"@"855e5b74e3a52a40552e8f067169d747d48743fd"
 

Mathlib/Init/IteSimp.lean

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 
-import Mathlib.Init.Data.Bool.Basic
-import Mathlib.Init.Data.Bool.Lemmas
+import Mathlib.Mathport.Rename
 
 #align_import init.ite_simp from "leanprover-community/lean"@"4a03bdeb31b3688c31d02d7ff8e0ff2e5d6174db"
 

Mathlib/Init/Meta/WellFoundedTactics.lean

@@ -3,8 +3,8 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-prelude
-import Mathlib.Init.Data.Nat.Lemmas
+import Std.Data.Nat.Lemmas
+import Mathlib.Mathport.Rename
 
 #align_import init.meta.well_founded_tactics from "leanprover-community/lean"@"855e5b74e3a52a40552e8f067169d747d48743fd"
 

Mathlib/Lean/Elab/Term.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
-import Lean.Elab
+import Lean.Elab.SyntheticMVars
 
 /-!
 # Additions to `Lean.Elab.Term`

Mathlib/NumberTheory/LucasLehmer.lean

@@ -9,6 +9,7 @@ import Mathlib.Data.ZMod.Basic
 import Mathlib.GroupTheory.OrderOfElement
 import Mathlib.RingTheory.Fintype
 import Mathlib.Tactic.IntervalCases
+import Mathlib.Algebra.GroupPower.Order
 
 #align_import number_theory.lucas_lehmer from "leanprover-community/mathlib"@"10b4e499f43088dd3bb7b5796184ad5216648ab1"
 

Mathlib/NumberTheory/Multiplicity.lean

@@ -9,6 +9,7 @@ import Mathlib.Data.ZMod.Basic
 import Mathlib.NumberTheory.Padics.PadicVal
 import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.Init.Meta.WellFoundedTactics
+import Mathlib.Algebra.GroupPower.Order
 
 #align_import number_theory.multiplicity from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
 

Mathlib/NumberTheory/PellMatiyasevic.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Star.Unitary
 import Mathlib.Data.Nat.ModEq
 import Mathlib.NumberTheory.Zsqrtd.Basic
 import Mathlib.Tactic.Monotonicity
+import Mathlib.Algebra.GroupPower.Order
 
 #align_import number_theory.pell_matiyasevic from "leanprover-community/mathlib"@"795b501869b9fa7aa716d5fdadd00c03f983a605"
 

Mathlib/NumberTheory/PythagoreanTriples.lean

@@ -9,6 +9,7 @@ import Mathlib.Tactic.Ring
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Data.Int.NatPrime
 import Mathlib.Data.ZMod.Basic
+import Mathlib.Algebra.GroupPower.Order
 
 #align_import number_theory.pythagorean_triples from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
 

Mathlib/Probability/Distributions/Gaussian.lean

@@ -5,6 +5,7 @@ Authors: Lorenzo Luccioli, Rémy Degenne, Alexander Bentkamp
 -/
 import Mathlib.Analysis.SpecialFunctions.Gaussian
 import Mathlib.Probability.Notation
+import Mathlib.MeasureTheory.Decomposition.Lebesgue
 
 /-!
 # Gaussian distributions over ℝ

Mathlib/Probability/Distributions/Poisson.lean

@@ -7,6 +7,7 @@ Authors: Josha Dekker
 import Mathlib.Analysis.NormedSpace.Exponential
 import Mathlib.Analysis.SpecialFunctions.Exponential
 import Mathlib.Probability.Notation
+import Mathlib.Probability.ProbabilityMassFunction.Basic
 
 /-! # Poisson distributions over ℕ
 

Mathlib/Probability/Notation.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import Mathlib.Probability.ProbabilityMassFunction.Basic
 import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
 import Mathlib.MeasureTheory.Decomposition.Lebesgue
 

Mathlib/RingTheory/QuotientNoetherian.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 import Mathlib.RingTheory.Noetherian
-import Mathlib.RingTheory.QuotientNilpotent
+import Mathlib.RingTheory.Ideal.QuotientOperations
 
 #align_import ring_theory.quotient_noetherian from "leanprover-community/mathlib"@"da420a8c6dd5bdfb85c4ced85c34388f633bc6ff"
 

Mathlib/RingTheory/Valuation/Basic.lean

@@ -6,6 +6,7 @@ Authors: Kevin Buzzard, Johan Commelin, Patrick Massot
 import Mathlib.Algebra.Order.WithZero
 import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.Tactic.TFAE
+import Mathlib.Algebra.GroupPower.Order
 
 #align_import ring_theory.valuation.basic from "leanprover-community/mathlib"@"2196ab363eb097c008d4497125e0dde23fb36db2"