mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Side
AffineSubspace.setOfPred_sSameSide_eq_image2 : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x p : P},
  x ∉ s → p ∈ s → {y | s.SSameSide x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instSemigroup : {α : Type u_1} → [Semigroup α] → Semigroup (Lex α)
-- Std.Data.ExtHashSet.Basic
/-- Removes the element if it exists.  -/
Std.ExtHashSet.erase : {α : Type u} →
  {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashSet α → α → Std.ExtHashSet α
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.leftQuotientEquiv_apply : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {f : G ⧸ H → G} (hf : ∀ (q : G ⧸ H), ↑(f q) = q) (q : G ⧸ H),
  ↑(⋯.leftQuotientEquiv q) = f q
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.insert.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a),
  m.insert a b = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.insert ⟨m, h⟩ a b) else m
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
/-- If `I` is initial, then `I ⨯ X` is isomorphic to it.  -/
CategoryTheory.Limits.isInitialMul : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasStrictInitialObjects C] →
      {I : C} →
        (X : C) →
          [inst_2 : CategoryTheory.Limits.HasBinaryProduct I X] → CategoryTheory.Limits.IsInitial I → (I ⨯ X ≅ I)
-- Mathlib.Algebra.Module.Torsion.Basic
/-- An `(R ⧸ Ideal.span {r})`-module is an `R`-module for which `IsTorsionBy R M r`.  -/
Module.IsTorsionBy.module : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {r : R} → [h : (Ideal.span {r}).IsTwoSided] → Module.IsTorsionBy R M r → Module (R ⧸ Ideal.span {r}) M
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.ofHom_hom : ∀ {X Y : Semigrp} (f : X ⟶ Y), Semigrp.ofHom (Semigrp.Hom.hom f) = f
-- Mathlib.Order.CompleteBooleanAlgebra
sSup_symmDiff_sSup_le : ∀ {α : Type u} [inst : CompleteBooleanAlgebra α] {s t : Set α},
  s.Nonempty → t.Nonempty → symmDiff (sSup s) (sSup t) ≤ sSup (Set.image2 (fun x1 x2 => symmDiff x1 x2) s t)
-- Lean.LocalContext
Lean.LocalDecl.setBinderInfo : Lean.LocalDecl → Lean.BinderInfo → Lean.LocalDecl
-- Batteries.Data.HashMap.Basic
/-- The inner `Std.HashMap` powering the `Batteries.HashMap`.  -/
Batteries.HashMap.inner : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Batteries.HashMap α β → Std.HashMap α β
-- Mathlib.Order.Lattice
/-- The supremum is an upper bound on the second argument  -/
SemilatticeSup.le_sup_right : ∀ {α : Type u} [self : SemilatticeSup α] (a b : α), b ≤ SemilatticeSup.sup a b
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- Auxiliary definition for `MonOpOpToComonObj`.  -/
CategoryTheory.Comon.MonOpOpToComonObjComon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : CategoryTheory.Mon Cᵒᵖ) → CategoryTheory.ComonObj (Opposite.unop A.X)
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.ext_iff : ∀ {α : Sort u_1} {β : Sort u_2} {f g : α ↪ β}, f = g ↔ ∀ (x : α), f x = g x
-- Init.Data.String.Lemmas.Slice
String.Slice.Pos.get?_eq_none_iff : ∀ {s : String.Slice} {p : s.Pos}, p.get? = none ↔ p = s.endPos
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmooth.baseChange : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_1)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Algebra.IsStandardSmooth R S],
  Algebra.IsStandardSmooth T (TensorProduct R T S)
-- Mathlib.CategoryTheory.Localization.Preadditive
CategoryTheory.Localization.liftNatTrans_add : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : CategoryTheory.Preadditive E] (F₁ F₂ : CategoryTheory.Functor C E) (F₁' F₂' : CategoryTheory.Functor D E)
  [inst_5 : CategoryTheory.Localization.Lifting L W F₁ F₁'] [inst_6 : CategoryTheory.Localization.Lifting L W F₂ F₂']
  (τ τ' : F₁ ⟶ F₂),
  CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' (τ + τ') =
    CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ +
      CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ'
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- `tilde.isoTop` bundled as a natural isomorphism.
This is the unit of the tilde-Gamma adjunction.  -/
AlgebraicGeometry.tilde.toTildeΓNatIso : {R : CommRingCat} →
  CategoryTheory.Functor.id (ModuleCat ↑R) ≅
    (AlgebraicGeometry.tilde.functor R).comp AlgebraicGeometry.moduleSpecΓFunctor
