diff --git a/EvalTools/Markers.lean b/EvalTools/Markers.lean index 34245f10..38fe8dba 100644 --- a/EvalTools/Markers.lean +++ b/EvalTools/Markers.lean @@ -1,8 +1,9 @@ -import Lake.Toml -import Lake.Util.Message -import Lean import LeanEvalGenerator.Core.Markers +-- The workspace generator drops Core.Markers and forwards other imports here. +-- Keep marker implementation dependencies in Core.Markers so they do not leak +-- into generated challenges. + namespace EvalTools end EvalTools diff --git a/LeanEval/GroupTheory/CommProbClosed.lean b/LeanEval/GroupTheory/CommProbClosed.lean index fcb65377..314c39f6 100644 --- a/LeanEval/GroupTheory/CommProbClosed.lean +++ b/LeanEval/GroupTheory/CommProbClosed.lean @@ -15,7 +15,7 @@ so there is no need to add in `0` to make the set of commuting probabilities clo /-- The set of commuting probabilities of finite groups is closed. -/ @[eval_problem] -theorem commProb_closed : IsClosed ({p : ℝ | βˆƒ (G : Type) (hG : Group G), commProb G = p}) := by +theorem commProb_closed : IsClosed ({p : ℝ | βˆƒ (G : Type) (_hG : Group G), commProb G = p}) := by sorry end GroupTheory diff --git a/generated/H1_not_closedComplemented/ChallengeDeps.lean b/generated/H1_not_closedComplemented/ChallengeDeps.lean index f0c39f1c..1fc5d209 100644 --- a/generated/H1_not_closedComplemented/ChallengeDeps.lean +++ b/generated/H1_not_closedComplemented/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.Fourier.AddCircle import Mathlib.MeasureTheory.Function.L1Space.Integrable import Mathlib.Topology.Algebra.Module.Complement -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/abel_ruffini/Challenge.lean b/generated/abel_ruffini/Challenge.lean index 79e49c68..a2b939fb 100644 --- a/generated/abel_ruffini/Challenge.lean +++ b/generated/abel_ruffini/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Polynomial diff --git a/generated/abel_ruffini/Solution.lean b/generated/abel_ruffini/Solution.lean index 06aa596e..175e7ef3 100644 --- a/generated/abel_ruffini/Solution.lean +++ b/generated/abel_ruffini/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Polynomial diff --git a/generated/abel_ruffini/Submission.lean b/generated/abel_ruffini/Submission.lean index ba8756e4..e7cdf3fb 100644 --- a/generated/abel_ruffini/Submission.lean +++ b/generated/abel_ruffini/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Polynomial diff --git a/generated/adoCharZero/ChallengeDeps.lean b/generated/adoCharZero/ChallengeDeps.lean index 09cbdd6e..cd3c6d1f 100644 --- a/generated/adoCharZero/ChallengeDeps.lean +++ b/generated/adoCharZero/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.RepresentationTheory.AdoIwasawa diff --git a/generated/adoIwasawa/ChallengeDeps.lean b/generated/adoIwasawa/ChallengeDeps.lean index 09cbdd6e..cd3c6d1f 100644 --- a/generated/adoIwasawa/ChallengeDeps.lean +++ b/generated/adoIwasawa/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.RepresentationTheory.AdoIwasawa diff --git a/generated/alternating_sign_matrix_count/ChallengeDeps.lean b/generated/alternating_sign_matrix_count/ChallengeDeps.lean index 3989e22e..3d56c1e7 100644 --- a/generated/alternating_sign_matrix_count/ChallengeDeps.lean +++ b/generated/alternating_sign_matrix_count/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Combinatorics.AlternatingSignMatrix diff --git a/generated/annals_absolute_profinite_rigidity/ChallengeDeps.lean b/generated/annals_absolute_profinite_rigidity/ChallengeDeps.lean index a5297a62..0874c154 100644 --- a/generated/annals_absolute_profinite_rigidity/ChallengeDeps.lean +++ b/generated/annals_absolute_profinite_rigidity/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup import Mathlib.NumberTheory.NumberField.Basic import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Absolute profinite rigidity and hyperbolic geometry diff --git a/generated/annals_algebraic_integers/ChallengeDeps.lean b/generated/annals_algebraic_integers/ChallengeDeps.lean index 76f3013e..e656f612 100644 --- a/generated/annals_algebraic_integers/ChallengeDeps.lean +++ b/generated/annals_algebraic_integers/ChallengeDeps.lean @@ -2,9 +2,6 @@ import Mathlib.Algebra.Polynomial.Roots import Mathlib.Analysis.CStarAlgebra.Classes import Mathlib.FieldTheory.Minpoly.Basic import Mathlib.RingTheory.Algebraic.Defs -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Algebraic integers with conjugates in a prescribed distribution diff --git a/generated/annals_bose_gases/ChallengeDeps.lean b/generated/annals_bose_gases/ChallengeDeps.lean index 0009d9bc..3eb3e333 100644 --- a/generated/annals_bose_gases/ChallengeDeps.lean +++ b/generated/annals_bose_gases/ChallengeDeps.lean @@ -3,9 +3,6 @@ import Mathlib.Analysis.Normed.Lp.MeasurableSpace import Mathlib.MeasureTheory.Function.LocallyIntegrable import Mathlib.MeasureTheory.Integral.Bochner.Basic import Mathlib.MeasureTheory.Measure.Haar.OfBasis -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from The energy of dilute Bose gases diff --git a/generated/annals_bounded_multiplicative_functions/ChallengeDeps.lean b/generated/annals_bounded_multiplicative_functions/ChallengeDeps.lean index 6871535b..17b61334 100644 --- a/generated/annals_bounded_multiplicative_functions/ChallengeDeps.lean +++ b/generated/annals_bounded_multiplicative_functions/ChallengeDeps.lean @@ -2,9 +2,6 @@ import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic import Mathlib.NumberTheory.ArithmeticFunction.Liouville import Mathlib.NumberTheory.DirichletCharacter.Basic import Mathlib.NumberTheory.SmoothNumbers -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statements from Higher uniformity of bounded multiplicative functions in short intervals diff --git a/generated/annals_chowla_and_twin_prime_over_fq_t/ChallengeDeps.lean b/generated/annals_chowla_and_twin_prime_over_fq_t/ChallengeDeps.lean index c82fecff..d46eaa04 100644 --- a/generated/annals_chowla_and_twin_prime_over_fq_t/ChallengeDeps.lean +++ b/generated/annals_chowla_and_twin_prime_over_fq_t/ChallengeDeps.lean @@ -3,9 +3,6 @@ import Mathlib.Analysis.SpecialFunctions.Log.Base import Mathlib.FieldTheory.Finite.GaloisField import Mathlib.RingTheory.Ideal.Norm.AbsNorm import Mathlib.RingTheory.UniqueFactorizationDomain.Moebius -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statements from On the Chowla and twin primes conjectures over 𝔽_q[T] diff --git a/generated/annals_conjecture_of_marton/ChallengeDeps.lean b/generated/annals_conjecture_of_marton/ChallengeDeps.lean index e102280d..6e7a1d02 100644 --- a/generated/annals_conjecture_of_marton/ChallengeDeps.lean +++ b/generated/annals_conjecture_of_marton/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.Algebra.Field.ZMod import Mathlib.Combinatorics.Additive.CovBySMul -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from On a conjecture of Marton diff --git a/generated/annals_dirichlet_weyl_bound/ChallengeDeps.lean b/generated/annals_dirichlet_weyl_bound/ChallengeDeps.lean index fa6914f5..359295fd 100644 --- a/generated/annals_dirichlet_weyl_bound/ChallengeDeps.lean +++ b/generated/annals_dirichlet_weyl_bound/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib.NumberTheory.LSeries.DirichletContinuation -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from The Weyl bound for Dirichlet L-functions of cube-free conductor diff --git a/generated/annals_duffin_schaeffer_conjecture/ChallengeDeps.lean b/generated/annals_duffin_schaeffer_conjecture/ChallengeDeps.lean index b7a9f463..eb4c33a0 100644 --- a/generated/annals_duffin_schaeffer_conjecture/ChallengeDeps.lean +++ b/generated/annals_duffin_schaeffer_conjecture/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib.Topology.MetricSpace.HausdorffDimension -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statements from On the Duffin-Schaeffer conjecture diff --git a/generated/annals_enumerating_number_fields/ChallengeDeps.lean b/generated/annals_enumerating_number_fields/ChallengeDeps.lean index 4f2dcad7..fa959a75 100644 --- a/generated/annals_enumerating_number_fields/ChallengeDeps.lean +++ b/generated/annals_enumerating_number_fields/ChallengeDeps.lean @@ -2,9 +2,6 @@ import Mathlib.Algebra.Lie.OfAssociative import Mathlib.Algebra.MvPolynomial.PDeriv import Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent import Mathlib.NumberTheory.NumberField.Discriminant.Basic -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statements from Enumerating number fields diff --git a/generated/annals_equiangular_lines_fixed_angle/ChallengeDeps.lean b/generated/annals_equiangular_lines_fixed_angle/ChallengeDeps.lean index 2938b24c..d5a37384 100644 --- a/generated/annals_equiangular_lines_fixed_angle/ChallengeDeps.lean +++ b/generated/annals_equiangular_lines_fixed_angle/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Analysis.Normed.Algebra.Spectrum import Mathlib.Combinatorics.SimpleGraph.AdjMatrix -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Equiangular lines with a fixed angle diff --git a/generated/annals_erdos_faber_lovasz_conjecture/ChallengeDeps.lean b/generated/annals_erdos_faber_lovasz_conjecture/ChallengeDeps.lean index 57630426..f530a2df 100644 --- a/generated/annals_erdos_faber_lovasz_conjecture/ChallengeDeps.lean +++ b/generated/annals_erdos_faber_lovasz_conjecture/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Order.Lattice.Nat import Mathlib.Data.Set.Card import Mathlib.Order.Filter.AtTopBot.Defs -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from A proof of the ErdΕ‘s–Faber–LovΓ‘sz conjecture diff --git a/generated/annals_erdos_supersingular_primes/ChallengeDeps.lean b/generated/annals_erdos_supersingular_primes/ChallengeDeps.lean index af5fec2d..87275d2f 100644 --- a/generated/annals_erdos_supersingular_primes/ChallengeDeps.lean +++ b/generated/annals_erdos_supersingular_primes/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Complex.Exponential -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from A conjecture of ErdΕ‘s, supersingular primes and short character sums diff --git a/generated/annals_finite_time_singularity/ChallengeDeps.lean b/generated/annals_finite_time_singularity/ChallengeDeps.lean index f9fa116c..504a58ec 100644 --- a/generated/annals_finite_time_singularity/ChallengeDeps.lean +++ b/generated/annals_finite_time_singularity/ChallengeDeps.lean @@ -4,9 +4,6 @@ import Mathlib.LinearAlgebra.CrossProduct import Mathlib.LinearAlgebra.Trace import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic import Mathlib.Topology.MetricSpace.Holder -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Finite-time singularity formation for C^{1,Ξ±} solutions to diff --git a/generated/annals_flat_littlewood_poly/ChallengeDeps.lean b/generated/annals_flat_littlewood_poly/ChallengeDeps.lean index 31970f28..bb347b98 100644 --- a/generated/annals_flat_littlewood_poly/ChallengeDeps.lean +++ b/generated/annals_flat_littlewood_poly/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Algebra.Polynomial.Degree.Defs import Mathlib.Algebra.Polynomial.Eval.Defs import Mathlib.Analysis.Complex.Norm -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Flat Littlewood polynomials exist diff --git a/generated/annals_fractal_uncertainty/ChallengeDeps.lean b/generated/annals_fractal_uncertainty/ChallengeDeps.lean index aaa6ec54..dcc31f99 100644 --- a/generated/annals_fractal_uncertainty/ChallengeDeps.lean +++ b/generated/annals_fractal_uncertainty/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Fourier.LpSpace -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Fractal uncertainty in higher dimensions diff --git a/generated/annals_fractional_expectation_thresholds/ChallengeDeps.lean b/generated/annals_fractional_expectation_thresholds/ChallengeDeps.lean index c96b89b6..342b4dc2 100644 --- a/generated/annals_fractional_expectation_thresholds/ChallengeDeps.lean +++ b/generated/annals_fractional_expectation_thresholds/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib.Probability.Distributions.SetBernoulli -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Thresholds versus fractional expectation-thresholds diff --git a/generated/annals_good_lt_codes/ChallengeDeps.lean b/generated/annals_good_lt_codes/ChallengeDeps.lean index cdc5de16..73177aa9 100644 --- a/generated/annals_good_lt_codes/ChallengeDeps.lean +++ b/generated/annals_good_lt_codes/ChallengeDeps.lean @@ -2,9 +2,6 @@ import Mathlib.Algebra.Field.ZMod import Mathlib.InformationTheory.Hamming import Mathlib.LinearAlgebra.Dimension.Finrank import Mathlib.Probability.ProbabilityMassFunction.Basic -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Good Locally Testable Codes diff --git a/generated/annals_hasse_principle_random_fano/ChallengeDeps.lean b/generated/annals_hasse_principle_random_fano/ChallengeDeps.lean index 77454ea3..3c5ea8c3 100644 --- a/generated/annals_hasse_principle_random_fano/ChallengeDeps.lean +++ b/generated/annals_hasse_principle_random_fano/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.LinearAlgebra.Projectivization.Basic import Mathlib.NumberTheory.NumberField.AdeleRing import Mathlib.RingTheory.MvPolynomial.Homogeneous -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from The Hasse principle for random Fano hypersurfaces diff --git a/generated/annals_hessian_estimates/ChallengeDeps.lean b/generated/annals_hessian_estimates/ChallengeDeps.lean index 5b0fc3ec..69c0112d 100644 --- a/generated/annals_hessian_estimates/ChallengeDeps.lean +++ b/generated/annals_hessian_estimates/ChallengeDeps.lean @@ -3,9 +3,6 @@ import Mathlib.Analysis.InnerProductSpace.Spectrum import Mathlib.Analysis.Normed.Lp.MeasurableSpace import Mathlib.MeasureTheory.Function.LpSeminorm.Defs import Mathlib.MeasureTheory.Measure.Haar.OfBasis -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Hessian estimates for the sigma-2 equation in dimension four diff --git a/generated/annals_improved_bounds_sunflower_lemma/ChallengeDeps.lean b/generated/annals_improved_bounds_sunflower_lemma/ChallengeDeps.lean index 10320760..68d32020 100644 --- a/generated/annals_improved_bounds_sunflower_lemma/ChallengeDeps.lean +++ b/generated/annals_improved_bounds_sunflower_lemma/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.SpecialFunctions.Log.Base -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Improved bounds for the sunflower lemma diff --git a/generated/annals_inscribed_rectangles/ChallengeDeps.lean b/generated/annals_inscribed_rectangles/ChallengeDeps.lean index e68ee0bb..120ac53e 100644 --- a/generated/annals_inscribed_rectangles/ChallengeDeps.lean +++ b/generated/annals_inscribed_rectangles/ChallengeDeps.lean @@ -2,9 +2,6 @@ import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Geometry.Manifold.SmoothEmbedding import Mathlib.MeasureTheory.Measure.Haar.OfBasis import Mathlib.Probability.Distributions.Fernique -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Inscribed rectangles in a smooth Jordan curve attain at least diff --git a/generated/annals_integer_multiplication/ChallengeDeps.lean b/generated/annals_integer_multiplication/ChallengeDeps.lean index 2d781f8d..01d81f81 100644 --- a/generated/annals_integer_multiplication/ChallengeDeps.lean +++ b/generated/annals_integer_multiplication/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.SpecialFunctions.Log.Basic import Mathlib.Computability.TuringMachine.Computable -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Integer multiplication in time O(n log n) diff --git a/generated/annals_large_value_estimates/ChallengeDeps.lean b/generated/annals_large_value_estimates/ChallengeDeps.lean index ecc31478..049e1f4c 100644 --- a/generated/annals_large_value_estimates/ChallengeDeps.lean +++ b/generated/annals_large_value_estimates/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.SpecialFunctions.Pow.Real -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from New large value estimates for Dirichlet polynomials diff --git a/generated/annals_linear_subspaces/ChallengeDeps.lean b/generated/annals_linear_subspaces/ChallengeDeps.lean index a824ce26..d607df23 100644 --- a/generated/annals_linear_subspaces/ChallengeDeps.lean +++ b/generated/annals_linear_subspaces/ChallengeDeps.lean @@ -2,9 +2,6 @@ import Mathlib.Algebra.Module.ZLattice.Basic import Mathlib.Analysis.InnerProductSpace.ExteriorPower import Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic import Mathlib.LinearAlgebra.Projectivization.Basic -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Rational approximations to linear subspaces diff --git a/generated/annals_local_global_apollonian_circle_packings/ChallengeDeps.lean b/generated/annals_local_global_apollonian_circle_packings/ChallengeDeps.lean index b84f0bcc..27c0f6a1 100644 --- a/generated/annals_local_global_apollonian_circle_packings/ChallengeDeps.lean +++ b/generated/annals_local_global_apollonian_circle_packings/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib.LinearAlgebra.Matrix.Permutation -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statements from The local-global conjecture for Apollonian circle packings is false diff --git a/generated/annals_lorentzian_polynomials/ChallengeDeps.lean b/generated/annals_lorentzian_polynomials/ChallengeDeps.lean index 5b62bac2..cede3261 100644 --- a/generated/annals_lorentzian_polynomials/ChallengeDeps.lean +++ b/generated/annals_lorentzian_polynomials/ChallengeDeps.lean @@ -3,9 +3,6 @@ import Mathlib.Analysis.Complex.UpperHalfPlane.Basic import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic import Mathlib.RingTheory.MvPolynomial.EulerIdentity import Mathlib.Topology.Algebra.Module.ModuleTopology -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Lorentzian polynomials diff --git a/generated/annals_mckay_conjecture/ChallengeDeps.lean b/generated/annals_mckay_conjecture/ChallengeDeps.lean index 96e61ef9..81b62648 100644 --- a/generated/annals_mckay_conjecture/ChallengeDeps.lean +++ b/generated/annals_mckay_conjecture/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Basic.Complex.Basic import Mathlib.GroupTheory.Sylow import Mathlib.RepresentationTheory.Character -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from The McKay Conjecture on character degrees diff --git a/generated/annals_motivic_invariants/ChallengeDeps.lean b/generated/annals_motivic_invariants/ChallengeDeps.lean index de4891bf..43d9b06d 100644 --- a/generated/annals_motivic_invariants/ChallengeDeps.lean +++ b/generated/annals_motivic_invariants/ChallengeDeps.lean @@ -3,9 +3,6 @@ import Mathlib.AlgebraicGeometry.Birational.Composition import Mathlib.AlgebraicGeometry.Morphisms.Proper import Mathlib.Basic.Complex.Basic import Mathlib.NumberTheory.NumberField.Basic -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Motivic invariants of birational maps diff --git a/generated/annals_on_approximation_of_reals/ChallengeDeps.lean b/generated/annals_on_approximation_of_reals/ChallengeDeps.lean index d83e09a4..ae7dd728 100644 --- a/generated/annals_on_approximation_of_reals/ChallengeDeps.lean +++ b/generated/annals_on_approximation_of_reals/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.FieldTheory.Minpoly.Basic import Mathlib.RingTheory.Algebraic.Defs -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from On approximation to a real number by algebraic numbers of bounded degree diff --git a/generated/annals_on_coherence_of_one_relator_groups/ChallengeDeps.lean b/generated/annals_on_coherence_of_one_relator_groups/ChallengeDeps.lean index d51aa5a3..f598862b 100644 --- a/generated/annals_on_coherence_of_one_relator_groups/ChallengeDeps.lean +++ b/generated/annals_on_coherence_of_one_relator_groups/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.Algebra.Module.FinitePresentation import Mathlib.GroupTheory.FinitelyPresentedGroup -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from On the coherence of one-relator groups and their group algebras diff --git a/generated/annals_on_property_t/ChallengeDeps.lean b/generated/annals_on_property_t/ChallengeDeps.lean index 147f5eda..504b0f73 100644 --- a/generated/annals_on_property_t/ChallengeDeps.lean +++ b/generated/annals_on_property_t/ChallengeDeps.lean @@ -3,9 +3,6 @@ import Mathlib.Algebra.MonoidAlgebra.MapDomain import Mathlib.Basic.Real.Basic import Mathlib.GroupTheory.FreeGroup.Basic import Mathlib.SetTheory.Cardinal.Finite -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from On property (T) for Aut(F_n) and SL_n(Z) diff --git a/generated/annals_optimal_moebius/ChallengeDeps.lean b/generated/annals_optimal_moebius/ChallengeDeps.lean index a5ffe90f..93f9af7c 100644 --- a/generated/annals_optimal_moebius/ChallengeDeps.lean +++ b/generated/annals_optimal_moebius/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Calculus.ContDiff.Defs import Mathlib.Analysis.InnerProductSpace.PiL2 -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from The optimal paper Moebius band diff --git a/generated/annals_periodic_tiling_conjecture/ChallengeDeps.lean b/generated/annals_periodic_tiling_conjecture/ChallengeDeps.lean index 5ccd0900..ffd34507 100644 --- a/generated/annals_periodic_tiling_conjecture/ChallengeDeps.lean +++ b/generated/annals_periodic_tiling_conjecture/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib.Algebra.Module.ZLattice.Basic -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statements from A counterexample to the periodic tiling conjecture diff --git a/generated/annals_pointwise_ergodic_theorems/ChallengeDeps.lean b/generated/annals_pointwise_ergodic_theorems/ChallengeDeps.lean index 1c223412..c560c3bc 100644 --- a/generated/annals_pointwise_ergodic_theorems/ChallengeDeps.lean +++ b/generated/annals_pointwise_ergodic_theorems/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.Normed.Lp.PiLp import Mathlib.Algebra.Polynomial.Degree.Defs import Mathlib.MeasureTheory.Function.LpSpace.Basic -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statements from Pointwise ergodic theorems for non-conventional bilinear polynomial averages diff --git a/generated/annals_pseudorandom_grassmann/ChallengeDeps.lean b/generated/annals_pseudorandom_grassmann/ChallengeDeps.lean index b7f65210..fa512293 100644 --- a/generated/annals_pseudorandom_grassmann/ChallengeDeps.lean +++ b/generated/annals_pseudorandom_grassmann/ChallengeDeps.lean @@ -5,9 +5,6 @@ import Mathlib.Basic.Real.Basic import Mathlib.Data.SetLike.Fintype import Mathlib.LinearAlgebra.Dimension.Finrank import Mathlib.Order.Filter.AtTopBot.Defs -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Pseudorandom sets in Grassmann graph have near-perfect expansion diff --git a/generated/annals_rademacher_enflo_type/ChallengeDeps.lean b/generated/annals_rademacher_enflo_type/ChallengeDeps.lean index e5286bb8..6e8890ed 100644 --- a/generated/annals_rademacher_enflo_type/ChallengeDeps.lean +++ b/generated/annals_rademacher_enflo_type/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Probability.ProductMeasure import Mathlib.Probability.Distributions.Bernoulli import Mathlib.MeasureTheory.Integral.Bochner.Basic -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Notation for AnnalsChallenge diff --git a/generated/annals_random_bernoulli_matrices/ChallengeDeps.lean b/generated/annals_random_bernoulli_matrices/ChallengeDeps.lean index cb4b8f7c..aa46525d 100644 --- a/generated/annals_random_bernoulli_matrices/ChallengeDeps.lean +++ b/generated/annals_random_bernoulli_matrices/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.Probability.HasLaw import Mathlib.Probability.Distributions.Bernoulli -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statements from Singularity of random Bernoulli matrices diff --git a/generated/annals_rectangular_peg_problem/ChallengeDeps.lean b/generated/annals_rectangular_peg_problem/ChallengeDeps.lean index cdf2378b..1ff0038a 100644 --- a/generated/annals_rectangular_peg_problem/ChallengeDeps.lean +++ b/generated/annals_rectangular_peg_problem/ChallengeDeps.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.SpecialFunctions.Complex.Circle import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Geometry.Manifold.SmoothEmbedding import Mathlib.Topology.MetricSpace.Similarity -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from The rectangular peg problem diff --git a/generated/annals_reverse_minkowski/ChallengeDeps.lean b/generated/annals_reverse_minkowski/ChallengeDeps.lean index 81895297..7a226c07 100644 --- a/generated/annals_reverse_minkowski/ChallengeDeps.lean +++ b/generated/annals_reverse_minkowski/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib.Algebra.Module.ZLattice.Basic -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from A reverse Minkowski theorem diff --git a/generated/annals_simplicity_conjecture/ChallengeDeps.lean b/generated/annals_simplicity_conjecture/ChallengeDeps.lean index 590cec4c..1c0291f4 100644 --- a/generated/annals_simplicity_conjecture/ChallengeDeps.lean +++ b/generated/annals_simplicity_conjecture/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.Normed.Lp.MeasurableSpace import Mathlib.Dynamics.FixedPoints.Support import Mathlib.MeasureTheory.Measure.Haar.OfBasis -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Proof of the simplicity conjecture diff --git a/generated/annals_spread_of_a_finite_group/ChallengeDeps.lean b/generated/annals_spread_of_a_finite_group/ChallengeDeps.lean index 44168024..9ae7db0b 100644 --- a/generated/annals_spread_of_a_finite_group/ChallengeDeps.lean +++ b/generated/annals_spread_of_a_finite_group/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.GroupTheory.QuotientGroup.Defs import Mathlib.Data.ENat.Lattice -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from The spread of a finite group diff --git a/generated/annals_supremum_of_selector_processes/ChallengeDeps.lean b/generated/annals_supremum_of_selector_processes/ChallengeDeps.lean index f279d49c..81bc3619 100644 --- a/generated/annals_supremum_of_selector_processes/ChallengeDeps.lean +++ b/generated/annals_supremum_of_selector_processes/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.Probability.Distributions.SetBernoulli import Mathlib.MeasureTheory.Integral.Bochner.Basic -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Notation for AnnalsChallenge diff --git a/generated/annals_symplectic_monodromy/ChallengeDeps.lean b/generated/annals_symplectic_monodromy/ChallengeDeps.lean index f13ae9c8..379abb86 100644 --- a/generated/annals_symplectic_monodromy/ChallengeDeps.lean +++ b/generated/annals_symplectic_monodromy/ChallengeDeps.lean @@ -3,9 +3,6 @@ import Mathlib.LinearAlgebra.Dimension.Basic import Mathlib.RingTheory.Ideal.Quotient.Defs import Mathlib.RingTheory.MvPowerSeries.Derivative import Mathlib.Topology.UnitInterval -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Symplectic monodromy at radius zero and equimultiplicity of diff --git a/generated/annals_ulam/ChallengeDeps.lean b/generated/annals_ulam/ChallengeDeps.lean index 1811ac87..b2ade613 100644 --- a/generated/annals_ulam/ChallengeDeps.lean +++ b/generated/annals_ulam/ChallengeDeps.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Calculus.ContDiff.Defs import Mathlib.Analysis.Normed.Lp.MeasurableSpace import Mathlib.MeasureTheory.Integral.Average import Mathlib.MeasureTheory.Measure.Haar.OfBasis -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from A negative answer to Ulam's Problem 19 from the Scottish Book diff --git a/generated/annals_uniform_mordell_lang/Challenge.lean b/generated/annals_uniform_mordell_lang/Challenge.lean index 51ff2a94..970bdcaf 100644 --- a/generated/annals_uniform_mordell_lang/Challenge.lean +++ b/generated/annals_uniform_mordell_lang/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib.AlgebraicGeometry.Group.Abelian -import Lake.Toml -import Lake.Util.Message -import Lean /- Copyright (c) 2026 Thomas Browning. All rights reserved. diff --git a/generated/annals_unit_conjecture/ChallengeDeps.lean b/generated/annals_unit_conjecture/ChallengeDeps.lean index 428a0c52..fcc0997c 100644 --- a/generated/annals_unit_conjecture/ChallengeDeps.lean +++ b/generated/annals_unit_conjecture/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Algebra.Field.ZMod import Mathlib.Algebra.MonoidAlgebra.Defs import Mathlib.GroupTheory.PresentedGroup -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from A counterexample to the unit conjecture for group rings diff --git a/generated/annals_van_der_waerden_conjecture/ChallengeDeps.lean b/generated/annals_van_der_waerden_conjecture/ChallengeDeps.lean index ddc8ca27..c18d92eb 100644 --- a/generated/annals_van_der_waerden_conjecture/ChallengeDeps.lean +++ b/generated/annals_van_der_waerden_conjecture/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Asymptotics.Defs import Mathlib.FieldTheory.PolynomialGaloisGroup -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Galois groups of random integer polynomials and van der Waerden's Conjecture diff --git a/generated/annals_viscosity_solutions/ChallengeDeps.lean b/generated/annals_viscosity_solutions/ChallengeDeps.lean index 5f376302..8bb7154b 100644 --- a/generated/annals_viscosity_solutions/ChallengeDeps.lean +++ b/generated/annals_viscosity_solutions/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Calculus.Gradient.Basic import Mathlib.Analysis.Calculus.IteratedDeriv.Defs -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Viscosity solutions and hyperbolic motions: diff --git a/generated/annals_wilkies_conjecture/ChallengeDeps.lean b/generated/annals_wilkies_conjecture/ChallengeDeps.lean index 6be43d47..ec984ef2 100644 --- a/generated/annals_wilkies_conjecture/ChallengeDeps.lean +++ b/generated/annals_wilkies_conjecture/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.ModelTheory.Algebra.Ring.Basic import Mathlib.ModelTheory.Definability import Mathlib.NumberTheory.Height.NumberField -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statement from Wilkie's conjecture for Pfaffian structures diff --git a/generated/annals_zagier_hoffman_positive_char/ChallengeDeps.lean b/generated/annals_zagier_hoffman_positive_char/ChallengeDeps.lean index 125cccd9..78168268 100644 --- a/generated/annals_zagier_hoffman_positive_char/ChallengeDeps.lean +++ b/generated/annals_zagier_hoffman_positive_char/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.NumberTheory.FunctionField import Mathlib.RingTheory.SimpleRing.Principal import Mathlib.Topology.Algebra.InfiniteSum.Defs -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Main Statements from On Zagier-Hoffman's conjectures in positive characteristic diff --git a/generated/annulus_theorem_dim_four/ChallengeDeps.lean b/generated/annulus_theorem_dim_four/ChallengeDeps.lean index 4059a396..0ee95c9b 100644 --- a/generated/annulus_theorem_dim_four/ChallengeDeps.lean +++ b/generated/annulus_theorem_dim_four/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Topology diff --git a/generated/annulus_theorem_high_dim/ChallengeDeps.lean b/generated/annulus_theorem_high_dim/ChallengeDeps.lean index 4059a396..0ee95c9b 100644 --- a/generated/annulus_theorem_high_dim/ChallengeDeps.lean +++ b/generated/annulus_theorem_high_dim/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Topology diff --git a/generated/anosov_bowen_shadowing/ChallengeDeps.lean b/generated/anosov_bowen_shadowing/ChallengeDeps.lean index 053c3078..f2a1fbaa 100644 --- a/generated/anosov_bowen_shadowing/ChallengeDeps.lean +++ b/generated/anosov_bowen_shadowing/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Dynamics diff --git a/generated/aspherical_integer_homology_four_sphere/ChallengeDeps.lean b/generated/aspherical_integer_homology_four_sphere/ChallengeDeps.lean index be8af65a..9ed87753 100644 --- a/generated/aspherical_integer_homology_four_sphere/ChallengeDeps.lean +++ b/generated/aspherical_integer_homology_four_sphere/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Topology diff --git a/generated/baer_suzuki/ChallengeDeps.lean b/generated/baer_suzuki/ChallengeDeps.lean index 153c4c6f..5b4079ba 100644 --- a/generated/baer_suzuki/ChallengeDeps.lean +++ b/generated/baer_suzuki/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace GroupTheory diff --git a/generated/bakerWustholz_linearForms_logs/ChallengeDeps.lean b/generated/bakerWustholz_linearForms_logs/ChallengeDeps.lean index 063cb6f1..6ffc5d43 100644 --- a/generated/bakerWustholz_linearForms_logs/ChallengeDeps.lean +++ b/generated/bakerWustholz_linearForms_logs/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.NumberTheory.Height.NumberField import Mathlib.Analysis.SpecialFunctions.Complex.Log -import Lake.Toml -import Lake.Util.Message -import Lean /-! # The Baker–WΓΌstholz theorem on linear forms in logarithms diff --git a/generated/balanceable_bounded_partitions/ChallengeDeps.lean b/generated/balanceable_bounded_partitions/ChallengeDeps.lean index c6423d32..2b86a1c2 100644 --- a/generated/balanceable_bounded_partitions/ChallengeDeps.lean +++ b/generated/balanceable_bounded_partitions/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.Combinatorics.Enumerative.Partition.Basic import Mathlib.Algebra.GCDMonoid.Finset -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Combinatorics diff --git a/generated/banach_alaoglu_bourbaki/ChallengeDeps.lean b/generated/banach_alaoglu_bourbaki/ChallengeDeps.lean index 2e44fb22..0315385c 100644 --- a/generated/banach_alaoglu_bourbaki/ChallengeDeps.lean +++ b/generated/banach_alaoglu_bourbaki/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/bauer_extreme_point_uniqueness/Challenge.lean b/generated/bauer_extreme_point_uniqueness/Challenge.lean index 6a49a76c..464b861b 100644 --- a/generated/bauer_extreme_point_uniqueness/Challenge.lean +++ b/generated/bauer_extreme_point_uniqueness/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open MeasureTheory diff --git a/generated/bauer_extreme_point_uniqueness/Solution.lean b/generated/bauer_extreme_point_uniqueness/Solution.lean index 6f399108..f2f9201d 100644 --- a/generated/bauer_extreme_point_uniqueness/Solution.lean +++ b/generated/bauer_extreme_point_uniqueness/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open MeasureTheory diff --git a/generated/bauer_extreme_point_uniqueness/Submission.lean b/generated/bauer_extreme_point_uniqueness/Submission.lean index adb469f0..5aa55218 100644 --- a/generated/bauer_extreme_point_uniqueness/Submission.lean +++ b/generated/bauer_extreme_point_uniqueness/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open MeasureTheory diff --git a/generated/bender_suzuki/ChallengeDeps.lean b/generated/bender_suzuki/ChallengeDeps.lean index 0bab3fef..72185160 100644 --- a/generated/bender_suzuki/ChallengeDeps.lean +++ b/generated/bender_suzuki/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Matrix diff --git a/generated/bezout_projective_multiplicity/ChallengeDeps.lean b/generated/bezout_projective_multiplicity/ChallengeDeps.lean index 57aa94ea..4c1ea1b5 100644 --- a/generated/bezout_projective_multiplicity/ChallengeDeps.lean +++ b/generated/bezout_projective_multiplicity/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace AlgebraicGeometry diff --git a/generated/boone_higman_embedding/ChallengeDeps.lean b/generated/boone_higman_embedding/ChallengeDeps.lean index f7fa8a6a..091fd373 100644 --- a/generated/boone_higman_embedding/ChallengeDeps.lean +++ b/generated/boone_higman_embedding/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.GroupTheory.BooneHigmanEmbedding diff --git a/generated/boone_higman_simple/ChallengeDeps.lean b/generated/boone_higman_simple/ChallengeDeps.lean index 937376f4..ea02c488 100644 --- a/generated/boone_higman_simple/ChallengeDeps.lean +++ b/generated/boone_higman_simple/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace GroupTheory diff --git a/generated/bourgain_polynomial_ergodic/ChallengeDeps.lean b/generated/bourgain_polynomial_ergodic/ChallengeDeps.lean index 2172085d..b52e53a9 100644 --- a/generated/bourgain_polynomial_ergodic/ChallengeDeps.lean +++ b/generated/bourgain_polynomial_ergodic/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Dynamics.BourgainErgodic diff --git a/generated/brauer_character_in_cyclotomic/Challenge.lean b/generated/brauer_character_in_cyclotomic/Challenge.lean index d6cb93d1..ed736ba9 100644 --- a/generated/brauer_character_in_cyclotomic/Challenge.lean +++ b/generated/brauer_character_in_cyclotomic/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem brauer_character_in_cyclotomic (G : Type) [Group G] [Fintype G] : βˆƒ Ο† : CyclotomicField (Monoid.exponent G) β„š β†’+* β„‚, diff --git a/generated/brauer_character_in_cyclotomic/Solution.lean b/generated/brauer_character_in_cyclotomic/Solution.lean index 70982aee..9186862d 100644 --- a/generated/brauer_character_in_cyclotomic/Solution.lean +++ b/generated/brauer_character_in_cyclotomic/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem brauer_character_in_cyclotomic (G : Type) [Group G] [Fintype G] : diff --git a/generated/brauer_character_in_cyclotomic/Submission.lean b/generated/brauer_character_in_cyclotomic/Submission.lean index 42b3adfc..41ef0ff7 100644 --- a/generated/brauer_character_in_cyclotomic/Submission.lean +++ b/generated/brauer_character_in_cyclotomic/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/brauer_fowler/Challenge.lean b/generated/brauer_fowler/Challenge.lean index 90bfec15..dfc666ae 100644 --- a/generated/brauer_fowler/Challenge.lean +++ b/generated/brauer_fowler/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem brauer_fowler : βˆƒ f : β„• β†’ β„•, βˆ€ (G : Type) [Group G] [Finite G], diff --git a/generated/brauer_fowler/Solution.lean b/generated/brauer_fowler/Solution.lean index 7e2295f3..d1a71134 100644 --- a/generated/brauer_fowler/Solution.lean +++ b/generated/brauer_fowler/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem brauer_fowler : diff --git a/generated/brauer_fowler/Submission.lean b/generated/brauer_fowler/Submission.lean index 4e8d35a2..db5ca526 100644 --- a/generated/brauer_fowler/Submission.lean +++ b/generated/brauer_fowler/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/brauer_splitting_field/Challenge.lean b/generated/brauer_splitting_field/Challenge.lean index f4907203..1c7c755d 100644 --- a/generated/brauer_splitting_field/Challenge.lean +++ b/generated/brauer_splitting_field/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open scoped TensorProduct diff --git a/generated/brauer_splitting_field/Solution.lean b/generated/brauer_splitting_field/Solution.lean index b6771a33..f4db9461 100644 --- a/generated/brauer_splitting_field/Solution.lean +++ b/generated/brauer_splitting_field/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped TensorProduct diff --git a/generated/brauer_splitting_field/Submission.lean b/generated/brauer_splitting_field/Submission.lean index eebe5f3d..c50c52e6 100644 --- a/generated/brauer_splitting_field/Submission.lean +++ b/generated/brauer_splitting_field/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped TensorProduct diff --git a/generated/brauer_suzuki/ChallengeDeps.lean b/generated/brauer_suzuki/ChallengeDeps.lean index d9bb80d8..1e1ae67f 100644 --- a/generated/brauer_suzuki/ChallengeDeps.lean +++ b/generated/brauer_suzuki/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace GroupTheory diff --git a/generated/brouwer_fixed_point/Challenge.lean b/generated/brouwer_fixed_point/Challenge.lean index b6e1a0ac..8499c4cc 100644 --- a/generated/brouwer_fixed_point/Challenge.lean +++ b/generated/brouwer_fixed_point/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Set diff --git a/generated/brouwer_fixed_point/Solution.lean b/generated/brouwer_fixed_point/Solution.lean index 12d15484..bd3dc6e2 100644 --- a/generated/brouwer_fixed_point/Solution.lean +++ b/generated/brouwer_fixed_point/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Set diff --git a/generated/brouwer_fixed_point/Submission.lean b/generated/brouwer_fixed_point/Submission.lean index 160bef0f..e9ebfa49 100644 --- a/generated/brouwer_fixed_point/Submission.lean +++ b/generated/brouwer_fixed_point/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Set diff --git a/generated/brun_constant_converges/ChallengeDeps.lean b/generated/brun_constant_converges/ChallengeDeps.lean index 171037cc..e5fa1b58 100644 --- a/generated/brun_constant_converges/ChallengeDeps.lean +++ b/generated/brun_constant_converges/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.NumberTheory.BrunConstant diff --git a/generated/budney_gabai_knotted_three_spheres/Challenge.lean b/generated/budney_gabai_knotted_three_spheres/Challenge.lean index 5fd528ff..447c4ae6 100644 --- a/generated/budney_gabai_knotted_three_spheres/Challenge.lean +++ b/generated/budney_gabai_knotted_three_spheres/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open scoped ContDiff Manifold open Metric (sphere) diff --git a/generated/budney_gabai_knotted_three_spheres/Solution.lean b/generated/budney_gabai_knotted_three_spheres/Solution.lean index d56cee90..e850ff05 100644 --- a/generated/budney_gabai_knotted_three_spheres/Solution.lean +++ b/generated/budney_gabai_knotted_three_spheres/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped ContDiff Manifold diff --git a/generated/budney_gabai_knotted_three_spheres/Submission.lean b/generated/budney_gabai_knotted_three_spheres/Submission.lean index 5a459edd..29ac2e6f 100644 --- a/generated/budney_gabai_knotted_three_spheres/Submission.lean +++ b/generated/budney_gabai_knotted_three_spheres/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped ContDiff Manifold diff --git a/generated/bvp_comparison/Challenge.lean b/generated/bvp_comparison/Challenge.lean index 3c78c2e3..640d2489 100644 --- a/generated/bvp_comparison/Challenge.lean +++ b/generated/bvp_comparison/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Calculus.Deriv.Basic -import Lake.Toml -import Lake.Util.Message -import Lean theorem bvp_comparison (J : Set ℝ) (hJ_open : IsOpen J) (hJ_sub : Set.Icc (0 : ℝ) 1 βŠ† J) (u v : ℝ β†’ ℝ) diff --git a/generated/bvp_comparison/Solution.lean b/generated/bvp_comparison/Solution.lean index fd5776ee..f21cbe41 100644 --- a/generated/bvp_comparison/Solution.lean +++ b/generated/bvp_comparison/Solution.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Calculus.Deriv.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem bvp_comparison (J : Set ℝ) (hJ_open : IsOpen J) (hJ_sub : Set.Icc (0 : ℝ) 1 βŠ† J) diff --git a/generated/bvp_comparison/Submission.lean b/generated/bvp_comparison/Submission.lean index 7a3917b9..ae03e3e7 100644 --- a/generated/bvp_comparison/Submission.lean +++ b/generated/bvp_comparison/Submission.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Calculus.Deriv.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/cauchy_kovalevskaya/ChallengeDeps.lean b/generated/cauchy_kovalevskaya/ChallengeDeps.lean index 5c90cf64..593d747f 100644 --- a/generated/cauchy_kovalevskaya/ChallengeDeps.lean +++ b/generated/cauchy_kovalevskaya/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/cdt_linearIndependent/Challenge.lean b/generated/cdt_linearIndependent/Challenge.lean index e0c62b04..33ee9875 100644 --- a/generated/cdt_linearIndependent/Challenge.lean +++ b/generated/cdt_linearIndependent/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem cdt_linearIndependent : letI Ο‡ : ZMod 3 β†’ β„‚ := ![0, 1, -1] diff --git a/generated/cdt_linearIndependent/Solution.lean b/generated/cdt_linearIndependent/Solution.lean index 3ab6e4f8..3a5aa6d3 100644 --- a/generated/cdt_linearIndependent/Solution.lean +++ b/generated/cdt_linearIndependent/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem cdt_linearIndependent : diff --git a/generated/cdt_linearIndependent/Submission.lean b/generated/cdt_linearIndependent/Submission.lean index 1ab406c3..7394004f 100644 --- a/generated/cdt_linearIndependent/Submission.lean +++ b/generated/cdt_linearIndependent/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/cerf_gamma_four/Challenge.lean b/generated/cerf_gamma_four/Challenge.lean index 642582ac..865087a7 100644 --- a/generated/cerf_gamma_four/Challenge.lean +++ b/generated/cerf_gamma_four/Challenge.lean @@ -2,9 +2,6 @@ import Mathlib.Geometry.Manifold.Diffeomorph import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Geometry.Manifold.Instances.Real import Mathlib.LinearAlgebra.UnitaryGroup -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Manifold ContDiff open Metric (sphere) diff --git a/generated/cerf_gamma_four/Solution.lean b/generated/cerf_gamma_four/Solution.lean index 9ee72308..90f290af 100644 --- a/generated/cerf_gamma_four/Solution.lean +++ b/generated/cerf_gamma_four/Solution.lean @@ -2,9 +2,6 @@ import Mathlib.Geometry.Manifold.Diffeomorph import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Geometry.Manifold.Instances.Real import Mathlib.LinearAlgebra.UnitaryGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped Manifold ContDiff diff --git a/generated/cerf_gamma_four/Submission.lean b/generated/cerf_gamma_four/Submission.lean index ff448642..497e982a 100644 --- a/generated/cerf_gamma_four/Submission.lean +++ b/generated/cerf_gamma_four/Submission.lean @@ -2,9 +2,6 @@ import Mathlib.Geometry.Manifold.Diffeomorph import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Geometry.Manifold.Instances.Real import Mathlib.LinearAlgebra.UnitaryGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped Manifold ContDiff diff --git a/generated/chebyshev_sign_change/ChallengeDeps.lean b/generated/chebyshev_sign_change/ChallengeDeps.lean index 665e9dfa..85593401 100644 --- a/generated/chebyshev_sign_change/ChallengeDeps.lean +++ b/generated/chebyshev_sign_change/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace NumberTheory diff --git a/generated/chen_theorem/ChallengeDeps.lean b/generated/chen_theorem/ChallengeDeps.lean index c934040e..cce05c28 100644 --- a/generated/chen_theorem/ChallengeDeps.lean +++ b/generated/chen_theorem/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.NumberTheory.ChenTheorem diff --git a/generated/choquet_representation_theorem/Challenge.lean b/generated/choquet_representation_theorem/Challenge.lean index 72f2d5e7..f887d07a 100644 --- a/generated/choquet_representation_theorem/Challenge.lean +++ b/generated/choquet_representation_theorem/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open MeasureTheory diff --git a/generated/choquet_representation_theorem/Solution.lean b/generated/choquet_representation_theorem/Solution.lean index cf72aa84..d7420503 100644 --- a/generated/choquet_representation_theorem/Solution.lean +++ b/generated/choquet_representation_theorem/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open MeasureTheory diff --git a/generated/choquet_representation_theorem/Submission.lean b/generated/choquet_representation_theorem/Submission.lean index d88c9c28..462f2e55 100644 --- a/generated/choquet_representation_theorem/Submission.lean +++ b/generated/choquet_representation_theorem/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open MeasureTheory diff --git a/generated/chudnovsky_formula_for_pi_inv/Challenge.lean b/generated/chudnovsky_formula_for_pi_inv/Challenge.lean index 14685478..294de6c8 100644 --- a/generated/chudnovsky_formula_for_pi_inv/Challenge.lean +++ b/generated/chudnovsky_formula_for_pi_inv/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Real.Pi.Chudnovsky -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Real diff --git a/generated/chudnovsky_formula_for_pi_inv/Solution.lean b/generated/chudnovsky_formula_for_pi_inv/Solution.lean index d79dcd2b..2712cc53 100644 --- a/generated/chudnovsky_formula_for_pi_inv/Solution.lean +++ b/generated/chudnovsky_formula_for_pi_inv/Solution.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Real.Pi.Chudnovsky -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped Real diff --git a/generated/chudnovsky_formula_for_pi_inv/Submission.lean b/generated/chudnovsky_formula_for_pi_inv/Submission.lean index 351168d8..30cf6b4f 100644 --- a/generated/chudnovsky_formula_for_pi_inv/Submission.lean +++ b/generated/chudnovsky_formula_for_pi_inv/Submission.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Real.Pi.Chudnovsky -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped Real diff --git a/generated/ci_regenerate_main_check/Challenge.lean b/generated/ci_regenerate_main_check/Challenge.lean index c7ec9ee5..15203824 100644 --- a/generated/ci_regenerate_main_check/Challenge.lean +++ b/generated/ci_regenerate_main_check/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem ci_regenerate_main_check : True := by sorry diff --git a/generated/ci_regenerate_main_check/Solution.lean b/generated/ci_regenerate_main_check/Solution.lean index db839a8a..6d1643b8 100644 --- a/generated/ci_regenerate_main_check/Solution.lean +++ b/generated/ci_regenerate_main_check/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem ci_regenerate_main_check : True := by diff --git a/generated/ci_regenerate_main_check/Submission.lean b/generated/ci_regenerate_main_check/Submission.lean index 9d2a821e..1239f963 100644 --- a/generated/ci_regenerate_main_check/Submission.lean +++ b/generated/ci_regenerate_main_check/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/ckmrv_fourier_interpolation/ChallengeDeps.lean b/generated/ckmrv_fourier_interpolation/ChallengeDeps.lean index 9948fae0..2bb2e847 100644 --- a/generated/ckmrv_fourier_interpolation/ChallengeDeps.lean +++ b/generated/ckmrv_fourier_interpolation/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Analysis.CKMRVInterpolation diff --git a/generated/classification_finite_simple_groups/Challenge.lean b/generated/classification_finite_simple_groups/Challenge.lean index f6775b98..6b96b284 100644 --- a/generated/classification_finite_simple_groups/Challenge.lean +++ b/generated/classification_finite_simple_groups/Challenge.lean @@ -1,7 +1,4 @@ import TauCeti.GroupTheory.SpecificGroups.CFSG.Classification -import Lake.Toml -import Lake.Util.Message -import Lean theorem classification_finite_simple_groups (G : Type) [Group G] [Finite G] [IsSimpleGroup G] : βˆƒ i : TauCeti.CFSGIndex, Nonempty (G ≃* i.Group) := by diff --git a/generated/classification_finite_simple_groups/Solution.lean b/generated/classification_finite_simple_groups/Solution.lean index 0d6271bd..c609dc68 100644 --- a/generated/classification_finite_simple_groups/Solution.lean +++ b/generated/classification_finite_simple_groups/Solution.lean @@ -1,7 +1,4 @@ import TauCeti.GroupTheory.SpecificGroups.CFSG.Classification -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem classification_finite_simple_groups (G : Type) [Group G] [Finite G] [IsSimpleGroup G] : diff --git a/generated/classification_finite_simple_groups/Submission.lean b/generated/classification_finite_simple_groups/Submission.lean index 28b7fe59..ebf5bff6 100644 --- a/generated/classification_finite_simple_groups/Submission.lean +++ b/generated/classification_finite_simple_groups/Submission.lean @@ -1,7 +1,4 @@ import TauCeti.GroupTheory.SpecificGroups.CFSG.Classification -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/coc_strong_normalization/ChallengeDeps.lean b/generated/coc_strong_normalization/ChallengeDeps.lean index e8051800..7e1bb5d8 100644 --- a/generated/coc_strong_normalization/ChallengeDeps.lean +++ b/generated/coc_strong_normalization/ChallengeDeps.lean @@ -1,6 +1,3 @@ -import Lake.Toml -import Lake.Util.Message -import Lean /-! The fixed calculus used by the CoC strong-normalization evaluation problem. diff --git a/generated/coherent_cohomology_finite_dimensional/ChallengeDeps.lean b/generated/coherent_cohomology_finite_dimensional/ChallengeDeps.lean index 87e53770..2505d3eb 100644 --- a/generated/coherent_cohomology_finite_dimensional/ChallengeDeps.lean +++ b/generated/coherent_cohomology_finite_dimensional/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Finite-dimensionality of coherent cohomology diff --git a/generated/commProb_closed/Challenge.lean b/generated/commProb_closed/Challenge.lean index 3ef50beb..f2255a96 100644 --- a/generated/commProb_closed/Challenge.lean +++ b/generated/commProb_closed/Challenge.lean @@ -1,8 +1,5 @@ import Mathlib.GroupTheory.CommutingProbability import Mathlib.Topology.MetricSpace.Pseudo.Defs -import Lake.Toml -import Lake.Util.Message -import Lean -theorem commProb_closed : IsClosed ({p : ℝ | βˆƒ (G : Type) (hG : Group G), commProb G = p}) := by +theorem commProb_closed : IsClosed ({p : ℝ | βˆƒ (G : Type) (_hG : Group G), commProb G = p}) := by sorry diff --git a/generated/commProb_closed/Solution.lean b/generated/commProb_closed/Solution.lean index b14b7706..a3dfd6e3 100644 --- a/generated/commProb_closed/Solution.lean +++ b/generated/commProb_closed/Solution.lean @@ -1,9 +1,6 @@ import Mathlib.GroupTheory.CommutingProbability import Mathlib.Topology.MetricSpace.Pseudo.Defs -import Lake.Toml -import Lake.Util.Message -import Lean import Submission -theorem commProb_closed : IsClosed ({p : ℝ | βˆƒ (G : Type) (hG : Group G), commProb G = p}) := by +theorem commProb_closed : IsClosed ({p : ℝ | βˆƒ (G : Type) (_hG : Group G), commProb G = p}) := by exact Submission.commProb_closed diff --git a/generated/commProb_closed/Submission.lean b/generated/commProb_closed/Submission.lean index f631b2d3..c464742a 100644 --- a/generated/commProb_closed/Submission.lean +++ b/generated/commProb_closed/Submission.lean @@ -1,13 +1,10 @@ import Mathlib.GroupTheory.CommutingProbability import Mathlib.Topology.MetricSpace.Pseudo.Defs -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission -theorem commProb_closed : IsClosed ({p : ℝ | βˆƒ (G : Type) (hG : Group G), commProb G = p}) := by +theorem commProb_closed : IsClosed ({p : ℝ | βˆƒ (G : Type) (_hG : Group G), commProb G = p}) := by sorry end Submission diff --git a/generated/commProb_closed/holes.json b/generated/commProb_closed/holes.json index 97158101..1ddbe6b1 100644 --- a/generated/commProb_closed/holes.json +++ b/generated/commProb_closed/holes.json @@ -6,7 +6,7 @@ "name": "LeanEval.GroupTheory.commProb_closed", "basename": "commProb_closed", "kind": "theorem", - "body": "/-- The set of commuting probabilities of finite groups is closed. -/\ntheorem commProb_closed : IsClosed ({p : \u211d | \u2203 (G : Type) (hG : Group G), commProb G = p}) := by\n sorry" + "body": "/-- The set of commuting probabilities of finite groups is closed. -/\ntheorem commProb_closed : IsClosed ({p : \u211d | \u2203 (G : Type) (_hG : Group G), commProb G = p}) := by\n sorry" } ] } diff --git a/generated/compact_group_semisimple/Challenge.lean b/generated/compact_group_semisimple/Challenge.lean index 6bf6ec68..7293f254 100644 --- a/generated/compact_group_semisimple/Challenge.lean +++ b/generated/compact_group_semisimple/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Representation diff --git a/generated/compact_group_semisimple/Solution.lean b/generated/compact_group_semisimple/Solution.lean index 262a2357..2c6d0bed 100644 --- a/generated/compact_group_semisimple/Solution.lean +++ b/generated/compact_group_semisimple/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Representation diff --git a/generated/compact_group_semisimple/Submission.lean b/generated/compact_group_semisimple/Submission.lean index 19bf2be0..7163cae5 100644 --- a/generated/compact_group_semisimple/Submission.lean +++ b/generated/compact_group_semisimple/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Representation diff --git a/generated/contractibleSpace_houseWithTwoRooms/ChallengeDeps.lean b/generated/contractibleSpace_houseWithTwoRooms/ChallengeDeps.lean index 3bbbe139..98a0f5f1 100644 --- a/generated/contractibleSpace_houseWithTwoRooms/ChallengeDeps.lean +++ b/generated/contractibleSpace_houseWithTwoRooms/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib.Topology.Homotopy.Contractible -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Topology diff --git a/generated/conway_knot_not_smoothly_slice/ChallengeDeps.lean b/generated/conway_knot_not_smoothly_slice/ChallengeDeps.lean index 64238c9c..6ea749ba 100644 --- a/generated/conway_knot_not_smoothly_slice/ChallengeDeps.lean +++ b/generated/conway_knot_not_smoothly_slice/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Analysis.Calculus.ContDiff.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace KnotTheory diff --git a/generated/conway_knot_topologically_slice/ChallengeDeps.lean b/generated/conway_knot_topologically_slice/ChallengeDeps.lean index 64238c9c..6ea749ba 100644 --- a/generated/conway_knot_topologically_slice/ChallengeDeps.lean +++ b/generated/conway_knot_topologically_slice/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Analysis.Calculus.ContDiff.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace KnotTheory diff --git a/generated/conway_schneeberger_fifteen/ChallengeDeps.lean b/generated/conway_schneeberger_fifteen/ChallengeDeps.lean index 10fedbe3..3e9a34ef 100644 --- a/generated/conway_schneeberger_fifteen/ChallengeDeps.lean +++ b/generated/conway_schneeberger_fifteen/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace NumberTheory diff --git a/generated/cubic_decay_asymptotic/Challenge.lean b/generated/cubic_decay_asymptotic/Challenge.lean index 3830064e..9549edd5 100644 --- a/generated/cubic_decay_asymptotic/Challenge.lean +++ b/generated/cubic_decay_asymptotic/Challenge.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Analysis.SpecialFunctions.Pow.Real -import Lake.Toml -import Lake.Util.Message -import Lean open Filter Topology diff --git a/generated/cubic_decay_asymptotic/Solution.lean b/generated/cubic_decay_asymptotic/Solution.lean index e040b0c6..9869ea6e 100644 --- a/generated/cubic_decay_asymptotic/Solution.lean +++ b/generated/cubic_decay_asymptotic/Solution.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Analysis.SpecialFunctions.Pow.Real -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Filter Topology diff --git a/generated/cubic_decay_asymptotic/Submission.lean b/generated/cubic_decay_asymptotic/Submission.lean index 624668c5..4fd47c28 100644 --- a/generated/cubic_decay_asymptotic/Submission.lean +++ b/generated/cubic_decay_asymptotic/Submission.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Analysis.SpecialFunctions.Pow.Real -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Filter Topology diff --git a/generated/cyclotomic_integer_house_between_two_and_76_33/Challenge.lean b/generated/cyclotomic_integer_house_between_two_and_76_33/Challenge.lean index c2dbaff7..da48303d 100644 --- a/generated/cyclotomic_integer_house_between_two_and_76_33/Challenge.lean +++ b/generated/cyclotomic_integer_house_between_two_and_76_33/Challenge.lean @@ -1,8 +1,5 @@ import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic import Mathlib.NumberTheory.NumberField.House -import Lake.Toml -import Lake.Util.Message -import Lean open NumberField diff --git a/generated/cyclotomic_integer_house_between_two_and_76_33/Solution.lean b/generated/cyclotomic_integer_house_between_two_and_76_33/Solution.lean index 49b25dd1..700852ac 100644 --- a/generated/cyclotomic_integer_house_between_two_and_76_33/Solution.lean +++ b/generated/cyclotomic_integer_house_between_two_and_76_33/Solution.lean @@ -1,8 +1,5 @@ import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic import Mathlib.NumberTheory.NumberField.House -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open NumberField diff --git a/generated/cyclotomic_integer_house_between_two_and_76_33/Submission.lean b/generated/cyclotomic_integer_house_between_two_and_76_33/Submission.lean index 426fccf1..1f23fb04 100644 --- a/generated/cyclotomic_integer_house_between_two_and_76_33/Submission.lean +++ b/generated/cyclotomic_integer_house_between_two_and_76_33/Submission.lean @@ -1,8 +1,5 @@ import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic import Mathlib.NumberTheory.NumberField.House -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open NumberField diff --git a/generated/cyclotomic_integer_house_le_two/Challenge.lean b/generated/cyclotomic_integer_house_le_two/Challenge.lean index 2a1d6119..b7ee8fb8 100644 --- a/generated/cyclotomic_integer_house_le_two/Challenge.lean +++ b/generated/cyclotomic_integer_house_le_two/Challenge.lean @@ -1,8 +1,5 @@ import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic import Mathlib.NumberTheory.NumberField.House -import Lake.Toml -import Lake.Util.Message -import Lean open NumberField diff --git a/generated/cyclotomic_integer_house_le_two/Solution.lean b/generated/cyclotomic_integer_house_le_two/Solution.lean index 91e2a59c..6fd32321 100644 --- a/generated/cyclotomic_integer_house_le_two/Solution.lean +++ b/generated/cyclotomic_integer_house_le_two/Solution.lean @@ -1,8 +1,5 @@ import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic import Mathlib.NumberTheory.NumberField.House -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open NumberField diff --git a/generated/cyclotomic_integer_house_le_two/Submission.lean b/generated/cyclotomic_integer_house_le_two/Submission.lean index 5405eab3..8e1c96ae 100644 --- a/generated/cyclotomic_integer_house_le_two/Submission.lean +++ b/generated/cyclotomic_integer_house_le_two/Submission.lean @@ -1,8 +1,5 @@ import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic import Mathlib.NumberTheory.NumberField.House -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open NumberField diff --git a/generated/darboux/ChallengeDeps.lean b/generated/darboux/ChallengeDeps.lean index a7a56446..84d4f0e8 100644 --- a/generated/darboux/ChallengeDeps.lean +++ b/generated/darboux/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/deBranges_theorem/Challenge.lean b/generated/deBranges_theorem/Challenge.lean index c88a1e50..63730c37 100644 --- a/generated/deBranges_theorem/Challenge.lean +++ b/generated/deBranges_theorem/Challenge.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Calculus.IteratedDeriv.Defs import Mathlib.Analysis.Complex.Basic -import Lake.Toml -import Lake.Util.Message -import Lean open Metric diff --git a/generated/deBranges_theorem/Solution.lean b/generated/deBranges_theorem/Solution.lean index e433fee9..2dd476d5 100644 --- a/generated/deBranges_theorem/Solution.lean +++ b/generated/deBranges_theorem/Solution.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Calculus.IteratedDeriv.Defs import Mathlib.Analysis.Complex.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Metric diff --git a/generated/deBranges_theorem/Submission.lean b/generated/deBranges_theorem/Submission.lean index b2f66fa6..64def0c8 100644 --- a/generated/deBranges_theorem/Submission.lean +++ b/generated/deBranges_theorem/Submission.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Calculus.IteratedDeriv.Defs import Mathlib.Analysis.Complex.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Metric diff --git a/generated/dehn_sommerville/ChallengeDeps.lean b/generated/dehn_sommerville/ChallengeDeps.lean index bb45cb20..3b68b45d 100644 --- a/generated/dehn_sommerville/ChallengeDeps.lean +++ b/generated/dehn_sommerville/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Combinatorics.DehnSommerville diff --git a/generated/derived_solidification_free_CW_homology/ChallengeDeps.lean b/generated/derived_solidification_free_CW_homology/ChallengeDeps.lean index 1f7b01b9..3e4b4b08 100644 --- a/generated/derived_solidification_free_CW_homology/ChallengeDeps.lean +++ b/generated/derived_solidification_free_CW_homology/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Derived solidification of free CW complexes diff --git a/generated/dimitrov/Challenge.lean b/generated/dimitrov/Challenge.lean index 1fef4c90..5239ca49 100644 --- a/generated/dimitrov/Challenge.lean +++ b/generated/dimitrov/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib.NumberTheory.NumberField.House -import Lake.Toml -import Lake.Util.Message -import Lean theorem dimitrov {K : Type*} [Field K] [NumberField K] (Ξ± : K) diff --git a/generated/dimitrov/Solution.lean b/generated/dimitrov/Solution.lean index 1855d0a4..99a444b0 100644 --- a/generated/dimitrov/Solution.lean +++ b/generated/dimitrov/Solution.lean @@ -1,7 +1,4 @@ import Mathlib.NumberTheory.NumberField.House -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem dimitrov {K : Type*} [Field K] [NumberField K] diff --git a/generated/dimitrov/Submission.lean b/generated/dimitrov/Submission.lean index 5df2d898..06cda00a 100644 --- a/generated/dimitrov/Submission.lean +++ b/generated/dimitrov/Submission.lean @@ -1,7 +1,4 @@ import Mathlib.NumberTheory.NumberField.House -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/direct_summand/ChallengeDeps.lean b/generated/direct_summand/ChallengeDeps.lean index 19a8c16c..e0a61f1e 100644 --- a/generated/direct_summand/ChallengeDeps.lean +++ b/generated/direct_summand/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Direct summand conjecture and its derived variant diff --git a/generated/dirichlet_eigenvalues_eq_nat_sq/Challenge.lean b/generated/dirichlet_eigenvalues_eq_nat_sq/Challenge.lean index 5fcfc254..ec6bbbb1 100644 --- a/generated/dirichlet_eigenvalues_eq_nat_sq/Challenge.lean +++ b/generated/dirichlet_eigenvalues_eq_nat_sq/Challenge.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Real diff --git a/generated/dirichlet_eigenvalues_eq_nat_sq/Solution.lean b/generated/dirichlet_eigenvalues_eq_nat_sq/Solution.lean index e7e52dab..e80229fc 100644 --- a/generated/dirichlet_eigenvalues_eq_nat_sq/Solution.lean +++ b/generated/dirichlet_eigenvalues_eq_nat_sq/Solution.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped Real diff --git a/generated/dirichlet_eigenvalues_eq_nat_sq/Submission.lean b/generated/dirichlet_eigenvalues_eq_nat_sq/Submission.lean index 27a0ba4e..04ccd39f 100644 --- a/generated/dirichlet_eigenvalues_eq_nat_sq/Submission.lean +++ b/generated/dirichlet_eigenvalues_eq_nat_sq/Submission.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped Real diff --git a/generated/duffin_schaeffer/Challenge.lean b/generated/duffin_schaeffer/Challenge.lean index 58ea96dc..ccd06cb6 100644 --- a/generated/duffin_schaeffer/Challenge.lean +++ b/generated/duffin_schaeffer/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib.NumberTheory.WellApproximable -import Lake.Toml -import Lake.Util.Message -import Lean open MeasureTheory diff --git a/generated/duffin_schaeffer/Solution.lean b/generated/duffin_schaeffer/Solution.lean index 85ea18eb..24c5ea30 100644 --- a/generated/duffin_schaeffer/Solution.lean +++ b/generated/duffin_schaeffer/Solution.lean @@ -1,7 +1,4 @@ import Mathlib.NumberTheory.WellApproximable -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open MeasureTheory diff --git a/generated/duffin_schaeffer/Submission.lean b/generated/duffin_schaeffer/Submission.lean index a82a541c..e04b715e 100644 --- a/generated/duffin_schaeffer/Submission.lean +++ b/generated/duffin_schaeffer/Submission.lean @@ -1,7 +1,4 @@ import Mathlib.NumberTheory.WellApproximable -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open MeasureTheory diff --git a/generated/dvd_card_connectedComponent_markoffGraph/ChallengeDeps.lean b/generated/dvd_card_connectedComponent_markoffGraph/ChallengeDeps.lean index 6d5b3197..e487dd5e 100644 --- a/generated/dvd_card_connectedComponent_markoffGraph/ChallengeDeps.lean +++ b/generated/dvd_card_connectedComponent_markoffGraph/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite import Mathlib.Data.ZMod.Basic -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Combinatorics diff --git a/generated/e8_irrep_tensor_square_decomp/ChallengeDeps.lean b/generated/e8_irrep_tensor_square_decomp/ChallengeDeps.lean index 76442236..2937c68b 100644 --- a/generated/e8_irrep_tensor_square_decomp/ChallengeDeps.lean +++ b/generated/e8_irrep_tensor_square_decomp/ChallengeDeps.lean @@ -5,9 +5,6 @@ import Mathlib.Algebra.Lie.Semisimple.Defs import Mathlib.Basic.Complex.Basic import Mathlib.LinearAlgebra.Dimension.Finrank import Mathlib.RingTheory.SimpleModule.Isotypic -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace RepresentationTheory diff --git a/generated/einsiedler_katok_lindenstrauss/ChallengeDeps.lean b/generated/einsiedler_katok_lindenstrauss/ChallengeDeps.lean index 2b0c95aa..ae4efdd3 100644 --- a/generated/einsiedler_katok_lindenstrauss/ChallengeDeps.lean +++ b/generated/einsiedler_katok_lindenstrauss/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Smallness of exceptional set to Littlewood's conjecture diff --git a/generated/entropy_dimension_lyapunov/ChallengeDeps.lean b/generated/entropy_dimension_lyapunov/ChallengeDeps.lean index f2590845..ac9eff3f 100644 --- a/generated/entropy_dimension_lyapunov/ChallengeDeps.lean +++ b/generated/entropy_dimension_lyapunov/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Dynamics diff --git a/generated/equichordal_point_unique/ChallengeDeps.lean b/generated/equichordal_point_unique/ChallengeDeps.lean index 07fded1f..04015c81 100644 --- a/generated/equichordal_point_unique/ChallengeDeps.lean +++ b/generated/equichordal_point_unique/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Geometry.Equichordal diff --git a/generated/erdos_unit_distance_conjecture_false/ChallengeDeps.lean b/generated/erdos_unit_distance_conjecture_false/ChallengeDeps.lean index f1d2373e..4c423807 100644 --- a/generated/erdos_unit_distance_conjecture_false/ChallengeDeps.lean +++ b/generated/erdos_unit_distance_conjecture_false/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Combinatorics diff --git a/generated/euler_lagrange_equation/ChallengeDeps.lean b/generated/euler_lagrange_equation/ChallengeDeps.lean index 078b9506..8968b73a 100644 --- a/generated/euler_lagrange_equation/ChallengeDeps.lean +++ b/generated/euler_lagrange_equation/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/exists_chiral_knot/ChallengeDeps.lean b/generated/exists_chiral_knot/ChallengeDeps.lean index f529acfa..62913fd4 100644 --- a/generated/exists_chiral_knot/ChallengeDeps.lean +++ b/generated/exists_chiral_knot/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Analysis.Calculus.ContDiff.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace KnotTheory diff --git a/generated/exists_complementary_polynomial_on_unit_circle/Challenge.lean b/generated/exists_complementary_polynomial_on_unit_circle/Challenge.lean index 4961bac5..9b60c09a 100644 --- a/generated/exists_complementary_polynomial_on_unit_circle/Challenge.lean +++ b/generated/exists_complementary_polynomial_on_unit_circle/Challenge.lean @@ -1,9 +1,6 @@ import Mathlib.Algebra.Polynomial.Basic import Mathlib.Algebra.Polynomial.Degree.Defs import Mathlib.Analysis.Complex.Circle -import Lake.Toml -import Lake.Util.Message -import Lean open Polynomial diff --git a/generated/exists_complementary_polynomial_on_unit_circle/Solution.lean b/generated/exists_complementary_polynomial_on_unit_circle/Solution.lean index fc211b5c..ba21a5df 100644 --- a/generated/exists_complementary_polynomial_on_unit_circle/Solution.lean +++ b/generated/exists_complementary_polynomial_on_unit_circle/Solution.lean @@ -1,9 +1,6 @@ import Mathlib.Algebra.Polynomial.Basic import Mathlib.Algebra.Polynomial.Degree.Defs import Mathlib.Analysis.Complex.Circle -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Polynomial diff --git a/generated/exists_complementary_polynomial_on_unit_circle/Submission.lean b/generated/exists_complementary_polynomial_on_unit_circle/Submission.lean index 480c16cd..dfdbc2ac 100644 --- a/generated/exists_complementary_polynomial_on_unit_circle/Submission.lean +++ b/generated/exists_complementary_polynomial_on_unit_circle/Submission.lean @@ -1,9 +1,6 @@ import Mathlib.Algebra.Polynomial.Basic import Mathlib.Algebra.Polynomial.Degree.Defs import Mathlib.Analysis.Complex.Circle -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Polynomial diff --git a/generated/exists_nonisotopic_knots/ChallengeDeps.lean b/generated/exists_nonisotopic_knots/ChallengeDeps.lean index f529acfa..62913fd4 100644 --- a/generated/exists_nonisotopic_knots/ChallengeDeps.lean +++ b/generated/exists_nonisotopic_knots/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Analysis.Calculus.ContDiff.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace KnotTheory diff --git a/generated/exists_nonisotopic_link/ChallengeDeps.lean b/generated/exists_nonisotopic_link/ChallengeDeps.lean index f529acfa..62913fd4 100644 --- a/generated/exists_nonisotopic_link/ChallengeDeps.lean +++ b/generated/exists_nonisotopic_link/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Analysis.Calculus.ContDiff.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace KnotTheory diff --git a/generated/exists_topologically_slice_not_smoothly_slice/ChallengeDeps.lean b/generated/exists_topologically_slice_not_smoothly_slice/ChallengeDeps.lean index ac96ee0b..c828a3d7 100644 --- a/generated/exists_topologically_slice_not_smoothly_slice/ChallengeDeps.lean +++ b/generated/exists_topologically_slice_not_smoothly_slice/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Analysis.Calculus.ContDiff.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace KnotTheory diff --git a/generated/faltings/ChallengeDeps.lean b/generated/faltings/ChallengeDeps.lean index 2e698156..87cbdcf3 100644 --- a/generated/faltings/ChallengeDeps.lean +++ b/generated/faltings/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Faltings' theorem (Mordell conjecture) diff --git a/generated/families_of_maps_b01/ChallengeDeps.lean b/generated/families_of_maps_b01/ChallengeDeps.lean index 2367351f..9615b43f 100644 --- a/generated/families_of_maps_b01/ChallengeDeps.lean +++ b/generated/families_of_maps_b01/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Adapting families of maps to open covers (Morrison–Walker, *The Blob Complex*) diff --git a/generated/fang_xia_tiling_partition_transitive/ChallengeDeps.lean b/generated/fang_xia_tiling_partition_transitive/ChallengeDeps.lean index ae59650a..7ba8da14 100644 --- a/generated/fang_xia_tiling_partition_transitive/ChallengeDeps.lean +++ b/generated/fang_xia_tiling_partition_transitive/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Combinatorics diff --git a/generated/fary_milnor/ChallengeDeps.lean b/generated/fary_milnor/ChallengeDeps.lean index 89b83745..86c902d5 100644 --- a/generated/fary_milnor/ChallengeDeps.lean +++ b/generated/fary_milnor/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/fatou_julia_dichotomy/ChallengeDeps.lean b/generated/fatou_julia_dichotomy/ChallengeDeps.lean index 54f7a462..acfafcef 100644 --- a/generated/fatou_julia_dichotomy/ChallengeDeps.lean +++ b/generated/fatou_julia_dichotomy/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace ComplexAnalysis diff --git a/generated/feit_thompson/Challenge.lean b/generated/feit_thompson/Challenge.lean index b19d25b7..e1b93796 100644 --- a/generated/feit_thompson/Challenge.lean +++ b/generated/feit_thompson/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem feit_thompson {G : Type*} [Group G] [Finite G] (_h : Odd (Nat.card G)) : Group.IsSolvable G := by diff --git a/generated/feit_thompson/Solution.lean b/generated/feit_thompson/Solution.lean index 4415815c..02ee7045 100644 --- a/generated/feit_thompson/Solution.lean +++ b/generated/feit_thompson/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem feit_thompson {G : Type*} [Group G] [Finite G] diff --git a/generated/feit_thompson/Submission.lean b/generated/feit_thompson/Submission.lean index d89ce5f1..cedb3b06 100644 --- a/generated/feit_thompson/Submission.lean +++ b/generated/feit_thompson/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/fermat_last_theorem/Challenge.lean b/generated/fermat_last_theorem/Challenge.lean index 59a6dd5f..a3efaf0d 100644 --- a/generated/fermat_last_theorem/Challenge.lean +++ b/generated/fermat_last_theorem/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib.NumberTheory.FLT.Basic -import Lake.Toml -import Lake.Util.Message -import Lean theorem fermat_last_theorem : FermatLastTheorem := by diff --git a/generated/fermat_last_theorem/Solution.lean b/generated/fermat_last_theorem/Solution.lean index 45ff0d17..2ff998e1 100644 --- a/generated/fermat_last_theorem/Solution.lean +++ b/generated/fermat_last_theorem/Solution.lean @@ -1,7 +1,4 @@ import Mathlib.NumberTheory.FLT.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem fermat_last_theorem : diff --git a/generated/fermat_last_theorem/Submission.lean b/generated/fermat_last_theorem/Submission.lean index 6043eeef..647de8e9 100644 --- a/generated/fermat_last_theorem/Submission.lean +++ b/generated/fermat_last_theorem/Submission.lean @@ -1,7 +1,4 @@ import Mathlib.NumberTheory.FLT.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/finite_graph_ramsey_theorem/Challenge.lean b/generated/finite_graph_ramsey_theorem/Challenge.lean index 0792d916..e0c69820 100644 --- a/generated/finite_graph_ramsey_theorem/Challenge.lean +++ b/generated/finite_graph_ramsey_theorem/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib.Combinatorics.SimpleGraph.Clique -import Lake.Toml -import Lake.Util.Message -import Lean open SimpleGraph diff --git a/generated/finite_graph_ramsey_theorem/Solution.lean b/generated/finite_graph_ramsey_theorem/Solution.lean index 8d126113..c1d488af 100644 --- a/generated/finite_graph_ramsey_theorem/Solution.lean +++ b/generated/finite_graph_ramsey_theorem/Solution.lean @@ -1,7 +1,4 @@ import Mathlib.Combinatorics.SimpleGraph.Clique -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open SimpleGraph diff --git a/generated/finite_graph_ramsey_theorem/Submission.lean b/generated/finite_graph_ramsey_theorem/Submission.lean index c8078497..42762637 100644 --- a/generated/finite_graph_ramsey_theorem/Submission.lean +++ b/generated/finite_graph_ramsey_theorem/Submission.lean @@ -1,7 +1,4 @@ import Mathlib.Combinatorics.SimpleGraph.Clique -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open SimpleGraph diff --git a/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/Challenge.lean b/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/Challenge.lean index afdeddc2..ffa1374d 100644 --- a/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/Challenge.lean +++ b/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/Challenge.lean @@ -1,8 +1,5 @@ import Mathlib.GroupTheory.Solvable import Mathlib.Data.Nat.Prime.Basic -import Lake.Toml -import Lake.Util.Message -import Lean theorem finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow {G : Type*} [Group G] [Fintype G] {p q a b : β„•} diff --git a/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/Solution.lean b/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/Solution.lean index 0624018f..ba81b815 100644 --- a/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/Solution.lean +++ b/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/Solution.lean @@ -1,8 +1,5 @@ import Mathlib.GroupTheory.Solvable import Mathlib.Data.Nat.Prime.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow {G : Type*} [Group G] [Fintype G] diff --git a/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/Submission.lean b/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/Submission.lean index f894b4e6..be999788 100644 --- a/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/Submission.lean +++ b/generated/finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow/Submission.lean @@ -1,8 +1,5 @@ import Mathlib.GroupTheory.Solvable import Mathlib.Data.Nat.Prime.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/five_transitive_card_classification/Challenge.lean b/generated/five_transitive_card_classification/Challenge.lean index 67fc17e5..6f9528f7 100644 --- a/generated/five_transitive_card_classification/Challenge.lean +++ b/generated/five_transitive_card_classification/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem five_transitive_card_classification (G X : Type) [Group G] [Fintype G] [Fintype X] [MulAction G X] [FaithfulSMul G X] diff --git a/generated/five_transitive_card_classification/Solution.lean b/generated/five_transitive_card_classification/Solution.lean index 0ed5ca0b..d2c86742 100644 --- a/generated/five_transitive_card_classification/Solution.lean +++ b/generated/five_transitive_card_classification/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem five_transitive_card_classification (G X : Type) [Group G] [Fintype G] [Fintype X] diff --git a/generated/five_transitive_card_classification/Submission.lean b/generated/five_transitive_card_classification/Submission.lean index dcf01bdc..b59c0acb 100644 --- a/generated/five_transitive_card_classification/Submission.lean +++ b/generated/five_transitive_card_classification/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/four_manifold_not_smooth/Challenge.lean b/generated/four_manifold_not_smooth/Challenge.lean index 66864b72..eec0ae07 100644 --- a/generated/four_manifold_not_smooth/Challenge.lean +++ b/generated/four_manifold_not_smooth/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Manifold ContDiff diff --git a/generated/four_manifold_not_smooth/Solution.lean b/generated/four_manifold_not_smooth/Solution.lean index 2bfbe575..b90c4998 100644 --- a/generated/four_manifold_not_smooth/Solution.lean +++ b/generated/four_manifold_not_smooth/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped Manifold ContDiff diff --git a/generated/four_manifold_not_smooth/Submission.lean b/generated/four_manifold_not_smooth/Submission.lean index 1efe2f01..6e23be62 100644 --- a/generated/four_manifold_not_smooth/Submission.lean +++ b/generated/four_manifold_not_smooth/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped Manifold ContDiff diff --git a/generated/fourier_dirichlet_fejer/ChallengeDeps.lean b/generated/fourier_dirichlet_fejer/ChallengeDeps.lean index 3dbedfdb..b3c3e0d3 100644 --- a/generated/fourier_dirichlet_fejer/ChallengeDeps.lean +++ b/generated/fourier_dirichlet_fejer/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/fraser_kakeya_fourier_decay/ChallengeDeps.lean b/generated/fraser_kakeya_fourier_decay/ChallengeDeps.lean index 190a865d..1de658fc 100644 --- a/generated/fraser_kakeya_fourier_decay/ChallengeDeps.lean +++ b/generated/fraser_kakeya_fourier_decay/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Combinatorics diff --git a/generated/friedlander_iwaniec/Challenge.lean b/generated/friedlander_iwaniec/Challenge.lean index 51a24343..cbd6293c 100644 --- a/generated/friedlander_iwaniec/Challenge.lean +++ b/generated/friedlander_iwaniec/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem friedlander_iwaniec : {p : β„• | p.Prime ∧ βˆƒ a b, p = a ^ 2 + b ^ 4}.Infinite := by sorry diff --git a/generated/friedlander_iwaniec/Solution.lean b/generated/friedlander_iwaniec/Solution.lean index 04c5a536..c2017dce 100644 --- a/generated/friedlander_iwaniec/Solution.lean +++ b/generated/friedlander_iwaniec/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem friedlander_iwaniec : {p : β„• | p.Prime ∧ βˆƒ a b, p = a ^ 2 + b ^ 4}.Infinite := by diff --git a/generated/friedlander_iwaniec/Submission.lean b/generated/friedlander_iwaniec/Submission.lean index e12c0f71..d66cfd88 100644 --- a/generated/friedlander_iwaniec/Submission.lean +++ b/generated/friedlander_iwaniec/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/frobenius_group_determinant/ChallengeDeps.lean b/generated/frobenius_group_determinant/ChallengeDeps.lean index 95336d45..b366074a 100644 --- a/generated/frobenius_group_determinant/ChallengeDeps.lean +++ b/generated/frobenius_group_determinant/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.RepresentationTheory.FrobeniusDeterminant diff --git a/generated/frobenius_kernel_isNormal/Challenge.lean b/generated/frobenius_kernel_isNormal/Challenge.lean index ad6bbee8..a0251fd0 100644 --- a/generated/frobenius_kernel_isNormal/Challenge.lean +++ b/generated/frobenius_kernel_isNormal/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem frobenius_kernel_isNormal (G X : Type) [Group G] [Fintype G] [Fintype X] [MulAction G X] [FaithfulSMul G X] diff --git a/generated/frobenius_kernel_isNormal/Solution.lean b/generated/frobenius_kernel_isNormal/Solution.lean index c91c3dba..6cfca4a5 100644 --- a/generated/frobenius_kernel_isNormal/Solution.lean +++ b/generated/frobenius_kernel_isNormal/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem frobenius_kernel_isNormal (G X : Type) [Group G] [Fintype G] [Fintype X] diff --git a/generated/frobenius_kernel_isNormal/Submission.lean b/generated/frobenius_kernel_isNormal/Submission.lean index 95100580..0e0fb265 100644 --- a/generated/frobenius_kernel_isNormal/Submission.lean +++ b/generated/frobenius_kernel_isNormal/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/fundamental_topos_theory/ChallengeDeps.lean b/generated/fundamental_topos_theory/ChallengeDeps.lean index 14788907..a01820b0 100644 --- a/generated/fundamental_topos_theory/ChallengeDeps.lean +++ b/generated/fundamental_topos_theory/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.ToposTheory diff --git a/generated/furstenberg_measure/Challenge.lean b/generated/furstenberg_measure/Challenge.lean index 91e9a48f..25d6f4d1 100644 --- a/generated/furstenberg_measure/Challenge.lean +++ b/generated/furstenberg_measure/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open MeasureTheory diff --git a/generated/furstenberg_measure/Solution.lean b/generated/furstenberg_measure/Solution.lean index 0b712670..95e2513c 100644 --- a/generated/furstenberg_measure/Solution.lean +++ b/generated/furstenberg_measure/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open MeasureTheory diff --git a/generated/furstenberg_measure/Submission.lean b/generated/furstenberg_measure/Submission.lean index c70dc0f5..6a902050 100644 --- a/generated/furstenberg_measure/Submission.lean +++ b/generated/furstenberg_measure/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open MeasureTheory diff --git a/generated/furstenberg_topological/ChallengeDeps.lean b/generated/furstenberg_topological/ChallengeDeps.lean index 92febd9f..98cc28b8 100644 --- a/generated/furstenberg_topological/ChallengeDeps.lean +++ b/generated/furstenberg_topological/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Dynamics diff --git a/generated/g2_irrep_tensor_square_decomp/ChallengeDeps.lean b/generated/g2_irrep_tensor_square_decomp/ChallengeDeps.lean index 76442236..2937c68b 100644 --- a/generated/g2_irrep_tensor_square_decomp/ChallengeDeps.lean +++ b/generated/g2_irrep_tensor_square_decomp/ChallengeDeps.lean @@ -5,9 +5,6 @@ import Mathlib.Algebra.Lie.Semisimple.Defs import Mathlib.Basic.Complex.Basic import Mathlib.LinearAlgebra.Dimension.Finrank import Mathlib.RingTheory.SimpleModule.Isotypic -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace RepresentationTheory diff --git a/generated/gauss_wantzel_constructible_polygon/ChallengeDeps.lean b/generated/gauss_wantzel_constructible_polygon/ChallengeDeps.lean index 53b0ae0a..83006d0f 100644 --- a/generated/gauss_wantzel_constructible_polygon/ChallengeDeps.lean +++ b/generated/gauss_wantzel_constructible_polygon/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.NumberTheory.GaussWantzel diff --git a/generated/glAction_range_eq_centralizer_symAction/ChallengeDeps.lean b/generated/glAction_range_eq_centralizer_symAction/ChallengeDeps.lean index 0bfc99cc..c1ef010b 100644 --- a/generated/glAction_range_eq_centralizer_symAction/ChallengeDeps.lean +++ b/generated/glAction_range_eq_centralizer_symAction/ChallengeDeps.lean @@ -2,9 +2,6 @@ import Mathlib.LinearAlgebra.TensorPower.Basic import Mathlib.LinearAlgebra.PiTensorProduct.Basic import Mathlib.Algebra.Algebra.Subalgebra.Centralizer import Mathlib.LinearAlgebra.FiniteDimensional.Defs -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace RepresentationTheory diff --git a/generated/glauberman_zStar/Challenge.lean b/generated/glauberman_zStar/Challenge.lean index 9fa72261..fb48f11f 100644 --- a/generated/glauberman_zStar/Challenge.lean +++ b/generated/glauberman_zStar/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem glauberman_zStar (G : Type) [Group G] [Fintype G] (t : G) (ht1 : t β‰  1) (ht2 : t * t = 1) diff --git a/generated/glauberman_zStar/Solution.lean b/generated/glauberman_zStar/Solution.lean index 63736b30..e14c5a4c 100644 --- a/generated/glauberman_zStar/Solution.lean +++ b/generated/glauberman_zStar/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem glauberman_zStar (G : Type) [Group G] [Fintype G] diff --git a/generated/glauberman_zStar/Submission.lean b/generated/glauberman_zStar/Submission.lean index 0aaab535..5caa5e53 100644 --- a/generated/glauberman_zStar/Submission.lean +++ b/generated/glauberman_zStar/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/gleason_theorem_finite/ChallengeDeps.lean b/generated/gleason_theorem_finite/ChallengeDeps.lean index 2e7f8eb3..967640a1 100644 --- a/generated/gleason_theorem_finite/ChallengeDeps.lean +++ b/generated/gleason_theorem_finite/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.InnerProductSpace.Positive import Mathlib.Analysis.InnerProductSpace.l2Space import Mathlib.LinearAlgebra.Trace -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/gleason_theorem_separable/ChallengeDeps.lean b/generated/gleason_theorem_separable/ChallengeDeps.lean index 74fd0085..2cbb262e 100644 --- a/generated/gleason_theorem_separable/ChallengeDeps.lean +++ b/generated/gleason_theorem_separable/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.InnerProductSpace.Positive import Mathlib.Analysis.InnerProductSpace.l2Space import Mathlib.LinearAlgebra.Trace -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/golod_shafarevich_inequality/ChallengeDeps.lean b/generated/golod_shafarevich_inequality/ChallengeDeps.lean index caddfb02..f8a83904 100644 --- a/generated/golod_shafarevich_inequality/ChallengeDeps.lean +++ b/generated/golod_shafarevich_inequality/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace GroupTheory diff --git a/generated/gorenstein_walter/Challenge.lean b/generated/gorenstein_walter/Challenge.lean index f10a5815..330e6b00 100644 --- a/generated/gorenstein_walter/Challenge.lean +++ b/generated/gorenstein_walter/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open scoped MatrixGroups diff --git a/generated/gorenstein_walter/Solution.lean b/generated/gorenstein_walter/Solution.lean index 170fa4e9..066369e8 100644 --- a/generated/gorenstein_walter/Solution.lean +++ b/generated/gorenstein_walter/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped MatrixGroups diff --git a/generated/gorenstein_walter/Submission.lean b/generated/gorenstein_walter/Submission.lean index 166154f7..d8912793 100644 --- a/generated/gorenstein_walter/Submission.lean +++ b/generated/gorenstein_walter/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped MatrixGroups diff --git a/generated/green_tao/ChallengeDeps.lean b/generated/green_tao/ChallengeDeps.lean index 00a58d35..3745b63a 100644 --- a/generated/green_tao/ChallengeDeps.lean +++ b/generated/green_tao/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace NumberTheory diff --git a/generated/hSpace_sphere_iff/Challenge.lean b/generated/hSpace_sphere_iff/Challenge.lean index 47b2d791..cb77dd0b 100644 --- a/generated/hSpace_sphere_iff/Challenge.lean +++ b/generated/hSpace_sphere_iff/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem hSpace_sphere_iff (n : β„•) : Nonempty (HSpace (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1)) ↔ diff --git a/generated/hSpace_sphere_iff/Solution.lean b/generated/hSpace_sphere_iff/Solution.lean index beb3e103..40845900 100644 --- a/generated/hSpace_sphere_iff/Solution.lean +++ b/generated/hSpace_sphere_iff/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem hSpace_sphere_iff (n : β„•) : diff --git a/generated/hSpace_sphere_iff/Submission.lean b/generated/hSpace_sphere_iff/Submission.lean index 1538d4dd..1b03f235 100644 --- a/generated/hSpace_sphere_iff/Submission.lean +++ b/generated/hSpace_sphere_iff/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/hadwiger/ChallengeDeps.lean b/generated/hadwiger/ChallengeDeps.lean index 01fcaf72..bb408fdf 100644 --- a/generated/hadwiger/ChallengeDeps.lean +++ b/generated/hadwiger/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace ConvexGeometry diff --git a/generated/halmos_generic_weak_mixing/ChallengeDeps.lean b/generated/halmos_generic_weak_mixing/ChallengeDeps.lean index b8689612..c6e29873 100644 --- a/generated/halmos_generic_weak_mixing/ChallengeDeps.lean +++ b/generated/halmos_generic_weak_mixing/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Dynamics diff --git a/generated/hausdorff_absolute_continuity/ChallengeDeps.lean b/generated/hausdorff_absolute_continuity/ChallengeDeps.lean index 6cf3e6d9..bfaa8ad1 100644 --- a/generated/hausdorff_absolute_continuity/ChallengeDeps.lean +++ b/generated/hausdorff_absolute_continuity/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Analysis.HausdorffAbsoluteContinuity diff --git a/generated/hausdorff_hildebrandt_schoenberg/ChallengeDeps.lean b/generated/hausdorff_hildebrandt_schoenberg/ChallengeDeps.lean index 8e713e3e..f5903aa8 100644 --- a/generated/hausdorff_hildebrandt_schoenberg/ChallengeDeps.lean +++ b/generated/hausdorff_hildebrandt_schoenberg/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/hausdorff_positivity_criterion/ChallengeDeps.lean b/generated/hausdorff_positivity_criterion/ChallengeDeps.lean index 7aca2386..38cb23bd 100644 --- a/generated/hausdorff_positivity_criterion/ChallengeDeps.lean +++ b/generated/hausdorff_positivity_criterion/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/heat_kernel_solves_heat_equation/ChallengeDeps.lean b/generated/heat_kernel_solves_heat_equation/ChallengeDeps.lean index 0e15c692..695c76ce 100644 --- a/generated/heat_kernel_solves_heat_equation/ChallengeDeps.lean +++ b/generated/heat_kernel_solves_heat_equation/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral import Mathlib.MeasureTheory.Integral.Bochner.Basic -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/higman_infinite_simple/Challenge.lean b/generated/higman_infinite_simple/Challenge.lean index cafb8a1d..b8e3a3ff 100644 --- a/generated/higman_infinite_simple/Challenge.lean +++ b/generated/higman_infinite_simple/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem higman_infinite_simple : βˆƒ (n : β„•) (rels : Set (FreeGroup (Fin n))), diff --git a/generated/higman_infinite_simple/Solution.lean b/generated/higman_infinite_simple/Solution.lean index 3ca07275..a04e4e4a 100644 --- a/generated/higman_infinite_simple/Solution.lean +++ b/generated/higman_infinite_simple/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem higman_infinite_simple : diff --git a/generated/higman_infinite_simple/Submission.lean b/generated/higman_infinite_simple/Submission.lean index 4479b622..ff954ac4 100644 --- a/generated/higman_infinite_simple/Submission.lean +++ b/generated/higman_infinite_simple/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/hilbert_smith_padic_dimension_three/Challenge.lean b/generated/hilbert_smith_padic_dimension_three/Challenge.lean index b0eb6dfe..40e99876 100644 --- a/generated/hilbert_smith_padic_dimension_three/Challenge.lean +++ b/generated/hilbert_smith_padic_dimension_three/Challenge.lean @@ -3,9 +3,6 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Geometry.Manifold.ChartedSpace import Mathlib.NumberTheory.Padics.PadicIntegers import Mathlib.Topology.Algebra.MulAction -import Lake.Toml -import Lake.Util.Message -import Lean theorem hilbert_smith_padic_dimension_three (p : β„•) [Fact p.Prime] (M : Type*) [TopologicalSpace M] [T2Space M] [SecondCountableTopology M] diff --git a/generated/hilbert_smith_padic_dimension_three/Solution.lean b/generated/hilbert_smith_padic_dimension_three/Solution.lean index a32d48ea..29e46fa2 100644 --- a/generated/hilbert_smith_padic_dimension_three/Solution.lean +++ b/generated/hilbert_smith_padic_dimension_three/Solution.lean @@ -3,9 +3,6 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Geometry.Manifold.ChartedSpace import Mathlib.NumberTheory.Padics.PadicIntegers import Mathlib.Topology.Algebra.MulAction -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem hilbert_smith_padic_dimension_three (p : β„•) [Fact p.Prime] diff --git a/generated/hilbert_smith_padic_dimension_three/Submission.lean b/generated/hilbert_smith_padic_dimension_three/Submission.lean index 8225aca3..b5ff6305 100644 --- a/generated/hilbert_smith_padic_dimension_three/Submission.lean +++ b/generated/hilbert_smith_padic_dimension_three/Submission.lean @@ -3,9 +3,6 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Geometry.Manifold.ChartedSpace import Mathlib.NumberTheory.Padics.PadicIntegers import Mathlib.Topology.Algebra.MulAction -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/hippocrates_lunes/ChallengeDeps.lean b/generated/hippocrates_lunes/ChallengeDeps.lean index 3bc0d61b..b7b8d59f 100644 --- a/generated/hippocrates_lunes/ChallengeDeps.lean +++ b/generated/hippocrates_lunes/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Geometry.HippocratesLunes diff --git a/generated/honeycomb_connective_constant/ChallengeDeps.lean b/generated/honeycomb_connective_constant/ChallengeDeps.lean index 9468c3ce..c04113fd 100644 --- a/generated/honeycomb_connective_constant/ChallengeDeps.lean +++ b/generated/honeycomb_connective_constant/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Combinatorics.HoneycombConnectiveConstant diff --git a/generated/hopf_rinow/ChallengeDeps.lean b/generated/hopf_rinow/ChallengeDeps.lean index 11acfc43..3a2cd178 100644 --- a/generated/hopf_rinow/ChallengeDeps.lean +++ b/generated/hopf_rinow/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Manifold ENNReal ContDiff open Bundle diff --git a/generated/hopf_umlaufsatz/ChallengeDeps.lean b/generated/hopf_umlaufsatz/ChallengeDeps.lean index 5b041d0c..18db89c4 100644 --- a/generated/hopf_umlaufsatz/ChallengeDeps.lean +++ b/generated/hopf_umlaufsatz/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Geometry.HopfUmlaufsatz diff --git a/generated/hurewicz_h1_abelianization/ChallengeDeps.lean b/generated/hurewicz_h1_abelianization/ChallengeDeps.lean index 85b0a027..35491169 100644 --- a/generated/hurewicz_h1_abelianization/ChallengeDeps.lean +++ b/generated/hurewicz_h1_abelianization/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Topology.Hurewicz diff --git a/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/Challenge.lean b/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/Challenge.lean index 71693e16..ac7624d3 100644 --- a/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/Challenge.lean +++ b/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/Challenge.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.Normed.Algebra.Spectrum import Mathlib.LinearAlgebra.Eigenspace.Basic import Mathlib.LinearAlgebra.Matrix.Irreducible.Defs -import Lake.Toml -import Lake.Util.Message -import Lean open scoped NNReal diff --git a/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/Solution.lean b/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/Solution.lean index 367fb8a9..ceea673b 100644 --- a/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/Solution.lean +++ b/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/Solution.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.Normed.Algebra.Spectrum import Mathlib.LinearAlgebra.Eigenspace.Basic import Mathlib.LinearAlgebra.Matrix.Irreducible.Defs -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped NNReal diff --git a/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/Submission.lean b/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/Submission.lean index b54333e1..89ca5058 100644 --- a/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/Submission.lean +++ b/generated/irreducible_nonnegative_matrix_has_positive_eigenvector_at_spectralRadius/Submission.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.Normed.Algebra.Spectrum import Mathlib.LinearAlgebra.Eigenspace.Basic import Mathlib.LinearAlgebra.Matrix.Irreducible.Defs -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped NNReal diff --git a/generated/ising_2d_phase_transition/ChallengeDeps.lean b/generated/ising_2d_phase_transition/ChallengeDeps.lean index dd573638..85a49c97 100644 --- a/generated/ising_2d_phase_transition/ChallengeDeps.lean +++ b/generated/ising_2d_phase_transition/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Analysis.IsingPhaseTransition diff --git a/generated/isoperimetric_inequality/ChallengeDeps.lean b/generated/isoperimetric_inequality/ChallengeDeps.lean index d37c534f..9f2fe740 100644 --- a/generated/isoperimetric_inequality/ChallengeDeps.lean +++ b/generated/isoperimetric_inequality/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/jacobian_challenge_alggeo/Challenge.lean b/generated/jacobian_challenge_alggeo/Challenge.lean index 8fc2986c..746752b8 100644 --- a/generated/jacobian_challenge_alggeo/Challenge.lean +++ b/generated/jacobian_challenge_alggeo/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean /- Copyright (c) 2026 Christian Merten. All rights reserved. diff --git a/generated/jordan_brouwer/Challenge.lean b/generated/jordan_brouwer/Challenge.lean index 8328fe46..83387dcf 100644 --- a/generated/jordan_brouwer/Challenge.lean +++ b/generated/jordan_brouwer/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem jordan_brouwer (d : β„•) (_hd : 2 ≀ d) (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin d)) 1 β†’ EuclideanSpace ℝ (Fin d)) diff --git a/generated/jordan_brouwer/Solution.lean b/generated/jordan_brouwer/Solution.lean index 6a2871c3..a5f36b38 100644 --- a/generated/jordan_brouwer/Solution.lean +++ b/generated/jordan_brouwer/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem jordan_brouwer (d : β„•) (_hd : 2 ≀ d) diff --git a/generated/jordan_brouwer/Submission.lean b/generated/jordan_brouwer/Submission.lean index fa71b500..8de98b26 100644 --- a/generated/jordan_brouwer/Submission.lean +++ b/generated/jordan_brouwer/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/jordan_curve/Challenge.lean b/generated/jordan_curve/Challenge.lean index 2c8ce28b..c905611a 100644 --- a/generated/jordan_curve/Challenge.lean +++ b/generated/jordan_curve/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem jordan_curve (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 β†’ EuclideanSpace ℝ (Fin 2)) (_hcont : Continuous r) (_hinj : Function.Injective r) : diff --git a/generated/jordan_curve/Solution.lean b/generated/jordan_curve/Solution.lean index 031f6bae..cbfe68cf 100644 --- a/generated/jordan_curve/Solution.lean +++ b/generated/jordan_curve/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem jordan_curve (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 β†’ EuclideanSpace ℝ (Fin 2)) diff --git a/generated/jordan_curve/Submission.lean b/generated/jordan_curve/Submission.lean index d58329bc..6234e34b 100644 --- a/generated/jordan_curve/Submission.lean +++ b/generated/jordan_curve/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/jordan_normal_form/ChallengeDeps.lean b/generated/jordan_normal_form/ChallengeDeps.lean index cc332a40..af4c1ac5 100644 --- a/generated/jordan_normal_form/ChallengeDeps.lean +++ b/generated/jordan_normal_form/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.LinearAlgebra.JordanNormalForm diff --git a/generated/kakutani_fixed_point/ChallengeDeps.lean b/generated/kakutani_fixed_point/ChallengeDeps.lean index 203119db..3bda7a3d 100644 --- a/generated/kakutani_fixed_point/ChallengeDeps.lean +++ b/generated/kakutani_fixed_point/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Topology diff --git a/generated/kam_invariant_curve/ChallengeDeps.lean b/generated/kam_invariant_curve/ChallengeDeps.lean index 8bd44740..a0d9e477 100644 --- a/generated/kam_invariant_curve/ChallengeDeps.lean +++ b/generated/kam_invariant_curve/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Dynamics diff --git a/generated/kepler_conjecture/ChallengeDeps.lean b/generated/kepler_conjecture/ChallengeDeps.lean index f224dbb6..7572e080 100644 --- a/generated/kepler_conjecture/ChallengeDeps.lean +++ b/generated/kepler_conjecture/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/kirk_normal_structure/ChallengeDeps.lean b/generated/kirk_normal_structure/ChallengeDeps.lean index 0ad11d92..46c39e94 100644 --- a/generated/kirk_normal_structure/ChallengeDeps.lean +++ b/generated/kirk_normal_structure/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Topology.KirkNormalStructure diff --git a/generated/klartag_packing/Challenge.lean b/generated/klartag_packing/Challenge.lean index 2c949423..9ebf368b 100644 --- a/generated/klartag_packing/Challenge.lean +++ b/generated/klartag_packing/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem klartag_packing : βˆƒ c : ℝ, 0 < c ∧ βˆ€ n : β„•, let V := EuclideanSpace ℝ (Fin (n + 1)) diff --git a/generated/klartag_packing/Solution.lean b/generated/klartag_packing/Solution.lean index 7eb19de9..2e077d70 100644 --- a/generated/klartag_packing/Solution.lean +++ b/generated/klartag_packing/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem klartag_packing : βˆƒ c : ℝ, 0 < c ∧ βˆ€ n : β„•, diff --git a/generated/klartag_packing/Submission.lean b/generated/klartag_packing/Submission.lean index 3b57416b..5a5f70a1 100644 --- a/generated/klartag_packing/Submission.lean +++ b/generated/klartag_packing/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/kollar_lieblich_olsson_sawin/ChallengeDeps.lean b/generated/kollar_lieblich_olsson_sawin/ChallengeDeps.lean index 46366186..6b06193a 100644 --- a/generated/kollar_lieblich_olsson_sawin/ChallengeDeps.lean +++ b/generated/kollar_lieblich_olsson_sawin/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Topological reconstruction theorems for varieties diff --git a/generated/kolmogorov_arnold_superposition/Challenge.lean b/generated/kolmogorov_arnold_superposition/Challenge.lean index f190e199..2865a741 100644 --- a/generated/kolmogorov_arnold_superposition/Challenge.lean +++ b/generated/kolmogorov_arnold_superposition/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open scoped BigOperators diff --git a/generated/kolmogorov_arnold_superposition/Solution.lean b/generated/kolmogorov_arnold_superposition/Solution.lean index 4e37ba27..7929608b 100644 --- a/generated/kolmogorov_arnold_superposition/Solution.lean +++ b/generated/kolmogorov_arnold_superposition/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped BigOperators diff --git a/generated/kolmogorov_arnold_superposition/Submission.lean b/generated/kolmogorov_arnold_superposition/Submission.lean index 3f400ed1..74b5dba9 100644 --- a/generated/kolmogorov_arnold_superposition/Submission.lean +++ b/generated/kolmogorov_arnold_superposition/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped BigOperators diff --git a/generated/koszul_formula/ChallengeDeps.lean b/generated/koszul_formula/ChallengeDeps.lean index 51e33389..9f236f44 100644 --- a/generated/koszul_formula/ChallengeDeps.lean +++ b/generated/koszul_formula/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/landsberg_schaar/ChallengeDeps.lean b/generated/landsberg_schaar/ChallengeDeps.lean index 916acccc..deadd834 100644 --- a/generated/landsberg_schaar/ChallengeDeps.lean +++ b/generated/landsberg_schaar/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.NumberTheory.LandsbergSchaar diff --git a/generated/lax_approximation/ChallengeDeps.lean b/generated/lax_approximation/ChallengeDeps.lean index b62c70c6..8f668f70 100644 --- a/generated/lax_approximation/ChallengeDeps.lean +++ b/generated/lax_approximation/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Dynamics.LaxApproximation diff --git a/generated/levi_civita_exists_unique/ChallengeDeps.lean b/generated/levi_civita_exists_unique/ChallengeDeps.lean index ce07febb..80f578ea 100644 --- a/generated/levi_civita_exists_unique/ChallengeDeps.lean +++ b/generated/levi_civita_exists_unique/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/lidskii_inequality/Challenge.lean b/generated/lidskii_inequality/Challenge.lean index 966f763a..0b2f70a0 100644 --- a/generated/lidskii_inequality/Challenge.lean +++ b/generated/lidskii_inequality/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Matrix diff --git a/generated/lidskii_inequality/Solution.lean b/generated/lidskii_inequality/Solution.lean index 135295e9..1cc89b25 100644 --- a/generated/lidskii_inequality/Solution.lean +++ b/generated/lidskii_inequality/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Matrix diff --git a/generated/lidskii_inequality/Submission.lean b/generated/lidskii_inequality/Submission.lean index c9b3e3ae..65d31fcd 100644 --- a/generated/lidskii_inequality/Submission.lean +++ b/generated/lidskii_inequality/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Matrix diff --git a/generated/lidskii_last/Challenge.lean b/generated/lidskii_last/Challenge.lean index 9552ea6f..9d1f2db3 100644 --- a/generated/lidskii_last/Challenge.lean +++ b/generated/lidskii_last/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Matrix diff --git a/generated/lidskii_last/Solution.lean b/generated/lidskii_last/Solution.lean index 70a3f94d..5f4d7bd1 100644 --- a/generated/lidskii_last/Solution.lean +++ b/generated/lidskii_last/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Matrix diff --git a/generated/lidskii_last/Submission.lean b/generated/lidskii_last/Submission.lean index 0adaceea..b82027f7 100644 --- a/generated/lidskii_last/Submission.lean +++ b/generated/lidskii_last/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Matrix diff --git a/generated/lindemann/Challenge.lean b/generated/lindemann/Challenge.lean index 088a4502..35fafdcf 100644 --- a/generated/lindemann/Challenge.lean +++ b/generated/lindemann/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Polynomial diff --git a/generated/lindemann/Solution.lean b/generated/lindemann/Solution.lean index ff0ffc7d..08de169d 100644 --- a/generated/lindemann/Solution.lean +++ b/generated/lindemann/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Polynomial diff --git a/generated/lindemann/Submission.lean b/generated/lindemann/Submission.lean index bc41b594..74334a13 100644 --- a/generated/lindemann/Submission.lean +++ b/generated/lindemann/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Polynomial diff --git a/generated/lindemann_weierstrass/Challenge.lean b/generated/lindemann_weierstrass/Challenge.lean index 62bfafd3..8020f424 100644 --- a/generated/lindemann_weierstrass/Challenge.lean +++ b/generated/lindemann_weierstrass/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Polynomial diff --git a/generated/lindemann_weierstrass/Solution.lean b/generated/lindemann_weierstrass/Solution.lean index 007cbe92..8ce91242 100644 --- a/generated/lindemann_weierstrass/Solution.lean +++ b/generated/lindemann_weierstrass/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Polynomial diff --git a/generated/lindemann_weierstrass/Submission.lean b/generated/lindemann_weierstrass/Submission.lean index 31a00574..48d1f22b 100644 --- a/generated/lindemann_weierstrass/Submission.lean +++ b/generated/lindemann_weierstrass/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Polynomial diff --git a/generated/linear_ode_asymptotic_stability/Challenge.lean b/generated/linear_ode_asymptotic_stability/Challenge.lean index 723dd078..5ca2899e 100644 --- a/generated/linear_ode_asymptotic_stability/Challenge.lean +++ b/generated/linear_ode_asymptotic_stability/Challenge.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Analysis.Calculus.FDeriv.Basic import Mathlib.Analysis.Normed.Algebra.MatrixExponential import Mathlib.LinearAlgebra.Eigenspace.Basic -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Matrix diff --git a/generated/linear_ode_asymptotic_stability/Solution.lean b/generated/linear_ode_asymptotic_stability/Solution.lean index 0bb4c9e1..e5e1297f 100644 --- a/generated/linear_ode_asymptotic_stability/Solution.lean +++ b/generated/linear_ode_asymptotic_stability/Solution.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Analysis.Calculus.FDeriv.Basic import Mathlib.Analysis.Normed.Algebra.MatrixExponential import Mathlib.LinearAlgebra.Eigenspace.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped Matrix diff --git a/generated/linear_ode_asymptotic_stability/Submission.lean b/generated/linear_ode_asymptotic_stability/Submission.lean index 1433ec6d..e55d98a1 100644 --- a/generated/linear_ode_asymptotic_stability/Submission.lean +++ b/generated/linear_ode_asymptotic_stability/Submission.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Analysis.Calculus.FDeriv.Basic import Mathlib.Analysis.Normed.Algebra.MatrixExponential import Mathlib.LinearAlgebra.Eigenspace.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped Matrix diff --git a/generated/linnik/ChallengeDeps.lean b/generated/linnik/ChallengeDeps.lean index 6338a8a1..72dd72d4 100644 --- a/generated/linnik/ChallengeDeps.lean +++ b/generated/linnik/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.NumberTheory.Linnik diff --git a/generated/liouville_arnold/ChallengeDeps.lean b/generated/liouville_arnold/ChallengeDeps.lean index cc43e38e..802c7138 100644 --- a/generated/liouville_arnold/ChallengeDeps.lean +++ b/generated/liouville_arnold/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/list_append_singleton_length/Challenge.lean b/generated/list_append_singleton_length/Challenge.lean index bd4ead51..fc0de12b 100644 --- a/generated/list_append_singleton_length/Challenge.lean +++ b/generated/list_append_singleton_length/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem list_append_singleton_length : (([1, 2] : List Nat).append [3]).length = 3 := by diff --git a/generated/list_append_singleton_length/Solution.lean b/generated/list_append_singleton_length/Solution.lean index 1d56834f..d0403722 100644 --- a/generated/list_append_singleton_length/Solution.lean +++ b/generated/list_append_singleton_length/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem list_append_singleton_length : diff --git a/generated/list_append_singleton_length/Submission.lean b/generated/list_append_singleton_length/Submission.lean index 524dcfdc..ca2da421 100644 --- a/generated/list_append_singleton_length/Submission.lean +++ b/generated/list_append_singleton_length/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/lp_maximum_principle/ChallengeDeps.lean b/generated/lp_maximum_principle/ChallengeDeps.lean index 2915c860..002042c2 100644 --- a/generated/lp_maximum_principle/ChallengeDeps.lean +++ b/generated/lp_maximum_principle/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace ConvexGeometry diff --git a/generated/m23_irrep_tensor_square_decomp/Challenge.lean b/generated/m23_irrep_tensor_square_decomp/Challenge.lean index 29bb8231..0b2a318b 100644 --- a/generated/m23_irrep_tensor_square_decomp/Challenge.lean +++ b/generated/m23_irrep_tensor_square_decomp/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open scoped TensorProduct diff --git a/generated/m23_irrep_tensor_square_decomp/Solution.lean b/generated/m23_irrep_tensor_square_decomp/Solution.lean index ce6dc34c..af03a20a 100644 --- a/generated/m23_irrep_tensor_square_decomp/Solution.lean +++ b/generated/m23_irrep_tensor_square_decomp/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped TensorProduct diff --git a/generated/m23_irrep_tensor_square_decomp/Submission.lean b/generated/m23_irrep_tensor_square_decomp/Submission.lean index f46c4a70..c278a593 100644 --- a/generated/m23_irrep_tensor_square_decomp/Submission.lean +++ b/generated/m23_irrep_tensor_square_decomp/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped TensorProduct diff --git a/generated/mandelbar_not_path_connected/ChallengeDeps.lean b/generated/mandelbar_not_path_connected/ChallengeDeps.lean index d024403c..d2c638b6 100644 --- a/generated/mandelbar_not_path_connected/ChallengeDeps.lean +++ b/generated/mandelbar_not_path_connected/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace ComplexAnalysis diff --git a/generated/mandelbrot_boundary_dimh/ChallengeDeps.lean b/generated/mandelbrot_boundary_dimh/ChallengeDeps.lean index 7ce608e3..b6035199 100644 --- a/generated/mandelbrot_boundary_dimh/ChallengeDeps.lean +++ b/generated/mandelbrot_boundary_dimh/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Dynamics.MandelbrotBoundary diff --git a/generated/mandelbrot_connected/ChallengeDeps.lean b/generated/mandelbrot_connected/ChallengeDeps.lean index ddf678ee..1a2ba68e 100644 --- a/generated/mandelbrot_connected/ChallengeDeps.lean +++ b/generated/mandelbrot_connected/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace ComplexAnalysis diff --git a/generated/manolescu_triangulation_disproof/ChallengeDeps.lean b/generated/manolescu_triangulation_disproof/ChallengeDeps.lean index 558a95db..c07de8cc 100644 --- a/generated/manolescu_triangulation_disproof/ChallengeDeps.lean +++ b/generated/manolescu_triangulation_disproof/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Geometry diff --git a/generated/margulis_ruelle/ChallengeDeps.lean b/generated/margulis_ruelle/ChallengeDeps.lean index b5bb297d..004622f8 100644 --- a/generated/margulis_ruelle/ChallengeDeps.lean +++ b/generated/margulis_ruelle/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Dynamics diff --git a/generated/martinet_totally_real_towers/Challenge.lean b/generated/martinet_totally_real_towers/Challenge.lean index 20d23448..b2379784 100644 --- a/generated/martinet_totally_real_towers/Challenge.lean +++ b/generated/martinet_totally_real_towers/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open NumberField diff --git a/generated/martinet_totally_real_towers/Solution.lean b/generated/martinet_totally_real_towers/Solution.lean index b564de78..7c886216 100644 --- a/generated/martinet_totally_real_towers/Solution.lean +++ b/generated/martinet_totally_real_towers/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open NumberField diff --git a/generated/martinet_totally_real_towers/Submission.lean b/generated/martinet_totally_real_towers/Submission.lean index e3c5e06e..6f83b3dc 100644 --- a/generated/martinet_totally_real_towers/Submission.lean +++ b/generated/martinet_totally_real_towers/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open NumberField diff --git a/generated/mazur_torsion/ChallengeDeps.lean b/generated/mazur_torsion/ChallengeDeps.lean index 27068435..d6b59fb9 100644 --- a/generated/mazur_torsion/ChallengeDeps.lean +++ b/generated/mazur_torsion/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.NumberTheory.MazurTorsion diff --git a/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/Challenge.lean b/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/Challenge.lean index c92c03ad..22538527 100644 --- a/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/Challenge.lean +++ b/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/Challenge.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Convex.Caratheodory import Mathlib.Analysis.Convex.KreinMilman -import Lake.Toml -import Lake.Util.Message -import Lean open Set diff --git a/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/Solution.lean b/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/Solution.lean index d7e05191..a5abab0d 100644 --- a/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/Solution.lean +++ b/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/Solution.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Convex.Caratheodory import Mathlib.Analysis.Convex.KreinMilman -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Set diff --git a/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/Submission.lean b/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/Submission.lean index 1d94f8be..bf790923 100644 --- a/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/Submission.lean +++ b/generated/mem_convexHull_finset_extremePoints_of_mem_compact_convex/Submission.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Convex.Caratheodory import Mathlib.Analysis.Convex.KreinMilman -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Set diff --git a/generated/mergelyan_theorem/Challenge.lean b/generated/mergelyan_theorem/Challenge.lean index 7556c20f..61b91ae8 100644 --- a/generated/mergelyan_theorem/Challenge.lean +++ b/generated/mergelyan_theorem/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Polynomial diff --git a/generated/mergelyan_theorem/Solution.lean b/generated/mergelyan_theorem/Solution.lean index f8db664c..035044b5 100644 --- a/generated/mergelyan_theorem/Solution.lean +++ b/generated/mergelyan_theorem/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped Polynomial diff --git a/generated/mergelyan_theorem/Submission.lean b/generated/mergelyan_theorem/Submission.lean index e8f973b2..381ed8d3 100644 --- a/generated/mergelyan_theorem/Submission.lean +++ b/generated/mergelyan_theorem/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped Polynomial diff --git a/generated/mihailescu/Challenge.lean b/generated/mihailescu/Challenge.lean index 297c61a5..a83654b2 100644 --- a/generated/mihailescu/Challenge.lean +++ b/generated/mihailescu/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem mihailescu {x y m n : β„•} (hx : 0 < x) (hy : 0 < y) (hm : 1 < m) (hn : 1 < n) diff --git a/generated/mihailescu/Solution.lean b/generated/mihailescu/Solution.lean index 5c975096..9095f901 100644 --- a/generated/mihailescu/Solution.lean +++ b/generated/mihailescu/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem mihailescu {x y m n : β„•} diff --git a/generated/mihailescu/Submission.lean b/generated/mihailescu/Submission.lean index bfc88f65..36236858 100644 --- a/generated/mihailescu/Submission.lean +++ b/generated/mihailescu/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/milnor_exotic_sphere_seven/Challenge.lean b/generated/milnor_exotic_sphere_seven/Challenge.lean index 9f0e9af6..6bed0bee 100644 --- a/generated/milnor_exotic_sphere_seven/Challenge.lean +++ b/generated/milnor_exotic_sphere_seven/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Manifold ContDiff open Metric (sphere) diff --git a/generated/milnor_exotic_sphere_seven/Solution.lean b/generated/milnor_exotic_sphere_seven/Solution.lean index 80add296..c7da6b42 100644 --- a/generated/milnor_exotic_sphere_seven/Solution.lean +++ b/generated/milnor_exotic_sphere_seven/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped Manifold ContDiff diff --git a/generated/milnor_exotic_sphere_seven/Submission.lean b/generated/milnor_exotic_sphere_seven/Submission.lean index 0d823bf4..a535504e 100644 --- a/generated/milnor_exotic_sphere_seven/Submission.lean +++ b/generated/milnor_exotic_sphere_seven/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped Manifold ContDiff diff --git a/generated/monge_kantorovich/ChallengeDeps.lean b/generated/monge_kantorovich/ChallengeDeps.lean index 54ed58fa..027df424 100644 --- a/generated/monge_kantorovich/ChallengeDeps.lean +++ b/generated/monge_kantorovich/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/moran_equality_affine/ChallengeDeps.lean b/generated/moran_equality_affine/ChallengeDeps.lean index 9f8a6a5e..77698055 100644 --- a/generated/moran_equality_affine/ChallengeDeps.lean +++ b/generated/moran_equality_affine/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Dynamics diff --git a/generated/morley_categoricity_theorem/Challenge.lean b/generated/morley_categoricity_theorem/Challenge.lean index 4840758b..f36848c1 100644 --- a/generated/morley_categoricity_theorem/Challenge.lean +++ b/generated/morley_categoricity_theorem/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib.ModelTheory.Satisfiability -import Lake.Toml -import Lake.Util.Message -import Lean open Cardinal diff --git a/generated/morley_categoricity_theorem/Solution.lean b/generated/morley_categoricity_theorem/Solution.lean index db486f02..1408d764 100644 --- a/generated/morley_categoricity_theorem/Solution.lean +++ b/generated/morley_categoricity_theorem/Solution.lean @@ -1,7 +1,4 @@ import Mathlib.ModelTheory.Satisfiability -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Cardinal diff --git a/generated/morley_categoricity_theorem/Submission.lean b/generated/morley_categoricity_theorem/Submission.lean index c320fc4b..b64fe23b 100644 --- a/generated/morley_categoricity_theorem/Submission.lean +++ b/generated/morley_categoricity_theorem/Submission.lean @@ -1,7 +1,4 @@ import Mathlib.ModelTheory.Satisfiability -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Cardinal diff --git a/generated/morley_theorem/ChallengeDeps.lean b/generated/morley_theorem/ChallengeDeps.lean index 2e7995cb..bed9568f 100644 --- a/generated/morley_theorem/ChallengeDeps.lean +++ b/generated/morley_theorem/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Geometry.Morley diff --git a/generated/morse_inequality/ChallengeDeps.lean b/generated/morse_inequality/ChallengeDeps.lean index 22be0dbc..e366e849 100644 --- a/generated/morse_inequality/ChallengeDeps.lean +++ b/generated/morse_inequality/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/mostow_rigidity/ChallengeDeps.lean b/generated/mostow_rigidity/ChallengeDeps.lean index 937dbe1f..7a09dedf 100644 --- a/generated/mostow_rigidity/ChallengeDeps.lean +++ b/generated/mostow_rigidity/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Mostow rigidity diff --git a/generated/mountain_pass/ChallengeDeps.lean b/generated/mountain_pass/ChallengeDeps.lean index 4e1dad01..24f8af3c 100644 --- a/generated/mountain_pass/ChallengeDeps.lean +++ b/generated/mountain_pass/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/mulCayley_connected_iff_closure_eq_top/Challenge.lean b/generated/mulCayley_connected_iff_closure_eq_top/Challenge.lean index 36551081..5cf69627 100644 --- a/generated/mulCayley_connected_iff_closure_eq_top/Challenge.lean +++ b/generated/mulCayley_connected_iff_closure_eq_top/Challenge.lean @@ -1,9 +1,6 @@ import Mathlib.Combinatorics.SimpleGraph.Cayley import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected import Mathlib.Algebra.Group.Subgroup.Lattice -import Lake.Toml -import Lake.Util.Message -import Lean theorem mulCayley_connected_iff_closure_eq_top {G : Type*} [Group G] (S : Set G) : diff --git a/generated/mulCayley_connected_iff_closure_eq_top/Solution.lean b/generated/mulCayley_connected_iff_closure_eq_top/Solution.lean index 55864e39..793f79b1 100644 --- a/generated/mulCayley_connected_iff_closure_eq_top/Solution.lean +++ b/generated/mulCayley_connected_iff_closure_eq_top/Solution.lean @@ -1,9 +1,6 @@ import Mathlib.Combinatorics.SimpleGraph.Cayley import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected import Mathlib.Algebra.Group.Subgroup.Lattice -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem mulCayley_connected_iff_closure_eq_top {G : Type*} [Group G] diff --git a/generated/mulCayley_connected_iff_closure_eq_top/Submission.lean b/generated/mulCayley_connected_iff_closure_eq_top/Submission.lean index 23e146cd..ce32ff79 100644 --- a/generated/mulCayley_connected_iff_closure_eq_top/Submission.lean +++ b/generated/mulCayley_connected_iff_closure_eq_top/Submission.lean @@ -1,9 +1,6 @@ import Mathlib.Combinatorics.SimpleGraph.Cayley import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected import Mathlib.Algebra.Group.Subgroup.Lattice -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/multi_hole_helpers_example/ChallengeDeps.lean b/generated/multi_hole_helpers_example/ChallengeDeps.lean index de307c57..a0a46503 100644 --- a/generated/multi_hole_helpers_example/ChallengeDeps.lean +++ b/generated/multi_hole_helpers_example/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean /-! Regression test for the multi-hole / trusted-helpers pipeline. Exercises diff --git a/generated/nash_equilibrium_exists/ChallengeDeps.lean b/generated/nash_equilibrium_exists/ChallengeDeps.lean index 62fb2cec..10ab3c1c 100644 --- a/generated/nash_equilibrium_exists/ChallengeDeps.lean +++ b/generated/nash_equilibrium_exists/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace GameTheory diff --git a/generated/neukirch_uchida/Challenge.lean b/generated/neukirch_uchida/Challenge.lean index 3c0cf0aa..0132ccde 100644 --- a/generated/neukirch_uchida/Challenge.lean +++ b/generated/neukirch_uchida/Challenge.lean @@ -1,8 +1,5 @@ import Mathlib.FieldTheory.KrullTopology import Mathlib.NumberTheory.NumberField.Basic -import Lake.Toml -import Lake.Util.Message -import Lean theorem neukirch_uchida {K₁ Kβ‚‚ K₁' Kβ‚‚' : Type*} [Field K₁] [Field Kβ‚‚] [Field K₁'] [Field Kβ‚‚'] [NumberField K₁] [NumberField Kβ‚‚] [Algebra K₁ K₁'] [Algebra Kβ‚‚ Kβ‚‚'] [IsSepClosure K₁ K₁'] diff --git a/generated/neukirch_uchida/Solution.lean b/generated/neukirch_uchida/Solution.lean index 0cc8cf50..687ef929 100644 --- a/generated/neukirch_uchida/Solution.lean +++ b/generated/neukirch_uchida/Solution.lean @@ -1,8 +1,5 @@ import Mathlib.FieldTheory.KrullTopology import Mathlib.NumberTheory.NumberField.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem neukirch_uchida {K₁ Kβ‚‚ K₁' Kβ‚‚' : Type*} [Field K₁] [Field Kβ‚‚] [Field K₁'] [Field Kβ‚‚'] diff --git a/generated/neukirch_uchida/Submission.lean b/generated/neukirch_uchida/Submission.lean index 9d3dfb3a..f54c4e35 100644 --- a/generated/neukirch_uchida/Submission.lean +++ b/generated/neukirch_uchida/Submission.lean @@ -1,8 +1,5 @@ import Mathlib.FieldTheory.KrullTopology import Mathlib.NumberTheory.NumberField.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/newlander_nirenberg/ChallengeDeps.lean b/generated/newlander_nirenberg/ChallengeDeps.lean index 615cdef7..50129b3f 100644 --- a/generated/newlander_nirenberg/ChallengeDeps.lean +++ b/generated/newlander_nirenberg/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/nikolov_segal/ChallengeDeps.lean b/generated/nikolov_segal/ChallengeDeps.lean index 7fe4eb3f..360e814b 100644 --- a/generated/nikolov_segal/ChallengeDeps.lean +++ b/generated/nikolov_segal/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace GroupTheory diff --git a/generated/nonlinear_three_manifold_group/ChallengeDeps.lean b/generated/nonlinear_three_manifold_group/ChallengeDeps.lean index fd5b02d6..0559ce0a 100644 --- a/generated/nonlinear_three_manifold_group/ChallengeDeps.lean +++ b/generated/nonlinear_three_manifold_group/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Topology diff --git a/generated/normal_spectral_theorem/Challenge.lean b/generated/normal_spectral_theorem/Challenge.lean index a75e0c24..58926ea2 100644 --- a/generated/normal_spectral_theorem/Challenge.lean +++ b/generated/normal_spectral_theorem/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Matrix diff --git a/generated/normal_spectral_theorem/Solution.lean b/generated/normal_spectral_theorem/Solution.lean index 34f92e18..ef0d4b83 100644 --- a/generated/normal_spectral_theorem/Solution.lean +++ b/generated/normal_spectral_theorem/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Matrix diff --git a/generated/normal_spectral_theorem/Submission.lean b/generated/normal_spectral_theorem/Submission.lean index b9105496..beb5181f 100644 --- a/generated/normal_spectral_theorem/Submission.lean +++ b/generated/normal_spectral_theorem/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Matrix diff --git a/generated/novikov_unsolvable/ChallengeDeps.lean b/generated/novikov_unsolvable/ChallengeDeps.lean index 1e7ac5a1..e1cf25c5 100644 --- a/generated/novikov_unsolvable/ChallengeDeps.lean +++ b/generated/novikov_unsolvable/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace GroupTheory diff --git a/generated/nyquist_shannon_sampling/ChallengeDeps.lean b/generated/nyquist_shannon_sampling/ChallengeDeps.lean index b9b5fd41..7514e996 100644 --- a/generated/nyquist_shannon_sampling/ChallengeDeps.lean +++ b/generated/nyquist_shannon_sampling/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Analysis.NyquistShannon diff --git a/generated/oppenheim_inequality/Challenge.lean b/generated/oppenheim_inequality/Challenge.lean index 76efb744..e8b5cb16 100644 --- a/generated/oppenheim_inequality/Challenge.lean +++ b/generated/oppenheim_inequality/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Matrix.Order -import Lake.Toml -import Lake.Util.Message -import Lean open scoped MatrixOrder Matrix diff --git a/generated/oppenheim_inequality/Solution.lean b/generated/oppenheim_inequality/Solution.lean index 914a9e90..6f314ba3 100644 --- a/generated/oppenheim_inequality/Solution.lean +++ b/generated/oppenheim_inequality/Solution.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Matrix.Order -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped MatrixOrder Matrix diff --git a/generated/oppenheim_inequality/Submission.lean b/generated/oppenheim_inequality/Submission.lean index c3a162e7..4f26dbf9 100644 --- a/generated/oppenheim_inequality/Submission.lean +++ b/generated/oppenheim_inequality/Submission.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Matrix.Order -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped MatrixOrder Matrix diff --git a/generated/ore_conjecture/Challenge.lean b/generated/ore_conjecture/Challenge.lean index 3db44efa..06f16894 100644 --- a/generated/ore_conjecture/Challenge.lean +++ b/generated/ore_conjecture/Challenge.lean @@ -1,9 +1,6 @@ import Mathlib.Basic.Finite.Defs import Mathlib.GroupTheory.Commutator.Basic import Mathlib.GroupTheory.Subgroup.Simple -import Lake.Toml -import Lake.Util.Message -import Lean theorem ore_conjecture (G : Type*) [Group G] [Finite G] [IsSimpleGroup G] (hG : Β¬ IsMulCommutative G) : diff --git a/generated/ore_conjecture/Solution.lean b/generated/ore_conjecture/Solution.lean index 679a664a..673d996c 100644 --- a/generated/ore_conjecture/Solution.lean +++ b/generated/ore_conjecture/Solution.lean @@ -1,9 +1,6 @@ import Mathlib.Basic.Finite.Defs import Mathlib.GroupTheory.Commutator.Basic import Mathlib.GroupTheory.Subgroup.Simple -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem ore_conjecture (G : Type*) [Group G] [Finite G] [IsSimpleGroup G] diff --git a/generated/ore_conjecture/Submission.lean b/generated/ore_conjecture/Submission.lean index a7a3c61c..6562d7d7 100644 --- a/generated/ore_conjecture/Submission.lean +++ b/generated/ore_conjecture/Submission.lean @@ -1,9 +1,6 @@ import Mathlib.Basic.Finite.Defs import Mathlib.GroupTheory.Commutator.Basic import Mathlib.GroupTheory.Subgroup.Simple -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/ornstein_weiss_rokhlin/ChallengeDeps.lean b/generated/ornstein_weiss_rokhlin/ChallengeDeps.lean index 2692884c..e36dbe38 100644 --- a/generated/ornstein_weiss_rokhlin/ChallengeDeps.lean +++ b/generated/ornstein_weiss_rokhlin/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Dynamics diff --git a/generated/parallel_postulate_independent/ChallengeDeps.lean b/generated/parallel_postulate_independent/ChallengeDeps.lean index 02aa11a2..ab2fbbe2 100644 --- a/generated/parallel_postulate_independent/ChallengeDeps.lean +++ b/generated/parallel_postulate_independent/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib.Data.Set.Basic -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/pardon_torus_knot_distortion/ChallengeDeps.lean b/generated/pardon_torus_knot_distortion/ChallengeDeps.lean index 7bcd8009..7b6d98a9 100644 --- a/generated/pardon_torus_knot_distortion/ChallengeDeps.lean +++ b/generated/pardon_torus_knot_distortion/ChallengeDeps.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Calculus.ContDiff.Basic import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace KnotTheory diff --git a/generated/pascal/ChallengeDeps.lean b/generated/pascal/ChallengeDeps.lean index 9b2b5d98..b2ce7e6f 100644 --- a/generated/pascal/ChallengeDeps.lean +++ b/generated/pascal/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Geometry.PascalPappus diff --git a/generated/peano_existence/Challenge.lean b/generated/peano_existence/Challenge.lean index 2e783352..ceba3b4e 100644 --- a/generated/peano_existence/Challenge.lean +++ b/generated/peano_existence/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Set open scoped NNReal diff --git a/generated/peano_existence/Solution.lean b/generated/peano_existence/Solution.lean index b47daef8..40d56c6f 100644 --- a/generated/peano_existence/Solution.lean +++ b/generated/peano_existence/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Set diff --git a/generated/peano_existence/Submission.lean b/generated/peano_existence/Submission.lean index c5c66006..8da5d949 100644 --- a/generated/peano_existence/Submission.lean +++ b/generated/peano_existence/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Set diff --git a/generated/pell_solution_convergent/Challenge.lean b/generated/pell_solution_convergent/Challenge.lean index 08ea4f05..6eae134a 100644 --- a/generated/pell_solution_convergent/Challenge.lean +++ b/generated/pell_solution_convergent/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Real diff --git a/generated/pell_solution_convergent/Solution.lean b/generated/pell_solution_convergent/Solution.lean index 42f8c708..34bd2545 100644 --- a/generated/pell_solution_convergent/Solution.lean +++ b/generated/pell_solution_convergent/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped Real diff --git a/generated/pell_solution_convergent/Submission.lean b/generated/pell_solution_convergent/Submission.lean index cb4fd8bb..88c52066 100644 --- a/generated/pell_solution_convergent/Submission.lean +++ b/generated/pell_solution_convergent/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped Real diff --git a/generated/permute_to_unimodal/ChallengeDeps.lean b/generated/permute_to_unimodal/ChallengeDeps.lean index 7e4a374a..bd1864b6 100644 --- a/generated/permute_to_unimodal/ChallengeDeps.lean +++ b/generated/permute_to_unimodal/ChallengeDeps.lean @@ -1,6 +1,3 @@ -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace ProgramVerification diff --git a/generated/pesin_formula/ChallengeDeps.lean b/generated/pesin_formula/ChallengeDeps.lean index 810bfa5a..c0af2583 100644 --- a/generated/pesin_formula/ChallengeDeps.lean +++ b/generated/pesin_formula/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Dynamics diff --git a/generated/pi1_circle_mulEquiv_int/Challenge.lean b/generated/pi1_circle_mulEquiv_int/Challenge.lean index 97bdc286..e52d37fe 100644 --- a/generated/pi1_circle_mulEquiv_int/Challenge.lean +++ b/generated/pi1_circle_mulEquiv_int/Challenge.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Complex.Circle import Mathlib.Data.ZMod.Basic import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Topology.Homotopy.HomotopyGroup -import Lake.Toml -import Lake.Util.Message -import Lean theorem pi1_circle_mulEquiv_int : Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative β„€) := by diff --git a/generated/pi1_circle_mulEquiv_int/Solution.lean b/generated/pi1_circle_mulEquiv_int/Solution.lean index 07941a1c..03058f53 100644 --- a/generated/pi1_circle_mulEquiv_int/Solution.lean +++ b/generated/pi1_circle_mulEquiv_int/Solution.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Complex.Circle import Mathlib.Data.ZMod.Basic import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Topology.Homotopy.HomotopyGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem pi1_circle_mulEquiv_int : diff --git a/generated/pi1_circle_mulEquiv_int/Submission.lean b/generated/pi1_circle_mulEquiv_int/Submission.lean index ac07fcca..9f0e0034 100644 --- a/generated/pi1_circle_mulEquiv_int/Submission.lean +++ b/generated/pi1_circle_mulEquiv_int/Submission.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Complex.Circle import Mathlib.Data.ZMod.Basic import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Topology.Homotopy.HomotopyGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/pi3_sphere_two_mulEquiv_int/Challenge.lean b/generated/pi3_sphere_two_mulEquiv_int/Challenge.lean index 7e553561..9d1d252b 100644 --- a/generated/pi3_sphere_two_mulEquiv_int/Challenge.lean +++ b/generated/pi3_sphere_two_mulEquiv_int/Challenge.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Complex.Circle import Mathlib.Data.ZMod.Basic import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Topology.Homotopy.HomotopyGroup -import Lake.Toml -import Lake.Util.Message -import Lean theorem pi3_sphere_two_mulEquiv_int (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) : Nonempty diff --git a/generated/pi3_sphere_two_mulEquiv_int/Solution.lean b/generated/pi3_sphere_two_mulEquiv_int/Solution.lean index b734d6a1..4ebc84a9 100644 --- a/generated/pi3_sphere_two_mulEquiv_int/Solution.lean +++ b/generated/pi3_sphere_two_mulEquiv_int/Solution.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Complex.Circle import Mathlib.Data.ZMod.Basic import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Topology.Homotopy.HomotopyGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem pi3_sphere_two_mulEquiv_int (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) : diff --git a/generated/pi3_sphere_two_mulEquiv_int/Submission.lean b/generated/pi3_sphere_two_mulEquiv_int/Submission.lean index f2a6af0b..03bb63af 100644 --- a/generated/pi3_sphere_two_mulEquiv_int/Submission.lean +++ b/generated/pi3_sphere_two_mulEquiv_int/Submission.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Complex.Circle import Mathlib.Data.ZMod.Basic import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Topology.Homotopy.HomotopyGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/pi6_sphere_three_mulEquiv_zmod_twelve/Challenge.lean b/generated/pi6_sphere_three_mulEquiv_zmod_twelve/Challenge.lean index 23c10449..dfaecf63 100644 --- a/generated/pi6_sphere_three_mulEquiv_zmod_twelve/Challenge.lean +++ b/generated/pi6_sphere_three_mulEquiv_zmod_twelve/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem pi6_sphere_three_mulEquiv_zmod_twelve (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) : Nonempty diff --git a/generated/pi6_sphere_three_mulEquiv_zmod_twelve/Solution.lean b/generated/pi6_sphere_three_mulEquiv_zmod_twelve/Solution.lean index bb6e22ba..1035f18d 100644 --- a/generated/pi6_sphere_three_mulEquiv_zmod_twelve/Solution.lean +++ b/generated/pi6_sphere_three_mulEquiv_zmod_twelve/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem pi6_sphere_three_mulEquiv_zmod_twelve (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) : diff --git a/generated/pi6_sphere_three_mulEquiv_zmod_twelve/Submission.lean b/generated/pi6_sphere_three_mulEquiv_zmod_twelve/Submission.lean index 2ed8c30b..46025a5b 100644 --- a/generated/pi6_sphere_three_mulEquiv_zmod_twelve/Submission.lean +++ b/generated/pi6_sphere_three_mulEquiv_zmod_twelve/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/pi_sphere_infinite_iff/Challenge.lean b/generated/pi_sphere_infinite_iff/Challenge.lean index 17be54aa..a3fafb54 100644 --- a/generated/pi_sphere_infinite_iff/Challenge.lean +++ b/generated/pi_sphere_infinite_iff/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem pi_sphere_infinite_iff (k n : β„•) (hn : 1 ≀ n) (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) : diff --git a/generated/pi_sphere_infinite_iff/Solution.lean b/generated/pi_sphere_infinite_iff/Solution.lean index 0224699e..d4cf432c 100644 --- a/generated/pi_sphere_infinite_iff/Solution.lean +++ b/generated/pi_sphere_infinite_iff/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem pi_sphere_infinite_iff (k n : β„•) (hn : 1 ≀ n) diff --git a/generated/pi_sphere_infinite_iff/Submission.lean b/generated/pi_sphere_infinite_iff/Submission.lean index 90257442..71dcd1b6 100644 --- a/generated/pi_sphere_infinite_iff/Submission.lean +++ b/generated/pi_sphere_infinite_iff/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/pi_succ_sphere_n_mulEquiv_zmod_two/Challenge.lean b/generated/pi_succ_sphere_n_mulEquiv_zmod_two/Challenge.lean index 7159674a..6a0aae29 100644 --- a/generated/pi_succ_sphere_n_mulEquiv_zmod_two/Challenge.lean +++ b/generated/pi_succ_sphere_n_mulEquiv_zmod_two/Challenge.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Complex.Circle import Mathlib.Data.ZMod.Basic import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Topology.Homotopy.HomotopyGroup -import Lake.Toml -import Lake.Util.Message -import Lean theorem pi_succ_sphere_n_mulEquiv_zmod_two (n : β„•) (hn : 3 ≀ n) (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) : diff --git a/generated/pi_succ_sphere_n_mulEquiv_zmod_two/Solution.lean b/generated/pi_succ_sphere_n_mulEquiv_zmod_two/Solution.lean index d481555c..1e30dea8 100644 --- a/generated/pi_succ_sphere_n_mulEquiv_zmod_two/Solution.lean +++ b/generated/pi_succ_sphere_n_mulEquiv_zmod_two/Solution.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Complex.Circle import Mathlib.Data.ZMod.Basic import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Topology.Homotopy.HomotopyGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem pi_succ_sphere_n_mulEquiv_zmod_two (n : β„•) (hn : 3 ≀ n) diff --git a/generated/pi_succ_sphere_n_mulEquiv_zmod_two/Submission.lean b/generated/pi_succ_sphere_n_mulEquiv_zmod_two/Submission.lean index 2b3cc161..8ed6dabc 100644 --- a/generated/pi_succ_sphere_n_mulEquiv_zmod_two/Submission.lean +++ b/generated/pi_succ_sphere_n_mulEquiv_zmod_two/Submission.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Complex.Circle import Mathlib.Data.ZMod.Basic import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Topology.Homotopy.HomotopyGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/pick/ChallengeDeps.lean b/generated/pick/ChallengeDeps.lean index aea44d1a..56547b3e 100644 --- a/generated/pick/ChallengeDeps.lean +++ b/generated/pick/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Geometry.PicksTheorem diff --git a/generated/pin_sphere_n_mulEquiv_int/Challenge.lean b/generated/pin_sphere_n_mulEquiv_int/Challenge.lean index 19c06e96..7193c54c 100644 --- a/generated/pin_sphere_n_mulEquiv_int/Challenge.lean +++ b/generated/pin_sphere_n_mulEquiv_int/Challenge.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Complex.Circle import Mathlib.Data.ZMod.Basic import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Topology.Homotopy.HomotopyGroup -import Lake.Toml -import Lake.Util.Message -import Lean theorem pin_sphere_n_mulEquiv_int (n : β„•) (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 2))) 1) : diff --git a/generated/pin_sphere_n_mulEquiv_int/Solution.lean b/generated/pin_sphere_n_mulEquiv_int/Solution.lean index 92b38fe7..cd059d83 100644 --- a/generated/pin_sphere_n_mulEquiv_int/Solution.lean +++ b/generated/pin_sphere_n_mulEquiv_int/Solution.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Complex.Circle import Mathlib.Data.ZMod.Basic import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Topology.Homotopy.HomotopyGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem pin_sphere_n_mulEquiv_int (n : β„•) diff --git a/generated/pin_sphere_n_mulEquiv_int/Submission.lean b/generated/pin_sphere_n_mulEquiv_int/Submission.lean index d2f4c8ad..ed77b453 100644 --- a/generated/pin_sphere_n_mulEquiv_int/Submission.lean +++ b/generated/pin_sphere_n_mulEquiv_int/Submission.lean @@ -2,9 +2,6 @@ import Mathlib.Analysis.Complex.Circle import Mathlib.Data.ZMod.Basic import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Topology.Homotopy.HomotopyGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/platonic_classification/ChallengeDeps.lean b/generated/platonic_classification/ChallengeDeps.lean index 7e098f75..5d73511f 100644 --- a/generated/platonic_classification/ChallengeDeps.lean +++ b/generated/platonic_classification/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/poincare_3d_smooth/Challenge.lean b/generated/poincare_3d_smooth/Challenge.lean index 61a7764e..0cb635fe 100644 --- a/generated/poincare_3d_smooth/Challenge.lean +++ b/generated/poincare_3d_smooth/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Manifold ContDiff open Metric (sphere) diff --git a/generated/poincare_3d_smooth/Solution.lean b/generated/poincare_3d_smooth/Solution.lean index e6ee622d..4631dbcf 100644 --- a/generated/poincare_3d_smooth/Solution.lean +++ b/generated/poincare_3d_smooth/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped Manifold ContDiff diff --git a/generated/poincare_3d_smooth/Submission.lean b/generated/poincare_3d_smooth/Submission.lean index 271e192d..749cd6ca 100644 --- a/generated/poincare_3d_smooth/Submission.lean +++ b/generated/poincare_3d_smooth/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped Manifold ContDiff diff --git a/generated/poincare_3d_topological/Challenge.lean b/generated/poincare_3d_topological/Challenge.lean index 1d32bd55..e569bf68 100644 --- a/generated/poincare_3d_topological/Challenge.lean +++ b/generated/poincare_3d_topological/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Metric (sphere) diff --git a/generated/poincare_3d_topological/Solution.lean b/generated/poincare_3d_topological/Solution.lean index 69dd3bf4..9901750b 100644 --- a/generated/poincare_3d_topological/Solution.lean +++ b/generated/poincare_3d_topological/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Metric (sphere) diff --git a/generated/poincare_3d_topological/Submission.lean b/generated/poincare_3d_topological/Submission.lean index 933cc17b..a1048faa 100644 --- a/generated/poincare_3d_topological/Submission.lean +++ b/generated/poincare_3d_topological/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Metric (sphere) diff --git a/generated/poincare_4d_topological/Challenge.lean b/generated/poincare_4d_topological/Challenge.lean index af3d8f84..b258511f 100644 --- a/generated/poincare_4d_topological/Challenge.lean +++ b/generated/poincare_4d_topological/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Metric (sphere) open ContinuousMap diff --git a/generated/poincare_4d_topological/Solution.lean b/generated/poincare_4d_topological/Solution.lean index 1c9cda5c..83932265 100644 --- a/generated/poincare_4d_topological/Solution.lean +++ b/generated/poincare_4d_topological/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Metric (sphere) diff --git a/generated/poincare_4d_topological/Submission.lean b/generated/poincare_4d_topological/Submission.lean index 1dc49064..b10e1129 100644 --- a/generated/poincare_4d_topological/Submission.lean +++ b/generated/poincare_4d_topological/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Metric (sphere) diff --git a/generated/poincare_bendixson/ChallengeDeps.lean b/generated/poincare_bendixson/ChallengeDeps.lean index 721b5b16..26e466ac 100644 --- a/generated/poincare_bendixson/ChallengeDeps.lean +++ b/generated/poincare_bendixson/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Dynamics diff --git a/generated/poincare_high_dim_topological/Challenge.lean b/generated/poincare_high_dim_topological/Challenge.lean index 693f0533..195bda2c 100644 --- a/generated/poincare_high_dim_topological/Challenge.lean +++ b/generated/poincare_high_dim_topological/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Metric (sphere) open ContinuousMap diff --git a/generated/poincare_high_dim_topological/Solution.lean b/generated/poincare_high_dim_topological/Solution.lean index 299e239d..65edc3b1 100644 --- a/generated/poincare_high_dim_topological/Solution.lean +++ b/generated/poincare_high_dim_topological/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Metric (sphere) diff --git a/generated/poincare_high_dim_topological/Submission.lean b/generated/poincare_high_dim_topological/Submission.lean index 080fd902..352b538e 100644 --- a/generated/poincare_high_dim_topological/Submission.lean +++ b/generated/poincare_high_dim_topological/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Metric (sphere) diff --git a/generated/poincare_siegel_linearisation/ChallengeDeps.lean b/generated/poincare_siegel_linearisation/ChallengeDeps.lean index f89ed6e7..882bfd7d 100644 --- a/generated/poincare_siegel_linearisation/ChallengeDeps.lean +++ b/generated/poincare_siegel_linearisation/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace ComplexAnalysis diff --git a/generated/posSemidef_map_exp/Challenge.lean b/generated/posSemidef_map_exp/Challenge.lean index 1aa50093..d3f99913 100644 --- a/generated/posSemidef_map_exp/Challenge.lean +++ b/generated/posSemidef_map_exp/Challenge.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Matrix.Order import Mathlib.Analysis.SpecialFunctions.ExpDeriv -import Lake.Toml -import Lake.Util.Message -import Lean open scoped MatrixOrder Matrix diff --git a/generated/posSemidef_map_exp/Solution.lean b/generated/posSemidef_map_exp/Solution.lean index 6fa345fc..a2923579 100644 --- a/generated/posSemidef_map_exp/Solution.lean +++ b/generated/posSemidef_map_exp/Solution.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Matrix.Order import Mathlib.Analysis.SpecialFunctions.ExpDeriv -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped MatrixOrder Matrix diff --git a/generated/posSemidef_map_exp/Submission.lean b/generated/posSemidef_map_exp/Submission.lean index 29d64c3f..c208d4b1 100644 --- a/generated/posSemidef_map_exp/Submission.lean +++ b/generated/posSemidef_map_exp/Submission.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Matrix.Order import Mathlib.Analysis.SpecialFunctions.ExpDeriv -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped MatrixOrder Matrix diff --git a/generated/q_tspp/ChallengeDeps.lean b/generated/q_tspp/ChallengeDeps.lean index 2b357c0d..8cd4430f 100644 --- a/generated/q_tspp/ChallengeDeps.lean +++ b/generated/q_tspp/ChallengeDeps.lean @@ -2,9 +2,6 @@ import Mathlib.Algebra.Polynomial.Basic import Mathlib.Data.Finset.Powerset import Mathlib.Data.Finset.Prod import Mathlib.Order.UpperLower.Basic -import Lake.Toml -import Lake.Util.Message -import Lean /-! # The q-TSPP theorem diff --git a/generated/rado_riemannSurface/Challenge.lean b/generated/rado_riemannSurface/Challenge.lean index e2007f9e..b223f73d 100644 --- a/generated/rado_riemannSurface/Challenge.lean +++ b/generated/rado_riemannSurface/Challenge.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Complex.Basic import Mathlib.Geometry.Manifold.IsManifold.Basic -import Lake.Toml -import Lake.Util.Message -import Lean theorem rado_riemannSurface {X : Type*} [TopologicalSpace X] [T2Space X] [ConnectedSpace X] [ChartedSpace β„‚ X] [IsManifold (modelWithCornersSelf β„‚ β„‚) 1 X] : diff --git a/generated/rado_riemannSurface/Solution.lean b/generated/rado_riemannSurface/Solution.lean index db3d610e..e2021167 100644 --- a/generated/rado_riemannSurface/Solution.lean +++ b/generated/rado_riemannSurface/Solution.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Complex.Basic import Mathlib.Geometry.Manifold.IsManifold.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem rado_riemannSurface {X : Type*} [TopologicalSpace X] [T2Space X] [ConnectedSpace X] diff --git a/generated/rado_riemannSurface/Submission.lean b/generated/rado_riemannSurface/Submission.lean index eb2e4dc7..ef4da552 100644 --- a/generated/rado_riemannSurface/Submission.lean +++ b/generated/rado_riemannSurface/Submission.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Complex.Basic import Mathlib.Geometry.Manifold.IsManifold.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/radon_transform_inversion/ChallengeDeps.lean b/generated/radon_transform_inversion/ChallengeDeps.lean index 563b2201..30818f33 100644 --- a/generated/radon_transform_inversion/ChallengeDeps.lean +++ b/generated/radon_transform_inversion/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Analysis.RadonTransform diff --git a/generated/ramanujan_petersson/ChallengeDeps.lean b/generated/ramanujan_petersson/ChallengeDeps.lean index 239a2dfd..b34418ad 100644 --- a/generated/ramanujan_petersson/ChallengeDeps.lean +++ b/generated/ramanujan_petersson/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace NumberTheory diff --git a/generated/rcf_quantifier_elimination/ChallengeDeps.lean b/generated/rcf_quantifier_elimination/ChallengeDeps.lean index fc74cff4..eebb90c6 100644 --- a/generated/rcf_quantifier_elimination/ChallengeDeps.lean +++ b/generated/rcf_quantifier_elimination/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Real.Sqrt -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Quantifier elimination for real closed fields diff --git a/generated/regular_value_ae/ChallengeDeps.lean b/generated/regular_value_ae/ChallengeDeps.lean index 34d04dd7..164bde44 100644 --- a/generated/regular_value_ae/ChallengeDeps.lean +++ b/generated/regular_value_ae/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Geometry.RegularValue diff --git a/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/ChallengeDeps.lean b/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/ChallengeDeps.lean index 39c19231..0767126e 100644 --- a/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/ChallengeDeps.lean +++ b/generated/riemann_hypothesis_iff_lagarias_elementary_criterion/ChallengeDeps.lean @@ -1,9 +1,6 @@ import Mathlib.NumberTheory.ArithmeticFunction.Misc import Mathlib.NumberTheory.Harmonic.Defs import Mathlib.NumberTheory.LSeries.RiemannZeta -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace NumberTheory diff --git a/generated/riesz_brothers_theorem/Challenge.lean b/generated/riesz_brothers_theorem/Challenge.lean index 9f45a6ca..9426b1c9 100644 --- a/generated/riesz_brothers_theorem/Challenge.lean +++ b/generated/riesz_brothers_theorem/Challenge.lean @@ -3,9 +3,6 @@ import Mathlib.Analysis.Normed.Operator.Mul import Mathlib.MeasureTheory.Measure.Complex import Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym import Mathlib.MeasureTheory.VectorMeasure.Integral -import Lake.Toml -import Lake.Util.Message -import Lean open MeasureTheory diff --git a/generated/riesz_brothers_theorem/Solution.lean b/generated/riesz_brothers_theorem/Solution.lean index 6c07c210..339ba74f 100644 --- a/generated/riesz_brothers_theorem/Solution.lean +++ b/generated/riesz_brothers_theorem/Solution.lean @@ -3,9 +3,6 @@ import Mathlib.Analysis.Normed.Operator.Mul import Mathlib.MeasureTheory.Measure.Complex import Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym import Mathlib.MeasureTheory.VectorMeasure.Integral -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open MeasureTheory diff --git a/generated/riesz_brothers_theorem/Submission.lean b/generated/riesz_brothers_theorem/Submission.lean index f03feb8b..6de3c2e5 100644 --- a/generated/riesz_brothers_theorem/Submission.lean +++ b/generated/riesz_brothers_theorem/Submission.lean @@ -3,9 +3,6 @@ import Mathlib.Analysis.Normed.Operator.Mul import Mathlib.MeasureTheory.Measure.Complex import Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym import Mathlib.MeasureTheory.VectorMeasure.Integral -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open MeasureTheory diff --git a/generated/rising_sun_lemma/ChallengeDeps.lean b/generated/rising_sun_lemma/ChallengeDeps.lean index 7738974f..a67d9027 100644 --- a/generated/rising_sun_lemma/ChallengeDeps.lean +++ b/generated/rising_sun_lemma/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Analysis.RisingSun diff --git a/generated/rokhlin_lemma/ChallengeDeps.lean b/generated/rokhlin_lemma/ChallengeDeps.lean index 1d312fd6..ca46f224 100644 --- a/generated/rokhlin_lemma/ChallengeDeps.lean +++ b/generated/rokhlin_lemma/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Dynamics diff --git a/generated/rouche_zero_count_eq/Challenge.lean b/generated/rouche_zero_count_eq/Challenge.lean index 8c9db0ce..0f195574 100644 --- a/generated/rouche_zero_count_eq/Challenge.lean +++ b/generated/rouche_zero_count_eq/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic -import Lake.Toml -import Lake.Util.Message -import Lean open MeromorphicOn diff --git a/generated/rouche_zero_count_eq/Solution.lean b/generated/rouche_zero_count_eq/Solution.lean index 60aafcff..9aec9a2c 100644 --- a/generated/rouche_zero_count_eq/Solution.lean +++ b/generated/rouche_zero_count_eq/Solution.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open MeromorphicOn diff --git a/generated/rouche_zero_count_eq/Submission.lean b/generated/rouche_zero_count_eq/Submission.lean index c9363ac8..14d3a8be 100644 --- a/generated/rouche_zero_count_eq/Submission.lean +++ b/generated/rouche_zero_count_eq/Submission.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open MeromorphicOn diff --git a/generated/runge_theorem/Challenge.lean b/generated/runge_theorem/Challenge.lean index 5a43bf82..b170ed53 100644 --- a/generated/runge_theorem/Challenge.lean +++ b/generated/runge_theorem/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Polynomial diff --git a/generated/runge_theorem/Solution.lean b/generated/runge_theorem/Solution.lean index a31581db..405faa06 100644 --- a/generated/runge_theorem/Solution.lean +++ b/generated/runge_theorem/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped Polynomial diff --git a/generated/runge_theorem/Submission.lean b/generated/runge_theorem/Submission.lean index 1831e9d9..48601d7d 100644 --- a/generated/runge_theorem/Submission.lean +++ b/generated/runge_theorem/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped Polynomial diff --git a/generated/sard_theorem/ChallengeDeps.lean b/generated/sard_theorem/ChallengeDeps.lean index 767563e8..cf0b03c6 100644 --- a/generated/sard_theorem/ChallengeDeps.lean +++ b/generated/sard_theorem/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/schauder_fixed_point/Challenge.lean b/generated/schauder_fixed_point/Challenge.lean index 88f6482c..721e8272 100644 --- a/generated/schauder_fixed_point/Challenge.lean +++ b/generated/schauder_fixed_point/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem schauder_fixed_point {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] diff --git a/generated/schauder_fixed_point/Solution.lean b/generated/schauder_fixed_point/Solution.lean index 94d60d7d..d66b2b56 100644 --- a/generated/schauder_fixed_point/Solution.lean +++ b/generated/schauder_fixed_point/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem schauder_fixed_point {E : Type*} diff --git a/generated/schauder_fixed_point/Submission.lean b/generated/schauder_fixed_point/Submission.lean index 070bb22c..e466dcd6 100644 --- a/generated/schauder_fixed_point/Submission.lean +++ b/generated/schauder_fixed_point/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/schlafli_classification/ChallengeDeps.lean b/generated/schlafli_classification/ChallengeDeps.lean index 6814134d..0d25d79f 100644 --- a/generated/schlafli_classification/ChallengeDeps.lean +++ b/generated/schlafli_classification/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/schmidt_subspace/Challenge.lean b/generated/schmidt_subspace/Challenge.lean index 059167a9..18813ecc 100644 --- a/generated/schmidt_subspace/Challenge.lean +++ b/generated/schmidt_subspace/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem schmidt_subspace (Οƒ : Type*) [Fintype Οƒ] (hΟƒ : 2 ≀ Fintype.card Οƒ) (L : Οƒ β†’ Οƒ β†’ β„‚) diff --git a/generated/schmidt_subspace/Solution.lean b/generated/schmidt_subspace/Solution.lean index 92731d4b..b9b70809 100644 --- a/generated/schmidt_subspace/Solution.lean +++ b/generated/schmidt_subspace/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem schmidt_subspace (Οƒ : Type*) [Fintype Οƒ] (hΟƒ : 2 ≀ Fintype.card Οƒ) diff --git a/generated/schmidt_subspace/Submission.lean b/generated/schmidt_subspace/Submission.lean index 8363a625..e790e8f3 100644 --- a/generated/schmidt_subspace/Submission.lean +++ b/generated/schmidt_subspace/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/schoenflies/Challenge.lean b/generated/schoenflies/Challenge.lean index fe32cc44..8dd8ba40 100644 --- a/generated/schoenflies/Challenge.lean +++ b/generated/schoenflies/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem schoenflies (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 β†’ EuclideanSpace ℝ (Fin 2)) (_hcont : Continuous r) (_hinj : Function.Injective r) : diff --git a/generated/schoenflies/Solution.lean b/generated/schoenflies/Solution.lean index 82cf30f0..4730a76a 100644 --- a/generated/schoenflies/Solution.lean +++ b/generated/schoenflies/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem schoenflies (r : Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 β†’ EuclideanSpace ℝ (Fin 2)) diff --git a/generated/schoenflies/Submission.lean b/generated/schoenflies/Submission.lean index 3ff60a9e..9ad713d5 100644 --- a/generated/schoenflies/Submission.lean +++ b/generated/schoenflies/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/schreier_conjecture/ChallengeDeps.lean b/generated/schreier_conjecture/ChallengeDeps.lean index 3ea18e2e..6e7ef897 100644 --- a/generated/schreier_conjecture/ChallengeDeps.lean +++ b/generated/schreier_conjecture/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace GroupTheory diff --git a/generated/semilinear_poisson_radial_symmetry/ChallengeDeps.lean b/generated/semilinear_poisson_radial_symmetry/ChallengeDeps.lean index b6d22d65..1e0e53c6 100644 --- a/generated/semilinear_poisson_radial_symmetry/ChallengeDeps.lean +++ b/generated/semilinear_poisson_radial_symmetry/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.InnerProductSpace.Laplacian import Mathlib.Topology.MetricSpace.Lipschitz -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/shafarevich_relation_rank_bound/ChallengeDeps.lean b/generated/shafarevich_relation_rank_bound/ChallengeDeps.lean index 7273fdac..a4cd8e82 100644 --- a/generated/shafarevich_relation_rank_bound/ChallengeDeps.lean +++ b/generated/shafarevich_relation_rank_bound/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace NumberTheory diff --git a/generated/shafarevich_solvable_galois/Challenge.lean b/generated/shafarevich_solvable_galois/Challenge.lean index 75485cf1..f2a5553f 100644 --- a/generated/shafarevich_solvable_galois/Challenge.lean +++ b/generated/shafarevich_solvable_galois/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem shafarevich_solvable_galois (G : Type*) [Group G] [Finite G] [Group.IsSolvable G] : βˆƒ (K : Type) (_ : Field K) (_ : Algebra β„š K) (_ : FiniteDimensional β„š K) (_ : IsGalois β„š K), diff --git a/generated/shafarevich_solvable_galois/Solution.lean b/generated/shafarevich_solvable_galois/Solution.lean index 3b0a00d2..ad884e22 100644 --- a/generated/shafarevich_solvable_galois/Solution.lean +++ b/generated/shafarevich_solvable_galois/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem shafarevich_solvable_galois (G : Type*) [Group G] [Finite G] [Group.IsSolvable G] : diff --git a/generated/shafarevich_solvable_galois/Submission.lean b/generated/shafarevich_solvable_galois/Submission.lean index 8f0b0fa5..855316d1 100644 --- a/generated/shafarevich_solvable_galois/Submission.lean +++ b/generated/shafarevich_solvable_galois/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/shannon_capacity_pentagon/ChallengeDeps.lean b/generated/shannon_capacity_pentagon/ChallengeDeps.lean index fbd3c625..8bdf9f04 100644 --- a/generated/shannon_capacity_pentagon/ChallengeDeps.lean +++ b/generated/shannon_capacity_pentagon/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Combinatorics.ShannonCapacityPentagon diff --git a/generated/smale_conjecture/Challenge.lean b/generated/smale_conjecture/Challenge.lean index 38eb6b00..c0d07613 100644 --- a/generated/smale_conjecture/Challenge.lean +++ b/generated/smale_conjecture/Challenge.lean @@ -3,9 +3,6 @@ import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Geometry.Manifold.Instances.Real import Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary import Mathlib.LinearAlgebra.UnitaryGroup -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Manifold ContDiff open Metric (sphere) diff --git a/generated/smale_conjecture/Solution.lean b/generated/smale_conjecture/Solution.lean index e343c5fa..01804a63 100644 --- a/generated/smale_conjecture/Solution.lean +++ b/generated/smale_conjecture/Solution.lean @@ -3,9 +3,6 @@ import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Geometry.Manifold.Instances.Real import Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary import Mathlib.LinearAlgebra.UnitaryGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped Manifold ContDiff diff --git a/generated/smale_conjecture/Submission.lean b/generated/smale_conjecture/Submission.lean index 5fb9abad..29196636 100644 --- a/generated/smale_conjecture/Submission.lean +++ b/generated/smale_conjecture/Submission.lean @@ -3,9 +3,6 @@ import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Geometry.Manifold.Instances.Real import Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary import Mathlib.LinearAlgebra.UnitaryGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped Manifold ContDiff diff --git a/generated/smooth_knot_has_quadrisecant/ChallengeDeps.lean b/generated/smooth_knot_has_quadrisecant/ChallengeDeps.lean index 8eb23791..96e6ad87 100644 --- a/generated/smooth_knot_has_quadrisecant/ChallengeDeps.lean +++ b/generated/smooth_knot_has_quadrisecant/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.KnotTheory.Quadrisecant diff --git a/generated/sobolev_embedding_morrey/ChallengeDeps.lean b/generated/sobolev_embedding_morrey/ChallengeDeps.lean index 7540e2ff..05cf0e9e 100644 --- a/generated/sobolev_embedding_morrey/ChallengeDeps.lean +++ b/generated/sobolev_embedding_morrey/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/solvable_by_radicals_converse/Challenge.lean b/generated/solvable_by_radicals_converse/Challenge.lean index 0eaeb460..5b757d31 100644 --- a/generated/solvable_by_radicals_converse/Challenge.lean +++ b/generated/solvable_by_radicals_converse/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Polynomial IntermediateField diff --git a/generated/solvable_by_radicals_converse/Solution.lean b/generated/solvable_by_radicals_converse/Solution.lean index ccdd8ecd..bbcd05db 100644 --- a/generated/solvable_by_radicals_converse/Solution.lean +++ b/generated/solvable_by_radicals_converse/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Polynomial IntermediateField diff --git a/generated/solvable_by_radicals_converse/Submission.lean b/generated/solvable_by_radicals_converse/Submission.lean index c8863954..02ab606b 100644 --- a/generated/solvable_by_radicals_converse/Submission.lean +++ b/generated/solvable_by_radicals_converse/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Polynomial IntermediateField diff --git a/generated/space_groups_230/ChallengeDeps.lean b/generated/space_groups_230/ChallengeDeps.lean index 1922cc1d..1c423917 100644 --- a/generated/space_groups_230/ChallengeDeps.lean +++ b/generated/space_groups_230/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/sphere_theorem_differentiable/ChallengeDeps.lean b/generated/sphere_theorem_differentiable/ChallengeDeps.lean index 114deb32..a64c21f9 100644 --- a/generated/sphere_theorem_differentiable/ChallengeDeps.lean +++ b/generated/sphere_theorem_differentiable/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Geometry.SphereTheorem diff --git a/generated/sphere_theorem_topological/ChallengeDeps.lean b/generated/sphere_theorem_topological/ChallengeDeps.lean index 114deb32..a64c21f9 100644 --- a/generated/sphere_theorem_topological/ChallengeDeps.lean +++ b/generated/sphere_theorem_topological/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Geometry.SphereTheorem diff --git a/generated/stable_unstable_manifolds/ChallengeDeps.lean b/generated/stable_unstable_manifolds/ChallengeDeps.lean index 105ac56b..f30dd167 100644 --- a/generated/stable_unstable_manifolds/ChallengeDeps.lean +++ b/generated/stable_unstable_manifolds/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Dynamics diff --git a/generated/strong_mason_conjecture/ChallengeDeps.lean b/generated/strong_mason_conjecture/ChallengeDeps.lean index 3178bed6..9d806818 100644 --- a/generated/strong_mason_conjecture/ChallengeDeps.lean +++ b/generated/strong_mason_conjecture/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Combinatorics.StrongMason diff --git a/generated/strong_subadditivity/ChallengeDeps.lean b/generated/strong_subadditivity/ChallengeDeps.lean index 453c9ad9..0555ad88 100644 --- a/generated/strong_subadditivity/ChallengeDeps.lean +++ b/generated/strong_subadditivity/ChallengeDeps.lean @@ -1,6 +1,3 @@ -import Lake.Toml -import Lake.Util.Message -import Lean import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus import Mathlib.LinearAlgebra.Matrix.PosDef diff --git a/generated/sturm/ChallengeDeps.lean b/generated/sturm/ChallengeDeps.lean index 63ccfcc3..b4dc58f7 100644 --- a/generated/sturm/ChallengeDeps.lean +++ b/generated/sturm/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Algebra diff --git a/generated/sturm_separation/Challenge.lean b/generated/sturm_separation/Challenge.lean index 4eea14e5..238f0654 100644 --- a/generated/sturm_separation/Challenge.lean +++ b/generated/sturm_separation/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Calculus.Deriv.Basic -import Lake.Toml -import Lake.Util.Message -import Lean theorem sturm_separation (p q y₁ yβ‚‚ : ℝ β†’ ℝ) (a b : ℝ) (hab : a < b) (J : Set ℝ) (hJ_open : IsOpen J) (hJ_conn : IsPreconnected J) diff --git a/generated/sturm_separation/Solution.lean b/generated/sturm_separation/Solution.lean index 1a67696f..892316aa 100644 --- a/generated/sturm_separation/Solution.lean +++ b/generated/sturm_separation/Solution.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Calculus.Deriv.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem sturm_separation (p q y₁ yβ‚‚ : ℝ β†’ ℝ) (a b : ℝ) (hab : a < b) diff --git a/generated/sturm_separation/Submission.lean b/generated/sturm_separation/Submission.lean index 089de85c..c2640483 100644 --- a/generated/sturm_separation/Submission.lean +++ b/generated/sturm_separation/Submission.lean @@ -1,7 +1,4 @@ import Mathlib.Analysis.Calculus.Deriv.Basic -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/substInv_X_sub_X_sq_eq_catalan/Challenge.lean b/generated/substInv_X_sub_X_sq_eq_catalan/Challenge.lean index 724fd27c..a15ec477 100644 --- a/generated/substInv_X_sub_X_sq_eq_catalan/Challenge.lean +++ b/generated/substInv_X_sub_X_sq_eq_catalan/Challenge.lean @@ -1,8 +1,5 @@ import Mathlib.RingTheory.PowerSeries.Substitution import Mathlib.Data.Nat.Choose.Central -import Lake.Toml -import Lake.Util.Message -import Lean open PowerSeries diff --git a/generated/substInv_X_sub_X_sq_eq_catalan/Solution.lean b/generated/substInv_X_sub_X_sq_eq_catalan/Solution.lean index 296bced0..4d0b57c9 100644 --- a/generated/substInv_X_sub_X_sq_eq_catalan/Solution.lean +++ b/generated/substInv_X_sub_X_sq_eq_catalan/Solution.lean @@ -1,8 +1,5 @@ import Mathlib.RingTheory.PowerSeries.Substitution import Mathlib.Data.Nat.Choose.Central -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open PowerSeries diff --git a/generated/substInv_X_sub_X_sq_eq_catalan/Submission.lean b/generated/substInv_X_sub_X_sq_eq_catalan/Submission.lean index 9b91e404..03523998 100644 --- a/generated/substInv_X_sub_X_sq_eq_catalan/Submission.lean +++ b/generated/substInv_X_sub_X_sq_eq_catalan/Submission.lean @@ -1,8 +1,5 @@ import Mathlib.RingTheory.PowerSeries.Substitution import Mathlib.Data.Nat.Choose.Central -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open PowerSeries diff --git a/generated/symAction_range_eq_centralizer_glAction/ChallengeDeps.lean b/generated/symAction_range_eq_centralizer_glAction/ChallengeDeps.lean index 0bfc99cc..c1ef010b 100644 --- a/generated/symAction_range_eq_centralizer_glAction/ChallengeDeps.lean +++ b/generated/symAction_range_eq_centralizer_glAction/ChallengeDeps.lean @@ -2,9 +2,6 @@ import Mathlib.LinearAlgebra.TensorPower.Basic import Mathlib.LinearAlgebra.PiTensorProduct.Basic import Mathlib.Algebra.Algebra.Subalgebra.Centralizer import Mathlib.LinearAlgebra.FiniteDimensional.Defs -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace RepresentationTheory diff --git a/generated/symplectic_matrix_det/Challenge.lean b/generated/symplectic_matrix_det/Challenge.lean index 12b778f7..3dd6f838 100644 --- a/generated/symplectic_matrix_det/Challenge.lean +++ b/generated/symplectic_matrix_det/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Matrix diff --git a/generated/symplectic_matrix_det/Solution.lean b/generated/symplectic_matrix_det/Solution.lean index 6a072ac3..601eab6a 100644 --- a/generated/symplectic_matrix_det/Solution.lean +++ b/generated/symplectic_matrix_det/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Matrix diff --git a/generated/symplectic_matrix_det/Submission.lean b/generated/symplectic_matrix_det/Submission.lean index e266f3f2..47dd186a 100644 --- a/generated/symplectic_matrix_det/Submission.lean +++ b/generated/symplectic_matrix_det/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Matrix diff --git a/generated/szemeredi/ChallengeDeps.lean b/generated/szemeredi/ChallengeDeps.lean index 37d3a793..bbb18258 100644 --- a/generated/szemeredi/ChallengeDeps.lean +++ b/generated/szemeredi/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Combinatorics diff --git a/generated/ten_martini_problem/ChallengeDeps.lean b/generated/ten_martini_problem/ChallengeDeps.lean index d249de23..459521af 100644 --- a/generated/ten_martini_problem/ChallengeDeps.lean +++ b/generated/ten_martini_problem/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Analysis.TenMartini diff --git a/generated/thue_siegel_roth/ChallengeDeps.lean b/generated/thue_siegel_roth/ChallengeDeps.lean index 48c11e7d..e6e56b85 100644 --- a/generated/thue_siegel_roth/ChallengeDeps.lean +++ b/generated/thue_siegel_roth/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace NumberTheory diff --git a/generated/topological_classification_of_surfaces/ChallengeDeps.lean b/generated/topological_classification_of_surfaces/ChallengeDeps.lean index 112fb368..906be155 100644 --- a/generated/topological_classification_of_surfaces/ChallengeDeps.lean +++ b/generated/topological_classification_of_surfaces/ChallengeDeps.lean @@ -1,8 +1,5 @@ import Mathlib.Analysis.Complex.Circle import Mathlib.Geometry.Manifold.Instances.Real -import Lake.Toml -import Lake.Util.Message -import Lean /-! Benchmark statements for topological classification of compact connected surfaces with boundary. diff --git a/generated/trace_cayley_hamilton_newton/ChallengeDeps.lean b/generated/trace_cayley_hamilton_newton/ChallengeDeps.lean index f2500d6d..576fc53c 100644 --- a/generated/trace_cayley_hamilton_newton/ChallengeDeps.lean +++ b/generated/trace_cayley_hamilton_newton/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.LinearAlgebra.TraceNewton diff --git a/generated/turing_recursive_equiv/Challenge.lean b/generated/turing_recursive_equiv/Challenge.lean index 038c7e6f..da0ef273 100644 --- a/generated/turing_recursive_equiv/Challenge.lean +++ b/generated/turing_recursive_equiv/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Computability Turing diff --git a/generated/turing_recursive_equiv/Solution.lean b/generated/turing_recursive_equiv/Solution.lean index b1ed6ff0..2efedde1 100644 --- a/generated/turing_recursive_equiv/Solution.lean +++ b/generated/turing_recursive_equiv/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Computability Turing diff --git a/generated/turing_recursive_equiv/Submission.lean b/generated/turing_recursive_equiv/Submission.lean index 270ddf07..f75b2be2 100644 --- a/generated/turing_recursive_equiv/Submission.lean +++ b/generated/turing_recursive_equiv/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Computability Turing diff --git a/generated/tverberg_theorem/ChallengeDeps.lean b/generated/tverberg_theorem/ChallengeDeps.lean index ae6db40f..1022483e 100644 --- a/generated/tverberg_theorem/ChallengeDeps.lean +++ b/generated/tverberg_theorem/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Combinatorics.Tverberg diff --git a/generated/two_ninety_theorem/ChallengeDeps.lean b/generated/two_ninety_theorem/ChallengeDeps.lean index b4da6e6c..7e9355c7 100644 --- a/generated/two_ninety_theorem/ChallengeDeps.lean +++ b/generated/two_ninety_theorem/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.NumberTheory.TwoNinety diff --git a/generated/two_plus_two/Challenge.lean b/generated/two_plus_two/Challenge.lean index 110e7a00..6daaa54e 100644 --- a/generated/two_plus_two/Challenge.lean +++ b/generated/two_plus_two/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem two_plus_two_eq_four : (2 : Nat) + 2 = 4 := by sorry diff --git a/generated/two_plus_two/Solution.lean b/generated/two_plus_two/Solution.lean index 6c735ead..02c11f8d 100644 --- a/generated/two_plus_two/Solution.lean +++ b/generated/two_plus_two/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem two_plus_two_eq_four : (2 : Nat) + 2 = 4 := by diff --git a/generated/two_plus_two/Submission.lean b/generated/two_plus_two/Submission.lean index e1a4e41e..35d29ebd 100644 --- a/generated/two_plus_two/Submission.lean +++ b/generated/two_plus_two/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/uniformization/ChallengeDeps.lean b/generated/uniformization/ChallengeDeps.lean index dc3ff8fe..0b20ed9d 100644 --- a/generated/uniformization/ChallengeDeps.lean +++ b/generated/uniformization/ChallengeDeps.lean @@ -2,9 +2,6 @@ import Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Complex.UpperHalfPlane.Manifold import Mathlib.Geometry.Manifold.Diffeomorph -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Uniformization theorem for Riemann surfaces diff --git a/generated/unit_distance_upper_bound/ChallengeDeps.lean b/generated/unit_distance_upper_bound/ChallengeDeps.lean index f1d2373e..4c423807 100644 --- a/generated/unit_distance_upper_bound/ChallengeDeps.lean +++ b/generated/unit_distance_upper_bound/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Combinatorics diff --git a/generated/upper_bound_simplicial_spheres/ChallengeDeps.lean b/generated/upper_bound_simplicial_spheres/ChallengeDeps.lean index 001d4294..4c84d578 100644 --- a/generated/upper_bound_simplicial_spheres/ChallengeDeps.lean +++ b/generated/upper_bound_simplicial_spheres/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Combinatorics diff --git a/generated/variable_binder_example/Challenge.lean b/generated/variable_binder_example/Challenge.lean index 87817ef2..4fe34e73 100644 --- a/generated/variable_binder_example/Challenge.lean +++ b/generated/variable_binder_example/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean variable {n : Type*} [Fintype n] [DecidableEq n] diff --git a/generated/variable_binder_example/Solution.lean b/generated/variable_binder_example/Solution.lean index 362cdbd4..d31230af 100644 --- a/generated/variable_binder_example/Solution.lean +++ b/generated/variable_binder_example/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission variable {n : Type*} [Fintype n] [DecidableEq n] diff --git a/generated/variable_binder_example/Submission.lean b/generated/variable_binder_example/Submission.lean index ebe419ba..4b48835a 100644 --- a/generated/variable_binder_example/Submission.lean +++ b/generated/variable_binder_example/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers variable {n : Type*} [Fintype n] [DecidableEq n] diff --git a/generated/vinogradov_mean_value/ChallengeDeps.lean b/generated/vinogradov_mean_value/ChallengeDeps.lean index a977954a..3f9d4e96 100644 --- a/generated/vinogradov_mean_value/ChallengeDeps.lean +++ b/generated/vinogradov_mean_value/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean /-! # Vinogradov mean value theorem diff --git a/generated/vonNeumann_doubleCommutant_tfae/Challenge.lean b/generated/vonNeumann_doubleCommutant_tfae/Challenge.lean index 494b4b3b..7b654011 100644 --- a/generated/vonNeumann_doubleCommutant_tfae/Challenge.lean +++ b/generated/vonNeumann_doubleCommutant_tfae/Challenge.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.VonNeumannAlgebra.Basic import Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology import Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM -import Lake.Toml -import Lake.Util.Message -import Lean theorem vonNeumann_doubleCommutant_tfae {H : Type*} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] (S : StarSubalgebra β„‚ (H β†’L[β„‚] H)) : diff --git a/generated/vonNeumann_doubleCommutant_tfae/Solution.lean b/generated/vonNeumann_doubleCommutant_tfae/Solution.lean index a89484d9..4ed3138c 100644 --- a/generated/vonNeumann_doubleCommutant_tfae/Solution.lean +++ b/generated/vonNeumann_doubleCommutant_tfae/Solution.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.VonNeumannAlgebra.Basic import Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology import Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem vonNeumann_doubleCommutant_tfae {H : Type*} [NormedAddCommGroup H] [InnerProductSpace β„‚ H] [CompleteSpace H] diff --git a/generated/vonNeumann_doubleCommutant_tfae/Submission.lean b/generated/vonNeumann_doubleCommutant_tfae/Submission.lean index 5690c1c8..dc8a7273 100644 --- a/generated/vonNeumann_doubleCommutant_tfae/Submission.lean +++ b/generated/vonNeumann_doubleCommutant_tfae/Submission.lean @@ -1,9 +1,6 @@ import Mathlib.Analysis.VonNeumannAlgebra.Basic import Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology import Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/wallpaper_groups_17/ChallengeDeps.lean b/generated/wallpaper_groups_17/ChallengeDeps.lean index fb50c621..7531abd5 100644 --- a/generated/wallpaper_groups_17/ChallengeDeps.lean +++ b/generated/wallpaper_groups_17/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/wang_zahl_kakeya_dimH/ChallengeDeps.lean b/generated/wang_zahl_kakeya_dimH/ChallengeDeps.lean index 829fca9f..e9d5e43e 100644 --- a/generated/wang_zahl_kakeya_dimH/ChallengeDeps.lean +++ b/generated/wang_zahl_kakeya_dimH/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Analysis.WangZahlKakeya diff --git a/generated/watanabe_four_dim_smale_disproof/Challenge.lean b/generated/watanabe_four_dim_smale_disproof/Challenge.lean index 3d27e7e3..d6886cab 100644 --- a/generated/watanabe_four_dim_smale_disproof/Challenge.lean +++ b/generated/watanabe_four_dim_smale_disproof/Challenge.lean @@ -3,9 +3,6 @@ import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Geometry.Manifold.Instances.Real import Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary import Mathlib.LinearAlgebra.UnitaryGroup -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Manifold ContDiff open Metric (sphere) diff --git a/generated/watanabe_four_dim_smale_disproof/Solution.lean b/generated/watanabe_four_dim_smale_disproof/Solution.lean index d7b60398..2186a893 100644 --- a/generated/watanabe_four_dim_smale_disproof/Solution.lean +++ b/generated/watanabe_four_dim_smale_disproof/Solution.lean @@ -3,9 +3,6 @@ import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Geometry.Manifold.Instances.Real import Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary import Mathlib.LinearAlgebra.UnitaryGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped Manifold ContDiff diff --git a/generated/watanabe_four_dim_smale_disproof/Submission.lean b/generated/watanabe_four_dim_smale_disproof/Submission.lean index d0ce82e5..b03b37b7 100644 --- a/generated/watanabe_four_dim_smale_disproof/Submission.lean +++ b/generated/watanabe_four_dim_smale_disproof/Submission.lean @@ -3,9 +3,6 @@ import Mathlib.Geometry.Manifold.Instances.Sphere import Mathlib.Geometry.Manifold.Instances.Real import Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary import Mathlib.LinearAlgebra.UnitaryGroup -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped Manifold ContDiff diff --git a/generated/weak_goldbach/Challenge.lean b/generated/weak_goldbach/Challenge.lean index 6965f7d9..b7ead72a 100644 --- a/generated/weak_goldbach/Challenge.lean +++ b/generated/weak_goldbach/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean theorem weak_goldbach (n : β„•) (hn : 5 < n) (hodd : Odd n) : βˆƒ p q r : β„•, p.Prime ∧ q.Prime ∧ r.Prime ∧ n = p + q + r := by diff --git a/generated/weak_goldbach/Solution.lean b/generated/weak_goldbach/Solution.lean index bea5a59a..0e9a4551 100644 --- a/generated/weak_goldbach/Solution.lean +++ b/generated/weak_goldbach/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission theorem weak_goldbach (n : β„•) (hn : 5 < n) (hodd : Odd n) : diff --git a/generated/weak_goldbach/Submission.lean b/generated/weak_goldbach/Submission.lean index 6d64a9c5..0ad493b3 100644 --- a/generated/weak_goldbach/Submission.lean +++ b/generated/weak_goldbach/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers namespace Submission diff --git a/generated/weak_morse_inequality/ChallengeDeps.lean b/generated/weak_morse_inequality/ChallengeDeps.lean index d457351f..c56e4bad 100644 --- a/generated/weak_morse_inequality/ChallengeDeps.lean +++ b/generated/weak_morse_inequality/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/weil_conjectures/Challenge.lean b/generated/weil_conjectures/Challenge.lean index 787999ca..8c63ad1e 100644 --- a/generated/weil_conjectures/Challenge.lean +++ b/generated/weil_conjectures/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open CategoryTheory AlgebraicGeometry diff --git a/generated/weil_conjectures/Solution.lean b/generated/weil_conjectures/Solution.lean index ac6d5a39..41964273 100644 --- a/generated/weil_conjectures/Solution.lean +++ b/generated/weil_conjectures/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open CategoryTheory AlgebraicGeometry diff --git a/generated/weil_conjectures/Submission.lean b/generated/weil_conjectures/Submission.lean index 0f2062f7..b6cf644c 100644 --- a/generated/weil_conjectures/Submission.lean +++ b/generated/weil_conjectures/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open CategoryTheory AlgebraicGeometry diff --git a/generated/weinstein_conjecture_dim3/ChallengeDeps.lean b/generated/weinstein_conjecture_dim3/ChallengeDeps.lean index 16121893..fa7c77fe 100644 --- a/generated/weinstein_conjecture_dim3/ChallengeDeps.lean +++ b/generated/weinstein_conjecture_dim3/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Geometry diff --git a/generated/whitney_embedding/Challenge.lean b/generated/whitney_embedding/Challenge.lean index 8a47b1db..befefcd0 100644 --- a/generated/whitney_embedding/Challenge.lean +++ b/generated/whitney_embedding/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open scoped Manifold ContDiff open Topology diff --git a/generated/whitney_embedding/Solution.lean b/generated/whitney_embedding/Solution.lean index 50d7d705..70bae197 100644 --- a/generated/whitney_embedding/Solution.lean +++ b/generated/whitney_embedding/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open scoped Manifold ContDiff diff --git a/generated/whitney_embedding/Submission.lean b/generated/whitney_embedding/Submission.lean index abfbf3e5..5a371ccd 100644 --- a/generated/whitney_embedding/Submission.lean +++ b/generated/whitney_embedding/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open scoped Manifold ContDiff diff --git a/generated/wieferich_g_three/ChallengeDeps.lean b/generated/wieferich_g_three/ChallengeDeps.lean index 77e29358..1ae25998 100644 --- a/generated/wieferich_g_three/ChallengeDeps.lean +++ b/generated/wieferich_g_three/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace NumberTheory diff --git a/generated/wiener_atom_detection/ChallengeDeps.lean b/generated/wiener_atom_detection/ChallengeDeps.lean index 3499ace2..d0a8b07e 100644 --- a/generated/wiener_atom_detection/ChallengeDeps.lean +++ b/generated/wiener_atom_detection/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/wiener_inverse_closed/ChallengeDeps.lean b/generated/wiener_inverse_closed/ChallengeDeps.lean index 8a7716f3..56f21100 100644 --- a/generated/wiener_inverse_closed/ChallengeDeps.lean +++ b/generated/wiener_inverse_closed/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Analysis.WienerOneOverF diff --git a/generated/wiener_levy_analytic_calculus/ChallengeDeps.lean b/generated/wiener_levy_analytic_calculus/ChallengeDeps.lean index 282d0111..846b8b54 100644 --- a/generated/wiener_levy_analytic_calculus/ChallengeDeps.lean +++ b/generated/wiener_levy_analytic_calculus/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval.Analysis.WienerLevy diff --git a/generated/wigner_semicircle/ChallengeDeps.lean b/generated/wigner_semicircle/ChallengeDeps.lean index a5da14c2..254ca905 100644 --- a/generated/wigner_semicircle/ChallengeDeps.lean +++ b/generated/wigner_semicircle/ChallengeDeps.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean namespace LeanEval namespace Analysis diff --git a/generated/zhang_bounded_prime_gaps/Challenge.lean b/generated/zhang_bounded_prime_gaps/Challenge.lean index 3289e500..fa7bfd87 100644 --- a/generated/zhang_bounded_prime_gaps/Challenge.lean +++ b/generated/zhang_bounded_prime_gaps/Challenge.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean open Filter Finset MeasureTheory open scoped BigOperators Topology diff --git a/generated/zhang_bounded_prime_gaps/Solution.lean b/generated/zhang_bounded_prime_gaps/Solution.lean index 67c4a774..6a1a03d4 100644 --- a/generated/zhang_bounded_prime_gaps/Solution.lean +++ b/generated/zhang_bounded_prime_gaps/Solution.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission open Filter Finset MeasureTheory diff --git a/generated/zhang_bounded_prime_gaps/Submission.lean b/generated/zhang_bounded_prime_gaps/Submission.lean index 2fad20b3..f49f306c 100644 --- a/generated/zhang_bounded_prime_gaps/Submission.lean +++ b/generated/zhang_bounded_prime_gaps/Submission.lean @@ -1,7 +1,4 @@ import Mathlib -import Lake.Toml -import Lake.Util.Message -import Lean import Submission.Helpers open Filter Finset MeasureTheory diff --git a/tests/lean/EvalToolsTests/GenerateTest.lean b/tests/lean/EvalToolsTests/GenerateTest.lean index 813768a6..29a9fa65 100644 --- a/tests/lean/EvalToolsTests/GenerateTest.lean +++ b/tests/lean/EvalToolsTests/GenerateTest.lean @@ -1220,15 +1220,16 @@ def main : IO UInt32 := do catch _ => pure true pure <| assertEq "prelude rejected" rejected true - check "problemImportHeader preserves the environment behind EvalTools.Markers" passes fails do + check "problemImportHeader omits marker implementation imports" passes fails do let root ← IO.currentDir let header ← problemImportHeader root "LeanEval.ProgramVerification.PermuteToUnimodal" - pure <| assertEq "Lean retained" (header.find? "import Lean\n").isSome true |>.or - (assertEq "Lake Toml retained" (header.find? "import Lake.Toml\n").isSome true) |>.or - (assertEq "Lake messages retained" - (header.find? "import Lake.Util.Message\n").isSome true) |>.or - (assertEq "repository-only marker removed" - (header.find? "import EvalTools.Markers\n").isSome false) + pure <| assertEq "marker-only module needs no imports" header "" + + check "problemImportHeader preserves narrow mathematical imports" passes fails do + let root ← IO.currentDir + let header ← problemImportHeader root "LeanEval.Combinatorics.Ramsey" + pure <| assertEq "only the mathematical import" header + "import Mathlib.Combinatorics.SimpleGraph.Clique\n" -- `section` opens a scope for `open` just as `namespace` does. Counting only -- namespaces meant the matching `end` popped a namespace frame and discarded