mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
  (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [inst_2 : CategoryTheory.Limits.HasPullback i₁ i₂],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f)
        (CategoryTheory.Limits.pullback.map
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f
          (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
          (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst i₁ i₂)
      (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
hasProd_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β},
  ¬L.NeBot → ∀ (f : β → α) (a : α), HasProd f a L
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_inf_le : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H K : AddSubgroup G) (f : G →+ N),
  AddSubgroup.map f (H ⊓ K) ≤ AddSubgroup.map f H ⊓ AddSubgroup.map f K
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.matchesAt_iff_exists_isLongestMatchAt : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt pat pos ↔ ∃ endPos, String.Slice.Pattern.Model.IsLongestMatchAt pat pos endPos
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_lt_beth_ofNat : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Cardinal.lift.{v, u} c < Cardinal.beth (OfNat.ofNat n) ↔ c < Cardinal.beth (OfNat.ofNat n)
-- Mathlib.Order.RelIso.Basic
/-- For a `β`-relation `r`, an equivalence `f : α ≃ β` induces a relation isomorphism from
`r.onFun f` to `r`.  -/
RelIso.ofOnFun : {α : Type u_1} → {β : Type u_2} → (r : β → β → Prop) → (f : α ≃ β) → Function.onFun r ⇑f ≃r r
-- Mathlib.Topology.Algebra.ConstMulAction
ProperlyDiscontinuousSMul.finite_stabilizer : ∀ {Γ : Type u_4} [inst : Group Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : MulAction Γ T]
  [ProperlyDiscontinuousSMul Γ T] (x : T), (↑(MulAction.stabilizer Γ x)).Finite
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_inter_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iio a ∩ Set.Iio b = Set.Iio (min a b)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (σ : Gal(K/ℚ)) {x : K},
  x ^ n = 1 → σ x = x ^ (↑((IsCyclotomicExtension.Rat.galEquivZMod n K) σ)).val
-- Std.Internal.Parsec.Basic
/-- Interface for an input iterator with position tracking and lookahead support.
 -/
Std.Internal.Parsec.Input : Type → (elem idx : outParam Type) → [DecidableEq idx] → [DecidableEq elem] → Type
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCocone_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F), (H.mapCocone c).pt = H.obj c.pt
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instCommSemiring : {σ : Type u_1} → {R : Type u_2} → [CommSemiring R] → CommSemiring (MvPowerSeries σ R)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- If a short complex `S` in a balanced category is exact and such that `S.f` is a mono,
then a morphism `k : A ⟶ S.X₂` such that `k ≫ S.g = 0` lifts to a morphism `A ⟶ S.X₁`.  -/
CategoryTheory.ShortComplex.Exact.lift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} →
        [CategoryTheory.Balanced C] →
          S.Exact →
            {A : C} →
              (k : A ⟶ S.X₂) → CategoryTheory.CategoryStruct.comp k S.g = 0 → [CategoryTheory.Mono S.f] → A ⟶ S.X₁
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- The canonical map from the type to the additive free group is an injection.  -/
FreeAddGroup.of_injective : ∀ {α : Type u}, Function.Injective FreeAddGroup.of
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.inv_nonneg_iff : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a : R}, 0 ≤ a⁻¹ ↔ 0 ≤ a
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.instAddCancelMonoid : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddCancelMonoid α] → AddCancelMonoid (Matrix m n α)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.instDecidableEvalLiteral : {α : Type u_1} →
  (p : α → Bool) → (l : Std.Sat.Literal α) → Decidable (Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p l)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.refl : ∀ {α : Type u} (m : Std.HashSet.Raw α), m.Equiv m
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.hom_ext_nonempty_iff : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [inst : Monoid K] [inst_1 : (i : ι) → Monoid (G i)]
  [inst_2 : Monoid H] {φ : (i : ι) → H →* G i} [hn : Nonempty ι] {f g : Monoid.PushoutI φ →* K},
  f = g ↔ ∀ (i : ι), f.comp (Monoid.PushoutI.of i) = g.comp (Monoid.PushoutI.of i)
