mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.Quotient.equiv_apply : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_5} [inst_1 : Ring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M : Type u_6} {N : Type u_7}
  [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N] [inst_7 : Module R₂ N] (P : Submodule R M)
  (Q : Submodule R₂ N) (f : M ≃ₛₗ[σ₁₂] N) (hf : Submodule.map (↑f) P = Q) (a : M ⧸ P),
  (Submodule.Quotient.equiv P Q f hf) a = (P.mapQ Q ↑f ⋯) a
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.toPoly'.go.match_1.splitter : (motive : Int.Internal.Linear.Expr → Sort u_1) →
  (x : Int.Internal.Linear.Expr) →
    ((k : ℤ) → motive (Int.Internal.Linear.Expr.num k)) →
      ((v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v)) →
        ((a b : Int.Internal.Linear.Expr) → motive (a.add b)) →
          ((a b : Int.Internal.Linear.Expr) → motive (a.sub b)) →
            ((k : ℤ) → (a : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k a)) →
              ((a : Int.Internal.Linear.Expr) → (k : ℤ) → motive (a.mulR k)) →
                ((a : Int.Internal.Linear.Expr) → motive a.neg) → motive x
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- A pair of morphisms `h : W ⟶ X` and `k : W ⟶ Y` satisfying `h ≫ f = k ≫ g` induces a morphism
`weakPullback.lift : W ⟶ weakPullback f g`.  -/
CategoryTheory.Limits.weakPullback.lift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] →
            (h : W ⟶ X) →
              (k : W ⟶ Y) →
                autoParam (CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
                    CategoryTheory.Limits.weakPullback.lift._auto_1 →
                  (W ⟶ CategoryTheory.Limits.weakPullback f g)
-- Std.Time.Format.Modifier
/-- 21:00–06:00 (exclusive of midnight)
 -/
Std.Time.ExtendedDayPeriod.night : Std.Time.ExtendedDayPeriod
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.isUpperSet_iff_nhds : ∀ {α : Type u_4} [inst : TopologicalSpace α] [inst_1 : Preorder α],
  Topology.IsUpperSet α ↔ ∀ (a : α), nhds a = Filter.principal (Set.Ici a)
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory CommRingCat fun R S => ↑R →+* ↑S
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Eta-expanded form of `MeasureTheory.AEStronglyMeasurable.const_smul` -/
MeasureTheory.AEStronglyMeasurable.fun_const_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {𝕜 : Type u_5} [inst_1 : SMul 𝕜 β] [ContinuousConstSMul 𝕜 β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : 𝕜), MeasureTheory.AEStronglyMeasurable (fun i => c • f i) μ
-- Std.Http.Data.Method
Std.Http.Method.options.sizeOf_spec : sizeOf Std.Http.Method.options = 1
-- Batteries.Lean.Meta.Basic
/-- Auxiliary definition for `saturate1`.  -/
_private.Batteries.Lean.Meta.Basic.0.Lean.Meta.saturate1.go : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      [Lean.MonadRecDepth m] →
        [MonadLiftT (ST IO.RealWorld) m] →
          (Lean.MVarId → m (Option (Array Lean.MVarId))) → IO.Ref (Array Lean.MVarId) → Lean.MVarId → m Unit
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.instUniqueHomStar : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : CategoryTheory.WithTerminal C} → Unique (X ⟶ CategoryTheory.WithTerminal.star)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit
FundamentalGroupoid.punitEquivDiscretePUnit_unitIso : FundamentalGroupoid.punitEquivDiscretePUnit.unitIso =
  CategoryTheory.NatIso.ofComponents
    (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (FundamentalGroupoid PUnit.{u + 1})).obj x))
    @FundamentalGroupoid.punitEquivDiscretePUnit._proof_2
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.Hom.match_1.eq_3 : ∀ {C : Type u_1} (motive : CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Sort u_2)
  (x : CategoryTheory.WithTerminal C)
  (h_1 : (X Y : C) → motive (CategoryTheory.WithTerminal.of X) (CategoryTheory.WithTerminal.of Y))
  (h_2 : (a : C) → motive CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of a))
  (h_3 : (x : CategoryTheory.WithTerminal C) → motive x CategoryTheory.WithTerminal.star),
  (match x, CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of X, CategoryTheory.WithTerminal.of Y => h_1 X Y
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of a => h_2 a
    | x, CategoryTheory.WithTerminal.star => h_3 x) =
    h_3 x
