mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.DirectSum.Module
DirectSum.coeLinearMap.eq_1 : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (A : ι → Submodule R M),
  DirectSum.coeLinearMap A = DirectSum.toModule R ι M fun i => (A i).subtype
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.le_antisymm : ∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d] {a b : ℤ√↑d}, a ≤ b → b ≤ a → a = b
-- Mathlib.Order.WithBot
/-- The equivalence between the non-top elements of `WithTop α` and `α`.  -/
Equiv.withTopSubtypeNe : {α : Type u_1} → { y // y ≠ ⊤ } ≃ α
-- Batteries.Lean.Expr
/-- Converts an `Expr` into a `Syntax`, by creating a fresh metavariable
assigned to the expr and  returning a named metavariable syntax `?a`.  -/
Lean.Expr.toSyntax : Lean.Expr → Lean.Elab.TermElabM Lean.Term
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.toSymmetricCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.SymmetricCategory C
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.closure_inv : ∀ {G : Type u_2} [inst : Group G] (s : Set G), Subgroup.closure s⁻¹ = Subgroup.closure s
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.insert k).contains k = true
-- Mathlib.SetTheory.Ordinal.Notation
ONote.instWellFoundedRelation : WellFoundedRelation ONote
-- Init.Data.BitVec.Lemmas
BitVec.ofFin_sub : ∀ {n : ℕ} (x : Fin (2 ^ n)) (y : BitVec n), { toFin := x } - y = { toFin := x - y.toFin }
-- Init.Data.String.Basic
/-- Returns the first position where the two strings differ.

If one string is a prefix of the other, then the returned position is the end position of the
shorter string. If the strings are identical, then their end position is returned.

Examples:
* `"tea".firstDiffPos "ten" = ⟨2⟩`
* `"tea".firstDiffPos "tea" = ⟨3⟩`
* `"tea".firstDiffPos "teas" = ⟨3⟩`
* `"teas".firstDiffPos "tea" = ⟨3⟩`
 -/
String.firstDiffPos : String → String → String.Pos.Raw
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.inter_vsub_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s₁ s₂ t : Finset β}
  [inst_2 : DecidableEq β], s₁ ∩ s₂ -ᵥ t ⊆ (s₁ -ᵥ t) ∩ (s₂ -ᵥ t)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableWithinAt.smul_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {f : B → 𝕜}
  {s : (x : B) → E x} {u : Set B} {x₀ : B},
  MDiffAt[u] f x₀ → MDiffAt[u] (T% s) x₀ → (MDiffAt[u] fun x => ⟨x, (f • s) x⟩) x₀
