mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.of_map_of_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f g) F] [F.Faithful],
  CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i) → CategoryTheory.IsPushout f g h i
-- Mathlib.CategoryTheory.Abelian.Basic
/-- The cofork induced by the canonical map `Y ⊞ Z ⟶ pushout f g` is in fact a colimit cokernel
cofork.  -/
CategoryTheory.Abelian.BiproductToPushoutIsCokernel.isColimitBiproductToPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.Limits.HasPushouts C] →
        {X Y Z : C} →
          (f : X ⟶ Y) →
            (g : X ⟶ Z) →
              CategoryTheory.Limits.IsColimit
                (CategoryTheory.Abelian.BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Icc_add_Ico_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [AddLeftStrictMono α]
  [AddRightStrictMono α] [inst_5 : LocallyFiniteOrder α] (a b c d : α),
  Finset.Icc a b + Finset.Ico c d ⊆ Finset.Ico (a + c) (b + d)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoRightHomology_hom_inv_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] (hg : S.g = 0) {Z : C} (h : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.opcyclesIsoRightHomology hg).hom
      (CategoryTheory.CategoryStruct.comp S.rightHomologyι h) =
    h
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
/-- The type of cohomology classes of degree `n` in the complex of morphisms
from `K` to `L`.  -/
CochainComplex.HomComplex.CohomologyClass : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CochainComplex C ℤ → CochainComplex C ℤ → ℤ → Type v
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m m_1 : Std.DHashMap.Internal.Raw₀ α β)
  (e_m : m = m_1) (a a_1 : α) (e_a : a = a_1) (hma : m.contains a = true), m.getKey a hma = m_1.getKey a_1 ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
_private.Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree.0.WeierstrassCurve.expCoeff_rec : ∀ (m : ℕ),
  WeierstrassCurve.expCoeff✝ (2 * (m + 3)) =
      WeierstrassCurve.expCoeff✝ (m + 2) ^ 2 * WeierstrassCurve.expCoeff✝ (m + 3) * WeierstrassCurve.expCoeff✝ (m + 5) -
        WeierstrassCurve.expCoeff✝ (m + 1) * WeierstrassCurve.expCoeff✝ (m + 3) *
          WeierstrassCurve.expCoeff✝ (m + 4) ^ 2 ∧
    WeierstrassCurve.expCoeff✝ (2 * (m + 2) + 1) =
      (WeierstrassCurve.expCoeff✝ (m + 4) * WeierstrassCurve.expCoeff✝ (m + 2) ^ 3 * if Even m then 4 ^ 2 else 1) -
        WeierstrassCurve.expCoeff✝ (m + 1) * WeierstrassCurve.expCoeff✝ (m + 3) ^ 3 * if Even m then 1 else 4 ^ 2
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.ker_incl : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  I.incl.ker = ⊥
-- Mathlib.Logic.Function.Basic
Function.const_inj : ∀ {α : Sort u_1} {β : Sort u_2} [Nonempty α] {y₁ y₂ : β}, Function.const α y₁ = Function.const α y₂ ↔ y₁ = y₂
-- Init.Data.Ord.Basic
Ordering.isLT_lt : Ordering.lt.isLT = true
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
/-- Given the set `i`, if `i` is not negative, `findExistsOneDivLT s i` is the
least natural number `n` such that `ExistsOneDivLT s i n`, otherwise, it returns 0.  -/
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.findExistsOneDivLT : {α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.SignedMeasure α → Set α → ℕ
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F H G : CategoryTheory.Functor C V}
  [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  (ℌ :
    CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H)
  (c j : C),
  CategoryTheory.CategoryStruct.comp (ℌ.coev_app.app c) (ℌ.π c j) =
    CategoryTheory.MonoidalClosed.curry ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (j, c))
