mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.initial_isIso_to : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] {A : C} (f : A ⟶ ⊥_ C), CategoryTheory.IsIso f
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
SSet.opEquivalence_functor : SSet.opEquivalence.functor = SSet.opFunctor
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
/-- The natural isomorphism `HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh ≅ Q`.  -/
DerivedCategory.quotientCompQhIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).comp DerivedCategory.Qh ≅ DerivedCategory.Q
-- Mathlib.Data.Multiset.ZeroCons
Multiset.mem_cons_self : ∀ {α : Type u_1} (a : α) (s : Multiset α), a ∈ a ::ₘ s
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.locallyConstantIsoFinYoneda.eq_1 : ∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)),
  LightCondensed.locallyConstantIsoFinYoneda F =
    CategoryTheory.NatIso.ofComponents
      (fun Y =>
        { hom := TypeCat.ofHom fun f => f.toFun, inv := TypeCat.ofHom fun f => { toFun := f, isLocallyConstant := ⋯ },
          hom_inv_id := ⋯, inv_hom_id := ⋯ })
      ⋯
-- Mathlib.AlgebraicGeometry.Gluing
/-- (Implementation detail)
The cocone associated to a locally directed diagram is a colimit.

One usually does not want to use this directly, and instead use the generic `colimit` API.
 -/
AlgebraicGeometry.Scheme.IsLocallyDirected.isColimit : {J : Type w} →
  [inst : CategoryTheory.Category.{v, w} J] →
    (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) →
      [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] →
        [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] →
          [inst_3 : Quiver.IsThin J] →
            [inst_4 : Small.{u, w} J] →
              CategoryTheory.Limits.IsColimit (AlgebraicGeometry.Scheme.IsLocallyDirected.cocone F)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_congr : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] {f g : MeasureTheory.SimpleFunc α E},
  MeasureTheory.Integrable (⇑f) μ →
    ⇑f =ᵐ[μ] ⇑g → MeasureTheory.SimpleFunc.integral μ f = MeasureTheory.SimpleFunc.integral μ g
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toArray_roo : ∀ {m n k : ℕ}, Array.map (fun x => x + k) (m<...n).toArray = ((m + k)<...n + k).toArray
-- Batteries.Data.List.Lemmas
List.disjoint_cons_right : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁.Disjoint (a :: l₂) ↔ a ∉ l₁ ∧ l₁.Disjoint l₂
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.coe_transpose : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (A : Matrix.SpecialLinearGroup n R), ↑A.transpose = (↑A).transpose
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
/-- The predicate satisfied by all objects in this subcategory  -/
CategoryTheory.ObjectProperty.FullSubcategory.property : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C}
  (self : P.FullSubcategory), P self.obj
-- Mathlib.LinearAlgebra.Determinant
Matrix.det_map : ∀ {K : Type u_5} {m : Type u_6} {n : Type u_7} [inst : Field K] [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] {F : Type u_8} [inst_5 : EquivLike F (Matrix m m K) (Matrix n n K)]
  [AlgEquivClass F K (Matrix m m K) (Matrix n n K)] (f : F) (x : Matrix m m K), (f x).det = x.det
-- Plausible.Testable
Plausible.TestResult.success.inj : ∀ {p : Prop} {a a_1 : Unit ⊕' p}, Plausible.TestResult.success a = Plausible.TestResult.success a_1 → a = a_1
-- Lean.Parser.Term.Basic
_private.Lean.Parser.Term.Basic.0.Lean.Parser.Term.binderDefaultM : Lean.Parser.Parser
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.integral_klFun_rnDeriv : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
      ∫ (x : α), InformationTheory.klFun (μ.rnDeriv ν x).toReal ∂ν =
        ∫ (x : α), MeasureTheory.llr μ ν x ∂μ + ν.real Set.univ - μ.real Set.univ
-- Mathlib.LinearAlgebra.Dimension.Finrank
/-- Pushforwards of finite-dimensional submodules along a `LinearEquiv` have the same finrank.  -/
LinearEquiv.finrank_map_eq : ∀ {R : Type u} {M : Type v} {N : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M ≃ₗ[R] N) (p : Submodule R M),
  Module.finrank R ↥(Submodule.map (↑f) p) = Module.finrank R ↥p
-- Batteries.Util.ProofWanted
/-- Wrapper recording that a `def_wanted` of type `α` has been declared.  -/
DefWanted : Sort u → Type
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Get the `j`th "projection" in the fan.
(Note that the initial letter of `proj` matches the greek letter in `Cone.π`.)  -/
CategoryTheory.Limits.Fan.proj : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] → {f : β → C} → (p : CategoryTheory.Limits.Fan f) → (j : β) → p.pt ⟶ f j
-- Mathlib.Algebra.Order.Hom.Basic
MulRingSeminormClass.toMonoidWithZeroHomClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : NonAssocRing α] [inst_1 : Semiring β]
  [inst_2 : PartialOrder β] [inst_3 : FunLike F α β] [self : MulRingSeminormClass F α β], MonoidWithZeroHomClass F α β
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.unitsEquivAut_apply : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : ContinuousMul R] (u : Rˣ) (x : R),
  ((ContinuousLinearEquiv.unitsEquivAut R) u) x = x * ↑u
