mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Module.FiniteDimension
ContinuousLinearMap.continuous_det : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace 𝕜], Continuous fun f => f.det
-- Mathlib.RingTheory.Smooth.Basic
Algebra.Extension.H1Cotangent.equivOfFormallySmooth_toLinearMap : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {P₁ : Algebra.Extension R A} {P₂ : Algebra.Extension R A} (f : P₁.Hom P₂) [inst_3 : Algebra.FormallySmooth R P₁.Ring]
  [inst_4 : Algebra.FormallySmooth R P₂.Ring],
  ↑(Algebra.Extension.H1Cotangent.equivOfFormallySmooth P₁ P₂) = Algebra.Extension.H1Cotangent.map f
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.pnat_to_nat_coe_proc : Lean.ParserDescr
-- Init.Data.List.Basic
List.flatten_cons : ∀ {α : Type u_1} {l : List α} {L : List (List α)}, (l :: L).flatten = l ++ L.flatten
-- Mathlib.Topology.Category.Sequential
/-- The underlying topological space of an object of `Sequential`.  -/
Sequential.toTop : Sequential → TopCat
-- Mathlib.GroupTheory.GroupAction.IterateAct
/-- A structure with a single field `val : ℕ` that acts on `α` by `⟨n⟩ • x = f^[n] x`.  -/
IterateMulAct : {α : Type u_1} → (α → α) → Type
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
pentagonal_neg_lt_pentagonal_add_one : ∀ {k : ℤ}, 0 ≤ k → pentagonal (-k) < pentagonal (k + 1)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Increment.0.SzemerediRegularity.distinctPairs.congr_simp : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} (hP : P.IsEquipartition)
  (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ {inst_2 : DecidableRel G.Adj} [inst_3 : DecidableRel G_1.Adj] (ε ε_1 : ℝ),
      ε = ε_1 →
        ∀ (x x_1 : ↥P.parts.offDiag),
          x = x_1 → SzemerediRegularity.distinctPairs✝ hP G ε x = SzemerediRegularity.distinctPairs✝ hP G_1 ε_1 x_1
-- Mathlib.Algebra.Ring.Parity
natCast_eq_one_of_odd_of_two_eq_zero : ∀ {R : Type u_4} [inst : AddMonoidWithOne R] {n : ℕ}, Odd n → 2 = 0 → ↑n = 1
-- Init.Data.List.Attach
List.pmap_cons : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {a : α} {l : List α} (h : ∀ b ∈ a :: l, P b),
  List.pmap f (a :: l) h = f a ⋯ :: List.pmap f l ⋯
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_mono : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : Zero M] {s : Set α} {f g : α → M},
  f ≤ g → s.indicator f ≤ s.indicator g
-- Mathlib.Topology.Algebra.Group.Basic
continuousOn_inv_iff : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G]
  [inst_3 : TopologicalSpace α] {f : α → G} {s : Set α}, ContinuousOn f⁻¹ s ↔ ContinuousOn f s
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_erase_eq_of_not_compare_eq_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (∀ {km : α}, t.max? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).max? = t.max?
-- Mathlib.Topology.MetricSpace.Polish
TopologicalSpace.Opens.CompleteCopy.instT0Space : ∀ {α : Type u_1} [inst : MetricSpace α] {s : TopologicalSpace.Opens α}, T0Space s.CompleteCopy
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac_app : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H] {D₁ : Type u₄}
  {D₂ : Type u₅} [inst_3 : CategoryTheory.Category.{v₄, u₄} D₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} D₂]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₁.IsLocalization W₁] [inst_6 : L₂.IsLocalization W₂] (F : CategoryTheory.Functor C₂ H)
  (F₁ : CategoryTheory.Functor D₁ H) (α₁ : Φ.functor.comp F ⟶ L₁.comp F₁) (F₂ : CategoryTheory.Functor D₂ H)
  (α₂ : F ⟶ L₂.comp F₂) [inst_7 : F₁.IsRightDerivedFunctor α₁ W₁] (X : C₁),
  CategoryTheory.CategoryStruct.comp (α₁.app X) ((Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂).app (L₁.obj X)) =
    CategoryTheory.CategoryStruct.comp (α₂.app (Φ.functor.obj X))
      (F₂.map ((CategoryTheory.CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom.app X))
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.ιCofibrantObjectLocalizerMorphism_functor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.BifibrantObject.ιCofibrantObjectLocalizerMorphism C).functor =
    HomotopicalAlgebra.BifibrantObject.ιCofibrantObject
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.foldM_filterWithPostcondition : ∀ {ps : Std.Do.PostShape} {α β δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : Monad o] [LawfulMonad n] [LawfulMonad o]
  [inst_6 : Std.Do.WPMonad o ps] [inst_7 : Std.IteratorLoop α Id n] [inst_8 : Std.IteratorLoop α Id o]
  [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o] [inst_11 : MonadLiftT n o] [LawfulMonadLiftT n o]
  {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} {g : δ → β → o δ} {init : δ} {it : Std.Iter β}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b => do
          let __do_lift ← liftM (f b).run
          if __do_lift.down = true then g d b else pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.Iter.filterWithPostcondition f it) ⦃Q⦄
