mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_mul_union_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemigroup α] {s t : Finset α}, s ∩ t * (s ∪ t) ⊆ s * t
-- Init.Data.String.Lemmas.Pattern.Split.Basic
String.Slice.toList_split_eq_splitToSubslice : ∀ {ρ : Type} (pat : ρ) {σ : String.Slice → Type} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  [inst_1 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id] {s : String.Slice},
  (s.split pat).toList = List.map String.Slice.Subslice.toSlice (s.splitToSubslice pat).toList
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.instIsMulCommutative_closure : ∀ {G : Type u_1} [inst : Group G] {S : Type u_3} [inst_1 : SetLike S G] [inst_2 : MulMemClass S G] (s : S)
  [IsMulCommutative ↥s], IsMulCommutative ↥(Subgroup.closure ↑s)
-- Mathlib.Order.Directed
OrderDual.isDirected_ge : ∀ {α : Type u_1} [inst : LE α] [IsDirectedOrder α], IsCodirectedOrder αᵒᵈ
-- Mathlib.Algebra.PresentedMonoid.Basic
_private.Mathlib.Algebra.PresentedMonoid.Basic.0.PresentedMonoid.termP₃ : Lean.ParserDescr
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K K_1 : HomologicalComplex C c),
  K = K_1 → ∀ (e e_1 : c.Embedding c'), e = e_1 → K.extend e = K_1.extend e_1
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.finite_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.IsFinite f] (U : Y.Opens),
  AlgebraicGeometry.IsAffineOpen U → (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)).Finite
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiff.sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {ι : Type u_3} {f : ι → E → F} {s : Finset ι},
  (∀ i ∈ s, ContDiff 𝕜 n fun x => f i x) → ContDiff 𝕜 n fun x => ∑ i ∈ s, f i x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β},
  m.WF →
    Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.Const.modify m k f) k' fallback =
      if (k == k') = true then (Option.map f (Std.DHashMap.Raw.Const.get? m k)).getD fallback
      else Std.DHashMap.Raw.Const.getD m k' fallback
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyRel.refl_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)) (S : Set X)
  (x : ↑unitInterval × X), (ContinuousMap.HomotopyRel.refl f S) x = f x.2
-- Std.Time.Date.Basic
/-- Convert `Millisecond.Offset` into `Week.Offset`.
 -/
Std.Time.Millisecond.Offset.toWeeks : Std.Time.Millisecond.Offset → Std.Time.Week.Offset
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.instOrderBot.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] {x : CompleteLattice β},
  sSupHom.instOrderBot = { toBot := sSupHom.instBot, bot_le := ⋯ }
-- Mathlib.Analysis.Complex.JensenFormula
_private.Mathlib.Analysis.Complex.JensenFormula.0.const_mul_norm_sub_circleMap_le_norm_sub_circleMap : ∀ {r₀ r R : ℝ} {ρ : ℂ},
  ‖ρ‖ = R → 0 < r₀ → 0 < R → r₀ ≤ r → r ≤ R → ∀ (θ : ℝ), √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
-- Lean.Parser.Term
/-- `+usedOnly` causes unused `let`s bindings to be eliminated.
 -/
Lean.Parser.Term.letOptUsedOnly : Lean.Parser.Parser
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.colimitCocone_ι_app_base : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) (j : J),
  ((AlgebraicGeometry.PresheafedSpace.colimitCocone F).ι.app j).base =
    CategoryTheory.Limits.colimit.ι (F.comp (AlgebraicGeometry.PresheafedSpace.forget C)) j
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.ofCocone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} (t : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.PushoutCocone.ofCocone t).pt = t.pt
-- Mathlib.CategoryTheory.Localization.Predicate
/-- The functor `(D ⥤ E) ⥤ (C ⥤ E)` given by the composition with a localization
functor `L : C ⥤ D` with respect to `W : MorphismProperty C`.  -/
CategoryTheory.Localization.whiskeringLeftFunctor' : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [L.IsLocalization W] →
              (E : Type u_4) →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} E] →
                  CategoryTheory.Functor (CategoryTheory.Functor D E) (CategoryTheory.Functor C E)
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.toDigitsCore.eq_1 : ∀ (base x : ℕ) (x_1 : List Char), base.toDigitsCore 0 x x_1 = x_1
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.limit_ext'_iff : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F' : CategoryTheory.Functor J (Type v)}
  {x y : CategoryTheory.Limits.limit F'},
  x = y ↔
    ∀ (j : J),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) x =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j)) y