-- Lean.Environment
/-- Constructs a DefinitionVal, inferring the `unsafe` field  -/
Lean.mkDefinitionValInferringUnsafe : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      Lean.Name → List Lean.Name → Lean.Expr → Lean.Expr → Lean.ReducibilityHints → m Lean.DefinitionVal
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- An additive monoid object internal to a monoidal category.  -/
CategoryTheory.AddMonObj : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.MonoidalCategory C] → C → Type v₁
-- Mathlib.Algebra.Lie.Basic
LieEquiv.toLinearEquiv_injective : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂], Function.Injective LieEquiv.toLinearEquiv
-- Mathlib.Algebra.Order.GroupWithZero.Defs
le_of_mul_le_mul_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [MulPosReflectLE α],
  b * a ≤ c * a → 0 < a → b ≤ c
-- Lean.MetavarContext
Lean.MetavarContext.mkBinding : Bool →
  Array Lean.Expr →
    Lean.Expr →
      optParam Bool false →
        optParam Bool true →
          optParam Bool false →
            optParam Bool true →
              optParam Lean.BinderInfo Lean.BinderInfo.implicit → Lean.MetavarContext.MkBindingM Lean.Expr
-- Mathlib.Analysis.Seminorm
Seminorm.ball_zero_eq : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) {r : ℝ}, p.ball 0 r = {y | p y < r}
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabDescr.mkInductiveView : Lean.Elab.Command.InductiveElabDescr →
  Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep1
-- Init.Data.Nat.Div.Lemmas
Nat.le_mul_iff_le_right : ∀ {y x z : ℕ}, 0 < y → (x ≤ y * z ↔ (x + y - 1) / y ≤ z)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The composition of two pullback functors for sheaves of modules on schemes
identify to the pullback for the composition.  -/
AlgebraicGeometry.Scheme.Modules.pullbackComp : {X Y Z : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (g : Y ⟶ Z) →
      (AlgebraicGeometry.Scheme.Modules.pullback g).comp (AlgebraicGeometry.Scheme.Modules.pullback f) ≅
        AlgebraicGeometry.Scheme.Modules.pullback (CategoryTheory.CategoryStruct.comp f g)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonServerCapabilities : Lean.FromJson Lean.Lsp.ServerCapabilities
-- Mathlib.Analysis.Normed.Group.Real
Real.nnnorm_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ‖OfNat.ofNat n‖₊ = OfNat.ofNat n
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Icc_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Icc a b)), Subtype.val '' Set.Ioi c = Set.Ioc (↑c) b
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheckIdent : Lean.Elab.Term.Quotation.Precheck
-- Lean.Meta.Tactic.Contradiction
_private.Lean.Meta.Tactic.Contradiction.0.Lean.Meta.mkGenDiseqMask.go : Lean.Expr → Array Bool → Array Bool
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_one_div_cancel : ∀ {α : Type u} [inst : DivisionMonoid α] {a : α}, IsUnit a → a * (1 / a) = 1
-- Mathlib.Analysis.Calculus.Deriv.Add
hasDerivAt_neg' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), HasDerivAt (fun x => -x) (-1) x
-- Init.Meta
/-- `simp_arith!` has been deprecated. It was a shorthand for `simp! +arith +decide`.
Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
 -/