-- Init.Data.List.Sublist
List.Sublist.middle : ∀ {α : Type u_1} {l₁ l₂ l : List α}, l.Sublist (l₁ ++ l₂) → ∀ (a : α), l.Sublist (l₁ ++ a :: l₂)
-- Mathlib.Algebra.Group.PUnit
PUnit.addCommGroup.eq_1 : PUnit.addCommGroup =
  { add := fun x x_1 => PUnit.unit, add_assoc := PUnit.addCommGroup._proof_7, zero := PUnit.unit,
    zero_add := PUnit.addCommGroup._proof_8, add_zero := PUnit.addCommGroup._proof_9, nsmul := fun x x_1 => PUnit.unit,
    nsmul_zero := PUnit.addCommGroup._proof_1, nsmul_succ := PUnit.addCommGroup._proof_2, neg := fun x => PUnit.unit,
    zsmul := fun x x_1 => PUnit.unit, sub_eq_add_neg := PUnit.addCommGroup._proof_3,
    zsmul_zero' := PUnit.addCommGroup._proof_4, zsmul_succ' := PUnit.addCommGroup._proof_5,
    zsmul_neg' := PUnit.addCommGroup._proof_6, neg_add_cancel := PUnit.addCommGroup._proof_10,
    add_comm := PUnit.addCommGroup._proof_11 }
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
/-- `C` has all finite coproducts  -/
CategoryTheory.Limits.HasFiniteCoproducts.out : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasFiniteCoproducts C] (n : ℕ),
  CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (Fin n)) C
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_le_one_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a : G₀} [PosMulStrictMono G₀]
  [ZeroLEOneClass G₀], a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the coherence composition `η ≪⊗≫ θ := η ≪≫ α ≪≫ θ`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.coherenceCompM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
    Mathlib.Tactic.BicategoryLike.CoherenceHom →
      Mathlib.Tactic.BicategoryLike.Mor₂Iso →
        Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_mul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.SemiCartesianMonoidalCategory.fst X X + CategoryTheory.SemiCartesianMonoidalCategory.snd X X
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- Variant of `prod_singleton` not applied to a function.  -/
Finset.prod_singleton' : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] (a : ι), {a}.prod = fun f => f a
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.instSetLikeProdNat : SetLike YoungDiagram (ℕ × ℕ)
-- Mathlib.Data.ENNReal.Basic
ENNReal.instOne : One ENNReal
-- Mathlib.Topology.ContinuousOn
/-- A function is continuous on a union of open sets `s i` iff it is continuous on each `s i`.  -/
continuousOn_iUnion_iff_of_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Type u_5}
  {s : ι → Set α}, (∀ (i : ι), IsOpen (s i)) → (ContinuousOn f (⋃ i, s i) ↔ ∀ (i : ι), ContinuousOn f (s i))
