mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.instUniqueHomTerminal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → (d : CategoryTheory.Factorisation f) → Unique (d ⟶ CategoryTheory.Factorisation.terminal)
-- Mathlib.Dynamics.Ergodic.Action.Basic
/-- An additive group action of `G` on a space `α` with measure `μ` is called *ergodic*,
if for any (null) measurable set `s`,
if it is a.e.-invariant under each scalar addition `(g +ᵥ ·)`, `g : G`,
then it is either null or conull.
 -/
ErgodicVAdd : (G : Type u_1) → (α : Type u_2) → [VAdd G α] → {x : MeasurableSpace α} → MeasureTheory.Measure α → Prop
-- Mathlib.Data.Multiset.Powerset
/-- Helper function for `powersetCard`. Given a list `l`, `powersetCardAux n l` is the list
of sublists of length `n`, as multisets.  -/
Multiset.powersetCardAux : {α : Type u_1} → ℕ → List α → List (Multiset α)
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.fromIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y)
  (f : CategoryTheory.WalkingIso.one ⟶ CategoryTheory.WalkingIso.zero),
  (CategoryTheory.WalkingIso.fromIso e).map f = e.inv
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_ofHom_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n : ℤ} (f : F ⟶ G) (z : CochainComplex.HomComplex.Cochain G K n) (m : ℤ),
  CochainComplex.HomComplex.δ n m ((CochainComplex.HomComplex.Cochain.ofHom f).comp z ⋯) =
    (CochainComplex.HomComplex.Cochain.ofHom f).comp (CochainComplex.HomComplex.δ n m z) ⋯
-- Mathlib.Topology.Algebra.ConstMulAction
/-- `smul` is a closed map in the second argument.

The lemma that `smul` is a closed map in the first argument (for a normed space over a complete
normed field) is `isClosedMap_smul_left` in `Analysis.Normed.Module.FiniteDimension`.  -/
isClosedMap_smul_of_ne_zero : ∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [ContinuousConstSMul G₀ α] {c : G₀}, c ≠ 0 → IsClosedMap fun x => c • x
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The angle ∠ABA at a point is `0`, unless `A = B`.  -/
EuclideanGeometry.angle_self_of_ne : ∀ {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 ≠ p₀ → EuclideanGeometry.angle p p₀ p = 0
-- Mathlib.Order.Filter.IsBounded
Antitone.isBoundedUnder_le_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : Filter γ} {u : γ → α}
  {v : α → β},
  Antitone v → Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l u → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (v ∘ u)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.w : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (φ : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left φ) g.hom = f.hom
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- The affine homeomorphism `V ≃ᴬ[k] P` given by `v ↦ v +ᵥ p`. This is `Equiv.vaddConst`
as a `ContinuousAffineEquiv`.  -/
ContinuousAffineEquiv.vaddConst : (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₁] →
                [inst_5 : TopologicalSpace V₁] → [IsTopologicalAddTorsor P₁] → P₁ → V₁ ≃ᴬ[k] P₁
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.compactSpace_iff_exists : ∀ {X : AlgebraicGeometry.Scheme}, CompactSpace ↥X ↔ ∃ R f, Function.Surjective ⇑f
-- Mathlib.RingTheory.Polynomial.Pochhammer
monic_descPochhammer : ∀ (R : Type u) [inst : Ring R] (n : ℕ) [Nontrivial R] [NoZeroDivisors R], (descPochhammer R n).Monic
-- Mathlib.Algebra.GroupWithZero.Basic
NeZero.pow : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀] [NeZero a], NeZero (a ^ n)
-- Mathlib.Tactic.FunProp.Theorems
/-- function property name  -/
Mathlib.Meta.FunProp.FunctionTheorem.funPropName : Mathlib.Meta.FunProp.FunctionTheorem → Lean.Name
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- See also `Multipliable.congr_cofinite`, which does not have a non-vanishing condition, but instead
requires the target to be a group under multiplication (and hence fails for infinite products in a
ring).
 -/
