mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.homRestrict_comp_extendMap : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L L' : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (ψ : K ⟶ L.extend e) (β : L ⟶ L'),
  e.homRestrict (CategoryTheory.CategoryStruct.comp ψ (HomologicalComplex.extendMap β e)) =
    CategoryTheory.CategoryStruct.comp (e.homRestrict ψ) β
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.hom_zero : ∀ (X Y : AddMonCat), AddMonCat.Hom.hom 0 = 0
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Differentiable.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : E → ℂ},
  Differentiable 𝕜 f → Differentiable 𝕜 fun x => Complex.exp (f x)
-- Mathlib.Algebra.Ring.Subgroup
/-- For additive subgroups `S` and `T` of a ring, the product of `S` and `T` as submonoids
is automatically a subgroup, which we define as the product of `S` and `T` as subgroups.  -/
AddSubgroup.mul : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → Mul (AddSubgroup R)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inr_desc_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0)
  {Z : HomologicalComplex C c} (h : K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr φ)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.desc φ α hα) h) =
    CategoryTheory.CategoryStruct.comp α h
-- Mathlib.Algebra.AddConstMap.Basic
/-- Composition of two `AddConstMap`s.  -/
AddConstMap.comp : {G : Type u_1} →
  {H : Type u_2} →
    [inst : Add G] →
      [inst_1 : Add H] →
        {a : G} →
          {b : H} →
            {K : Type u_3} →
              [inst_2 : Add K] → {c : K} → AddConstMap H K b c → AddConstMap G H a b → AddConstMap G K a c
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.filter!_equiv_self_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filter! f t).Equiv t ↔
      ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true),
        f (t.getKey a h) (Std.DTreeMap.Internal.Impl.Const.get t a h) = true)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.instInhabited : {n : ℕ} → Inhabited (DihedralGroup n)
-- Mathlib.GroupTheory.FixedPointFree
MonoidHom.FixedPointFree.prod_pow_eq_one : ∀ {F : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : FunLike F G G] [MonoidHomClass F G G] {φ : F} [Finite G],
  MonoidHom.FixedPointFree ⇑φ →
    ∀ {n : ℕ}, (⇑φ)^[n] = id → ∀ (g : G), (List.map (fun k => (⇑φ)^[k] g) (List.range n)).prod = 1
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] [inst_4 : CategoryTheory.HasSheafify J AddCommGrpCat],
  CategoryTheory.Limits.PreservesFiniteLimits ((PresheafOfModules.sheafification α).comp (SheafOfModules.toSheaf R))
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure.eq_2 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  (f : α → C) (n : ℕ),
  CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure✝ f n.succ =
    ⟨CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep✝ (n + 1) fun m x =>
        CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure✝ f m,
      CategoryTheory.IsCofiltered.CofilteredClosureSmall.inductiveStepRealization✝ (n + 1) fun m x =>
        CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure✝ f m⟩
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.Hom.ext : ∀ {k : Type u} {G : Type v} {inst : Semiring k} {inst_1 : Monoid G} {A B : Rep.{w, u, v} k G} {x y : A.Hom B},
  x.hom' = y.hom' → x = y
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.iso_mk_one : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (x : M), (IsLocalizedModule.iso S f) (LocalizedModule.mk x 1) = f x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.minKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Order.Minimal
Minimal.mono : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : LE α], Minimal P x → Q ≤ P → Q x → Minimal Q x
-- Mathlib.RingTheory.Algebraic.Denominator
Algebra.isIntegral_natDenominator_smul : ∀ {S : Type u_2} [inst : CommRing S] (x : S), IsIntegral ℤ (Algebra.natDenominator x • x)
-- Mathlib.Tactic.Positivity.Basic
/-- **Alias** of the reverse direction of `NNRat.num_ne_zero`. -/
Mathlib.Meta.Positivity.NNRat.num_ne_zero_of_ne_zero : ∀ {q : ℚ≥0}, q ≠ 0 → q.num ≠ 0
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- The morphism `(A₁ ×_X A₂) ×_{A₁} (A₁ ×_X A₃) ⟶ A₂`.  -/
CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          [inst_2 : F.Full] →
            {A₁ A₂ A₃ : C} →
              {X : D} →
                {f₁ : F.obj A₁ ⟶ X} →
                  (hf₁ : F.relativelyRepresentable f₁) →
                    (f₂ : F.obj A₂ ⟶ X) →
                      (f₃ : F.obj A₃ ⟶ X) →
                        [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] →
                          hf₁.pullback₃ f₂ f₃ ⟶ A₂
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.CostructuredArrow.createsLimitsOfShape_walkingCospan : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      {A : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} A] →
          {L : CategoryTheory.Functor A T} →
            (X : T) →
              [P.IsStableUnderComposition] →
                [P.IsStableUnderBaseChange] →
                  [P.HasOfPostcompProperty P] →
                    [CategoryTheory.Limits.HasPullbacks A] →
                      [CategoryTheory.Limits.HasPullbacks T] →
                        [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan L] →
                          CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingCospan
                            (CategoryTheory.MorphismProperty.CostructuredArrow.forget P ⊤ L X)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_alter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k k' : α} {f : Option β → Option β},
  k' ∈ (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl ↔
    if compare k k' = Ordering.eq then (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true else k' ∈ t
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.sumArrowIsometryEquivProdArrow_apply : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace γ] [inst_1 : Fintype α] [inst_2 : Fintype β]
  (f : α ⊕ β → γ), IsometryEquiv.sumArrowIsometryEquivProdArrow f = (f ∘ Sum.inl, f ∘ Sum.inr)
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.zpow_mod_period_smul : ∀ {α : Type v} {G : Type u} [inst : Group G] [inst_1 : MulAction G α] (j : ℤ) {g : G} {a : α},
  g ^ (j % ↑(MulAction.period g a)) • a = g ^ j • a
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.comp_clm : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} {M₃ : Type u_6} [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂]
  [inst_4 : TopologicalSpace M₃] [inst_5 : AddCommMonoid M₁] [inst_6 : Module R₁ M₁] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₂ M₂] {f : M₂ → M₃}, IsCompactOperator f → ∀ (g : M₁ →SL[σ₁₂] M₂), IsCompactOperator (f ∘ ⇑g)
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring is closed under subtraction  -/
Subring.sub_mem : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) {x y : R}, x ∈ s → y ∈ s → x - y ∈ s
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- Eta-expanded form of `Function.HasTemperateGrowth.neg` -/
Function.HasTemperateGrowth.fun_neg : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F}, Function.HasTemperateGrowth f → Function.HasTemperateGrowth fun i => -f i
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_iff_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, m.contains a = true ↔ a ∈ m
-- Mathlib.Algebra.WithConv
/-- A type synonym for the convolutive product of linear maps and intrinsic star.

