mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- Whiskering left of a `CatCospanTransformMorphism` by a `CatCospanTransform`.  -/
CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {A' : Type u₄} →
        {B' : Type u₅} →
          {C' : Type u₆} →
            {A'' : Type u₇} →
              {B'' : Type u₈} →
                {C'' : Type u₉} →
                  [inst : CategoryTheory.Category.{v₁, u₁} A] →
                    [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
                      [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                        {F : CategoryTheory.Functor A B} →
                          {G : CategoryTheory.Functor C B} →
                            [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                              [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                                [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                                  {F' : CategoryTheory.Functor A' B'} →
                                    {G' : CategoryTheory.Functor C' B'} →
                                      [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] →
                                        [inst_7 : CategoryTheory.Category.{v₈, u₈} B''] →
                                          [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] →
                                            {F'' : CategoryTheory.Functor A'' B''} →
                                              {G'' : CategoryTheory.Functor C'' B''} →
                                                (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') →
                                                  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} →
                                                    (ψ ⟶ ψ') → (φ.comp ψ ⟶ φ.comp ψ')
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.coe_one : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R], ↑1 = 1
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.Section.equivComp.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (σ : S.Section)
  (equiv : S.Equiv S'), σ.equivComp equiv = { toFun := ⇑equiv ∘ ⇑σ, rightInverse_rightHom := ⋯ }
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.mk.inj : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {inst : Semiring R} {inst_1 : AddCommMonoid M}
  {inst_2 : Module R M} {inst_3 : TopologicalSpace M} {inst_4 : AddCommMonoid N} {inst_5 : Module R N}
  {inst_6 : TopologicalSpace N} {toContinuousMultilinearMap : ContinuousMultilinearMap R (fun x => M) N}
  {map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toContinuousMultilinearMap.toFun v = 0}
  {toContinuousMultilinearMap_1 : ContinuousMultilinearMap R (fun x => M) N}
  {map_eq_zero_of_eq'_1 : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toContinuousMultilinearMap_1.toFun v = 0},
  { toContinuousMultilinearMap := toContinuousMultilinearMap, map_eq_zero_of_eq' := map_eq_zero_of_eq' } =
      { toContinuousMultilinearMap := toContinuousMultilinearMap_1, map_eq_zero_of_eq' := map_eq_zero_of_eq'_1 } →
    toContinuousMultilinearMap = toContinuousMultilinearMap_1
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} (f : P ⟶ Q) (a : CategoryTheory.Over P),
  (CategoryTheory.Abelian.app f a).hom = CategoryTheory.CategoryStruct.comp a.hom f
-- Mathlib.Analysis.Convex.Between
Wbtw.trans_left_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V]
  {w x y z : P}, Wbtw R w y z → Wbtw R w x y → y ≠ z → x ≠ z
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_relabel : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} {φ : L.Formula α}
  {g : α → β} {v : β → M}, (FirstOrder.Language.Formula.relabel g φ).Realize v ↔ φ.Realize (v ∘ g)
-- Init.Data.Int.Pow
Int.sq_nonnneg : ∀ (m : ℤ), 0 ≤ m ^ 2
-- Mathlib.FieldTheory.PerfectClosure
_private.Mathlib.FieldTheory.PerfectClosure.0.PerfectClosure.add_aux_left : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x1 x2 y : ℕ × K),
  PerfectClosure.R K p x1 x2 →
    PerfectClosure.mk K p (x1.1 + y.1, (⇑(frobenius K p))^[y.1] x1.2 + (⇑(frobenius K p))^[x1.1] y.2) =
      PerfectClosure.mk K p (x2.1 + y.1, (⇑(frobenius K p))^[y.1] x2.2 + (⇑(frobenius K p))^[x2.1] y.2)
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.cokernel_var : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hg₁ : Submodule.span A (Set.range g₁) = ⊤)
  (g : (pres₂.cokernelRelations data).G), (pres₂.cokernel data hg₁).var g = Submodule.Quotient.mk (pres₂.var g)
-- Std.Http.Data.Status
/-- 510 Not Extended
 -/
Std.Http.Status.notExtended : Std.Http.Status
-- Mathlib.Order.Heyting.Basic
/-- See `himp_le` for a stronger version in Boolean algebras.  -/
Codisjoint.himp_le_of_right_le : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, Codisjoint a c → b ≤ a → c ⇨ b ≤ a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.contains (t.maxKey he) = true
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.forall_coe_zero_iff_zero : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β]
  (f : BoundedContinuousFunction α β), (∀ (x : α), f x = 0) ↔ f = 0
-- Mathlib.Data.Fintype.Pigeonhole
/-- The pigeonhole principle for infinitely many pigeons in finitely many pigeonholes. If there are
infinitely many pigeons in finitely many pigeonholes, then there are at least two pigeons in the
same pigeonhole.

See also: `Fintype.exists_ne_map_eq_of_card_lt`, `Finite.exists_infinite_fiber`.
 -/
Finite.exists_ne_map_eq_of_infinite : ∀ {α : Sort u_4} {β : Sort u_5} [Infinite α] [Finite β] (f : α → β), ∃ x y, x ≠ y ∧ f x = f y
-- Lean.Compiler.IR.Basic
/-- `reuse x in ctor_i ys` instruction in the paper.  -/
Lean.IR.Expr.reuse : Lean.IR.VarId → Lean.IR.CtorInfo → Bool → Array Lean.IR.Arg → Lean.IR.Expr
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- An element `s` of `Sym σ n` induces a partition given by its multiplicities.  -/
Nat.Partition.ofSym : {n : ℕ} → {σ : Type u_1} → Sym σ n → [DecidableEq σ] → n.Partition
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_insertIfNew_le_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {he : t ≠ ∅}, (cmp ((t.insertIfNew k v).minKey ⋯) (t.minKey he)).isLE = true
-- Std.Http.Data.Body.Stream
Std.Http.Body.instCoeStreamAny : Coe Std.Http.Body.Stream Std.Http.Body.Any
-- Mathlib.Order.Filter.Interval
Filter.OrdConnected.tendsto_Icc : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [hs : s.OrdConnected],
  Filter.TendstoIxxClass Set.Icc (Filter.principal s) (Filter.principal s)
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.instIteratorIdSearchStep.match_3.eq_1 : ∀ (s : String.Slice)
  (motive :
    Std.IterStep (Std.IterM Id (String.Slice.Pattern.SearchStep s)) (String.Slice.Pattern.SearchStep s) → Sort u_1)
  (it' : Std.IterM Id (String.Slice.Pattern.SearchStep s)) (out : String.Slice.Pattern.SearchStep s)
  (h_1 :
    (it' : Std.IterM Id (String.Slice.Pattern.SearchStep s)) →
      (out : String.Slice.Pattern.SearchStep s) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM Id (String.Slice.Pattern.SearchStep s)) → motive (Std.IterStep.skip it'))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.lt_of_eq_of_lt : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f g h : CauSeq α abs},
  f ≈ g → g < h → f < h
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Mapping from a type `α` to its corresponding `ToIntInfo` object idx in `toInfos`, which contains
the information needed to embed `α` terms into `Int` terms.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.toIntIds : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.prod_mem_iff_exists_mem : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R}, I.IsPrime → ∀ (s : Finset R), ∏ x ∈ s, x ∈ I ↔ ∃ p ∈ s, p ∈ I
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharThreeJNeZeroNF.a₄ : ∀ {R : Type u_1} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsCharThreeJNeZeroNF], W.a₄ = 0
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fintypeEdgeSetBot : {V : Type u} → Fintype ↑⊥.edgeSet
-- Init.SizeOf
Option.some.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (val : α), sizeOf (some val) = 1 + sizeOf val
-- Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall
/-- If `f` is analytic on `Bᵣ(x₀)` and its Taylor series converges on this ball, then it converges
to `f`.  -/
AnalyticOn.hasFPowerSeriesOnSubball : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} {r : ENNReal},
  0 < r →
    AnalyticOn 𝕜 f (Metric.eball x r) →
      r ≤ (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial).radius →
        HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) x r
-- Mathlib.Algebra.Order.Module.Defs
neg_of_smul_neg_left' : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : LinearOrder α] [inst_4 : LinearOrder β] [SMulPosMono α β], a • b < 0 → 0 ≤ a → b < 0
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.colimitCoconeOfUnique_isColimit_desc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C)
  (s : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)),
  (CategoryTheory.Limits.colimitCoconeOfUnique f).isColimit.desc s = s.ι.app default
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- This typeclass ensures that an `UpwardEnumerable α` instance is compatible with `<`.
In this case, `UpwardEnumerable α` fully characterizes the `LT α` instance.
 -/
Std.PRange.LawfulUpwardEnumerableLT : (α : Type u) → [Std.PRange.UpwardEnumerable α] → [LT α] → Prop
-- Lean.ProjFns
Lean.isProjectionFn : {m : Type → Type} → [Lean.MonadEnv m] → [Monad m] → Lean.Name → m Bool
-- Lean.DocString.Syntax
/-- Named argument  -/
Lean.Doc.Syntax.named : Lean.ParserDescr
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_anti`.

---

The edist is antitone with respect to inclusion.  -/
EMetric.infEdist_anti : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α}, s ⊆ t → Metric.infEDist x t ≤ Metric.infEDist x s
-- Init.Data.String.Pattern.String
String.Slice.Pattern.BackwardSliceSearcher.endsWith : String.Slice → String.Slice → Bool
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_symm : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P ∧ Q ⊢ₛ Q ∧ P
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.instFinite : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m (Std.IterM m β)]
  [inst_2 : Std.Iterator α₂ m β] [Std.Iterators.Finite α m] [Std.Iterators.Finite α₂ m],
  Std.Iterators.Finite (Std.Iterators.Types.Flatten α α₂ β m) m
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_nonpos_iff_of_base_lt_one : ∀ {b x : ℝ}, 0 < b → b < 1 → 0 < x → (Real.logb b x ≤ 0 ↔ 1 ≤ x)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category `C` which has countable coproducts is said to have countable `AB4` provided that
countable coproducts are exact.
 -/
CategoryTheory.CountableAB4 : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasCountableCoproducts C] → Prop
-- Mathlib.Algebra.Polynomial.Module.FiniteDimensional
Module.AEval.isTorsion_of_aeval_eq_zero : ∀ {R : Type u_1} {M : Type u_3} {A : Type u_4} {a : A} [inst : CommSemiring R] [NoZeroDivisors R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : AddCommMonoid M] [inst_5 : Module A M] [inst_6 : Module R M]
  [inst_7 : IsScalarTower R A M] {p : Polynomial R},
  (Polynomial.aeval a) p = 0 → p ≠ 0 → Module.IsTorsion (Polynomial R) (Module.AEval R M a)
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.EncodedString.mk.sizeOf_spec : ∀ {r : UInt8 → Bool} (toByteArray : ByteArray) (valid : Std.Http.URI.IsAllowedEncodedChars r toByteArray),
  sizeOf { toByteArray := toByteArray, valid := valid } = 1 + sizeOf toByteArray + sizeOf valid
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- The `G`-valued integral of `E`-valued function and the `F`-valued vector measure `μ` with linear
paring `B : E →L[ℝ] F →L[ℝ] G` . This is set to be `0` if `G` is not complete or if `f` is not
integrable with respect to `(μ.transpose B).variation`. Notation `∫ᵛ x, f x ∂[B; μ]`.

When `μ` is `G`-valued, to get the integral in `G` of a real-valued function, take
`B = ContinousLinearMap.lsmul ℝ ℝ`. Notation `∫ᵛ x, f x ∂•μ`.
When `μ` is a signed measure, to get the integral in `G` of a `G`-valued function, take
`B = (ContinousLinearMap.lsmul ℝ ℝ).flip`. Notation `∫ᵛ x, f x ∂<•μ`.
 -/
MeasureTheory.VectorMeasure.«term∫ᵛ_,_∂[_;_]» : Lean.ParserDescr
-- Mathlib.Analysis.Convex.Body
ConvexBody.mk.sizeOf_spec : ∀ {V : Type u_2} [inst : TopologicalSpace V] [inst_1 : AddCommMonoid V] [inst_2 : SMul ℝ V] [inst_3 : SizeOf V]
  (carrier : Set V) (convex' : Convex ℝ carrier) (isCompact' : IsCompact carrier) (nonempty' : carrier.Nonempty),
  sizeOf { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' } =
    1 + sizeOf nonempty'
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trPosNum.eq_2 : ∀ (n : PosNum), Turing.PartrecToTM2.trPosNum n.bit0 = Turing.PartrecToTM2.Γ'.bit0 :: Turing.PartrecToTM2.trPosNum n
-- Init.Data.SInt.Lemmas
Int32.toBitVec_ofIntClamp : ∀ {n : ℤ}, Int32.minValue.toInt ≤ n → n ≤ Int32.maxValue.toInt → (Int32.ofIntClamp n).toBitVec = BitVec.ofInt 32 n
-- Mathlib.CategoryTheory.Limits.Constructions.EpiMono
CategoryTheory.Limits.PullbackCone.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst fst_1 : W ⟶ X)
  (e_fst : fst = fst_1) (snd snd_1 : W ⟶ Y) (e_snd : snd = snd_1)
  (eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g),
  CategoryTheory.Limits.PullbackCone.mk fst snd eq = CategoryTheory.Limits.PullbackCone.mk fst_1 snd_1 ⋯
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.equivMapOfInjective_coe_addEquiv : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) (e : G ≃+ G'),
  H.equivMapOfInjective ↑e ⋯ = e.addSubgroupMap H
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.instSMul : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {R : Type u_1} →
        [inst_2 : Ring R] →
          [CategoryTheory.Linear R C] →
            {F G : CochainComplex C ℤ} → {n : ℤ} → SMul R (CochainComplex.HomComplex.Cocycle F G n)
-- Mathlib.Analysis.Normed.Field.Basic
enorm_inv : ∀ {α : Type u_2} [inst : NormedDivisionRing α] {a : α}, a ≠ 0 → ‖a⁻¹‖ₑ = ‖a‖ₑ⁻¹
-- Mathlib.RingTheory.Length
Module.finiteDimensionalOrder_submodule_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  FiniteDimensionalOrder (Submodule R M) ↔ IsFiniteLength R M
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.support_restrict_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] {s : Set X}, (μ.restrict s).support ⊆ closure s ∩ μ.support
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sectL_swapRight : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ), κ.swapLeft.sectL = κ.sectR
-- Mathlib.CategoryTheory.Yoneda
/-- The natural transformation `uliftYoneda.obj X ⟶ F.op ⋙ uliftYoneda.obj (F.obj X)`
when `F : C ⥤ D` and `X : C`.  -/
CategoryTheory.uliftYonedaMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (X : C) →
            CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶
              F.op.comp (CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X))
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isSeparating_bot_of_isThin : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C], ⊥.IsSeparating
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- A sequence of uniformly integrable functions which converges μ-a.e. converges in Lp.  -/
MeasureTheory.tendsto_Lp_finite_of_tendsto_ae : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} [MeasureTheory.IsFiniteMeasure μ],
  1 ≤ p →
    p ≠ ⊤ →
      ∀ {f : ℕ → α → β} {g : α → β},
        (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
          MeasureTheory.MemLp g p μ →
            MeasureTheory.UnifIntegrable f p μ →
              (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
                Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)
-- Mathlib.Analysis.Distribution.Support
/-- **Alias** of `Distribution.TemperedDistribution.dsupport_smulLeftCLM_subset`. -/
Distribution.dsupport_smulLeftCLM_subset : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedSpace ℂ F] {f : TemperedDistribution E F} {g : E → ℂ},
  Function.HasTemperateGrowth g →
    Distribution.dsupport ⇑((TemperedDistribution.smulLeftCLM F g) f) ⊆ Distribution.dsupport ⇑f
-- Mathlib.Data.Set.Image
Set.image_comp_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ}, Set.image (g ∘ f) = Set.image g ∘ Set.image f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_keys : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, t.keys.isEmpty = t.isEmpty
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableAtFilter_rpow_atTop_iff : ∀ {s : ℝ}, MeasureTheory.IntegrableAtFilter (fun x => x ^ s) Filter.atTop MeasureTheory.volume ↔ s < -1
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (Y.presheaf.obj (Opposite.op U)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).toSpecΓ
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.app f U)) h) =
    CategoryTheory.CategoryStruct.comp (f ∣_ U) (CategoryTheory.CategoryStruct.comp U.toSpecΓ h)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mk : {L : FirstOrder.Language} →
  {M : Type w} →
    [inst : L.Structure M] →
      (carrier : Set M) → (∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier) → L.Substructure M
-- Mathlib.Data.Set.Pairwise.Basic
/-- Simp normal form of `pairwise_ne_iff_injective`.  -/
pairwise_not_eq_iff_injective : ∀ {α : Type u_1} {ι : Type u_4} {f : ι → α}, (Pairwise fun i j => ¬f i = f j) ↔ Function.Injective f
-- Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
/-- The combination `E₄³ - E₆²` viewed as a level-1 modular form of weight 12.  -/
_private.Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing.0.ModularForm.E₄CubeSubE₆SqForm : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
-- Mathlib.GroupTheory.Commensurable
Subgroup.Commensurable.commensurable_conj : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (g : ConjAct G), H.Commensurable K ↔ (g • H).Commensurable (g • K)
-- Std.Http.Internal.LowerCase
_private.Std.Http.Internal.LowerCase.0.Std.Http.Internal.String.toLower_eq_self_iff : ∀ {s : String}, s.toLower = s ↔ s.toList.any Char.isUpper = false
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_insert_zero : ∀ {R : Type u} [inst : NonAssocRing R] (s : Set R), Subring.closure (insert 0 s) = Subring.closure s
-- Init.Data.Int.Linear
Int.Internal.Linear.not_le_norm_expr_cert : Int.Internal.Linear.Expr → Int.Internal.Linear.Expr → Int.Internal.Linear.Poly → Bool
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.toDigitsCore.eq_def : ∀ (base x x_1 : ℕ) (x_2 : List Char),
  base.toDigitsCore x x_1 x_2 =
    match x, x_1, x_2 with
    | 0, x, ds => ds
    | fuel.succ, n, ds =>
      have d := (n % base).digitChar;
      have n' := n / base;
      if n' = 0 then d :: ds else base.toDigitsCore fuel n' (d :: ds)
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compl₁₂_comp_left : ∀ {R₁ : Type u_3} {R₂ : Type u_4} [inst : Semiring R₁] [inst_1 : Semiring R₂] {Mₗ : Type u_6} {N : Type u_7}
  {Pₗ : Type u_9} {Qₗ : Type u_10} {Qₗ' : Type u_11} [inst_2 : AddCommMonoid Mₗ] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid Pₗ] [inst_5 : AddCommMonoid Qₗ] [inst_6 : AddCommMonoid Qₗ'] [inst_7 : Module R₁ Mₗ]
  [inst_8 : Module R₂ N] [inst_9 : Module R₂ Pₗ] [inst_10 : Module R₁ Pₗ] [inst_11 : Module R₁ Qₗ]
  [inst_12 : Module R₂ Qₗ'] {Tₗ : Type u_12} [inst_13 : AddCommMonoid Tₗ] [inst_14 : Module R₁ Tₗ]
  [inst_15 : SMulCommClass R₂ R₁ Pₗ] (f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ) (g : Qₗ →ₗ[R₁] Mₗ) (g' : Qₗ' →ₗ[R₂] N)
  (h : Tₗ →ₗ[R₁] Qₗ), f.compl₁₂ (g ∘ₗ h) g' = f.compl₁₂ g g' ∘ₗ h
-- Init.GrindInstances.ToInt
Lean.Grind.instDivBitVecUint : ∀ {v : ℕ}, Lean.Grind.ToInt.Div (BitVec v) (Lean.Grind.IntInterval.uint v)
-- Mathlib.Data.Num.Lemmas
Num.cast_one : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α], ↑1 = 1
-- Mathlib.GroupTheory.Abelianization.Defs
instUniqueAbelianization : (G : Type u) → [inst : Group G] → [Unique G] → Unique (Abelianization G)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeValueResult : Type
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- Extension of `PolynomialLaw.add_def_apply`  -/
PolynomialLaw.toFun_add_apply : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_4}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f g : M →ₚₗ[R] N) {S : Type u_5} [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S] (t : TensorProduct R S M),
  PolynomialLaw.toFun S (f + g) t = PolynomialLaw.toFun S f t + PolynomialLaw.toFun S g t
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.closure_eq_of_le : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Set M} {S : Submonoid M},
  s ⊆ ↑S → S ≤ Submonoid.closure s → Submonoid.closure s = S