mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_lt_aleph : ∀ {o₁ o₂ : Ordinal.{u_1}}, Cardinal.aleph o₁ < Cardinal.aleph o₂ ↔ o₁ < o₂
-- Mathlib.Algebra.Order.SuccPred
Order.sub_one_covBy : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Sub α] [inst_2 : One α] [PredSubOrder α] [NoMinOrder α] (x : α),
  x - 1 ⋖ x
-- Lean.Meta.SizeOf
_private.Lean.Meta.SizeOf.0.Lean.Meta.mkSizeOfMinors : {α : Type} → Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A morphism between the two vertex objects of the bicones  -/
CategoryTheory.Limits.BinaryBiconeMorphism.hom : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        {A B : CategoryTheory.Limits.BinaryBicone P Q} → CategoryTheory.Limits.BinaryBiconeMorphism A B → (A.pt ⟶ B.pt)
-- Mathlib.Topology.Inseparable
/-- **Alias** of `SpecializingMap.stableUnderSpecialization_image`. -/
StableUnderSpecialization.image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  SpecializingMap f → ∀ {s : Set X}, StableUnderSpecialization s → StableUnderSpecialization (f '' s)
-- Init.Data.Nat.Lemmas
Nat.add_mod_eq_ite : ∀ {k m n : ℕ}, (m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k
-- Mathlib.Algebra.Group.Action.Basic
AddAction.toPerm_apply : ∀ {α : Type u_5} {β : Type u_6} [inst : AddGroup α] [inst_1 : AddAction α β] (a : α) (x : β),
  (AddAction.toPerm a) x = a +ᵥ x
-- Mathlib.Data.Nat.Prime.Basic
/-- If `0 < m < minFac n`, then `n` and `m` are coprime.  -/
Nat.coprime_of_lt_minFac : ∀ {n m : ℕ}, m ≠ 0 → m < n.minFac → n.Coprime m
-- Mathlib.Algebra.Algebra.Equiv
/-- The algebra equivalence between `ULift A` and `A`.  -/
ULift.algEquiv : {R : Type u} →
  {A : Type v} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → ULift.{w, v} A ≃ₐ[R] A
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
/-- The underlying space of a simplicial complex is the union of its faces.  -/
Geometry.SimplicialComplex.space : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : Ring 𝕜] →
      [inst_1 : PartialOrder 𝕜] →
        [inst_2 : AddCommGroup E] → [inst_3 : Module 𝕜 E] → Geometry.SimplicialComplex 𝕜 E → Set E
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- **Alias** of `AlgebraicGeometry.SmoothOfRelativeDimension.smooth`.

---

If `f` is smooth of any relative dimension, it is smooth.  -/
AlgebraicGeometry.IsSmoothOfRelativeDimension.isSmooth : ∀ (n : ℕ) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.SmoothOfRelativeDimension n f],
  AlgebraicGeometry.Smooth f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_eq_some_getElem! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α}, a ∈ t → t[a]? = some t[a]!
-- Mathlib.Order.LiminfLimsup
Filter.limsup_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : Filter β} {u : β → α},
  Filter.limsup u f = sInf {a | ∀ᶠ (n : β) in f, u n ≤ a}
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- If two valuations `v` and `w` are equivalent then `WithVal v` is order-isomorphic
to `WithVal w`.  -/
Valuation.IsEquiv.orderRingIso : {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 Γ₀'} → v.IsEquiv w → WithVal v ≃+*o WithVal w
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.disjoint_right_ordSeparatingSet : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α}, Disjoint t (s.ordSeparatingSet t)
-- Mathlib.Data.Finite.Prod
Function.Embedding.finite : ∀ {α : Sort u_3} {β : Sort u_4} [Finite β], Finite (α ↪ β)
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.mk.sizeOf_spec : ∀ (zonesPaths : Array System.FilePath), sizeOf { zonesPaths := zonesPaths } = 1 + sizeOf zonesPaths
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
/-- Two multiplicative functions `f` and `g` are equal if and only if
they agree on prime powers  -/
ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] (f : ArithmeticFunction R),
  f.IsMultiplicative →
    ∀ (g : ArithmeticFunction R), g.IsMultiplicative → (f = g ↔ ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i))
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_eq_zero_iff : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ) [IsDomain R] [NeZero 2], Polynomial.Chebyshev.U R n = 0 ↔ n = -1
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.Quotient.orbit_injective : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α],
  Function.Injective AddAction.orbitRel.Quotient.orbit
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.compl_compl : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Closeds α), s.compl.compl = s
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
DifferentiableAt.lineDifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {x v : E}, DifferentiableAt 𝕜 f x → LineDifferentiableAt 𝕜 f x v
-- Mathlib.Algebra.Group.Center
isMulCentral_iff : ∀ {M : Type u_1} [inst : Mul M] (z : M),
  IsMulCentral z ↔
    (∀ (a : M), Commute z a) ∧ (∀ (b c : M), z * (b * c) = z * b * c) ∧ ∀ (a b : M), a * b * z = a * (b * z)