-- Mathlib.Order.Fin.Finset
/-- This is the order isomorphism from `Fin 2` to a finset `{a, b}` when `a < b`.  -/
Fin.orderIsoPair : {α : Type u_1} → [inst : Preorder α] → [inst_1 : DecidableEq α] → (a b : α) → a < b → Fin 2 ≃o ↥{a, b}
-- Lean.Expr
Lean.eagerReflBoolTrue : Lean.Expr
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.instInhabited : Inhabited AddSemigrp
-- Mathlib.Order.Hom.CompleteLattice
/-- `Set.preimage` as a complete lattice homomorphism.

See also `sSupHom.setImage`.  -/
CompleteLatticeHom.setPreimage : {α : Type u_2} → {β : Type u_3} → (α → β) → CompleteLatticeHom (Set β) (Set α)
-- Mathlib.Algebra.Algebra.Shrink
Shrink.algEquiv_apply : ∀ (R : Type u_1) (α : Type u_2) [inst : Small.{v, u_2} α] [inst_1 : CommSemiring R] [inst_2 : Semiring α]
  [inst_3 : Algebra R α] (a : Shrink.{v, u_2} α), (Shrink.algEquiv R α) a = (equivShrink α).symm a
-- Init.Data.Format.Basic
Std.Format.tag.inj : ∀ {a : ℕ} {a_1 : Std.Format} {a_2 : ℕ} {a_3 : Std.Format},
  Std.Format.tag a a_1 = Std.Format.tag a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Order.Category.BddOrd
BddOrd.ofHom_comp : ∀ {X Y Z : Type u} [inst : PartialOrder X] [inst_1 : BoundedOrder X] [inst_2 : PartialOrder Y] [inst_3 : BoundedOrder Y]
  [inst_4 : PartialOrder Z] [inst_5 : BoundedOrder Z] (f : BoundedOrderHom X Y) (g : BoundedOrderHom Y Z),
  BddOrd.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (BddOrd.ofHom f) (BddOrd.ofHom g)
-- Mathlib.Order.Types.Arithmetic
OrderType.card_type : ∀ {α : Type u} [inst : LinearOrder α], (OrderType.type α).card = Cardinal.mk α
-- Batteries.Recycling.RBTree.Depth
_private.Batteries.Recycling.RBTree.Depth.0.RBTree.RBNode.depth.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (Unit → motive RBTree.RBNode.nil) →
        ((c : RBTree.RBColor) →
            (a : RBTree.RBNode α) → (v : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node c a v b)) →
          motive x
-- Init.Internal.Order.Basic
Lean.Order.ReverseImplicationOrder : Type
-- Mathlib.Data.List.DropRight
List.rtakeWhile_eq_self_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.rtakeWhile p l = l ↔ ∀ x ∈ l, p x = true
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.Std.Legacy.Range.forIn'.loop.eq_def : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (range : Std.Legacy.Range)
  (f : (i : ℕ) → i ∈ range → β → m (ForInStep β)) (b : β) (i : ℕ) (hs : (i - range.start) % range.step = 0)
  (hl : range.start ≤ i),
  Std.Legacy.Range.forIn'.loop✝ range f b i hs hl =
    if h : i < range.stop then do
      let __do_lift ← f i ⋯ b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b =>
          have this := ⋯;
          Std.Legacy.Range.forIn'.loop✝ range f b (i + range.step) ⋯ ⋯
    else pure b
-- Mathlib.Control.Traversable.Lemmas
Traversable.comp_sequence : ∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {F G : Type u → Type u} [inst_2 : Applicative F]
  [LawfulApplicative F] [inst_4 : Applicative G] [LawfulApplicative G] {α : Type u} (x : t (F (G α))),
  sequence (Functor.Comp.mk <$> x) = Functor.Comp.mk (sequence <$> sequence x)