The instances for the convolutive product and intrinsic star are only available with this type.

Use `WithConv.linearEquiv` to coerce into this type.  -/
WithConv : Sort u_1 → Sort (max 1 u_1)
-- Mathlib.Analysis.ODE.ExistUnique
/-- **Picard-Lindelöf (Cauchy-Lipschitz) theorem**, differential form. This version shows the
existence of a local solution whose initial point `x` may be different from the centre `x₀` of
the closed ball within which the properties of the vector field hold.  -/
IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E}
  {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K →
    x ∈ Metric.closedBall x₀ ↑r →
      ∃ α, α ↑t₀ = x ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Set.Icc tmin tmax) t
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_obj₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C), ((t.triangleLEGT n).obj j).obj₃ = (t.truncGT n).obj j
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasProducts A]
  (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C))
  [inst_3 : CategoryTheory.Preadditive A] {X Y : CategoryTheory.Functor Cᵒᵖ A} (f : X ⟶ Y) (n : ℕ),
  ((CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor E).map f).f n =
    CategoryTheory.Limits.Pi.map fun i => f.app (Opposite.op ((E.obj (Opposite.op { len := n })).obj i))
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.lhom_ext'_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] {N : Type u_7} [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R N] [inst_4 : Module R S] {f g : MonoidAlgebra S M →ₗ[R] N},
  f = g ↔ ∀ (x : M), f ∘ₗ MonoidAlgebra.lsingle x = g ∘ₗ MonoidAlgebra.lsingle x
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_diff_eq_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  (∀ a ∈ m₁, a ∉ m₂) → (m₁ \ m₂).size = m₁.size
-- Init.Data.List.MinMaxIdx
List.get_maxIdxOn?_lt_length : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α}
  (h : (List.maxIdxOn? f xs).isSome = true), (List.maxIdxOn? f xs).get h < xs.length
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
AddOpposite.comap_op_rightUniformSpace : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  UniformSpace.comap AddOpposite.op (IsTopologicalAddGroup.rightUniformSpace Gᵃᵒᵖ) =
    IsTopologicalAddGroup.leftUniformSpace G
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] (x : E) {r : ℝ},
  0 ≤ r → μ (Metric.ball x r) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.ball 0 1)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_add_tsub_comm : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c d : α} [AddLeftReflectLE α], b ≤ a → d ≤ c → a - b + (c - d) = a + c - (b + d)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulForwardPatternModel.skipPrefix?_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice},
  String.Slice.Pattern.ForwardPattern.skipPrefix? pat s = none ↔ ¬String.Slice.Pattern.Model.MatchesAt pat s.startPos
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpaceCore.open_source' : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] (c : ChartedSpaceCore H M) {e : PartialEquiv M H},
  e ∈ c.atlas → IsOpen e.source
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
/-- The free additive monoid on `α` is isomorphic to
the free additive semigroup on `α` with a `0` added.  -/
FreeAddMonoid.equivWithZeroFreeAddSemigroup : {α : Type u_1} → FreeAddMonoid α ≃+ WithZero (FreeAddSemigroup α)
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddCommGroup.toNormedAddGroup : {E : Type u_5} → [NormedAddCommGroup E] → NormedAddGroup E
-- Mathlib.NumberTheory.Real.Irrational
irrational_add_ratCast_iff : ∀ {q : ℚ} {x : ℝ}, Irrational (x + ↑q) ↔ Irrational x
-- Lean.Data.Lsp.Client
Lean.Lsp.instToJsonRegistrationParams : Lean.ToJson Lean.Lsp.RegistrationParams
-- Mathlib.RingTheory.Ideal.Operations
Submodule.mul_smul : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (I J : Ideal R)
  (N : Submodule R M), (I * J) • N = I • J • N
