mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Hygiene
/-- Simplistic MonadQuotation that does not guarantee globally fresh names, that
is, between different runs of this or other MonadQuotation implementations.
It is only safe if the syntax quotations do not introduce bindings around
antiquotations, and if references to globals are prefixed with `_root_.`
(which is not allowed to refer to a local variable)
`Unhygienic` can also be seen as a model implementation of `MonadQuotation`
(since it is completely hygienic as long as it is "run" only once and can
assume that there are no other implementations in use, as is the case for the
elaboration monads that carry their macro scope state through the entire
processing of a file). It uses the state monad to query and allocate the
next macro scope, and uses the reader monad to store the stack of scopes
corresponding to `withFreshMacroScope` calls.
 -/
Lean.Unhygienic : Type → Type
-- Init.Control.Lawful.Instances
Option.map.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Option.map f none = none
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Fin.mk.hcongr_3 : ∀ (n n' : ℕ),
  n = n' →
    ∀ (val val' : ℕ), val = val' → ∀ (isLt : val < n) (isLt' : val' < n'), isLt ≍ isLt' → ⟨val, isLt⟩ ≍ ⟨val', isLt'⟩
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version
assumes `0≤K`.  -/
LipschitzWith.of_le_add_mul : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : α → ℝ} (K : NNReal),
  (∀ (x y : α), f x ≤ f y + ↑K * dist x y) → LipschitzWith K f
-- Mathlib.Topology.VectorBundle.Basic
/-- Promotion from a `Pretrivialization` in the `pretrivializationAtlas` of a
`VectorPrebundle` to a `Trivialization`.  -/
VectorPrebundle.trivializationOfMemPretrivializationAtlas : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [inst_2 : (x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace R F] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : (x : B) → TopologicalSpace (E x)] →
                      (a : VectorPrebundle R F E) →
                        {e : Bundle.Pretrivialization F Bundle.TotalSpace.proj} →
                          e ∈ a.pretrivializationAtlas → Bundle.Trivialization F Bundle.TotalSpace.proj
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instIsZeroApply : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], IsZeroApply (SchwartzMap E F) E F
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The converse of this is true with additional assumptions, see `mono_iff_mono_right`.  -/
CategoryTheory.StructuredArrow.mono_of_mono_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f : A ⟶ B)
  [h : CategoryTheory.Mono (CategoryTheory.StructuredArrow.Hom.right f)], CategoryTheory.Mono f
-- Lean.Meta.CongrTheorems
/-- It is a parameter for the congruence theorem, the parameter occurs in the left and right hand sides.  -/
Lean.Meta.CongrArgKind.fixed : Lean.Meta.CongrArgKind
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_isEquivalent_of_nonzero_head : ∀ {exps_hd : ℝ} {exps_tl : Tactic.ComputeAsymptotics.UnitMonomial} {basis_hd : ℝ → ℝ}
  {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis (basis_hd :: basis_tl) →
    exps_hd ≠ 0 →
      Asymptotics.IsEquivalent Filter.atTop
        (Tactic.ComputeAsymptotics.UnitMonomial.toLogFun (exps_hd :: exps_tl) (basis_hd :: basis_tl))
        (exps_hd • Real.log ∘ basis_hd)
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] {X Y : C}
  (f g : X ⟶ Y),
  CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv F f g =
    (CategoryTheory.Limits.PreservesEqualizer.iso (F.comp FintypeCat.incl) f g ≪≫
        CategoryTheory.Limits.Types.equalizerIso (F.map f).hom (F.map g).hom).toEquiv
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- A characterization lemma for the multiplication on the Ore localization, allowing for a choice
of Ore numerator and Ore denominator.  -/
OreLocalization.oreDiv_mul_char : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (r₁ r₂ : R) (s₁ s₂ : ↥S)
  (r' : R) (s' : ↥S), ↑s' * r₁ = r' * ↑s₂ → r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The canonical isomorphism `tensorUnit 0 ≅ 𝟙_ C`  -/
CategoryTheory.GradedObject.Monoidal.tensorUnit₀ : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : DecidableEq I] →
            [inst_4 : CategoryTheory.Limits.HasInitial C] →
              CategoryTheory.GradedObject.Monoidal.tensorUnit 0 ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Lean.Data.Json.FromToJson.Basic
