mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.proj_of_le : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (L : FiniteGaloisIntermediateField k K)
  (g : ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop)
  (x : ↥L.toIntermediateField) (L' : FiniteGaloisIntermediateField k K) (h : L ≤ L'),
  ↑(((InfiniteGalois.proj L) g) x) = ↑(((InfiniteGalois.proj L') g) ⟨↑x, ⋯⟩)
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
/-- `log` is analytic away from nonpositive reals  -/
AnalyticAt.clog : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E},
  AnalyticAt ℂ f x → f x ∈ Complex.slitPlane → AnalyticAt ℂ (fun z => Complex.log (f z)) x
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.eq_one_of_unique : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} [inst_2 : Fintype X] [IsOrderedRing S]
  [Unique X] (s : ↑(stdSimplex S X)) (x : X), s x = 1
-- Mathlib.Topology.Order.ExtendFrom
eq_lim_at_right_extendFrom_uIoo : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [DenselyOrdered α]
  [OrderTopology α] [inst_4 : TopologicalSpace β] {f : α → β} {a b : α} {lb : β} [T2Space β],
  a ≠ b → Filter.Tendsto f (nhdsWithin b (Set.uIoo a b)) (nhds lb) → extendFrom (Set.uIoo a b) f b = lb
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedRefInfo.mk.injEq : ∀ (kind : WantedRefKind✝) (binderType : Lean.TSyntax `term) (isClass : Bool) (deps : Array WantedDep✝)
  (transparent : Option (Lean.TSyntax `term)) (kind_1 : WantedRefKind✝) (binderType_1 : Lean.TSyntax `term)
  (isClass_1 : Bool) (deps_1 : Array WantedDep✝) (transparent_1 : Option (Lean.TSyntax `term)),
  ({ kind := kind, binderType := binderType, isClass := isClass, deps := deps, transparent := transparent } =
      { kind := kind_1, binderType := binderType_1, isClass := isClass_1, deps := deps_1,
        transparent := transparent_1 }) =
    (kind = kind_1 ∧ binderType = binderType_1 ∧ isClass = isClass_1 ∧ deps = deps_1 ∧ transparent = transparent_1)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_of_equivalence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {J' : Type u''} [inst_2 : CategoryTheory.Category.{v'', u''} J']
  (e : J ≌ J'), P.IsClosedUnderColimitsOfShape J ↔ P.IsClosedUnderColimitsOfShape J'
-- Init.Data.Vector.Count
Vector.size_eq_countP_add_countP : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {xs : Vector α n},
  n = Vector.countP p xs + Vector.countP (fun a => decide ¬p a = true) xs
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeParams.mk : Option ℤ →
  Option Lean.Lsp.ClientInfo →
    Option String →
      Option Lean.Lsp.InitializationOptions →
        Lean.Lsp.ClientCapabilities →
          Lean.Lsp.Trace → Option (Array Lean.Lsp.WorkspaceFolder) → Lean.Lsp.InitializeParams
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.re_smul : ∀ {d : ℤ} (a : ℤ) (b : ℤ√d), (↑a * b).re = a * b.re
-- Mathlib.Data.Semiquot
Semiquot.mem_pure_self : ∀ {α : Type u_1} (a : α), a ∈ pure a
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.instIsExtensionInlProjr : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K),
  LieAlgebra.IsExtension (LieAlgebra.SemiDirectSum.inl ψ) (LieAlgebra.SemiDirectSum.projr ψ)
