mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.pos_of_isNat' : ∀ {A : Type u_1} {e : A} {n : ℕ} [inst : AddMonoidWithOne A] [inst_1 : PartialOrder A] [AddLeftMono A]
  [ZeroLEOneClass A] [h'' : NeZero 1], Mathlib.Meta.NormNum.IsNat e n → Nat.ble 1 n = true → 0 < e
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The forgetful functor from comonoid objects to the ambient category reflects isomorphisms.  -/
CategoryTheory.Comon.instReflectsIsomorphismsForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Comon.forget C).ReflectsIsomorphisms
-- Init.Grind.Annotated
/-- `grind_annotated "YYYY-MM-DD"` marks the current file as having been manually annotated for `grind`.

When the LibrarySuggestion framework is called with `caller := "grind"` (as happens when using
`grind +suggestions`), theorems from grind-annotated files are excluded from premise selection.
This is because these files have already been manually reviewed and annotated with appropriate
`@[grind]` attributes.

The date argument (in YYYY-MM-DD format) records when the file was annotated. This is currently
informational only, but may be used in the future to detect files that have been significantly
modified since annotation and may need re-review.

Example:
```
grind_annotated "2025-01-15"
```

This command should typically appear near the top of a file, after imports.
 -/
Lean.Parser.Command.grindAnnotated : Lean.ParserDescr
-- Mathlib.Tactic.NormNum.Core
/-- Erased `norm_num`s.  -/
Mathlib.Meta.NormNum.NormNums.erased : Mathlib.Meta.NormNum.NormNums → Lean.PHashSet Lean.Name
-- Std.Time.Date.Unit.Day
Std.Time.Day.instLTOrdinal : LT Std.Time.Day.Ordinal
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceShiftRight : Lean.Meta.Simp.DSimproc
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_insertIfNew : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β},
  Std.ExtDTreeMap.Const.get? (t.insertIfNew k v) a =
    if cmp k a = Ordering.eq ∧ k ∉ t then some v else Std.ExtDTreeMap.Const.get? t a
