mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.instNormedAddCommGroupSmallComplement : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        {F : Type u_5} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup E''] →
                [inst_4 : NormedSpace 𝕜 E''] →
                  [inst_5 : NormedAddCommGroup F] →
                    [inst_6 : NormedSpace 𝕜 F] →
                      {H : Type u_7} →
                        [inst_7 : TopologicalSpace H] →
                          {G : Type u_9} →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    [inst_9 : TopologicalSpace M] →
                                      [inst_10 : ChartedSpace H M] →
                                        {N : Type u_13} →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} →
                                                    (hf : Manifold.IsImmersionAtOfComplement F I J n f x) →
                                                      NormedAddCommGroup hf.smallComplement
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.rcons_injective : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] {i : ι}, Function.Injective (Monoid.PushoutI.NormalWord.rcons i)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.insphere.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n), s.insphere = s.exsphere ∅
-- Mathlib.Data.Finsupp.Sigma
Finsupp.embSigma.eq_1 : ∀ {κ : Type u_1} {ι : κ → Type u_2} {M : Type u_3} [inst : Zero M] {k : κ} (f : ι k →₀ M),
  f.embSigma = Finsupp.embDomain (Function.Embedding.sigmaMk k) f
-- Init.Data.Nat.Basic
Nat.lt_of_add_one_le : ∀ {n m : ℕ}, n + 1 ≤ m → n < m
-- Mathlib.Order.UpperLower.Closure
LowerSet.sdiff_sup_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : LowerSet α} {t : Set α},
  t ⊆ ↑s → (∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) → s.sdiff t ⊔ lowerClosure t = s
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.coe_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.Injective fun B x y => (B x) y
-- Mathlib.Tactic.FunProp.FunctionData
/-- Type of morphism application.  -/
Mathlib.Meta.FunProp.MorApplication : Type
-- Mathlib.Topology.Order.OrderClosed
not_tendsto_nhds_of_tendsto_atTop : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [NoTopOrder α] [inst_2 : TopologicalSpace α] [ClosedIciTopology α]
  {l : Filter β} [l.NeBot] {f : β → α}, Filter.Tendsto f l Filter.atTop → ∀ (a : α), ¬Filter.Tendsto f l (nhds a)
-- Lean.Util.ParamMinimizer
/-- Removes parameter `i` from current set.
Sets bit `i` to `false`.
 -/
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.erase : {m : Type → Type} → ℕ → [Monad m] → Lean.Util.ParamMinimizer.M✝ m Unit
-- Std.Data.HashMap.Raw
/-- Returns the number of buckets in the internal representation of the hash map. This function may be
useful for things like monitoring system health, but it should be considered an internal
implementation detail.
 -/
Std.HashMap.Raw.Internal.numBuckets : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → ℕ
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiableOn_neg_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s : (x : B) → E x}
  {u : Set B}, MDiff[u] (T% s) → MDiff[u] fun x => ⟨x, (-s) x⟩
-- Mathlib.Topology.Sequences
/-- In a (pseudo)metrizable space, any sequentially compact set is compact.  -/
IsSeqCompact.isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] {s : Set X},
  IsSeqCompact s → IsCompact s
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
/-- The lex order on multivariate power series.  -/
MvPowerSeries.lexOrder : {σ : Type u_1} →
  {R : Type u_2} →
    [Semiring R] → [inst : LinearOrder σ] → [WellFoundedGT σ] → MvPowerSeries σ R → WithTop (Lex (σ →₀ ℕ))
-- Mathlib.Data.Semiquot
/-- Apply a function to the unknown value stored in a `Semiquot α`.  -/
Semiquot.map : {α : Type u_1} → {β : Type u_2} → (α → β) → Semiquot α → Semiquot β
-- Init.Data.Vector.Find
Vector.findSome?_eq_some_iff : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → Option β} {xs : Vector α n} {b : β},
  Vector.findSome? f xs = some b ↔
    ∃ k₁ k₂,
      ∃ (w : n = k₁ + 1 + k₂), ∃ ys a zs, xs = Vector.cast ⋯ (ys.push a ++ zs) ∧ f a = some b ∧ ∀ x ∈ ys, f x = none
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.isSplit : Lean.Name → Lean.Meta.Grind.GrindM Bool
-- Mathlib.Order.Cover
CovBy.of_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} (f : α ↪o β), f a ⋖ f b → a ⋖ b
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
cbiSup_eq_of_forall : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α] {p : ι → Prop} {f : Subtype p → α},
  (∀ (i : ι), p i) → ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smul_finset_inter : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {s t : Finset β}
  {a : α}, a • (s ∩ t) = a • s ∩ a • t
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_C_add : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a : R}, (Polynomial.C a + p).natDegree = p.natDegree
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_last_apply : ∀ {n : ℕ} {i : Fin (n + 2)}, (Fin.last n).predAbove i = if hi : i = Fin.last (n + 1) then Fin.last n else i.castPred hi
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induceHom_comp : ∀ {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X}
  {s : Set V} {t : Set W} {r : Set X} (φ : G →g G') (φst : Set.MapsTo (⇑φ) s t) (ψ : G' →g G'')
  (ψtr : Set.MapsTo (⇑ψ) t r),
  (SimpleGraph.induceHom ψ ψtr).comp (SimpleGraph.induceHom φ φst) = SimpleGraph.induceHom (ψ.comp φ) ⋯
