mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.trW_inverseImage_ι_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty 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]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : A.IsTriangulated] {X Y : A.FullSubcategory} (f : X ⟶ Y),
  (B.inverseImage A.ι).trW f ↔ (A ⊓ B).trW f.hom
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.separatingRight_toBilin_iff : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] {ι : Type u_6}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {M : Matrix ι ι R₂} (b : Module.Basis ι R₂ M₂),
  LinearMap.SeparatingRight ((Matrix.toBilin b) M) ↔ M.SeparatingRight
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- Given a cone `c` on a cofiltered diagram `F` which `IsEventuallyConstantTo i₀`, such that
`c.π.app i₀` is an isomorphism, `c` a limit cone.  -/
CategoryTheory.Functor.IsEventuallyConstantTo.isLimitOfIsIso : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {F : CategoryTheory.Functor J C} →
          {i₀ : J} →
            F.IsEventuallyConstantTo i₀ →
              [CategoryTheory.IsCofiltered J] →
                (c : CategoryTheory.Limits.Cone F) →
                  [CategoryTheory.IsIso (c.π.app i₀)] → CategoryTheory.Limits.IsLimit c
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.mem_pullSub_append : ∀ {A : Type u_1} {T : ↥(Descriptive.tree A)} {x y : List A}, x ++ y ∈ Descriptive.Tree.pullSub T x ↔ y ∈ T
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall.eq_1 : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) (x : E) (r : ℝ), p.closedBall x r = {y | p (y - x) ≤ r}
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.mk_coe : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A →ₛₙₐ[φ] B) (h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x)
  (h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0)
  (h₃ :
    ∀ (x y : A),
      { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) =
        { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y)
  (h₄ :
    ∀ (x y : A),
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
        { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
          { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y),
  { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = f
-- Mathlib.Topology.Algebra.Monoid
Subsemigroup.top_closure_mul_self_subset : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Semigroup M] [SeparatelyContinuousMul M] (s : Subsemigroup M),
  closure ↑s * closure ↑s ⊆ closure ↑s
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `dist_eq_norm_sub`. -/
dist_eq_norm : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E), dist a b = ‖a - b‖
-- Mathlib.MeasureTheory.MeasurableSpace.Card
/-- `generateMeasurableRec` is constant for ordinals `≥ ω₁`.  -/
MeasurableSpace.generateMeasurableRec_of_omega_one_le : ∀ {α : Type u} (s : Set (Set α)) {i : Ordinal.{v}},
  Ordinal.omega 1 ≤ i →
    MeasurableSpace.generateMeasurableRec s i = MeasurableSpace.generateMeasurableRec s (Ordinal.omega 1)
-- Init.Data.UInt.Bitwise
UInt8.not_eq_neg_sub : ∀ (a : UInt8), ~~~a = -a - 1
-- Mathlib.Tactic.WithoutCDot
Lean.Elab.Term.withoutCDotImpl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.toLaxMonoidal : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {D : Type u₂} →
        {inst_2 : CategoryTheory.Category.{v₂, u₂} D} →
          {inst_3 : CategoryTheory.MonoidalCategory D} →
            {F : CategoryTheory.Functor C D} → [self : F.Monoidal] → F.LaxMonoidal
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.IsSubDPIdeal.isSubideal : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {J : Ideal A}, hI.IsSubDPIdeal J → J ≤ I
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  CategoryTheory.CategoryStruct.comp S.homologyπ S.moduleCatHomologyIso.hom =
    CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom S.moduleCatLeftHomologyData.π
-- Init.Control.Lawful.Instances
EStateM.run_adaptExcept : ∀ {ε ε' σ α : Type u_1} (f : ε → ε') (x : EStateM ε σ α) (s : σ),
  (EStateM.adaptExcept f x).run s =
    match x.run s with
    | EStateM.Result.ok x s => EStateM.Result.ok x s
    | EStateM.Result.error e s => EStateM.Result.error (f e) s
-- Std.Http.Data.Chunk
/-- Checks if a trailer header with the given name exists.
 -/
Std.Http.Trailer.contains : Std.Http.Trailer → Std.Http.Header.Name → Bool
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
/-- Glue sections of a `Type`-valued sheaf over a `1`-hypercover.  -/
CategoryTheory.PreOneHypercover.IsStronglySheafFor.amalgamate : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : C} →
      {E : CategoryTheory.PreOneHypercover X} →
        {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} →
          E.IsStronglySheafFor F →
            (x : (i : E.I₀) → F.obj (Opposite.op (E.X i))) →
              (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
                  (CategoryTheory.ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) =
                    (CategoryTheory.ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j)) →
                F.obj (Opposite.op X)
-- Mathlib.Data.Fin.SuccPred
Fin.castLE_inj : ∀ {n m : ℕ} {hmn : m ≤ n} {a b : Fin m}, Fin.castLE hmn a = Fin.castLE hmn b ↔ a = b
-- Init.Data.Option.Lemmas
Option.eq_some_of_filter_eq_some : ∀ {α : Type u_1} {p : α → Bool} {o : Option α} {a : α}, Option.filter p o = some a → o = some a
-- Mathlib.GroupTheory.Coset.Basic
MonoidHom.fiberEquiv.eq_1 : ∀ {α : Type u_1} [inst : Group α] {H : Type u_2} [inst_1 : Group H] (f : α →* H) (a b : α),
  f.fiberEquiv a b = (f.fiberEquivKer a).trans (f.fiberEquivKer b).symm
-- Mathlib.CategoryTheory.GuitartExact.Basic
/-- Constructor for objects in `w.CostructuredArrowDownwards g`.  -/
CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        (w : CategoryTheory.TwoSquare T L R B) →
                          {X₂ : C₂} →
                            {X₃ : C₃} →
                              (g : R.obj X₂ ⟶ B.obj X₃) →
                                (X₁ : C₁) →
                                  (a : X₂ ⟶ T.obj X₁) →
                                    (b : L.obj X₁ ⟶ X₃) →
                                      CategoryTheory.CategoryStruct.comp (R.map a)
                                            (CategoryTheory.CategoryStruct.comp (w.app X₁) (B.map b)) =
                                          g →
                                        w.CostructuredArrowDownwards g
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Connected.ofBoxProdRight : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β}, (G □ H).Connected → H.Connected
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- A cubic polynomial whose discriminant is a multiple of the Weierstrass curve discriminant. If
`W` is an elliptic curve over a field `R` of characteristic different from 2, then its roots over a
splitting field of `R` are precisely the `X`-coordinates of the non-zero 2-torsion points of `W`.  -/
WeierstrassCurve.twoTorsionPolynomial : {R : Type u} → [CommRing R] → WeierstrassCurve R → Cubic R
-- Mathlib.Analysis.Convex.Exposed
/-- Exposed points exactly correspond to exposed singletons.  -/
mem_exposedPoints_iff_exposed_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] {A : Set E} {x : E},
  x ∈ Set.exposedPoints 𝕜 A ↔ IsExposed 𝕜 A {x}
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.toPresheafedSpace_obj : ∀ (R : CommRingCatᵒᵖ),
  AlgebraicGeometry.Spec.toPresheafedSpace.obj R =
    (AlgebraicGeometry.Spec.sheafedSpaceObj (Opposite.unop R)).toPresheafedSpace
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.add_comm : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a b : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (a + b) (b + a)
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instMulActionOfUniformContinuousConstSMul : (M : Type v) →
  (X : Type x) →
    [inst : UniformSpace X] →
      [inst_1 : Monoid M] →
        [inst_2 : MulAction M X] → [UniformContinuousConstSMul M X] → MulAction M (UniformSpace.Completion X)
