mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.cosk.faithful : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (n : ℕ)
  [inst_1 :
    ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F]
  [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F],
  (CategoryTheory.SimplicialObject.Truncated.cosk n).Faithful
-- Mathlib.Algebra.Order.Floor.Div
Finsupp.ceilDiv_def : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : AddCommMonoid β] [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : CeilDiv α β] (f : ι →₀ β)
  (a : α), f ⌈/⌉ a = Finsupp.mapRange (fun x => x ⌈/⌉ a) ⋯ f
-- Mathlib.RingTheory.FinitePresentation
/-- An algebra over a Noetherian ring is finitely generated if and only if it is finitely
presented.  -/
Algebra.FinitePresentation.of_finiteType : ∀ {R : Type w₁} {A : Type w₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [IsNoetherianRing R],
  Algebra.FiniteType R A ↔ Algebra.FinitePresentation R A
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.strictMono_valueGroupEquiv_symm : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : Ring R] (v : Valuation R Γ₀),
  StrictMono ⇑(WithVal.valueGroupEquiv v).symm
-- Mathlib.Topology.AlexandrovDiscrete
isOpen_iInter : ∀ {ι : Sort u_1} {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {f : ι → Set α},
  (∀ (i : ι), IsOpen (f i)) → IsOpen (⋂ i, f i)
-- Mathlib.RingTheory.Finiteness.Ideal
Ideal.FG.mul : ∀ {R : Type u_1} [inst : Semiring R] {I J : Ideal R} [I.IsTwoSided], I.FG → J.FG → (I * J).FG
-- Mathlib.Topology.Bases
TopologicalSpace.instSeparableSpaceQuotient : ∀ {α : Type u} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] {s : Setoid α},
  TopologicalSpace.SeparableSpace (Quotient s)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.symm_apply : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : ∀ (x : B), Nonempty (E x)] (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) {b : B}
  (hb : b ∈ e.baseSet) (y : F), e.symm b y = cast ⋯ (↑e.symm (b, y)).snd
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1 : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E) (X : Type u_3)
  [inst_3 : MulAction E X], IsScalarTower (↥(Algebra.adjoin F S)) (↥(IntermediateField.adjoin F S)) X