-- Mathlib.Data.FunLike.Group
FunLike.coeAddHom.eq_1 : ∀ (F : Type u_1) (α : Type u_2) (β : Type u_3) [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [inst_3 : IsAddApply F α β], FunLike.coeAddHom F α β = { toFun := fun f => ⇑f, map_add' := ⋯ }
-- Mathlib.LinearAlgebra.TensorProduct.Associator
LinearMap.rid_comp_lTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_5) {N : Type u_6} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : M →ₗ[R] R),
  ↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N f = TensorProduct.lift ((LinearMap.lsmul R N).flip.compl₂ f)
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff_target : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (M : Type w')
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] (X : C) {Y : C} [W.IsCompatibleWithShift M] {Y' : C}
  (f : Y ⟶ Y'),
  W f →
    (CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y ↔
      CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y')
-- Mathlib.Topology.Bornology.Constructions
Bornology.IsBounded.image_snd : ∀ {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst_1 : Bornology β] {s : Set (α × β)},
  Bornology.IsBounded s → Bornology.IsBounded (Prod.snd '' s)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_lt_mul_of_lt_of_le_of_pos_of_nonneg : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α]
  [MulPosStrictMono α], a < b → c ≤ d → 0 < c → 0 ≤ b → a * c < b * d
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The comultiplication morphism of a comonoid object.  -/
CategoryTheory.ComonObj.«termΔ[_]» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.congr_fun : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] {f g : MultilinearMap R M₁ M₂}, f = g → ∀ (x : (i : ι) → M₁ i), f x = g x
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_suffix.injEq : ∀ (lhs : Bool) (s : Lean.Grind.AC.Seq) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) (lhs_1 : Bool) (s_1 : Lean.Grind.AC.Seq)
  (c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.simp_suffix lhs s c₁ c₂ =
      Lean.Meta.Grind.AC.EqCnstrProof.simp_suffix lhs_1 s_1 c₁_1 c₂_1) =
    (lhs = lhs_1 ∧ s = s_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domLCongr_symm : ∀ (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) {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (S : Type u_12) [inst_7 : Semiring S] [inst_8 : Module S N] [inst_9 : SMulCommClass R S N]
  (e : M ≃ₗ[R] M₂), (AlternatingMap.domLCongr R N ι S e).symm = AlternatingMap.domLCongr R N ι S e.symm
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.lt_symm_apply : ∀ {R : Type u_6} {S : Type u_7} [inst : Mul R] [inst_1 : Add R] [inst_2 : Mul S] [inst_3 : Add S] [inst_4 : Preorder R]
  [inst_5 : Preorder S] (e : R ≃+*o S) {x : R} {y : S}, x < e.symm y ↔ e x < y
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getEntry?ₘ_eq_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α}, m.getEntry?ₘ a = Std.Internal.List.getEntry? a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- If `cov` is a covariant derivative on each set in an open cover, it is a covariant derivative.
 -/
CovariantDerivative.ofIsCovariantDerivativeOnOfOpenCover : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            {ι : Type u_7} →
                                              {s : ι → Set M} →
                                                {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} →
                                                  (∀ (i : ι), IsCovariantDerivativeOn F cov (s i)) →
                                                    ⋃ i, s i = Set.univ → CovariantDerivative I F V
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.inv.congr_simp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ Φ_1 : CategoryTheory.LocalizerMorphism W₁ W₂) (e_Φ : Φ = Φ_1)
  [inst_2 : Φ.functor.IsEquivalence] [inst_3 : Φ.IsInduced] [inst_4 : W₂.RespectsIso], Φ.inv = Φ_1.inv
-- Mathlib.Order.BoundedOrder.Basic
subsingleton_of_top_eq_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α], ⊤ = ⊥ → Subsingleton α
-- Mathlib.RingTheory.DedekindDomain.Factorization
IsDedekindDomain.HeightOneSpectrum.maxPowDividing.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  (I : Ideal R), v.maxPowDividing I = v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Pullback the coefficients of an element of `R[N]` under an injective `f : M → N`.

