mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_mul_const : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} (x : 𝕜) (a : 𝕜'), a ≠ 0 → logDeriv (fun z => f z * a) x = logDeriv f x
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.uniqueLinearEquiv_apply : ∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : One M] [inst_4 : Subsingleton M] (x : MonoidAlgebra S M),
  (MonoidAlgebra.uniqueLinearEquiv R M) x = x.coeff 1
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- If `A`, `B`, `C`, `D` are cospherical and `P` is on both lines `AB` and `CD`, then
`AP * BP = CP * DP`.  -/
EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c d p : P},
  EuclideanGeometry.Cospherical {a, b, c, d} →
    p ∈ line[ℝ, a, b] → p ∈ line[ℝ, c, d] → dist a p * dist b p = dist c p * dist d p
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instZeroGroupSeminorm.eq_1 : ∀ {E : Type u_3} [inst : Group E],
  GroupSeminorm.instZeroGroupSeminorm = { zero := { toFun := 0, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.instNeBotSymmetricIco : ∀ (G : Type u_1) [inst : Neg G] [inst_1 : Preorder G] [inst_2 : LocallyFiniteOrder G] [Filter.atTop.NeBot],
  (SummationFilter.symmetricIco G).NeBot
-- Init.Data.List.Erase
List.eraseP_append : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α},
  List.eraseP p (l₁ ++ l₂) = if l₁.any p = true then List.eraseP p l₁ ++ l₂ else l₁ ++ List.eraseP p l₂
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- The `MonoidHom` that takes an automorphism to the power of `μ` that `μ` gets mapped to
under it.  -/
IsPrimitiveRoot.autToPow : (R : Type u_4) →
  {S : Type u_5} →
    [inst : CommRing S] →
      [IsDomain S] →
        {μ : S} →
          {n : ℕ} →
            IsPrimitiveRoot μ n → [inst_2 : CommRing R] → [inst_3 : Algebra R S] → [NeZero n] → (S ≃ₐ[R] S) →* (ZMod n)ˣ
-- Mathlib.Order.Hom.Bounded
/-- Reinterpret a `BoundedOrderHom` as a `BotHom`.  -/
BoundedOrderHom.toBotHom : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : BoundedOrder α] → [inst_3 : BoundedOrder β] → BoundedOrderHom α β → BotHom α β
-- Lean.Data.Lsp.Basic
Lean.Lsp.LocationLink.originSelectionRange? : Lean.Lsp.LocationLink → Option Lean.Lsp.Range
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  k ∈ Std.HashMap.unitOfList l ↔ l.contains k = true
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T.eq_def : ∀ (R : Type u_1) [inst : CommRing R] (x : ℤ),
  Polynomial.Chebyshev.T R x =
    match x with
    | 0 => 1
    | 1 => Polynomial.X
    | Int.ofNat n.succ.succ => 2 * Polynomial.X * Polynomial.Chebyshev.T R (↑n + 1) - Polynomial.Chebyshev.T R ↑n
    | Int.negSucc n => 2 * Polynomial.X * Polynomial.Chebyshev.T R (-↑n) - Polynomial.Chebyshev.T R (-↑n + 1)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.instFunLike : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} → {N : Type u_2} → [inst_1 : CommMonoid N] → FunLike (S.LocalizationMap N) M N
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.MemLp.integrable_norm_pow : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β} {p : ℕ}, MeasureTheory.MemLp f (↑p) μ → p ≠ 0 → MeasureTheory.Integrable (fun x => ‖f x‖ ^ p) μ
-- Mathlib.Algebra.Notation.Prod
Prod.neg_mk : ∀ {G : Type u_8} {H : Type u_9} [inst : Neg G] [inst_1 : Neg H] (a : G) (b : H), -(a, b) = (-a, -b)
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `dist_nonneg`.  -/
hammingDist_nonneg : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
  0 ≤ hammingDist x y
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_lt_cos_of_nonneg_of_le_pi : ∀ {x y : ℝ}, 0 ≤ x → y ≤ Real.pi → x < y → Real.cos y < Real.cos x
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.ofSuppBddBelow_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] [inst_2 : LocallyFiniteOrder Γ]
  [inst_3 : Nonempty Γ], HahnSeries.ofSuppBddBelow 0 ⋯ = 0
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- An extensionality lemma for being the zero arrow.  -/
CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  (∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0) → f = 0
-- Mathlib.Algebra.Module.Presentation.DirectSum
/-- The obvious presentation of the module `⨁ i, M i` that is obtained from
the data of presentations of the module `M i` for each `i`.  -/
Module.Presentation.directSum : {A : Type u} →
  [inst : Ring A] →
    {ι : Type w} →
      [DecidableEq ι] →
        {M : ι → Type v} →
          [inst_2 : (i : ι) → AddCommGroup (M i)] →
            [inst_3 : (i : ι) → Module A (M i)] →
              ((i : ι) → Module.Presentation A (M i)) → Module.Presentation A (DirectSum ι fun i => M i)
