mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.dual.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (x : GaloisCoinsertion l u), x.dual = { choice := x.choice, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
-- Init.Data.Random
StdGen.s1 : StdGen → ℕ
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.instSmoothFstScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.Smooth g],
  AlgebraicGeometry.Smooth (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.RingTheory.MvPolynomial.Groebner
/-- Delete the leading term in a multivariate polynomial (for some monomial order)  -/
MonomialOrder.subLTerm : {σ : Type u_1} → MonomialOrder σ → {R : Type u_2} → [inst : CommRing R] → MvPolynomial σ R → MvPolynomial σ R
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- `MeromorphicNFOn` is invariant under translation, special case where the set is a closed ball.
 -/
meromorphicNFOn_closedBall_comp_sub_const_iff_meromorphicNFOn_closedBall : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ},
  MeromorphicNFOn (f ∘ fun x => x - c) (Metric.closedBall c R) ↔ MeromorphicNFOn f (Metric.closedBall 0 R)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.exists_sup_eq_iSup : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] [WellFoundedGT β] (f : α → β), ∃ t, t.sup f = ⨆ a, f a
-- Mathlib.Topology.FiberBundle.Constructions
/-- Homeomorphism between the total space of the trivial bundle and the Cartesian product.  -/
Bundle.Trivial.homeomorphProd : (B : Type u_1) →
  (F : Type u_2) →
    [inst : TopologicalSpace B] → [inst_1 : TopologicalSpace F] → Bundle.TotalSpace F (Bundle.Trivial B F) ≃ₜ B × F
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_f : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f g).f i =
    CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.snd f (𝒰.f i))
      (CategoryTheory.Limits.pullback.snd g (𝒰.f i)) f g (CategoryTheory.Limits.pullback.fst f (𝒰.f i))
      (CategoryTheory.Limits.pullback.fst g (𝒰.f i)) (𝒰.f i) ⋯ ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k} {fallback : α},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.maxKeyD fallback =
    t.maxKey?.elim k fun k' => if compare k' k = Ordering.lt then k else k'
-- Mathlib.Order.GaloisConnection.Basic
OrderIso.bddAbove_preimage : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {s : Set β},
  BddAbove (⇑e ⁻¹' s) ↔ BddAbove s
-- Mathlib.Geometry.Manifold.Instances.Real
boundary_Icc : ∀ {x y : ℝ} [hxy : Fact (x < y)], ModelWithCorners.boundary ↑(Set.Icc x y) = {⊥, ⊤}
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.QuotientBot.infinite : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Infinite M],
  Infinite (M ⧸ ⊥)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceDiv : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