Coefficients not in the range of `f` are dropped.  -/
AddMonoidAlgebra.comapDomain : {R : Type u_3} →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : Semiring R] → (f : M → N) → Function.Injective f → AddMonoidAlgebra R N → AddMonoidAlgebra R M
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_ofNat_le_lift : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Cardinal.aleph (OfNat.ofNat n) ≤ Cardinal.lift.{v, u} c ↔ Cardinal.aleph (OfNat.ofNat n) ≤ c
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
/-- Normalised Eisenstein series of level 1 and weight `k`,
here they have been scaled by `1/2` since we sum over coprime pairs.  -/
ModularForm.E : {k : ℕ} → 3 ≤ k → ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
-- Mathlib.Data.Nat.Basic
Nat.instPartialOrder : PartialOrder ℕ
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatch_iff_splits : ∀ {pat s : String.Slice} {pos : s.Pos}, String.Slice.Pattern.Model.IsLongestMatch pat pos ↔ ∃ t, pos.Splits pat.copy t
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.pow_mul_pow_lcm : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ ζ' : M} {k' : ℕ},
  IsPrimitiveRoot ζ k →
    IsPrimitiveRoot ζ' k' →
      k ≠ 0 →
        k' ≠ 0 →
          IsPrimitiveRoot (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k')) (k.lcm k')
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.homOfLE_apply' : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (e : U ≤ V) (x : ↥X) (hx : x ∈ U), (X.homOfLE e) ⟨x, hx⟩ = ⟨x, ⋯⟩
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.map_nsmul : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (n : ℕ) (s : Multiset α), Multiset.map f (n • s) = n • Multiset.map f s
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
CategoryTheory.IsSplitEqualizer.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X}
  {leftRetraction : X ⟶ W} {rightRetraction : Y ⟶ X}
  {condition :
    autoParam (CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
      CategoryTheory.IsSplitEqualizer.condition._autoParam}
  {ι_leftRetraction :
    autoParam (CategoryTheory.CategoryStruct.comp ι leftRetraction = CategoryTheory.CategoryStruct.id W)
      CategoryTheory.IsSplitEqualizer.ι_leftRetraction._autoParam}
  {bottom_rightRetraction :
    autoParam (CategoryTheory.CategoryStruct.comp g rightRetraction = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.IsSplitEqualizer.bottom_rightRetraction._autoParam}
  {top_rightRetraction :
    autoParam
      (CategoryTheory.CategoryStruct.comp f rightRetraction = CategoryTheory.CategoryStruct.comp leftRetraction ι)
      CategoryTheory.IsSplitEqualizer.top_rightRetraction._autoParam}
  {leftRetraction_1 : X ⟶ W} {rightRetraction_1 : Y ⟶ X}
  {condition_1 :
    autoParam (CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
      CategoryTheory.IsSplitEqualizer.condition._autoParam}
  {ι_leftRetraction_1 :
    autoParam (CategoryTheory.CategoryStruct.comp ι leftRetraction_1 = CategoryTheory.CategoryStruct.id W)
      CategoryTheory.IsSplitEqualizer.ι_leftRetraction._autoParam}
  {bottom_rightRetraction_1 :
    autoParam (CategoryTheory.CategoryStruct.comp g rightRetraction_1 = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.IsSplitEqualizer.bottom_rightRetraction._autoParam}
  {top_rightRetraction_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp f rightRetraction_1 = CategoryTheory.CategoryStruct.comp leftRetraction_1 ι)
      CategoryTheory.IsSplitEqualizer.top_rightRetraction._autoParam},
  { leftRetraction := leftRetraction, rightRetraction := rightRetraction, condition := condition,
        ι_leftRetraction := ι_leftRetraction, bottom_rightRetraction := bottom_rightRetraction,
        top_rightRetraction := top_rightRetraction } =
      { leftRetraction := leftRetraction_1, rightRetraction := rightRetraction_1, condition := condition_1,
        ι_leftRetraction := ι_leftRetraction_1, bottom_rightRetraction := bottom_rightRetraction_1,
        top_rightRetraction := top_rightRetraction_1 } →
    leftRetraction = leftRetraction_1 ∧ rightRetraction = rightRetraction_1
-- Lean.Attributes
Lean.instInhabitedAttributeImpl : Inhabited Lean.AttributeImpl
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_right_nil : ∀ {m n : ℕ} {α : Sort u_1} (u : Fin m → α) (v : Fin n → α) (hv : n = 0), Fin.append u v = u ∘ Fin.cast ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
SSet.finite_of_isPullback : ∀ {X₁ X₂ X₃ X₄ : SSet} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄},
  CategoryTheory.IsPullback t l r b → ∀ [X₂.Finite] [X₃.Finite], X₁.Finite
-- Mathlib.Tactic.Linarith.Verification
/-- `mulExpr n e` creates an `Expr` representing `n*e`.
When elaborated, the coefficient will be a native numeral of the same type as `e`.
 -/
Mathlib.Tactic.Linarith.mulExpr : ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Ring.BooleanRing
toBoolAlg_ofBoolAlg : ∀ {α : Type u_1} (a : AsBoolAlg α), toBoolAlg (ofBoolAlg a) = a
-- Lean.Elab.Declaration
Lean.Elab.Command.elabAttr : Lean.Elab.Command.CommandElab
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.FinStronglyMeasurable.exists_set_sigmaFinite : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [inst : Zero β]
  [inst_1 : TopologicalSpace β] [T2Space β],
  MeasureTheory.FinStronglyMeasurable f μ →
    ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ MeasureTheory.SigmaFinite (μ.restrict t)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpCompIso_hom_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  (X : CategoryTheory.Grp C),
  (CategoryTheory.Functor.mapGrpCompIso.hom.app X).hom.hom = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.X))
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.State.debug : Lean.Meta.Sym.State → Bool
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso_inv_app_app : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (X : CategoryTheory.Functor A B × CategoryTheory.Functor A' B) (X_1 : A'),
  (CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInrIso.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.2.obj X_1)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.instFaithfulSMul : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B},
  FaithfulSMul G (HNNExtension.NormalWord d)
-- Mathlib.Data.String.Defs
/-- Pad `s : String` with repeated occurrences of `c : Char` until it's of length `n`.
If `s` is initially larger than `n`, just return `s`.  -/
String.leftpad : ℕ → optParam Char ' ' → String → String
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.mul_2 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x y y' : RingCat.Colimits.Prequotient F),
  RingCat.Colimits.Relation F y y' → RingCat.Colimits.Relation F (x.mul y) (x.mul y')