-- Mathlib.Topology.Order
coinduced_sSup : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (TopologicalSpace α)},
  TopologicalSpace.coinduced f (sSup s) = sSup (TopologicalSpace.coinduced f '' s)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isOpenEmbedding_toCompacts : ∀ {α : Type u_1} [inst : TopologicalSpace α], Topology.IsOpenEmbedding TopologicalSpace.NonemptyCompacts.toCompacts
-- Lean.Meta.Tactic.Constructor
Lean.MVarId.existsIntro : Lean.MVarId → Lean.Expr → Lean.MetaM Lean.MVarId
-- Mathlib.Topology.Compactness.Compact
isCompact_range : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace X] {f : X → Y},
  Continuous f → IsCompact (Set.range f)
-- Mathlib.NumberTheory.Cyclotomic.Basic
instInhabitedCyclotomicRing : (n : ℕ) →
  (A : Type u_2) →
    (K : Type u_1) →
      [inst : CommRing A] → [inst_1 : Field K] → [inst_2 : Algebra A K] → Inhabited (CyclotomicRing n A K)
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.containsKey a (Std.Internal.List.insertEntryIfNew k v l) =
    (k == a || Std.Internal.List.containsKey a l)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The orthogonal complement of the closure of a submodule (as a `Submodule`) is equal to
the orthogonal complement.  -/
ClosedSubmodule.orthogonal_closure : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E), (↑K.closure)ᗮ = Kᗮ
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
/-- An element of `contDiffGroupoid n I` is `C^n`.  -/
contMDiffOn_of_mem_contDiffGroupoid : ∀ {𝕜 : 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} {n : WithTop ℕ∞}
  {e' : OpenPartialHomeomorph H H}, e' ∈ contDiffGroupoid n I → ContMDiffOn I I n (↑e') e'.source
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.instLE : {ι : Type u_1} → LE (AbstractSimplicialComplex ι)
-- Mathlib.Data.Set.Function
Set.SurjOn.mono : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
  s₁ ⊆ s₂ → t₁ ⊆ t₂ → Set.SurjOn f s₁ t₂ → Set.SurjOn f s₂ t₁
-- Init.Data.Array.Find
Array.findFinIdx?_eq_bind_find?_finIdxOf? : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool},
  Array.findFinIdx? p xs = (Array.find? p xs).bind fun x => xs.finIdxOf? x
-- Init.Core
/-- `x ≈ y` says that `x` and `y` are equivalent. Because this is a typeclass,
the notion of equivalence is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `≈` in identifiers is `equiv`. -/
HasEquiv.Equiv : {α : Sort u} → [self : HasEquiv α] → α → α → Sort v
-- Mathlib.Order.Circular
/-- The order of the `↔` has been chosen so that `rw [sbtw_cyclic]` cycles to the right while
`rw [← sbtw_cyclic]` cycles to the left (thus following the prepended arrow).  -/
sbtw_cyclic : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c ↔ sbtw c a b
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.preimage_ball : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (x : β) (r : ℝ),
  ⇑h ⁻¹' Metric.ball x r = Metric.ball (h.symm x) r
-- Init.Data.Option.Lemmas
Option.all_bind : ∀ {β : Type u_1} {α : Type u_2} {p : β → Bool} {f : α → Option β} {o : Option α},
  Option.all p (o.bind f) = Option.all (Option.all p ∘ f) o
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.nontrivial_iff_ne_bot : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p : Submodule R M}, Nontrivial ↥p ↔ p ≠ ⊥
-- Mathlib.Topology.Constructions.SumProd
isOpenMap_inr : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsOpenMap Sum.inr
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instHashableCanonArgKey.hash : Lean.Meta.Grind.CanonArgKey → UInt64
-- Mathlib.Order.BoundedOrder.Basic
/-- **Alias** of the forward direction of `isMax_iff_eq_top`. -/
IsMax.eq_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, IsMax a → a = ⊤
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.hasForgetToAddMonCat.eq_1 : AddCommMonCat.hasForgetToAddMonCat =
  {
    forget₂ :=
      { obj := fun R => AddMonCat.of ↑R, map := fun {X Y} f => AddMonCat.ofHom (AddCommMonCat.Hom.hom f),
        map_id := AddCommMonCat.hasForgetToAddMonCat._proof_1,
        map_comp := @AddCommMonCat.hasForgetToAddMonCat._proof_2 },
    forget_comp := AddCommMonCat.hasForgetToAddMonCat._proof_4 }
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_whisker_left_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) (X : ↑(self.obj a)),
  (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((self.mapComp f g).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X))
        ((self.mapComp f h).inv.toNatTrans.app X))