-- Mathlib.Algebra.Order.Group.PosPart
posPart_eq_ite_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddGroup α] {a : α}, a⁺ = if 0 < a then a else 0
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.norm_toSpanSingleton : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] (x : E), ‖ContinuousLinearMap.toSpanSingleton 𝕜 x‖ = ‖x‖
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.toFun.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (S : Type v) [inst_5 : CommSemiring S] [inst_6 : Algebra R S]
  (f : M →ₚₗ[R] N),
  PolynomialLaw.toFun S f = Function.extend (PolynomialLaw.π R M S) (PolynomialLaw.toFunLifted S f) fun x => 0
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.commShiftIso_unopUnop_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖᵒᵖ)
  (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.commShiftIso_unopUnop_inv_app._auto_1),
  (CategoryTheory.Functor.commShiftIso (CategoryTheory.unopUnop C) n).inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).hom.app (Opposite.unop X)).unop
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app X).unop.unop
-- Mathlib.Data.Sign.Defs
SignType.neg_eq_neg_one : SignType.neg = -1
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
CategoryTheory.coherentTopology.epi_π_app_zero_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preregular C]
  [inst_2 : CategoryTheory.FinitaryExtensive C] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape ℕᵒᵖ C],
  (∀ (G : CategoryTheory.Functor ℕᵒᵖ C),
      (∀ (n : ℕ), CategoryTheory.EffectiveEpi (G.map (CategoryTheory.homOfLE ⋯).op)) →
        CategoryTheory.EffectiveEpi (CategoryTheory.Limits.limit.π G (Opposite.op 0))) →
    ∀ [CategoryTheory.HasSheafify (CategoryTheory.coherentTopology C) (Type v)]
      [CategoryTheory.Balanced (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))]
      [(CategoryTheory.coherentTopology C).WEqualsLocallyBijective (Type v)]
      {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))}
      {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c),
      (∀ (n : ℕ), CategoryTheory.Epi (F.map (CategoryTheory.homOfLE ⋯).op)) →
        CategoryTheory.Epi (c.π.app (Opposite.op 0))
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- The diagonal path, but starting from `f x₀` and going to `g x₁`  -/
ContinuousMap.Homotopy.diagonalPath' : {X Y : TopCat} →
  {f g : C(↑X, ↑Y)} →
    f.Homotopy g →
      {x₀ x₁ : ↑X} →
        (FundamentalGroupoid.fromTop x₀ ⟶ FundamentalGroupoid.fromTop x₁) →
          (FundamentalGroupoid.fromTop (f x₀) ⟶ FundamentalGroupoid.fromTop (g x₁))
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instVAdd : {α : Type u_1} → [inst : AddCommGroup α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → VAdd α (UpperSet α)
-- Init.SimpLemmas
true_implies : ∀ (p : Prop), (True → p) = p
-- Mathlib.Order.Category.PartOrd
/-- `Antisymmetrization` as a functor. It is the free functor.  -/
preordToPartOrd : CategoryTheory.Functor Preord PartOrd
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.apply_eigenvectorBasis : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
  (i : Fin n), T ((hT.eigenvectorBasis hn) i) = ↑(hT.eigenvalues hn i) • (hT.eigenvectorBasis hn) i
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.AlgHom.inhabited : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] → [inst_2 : Algebra K L] → (S : IntermediateField K L) → Inhabited (↥S →ₐ[K] L)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The **first isomorphism theorem** for commutative rings (`RingHom.range` version).  -/
RingHom.quotientKerEquivRange : {R : Type u} → [inst : Ring R] → {S : Type v} → [inst_1 : Ring S] → (f : R →+* S) → R ⧸ RingHom.ker f ≃+* ↥f.range
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabRio : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.natCast_nat : ∀ {R : Type u_1} [inst : CommSemiring R] (n : ℕ), ↑n.rawCast = n.rawCast
-- Mathlib.Analysis.Matrix.PosDef
Matrix.PosSemidef.det_nonneg : ∀ {n : Type u_2} {𝕜 : Type u_3} [inst : Fintype n] [inst_1 : RCLike 𝕜] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n],
  A.PosSemidef → 0 ≤ A.det
