mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Comp
HasFDerivAt.iterate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {f : E → E} {f' : E →L[𝕜] E},
  HasFDerivAt f f' x → f x = x → ∀ (n : ℕ), HasFDerivAt f^[n] (f' ^ n) x
-- Mathlib.Algebra.Algebra.Unitization
Unitization.algHom_ext'_iff : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] {C : Type u_5} [inst_5 : Semiring C]
  [inst_6 : Algebra R C] {φ ψ : Unitization R A →ₐ[R] C},
  φ = ψ ↔ (↑φ).comp (Unitization.inrNonUnitalAlgHom R A) = (↑ψ).comp (Unitization.inrNonUnitalAlgHom R A)
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation maps closed balls to closed balls and scales the radius by `ratio f`.  -/
Dilation.mapsTo_closedBall : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x : α) (r' : ℝ),
  Set.MapsTo (⇑f) (Metric.closedBall x r') (Metric.closedBall (f x) (↑(Dilation.ratio f) * r'))
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.slash_action_eq' : ∀ {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} (self : SlashInvariantForm Γ k),
  ∀ γ ∈ Γ, SlashAction.map k γ self.toFun = self.toFun
-- Mathlib.Tactic.Order.CollectFacts
/-- Implementation for `collectFacts` in `CollectFactsM` monad.  -/
Mathlib.Tactic.Order.collectFactsImp : Bool → Array Lean.Expr → Lean.Expr → Mathlib.Tactic.Order.CollectFactsM Unit
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- `multiplicativeClosure W` is multiplicative.  -/
CategoryTheory.MorphismProperty.instIsMultiplicativeMultiplicativeClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  W.multiplicativeClosure.IsMultiplicative
-- Mathlib.Topology.Category.CompHaus.Basic
/-- A constructor for objects of the category `CompHaus`,
taking a type, and bundling the compact Hausdorff topology
found by typeclass inference.  -/
CompHaus.of : (X : Type u_1) → [inst : TopologicalSpace X] → [CompactSpace X] → [T2Space X] → CompHaus
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.adj_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C),
  G.adj.counit = { app := fun Y => G.ε.app Y, naturality := ⋯ }
-- Mathlib.Tactic.DepRewrite
/-- The set of all *dependent* `ldecl`s that we have introduced.  -/
Mathlib.Tactic.DepRewrite.Context.δ : Mathlib.Tactic.DepRewrite.Context → Std.HashSet Lean.FVarId
-- Mathlib.Analysis.Seminorm
Seminorm.smul_closedBall_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ}, 0 < ‖k‖ → k • p.closedBall 0 r = p.closedBall 0 (‖k‖ * r)
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_of : ∀ {m : Type u_2} {n : Type u_1} {R : Type u_3} (f : m → n → R), (Matrix.of f).vec = Function.uncurry (flip f)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- A version of `delete_contract_comm'` without the disjointness hypothesis,
and hence a less simple RHS.  -/
Matroid.delete_contract_comm' : ∀ {α : Type u_1} (M : Matroid α) (D C : Set α), (M.delete D).contract C = (M.contract (C \ D)).delete D
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algHom_ext_iff : ∀ {R : Type u} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring B] [inst_2 : Algebra R B]
  {f g : Polynomial R →ₐ[R] B}, f = g ↔ f Polynomial.X = g Polynomial.X
-- Init.System.IO
/-- POSIX-style file permissions.

The `FileRight` structure describes these permissions for a file's owner, members of its designated
group, and all others.
 -/
IO.AccessRight : Type
-- Mathlib.Tactic.ModCases
/-- `mod_cases h : e % n`, where `n` is a positive numeral and `e` is an expression of type `ℕ` or `ℤ`,
performs a case disjunction on the value of `e` modulo `n`. If `e : ℤ`, the goal is split into
`n` subgoals containing the new hypotheses `h : e ≡ 0 [ZMOD n]`, ..., `h : e ≡ n-1 [ZMOD n]`
respectively. If `e : ℕ` instead, then the hypotheses contain `[MOD n]` instead of `[ZMOD n]`.

* `mod_cases e % n`, with `h` omitted, gives the default name `H` to the new hypotheses.
 -/