-- Mathlib.Algebra.Order.Ring.Abs
_private.Mathlib.Algebra.Order.Ring.Abs.0.geomSum.eq_1 : ∀ {α : Type u_1} [inst : CommRing α] (a b : α), geomSum✝ a b 0 = 1
-- Mathlib.Data.PFun
PFun.fix.match_1.congr_eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : β ⊕ α → Sort u_3) (x : β ⊕ α)
  (h_1 : (b : β) → x = Sum.inl b → motive (Sum.inl b)) (h_2 : (a' : α) → x = Sum.inr a' → motive (Sum.inr a')) (a' : α)
  (heq_1 : x = Sum.inr a'),
  (match e : x with
    | Sum.inl b => h_1 b e
    | Sum.inr a' => h_2 a' e) ≍
    h_2 a' heq_1
-- Mathlib.Data.Multiset.Sort
Multiset.coe_sort : ∀ {α : Type u_1} (l : List α) (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], (↑l).sort r = l.mergeSort fun x1 x2 => decide (r x1 x2)
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.unop_top : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], ⊤.unop = ⊤
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F}
  [inst_2 : SizeOf C] (val : A.obj ⟶ B.obj)
  (comp :
    autoParam ((CategoryTheory.ConcreteCategory.hom (F.map val)) A.pt = B.pt)
      CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp._autoParam),
  sizeOf { val := val, comp := comp } = 1 + sizeOf val + sizeOf comp
-- Mathlib.MeasureTheory.Function.EssSup
essSup_map_measure : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {γ : Type u_3} {mγ : MeasurableSpace γ} {f : α → γ} {g : γ → β}
  [inst_1 : MeasurableSpace β] [inst_2 : TopologicalSpace β] [SecondCountableTopology β] [OrderClosedTopology β]
  [OpensMeasurableSpace β],
  AEMeasurable g (MeasureTheory.Measure.map f μ) →
    AEMeasurable f μ →
      autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae (MeasureTheory.Measure.map f μ)) g)
          essSup_map_measure._auto_1 →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) (g ∘ f))
            essSup_map_measure._auto_3 →
          autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) (g ∘ f))
              essSup_map_measure._auto_5 →
            autoParam
                (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae (MeasureTheory.Measure.map f μ)) g)
                essSup_map_measure._auto_7 →
              essSup g (MeasureTheory.Measure.map f μ) = essSup (g ∘ f) μ
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.instInhabited : (ι : Type u_1) → (β : ι → Type u_2) → [inst : (i : ι) → AddCommMonoid (β i)] → Inhabited (DirectSum ι β)
-- Init.Data.List.Scan.Lemmas
Id.run.eq_1 : ∀ {α : Type u_1} (x : Id α), x.run = x
-- Mathlib.GroupTheory.Finiteness
AddMonoid.fg_def : ∀ {M : Type u_1} [inst : AddMonoid M], AddMonoid.FG M ↔ ⊤.FG
-- Init.Data.Nat.Power2.Basic
Nat.nextPowerOfTwo_dec : ∀ {n power : ℕ}, power > 0 → power < n → n - power * 2 < n - power
-- Mathlib.Data.Num.Lemmas
PosNum.le_iff_cmp : ∀ {m n : PosNum}, m ≤ n ↔ m.cmp n ≠ Ordering.gt
-- Mathlib.AlgebraicGeometry.Sites.Representability
/-- We get a family of gluing data by taking `U i = X i` and `V i j = (hf i).rep.pullback (f j)`.  -/
AlgebraicGeometry.Scheme.LocalRepresentability.glueData : {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} →
  {ι : Type u} →
    {X : ι → AlgebraicGeometry.Scheme} →
      {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} →
        (∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) → AlgebraicGeometry.Scheme.GlueData
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.id_apply : ∀ (α : Type u_7) [inst : MulZeroOneClass α] (x : α), (MonoidWithZeroHom.id α) x = x
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The L-function of a non-trivial Dirichlet character is differentiable everywhere.  -/
DirichletCharacter.differentiable_LFunction : ∀ {N : ℕ} [inst : NeZero N] {χ : DirichletCharacter ℂ N}, χ ≠ 1 → Differentiable ℂ (DirichletCharacter.LFunction χ)
-- Lean.Meta.Tactic.Grind.OrderInsts
Lean.Meta.Grind.mkIsLinearPreorderInst? : Lean.Level → Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minEntry?_nil : ∀ {α : Type u} {β : α → Type v} [inst : Ord α], Std.Internal.List.minEntry? [] = none
-- Init.Meta.Defs
/-- Creates literal syntax for the given character.

If `info` is provided, then the literal's source information is copied from it.
 -/
Lean.Syntax.mkCharLit : Char → optParam Lean.SourceInfo Lean.SourceInfo.none → Lean.CharLit
-- Mathlib.RingTheory.Algebraic.Basic
/-- An element `x` is transcendental over `R` if and only if the kernel of the ring homomorphism
`Polynomial.aeval x` is the zero ideal. This is similar to `algebraicIndependent_iff_ker_eq_bot`.  -/
transcendental_iff_ker_eq_bot : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x : A},
  Transcendental R x ↔ RingHom.ker (Polynomial.aeval x) = ⊥
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.dist_def : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f g : ↥(MeasureTheory.Lp E p μ)),
  dist f g = (MeasureTheory.eLpNorm (↑↑f - ↑↑g) p μ).toReal
-- Std.Do.SPred.SPred
Std.Do.SPred.down_pure_nil : ∀ {P : Prop}, ⌜P⌝.down = P
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.mk_smul : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] {α : Type u_4}
  [inst_3 : MulAction (GL n R) α] (h : ∀ (u : Rˣ) (a : α), (Matrix.GeneralLinearGroup.scalar n) u • a = a) (g : GL n R)
  (a : α), Matrix.ProjGenLinGroup.mk g • a = g • a
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.foldl_filterMap'.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Mathlib.Data.Rel
SetRel.exists_graph_eq_iff : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β), (∃! f, Function.graph f = R) ↔ ∀ (a : α), ∃! b, (a, b) ∈ R
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.mk.injEq : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} (idxFun : ι → α ⊕ η) (proper : ∀ (e : η), ∃ i, idxFun i = Sum.inr e)
  (idxFun_1 : ι → α ⊕ η) (proper_1 : ∀ (e : η), ∃ i, idxFun_1 i = Sum.inr e),
  ({ idxFun := idxFun, proper := proper } = { idxFun := idxFun_1, proper := proper_1 }) = (idxFun = idxFun_1)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `MulDistribMulActionHomClass F M A B` states that `F` is a type of morphisms preserving