hasFDerivWithinAt_comp_smul_smul_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {f' : E →L[𝕜] F} {x : E} {c : 𝕜},
  HasFDerivWithinAt (fun x => f (c • x)) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₂_le_iff : ∀ {a x : Ordinal.{u}}, x.invVeblen₂ ≤ a ↔ Ordinal.omega0 ^ x ≤ Ordinal.veblen x.invVeblen₁ a
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.divInvOneMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : Pow M₁ ℕ] [inst_3 : Inv M₁]
  [inst_4 : Div M₁] [inst_5 : Pow M₁ ℤ] [inst_6 : DivInvOneMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
  (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n),
  Function.Injective.divInvOneMonoid f hf one mul inv div npow zpow =
    { toDivInvMonoid := Function.Injective.divInvMonoid f hf one mul inv div npow zpow, inv_one := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasDerivWithinAt.ccosh : ∀ {f : ℂ → ℂ} {f' x : ℂ} {s : Set ℂ},
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) * f') s x
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.mod_X_sub_C_eq_C_eval : ∀ {R : Type u} [inst : Field R] (p : Polynomial R) (a : R),
  p % (Polynomial.X - Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
/-- If `P` holds for `f` over affine opens `U₂` of `Y` and `V₂` of `X` and `U₁` (resp. `V₁`) are
open affine neighborhoods of `x` (resp. `f.base x`), then `P` also holds for `f`
over some basic open of `U₁` (resp. `V₁`).  -/
AlgebraicGeometry.exists_basicOpen_le_appLE_of_appLE_of_isAffine : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {X Y : AlgebraicGeometry.Scheme}
  {f : X ⟶ Y},
  (RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P) →
      ∀ (x : ↥X) (U₁ U₂ : ↑Y.affineOpens) (V₁ V₂ : ↑X.affineOpens),
        x ∈ ↑V₁ →
          x ∈ ↑V₂ →
            ∀ (e₂ : ↑V₂ ≤ (TopologicalSpace.Opens.map f.base).obj ↑U₂),
              P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) →
                f x ∈ ↑U₁ →
                  ∃ r s,
                    ∃ (_ : x ∈ X.basicOpen s) (e :
                      X.basicOpen s ≤ (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen r)),
                      P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.ofAlgEquiv_toAlgEquiv : ∀ {R : Type u_6} {A : Type u_7} {B : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Star A] [inst_6 : Star B] (f : A ≃⋆ₐ[R] B)
  (map_star : ∀ (x : A), f.toAlgEquiv (star x) = star (f.toAlgEquiv x)),
  StarAlgEquiv.ofAlgEquiv f.toAlgEquiv map_star = f
-- Mathlib.Data.List.Cycle
Cycle.nodup_coe_iff : ∀ {α : Type u_1} {l : List α}, (↑l).Nodup ↔ l.Nodup
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_image_prod : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, (fun x => x.1 + x.2) '' s ×ˢ t = s + t
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.assignLevel : ℕ → Lean.Level → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_zero_measure : ∀ {α : Type u_1} {ε : Type u_4} [inst : ENorm ε] {m : MeasurableSpace α} (f : α → ε),
  MeasureTheory.HasFiniteIntegral f 0
-- Mathlib.LinearAlgebra.Dimension.LinearMap
LinearMap.rank_finsetSum_le : ∀ {K : Type u} {V : Type v} {V' : Type v'} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V'] [inst_4 : Module K V'] {η : Type u_1} (s : Finset η) (f : η → V →ₗ[K] V'),
  (∑ d ∈ s, f d).rank ≤ ∑ d ∈ s, (f d).rank
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.mem_source_at : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) (b : B)
  (a : F), ⟨b, a⟩ ∈ (Z.localTrivAt b).source
-- Mathlib.Topology.Sheaves.Skyscraper
/-- Taking skyscraper presheaf at a point is functorial: `c ↦ skyscraper p₀ c` defines a functor by
sending every `f : a ⟶ b` to the natural transformation `α` defined as: `α(U) = f : a ⟶ b` if
`p₀ ∈ U` and the unique morphism to a terminal object in `C` if `p₀ ∉ U`.
 -/
SkyscraperPresheafFunctor.map' : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{w, v} C] →
          [inst_2 : CategoryTheory.Limits.HasTerminal C] →
            {a b : C} → (a ⟶ b) → (skyscraperPresheaf p₀ a ⟶ skyscraperPresheaf p₀ b)
-- Mathlib.Tactic.LinearCombination
/-- Implementation of `linear_combination`.  -/
Mathlib.Tactic.LinearCombination.elabLinearCombination : Lean.Syntax → Option Lean.Syntax.Tactic → Option Lean.NumLit → Option Lean.Term → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Order.Booleanisation
/-- The complement operator on `Booleanisation α` sends `a` to `aᶜ` and `aᶜ` to `a`, for `a : α`.  -/
Booleanisation.instCompl : {α : Type u_1} → Compl (Booleanisation α)
-- Init.Data.Zero
Zero.toOfNat0 : {α : Type u_1} → [Zero α] → OfNat α 0
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor on `GrpCat.{u}` creates `u`-small limits.
 -/
GrpCat.instCreatesLimitsOfSizeUliftFunctor : CategoryTheory.CreatesLimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} GrpCat.uliftFunctor
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `C` has all (small) limits if it has limits of every shape that is as big as its hom-sets.  -/
CategoryTheory.Limits.HasLimits : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.insert_ne_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}, t.insert k ≠ ∅
-- Std.Http.Data.Status
/-- 424 Failed Dependency
 -/
Std.Http.Status.failedDependency : Std.Http.Status
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.forIn'_toArray_eq_forIn' : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α] [DecidableLT α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.Rxc.IsAlwaysFinite α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_9 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)},
  forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- If `s` is a set in an extended metric space `X` with second countable topology and `f : X → Y`