-- Mathlib.Tactic.FunProp.FunctionData
/-- local instances  -/
Mathlib.Meta.FunProp.FunctionData.insts : Mathlib.Meta.FunProp.FunctionData → Lean.LocalInstances
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.update.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R) (x : MonoidAlgebra R M),
  MonoidAlgebra.update m r x = MonoidAlgebra.ofCoeff (x.coeff.update m r)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.contDiff_sinh : ∀ {n : WithTop ℕ∞}, ContDiff ℂ n Complex.sinh
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra}
  (f : A.A ⟶ B.A)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp (T.map f) B.a = CategoryTheory.CategoryStruct.comp A.a f)
      CategoryTheory.Monad.Algebra.Hom.h._autoParam)
  (f_1 : A.A ⟶ B.A)
  (h_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (T.map f_1) B.a = CategoryTheory.CategoryStruct.comp A.a f_1)
      CategoryTheory.Monad.Algebra.Hom.h._autoParam),
  ({ f := f, h := h } = { f := f_1, h := h_1 }) = (f = f_1)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_union_loops_eq : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.closure (X ∪ M.loops) = M.closure X
-- Batteries.Recycling.MonadSatisfying.Array
Array.SatisfiesM_mapFinIdxM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {as : Array α}
  {f : (i : ℕ) → α → i < as.size → m β} {motive : ℕ → Prop} {p : (i : ℕ) → β → i < as.size → Prop},
  motive 0 →
    (∀ (i : ℕ) (h : i < as.size), motive i → SatisfiesM (fun x => p i x h ∧ motive (i + 1)) (f i as[i] h)) →
      SatisfiesM (fun arr => motive as.size ∧ ∃ (eq : arr.size = as.size), ∀ (i : ℕ) (h : i < as.size), p i arr[i] h)
        (as.mapFinIdxM f)
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.move.eq_1 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (a : Γ) (L R : Turing.ListBlank Γ),
  Turing.Tape.move Turing.Dir.left { head := a, left := L, right := R } =
    { head := L.head, left := L.tail, right := Turing.ListBlank.cons a R }