the monoid structure and equivariant with respect to the action of `M`.
It is an abbreviation to `MulDistribMulActionHomClass F (MonoidHom.id M) A B`
You should extend this class when you extend `MulDistribMulActionHom`.  -/
MulDistribMulActionHomClass : (F : Type u_10) →
  (M : outParam (Type u_11)) →
    (A : outParam (Type u_12)) →
      (B : outParam (Type u_13)) →
        [inst : Monoid M] →
          [inst_1 : Monoid A] →
            [inst_2 : Monoid B] → [MulDistribMulAction M A] → [MulDistribMulAction M B] → [FunLike F A B] → Prop
-- Init.Data.Fin.Lemmas
Fin.val_add_one_of_lt : ∀ {n : ℕ} {i : Fin n.succ}, i < Fin.last n → ↑(i + 1) = ↑i + 1
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.uniformContinuous_map₂ : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
  [inst_2 : UniformSpace γ] (f : α → β → γ), UniformContinuous₂ (UniformSpace.Completion.map₂ f)
-- Mathlib.RingTheory.WittVector.Compare
TruncatedWittVector.charP_zmod : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), CharP (TruncatedWittVector p n (ZMod p)) (p ^ n)
-- Mathlib.Topology.ContinuousMap.T0Sierpinski
TopologicalSpace.eq_induced_by_maps_to_sierpinski : ∀ (X : Type u_1) [t : TopologicalSpace X], t = ⨅ u, TopologicalSpace.induced (fun x => x ∈ u) sierpinskiSpace
-- Mathlib.Data.Complex.Basic
Complex.ofReal_qsmul : ∀ (q : ℚ) (r : ℝ), ↑(q • r) = q • ↑r
-- Mathlib.Data.PNat.Basic
PNat.mod_add_div : ∀ (m k : ℕ+), ↑(m.mod k) + ↑k * m.div k = ↑m
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.atomic_length : ∀ (n : ℕ), (OrderedFinpartition.atomic n).length = n
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.reduceCyclically.conjugator.singleton : ∀ {α : Type u} [inst : DecidableEq α] {a : α × Bool}, FreeAddGroup.reduceCyclically.conjugator [a] = []
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.other : Lean.Meta.DiscrTree.Key
-- Mathlib.AlgebraicTopology.DoldKan.Equivalence
/-- The Dold-Kan equivalence for abelian categories  -/
CategoryTheory.Abelian.DoldKan.equivalence : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [inst_1 : CategoryTheory.Abelian A] → CategoryTheory.SimplicialObject A ≌ ChainComplex A ℕ
-- Init.Data.List.Lemmas
List.length_insert_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, a ∉ l → (List.insert a l).length = l.length + 1
-- Mathlib.Algebra.Order.CauSeq.Completion
/-- Show the first 10 items of a representative of this equivalence class of Cauchy sequences.

The representative chosen is the one passed in the VM to `Quot.mk`, so two Cauchy sequences
converging to the same number may be printed differently.
 -/
CauSeq.Completion.instReprCauchy : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : DivisionRing β] →
            {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → [Repr β] → Repr (CauSeq.Completion.Cauchy abv)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.«term_∙_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.eLpNorm_sum_le : ∀ {α : Type u_1} {ε' : Type u_4} {m : MeasurableSpace α} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddCommMonoid ε'] {p : ENNReal} {μ : MeasureTheory.Measure α} [ContinuousAdd ε'] {ι : Type u_5}
  {f : ι → α → ε'} {s : Finset ι},
  (∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) →
    1 ≤ p → MeasureTheory.eLpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, MeasureTheory.eLpNorm (f i) p μ
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.ofMapSub.eq_1 : ∀ {G : Type u_5} [inst : AddGroup G] {H : Type u_8} [inst_1 : AddGroup H] (f : G → H)
  (hf : ∀ (x y : G), f (x - y) = f x - f y), AddMonoidHom.ofMapSub f hf = AddMonoidHom.ofMapAddNeg f ⋯
-- Mathlib.RingTheory.PowerSeries.Log
PowerSeries.HasSubst.exp_sub_one : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A], PowerSeries.HasSubst (PowerSeries.exp A - 1)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldrM_eq_foldrM_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ},
  Std.TreeMap.Raw.foldrM (fun a x d => f a d) init t = List.foldrM f init t.keys
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_rpow_eq_mul_logb_of_pos : ∀ {b x y : ℝ}, 0 < x → Real.logb b (x ^ y) = y * Real.logb b x
-- Mathlib.NumberTheory.SumPrimeReciprocals
/-- Reindex a sum over `Nat.Primes` as a sum over `ℕ`, extending `f` by `0`.  -/
Nat.Primes.tsum_eq_tsum_ite : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] (f : ℕ → M),
  ∑' (p : Nat.Primes), f ↑p = ∑' (n : ℕ), if Nat.Prime n then f n else 0