Lean.List.fromJson? : {α : Type u_1} → [Lean.FromJson α] → Lean.Json → Except String (List α)
-- Mathlib.Topology.Bases
TopologicalSpace.isTopologicalBasis_of_subbasis_of_inter : ∀ {α : Type u} [t : TopologicalSpace α] {r : Set (Set α)},
  t = TopologicalSpace.generateFrom r →
    (∀ ⦃s : Set α⦄, s ∈ r → ∀ ⦃t : Set α⦄, t ∈ r → s ∩ t ∈ r) → TopologicalSpace.IsTopologicalBasis (insert Set.univ r)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.mvars.withType : Lean.Option Bool
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (complex : ChainComplex C ℕ)
  (projective :
    autoParam (∀ (n : ℕ), CategoryTheory.Projective (complex.X n))
      CategoryTheory.ProjectiveResolution.projective._autoParam)
  [hasHomology : ∀ (i : ℕ), HomologicalComplex.HasHomology complex i] (π : complex ⟶ (ChainComplex.single₀ C).obj Z)
  (quasiIso : autoParam (QuasiIso π) CategoryTheory.ProjectiveResolution.quasiIso._autoParam)
  (complex_1 : ChainComplex C ℕ)
  (projective_1 :
    autoParam (∀ (n : ℕ), CategoryTheory.Projective (complex_1.X n))
      CategoryTheory.ProjectiveResolution.projective._autoParam)
  (hasHomology_1 : ∀ (i : ℕ), HomologicalComplex.HasHomology complex_1 i)
  (π_1 : complex_1 ⟶ (ChainComplex.single₀ C).obj Z)
  (quasiIso_1 : autoParam (QuasiIso π_1) CategoryTheory.ProjectiveResolution.quasiIso._autoParam),
  ({ complex := complex, projective := projective, hasHomology := hasHomology, π := π, quasiIso := quasiIso } =
      { complex := complex_1, projective := projective_1, hasHomology := hasHomology_1, π := π_1,
        quasiIso := quasiIso_1 }) =
    (complex = complex_1 ∧ π ≍ π_1)
-- Mathlib.Data.Nat.Bits
Nat.mod_two_of_bodd : ∀ (n : ℕ), n % 2 = n.bodd.toNat
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.prod_bot_sup_bot_prod : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (s : Subring R) (t : Subring S),
  s.prod ⊥ ⊔ ⊥.prod t = s.prod t
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α}
  [inst_1 : Inhabited (β a)], (m.erase k).get! a = if (k == a) = true then default else m.get! a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintOptions.toWorkDoneProgressOptions : Lean.Lsp.InlayHintOptions → Lean.Lsp.WorkDoneProgressOptions
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.functoriality_obj_ι_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) (A : CategoryTheory.Limits.Cocone F) (j : J),
  ((CategoryTheory.Limits.Cocone.functoriality F G).obj A).ι.app j = G.map (A.ι.app j)
-- Init.Data.UInt.Bitwise
UInt8.toUInt16_not : ∀ (a : UInt8), (~~~a).toUInt16 = ~~~a.toUInt16 % 256
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α}, k ∉ m₁ → (m₁ ∪ m₂).get? k = m₂.get? k
-- Mathlib.LinearAlgebra.Finsupp.Pi
FunOnFinite.linearMap.congr_simp : ∀ (R : Type u_5) (M : Type u_6) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {X : Type u_7}
  {Y : Type u_8} [inst_3 : Finite X] [inst_4 : Finite Y] (f f_1 : X → Y),
  f = f_1 → FunOnFinite.linearMap R M f = FunOnFinite.linearMap R M f_1
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_succ_comp_δ_castSucc_of_lt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
  i ≤ j.castSucc →
    CategoryTheory.CategoryStruct.comp (self.h j.succ) (Y.δ i.castSucc) =
      CategoryTheory.CategoryStruct.comp (X.δ i) (self.h j)
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.instRpcEncodableDiagramProps : Lean.Server.RpcEncodable ProofWidgets.Penrose.DiagramProps
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.isOrtho_zero_left : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} (x : M), B.IsOrtho 0 x
-- Mathlib.Order.Irreducible
IsMax.not_infIrred : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : α}, IsMax a → ¬InfIrred a
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.isoLimitCone_inv_π_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (t : CategoryTheory.Limits.LimitCone F)
  (j : J) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) h) =
    CategoryTheory.CategoryStruct.comp (t.cone.π.app j) h
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] (f : MeasureTheory.SimpleFunc α β)
  {s : Set α}, MeasurableSet s → ⇑(f.restrict s) = s.indicator ⇑f
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le_max_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, ↑a ≤ max ↑b ↑c ↔ a ≤ max b c
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.memLp_indicator_const : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  {s : Set α} (p : ENNReal),
  MeasurableSet s → ∀ (c : E), c = 0 ∨ μ s ≠ ⊤ → MeasureTheory.MemLp (s.indicator fun x => c) p μ
-- Init.Data.BitVec.Basic
/-- Shifts a bitvector to the right. This is an arithmetic right shift - the high bits are filled with
most significant bit's value.

As a numeric operation, this is equivalent to `x.toInt >>> s`.

SMT-LIB name: `bvashr` except this operator uses a `Nat` shift value.
 -/
