mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Given a function `f : ι → M` and a nonempty finite set `t ⊆ ι`, we can always find `i ∈ t` such that
`‖∏ j in t, f j‖ ≤ ‖f i‖`.
 -/
IsUltrametricDist.exists_norm_finsetProd_le_of_nonempty : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] {t : Finset ι},
  t.Nonempty → ∀ (f : ι → M), ∃ i ∈ t, ‖∏ j ∈ t, f j‖ ≤ ‖f i‖
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.strLitNoAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsStrictMinor.lt : ∀ {α : Type u_1} {M N : Matroid α}, N <m M → N < M
-- Mathlib.Analysis.InnerProductSpace.PiL2
DirectSum.IsInternal.subordinateOrthonormalBasis_def : ∀ {ι : Type u_7} {𝕜 : Type u_8} [inst : RCLike 𝕜] {E : Type u_9} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : FiniteDimensional 𝕜 E] {n : ℕ}
  (hn : Module.finrank 𝕜 E = n) [inst_5 : DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V)
  (hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ),
  DirectSum.IsInternal.subordinateOrthonormalBasis hn hV hV' =
    (DirectSum.IsInternal.collectedOrthonormalBasis hV' hV fun i => stdOrthonormalBasis 𝕜 ↥(V i)).reindex
      (DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv hn hV hV')
-- Mathlib.Topology.Bornology.Constructions
Bornology.IsBounded.pi : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → Bornology (X i)] {S : (i : ι) → Set (X i)},
  (∀ (i : ι), Bornology.IsBounded (S i)) → Bornology.IsBounded (Set.univ.pi S)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.tensorObj.one_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.MonObj M]
  [inst_4 : CategoryTheory.MonObj N],
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)
-- Mathlib.Algebra.Group.End
MulAut.inv_symm : ∀ (M : Type u_2) [inst : Mul M] (e : MulAut M), MulEquiv.symm e⁻¹ = e
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Lean.Nat.fromExpr? : Lean.Expr → Lean.Meta.SimpM (Option ℕ)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf.eq_1 : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) (t : ℝ),
  ProbabilityTheory.mgf X μ t = ∫ (x : Ω), (fun ω => Real.exp (t * X ω)) x ∂μ
-- Lean.LoadDynlib
_private.Lean.LoadDynlib.0.Lean.loadPlugin.unsafe_impl_5 : Lean.Dynlib → BaseIO Lean.Dynlib
-- Mathlib.Data.Nat.Log
Nat.clog_of_two_le : ∀ {b n : ℕ}, 1 < b → 2 ≤ n → Nat.clog b n = Nat.clog b ((n + b - 1) / b) + 1
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.completion_def : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  (f : NormedAddGroupHom G H) (x : UniformSpace.Completion G), f.completion x = UniformSpace.Completion.map (⇑f) x
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_iff_norm_sub_tendsto_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] {f : α → E} {a : Filter α} {b : E},
  Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun e => ‖f e - b‖) a (nhds 0)
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.equivalence_inverse : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  ContinuousGeneratedByCat.equivalence.inverse = ContinuousGeneratedByCat.toGeneratedByTopCat
-- Init.Data.List.Nat.Sublist
List.suffix_iff_getElem? : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁ <:+ l₂ ↔ l₁.length ≤ l₂.length ∧ ∀ (i : ℕ) (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i]
-- Mathlib.Algebra.Ring.CentroidHom
instCoeTCCentroidHomOfCentroidHomClass : {F : Type u_1} →
  {α : Type u_5} →
    [inst : NonUnitalNonAssocSemiring α] → [inst_1 : FunLike F α α] → [CentroidHomClass F α] → CoeTC F (CentroidHom α)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.ext_iff : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : Zero V] [inst_2 : SMul R V]
  {x y : HahnModule Γ R V}, x = y ↔ ((HahnModule.of R).symm x).coeff = ((HahnModule.of R).symm y).coeff
-- Mathlib.Analysis.Complex.Poisson
/-- Companion theorem to the Poisson Integral Formula: Upper estimate for the real part of the
Herglotz-Riesz kernel.
 -/
re_herglotzRieszKernel_le : ∀ {R : ℝ} {w c z : ℂ},
  z ∈ Metric.sphere c R →
    w ∈ Metric.ball c R → ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (R + ‖w - c‖) / (R - ‖w - c‖)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_sigma : ∀ {α : Type u_1} {β : α → Type u_4} (f : (a : α) → β a → ENNReal),
  ∑' (p : (a : α) × β a), f p.fst p.snd = ∑' (a : α) (b : β a), f a b
