mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.Trivialization.contMDiffOn_symm_trans : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e]
  [MemTrivializationAtlas e'],
  ContMDiffOn (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) n
    (↑(e.symm.trans e'.toOpenPartialHomeomorph)) (e.target ∩ e'.target)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.baseChange_dblXYZ : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Projective R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).dblXYZ (⇑f ∘ P) = ⇑f ∘ (W'.baseChange A).dblXYZ P
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.any_eq_not_all_not : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α]
  {p : (a : α) → β a → Bool}, m.WF → m.any p = !m.all fun a b => !p a b
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.findMin.match_1.splitter : {α : Type u_1} →
  (motive : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.FindMin α → Sort u_2) →
    (x : Batteries.BinomialHeap.Imp.Heap α) →
      (x_1 : Batteries.BinomialHeap.Imp.FindMin α) →
        ((res : Batteries.BinomialHeap.Imp.FindMin α) → motive Batteries.BinomialHeap.Imp.Heap.nil res) →
          ((r : ℕ) →
              (a : α) →
                (c : Batteries.BinomialHeap.Imp.HeapNode α) →
                  (s : Batteries.BinomialHeap.Imp.Heap α) →
                    (res : Batteries.BinomialHeap.Imp.FindMin α) →
                      motive (Batteries.BinomialHeap.Imp.Heap.cons r a c s) res) →
            motive x x_1
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.instIsIsoMapF : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : SuccOrder J]
  [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] {X Y : C} {f : X ⟶ Y}
  (h : (CategoryTheory.MorphismProperty.isomorphisms C).TransfiniteCompositionOfShape J f) {i j : J} (f_1 : i ⟶ j),
  CategoryTheory.IsIso (h.F.map f_1)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instZero : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → Zero (CentroidHom α)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.type₁_x : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d + 1} {i : Fin (d + 1)} (h : SSet.prodStdSimplex.pairingCore.IsIndex x hd i.succ), h.type₁.x = x
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_inf_right : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x₁ x₂ : Filter α} {y : Filter β},
  Filter.Tendsto f x₂ y → Filter.Tendsto f (x₁ ⊓ x₂) y
-- Lean.Parser.Term
Lean.Parser.Term.funBinder.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.liftOfStrictSegal.spineEquiv_f₂_arrow_zero : ∀ {X Y : SSet.Truncated 2}
  (f₀ :
    X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
      Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }))
  (f₁ :
    X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
      Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }))
  (hδ₁ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hδ₀ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ })),
  ((hY.spineEquiv 2 SSet.Truncated.liftOfStrictSegal.f₂._proof_5)
          (SSet.Truncated.liftOfStrictSegal.f₂ f₀ f₁ hδ₁ hδ₀ hY x)).arrow
      0 =
    f₁ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op)) x)
-- Aesop.Frontend.Tactic
_private.Aesop.Frontend.Tactic.0.Aesop.Frontend.elabSimpConfig.unsafe_impl_2 : Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.Simp.Config
-- Mathlib.Data.FunLike.IsApply
IsPowApply.mk : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} [inst : FunLike F α β]
  [inst_1 : Pow β M] [inst_2 : Pow F M], (∀ (f : F) (n : M) (x : α), (f ^ n) x = f x ^ n) → IsPowApply M F α β
-- Mathlib.Algebra.Group.Semiconj.Units
SemiconjBy.units_zpow_right : ∀ {M : Type u_1} [inst : Monoid M] {a : M} {x y : Mˣ}, SemiconjBy a ↑x ↑y → ∀ (m : ℤ), SemiconjBy a ↑(x ^ m) ↑(y ^ m)
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instPreservesFiniteColimitsSingle : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : DecidableEq ι] (i : ι), CategoryTheory.Limits.PreservesFiniteColimits (HomologicalComplex.single C c i)
-- Mathlib.Tactic.Translate.ToDual
/-- The global `do_translate`/`dont_translate` attributes specify whether operations on
a given type should be translated. `dont_translate` can be used for types that are translated,
such as `MonoidAlgebra` -> `AddMonoidAlgebra`, or for fixed types, such as `Fin n`/`ZMod n`.
`do_translate` is for types without arguments, like `Unit` and `Empty`, where the structure on it
can be translated.