-- Batteries.Data.Fin.Lemmas
Fin.countP.eq_1 : ∀ {n : ℕ} (p : Fin n → Bool), Fin.countP p = Fin.sum fun x => (p x).toNat
-- Mathlib.Computability.Encoding
/-- Deprecated alias for `encodingNatBool`.  -/
Computability.finEncodingNatBool : Computability.Encoding ℕ Bool
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Functor.IsRightAdjoint.rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor Cᵒᵖ D} [F.IsRightAdjoint], F.rightOp.IsLeftAdjoint
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.congr_symm_apply_right : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂)
  (h : ∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))) (x : N₂ ⋊[φ₂] G₂),
  ((SemidirectProduct.congr fn fg h).symm x).right = fg.symm x.right
-- Mathlib.Control.ULiftable
/-- for specific continuation passing monads, this function helps to create a uliftable instance  -/
ContT.uliftable' : {r : Type u_1} →
  {r' : Type u_2} →
    {m : Type u_1 → Type u_5} →
      {m' : Type u_2 → Type u_6} → [ULiftable m m'] → r ≃ r' → ULiftable (ContT r m) (ContT r' m')
-- Mathlib.Data.Finset.Image
Finset.image_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β},
  Function.Injective f → Function.Injective (Finset.image f)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getGTD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.Equiv t₂ → t₁.getGTD k fallback = t₂.getGTD k fallback
-- Mathlib.Topology.MetricSpace.Thickening
Metric.mem_nhdsSet_iff : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {s t : Set α},
  IsCompact s → (t ∈ nhdsSet s ↔ ∃ ε > 0, Metric.thickening ε s ⊆ t)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- action on 1-morphisms  -/
CategoryTheory.StrictlyUnitaryPseudofunctorCore.map : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (self : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) → {X Y : B} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAt_iff_tendsto : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
  HasDerivAt f f' x ↔ Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - (x' - x) • f'‖) (nhds x) (nhds 0)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
_private.Mathlib.LinearAlgebra.CliffordAlgebra.Contraction.0.CliffordAlgebra.«term_⌊_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.map_eq_comap : ∀ {α : Type u_2} {β : Type u_3} {x : MeasurableSpace α} {x_1 : MeasurableSpace β} {f : α → β} {g : β → α}
  {μ : MeasureTheory.Measure α},
  Measurable f →
    MeasurableEmbedding g →
      (∀ᵐ (a : α) ∂μ, a ∈ Set.range g) →
        (∀ (a : β), f (g a) = a) → MeasureTheory.Measure.map f μ = MeasureTheory.Measure.comap g μ
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.prod_inf_prod : ∀ {k : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddTorsor W Q] (s₁ s₂ : AffineSubspace k P) (t₁ t₂ : AffineSubspace k Q),
  s₁.prod t₁ ⊓ s₂.prod t₂ = (s₁ ⊓ s₂).prod (t₁ ⊓ t₂)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.addHom_ext'_iff : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {N : Type u_3} [inst_1 : AddZeroClass N]
  {f g : SkewMonoidAlgebra k G →+ N},
  f = g ↔ ∀ (x : G), f.comp (SkewMonoidAlgebra.singleAddHom x) = g.comp (SkewMonoidAlgebra.singleAddHom x)
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.mul_ev : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} (γ₁ γ₂ : CategoryTheory.PresheafOfGroups.OneCochain G U) (i j : I) {T : C} (a : T ⟶ U i) (b : T ⟶ U j),
  (γ₁ * γ₂).ev i j a b = γ₁.ev i j a b * γ₂.ev i j a b
-- Mathlib.Data.Finset.Union
Finset.disjiUnion_filter_eq_of_maps_to : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β},
  (∀ x ∈ s, f x ∈ t) → t.disjiUnion (fun a => {x ∈ s | f x = a}) ⋯ = s
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.associator_hom_iso : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c d : CategoryTheory.Bicategory.Pith B} (x : a ⟶ b)
  (y : b ⟶ c) (z : c ⟶ d),
  (CategoryTheory.Bicategory.associator x y z).hom.iso = CategoryTheory.Bicategory.associator x.of y.of z.of
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsion'.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_3)
  [inst_3 : CommMonoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M],
  Submodule.torsion' R M S = { carrier := {x | ∃ a, a • x = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Mathlib.Order.Concept
Order.isExtent_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α}, Order.IsExtent r s ↔ lowerPolar r (upperPolar r s) = s
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.Hom.Simps.hom.eq_1 : ∀ (X Y : AddMonCat) (f : X.Hom Y), AddMonCat.Hom.Simps.hom X Y f = f.hom
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.prod_finset_product_right : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] (r : Finset (α × γ)) (s : Finset γ)
  (t : γ → Finset α),
  (∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) → ∀ {f : α × γ → β}, ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (a, c)
-- Mathlib.Order.SuccPred.Limit
Order.not_isSuccLimit_of_isSuccArchimedean : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α], ¬Order.IsSuccLimit a
-- Lean.Server.Completion.CompletionInfoSelection
Lean.Server.Completion.findCompletionInfosAt : Lean.FileMap →
  String.Pos.Raw → Lean.Syntax → Lean.Elab.InfoTree → Array Lean.Server.Completion.ContextualizedCompletionInfo × Bool
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.inner_condExpL2_eq_inner_fun : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (hm : m ≤ m0) (f g : ↥(MeasureTheory.Lp E 2 μ)),
  MeasureTheory.AEStronglyMeasurable (↑↑g) μ → inner 𝕜 (↑((MeasureTheory.condExpL2 E 𝕜 hm) f)) g = inner 𝕜 f g
-- Mathlib.Data.Prod.Lex
/-- See also `monotone_fst_ofLex` for a version stated in terms of `Monotone`.  -/
Prod.Lex.monotone_fst : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : LE β] (t c : Lex (α × β)),
  t ≤ c → (ofLex t).1 ≤ (ofLex c).1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_maxKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false → Std.Internal.List.getKey? (Std.Internal.List.maxKey! l) l = some (Std.Internal.List.maxKey! l)
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.ofFunction_caratheodory : ∀ {α : Type u_1} {m : Set α → ENNReal} {s : Set α} {h₀ : m ∅ = 0},
  (∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t) → MeasurableSet s
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.pos_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {x : R}, 0 < v₁ x ↔ 0 < v₂ x
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.unzeroD_eq_unzeroD_iff : ∀ {α : Type u} {d : α} {x y : WithZero α},
  WithZero.unzeroD d x = WithZero.unzeroD d y ↔ x = y ∨ x = ↑d ∧ y = 0 ∨ x = 0 ∧ y = ↑d
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalClosure.eq_1 : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Subgroup.normalClosure s = Subgroup.closure (Group.conjugatesOfSet s)
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.linearEquivAt_apply : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] (b : B)
  (hb : b ∈ e.baseSet) (v : E b), (Bundle.Trivialization.linearEquivAt R e b hb) v = (↑e ⟨b, v⟩).2
-- Init.GrindInstances.ToInt
Lean.Grind.instModIntIi : Lean.Grind.ToInt.Mod ℤ Lean.Grind.IntInterval.ii
-- Mathlib.Data.Sym.Basic
Sym.eq_replicate_of_subsingleton : ∀ {α : Type u_1} [Subsingleton α] (a : α) {n : ℕ} (s : Sym α n), s = Sym.replicate n a
-- Mathlib.Algebra.BigOperators.Finprod
/-- The product of `f y` over `y ∈ Set.range g` equals the product of `f (g i)` over all `i`
provided that `g` is injective on `mulSupport (f ∘ g)`.  -/
finprod_mem_range' : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {g : β → α},
  Set.InjOn g (Function.mulSupport (f ∘ g)) → ∏ᶠ (i : α) (_ : i ∈ Set.range g), f i = ∏ᶠ (j : β), f (g j)
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.hg : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (self : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  Algebra.Generators.PresentationOfFreeCotangent.Aux.g✝ self • P.ker ≤
    Ideal.span (Set.range (Subtype.val ∘ Algebra.Generators.PresentationOfFreeCotangent.Aux.f✝ self ∘ ⇑b))
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.forget_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C C)
  {X Y : CategoryTheory.Endofunctor.Coalgebra F} (f : X ⟶ Y),
  (CategoryTheory.Endofunctor.Coalgebra.forget F).map f = f.f
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.rTensorEquivAlgEquiv.invFun_tmul : ∀ {R : Type u_1} {M : Type u_2} {S : Type u_4} {A : Type u_5} {B : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A]
  [inst_9 : CommMonoid M] (a : A) (m : M) (b : B),
  MonoidAlgebra.rTensorEquivAlgEquiv.invFun (MonoidAlgebra.single m (a ⊗ₜ[R] b)) = a ⊗ₜ[R] MonoidAlgebra.single m b
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.LocallyRingedSpace.GlueData.mk.injEq : ∀ (toGlueData : CategoryTheory.GlueData AlgebraicGeometry.LocallyRingedSpace)
  (f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (toGlueData.f i j))
  (toGlueData_1 : CategoryTheory.GlueData AlgebraicGeometry.LocallyRingedSpace)
  (f_open_1 : ∀ (i j : toGlueData_1.J), AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (toGlueData_1.f i j)),
  ({ toGlueData := toGlueData, f_open := f_open } = { toGlueData := toGlueData_1, f_open := f_open_1 }) =
    (toGlueData = toGlueData_1)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The "derivative" of a multilinear map, as a linear map from `(i : ι) → M₁ i` to `M₂`.
For continuous multilinear maps, this will indeed be the derivative.  -/
MultilinearMap.linearDeriv : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [DecidableEq ι] → [Fintype ι] → MultilinearMap R M₁ M₂ → ((i : ι) → M₁ i) → ((i : ι) → M₁ i) →ₗ[R] M₂
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.lt_extend : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M} (hx : x ∉ (↑f).domain), f < f.extend hx
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.union_insert_right_equiv_union_insert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {p : (a : α) × β a},
  m₁.WF → m₂.WF → (m₁ ∪ m₂.insert p.fst p.snd).Equiv ((m₁ ∪ m₂).insert p.fst p.snd)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_finsetSum_vectorMeasure : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f : X → E} {B : E →L[ℝ] F →L[ℝ] G}
  {μ : ι → MeasureTheory.VectorMeasure X F} {s : Finset ι},
  (∀ i ∈ s, (μ i).Integrable f) → ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
-- Std.Do.SPred.SVal
/-- Curries a function taking a `StateTuple` into an `SVal`.  -/
Std.Do.SVal.curry : {α : Type u} → {σs : List (Type u)} → (Std.Do.SVal.StateTuple σs → α) → Std.Do.SVal σs α
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c)
  [inst_2 : CategoryTheory.Bicategory.LanLift.CommuteWith f g h],
  (CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso f g h).inv =
    (CategoryTheory.Bicategory.LanLift.CommuteWith.isKan f g h).desc
      (CategoryTheory.Bicategory.lanLiftLeftLift f (CategoryTheory.CategoryStruct.comp h g))
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_mono_ae : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E]
  [ClosedIciTopology E] {f g : α → E},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → f ≤ᵐ[μ] g → ∫ (x : α), f x ∂μ ≤ ∫ (x : α), g x ∂μ
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.lift_unique : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : M →ₗ[R] A} (h : IsSymmetricAlgebra f) {A' : Type u_4}
  [inst_5 : CommSemiring A'] [inst_6 : Algebra R A'] {g : M →ₗ[R] A'} {F : A →ₐ[R] A'}, ↑F ∘ₗ f = g → F = h.lift g
-- Lean.Data.DeclarationRange
Lean.DeclarationRange.mk.injEq : ∀ (pos : Lean.Position) (charUtf16 : ℕ) (endPos : Lean.Position) (endCharUtf16 : ℕ) (pos_1 : Lean.Position)
  (charUtf16_1 : ℕ) (endPos_1 : Lean.Position) (endCharUtf16_1 : ℕ),
  ({ pos := pos, charUtf16 := charUtf16, endPos := endPos, endCharUtf16 := endCharUtf16 } =
      { pos := pos_1, charUtf16 := charUtf16_1, endPos := endPos_1, endCharUtf16 := endCharUtf16_1 }) =
    (pos = pos_1 ∧ charUtf16 = charUtf16_1 ∧ endPos = endPos_1 ∧ endCharUtf16 = endCharUtf16_1)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_monomial_subset : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) {a : R}, ((SkewPolynomial.monomial n) a).support ⊆ {n}
-- Mathlib.Data.Set.Lattice
Set.insert_iUnion : ∀ {β : Type u_2} {ι : Sort u_5} [Nonempty ι] (x : β) (t : ι → Set β), insert x (⋃ i, t i) = ⋃ i, insert x (t i)
-- Mathlib.Order.CompleteLattice.Basic
iInf_true : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : True → α}, iInf s = s trivial
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.instZeroHom : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → (X Y : HomologicalComplex V c) → Zero (X ⟶ Y)
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.smul_set_sdiff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {s t : Set β} {a : α},
  a ≠ 0 → a • (s \ t) = a • s \ a • t