-- Init.Data.List.Basic
List.nil_lex_cons : ∀ {α : Type u} {lt : α → α → Bool} [inst : BEq α] {b : α} {bs : List α}, [].lex (b :: bs) lt = true
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_comm : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) {α : l₂ ⟶ l₁}
  {β : l₁ ⟶ l₂},
  CategoryTheory.CategoryStruct.comp β α = CategoryTheory.CategoryStruct.id l₁ →
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂) α)
        ((CategoryTheory.Bicategory.conjugateEquiv adj₂ adj₁) β) =
      CategoryTheory.CategoryStruct.id r₁
-- Mathlib.GroupTheory.Nilpotent
/-- A quotient of a nilpotent group is nilpotent.  -/
Group.nilpotent_quotient_of_nilpotent : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Normal] [_h : Group.IsNilpotent G],
  Group.IsNilpotent (G ⧸ H)
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- The standard one-dimensional isocrystal of slope `m : ℤ` is an isocrystal.  -/
WittVector.instIsocrystalStandardOneDimIsocrystal : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (k : Type u_1) →
      [inst_1 : CommRing k] →
        [IsDomain k] →
          [inst_3 : CharP k p] →
            [inst_4 : PerfectRing k p] → (m : ℤ) → WittVector.Isocrystal p k (WittVector.StandardOneDimIsocrystal p k m)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.le_limitsClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)], P ≤ P.limitsClosure J
-- Std.Do.SPred.SVal
_private.Std.Do.SPred.SVal.0.Std.Do.SVal.curry.match_1.eq_1 : ∀ {α : Type u_1} (motive : (σs : List (Type u_1)) → (Std.Do.SVal.StateTuple σs → α) → Sort u_2)
  (f : Std.Do.SVal.StateTuple [] → α) (h_1 : (f : Std.Do.SVal.StateTuple [] → α) → motive [] f)
  (h_2 :
    (head : Type u_1) →
      (tail : List (Type u_1)) → (f : Std.Do.SVal.StateTuple (head :: tail) → α) → motive (head :: tail) f),
  (match [], f with
    | [], f => h_1 f
    | head :: tail, f => h_2 head tail f) =
    h_1 f
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Let `C(G, A)` denote the complex of inhomogeneous cochains of `A : Rep k G`. This lemma
says `d₀₁` gives a simpler expression for the 0th differential: that is, the following
square commutes:
```
  C⁰(G, A) --d 0 1--> C¹(G, A)
  |                     |
  |                     |
  |                     |
  v                     v
  A ------d₀₁-----> Fun(G, A)
```
where the vertical arrows are `cochainsIso₀` and `cochainsIso₁` respectively.
 -/
groupCohomology.comp_d₀₁_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₀ A).hom (groupCohomology.d₀₁ A) =
    CategoryTheory.CategoryStruct.comp ((groupCohomology.inhomogeneousCochains A).d 0 1)
      (groupCohomology.cochainsIso₁ A).hom
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.ext_iff : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {f g : ModularForm Γ k}, f = g ↔ ∀ (x : UpperHalfPlane), f x = g x
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterMapWithPostcondition.match_3.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Init.Data.UInt.Lemmas
UInt64.ofNatClamp_uSizeToNat : ∀ (n : USize), UInt64.ofNatClamp n.toNat = n.toUInt64
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The `R`-algebra isomorphism from `R[W] / ⟨X - x, Y - y(X)⟩` to `R` obtained by evaluation at
some `y(X)` in `R[X]` and at some `x` in `R` provided that `W(x, y(x)) = 0`.  -/
WeierstrassCurve.Affine.CoordinateRing.quotientXYIdealEquiv : {R : Type r} →
  [inst : CommRing R] →
    {W' : WeierstrassCurve.Affine R} →
      {x : R} →
        {y : Polynomial R} →
          Polynomial.eval x (Polynomial.eval y W'.polynomial) = 0 →
            (W'.CoordinateRing ⧸ WeierstrassCurve.Affine.CoordinateRing.XYIdeal W' x y) ≃ₐ[R] R
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.MorphismProperty.IsCompatibleWithShift.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {A : Type w}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A],
  (∀ (a : A), W.inverseImage (CategoryTheory.shiftFunctor C a) = W) → W.IsCompatibleWithShift A
-- Mathlib.CategoryTheory.Limits.EpiMono
CategoryTheory.epi_iff_isPushout : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔
    CategoryTheory.IsPushout f f (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y)
-- Mathlib.Order.Defs.Unbundled
irrefl_def : ∀ {α : Sort u_1} {r : α → α → Prop}, Std.Irrefl r ↔ ∀ ⦃a : α⦄, ¬r a a
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.union.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Raw α β),
  m₁.union m₂ =
    if h₁ : 0 < m₁.buckets.size then
      if h₂ : 0 < m₂.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.union ⟨m₁, h₁⟩ ⟨m₂, h₂⟩) else m₁
    else m₂