-- Mathlib.Topology.Bornology.Basic
/-- The cofinite filter as a bornology  -/
Bornology.cofinite : {α : Type u_2} → Bornology α
-- Mathlib.Topology.Order.Lattice
OrderDual.continuousSup : ∀ (L : Type u_1) [inst : TopologicalSpace L] [inst_1 : Min L] [h : ContinuousInf L], ContinuousSup Lᵒᵈ
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.measurable_of_not_restrict_le_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v : MeasureTheory.VectorMeasure α M) {i : Set α},
  ¬v.restrict i ≤ MeasureTheory.VectorMeasure.restrict 0 i → MeasurableSet i
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.preComp_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasImage g]
  [inst_2 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.preComp f g) (CategoryTheory.Limits.image.ι g) =
    CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)
-- Init.Data.SInt.Lemmas
ISize.ofNat_bitVecToNat : ∀ (n : BitVec System.Platform.numBits), ISize.ofNat n.toNat = ISize.ofBitVec n
-- Lean.Elab.Binders
Lean.Elab.Term.FunBinders.State : Type
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.preimage_coe_Iio_top : ∀ {α : Type u_1} [inst : Preorder α], WithTop.some ⁻¹' Set.Iio ⊤ = Set.univ
-- Std.Http.Data.Status
Std.Http.Status.notModified.sizeOf_spec : sizeOf Std.Http.Status.notModified = 1
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.subset_ground : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → I ⊆ M.E
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_sum : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E]
  [SecondCountableTopology E],
  ProbabilityTheory.IsGaussianProcess X P → ∀ {I : Finset T}, ProbabilityTheory.HasGaussianLaw (∑ i ∈ I, X i) P
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.symm_mulLeft₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : MeasurableSpace G₀] [inst_2 : MeasurableMul G₀] {g : G₀}
  (hg : g ≠ 0), (MeasurableEquiv.mulLeft₀ g hg).symm = MeasurableEquiv.mulLeft₀ g⁻¹ ⋯
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ (k : α) (f : Option β → Option β), m₁.Equiv m₂ → (m₁.alter k f).Equiv (m₂.alter k f)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.map.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid N']
  [inst_8 : Module R N] [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g],
  IsLocalizedModule.map S f g =
    { toFun := fun h => IsLocalizedModule.lift S f (g ∘ₗ h) ⋯, map_add' := ⋯, map_smul' := ⋯ }
-- Init.Grind.ToInt
Lean.Grind.ToInt.Zero.mk : ∀ {α : Type u} [inst : Zero α] {I : outParam Lean.Grind.IntInterval} [inst_1 : Lean.Grind.ToInt α I],
  ↑0 = 0 → Lean.Grind.ToInt.Zero α I
-- Mathlib.Data.Set.MemPartition
memPartitionSet.eq_def : ∀ {α : Type u_1} (f : ℕ → Set α) (x : ℕ),
  memPartitionSet f x =
    match (motive := ℕ → α → Set α) x with
    | 0 => fun x => Set.univ
    | n.succ => fun a => if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