Mathlib.Tactic.ModCases.«tacticMod_cases_:_%_» : Lean.ParserDescr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
le_algebraMap_iff_spectrum_le : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  {r : R} {a : A},
  autoParam (p a) le_algebraMap_iff_spectrum_le._auto_1 → (a ≤ (algebraMap R A) r ↔ ∀ x ∈ spectrum R a, x ≤ r)
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.le_normalizer_iff_commutator_le_right : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ Subgroup.normalizer ↑K ↔ ⁅H, K⁆ ≤ K
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j : J)
  (x y : ↑(F.obj j)),
  RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.of j (x * y))
    ((RingCat.Colimits.Prequotient.of j x).mul (RingCat.Colimits.Prequotient.of j y))
-- Mathlib.Data.Setoid.Basic
/-- The quotient of α by the kernel of a surjective function f bijects with f's codomain.

If a specific right-inverse of `f` is known, `Setoid.quotientKerEquivOfRightInverse` can be
definitionally more useful.  -/
Setoid.quotientKerEquivOfSurjective : {α : Type u_1} → {β : Type u_2} → (f : α → β) → Function.Surjective f → Quotient (Setoid.ker f) ≃ β
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- `b i` is the `i`th basis vector.  -/
HilbertBasis.instFunLike : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] →
      {E : Type u_3} →
        [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → FunLike (HilbertBasis ι 𝕜 E) ι E
-- Mathlib.Algebra.Module.ULift
ULift.instIsCentralScalar : ∀ {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SMul Rᵐᵒᵖ M] [IsCentralScalar R M],
  IsCentralScalar R (ULift.{u_1, v} M)
-- Mathlib.Order.Sublattice
Sublattice.prod_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L₁ L₂ : Sublattice α} {M₁ M₂ : Sublattice β},
  L₁ ≤ L₂ → M₁ ≤ M₂ → L₁.prod M₁ ≤ L₂.prod M₂
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_13.splitter : (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
  (w : ℕ) →
    (motive : Std.Tactic.BVDecide.BVExpr.Return aig w → Sort u_1) →
      (x : Std.Tactic.BVDecide.BVExpr.Return aig w) →
        ((aig_1 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
            (lhs : aig_1.RefVec w) →
              (hlaig : aig.decls.size ≤ { aig := aig_1, vec := lhs }.aig.decls.size) →
                (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑⟨{ aig := aig_1, vec := lhs }, hlaig⟩).aig) →
                  motive { result := ⟨{ aig := aig_1, vec := lhs }, hlaig⟩, cache := cache }) →
          motive x
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.index_tag : ∀ {ι : Type u_1} (n : ℕ) [NeZero n] (ν : ι → ℤ),
  BoxIntegral.unitPartition.index n (BoxIntegral.unitPartition.tag n ν) = ν
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)),
  (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.CostructuredArrow.isoMk
          (CategoryTheory.Iso.refl
            (((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp.comp
                    (CategoryTheory.CategoryOfElements.toCostructuredArrow F)).obj
                X).left)
          ⋯)
      ⋯
-- Mathlib.Analysis.Quaternion
Quaternion.inner_self : ∀ (a : Quaternion ℝ), inner ℝ a a = Quaternion.normSq a
-- Mathlib.Topology.Order.ScottTopology
/-- Predicate for an ordered topological space to be equipped with its Scott topology.

The Scott topology is defined as the join of the topology of upper sets and the Scott Hausdorff
topology.  -/
Topology.IsScott : (α : Type u_1) → Set (Set α) → [Preorder α] → [TopologicalSpace α] → Prop
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.instMonadLiftHetTOfMonad : (m : Type w → Type w') → [Monad m] → MonadLift m (Std.Iterators.HetT m)
-- Init.Sym.Lemmas
Lean.Sym.BitVec.eq_eq_true : ∀ {n : ℕ} (a b : BitVec n), decide (a = b) = true → (a = b) = True
-- Mathlib.Topology.Algebra.Module.FiniteDimension
Module.Basis.coe_constrL : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w}
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] {ι : Type u_1} [inst_11 : Finite ι] [inst_12 : T2Space E]
  (v : Module.Basis ι 𝕜 E) (f : ι → F), ↑(v.constrL f) = (v.constr 𝕜) f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.smul_eq : ∀ {R : Type r} [inst : CommRing R] (P : Fin 3 → R) {u : R}, IsUnit u → ⟦u • P⟧ = ⟦P⟧