-- Mathlib.Data.Stream.Init
Stream'.get_drop : ∀ {α : Type u} (n m : ℕ) (s : Stream' α), (Stream'.drop m s).get n = s.get (m + n)
-- Mathlib.Order.CompleteLattice.Basic
Antitone.map_iSup_le : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice α] {s : ι → α} [inst_1 : CompleteLattice β]
  {f : α → β}, Antitone f → f (iSup s) ≤ ⨅ i, f (s i)
-- Mathlib.Algebra.Group.Defs
isAddTorsionFree_iff : ∀ (M : Type u_2) [inst : AddMonoid M], IsAddTorsionFree M ↔ ∀ ⦃n : ℕ⦄, n ≠ 0 → Function.Injective fun a => n • a
-- Mathlib.Algebra.RingQuot
RingQuot.mkAlgHom_rel : ∀ (S : Type uS) [inst : CommSemiring S] {A : Type uA} [inst_1 : Semiring A] [inst_2 : Algebra S A] {s : A → A → Prop}
  {x y : A}, s x y → (RingQuot.mkAlgHom S s) x = (RingQuot.mkAlgHom S s) y
-- Lean.Meta.Match.MatcherApp.Transform
/-- Discriminant equation fvars from the matcher's own type (`numDiscrEqs`).  -/
Lean.Meta.MatcherApp.TransformAltFVars.discrEqs : Lean.Meta.MatcherApp.TransformAltFVars → Array Lean.Expr
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.comp_symm_eq : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {α : Type u_9} (e : M ≃* N) (f : N → α) (g : M → α),
  g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
-- Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerLeft : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) {Y Z : C} (f : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f =
    CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) f
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- Eta-expanded form of `UniformContinuousOn.inv₀` -/
UniformContinuousOn.fun_inv₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} [inst_1 : UniformSpace X] {f : X → α} {s : Set X},
  UniformContinuousOn f s → (f '' s)ᶜ ∈ nhds 0 → UniformContinuousOn (fun i => (f i)⁻¹) s
-- Mathlib.Topology.ClusterPt
mapClusterPt_def : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X},
  MapClusterPt x F u ↔ ClusterPt x (Filter.map u F)
-- Mathlib.Order.TypeTags
_private.Mathlib.Order.TypeTags.0.WithBot.instRepr.match_1.eq_2 : ∀ {α : Type u_1} (motive : WithBot α → Sort u_2) (a : α) (h_1 : Unit → motive none) (h_2 : (a : α) → motive (some a)),
  (match some a with
    | none => h_1 ()
    | some a => h_2 a) =
    h_2 a
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.chaar.congr_simp : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  (K₀ K₀_1 : TopologicalSpace.PositiveCompacts G),
  K₀ = K₀_1 →
    ∀ (K K_1 : TopologicalSpace.Compacts G),
      K = K_1 → MeasureTheory.Measure.haar.chaar K₀ K = MeasureTheory.Measure.haar.chaar K₀_1 K_1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry!.eq_3 : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited ((a : α) × β a)] (size : ℕ) (k : α) (v : β k)
  (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l_1 r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).maxEntry! =
    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxEntry!
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- A comonad in `B` defines an oplax functor from the trivial bicategory to `B`.  -/
CategoryTheory.Bicategory.Comonad.toOplax : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a : B} →
      (t : a ⟶ a) →
        [CategoryTheory.Bicategory.Comonad t] →
          CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Discrete Unit)) B