Std.Iter.val_step_intermediateDropWhile : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} {P : β → Bool} {dropping : Bool},
  ↑(Std.Iter.Intermediate.dropWhile P dropping it).step =
    match ↑it.step with
    | Std.IterStep.yield it' out =>
      if dropping = true then
        match P out with
        | true => Std.IterStep.skip (Std.Iter.Intermediate.dropWhile P true it')
        | false => Std.IterStep.yield (Std.Iter.Intermediate.dropWhile P false it') out
      else Std.IterStep.yield (Std.Iter.Intermediate.dropWhile P false it') out
    | Std.IterStep.skip it' => Std.IterStep.skip (Std.Iter.Intermediate.dropWhile P dropping it')
    | Std.IterStep.done => Std.IterStep.done
-- Batteries.Tactic.Lint.Basic
/-- `noErrorsFound` is the message printed when all tests are negative  -/
Batteries.Tactic.Lint.Linter.noErrorsFound : Batteries.Tactic.Lint.Linter → Lean.MessageData
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] (u : HahnEmbedding.ArchimedeanStrata K M), iSupIndep u.stratum
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.IsPrincipal.sSup : ∀ {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}} {s : Set Ordinal.{u_1}},
  (∀ x ∈ s, Ordinal.IsPrincipal op x) → Ordinal.IsPrincipal op (sSup s)
-- Init.Data.SInt.Lemmas
UInt32.toInt32_ofNat' : ∀ {n : ℕ}, (UInt32.ofNat n).toInt32 = Int32.ofNat n
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.simpForall : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.instInhabitedPrequotient : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → Inhabited (RingCat.Colimits.Prequotient F)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOver : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDedekindDomain S]
  [IsDomain R] [Module.IsTorsionFree R S] (P : Ideal S) [hP : P.IsPrime] {p : Ideal R},
  p ≠ ⊥ → ∀ [hPp : P.LiesOver p], p.ramificationIdx' P ≠ 0
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.Quotient.orbit_inj : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {x y : MulAction.orbitRel.Quotient G α},
  x.orbit = y.orbit ↔ x = y
-- Mathlib.Topology.Semicontinuity.Basic
LowerSemicontinuous.isOpen_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} [inst_1 : Preorder β],
  LowerSemicontinuous f → ∀ (y : β), IsOpen (f ⁻¹' Set.Ioi y)
-- Mathlib.RingTheory.Unramified.LocalRing
Algebra.FormallyUnramified.isField_quotient_map_maximalIdeal : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [Algebra.EssFiniteType R S]
  [Algebra.FormallyUnramified R S], IsField (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))
-- Init.Data.String.Modify
/-- Replaces the first character in `s` with the result of applying `Char.toUpper` to it. Returns the
empty string if the string is empty.

`Char.toUpper` has no effect on characters outside of the range `'a'`–`'z'`.

Examples:
* `"orange".capitalize = "Orange"`
* `"ORANGE".capitalize = "ORANGE"`
* `"".capitalize = ""`
 -/
String.capitalize : String → String
-- Mathlib.Data.Analysis.Topology
/-- A `LocallyFinite.Realizer F f` is a realization that `f` is locally finite, namely it is a
choice of open sets from the basis of `F` such that they intersect only finitely many of the values
of `f`.  -/
LocallyFinite.Realizer : {α : Type u_1} →
  {β : Type u_2} → [inst : TopologicalSpace α] → Ctop.Realizer α → (β → Set α) → Type (max (max u_1 u_2) u_5)
-- Lean.Elab.Term.TermElabM
/-- Return `true` if `e` contains a pending metavariable. Remark: it also visits let-declarations.  -/
Lean.Elab.Term.containsPendingMVar : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticOn.clog : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E},
  AnalyticOn ℂ f s → (∀ z ∈ s, f z ∈ Complex.slitPlane) → AnalyticOn ℂ (fun z => Complex.log (f z)) s
-- Mathlib.Topology.Algebra.GroupCompletion
AddMonoidHom.completion.congr_simp : ∀ {α : Type u_3} {β : Type u_4} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α]
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [inst_5 : IsUniformAddGroup β] (f f_1 : α →+ β) (e_f : f = f_1)
  (hf : Continuous ⇑f), f.completion hf = f_1.completion ⋯
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.StrictMono.eq_liftRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S) {a : ℕ → ℕ}
  (ha : StrictMono a) (f : (n : ℕ) → R →+* S ⧸ I ^ a n)
  (hf : ∀ {m : ℕ}, (Ideal.Quotient.factorPow I ⋯).comp (f (m + 1)) = f m) [inst_2 : IsAdicComplete I S] {F : R →+* S},
  (∀ (n : ℕ), (Ideal.Quotient.mk (I ^ a n)).comp F = f n) → F = IsAdicComplete.StrictMono.liftRingHom I ha f ⋯
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_fun_neg : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (f : X → E),
  ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialOn.continuousOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  CPolynomialOn 𝕜 f s → ContinuousOn f s