mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.FunctorHom
/-- Given functors `F G : C ⥤ D`, `HomObj F G A` is a proxy for the type
of "morphisms" `F ⊗ A ⟶ G`, where `A : C ⥤ Type w` (`w` an arbitrary universe).  -/
CategoryTheory.Functor.HomObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.Functor C D → CategoryTheory.Functor C (Type w) → Type (max (max u v') w)
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.not_of_unit_left : ∀ {α : Type u_1} [inst : Monoid α] (a : α) (u : αˣ), ¬FiniteMultiplicity (↑u) a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.nonsingular_add : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Nonsingular P → W.Nonsingular Q → W.Nonsingular (W.add P Q)
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.ext : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A B : ↥(Matrix.unitaryGroup n α)), (∀ (i j : n), ↑A i j = ↑B i j) → A = B
-- Init.Data.SInt.Lemmas
Int64.toInt_ofInt_of_le : ∀ {n : ℤ}, -2 ^ 63 ≤ n → n < 2 ^ 63 → (Int64.ofInt n).toInt = n
-- Mathlib.Combinatorics.Hindman
Hindman.exists_idempotent_ultrafilter_le_FP : ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M), ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ Hindman.FP a
-- Mathlib.Order.Defs.Unbundled
/-- `Std.Refl` as a definition, suitable for use in proofs.  -/
Reflexive : {α : Sort u_1} → (α → α → Prop) → Prop
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.moment_zero_measure : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {p : ℕ}, ProbabilityTheory.moment X p 0 = 0
-- Mathlib.Topology.UniformSpace.Equiv
/-- Composition of two uniform isomorphisms.  -/
UniformEquiv.trans : {α : Type u} →
  {β : Type u_1} →
    {γ : Type u_2} →
      [inst : UniformSpace α] → [inst_1 : UniformSpace β] → [inst_2 : UniformSpace γ] → α ≃ᵤ β → β ≃ᵤ γ → α ≃ᵤ γ
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOn.curry_right : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {x : E} {s : Set (E × F)},
  AnalyticOn 𝕜 f s → AnalyticOn 𝕜 (fun y => f (x, y)) {y | (x, y) ∈ s}
-- Mathlib.Algebra.RingQuot
RingQuot.ringQuotToIdealQuotient.eq_1 : ∀ {B : Type uR} [inst : CommRing B] (r : B → B → Prop),
  RingQuot.ringQuotToIdealQuotient r = RingQuot.lift ⟨Ideal.Quotient.mk (Ideal.ofRel r), ⋯⟩
-- Lean.SubExpr
Lean.SubExpr.GoalsLocation.mk.sizeOf_spec : ∀ (mvarId : Lean.MVarId) (loc : Lean.SubExpr.GoalLocation),
  sizeOf { mvarId := mvarId, loc := loc } = 1 + sizeOf mvarId + sizeOf loc
-- Mathlib.NumberTheory.SelbergSieve
/-- The main sum we get from Λ² coefficients can be written as a diagonalized quadratic form with
eigenvalues given by `1/selbergTerms`  -/
BoundingSieve.mainSum_lambdaSquared_eq_sum_mul_sum_sq : ∀ {s : BoundingSieve} (w : ℕ → ℝ),
  BoundingSieve.mainSum (BoundingSieve.lambdaSquared w) =
    ∑ l ∈ s.prodPrimes.divisors,
      (BoundingSieve.selbergTerms l)⁻¹ * (∑ d ∈ s.prodPrimes.divisors, if l ∣ d then s.nu d * w d else 0) ^ 2
-- Mathlib.Order.Sublattice
Sublattice.coe_iInf : ∀ {ι : Sort u_1} {α : Type u_2} [inst : Lattice α] (f : ι → Sublattice α), ↑(⨅ i, f i) = ⋂ i, ↑(f i)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.Simps.symm_apply.eq_1 : ∀ (G : Type u) [inst : TopologicalSpace G] (H : Type v) [inst_1 : TopologicalSpace H] [inst_2 : Mul G] [inst_3 : Mul H]
  (e : G ≃ₜ* H), ContinuousMulEquiv.Simps.symm_apply G H e = ⇑e.symm
