mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.smul : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {f : X → E} {𝕜 : Type u_9} [inst_3 : NormedAddCommGroup 𝕜] [inst_4 : SMulZeroClass 𝕜 E]
  [IsBoundedSMul 𝕜 E], MeasureTheory.LocallyIntegrable f μ → ∀ (c : 𝕜), MeasureTheory.LocallyIntegrable (c • f) μ
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sigma.dist_ne : ∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → MetricSpace (E i)] {i j : ι},
  i ≠ j → ∀ (x : E i) (y : E j), dist ⟨i, x⟩ ⟨j, y⟩ = dist x ⋯.some + 1 + dist ⋯.some y
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromRows_toRows : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R),
  A.toRows₁.fromRows A.toRows₂ = A
-- Mathlib.Order.Hom.Bounded
BotHom.instInhabited : {α : Type u_2} → {β : Type u_3} → [inst : Bot α] → [inst_1 : Bot β] → Inhabited (BotHom α β)
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_le : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), G.edist u v ≤ ↑p.length
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.empty : ∀ {α : Type u_2} [inst : LE α], CountableSupClosed ∅
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_eq_some_iff_exists_beq_and_mem_toList : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, m[k]? = some v ↔ ∃ k', (k == k') = true ∧ (k', v) ∈ m.toList
-- Mathlib.RingTheory.Etale.Weakly
Algebra.WeaklyEtale.ulift_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Algebra.WeaklyEtale (ULift.{u₁, u_1} R) (ULift.{u₂, u_2} S) ↔ Algebra.WeaklyEtale R S
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.profiniteCompletion_map : ∀ {X Y : GrpCat} (f : X ⟶ Y),
  ProfiniteGrp.profiniteCompletion.map f =
    ProfiniteGrp.ProfiniteCompletion.lift
      (CategoryTheory.CategoryStruct.comp f (ProfiniteGrp.ProfiniteCompletion.eta Y))
-- Lean.Meta.Basic
/-- Simpler version of `withLCtx` which just updates the local context. It is the responsibility of the
caller ensure the local instances are also properly updated.
 -/
Lean.Meta.withLCtx' : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Lean.LocalContext → n α → n α
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.edist_continuousRestrict_of_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : TopologicalSpace α] {s : Set α}
  {f g : UniformOnFun α β {s}} [inst_2 : CompactSpace ↑s] (hf : ContinuousOn ((UniformOnFun.toFun {s}) f) s)
  (hg : ContinuousOn ((UniformOnFun.toFun {s}) g) s),
  edist { toFun := s.domRestrict ((UniformOnFun.toFun {s}) f), continuous_toFun := ⋯ }
      { toFun := s.domRestrict ((UniformOnFun.toFun {s}) g), continuous_toFun := ⋯ } =
    edist f g
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_smul : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ) (z : K), (starRingEnd K) (r • z) = r • (starRingEnd K) z
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` reflects limits of shape `Jᵒᵖ`, then `F.rightOp : C ⥤ Dᵒᵖ` reflects colimits
of shape `J`.  -/
CategoryTheory.Limits.reflectsColimitsOfShape_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ D)
  [CategoryTheory.Limits.ReflectsLimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.ReflectsColimitsOfShape J F.rightOp
-- Init.Sym.Simp.SimprocDSL
/-- Rewrite using a named theorem set. Optionally specify a discharger for conditional rewrites.  -/
Lean.Parser.Sym.Simp.rewriteSet : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso_hom_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right] (X : CategoryTheory.Limits.Multicofork I),
  (I.multicoforkEquivSigmaCofork.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.isoOver_inv_app_hom_apply : ∀ {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} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} {ℱ ℱ' : CategoryTheory.Sheaf K A}
  (α : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) (X : A) (X_1 : Cᵒᵖ)
  (g :
    { obj := fun Y => Opposite.unop Y ⟶ (G.op.comp ℱ'.obj).obj X_1,
          map := fun {X Y} f => TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp f.unop g, map_id := ⋯,
          map_comp := ⋯ }.obj
      (Opposite.op X)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.IsCoverDense.isoOver α X).inv.app X_1)) g =
    CategoryTheory.CategoryStruct.comp g (α.inv.app X_1)
-- Std.Http.Data.Status
Std.Http.instInhabitedStatus : Inhabited Std.Http.Status
-- Lean.Environment
Lean.Kernel.Environment.find? : Lean.Kernel.Environment → Lean.Name → Option Lean.ConstantInfo
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
FractionalIdeal.sup_mul_inf : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [IsDedekindDomain A] [inst_3 : Algebra A K]
  [IsFractionRing A K] (I J : FractionalIdeal (nonZeroDivisors A) K), (I ⊓ J) * (I ⊔ J) = I * J
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_add_left_singleton : ∀ {α : Type u_2} [inst : AddGroup α] {a b : α}, {b}.preimage (fun x => a + x) ⋯ = {-a + b}
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.mem_multiples : ∀ {M : Type u_1} [inst : AddMonoid M] (n : M), n ∈ AddSubmonoid.multiples n
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.EAdj.eq_1 : ∀ {α : Type u_1} (H : Hypergraph α) (e f : Set α), H.EAdj e f = (e ∈ H.edgeSet ∧ f ∈ H.edgeSet ∧ ∃ x ∈ e, x ∈ f)
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The isomorphism between the automorphism group of a root pairing and the group of invertible
endomorphisms.  -/
RootPairing.Equiv.toEndUnit : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → P.Aut ≃* P.Endˣ
-- Mathlib.RingTheory.Jacobson.Radical
Module.map_jacobson_le : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂), Submodule.map f (Module.jacobson R M) ≤ Module.jacobson R₂ M₂
-- Init.Data.SInt.Lemmas
Int64.le_antisymm_iff : ∀ {a b : Int64}, a = b ↔ a ≤ b ∧ b ≤ a
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Around the image of the base point, the neighborhoods are the same
within `(extChartAt I x).target` and within `range I`.  -/
nhdsWithin_extChartAt_target_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M),
  nhdsWithin (↑(extChartAt I x) x) (extChartAt I x).target = nhdsWithin (↑(extChartAt I x) x) (Set.range ↑I)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_of_le_ge_cert : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Bool
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.revAll_char_iff : ∀ {c : Char} {s : String.Slice}, s.revAll c = true ↔ s.copy.toList = List.replicate s.copy.toList.length c
-- Mathlib.Data.ENat.Basic
ENat.add_one_natCast_le_withTop_of_lt : ∀ {m : ℕ} {n : WithTop ℕ∞}, ↑m < n → ↑(m + 1) ≤ n
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
WithBot.coe_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : Preorder α] [inst_1 : InfSet α] (f : ι → α),
  BddBelow (Set.range f) → ↑(⨅ i, f i) = ⨅ i, ↑(f i)
-- Init.Data.List.Count
_private.Init.Data.List.Count.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.comp_assoc : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {R₄ : Type u_14}
  {M₄ : Type u_15} [inst_7 : Semiring R₄] [inst_8 : AddCommMonoid M₄] [inst_9 : Module R₄ M₄] {σ₃₄ : R₃ →+* R₄}
  {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [inst_10 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄]
  [inst_11 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [inst_12 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (f : M₁ →ₛₗ[σ₁₂] M₂)
  (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₃ →ₛₗ[σ₃₄] M₄), (h ∘ₛₗ g) ∘ₛₗ f = h ∘ₛₗ g ∘ₛₗ f
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimage.iso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasKernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))],
  CategoryTheory.Abelian.PreservesCoimage.iso F f = CategoryTheory.Abelian.PreservesCoimage.iso F f
-- Mathlib.Data.Fin.Tuple.Sort
Tuple.monotone_proj : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] (f : Fin n → α), Monotone Tuple.graph.proj
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainTopCoeff_eq_zero_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  RootPairing.chainTopCoeff i j = 0 ↔
    ¬LinearIndependent R ![P.root i, P.root j] ∨ P.root j + P.root i ∉ Set.range ⇑P.root
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
/-- When `C` has limits, the category of presheafed spaces with values in `C` itself has colimits.
 -/
AlgebraicGeometry.PresheafedSpace.instHasColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C],
  CategoryTheory.Limits.HasColimits (AlgebraicGeometry.PresheafedSpace C)
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Continuous.arsinh : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℝ}, Continuous f → Continuous fun x => Real.arsinh (f x)
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.instFunLikeForall : {X : Type u_1} →
  {R : Type u_2} → [inst : Zero R] → [inst_1 : Add R] → [inst_2 : LE R] → FunLike (PseudoMetric X R) X (X → R)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.natDegree_modByMonic_le_left : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, (p %ₘ q).natDegree ≤ p.natDegree
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `SeminormedAddCommGroup E` instance from a `SeminormedSpace.Core` on a type
that already has an existing topology. This requires a proof that the uniformity
induced by the norm is equal to the preexisting uniformity. See note [reducible non-instances].  -/
SeminormedAddCommGroup.ofCoreReplaceTopology : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Norm E] →
          [inst_3 : Module 𝕜 E] →
            [T : TopologicalSpace E] →
              (core : SeminormedSpace.Core 𝕜 E) →
                T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace → SeminormedAddCommGroup E
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM.run : {α : Type} → Aesop.Script.UScript → Aesop.Script.StaticStructureM α → Lean.CoreM (α × Bool)
-- Mathlib.Data.Fintype.Sets
Multiset.Subtype.fintype : {α : Type u_1} → [DecidableEq α] → (s : Multiset α) → Fintype { x // x ∈ s }
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.recOnSubsingleton₂.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {r : Localization S → Localization S → Sort u}
  [h : ∀ (a c : M) (b d : ↥S), Subsingleton (r (Localization.mk a b) (Localization.mk c d))] (x y : Localization S)
  (f : (a c : M) → (b d : ↥S) → r (Localization.mk a b) (Localization.mk c d)),
  x.recOnSubsingleton₂ y f =
    Quotient.recOnSubsingleton₂' x y fun t =>
      Prod.rec (motive := fun x => (a₂ : M × ↥S) → r (Quotient.mk'' x) (Quotient.mk'' a₂))
        (fun x x_1 t => Prod.rec (fun x_2 x_3 => f x x_2 x_1 x_3) t) t
-- Aesop.Script.Step
Aesop.Script.Step.postState : Aesop.Script.Step → Lean.Meta.SavedState
-- Mathlib.NumberTheory.MulChar.Basic
/-- The restriction of a `MulChar` to a submonoid as an homomorphism.
 -/
MulChar.domRestrictHom : {R : Type u_1} →
  [inst : CommMonoid R] →
    {S : Type u_3} →
      [inst_1 : SetLike S R] →
        [inst_2 : SubmonoidClass S R] →
          (T : S) → (R'' : Type u_4) → [inst_3 : CommMonoidWithZero R''] → MulChar R R'' →* MulChar (↥T) R''
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instSemigroup.eq_1 : ∀ {α : Type u_1} [inst : Semigroup α], MulOpposite.instSemigroup = { toMul := MulOpposite.instMul, mul_assoc := ⋯ }
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.prod_expMapBasis_pow : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K),
  ∏ w, ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x w ^ w.mult =
    Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀) ^ Module.finrank ℚ K
-- Batteries.Recycling.MonadSatisfying.Array
Array.SatisfiesM_mapM' : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {as : Array α} {f : α → m β}
  {p : Fin as.size → β → Prop},
  (∀ (i : Fin as.size), SatisfiesM (p i) (f as[i])) →
    SatisfiesM (fun arr => ∃ (eq : arr.size = as.size), ∀ (i : ℕ) (h : i < as.size), p ⟨i, h⟩ arr[i]) (Array.mapM f as)
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- If the derivative of `f` is negative at a root `x₀` of `f`, then locally the sign of `f x`
matches `x₀ - x`.  -/
eventually_nhdsWithin_sign_eq_of_deriv_neg : ∀ {f : ℝ → ℝ} {x₀ : ℝ}, deriv f x₀ < 0 → f x₀ = 0 → ∀ᶠ (x : ℝ) in nhds x₀, SignType.sign (f x) = SignType.sign (x₀ - x)
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.kind.inj : ∀ {val val_1 : Lean.SyntaxNodeKind},
  Lean.Parser.ParserExtension.Entry.kind val = Lean.Parser.ParserExtension.Entry.kind val_1 → val = val_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_of_add_le_add_right : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] [AddRightReflectLE α] {a b c : α}, b + a ≤ c + a → b ≤ c
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_add_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f g : MvPolynomial σ R),
  m.toWithBotSyn (m.withBotDegree (f + g)) ≤
    max (m.toWithBotSyn (m.withBotDegree f)) (m.toWithBotSyn (m.withBotDegree g))
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The arrow in the ReflQuiver `OneTruncation₂ V` of a 2-truncated simplicial set arising from the
2nd face of a 2-simplex.  -/
SSet.Truncated.ev01₂ : {V : SSet.Truncated 2} →
  (φ : V.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.ι0₂._proof_3 })) →
    SSet.Truncated.ev0₂ φ ⟶ SSet.Truncated.ev1₂ φ
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
CategoryTheory.Grpd.coe_of : ∀ (C : Type u) [inst : CategoryTheory.Groupoid C], ↑(CategoryTheory.Grpd.of C) = C
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.instSemilatticeSup : {α : Type u_1} → [inst : TopologicalSpace α] → SemilatticeSup (TopologicalSpace.PositiveCompacts α)
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.SearchControl.continue.sizeOf_spec : sizeOf Lean.Server.FileWorker.SignatureHelp.SearchControl.continue = 1
-- Mathlib.MeasureTheory.Measure.LevyConvergence
/-- If the characteristic functions of a sequence of measures `μ : ℕ → Measure E` converge pointwise
to a function which is continuous at 0, then `{μ n | n}` is tight.  -/
MeasureTheory.isTightMeasureSet_of_tendsto_charFun : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : ℕ → MeasureTheory.Measure E}
  [∀ (i : ℕ), MeasureTheory.IsProbabilityMeasure (μ i)] {f : E → ℂ},
  ContinuousAt f 0 →
    (∀ (t : E), Filter.Tendsto (fun n => MeasureTheory.charFun (μ n) t) Filter.atTop (nhds (f t))) →
      MeasureTheory.IsTightMeasureSet (Set.range μ)
-- Lean.CoreM
Lean.Core.Context.currMacroScope : Lean.Core.Context → Lean.MacroScope
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M` and a map of `CommMonoid`s
`g : M →* P` such that `g(S) ⊆ Units P`, `f x = f y → g x = g y` for all `x y : M`.  -/
Submonoid.LocalizationMap.eq_of_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P},
  (∀ (y : ↥S), IsUnit (g ↑y)) → ∀ {x y : M}, f x = f y → g x = g y