Note: The name generation is not aware of `dont_translate`, so if some part of a lemma is not
  translated thanks to this, you generally have to specify the translated name manually.
 -/
Mathlib.Tactic.ToDual.to_dual_do_translate : Lean.ParserDescr
-- Mathlib.Topology.Order
TopologicalSpace.ne_top_iff_exists_not_inseparable : ∀ {α : Type u} {t : TopologicalSpace α}, t ≠ ⊤ ↔ ∃ x y, ¬Inseparable x y
-- Lean.Elab.Tactic.Classical
Lean.Elab.Tactic.evalClassical : Lean.Elab.Tactic.Tactic
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- The precylinder object obtained from a pre-path object in the opposite category.  -/
HomotopicalAlgebra.PrepathObject.unop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Cᵒᵖ} → HomotopicalAlgebra.PrepathObject A → HomotopicalAlgebra.Precylinder (Opposite.unop A)
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
DirectSum.toAddMonoidAlgebra_toDirectSum : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : DirectSum ι fun x => M), f.toAddMonoidAlgebra.toDirectSum = f
-- Init.Data.Option.Attach
Option.mem_attach : ∀ {α : Type u_1} (o : Option α) (x : { x // o = some x }), x ∈ o.attach
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {f : Option (β k) → Option (β k)},
          (Std.DTreeMap.Internal.Impl.alter! k f t₁).Equiv (Std.DTreeMap.Internal.Impl.alter! k f t₂)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_filter_not_contains : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getValue? k (List.filter (fun p => !l₂.contains p.fst) l₁) =
      if l₂.contains k = true then none else Std.Internal.List.getValue? k l₁
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Generators.localizationAway.congr_simp : ∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r r_1 : R) (e_r : r = r_1)
  [inst_3 : IsLocalization.Away r S],
  Algebra.Generators.localizationAway S r = Algebra.Generators.localizationAway S r_1
-- Mathlib.Order.Bounds.Image
bddAbove_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set (α × β)},
  BddAbove s ↔ BddAbove (Prod.fst '' s) ∧ BddAbove (Prod.snd '' s)
-- Mathlib.CategoryTheory.Localization.FiniteProducts
CategoryTheory.Localization.instHasFiniteProductsLocalization : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C)
  [W.ContainsIdentities] [CategoryTheory.Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts],
  CategoryTheory.Limits.HasFiniteProducts W.Localization
-- Batteries.Tactic.SqueezeScope
/-- `squeeze_wrap a x => tac` is part of the implementation of `squeeze_scope`.
Here `tac` will be a `simp` or `dsimp` syntax, and `squeeze_wrap` will run the tactic
and contribute the generated `usedSimps` to the `squeezeScopes[a][x]` variable.
 -/
_private.Batteries.Tactic.SqueezeScope.0.Batteries.Tactic.squeezeWrap : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Reindexing a matrix preserves column-stochasticity.  -/
Matrix.reindex_mem_colStochastic_iff : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {m : Type u_3} [inst_5 : Fintype m] [inst_6 : DecidableEq m]
  {M : Matrix n n R} {e₁ e₂ : n ≃ m}, (Matrix.reindex e₁ e₂) M ∈ Matrix.colStochastic R m ↔ M ∈ Matrix.colStochastic R n
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Given a chart `f` on a manifold with corners, `f.extend I` is the extended chart to the model
vector space.  -/
OpenPartialHomeomorph.extend : {𝕜 : 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] → OpenPartialHomeomorph M H → ModelWithCorners 𝕜 E H → PartialEquiv M E
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {a : α} {b : β a}, (t.insert a b).getKey! a = a
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPairIsoMk_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
  (p : F.obj CategoryTheory.Limits.WalkingParallelPair.zero ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.zero)
  (q : F.obj CategoryTheory.Limits.WalkingParallelPair.one ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.one)
  (hl :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) q.hom =
        CategoryTheory.CategoryStruct.comp p.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.left))
      CategoryTheory.Limits.parallelPairIsoMk._auto_1)
  (hr :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) q.hom =
        CategoryTheory.CategoryStruct.comp p.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.right))
      CategoryTheory.Limits.parallelPairIsoMk._auto_3)
  (X : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.parallelPairIsoMk p q hl hr).hom.app X =
    (CategoryTheory.Limits.WalkingParallelPair.rec p q X).hom