-- Mathlib.Data.Set.Image
Function.Surjective.image_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective f → ∀ (s : Set β), f '' f ⁻¹' s = s
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.restoreM_StateT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α σ : Type u}
  {epost : EPred} (x : m (α × σ)) (post : α → σ → Pred),
  ⦃ fun x_1 =>
    Std.Internal.Do.wp x
      (fun x =>
        match x with
        | (a, s) => post a s)
      epost ⦄
    MonadControl.restoreM x ⦃ post; epost ⦄
-- Mathlib.Data.Set.Prod
Set.offDiag_empty : ∀ {α : Type u_1}, ∅.offDiag = ∅
-- Mathlib.Algebra.Order.Hom.Monoid
instCoeTCOrderMonoidIsoOfOrderIsoClassOfMulEquivClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] [inst_4 : EquivLike F α β] [inst_5 : OrderIsoClass F α β] [inst_6 : MulEquivClass F α β],
  instCoeTCOrderMonoidIsoOfOrderIsoClassOfMulEquivClass = { coe := OrderMonoidIsoClass.toOrderMonoidIso }
-- Mathlib.Computability.TuringMachine.Tape
_private.Mathlib.Computability.TuringMachine.Tape.0.Turing.Tape.move.match_1.splitter : {Γ : Type u_1} →
  [inst : Inhabited Γ] →
    (motive : Turing.Dir → Turing.Tape Γ → Sort u_2) →
      (x : Turing.Dir) →
        (x_1 : Turing.Tape Γ) →
          ((a : Γ) → (L R : Turing.ListBlank Γ) → motive Turing.Dir.left { head := a, left := L, right := R }) →
            ((a : Γ) → (L R : Turing.ListBlank Γ) → motive Turing.Dir.right { head := a, left := L, right := R }) →
              motive x x_1
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₂_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (β : CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip)
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₂ β).app X₁).app X₂).app X₃ =
    (β.hom.app X₁).app (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃)
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.toAddMonoidHom_injective : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  Function.Injective AddEquiv.toAddMonoidHom
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.isFiniteMeasure_of_map : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [mβ : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : α → β},
  AEMeasurable f μ → ∀ [MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.map f μ)], MeasureTheory.IsFiniteMeasure μ
-- Mathlib.Combinatorics.Additive.Dissociation
/-- If every dissociated subset of `s` has size at most `d`, then `s` is actually
generated by a subset of size at most `d`.

This is a dissociation analog of the fact that a set whose linearly independent subspaces all have
size at most `d` is of dimension at most `d` itself.  -/
Finset.exists_subset_addSpan_card_le_of_forall_addDissociated : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] {s : Finset α} {d : ℕ},
  (∀ s' ⊆ s, AddDissociated ↑s' → s'.card ≤ d) → ∃ s' ⊆ s, s'.card ≤ d ∧ s ⊆ s'.addSpan
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation
_private.Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation.0.ValueDistribution.Cartan.cartanKernel.eq_1 : ∀ (f : ℂ → ℂ) (R α β : ℝ),
  ValueDistribution.Cartan.cartanKernel f R α β = Real.log ‖f (circleMap 0 R β) - circleMap 0 1 α‖
-- Mathlib.Topology.Algebra.Constructions
Units.continuous_map : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : TopologicalSpace N]
  [inst_3 : Monoid N] {f : M →* N}, Continuous ⇑f → Continuous ⇑(Units.map f)
-- Init.Data.UInt.Lemmas
UInt8.toNat_mod_uInt64Size : ∀ (n : UInt8), n.toNat % UInt64.size = n.toNat
-- Mathlib.Order.Antichain
/-- If `t` is an antichain shadowing and including the set of maximal elements of `s`,
then `t` *is* the set of maximal elements of `s`.  -/
IsAntichain.eq_setOfPred_maximal : ∀ {α : Type u_1} {s t : Set α} [inst : Preorder α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) t →
    (∀ (x : α), Maximal (fun x => x ∈ s) x → x ∈ t) →
      (∀ a ∈ t, ∃ b ≤ a, Maximal (fun x => x ∈ s) b) → {x | Maximal (fun x => x ∈ s) x} = t
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.instPreorder.eq_1 : ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  ArchimedeanOrder.instPreorder =
    { toLE := ArchimedeanOrder.instLE, toLT := ArchimedeanOrder.instLT, le_refl := ⋯, le_trans := ⋯,
      lt_iff_le_not_ge := ⋯ }