-- Lean.Elab.Do.Legacy
/-- Syntax to reference the result of the monadic computation performed by the do notation.  -/
Lean.Elab.Term.Do.ToCodeBlock.Context.returnType : Lean.Elab.Term.Do.ToCodeBlock.Context → Lean.Syntax
-- Mathlib.Analysis.Calculus.FDeriv.Add
Differentiable.sum : ∀ {𝕜 : 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] {ι : Type u_4}
  {u : Finset ι} {A : ι → E → F}, (∀ i ∈ u, Differentiable 𝕜 (A i)) → Differentiable 𝕜 (∑ i ∈ u, A i)
-- Aesop.RuleTac.Forward
Aesop.RuleTac.forwardMatches : Array Aesop.ForwardRuleMatch → Aesop.RuleTac
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nnnorm_toLp_one : ∀ {p : ENNReal} {ι : Type u_2} [hp : Fact (1 ≤ p)] [inst : Fintype ι] {β : Type u_5}
  [inst_1 : SeminormedAddCommGroup β],
  p ≠ ⊤ → ∀ [inst_2 : One β], ‖WithLp.toLp p 1‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖1‖₊
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_ofReal_of_nonneg : ∀ {x : ℝ}, 0 ≤ x → (↑x).arg = 0
-- Mathlib.CategoryTheory.Monoidal.Tor
CategoryTheory.Tor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.HasProjectiveResolutions C] (n : ℕ) {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Tor C n).map f =
    CategoryTheory.NatTrans.leftDerived ((CategoryTheory.MonoidalCategory.tensoringLeft C).map f) n
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_sInf : ∀ {G : Type u_1} [inst : Group G] {Hs : Set (Subgroup G)}, (∀ H ∈ Hs, H.Characteristic) → (sInf Hs).Characteristic
-- Mathlib.Topology.Separation.PerfectlyNormal
/-- A topological space is perfectly normal iff every closed set is the zero set of a continuous
function taking values in the unit interval.  -/
perfectlyNormalSpace_iff_forall_isClosed_preimage_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  PerfectlyNormalSpace X ↔ ∀ (s : Set X), IsClosed s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
-- Std.Time.Zoned.TimeZone
/-- Creates a `WallTime` from a `Timestamp` given a timezone `offset`. The result is the local
civil time: `wall = UTC + offset`.
 -/