-- Mathlib.Order.Partition.Finpartition
/-- **Alias** of the reverse direction of `Finpartition.mem_part_self`. -/
Finpartition.mem_part : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α}, a ∈ s → a ∈ P.part a
-- Mathlib.Data.Finset.Card
/-- a variant of `Finset.exists_ne_map_eq_of_card_image_lt` using `Set.InjOn`  -/
Finset.not_injOn_of_card_image_lt : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} [inst : DecidableEq β] {f : α → β},
  (Finset.image f s).card < s.card → ¬Set.InjOn f ↑s
-- Init.Data.Vector.Algebra
Vector.instAddCommGroup : {α : Type u_1} → {n : ℕ} → [Lean.Grind.AddCommGroup α] → Lean.Grind.AddCommGroup (Vector α n)
-- Mathlib.Order.Interval.Set.Image
Antitone.image_Ici_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  Antitone f → f '' Set.Ici a ⊆ Set.Iic (f a)
-- Mathlib.Algebra.Homology.Additive
/-- Turning an object into a complex supported at `j` then applying a functor is
the same as applying the functor then forming the complex.
 -/
HomologicalComplex.singleMapHomologicalComplex : {ι : Type u_1} →
  {W₁ : Type u_3} →
    {W₂ : Type u_4} →
      [inst : CategoryTheory.Category.{v_2, u_3} W₁] →
        [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] →
              [inst_4 : CategoryTheory.Limits.HasZeroObject W₁] →
                [inst_5 : CategoryTheory.Limits.HasZeroObject W₂] →
                  (F : CategoryTheory.Functor W₁ W₂) →
                    [inst_6 : F.PreservesZeroMorphisms] →
                      (c : ComplexShape ι) →
                        [inst_7 : DecidableEq ι] →
                          (j : ι) →
                            (HomologicalComplex.single W₁ c j).comp (F.mapHomologicalComplex c) ≅
                              F.comp (HomologicalComplex.single W₂ c j)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.structureMapCLM_zero_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {f : ContDiffMapSupportedIn E F n K}
  {x : E}, ((ContDiffMapSupportedIn.structureMapCLM 𝕜 n 0) f) x = ContinuousMultilinearMap.uncurry0 ℝ E (f x)
-- Mathlib.Topology.Inseparable
SeparationQuotient.comap_mk_nhdsSet_image : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  Filter.comap SeparationQuotient.mk (nhdsSet (SeparationQuotient.mk '' s)) = nhdsSet s
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.Finitary.sum' : ∀ {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α}, (∀ (i : ι), (M i).Finitary) → (Matroid.sum' M).Finitary
-- Mathlib.Algebra.BigOperators.Ring.Finset
/-- The product of `f i - g i` over all of `s` is the sum over the powerset of `s` of the product of
`g` over a subset `t` times the product of `f` over the complement of `t` times `(-1) ^ #t`.  -/
Finset.prod_sub : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommRing R] [inst_1 : DecidableEq ι] (f g : ι → R) (s : Finset ι),
  ∏ i ∈ s, (f i - g i) = ∑ t ∈ s.powerset, ((-1) ^ t.card * ∏ i ∈ s \ t, f i) * ∏ i ∈ t, g i
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.sub_le_sub_iff_left_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a b c : α}, a ≠ ⊤ → (b - a ≤ c - a ↔ b ≤ c)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- **Alias** of `SimpleGraph.Walk.darts_takeUntil_subset_darts`. -/
SimpleGraph.Walk.darts_takeUntil_subset : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.takeUntil u h).darts ⊆ p.darts
-- Aesop.Tree.Data
Aesop.TreeSpec.introRapp : (self : Aesop.TreeSpec) → Aesop.RappData self.Goal self.MVarCluster → self.Rapp
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.hasForgetToMonCat : CategoryTheory.HasForget₂ CommMonCat MonCat
-- Mathlib.Analysis.InnerProductSpace.OfNorm
InnerProductSpaceable.mk : ∀ {E : Type u_2} [inst : NormedAddCommGroup E],
  (∀ (x y : E), ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) → InnerProductSpaceable E
-- Lean.Elab.Tactic.Omega.Core
/-- We deal with a hard equality by introducing a new easy equality.