-- Mathlib.Data.Nat.PSub
Nat.psub_eq_sub : ∀ {m n : ℕ}, n ≤ m → m.psub n = some (m - n)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (List.map Sigma.fst l).contains k = false → (t.insertMany l).getKey? k = t.getKey? k
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneUnopOfCoconeEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ},
  CategoryTheory.Limits.coneUnopOfCoconeEquiv =
    CategoryTheory.Equivalence.mk''
      { obj := fun c => CategoryTheory.Limits.coneUnopOfCocone (Opposite.unop c),
        map := fun {Y X} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }
      { obj := fun c => Opposite.op (CategoryTheory.Limits.coconeOfConeUnop c),
        map := fun {Y X} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }
      (CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)ᵒᵖ))
      (CategoryTheory.Iso.refl
        ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coconeOfConeUnop c),
              map := fun {Y X} f => Opposite.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp
          { obj := fun c => CategoryTheory.Limits.coneUnopOfCocone (Opposite.unop c),
            map := fun {Y X} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }))
      ⋯
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ioo_inl_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (a : α) (b : β),
  Finset.Ioo (Sum.inlₗ a) (Sum.inrₗ b) = Finset.map toLex.toEmbedding ((Finset.Ioi a).disjSum (Finset.Iio b))
-- Init.Data.Vector.Lemmas
Vector.mem_of_ne_of_mem : ∀ {α : Type u_1} {n : ℕ} {a y : α} {xs : Vector α n}, a ≠ y → a ∈ xs.push y → a ∈ xs
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The constructed pointwise left Kan extension when `HasPointwiseLeftKanExtension L F` holds.  -/
CategoryTheory.Functor.pointwiseLeftKanExtension : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) → [L.HasPointwiseLeftKanExtension F] → CategoryTheory.Functor D H
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.subtype_comp_rangeRestrict : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N),
  f.range.subtype.comp f.rangeRestrict = f
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of a scalar product is the scalar product of the trailing coefficients.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f₁ : 𝕜 → 𝕜} {f₂ : 𝕜 → E},
  MeromorphicAt f₁ x →
    MeromorphicAt f₂ x →
      meromorphicTrailingCoeffAt (f₁ • f₂) x = meromorphicTrailingCoeffAt f₁ x • meromorphicTrailingCoeffAt f₂ x
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.applyPartition_eq_apply_toListModel' : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering}
  [Std.Internal.IsStrictCut compare k] {l : Std.DTreeMap.Internal.Impl α β},
  l.Ordered →
    ∀
      {f :
        List ((a : α) × β a) →
          (c : Std.DTreeMap.Internal.Cell α β k) →
            (Std.DTreeMap.Internal.Impl.contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ}
      (g : List ((a : α) × β a) → δ),
      (∀ {ll rr : List ((a : α) × β a)} {c : Std.DTreeMap.Internal.Cell α β k}
          {h₁ : Std.DTreeMap.Internal.Impl.contains' k l = true → c.contains = true},
          List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) (ll ++ c.inner.toList ++ rr) →
            (∀ p ∈ ll, k p.fst = Ordering.gt) →
              (∀ p ∈ rr, k p.fst = Ordering.lt) → f ll c h₁ rr = g (ll ++ c.inner.toList ++ rr)) →
        Std.DTreeMap.Internal.Impl.applyPartition k l f = g l.toListModel
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.eulerChar_orderDual : ∀ (𝕜 : Type u_2) {α : Type u_5} [inst : Ring 𝕜] [inst_1 : PartialOrder α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq α] [inst_4 : BoundedOrder α], IncidenceAlgebra.eulerChar 𝕜 αᵒᵈ = IncidenceAlgebra.eulerChar 𝕜 α
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.closure.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] (s : Set M), Submonoid.closure s = sInf {S | s ⊆ ↑S}
-- Lean.Parser.Basic
/-- Specifies how the parsing table lookup function behaves for identifiers.