Std.Time.WallTime.ofTimestamp : Std.Time.Timestamp → Std.Time.TimeZone.Offset → Std.Time.WallTime
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CochainComplex.mk.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) →
      (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0),
  CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ =
    CochainComplex.of (fun n => (CochainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₁)
      (fun n => (CochainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n).f) ⋯
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.BitVec.lt_ult : ∀ {w : ℕ} (x y : BitVec w), (x < y) = (x.ult y = true)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
/-- Notation for discrete convolution with explicit bilinear map:
`(f ⋆[L] g) x = ∑' ab : mulFiber x, L (f ab.1) (g ab.2)`.  -/
DiscreteConvolution.«term_⋆[_]_» : Lean.TrailingParserDescr
-- Init.Data.Nat.Log2
Nat.log2_le_self : ∀ (n : ℕ), n.log2 ≤ n
-- Mathlib.Data.Sym.Basic
/-- This is `cons` but for the alternative `Sym'` definition.
 -/
Sym.cons' : {α : Type u_3} → {n : ℕ} → α → Sym.Sym' α n → Sym.Sym' α n.succ
-- Init.Data.Slice.InternalLemmas
Std.Slice.Internal.foldM_iter : ∀ {γ : Type u} {α β : Type v} {δ : Type w} {init : δ} {m : Type w → Type w'} [inst : Monad m]
  [inst_1 : Std.ToIterator (Std.Slice γ) Id α β] [inst_2 : Std.Iterator α Id β] [inst_3 : Std.IteratorLoop α Id m]
  [Std.Iterators.Finite α Id] {s : Std.Slice γ} {f : δ → β → m δ},
  Std.Iter.foldM f init (Std.Slice.Internal.iter s) = Std.Slice.foldlM f init s
-- Mathlib.Topology.Algebra.Ring.Basic
IsTopologicalRing.of_nhds_zero : ∀ {R : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : TopologicalSpace R],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0) →
    Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0) →
      Filter.Tendsto (Function.uncurry fun x1 x2 => x1 * x2) (nhds 0 ×ˢ nhds 0) (nhds 0) →
        (∀ (x₀ : R), Filter.Tendsto (fun x => x₀ * x) (nhds 0) (nhds 0)) →
          (∀ (x₀ : R), Filter.Tendsto (fun x => x * x₀) (nhds 0) (nhds 0)) →
            (∀ (x₀ : R), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) → IsTopologicalRing R
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mod.injEq : ∀ (k : ℤ) (y? : Option Int.Internal.Linear.Var) (c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) (k_1 : ℤ)
  (y?_1 : Option Int.Internal.Linear.Var) (c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mod k y? c = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.mod k_1 y?_1 c_1) =
    (k = k_1 ∧ y? = y?_1 ∧ c = c_1)
-- Init.Grind.AC
Lean.Grind.AC.instInhabitedExpr.default : Lean.Grind.AC.Expr
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CochainComplex.Plus.instIsInducedInjectiveObjectInverseImageQuasiIsoMapCochainComplexPlusιLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (CochainComplex.Plus.localizerMorphism C).IsInduced
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run `aesop` at every step in proofs, reporting where it succeeds.  -/
tryAtEachStepAesop : Mathlib.TacticAnalysis.Config