mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Concept
Concept.leftInvOn_extent_ofObjects : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop},
  Set.LeftInvOn Concept.extent (Concept.ofObjects r) {s | Order.IsExtent r s}
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- A path of length `n` in a simplicial set `X` is defined as a 1-truncated
path in the 1-truncation of `X`.  -/
SSet.Path : SSet → ℕ → Type u
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result.mk.injEq : ∀ (failure? : Option Lean.Meta.Grind.Goal) (issues : List Lean.MessageData) (config : Lean.Grind.Config)
  (counters : Lean.Meta.Grind.Counters) (simp : Lean.Meta.Simp.Stats)
  (splitDiags : Lean.PArray Lean.Meta.Grind.SplitDiagInfo) (ematchDiags : Lean.PArray Lean.Meta.Grind.EMatchDiagInfo)
  (failure?_1 : Option Lean.Meta.Grind.Goal) (issues_1 : List Lean.MessageData) (config_1 : Lean.Grind.Config)
  (counters_1 : Lean.Meta.Grind.Counters) (simp_1 : Lean.Meta.Simp.Stats)
  (splitDiags_1 : Lean.PArray Lean.Meta.Grind.SplitDiagInfo)
  (ematchDiags_1 : Lean.PArray Lean.Meta.Grind.EMatchDiagInfo),
  ({ failure? := failure?, issues := issues, config := config, counters := counters, simp := simp,
        splitDiags := splitDiags, ematchDiags := ematchDiags } =
      { failure? := failure?_1, issues := issues_1, config := config_1, counters := counters_1, simp := simp_1,
        splitDiags := splitDiags_1, ematchDiags := ematchDiags_1 }) =
    (failure? = failure?_1 ∧
      issues = issues_1 ∧
        config = config_1 ∧
          counters = counters_1 ∧ simp = simp_1 ∧ splitDiags = splitDiags_1 ∧ ematchDiags = ematchDiags_1)
-- Init.Data.Nat.Lemmas
Nat.mul_add_mod' : ∀ (a b c : ℕ), (a * b + c) % b = c % b
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- If `F` and `G` are left adjoints then `F ⋙ G` is a left adjoint too.  -/
CategoryTheory.Functor.isLeftAdjoint_comp : ∀ {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] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.IsLeftAdjoint] [G.IsLeftAdjoint], (F.comp G).IsLeftAdjoint
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.toSubmersivePresentation.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePresentation R S),
  P.toSubmersivePresentation =
    { toPresentation := P.toPresentation, map := id,
      map_inj := StandardEtalePresentation.toSubmersivePresentation._proof_3, jacobian_isUnit := ⋯ }
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
_private.Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis.0.AlgebraicIndependent.indepMatroid : (R : Type u_1) →
  (A : Type w) →
    [inst : CommRing R] →
      [inst_1 : CommRing A] → [inst_2 : Algebra R A] → [FaithfulSMul R A] → [NoZeroDivisors A] → IndepMatroid A
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_biUnion_finset_le : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Finset β) (f : β → Set α),
  μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.smul_coe_torsionBy : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R)
  (x : ↥(Submodule.torsionBy R M a)), a • ↑x = 0
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.cuspFunction_add : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2}
  [inst_1 : FunLike G UpperHalfPlane ℂ],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b],
        UpperHalfPlane.cuspFunction h (⇑f + ⇑g) = UpperHalfPlane.cuspFunction h ⇑f + UpperHalfPlane.cuspFunction h ⇑g
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Subtracting the second vector passed to `oangle` from the first vector does not change the
sign of the angle.  -/
Orientation.oangle_sign_sub_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), (o.oangle (x - y) y).sign = (o.oangle x y).sign
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_injective_of_isUnit : ∀ {m : Type u_2} {R : Type u_7} [inst : Semiring R] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {A : Matrix m m R},
  IsUnit A → Function.Injective fun v => Matrix.vecMul v A
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraEquivOfIsoMonads_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂),
  (CategoryTheory.Monad.algebraEquivOfIsoMonads h).counitIso =
    (CategoryTheory.Monad.algebraFunctorOfMonadHomComp h.inv h.hom).symm ≪≫
      CategoryTheory.Monad.algebraFunctorOfMonadHomEq ⋯ ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomId
-- Lean.Parser.Command
Lean.Parser.Command.coinductive : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoAdd'.congr_simp : ∀ {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] {F : CategoryTheory.Functor C D} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] {a b c : A} (h : a + b = c)
  (e₁ e₁_1 : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)),
  e₁ = e₁_1 →
    ∀ (e₂ e₂_1 : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)),
      e₂ = e₂_1 →
        CategoryTheory.Functor.CommShift.isoAdd' h e₁ e₂ = CategoryTheory.Functor.CommShift.isoAdd' h e₁_1 e₂_1