The function `Lean.Parser.prattParser` uses two tables: one each for leading and trailing parsers.
These tables map tokens to parsers. Because keyword tokens are distinct from identifier tokens,
keywords and identifiers cannot be confused, even when they are syntactically identical.
Specifying an alternative leading identifier behavior allows greater flexibility and makes it
possible to avoid reserved keywords in some situations.

When the leading token is syntactically an identifier, the current syntax category's
`LeadingIdentBehavior` specifies how the parsing table lookup function behaves, and allows
controlled “punning” between identifiers and keywords. This feature is used to avoid creating a
reserved symbol for each built-in tactic (e.g., `apply` or `assumption`). As a result, tactic names
can be used as identifiers.
 -/
Lean.Parser.LeadingIdentBehavior : Type
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.instInhabitedTaggedState.default : Lean.Widget.TaggedText.TaggedState✝
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.op_ι_app_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Fork f g),
  c.op.ι.app CategoryTheory.Limits.WalkingParallelPair.one = (c.π.app CategoryTheory.Limits.WalkingParallelPair.zero).op
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Counting.0.SimpleGraph.finsetWalkLength.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₂ → k ∈ m₁
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.coeAddHom_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [inst_13 : VectorBundle 𝕜 F V] (s : ContMDiffSection I F n V),
  (ContMDiffSection.coeAddHom I F n V) s = ⇑s
-- Mathlib.Data.Finsupp.Defs
_private.Mathlib.Data.Finsupp.Defs.0.Finsupp.embDomain.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k a : α} {v : β},
  Std.DHashMap.Const.get? (m.insertIfNew k v) a =
    if (k == a) = true ∧ k ∉ m then some v else Std.DHashMap.Const.get? m a
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.pow : ∀ {R : Type u_1} [inst : CommSemiring R] {f : ArithmeticFunction R},
  f.IsMultiplicative → ∀ {k : ℕ}, (f ^ k).IsMultiplicative
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.norm.go.eq_2 : ∀ (r : Nat.Internal.Linear.Poly) (k : ℕ) (v : Nat.Internal.Linear.Var) (p_2 : List (ℕ × Nat.Internal.Linear.Var)),
  Nat.Internal.Linear.Poly.norm.go ((k, v) :: p_2) r =
    Nat.Internal.Linear.Poly.norm.go p_2 (Nat.Internal.Linear.Poly.insert k v r)
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.trace_nonneg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {f : E →ₗ[𝕜] E}, f.IsPositive → 0 ≤ (LinearMap.trace 𝕜 E) f
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The bottom map in the oplax right unitality square.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapᵣ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                  CategoryTheory.MonoidalCategoryStruct.tensorUnit D) →
                ((CategoryTheory.MonoidalCategory.curriedTensorPre F).flip.obj
                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                  F.comp (CategoryTheory.MonoidalCategory.tensorUnitRight D))
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- `F ⋙ FintypeCat.incl` as a cocone over `(can F).op ⋙ coyoneda`.
This is a colimit cocone (see `PreGaloisCategory.isColimit`)  -/
CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        CategoryTheory.Limits.Cocone
          ((CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).op.comp CategoryTheory.coyoneda)