-- Mathlib.Order.RelSeries
RelSeries.toList_tail : ∀ {α : Type u_1} {r : SetRel α α} {p : RelSeries r} (hp : p.length ≠ 0), (p.tail hp).toList = p.toList.tail
-- Init.Data.List.Nat.Modify
List.modifyHead_eq_set : ∀ {α : Type u_1} [inst : Inhabited α] (f : α → α) (l : List α), List.modifyHead f l = l.set 0 (f (l[0]?.getD default))
-- Mathlib.RingTheory.Valuation.RankOne
/-- A proof that `RankOne.unit v ≠ 1`.  -/
Valuation.RankOne.unit_ne_one : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  [hv : v.RankOne], Valuation.RankOne.unit v ≠ 1
-- Mathlib.Order.PiLex
Pi.instNoMinOrderColexForallOfWellFoundedGTOfNonempty : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] [WellFoundedGT ι] [Nonempty ι]
  [inst_3 : (i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMinOrder (β i)], NoMinOrder (Colex ((i : ι) → β i))
-- Mathlib.Data.Sym.Sym2
Sym2.instPartialOrder : {α : Type u_1} → PartialOrder (Sym2 α)
-- Mathlib.Order.Filter.Pointwise
/-- Repeated pointwise addition/subtraction (not the same as pointwise repeated
addition/subtraction!) of a `Filter`. See Note [pointwise nat action].  -/
Filter.instZSMul : {α : Type u_2} → [Zero α] → [Add α] → [Neg α] → SMul ℤ (Filter α)
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
/-- If a sequence of functions real or complex functions are eventually differentiable on a
neighborhood of `x`, they are Cauchy _at_ `x`, and their derivatives
are a uniform Cauchy sequence in a neighborhood of `x`, then the functions form a uniform Cauchy
sequence in a neighborhood of `x`.  -/
uniformCauchySeqOnFilter_of_fderiv : ∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3}
  [inst_1 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] {G : Type u_4}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] {f : ι → E → G} {f' : ι → E → E →L[𝕜] G} {x : E},
  UniformCauchySeqOnFilter f' l (nhds x) →
    (∀ᶠ (n : ι × E) in l ×ˢ nhds x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2) →
      Cauchy (Filter.map (fun n => f n x) l) → UniformCauchySeqOnFilter f l (nhds x)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtDHashMap.Const.insertMany m l).getKey? k = m.getKey? k
-- Mathlib.Topology.Compactness.Compact
isCompact_iff_compactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsCompact s ↔ CompactSpace ↑s
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.toAffineEquiv_refl : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁], ↑(ContinuousAffineEquiv.refl k P₁) = AffineEquiv.refl k P₁
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.ZariskisMainProperty.quasiFiniteAt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S] (p : Ideal S) [inst_4 : p.IsPrime],
  Algebra.ZariskisMainProperty R p → Algebra.QuasiFiniteAt R p
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF → ∀ {k k' : α} {f : β → β}, k' ∈ Std.DTreeMap.Raw.Const.modify t k f ↔ k' ∈ t
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.instZeroHom.eq_1 : ∀ (X Y : AddMonCat), X.instZeroHom Y = { zero := AddMonCat.ofHom 0 }
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.instInhabited : {α : Type u_1} → {β : Type u_2} → [Inhabited α] → [Inhabited β] → Inhabited (PartialEquiv α β)
-- Mathlib.CategoryTheory.Functor.Flat
/-- If `C` is finitely cocomplete, then `F : C ⥤ D` is representably coflat iff it preserves
finite colimits.  -/
CategoryTheory.preservesFiniteColimits_iff_coflat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasFiniteColimits C] (F : CategoryTheory.Functor C D),
  CategoryTheory.RepresentablyCoflat F ↔ CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.Data.Finset.Image
Finset.equivMap_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) (b : ↥(Finset.map f s)),
  (Finset.equivMap f s).symm b = Function.surjInv ⋯ b
-- Mathlib.CategoryTheory.Action.Monoidal
Action.instRightRigidCategoryFunctorSingleObj : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (H : Type u_3) →
        [inst_2 : Group H] →
          [CategoryTheory.RightRigidCategory V] →
            CategoryTheory.RightRigidCategory (CategoryTheory.Functor (CategoryTheory.SingleObj H) V)
-- Std.Async.Basic
/-- Converts a `BaseIO` into a `BaseAsync`
 -/
Std.Async.BaseAsync.mk : {α : Type} → BaseIO (Std.Async.MaybeTask α) → Std.Async.BaseAsync α
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.IsSeparated.singleton : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : ENNReal} {x : X}, Metric.IsSeparated ε {x}
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.nonnegative.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {e : Q(«$α»)} {pα : Q(PartialOrder «$α»)}
  {pf pf_1 : Q(0 ≤ «$e»)},
  Mathlib.Meta.Positivity.Strictness.nonnegative pf = Mathlib.Meta.Positivity.Strictness.nonnegative pf_1 → pf = pf_1
-- Mathlib.RingTheory.PrincipalIdealDomain
span_gcd : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] [IsDomain R] [inst_3 : GCDMonoid R] (x y : R),
  Ideal.span {gcd x y} = Ideal.span {x, y}
