mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.EnrichedOrdinaryCategory.homEquiv_comp : ∀ {V : Type u'} {inst : CategoryTheory.Category.{v', u'} V} {inst_1 : CategoryTheory.MonoidalCategory V} {C : Type u}
  {inst_2 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.EnrichedOrdinaryCategory.homEquiv (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.EnrichedOrdinaryCategory.homEquiv f)
          (CategoryTheory.EnrichedOrdinaryCategory.homEquiv g))
        (CategoryTheory.eComp V X Y Z))
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- `checkCoverage` failed because some of the theorem parameters are missing,
`pos` contains their positions
 -/
Lean.Meta.Grind.CheckCoverageResult.missing : List ℕ → Lean.Meta.Grind.CheckCoverageResult
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.opRingEquiv_op_X : ∀ {R : Type u_1} [inst : Semiring R], (Polynomial.opRingEquiv R) (MulOpposite.op Polynomial.X) = Polynomial.X
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∉ t₂ → (t₁ \ t₂).getD k fallback = t₁.getD k fallback
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.eq_empty_iff_forall_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m = ∅ ↔ ∀ (a : α), m.contains a = false
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.FG.of_restrictScalars : ∀ {K : Type u_1} {L : Type u_2} {E : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field E]
  [inst_3 : Algebra K L] [inst_4 : Algebra K E] [inst_5 : Algebra L E] [inst_6 : IsScalarTower K L E]
  {E' : IntermediateField L E}, (IntermediateField.restrictScalars K E').FG → E'.FG
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonInitializeResult.fromJson : Lean.Json → Except String Lean.Lsp.InitializeResult
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.forallTelescopeReducingImp : {α : Type} → Lean.Expr → (Array Lean.Expr → Lean.Expr → Lean.MetaM α) → Bool → Bool → Lean.MetaM α
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.instInhabited : {R : Type u} → [inst : CommRing R] → Inhabited (CommHopfAlgCat R)
-- Std.Http.Protocol.H1
/-- Error thrown by the machine.
 -/
Std.Http.Protocol.H1.Machine.error : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Option Std.Http.Protocol.H1.Error
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_single_le : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] (a : Γ) (r : R),
  ((HahnSeries.single a) r).cardSupp ≤ 1