-- Mathlib.GroupTheory.Nilpotent
Group.nilpotencyClass_le_of_ker_le_center : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (f : G →* H),
  f.ker ≤ Subgroup.center G → ∀ [Group.IsNilpotent H], Group.nilpotencyClass G ≤ Group.nilpotencyClass H + 1
-- Mathlib.Topology.DenseEmbedding
Filter.HasBasis.hasBasis_of_isDenseInducing : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [RegularSpace β]
  {ι : Type u_5} {s : ι → Set α} {p : ι → Prop} {x : α},
  (nhds x).HasBasis p s → ∀ {f : α → β}, IsDenseInducing f → (nhds (f x)).HasBasis p fun i => closure (f '' s i)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- A bijective local diffeomorphism is a diffeomorphism.  -/
IsLocalDiffeomorph.diffeomorphOfBijective : {𝕜 : 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] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        {I : ModelWithCorners 𝕜 E H₁} →
                          {J : ModelWithCorners 𝕜 F H₂} →
                            {M : Type u_8} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H₂ N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            IsLocalDiffeomorph I J n f → Function.Bijective f → Diffeomorph I J M N n
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_zpow_le : ∀ {S : Type u_1} [inst : SeminormedGroup S] [IsUltrametricDist S] (x : S) (z : ℤ), ‖x ^ z‖ ≤ ‖x‖
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.addMonoid.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : AddMonoid G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffAdd I' n G], ContMDiffMap.addMonoid = Function.Injective.addMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Lean.Parser.Do
Lean.Parser.Term.doIfLetPure : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.kernelBiprodSndIso_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.kernelBiprodSndIso.inv =
    CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.snd 0)
      (CategoryTheory.Limits.biprod.sndKernelFork X Y)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.eq_of_toPolyC_eq : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (a b : Lean.Grind.CommRing.Expr),
  (a.toPolyC c == b.toPolyC c) = true → Lean.Grind.CommRing.Expr.denote ctx a = Lean.Grind.CommRing.Expr.denote ctx b
-- Lean.Parser.Command
Lean.Parser.Command.classInductive.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Array.Lex.Basic
/-- Compares arrays lexicographically with respect to a comparison `lt` on their elements.

Specifically, `Array.lex as bs lt` is true if
* `bs` is larger than `as` and `as` is pairwise equivalent via `==` to the initial segment of `bs`,
  or
* there is an index `i` such that `lt as[i] bs[i]`, and for all `j < i`, `as[j] == bs[j]`.
 -/
Array.lex : {α : Type u_1} → [BEq α] → Array α → Array α → autoParam (α → α → Bool) Array.lex._auto_1 → Bool
-- Mathlib.Algebra.Order.Group.Bounds
IsGLB.exists_between_self_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {s : Set α} {a ε : α},
  IsGLB s a → 0 < ε → ∃ b ∈ s, a ≤ b ∧ b < a + ε
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α], Set.Iic ⊤ = Set.univ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get!_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ \ t₂).get! k = default
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.TryTactic : Type
-- Std.Data.ExtHashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtHashMap.getKey! : {α : Type u} →
  {β : Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → [Inhabited α] → Std.ExtHashMap α β → α → α
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.TacticMVarKind.autoParam.sizeOf_spec : ∀ (argName : Lean.Name), sizeOf (Lean.Elab.Term.TacticMVarKind.autoParam argName) = 1 + sizeOf argName
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.one_toProd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A],
  DoubleCentralizer.toProd 1 = 1
-- Mathlib.Topology.MetricSpace.Isometry
/-- **Alias** of `Isometry.preimage_closedEBall`. -/
Isometry.preimage_emetric_closedBall : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ENNReal), f ⁻¹' Metric.closedEBall (f x) r = Metric.closedEBall x r
-- Init.Data.Float.Model.Float
/-- Converts a `Float.Model` to a `UInt16`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.toUInt16 : Float.Model → UInt16
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Everyone epimorphism is a regular epimorphism  -/
CategoryTheory.IsRegularEpiCategory.regularEpiOfEpi : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.IsRegularEpiCategory C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Epi f], CategoryTheory.IsRegularEpi f
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.IsFinite.isFiniteType_relations : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat}
  {inst_2 : J.WEqualsLocallyBijective AddCommGrpCat} {M : SheafOfModules R} {p : M.Presentation} [self : p.IsFinite],
  p.relations.IsFiniteType
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.eVariationOn_Ico_eq_Icc_of_continuousWithinAt : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [DenselyOrdered α] {f : α → E} {a b : α},
  ContinuousWithinAt f (Set.Iic a) a → eVariationOn f (Set.Ico b a) = eVariationOn f (Set.Icc b a)