Lean.Parser.Tactic.simpArithBang : Lean.ParserDescr
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.coe_emptySum : ∀ (X : Type u) (Y : Type v) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : IsEmpty Y],
  (Homeomorph.emptySum X Y).toEquiv = Equiv.emptySum Y X
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.PosDef.le_zero_iff : ∀ {M : Type u_4} {N : Type u_5} {R₂ : Type u} [inst : CommSemiring R₂] [inst_1 : AddCommMonoid M] [inst_2 : Module R₂ M]
  [inst_3 : PartialOrder N] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {Q : QuadraticMap R₂ M N},
  Q.PosDef → ∀ {x : M}, Q x ≤ 0 ↔ x = 0
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.instIsIsoCommRingCatStalkMapFromGlued : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : ↥(AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).glued),
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap (AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰) x)
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Coframe.toDistribLattice : {α : Type u} → [Order.Coframe α] → DistribLattice α
-- Mathlib.Data.Sym.Sym2
Sym2.eq_iff : ∀ {α : Type u_1} {x y z w : α}, s(x, y) = s(z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
-- Qq.AssertInstancesCommute
Qq.Impl.findRedundantLocalInstQuoted? : Lean.Elab.TermElabM (Option (Lean.FVarId × (u : Q(Lean.Level)) × (ty : Q(Q(Sort «$u»))) × Q(Q(«$$ty»)) × Q(Q(«$$ty»))))
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instToJsonDidCloseTextDocumentParams : Lean.ToJson Lean.Lsp.DidCloseTextDocumentParams
-- Mathlib.ModelTheory.Order
FirstOrder.Language.OrderedStructure.mk : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : LE M] [inst_2 : L.Structure M],
  (∀ (x : Fin 2 → M), FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb x ↔ x 0 ≤ x 1) →
    L.OrderedStructure M
-- Mathlib.CategoryTheory.EffectiveEpi.Comp
CategoryTheory.IsSplitEpi.EffectiveEpi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B X : C} (f : X ⟶ B) [CategoryTheory.IsSplitEpi f],
  CategoryTheory.EffectiveEpi f
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (r : R) (k : ℕ),
  (Polynomial.monomial n) r ^ k = (Polynomial.monomial (n * k)) (r ^ k)
-- Lean.Expr
Lean.Int.mkType : Lean.Expr
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_mul : ∀ {K : Type u_1} [inst : RCLike K] (z : K), (starRingEnd K) z * z = ↑‖z‖ ^ 2
-- Lean.Data.Json.Basic
Lean.Json.obj.injEq : ∀ (kvPairs kvPairs_1 : Std.TreeMap.Raw String Lean.Json compare),
  (Lean.Json.obj kvPairs = Lean.Json.obj kvPairs_1) = (kvPairs = kvPairs_1)
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Submodule.IsPrincipal.contentIdeal_le_span_iff_dvd : ∀ {R : Type u_3} [inst : CommSemiring R] {p : Polynomial R},
  Submodule.IsPrincipal p.contentIdeal → ∀ (r : R), p.contentIdeal ≤ Ideal.span {r} ↔ Polynomial.C r ∣ p
-- Mathlib.Order.Category.PartOrd
/-- The category of partial orders.  -/
PartOrd : Type (u_1 + 1)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- If the first and second components of a morphism of distinguished triangles are
isomorphisms, the third component is as well. This can be thought of as a
pretriangulated category theoretical version of the five lemma.  -/
CategoryTheory.Pretriangulated.isIso₃_of_isIso₁₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  {T T' : CategoryTheory.Pretriangulated.Triangle C} (φ : T ⟶ T'),
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
      CategoryTheory.IsIso φ.hom₁ → CategoryTheory.IsIso φ.hom₂ → CategoryTheory.IsIso φ.hom₃
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcompose₂_obj_left : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor H D')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)),
  ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj X).left = X.left