-- Mathlib.Algebra.Group.UniqueProds.Basic
Prod.instTwoUniqueSums : ∀ {G : Type u} {H : Type v} [inst : Add G] [inst_1 : Add H] [TwoUniqueSums G] [TwoUniqueSums H], TwoUniqueSums (G × H)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- The family of seminorms obtained by composing each seminorm by a linear map.  -/
SeminormFamily.comp : {𝕜 : Type u_2} →
  {𝕜₂ : Type u_3} →
    {E : Type u_6} →
      {F : Type u_7} →
        {ι : Type u_9} →
          [inst : NormedField 𝕜] →
            [inst_1 : AddCommGroup E] →
              [inst_2 : Module 𝕜 E] →
                [inst_3 : NormedField 𝕜₂] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module 𝕜₂ F] →
                      {σ₁₂ : 𝕜 →+* 𝕜₂} →
                        [RingHomIsometric σ₁₂] → SeminormFamily 𝕜₂ F ι → (E →ₛₗ[σ₁₂] F) → SeminormFamily 𝕜 E ι
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The variance of a real Gaussian distribution `gaussianReal μ v` is
its variance parameter `v`.  -/
ProbabilityTheory.variance_fun_id_gaussianReal : ∀ {μ : ℝ} {v : NNReal}, ProbabilityTheory.variance (fun x => x) (ProbabilityTheory.gaussianReal μ v) = ↑v
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.tensorHom_app_apply : ∀ {K K' L L' : SSet} (f : K ⟶ K') (g : L ⟶ L') {Δ : SimplexCategoryᵒᵖ}
  (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj K L).obj Δ),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (f.app Δ) (g.app Δ))) x =
    ((CategoryTheory.ConcreteCategory.hom (f.app Δ)) x.1, (CategoryTheory.ConcreteCategory.hom (g.app Δ)) x.2)
-- Mathlib.Data.Seq.Defs
/-- Append two sequences. If `s₁` is infinite, then `s₁ ++ s₂ = s₁`,
otherwise it puts `s₂` at the location of the `nil` in `s₁`.  -/
Stream'.Seq.append : {α : Type u} → Stream'.Seq α → Stream'.Seq α → Stream'.Seq α
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function is analytic on a set `s`, so is its Fréchet derivative.  -/
AnalyticAt.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}
  [CompleteSpace F], AnalyticAt 𝕜 f x → AnalyticAt 𝕜 (fderiv 𝕜 f) x