-- Mathlib.Logic.Encodable.Basic
Int.encodable : Encodable ℤ
-- Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_snd_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃)
  (α : CategoryTheory.Arrow.mk sq₁₂.ι ⟶ CategoryTheory.Arrow.mk f₃) {Z : C₂} (h : (G.obj (Opposite.op Y₁)).obj Y₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α))
      (CategoryTheory.CategoryStruct.comp sq₁₃.snd h) =
    CategoryTheory.CategoryStruct.comp (adj₂.homEquiv (CategoryTheory.Arrow.Hom.right α)) h
-- Mathlib.RingTheory.ChainOfDivisors
DivisorChain.element_of_chain_not_isUnit_of_index_ne_zero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {n : ℕ} {i : Fin (n + 1)},
  i ≠ 0 → ∀ {c : Fin (n + 1) → Associates M}, StrictMono c → ¬IsUnit (c i)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.Eqv.of_smul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (r : R) (m : M) (n : N),
  TensorProduct.Eqv R M N (FreeAddMonoid.of (r • m, n)) (FreeAddMonoid.of (m, r • n))
-- Lean.Meta.DecLevel
Lean.Meta.decLevel? : Lean.Level → Lean.MetaM (Option Lean.Level)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.Sign.pos : Tactic.ComputeAsymptotics.UnitMonomial.Sign
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If we have `IsFiltered C`, then for any functor `F : J ⥤ C` with `FinCategory J`,
there exists a cocone over `F`.
 -/
CategoryTheory.IsFiltered.cocone_nonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] {J : Type w}
  [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C),
  Nonempty (CategoryTheory.Limits.Cocone F)
-- Lean.Meta.Tactic.Split
/-- Split works best if all discriminants are already free variables. If they are not, it will generalize
them, but that may fail if the motive is dependent. So to avoid that, we first generalize all
non-FVar discriminants that are propositions; because of proof irrelevance, that's much simpler.
 -/
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.Split.generalizeMatchPropDiscrs : Lean.MVarId → Array Lean.Expr → Lean.MetaM (Array Lean.Expr × Lean.MVarId)
-- Mathlib.Order.Hom.Basic
denselyOrdered_iff_of_orderIsoClass : ∀ {X : Type u_6} {Y : Type u_7} {F : Type u_8} [inst : Preorder X] [inst_1 : Preorder Y] [inst_2 : EquivLike F X Y]
  [OrderIsoClass F X Y] (f : F), DenselyOrdered X ↔ DenselyOrdered Y
-- Mathlib.CategoryTheory.Subobject.Basic
/-- An equality of subobjects gives an isomorphism of the corresponding objects.  -/
CategoryTheory.Subobject.isoOfMkEqMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B A₁ A₂ : C} →
      (f : A₁ ⟶ B) →
        (g : A₂ ⟶ B) →
          [inst_1 : CategoryTheory.Mono f] →
            [inst_2 : CategoryTheory.Mono g] → CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk g → (A₁ ≅ A₂)
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
tendsto_log_mul_self_nhdsLT_zero : Filter.Tendsto (fun x => Real.log x * x) (nhdsWithin 0 (Set.Iio 0)) (nhds 0)
-- Init.Data.Iterators.Basic
Std.Iter.toIterM_mk : ∀ {α β : Type u_1} {it : α}, { internalState := it }.toIterM = { internalState := it }
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- Equivalent characterizations for equicontinuity of a family of continuous linear maps
between normed spaces. See also `WithSeminorms.equicontinuous_TFAE` for similar characterizations
between spaces satisfying `WithSeminorms`.  -/
NormedSpace.equicontinuous_TFAE : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} {ι : Type u_9} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂]
  [inst_3 : SeminormedAddCommGroup E] [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 E]
  [inst_6 : NormedSpace 𝕜₂ F] (f : ι → E →SL[σ₁₂] F),
  [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f),
      ∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖, ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖,
      ∃ C, ∀ (i : ι), ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (Set.range fun x => ‖f x‖),
      ⨆ i, ↑‖f i‖₊ < ⊤].TFAE