-- Std.Time.Duration
Std.Time.Duration.instHSubOffset_3 : HSub Std.Time.Duration Std.Time.Minute.Offset Std.Time.Duration
-- Mathlib.Data.Erased
Erased.bind_eq_out : ∀ {α : Sort u_1} {β : Sort u_2} (a : Erased α) (f : α → Erased β), a.bind f = f a.out
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.mk : ℕ →
  List Lean.Elab.Tactic.Omega.Fact →
    List (Lean.Elab.Tactic.Omega.Fact × ℤ) →
      List (Lean.Elab.Tactic.Omega.Fact × ℤ) → Bool → Bool → Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (motive : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput aig w → Sort u_1) (lhs : aig.RefVec w)
  (bit : aig.Ref) (h_1 : (lhs : aig.RefVec w) → (bit : aig.Ref) → motive { lhs := lhs, bit := bit }),
  (match { lhs := lhs, bit := bit } with
    | { lhs := lhs, bit := bit } => h_1 lhs bit) =
    h_1 lhs bit
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.union_mul_inter_subset_union : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s₁ s₂ t₁ t₂ : Finset α},
  (s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDeriv.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (x : 𝕜), iteratedDeriv n f x = (iteratedFDeriv 𝕜 n f x) fun x => 1
-- Mathlib.FieldTheory.Fixed
FixedPoints.minpoly.irreducible_aux : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [inst_3 : Fintype G]
  (x : F) (f g : Polynomial ↥(FixedPoints.subfield G F)),
  f.Monic → g.Monic → f * g = FixedPoints.minpoly G F x → f = 1 ∨ g = 1
-- Mathlib.Order.RelClasses
/-- **Alias** of `LE.le.ssubset_of_ne`.

---

Set notation form of `LE.le.lt_of_ne` -/
HasSubset.Subset.ssubset_of_ne : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → a ≠ b → a ⊂ b
-- Mathlib.Analysis.Complex.AbsMax
/-- **Alias** of `Complex.isOpen_setOfPred_mem_nhds_and_isMaxOn_norm`. -/
Complex.isOpen_setOf_mem_nhds_and_isMaxOn_norm : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {f : E → F} {s : Set E},
  DifferentiableOn ℂ f s → IsOpen {z | s ∈ nhds z ∧ IsMaxOn (norm ∘ f) s z}
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.openCell_subset_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.openCell n i ⊆ Topology.RelCWComplex.closedCell n i
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, k ∈ t.alter k f ↔ (f t[k]?).isSome = true
-- Mathlib.Algebra.Category.Grp.Basic
/-- Any element of an abelian group gives a unique morphism from `ℤ` sending
`1` to that element.  -/
AddCommGrpCat.asHom : {G : AddCommGrpCat} → ↑G → (AddCommGrpCat.of ℤ ⟶ G)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_natAdd_uIcc_natAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m ⁻¹' Set.uIcc (Fin.natAdd m i) (Fin.natAdd m j) = Set.uIcc i j
-- Mathlib.Algebra.Group.Commute.Basic
Commute.div_mul_div_comm : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b c d : G},
  Commute b d → Commute b⁻¹ c → a / b * (c / d) = a * c / (b * d)
-- Mathlib.Data.Multiset.Defs
/-- If `p` is a decidable predicate,
so is the predicate that all elements of a multiset satisfy `p`.  -/
Multiset.decidableForallMultiset : {α : Type u_1} → {m : Multiset α} → {p : α → Prop} → [(a : α) → Decidable (p a)] → Decidable (∀ a ∈ m, p a)
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Poly.toExpr.go : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.trivializationAtlas' : {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)} →
              [self : FiberBundle F E] → Set (Bundle.Trivialization F Bundle.TotalSpace.proj)
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The identity acts trivially.  -/
CategoryTheory.ModObj.one_smul_assoc : ∀ {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.MonoidalLeftAction C D}
  {M : C} {inst_4 : CategoryTheory.MonObj M} (X : D) [self : CategoryTheory.ModObj M X] {Z : D} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonObj.one X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom h