Multipliable.congr_cofinite₀ : ∀ {α : Type u_1} {K : Type u_4} [inst : CommGroupWithZero K] [inst_1 : TopologicalSpace K] {f g : α → K}
  [SeparatelyContinuousMul K],
  Multipliable f → (∀ (a : α), f a ≠ 0) → (∀ᶠ (a : α) in Filter.cofinite, f a = g a) → Multipliable g
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_union : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  Disjoint s₁ s₂ → MeasurableSet s₂ → μ (s₁ ∪ s₂) = μ s₁ + μ s₂
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
AbsConvexOpenSets.instCoeOut : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : TopologicalSpace E] →
      [inst_1 : AddCommMonoid E] →
        [inst_2 : SeminormedRing 𝕜] →
          [inst_3 : SMul 𝕜 E] → [inst_4 : PartialOrder 𝕜] → CoeOut (AbsConvexOpenSets 𝕜 E) (Set E)
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- The `AddSubmonoid` generated by an element of an `AddMonoid` equals the set of
natural number multiples of the element.  -/
AddSubmonoid.mem_closure_singleton : ∀ {A : Type u_2} [inst : AddMonoid A] {x y : A}, y ∈ AddSubmonoid.closure {x} ↔ ∃ n, n • x = y
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_iff_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α}, ¬IsMin a → (Order.pred a < b ↔ a ≤ b)
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.Hom.ext : ∀ {A B : AddCommGrpCat} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftId_inv_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  (X : CategoryTheory.MorphismProperty.Comma L R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftId L R).inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Std.Data.TreeMap.Basic
Std.TreeMap.instBEq : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [BEq β] → BEq (Std.TreeMap α β cmp)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.SurjectiveOnWith.mono : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {f : NormedAddGroupHom V₁ V₂} {K : AddSubgroup V₂} {C C' : ℝ},
  f.SurjectiveOnWith K C → C ≤ C' → f.SurjectiveOnWith K C'
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocExtension.getSimprocs : Lean.Meta.Simp.SimprocExtension → Lean.CoreM Lean.Meta.Simprocs
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₂_exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (self : CategoryTheory.ShortComplex.SnakeInput C), self.L₂.Exact
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} [inst_3 : G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A}
  (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D}
  {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y Y' : C} (f : G.obj Y ⟶ X) (f' : G.obj Y' ⟶ X)
  {W : C} (a : W ⟶ Y) (b : W ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (G.map a) f = CategoryTheory.CategoryStruct.comp (G.map b) f' →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f) (F.map a.op) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f') (F.map b.op)
-- Mathlib.Algebra.Module.ULift
ULift.smulLeft.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M], ULift.smulLeft = { smul := fun s x => s.down • x }
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.inrCompSum'_hom_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A C)
  (G : CategoryTheory.Functor B C) (X : B),
  (F.inrCompSum' G).hom.app X = CategoryTheory.CategoryStruct.id ((F.sum' G).obj (Sum.inr X))
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.epi_iff_range_eq_top : ∀ {A B : GrpCat} (f : A ⟶ B), CategoryTheory.Epi f ↔ (GrpCat.Hom.hom f).range = ⊤
-- Mathlib.CategoryTheory.Sites.RegularEpi
CategoryTheory.isRegularEpiCategory_sheaf : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasPushouts D] [CategoryTheory.IsRegularEpiCategory D],
  (∀ {F G : CategoryTheory.Sheaf J D} (f : F ⟶ G) [CategoryTheory.Epi f],
      ∃ I p i, CategoryTheory.Epi p ∧ CategoryTheory.Mono i ∧ CategoryTheory.CategoryStruct.comp p i = f.hom) →
    ∀ [CategoryTheory.HasSheafify J D] [CategoryTheory.Balanced (CategoryTheory.Sheaf J D)],
      CategoryTheory.IsRegularEpiCategory (CategoryTheory.Sheaf J D)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.mk.sizeOf_spec : ∀ (toSheafedSpace : AlgebraicGeometry.SheafedSpace CommRingCat)
  (isLocalRing : ∀ (x : ↑↑toSheafedSpace.toPresheafedSpace), IsLocalRing ↑(toSheafedSpace.presheaf.stalk x)),
  sizeOf { toSheafedSpace := toSheafedSpace, isLocalRing := isLocalRing } = 1 + sizeOf toSheafedSpace
-- Mathlib.Order.Heyting.Basic
OrderDual.instGeneralizedHeytingAlgebra : {α : Type u_2} → [GeneralizedCoheytingAlgebra α] → GeneralizedHeytingAlgebra αᵒᵈ
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.associator_hom_left_snd_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X) {Z : C} (h : S.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.snd R.hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd S.hom T.hom) T.hom))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst S.hom T.hom) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).hom T.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd R.hom S.hom) h)
-- Mathlib.Data.Rel
SetRel.core.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t : Set β), R.core t = {a | ∀ ⦃b : β⦄, (a, b) ∈ R → b ∈ t}
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.source_subset_preimage_source : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAtOfComplement F I J n f x), h.domChart.source ⊆ f ⁻¹' h.codChart.source
-- Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
/-- **Dominated convergence theorem** for filters with a countable basis and
AEMeasurable functions.  -/
MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_2} {l : Filter ι}
  [l.IsCountablyGenerated] {F : ι → α → ENNReal} {f : α → ENNReal} (bound : α → ENNReal),
  (∀ᶠ (n : ι) in l, AEMeasurable (F n) μ) →
    (∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) →
      ∫⁻ (a : α), bound a ∂μ ≠ ⊤ →
        (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) l (nhds (f a))) →
          Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) l (nhds (∫⁻ (a : α), f a ∂μ))
-- Mathlib.Data.List.Basic
List.cons_injective : ∀ {α : Type u} {a : α}, Function.Injective (List.cons a)
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.associatesNonZeroDivisorsEquivIsPrincipal.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R],
  Ideal.associatesNonZeroDivisorsEquivIsPrincipal R = Ideal.associatesNonZeroDivisorsEquivIsPrincipal R
-- Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
_private.Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear.0.mem_aux : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {EB : Type u_4} [inst_4 : NormedAddCommGroup EB]
  [inst_5 : NormedSpace 𝕜 EB] {HB : Type u_5} [inst_6 : TopologicalSpace HB] [inst_7 : ChartedSpace HB B]
  {IB : ModelWithCorners 𝕜 EB HB} {e : OpenPartialHomeomorph (B × F) (B × F)} {n : WithTop ℕ∞},
  e ∈
      ⋃ φ,
        ⋃ U,
          ⋃ (hU : IsOpen U),
            ⋃ (hφ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x)) U),
              ⋃ (h2φ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x).symm) U),
                {e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)} ↔
    ∃ φ U,
      ∃ (hU : IsOpen U) (hφ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x)) U) (h2φ :
        ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x).symm) U),
        e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableWithinAt.mono_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {s t : Set E} {x v : E},
  LineDifferentiableWithinAt 𝕜 f s x v → s ∈ nhdsWithin x t → LineDifferentiableWithinAt 𝕜 f t x v
-- Lean.Data.KVMap
Lean.DataValue.ofNat.sizeOf_spec : ∀ (v : ℕ), sizeOf (Lean.DataValue.ofNat v) = 1 + sizeOf v
-- Mathlib.Data.Nat.Nth
Nat.nth_mem_of_infinite : ∀ {p : ℕ → Prop}, (Set.ofPred p).Infinite → ∀ (n : ℕ), p (Nat.nth p n)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure.eq_1 : ∀ {α : Type u_2} (M : Matroid α) (X : Set α), M.closure X = ⋂₀ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F}
-- Lean.Syntax
Lean.Syntax.Range.mk.injEq : ∀ (start stop start_1 stop_1 : String.Pos.Raw),
  ({ start := start, stop := stop } = { start := start_1, stop := stop_1 }) = (start = start_1 ∧ stop = stop_1)
-- Mathlib.Tactic.Tauto
/-- Function elaborating `Config`.  -/
Mathlib.Tactic.Tauto.elabConfig : Lean.Syntax →
  optParam Mathlib.Tactic.Tauto.Config { } → optParam Bool true → Lean.Elab.Tactic.TacticM Mathlib.Tactic.Tauto.Config
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.filterAt_neBot : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) (x : X), (v.filterAt x).NeBot
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.one_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.MonObj M]
  [inst_4 : CategoryTheory.MonObj N],
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)
-- Batteries.Data.List.Basic
List.swap.eq_5 : ∀ {α : Type u_1} (a : α) (xs : List α) (i j : ℕ), (a :: xs).swap i.succ j.succ = a :: xs.swap i j
-- Batteries.Recycling.RBTree.Basic
/-- A path that goes down the right subtree.  -/
RBTree.RBNode.Path.right : {α : Type u} → RBTree.RBColor → RBTree.RBNode α → α → RBTree.RBNode.Path α → RBTree.RBNode.Path α
-- Mathlib.Order.Interval.Finset.Basic
Finset.left_notMem_Ioc : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], a ∉ Finset.Ioc a b
-- Aesop.Index
Aesop.Index.byTarget : {α : Type} → Aesop.Index α → Lean.Meta.DiscrTree (Aesop.Rule α)
-- Mathlib.Algebra.Group.Hom.Instances
/-- `(M →* N)` is a `CommMonoid` if `N` is commutative.  -/
MonoidHom.instCommMonoid : {M : Type uM} → {N : Type uN} → [inst : MulOneClass M] → [inst_1 : CommMonoid N] → CommMonoid (M →* N)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.equiv_inverse_obj_functor : ∀ (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]
  (F : CategoryTheory.Functor C V), ((CategoryTheory.MonoidalCategory.DayFunctor.equiv C V).inverse.obj F).functor = F
-- Mathlib.Algebra.Free
FreeMagma.length.eq_2 : ∀ {α : Type u} (x_1 y : FreeMagma α), (x_1.mul y).length = x_1.length + y.length
-- Mathlib.Algebra.Order.Group.DenselyOrdered
exists_pow_lt_of_one_lt : ∀ {M : Type u_2} [inst : LinearOrder M] [DenselyOrdered M] {x : M} [inst_2 : CommMonoid M] [ExistsMulOfLE M]
  [IsOrderedCancelMonoid M], 1 < x → ∀ (n : ℕ), ∃ y, 1 < y ∧ y ^ n < x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.simplex_fst_succ : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d} {l : Fin d},
  SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ → (x.cast hd).simplex.1 l.succ = k.succ
-- Lean.Meta.Diagnostics
Lean.Meta.instInhabitedDiagSummary : Inhabited Lean.Meta.DiagSummary
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.prun_ofPostconditionT : ∀ {m : Type u_1 → Type u_2} {α γ : Type u_1} [inst : Monad m] [LawfulMonad m] {x : Std.Iterators.PostconditionT m α}
  {f : (x_1 : α) → (Std.Iterators.HetT.ofPostconditionT x).Property x_1 → m γ},
  (Std.Iterators.HetT.ofPostconditionT x).prun f = do
    let a ← x.operation
    f ↑a ⋯
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.im_inv_neg_coe_pos : ∀ (z : UpperHalfPlane), 0 < (-↑z)⁻¹.im
-- Mathlib.Data.Nat.Choose.Basic
Nat.add_choose_mul_factorial_mul_factorial : ∀ (i j : ℕ), (i + j).choose j * i.factorial * j.factorial = (i + j).factorial
-- Mathlib.Topology.CompactOpen
/-- The uncurried form of a continuous map `X → C(Y, Z)` is a continuous map `X × Y → Z`.  -/
ContinuousMap.continuous_uncurry_of_continuous : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [LocallyCompactSpace Y] (f : C(X, C(Y, Z))),
  Continuous (Function.uncurry fun x y => (f x) y)
-- Batteries.Data.AssocList
Batteries.AssocList.all_eq : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (l : Batteries.AssocList α β),
  Batteries.AssocList.all p l =
    l.toList.all fun x =>
      match x with
      | (a, b) => p a b
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.LevyProkhorov.dist_finiteMeasure_def : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (μ ν : MeasureTheory.LevyProkhorov (MeasureTheory.FiniteMeasure Ω)),
  dist μ ν = MeasureTheory.levyProkhorovDist ↑μ.toMeasure ↑ν.toMeasure
-- Std.Http.Data.Chunk
Std.Http.Chunk.instToStringExtensionName : ToString Std.Http.Chunk.ExtensionName
-- Mathlib.LinearAlgebra.BilinearMap
/-- Make a bilinear map from a function and a bundled statement of bilinearity.  -/
IsBilinearMap.toLinearMap : {R : Type u_1} →
  [inst : CommSemiring R] →
    {E : Type u_2} →
      [inst_1 : AddCommMonoid E] →
        [inst_2 : Module R E] →
          {F : Type u_3} →
            [inst_3 : AddCommMonoid F] →
              [inst_4 : Module R F] →
                {G : Type u_4} →
                  [inst_5 : AddCommMonoid G] →
                    [inst_6 : Module R G] → {f : E → F → G} → IsBilinearMap R f → E →ₗ[R] F →ₗ[R] G
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic.0.tacticMap_simp : Lean.ParserDescr
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
CategoryTheory.Adjunction.derivedη_fac_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂}
  (W₁ : CategoryTheory.MorphismProperty C₁) [inst_4 : L₁.IsLocalization W₁] {G' : CategoryTheory.Functor D₁ D₂}
  {F' : CategoryTheory.Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F')
  [inst_5 :
    (G'.comp F').IsLeftDerivedFunctor
      (CategoryTheory.CategoryStruct.comp (L₁.associator G' F').inv (CategoryTheory.Functor.whiskerRight α F')) W₁]
  (X₁ : C₁),
  CategoryTheory.CategoryStruct.comp ((adj.derivedη W₁ α β).app (L₁.obj X₁)) (F'.map (α.app X₁)) =
    CategoryTheory.CategoryStruct.comp (L₁.map (adj.unit.app X₁)) (β.app (G.obj X₁))
-- Init.Data.Array.MapIdx
_private.Init.Data.Array.MapIdx.0.List.mapFinIdxM_toArray.go : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α}
  {f : (i : ℕ) → α → i < l.length → m β} (i : ℕ) (acc : Array β) (inv : i + acc.size = l.length),
  Array.mapFinIdxM.map l.toArray f i acc.size inv acc =
    List.toArray <$> List.mapFinIdxM.go l f (List.drop acc.size l) acc ⋯
-- Mathlib.Algebra.DirectSum.Module
DirectSum.instModule : {R : Type u} →
  [inst : Semiring R] →
    {ι : Type v} →
      {M : ι → Type w} →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] → [(i : ι) → Module R (M i)] → Module R (DirectSum ι fun i => M i)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If `(F', α)` is a left Kan extension of `F` along `L`, then `(F', α)` is an initial object
in the category `LeftExtension L F`.  -/
CategoryTheory.Functor.isUniversalOfIsLeftKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : F ⟶ L.comp F') →
                    [F'.IsLeftKanExtension α] →
                      CategoryTheory.StructuredArrow.IsUniversal (CategoryTheory.Functor.LeftExtension.mk F' α)