-- Mathlib.Algebra.Category.ModuleCat.Subobject
ModuleCat.toKernelSubobject_arrow : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} {f : M ⟶ N} (x : ↥(ModuleCat.Hom.hom f).ker),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject f).arrow)
      (ModuleCat.toKernelSubobject x) =
    ↑x
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_smul : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) {S : Type u_10}
  [inst_5 : Monoid S] [inst_6 : DistribMulAction S N] [inst_7 : SMulCommClass R S N] (c : S), ↑(c • f) = c • ↑f
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- A nonzero element in a domain integral over a field is a unit.  -/
IsIntegral.isUnit : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : Ring S] [IsDomain S] [inst_3 : Algebra R S] {x : S},
  IsIntegral R x → x ≠ 0 → IsUnit x
-- Mathlib.CategoryTheory.Monoidal.Limits.Colimits
/-- The tensor product of two cocones.  -/
CategoryTheory.Limits.Cocone.tensor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {J : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} J] →
          {F₁ F₂ : CategoryTheory.Functor J C} →
            CategoryTheory.Limits.Cocone F₁ →
              CategoryTheory.Limits.Cocone F₂ →
                CategoryTheory.Limits.Cocone (CategoryTheory.MonoidalCategoryStruct.tensorObj F₁ F₂)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo.α : Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo → Lean.Expr
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_last_comp_δ_last_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) (n : ℕ) {Z : C} (h : Y.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.h (Fin.last n))
      (CategoryTheory.CategoryStruct.comp (Y.δ (Fin.last (n + 1))) h) =
    CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n })) h
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `veblenWith f o` is always normal whenever `f` is. See `isNormal_veblenWith'` for a version
which does not assume `IsNormal f`.  -/
Ordinal.isNormal_veblenWith : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → ∀ (o : Ordinal.{u}), Order.IsNormal (Ordinal.veblenWith f o)
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.eq_top_iff' : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p : Submodule R M}, p = ⊤ ↔ ∀ (x : M), x ∈ p
-- Lean.Parser.Command
Lean.Parser.Command.example.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.triangleOpEquivalence_unitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ],
  (CategoryTheory.Pretriangulated.triangleOpEquivalence C).unitIso =
    CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso C
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Arrow.hasLimits : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [CategoryTheory.Limits.HasLimits T],
  CategoryTheory.Limits.HasLimits (CategoryTheory.Arrow T)
-- Init.Data.Array.Basic
/-- Pads `xs : Array α` on the right with repeated occurrences of `a : α` until it is of length `n`. If
`l` already has at least `n` elements, it is returned unmodified.

Examples:
 * `#[1, 2, 3].rightpad 5 0 = #[1, 2, 3, 0, 0]`
 * `#["red", "green", "blue"].rightpad 4 "blank" = #["red", "green", "blue", "blank"]`
 * `#["red", "green", "blue"].rightpad 3 "blank" = #["red", "green", "blue"]`
 * `#["red", "green", "blue"].rightpad 1 "blank" = #["red", "green", "blue"]`
 -/
