mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Hom.WithTopBot
Function.Embedding.coeWithTop.eq_1 : ∀ {α : Type u_1}, Function.Embedding.coeWithTop = { toFun := WithTop.some, inj' := ⋯ }
-- Mathlib.Algebra.Lie.Basic
/-- A Lie ring module may be pulled back along a morphism of Lie algebras.

See note [reducible non-instances].  -/
LieRingModule.compLieHom : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      (M : Type w₁) →
        [inst : CommRing R] →
          [inst_1 : LieRing L₁] →
            [inst_2 : LieAlgebra R L₁] →
              [inst_3 : LieRing L₂] →
                [inst_4 : LieAlgebra R L₂] →
                  [inst_5 : AddCommGroup M] → [LieRingModule L₂ M] → (L₁ →ₗ⁅R⁆ L₂) → LieRingModule L₁ M
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition with a linear isometry on the right preserves the norm of the iterated derivative
within a set.  -/
LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} (g : G ≃ₗᵢ[𝕜] E) (f : E → F),
  UniqueDiffOn 𝕜 s →
    ∀ {x : G},
      g x ∈ s → ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β},
  Std.DTreeMap.Const.get? (Std.DTreeMap.Const.alter t k f) k' =
    if cmp k k' = Ordering.eq then f (Std.DTreeMap.Const.get? t k) else Std.DTreeMap.Const.get? t k'
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- If a finset `u` is contained in the sum of two sets `s + t`, we can find two finsets
`s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' + t'`.  -/
Finset.subset_add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {u : Finset α} {s t : Set α},
  ↑u ⊆ s + t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' + t'
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- This instance is useful when talking about Bernoulli sequences of random variables or binomial
random graphs.  -/
Set.instMeasurableSpace : {α : Type u_1} → MeasurableSpace (Set α)
-- Mathlib.RingTheory.Etale.Finite
/-- If the geometric point `Ω` factors through `S`, the fiber can be computed after base change
to `S`.  -/
CommAlgCat.FiniteEtale.fiberIsoBaseChangeFiber : (R : Type u) →
  [inst : CommRing R] →
    (Ω : Type w) →
      [inst_1 : Field Ω] →
        [inst_2 : Algebra R Ω] →
          (S : Type w) →
            [inst_3 : CommRing S] →
              [inst_4 : Algebra R S] →
                [inst_5 : Algebra S Ω] →
                  [IsScalarTower R S Ω] →
                    CommAlgCat.FiniteEtale.fiber R Ω ≅
                      (CommAlgCat.FiniteEtale.baseChange R S).op.comp (CommAlgCat.FiniteEtale.fiber S Ω)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.DiscrInfo.mk.injEq : ∀ (hName? hName?_1 : Option Lean.Name), ({ hName? := hName? } = { hName? := hName?_1 }) = (hName? = hName?_1)
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic (2 ^ k) K)` (in particular for `K = ℚ`) and `k` is at least `2`,
then the norm of `zeta (2 ^ k) K L - 1` is `2`.  -/
IsCyclotomicExtension.norm_zeta_pow_sub_one_two : ∀ {K : Type u} (L : Type v) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {k : ℕ},
  2 ≤ k →
    ∀ [inst_3 : IsCyclotomicExtension {2 ^ k} K L],
      Irreducible (Polynomial.cyclotomic (2 ^ k) K) → (Algebra.norm K) (IsCyclotomicExtension.zeta (2 ^ k) K L - 1) = 2
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.comp_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type w}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (B : LinearMap.BilinForm R M') (l r : M →ₗ[R] M') (v w : M),
  ((B.comp l r) v) w = (B (l v)) (r w)
-- Mathlib.Order.Heyting.Basic
compl_sup_compl_le : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, aᶜ ⊔ bᶜ ≤ (a ⊓ b)ᶜ
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
IsGLB.inv : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G},
  IsGLB s a → IsLUB s⁻¹ a⁻¹
-- Init.MetaTypes
/-- TODO (currently unimplemented). When `true` (default: `true`), performs eta reduction for `fun` expressions.
That is, `(fun x => f x)` reduces to `f`.
 -/
Lean.Meta.DSimp.Config.eta : Lean.Meta.DSimp.Config → Bool
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.symm_bijective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Function.Bijective Homeomorph.symm
-- Mathlib.Order.Filter.Extr
IsMaxFilter.tendsto_principal_Iic : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter f l a → Filter.Tendsto f l (Filter.principal (Set.Iic (f a)))
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.x : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.TimeZone.Offset
-- Lean.Elab.DefView
/-- Untyped snapshots from `logSnapshotTask`, saved at this level for cancellation.  -/
Lean.Elab.BodyProcessedSnapshot.moreSnaps : Lean.Elab.BodyProcessedSnapshot → Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)
-- Mathlib.Algebra.Homology.Embedding.Extend
_private.Mathlib.Algebra.Homology.Embedding.Extend.0.HomologicalComplex.extend.X.match_1.eq_1 : ∀ {ι : Type u_1} (motive : Option ι → Sort u_2) (x : ι) (h_1 : (x : ι) → motive (some x)) (h_2 : Unit → motive none),
  (match some x with
    | some x => h_1 x
    | none => h_2 ()) =
    h_1 x
-- Mathlib.RingTheory.TensorProduct.Finite
/-- Every `x : N ⊗ M` is the image of some `y : J ⊗ M`, where `J` is a finitely generated
submodule of `N`, under the tensor product of the inclusion `J → N` and the identity `M → M`.  -/
Submodule.exists_fg_le_eq_rTensor_subtype : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x : TensorProduct R N M),
  ∃ J, ∃ (_ : J.FG), ∃ y, x = (LinearMap.rTensor M J.subtype) y
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.ofPrime_le_of_le : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (P Q : Ideal ↥A) [inst_1 : P.IsPrime] [inst_2 : Q.IsPrime],
  P ≤ Q → A.ofPrime Q ≤ A.ofPrime P
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swapEquiv_counitIso_inv_app_toFun : ∀ (X : Bipointed) (a : ((Bipointed.swap.comp Bipointed.swap).obj X).X),
  (Bipointed.swapEquiv.counitIso.inv.app X).toFun a = a
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.Data.Sym.Basic
Sym.mem_coe : ∀ {α : Type u_1} {n : ℕ} {s : Sym α n} {a : α}, a ∈ ↑s ↔ a ∈ s
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the associator `α_ f g h`.  -/
Mathlib.Tactic.BicategoryLike.StructuralAtom.associator : Lean.Expr →
  Mathlib.Tactic.BicategoryLike.Mor₁ →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.StructuralAtom
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.instL1NormedAlgebra : (𝕜 : Type u_1) →
  {R : Type u_3} →
    {M : Type u_4} →
      [inst : NormedField 𝕜] →
        [inst_1 : NormedRing R] →
          [inst_2 : NormedAddCommGroup M] →
            [inst_3 : NormedAlgebra 𝕜 R] →
              [inst_4 : NormedSpace 𝕜 M] →
                [inst_5 : Module R M] →
                  [inst_6 : Module Rᵐᵒᵖ M] →
                    [inst_7 : IsBoundedSMul R M] →
                      [inst_8 : IsBoundedSMul Rᵐᵒᵖ M] →
                        [inst_9 : SMulCommClass R Rᵐᵒᵖ M] →
                          [IsScalarTower 𝕜 R M] → [IsScalarTower 𝕜 Rᵐᵒᵖ M] → NormedAlgebra 𝕜 (TrivSqZeroExt R M)
-- Mathlib.CategoryTheory.Join.Basic
/-- A natural transformation `Fₗ ⟶ Gₗ` induces a natural transformation
`mapPair Fₗ H ⟶ mapPair Gₗ H` for every `H : D ⥤ E'`.  -/
CategoryTheory.Join.mapWhiskerRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {E' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] →
                {Fₗ Gₗ : CategoryTheory.Functor C E} →
                  (Fₗ ⟶ Gₗ) →
                    (H : CategoryTheory.Functor D E') →
                      CategoryTheory.Join.mapPair Fₗ H ⟶ CategoryTheory.Join.mapPair Gₗ H
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.add_neg_of_neg_of_nonpos`.  -/
Left.add_neg_of_neg_of_nonpos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b : α}, a < 0 → b ≤ 0 → a + b < 0
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instHasCoproductsIndOfHasFiniteCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Limits.HasCoproducts (CategoryTheory.Ind C)
-- Mathlib.Topology.FiberBundle.Basic
/-- Characterization of continuous sections within a set at a point of a vector bundle.  -/
FiberBundle.continuousWithinAt_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} {a : Set B} {x₀ : B},
  ContinuousWithinAt (fun x => ⟨x, s x⟩) a x₀ ↔
    ContinuousWithinAt (fun x => (↑(trivializationAt F E x₀) ⟨x, s x⟩).2) a x₀
-- Mathlib.Probability.Moments.ComplexMGF
ProbabilityTheory.analyticOnNhd_complexMGF : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AnalyticOnNhd ℂ (ProbabilityTheory.complexMGF X μ) {z | z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ)}
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.homOfEq_heq_left_iff : ∀ {V : Type u_1} [inst : Quiver V] {X Y X' Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X = X') (hY : Y = Y'),
  Quiver.homOfEq f hX hY ≍ g ↔ f ≍ g
-- Std.Time.Format.Modifier
/-- `a`: AM/PM of day (e.g., PM).
 -/
Std.Time.Modifier.a : Std.Time.Text → Std.Time.Modifier
-- Mathlib.Algebra.Module.Submodule.Ker
AddMonoidHom.coe_toIntLinearMap_ker : ∀ {M : Type u_11} {M₂ : Type u_12} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] (f : M →+ M₂),
  f.toIntLinearMap.ker = AddSubgroup.toIntSubmodule f.ker
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm_div_self_nhdsNE : ∀ {E : Type u_7} [inst : NormedCommGroup E] (a : E),
  Filter.Tendsto (fun x => ‖x / a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
-- Mathlib.Order.Monotone.Basic
StrictMono.lt_iff_lt : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → ∀ {a b : α}, f a < f b ↔ a < b
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a : α} {fallback : β}, ∅.getD a fallback = fallback
-- Mathlib.Algebra.Homology.LocalCohomology
localCohomology.hasColimitDiagram : ∀ {R : Type (max u v)} [inst : CommRing R] {D : Type v} [inst_1 : CategoryTheory.SmallCategory D]
  (I : CategoryTheory.Functor D (Ideal R)) (i : ℕ), CategoryTheory.Limits.HasColimit (localCohomology.diagram I i)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀) {Z_1 : AlgebraicGeometry.Scheme} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)
          (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
            (𝒰.f i))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) h))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f j))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) h))
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.vonNeumann_mem_of_lt : ∀ {a b : Ordinal.{u}}, a < b → ZFSet.vonNeumann a ∈ ZFSet.vonNeumann b
-- Mathlib.Analysis.Calculus.VectorField
Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s : Set E} {x : E},
  V₁ =ᶠ[nhdsWithin x s] V →
    W₁ =ᶠ[nhdsWithin x s] W → x ∈ s → VectorField.lieBracketWithin 𝕜 V₁ W₁ s x = VectorField.lieBracketWithin 𝕜 V W s x
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.decidableMemMultiples : {M : Type u_1} → [inst : AddMonoid M] → {a : M} → DecidablePred fun x => x ∈ AddSubmonoid.multiples a
-- Lean.Meta.Tactic.Grind.EMatch
/-- Similar to `matchArgs?` but if `p` has fewer arguments than `e`, we match `p` with a prefix of `e`.  -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.matchArgsPrefix? : Lean.Meta.Grind.EMatch.Choice → Lean.Expr → Lean.Expr → OptionT Lean.Meta.Grind.GoalM Lean.Meta.Grind.EMatch.Choice
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpNatTrans.eq_1 : ∀ {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]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [inst_5 : F'.Monoidal] (f : F ⟶ F'),
  CategoryTheory.Functor.mapAddGrpNatTrans f =
    { app := fun X => CategoryTheory.AddGrp.homMk' ((CategoryTheory.Functor.mapAddMonNatTrans f).app X.toAddMon),
      naturality := ⋯ }
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.eq_emptyOn_or_nonempty : ∀ {α : Type u_1} (M : Matroid α), M = Matroid.emptyOn α ∨ M.Nonempty
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.mono_homologyMap_τ₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂),
  S₁.ShortExact →
    S₂.ShortExact →
      ∀ (i : ι),
        CategoryTheory.Epi (HomologicalComplex.homologyMap φ.τ₁ i) →
          CategoryTheory.Mono (HomologicalComplex.homologyMap φ.τ₂ i) →
            (∀ (j : ι), c.Rel i j → CategoryTheory.Mono (HomologicalComplex.homologyMap φ.τ₁ j)) →
              CategoryTheory.Mono (HomologicalComplex.homologyMap φ.τ₃ i)
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Mathlib.Tactic.Bicategory.naturality_associator : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} {p : a ⟶ b} {f : b ⟶ c} {g : c ⟶ d} {h : d ⟶ e}
  {pf : a ⟶ c} {pfg : a ⟶ d} {pfgh : a ⟶ e} (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf)
  (η_g : CategoryTheory.CategoryStruct.comp pf g ≅ pfg) (η_h : CategoryTheory.CategoryStruct.comp pfg h ≅ pfgh),
  CategoryTheory.Bicategory.whiskerLeftIso p (CategoryTheory.Bicategory.associator f g h) ≪≫
      Mathlib.Tactic.Bicategory.normalizeIsoComp η_f (Mathlib.Tactic.Bicategory.normalizeIsoComp η_g η_h) =
    Mathlib.Tactic.Bicategory.normalizeIsoComp (Mathlib.Tactic.Bicategory.normalizeIsoComp η_f η_g) η_h
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_one : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.T R 1 = Polynomial.X
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheorem.patterns : Lean.Meta.Grind.EMatchTheorem → List Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Skeleton
/-- The skeleton of a braided monoidal category has a braided monoidal structure itself, induced by
the equivalence.  -/
CategoryTheory.Skeleton.instBraidedCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.BraidedCategory (CategoryTheory.Skeleton C)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_bot : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Hom M N),
  FirstOrder.Language.Substructure.map f ⊥ = ⊥
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.map_nonsingular : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] {f : R →+* S},
  Function.Injective ⇑f → ∀ (P : Fin 3 → R), (W'.map f).Nonsingular (⇑f ∘ P) ↔ W'.Nonsingular P
-- Lean.Elab.DocString
/-- Adds a builtin documentation role.

Should be run during initialization.
 -/
Lean.Doc.addBuiltinDocRole : Lean.Name → Lean.Name → Lean.Doc.DocRoleExpander → IO Unit
-- Mathlib.Geometry.Manifold.Algebra.SMul
/-- The diffeomorphism given by affine-addition of an element of an additive group `G` acting
Cⁿ-differentiably on a manifold `M` is a diffeomorphism from `M` to itself. Its inverse is
addition of `-g`.  -/
Diffeomorph.vadd : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              (I : ModelWithCorners 𝕜 E H) →
                {H' : Type u_4} →
                  [inst_4 : TopologicalSpace H'] →
                    {E' : Type u_5} →
                      [inst_5 : NormedAddCommGroup E'] →
                        [inst_6 : NormedSpace 𝕜 E'] →
                          (I' : ModelWithCorners 𝕜 E' H') →
                            {G : Type u_8} →
                              [inst_7 : TopologicalSpace G] →
                                [inst_8 : ChartedSpace H G] →
                                  {M : Type u_9} →
                                    [inst_9 : TopologicalSpace M] →
                                      [inst_10 : ChartedSpace H' M] →
                                        [inst_11 : AddGroup G] →
                                          [inst_12 : AddAction G M] →
                                            (n : WithTop ℕ∞) → [ContMDiffVAdd I I' n G M] → G → Diffeomorph I' I' M M n
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- Given a measurable function `g : β → γ`, and an almost everywhere equal function `[f] : α →ₘ β`,
return the equivalence class of `g ∘ f`, i.e., the almost everywhere equal function
`[g ∘ f] : α →ₘ γ`. This requires that `γ` has a second countable topology.  -/
MeasureTheory.AEEqFun.compMeasurable : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : TopologicalSpace γ] →
              [inst_3 : MeasurableSpace β] →
                [TopologicalSpace.PseudoMetrizableSpace β] →
                  [BorelSpace β] →
                    [inst_6 : MeasurableSpace γ] →
                      [TopologicalSpace.PseudoMetrizableSpace γ] →
                        [OpensMeasurableSpace γ] →
                          [SecondCountableTopology γ] → (g : β → γ) → Measurable g → (α →ₘ[μ] β) → α →ₘ[μ] γ
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- We show that the converse to `isSplitEpiEqualizes` is true:
Whenever `f` coequalizes `(f ≫ s)` and `(𝟙 X)`, then `s` is a section of `f`.  -/
CategoryTheory.Limits.splitEpiOfCoequalizer : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        {s : Y ⟶ X} →
          (hs : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp s f) = f) →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯) → CategoryTheory.SplitEpi f
-- Init.Data.Rat.Lemmas
Rat.normalize_eq_mkRat : ∀ {num : ℤ} {den : ℕ} (den_nz : den ≠ 0), Rat.normalize num den den_nz = mkRat num den
-- Mathlib.GroupTheory.Finiteness
AddSubgroup.FG.iSup : ∀ {G : Type u_3} [inst : AddGroup G] {ι : Sort u_5} [Finite ι] (P : ι → AddSubgroup G),
  (∀ (i : ι), (P i).FG) → (iSup P).FG
-- Lean.Elab.Tactic.Omega.OmegaM
_private.Lean.Elab.Tactic.Omega.OmegaM.0.Lean.Elab.Tactic.Omega.groundInt?.op : (ℤ → ℤ → ℤ) → Lean.Expr → Lean.Expr → Option ℤ
-- Lean.ToExpr
Lean.instToExprString : Lean.ToExpr String
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.toSlashInvariantForm_coe : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f : ModularForm Γ k), ⇑f.toSlashInvariantForm = ⇑f
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.isStableUnderCobaseChange_iff_pushouts_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
  P.IsStableUnderCobaseChange ↔ P.pushouts ≤ P
-- Lean.Parser.Term
Lean.Parser.Term.proj.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Vector.Lex
Vector.lt_asymm : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [i : Std.Asymm fun x1 x2 => x1 < x2] {xs ys : Vector α n}, xs < ys → ¬ys < xs
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.map_dirac' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β},
  Measurable f →
    ∀ (a : α), MeasureTheory.Measure.map f (MeasureTheory.Measure.dirac a) = MeasureTheory.Measure.dirac (f a)
-- Mathlib.Algebra.Group.Translate
translate_prod_right : ∀ {ι : Type u_1} {M : Type u_4} {G : Type u_5} [inst : AddCommGroup G] [inst_1 : CommMonoid M] (a : G) (f : ι → G → M)
  (s : Finset ι), translate a (∏ i ∈ s, f i) = ∏ i ∈ s, translate a (f i)
-- Aesop.Frontend.Extension.Init
/-- The set of Aesop rule sets that are enabled by default.
 -/
Aesop.DeclaredRuleSets.defaultRuleSets : Aesop.DeclaredRuleSets → Std.HashSet Aesop.RuleSetName
-- Init.Data.List.OfFn
/-- `ofFn` on an empty domain is the empty list.  -/
List.ofFn_zero : ∀ {α : Type u_1} {f : Fin 0 → α}, List.ofFn f = []
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.ext_iff : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {f g : X →ₑ[φ] Y}, f = g ↔ ∀ (x : X), f x = g x
-- Init.Data.Vector.Lemmas
Vector.append_reverse : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m},
  ys.reverse ++ xs.reverse = Vector.cast ⋯ (xs ++ ys).reverse
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.addNonRec : Lean.LocalContext × Lean.LocalInstances →
  (preDef : Lean.Elab.PreDefinition) →
    optParam Bool true →
      optParam (List Lean.Name) [preDef.declName] →
        optParam Bool true → optParam Bool false → optParam Bool false → Lean.Elab.TermElabM Unit
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.insertMany.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {ρ : Type v}
  [inst_2 : ForIn Id ρ α] (m m_1 : Std.ExtHashSet α),
  m = m_1 → ∀ (l l_1 : ρ), l = l_1 → m.insertMany l = m_1.insertMany l_1