-- Mathlib.Topology.Continuous
continuous_iff_isClosed : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f ↔ ∀ (s : Set Y), IsClosed s → IsClosed (f ⁻¹' s)
-- Mathlib.Logic.Equiv.Fin.Basic
/-- The space of functions `Fin 2 → α` is equivalent to `α × α`. See also `piFinTwoEquiv` and
`prodEquivPiFinTwo`.  -/
finTwoArrowEquiv : (α : Type u_1) → (Fin 2 → α) ≃ α × α
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.EqnInfo.mk.injEq : ∀ (declName : Lean.Name) (levelParams : List Lean.Name) (type value : Lean.Expr) (recArgPos : ℕ)
  (declNames : Array Lean.Name) (fixedParamPerms : Lean.Elab.FixedParamPerms) (declName_1 : Lean.Name)
  (levelParams_1 : List Lean.Name) (type_1 value_1 : Lean.Expr) (recArgPos_1 : ℕ) (declNames_1 : Array Lean.Name)
  (fixedParamPerms_1 : Lean.Elab.FixedParamPerms),
  ({ declName := declName, levelParams := levelParams, type := type, value := value, recArgPos := recArgPos,
        declNames := declNames, fixedParamPerms := fixedParamPerms } =
      { declName := declName_1, levelParams := levelParams_1, type := type_1, value := value_1,
        recArgPos := recArgPos_1, declNames := declNames_1, fixedParamPerms := fixedParamPerms_1 }) =
    (declName = declName_1 ∧
      levelParams = levelParams_1 ∧
        type = type_1 ∧
          value = value_1 ∧ recArgPos = recArgPos_1 ∧ declNames = declNames_1 ∧ fixedParamPerms = fixedParamPerms_1)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RicSliceData.mk.sizeOf_spec : ∀ {α : Type u} [inst : Ord α] [inst_1 : SizeOf α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit)
  (range : Std.Ric α), sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.Topology.Algebra.Group.Basic
ContinuousAt.fun_zsmul : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G} {x : α}, ContinuousAt f x → ∀ (z : ℤ), ContinuousAt (fun i => z • f i) x
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorCompIsoId.congr_simp : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (i j : A) (h : i + j = 0),
  CategoryTheory.shiftFunctorCompIsoId C i j h = CategoryTheory.shiftFunctorCompIsoId C i j h
-- Mathlib.Topology.Separation.Hausdorff
/-- If two continuous maps are equal on `s`, then they are equal on the closure of `s`. See also
`Set.EqOn.of_subset_closure` for a more general version.  -/
Set.EqOn.closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space X] {s : Set Y}
  {f g : Y → X}, Set.EqOn f g s → Continuous f → Continuous g → Set.EqOn f g (closure s)
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.exists_iff_exists_existsUnique : ∀ {G : Type u_1} [inst : Mul G] {A B : Finset G},
  (∃ a0 b0, a0 ∈ A ∧ b0 ∈ B ∧ UniqueMul A B a0 b0) ↔ ∃ g, ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = g