-- Mathlib.Algebra.Homology.CochainComplexPlus
CochainComplex.Plus.instIsClosedUnderLimitsOfShapeIntPlusOfFinCategoryOfHasLimitsOfShape : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (J : Type u_2) [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
  [CategoryTheory.Limits.HasLimitsOfShape J C], (CochainComplex.plus C).IsClosedUnderLimitsOfShape J
-- Mathlib.LinearAlgebra.Projection
/-- An idempotent operator `f` commutes with a linear operator `T` if and only if
both `range f` and `ker f` are invariant under `T`.  -/
LinearMap.IsIdempotentElem.commute_iff : ∀ {E : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T f : E →ₗ[R] E},
  IsIdempotentElem f → (Commute f T ↔ f.range ∈ Module.End.invtSubmodule T ∧ f.ker ∈ Module.End.invtSubmodule T)
-- Std.Time.DateTime.PlainDateTime
/-- Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`.
 -/
Std.Time.PlainTime.atDate : Std.Time.PlainTime → Std.Time.PlainDate → Std.Time.PlainDateTime
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleResult.success : Array LeanSearchClient.SearchResult → LeanSearchClient.LoogleResult
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
/-- An auxiliary equivalence to be used in `multiequalizerEquiv` below.  -/
CategoryTheory.Limits.Concrete.multiequalizerEquivAux : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type s} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {J : CategoryTheory.Limits.MulticospanShape} →
              (I : CategoryTheory.Limits.MulticospanIndex J C) →
                ↑(I.multicospan.comp (CategoryTheory.forget C)).sections ≃
                  { x //
                    ∀ (i : J.R),
                      (CategoryTheory.ConcreteCategory.hom (I.fst i)) (x (J.fst i)) =
                        (CategoryTheory.ConcreteCategory.hom (I.snd i)) (x (J.snd i)) }
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] (S : CategoryTheory.ShortComplex C) [F.PreservesHomology],
  F.PreservesLeftHomologyOf S
-- Mathlib.RingTheory.Flat.Basic
/-- See also `Module.FaithfullyFlat.tensorProduct_mk_injective`.  -/
Module.Flat.tensorProduct_mk_injective : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_4)
  [inst_3 : Semiring S] [inst_4 : Algebra R S] [FaithfulSMul R S] [Module.Flat R M],
  Function.Injective ⇑((TensorProduct.mk R S M) 1)
-- Lean.Declaration
Lean.Constructor.type : Lean.Constructor → Lean.Expr
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_filter_eq_size_iff : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool},
  m.WF → ((Std.HashMap.Raw.filter f m).size = m.size ↔ ∀ (a : α) (h : a ∈ m), f (m.getKey a h) m[a] = true)
-- Mathlib.Analysis.InnerProductSpace.PiL2
Complex.isometryOfOrthonormal_symm_apply : ∀ {F : Type u_5} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (v : OrthonormalBasis (Fin 2) ℝ F)
  (f : F), (Complex.isometryOfOrthonormal v).symm f = ↑((v.toBasis.coord 0) f) + ↑((v.toBasis.coord 1) f) * Complex.I
-- Mathlib.Order.Hom.Basic
/-- Note that this goal could also be stated `(Disjoint on f) a b`  -/
Disjoint.map_orderIso : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : SemilatticeInf β]
  [inst_3 : OrderBot β] {a b : α} (f : α ≃o β), Disjoint a b → Disjoint (f a) (f b)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_base : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat}
  {x x_1 Z : F.CoGrothendieck} (f : x.Hom x_1) (g : x_1.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base
-- Init.Data.SInt.Lemmas
Int64.sub_sub : ∀ (a b c : Int64), a - b - c = a - (b + c)
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.List.findSome?.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Mathlib.LinearAlgebra.Span.Defs
/-- **Alias** of `Submodule.span_setOfPred_mem_eq_top`. -/
Submodule.span_setOf_mem_eq_top : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  Submodule.span R {x | ↑x ∈ s} = ⊤
-- Mathlib.Analysis.Convex.Approximation
ConvexOn.convex_re_epigraph : ∀ {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [inst : RCLike 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module ℝ E], ConvexOn ℝ s φ → Convex ℝ {p | p.1 ∈ s ∧ φ p.1 ≤ RCLike.re p.2}
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.nonempty_iInter_clPrehaar : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G),
  (MeasureTheory.Measure.haar.haarProduct ↑K₀ ∩ ⋂ V, MeasureTheory.Measure.haar.clPrehaar (↑K₀) V).Nonempty
-- Init.Data.Option.Basic
/-- Keeps an optional value only if it satisfies a Boolean predicate.

If `Option` is thought of as a collection that contains at most one element, then `Option.filter` is
analogous to `List.filter` or `Array.filter`.

Examples:
 * `(some 5).filter (· % 2 == 0) = none`
 * `(some 4).filter (· % 2 == 0) = some 4`
 * `none.filter (fun x : Nat => x % 2 == 0) = none`
 * `none.filter (fun x : Nat => true) = none`
 -/
Option.filter : {α : Type u_1} → (α → Bool) → Option α → Option α
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- A family of morphisms `T' ⟶ T j` lifts to a morphism `T' ⟶ productTriangle T`.  -/
CategoryTheory.Pretriangulated.productTriangle.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {J : Type u_1} →
        (T : J → CategoryTheory.Pretriangulated.Triangle C) →
          [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] →
            [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] →
              [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] →
                [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] →
                  {T' : CategoryTheory.Pretriangulated.Triangle C} →
                    ((j : J) → T' ⟶ T j) → (T' ⟶ CategoryTheory.Pretriangulated.productTriangle T)
-- Mathlib.Topology.Connected.PathConnected
/-- The path component of `(x, y)` in the product space is the product of the path components
of `x` and `y`.  -/
pathComponent_prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X) (y : Y),
  pathComponent (x, y) = pathComponent x ×ˢ pathComponent y
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.range_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
  p.mkQ.range = ⊤
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_div_self_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] (a : α) {b : α}, a ≤ a / b ↔ b ≤ 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.WalkingSpan.instSubsingletonHom : ∀ (X Y : CategoryTheory.Limits.WalkingSpan), Subsingleton (X ⟶ Y)
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.restrict_preimage_emb : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb →
    MeasurableEmbedding f → ∀ (s : Set β), MeasureTheory.MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s)
-- Mathlib.Topology.ContinuousOn
/-- `continuousWithinAt_insert` gives the same equivalence but at a point `y` possibly different
from `x`. As this requires the space to be T1, and this property is not available in this file,
this is found in another file although it is part of the basic API for `continuousWithinAt`.  -/
ContinuousWithinAt.sdiff_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s t : Set α}
  {x : α}, ContinuousWithinAt f t x → (ContinuousWithinAt f (s \ t) x ↔ ContinuousWithinAt f s x)
-- Std.Time.Format
Std.Time.PlainDate.instRepr : Repr Std.Time.PlainDate
-- Mathlib.Algebra.Group.Prod
Prod.instDivisionCommMonoid.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : DivisionCommMonoid G] [inst_1 : DivisionCommMonoid H],
  Prod.instDivisionCommMonoid = { toDivisionMonoid := Prod.instDivisionMonoid, mul_comm := ⋯ }
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
/-- Equivalence between `M` and `Mᵈᵐᵃ`.  -/
DomAddAct.mk : {M : Type u_1} → M ≃ Mᵈᵃᵃ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get!_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∉ t₁ → (t₁ ∪ t₂).get! k = t₂.get! k
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.toMultilinearMapLM_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {S : Type u_10} [inst_5 : Semiring S]
  [inst_6 : Module S N] [inst_7 : SMulCommClass R S N] (self : M [⋀^ι]→ₗ[R] N),
  AlternatingMap.toMultilinearMapLM self = ↑self
-- Lean.Expr
Lean.instBEqFVarId.beq : Lean.FVarId → Lean.FVarId → Bool
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : β → β}, (t.modify k f).contains k' = t.contains k'
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_top : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F), Submonoid.comap f ⊤ = ⊤
-- Mathlib.Order.Cofinal
IsCofinal.univ : ∀ {α : Type u_1} [inst : Preorder α], IsCofinal Set.univ
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.map.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι}
  (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃') (n₀ n₁ n₂ : ℤ)
  (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ =
    CategoryTheory.ShortComplex.homologyMap (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯)
-- Mathlib.Algebra.Algebra.Epi
TensorProduct.lid'.congr_simp : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : Algebra.IsEpi R A] (M : Type u_3) [inst_4 : AddCommMonoid M] [inst_5 : Module R M] [inst_6 : Module A M]
  [inst_7 : IsScalarTower R A M], TensorProduct.lid' R A M = TensorProduct.lid' R A M
-- Batteries.Tactic.Trans
/-- Compose using transitivity, homogeneous case.  -/
Trans.simple : {α : Sort u_1} → {a b c : α} → {r : α → α → Sort u_2} → [Trans r r r] → r a b → r b c → r a c
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are field extensions of `F`, such that `A ⊗[F] B` is a field, then for any
field extension of `F` that `A` and `B` embed into, their images are linearly disjoint.  -/
IntermediateField.LinearDisjoint.of_isField' : ∀ {F : Type u} [inst : Field F] {A : Type v} [inst_1 : Field A] {B : Type w} [inst_2 : Field B] [inst_3 : Algebra F A]
  [inst_4 : Algebra F B],
  IsField (TensorProduct F A B) →
    ∀ {K : Type u_1} [inst_5 : Field K] [inst_6 : Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K),
      fa.fieldRange.LinearDisjoint ↥fb.fieldRange
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.monotone_distinctConstantsTheory : ∀ {L : FirstOrder.Language} {α : Type u'}, Monotone L.distinctConstantsTheory
-- Lean.Widget.Types
/-- The hash is cached to avoid recomputing it whenever the `Module` is used.  -/
Lean.Widget.Module.javascriptHash : (self : Lean.Widget.Module) → { x // x = hash self.javascript }
-- Mathlib.Analysis.InnerProductSpace.Completion
UniformSpace.Completion.toInner : {𝕜' : Type u_4} →
  {E' : Type u_5} →
    [TopologicalSpace 𝕜'] → [inst : UniformSpace E'] → [Inner 𝕜' E'] → Inner 𝕜' (UniformSpace.Completion E')
-- Mathlib.Analysis.Convex.Between
Wbtw.trans_sbtw_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V]
  {w x y z : P}, Wbtw R w y z → Sbtw R w x y → Sbtw R w x z
-- Lean.Parser.Term
Lean.Parser.Term.matchExprAlt : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod'_δ_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C E) [inst_6 : F.OplaxMonoidal]
  [inst_7 : G.OplaxMonoidal] (X Y : C),
  (CategoryTheory.Functor.OplaxMonoidal.δ (F.prod' G) X Y).2 = CategoryTheory.Functor.OplaxMonoidal.δ G X Y
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyData.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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h.IsPreservedBy F],
  (h.map F).π = F.map h.π
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.map_mul_of_coprime : ∀ {R : Type u_1} [inst : MonoidWithZero R] {f : ArithmeticFunction R},
  f.IsMultiplicative → ∀ {m n : ℕ}, m.gcd n = 1 → f (m * n) = f m * f n
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_hasFPowerSeriesOnBall : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : CharZero 𝕂] [ContinuousSMul ℚ 𝕂]
  [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸],
  HasFPowerSeriesOnBall NormedSpace.exp (NormedSpace.expSeries 𝕂 𝔸) 0 ⊤
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_mulOpposite : ∀ {α : Type u}, Cardinal.mk αᵐᵒᵖ = Cardinal.mk α
-- Mathlib.LinearAlgebra.Ray
/-- `SameRay.neg` as an `iff`.  -/
sameRay_neg_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x y : M}, SameRay R (-x) (-y) ↔ SameRay R x y
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.prod_left_snd : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'}
  {l : Filter α}, (fun x => (f' x, g' x)) =O[l] k' → g' =O[l] k'
-- Mathlib.Analysis.Normed.Operator.Completeness
/-- If a Cauchy sequence of continuous linear map converges to a continuous linear map pointwise,
then it converges to the same map in norm. This lemma is used to prove that the space of continuous
linear maps is complete provided that the codomain is a complete space.  -/
ContinuousLinearMap.tendsto_of_tendsto_pointwise_of_cauchySeq : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6}
  [inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] {f : ℕ → E' →SL[σ₁₂] F}
  {g : E' →SL[σ₁₂] F},
  Filter.Tendsto (fun n x => (f n) x) Filter.atTop (nhds ⇑g) → CauchySeq f → Filter.Tendsto f Filter.atTop (nhds g)
-- Aesop.RuleSet.Member
Aesop.GlobalRuleSetMember.normSimpRule : Aesop.NormSimpRule → Aesop.GlobalRuleSetMember
-- Init.Coe
CoeDep.mk : {α : Sort u} → {x : α} → {β : Sort v} → β → CoeDep α x β
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.mem_doubleCoset_self : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G) (a : G), a ∈ DoubleCoset.doubleCoset a ↑H ↑K
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.IsAcc.pos : ∀ {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}}, o.IsAcc S → 0 < o
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.preprocessOutParam.preprocessLevels : Array ℕ → List Lean.Level → ℕ → Lean.MetaM (List Lean.Level)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure.of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {x y : C} (f : x ⟶ y),
  W f → W.multiplicativeClosure f
-- Mathlib.LinearAlgebra.Eigenspace.Semisimple
Module.End.IsSemisimple.eq_zero_iff_forall_eigenvalue : ∀ {K : Type u_3} {V : Type u_4} [inst : Field K] [IsAlgClosed K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [FiniteDimensional K V] {f : Module.End K V}, f.IsSemisimple → (f = 0 ↔ ∀ (μ : K), f.HasEigenvalue μ → μ = 0)
-- Init.Data.SInt.Lemmas
Int16.toInt32_toISize : ∀ (n : Int16), n.toISize.toInt32 = n.toInt32
-- Mathlib.Analysis.Normed.Group.Uniform
AntilipschitzWith.add_lipschitzWith : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E},
  AntilipschitzWith Kf f → LipschitzWith Kg g → Kg < Kf⁻¹ → AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun x => f x + g x
-- Mathlib.Analysis.Convolution
MeasureTheory.AEStronglyMeasurable.convolution_integrand' : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ ν : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [MeasurableAdd₂ G] [MeasurableNeg G],
  MeasureTheory.AEStronglyMeasurable f ν →
    MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun p => p.1 - p.2) (μ.prod ν)) →
      MeasureTheory.AEStronglyMeasurable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.mapRingHom_comp`. -/
MonoidAlgebra.mapRangeRingHom_comp : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] [inst_3 : Monoid M] (f : S →+* T) (g : R →+* S),
  MonoidAlgebra.mapRingHom M (f.comp g) = (MonoidAlgebra.mapRingHom M f).comp (MonoidAlgebra.mapRingHom M g)
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.next : ∀ {l m₁ : List Char} {c : Char} {m₂ r : List Char} {s : Substring.Raw},
  Substring.Raw.ValidFor l (m₁ ++ c :: m₂) r s →
    s.next { byteIdx := String.utf8Len m₁ } = { byteIdx := String.utf8Len m₁ + c.utf8Size }
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.div_mem_ker_iff : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M] (f : G →* M) {x y : G},
  x / y ∈ f.ker ↔ f x = f y
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Ideal.strongNormalizationMonoid : {A : Type u_2} → [inst : CommRing A] → StrongNormalizationMonoid (Ideal A)
-- Lean.Attributes
Lean.EnumAttributes.setValue : {α : Type} → Lean.EnumAttributes α → Lean.Environment → Lean.Name → α → Except String Lean.Environment
-- Mathlib.Data.W.Constructions
WType.ofNat.eq_def : ∀ (x : ℕ),
  WType.ofNat x =
    match x with
    | Nat.zero => WType.mk WType.Natα.zero Empty.elim
    | n.succ => WType.mk WType.Natα.succ fun x => WType.ofNat n