mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The functor `SimplicialObject.Split C ⥤ SimplicialObject C` which forgets
the splitting.  -/
CategoryTheory.SimplicialObject.Split.forget : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.Functor (CategoryTheory.SimplicialObject.Split C) (CategoryTheory.SimplicialObject C)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.map_atomRel : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (W : ℤ → R) {F : Type u_3}
  [inst_2 : FunLike F R S] [RingHomClass F R S] (f : F) (a b c d : ℤ),
  f (IsEllipticNet.atomRel W a b c d) = IsEllipticNet.atomRel (⇑f ∘ W) a b c d
-- Mathlib.Computability.Partrec
Computable₂.mk : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ}, (Computable fun p => f p.1 p.2) → Computable₂ f
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.instInhabitedCont.default : Turing.ToPartrec.Cont
-- Mathlib.Data.Finset.Sort
Finset.sortedLT_sort : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α), (s.sort fun a b => a ≤ b).SortedLT
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.id_hom_c : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : AlgebraicGeometry.SheafedSpace C),
  (CategoryTheory.CategoryStruct.id X).hom.c = CategoryTheory.eqToHom ⋯
-- Lean.Elab.App
/-- Return true if the given type contains `OptParam` or `AutoParams`  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.hasOptAutoParams : Lean.Expr → Lean.MetaM Bool
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstr.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof → Sort u} (t : Lean.Meta.Grind.Arith.CommRing.EqCnstr)
  (F_1 : (t : Lean.Meta.Grind.Arith.CommRing.EqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.CommRing.EqCnstrProof) → t.below → motive_2 t),
  t.brecOn F_1 F_2 = F_1 t (Lean.Meta.Grind.Arith.CommRing.EqCnstr.brecOn.go t F_1 F_2).2
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.isCountablySpanning_spanningSets : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ],
  IsCountablySpanning (Set.range (MeasureTheory.spanningSets μ))
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationHints.decreasingBy? : Lean.Elab.TerminationHints → Option Lean.Elab.DecreasingBy
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₁ → k ∈ m₂
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_subtype_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  LinearIndependent R Subtype.val ↔ LinearIndepOn R id s
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_self_ofReal_norm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), ↑‖inner 𝕜 x x‖ = inner 𝕜 x x
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.sphere_eq_empty_of_subsingleton : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α], ε ≠ 0 → Metric.sphere x ε = ∅
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instBot.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M], Submonoid.instBot = { bot := { carrier := {1}, mul_mem' := ⋯, one_mem' := ⋯ } }
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.prod_rightl : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F']
  [inst_2 : SeminormedAddCommGroup G'] {f : α → E} {g' : α → F'} (k' : α → G') {l : Filter α},
  f =o[l] g' → f =o[l] fun x => (g' x, k' x)
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_withDensity_left_of_absolutelyContinuous : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {ν : MeasureTheory.Measure α}
  [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν → AEMeasurable f ν → (μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x => f x * μ.rnDeriv ν x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getKey!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.get! k = t₂.get! k
-- Mathlib.Order.Filter.Extr
IsMaxOn.iSup_eq : ∀ {α : Type u} {β : Type v} [inst : ConditionallyCompleteLinearOrder α] {f : β → α} {s : Set β} {x₀ : β},
  x₀ ∈ s → IsMaxOn f s x₀ → ⨆ x, f ↑x = f x₀
-- Init.Grind.Module.Basic
Lean.Grind.instNegCoOfZeroOfAdd : ∀ {α : Type u_1} {lo hi : ℤ} [inst : Lean.Grind.ToInt α (Lean.Grind.IntInterval.co lo hi)]
  [inst_1 : Lean.Grind.AddCommGroup α] [Lean.Grind.ToInt.Zero α (Lean.Grind.IntInterval.co lo hi)]
  [Lean.Grind.ToInt.Add α (Lean.Grind.IntInterval.co lo hi)], Lean.Grind.ToInt.Neg α (Lean.Grind.IntInterval.co lo hi)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.priority.inj : ∀ {p p_1 : Aesop.Frontend.Priority}, Aesop.Frontend.Feature.priority p = Aesop.Frontend.Feature.priority p_1 → p = p_1
-- Mathlib.Data.Seq.Defs
/-- If two streams are bisimilar, then they are equal. There are also versions
`eq_of_bisim'` and `eq_of_bisim_strong` that does not mention `IsBisimulation` and look
more like an induction principles.  -/
Stream'.Seq.eq_of_bisim : ∀ {α : Type u} (R : Stream'.Seq α → Stream'.Seq α → Prop),
  Stream'.Seq.IsBisimulation R → ∀ {s₁ s₂ : Stream'.Seq α}, R s₁ s₂ → s₁ = s₂
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.constantsOnSelfStructure : {M : Type w} → (FirstOrder.Language.constantsOn M).Structure M
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
CategoryTheory.Limits.IsInitial.isInitialOfObj.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X : C)
  [inst_2 : CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) G]
  (l l_1 : CategoryTheory.Limits.IsInitial (G.obj X)),
  l = l_1 →
    CategoryTheory.Limits.IsInitial.isInitialOfObj G X l = CategoryTheory.Limits.IsInitial.isInitialOfObj G X l_1
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.MappingConeCompHomotopyEquiv.inv.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃),
  CochainComplex.MappingConeCompHomotopyEquiv.inv f g =
    CochainComplex.mappingCone.desc (CochainComplex.mappingConeCompTriangle f g).mor₁
      ((CochainComplex.mappingCone.snd f).comp (CochainComplex.mappingCone.inl g)
        CochainComplex.MappingConeCompHomotopyEquiv.inv._proof_5)
      (CochainComplex.mappingCone.desc (CategoryTheory.CategoryStruct.comp f g)
        ((CochainComplex.HomComplex.Cochain.ofHom f).comp (CochainComplex.mappingCone.inl g)
          CochainComplex.MappingConeCompHomotopyEquiv.inv._proof_5)
        (CochainComplex.mappingCone.inr g) ⋯)
      ⋯
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.instIsTopologicalAddGroup : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F], IsTopologicalAddGroup (E [⋀^ι]→L[𝕜] F)
-- Init.Data.UInt.Lemmas
UInt32.mul_two : ∀ {a : UInt32}, a * 2 = a + a
-- Mathlib.RingTheory.FreeCommRing
/-- **Alias** of `freeRingPUnitEquivPolynomialInt`.