-- Init.Data.Array.FinRange
Array.getElem_finRange : ∀ {n i : ℕ} (h : i < (Array.finRange n).size), (Array.finRange n)[i] = Fin.cast ⋯ ⟨i, h⟩
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.cast_cast : ∀ {s t u : String.Slice} {hst : s.copy = t.copy} {htu : t.copy = u.copy} {st : String.Slice.Pattern.SearchStep s},
  String.Slice.Pattern.SearchStep.cast htu (String.Slice.Pattern.SearchStep.cast hst st) =
    String.Slice.Pattern.SearchStep.cast ⋯ st
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.coyoneda_preservesLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  (F : CategoryTheory.Functor J C) (X : Cᵒᵖ), CategoryTheory.Limits.PreservesLimit F (CategoryTheory.coyoneda.obj X)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.apply_revSkipWhile_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos : s.Pos} {h : pos.revSkipWhile P ≠ s.startPos},
  ¬P (((pos.revSkipWhile P).prev h).get ⋯)
-- Init.Data.String.Basic
String.Pos.sliceTo_ofSliceTo : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos}, p₀.sliceTo (String.Pos.ofSliceTo p) ⋯ = p
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (α β : X ⟶ Y)
  (w : α.base = β.base),
  CategoryTheory.CategoryStruct.comp α.c (CategoryTheory.Functor.whiskerRight (CategoryTheory.eqToHom ⋯) X.presheaf) =
      β.c →
    α = β
-- Mathlib.Analysis.Complex.Trigonometric
Real.cot_inv_eq_tan : ∀ (x : ℝ), x.cot⁻¹ = Real.tan x
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `insertMany` which can be used in absence of balance information but still
assumes the preconditions of `insertMany`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.insertMany! : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      {ρ : Type w} →
        [ForIn Id ρ ((a : α) × β a)] → (t : Std.DTreeMap.Internal.Impl α β) → ρ → t.IteratedSlowInsertionInto
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_roc_eq_zero_iff : ∀ {m n i : ℕ}, (m<...=n).toArray[i]! = 0 ↔ n ≤ i + m
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.inv_hom_id_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) {Z : D} (h : G.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.inv.app X) (CategoryTheory.CategoryStruct.comp (α.hom.app X) h) = h
-- Mathlib.GroupTheory.Subgroup.Simple
IsSimpleAddGroup.mk : ∀ {A : Type u_2} [inst : AddGroup A] [toNontrivial : Nontrivial A],
  (∀ (H : AddSubgroup A), H.Normal → H = ⊥ ∨ H = ⊤) → IsSimpleAddGroup A
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Implementation of `parallelPair`, do not use directly.  -/
CategoryTheory.Limits.parallelPair.parallelPairHom : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (X ⟶ Y) →
        (X ⟶ Y) →
          {x y : CategoryTheory.Limits.WalkingParallelPair} →
            (x ⟶ y) →
              (CategoryTheory.Limits.parallelPair.parallelPairObj X Y x ⟶
                CategoryTheory.Limits.parallelPair.parallelPairObj X Y y)