-- Mathlib.Data.Num.Basic
ZNum.instDiv : Div ZNum
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the pure predicate `p` returns `true` for
any element emitted by the iterator `it`.

`O(|it|)`. Short-circuits upon encountering the first match. The outputs of `it` are
examined in order of iteration.

This function is deprecated. Instead of `it.allowNontermination.any`, use `it.any`.
 -/
Std.IterM.Partial.any : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → (β → Bool) → Std.IterM.Partial m β → m (ULift.{w, 0} Bool)
-- Init.System.Uri
/-- Convert the given FilePath to a "file:///encodedpath" Uri.  -/
System.Uri.pathToUri : System.FilePath → String
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
/-- The equivalence `F.DescentData' sq sq₃ ≌ F.DescentData f`.  -/
CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)) →
                (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) →
                  F.DescentData' sq sq₃ ≌ F.DescentData f
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vsub_subset_vsub_left : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t₁ t₂ : Finset β},
  t₁ ⊆ t₂ → s -ᵥ t₁ ⊆ s -ᵥ t₂
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobjectMap_arrow_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X}
  [inst_1 : CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasImage g]
  (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [inst_3 : CategoryTheory.Limits.HasImageMap sq] {Z_1 : C}
  (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectMap sq)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject g).arrow h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right sq) h)
-- Init.Data.List.Nat.Sublist
List.append_right_sublist_self : ∀ {α : Type u_1} (xs : List α) {ys : List α}, (xs ++ ys).Sublist xs ↔ ys = []
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
_private.Mathlib.Analysis.Complex.UpperHalfPlane.Basic.0.UpperHalfPlane.termℍₒ : Lean.ParserDescr
-- Mathlib.Algebra.Homology.Refinements
HomologicalComplex.exactAt_iff_exact_up_to_refinements : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι),
  c.prev j = i →
    c.next j = k →
      (K.ExactAt j ↔
        ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
          CategoryTheory.CategoryStruct.comp x₂ (K.d j k) = 0 →
            ∃ A' π,
              ∃ (_ : CategoryTheory.Epi π),
                ∃ x₁, CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ (K.d i j))
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.mk : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {tmin tmax : ℝ} →
      {t₀ : ↑(Set.Icc tmin tmax)} →
        {x₀ : E} →
          {r L : NNReal} →
            (toFun : ↑(Set.Icc tmin tmax) → E) →
              LipschitzWith L toFun → toFun t₀ ∈ Metric.closedBall x₀ ↑r → ODE.FunSpace t₀ x₀ r L
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.self : ∀ (F : Type u_1) [inst : Field F], IsGalois F F
-- Mathlib.LinearAlgebra.TensorPower.Pairing
TensorPower.multilinearMapToDual.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ),
  TensorPower.multilinearMapToDual R M n =
    { toFun := fun f => PiTensorProduct.lift ((MultilinearMap.mkPiRing R (Fin n) 1).compLinearMap f),
      map_update_add' := ⋯, map_update_smul' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
/-- The colimit of `J : SingleObj G ⥤ Type u` is equivalent to the quotient of
`J.obj (SingleObj.star G)` by the induced action.  -/
CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient : {G : Type v} →
  [inst : Group G] →
    (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u)) →
      CategoryTheory.Limits.colimit J ≃ MulAction.orbitRel.Quotient G (J.obj (CategoryTheory.SingleObj.star G))
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_roo_eq_some_iff : ∀ {k m n : ℤ} {i : ℕ}, (m<...n).toArray[i]? = some k ↔ i < (n - (m + 1)).toNat ∧ m + 1 + ↑i = k
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier`.

---

A monomorphism `truth : Ω₀ ⟶ Ω` is a subobject classifier if, for every monomorphism
`m : U ⟶ X` in `C`, there is a unique map `χ : X ⟶ Ω` such that for some (necessarily unique)
`χ₀ : U ⟶ Ω₀` the following square is a pullback square:
```
      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω
```
An equivalent formulation replaces `Ω₀` with the terminal object.
 -/
CategoryTheory.Classifier : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.uliftFunctor_map : ∀ {x x_1 : MonCat} (f : x ⟶ x_1),
  MonCat.uliftFunctor.map f =
    MonCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((MonCat.Hom.hom f).comp MulEquiv.ulift.toMonoidHom))
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.map_id_map : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {x y : F.Grothendieck}
  (f : x ⟶ y), (CategoryTheory.Pseudofunctor.Grothendieck.map (CategoryTheory.CategoryStruct.id F)).map f = f
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Fan.mk_π_app : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b)
  (X : CategoryTheory.Discrete β), (CategoryTheory.Limits.Fan.mk P p).π.app X = p X.as
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} [inst : Inhabited β] {f : β → β}, (t.modify k f)[k]! = (Option.map f t[k]?).get!
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.isEmbedding_mk : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsEmbedding ⇑DomMulAct.mk
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- tensorator  -/
CategoryTheory.Functor.CoreMonoidal.μIso : {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} →
              F.CoreMonoidal →
                (X Y : C) →
                  CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅
                    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Init.Data.Vector.Lemmas
Vector.back_mem : ∀ {n : ℕ} {α : Type u_1} [inst : NeZero n] {xs : Vector α n}, xs.back ∈ xs
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity.congr_simp : ∀ (A A_1 : Set ℕ),
  A = A_1 →
    ∀ {inst : DecidablePred fun x => x ∈ A} [inst_1 : DecidablePred fun x => x ∈ A_1],
      schnirelmannDensity A = schnirelmannDensity A_1
-- Mathlib.Order.Filter.AtTopBot.Finite
/-- If `u` is a sequence which is unbounded below,
then it `Frequently` reaches a value strictly smaller than all previous values.
 -/
Filter.frequently_low_scores : ∀ {β : Type u_4} [inst : LinearOrder β] [NoMinOrder β] {u : ℕ → β},
  Filter.Tendsto u Filter.atTop Filter.atBot → ∃ᶠ (n : ℕ) in Filter.atTop, ∀ k < n, u n < u k
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_of_contains_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, (m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coe_linearMap_mk : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {f : A →ₗ[R] B} (h : CoalgebraStruct.counit ∘ₗ f = CoalgebraStruct.counit)
  (h₁ : TensorProduct.map f f ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ f),
  ↑{ toLinearMap := f, counit_comp := h, map_comp_comul := h₁ } = f
-- Init.Data.UInt.Lemmas
USize.size_eq_two_pow : USize.size = 2 ^ System.Platform.numBits
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- A rigid monoidal category is a monoidal category which is left rigid and right rigid.  -/
CategoryTheory.RigidCategory : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → Type (max u v)
-- Mathlib.Analysis.Asymptotics.Theta
/-- **Alias** of the reverse direction of `Asymptotics.isTheta_const_mul_right`. -/
Asymptotics.IsTheta.const_mul_right : ∀ {α : Type u_1} {E : Type u_3} {𝕜 : Type u_14} [inst : Norm E] [inst_1 : NormedField 𝕜] {f : α → E} {l : Filter α}
  {c : 𝕜} {g : α → 𝕜}, c ≠ 0 → f =Θ[l] g → f =Θ[l] fun x => c * g x
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.rTensorHomToHomRTensor_apply : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {P : Type u_9}
  {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid N₂]
  [inst_5 : Module R₂ M₂] [inst_6 : Module R₂ N₂] [inst_7 : Module R P] (f : P →ₛₗ[σ₁₂] M₂) (n₂ : N₂) (p : P),
  ((TensorProduct.rTensorHomToHomRTensor σ₁₂ P M₂ N₂) (f ⊗ₜ[R₂] n₂)) p = f p ⊗ₜ[R₂] n₂
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Text.parseIdList : Std.Internal.Parsec.ByteArray.Parser (Array ℕ)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.one_def : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  {π₁ : ContRepresentation R G V}, 1 = ContIntertwiningMap.id
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.instInsertOfEquivBEqOfLawfulHashable : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Insert α (Std.ExtHashSet α)
-- Lean.Elab.InfoTree.Types
Lean.Elab.ContextInfo.parentDecl? : Lean.Elab.ContextInfo → Option Lean.Name
-- Mathlib.Algebra.Module.Projective
Module.projective_def : ∀ {R : Type u_1} [inst : Semiring R] {P : Type u_2} [inst_1 : AddCommMonoid P] [inst_2 : Module R P],
  Module.Projective R P ↔ ∃ s, Function.LeftInverse ⇑(Finsupp.linearCombination R id) ⇑s
-- Mathlib.Algebra.Group.Defs
IsDedekindFiniteAddMonoid.of_exists_self_add_eq_zero : ∀ (M : Type u_2) [inst : AddMonoid M], (∀ (x y : M), x + y = 0 → ∃ z, y + z = 0) → IsDedekindFiniteAddMonoid M
-- Init.Grind.Config
/-- If `qlia` is `true`, `grind` may generate counterexamples for integer constraints
using rational numbers, and ignoring divisibility constraints.
This approach is cheaper but incomplete.  -/
Lean.Grind.Config.qlia : Lean.Grind.Config → Bool
-- Lean.Meta.Tactic.Grind.Types
/-- Case-split candidates.  -/
Lean.Meta.Grind.Split.State.candidates : Lean.Meta.Grind.Split.State → List Lean.Meta.Grind.SplitInfo
-- Init.Grind.Ordered.Linarith
/-- `p.mul k` multiplies all coefficients and constant of the polynomial `p` by `k`.
 -/
Lean.Grind.Linarith.Poly.mul' : Lean.Grind.Linarith.Poly → ℤ → Lean.Grind.Linarith.Poly
-- Std.Data.HashSet.Lemmas
Std.HashSet.any_eq_false_iff_forall_mem_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulHashable α] [EquivBEq α] {p : α → Bool},
  m.any p = false ↔ ∀ (a : α) (h : a ∈ m), p (m.get a h) = false
-- Mathlib.CategoryTheory.Monoidal.Hopf_
/-- The antipode is an endomorphism of the underlying object of the Hopf monoid.  -/
CategoryTheory.HopfObj.term𝒮 : Lean.ParserDescr
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_intCast : ∀ {α : Type u_3} [inst : DivisionRing α] (n : ℤ), ↑↑n = ↑n
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Origin.fvar.inj : ∀ {fvarId fvarId_1 : Lean.FVarId},
  Mathlib.Meta.FunProp.Origin.fvar fvarId = Mathlib.Meta.FunProp.Origin.fvar fvarId_1 → fvarId = fvarId_1
-- Mathlib.Order.SuccPred.CompleteLinearOrder
IsLUB.mem_of_nonempty_of_not_isSuccLimit : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {x : α},
  IsLUB s x → s.Nonempty → ¬Order.IsSuccLimit x → x ∈ s
-- Mathlib.Algebra.Group.Pi.Units
AddEquiv.piAddUnits.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → AddMonoid (M i)],
  AddEquiv.piAddUnits =
    { toFun := fun f i => { val := ↑f i, neg := f.neg i, val_neg := ⋯, neg_val := ⋯ },
      invFun := fun f => { val := fun x => ↑(f x), neg := fun x => (f x).neg, val_neg := ⋯, neg_val := ⋯ },
      left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.closure_toSubmodule_eq : ∀ {R : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : TopologicalSpace N]
  [inst_3 : Module R N] [inst_4 : ContinuousAdd N] [inst_5 : ContinuousConstSMul R N] {s : ClosedSubmodule R N},
  (↑s).closure = s