-- Std.Time.Format.Basic
/-- Parses the input string into a `DateTime` and panics if its wrong.
 -/
Std.Time.GenericFormat.parse! : {aw : Std.Time.Awareness} → Std.Time.GenericFormat aw → String → Std.Time.DateTime
-- Mathlib.RingTheory.PowerSeries.Schroder
PowerSeries.largeSchroderSeries_eq_one_add_X_mul_largeSchroderSeries_add_X_mul_largeSchroderSeries_sq : PowerSeries.largeSchroderSeries =
  1 + PowerSeries.X * PowerSeries.largeSchroderSeries + PowerSeries.X * PowerSeries.largeSchroderSeries ^ 2
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.ofUnique.eq_1 : ∀ {M : Type u_16} {N : Type u_17} [inst : Unique M] [inst_1 : Unique N] [inst_2 : Mul M] [inst_3 : Mul N],
  MulEquiv.ofUnique = { toEquiv := Equiv.ofUnique M N, map_mul' := ⋯ }
-- Mathlib.FieldTheory.Extension
IntermediateField.exists_algHom_of_adjoin_splits' : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {S : Set E} {L : Type u_4} [inst_5 : Field L] [inst_6 : Algebra F L]
  [inst_7 : Algebra L E] [inst_8 : IsScalarTower F L E] (f : L →ₐ[F] K),
  (∀ s ∈ S, IsIntegral L s ∧ (Polynomial.map f.toRingHom (minpoly L s)).Splits) →
    IntermediateField.adjoin L S = ⊤ → ∃ φ, AlgHom.domRestrict L φ = f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_diff_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₂ = false →
        Std.DTreeMap.Internal.Impl.Const.get! (m₁.diff m₂ ⋯) k = Std.DTreeMap.Internal.Impl.Const.get! m₁ k
-- Mathlib.Order.CompleteLattice.Basic
iSup_const_mono : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : CompleteLattice α] {a : α} (h : ι → ι'), ⨆ x, a ≤ ⨆ x, a
-- Init.Data.UInt.Bitwise
USize.left_le_or : ∀ {a b : USize}, a ≤ a ||| b
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.instProductive : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α],
  Std.Iterators.Productive (Std.Rxi.Iterator α) Id
-- Init.Omega.Coeffs
/-- Shim for `IntList.sdiv`.  -/
Lean.Omega.Coeffs.sdiv : Lean.Omega.Coeffs → ℤ → Lean.Omega.Coeffs
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product as a bilinear map in the real case.  -/
innerₗ : (F : Type u_3) → [inst : SeminormedAddCommGroup F] → [inst_1 : InnerProductSpace ℝ F] → F →ₗ[ℝ] F →ₗ[ℝ] ℝ
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
PresheafOfModules.pushforward_map_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R) {M N : PresheafOfModules R} (α : M ⟶ N) (X : Cᵒᵖ)
  (m : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))),
  (ModuleCat.Hom.hom (((PresheafOfModules.pushforward φ).map α).app X)) m =
    (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op (F.obj (Opposite.unop X))))) m
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_eq_getValue? : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Inhabited β] {l : List ((_ : α) × β)} {a : α},
  Std.Internal.List.getValue! a l = (Std.Internal.List.getValue? a l).get!
-- Lean.Parser.Term
Lean.Parser.Term.argument.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Ord.UInt
USize.instTransOrd : Std.TransOrd USize
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_pow : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  (k : ℕ), (A ^ k).adjugate = A.adjugate ^ k
-- Mathlib.Algebra.GroupWithZero.Action.Hom
AddMonoidHom.instSMulCommClass : ∀ {M : Type u_1} {N : Type u_2} {A : Type u_3} {B : Type u_4} [inst : AddZeroClass A] [inst_1 : AddZeroClass B]
  [inst_2 : DistribSMul M B] [inst_3 : DistribSMul N B] [SMulCommClass M N B], SMulCommClass M N (A →+ B)