-- Mathlib.Data.PFun
WellFounded.fixF.congr_simp : ∀ {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F F_1 : (x : α) → ((y : α) → r y x → C y) → C x),
  F = F_1 → ∀ (x : α) (a : Acc r x), WellFounded.fixF F x a = WellFounded.fixF F_1 x a
-- Mathlib.ModelTheory.Definability
/-- This lemma is only intended as a helper for `Definable.image_comp`.  -/
Set.Definable.image_comp_sumInl_fin : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} (m : ℕ)
  {s : Set (α ⊕ Fin m → M)}, A.Definable L s → A.Definable L ((fun g => g ∘ Sum.inl) '' s)
-- Mathlib.CategoryTheory.Limits.Preorder
/-- The cone associated to a lower bound of a functor.  -/
Preorder.coneOfLowerBound : {C : Type u} →
  [inst : Preorder C] →
    {J : Type u'} →
      [inst_1 : CategoryTheory.Category.{v, u'} J] →
        (F : CategoryTheory.Functor J C) → {x : C} → x ∈ lowerBounds (Set.range F.obj) → CategoryTheory.Limits.Cone F
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The isomorphism `S₁.cycles ≅ S₂.cycles` induced by an isomorphism
of short complexes `S₁ ≅ S₂`.  -/
CategoryTheory.ShortComplex.cyclesMapIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ≅ S₂) → [inst_2 : S₁.HasLeftHomology] → [inst_3 : S₂.HasLeftHomology] → S₁.cycles ≅ S₂.cycles
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- **Alias** of `CircleIntegrable.fun_continuousOn_smul`.

---

Eta-expanded form of `CircleIntegrable.continuousOn_smul`

---

If `g` is continuous on the circle `sphere c |R|` and `f` is circle integrable, then `g • f` is
circle integrable.
 -/
CircleIntegrable.fun_smul_of_continuousOn : ∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} {F : Type u_4} [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : Module 𝕜 F] [NormSMulClass 𝕜 F] {f : ℂ → F} {g : ℂ → 𝕜},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (fun i => g i • f i) c R
-- Mathlib.CategoryTheory.Abelian.Refinements
CategoryTheory.Limits.CokernelCofork.IsColimit.comp_π_eq_zero_iff_up_to_refinements : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} {f : X ⟶ Y}
  {c : CategoryTheory.Limits.CokernelCofork f} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (y : A ⟶ Y),
  CategoryTheory.CategoryStruct.comp y (CategoryTheory.Limits.Cofork.π c) = 0 ↔
    ∃ A' π,
      ∃ (_ : CategoryTheory.Epi π), ∃ x, CategoryTheory.CategoryStruct.comp π y = CategoryTheory.CategoryStruct.comp x f
-- Lean.Elab.BuiltinNotation
/-- Elaborator for `by_elab`.  -/
Lean.Elab.Term.elabRunElab : Lean.Elab.Term.TermElab
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (n : σ →₀ ℕ), (MvPowerSeries.coeff n) 0 = 0
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.map_counit_comp_comul_left_assoc : ∀ {R : Type u_1} {M : Type u_3} {P : Type u_5} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid P] [inst_4 : Module R P] [inst_5 : AddCommMonoid M']
  [inst_6 : Module R M'] [inst_7 : Coalgebra R M] (f : M →ₗ[R] M') (g : P →ₗ[R] M),
  TensorProduct.map CoalgebraStruct.counit f ∘ₗ CoalgebraStruct.comul ∘ₗ g =
    TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.lid R M).symm ∘ₗ g
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
/-- For `A : Matrix V V α` and `h : IsAdjMatrix A`,
`h.toGraph` is the simple graph whose adjacency matrix is `A`.  -/
Matrix.IsAdjMatrix.toGraph : {α : Type u_1} →
  {V : Type u_2} → {A : Matrix V V α} → [inst : MulZeroOneClass α] → [Nontrivial α] → A.IsAdjMatrix → SimpleGraph V