-- Mathlib.Topology.Order.IntermediateValue
Continuous.strictMono_of_inj_boundedOrder' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  [BoundedOrder α] {f : α → δ}, Continuous f → Function.Injective f → StrictMono f ∨ StrictAnti f
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.add_apply : ∀ {A : Type u_2} {E : Type u_6} [inst : AddMonoid A] [inst_1 : TopologicalSpace A] [inst_2 : AddCommMonoid E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] (f g : A →ₜ+ E) (a : A), (f + g) a = f a + g a
-- Mathlib.Order.Concept
/-- The concept generated from the lower polar of a set, i.e. the smallest concept whose set of
attributes is contained in `t`.  -/
Concept.ofAttributes : {α : Type u_2} → {β : Type u_3} → (r : α → β → Prop) → Set β → Concept α β r
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- If `X` is compactly generated, to prove that `f : X → Y` is continuous it is enough to show
that for every compact Hausdorff space `K` and every continuous map `g : K → X`,
`f ∘ g` is continuous.  -/
continuous_from_compactlyGeneratedSpace : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactlyGeneratedSpace X]
  (f : X → Y),
  (∀ (K : Type u) [inst_3 : TopologicalSpace K] [CompactSpace K] [T2Space K] (g : K → X),
      Continuous g → Continuous (f ∘ g)) →
    Continuous f
-- Lean.Elab.ConfigEval.Types
Lean.Elab.ConfigEval.EvalConfigItem.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (set : α → Lean.Elab.ConfigEval.ConfigItem → Lean.Elab.TermElabM α),
  sizeOf { set := set } = 1
-- Mathlib.Analysis.InnerProductSpace.PiL2
FiniteDimensional.orthonormalBasisSingleton.congr_simp : ∀ (ι : Type u_1) (𝕜 : Type u_3) [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : Unique ι] (h : Module.finrank 𝕜 E = 1) (v v_1 : E)
  (e_v : v = v_1) (hv : ‖v‖ = 1),
  FiniteDimensional.orthonormalBasisSingleton ι 𝕜 h v hv = FiniteDimensional.orthonormalBasisSingleton ι 𝕜 h v_1 ⋯
-- Mathlib.Topology.Algebra.Group.Basic
instContinuousNegAdditiveOfContinuousInv : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : Inv H] [ContinuousInv H], ContinuousNeg (Additive H)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- The chromatic number of a graph is the minimal number of colors needed to color it.
This is `⊤` (infinity) iff `G` isn't colorable with finitely many colors.

If `G` is colorable, then `ENat.toNat G.chromaticNumber` is the `ℕ`-valued chromatic number.  -/
SimpleGraph.chromaticNumber : {V : Type u} → SimpleGraph V → ℕ∞
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.isDenseSubsite_inverse_of_isCocontinuous : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D)
  [e.functor.IsCocontinuous J K] [e.inverse.IsCocontinuous K J], CategoryTheory.Functor.IsDenseSubsite K J e.inverse
-- Std.Data.HashMap.Raw
/-- Computes the intersection of the given hash maps. The result will only contain entries from the first map.

This function always merges the smaller map into the larger map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.HashMap.Raw.diff : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Std.HashMap.Raw α β → Std.HashMap.Raw α β → Std.HashMap.Raw α β
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- Formula for `IsLocalizedModule.map` when each localized module is a `LocalizedModule`.  -/
IsLocalizedModule.map_LocalizedModules : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} [inst_1 : AddCommMonoid M₀]
  [inst_2 : Module R M₀] {M₁ : Type u_7} [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (g : M₀ →ₗ[R] M₁) (m : M₀)
  (s : ↥S),
  ((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g)
      (LocalizedModule.mk m s) =
    LocalizedModule.mk (g m) s
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.lift_comp_neg_left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj B] (f : A ⟶ B) {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg)
        f)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.between_verts_isBipartiteWith : ∀ {n : ℕ} {G : SimpleGraph (Fin n)} {r t' : ℕ} (K : G.CompleteEquipartiteSubgraph r t'),
  (SimpleGraph.between (↑K.verts) (↑K.verts)ᶜ G).IsBipartiteWith ↑K.verts ↑K.vertsᶜ
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.instHasFiniteProductsFullSubcategoryOfIsClosedUnderFiniteProducts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.Limits.HasFiniteProducts C] [P.IsClosedUnderFiniteProducts],
  CategoryTheory.Limits.HasFiniteProducts P.FullSubcategory
-- Init.Syntax
/-- Updates the argument list without changing the node kind.
Does nothing for non-`node` nodes.
 -/
Lean.Syntax.setArgs : Lean.Syntax → Array Lean.Syntax → Lean.Syntax
-- Lean.Parser.Term
Lean.Parser.Term.whereDecls : Lean.Parser.Parser
-- Mathlib.Data.Multiset.Filter
Multiset.filterMap_cons_none : ∀ {α : Type u_1} {β : Type v} {f : α → Option β} (a : α) (s : Multiset α),
  f a = none → Multiset.filterMap f (a ::ₘ s) = Multiset.filterMap f s