mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
/-- If there is a diagram where the morphisms `W ⟶ Y` and `X ⟶ Z` are embeddings,
then the induced morphism `W ×ₛ X ⟶ Y ×ₜ Z` is also an embedding.

```
W ⟶ Y
 ↘   ↘
  S ⟶ T
 ↗   ↗
X ⟶ Z
```
 -/
TopCat.pullback_map_isEmbedding : ∀ {W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z},
  Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₁) →
    Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₂) →
      ∀ (i₃ : S ⟶ T) (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁)
        (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂),
        Topology.IsEmbedding
          ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.isOfFinAddOrder_iff_exists_rat_eq_div : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {a : 𝕜},
  IsOfFinAddOrder ↑a ↔ ∃ q, ↑q = a / p
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k k' fallback : α},
  (k == k') = true →
    k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertManyIfNewUnit l).getKeyD k' fallback = k
-- Std.Time.Duration
/-- Converts a `Duration` to a `Nanosecond.Offset`
 -/
Std.Time.Duration.toNanoseconds : Std.Time.Duration → Std.Time.Nanosecond.Offset
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.HasRightDerivedFunctor.mk : ∀ {C : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_2} H] {F : CategoryTheory.Functor C H}
  {W : CategoryTheory.MorphismProperty C}, W.Q.HasLeftKanExtension F → F.HasRightDerivedFunctor W
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.hom_ext : ∀ {X Y : FinPartOrd} {f g : X ⟶ Y}, PartOrd.Hom.hom f.hom = PartOrd.Hom.hom g.hom → f = g
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eccent.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α) (u : α), G.eccent u = ⨆ v, G.edist u v
-- Mathlib.Algebra.GroupWithZero.Defs
isLeftCancelMulZero_iff : ∀ (M₀ : Type u) [inst : Mul M₀] [inst_1 : Zero M₀], IsLeftCancelMulZero M₀ ↔ ∀ {a : M₀}, a ≠ 0 → IsLeftRegular a
-- Mathlib.Data.Ordmap.Ordnode
/-- O(m * log(|m ∪ n| + 1)), m ≤ n. The union of two sets, preferring members of
  `t₁` over those of `t₂` when equivalent elements are encountered.

```
union {1, 2} {2, 3} = {1, 2, 3}
union {1, 3} {2} = {1, 2, 3}
```

Using a preorder on `ℕ × ℕ` that only compares the first coordinate:

```
union {(1, 1)} {(0, 1), (1, 2)} = {(0, 1), (1, 1)}
```  -/
Ordnode.union : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → Ordnode α → Ordnode α → Ordnode α
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.isNatLitAux : Lean.SyntaxNodeKind → Lean.Syntax → Option ℕ
-- Init.Data.Slice.Array.Lemmas
Array.size_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, Std.Slice.size (Std.Rco.Sliceable.mkSlice xs lo...hi) = min hi xs.size - lo
-- Init.Core
Nat.add_zero : ∀ (n : ℕ), n + 0 = n
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
/-- The underlying prelax functor.  -/
CategoryTheory.Pseudofunctor.toPrelaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.Pseudofunctor B C → CategoryTheory.PrelaxFunctor B C
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₂_app_two : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 2}
  (app₀ : f.obj' 0 _proof_245✝ ⟶ g.obj' 0 _proof_245✝) (app₁ : f.obj' 1 _proof_246✝ ⟶ g.obj' 1 _proof_246✝)
  (app₂ : f.obj' 2 _proof_247✝ ⟶ g.obj' 2 _proof_247✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝))
      _auto_261✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_247✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_247✝))
      _auto_263✝),
  (CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app 2 = app₂
-- Mathlib.CategoryTheory.Comma.Basic
/-- Taking the comma category of a functor into `A ⥤ Discrete PUnit` and the identity
`Discrete PUnit ⥤ Discrete PUnit` results in a category equivalent to `A`.  -/
CategoryTheory.Comma.toPUnitIdEquiv : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) →
      (R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1})) →
        CategoryTheory.Comma L R ≌ A
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.fill.eq_3 : ∀ {α : Type u_1} (x : RBTree.RBNode α) (c : RBTree.RBColor) (a : RBTree.RBNode α) (y : α)
  (parent : RBTree.RBNode.Path α),
  (RBTree.RBNode.Path.right c a y parent).fill x = parent.fill (RBTree.RBNode.node c a y x)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