BitVec.sshiftRight : {n : ℕ} → BitVec n → ℕ → BitVec n
-- Mathlib.Topology.CompactOpen
/-- `C(X, ·)` is a functor.  -/
ContinuousMap.continuous_postcomp : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (g : C(Y, Z)), Continuous g.comp
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.CofibrantObject C),
  HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'.obj X =
    HomotopicalAlgebra.BifibrantObject.toHoCat.obj X.bifibrantResolutionObj
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- **Alias** of `sub_apply`. -/
MultilinearMap.sub_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Sub β}
  {inst_2 : Sub F} [self : IsSubApply F α β] (f g : F) (x : α), (f - g) x = f x - g x
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.neg_def`. -/
AddAut.inv_def : ∀ (M : Type u_2) [inst : Add M] (e₁ : AddAut M), -e₁ = AddEquiv.symm e₁
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.instMembership : {α : Type u_2} → [inst : Preorder α] → Membership α (OmegaCompletePartialOrder.Chain α)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_keysArray : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.keysArray.isEmpty = m.isEmpty
-- Mathlib.Order.Bounds.Basic
isGreatest_univ_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsGreatest Set.univ a ↔ IsTop a
-- Init.Data.Range.Polymorphic.Iterators
/-- Internal function that constructs an iterator for a closed range `lo...=hi`.
This is an internal function.
Use `Rcc.iter` instead, which requires
importing `Std.Data.Iterators`.
 -/
Std.Rcc.Internal.iter : {α : Type u} → [Std.PRange.UpwardEnumerable α] → Std.Rcc α → Std.Iter α
-- Mathlib.Order.KrullDimension
Order.KrullDimLE.krullDim_le : ∀ {n : ℕ} {α : Type u_1} {inst : Preorder α} [self : Order.KrullDimLE n α], Order.krullDim α ≤ ↑n
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
ContinuousMultilinearMap.iteratedFDeriv.eq_1 : ∀ {𝕜 : Type u} {ι : Type v} {E₁ : ι → Type wE₁} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E₁ G) (k : ℕ) (x : (i : ι) → E₁ i),
  f.iteratedFDeriv k x = ∑ e, (f.iteratedFDerivComponent e.toEquivRange) ((Pi.compRightL 𝕜 E₁ Subtype.val) x)
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.numSectionVars : Lean.Elab.PreDefinition → ℕ
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.swapTrue_mem_C1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  Profinite.NobelingProof.contained C (Order.succ o) →
    ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2)
      (f : ↑(Profinite.NobelingProof.π (Profinite.NobelingProof.C1 C ho) fun x => Profinite.NobelingProof.ord I x < o)),
      Profinite.NobelingProof.SwapTrue o ↑f ∈ Profinite.NobelingProof.C1 C ho
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
/-- The **Triangle Counting Lemma**. If `G` is a graph and `s`, `t`, `u` are disjoint sets of
vertices such that each pair is `ε`-uniform and `2 * ε`-dense, then `G` contains at least
`(1 - 2 * ε) * ε ^ 3 * |s| * |t| * |u|` triangles.  -/
SimpleGraph.triangle_counting : ∀ {α : Type u_1} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {ε : ℝ} {s t u : Finset α} [inst_1 : DecidableEq α]
  [inst_2 : Fintype α],
  2 * ε ≤ ↑(G.edgeDensity s t) →
    G.IsUniform ε s t →
      Disjoint s t →
        2 * ε ≤ ↑(G.edgeDensity s u) →
          G.IsUniform ε s u →
            Disjoint s u →
              2 * ε ≤ ↑(G.edgeDensity t u) →
                G.IsUniform ε t u →
                  Disjoint t u → (1 - 2 * ε) * ε ^ 3 * ↑s.card * ↑t.card * ↑u.card ≤ ↑(G.cliqueFinset 3).card
-- Mathlib.Topology.Algebra.Ring.Compact
IsDiscreteValuationRing.isOpen_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R]
  [inst_5 : IsDomain R] [IsDiscreteValuationRing R] {I : Ideal R}, IsOpen ↑I ↔ I ≠ ⊥
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `inv_le_iff_one_le_mul₀` for a version with multiplication on the other side.  -/
inv_le_iff_one_le_mul₀' : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀},
  0 < a → (a⁻¹ ≤ b ↔ 1 ≤ a * b)
-- Mathlib.Order.Disjoint
Complementeds.disjoint_coe : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {a b : Complementeds α},
  Disjoint ↑a ↑b ↔ Disjoint a b
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.forInStep.go.match_1.eq_1 : ∀ {δ : Type u_1} (motive : ForInStep δ → Sort u_2) (d : δ) (h_1 : (d : δ) → motive (ForInStep.done d))
  (h_2 : (d : δ) → motive (ForInStep.yield d)),
  (match ForInStep.done d with
    | ForInStep.done d => h_1 d
    | ForInStep.yield d => h_2 d) =
    h_1 d
-- Lean.Parser.Syntax
Lean.Parser.Syntax.unicodeAtom.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulStrictMono.mk : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α],
  (∀ ⦃a : α⦄, 0 < a → ∀ ⦃b c : α⦄, b < c → a * b < a * c) → PosMulStrictMono α
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instAddAction_1.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α],
  OrderDual.instAddAction_1 = { toVAdd := OrderDual.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential map in a commutative Banach algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has
Fréchet derivative `NormedSpace.exp x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x`.  -/
hasFDerivAt_exp : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : RCLike 𝕂] [inst_1 : NormedCommRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸] {x : 𝔸}, HasFDerivAt NormedSpace.exp (NormedSpace.exp x • 1) x
-- Mathlib.Analysis.Normed.Module.Convex
convexOn_dist : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} (z : E),
  Convex ℝ s → ConvexOn ℝ s fun z' => dist z' z
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
mdifferentiable_addInvariantVectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G]
  [inst_7 : LieAddGroup I (minSmoothness 𝕜 3) G] (v : AddGroupLieAlgebra I G),
  MDiff fun g => ⟨g, addInvariantVectorField v g⟩
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.GrothendieckTopology.preservesLimit_diagramFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (X : C) (K : Type s) [inst_3 : CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D]
  (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)),
  CategoryTheory.Limits.PreservesLimit F (J.diagramFunctor D X)
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquivClass.apply_coe_symm_apply : ∀ {α : Type u_9} {β : Type u_10} [inst : Mul α] [inst_1 : Mul β] {F : Type u_11} [inst_2 : EquivLike F α β]
  [inst_3 : MulEquivClass F α β] (e : F) (x : β), e ((↑e).symm x) = x
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Raw.all.eq_1 : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) (p : (a : α) → β a → Bool),
  m.all p =
    (do
        let __s ←
          forIn m (none, ()) fun a __s =>
              if ¬p a.fst a.snd = true then pure (ForInStep.done (some false, ()))
              else pure (ForInStep.yield (none, ()))
        have __r : Option Bool × Unit := __s
        match __r.1 with
          | some r => pure r
          | none => pure true).run
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_iInf : ∀ {α : Type u_2} [inst : TopologicalSpace α] {ι : Type u_5} [Finite ι] (U : ι → TopologicalSpace.Opens α),
  ↑(⨅ i, U i) = ⋂ i, ↑(U i)
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A]
  {X W : CategoryTheory.Sheaf J A} (f : W ⟶ X),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom X.obj
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.map_div_right_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : DivInvMonoid G] (μ : MeasureTheory.Measure G)
  [μ.IsMulRightInvariant] (g : G), MeasureTheory.Measure.map (fun x => x / g) μ = μ
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.NoSuffixPatternModel.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat],
  (∀ (s t : String),
      String.Slice.Pattern.Model.PatternModel.Matches pat t →
        String.Slice.Pattern.Model.PatternModel.Matches pat (s ++ t) → s = "") →
    String.Slice.Pattern.Model.NoSuffixPatternModel pat
-- Mathlib.MeasureTheory.Measure.Dirac
/-- Two measures on a countable space are equal if they agree on singletons.  -/
MeasureTheory.Measure.ext_of_singleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Countable α] {μ ν : MeasureTheory.Measure α},
  (∀ (a : α), μ {a} = ν {a}) → μ = ν
-- Init.Data.UInt.Lemmas
Nat.toUInt64_eq : ∀ {n : ℕ}, n.toUInt64 = UInt64.ofNat n
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.AddMonObj M] (f : X ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X M M).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.AddMonObj.add) CategoryTheory.AddMonObj.add) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id M))
          CategoryTheory.AddMonObj.add)
        (CategoryTheory.CategoryStruct.id M))
      CategoryTheory.AddMonObj.add
-- Mathlib.RingTheory.Finiteness.Basic
RingEquiv.finite : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] (e : A ≃+* B), e.toRingHom.Finite
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the reverse direction of `lowerHemicontinuous_singleton_iff`. -/
Continuous.lowerHemicontinuous : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Continuous f → LowerHemicontinuous fun x => {f x}
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Icc_union_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, c ≤ max a b → Set.Icc a b ∪ Set.Ici c = Set.Ici (min a c)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainBialgHomEquiv.eq_1 : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G]
  [inst_3 : Group H],
  MonoidAlgebra.mapDomainBialgHomEquiv =
    { toFun := MonoidAlgebra.mapDomainBialgHom R, invFun := MonoidAlgebra.mapDomainOfBialgHom, left_inv := ⋯,
      right_inv := ⋯ }