-- Mathlib.Data.Sigma.Interval
Sigma.card_Ioc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (α i)]
  [inst_2 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) × α i),
  (Finset.Ioc a b).card = if h : a.fst = b.fst then (Finset.Ioc (h ▸ a.snd) b.snd).card else 0
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.germ_stalkClosedPointTo : ∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCat} [inst : IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X)
  (U : X.Opens) (hU : f (IsLocalRing.closedPoint ↑R) ∈ U),
  CategoryTheory.CategoryStruct.comp (X.presheaf.germ U (f (IsLocalRing.closedPoint ↑R)) hU)
      (AlgebraicGeometry.Scheme.stalkClosedPointTo f) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (CategoryTheory.Functor.mapIso (AlgebraicGeometry.Spec R).presheaf (CategoryTheory.eqToIso ⋯).op ≪≫
          AlgebraicGeometry.Scheme.ΓSpecIso R).hom
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Valuation.satisfies_fmla.prop : ∀ {v : Sat.Valuation} {f : Sat.Fmla}, v.satisfies_fmla f → ∀ c ∈ f, v.satisfies c
-- Init.Data.BitVec.Lemmas
BitVec.toInt_mul_toInt_le : ∀ {w : ℕ} {x y : BitVec w}, x.toInt * y.toInt ≤ 2 ^ (w * 2 - 2)
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
finsetBasisOfLinearIndependentOfCardEqFinrank.eq_1 : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Finset V}
  (hs : s.Nonempty) (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.card = Module.finrank K V),
  finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq = basisOfLinearIndependentOfCardEqFinrank lin_ind ⋯
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instHashableMon : Hashable Lean.Grind.CommRing.Mon
-- Init.Data.Int.DivMod.Lemmas
Int.mod_def' : ∀ (m n : ℤ), m % n = m.emod n
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.uniqueBaseOn_closure_eq : ∀ {α : Type u_2} (I E X : Set α), (Matroid.uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I
-- Mathlib.GroupTheory.Submonoid.Centralizer
/-- The centralizer of a subset of an additive monoid.  -/
AddSubmonoid.centralizer : {M : Type u_1} → Set M → [inst : AddMonoid M] → AddSubmonoid M
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_iSup_of_directed : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι]
  {S : ι → NonUnitalSubalgebra R A}, Directed (fun x1 x2 => x1 ≤ x2) S → ↑(iSup S) = ⋃ i, ↑(S i)
-- Mathlib.CategoryTheory.Enriched.Basic
/-- `EnrichedFunctor.forget` distributes over composition of enriched functors up to isomorphism.  -/
CategoryTheory.EnrichedFunctor.forgetComp : {W : Type v'} →
  [inst : CategoryTheory.Category.{w', v'} W] →
    [inst_1 : CategoryTheory.MonoidalCategory W] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory W C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory W D] →
              {E : Type u₃} →
                [inst_4 : CategoryTheory.EnrichedCategory W E] →
                  (F : CategoryTheory.EnrichedFunctor W C D) →
                    (G : CategoryTheory.EnrichedFunctor W D E) →
                      (CategoryTheory.EnrichedFunctor.comp W F G).forget ≅ F.forget.comp G.forget
-- Mathlib.Algebra.Group.Action.Units
/-- Transfer `VAddCommClass G H M` to `VAddCommClass G H (AddUnits M)`.  -/
AddUnits.vaddCommClass' : ∀ {G : Type u_1} {H : Type u_2} {M : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : AddMonoid M]
  [inst_3 : AddAction G M] [inst_4 : VAddCommClass G M M] [inst_5 : AddAction H M] [inst_6 : VAddCommClass H M M]
  [inst_7 : VAddAssocClass G M M] [inst_8 : VAddAssocClass H M M] [VAddCommClass G H M], VAddCommClass G H (AddUnits M)
-- Mathlib.CategoryTheory.Category.KleisliCat
/-- Construct an object of the Kleisli category from a type.  -/
CategoryTheory.KleisliCat.mk : (m : Type u → Type u_1) → Type u → CategoryTheory.KleisliCat m
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.findDiscrRefinementPath.goIndex : Lean.Expr → Lean.Expr → OptionT Lean.MetaM (List ℕ)
-- Lean.Meta.LazyDiscrTree
/-- Index of trie matching star.  -/
Lean.Meta.LazyDiscrTree.Trie.star : {α : Type} → Lean.Meta.LazyDiscrTree.Trie α → Lean.Meta.LazyDiscrTree.TrieIndex
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- Let `E` be a topological vector space (over a `NontriviallyNormedField`) whose topology is
generated by some family of seminorms `p`, and let `q` be a seminorm on `E`. If `q` is continuous,
then it is uniformly controlled by *finitely many* seminorms of `p`, that is there
is some finset `s` of the index set and some `C > 0` such that `q ≤ C • s.sup p`.  -/
Seminorm.bound_of_continuous : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E],
  WithSeminorms p → ∀ (q : Seminorm 𝕜 E), Continuous ⇑q → ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p