-- Init.Data.SInt.Lemmas
Int32.toInt16_toInt64 : ∀ (n : Int32), n.toInt64.toInt16 = n.toInt16
-- Lean.Expr
/-- Given `a b : Int`, returns `a * b`  -/
Lean.mkIntMul : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBySet_quotient_set_smul : ∀ {R : Type u_1} (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (s : Set R),
  Module.IsTorsionBySet R (M ⧸ s • ⊤) s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        k ∉ m₂ → Std.DHashMap.Raw.Const.getD (m₁ ∪ m₂) k fallback = Std.DHashMap.Raw.Const.getD m₁ k fallback
-- Mathlib.Algebra.GroupWithZero.Action.Basic
/-- Each element of the group defines an additive monoid isomorphism.

This is a stronger version of `MulAction.toPermHom`.  -/
DistribMulAction.toAddAut : (G : Type u_1) →
  (A : Type u_3) → [inst : Group G] → [inst_1 : AddMonoid A] → [DistribMulAction G A] → G →* Multiplicative (AddAut A)
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- Pull back the normed algebra structure from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A` using the
algebra homomorphism `Unitization.splitMul 𝕜 A`. This uses the wrong `NormedRing` instance (i.e.,
`Unitization.normedRingAux`), so we only use it as a local instance to build the real one.  -/
Unitization.normedAlgebraAux : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : IsScalarTower 𝕜 A A] →
            [inst_4 : SMulCommClass 𝕜 A A] → [inst_5 : RegularNormedAlgebra 𝕜 A] → NormedAlgebra 𝕜 (Unitization 𝕜 A)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iio_ssubset_Iio : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α], a < b → Finset.Iio a ⊂ Finset.Iio b
-- Lean.Elab.Binders
/-- Like `elabBinders`, but also pass syntax node per binder.
`elabBinders(Ex)` automatically adds binder info nodes for the produced fvars, but storing the syntax nodes
might be necessary when later adding the same binders back to the local context so that info nodes can
manually be added for the new fvars; see `MutualDef` for an example.  -/
Lean.Elab.Term.elabBindersEx : {α : Type} → Array Lean.Syntax → (Array (Lean.Syntax × Lean.Expr) → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Array.0.Std.Iterators.Types.ArrayIterator.instIterator.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) (it : Std.IterM m α)
  (h_1 : (it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out))
  (h_2 : (it : Std.IterM m α) → motive (Std.IterStep.skip it)) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_2 it
-- Mathlib.Algebra.Ring.Basic
AddMonoid.End.mulLeft_apply_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (r x : R), (AddMonoid.End.mulLeft r) x = r * x
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.desc.multicofork_pt : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁),
  (SSet.horn₃₂.desc.multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).pt = X
-- Mathlib.Condensed.Discrete.Characterization
LightCondMod.isDiscrete_tfae : ∀ (R : Type u) [inst : Ring R] (M : LightCondMod R),
  [LightCondensed.IsDiscrete M,
      CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (LightCondensed.discrete (ModuleCat R)).essImage M, (LightCondMod.LocallyConstant.functor R).essImage M,
      CategoryTheory.IsIso ((LightCondMod.LocallyConstant.adjunction R).counit.app M),
      ∀ (S : LightProfinite),
        Nonempty
          (CategoryTheory.Limits.IsColimit
            (M.obj.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE
-- Mathlib.Topology.Algebra.Valued.WithVal
Valuation.IsEquiv.uniformContinuous_equiv : ∀ {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} [hval : Valued R Γ₀'],
  Valued.v = w → v.IsEquiv w → UniformContinuous ⇑(WithVal.equiv v)
-- Mathlib.Analysis.Complex.Exponential
Complex.exp'.eq_1 : ∀ (z : ℂ), Complex.exp' z = ⟨fun n => ∑ m ∈ Finset.range n, z ^ m / ↑m.factorial, ⋯⟩
-- Mathlib.SetTheory.Ordinal.Notation
/-- `TopBelow b o` asserts that the largest exponent in `o`, if it exists, is less than `b`. This is
an auxiliary definition for decidability of `NF`.  -/
ONote.TopBelow : ONote → ONote → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
measurable_fderiv_with_param : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [LocallyCompactSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] {α : Type u_4} [inst_6 : TopologicalSpace α] {f : α → E → F} [inst_7 : MeasurableSpace α]
  [OpensMeasurableSpace α] [inst_9 : MeasurableSpace E] [OpensMeasurableSpace E] [CompleteSpace F],
  Continuous (Function.uncurry f) → Measurable fun p => fderiv 𝕜 (f p.1) p.2
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- Considering all diagrams consisting of a morphism `f : X ⟶ Y` satisfying `W`
and of a morphism `d : X ⟶ Z`, this is the morphism from the coproduct of
all these `X` objects to `Z` given by these morphisms `d`.  -/
CategoryTheory.OrthogonalReflection.D₁.l : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (Z : C) →
        [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
          ∐ CategoryTheory.OrthogonalReflection.D₁.obj₁ ⟶ Z
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action map  -/
CategoryTheory.AddModObj.vadd : {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.MonoidalLeftAction C D} →
            {M : C} →
              {inst_4 : CategoryTheory.AddMonObj M} →
                {X : D} →
                  [self : CategoryTheory.AddModObj M X] →
                    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj M X ⟶ X
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Intermediate stage of assembling the counit.  -/
CategoryTheory.OverPresheafAux.counitAuxAux : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) →
        (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) →
          F.obj (Opposite.op s) ≅
            CategoryTheory.OverPresheafAux.OverArrows (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F)
              s.hom
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- Concatenate together two matrices A₁[m₁ × N] and A₂[m₂ × N] with the same columns (N) to get a
bigger matrix indexed by [(m₁ ⊕ m₂) × N]  -/
Matrix.fromRows : {R : Type u_1} →
  {m₁ : Type u_3} → {m₂ : Type u_4} → {n : Type u_5} → Matrix m₁ n R → Matrix m₂ n R → Matrix (m₁ ⊕ m₂) n R
-- Mathlib.Topology.UniformSpace.Defs
comp_comp_symm_mem_uniformity_sets : ∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α},
  s ∈ uniformity α → ∃ t ∈ uniformity α, SetRel.IsSymm t ∧ (SetRel.comp t t).comp t ⊆ s
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- The fiber functor on the category of sheaves that is given a by a point of a site.  -/
CategoryTheory.GrothendieckTopology.Point.sheafFiber : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      J.Point →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
              CategoryTheory.Functor (CategoryTheory.Sheaf J A) A
-- Mathlib.Topology.Order.LiminfLimsup
/-- A continuous antitone function between (conditionally) complete linear ordered spaces sends a
`Filter.liminf` to the `Filter.limsup` of the images (if the filter is bounded from below and
frequently bounded from above).  -/
Antitone.map_liminf_of_continuousAt : ∀ {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [F.NeBot] [inst : ConditionallyCompleteLinearOrder R]
  [inst_1 : TopologicalSpace R] [OrderTopology R] [inst_3 : ConditionallyCompleteLinearOrder S]
  [inst_4 : TopologicalSpace S] [OrderTopology S] {f : R → S},
  Antitone f →
    ∀ (a : ι → R),
      ContinuousAt f (Filter.liminf a F) →
        autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F a) Antitone.map_liminf_of_continuousAt._auto_1 →
          autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F a) Antitone.map_liminf_of_continuousAt._auto_3 →
            f (Filter.liminf a F) = Filter.limsup (f ∘ a) F
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFreeOn_univ : ∀ {α : Type u_1} (G : SimpleGraph α) {n : ℕ}, G.CliqueFreeOn Set.univ n ↔ G.CliqueFree n
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
/-- A `RightPreLieAlgebra` is a `RightPreLieRing` with an action of a `CommRing` satisfying
`r • x * y = r • (x * y)` and ` x * (r • y) = r • (x * y)`.  -/
RightPreLieAlgebra : (R : Type u_1) → [CommRing R] → (L : Type u_2) → [RightPreLieRing L] → Type (max u_1 u_2)
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.instFullModuleCatForget₂LinearMapIdCarrierObjIsFG : ∀ (R : Type u) [inst : Ring R], (CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).Full
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- The natural transformation `ι S ≅ (inducedFunctor p S) ⋙ (fiberInclusion p S)`  -/
HasFibers.inducedFunctor.natIso : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        (p : CategoryTheory.Functor 𝒳 𝒮) →
          [inst_2 : HasFibers p] →
            (S : 𝒮) → HasFibers.ι S ≅ (HasFibers.inducedFunctor p S).comp CategoryTheory.Functor.Fiber.fiberInclusion
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.instUniqueTerminalType : Unique (⊤_ Type u)
-- Init.Data.List.Basic
/-- Returns the first element of the list for which the predicate `p` returns `true`, or `none` if no
such element is found.

`O(|l|)`.

Examples:
* `[7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 1`
* `[7, 6, 5, 8, 1, 2, 6].find? (· < 1) = none`
 -/
List.find? : {α : Type u} → (α → Bool) → List α → Option α
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableWithinAt_of_isInvertible_fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E},
  (fderivWithin 𝕜 f s x).IsInvertible → DifferentiableWithinAt 𝕜 f s x
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.checkNoWsBefore.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k k' : α}, cmp k k' = Ordering.eq → t.getKey! k = t.getKey! k'
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessKind.noConfusionType : Sort v✝ → Lean.Meta.PreprocessKind✝ → Lean.Meta.PreprocessKind✝ → Sort v✝
-- Init.Data.Array.Lemmas
Array.map_inj_left : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f g : α → β}, Array.map f xs = Array.map g xs ↔ ∀ a ∈ xs, f a = g a
-- Mathlib.Order.InitialSeg
PrincipalSeg.top_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  [IsWellOrder γ t] (e : r ≃r s) (f : PrincipalSeg r t) (g : PrincipalSeg s t), f.top = g.top
-- Init.Data.Vector.Basic
Vector.cast.eq_1 : ∀ {n m : ℕ} {α : Type u_1} (h : n = m) (xs : Vector α n), Vector.cast h xs = Vector.mk xs.toArray ⋯
-- Mathlib.LinearAlgebra.Finsupp.Span
Finsupp.span_single_eq_top : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Submodule.span R {x | ∃ i x_1, (fun₀ | i => x_1) = x} = ⊤
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_mul : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (x y : ↥H), ↑(x * y) = ↑x * ↑y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.isSome_minKey?_modify_eq_isSome : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β}, (Std.ExtDTreeMap.Const.modify t k f).minKey?.isSome = t.minKey?.isSome
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.d₃.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄),
  HomologicalComplex.mapBifunctor₂₃.d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j =
    HomologicalComplex.mapBifunctor₂₃.d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_algebraMap : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {r : NNReal},
  CFC.sqrt ((algebraMap NNReal A) r) = (algebraMap NNReal A) (NNReal.sqrt r)
-- Mathlib.Topology.Algebra.Group.Units
/-- If a submonoid is open in a topological monoid, then its units form an open subset
of the units of the monoid.  -/
Submonoid.isOpen_units : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M] {U : Submonoid M}, IsOpen ↑U → IsOpen ↑U.units
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
/-- The topology of compact convergence on `E →L[𝕜] F`.  -/
CompactConvergenceCLM.«term_→SL_c[_]_» : Lean.TrailingParserDescr
-- Mathlib.RepresentationTheory.Equiv
/-- The equivalence of representations between `(Fin 1 → G) →₀ k` and `G →₀ k`.  -/
Representation.diagonalOneEquivLeftRegular : (k : Type u) →
  [inst : Semiring k] →
    (G : Type v) → [inst_1 : Monoid G] → (Representation.diagonal k G 1).Equiv (Representation.leftRegular k G)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
/-- The short complex `Hᵢ(G, X₁) ⟶ Hᵢ(G, X₂) ⟶ Hᵢ(G, X₃)` associated to a short complex of
representations `X₁ ⟶ X₂ ⟶ X₃`.  -/
groupHomology.mapShortComplex₂ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → CategoryTheory.ShortComplex (Rep.{u, u, u} k G) → ℕ → CategoryTheory.ShortComplex (ModuleCat k)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_comp_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X W] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z W]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct Y W] {Z_1 : C} (h : Z ⨯ W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id W))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g (CategoryTheory.CategoryStruct.id W)) h)
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- The left adjoint functor to `R` given by `[MonadicRightAdjoint R]`.  -/
CategoryTheory.monadicLeftAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (R : CategoryTheory.Functor D C) → [CategoryTheory.MonadicRightAdjoint R] → CategoryTheory.Functor C D
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- Given `f : α → β` and a topology on `α`, the coinduced additive group topology on `β`
is the finest topology such that `f` is continuous and `β` is a topological additive group.  -/
AddGroupTopology.coinduced : {α : Type u_1} → {β : Type u_2} → [t : TopologicalSpace α] → [inst : AddGroup β] → (α → β) → AddGroupTopology β
-- Mathlib.Algebra.Polynomial.Homogenize
/-- `homogenize` as a bundled linear map.  -/
Polynomial.homogenizeLM : {R : Type u_1} → [inst : CommSemiring R] → ℕ → Polynomial R →ₗ[R] MvPolynomial (Fin 2) R
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.norm_num_ext.sModNatAux_eq : ∀ (q k : ℕ), LucasLehmer.norm_num_ext.sModNatAux (4 % q) q k = LucasLehmer.norm_num_ext.sModNat q k
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum_of_ac : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G]
  {ν : MeasureTheory.Measure α},
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ν.AbsolutelyContinuous μ → ∀ (t : Set α), ν t = ∑' (g : G), ν (t ∩ (g +ᵥ s))
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.smul_isUnit_iff : ∀ {M₁ : Type u_3} {M₂ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁]
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] {S : Type u_6} [inst_4 : Monoid S]
  [inst_5 : DistribMulAction S M₂] [ContinuousConstSMul S M₂] {f : M₁ → M₂} {c : S},
  IsUnit c → (IsCompactOperator (c • f) ↔ IsCompactOperator f)
-- Init.Data.Ord.Basic
Ordering.swap_eq : Ordering.eq.swap = Ordering.eq
-- Aesop.Index.Basic
Aesop.instInhabitedIndexingMode.default : Aesop.IndexingMode
-- Mathlib.Data.Set.Image
Set.range_const : ∀ {α : Type u_1} {ι : Sort u_4} [Nonempty ι] {c : α}, (Set.range fun x => c) = {c}
-- Mathlib.Data.Set.Card
Set.nonempty_of_ncard_ne_zero : ∀ {α : Type u_1} {s : Set α}, s.ncard ≠ 0 → s.Nonempty