mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffWithinAt.sub : ∀ {𝕜 : 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} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieAddGroup I n G] {f g : M → G} {s : Set M} {x₀ : M},
  ContMDiffWithinAt I' I n f s x₀ → ContMDiffWithinAt I' I n g s x₀ → ContMDiffWithinAt I' I n (fun x => f x - g x) s x₀
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The unique morphism into `Factorisation.terminal f`.  -/
CategoryTheory.Factorisation.terminalHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → (d : CategoryTheory.Factorisation f) → d.Hom CategoryTheory.Factorisation.terminal
-- Lean.Elab.Open
Lean.Elab.OpenDecl.resolveNameUsingNamespaces : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [MonadExceptOf Lean.Exception m] →
        [Lean.MonadRef m] →
          [Lean.AddMessageContext m] →
            [MonadLiftT (ST IO.RealWorld) m] →
              [Lean.MonadLog m] →
                [Lean.MonadOptions m] → [Lean.MonadResolveName m] → List Lean.Name → Lean.Ident → m Lean.Name
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_natCast : ∀ (n : ℕ), (↑n).ord = ↑n
-- Mathlib.MeasureTheory.Integral.MeanInequalities
/-- A version of Hölder with multiple arguments  -/
ENNReal.lintegral_prod_norm_pow_le : ∀ {α : Type u_2} {ι : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Finset ι)
  {f : ι → α → ENNReal},
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
-- Mathlib.Data.Sym.Sym2
/-- Dependent recursion principal for `Sym2` when the target is a `Subsingleton` type.
See `Quot.recOnSubsingleton`.  -/
Sym2.recOnSubsingleton : {α : Type u_1} →
  {motive : Sym2 α → Sort u_4} →
    [∀ (a b : α), Subsingleton (motive s(a, b))] → (z : Sym2 α) → ((a b : α) → motive s(a, b)) → motive z
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionOptions : Lean.ToJson Lean.Lsp.CodeActionOptions
-- Mathlib.Order.CompleteLattice.Basic
iSup_ulift : ∀ {α : Type u_1} {ι : Type u_8} [inst : SupSet α] (f : ULift.{u_9, u_8} ι → α), ⨆ i, f i = ⨆ i, f { down := i }
-- Aesop.Search.SearchM
Aesop.SearchM.Context.options : Aesop.SearchM.Context → Aesop.Options'
-- Init.Data.String.PosRaw
String.Pos.Raw.le_refl : ∀ {p : String.Pos.Raw}, p ≤ p
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.op_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) {Z : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (h : F.op ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.op (CategoryTheory.CategoryStruct.comp α β)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.op β)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.op α) h)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` preserves colimits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.rightOp : C ⥤ Dᵒᵖ` preserves
limits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.preservesLimit_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimit K.op F],
  CategoryTheory.Limits.PreservesLimit K F.rightOp
-- Mathlib.Topology.Algebra.ConstMulAction
continuousAt_const_smul_iff₀ : ∀ {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀]
  [inst_2 : MulAction G₀ α] [ContinuousConstSMul G₀ α] [inst_4 : TopologicalSpace β] {f : β → α} {b : β} {c : G₀},
  c ≠ 0 → (ContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b)