groupHomology.cyclesMkOfCompEqD.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) {i j : ℕ} {y y_1 : (Fin i → G) →₀ ↑X.X₂} (e_y : y = y_1) {x x_1 : (Fin j → G) →₀ ↑X.X₁}
  (e_x : x = x_1)
  (hx :
    (Finsupp.mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x =
      (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains X.X₂).d i j)) y),
  groupHomology.cyclesMkOfCompEqD hX hx = groupHomology.cyclesMkOfCompEqD hX ⋯
-- Mathlib.Control.Bitraversable.Instances
_private.Mathlib.Control.Bitraversable.Instances.0.Sum.bitraverse.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (x : β) (h_1 : (x : α) → motive (Sum.inl x))
  (h_2 : (x : β) → motive (Sum.inr x)),
  (match Sum.inr x with
    | Sum.inl x => h_1 x
    | Sum.inr x => h_2 x) =
    h_2 x
-- Mathlib.Analysis.Convex.Function
/-- If a function is concave on `s`, it remains concave when precomposed by an affine map.  -/
ConcaveOn.comp_affineMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : AddCommGroup F] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β]
  [inst_6 : Module 𝕜 E] [inst_7 : Module 𝕜 F] [inst_8 : SMul 𝕜 β] {f : F → β} (g : E →ᵃ[𝕜] F) {s : Set F},
  ConcaveOn 𝕜 s f → ConcaveOn 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)
-- Mathlib.Topology.Spectral.Basic
SpectralSpace.toQuasiSeparatedSpace : ∀ {X : Type u_3} {inst : TopologicalSpace X} [self : SpectralSpace X], QuasiSeparatedSpace X
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get.eq_def : ∀ {α : Type u} {δ : Type w} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α fun x => δ) (k : α)
  (hlk : Std.DTreeMap.Internal.Impl.contains k t = true),
  Std.DTreeMap.Internal.Impl.Const.get t k hlk =
    match t, hlk with
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r, hlk =>
      match h : compare k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.get l k ⋯
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.get r k ⋯
      | Ordering.eq => v'
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_congr_of_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] {f g : α → ℕ} {s t : Finset α},
  s ⊆ t → (∀ a ∈ t \ s, g a = 0) → (∀ a ∈ s, f a = g a) → Nat.multinomial s f = Nat.multinomial t g
-- Mathlib.Order.Completion
/-- `DedekindCut.principal` as an `OrderIso`.

This provides the second half of the **fundamental theorem of concept lattices**: every complete
lattice is isomorphic to a concept lattice (its own Dedekind completion).