-- Mathlib.AlgebraicTopology.Reedy.Basic
/-- A Reedy structure on a category `C` equipped with two multiplicative
classes of morphisms `W₁` and `W₂` consists of the data of a degree
map for objects `deg : C → α`, where `α` is a well ordered type. The first
two axioms `lt₁` and `lt₂` express the behaviour of the degree with
respect to morphisms in `W₁` (resp. `W₂`) that are not identities, and
the last axiom says that any morphism can be factored in a unique way
as a morphism in `W₁` followed by a morphism in `W₂`.  -/
HomotopicalAlgebra.ReedyStructure : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W₁ W₂ : CategoryTheory.MorphismProperty C) →
      [W₁.IsMultiplicative] →
        [W₂.IsMultiplicative] →
          (α : Type u_2) →
            [inst : LinearOrder α] → [OrderBot α] → [SuccOrder α] → [WellFoundedLT α] → Type (max u_1 u_2)
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The cylinder object of a homological complex `K` is the homotopy cofiber
of the morphism  `biprod.lift (𝟙 K) (-𝟙 K) : K ⟶ K ⊞ K`.  -/
HomologicalComplex.cylinder : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            [DecidableRel c.Rel] →
              [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [K.HasCylinder] → HomologicalComplex C c
-- Mathlib.Topology.Gluing
/-- For each `i j : J`, an open set `V i j ⊆ U i`  -/
TopCat.GlueData.MkCore.V : (self : TopCat.GlueData.MkCore) → (i : self.J) → self.J → TopologicalSpace.Opens ↑(self.U i)
-- Mathlib.Algebra.Group.Conj
MonoidHom.map_isConj : ∀ {α : Type u} {β : Type v} [inst : Monoid α] [inst_1 : Monoid β] (f : α →* β) {a b : α},
  IsConj a b → IsConj (f a) (f b)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- The unit of the equivalence we're constructing.  -/
CategoryTheory.OverPresheafAux.unit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      CategoryTheory.Functor.id (CategoryTheory.Over A) ≅
        (CategoryTheory.OverPresheafAux.restrictedYoneda A).comp
          (CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver A)
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.zariskisMainProperty_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal S},
  Algebra.ZariskisMainProperty R p ↔ ∃ r ∉ p, IsIntegral R r ∧ ∀ (x : S), ∃ m, IsIntegral R (r ^ m * x)
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.Result.cast : Lean.Meta.Grind.Result✝
-- Mathlib.Order.RelIso.Basic
preimage_equivalence : ∀ {α : Type u_5} {β : Type u_6} (f : α → β) {s : β → β → Prop}, Equivalence s → Equivalence (f ⁻¹'o s)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addLECancellable_of_ne_bot : ∀ {α : Type u} [inst : Add α] {x : WithBot α} [inst_1 : LE α] [AddLeftReflectLE α], x ≠ ⊥ → AddLECancellable x
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
Submodule.FG.lTensor.directLimit_apply' : ∀ (R : Type u) (M : Type u_1) (N : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq { Q // Q.FG }] (Q : Submodule R N) (hQ : Q.FG)
  (u : TensorProduct R M ↥Q),
  (Submodule.FG.lTensor.directLimit R M N)
      ((Module.DirectLimit.of R { Q // Q.FG } (fun Q => TensorProduct R M ↥↑Q)
          (fun x x_1 hPQ => LinearMap.lTensor M (Submodule.inclusion hPQ)) ⟨Q, hQ⟩)
        u) =
    (LinearMap.lTensor M Q.subtype) u
-- Batteries.Data.AssocList
/-- `O(n)`. Fold a function over the list, from head to tail.  -/
Batteries.AssocList.foldl : {δ : Type u_1} → {α : Type u_2} → {β : Type u_3} → (δ → α → β → δ) → δ → Batteries.AssocList α β → δ
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor_obj_g : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c),
  ((HomologicalComplex.shortComplexFunctor C c i).obj K).g = K.d i (c.next i)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_rco_eq_some_iff : ∀ {k m n : ℤ} {i : ℕ}, (m...n).toArray[i]? = some k ↔ i < (n - m).toNat ∧ m + ↑i = k
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.diagramIso_inv_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i : D.J × D.J),
  (D.diagramIso F).inv.app (CategoryTheory.Limits.WalkingMultispan.left i) =
    CategoryTheory.CategoryStruct.id
      ((D.mapGlueData F).diagram.multispan.obj (CategoryTheory.Limits.WalkingMultispan.left i))
-- Mathlib.Analysis.Normed.Group.Defs
/-- the `ℝ≥0`-valued norm function.  -/
NNNorm.nnnorm : {E : Type u_8} → [self : NNNorm E] → E → NNReal
-- Mathlib.Data.Set.Sigma
Set.sigma_eq_empty_iff : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)}, s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅
-- Mathlib.Order.SuccPred.LinearLocallyFinite
/-- If the order has a bot but no top, `toZ` defines an `OrderIso` between `ι` and `ℕ`.  -/
orderIsoNatOfLinearSuccPredArch : {ι : Type u_1} →
  [inst : LinearOrder ι] →
    [inst_1 : SuccOrder ι] → [PredOrder ι] → [IsSuccArchimedean ι] → [NoMaxOrder ι] → [OrderBot ι] → ι ≃o ℕ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.ordered_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  List.Pairwise (fun a b => cmp a b = Ordering.lt) t.keys
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.isoMk_inv : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} {x : CommRing X} {x_1 : CommRing Y} {x_2 : Algebra R X}
  {x_3 : Algebra R Y} (e : X ≃ₐ[R] Y), (CommAlgCat.isoMk e).inv = CommAlgCat.ofHom ↑e.symm
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
/-- `Fiber p S` has the structure of a category with morphisms being those lying over `𝟙 S`.  -/
CategoryTheory.Functor.Fiber.fiberCategory : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} → {S : 𝒮} → CategoryTheory.Category.{v₂, u₂} (p.Fiber S)
-- Mathlib.CategoryTheory.Limits.Skeleton
CategoryTheory.Limits.hasColimitsOfShape_thinSkeleton : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  [Quiver.IsThin C] [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.ThinSkeleton C)
-- Mathlib.Data.Real.Basic
Real.ofCauchy.sizeOf_spec : ∀ (cauchy : CauSeq.Completion.Cauchy abs), sizeOf { cauchy := cauchy } = 1 + sizeOf cauchy
-- Mathlib.RingTheory.FiniteLength
IsFiniteLength.of_surjective : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N},
  IsFiniteLength R M → Function.Surjective ⇑f → IsFiniteLength R N