is Lipschitz in a neighborhood within `s` of every point `x ∈ s`, then the Hausdorff dimension of
the image `f '' s` is at most the Hausdorff dimension of `s`.  -/
dimH_image_le_of_locally_lipschitzOn : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [SecondCountableTopology X]
  {f : X → Y} {s : Set X}, (∀ x ∈ s, ∃ C, ∃ t ∈ nhdsWithin x s, LipschitzOnWith C f t) → dimH (f '' s) ≤ dimH s
-- Mathlib.Topology.Algebra.Module.LinearPMap
LinearPMap.hasCore_def : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F} {S : Submodule R E}, f.HasCore S → (f.domRestrict S).closure = f
-- Mathlib.Tactic.Linarith.Frontend
/-- If true, `linarith?` attempts to greedily remove unused hypotheses from its
suggestion.  -/
Mathlib.Tactic.Linarith.LinarithConfig.minimize : Mathlib.Tactic.Linarith.LinarithConfig → Bool
-- Mathlib.Logic.Relation
Relation.ReflGen.refl : ∀ {α : Type u_1} {r : α → α → Prop} {a : α}, Relation.ReflGen r a a
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- The additive subgroup fixing a set under an `AddAction`.  -/
fixingAddSubgroup : (M : Type u_1) → {α : Type u_2} → [inst : AddGroup M] → [AddAction M α] → Set α → AddSubgroup M
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.rfl : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp}, t.Equiv t
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.ACM.Context.mk.injEq : ∀ (opId opId_1 : ℕ), ({ opId := opId } = { opId := opId_1 }) = (opId = opId_1)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_eq_of_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → ∀ {k : α}, m₁.contains k = m₂.contains k
-- Mathlib.Topology.Homeomorph.Lemmas
/-- The product `Π t : α, f t` of a family of topological spaces is homeomorphic to the
space `f ⬝` when `α` only contains `⬝`.

This is `Equiv.piUnique` as a `Homeomorph`.
 -/
Homeomorph.piUnique : {α : Type u_7} →
  [inst : Unique α] → (f : α → Type u_8) → [inst_1 : (x : α) → TopologicalSpace (f x)] → ((t : α) → f t) ≃ₜ f default
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- An `InjectiveResolution Z` consists of a bundled `ℕ`-indexed cochain complex of injective objects,
along with a quasi-isomorphism from the complex consisting of just `Z` supported in degree `0`.
 -/
CategoryTheory.InjectiveResolution : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroObject C] → [CategoryTheory.Limits.HasZeroMorphisms C] → C → Type (max u v)
-- Init.Data.String.Lemmas.FindPos
_private.Init.Data.String.Lemmas.FindPos.0.String.Slice.Pos.prevn.eq_1 : ∀ {s : String.Slice} (p : s.Pos), p.prevn 0 = p
-- Init.Data.Rat.Lemmas
Rat.ofScientific_true_def : ∀ {m e : ℕ}, Rat.ofScientific m true e = mkRat (↑m) (10 ^ e)
-- Mathlib.Algebra.Homology.EulerCharacteristic
GradedObject.eulerChar.eq_1 : ∀ {R : Type u_1} [inst : Ring R] {ι : Type u_2} (c : ComplexShape ι) [inst_1 : c.EulerCharSigns]
  (X : CategoryTheory.GradedObject ι (ModuleCat R)),
  GradedObject.eulerChar c X = ∑ᶠ (i : ι), ↑(c.χ i) * ↑(Module.finrank R ↑(X i))
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.FunctorCategory.tensorObj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (F G : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Monoidal.FunctorCategory.tensorObj F G).map f =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (G.map f)
-- Mathlib.Algebra.Category.CommHopfAlgCat
/-- Commutative Hopf algebra equivalences between `HopfAlgebra`s are the same as isomorphisms in
`CommHopfAlgCat R`.  -/
CommHopfAlgCat.isoEquivBialgEquiv : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      [inst_1 : CommRing X] →
        [inst_2 : HopfAlgebra R X] →
          [inst_3 : CommRing Y] →
            [inst_4 : HopfAlgebra R Y] →
              ({ X := X, commRing := inst_1, hopfAlgebra := inst_2 } ≅
                  { X := Y, commRing := inst_3, hopfAlgebra := inst_4 }) ≃
                X ≃ₐc[R] Y