-- Mathlib.RingTheory.HahnSeries.Binomial
/-- A summable family of Hahn series, whose `n`th term is `Ring.choose r n • (x - 1) ^ n` when
`x` is close to `1` (more precisely, when `0 < (x - 1).orderTop`), and `0 ^ n` otherwise. These
terms give a formal expansion of `x ^ r` as `(1 + (x - 1)) ^ r`.  -/
HahnSeries.SummableFamily.binomialFamily : {Γ : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : LinearOrder Γ] →
        [inst_1 : AddCommMonoid Γ] →
          [IsOrderedCancelAddMonoid Γ] →
            [inst_3 : CommRing R] →
              [BinomialRing R] →
                [inst_5 : CommRing A] → [Algebra R A] → HahnSeries Γ A → R → HahnSeries.SummableFamily Γ A ℕ
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- `WithLp.fst` as a linear map.  -/
WithLp.fstₗ : (p : ENNReal) →
  (𝕜 : Type u_1) →
    (α : Type u_2) →
      (β : Type u_3) →
        [inst : Semiring 𝕜] →
          [inst_1 : AddCommGroup α] →
            [inst_2 : AddCommGroup β] → [inst_3 : Module 𝕜 α] → [inst_4 : Module 𝕜 β] → WithLp p (α × β) →ₗ[𝕜] α
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Additive subsemigroups of an additive semigroup `Additive M` are isomorphic to subsemigroups
of `M`.  -/
AddSubsemigroup.toSubsemigroup' : {M : Type u_1} → [inst : Mul M] → AddSubsemigroup (Additive M) ≃o Subsemigroup M
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_C : ∀ {R : Type u_1} [inst : Semiring R] (k : ℕ) (r : R), 0 < k → (Polynomial.hasseDeriv k) (Polynomial.C r) = 0
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The left Kan lift of `g` along `f` at the level of structured arrows.  -/
CategoryTheory.Bicategory.lanLiftLeftLift : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : b ⟶ a) →
        (g : c ⟶ a) → [CategoryTheory.Bicategory.HasLeftKanLift f g] → CategoryTheory.Bicategory.LeftLift f g
-- Init.Sym.Lemmas
Lean.Sym.Int64.le_eq_false : ∀ (a b : Int64), decide (a ≤ b) = false → (a ≤ b) = False
-- Mathlib.Algebra.MonoidAlgebra.Division
/-- **Alias** of `AddMonoidAlgebra.coeff_modOf_self_add`. -/
AddMonoidAlgebra.modOf_apply_self_add : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] (x : AddMonoidAlgebra k G) (g d : G),
  (x.modOf g).coeff (g + d) = 0
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.ballSubgroup.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] (c : MulArchimedeanClass M),
  c.ballSubgroup = MulArchimedeanClass.subgroup (UpperSet.Ioi c)