-- Mathlib.Data.Finset.Lattice.Fold
Finset.disjoint_sup_right : ∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α} {a : α},
  Disjoint a (s.sup f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint a (f i)
-- Mathlib.CategoryTheory.Monoidal.Tor
/-- The higher `Tor` groups for `X` and `Y` are zero if `Y` is projective.  -/
CategoryTheory.isZero_Tor_succ_of_projective : ∀ (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] (X Y : C) [CategoryTheory.Projective Y] (n : ℕ),
  CategoryTheory.Limits.IsZero (((CategoryTheory.Tor C (n + 1)).obj X).obj Y)
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) {Δ Δ' : SimplexCategory} (i : Δ ⟶ Δ') [inst_2 : CategoryTheory.Mono i] {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X Δ.len ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono (AlgebraicTopology.AlternatingFaceMapComplex.obj X) i)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f Δ.len) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f Δ'.len)
      (CategoryTheory.CategoryStruct.comp (X.map i.op) h)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.negPart.eq_1 : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp ℝ p μ)),
  MeasureTheory.Lp.negPart f = MeasureTheory.Lp.posPart (-f)
-- Aesop.Util.EqualUpToIds
Aesop.unassignedMVarsEqualUptoIds' : Option Lean.MetavarContext →
  Lean.MetavarContext →
    Lean.MetavarContext →
      Lean.MVarId → Lean.MVarId → optParam Bool false → Lean.MetaM (Bool × Aesop.EqualUpToIdsM.State)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 0-cycles of the complex of inhomogeneous chains of `A` are isomorphic to
`A.ρ.coinvariants`, which is a simpler type.  -/
groupHomology.opcyclesIso₀ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        HomologicalComplex.opcycles (groupHomology.inhomogeneousChains A) 0 ≅ (Rep.coinvariantsFunctor k G).obj A
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.instIsFiniteKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsFiniteKernel (κ n)] (a b : ℕ),
  ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.Kernel.partialTraj κ a b)
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instTransOrdOffset : Std.TransOrd Std.Time.Minute.Offset
-- Init.Data.List.Basic
/-- Returns the last element of the list for which the predicate `p` returns `true`, or `none` if no
such element is found.

`O(|l|)`.

Examples:
* `[7, 6, 5, 8, 1, 2, 6].findRev? (· < 5) = some 2`
* `[7, 6, 5, 8, 1, 2, 6].findRev? (· < 1) = none`
 -/
List.findRev? : {α : Type u} → (α → Bool) → List α → Option α
-- Mathlib.Geometry.Convex.Set
_private.Mathlib.Geometry.Convex.Set.0.Convexity.IsConvexSet.eq_1 : ∀ (R : Type u_3) {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] (s : Set X),
  Convexity.IsConvexSet R s = ∀ ⦃w : Convexity.StdSimplex R X⦄, ↑w.weights.support ⊆ s → Convexity.sConvexComb w ∈ s
-- Batteries.CodeAction.Attr
/-- Read a tacticSeq code action from a declaration of the right type.  -/
Batteries.CodeAction.mkTacticSeqCodeAction : Lean.Name → Lean.ImportM Batteries.CodeAction.TacticSeqCodeAction
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_get?_eq_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a : α},
  (t.get? a).isSome = t.contains a