-- Init.Data.Array.DecidableEq
List.isEqv_toArray : ∀ {α : Type u_1} {r : α → α → Bool} [BEq α] (as bs : List α), as.toArray.isEqv bs.toArray r = as.isEqv bs r
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- **Alias** of `FractionalIdeal.one_le_extendedHom_iff`. -/
FractionalIdeal.one_le_extendedHomₐ_iff : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [inst_12 : Algebra K L]
  [inst_13 : Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain A]
  [IsDedekindDomain B], I ≠ 0 → (1 ≤ (FractionalIdeal.extendedHom L B) I ↔ 1 ≤ I)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_Iio_eq_bsup : ∀ {o : Ordinal.{u_3}} {f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}}, ⨆ a, f ↑a ⋯ = o.bsup f
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.min?.eq_1 : ∀ {α : Type u_1}, RBTree.RBNode.nil.min? = none
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.uncurryObjFlip_hom_app : ∀ {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]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : D × C),
  F.uncurryObjFlip.hom.app X = CategoryTheory.CategoryStruct.id ((F.obj X.2).obj X.1)
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- The algebra equivalence between `AddMonoidAlgebra` and `MonoidAlgebra` in terms of
`Multiplicative`.  -/
AddMonoidAlgebra.toMultiplicativeAlgEquiv : (R : Type u_1) →
  (A : Type u_4) →
    (M : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddMonoid M] → AddMonoidAlgebra A M ≃ₐ[R] MonoidAlgebra A (Multiplicative M)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.exists_fixed_point_of_contractible : ∀ {α : Type u_1} {β : Type u_2} (F : UniformFun β (Stream'.Seq α) → UniformFun β (Stream'.Seq α)),
  LipschitzWith 2⁻¹ F → ∃ f, Function.IsFixedPt F f
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.prodMap_apply : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7}
  {V4 : Type u_8} {P4 : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2]
  [inst_7 : AddCommGroup V3] [inst_8 : Module k V3] [inst_9 : AddTorsor V3 P3] [inst_10 : AddCommGroup V4]
  [inst_11 : Module k V4] [inst_12 : AddTorsor V4 P4] (f : P1 →ᵃ[k] P2) (g : P3 →ᵃ[k] P4) (x : P1 × P3),
  (f.prodMap g) x = (f x.1, g x.2)
-- Mathlib.Algebra.Group.Invertible.Basic
/-- Units are invertible in their associated monoid.  -/
Units.invertible : {α : Type u} → [inst : Monoid α] → (u : αˣ) → Invertible ↑u
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- A bialgebra homomorphism `R[G] → R[H]` between group algebras over a domain `R` comes from a
group hom `G → H`.

See `MonoidAlgebra.mapDomainBialgHom` for the forward map.  -/
MonoidAlgebra.mapDomainOfBialgHom : {R : Type u_1} →
  {G : Type u_5} →
    {H : Type u_6} →
      [inst : CommRing R] →
        [IsDomain R] → [inst_2 : Group G] → [inst_3 : Group H] → (MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H) → G →* H
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getKey.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : Std.DHashMap.Internal.AssocList α β)
  (x_1 : Std.DHashMap.Internal.AssocList.contains a x = true),
  Std.DHashMap.Internal.AssocList.getKey a x x_1 =
    match x, x_1 with
    | Std.DHashMap.Internal.AssocList.cons k value es, h =>
      if hka : (k == a) = true then k else Std.DHashMap.Internal.AssocList.getKey a es ⋯
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SavedState.mk : Lean.Elab.Term.SavedState → Lean.Elab.Tactic.Grind.State → Lean.Elab.Tactic.Grind.SavedState
-- Lean.CoreM
Lean.instMonadRuntimeExceptionCoreM : Lean.MonadRuntimeException Lean.CoreM
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ιMulti_succ_apply : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  (v : Fin n.succ → M),
  (ExteriorAlgebra.ιMulti R n.succ) v = (ExteriorAlgebra.ι R) (v 0) * (ExteriorAlgebra.ιMulti R n) (Matrix.vecTail v)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldlM_eq_foldlM_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ},
  Std.DTreeMap.foldlM (fun d a x => f d a) init t = Array.foldlM f init t.keysArray
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsAddCyclic.exponent_eq_zero_of_infinite : ∀ {α : Type u_1} [inst : AddGroup α] [IsAddCyclic α] [Infinite α], AddMonoid.exponent α = 0
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrLeft.eq_1 : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [inst : AddZeroClass M₁] [inst_1 : AddZeroClass M₂]
  [inst_2 : AddCommMonoid N] (e : M₁ ≃+ M₂),
  e.addMonoidHomCongrLeft = { toEquiv := e.addMonoidHomCongrLeftEquiv, map_add' := ⋯ }