-- Lean.Environment
/-- Create `OLeanEntries` with the same value for all levels.  -/
Lean.OLeanEntries.uniform : {α : Type} → α → Lean.OLeanEntries α
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.quotientToEndObjectHom.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (V : OpenSubgroup (CategoryTheory.Aut F)) {U : OpenSubgroup (CategoryTheory.Aut F)} (h : (↑U).Normal) {A : C}
  (u :
    (CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑U))),
  CategoryTheory.PreGaloisCategory.quotientToEndObjectHom✝ V h u =
    (((CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
                      (CategoryTheory.PreGaloisCategory.functorToAction F)).mulEquivEnd
                  A).trans
              u.conj).symm.toMonoidHom.comp
      (Action.FintypeCat.quotientToEndHom ↑V ↑U)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.ctor.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {i : Lean.Compiler.LCNF.CtorInfo} {args : Array (Lean.Compiler.LCNF.Arg pu)}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_5}
  {i_1 : Lean.Compiler.LCNF.CtorInfo} {args_1 : Array (Lean.Compiler.LCNF.Arg pu)}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_5},
  Lean.Compiler.LCNF.LetValue.ctor i args h = Lean.Compiler.LCNF.LetValue.ctor i_1 args_1 h_1 → i = i_1 ∧ args = args_1
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.adjoinRootAlgEquiv_apply_eq_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) (a : AdjoinRoot f), h.adjoinRootAlgEquiv a = h.map ⋯.choose
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : β}, k ∉ t₂ → Std.DTreeMap.Const.getD (t₁ \ t₂) k fallback = Std.DTreeMap.Const.getD t₁ k fallback
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instCanLiftSetCoeIsCompact : ∀ {α : Type u_1} [inst : TopologicalSpace α], CanLift (Set α) (TopologicalSpace.Compacts α) SetLike.coe IsCompact
-- Mathlib.Analysis.Normed.Group.Indicator
enorm_indicator_le_of_subset : ∀ {α : Type u_1} {ε : Type u_2} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {s t : Set α},
  s ⊆ t → ∀ (f : α → ε) (a : α), ‖s.indicator f a‖ₑ ≤ ‖t.indicator f a‖ₑ
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.counit_comul : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.ComonObj X],
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ComonObj.counit X) =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
-- Mathlib.Order.SymmDiff
top_bihimp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a : α), bihimp ⊤ a = a
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.fixedPoints.iterateChain.congr_simp : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] (f f_1 : α →o α) (e_f : f = f_1) (x x_1 : α) (e_x : x = x_1)
  (h : x ≤ f x),
  OmegaCompletePartialOrder.fixedPoints.iterateChain f x h =
    OmegaCompletePartialOrder.fixedPoints.iterateChain f_1 x_1 ⋯
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- **Alias** of `PowerSeries.weierstrassMod_zero_right`. -/
PowerSeries.weierstrassMod_zero : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f : PowerSeries A)
  [inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A], f %ʷ 0 = 0
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- `comp p`, regarded as a ring homomorphism from `R[X]` to itself.  -/
Polynomial.compRingHom : {R : Type u} → [inst : CommSemiring R] → Polynomial R → Polynomial R →+* Polynomial R
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opSymm_X : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V c.symm) (i : ι),
  X.opSymm.X i = Opposite.op (X.X i)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Ici : Lean.Term → BigOperators.FinsetResult✝
-- Mathlib.Data.List.Sigma
List.mem_ext : ∀ {α : Type u} {β : α → Type v} {l₀ l₁ : List (Sigma β)},
  l₀.Nodup → l₁.Nodup → (∀ (x : Sigma β), x ∈ l₀ ↔ x ∈ l₁) → l₀.Perm l₁
-- Init.Data.Vector.Basic
Vector.findSomeM? : {m : Type u_1 → Type u_2} →
  {α : Type u_3} → {β : Type u_1} → {n : ℕ} → [Monad m] → (α → m (Option β)) → Vector α n → m (Option β)
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Slice.Pos.nextn.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Computability.Reduce
ManyOneEquiv.congr_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, ManyOneEquiv p q → (ManyOneEquiv p r ↔ ManyOneEquiv q r)
-- Mathlib.Topology.MetricSpace.Algebra
/-- Mixin typeclass on a scalar action of a metric space `α` on a metric space `β` both with
distinguished points `0`, requiring compatibility of the action in the sense that
`dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂` and
`dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0`.

If `[NormedDivisionRing α] [SeminormedAddCommGroup β] [Module α β]` are assumed, then prefer writing
`[NormSMulClass α β]` instead of using `[IsBoundedSMul α β]`, since while equivalent, typeclass
search can only infer the latter from the former and not vice versa.  -/
IsBoundedSMul : (α : Type u_1) →
  (β : Type u_2) → [PseudoMetricSpace α] → [PseudoMetricSpace β] → [Zero α] → [Zero β] → [SMul α β] → Prop