-- Lean.Linter.UnusedVariables
/-- The user-provided name of the `FVarId`  -/
Lean.Linter.UnusedVariables.FVarDefinition.userName : Lean.Linter.UnusedVariables.FVarDefinition → Lean.Name
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_eq_some_getKey!_of_contains : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, m.contains a = true → m.getKey? a = some (m.getKey! a)
-- Init.Data.String.Basic
/-- Returns the next position in a string after position `p`. The result is unspecified if `p` is not a
valid position.

Requires evidence, `h`, that `p` is within bounds. No run-time bounds check is performed, as in
`String.next`.

A typical pattern combines `String.next'` with a dependent `if`-expression to avoid the overhead of
an additional bounds check. For example:
```
def next? (s : String) (p : String.Pos) : Option Char :=
  if h : s.atEnd p then none else s.get (s.next' p h)
```

This is a legacy function. The recommended alternative is `String.Pos.next`, combined with
`String.pos` or another means of obtaining a `String.Pos`.

Example:
* `let abc := "abc"; abc.get (abc.next' 0 (by decide)) = 'b'`
 -/
String.Pos.Raw.next' : (s : String) → (p : String.Pos.Raw) → ¬String.Pos.Raw.atEnd s p = true → String.Pos.Raw
-- Mathlib.Analysis.Fourier.RiemannLebesgueLemma
/-- Rewrite the Fourier integral in a form that allows us to use uniform continuity.  -/
fourierIntegral_eq_half_sub_half_period_translate : ∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : V → E}
  [inst_2 : NormedAddCommGroup V] [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] [inst_5 : InnerProductSpace ℝ V]
  [inst_6 : FiniteDimensional ℝ V] {w : V},
  w ≠ 0 →
    MeasureTheory.Integrable f MeasureTheory.volume →
      ∫ (v : V), Real.fourierChar (-inner ℝ v w) • f v =
        (1 / 2) • ∫ (v : V), Real.fourierChar (-inner ℝ v w) • (f v - f (v + (fun w => (1 / (2 * ‖w‖ ^ 2)) • w) w))
-- Lean.AuxRecursor
Lean.belowSuffix : String
-- Mathlib.Data.Set.Operations
Set.mem_offDiag : ∀ {α : Type u} {x : α × α} {s : Set α}, x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.simp : Lean.Expr →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.SimprocsArray #[] →
      optParam (Option Lean.Meta.Simp.Discharge) none →
        optParam Lean.Meta.Simp.Stats { } → Lean.MetaM (Lean.Meta.Simp.Result × Lean.Meta.Simp.Stats)
-- Mathlib.CategoryTheory.ComposableArrows.Two
CategoryTheory.ComposableArrows.twoδ₂Toδ₁_app_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg),
  (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h).app 0 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₁ f).obj 0)
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- `AddMonoid.End M` is equivalent to `Monoid.End (Multiplicative M)`.  -/
MulEquiv.AddMonoid.End : {M : Type u_4} → [inst : AddMonoid M] → AddMonoid.End M ≃* Monoid.End (Multiplicative M)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.isUnit_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Group α] (a : α), IsUnit {a}
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciSup_neg : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {p : Prop} {f : p → α}, ¬p → ⨆ (h : p), f h = sSup ∅
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.Indep.diff_indep_contract_of_subset : ∀ {α : Type u_1} {M : Matroid α} {I J : Set α}, M.Indep J → I ⊆ J → (M.contract I).Indep (J \ I)
-- Mathlib.Data.Finset.Union
Finset.biUnion_singleton : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} [inst : DecidableEq β] {f : α → β},
  (s.biUnion fun a => {f a}) = Finset.image f s