-- Mathlib.Analysis.Calculus.FDeriv.Norm
HasStrictFDerivAt.hasStrictDerivAt_norm_smul_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : StrongDual ℝ E} {x : E} {t : ℝ},
  0 < t → HasStrictFDerivAt (fun x => ‖x‖) f x → HasStrictFDerivAt (fun x => ‖x‖) f (t • x)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- Eta-expanded form of `differentiableWithinAt_id` -/
differentiableWithinAt_fun_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 (fun x => x) s x
-- Std.Sync.StreamMap
_private.Std.Sync.StreamMap.0.Std.StreamMap.mk : {α β : Type} → Array (α × Std.Async.Selector β × IO Unit) → Std.StreamMap α β
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- Computing ind-lims in `Ind C` is the same as computing them in `Cᵒᵖ ⥤ Type v`.  -/
CategoryTheory.Ind.limCompInclusion : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type v} →
      [inst_1 : CategoryTheory.SmallCategory I] →
        [inst_2 : CategoryTheory.IsFiltered I] →
          (CategoryTheory.Ind.lim I).comp (CategoryTheory.Ind.inclusion C) ≅
            ((CategoryTheory.Functor.whiskeringRight I C (CategoryTheory.Functor Cᵒᵖ (Type v))).obj
                  CategoryTheory.yoneda).comp
              CategoryTheory.Limits.colim
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.equivalenceOfReindexing_inverse : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G),
  (CategoryTheory.Limits.Cone.equivalenceOfReindexing e α).inverse =
    (CategoryTheory.Limits.Cone.postcompose α.inv).comp
      ((CategoryTheory.Limits.Cone.whiskering e.inverse).comp
        (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom))
-- Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
measurable_smul_const : ∀ {α : Type u_1} [inst : MeasurableSpace α] {𝕜 : Type u_2} [inst_1 : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_3 : MeasurableSpace 𝕜] [BorelSpace 𝕜] {E : Type u_3} [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace 𝕜 E]
  [inst_7 : MeasurableSpace E] [BorelSpace E] {f : α → 𝕜} {c : E},
  c ≠ 0 → ((Measurable fun x => f x • c) ↔ Measurable f)
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.cylinder_eq_cylinder_of_le_firstDiff : ∀ {E : ℕ → Type u_1} (x y : (n : ℕ) → E n) {n : ℕ}, n ≤ PiNat.firstDiff x y → PiNat.cylinder x n = PiNat.cylinder y n
-- Mathlib.LinearAlgebra.Dimension.RankNullity
LinearMap.lift_rank_range_add_rank_ker : ∀ {R : Type u_1} {M : Type u} {M' : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
  [inst_3 : Module R M] [inst_4 : Module R M'] [HasRankNullity.{u, u_1} R] (f : M →ₗ[R] M'),
  Cardinal.lift.{u, v} (Module.rank R ↥f.range) + Cardinal.lift.{v, u} (Module.rank R ↥f.ker) =
    Cardinal.lift.{v, u} (Module.rank R M)
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.retractClosure_eq_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsStableUnderRetracts], P.retractClosure = P
-- Mathlib.Topology.Constructions.SumProd
/-- A version of `ContinuousAt.prodMap` that avoids `Prod.fst`/`Prod.snd`
by assuming that the point is `(x, y)`.  -/
ContinuousAt.prodMap' : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : X → Z} {g : Y → W} {x : X} {y : Y},
  ContinuousAt f x → ContinuousAt g y → ContinuousAt (Prod.map f g) (x, y)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_comap_map : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (S : L.Substructure M) {f : L.Hom M N},
  FirstOrder.Language.Substructure.map f
      (FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f S)) =
    FirstOrder.Language.Substructure.map f S
-- Mathlib.RingTheory.LocalRing.Quotient
IsLocalRing.finite_quotient_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R] [Finite (IsLocalRing.ResidueField R)]
  {I : Ideal R}, Finite (R ⧸ I) ↔ ∃ n, IsLocalRing.maximalIdeal R ^ n ≤ I