-- Lean.Declaration
Lean.QuotVal.kind : Lean.QuotVal → Lean.QuotKind
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
basisOfPiSpaceOfLinearIndependent.eq_1 : ∀ {K : Type u} [inst : DivisionRing K] {ι : Type u_1} [inst_1 : Fintype ι] [inst_2 : Decidable (Nonempty ι)]
  {b : ι → ι → K} (hb : LinearIndependent K b),
  basisOfPiSpaceOfLinearIndependent hb =
    if hι : Nonempty ι then basisOfLinearIndependentOfCardEqFinrank hb ⋯
    else
      have this := ⋯;
      Module.Basis.empty (ι → K)
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.subLeft_apply : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α] (a a_1 : α),
  (OrderIso.subLeft a) a_1 = OrderDual.toDual (a - a_1)
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) {m n : ℕ},
  p.natDegree ≤ m → q.natDegree ≤ n → (p * q).homogenize (m + n) = p.homogenize m * q.homogenize n
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimitCore.fac : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes}
  (self : c.IsColimitCore) (c' : F.CoconeTypes) (j : J), self.desc c' ∘ c.ι j = c'.ι j
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.add_martingale : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f g : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : Preorder E] [AddLeftMono E],
  MeasureTheory.Submartingale f ℱ μ → MeasureTheory.Martingale g ℱ μ → MeasureTheory.Submartingale (f + g) ℱ μ
-- Init.Data.Fin.Basic
/-- Returns `a` modulo `n` as a `Fin n`.

The assumption `NeZero n` ensures that `Fin n` is nonempty.
 -/
Fin.ofNat : (n : ℕ) → [NeZero n] → ℕ → Fin n
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opProdIsoCoprod.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A B : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B],
  CategoryTheory.Limits.opProdIsoCoprod A B =
    {
      hom :=
        (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.coprod.inl.unop
            CategoryTheory.Limits.coprod.inr.unop).op,
      inv := CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.prod.fst.op CategoryTheory.Limits.prod.snd.op,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Init.Data.String.Slice
String.Slice.instLT : LT String.Slice
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Complex.hasStrictFDerivAt_cpow' : ∀ {x y : ℂ},
  x ∈ Complex.slitPlane →
    HasStrictFDerivAt (fun x => x.1 ^ x.2)
      ((y * x ^ (y - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (x ^ y * Complex.log x) • ContinuousLinearMap.snd ℂ ℂ ℂ)
      (x, y)
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.apply_toPerfPair_flip : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) [inst_5 : p.IsPerfPair] (f : Module.Dual R M)
  (x : M), (p x) (p.flip.toPerfPair.symm f) = f x
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasStrictFDerivAt_intCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IntCast F] (z : ℤ) (x : E), HasStrictFDerivAt (↑z) 0 x
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.dist_eq_of_L1 : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)]
  (x y : PiLp 1 β), dist x y = ∑ i, dist (x.ofLp i) (y.ofLp i)
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.hasFiniteColimits_of_hasColimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C],
  CategoryTheory.Limits.HasFiniteColimits C
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.id : ∀ {α : Type u} [pα : Preorder α], GaloisConnection id id
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_iUnion_le : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  μ.restrict (⋃ i, s i) ≤ MeasureTheory.Measure.sum fun i => μ.restrict (s i)
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.zero_of_isLE_of_isGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ),
  n₀ < n₁ → t.IsLE X n₀ → t.IsGE Y n₁ → f = 0
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for `ComposableArrows C 4`.  -/
CategoryTheory.ComposableArrows.mk₄ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X₀ X₁ X₂ X₃ X₄ : C} → (X₀ ⟶ X₁) → (X₁ ⟶ X₂) → (X₂ ⟶ X₃) → (X₃ ⟶ X₄) → CategoryTheory.ComposableArrows C 4
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.toLinearIsometry_toDual : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E], (InnerProductSpace.toDual 𝕜 E).toLinearIsometry = InnerProductSpace.toDualMap 𝕜 E
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.mem_smul_span_iff : ∀ {ι : Type u_1} {n : ℕ} [NeZero n] [inst : Finite ι] {v : ι → ℝ},
  v ∈ (↑n)⁻¹ • Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)) ↔ ∀ (i : ι), ↑n * v i ∈ Set.range ⇑(algebraMap ℤ ℝ)