-- Init.Data.Int.Lemmas
Int.natCast_mul : ∀ (n m : ℕ), ↑(n * m) = ↑n * ↑m
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.Ordnode.ofAscListAux₁.match_5.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (x : α) → (xs : List α) → motive (x :: xs)),
  (match [] with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_1 ()
-- Mathlib.Topology.Compactness.Lindelof
Set.Countable.isLindelof_biUnion : ∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {s : Set ι} {f : ι → Set X},
  s.Countable → (∀ i ∈ s, IsLindelof (f i)) → IsLindelof (⋃ i ∈ s, f i)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- `RestrictedProduct.evalRingHom j` is the ring homomorphism from the restricted
product `Πʳ i, [R i, B i]_[𝓕]` to the component `R j`.
 -/
RestrictedProduct.evalRingHom : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            (j : ι) →
              [inst_1 : (i : ι) → Ring (R i)] →
                [inst_2 : ∀ (i : ι), SubringClass (S i) (R i)] →
                  RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕 →+* R j
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable Int64
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
Submodule.FG.rTensor.directLimit_apply : ∀ (R : Type u) (M : Type u_1) (N : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq { P // P.FG }] {P : { P // P.FG }}
  (u : TensorProduct R (↥↑P) N),
  (Submodule.FG.rTensor.directLimit R M N)
      ((Module.DirectLimit.of R { P // P.FG } (fun P => TensorProduct R (↥↑P) N)
          (fun ⦃x x_1⦄ h => LinearMap.rTensor N (Submodule.inclusion h)) P)
        u) =
    (LinearMap.rTensor N (↑P).subtype) u
-- Mathlib.Analysis.Calculus.ContDiff.Convolution
/-- The convolution `f * g` is `C^n` when `f` is locally integrable and `g` is `C^n` and compactly
supported. Version where `g` depends on an additional parameter in an open subset `s` of a
parameter space `P` (and the compact support `k` is independent of the parameter in `s`).
In this version, all the types belong to the same universe (to get an induction working in the
proof). Use instead `contDiffOn_convolution_right_with_param`, which removes this restriction.  -/
MeasureTheory.contDiffOn_convolution_right_with_param_aux : ∀ {𝕜 : Type u𝕜} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : RCLike 𝕜] [inst_2 : NormedSpace 𝕜 E]
  {G E' F P : Type uP} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 E']
  [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F] [inst_8 : MeasurableSpace G] {μ : MeasureTheory.Measure G}
  [inst_9 : NormedAddCommGroup G] [BorelSpace G] [inst_11 : NormedSpace 𝕜 G] [inst_12 : NormedAddCommGroup P]
  [inst_13 : NormedSpace 𝕜 P] {f : G → E} {n : ℕ∞} (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'} {s : Set P} {k : Set G},
  IsOpen s →
    IsCompact k →
      (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
        MeasureTheory.LocallyIntegrable f μ →
          ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ) →
            ContDiffOn 𝕜 (↑n) (fun q => MeasureTheory.convolution f (g q.1) L μ q.2) (s ×ˢ Set.univ)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.div_wf_lemma : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R},
  q.degree ≤ p.degree ∧ p ≠ 0 →
    q.Monic → (p - q * (Polynomial.C p.leadingCoeff * Polynomial.X ^ (p.natDegree - q.natDegree))).degree < p.degree
-- Mathlib.CategoryTheory.Action
/-- Any morphism in the action groupoid is given by some pair.  -/
CategoryTheory.ActionCategory.cases : {X : Type u} →
  {G : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G X] →
        {P : ⦃a b : CategoryTheory.ActionCategory G X⦄ → (a ⟶ b) → Sort u_3} →
          ((t : X) → (g : G) → P (CategoryTheory.ActionCategory.homOfPair t g)) →
            ⦃a b : CategoryTheory.ActionCategory G X⦄ → (f : a ⟶ b) → P f
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inr_XIsoBiprod_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel j i) {Z : C} (h : HomologicalComplex.homotopyCofiber.X φ j ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.XIsoBiprod φ j i hij).inv h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ j) h
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.instFaithfulProdUncurry : ∀ {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], CategoryTheory.Functor.uncurry.Faithful
-- Mathlib.Algebra.Group.Pi.Lemmas
AddMonoidHom.piMap.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [inst : (i : ι) → AddZeroClass (M i)]
  [inst_1 : (i : ι) → AddZeroClass (N i)] (g : (i : ι) → M i →+ N i),
  AddMonoidHom.piMap g = AddMonoidHom.pi fun i => (g i).comp (Pi.evalAddMonoidHom M i)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.eventually_fintsupport_subset : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M),
  ∀ᶠ (y : M) in nhds x₀, ρ.fintsupport y ⊆ ρ.fintsupport x₀
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Preserving colimits at any universe implies preserving colimits at universe `0`.  -/
CategoryTheory.Limits.preservesSmallestColimits_of_preservesColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.colimitAuxiliaryCocone_ι_app : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (X : J),
  (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂).ι.app X =
    CategoryTheory.CategoryStruct.comp (F.obj X).hom (R.map (c₂.ι.app X))