-- Mathlib.Topology.FiberBundle.Basic
/-- Characterization of continuous sections of a vector bundle.  -/
FiberBundle.continuousAt_section : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {E : B → Type u_5}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
  [inst_4 : FiberBundle F E] {s : (x : B) → E x} (x₀ : B),
  ContinuousAt (fun x => ⟨x, s x⟩) x₀ ↔ ContinuousAt (fun x => (↑(trivializationAt F E x₀) ⟨x, s x⟩).2) x₀
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
/-- An invariant inner product on the weight space.  -/
RootPairing.RootForm : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] → RootPairing ι R M N → [Fintype ι] → LinearMap.BilinForm R M
-- Mathlib.Topology.ContinuousOn
ContinuousOn.mapsToRestrict : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {t : Set β}, ContinuousOn f s → ∀ (ht : Set.MapsTo f s t), Continuous (Set.MapsTo.restrict f s t ht)
-- Mathlib.NumberTheory.Padics.WithVal
Padic.coe_withValRingEquiv_symm : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], ⇑Padic.withValRingEquiv.symm = ⋯.extend UniformSpace.Completion.coe'
-- Init.Data.Option.Lemmas
Option.bind_congr : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f g : α → Option β},
  (∀ (a : α), o = some a → f a = g a) → o.bind f = o.bind g
-- Mathlib.Computability.Ackermann
one_lt_ack_succ_right : ∀ (m n : ℕ), 1 < ack m (n + 1)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_map_piCongrLeft : ∀ {ι : Type u_1} {ι' : Type u_2} [inst : Fintype ι] [inst_1 : Fintype ι'] (e : ι ≃ ι') {β : ι' → Type u_4}
  [inst_2 : (i : ι') → MeasurableSpace (β i)] (μ : (i : ι') → MeasureTheory.Measure (β i))
  [∀ (i : ι'), MeasureTheory.SigmaFinite (μ i)],
  MeasureTheory.Measure.map (⇑(MeasurableEquiv.piCongrLeft (fun i => β i) e))
      (MeasureTheory.Measure.pi fun i => μ (e i)) =
    MeasureTheory.Measure.pi μ
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.inr_isoPushout_hom_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight inr Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight hP.isoPushout.hom Q) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inr f g) Q
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.op_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (α : X ≅ Y), α.symm.op = α.op.symm
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X : CategoryTheory.SimplicialObject C} {N : ℕ → C}
  {ι : (n : ℕ) → N n ⟶ X.obj (Opposite.op { len := n })}
  {isColimit' :
    (Δ : SimplexCategoryᵒᵖ) →
      CategoryTheory.Limits.IsColimit (CategoryTheory.SimplicialObject.Splitting.cofan' N X ι Δ)}
  {N_1 : ℕ → C} {ι_1 : (n : ℕ) → N_1 n ⟶ X.obj (Opposite.op { len := n })}
  {isColimit'_1 :
    (Δ : SimplexCategoryᵒᵖ) →
      CategoryTheory.Limits.IsColimit (CategoryTheory.SimplicialObject.Splitting.cofan' N_1 X ι_1 Δ)},
  { N := N, ι := ι, isColimit' := isColimit' } = { N := N_1, ι := ι_1, isColimit' := isColimit'_1 } →
    N = N_1 ∧ ι ≍ ι_1 ∧ isColimit' ≍ isColimit'_1
-- Lean.Elab.InfoTree.Types
Lean.Elab.OptionInfo.declName : Lean.Elab.OptionInfo → Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- A comonoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called a "coalgebra object".
 -/
CategoryTheory.Comon : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.MonoidalCategory C] → Type (max u₁ v₁)
-- Lean.DocString.Extension
Lean.ElabBlock.custom.sizeOf_spec : ∀ (val : Dynamic), sizeOf (Lean.ElabBlock.custom val) = 1 + sizeOf val
-- Mathlib.Order.Cover
covBy_congr_left : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → (a ⋖ c ↔ b ⋖ c)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.insertMin.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Sort u_3) →
      (t : Std.DTreeMap.Internal.Impl α β) →
        (hr : t.Balanced) →
          ((hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hr) →
            ((sz : ℕ) →
                (k' : α) →
                  (v' : β k') →
                    (l' r' : Std.DTreeMap.Internal.Impl α β) →
                      (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
                        motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr) →
              motive t hr
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
/-- The cone `limitCone F` is limit for any `F : J ⥤ PresheafOfModules.{v} R`.  -/
PresheafOfModules.isLimitLimitCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {J : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
          (F : CategoryTheory.Functor J (PresheafOfModules R)) →
            [inst_2 :
                ∀ (X : Cᵒᵖ),
                  Small.{v, max u₂ v}
                    ↑((F.comp (PresheafOfModules.evaluation R X)).comp
                          (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] →
              CategoryTheory.Limits.IsLimit (PresheafOfModules.limitCone F)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialCosimplicialAugmentedEquiv_inverse : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.simplicialCosimplicialAugmentedEquiv C).inverse = CategoryTheory.cosimplicialToSimplicialAugmented C