See `Concept.instCompleteLattice` for the first half.  -/
DedekindCut.principalIso : {α : Type u_1} → [inst : CompleteLattice α] → α ≃o DedekindCut α
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t_fac_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i j k : self.J) {Z : C}
  (h : self.V (j, i) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.t' i j k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (self.f j k) (self.f j i)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (self.f i j) (self.f i k))
      (CategoryTheory.CategoryStruct.comp (self.t i j) h)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.oreEqv_eq_r : ∀ {R : Type u} [inst : CommSemiring R] (S : Submonoid R) (M : Type v) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⇑(OreLocalization.oreEqv S M) = LocalizedModule.r S M
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- Restriction (in the target) of a bounded continuous function taking values in a subset.  -/
BoundedContinuousFunction.codRestrict : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace β] →
        (s : Set β) → (f : BoundedContinuousFunction α β) → (∀ (x : α), f x ∈ s) → BoundedContinuousFunction α ↑s
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.checkEndHeader : Lean.Name → List Lean.Elab.Command.Scope → Option Lean.Name
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.MatcherInfo.mk.inj : ∀ {numParams numDiscrs : ℕ} {altInfos : Array Lean.Meta.Match.AltParamInfo} {uElimPos? : Option ℕ}
  {discrInfos : Array Lean.Meta.Match.DiscrInfo} {overlaps : Lean.Meta.Match.Overlaps} {numParams_1 numDiscrs_1 : ℕ}
  {altInfos_1 : Array Lean.Meta.Match.AltParamInfo} {uElimPos?_1 : Option ℕ}
  {discrInfos_1 : Array Lean.Meta.Match.DiscrInfo} {overlaps_1 : Lean.Meta.Match.Overlaps},
  { numParams := numParams, numDiscrs := numDiscrs, altInfos := altInfos, uElimPos? := uElimPos?,
        discrInfos := discrInfos, overlaps := overlaps } =
      { numParams := numParams_1, numDiscrs := numDiscrs_1, altInfos := altInfos_1, uElimPos? := uElimPos?_1,
        discrInfos := discrInfos_1, overlaps := overlaps_1 } →
    numParams = numParams_1 ∧
      numDiscrs = numDiscrs_1 ∧
        altInfos = altInfos_1 ∧ uElimPos? = uElimPos?_1 ∧ discrInfos = discrInfos_1 ∧ overlaps = overlaps_1
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le : ∀ {a b c : ℕ}, Multiplicative.ofAdd (-↑c) ≤ max (Multiplicative.ofAdd (-↑a)) (Multiplicative.ofAdd (-↑b)) ↔ min a b ≤ c
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.const_val_apply : ∀ (n : ℕ) (i k : Fin (n + 3)) {m : ℕ} (a : Fin (m + 1)), ↑(SSet.horn.const n i k (Opposite.op { len := m })) a = k
-- Mathlib.Data.Matrix.Mul
Matrix.mul_diagonal : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  [inst_2 : DecidableEq n] (d : n → α) (M : Matrix m n α) (i : m) (j : n), (M * Matrix.diagonal d) i j = M i j * d j
-- Mathlib.Data.Fin.Basic
Fin.castLT_sub_nezero : ∀ {n : ℕ} {i j : Fin n} (hij : i < j), (j - i).castLT ⋯ ≠ 0
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
MonoidHom.CompTriple.IsId.mk : ∀ {M : Type u_1} [inst : Monoid M] {σ : M →* M}, σ = MonoidHom.id M → MonoidHom.CompTriple.IsId σ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfcHom_nnreal_eq_restrict : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : PartialOrder A] [inst_3 : StarRing A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [IsSemitopologicalRing A] [T2Space A]
  [inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] {a : A} (ha : 0 ≤ a),
  cfcHom ha = SpectrumRestricts.starAlgHom (cfcHom ⋯) ⋯
-- Mathlib.Order.Category.DistLat
/-- The underlying distributive lattice.  -/
DistLat.carrier : DistLat → Type u_1
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- To check that a measure `ν` is the projective limit of a projective family of measures indexed
by `Finset ℕ`, it is enough to check on intervals of the form `Iic n`, where `n` is larger than
a given integer.  -/
MeasureTheory.isProjectiveLimit_nat_iff' : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {μ : (I : Finset ℕ) → MeasureTheory.Measure ((i : ↥I) → X ↑i)},
  MeasureTheory.IsProjectiveMeasureFamily μ →
    ∀ (ν : MeasureTheory.Measure ((n : ℕ) → X n)) (a : ℕ),
      MeasureTheory.IsProjectiveLimit ν μ ↔
        ∀ ⦃n : ℕ⦄, a ≤ n → MeasureTheory.Measure.map (Preorder.frestrictLe n) ν = μ (Finset.Iic n)
-- Mathlib.Algebra.GCDMonoid.Basic
nonempty_normalizedGCDMonoid_iff_isGCDMonoid : ∀ {α : Type u_2} [inst : CommMonoidWithZero α], Nonempty (NormalizedGCDMonoid α) ↔ IsGCDMonoid α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α] {k : α} {f : β k → β k}, (t.modify k f).minKey! = t.minKey!
-- Lean.ErrorExplanation
/-- Returns the error explanation summary prepended with its severity. For use in completions and
hovers.
 -/
Lean.ErrorExplanation.summaryWithSeverity : Lean.ErrorExplanation → String
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.auxEquiv_symm_one : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  (GradedTensorProduct.auxEquiv R 𝒜 ℬ).symm 1 = 1
-- Mathlib.Analysis.Complex.RealDeriv
HasDerivWithinAt.complexToReal_fderiv' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {s : Set ℂ} {x : ℂ} {f' : E},
  HasDerivWithinAt f f' s x →
    HasFDerivWithinAt f (Complex.reCLM.smulRight f' + Complex.I • Complex.imCLM.smulRight f') s x
-- Mathlib.NumberTheory.Modular
UpperHalfPlane.ofComplex.eq_1 : UpperHalfPlane.ofComplex =
  (Topology.IsOpenEmbedding.toOpenPartialHomeomorph UpperHalfPlane.coe UpperHalfPlane.isOpenEmbedding_coe).symm