-- Mathlib.MeasureTheory.Integral.Pi
MeasureTheory.integral_fintype_prod_eq_pow : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : Fintype ι] [inst_1 : RCLike 𝕜] {E : Type u_3} (f : E → 𝕜)
  {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [MeasureTheory.SigmaFinite μ],
  (∫ (x : ι → E), ∏ i, f (x i) ∂MeasureTheory.Measure.pi fun x => μ) = (∫ (x : E), f x ∂μ) ^ Fintype.card ι
-- Lean.Elab.Quotation.Util
/-- Get all pattern vars (as `Syntax.ident`s) in `stx`  -/
Lean.Elab.Term.Quotation.getPatternVars : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Syntax)
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.elabAppFnId : Lean.Syntax →
  List Lean.Level →
    List Lean.Elab.Term.LVal →
      Array Lean.Elab.Term.NamedArg →
        Array Lean.Elab.Term.Arg →
          Option Lean.Expr →
            Bool →
              Bool →
                Bool →
                  Array (Lean.Elab.Term.TermElabResult Lean.Expr) →
                    Lean.Elab.TermElabM (Array (Lean.Elab.Term.TermElabResult Lean.Expr))
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.algebraMap_apply : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) (x : P.Ring), (algebraMap P.Ring S) x = (MvPolynomial.aeval P.val) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_minKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback)
-- Mathlib.RingTheory.Localization.Defs
Localization.isLocalization : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R}, IsLocalization M (Localization M)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The cokernel of a zero morphism is isomorphic to the target.  -/
CategoryTheory.Limits.cokernelZeroIsoTarget : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → {X Y : C} → CategoryTheory.Limits.cokernel 0 ≅ Y
-- Mathlib.Algebra.Category.AlgCat.FilteredColimits
instPreservesFilteredColimitsAlgCatRingCatForget₂AlgHomCarrierRingHomCarrier : ∀ {R : Type u} [inst : CommRing R],
  CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ (AlgCat R) RingCat)
-- Init.Data.Int.Gcd
Int.lcm_dvd_iff : ∀ {a b : ℤ} {c : ℕ}, a.lcm b ∣ c ↔ a ∣ ↑c ∧ b ∣ ↑c
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_map_zero_lt : ∀ (f g : CircleDeg1Lift), f (g 0) < f 0 + g 0 + 1
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instStarModule : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Star R]
  [inst_5 : (i : ι) → Star (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)]
  [inst_7 : (i : ι) → SMul R (G i)] [inst_8 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)]
  [∀ (i : ι), StarModule R (G i)], StarModule R (DirectLimit G f)
-- Mathlib.Analysis.Normed.Field.Lemmas
DilationEquiv.mulRight_apply : ∀ {α : Type u_1} [inst : NormedDivisionRing α] (a : α) (ha : a ≠ 0) (x : α), (DilationEquiv.mulRight a ha) x = x * a
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.mapZeroObject_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroObject D]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.PreservesZeroMorphisms], F.mapZeroObject.inv = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The pointwise division of sets `s / t` is defined as `{x / y | x ∈ s, y ∈ t}` in locale
`Pointwise`.  -/
Set.div : {α : Type u_2} → [Div α] → Div (Set α)
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.InlayHintState.mk.sizeOf_spec : ∀ (oldInlayHints : Array Lean.Elab.InlayHintInfo) (oldFinishedSnaps : ℕ) (lastEditTimestamp? : Option ℕ)
  (isFirstRequestAfterEdit : Bool),
  sizeOf
      { oldInlayHints := oldInlayHints, oldFinishedSnaps := oldFinishedSnaps, lastEditTimestamp? := lastEditTimestamp?,
        isFirstRequestAfterEdit := isFirstRequestAfterEdit } =
    1 + sizeOf oldInlayHints + sizeOf oldFinishedSnaps + sizeOf lastEditTimestamp? + sizeOf isFirstRequestAfterEdit
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S : Type
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- `mapAddMon` is functorial in the lax monoidal functor.  -/
CategoryTheory.Functor.mapAddMonFunctor : (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] →
            CategoryTheory.Functor (CategoryTheory.LaxMonoidalFunctor C D)
              (CategoryTheory.Functor (CategoryTheory.AddMon C) (CategoryTheory.AddMon D))
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.Hom.mk.inj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C₁}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {R R' : Φ.RightResolution X₂} {f : R.X₁ ⟶ R'.X₁}
  {comm :
    autoParam (CategoryTheory.CategoryStruct.comp R.w (Φ.functor.map f) = R'.w)
      CategoryTheory.LocalizerMorphism.RightResolution.Hom.comm._autoParam}
  {f_1 : R.X₁ ⟶ R'.X₁}
  {comm_1 :
    autoParam (CategoryTheory.CategoryStruct.comp R.w (Φ.functor.map f_1) = R'.w)
      CategoryTheory.LocalizerMorphism.RightResolution.Hom.comm._autoParam},
  { f := f, comm := comm } = { f := f_1, comm := comm_1 } → f = f_1