-- Lean.Elab.Command
/-- Elaborate `x` with `stx` on the macro stack  -/
Lean.Elab.Command.withMacroExpansion : {α : Type} → Lean.Syntax → Lean.Syntax → Lean.Elab.Command.CommandElabM α → Lean.Elab.Command.CommandElabM α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α}
  {h' : k ∈ Std.DTreeMap.Raw.filterMap f t} (h : t.WF),
  (Std.DTreeMap.Raw.filterMap f t).get k h' = (f k (t.get k ⋯)).get ⋯
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_iSup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) {ι : Type u_3} (P : ι → CategoryTheory.MorphismProperty D),
  (⨆ i, P i).inverseImage F = ⨆ i, (P i).inverseImage F
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_eq_zero : ∀ {r : ℝ}, r.toNNReal = 0 ↔ r ≤ 0
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.evalCLM_apply : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : CommSemiring R] [inst_4 : IsTopologicalSemiring R] {𝕜 : Type u_3} [inst_5 : Semiring 𝕜]
  [inst_6 : Module 𝕜 R] [inst_7 : ContinuousConstSMul 𝕜 R] (x : X) (f : ContinuousMapZero X R),
  (ContinuousMapZero.evalCLM 𝕜 x) f = f x
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumAlgEquiv_X_inl : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (c : S₁),
  (MvPolynomial.sumAlgEquiv R S₁ S₂) (MvPolynomial.X (Sum.inl c)) = MvPolynomial.X c
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the auxiliary object of right fractions  -/
CategoryTheory.MorphismProperty.RightFraction₂.X' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.RightFraction₂ X Y → C
-- Mathlib.Order.SuccPred.Basic
WithBot.succ_unbot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α] (a : WithBot α) (ha : a ≠ ⊥),
  Order.succ (a.unbot ha) = (Order.succ a).unbot ⋯
-- Mathlib.ModelTheory.Satisfiability
Cardinal.empty_theory_categorical : ∀ (κ : Cardinal.{w}) (T : FirstOrder.Language.empty.Theory), κ.Categorical T
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.mk : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  (∀ (t : Set α), t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t) → l.HasBasis p s
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.Equiv.mapM : ∀ {α₁ α₂ β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : Monad n] [inst_3 : MonadAttach n] [inst_4 : LawfulMonad n] [inst_5 : Std.Iterator α₁ m β]
  [inst_6 : Std.Iterator α₂ m β] [inst_7 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n γ} {ita : Std.IterM m β}
  {itb : Std.IterM m β}, ita.Equiv itb → (Std.IterM.mapM f ita).Equiv (Std.IterM.mapM f itb)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.SubgoalsResult.instTypeBody : Lean.Meta.SynthInstance.SubgoalsResult → Lean.Expr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryGED_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {fallback : (a : α) × β a},
          Std.DTreeMap.Internal.Impl.getEntryGED k t₁ fallback = Std.DTreeMap.Internal.Impl.getEntryGED k t₂ fallback
-- Init.System.Platform
/-- The platform's native concurrency limit (number of hardware threads), or `0` if indeterminate.
 -/
System.Platform.Internal.getHardwareConcurrency : Unit → UInt32
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.diagramIsoParallelPair_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C)
  (X : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.diagramIsoParallelPair F).hom.app X = CategoryTheory.eqToHom ⋯
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  I.glueDataObjι U =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))
      (AlgebraicGeometry.IsAffineOpen.isoSpec ⋯).inv
-- Init.Data.Iterators.Basic
Std.Iter.isPlausibleSuccessorOf_iff_exists : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it' it : Std.Iter β},
  it'.IsPlausibleSuccessorOf it ↔ ∃ step, step.successor = some it' ∧ it.IsPlausibleStep step
-- Mathlib.Order.CompleteLattice.Group
le_iInf₂_add : ∀ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] [inst_1 : Add α] [AddLeftMono α]
  [AddRightMono α] (u v : (i : ι) → κ i → α), (⨅ i, ⨅ j, u i j) + ⨅ i, ⨅ j, v i j ≤ ⨅ i, ⨅ j, u i j + v i j
-- Mathlib.RingTheory.Frobenius
AlgHom.IsArithFrobAt.mk_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ : S →ₐ[R] S}
  {Q : Ideal S},
  φ.IsArithFrobAt Q → ∀ (x : S), (Ideal.Quotient.mk Q) (φ x) = (Ideal.Quotient.mk Q) x ^ Nat.card (R ⧸ Ideal.under R Q)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.coconeSMul_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R}
  {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM),
  (PresheafOfModules.ModuleColimit.coconeSMul hcR hcM).pt = PresheafOfModules.ModuleColimit hcR hcM