Array.rightpad : {α : Type u} → ℕ → α → Array α → Array α
-- Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Complex.measurableEquivRealProd_apply : ∀ (a : ℂ), Complex.measurableEquivRealProd a = (a.re, a.im)
-- Mathlib.Algebra.Order.Kleene
Pi.instIdemCommSemiringForall : {ι : Type u_3} → {π : ι → Type u_4} → [(i : ι) → IdemCommSemiring (π i)] → IdemCommSemiring ((i : ι) → π i)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddCommMagma.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddCommMagma M] [inst_2 : ContinuousAdd M],
  SeparationQuotient.instAddCommMagma = { toAdd := SeparationQuotient.instAdd, add_comm := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.unmopEquiv_unitIso_hom_app_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Cᴹᵒᵖ),
  ((CategoryTheory.MonoidalOpposite.unmopEquiv C).unitIso.hom.app X).unmop = CategoryTheory.CategoryStruct.id X.unmop
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.instSliceableRiiSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.instSliceableRiiSlice._auto_1) →
      Std.Rii.Sliceable (Std.DTreeMap α β cmp) α (Std.DTreeMap.Internal.RiiSlice α β)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (n d : aig.RefVec w)
  (wn wr : ℕ) (q r : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr n d wn wr q r =
    match curr with
    | 0 => { aig := aig, q := q, r := r, hle := ⋯ }
    | curr.succ =>
      let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r;
      let aig_1 := res.aig;
      let wn_1 := res.wn;
      let wr_1 := res.wr;
      let q_1 := res.q;
      let r_1 := res.r;
      have this := ⋯;
      let n_1 := n.cast this;
      let d_1 := d.cast this;
      let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig_1 curr n_1 d_1 wn_1 wr_1 q_1 r_1;
      let aig_2 := res.aig;
      have q_2 := res.q;
      have r_2 := res.r;
      have this := ⋯;
      { aig := aig_2, q := q_2, r := r_2, hle := this }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- The semantics for `BVBinOp`.
 -/
Std.Tactic.BVDecide.BVBinOp.eval : {w : ℕ} → Std.Tactic.BVDecide.BVBinOp → BitVec w → BitVec w → BitVec w
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
/-- Given a colimit cocone for a presheaf of rings `R` on a cofiltered category `C`,
`M` a presheaf of modules over `R`, and a colimit cocone `cM` for the underlying
functor `Cᵒᵖ ⥤ AddCommGrpCat` of `M`, this is the type `cM.pt` on which we define
a module structure below.  -/
PresheafOfModules.ModuleColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {cR : CategoryTheory.Limits.Cocone R} →
        {M : PresheafOfModules R} →
          {cM : CategoryTheory.Limits.Cocone M.presheaf} →
            CategoryTheory.Limits.IsColimit cR → CategoryTheory.Limits.IsColimit cM → Type w
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.exists_equivalence_iff_of_locallySmall : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.LocallySmall.{w', v_1, u_1} C],
  (∃ J x, Nonempty (C ≌ J)) ↔ CategoryTheory.ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤
-- Std.Data.HashMap.Lemmas
_private.Std.Data.HashMap.Lemmas.0.GetElem?.match_1.eq_1 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (e : elem) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match some e with
    | some e => h_1 e
    | none => h_2 ()) =
    h_1 e
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- Given an open cover `{ Xᵢ }` of `X` and an open cover `{ Yⱼ }` of `Y`, then
`X ×[Z] Y` is covered by `Xᵢ ×[Z] Yⱼ`.  -/
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight : {X Y Z : AlgebraicGeometry.Scheme} →
  X.OpenCover → Y.OpenCover → (f : X ⟶ Z) → (g : Y ⟶ Z) → (CategoryTheory.Limits.pullback f g).OpenCover
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.FG.map_of_surjective : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : Type u_2} [inst_1 : L.Structure N],
  FirstOrder.Language.Structure.FG L M →
    ∀ (f : L.Hom M N), Function.Surjective ⇑f → FirstOrder.Language.Structure.FG L N
-- Mathlib.Order.Booleanisation
/-- The infimum on `Booleanisation α` is as follows: For `a b : α`,
* `a ⊓ b` is `a ⊓ b`
* `a ⊓ bᶜ` is `a \ b`
* `aᶜ ⊓ b` is `b \ a`
* `aᶜ ⊓ bᶜ` is `(a ⊔ b)ᶜ`  -/
Booleanisation.instInf : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → Min (Booleanisation α)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.instIsIsoGrpHom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.CommGrp C} {f : G ⟶ H} [CategoryTheory.IsIso f],
  CategoryTheory.IsIso f.hom
-- Mathlib.Algebra.Group.Prod
MonoidHom.prod.eq_1 : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : M →* N) (g : M →* P), f.prod g = { toFun := Function.prod ⇑f ⇑g, map_one' := ⋯, map_mul' := ⋯ }
-- Init.Data.Order.Lemmas
Std.instAsymmLtOfLawfulOrderLT : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [Std.LawfulOrderLT α], Std.Asymm fun x1 x2 => x1 < x2
-- Std.Internal.Parsec.Basic
/-- Checks if the next input element matches some condition.
 -/
Std.Internal.Parsec.satisfy : {ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] → [Std.Internal.Parsec.Input ι elem idx] → (elem → Bool) → Std.Internal.Parsec ι elem
-- LeanSearchClient.Basic
statesearch.revision : Lean.Option String
-- Mathlib.Analysis.RCLike.Basic
RCLike.lipschitzWith_ofReal : ∀ {K : Type u_1} [inst : RCLike K], LipschitzWith 1 RCLike.ofReal
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.generateFrom_memPartition_le_succ : ∀ {α : Type u_1} (t : ℕ → Set α) (n : ℕ),
  MeasurableSpace.generateFrom (memPartition t n) ≤ MeasurableSpace.generateFrom (memPartition t (n + 1))