-- Mathlib.CategoryTheory.Limits.Types.Images
/-- the universal property for the image factorisation  -/
CategoryTheory.Limits.Types.Image.lift : {α β : Type u} →
  {f : α ⟶ β} → (F' : CategoryTheory.Limits.MonoFactorisation f) → CategoryTheory.Limits.Types.Image f ⟶ F'.I
-- Lean.Elab.Binders
/-- Configuration for `let` elaboration.
 -/
Lean.Elab.Term.LetConfig : Type
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The morphism `(sequence f n₀ (q + 1)).obj ⟶ (sequence f n₀ q).obj` given by `fromNext`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.toSequenceNext : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (f : K ⟶ L) →
          [inst_2 : CategoryTheory.EnoughInjectives C] →
            [inst_3 : CategoryTheory.Mono f] →
              (n₀ : ℤ) →
                [inst_4 : K.IsStrictlyGE (n₀ + 1)] →
                  [inst_5 : L.IsStrictlyGE (n₀ + 1)] →
                    (q : ℕ) →
                      (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.sequence✝ f n₀
                            (q + 1)).obj ⟶
                        (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.sequence✝ f n₀
                            q).obj
-- Mathlib.Data.Set.Image
Set.range_eq_singleton : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} [Nonempty ι] {y : α}, (∀ (x : ι), f x = y) → Set.range f = {y}
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
CategoryTheory.IsGrothendieckAbelian.hasFilteredColimitsOfSize : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Abelian C}
  [self : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C],
  CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C
-- Mathlib.Topology.SeparatedMap
Function.Injective.isSeparatedMap : ∀ {X : Type u_1} {Y : Sort u_2} [inst : TopologicalSpace X] {f : X → Y}, Function.Injective f → IsSeparatedMap f
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Real.Angle.toCircle_neg : ∀ (θ : Real.Angle), (-θ).toCircle = θ.toCircle⁻¹
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
/-- An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces.
It is the characteristic function of the closed unit ball.  -/
ExistsContDiffBumpBase.φ : {E : Type u_1} → [NormedAddCommGroup E] → E → ℝ
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Biprod.ofComponents.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂)
  (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂),
  CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst
            (CategoryTheory.CategoryStruct.comp f₁₁ CategoryTheory.Limits.biprod.inl) +
          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst
            (CategoryTheory.CategoryStruct.comp f₁₂ CategoryTheory.Limits.biprod.inr) +
        CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd
          (CategoryTheory.CategoryStruct.comp f₂₁ CategoryTheory.Limits.biprod.inl) +
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd
        (CategoryTheory.CategoryStruct.comp f₂₂ CategoryTheory.Limits.biprod.inr)
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
/-- The product over a product set equals the product of the fiberwise products. For rewriting
in the reverse direction, use `Finset.prod_product`.  -/
Finset.prod_product' : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] (s : Finset γ) (t : Finset α) (f : γ → α → β),
  ∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ x ∈ s, ∏ y ∈ t, f x y
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.isAtom_coe : ∀ {α : Type u_2} [inst : TopologicalSpace α] [T1Space α] {s : TopologicalSpace.Closeds α}, IsAtom ↑s ↔ IsAtom s
-- Mathlib.RingTheory.Noetherian.Basic
Module.exists_finite_presentation : ∀ (R : Type u) [inst : CommRing R] [Small.{v, u} R] (M : Type v) [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.Finite R M], ∃ P x x_1, ∃ (_ : Module.Free R P) (_ : Module.Finite R P), ∃ f, Function.Surjective ⇑f
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instCommGroupWithZeroOfMonoidWithZeroHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → CommGroupWithZero (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] →
                      CommGroupWithZero (DirectLimit G f)
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.instAddCommGroup : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          (a : A) →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module A M] →
                  [inst_5 : Module R M] → [inst_6 : IsScalarTower R A M] → AddCommGroup (Module.AEval R M a)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_unitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  (c : ComplexShape ι),
  (CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C c).unitIso =
    CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isEmpty_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp},
  (Std.DTreeMap.Const.toArray t).isEmpty = t.isEmpty
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.smul_mem_pointwise_smul : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] (m : M) (r : R)
  (S : Subring R), r ∈ S → m • r ∈ m • S