After solving the easy equality,
the minimum lexicographic value of `(c.minNatAbs, c.maxNatAbs)` will have been reduced.
 -/
Lean.Elab.Tactic.Omega.Problem.dealWithHardEquality : Lean.Elab.Tactic.Omega.Problem → Lean.Omega.Coeffs → Lean.Elab.Tactic.Omega.OmegaM Lean.Elab.Tactic.Omega.Problem
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y},
  e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.assignmentsInvariant_insertRupUnits_of_assignmentsInvariant : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRupAdd →
    ∀ (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
      (f.insertRupUnits units).1.AssignmentsInvariant
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Pos.Raw.offsetOfPosAux.eq_def : ∀ (s : String) (pos i : String.Pos.Raw) (offset : ℕ),
  String.Pos.Raw.offsetOfPosAux s pos i offset =
    if i ≥ pos then offset
    else
      if h : String.Pos.Raw.atEnd s i = true then offset
      else
        have this := ⋯;
        String.Pos.Raw.offsetOfPosAux s pos (String.Pos.Raw.next s i) (offset + 1)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue?_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] {f : α → β → γ} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      Std.Internal.List.getKey? k l = some k' →
        Std.Internal.List.getValue? k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) =
          Option.map (f k') (Std.Internal.List.getValue? k l)
-- Init.Data.Iterators.Basic
/-- Asserts that an iterator `it'` could plausibly produce `it'` as a successor iterator after
finitely many steps. This relation is reflexive.
 -/
Std.IterM.IsPlausibleIndirectSuccessorOf : {α β : Type w} → {m : Type w → Type w'} → [Std.Iterator α m β] → Std.IterM m β → Std.IterM m β → Prop
-- Mathlib.Data.Finset.Union
/-- Rewrite a `biUnion` over `s.attach` as a `biUnion` over `s` by extending the function to all of
`α` with `∅` outside `s`. See `Finset.attach_biUnion` for the version when the indexing function is
already defined on all of `α`.  -/
Finset.attach_biUnion' : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} [inst : DecidableEq β] [inst_1 : DecidableEq α] {f : ↥s → Finset β},
  s.attach.biUnion f = s.biUnion fun a => if h : a ∈ s then f ⟨a, h⟩ else ∅
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_eq_zero_of_lt_order : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ] {x : HahnSeries Γ R}
  {i : Γ}, i < x.order → x.coeff i = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- If `f` and `g` are isomorphic arrows, then a mono factorisation of `f` that is an image
gives a mono factorisation of `g` that is an image  -/
CategoryTheory.Limits.IsImage.ofArrowIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      {F : CategoryTheory.Limits.MonoFactorisation f.hom} →
        CategoryTheory.Limits.IsImage F →
          (sq : f ⟶ g) → [inst_1 : CategoryTheory.IsIso sq] → CategoryTheory.Limits.IsImage (F.ofArrowIso sq)
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.isSatisfiable_of_isSatisfiable_onTheory : ∀ {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} (φ : L →ᴸ L'),
  (φ.onTheory T).IsSatisfiable → T.IsSatisfiable
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.ProdPreservesConnectedLimits.γ₁_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : Type v₂} [inst_2 : CategoryTheory.SmallCategory J] {K : CategoryTheory.Functor J C} (X : C) (x : J),
  (CategoryTheory.ProdPreservesConnectedLimits.γ₁ X).app x = CategoryTheory.Limits.prod.fst
-- Init.Data.UInt.Lemmas
USize.toUInt32_sub : ∀ (a b : USize), (a - b).toUInt32 = a.toUInt32 - b.toUInt32
-- Aesop.Tree.RunMetaM
Aesop.Rapp.runMetaMModifying : {m : Type → Type u_1} →
  [Monad m] → [MonadLiftT Lean.MetaM m] → [MonadFinally m] → {α : Type} → m α → Aesop.Rapp → m (α × Aesop.Rapp)
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.card_le_of_le : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [Finite ↥K], H ≤ K → Nat.card ↥H ≤ Nat.card ↥K
-- Mathlib.Algebra.Group.Subgroup.Order
/-- An additive subgroup of an additive ordered group is an additive ordered group.  -/
AddSubgroup.toIsOrderedAddMonoid : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : Preorder G] [IsOrderedAddMonoid G] (H : AddSubgroup G),
  IsOrderedAddMonoid ↥H