-- Mathlib.Algebra.Homology.Single
CochainComplex.single₀_obj_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] (A : V), ((CochainComplex.single₀ V).obj A).X 0 = A
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.insertMany : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ (α × β)]
  {m : Std.HashMap.Raw α β} {l : ρ}, m.WF → (m.insertMany l).WF
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.desc_map_mk : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D) {i : I} (X Y : C i)
  (f : X ⟶ Y), (CategoryTheory.Sigma.desc F).map (CategoryTheory.Sigma.SigmaHom.mk f) = (F i).map f
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.tendsto_zero_inv_linear_sub : ∀ (z : ℂ) (b : ℤ), Filter.Tendsto (fun d => 1 / (↑b * z - ↑d)) Filter.atTop (nhds 0)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.read_ReaderT : ∀ {m : Type u → Type v} {psm : Std.Do.PostShape} {ρ : Type u} {Q : Std.Do.PostCond ρ (Std.Do.PostShape.arg ρ psm)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m psm], ⦃fun r => Q.1 r r⦄ MonadReaderOf.read ⦃Q⦄
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.wf.match_1.eq_2 : ∀ {α : Type u_1} (γ : Type u_1) (Pl : α → γ → ForInStep γ → Prop) (acc : γ) (next : α)
  (motive : { s // Pl next acc s } → Sort u_2) (acc' : γ) (property : Pl next acc (ForInStep.done acc'))
  (h_1 : (acc' : γ) → (property : Pl next acc (ForInStep.yield acc')) → motive ⟨ForInStep.yield acc', property⟩)
  (h_2 : (acc' : γ) → (property : Pl next acc (ForInStep.done acc')) → motive ⟨ForInStep.done acc', property⟩),
  (match ⟨ForInStep.done acc', property⟩ with
    | ⟨ForInStep.yield acc', property⟩ => h_1 acc' property
    | ⟨ForInStep.done acc', property⟩ => h_2 acc' property) =
    h_2 acc' property
-- Mathlib.MeasureTheory.Function.JacobianOneDim
/-- Change of variable formula for differentiable functions: if a real function `f` is
monotone and differentiable on a measurable set `s`, then the Bochner integral of a function
`g : ℝ → F` on `f '' s` coincides with the integral of `(f' x) • g ∘ f` on `s` .  -/
MeasureTheory.integral_image_eq_integral_deriv_smul_of_monotoneOn : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      MonotoneOn f s → ∀ (g : ℝ → F), ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, f' x • g (f x)
-- Mathlib.Data.Nat.MaxPowDiv
Nat.snd_maxPowDvdDiv : ∀ (p n : ℕ), (p.maxPowDvdDiv n).2 = n.divMaxPow p
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals
the opposite side.  -/
EuclideanGeometry.tan_angle_mul_dist_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
    p₁ = p₂ ∨ p₃ ≠ p₂ → Real.tan (EuclideanGeometry.angle p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
-- Init.Omega.Logic
Lean.Omega.and_not_not_of_not_or : ∀ {p q : Prop}, ¬(p ∨ q) → ¬p ∧ ¬q
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_def : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t : Finset β},
  s +ᵥ t = Finset.image (fun p => p.1 +ᵥ p.2) (s ×ˢ t)
-- Mathlib.FieldTheory.Perfect
/-- If `f` is a polynomial over an integral domain `R` of characteristic `p`, then there is
a map from the set of roots of `Polynomial.expand R (p ^ n) f` to the set of roots of `f`.
It's given by `x ↦ x ^ (p ^ n)`, see `rootsExpandPowToRoots_apply`.  -/
Polynomial.rootsExpandPowToRoots : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      (p n : ℕ) →
        [ExpChar R p] →
          (f : Polynomial R) →
            [inst_3 : DecidableEq R] → ↥((Polynomial.expand R (p ^ n)) f).roots.toFinset ↪ ↥f.roots.toFinset
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.tensorObj_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C),
  CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul
-- Mathlib.NumberTheory.Divisors
Nat.one_lt_of_mem_properDivisors : ∀ {m n : ℕ}, m ∈ n.properDivisors → 1 < n
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.relabel_ex : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ}
  (φ : L.BoundedFormula α (k + 1)),
  FirstOrder.Language.BoundedFormula.relabel g φ.ex = (FirstOrder.Language.BoundedFormula.relabel g φ).ex
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.swap.sizeOf_spec : ∀ (c : Lean.Meta.Grind.AC.EqCnstr), sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.swap c) = 1 + sizeOf c