---

The free ring on a type with one term is isomorphic to `ℤ[X]`.  -/
freeRingPunitEquivPolynomialInt : FreeRing PUnit.{u + 1} ≃+* Polynomial ℤ
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).unop =
    (CategoryTheory.MonoidalCategoryStruct.associator (Opposite.unop X) (Opposite.unop Y) (Opposite.unop Z)).symm
-- Init.Data.String.Modify
/-- Replaces the first character in `s` with the result of applying `Char.toLower` to it. Returns the
empty string if the string is empty.

`Char.toLower` has no effect on characters outside of the range `'A'`–`'Z'`.

Examples:
* `"Orange".decapitalize = "orange"`
* `"ORANGE".decapitalize = "oRANGE"`
* `"".decapitalize = ""`
 -/
String.decapitalize : String → String
-- Mathlib.Algebra.Group.Prod
MonoidHom.mk'.congr_simp : ∀ {M : Type u_4} {G : Type u_7} [inst : Group G] [inst_1 : MulOneClass M] (f f_1 : M → G) (e_f : f = f_1)
  (map_mul : ∀ (a b : M), f (a * b) = f a * f b), MonoidHom.mk' f map_mul = MonoidHom.mk' f_1 ⋯
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- An induction principle for closure membership, for predicates with two arguments.  -/
NonUnitalSubring.closure_induction₂ : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R}
  {p : (x y : R) → x ∈ NonUnitalSubring.closure s → y ∈ NonUnitalSubring.closure s → Prop},
  (∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) →
    (∀ (x : R) (hx : x ∈ NonUnitalSubring.closure s), p 0 x ⋯ hx) →
      (∀ (x : R) (hx : x ∈ NonUnitalSubring.closure s), p x 0 hx ⋯) →
        (∀ (x y : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s),
            p x y hx hy → p (-x) y ⋯ hy) →
          (∀ (x y : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s),
              p x y hx hy → p x (-y) hx ⋯) →
            (∀ (x y z : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s)
                (hz : z ∈ NonUnitalSubring.closure s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) →
              (∀ (x y z : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s)
                  (hz : z ∈ NonUnitalSubring.closure s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) →
                (∀ (x y z : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s)
                    (hz : z ∈ NonUnitalSubring.closure s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) →
                  (∀ (x y z : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s)
                      (hz : z ∈ NonUnitalSubring.closure s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) →
                    ∀ {x y : R} (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s), p x y hx hy
-- Lean.Environment
/-- An environment stores declarations provided by the user. The kernel
currently supports different kinds of declarations such as definitions, theorems,
and inductive families. Each has a unique identifier (i.e., `Name`), and can be
parameterized by a sequence of universe parameters.
A constant in Lean is just a reference to a `ConstantInfo` object. The main task of
the kernel is to type check these declarations and refuse type incorrect ones. The
kernel does not allow declarations containing metavariables and/or free variables
to be added to an environment. Environments are never destructively updated.

The environment also contains a collection of extensions. For example, the `simp` theorems
declared by users are stored in an environment extension. Users can declare new extensions
using meta-programming.
 -/
Lean.Kernel.Environment : Type
-- Std.Data.DHashMap.Basic
/-- Returns `true` if there is a mapping for the given key. There is also a `Prop`-valued version
of this: `a ∈ m` is equivalent to `m.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for comparisons, while for hash maps, both use `==`.
 -/
Std.DHashMap.contains : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → α → Bool
-- Mathlib.RingTheory.Algebraic.Basic
Polynomial.algEquivOfTranscendental_apply_X : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (s : S)
  (h : Transcendental R s), (Polynomial.algEquivOfTranscendental R s h) Polynomial.X = ⟨s, ⋯⟩
-- Mathlib.Topology.Category.Stonean.Adjunctions
/-- The Stone-Cech compactification functor from types to Stonean spaces.  -/
typeToStonean : CategoryTheory.Functor (Type u) Stonean
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.comp_id : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] (f : P.Hom P'),
  f.comp (Algebra.Extension.Hom.id P) = f
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `ω ↦ exp (u * X ω)` is integrable at `u` and `-u`, then it is integrable on `[-u, u]`.  -/
ProbabilityTheory.integrable_exp_mul_of_abs_le : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t u : ℝ},
  MeasureTheory.Integrable (fun ω => Real.exp (u * X ω)) μ →
    MeasureTheory.Integrable (fun ω => Real.exp (-u * X ω)) μ →
      |t| ≤ |u| → MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instNonUnitalRing : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] →
        [IsOrderedCancelAddMonoid Γ] → [inst : NonUnitalRing R] → NonUnitalRing (HahnSeries Γ R)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The difference with `Finset.sum_ninvolution` is that the involution is allowed to
use membership of the domain of the sum, rather than being a non-dependent function.  -/
Finset.sum_involution : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M} (g : (a : ι) → a ∈ s → ι),
  (∀ (a : ι) (ha : a ∈ s), f a + f (g a ha) = 0) →
    (∀ (a : ι) (ha : a ∈ s), f a ≠ 0 → g a ha ≠ a) →
      ∀ (g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s), (∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a) → ∑ x ∈ s, f x = 0
-- Mathlib.Order.Interval.Set.Disjoint
iUnion_Iic_eq_Iic_iSup : ∀ {ι : Sort u} {R : Type u_1} [inst : CompleteLinearOrder R] {f : ι → R},
  ⨆ i, f i ∈ Set.range f → ⋃ i, Set.Iic (f i) = Set.Iic (⨆ i, f i)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by projection onto the second factor.  -/
ContinuousAddMonoidHom.snd : (A : Type u_2) →
  (B : Type u_3) →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → A × B →ₜ+ B
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesBelow_eq_filter_Ioo_one : ∀ (n : ℕ), n.primesBelow = Finset.filter Nat.Prime (Finset.Ioo 1 n)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_eraseKey_eq_iff_beq_minKeyD_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k fallback : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (Std.Internal.List.minKeyD (Std.Internal.List.eraseKey k l) fallback = Std.Internal.List.minKeyD l fallback ↔
          (k == Std.Internal.List.minKeyD l fallback) = false)
-- Mathlib.Order.Hom.BoundedLattice
instCoeTCSupBotHomOfSupBotHomClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Max α] [inst_2 : Max β] [inst_3 : Bot α]
  [inst_4 : Bot β] [inst_5 : SupBotHomClass F α β],
  instCoeTCSupBotHomOfSupBotHomClass = { coe := fun f => { toFun := ⇑f, map_sup' := ⋯, map_bot' := ⋯ } }
-- Mathlib.Algebra.GroupWithZero.Action.Prod
Prod.distribSMul : {R : Type u_5} →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : AddZeroClass M] →
        [inst_1 : AddZeroClass N] → [DistribSMul R M] → [DistribSMul R N] → DistribSMul R (M × N)
-- Mathlib.Probability.Kernel.MeasurableIntegral
MeasureTheory.StronglyMeasurable.integral_kernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] ⦃f : β → E⦄,
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => ∫ (y : β), f y ∂κ x
-- Std.Do.SPred.SVal
Std.Do.SVal.curry.eq_def : ∀ {α : Type u} {σs : List (Type u)} (f : Std.Do.SVal.StateTuple σs → α),
  Std.Do.SVal.curry f =
    match σs, f with
    | [], f => f PUnit.unit
    | head :: tail, f => fun s => Std.Do.SVal.curry fun s' => f (s, s')
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instNegOfAddOpposite : {M : Type u_1} → [Neg Mᵃᵒᵖ] → Neg Mᵈᵃᵃ
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instInvolutiveNegOfAddOpposite : {M : Type u_1} → [InvolutiveNeg Mᵃᵒᵖ] → InvolutiveNeg Mᵈᵃᵃ
-- Mathlib.Data.Set.Function
Set.InjOn.image_of_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {f : α → β} {g : β → γ},
  Set.InjOn (g ∘ f) s → Set.InjOn g (f '' s)
-- Std.Async.DNS
/-- Asynchronously resolves a hostname and service to an array of socket addresses.
 -/
Std.Async.DNS.getAddrInfo : String → String → optParam (Option Std.Net.AddressFamily) none → Std.Async.Async (Array Std.Net.IPAddr)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpCompIso_hom_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  (X : CategoryTheory.AddGrp C),
  (CategoryTheory.Functor.mapAddGrpCompIso.hom.app X).hom.hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
-- Mathlib.Tactic.TacticAnalysis
/-- Decides what to report to the user.  -/
Mathlib.TacticAnalysis.ComplexConfig.tell : (self : Mathlib.TacticAnalysis.ComplexConfig) →
  Lean.Syntax → List Lean.MVarId → ℕ → self.out → ℕ → Lean.Elab.Command.CommandElabM (Option Lean.MessageData)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.appHom_restrict : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.Sheaf K (Type v)}
  (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) [inst_2 : G.IsCoverDense K] [inst_3 : G.IsLocallyFull K] {X : D} {Y : C}
  (f : Opposite.op X ⟶ Opposite.op (G.obj Y)) (x : (fun X => X) (ℱ.obj (Opposite.op X))),
  (CategoryTheory.ConcreteCategory.hom (ℱ'.obj.map f))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.IsCoverDense.Types.appHom α X)) x) =
    (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) ((CategoryTheory.ConcreteCategory.hom (ℱ.map f)) x)
-- Lean.Meta.Constructions.SparseCasesOn
/-- Information necessary to recognize and split on sparse casesOn (in particular in MatchEqs)  -/
Lean.Meta.SparseCasesOnInfo : Type
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.bot_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat} (x : C), ⊥.obj x = ⊥
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.symm : ∀ {C : Type u} {X Y : CategoryTheory.FreeMonoidalCategory C} (f g : X.Hom Y),
  CategoryTheory.FreeMonoidalCategory.HomEquiv f g → CategoryTheory.FreeMonoidalCategory.HomEquiv g f
-- Init.Data.Format.Basic
Std.Format.group.inj : ∀ {a : Std.Format} {behavior : Std.Format.FlattenBehavior} {a_1 : Std.Format} {behavior_1 : Std.Format.FlattenBehavior},
  a.group behavior = a_1.group behavior_1 → a = a_1 ∧ behavior = behavior_1
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_of_mem_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {f : α → Bool} {k : α}, k ∈ Std.ExtHashSet.filter f m → k ∈ m
-- Mathlib.Order.Bounds.Basic
lowerBounds_Ioc : ∀ {γ : Type u_3} [inst : SemilatticeSup γ] [DenselyOrdered γ] {a b : γ}, a < b → lowerBounds (Set.Ioc a b) = Set.Iic a
-- Std.Data.TreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.TreeMap.entryAtIdxD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → ℕ → α × β → α × β
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, k ∈ t₂ → (t₁ \ t₂).getKey! k = default
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- Custom structure to construct profunctors, i.e. bifunctors `C ⥤ Dᵒᵖ ⥤ Type w`.  -/
CategoryTheory.ProfunctorCore : (C : Type u₁) →
  (D : Type u₂) →
    [CategoryTheory.Category.{v₁, u₁} C] →
      [CategoryTheory.Category.{v₂, u₂} D] → Type (max (max (max (max u₁ u₂) v₁) v₂) (w + 1))
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.toFlag_carrier : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {n : ℕ}
  (b : Module.Basis (Fin n) K V), ↑b.toFlag = Set.range b.flag
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteAtFilter.measure_mono : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f : Filter α},
  μ ≤ ν → ν.FiniteAtFilter f → μ.FiniteAtFilter f
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Pos.skipWhile_eq_skipWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String} {pos : s.Pos},
  pos.skipWhile pat = String.Pos.ofToSlice (pos.toSlice.skipWhile pat)
-- Mathlib.RingTheory.Prime
Prime.neg : ∀ {α : Type u_1} [inst : CommRing α] {p : α}, Prime p → Prime (-p)
-- Mathlib.NumberTheory.Padics.ValuativeRel
Padic.instValuativeRel : {p : ℕ} → [hp : Fact (Nat.Prime p)] → ValuativeRel ℚ_[p]
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.mk.inj : ∀ {G : Type u} {inst : AddGroup G} {inst_1 : TopologicalSpace G} {toAddSubgroup : AddSubgroup G}
  {isClosed' : IsClosed toAddSubgroup.carrier} {toAddSubgroup_1 : AddSubgroup G}
  {isClosed'_1 : IsClosed toAddSubgroup_1.carrier},
  { toAddSubgroup := toAddSubgroup, isClosed' := isClosed' } =
      { toAddSubgroup := toAddSubgroup_1, isClosed' := isClosed'_1 } →
    toAddSubgroup = toAddSubgroup_1
-- Mathlib.Topology.Connected.Basic
Homeomorph.connectedSpace_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (e : α ≃ₜ β),
  ConnectedSpace α ↔ ConnectedSpace β
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- Auxiliary definition for `CategoryTheory.Mat.equivalenceSingleObj`.  -/
CategoryTheory.Mat.equivalenceSingleObjInverse : (R : Type) →
  [inst : Ring R] → CategoryTheory.Functor (CategoryTheory.Mat_ (CategoryTheory.SingleObj Rᵐᵒᵖ)) (CategoryTheory.Mat R)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nsmul_mem_nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] {s : Set α} {a : α} {n : ℕ}, a ∈ s → n • a ∈ n • s
-- Mathlib.Logic.Basic
Classical.choose_eq : ∀ {α : Sort u_1} (a : α), ⋯.choose = a
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.epimorphisms_le_epiModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass],
  CategoryTheory.MorphismProperty.epimorphisms C ≤ P.epiModSerre