-- Mathlib.Order.Partition.Finpartition
/-- Restrict a partition of `a` to `b` where `b ≤ a` by intersecting each part with `b`.  -/
Finpartition.restrict : {α : Type u_1} →
  [inst : DistribLattice α] →
    [inst_1 : OrderBot α] → [DecidableEq α] → {a b : α} → Finpartition a → b ≤ a → Finpartition b
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.atTop.isCountablyGenerated : ∀ {α : Type u_1} [inst : Preorder α] [Countable α], Filter.atTop.IsCountablyGenerated
-- Mathlib.RingTheory.MvPowerSeries.Equiv
_private.Mathlib.RingTheory.MvPowerSeries.Equiv.0.MvPowerSeries.coeff_optionInvFunLeft : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (p : PowerSeries (MvPowerSeries σ R)) (x : Option σ →₀ ℕ),
  (MvPowerSeries.coeff x) (MvPowerSeries.optionInvFunLeft✝ σ R p) =
    (MvPowerSeries.coeff x.some) ((PowerSeries.coeff (x none)) p)
-- Mathlib.Algebra.Module.Submodule.LinearMap
Submodule.coe_subtype : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M),
  ⇑p.subtype = Subtype.val
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.toSheafify_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  (X : Cᵒᵖ) (x : ↑(M₀.obj X)),
  (ModuleCat.Hom.hom ((PresheafOfModules.toSheafify α φ).app X)) x = (CategoryTheory.ConcreteCategory.hom (φ.app X)) x
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.zero_cpow : ∀ {x : ℂ}, x ≠ 0 → 0 ^ x = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f)[k]? = f t[k]?
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.match_1.eq_1 : ∀ (s : String) (motive : Char → Option (s.Pos × ℕ) → Sort u_1) (q : s.Pos) (v : ℕ)
  (h_1 : (q_1 : s.Pos) → (v_1 : ℕ) → some (q, v) = some (q_1, v_1) → motive 'U' (some (q_1, v_1)))
  (h_2 : (x : Char) → (x_1 : Option (s.Pos × ℕ)) → some (q, v) = x_1 → motive x x_1),
  (match 'U', h₃ : some (q, v) with
    | 'U', some (q_1, v_1) => h_1 q_1 v_1 h₃
    | x, x_1 => h_2 x x_1 h₃) =
    h_1 q v ⋯
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCallHierarchyPrepareParams.toJson : Lean.Lsp.CallHierarchyPrepareParams → Lean.Json
-- Lean.Meta.CollectMVars
/-- Collect unassigned metavariables occurring in the given expression.

Remark: if `e` contains `?m` and there is a `t` assigned to `?m`, we
collect unassigned metavariables occurring in `t`.

Remark: if `e` contains `?m` and `?m` is delayed assigned to some term `t`,
we collect `?m` and unassigned metavariables occurring in `t`.
We collect `?m` because it has not been assigned yet.  -/
Lean.Meta.collectMVars : Lean.Expr → StateRefT' IO.RealWorld Lean.CollectMVars.State Lean.MetaM Unit
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {k l m : CategoryTheory.Limits.ColimitPresentation.Total P} (f : k.Hom l) (g : l.Hom m),
  (f.comp g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Given a cone `c : Cone K` and a map `f : X ⟶ F.obj c.X`, we can construct a cone of structured
arrows over `X` with `f` as the cone point.
 -/
CategoryTheory.Limits.Cone.toStructuredArrowCone : {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] →
            {K : CategoryTheory.Functor J C} →
              (c : CategoryTheory.Limits.Cone K) →
                (F : CategoryTheory.Functor C D) →
                  {X : D} →
                    (f : X ⟶ F.obj c.pt) →
                      CategoryTheory.Limits.Cone
                        ((F.mapCone c).toStructuredArrow.comp
                          ((CategoryTheory.StructuredArrow.map f).comp (CategoryTheory.StructuredArrow.pre X K F)))
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.toContinuousAffineEquiv_symm : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂),
  e.symm.toContinuousAffineEquiv = e.toContinuousAffineEquiv.symm