-- Lean.Parser.Command
Lean.Parser.Command.eoi.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Measure.NullMeasurable
Set.Finite.nullMeasurableSet : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)], s.Finite → MeasureTheory.NullMeasurableSet s μ
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.jacobianRelations_spec : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) [inst_4 : DecidableEq σ]
  [inst_5 : Fintype σ], ∑ i, P.jacobianRelations i * P.relation i = P.jacobiMatrix.det * P.σ ↑⋯.unit⁻¹ - 1
-- Mathlib.Order.BoundedOrder.Monotone
antitone_le : ∀ {α : Type u} [inst : Preorder α] {x : α}, Antitone fun x_1 => x_1 ≤ x
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.card_support_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {p : SkewPolynomial R}, p.support.card = 0 ↔ p = 0
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.isPWO_support_smulAntidiagonal : ∀ {G : Type u_1} {P : Type u_2} [inst : SMul G P] [inst_1 : PartialOrder G] [inst_2 : PartialOrder P]
  [inst_3 : IsOrderedCancelSMul G P] {s : Set G} {t : Set P} (hs : s.IsPWO) (ht : t.IsPWO),
  {a | (Finset.SMulAntidiagonal a ⋯).Nonempty}.IsPWO
-- Lean.Meta.Constructions.NoConfusion
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.mkNoConfusionCoreImp : Lean.Name → Lean.MetaM Unit
-- Mathlib.Data.Nat.Digits.Defs
Nat.mul_ofDigits : ∀ (n : ℕ) {b : ℕ} {l : List ℕ}, n * Nat.ofDigits b l = Nat.ofDigits b (List.map (fun x => n * x) l)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.mk.injEq : ∀ {C : Type u} (I : Type w) (obj : I → C) (I_1 : Type w) (obj_1 : I_1 → C),
  ({ I := I, obj := obj } = { I := I_1, obj := obj_1 }) = (I = I_1 ∧ obj ≍ obj_1)
-- Batteries.Recycling.RBTree.WF
/-- The well-formedness invariant implies the ordering and balance properties.  -/
RBTree.RBNode.WF.out : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α},
  RBTree.RBNode.WF cmp t → RBTree.RBNode.Ordered cmp t ∧ ∃ c n, t.Balanced c n
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.moduleTk.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.sup : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SemilatticeSup β] {f g : α → β} {a : α} {s : Set α},
  IsLocalMaxOn f s a → IsLocalMaxOn g s a → IsLocalMaxOn (fun x => f x ⊔ g x) s a
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.Definable.mk : {n : ℕ} →
  {f : (Fin n → ZFSet.{u}) → ZFSet.{u}} →
    (out : (Fin n → PSet.{u}) → PSet.{u}) →
      autoParam (∀ (xs : Fin n → PSet.{u}), ZFSet.mk (out xs) = f fun x => ZFSet.mk (xs x))
          ZFSet.Definable.mk_out._autoParam →
        ZFSet.Definable n f
-- Mathlib.NumberTheory.ModularForms.NormTrace
ModularForm.norm.congr_simp : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f f_1 : F),
  f = f_1 →
    ∀ [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ} [inst_1 : 𝒢.IsFiniteRelIndex ℋ] [inst_2 : ℋ.HasDetPlusMinusOne]
      [inst_3 : ModularFormClass F 𝒢 k], ModularForm.norm ℋ f = ModularForm.norm ℋ f_1
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.J_sq : UpperHalfPlane.J ^ 2 = 1
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.brecOn.go : {motive : Lean.Grind.Linarith.Expr → Sort u} →
  (t : Lean.Grind.Linarith.Expr) →
    ((t : Lean.Grind.Linarith.Expr) → Lean.Grind.Linarith.Expr.below t → motive t) →
      motive t ×' Lean.Grind.Linarith.Expr.below t