-- Mathlib.Algebra.Symmetrized
SymAlg.instModule : {α : Type u_1} → {R : Type u_2} → [inst : Semiring R] → [inst_1 : AddCommMonoid α] → [Module R α] → Module R αˢʸᵐ
-- Init.Data.Order.PackageFactories
Std.Packages.PartialOrderOfLEArgs.mk.injEq : ∀ {α : Type u} (toPreorderOfLEArgs : Std.Packages.PreorderOfLEArgs α)
  (le_antisymm :
    autoParam
      (let this := toPreorderOfLEArgs.le;
      ∀ (a b : α), a ≤ b → b ≤ a → a = b)
      Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam)
  (toPreorderOfLEArgs_1 : Std.Packages.PreorderOfLEArgs α)
  (le_antisymm_1 :
    autoParam
      (let this := toPreorderOfLEArgs_1.le;
      ∀ (a b : α), a ≤ b → b ≤ a → a = b)
      Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam),
  ({ toPreorderOfLEArgs := toPreorderOfLEArgs, le_antisymm := le_antisymm } =
      { toPreorderOfLEArgs := toPreorderOfLEArgs_1, le_antisymm := le_antisymm_1 }) =
    (toPreorderOfLEArgs = toPreorderOfLEArgs_1)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_const_Iic : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x * a) '' Set.Iic b = Set.Iic (b * a)
-- Mathlib.Topology.Algebra.Group.Defs
/-- A typeclass saying that `p : G × G ↦ p.1 / p.2` is a continuous function. This property
automatically holds for topological groups. Lemmas using this class have primes.
The unprimed version is for `GroupWithZero`.  -/
ContinuousDiv : (G : Type u_4) → [TopologicalSpace G] → [Div G] → Prop
-- Mathlib.Control.Fold
Traversable.foldlm.ofFreeMonoid_comp_of : ∀ {α β : Type u} {m : Type u → Type u} [inst : Monad m] [inst_1 : LawfulMonad m] (f : α → β → m α),
  ⇑(Monoid.foldlM.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.foldlM.mk ∘ flip f
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.zero : Zero Ordinal.{u_1}
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_X_of_ne_one : ∀ {R : Type u_1} [inst : Semiring R] {n : ℕ}, n ≠ 1 → SkewPolynomial.X.coeff n = 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_comp_δ' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j),
  CategoryTheory.CategoryStruct.comp (X.δ j) (X.δ i) =
    CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (X.δ (j.pred ⋯))
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.toPowerSeriesAlg_symm_apply_coeff : ∀ (R : Type u_2) [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A] (f : PowerSeries A)
  (n : ℕ), ((HahnSeries.toPowerSeriesAlg R).symm f).coeff n = (PowerSeries.coeff n) f
-- Mathlib.Algebra.Order.Floor.Semifield
/-- `norm_num` extension for `Nat.floor`  -/
Mathlib.Meta.NormNum.evalNatFloor : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : OmegaCompletePartialOrder α]
  [inst_1 : OmegaCompletePartialOrder β] [inst_2 : OmegaCompletePartialOrder γ] [inst_3 : OmegaCompletePartialOrder δ]
  (f : γ →𝒄 δ) (g : β →𝒄 γ) (h : α →𝒄 β), f.comp (g.comp h) = (f.comp g).comp h
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.le_def : ∀ {E : Type u_3} [inst : Group E] {p q : GroupSeminorm E}, p ≤ q ↔ ⇑p ≤ ⇑q
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.unionProd.ι₁_ι_assoc : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) {Z : SSet}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.unionProd.ι₁ S T)
      (CategoryTheory.CategoryStruct.comp (S.unionProd T).ι h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X T.ι) h
-- Mathlib.Algebra.BigOperators.Ring.Finset
Fintype.sum_mul_sum : ∀ {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Fintype ι]
  [inst_2 : Fintype κ] (f : ι → R) (g : κ → R), (∑ i, f i) * ∑ j, g j = ∑ i, ∑ j, f i * g j