-- Mathlib.Topology.Algebra.Semigroup
/-- A version of `exists_idempotent_of_compact_t2_of_continuous_mul_left` where the idempotent lies
in some specified nonempty compact subsemigroup.  -/
exists_idempotent_in_compact_subsemigroup : ∀ {M : Type u_1} [inst : Semigroup M] [inst_1 : TopologicalSpace M] [T2Space M],
  (∀ (r : M), Continuous fun x => x * r) →
    ∀ (s : Set M), s.Nonempty → IsCompact s → (∀ x ∈ s, ∀ y ∈ s, x * y ∈ s) → ∃ m ∈ s, m * m = m
-- Batteries.Recycling.RBTree.Basic
RBTree.instReprRBColor : Repr RBTree.RBColor
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
          k ∈ List.map Sigma.fst l → ∀ {h' : k' ∈ m.insertMany l}, (m.insertMany l).getKey k' h' = k
-- Mathlib.Algebra.CubicDiscriminant
Cubic.of_d_eq_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.c = 0 → P.d = 0 → P.toPoly = 0
-- Mathlib.Data.NNReal.Defs
NNReal.coe_pos : ∀ {r : NNReal}, 0 < ↑r ↔ 0 < r
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.div_max_sq_ge_one : ∀ (x : Fin 2 → ℤ), x ≠ 0 → 1 ≤ (↑(x 0) / ‖x‖) ^ 2 ∨ 1 ≤ (↑(x 1) / ‖x‖) ^ 2
-- Mathlib.Control.Bifunctor
Bifunctor.comp_snd : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β₀ β₁ β₂ : Type u₁}
  (g : β₀ → β₁) (g' : β₁ → β₂) (x : F α β₀), Bifunctor.snd g' (Bifunctor.snd g x) = Bifunctor.snd (g' ∘ g) x
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_intCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIocDiv hp (a + ↑m * p) b = toIocDiv hp a b - m
-- Init.Data.List.Lemmas
List.map_map : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {g : β → γ} {f : α → β} {l : List α},
  List.map g (List.map f l) = List.map (g ∘ f) l
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.pap.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fn : Lean.Name) (args : Array (Lean.Compiler.LCNF.Arg pu))
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_15) (fn_1 : Lean.Name)
  (args_1 : Array (Lean.Compiler.LCNF.Arg pu))
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_15),
  (Lean.Compiler.LCNF.LetValue.pap fn args h = Lean.Compiler.LCNF.LetValue.pap fn_1 args_1 h_1) =
    (fn = fn_1 ∧ args = args_1)
-- Std.Async.Basic
Std.Async.MaybeTask.instFunctor : Functor Std.Async.MaybeTask
-- Mathlib.Topology.Connected.PathConnected
/-- The path component of the identity in an additive topological
group, as an additive subgroup.  -/
AddSubgroup.pathComponentZero : (G : Type u_4) → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [IsTopologicalAddGroup G] → AddSubgroup G
-- Init.Prelude
/-- Returns the lesser of its two arguments. 

Conventions for notations in identifiers:

 * The recommended spelling of `min` in identifiers is `min`.

 * The recommended spelling of `⊓` in identifiers is `inf` (`⊓` is the preferred notation for `min` when the type is not linearly ordered.). -/
Min.min : {α : Type u} → [self : Min α] → α → α → α
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.ret : Lean.IR.Arg → Lean.IR.FnBody
-- Init.Data.Int.Gcd
Int.lcm_mul_left_right_eq_mul_of_lcm_eq_mul : ∀ {n m k : ℤ}, n.lcm m = n.natAbs * m.natAbs → n.lcm (k * m) = n.lcm k * m.natAbs
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.ExtDHashMap.Const.insertMany m l).getKey? k' = some k