-- Mathlib.Analysis.Convex.Approximation
/-- The countable version of `sSup_affine_eq`.  -/
ConvexOn.sSup_of_countable_affine_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E],
  IsClosed s →
    LowerSemicontinuousOn φ s →
      ConvexOn ℝ s φ →
        ∃ 𝓕',
          𝓕'.Countable ∧
            sSup 𝓕' = s.domRestrict φ ∧
              ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑RCLike.re ∘ ⇑l) + Function.const (↑s) c
-- Lean.Declaration
Lean.InductiveType.type : Lean.InductiveType → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- If `sigma_comparison G f` is an isomorphism, then `G` preserves the colimit of `f`.  -/
CategoryTheory.Limits.PreservesCoproduct.of_iso_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [inst_2 : CategoryTheory.Limits.HasCoproduct f]
  [inst_3 : CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)]
  [i : CategoryTheory.IsIso (CategoryTheory.Limits.sigmaComparison G f)],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.sortDecls : Array Lean.IR.Decl → Array Lean.IR.Decl
-- Lean.DocString.Add
/-- Elaborates a Verso docstring for the specified declaration, which should already be present in the
environment.

`binders` should be the syntax of the parameters to the constant that is being documented, as a null
node that contains a sequence of bracketed binders. It is used to allow interactive features such as
document highlights and “find references” to work for documented parameters. If no parameter binders
are available, pass `Syntax.missing` or an empty null node.
 -/
Lean.versoDocString : Lean.Name → Lean.Syntax → Lean.TSyntax `Lean.Parser.Command.docComment → Lean.Elab.TermElabM Lean.VersoDocResult
-- Mathlib.Data.Nat.Upto
Nat.Upto.instLT : {p : ℕ → Prop} → LT (Nat.Upto p)
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.matches'.match_1.eq_6 : ∀ {α : Type u_1} (motive : RegularExpression α → Sort u_2) (P : RegularExpression α)
  (h_1 : Unit → motive RegularExpression.zero) (h_2 : Unit → motive RegularExpression.epsilon)
  (h_3 : (a : α) → motive (RegularExpression.char a)) (h_4 : (P Q : RegularExpression α) → motive (P.plus Q))
  (h_5 : (P Q : RegularExpression α) → motive (P.comp Q)) (h_6 : (P : RegularExpression α) → motive P.star),
  (match P.star with
    | RegularExpression.zero => h_1 ()
    | RegularExpression.epsilon => h_2 ()
    | RegularExpression.char a => h_3 a
    | P.plus Q => h_4 P Q
    | P.comp Q => h_5 P Q
    | P.star => h_6 P) =
    h_6 P
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.comp_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.OplaxTrans X Y)
  (θ : CategoryTheory.Lax.OplaxTrans Y Z) {a b : B} (f : a ⟶ b),
  (CategoryTheory.CategoryStruct.comp η θ).naturality f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (X.map f) (η.app b) (θ.app b)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) (θ.app b))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (Y.map f) (θ.app b)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f))
            (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (Z.map f)).inv)))
-- Mathlib.Algebra.Homology.SpectralObject.Basic
/-- The type of morphisms between spectral objects in abelian categories.  -/
CategoryTheory.Abelian.SpectralObject.Hom : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            CategoryTheory.Abelian.SpectralObject C ι → Type (max (max u_2 u_3) u_4)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.curryAlgEquiv_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (m : M) (n : N) (a : A),
  (AddMonoidAlgebra.curryAlgEquiv R) (AddMonoidAlgebra.single (m, n) a) =
    AddMonoidAlgebra.single m (AddMonoidAlgebra.single n a)
-- Mathlib.Analysis.RCLike.Extend
/-- **Alias** of `Module.Dual.extendRCLike_apply`. -/
LinearMap.extendTo𝕜_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : AddCommGroup F] [inst_2 : Module ℝ F] [inst_3 : Module 𝕜 F]
  [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F) (x : F),
  fr.extendRCLike x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_iff_exists_wbtw : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.WOppSide x y ↔ ∃ p ∈ s, Wbtw R x p y
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.Ordinal.instLEOfDay : LE Std.Time.Nanosecond.Ordinal.OfDay