-- Mathlib.GroupTheory.GroupAction.SubMulAction
fixedPointsSubMulOfNormal.eq_1 : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {H : Subgroup G} [hH : H.Normal],
  fixedPointsSubMulOfNormal = { carrier := MulAction.fixedPoints (↥H) α, smul_mem' := ⋯ }
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.IsometryEquiv.mk.sizeOf_spec : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} [inst_5 : SizeOf R] [inst_6 : SizeOf M₁] [inst_7 : SizeOf M₂]
  (toLinearEquiv : M₁ ≃ₗ[R] M₂)
  (map_app' : ∀ (n m : M₁), (B₂ ((↑toLinearEquiv).toFun n)) ((↑toLinearEquiv).toFun m) = (B₁ n) m),
  sizeOf { toLinearEquiv := toLinearEquiv, map_app' := map_app' } = 1 + sizeOf toLinearEquiv
-- Mathlib.Topology.List
_private.Mathlib.Topology.List.0.List.Vector.elim.match_3.eq_1 : ∀ {α : Type u_1} {n : ℕ} (motive : List.Vector α n → Sort u_2) (l : List α) (h : l.length = n)
  (h_1 : (l : List α) → (h : l.length = n) → motive ⟨l, h⟩),
  (match ⟨l, h⟩ with
    | ⟨l, h⟩ => h_1 l h) =
    h_1 l h
-- Mathlib.RingTheory.Congruence.Hom
/-- The kernel of the quotient map induced by a ring congruence relation `c` equals `c`.  -/
RingCon.ker_mk'_eq : ∀ {M : Type u_1} [inst : NonAssocSemiring M] (c : RingCon M), RingCon.ker c.mk' = c
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.toFun_eq_coe : ∀ {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} {f : SlashInvariantForm Γ k}, f.toFun = ⇑f
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
/-- `δ i` is a split epimorphism thanks to the simplicial identities.  -/
SimplexCategoryGenRel.splitEpiσ : {n : ℕ} → (i : Fin (n + 1)) → CategoryTheory.SplitEpi (SimplexCategoryGenRel.σ i)
-- Mathlib.RingTheory.WittVector.Defs
WittVector.instIntCast : {p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [CommRing R] → IntCast (WittVector p R)
-- Std.Data.String.ToNat
String.Slice.isNat_of_toNat?_eq_some : ∀ {n : ℕ} {s : String.Slice}, s.toNat? = some n → s.isNat = true
-- Lean.Server.GoTo
Lean.Server.locationLinksFromBinder : Lean.FVarId → Lean.Server.GoToM (Array Lean.Lsp.LeanLocationLink)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_add_measure : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ ν : MeasureTheory.Measure α} {f : α → G},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable f ν → ∫ (x : α), f x ∂(μ + ν) = ∫ (x : α), f x ∂μ + ∫ (x : α), f x ∂ν
-- Mathlib.RingTheory.Derivation.MapCoeffs
Differential.mapCoeffs_C : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] (x : A),
  Differential.mapCoeffs (Polynomial.C x) = Polynomial.C x′
-- Init.Data.List.Find
List.findFinIdx?_eq_pmap_findIdx? : ∀ {α : Type u_1} {xs : List α} {p : α → Bool},
  List.findFinIdx? p xs = Option.pmap (fun i m => ⟨i, ⋯⟩) (List.findIdx? p xs) ⋯
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Subtracting the first vector passed to `oangle` from the second vector then swapping the
vectors does not change the sign of the angle.  -/
Orientation.oangle_sign_sub_right_swap : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), (o.oangle y (y - x)).sign = (o.oangle x y).sign
-- Mathlib.Logic.Embedding.Basic
Equiv.asEmbedding_apply : ∀ {β : Sort u_1} {α : Sort u_2} {p : β → Prop} (e : α ≃ Subtype p) (a : α), e.asEmbedding a = ↑(e a)
-- Init.PropLemmas
Bool.ite_else_true_eq_false : ∀ {p : Prop} [inst : Decidable p] {x : Bool}, (if p then x else true) = false ↔ p ∧ x = false
-- Mathlib.Order.Minimal
Minimal.not_ssubset : ∀ {α : Type u_2} {P : Set α → Prop} {s t : Set α}, Minimal P s → P t → ¬t ⊂ s
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f g : M → E'} {s : Set M}, MDiffAt[s] f z → MDiffAt[s] g z → MDiffAt[s] (f + g) z
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.leftUnitor_inv_naturality : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.leftUnitor g).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).inv
      (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η)