-- Mathlib.Algebra.Group.Basic
div_eq_one : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a / b = 1 ↔ a = b
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.FG.of_finite : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {s : L.Substructure M} [h : Finite ↥s], s.FG
-- Mathlib.Analysis.Complex.Trigonometric
/-- The real cosine function, defined as the real part of the complex cosine  -/
Real.cos : ℝ → ℝ
-- Mathlib.Data.List.AList
AList.mem_erase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {s : AList β}, a' ∈ AList.erase a s ↔ a' ≠ a ∧ a' ∈ s
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.instInhabitedAltExpr : {a : Type} → [Inhabited a] → Inhabited (Lean.Elab.Term.Do.AltExpr a)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.freeHomEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {I : Type u} (f : SheafOfModules.free I ⟶ M)
  (i : I), M.freeHomEquiv f i = SheafOfModules.sectionsMap f (SheafOfModules.freeSection i)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isSymm_iff_basis : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} {ι : Type u_8} (b : Module.Basis ι R M),
  B.IsSymm ↔ ∀ (i j : ι), (B (b i)) (b j) = (B (b j)) (b i)
-- Mathlib.CategoryTheory.PEmpty
/-- The canonical functor out of the empty category.  -/
CategoryTheory.Functor.empty : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α], Set.Iio ⊥ = ∅
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.coe_toSubmodule : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] (s : ClosedSubmodule R M), ↑↑s = ↑s
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.add_toFun : ∀ (E : Type u_6) [inst : AddCommMonoid E] [inst_1 : TopologicalSpace E] [inst_2 : ContinuousAdd E] (a : E × E),
  (ContinuousAddMonoidHom.add E) a = a.1 + a.2
-- Mathlib.RingTheory.Ideal.Prod
Ideal.prod_mono_right : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R} {J₁ J₂ : Ideal S},
  J₁ ≤ J₂ → I.prod J₁ ≤ I.prod J₂
-- Mathlib.LinearAlgebra.Complex.Module
/-- `ℝ`-algebra isomorphism version of the complex conjugation function from `ℂ` to `ℂ`  -/
Complex.conjAe : Gal(ℂ/ℝ)
-- Mathlib.RingTheory.WittVector.WittPolynomial
xInTermsOfW.eq_1 : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible ↑p] (x : ℕ),
  xInTermsOfW p R x =
    (MvPolynomial.X x - ∑ i, MvPolynomial.C (↑p ^ ↑i) * xInTermsOfW p R ↑i ^ p ^ (x - ↑i)) * MvPolynomial.C (⅟↑p ^ x)
-- Mathlib.Data.List.Cycle
List.pmap_next_eq_rotate_one : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → List.pmap l.next l ⋯ = l.rotate 1
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.forIn_toArray : ∀ {m : Type w → Type u_1} {γ α β : Type w} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.IterM Id β}
  {f : β → γ → m (ForInStep γ)} {init : γ}, forIn it.toArray.run init f = forIn it init f
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.lift_lt_univ' : ∀ (c : Cardinal.{u}), Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
/-- See `MemLp.prod'` for the applied version.  -/
MeasureTheory.MemLp.prod : ∀ {ι : Type u_1} {α : Type u_2} {𝕜 : Type u_3} {x : MeasurableSpace α} [inst : NormedCommRing 𝕜]
  {μ : MeasureTheory.Measure α} {f : ι → α → 𝕜} {p : ι → ENNReal} {s : Finset ι},
  (∀ i ∈ s, MeasureTheory.MemLp (f i) (p i) μ) → MeasureTheory.MemLp (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.sum_right : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_2} [Countable ι]
  {ν : ι → MeasureTheory.Measure α},
  μ.MutuallySingular (MeasureTheory.Measure.sum ν) ↔ ∀ (i : ι), μ.MutuallySingular (ν i)
-- Mathlib.CategoryTheory.Sums.Basic
/-- The sum of two natural transformations.  -/
CategoryTheory.NatTrans.sum : {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] →
            {D : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                {F G : CategoryTheory.Functor A B} →
                  {H I : CategoryTheory.Functor C D} → (F ⟶ G) → (H ⟶ I) → (F.sum H ⟶ G.sum I)