-- Mathlib.RingTheory.Congruence.Defs
RingCon.toCon_inj : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R}, c.toCon = d.toCon ↔ c = d
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.triangle_mor₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  (CochainComplex.mappingCone.triangle φ).mor₂ = CochainComplex.mappingCone.inr φ
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.next.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f_1 : ℝ → E → E} (e_f : f = f_1)
  {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x x_1 : E} (e_x : x = x_1) {a a_1 : NNReal} (e_a : a = a_1)
  {r L K K_1 : NNReal} (e_K : K = K_1) (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r)
  (α α_1 : ODE.FunSpace t₀ x₀ r L), α = α_1 → ODE.FunSpace.next hf hx α = ODE.FunSpace.next ⋯ ⋯ α_1
-- Mathlib.RepresentationTheory.Intertwining
/-- The identity map, considered as an intertwining map from a representation to itself.  -/
Representation.IntertwiningMap.id : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module A V] → (ρ : Representation A G V) → ρ.IntertwiningMap ρ
-- Lean.Meta.PPGoal
Lean.Meta.pp.implementationDetailHyps : Lean.Option Bool
-- Mathlib.RepresentationTheory.Submodule
Representation.invtSubmodule.eq_1 : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V), ρ.invtSubmodule = ⨅ g, Module.End.invtSubmodule (ρ g)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_rpow_iff : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → 0 < z → (x ^ z ≤ y ^ z ↔ x ≤ y)
-- Mathlib.RingTheory.Smooth.IntegralClosure
TensorProduct.toIntegralClosure_injective_of_flat : ∀ {R : Type u_1} {S : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Module.Flat R S],
  Function.Injective ⇑(TensorProduct.toIntegralClosure R S B)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGE.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (size : ℕ) (ky : α) (y : β ky)
  (l r : Std.DTreeMap.Internal.Impl α β) (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.getEntryGE k (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he =
    match h : compare k ky with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.getEntryGED k l ⟨ky, y⟩
    | Ordering.eq => ⟨ky, y⟩
    | Ordering.gt => Std.DTreeMap.Internal.Impl.getEntryGE k r ⋯ ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
SSet.instFibrationMapIhom : ∀ {E B X : SSet} (p : E ⟶ B) [HomotopicalAlgebra.Fibration p],
  HomotopicalAlgebra.Fibration ((CategoryTheory.ihom X).map p)
-- Mathlib.Computability.Primrec.Basic
Primrec₂.primrecRel : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {R : α → β → Prop}
  [inst_2 : DecidableRel R], (Primrec₂ fun a b => decide (R a b)) → PrimrecRel R
-- Std.Internal.Do.WP.Basic
/-- `ReaderT` lifts a `WPMonad` instance by adding a reader argument.  -/
Std.Internal.Do.ReaderT.instWPMonad : {m : Type u → Type z} →
  {EPred : Type u_1} →
    {ρ : Type u} →
      {Pred : Type v} →
        [inst : Monad m] →
          [inst_1 : Std.Internal.Do.Assertion Pred] →
            [inst_2 : Std.Internal.Do.Assertion EPred] →
              [Std.Internal.Do.WPMonad m Pred EPred] → Std.Internal.Do.WPMonad (ReaderT ρ m) (ρ → Pred) EPred
-- Mathlib.Data.Int.Init
Int.leInduction_base : ∀ {m : ℤ} {motive : (n : ℤ) → m ≤ n → Sort u_1} (base : motive m ⋯)
  (succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯), Int.leInduction base succ m ⋯ = base
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.mk : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} →
      {hζ : IsPrimitiveRoot ζ 3} →
        (a b c : NumberField.RingOfIntegers K) →
          (u : (NumberField.RingOfIntegers K)ˣ) →
            ¬hζ.toInteger - 1 ∣ a →
              ¬hζ.toInteger - 1 ∣ b →
                c ≠ 0 →
                  IsCoprime a b →
                    hζ.toInteger - 1 ∣ c → a ^ 3 + b ^ 3 = ↑u * c ^ 3 → FermatLastTheoremForThreeGen.Solution'✝ hζ
-- Mathlib.Order.Irreducible
/-- **Alias** of the reverse direction of `infIrred_ofDual`. -/
SupIrred.ofDual : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : αᵒᵈ}, SupIrred a → InfIrred (OrderDual.ofDual a)
-- Mathlib.Algebra.Lie.Subalgebra
LieHom.range_eq_map : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂), f.range = LieSubalgebra.map f ⊤
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_singleton : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] (f : ι → M) (i : ι),
  ({i}.expect fun j => f j) = f i
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flipFunctor_map_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  (CategoryTheory.Square.flipFunctor.map φ).τ₃ = φ.τ₂
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instOrderedStructureOfOrderOfIsExpansionOnOrderLHom : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : LE M]
  [inst_3 : FirstOrder.Language.order.Structure M] [FirstOrder.Language.order.OrderedStructure M]
  [L.orderLHom.IsExpansionOn M], L.OrderedStructure M
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instIsTopologicalGroup : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : CommGroup β]
  [inst_3 : IsTopologicalGroup β], IsTopologicalGroup C(α, β)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.isClosed_setOfPred_totallyBounded : ∀ {α : Type u_1} [inst : UniformSpace α], IsClosed {s | TotallyBounded ↑s}
-- Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
MeasureTheory.closedCompactCylinders.eq_cylinder : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)}
  (ht : t ∈ MeasureTheory.closedCompactCylinders X),
  t =
    MeasureTheory.cylinder (MeasureTheory.closedCompactCylinders.finset ht)
      (MeasureTheory.closedCompactCylinders.set ht)
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_three : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄),
  (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄).app 3 = f₄
-- Mathlib.Probability.Distributions.Uniform
PMF.uniformOfFinset.congr_simp : ∀ {α : Type u_1} (s s_1 : Finset α) (e_s : s = s_1) (hs : s.Nonempty),
  PMF.uniformOfFinset s hs = PMF.uniformOfFinset s_1 ⋯
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.instPowNat : {G : Type u_1} → [inst : Add G] → {a : G} → Pow (AddConstMap G G a a) ℕ
-- Init.Tactics
/-- The simp lemma specification `*` means to rewrite with all hypotheses  -/
Lean.Parser.Tactic.simpStar : Lean.ParserDescr
-- Init.Data.Float.Float32
/-- Raises one floating-point number to the power of another. Typically used via the `^` operator.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`powf`.
 -/
Float32.pow : Float32 → Float32 → Float32
-- Lean.MonadEnv
Lean.getConstInfoDefn : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → m Lean.DefinitionVal
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivWithinAt.mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c d : 𝕜 → 𝔸} {c' d' : 𝔸},
  HasDerivWithinAt c c' s x → HasDerivWithinAt d d' s x → HasDerivWithinAt (c * d) (c' * d x + c x * d') s x
-- Mathlib.Geometry.Convex.Cone.Pointed
/-- Every pointed cone is a convex cone.  -/
PointedCone.toConvexCone : {R : Type u_1} →
  {E : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] → [inst_4 : Module R E] → PointedCone R E → ConvexCone R E
-- Std.Time.Zoned.TimeZone
/-- Creates a `Timestamp` from a `WallTime` and a timezone `offset`. Assumes the `WallTime` represents
civil time at the given offset: `UTC = wall − offset`.
 -/
Std.Time.Timestamp.ofWallTime : Std.Time.WallTime → Std.Time.TimeZone.Offset → Std.Time.Timestamp
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.whiskering_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {x : B} (h : x ⟶ c)
  (t : CategoryTheory.Bicategory.LeftLift f g), (CategoryTheory.Bicategory.LeftLift.whiskering h).obj t = t.whisker h
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.Parser.Text.parseClause.litWs : Std.Internal.Parsec.ByteArray.Parser ℤ