-- Mathlib.ModelTheory.Order
FirstOrder.Language.realize_noBotOrder_iff : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : LE M]
  [L.OrderedStructure M], M ⊨ L.noBotOrderSentence ↔ NoBotOrder M
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor Iᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F] (i : I),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F).hom
      (CategoryTheory.Limits.limit.π (F.rightOp.comp CategoryTheory.coyoneda) i) =
    CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsAffine X]
  [AlgebraicGeometry.IsAffine Y] [AlgebraicGeometry.IsAffine Z],
  AlgebraicGeometry.IsAffine (CategoryTheory.Limits.pullback f g)
-- Mathlib.Topology.UniformSpace.Cauchy
CauchySeq.eq_1 : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : Preorder β] (u : β → α),
  CauchySeq u = Cauchy (Filter.map u Filter.atTop)
-- Mathlib.Geometry.Manifold.VectorField.Pullback
instIsManifoldMinSmoothnessOfNatWithTopENat_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 2) M],
  IsManifold I (minSmoothness 𝕜 1) M
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeries.eq_def : ∀ (G : Type u_1) [inst : Group G] (n : ℕ), Subgroup.upperCentralSeries G n = (Subgroup.upperCentralSeriesAux G n).fst
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.termι : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.cocone_ι : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }],
  (CategoryTheory.Limits.Sigma.cocone X).ι =
    CategoryTheory.Discrete.natTrans fun x => CategoryTheory.Limits.Sigma.ι (fun j => X.obj { as := j }) x.as
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getEntry.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (l : List ((a : α) × β a))
  (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getEntry a l h = (Std.Internal.List.getEntry? a l).get ⋯
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric
CStarAlgebra.norm_posPart_le : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : NormedSpace ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A]
  [inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A), ‖a⁺‖ ≤ ‖a‖
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.orthogonalProjection_apply : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p : P},
  (EuclideanGeometry.orthogonalProjection s) p =
    s.direction.orthogonalProjectionOnto (p -ᵥ ↑(Classical.arbitrary ↥s)) +ᵥ Classical.arbitrary ↥s
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_Ioi_cpow_iff : ∀ {s : ℂ} {t : ℝ}, 0 < t → (MeasureTheory.IntegrableOn (fun x => ↑x ^ s) (Set.Ioi t) MeasureTheory.volume ↔ s.re < -1)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instNonAssocRing : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] → [inst_1 : Monoid G] → [MulSemiringAction G k] → NonAssocRing (SkewMonoidAlgebra k G)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.chainTopCoeff_if_one_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} [inst_5 : Finite ι]
  [inst_6 : CharZero R] [inst_7 : IsDomain R] {i j : ι} [inst_8 : P.IsNotG2],
  P.root i - P.root j ∈ Set.range ⇑P.root → RootPairing.chainTopCoeff i j = if P.pairingIn ℤ i j = 0 then 1 else 0
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- Any continuous intertwining map is an intertwining map.  -/
ContIntertwiningMap.toIntertwiningMap : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} →
                                ContIntertwiningMap π₁ π₂ →
                                  (ContRepresentation.toRepresentation R G V π₁).IntertwiningMap
                                    (ContRepresentation.toRepresentation R G W π₂)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_eq_of_locallyRingedSpace_eq : ∀ {X Y : AlgebraicGeometry.Scheme}, X.toLocallyRingedSpace = Y.toLocallyRingedSpace → X = Y
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongrₗ_toAddEquiv : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [inst_5 : Semiring S]
  [inst_6 : Module S N] [inst_7 : SMulCommClass R S N] (σ : ι ≃ ι'),
  ↑(AlternatingMap.domDomCongrₗ S σ) = AlternatingMap.domDomCongrEquiv σ
-- Std.Data.HashMap.Lemmas
Std.HashMap.keys_filter_key : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {f : α → Bool},
  (Std.HashMap.filter (fun k x => f k) m).keys.Perm (List.filter f m.keys)
-- Mathlib.Analysis.Analytic.Constructions
formalMultilinearSeries_geometric_apply_norm_le : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  (n : ℕ), ‖formalMultilinearSeries_geometric 𝕜 A n‖ ≤ max 1 ‖1‖
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.getKey? (t.maxKey he) = some (t.maxKey he)
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the smallest element that is greater than or equal to the
given element, returning `fallback` if no such element exists.
 -/
Std.TreeSet.getGED : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → α → α
-- Std.Internal.UV.System
/-- Gets information about the system's CPUs.
 -/
Std.Internal.UV.System.cpuInfo : IO (Array Std.Internal.UV.System.CPUInfo)
-- Lean.Server.InfoUtils
Lean.Elab.HoverableInfoPrio.isHoverPosOnStop : Lean.Elab.HoverableInfoPrio → Bool
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.toList.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → t.toList = t_1.toList
-- Mathlib.Analysis.RCLike.Basic
RCLike.map_same_eq_id : ∀ {K : Type u_1} [inst : RCLike K], RCLike.map K K = ContinuousLinearMap.id ℝ K
-- Init.Grind.Ring.Field
/-- A field is a commutative ring with inverses for all non-zero elements.
 -/
Lean.Grind.Field : Type u → Type u
-- Init.Data.String.Basic
String.empty_append : ∀ {s : String}, "" ++ s = s
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.not_isReduced_alternatingWord : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) {m : ℕ},
  M.M i i' ≠ 0 → m > M.M i i' → ¬cs.IsReduced (CoxeterSystem.alternatingWord i i' m)
-- Mathlib.Algebra.Group.Center
Set.centralizer_union : ∀ {M : Type u_1} {S T : Set M} [inst : Mul M], (S ∪ T).centralizer = S.centralizer ∩ T.centralizer
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The `AddMonoidHom` from an `AddSubmonoid` to its image.
See `AddEquiv.AddSubmonoidMap` for a variant for `AddEquiv`s.  -/
AddMonoidHom.addSubmonoidMap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] → (f : M →+ N) → (M' : AddSubmonoid M) → ↥M' →+ ↥(AddSubmonoid.map f M')
-- Mathlib.Order.Filter.Extr
IsMaxOn.on_preimage : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} (g : δ → α) {b : δ},
  IsMaxOn f s (g b) → IsMaxOn (f ∘ g) (g ⁻¹' s) b
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.scalarTensorEquiv.eq_1 : ∀ (R : Type u_1) {M : Type u_2} (A : Type u_5) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : CommMonoid M],
  MonoidAlgebra.scalarTensorEquiv R A =
    (MonoidAlgebra.rTensorEquivAlgEquiv R A A R).trans (MonoidAlgebra.mapAlgEquiv A M (Algebra.TensorProduct.rid R A A))
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_real_self : ∀ {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (x : ℝ),
  ((ProbabilityTheory.covarianceBilin μ) x) x = x ^ 2 * ProbabilityTheory.variance id μ
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.sizeLt.inj : ∀ {lhs n lhs_1 n_1 : ℕ},
  Lean.Meta.Grind.EMatchTheoremConstraint.sizeLt lhs n = Lean.Meta.Grind.EMatchTheoremConstraint.sizeLt lhs_1 n_1 →
    lhs = lhs_1 ∧ n = n_1
-- Mathlib.Data.EReal.Inv
EReal.div_bot : ∀ {a : EReal}, a / ⊥ = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.ExtDTreeMap.ofList l cmp).getKey? k = none
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_natCast : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), { toFinsupp := ↑n } = ↑n
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.instToFormatGuessLexRel : Std.ToFormat Lean.Elab.WF.GuessLex.GuessLexRel
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.derived_le_lower_central`. -/
derived_le_lower_central : ∀ {G : Type u_1} [inst : Group G] (n : ℕ), derivedSeries G n ≤ ⊤.lowerCentralSeries n
-- Mathlib.Data.Set.Monotone
AntitoneOn.congr : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  AntitoneOn f₁ s → Set.EqOn f₁ f₂ s → AntitoneOn f₂ s
-- Mathlib.CategoryTheory.IsConnected
/-- An inductive-like property for the objects of a connected category.
If the set `p` is nonempty, and `p` is closed under morphisms of `J`,
then `p` contains all of `J`.

The converse is given in `IsConnected.of_induct`.
 -/
CategoryTheory.induct_on_objects : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected J] (p : Set J) {j₀ : J},
  j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint32.sizeOf_spec : ∀ (val : UInt32), sizeOf (Lean.Compiler.LCNF.LitValue.uint32 val) = 1 + sizeOf val
-- Mathlib.Order.Monotone.Monovary
monovaryOn_id_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder α] {f : ι → α} {s : Set ι} [inst_1 : PartialOrder ι],
  MonovaryOn f id s ↔ MonotoneOn f s
-- Mathlib.NumberTheory.HeckeRing.Defs
HeckeCosetModule.ext : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} {Z : Type u_3} [inst_1 : Zero Z]
  {f g : HeckeCosetModule Δ H₁ H₂ Z}, (∀ (D : HeckeCoset Δ H₁ H₂), f D = g D) → f = g
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.JointlyMono₂.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X₁ X₂ : C} {p₁ : R ⟶ X₁} {p₂ : R ⟶ X₂},
  (∀ ⦃Y : C⦄ (f g : Y ⟶ R),
      CategoryTheory.CategoryStruct.comp f p₁ = CategoryTheory.CategoryStruct.comp g p₁ →
        CategoryTheory.CategoryStruct.comp f p₂ = CategoryTheory.CategoryStruct.comp g p₂ → f = g) →
    CategoryTheory.JointlyMono₂ p₁ p₂
-- Mathlib.Data.Part
Part.mem_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {o : Part α} {a : α}, a ∈ o → f a ∈ Part.map f o
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The tensor product expressed as a functor.  -/
CategoryTheory.MonoidalCategory.tensor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → CategoryTheory.Functor (C × C) C
-- Mathlib.AlgebraicGeometry.SpreadingOut
AlgebraicGeometry.instIsGermInjectiveOfIsLocallyNoetherian : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X], X.IsGermInjective
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.contains_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (Std.DTreeMap.Const.insertMany t l).contains k = (t.contains k || (List.map Prod.fst l).contains k)
-- Mathlib.Order.LiminfLimsup
limsup_finset_sup' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α}
  {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty),
  autoParam (∀ i ∈ s, Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) limsup_finset_sup'._auto_1 →
    autoParam (∀ i ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) limsup_finset_sup'._auto_3 →
      Filter.limsup (fun a => s.sup' hs fun i => F i a) f = s.sup' hs fun i => Filter.limsup (F i) f
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- A typeclass describing the property that forming all finite disjoint unions is stable under the
property `P`.
 -/
CompHausLike.HasExplicitFiniteCoproducts : (TopCat → Prop) → Prop
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonMarkupContent.toJson : Lean.Lsp.MarkupContent → Lean.Json
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
/-- If `M` and `N` are submodules in an algebra `S` over `R`, there is the natural `R`-linear map
`M ⊗[R] N →ₗ[R] M * N` induced by multiplication in `S`,
which is surjective (`Submodule.mulMap'_surjective`).  -/
Submodule.mulMap' : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (M N : Submodule R S) → TensorProduct R ↥M ↥N →ₗ[R] ↥(M * N)
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.Const.modify.eq_1 : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] [inst_2 : Hashable α] {β : Type v}
  (m : Std.DHashMap.Raw α fun x => β) (a : α) (f : β → β),
  Std.DHashMap.Raw.Const.modify m a f =
    if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.Const.modify ⟨m, h⟩ a f) else ∅
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ColorInformation.mk.inj : ∀ {range : Lean.Lsp.Range} {color : Lean.Lsp.Color} {range_1 : Lean.Lsp.Range} {color_1 : Lean.Lsp.Color},
  { range := range, color := color } = { range := range_1, color := color_1 } → range = range_1 ∧ color = color_1
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- Given a fixed continuous linear map `g`, associating to a continuous multilinear map `f` the
continuous multilinear map `f (g m₁, ..., g mₙ)` is a bounded linear operation.  -/
isBoundedLinearMap_continuousMultilinearMap_comp_linear : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {ι : Type u_5} [inst_7 : Fintype ι]
  (g : G →L[𝕜] E), IsBoundedLinearMap 𝕜 fun f => f.compContinuousLinearMap fun x => g
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_id : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) (X : C),
  CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj data G₀ X)
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
/-- real numbers `0 < rIn < rOut`  -/
ContDiffBump.rIn : {E : Type u_1} → {c : E} → ContDiffBump c → ℝ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle is unchanged by replacing the first point with the midpoint of the segment
between the second point and that point.  -/
EuclideanGeometry.oangle_midpoint_rev_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₂ p₃ : P), EuclideanGeometry.oangle (midpoint ℝ p₂ p₁) p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