-- Mathlib.Order.SupClosed
latticeClosure_isClosed : ∀ {α : Type u_3} [inst : Lattice α] (s : Set α), latticeClosure.IsClosed s = IsSublattice s
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.tensorUnit_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_finsetSum_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_4} (s : Finset ι) (f : α → ENNReal)
  (μ : ι → MeasureTheory.Measure α), ∫⁻ (a : α), f a ∂∑ i ∈ s, μ i = ∑ i ∈ s, ∫⁻ (a : α), f a ∂μ i
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.Impl.inner.inj : ∀ {α : Type u} {β : α → Type v} {size : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {size_1 : ℕ}
  {k_1 : α} {v_1 : β k_1} {l_1 r_1 : Std.DTreeMap.Internal.Impl α β},
  Std.DTreeMap.Internal.Impl.inner size k v l r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
    size = size_1 ∧ k = k_1 ∧ v ≍ v_1 ∧ l = l_1 ∧ r = r_1
-- Batteries.Data.Array.Basic
/-- Find the first maximal element of an array. If the array is empty, `default` is
returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered.
 -/
Array.rangeMaxI : {α : Type u_1} → [ord : Ord α] → [Inhabited α] → (xs : Array α) → optParam ℕ 0 → optParam ℕ xs.size → α
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰)
  [inst_5 :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.Limits.PreservesColimitsOfShape J
        (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
  [inst_6 : Quiver.IsThin 𝒰.I₀] [inst_7 : Small.{u, u_2} 𝒰.I₀] [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P]
  (a : J) (i : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme}
  (h : (((CategoryTheory.Functor.const J).obj d.gluedCocone.pt).obj a).left ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.obj a).hom (𝒰.f i))
      (CategoryTheory.CategoryStruct.comp (d.gluedCocone.ι.app a).left h) =
    CategoryTheory.CategoryStruct.comp ((d.cocone i).ι.app a).left
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι d.relativeGluingData.functor i) h)
-- Mathlib.CategoryTheory.Preadditive.Injective.Preserves
CategoryTheory.Functor.preservesInjectiveObjects_of_isEquivalence : ∀ {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.IsEquivalence], F.PreservesInjectiveObjects
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_add_int : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddGroupWithOne G]
  [inst_2 : AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℤ), f (x + ↑n) = f x + ↑n
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.OplaxFunctor B C} (θ : CategoryTheory.Oplax.OplaxTrans G H) {a b : B} {a' : C}
  (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) {Z : a' ⟶ H.obj b}
  (h_1 : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (θ.app a) (H.map h)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) (θ.app b)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality h)) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.map₂ β))) h_1)
-- Mathlib.Algebra.Lie.Ideal
/-- The kernel of a morphism of Lie algebras, as an ideal in the domain.  -/
LieHom.ker : {R : Type u} →
  {L : Type v} →
    {L' : Type w₂} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieRing L'] → [inst_3 : LieAlgebra R L'] → [inst_4 : LieAlgebra R L] → (L →ₗ⁅R⁆ L') → LieIdeal R L
-- Lean.Message
Lean.MessageSeverity.error : Lean.MessageSeverity
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
/-- Stated for readability of `δ₁_apply`.  -/
groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u_1, u, u} k G)},
  X.ShortExact →
    ∀ {y : G → ↑X.X₂} {x : G × G → ↑X.X₁},
      ⇑(Rep.Hom.hom X.f) ∘ x = (CategoryTheory.ConcreteCategory.hom (groupCohomology.d₁₂ X.X₂)) y →
        x ∈ groupCohomology.cocycles₂ X.X₁
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
/-- Given `h : toInt a = i.wrap b`, return `(b', h)` where
`b'` is the expanded form of `i.wrap b`, and `h : toInt a = b'`
 -/
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.expandWrap : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Lean.Expr × Lean.Expr)