-- Mathlib.Algebra.Category.Grp.Kernels
/-- The kernel cone induced by the concrete kernel.  -/
AddCommGrpCat.kernelCone : {G H : AddCommGrpCat} → (f : G ⟶ H) → CategoryTheory.Limits.KernelFork f
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.BodyState.closeDelimited.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Reader.BodyState.closeDelimited = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.BicartesianSq.toIsPushout : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z}, CategoryTheory.BicartesianSq f g h i → CategoryTheory.IsPushout f g h i
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_left_inj : ∀ {α : Type u} [inst : Add α] {x y z : WithTop α} [IsLeftCancelAdd α], x ≠ ⊤ → (x + y = x + z ↔ y = z)
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.changeOriginIndexEquiv_apply_fst : ∀ (s : (k : ℕ) × (l : ℕ) × { s // s.card = l }),
  (FormalMultilinearSeries.changeOriginIndexEquiv s).fst = s.fst + s.snd.fst
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongrLeft_symm : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂),
  (Equiv.prodCongrLeft e).symm = Equiv.prodCongrLeft (Equiv.symm ∘ e)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral_eq_of_subset' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal)
  {s : Finset ENNReal}, f.range \ {0} ⊆ s → f.lintegral μ = ∑ x ∈ s, x * μ (⇑f ⁻¹' {x})
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.continuous_transAssocReparamAux : Continuous Path.Homotopy.transAssocReparamAux
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.isInducing : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → Topology.IsInducing f
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instDistribMulAction : {R : Type u_1} →
  {S : Type u_2} →
    {a b : R} →
      [inst : Monoid S] → [inst_1 : AddMonoid R] → [DistribMulAction S R] → DistribMulAction S (QuadraticAlgebra R a b)
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
HomologicalComplex.extendXIso.hcongr_13 : ∀ (ι ι' : Type u_1),
  ι = ι' →
    ∀ (ι'_1 ι'' : Type u_2),
      ι'_1 = ι'' →
        ∀ (c : ComplexShape ι) (c' : ComplexShape ι'),
          c ≍ c' →
            ∀ (c'_1 : ComplexShape ι'_1) (c'' : ComplexShape ι''),
              c'_1 ≍ c'' →
                ∀ (C C' : Type u_3),
                  C = C' →
                    ∀ (inst : CategoryTheory.Category.{v_1, u_3} C) (inst' : CategoryTheory.Category.{v_1, u_3} C'),
                      inst ≍ inst' →
                        ∀ (inst_1 : CategoryTheory.Limits.HasZeroObject C)
                          (inst'_1 : CategoryTheory.Limits.HasZeroObject C'),
                          inst_1 ≍ inst'_1 →
                            ∀ (inst_2 : CategoryTheory.Limits.HasZeroMorphisms C)
                              (inst'_2 : CategoryTheory.Limits.HasZeroMorphisms C'),
                              inst_2 ≍ inst'_2 →
                                ∀ (K : HomologicalComplex C c) (K' : HomologicalComplex C' c'),
                                  K ≍ K' →
                                    ∀ (e : c.Embedding c'_1) (e' : c'.Embedding c''),
                                      e ≍ e' →
                                        ∀ (i' : ι'_1) (i'' : ι''),
                                          i' ≍ i'' →
                                            ∀ (i : ι) (i'_1 : ι'),
                                              i ≍ i'_1 →
                                                ∀ (h : e.f i = i') (h' : e'.f i'_1 = i''),
                                                  h ≍ h' → K.extendXIso e h ≍ K'.extendXIso e' h'
-- Init.Data.List.Monadic
List.foldlM_unattach : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {P : α → Prop} {xs : List (Subtype P)}
  {f : β → α → m β} {init : β},
  List.foldlM f init xs.unattach =
    List.foldlM
      (fun b x =>
        match x with
        | ⟨x, h⟩ => binderNameHint b f (binderNameHint x (f b) (binderNameHint h () (f b (wfParam x)))))
      init xs
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isGE_of_ge : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (p q : ℤ), p ≤ q → ∀ [K.IsGE q], K.IsGE p
-- Mathlib.CategoryTheory.Generator.StrongGenerator
CategoryTheory.ObjectProperty.IsStrongGenerator.isIso_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  P.IsStrongGenerator →
    ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [CategoryTheory.Mono i],
      (∀ (G : C), P G → Function.Surjective fun f => CategoryTheory.CategoryStruct.comp f i) → CategoryTheory.IsIso i
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.CastMode.all.sizeOf_spec : sizeOf Mathlib.Tactic.DepRewrite.CastMode.all = 1
-- Init.Data.String.Bootstrap
String.Internal.contains : String → Char → Bool
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.dist_integralSum_integral_le_of_memBaseSet : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι}
  {π : BoxIntegral.TaggedPrepartition I} [inst_4 : Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E}
  {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {c : NNReal} {ε : ℝ} (h : BoxIntegral.Integrable I l f vol),
  0 < ε →
    l.MemBaseSet I c (h.convergenceR ε c) π →
      π.IsPartition → dist (BoxIntegral.integralSum f vol π) (BoxIntegral.integral I l f vol) ≤ ε
-- Mathlib.Tactic.FunProp.Theorems
/-- Structure holding information about lambda theorem.  -/
Mathlib.Meta.FunProp.LambdaTheorem : Type
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_replaceEntry_of_beq_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {a : α} {b : β a} {l : List ((a : α) × β a)}
  (p : (a : α) × β a), (p.fst == a) = false → (p ∈ Std.Internal.List.replaceEntry a b l ↔ p ∈ l)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
/-- The conjugate transpose of a matrix defined in term of `star`.  -/
Matrix.conjTranspose : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [Star α] → Matrix m n α → Matrix n m α
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.kernelBiproductπIso_hom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J)
  [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)],
  (CategoryTheory.Limits.kernelBiproductπIso f i).hom =
    (CategoryTheory.Limits.biproduct.isLimitFromSubtype f i).lift
      (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.π f i) 0))
-- Aesop.Rule.Name
Aesop.instInhabitedPhaseName : Inhabited Aesop.PhaseName
-- Mathlib.Algebra.Field.Defs
/-- `a ^ (n + 1) = a ^ n * a`  -/
DivisionRing.zpow_succ' : ∀ {K : Type u_2} [self : DivisionRing K] (n : ℕ) (a : K), a ^ ↑n.succ = a ^ ↑n * a
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.union_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Finset α), s ∪ insert a t = insert a (s ∪ t)
-- Init.Data.List.Control
List.forM_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] {f : α → m PUnit.{u_1 + 1}} {a : α} {as : List α},
  forM (a :: as) f = do
    f a
    forM as f
-- Mathlib.CategoryTheory.Monoidal.Discrete
/-- A multiplicative morphism between monoids gives a monoidal functor between the corresponding
discrete monoidal categories.
 -/
CategoryTheory.Discrete.monoidalFunctor : {M : Type u} →
  [inst : Monoid M] →
    {N : Type u'} →
      [inst_1 : Monoid N] → (M →* N) → CategoryTheory.Functor (CategoryTheory.Discrete M) (CategoryTheory.Discrete N)
-- Mathlib.Data.Nat.Digits.Lemmas
List.mem_fixedLengthDigits_iff : ∀ {b : ℕ} (hb : 1 < b) {l : ℕ} {L : List ℕ}, L ∈ List.fixedLengthDigits hb l ↔ L.length = l ∧ ∀ x ∈ L, x < b
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- **Alias** of `NonUnitalAlgebra.toNonUnitalSubring_top`. -/
NonUnitalAlgebra.top_toSubring : ∀ {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A], ⊤.toNonUnitalSubring = ⊤
-- Init.Data.String.Lemmas.Splits
String.copy_sliceFrom_cast : ∀ {s t : String} (hst : s = t) {pos : s.Pos}, (t.sliceFrom (pos.cast hst)).copy = (s.sliceFrom pos).copy
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.comap_M : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_4} {H : Type u_5} {M : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M]
  [inst_7 : IsManifold I k M] [inst_8 : CompactSpace M] [inst_9 : BoundarylessManifold I M] (s : SingularManifold X k I)
  {φ : M → s.M} (hφ : Continuous φ), (s.comap hφ).M = M
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- A linear map preserves scalar multiplication.  -/
IsLinearMap.map_smul : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] {f : M → M₂}, IsLinearMap R f → ∀ (c : R) (x : M), f (c • x) = c • f x
-- Mathlib.Tactic.Linter.TextBased
/-- Create the underlying error message for a given `StyleError`.

Note: changes to the texts here must be accounted for in `parse?_errorContext`!
 -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.errorMessage : Mathlib.Linter.TextBased.StyleError✝ → String