-- Init.Data.Nat.Lemmas
Nat.self_add_sub_one : ∀ (n : ℕ), n + (n - 1) = 2 * n - 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a fallback : α}, ∅.getKeyD a fallback = fallback
-- Mathlib.Util.Export
Lean.Export.State.exprs : Lean.Export.State → Lean.Export.Alloc Lean.Expr
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- `SignedMeasure.toMeasureOfZeroLE` is a finite measure.  -/
MeasureTheory.SignedMeasure.toMeasureOfZeroLE_finite : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) {i : Set α}
  (hi : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i) (hi₁ : MeasurableSet i),
  MeasureTheory.IsFiniteMeasure (s.toMeasureOfZeroLE i hi₁ hi)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The obvious morphism `E.Y j ⟶ pullback (E.f i₁) (E.f i₂)` given by `E : PreOneHypercover S`.  -/
CategoryTheory.PreOneHypercover.toPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (E : CategoryTheory.PreOneHypercover S) →
        {i₁ i₂ : E.I₀} →
          [inst_1 : CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] →
            (j : E.I₁ i₁ i₂) → E.Y j ⟶ CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.getEntry?.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List ((a : α) × β a) → Sort u_3) (h_1 : Unit → motive [])
  (h_2 : (k : α) → (v : β k) → (l : List ((a : α) × β a)) → motive (⟨k, v⟩ :: l)),
  (match [] with
    | [] => h_1 ()
    | ⟨k, v⟩ :: l => h_2 k v l) =
    h_1 ()
-- Mathlib.Order.Interval.Set.Defs
Set.mem_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Ioc a b ↔ a < x ∧ x ≤ b
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasSumUniformlyOn_univ_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α], HasSumUniformlyOn f g Set.univ ↔ HasSumUniformly f g
-- Mathlib.CategoryTheory.Filtered.Small
/-- The full subcategory induced by the filtered closure of a family of objects is filtered.  -/
CategoryTheory.IsFiltered.instIsFilteredOrEmptyFullSubcategoryFilteredClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  (f : α → C), CategoryTheory.IsFilteredOrEmpty (CategoryTheory.IsFiltered.filteredClosure f).FullSubcategory
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.PreOneHypercover.map_p₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} (E : CategoryTheory.PreOneHypercover X) (F : CategoryTheory.Functor C D)
  (x x_1 : (CategoryTheory.PreZeroHypercover.map F E.toPreZeroHypercover).I₀) (j : E.I₁ x x_1),
  (E.map F).p₂ j = F.map (E.p₂ j)
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_fst_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => β} (h : m.WF) {a : α}
  {b : β},
  (Std.DHashMap.Raw.Const.getThenInsertIfNew? m a b).1 =
    (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? ⟨m, ⋯⟩ a b).1
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.mul_polynomial : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β]
  [ContinuousAdd β] [ContinuousMul β],
  Asymptotics.SuperpolynomialDecay l k f →
    ∀ (p : Polynomial β), Asymptotics.SuperpolynomialDecay l k fun x => f x * Polynomial.eval (k x) p
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The algebra isomorphism between multivariable polynomials in `Fin (n + 1)` and
polynomials over multivariable polynomials in `Fin n`.
 -/
MvPolynomial.finSuccEquiv : (R : Type u) →
  [inst : CommSemiring R] → (n : ℕ) → MvPolynomial (Fin (n + 1)) R ≃ₐ[R] Polynomial (MvPolynomial (Fin n) R)
-- Mathlib.Data.Rat.Floor
Rat.ceil_intCast_div_natCast : ∀ (n : ℤ) (d : ℕ), ⌈↑n / ↑d⌉ = -(-n / ↑d)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_lt_sub_right : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, a < b → ∀ (c : α), a - c < b - c
-- Mathlib.Dynamics.BirkhoffSum.Average
birkhoffAverage_zero : ∀ (R : Type u_1) {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (f : α → α) (g : α → M) (x : α), birkhoffAverage R f g 0 x = 0
-- Mathlib.RingTheory.Artinian.Module
isArtinian_submodule' : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsArtinian R M]
  (N : Submodule R M), IsArtinian R ↥N
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_cons_of_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  (k == a) = true → Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = true
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
MulOpposite.opUniformEquivRight.eq_1 : ∀ (G : Type u_2) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  MulOpposite.opUniformEquivRight G =
    { toEquiv := MulOpposite.opEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }