mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Index
Subgroup.index_toAddSubgroup : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, (Subgroup.toAddSubgroup H).index = H.index
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z T : C} {a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ} (α : CategoryTheory.Abelian.Ext X Y a₁)
  (β : CategoryTheory.Abelian.Ext Y Z a₂) (γ : CategoryTheory.Abelian.Ext Z T a₃) (h₁₂ : a₁ + a₂ = a₁₂)
  (h₂₃ : a₂ + a₃ = a₂₃) (h : a₁ + a₂ + a₃ = a), (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Functor.toStructuredArrow_comp_proj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (X : D)
  (F : CategoryTheory.Functor C D) (f : (Y : E) → X ⟶ F.obj (G.obj Y))
  (h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z),
  (G.toStructuredArrow X F f ⋯).comp (CategoryTheory.StructuredArrow.proj X F) = G
-- Batteries.Data.Nat.Basic
/-- Diagonal recursor for `Nat`
 -/
Nat.casesDiagOn : {motive : ℕ → ℕ → Sort u_1} →
  (m n : ℕ) →
    motive 0 0 →
      ((n : ℕ) → motive 0 (n + 1)) → ((m : ℕ) → motive (m + 1) 0) → ((m n : ℕ) → motive (m + 1) (n + 1)) → motive m n
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_eq_none_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t.max? = none ↔ t = ∅
-- Mathlib.Computability.Primrec.Basic
_private.Mathlib.Computability.Primrec.Basic.0.Encodable.decodeSum.match_1.eq_1 : ∀ (motive : Bool → ℕ → Sort u_1) (m : ℕ) (h_1 : (m : ℕ) → motive false m) (h_2 : (x : Bool) → (m : ℕ) → motive x m),
  (match false, m with
    | false, m => h_1 m
    | x, m => h_2 x m) =
    h_1 m
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.naturalityProperty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F₁ F₂ : CategoryTheory.Functor C D} (app : (X : C) → F₁.obj X ⟶ F₂.obj X),
  (CategoryTheory.MorphismProperty.naturalityProperty app).IsMultiplicative
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_eq_get! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {a : α} {h' : a ∈ m}, m.get a h' = m.get! a
-- Mathlib.Topology.Sets.VietorisTopology
/-- When `Set` is equipped with the Vietoris topology, taking the image under an embedding is an
embedding.  -/
Topology.IsEmbedding.image_vietoris : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsEmbedding f → Topology.IsEmbedding fun x => f '' x
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_neg : ∀ {u : ℕ → EReal}, LinearGrowth.linearGrowthInf (-u) = -LinearGrowth.linearGrowthSup u
-- Mathlib.Algebra.Lie.Abelian
Function.Surjective.isLieAbelian : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] {f : L₁ →ₗ⁅R⁆ L₂},
  Function.Surjective ⇑f → IsLieAbelian L₁ → IsLieAbelian L₂
-- Init.Data.Nat.Sqrt.Lemmas
_private.Init.Data.Nat.Sqrt.Lemmas.0.Nat.sqrt_isSqrt : ∀ (n : ℕ), Nat.IsSqrt✝ n n.sqrt
-- Mathlib.Order.Monotone.Basic
Nat.rel_of_forall_rel_succ_of_le_of_lt : ∀ {β : Type v} (r : β → β → Prop) [IsTrans β r] {f : ℕ → β} {a : ℕ},
  (∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))) → ∀ ⦃b c : ℕ⦄, a ≤ b → b < c → r (f b) (f c)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrictIndepMatroid_E : ∀ {α : Type u_1} (M : Matroid α) (R : Set α), (M.restrictIndepMatroid R).E = R
-- Init.Data.UInt.Lemmas
USize.toUInt8_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < USize.size → (USize.ofNatClamp n).toUInt8 = UInt8.ofNat n
-- Mathlib.Algebra.Group.Basic
inv_eq_iff_eq_inv : ∀ {G : Type u_3} [inst : InvolutiveInv G] {a b : G}, a⁻¹ = b ↔ a = b⁻¹
-- Mathlib.Topology.FiberBundle.Constructions
FiberBundle.pullback : {B : Type u} →
  {F : Type v} →
    {E : B → Type w₁} →
      {B' : Type w₂} →
        [inst : TopologicalSpace B'] →
          [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] →
            [inst_2 : TopologicalSpace F] →
              [inst_3 : TopologicalSpace B] →
                [∀ (_b : B), Nonempty (E _b)] →
                  {K : Type U} →
                    [inst_5 : FunLike K B' B] →
                      [ContinuousMapClass K B' B] →
                        [inst_7 : (x : B) → TopologicalSpace (E x)] →
                          [FiberBundle F E] → (f : K) → FiberBundle F (⇑f *ᵖ E)
-- Mathlib.RingTheory.MvPowerSeries.Rename
/-- `rename` is an equivalence when the underlying map is an equivalence.  -/
MvPowerSeries.renameEquiv : {σ : Type u_1} →
  {τ : Type u_2} → (R : Type u_4) → [inst : CommSemiring R] → σ ≃ τ → MvPowerSeries σ R ≃ₐ[R] MvPowerSeries τ R
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.pointwiseRightKanExtension_obj : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasPointwiseRightKanExtension F]
  (Y : D),
  (L.pointwiseRightKanExtension F).obj Y =
    CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj Y L).comp F)
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.isOpen_union_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → (IsOpen (s ∪ t) ↔ IsOpen s ∧ IsOpen t)
-- Mathlib.Order.Lattice
Monotone.le_map_sup : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {f : α → β},
  Monotone f → ∀ (x y : α), f x ⊔ f y ≤ f (x ⊔ y)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryLT!_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} [inst : Inhabited (α × β)],
          Std.DTreeMap.Internal.Impl.Const.getEntryLT! k t₁ = Std.DTreeMap.Internal.Impl.Const.getEntryLT! k t₂
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_eq_if : ∀ {n : ℕ}, (*...n).toList = if 0 < n then (*...n - 1).toList ++ [n - 1] else []
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instFunLike : {𝕜 : Type u_2} → {α : Type u_5} → [inst : Zero 𝕜] → [inst_1 : LE α] → FunLike (IncidenceAlgebra 𝕜 α) α (α → 𝕜)
-- Std.Http.Internal.ChunkedBuffer
/-- Writes a `String` to the `ChunkedBuffer`.
 -/
Std.Http.Internal.ChunkedBuffer.writeString : Std.Http.Internal.ChunkedBuffer → String → Std.Http.Internal.ChunkedBuffer
-- Mathlib.Topology.Algebra.Field
/-- Right-multiplication by a nonzero element of a topological division ring is proper, i.e.,
inverse images of compact sets are compact.  -/
Filter.tendsto_cocompact_mul_right₀ : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : TopologicalSpace K] [SeparatelyContinuousMul K] {a : K},
  a ≠ 0 → Filter.Tendsto (fun x => x * a) (Filter.cocompact K) (Filter.cocompact K)
-- Mathlib.Algebra.Order.Chebyshev
/-- **Chebyshev's Sum Inequality**: When `f` and `g` monovary together (e.g. they are both
monotone/antitone), the scalar product of their sum is less than the size of the set times their
scalar product.  -/
Monovary.sum_smul_sum_le_card_smul_sum : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulMono α β] {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Monovary f g → (∑ i, f i) • ∑ i, g i ≤ Fintype.card ι • ∑ i, f i • g i
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f g : 𝕜 → F},
  ContDiffAt 𝕜 (↑n) f x → ContDiffAt 𝕜 (↑n) g x → iteratedDeriv n (f - g) x = iteratedDeriv n f x - iteratedDeriv n g x
-- Lean.Parser.Term
Lean.Parser.Term.letRecDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- The homotopy between morphisms in `ShortComplex Cᵒᵖ` that is induced by a homotopy
between morphisms in `ShortComplex C`.  -/
CategoryTheory.ShortComplex.Homotopy.op : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ : S₁ ⟶ S₂} →
          CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ →
            CategoryTheory.ShortComplex.Homotopy (CategoryTheory.ShortComplex.opMap φ₁)
              (CategoryTheory.ShortComplex.opMap φ₂)
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Basis.ofRankEqZero_apply : ∀ {K : Type u} {V : Type v} [inst : Ring K] [inst_1 : StrongRankCondition K] [inst_2 : AddCommGroup V]
  [inst_3 : Module K V] [inst_4 : Module.Free K V] {ι : Type u_1} [inst_5 : IsEmpty ι] (hV : Module.rank K V = 0)
  (i : ι), (Basis.ofRankEqZero hV) i = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.prod_le_iff : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] {s : Submonoid M} {t : Submonoid N}
  {u : Submonoid (M × N)},
  s.prod t ≤ u ↔ Submonoid.map (MonoidHom.inl M N) s ≤ u ∧ Submonoid.map (MonoidHom.inr M N) t ≤ u
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvironmentHeader.mk.injEq : ∀ (trustLevel : UInt32) (mainModule : Lean.Name) (isModule : Bool) (imports : Array Lean.Import)
  (regions : Array Lean.CompactedRegion) (modules : Array Lean.EffectiveImport)
  (moduleName2Idx : Std.HashMap Lean.Name Lean.ModuleIdx) (importAllModules : Array Lean.EffectiveImport)
  (moduleData : Array Lean.ModuleData) (trustLevel_1 : UInt32) (mainModule_1 : Lean.Name) (isModule_1 : Bool)
  (imports_1 : Array Lean.Import) (regions_1 : Array Lean.CompactedRegion) (modules_1 : Array Lean.EffectiveImport)
  (moduleName2Idx_1 : Std.HashMap Lean.Name Lean.ModuleIdx) (importAllModules_1 : Array Lean.EffectiveImport)
  (moduleData_1 : Array Lean.ModuleData),
  ({ trustLevel := trustLevel, mainModule := mainModule, isModule := isModule, imports := imports, regions := regions,
        modules := modules, moduleName2Idx := moduleName2Idx, importAllModules := importAllModules,
        moduleData := moduleData } =
      { trustLevel := trustLevel_1, mainModule := mainModule_1, isModule := isModule_1, imports := imports_1,
        regions := regions_1, modules := modules_1, moduleName2Idx := moduleName2Idx_1,
        importAllModules := importAllModules_1, moduleData := moduleData_1 }) =
    (trustLevel = trustLevel_1 ∧
      mainModule = mainModule_1 ∧
        isModule = isModule_1 ∧
          imports = imports_1 ∧
            regions = regions_1 ∧
              modules = modules_1 ∧
                moduleName2Idx = moduleName2Idx_1 ∧ importAllModules = importAllModules_1 ∧ moduleData = moduleData_1)
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- For a reflective functor `i` (with left adjoint `L`), with unit `η`, we have `η_iL = iL η`.
 -/
CategoryTheory.unit_obj_eq_map_unit : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.Reflective i] (X : C),
  (CategoryTheory.reflectorAdjunction i).unit.app (i.obj ((CategoryTheory.reflector i).obj X)) =
    i.map ((CategoryTheory.reflector i).map ((CategoryTheory.reflectorAdjunction i).unit.app X))
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.comp_c : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C}
  (α : X.Hom Y) (β : Y.Hom Z),
  (AlgebraicGeometry.PresheafedSpace.comp α β).c =
    CategoryTheory.CategoryStruct.comp β.c ((TopCat.Presheaf.pushforward C β.base).map α.c)
-- Init.Data.Option.Lemmas
Option.pbind_congr : ∀ {α : Type u_1} {β : Type u_2} {o o' : Option α} (ho : o = o') {f : (a : α) → o = some a → Option β}
  {g : (a : α) → o' = some a → Option β}, (∀ (a : α) (h : o' = some a), f a ⋯ = g a h) → o.pbind f = o'.pbind g
-- Mathlib.NumberTheory.NumberField.CMField
/-- If `K/F` is a CM-extension then `K` is a CM-field.
 -/
NumberField.IsCMField.ofCMExtension : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [NumberField.IsTotallyReal F] [inst_2 : Field K] [inst_3 : CharZero K]
  [Algebra.IsIntegral ℚ K] [NumberField.IsTotallyComplex K] [inst_6 : Algebra F K] [Algebra.IsQuadraticExtension F K],
  NumberField.IsCMField K
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.adaptExcept_EStateM : ∀ {ε ε' α σ : Type u_1} {x : EStateM ε σ α} (f : ε → ε')
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε' (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))),
  ⦃(Std.Do.wp x).apply (Q.1, fun e => Q.2.1 (f e), Q.2.2)⦄ EStateM.adaptExcept f x ⦃Q⦄
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.primesOver.eq_1 : ∀ {A : Type u_2} [inst : CommSemiring A] (p : Ideal A) (B : Type u_3) [inst_1 : Semiring B] [inst_2 : Algebra A B],
  p.primesOver B = {P | P.IsPrime ∧ P.LiesOver p}
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false → (Std.ExtHashMap.ofList l).getKeyD k fallback = fallback
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mulArchimedean_of_mk_eq_mk : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  (∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → MulArchimedeanClass.mk a = MulArchimedeanClass.mk b) → MulArchimedean M
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.addCommute_inl_inr : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (m : M) (n : N),
  AddCommute ((AddMonoidHom.inl M N) m) ((AddMonoidHom.inr M N) n)
-- Mathlib.Analysis.Complex.Angle
/-- Chord-length is a multiple of arc-length up to constants.  -/
Complex.norm_sub_mem_Icc_angle : ∀ {x y : ℂ},
  ‖x‖ = 1 → ‖y‖ = 1 → ‖x - y‖ ∈ Set.Icc (2 / Real.pi * InnerProductGeometry.angle x y) (InnerProductGeometry.angle x y)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.convolution_comm : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} [inst : CommMonoid M] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid E] [inst_3 : Module S E] [inst_4 : TopologicalSpace E] (L : E →ₗ[S] E →ₗ[S] E) (f g : M → E),
  (∀ (x y : E), (L x) y = (L y) x) → DiscreteConvolution.convolution L f g = DiscreteConvolution.convolution L g f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.iteratedDeriv_add_one_cos : ∀ (n : ℕ), iteratedDeriv (n + 1) Complex.cos = -iteratedDeriv n Complex.sin
-- Mathlib.Data.Finset.Max
/-- `{a}.max' _` is `a`.  -/
Finset.max'_singleton : ∀ {α : Type u_2} [inst : LinearOrder α] (a : α), {a}.max' ⋯ = a
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.getThenInsertIfNew? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] {t : Std.DTreeMap.Internal.Impl α β} {k : α}
  {v : β k} {h : t.WF}, (t.getThenInsertIfNew? k v ⋯).2.WF
-- Init.System.ST
ST.instNonemptyRef : ∀ {σ α : Type} [s : Nonempty α], Nonempty (ST.Ref σ α)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.comap_comap_center : ∀ {G : Type u} [inst : Group G] {H₁ : Subgroup G} [inst_1 : H₁.Normal] {H₂ : Subgroup (G ⧸ H₁)} [inst_2 : H₂.Normal],
  Subgroup.comap (QuotientGroup.mk' H₁) (Subgroup.comap (QuotientGroup.mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) =
    Subgroup.comap (QuotientGroup.mk' (Subgroup.comap (QuotientGroup.mk' H₁) H₂))
      (Subgroup.center (G ⧸ Subgroup.comap (QuotientGroup.mk' H₁) H₂))
-- Mathlib.Algebra.Module.ZLattice.Summable
/-- Let `L` be a lattice with (possibly non-full) rank `d`, and `r : ℝ` such that `d < r`.
Then `∑ z ∈ L, ‖z‖⁻ʳ ≤ A⁻ʳ * ∑ k : ℕ, kᵈ⁻ʳ⁻¹` for some `A > 0` depending only on `L`.
This is an arbitrary choice of `A`. See `ZLattice.tsum_norm_rpow_le`.
 -/
ZLattice.tsumNormRPowBound : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] → [FiniteDimensional ℝ E] → (L : Submodule ℤ E) → [DiscreteTopology ↥L] → ℝ
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.of_subset : ∀ {α : Type u_1} {R R' : Set α} (M : Matroid α), R ⊆ R' → (M.restrict R).IsRestriction (M.restrict R')
-- Mathlib.Algebra.Category.Grp.Colimits
/-- The obvious additive map from `Quot (F ⋙ uliftFunctor.{u'})` to `Quot F`.
 -/
AddCommGrpCat.Colimits.quotUliftToQuot : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [inst_1 : DecidableEq J] →
        AddCommGrpCat.Colimits.Quot (F.comp AddCommGrpCat.uliftFunctor) →+ AddCommGrpCat.Colimits.Quot F
-- Mathlib.CategoryTheory.IsConnected
/-- If any functor to a discrete category is constant on objects, J is connected.
The converse of `any_functor_const_on_obj`.
 -/
CategoryTheory.IsConnected.of_any_functor_const_on_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [Nonempty J],
  (∀ {α : Type u₁} (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j j' : J), F.obj j = F.obj j') →
    CategoryTheory.IsConnected J
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonTextDocumentRegistrationOptions : Lean.ToJson Lean.Lsp.TextDocumentRegistrationOptions
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.toStructuredArrow_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (d : D) {X Y : (CategoryTheory.CostructuredArrow F d)ᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.CostructuredArrow.toStructuredArrow F d).map f = CategoryTheory.StructuredArrow.homMk f.unop.left.op ⋯
-- Std.Do.Triple.SpecLemmas
List.mem_of_range'_eq_append_cons : ∀ {s n step : ℕ} {xs : List ℕ} {i : ℕ} {ys : List ℕ}, List.range' s n step = xs ++ i :: ys → i ∈ List.range' s n step
-- Init.Data.List.BasicAux
_private.Init.Data.List.BasicAux.0.List.get.match_1.eq_2 : ∀ {α : Type u_1} (motive : (x : List α) → Fin x.length → Sort u_2) (head : α) (as : List α) (i : ℕ)
  (h : i.succ < (head :: as).length)
  (h_1 : (a : α) → (tail : List α) → (isLt : 0 < (a :: tail).length) → motive (a :: tail) ⟨0, isLt⟩)
  (h_2 : (head : α) → (as : List α) → (i : ℕ) → (h : i.succ < (head :: as).length) → motive (head :: as) ⟨i.succ, h⟩),
  (match head :: as, ⟨i.succ, h⟩ with
    | a :: tail, ⟨0, isLt⟩ => h_1 a tail isLt
    | head :: as, ⟨i.succ, h⟩ => h_2 head as i h) =
    h_2 head as i h
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
AddSubgroup.isClosed_of_discrete : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G]
  {H : AddSubgroup G} [DiscreteTopology ↥H], IsClosed ↑H
-- Init.Data.Array.Lex.Lemmas
Array.le_antisymm : ∀ {α : Type u_1} [inst : LT α] [inst_1 : LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] {xs ys : Array α},
  xs ≤ ys → ys ≤ xs → xs = ys
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsCompl.eq_1 : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (h : IsCompl p q) (φ : ↥p →ₗ[R] F)
  (ψ : ↥q →ₗ[R] F), LinearMap.ofIsCompl h φ ψ = φ.coprod ψ ∘ₗ ↑(p.prodEquivOfIsCompl q h).symm
-- Mathlib.CategoryTheory.Limits.Presentation
/-- A limit presentation of `X` over `J` is a diagram `{Dᵢ}` in `C` and natural maps
`sᵢ : X ⟶ Dᵢ` making `X` into the limit of the `Dᵢ`.  -/
CategoryTheory.Limits.LimitPresentation : {C : Type u} →
  [CategoryTheory.Category.{v, u} C] →
    (J : Type w) → [CategoryTheory.Category.{t, w} J] → C → Type (max (max (max t u) v) w)
-- Mathlib.Data.ENNReal.Basic
ENNReal.instLinearOrder : LinearOrder ENNReal
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.Reason.yes.sizeOf_spec : sizeOf Std.Time.Reason.yes✝ = 1
-- Mathlib.Order.Partition.Basic
Partition.mem_iff_exists_partOf : ∀ {α : Type u_1} {u s : Set α} {P : Partition u}, s ∈ P ↔ ∃ x ∈ u, P.partOf x = s
-- Mathlib.Tactic.MoveAdd
/-- Return a sorting key so that all `(a, true)`s are in the list's order
and sorted before all `(a, false)`s, which are also in the list's order.
Although `weight` does not require this, we use `weight` in the case where the list obtained
from `L` by only keeping the first component (i.e. `L.map Prod.fst`) has no duplicates.
The properties that we mention here assume that this is the case.

Thus, `weight L` is a function `α → ℤ` with the following properties:
* if `(a, true)  ∈ L`, then `weight L a` is strictly negative;
* if `(a, false) ∈ L`, then `weight L a` is strictly positive;
* if neither `(a, true)` nor `(a, false)` is in `L`, then `weight L a = 0`.

Moreover, the function `weight L` is strictly monotone increasing on both
`{a : α | (a, true) ∈ L}` and `{a : α | (a, false) ∈ L}`,
in the sense that if `a' = (a, true)` and `b' = (b, true)` are in `L`,
then `a'` appears before `b'` in `L` if and only if `weight L a < weight L b` and
similarly for the pairs with second coordinate equal to `false`.
 -/
Mathlib.MoveAdd.weight : {α : Type u_1} → [BEq α] → List (α × Bool) → α → ℤ
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.contains (t.maxD fallback) = true
-- Init.Data.Nat.Lemmas
Nat.pow_pos_iff : ∀ {a n : ℕ}, 0 < a ^ n ↔ 0 < a ∨ n = 0
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagations.mk.sizeOf_spec : ∀ (data : Lean.Meta.Grind.PendingSolverPropagationsData✝), sizeOf { data := data } = 1 + sizeOf data
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.abs_areaForm_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), |(o.areaForm x) y| ≤ ‖x‖ * ‖y‖
-- Mathlib.Algebra.GradedMonoid
/-- Multiplication is homogeneous  -/
SetLike.GradedMul.mul_mem : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {inst : SetLike S R} {inst_1 : Mul R} {inst_2 : Add ι} {A : ι → S}
  [self : SetLike.GradedMul A] ⦃i j : ι⦄ {gi gj : R}, gi ∈ A i → gj ∈ A j → gi * gj ∈ A (i + j)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.leftToRight_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C),
  CategoryTheory.Arrow.leftToRight.app f = f.hom
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.startsWith_dropWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String.Slice},
  (s.dropWhile pat).startsWith pat = false
-- Mathlib.GroupTheory.CoprodI
/-- Adjacent letters are not from the same summand.  -/
Monoid.CoprodI.Word.chain_ne : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (self : Monoid.CoprodI.Word M),
  List.IsChain (fun l l' => l.fst ≠ l'.fst) self.toList
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_mul : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ] {f : Π₀ (i : ι), β i}
  {h₁ h₂ : (i : ι) → β i → γ}, (f.prod fun i b => h₁ i b * h₂ i b) = f.prod h₁ * f.prod h₂
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
AEMeasurable.sinc : ∀ {α : Type u_1} {x : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable (fun x => Real.sinc (f x)) μ