-- Std.Async.Signal
Std.Async.Signal.sigxcpu.sizeOf_spec : sizeOf Std.Async.Signal.sigxcpu = 1
-- Std.Sat.AIG.LawfulVecOperator
Std.Sat.AIG.LawfulVecOperator.lt_size_of_lt_aig_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → ℕ → Type}
  {f : {len : ℕ} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
  [Std.Sat.AIG.LawfulVecOperator α β fun {len} => f] {len x : ℕ} (aig : Std.Sat.AIG α) (input : β aig len),
  x < aig.decls.size → x < (f aig input).aig.decls.size
-- Batteries.Lean.NameMapAttribute
Lean.NameMapAttributeImpl.mk.injEq : ∀ {α : Type} (name : Lean.Name) (ref : autoParam Lean.Name Lean.NameMapAttributeImpl.ref._autoParam) (descr : String)
  (add : Lean.Name → Lean.Syntax → Lean.AttrM α) (name_1 : Lean.Name)
  (ref_1 : autoParam Lean.Name Lean.NameMapAttributeImpl.ref._autoParam) (descr_1 : String)
  (add_1 : Lean.Name → Lean.Syntax → Lean.AttrM α),
  ({ name := name, ref := ref, descr := descr, add := add } =
      { name := name_1, ref := ref_1, descr := descr_1, add := add_1 }) =
    (name = name_1 ∧ ref = ref_1 ∧ descr = descr_1 ∧ add = add_1)
-- Init.Data.SInt.Float32
/-- Truncates a floating-point number to the nearest 16-bit signed integer, rounding towards zero.

If the `Float` is larger than the maximum value for `Int16` (including `Inf`), returns the maximum
value of `Int16` (i.e. `Int16.maxValue`). If it is smaller than the minimum value for `Int16`
(including `-Inf`), returns the minimum value of `Int16` (i.e. `Int16.minValue`). If it is `NaN`,
returns `0`.

This function does not reduce in the kernel.
 -/
Float32.toInt16 : Float32 → Int16
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.hom_ext : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c},
  e₁.AreComplementary e₂ →
    ∀ {K L : HomologicalComplex C c} [K.IsStrictlySupported e₁] [L.IsStrictlySupported e₂] (φ : K ⟶ L), φ = 0
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_eq_zero_iff : ∀ {K : Type u} [inst : Field K] {x : RatFunc K}, x.num = 0 ↔ x = 0
-- Mathlib.Data.ENNReal.Inv
ENNReal.one_half_lt_one : 2⁻¹ < 1
-- Mathlib.Data.Set.Lattice.Image
Set.iUnion_prod : ∀ {ι : Type u_9} {ι' : Type u_10} {α : Type u_11} {β : Type u_12} (s : ι → Set α) (t : ι' → Set β),
  ⋃ x, s x.1 ×ˢ t x.2 = (⋃ i, s i) ×ˢ ⋃ i, t i
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.Tendsto.mul : ∀ {α : Type u_2} {f : Filter α} {ma mb : α → EReal} {a b : EReal},
  Filter.Tendsto ma f (nhds a) →
    Filter.Tendsto mb f (nhds b) →
      a ≠ 0 ∨ b ≠ ⊥ →
        a ≠ 0 ∨ b ≠ ⊤ → a ≠ ⊥ ∨ b ≠ 0 → a ≠ ⊤ ∨ b ≠ 0 → Filter.Tendsto (fun x => ma x * mb x) f (nhds (a * b))
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.ContinuousRiemannianMetric.mk : {B : Type u_4} →
  [inst : TopologicalSpace B] →
    {F : Type u_5} →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : NormedSpace ℝ F] →
          {E : B → Type u_6} →
            [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] →
              [inst_4 : (b : B) → TopologicalSpace (E b)] →
                [inst_5 : (b : B) → AddCommGroup (E b)] →
                  [inst_6 : (b : B) → Module ℝ (E b)] →
                    [inst_7 : FiberBundle F E] →
                      [inst_8 : VectorBundle ℝ F E] →
                        (inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ) →
                          (∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v) →
                            (∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v) →
                              (∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1}) →
                                (Continuous fun b => ⟨b, inner b⟩) → Bundle.ContinuousRiemannianMetric F E
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.distinct_keys_toList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  List.Pairwise (fun a b => (a.fst == b.fst) = false) m.toList
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- We say that `F` preserves limits of shape `J` if `F` preserves limits for every diagram
`K : J ⥤ C`, i.e., `F` maps limit cones over `K` to limit cones.  -/
CategoryTheory.Limits.PreservesLimitsOfShape : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) → [CategoryTheory.Category.{w', w} J] → CategoryTheory.Functor C D → Prop
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.buildFinalizeContext : Array Lean.Elab.Command.InductiveElabStep2 →
  List Lean.Name →
    Array Lean.Expr →
      Array Lean.Expr →
        Array Lean.Elab.Command.InductiveView →
          Array Lean.Expr →
            Array Lean.Elab.Command.ElabHeaderResult → Lean.Elab.TermElabM Lean.Elab.Command.FinalizeContext✝
-- Mathlib.Algebra.Group.Units.Equiv
toUnits_symm_apply : ∀ {G : Type u_5} [inst : Group G] (x : Gˣ), toUnits.symm x = ↑x
-- Init.Data.Vector.Lemmas
Vector.some_getElem_eq_getElem?_iff : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n), some xs[i] = xs[i]? ↔ True
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLE_iff_pairwise`. -/
List.Pairwise.sortedLE : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], List.Pairwise (fun x1 x2 => x1 ≤ x2) l → l.SortedLE
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The natural isomorphism sending `single g r₁ ⊗ single a r₂ ↦ single a (single g r₁r₂)`.  -/
Rep.leftRegularTensorTrivialIsoFree : (k G α : Type u) →
  [inst : CommRing k] →
    [inst_1 : Monoid G] →
      CategoryTheory.MonoidalCategoryStruct.tensorObj (Rep.leftRegular k G) (Rep.trivial k G (MonoidAlgebra k α)) ≅
        Rep.free k G α
-- Mathlib.Topology.Category.LightProfinite.AsLimit
LightProfinite.surjective_transitionMapLE : ∀ (S : LightProfinite) {n m : ℕ} (h : n ≤ m),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (S.transitionMapLE h))
-- Init.Data.UInt.Lemmas
UInt16.le_refl : ∀ (a : UInt16), a ≤ a
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn_eq_match_step : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'} [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {γ : Type x} {it : Std.Iter β}
  {init : γ} {f : β → γ → m (ForInStep γ)},
  forIn it init f =
    match it.step with
    | ⟨Std.IterStep.yield it' out, property⟩ => do
      let __do_lift ← f out init
      match __do_lift with
        | ForInStep.yield c => forIn it' c f
        | ForInStep.done c => pure c
    | ⟨Std.IterStep.skip it', property⟩ => forIn it' init f
    | ⟨Std.IterStep.done, property⟩ => pure init
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Context.mk.sizeOf_spec : ∀ (toContext : Lean.Elab.Tactic.Context) (ctx : Lean.Meta.Grind.Context) (sctx : Lean.Meta.Sym.Context)
  (methods : Lean.Meta.Grind.Methods) (params : Lean.Meta.Grind.Params) (sym : Bool),
  sizeOf { toContext := toContext, ctx := ctx, sctx := sctx, methods := methods, params := params, sym := sym } =
    1 + sizeOf toContext + sizeOf ctx + sizeOf sctx + sizeOf methods + sizeOf params + sizeOf sym
-- Init.System.IOError
IO.Error.alreadyExists.injEq : ∀ (filename : Option String) (osCode : UInt32) (details : String) (filename_1 : Option String) (osCode_1 : UInt32)
  (details_1 : String),
  (IO.Error.alreadyExists filename osCode details = IO.Error.alreadyExists filename_1 osCode_1 details_1) =
    (filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toNonUnitalRingHom_apply_symm_toNonUnitalRingHom_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (e : R ≃+* S) (y : S), e.toNonUnitalRingHom (e.symm.toNonUnitalRingHom y) = y
-- Lean.Elab.DocString
/-- The name of the code block to suggest.  -/
Lean.Doc.CodeBlockSuggestion.name : Lean.Doc.CodeBlockSuggestion → Lean.Name
-- Mathlib.Analysis.MellinTransform
/-- If `f` is a locally integrable real-valued function which is `O(x ^ (-a))` at `∞`, then for any
`s < a`, its Mellin transform converges on some neighbourhood of `+∞`.  -/
mellin_convergent_top_of_isBigO : ∀ {f : ℝ → ℝ},
  MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0)) →
    ∀ {a s : ℝ},
      (f =O[Filter.atTop] fun x => x ^ (-a)) →
        s < a → ∃ c, 0 < c ∧ MeasureTheory.IntegrableOn (fun t => t ^ (s - 1) * f t) (Set.Ioi c) MeasureTheory.volume
-- Mathlib.Order.Interval.Multiset
Multiset.nodup_Icc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, (Multiset.Icc a b).Nodup
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- Evidence that `leftAdjoint f` is a left adjoint of `f`.  -/
CategoryTheory.Bicategory.Adjunction.ofIsRightAdjoint : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (f : b ⟶ a) →
        [inst_1 : CategoryTheory.Bicategory.IsRightAdjoint f] →
          CategoryTheory.Bicategory.Adjunction (CategoryTheory.Bicategory.leftAdjoint f) f
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Sub-sub-add version.  -/
Finset.card_sub_add_le_card_sub_add_card_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddCommGroup G] (A B C : Finset G),
  (A - C).card * B.card ≤ (A - B).card * (B + C).card
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_apply : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) {V : TopologicalSpace.Opens ↑Y.toTopCat}
  (x : ↥((TopologicalSpace.Opens.map f.base).obj V)) (a : ↑(Y.presheaf.obj (Opposite.op V))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f ↑x))
      ((CategoryTheory.ConcreteCategory.hom (Y.evaluation ⟨(CategoryTheory.ConcreteCategory.hom f.base) ↑x, ⋯⟩)) a) =
    (CategoryTheory.ConcreteCategory.hom (X.evaluation x))
      ((CategoryTheory.ConcreteCategory.hom (f.c.app (Opposite.op V))) a)
-- Mathlib.Topology.Bornology.Absorbs
absorbs_union : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s t₁ t₂ : Set α},
  Absorbs M s (t₁ ∪ t₂) ↔ Absorbs M s t₁ ∧ Absorbs M s t₂
-- Mathlib.Algebra.Order.Star.Basic
star_right_conjugate_pos : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {a : R}, 0 < a → ∀ {c : R}, IsRegular c → 0 < c * a * star c
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.isBoundedUnder_ge_exp_comp : ∀ {α : Type u_1} (l : Filter α) (f : α → ℝ), Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l fun x => Real.exp (f x)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.map_dualCoannihilator : ∀ {K : Type u_4} {V : Type u_5} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (W : Subspace K (Module.Dual K V)) [FiniteDimensional K V],
  Submodule.map (Module.Dual.eval K V) (Submodule.dualCoannihilator W) = Submodule.dualAnnihilator W
-- Init.Data.List.Lemmas
List.map_filterMap_of_inv : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {g : β → α},
  (∀ (x : α), Option.map g (f x) = some x) → ∀ {l : List α}, List.map g (List.filterMap f l) = l
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_eq_right : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P ⊢ₛ Q ↔ Q ⊣⊢ₛ P ∨ Q
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.mem_centralizer_singleton_iff : ∀ {G : Type u_1} [inst : Group G] {g k : G}, k ∈ Subgroup.centralizer {g} ↔ k * g = g * k
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.coe_bracket : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) (x y : ↥L'), ↑⁅x, y⁆ = ⁅↑x, ↑y⁆
-- Std.Sync.Broadcast
/-- Returns true if the buffer contains no elements.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.isEmpty : {m : Type → Type} →
  {α : Type} → [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → Std.AtomicT (Std.Bounded.State✝ α) m Bool
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.CnstrRHS : Type
-- Mathlib.Algebra.Group.Action.Sum
Sum.instMulAction.eq_1 : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} {m : Monoid M} [inst : MulAction M α] [inst_1 : MulAction M β],
  Sum.instMulAction = { toSMul := Sum.instSMul, mul_smul := ⋯, one_smul := ⋯ }
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.instInhabitedCommRing : Inhabited Lean.Meta.Sym.Arith.CommRing
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
/-- The regular topology on any preregular category is subcanonical.  -/
CategoryTheory.regularTopology.subcanonical : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C],
  (CategoryTheory.regularTopology C).Subcanonical
-- Mathlib.Algebra.Polynomial.Div
Polynomial.rootMultiplicity_pos : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R},
  p ≠ 0 → ∀ {x : R}, 0 < Polynomial.rootMultiplicity x p ↔ p.IsRoot x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_eq_get! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)] {h' : a ∈ t}, t.get a h' = t.get! a
-- Mathlib.Analysis.Convex.Basic
mem_convexAddSubmonoid : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, s ∈ convexAddSubmonoid 𝕜 E ↔ Convex 𝕜 s
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of isomorphic additive monoids are isomorphic.  -/
AddSubmonoid.centerCongr : {M : Type u_2} →
  {N : Type u_1} →
    [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M ≃+ N → ↥(AddSubmonoid.center M) ≃+ ↥(AddSubmonoid.center N)
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRightNat_congr : ∀ (n w : ℕ) (x x' : BitVec w), x = x' → x'.sshiftRight n = x.sshiftRight n
-- Mathlib.Algebra.Group.Prod
AddEquiv.prodUnique.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : Unique N],
  AddEquiv.prodUnique = { toEquiv := Equiv.prodUnique M N, map_add' := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Product of affine spaces is associative up to affine isomorphism.  -/
AffineEquiv.prodAssoc : (k : Type u_1) →
  (P₁ : Type u_2) →
    (P₂ : Type u_3) →
      (P₃ : Type u_4) →
        {V₁ : Type u_6} →
          {V₂ : Type u_7} →
            {V₃ : Type u_8} →
              [inst : Ring k] →
                [inst_1 : AddCommGroup V₁] →
                  [inst_2 : AddCommGroup V₂] →
                    [inst_3 : AddCommGroup V₃] →
                      [inst_4 : Module k V₁] →
                        [inst_5 : Module k V₂] →
                          [inst_6 : Module k V₃] →
                            [inst_7 : AddTorsor V₁ P₁] →
                              [inst_8 : AddTorsor V₂ P₂] →
                                [inst_9 : AddTorsor V₃ P₃] → (P₁ × P₂) × P₃ ≃ᵃ[k] P₁ × P₂ × P₃
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Scheme.instFullEtaleOverForget : ∀ (X : AlgebraicGeometry.Scheme), (AlgebraicGeometry.Scheme.Etale.forget X).Full
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The inclusion `Cocycle K L n →+ Cochain K L n`.  -/
CochainComplex.HomComplex.Cocycle.toCochainAddMonoidHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K L : CochainComplex C ℤ) →
        (n : ℤ) → CochainComplex.HomComplex.Cocycle K L n →+ CochainComplex.HomComplex.Cochain K L n
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- In the power series expansion of `℘(z) = ∑ᵢ aᵢ (z - x)ⁱ` at some `x ∉ L`,
each `aᵢ` can be written as a sum over `l ∈ L`, i.e.
`aᵢ = ∑ₗ, (i + 1) * (l - x)⁻ⁱ⁻²` for `i ≠ 0` and `a₀ = ∑ₗ, (l - x)⁻² - l⁻²`.

We show that the double sum converges if `z` falls in a ball centered at `x` that doesn't touch `L`.
 -/
PeriodPair.summable_weierstrassPExceptSummand : ∀ (L : PeriodPair) (l₀ z x : ℂ),
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖) →
    Summable (Function.uncurry fun b c => L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)
-- Mathlib.CategoryTheory.GradedObject.Single
CategoryTheory.GradedObject.singleCompEval_inv_app : ∀ {J : Type u_1} (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasInitial C] [inst_2 : DecidableEq J] (j : J) (X : C),
  (CategoryTheory.GradedObject.singleCompEval C j).inv.app X = (CategoryTheory.GradedObject.singleObjApplyIso j X).inv
-- Mathlib.Tactic.Widget.StringDiagram
/-- The horizontal position of the node in the string diagram, counting strings in codomains.  -/
Mathlib.Tactic.Widget.StringDiagram.AtomNode.hPosTar : Mathlib.Tactic.Widget.StringDiagram.AtomNode → ℕ
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.of_add_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α}, (s + t).Nonempty → s.Nonempty
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The top left map in the oplax associativity hexagon.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPre F) →
                (CategoryTheory.MonoidalCategory.curriedTensorPostPost F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPostPre F)
-- Lean.Expr
/-- Annotate `e` with the given option.
The information is stored using metadata around `e`.
 -/
Lean.Expr.setOption : {α : Type} → Lean.Expr → Lean.Name → [Lean.KVMap.Value α] → α → Lean.Expr
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- If a function `f` is differentiable at `x` with surjective `mfderiv I I' f x` and `x` is an
interior point with respect to `I`, `f x` must be an interior point with respect to `I'`.  -/
MDifferentiableAt.isInteriorPoint_of_surjective_mfderiv : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {f : M → N} {x : M},
  MDiffAt f x → Function.Surjective ⇑(mfderiv% f x) → I.IsInteriorPoint x → I'.IsInteriorPoint (f x)
-- Mathlib.RingTheory.WittVector.Truncated
/-- Given a family `fₖ : S → TruncatedWittVector p k R` and `s : S`, we produce a Witt vector by
defining the `k`th entry to be the final entry of `fₖ s`.
 -/
WittVector.liftFun : {p : ℕ} →
  {R : Type u_1} →
    [inst : CommRing R] →
      [inst_1 : Fact (Nat.Prime p)] →
        {S : Type u_2} → [inst_2 : Semiring S] → ((k : ℕ) → S →+* TruncatedWittVector p k R) → S → WittVector p R
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nsmul_val : ∀ {d : ℤ} (n : ℕ) (x y : ℤ), ↑n * { re := x, im := y } = { re := ↑n * x, im := ↑n * y }