-- Mathlib.GroupTheory.Perm.Centralizer
/-- A `Basis` of a permutation is a choice of an element in each of its cycles  -/
Equiv.Perm.Basis : {α : Type u_1} → [DecidableEq α] → [Fintype α] → Equiv.Perm α → Type u_1
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
/-- Given a presieve `R` on `Y`, if we take its associated family of opens via `coveringOfPresieve`
(which may not cover `Y` if `R` is not covering), and take the presieve on `Y` associated to the
family of opens via `presieveOfCoveringAux`, then we get back the original presieve `R`.  -/
TopCat.Presheaf.covering_presieve_eq_self : ∀ {X : TopCat} {Y : TopologicalSpace.Opens ↑X} (R : CategoryTheory.Presieve Y),
  TopCat.Presheaf.presieveOfCoveringAux (TopCat.Presheaf.coveringOfPresieve Y R) Y = R
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- The underlying linear map.  -/
ModuleCat.Hom.hom' : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → M.Hom N → ↑M →ₗ[R] ↑N
-- Std.Net.Addr
/-- An IP address, either IPv4 or IPv6.
 -/
Std.Net.IPAddr : Type
-- Mathlib.RingTheory.Localization.Defs
Localization.add_mk_self : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (a : R) (b : ↥M) (c : R),
  Localization.mk a b + Localization.mk c b = Localization.mk (a + c) b
-- Init.Data.String.Lemmas.Basic
String.Slice.sliceFrom_sliceFrom : ∀ {s : String.Slice} {pos : s.Pos} {pos' : (s.sliceFrom pos).Pos},
  (s.sliceFrom pos).sliceFrom pos' = s.sliceFrom (String.Slice.Pos.ofSliceFrom pos')
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.homAddEquiv_symm_add : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f f' : X ⟶ G.obj Y),
  (adj.homEquiv X Y).symm (f + f') = (adj.homEquiv X Y).symm f + (adj.homEquiv X Y).symm f'
-- Init.Data.SInt.Basic
/-- Bitwise or for 32-bit signed integers. Usually accessed via the `|||` operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of the input
integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.lor : Int32 → Int32 → Int32
-- Mathlib.Topology.Bornology.Constructions
Bornology.isBounded_pi : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → Bornology (X i)] {S : (i : ι) → Set (X i)},
  Bornology.IsBounded (Set.univ.pi S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), Bornology.IsBounded (S i)
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.annihilator_top_eq_ker_aeval : ∀ {R : Type u_3} {A : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] [FaithfulSMul A M], ⊤.annihilator = RingHom.ker (Polynomial.aeval a)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instStarRing : {R : Type u_3} → {c₁ c₂ c₃ : R} → [inst : CommRing R] → StarRing (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
CategoryTheory.ShiftedHom.opEquiv'.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y : C}
  (n a a' : ℤ) (h : n + a = a'),
  CategoryTheory.ShiftedHom.opEquiv' n a a' h = CategoryTheory.ShiftedHom.opEquiv' n a a' h
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.compHom_apply_apply : ∀ {M : Type uM} {N : Type uN} {P : Type uP} [inst : MulOneClass M] [inst_1 : CommMonoid N] [inst_2 : CommMonoid P]
  (g : N →* P) (hmn : M →* N), (MonoidHom.compHom g) hmn = g.comp hmn
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- Given two distinct paths with the same endpoints, we can extract a subwalk from each such that their
concatenation, with one reversed, forms a cycle.
 -/
SimpleGraph.Walk.IsPath.exists_isCycle_of_ne : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v},
  p.IsPath → q.IsPath → p ≠ q → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType : ∀ (S : LightProfiniteᵒᵖ),
  CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.CostructuredArrow FintypeCat.toLightProfinite.op S) (Type u)
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A product of copies of a topological space can be split as the binary product of one copy and
the product of all the remaining copies.  -/
Homeomorph.funSplitAt : (Y : Type u_2) →
  [inst : TopologicalSpace Y] → {ι : Type u_7} → [DecidableEq ι] → (i : ι) → (ι → Y) ≃ₜ Y × ({ j // j ≠ i } → Y)