-- Lean.Meta.Tactic.LibrarySearch
/-- Returns true if this is an abort speculation exception.  -/
Lean.Meta.LibrarySearch.isAbortSpeculation : Lean.Exception → Bool
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
BoundedVariationOn.continuousWithinAt_variationOnFromTo_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E}
  [inst_2 : TopologicalSpace α] [OrderTopology α],
  BoundedVariationOn f Set.univ →
    ∀ {a x : α}, ContinuousWithinAt f (Set.Ici x) x → ContinuousWithinAt (variationOnFromTo f Set.univ a) (Set.Ici x) x
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.preservesFiniteLimits_of_createsFiniteLimits_and_hasFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.CreatesFiniteLimits F]
  [CategoryTheory.Limits.HasFiniteLimits D], CategoryTheory.Limits.PreservesFiniteLimits F
-- Mathlib.Computability.NFA
DFA.toNFA_evalFrom_match : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) (start : σ) (s : List α), M.toNFA.evalFrom {start} s = {M.evalFrom start s}
-- Mathlib.Order.CompleteLattice.Finset
Finset.iInf_option_toFinset : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] (o : Option α) (f : α → β),
  ⨅ x ∈ o.toFinset, f x = ⨅ x ∈ o, f x
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientMapAddSubgroupOfOfLe.eq_1 : ∀ {G : Type u} [inst : AddGroup G] {A' A B' B : AddSubgroup G} [_hAN : (A'.addSubgroupOf A).Normal]
  [_hBN : (B'.addSubgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B),
  QuotientAddGroup.quotientMapAddSubgroupOfOfLe h' h =
    QuotientAddGroup.map (A'.addSubgroupOf A) (B'.addSubgroupOf B) (AddSubgroup.inclusion h) ⋯
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_finset_sup : ∀ {ι : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] (f : ι → TopologicalSpace.Opens α) (s : Finset ι),
  ↑(s.sup f) = s.sup (SetLike.coe ∘ f)
-- Mathlib.Algebra.Star.SelfAdjoint
isSelfAdjoint_iff : ∀ {R : Type u_1} [inst : Star R] {x : R}, IsSelfAdjoint x ↔ star x = x
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffOn_pi_space : ∀ {𝕜 : 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] {s : Set M} {n : WithTop ℕ∞} {ι : Type u_16}
  [inst_6 : Fintype ι] {Fi : ι → Type u_17} [inst_7 : (i : ι) → NormedAddCommGroup (Fi i)]
  [inst_8 : (i : ι) → NormedSpace 𝕜 (Fi i)] {φ : M → (i : ι) → Fi i},
  ContMDiffOn I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) n φ s ↔
    ∀ (i : ι), ContMDiffOn I (modelWithCornersSelf 𝕜 (Fi i)) n (fun x => φ x i) s
-- Init.Prelude
Array.extract.loop : {α : Type u_1} → Array α → ℕ → ℕ → Array α → Array α
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.toAddSubmonoid_injective : ∀ {R : Type u} [inst : NonAssocSemiring R], Function.Injective Subsemiring.toAddSubmonoid
-- Mathlib.InformationTheory.Coding.KraftMcMillan
/-- For uniquely decodable codes, the concatenation map is injective.

This is the key property: distinct tuples of codewords produce distinct concatenations.  -/
_private.Mathlib.InformationTheory.Coding.KraftMcMillan.0.InformationTheory.concatFn_injective_of_uniquelyDecodable : ∀ {α : Type u_1} {S : Finset (List α)},
  InformationTheory.UniquelyDecodable ↑S → ∀ (r : ℕ), Function.Injective InformationTheory.concatFn✝
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
/-- Name of the recursive data type. Assumes that it is not one of the auxiliary ones.
 -/
Lean.Elab.Structural.RecArgInfo.indName! : Lean.Elab.Structural.RecArgInfo → Lean.Name
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
/-- Interpret an `AddMonoidAlgebra` as a homogeneous `DirectSum`.  -/
AddMonoidAlgebra.toDirectSum : {ι : Type u_1} → {M : Type u_3} → [inst : Semiring M] → AddMonoidAlgebra M ι → DirectSum ι fun x => M
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedMor₂Iso.default : Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between a vector and the negation of another vector.  -/
InnerProductGeometry.angle_neg_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  InnerProductGeometry.angle x (-y) = Real.pi - InnerProductGeometry.angle x y