-- Lean.Language.Basic
Lean.Language.DynamicSnapshot.mk.inj : ∀ {val : Dynamic} {toSnapshotTreeM : Lean.Language.ToSnapshotTreeM Lean.Language.SnapshotTree} {val_1 : Dynamic}
  {toSnapshotTreeM_1 : Lean.Language.ToSnapshotTreeM Lean.Language.SnapshotTree},
  { val := val, toSnapshotTreeM := toSnapshotTreeM } = { val := val_1, toSnapshotTreeM := toSnapshotTreeM_1 } →
    val = val_1 ∧ toSnapshotTreeM = toSnapshotTreeM_1
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
hasLineDerivWithinAt_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {f' : F}
  {x v : E}, HasLineDerivWithinAt 𝕜 f f' Set.univ x v ↔ HasLineDerivAt 𝕜 f f' x v
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContinuousLinearMap.contMDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_6} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  (L : E →L[𝕜] F) {s : Set E}, ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n (⇑L) s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.fromAffine_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [inst_1 : Nontrivial R] {X Y : R}
  (h : W'.toAffine.Nonsingular X Y),
  WeierstrassCurve.Projective.Point.fromAffine (WeierstrassCurve.Affine.Point.some X Y h) =
    { point := ⟦![X, Y, 1]⟧, nonsingular := ⋯ }
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : β → β} {h : k ∈ m.modify k f}, (m.modify k f)[k] = f m[k]
-- Init.Data.List.Lemmas
List.foldlRecOn_nil : ∀ {β : Type u_1} {α : Type u_2} {b : β} {motive : β → Sort u_3} {op : β → α → β} (hb : motive b)
  (hl : (b : β) → motive b → (a : α) → a ∈ [] → motive (op b a)), List.foldlRecOn [] op hb hl = hb
-- Mathlib.Data.Sym.Card
/-- The multisets of size `k` over `Fin n+2` not containing `0`
are equivalent to those of size `k` over `Fin n+1`,
as demonstrated by respectively decrementing or incrementing every element of the multiset.
 -/
Sym.e2 : {n k : ℕ} → { s // 0 ∉ s } ≃ Sym (Fin n.succ) k
-- Mathlib.NumberTheory.FLT.Polynomial
_private.Mathlib.NumberTheory.FLT.Polynomial.0.Polynomial.flt_catalan_aux : ∀ {k : Type u_1} [inst : Field k] {p q r : ℕ} {a b c : Polynomial k} {u v w : k},
  Polynomial.C u * a ^ p + Polynomial.C v * b ^ q + Polynomial.C w * c ^ r = 0 →
    p ≠ 0 →
      q ≠ 0 →
        r ≠ 0 →
          q * r + r * p + p * q ≤ p * q * r →
            ↑p ≠ 0 → ↑q ≠ 0 → ↑r ≠ 0 → a ≠ 0 → b ≠ 0 → c ≠ 0 → IsCoprime a b → u ≠ 0 → v ≠ 0 → w ≠ 0 → a.natDegree = 0
-- Aesop.RuleTac.ElabRuleTerm
Aesop.elabRuleTermForSimpCore : Lean.MVarId →
  Lean.Term →
    Lean.Meta.Simp.Context →
      Lean.Meta.Simp.SimprocsArray → Bool → Lean.Elab.TermElabM (Lean.Meta.Simp.Context × Lean.Meta.Simp.SimprocsArray)
-- Mathlib.Order.Circular
Set.mem_cIoo : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b x : α}, x ∈ Set.cIoo a b ↔ sbtw a x b
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic.0.Tactic.ComputeAsymptotics.MultiseriesExpansion.const.match_1.eq_1 : ∀ (motive : Tactic.ComputeAsymptotics.Basis → Sort u_1) (h_1 : Unit → motive [])
  (h_2 : (basis_hd : ℝ → ℝ) → (basis_tl : List (ℝ → ℝ)) → motive (basis_hd :: basis_tl)),
  (match [] with
    | [] => h_1 ()
    | basis_hd :: basis_tl => h_2 basis_hd basis_tl) =
    h_1 ()
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_4} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R},
  TensorProduct.lift (LinearMap.lsmul R M ∘ₗ (LinearMap.mul R R) r) =
    (LinearMap.lsmul R M) r ∘ₗ TensorProduct.lift (LinearMap.lsmul R M)
-- Aesop.Forward.State
Aesop.instInhabitedRawHyp.default : Aesop.RawHyp