mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α}
  {fallback : β k}, (List.map Sigma.fst l).contains k = false → (t.insertMany l).getD k fallback = t.getD k fallback
-- Lean.Server.Completion.SyntheticCompletion
Lean.Server.Completion.findSyntheticCompletions : Lean.FileMap →
  String.Pos.Raw → Lean.Syntax → Lean.Elab.InfoTree → Array Lean.Server.Completion.ContextualizedCompletionInfo
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- If `f, g` is an `F`-cosplit pair, then `F` preserves limits of `parallelPair f g`.  -/
CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair.out : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₁, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair F] {A B : C}
  (f g : A ⟶ B) [F.IsCosplitPair f g], CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) F
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.unop_ringCon : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal Rᵐᵒᵖ), I.unop.ringCon = I.ringCon.unop
-- Lean.Server.ServerTask
Lean.Server.ServerTask.EIO.mapTaskCheap : {α : Type u_1} → {ε β : Type} → (α → EIO ε β) → Lean.Server.ServerTask α → BaseIO (Lean.Server.ServerTask (Except ε β))
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.nnnorm_ofSubsingleton_id : ∀ (𝕜 : Type u) {ι : Type v} (G : Type wG) [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace 𝕜 G] [inst_4 : Subsingleton ι] [Nontrivial G] (i : ι),
  ‖(ContinuousMultilinearMap.ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖₊ = 1
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.parseFirstByte_eq_oneMore_of_utf8DecodeChar?_eq_some : ∀ {b : ByteArray} {i : ℕ} {c : Char},
  b.utf8DecodeChar? i = some c →
    c.utf8Size = 2 →
      ∀ (h' : i < b.size), ByteArray.utf8DecodeChar?.parseFirstByte b[i] = ByteArray.utf8DecodeChar?.FirstByte.oneMore
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.freeGroupCongr_symm : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), (FreeGroup.freeGroupCongr e).symm = FreeGroup.freeGroupCongr e.symm
-- Mathlib.Algebra.Order.Sum
Sum.elim_nonpos_iff : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [inst : LE β] [inst_1 : Zero β] {v₁ : α₁ → β} {v₂ : α₂ → β},
  Sum.elim v₁ v₂ ≤ 0 ↔ v₁ ≤ 0 ∧ v₂ ≤ 0
-- Init.Prelude
/-- Translates an action from monad `m` into monad `n`.  -/
MonadLift.monadLift : {m : semiOutParam (Type u → Type v)} → {n : Type u → Type w} → [self : MonadLift m n] → {α : Type u} → m α → n α
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RciSliceData.treeMap : {α : Type u} →
  {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RciSliceData α β → Std.DTreeMap.Internal.Impl α fun x => β
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.mapRange.linearEquiv_apply : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ₁₂ : R →+* R₂}
  {σ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] (e : M ≃ₛₗ[σ₁₂] N) (g : α →₀ M),
  (Finsupp.mapRange.linearEquiv e) g = Finsupp.mapRange ⇑e ⋯ g
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- multiplicative equivalences between `Semigroup`s are the same as (isomorphic to) isomorphisms
in `Semigroup`  -/
mulEquivIsoSemigrpIso : {X Y : Type u} → [inst : Semigroup X] → [inst_1 : Semigroup Y] → X ≃* Y ≅ Semigrp.of X ≅ Semigrp.of Y
-- Std.Data.TreeMap.Raw.Basic
/-- Transforms an array of keys into a tree map.  -/
Std.TreeMap.Raw.unitOfArray : {α : Type u} →
  Array α → (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.unitOfArray._auto_1) → Std.TreeMap.Raw α Unit cmp
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
/-- The pullback by the identity morphism identifies to the identity functor of the
category of sheaves of modules.  -/
SheafOfModules.pullbackId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (S : CategoryTheory.Sheaf J RingCat) →
        SheafOfModules.pullback (CategoryTheory.CategoryStruct.id S) ≅ CategoryTheory.Functor.id (SheafOfModules S)
-- Mathlib.LinearAlgebra.TensorPower.Basic
/-- As a graded monoid, `⨂[R]^i M` has a `(*) : ⨂[R]^i M → ⨂[R]^j M → ⨂[R]^(i + j) M`.  -/
TensorPower.gMul : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → GradedMonoid.GMul fun i => TensorPower R i M
-- Init.Data.SInt.Lemmas
Int64.sub_eq_add_neg : ∀ (a b : Int64), a - b = a + -b
-- Mathlib.Order.Atoms
IsCoatomic.mk : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α],
  (∀ (b : α), b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a) → IsCoatomic α
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.map_ιFree_mapFreeIso_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u)
  [inst_6 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (i : I) {Z : SheafOfModules S}
  (h : SheafOfModules.free I ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (SheafOfModules.ιFree i))
      (CategoryTheory.CategoryStruct.comp (SheafOfModules.mapFreeIso F I η).inv h) =
    CategoryTheory.CategoryStruct.comp η.inv (CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) h)
-- Mathlib.Algebra.Category.CommBialgCat
CommAlgCat.mul_op_of_unop_hom : ∀ {R : Type u} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : Bialgebra R A],
  CommAlgCat.Hom.hom CategoryTheory.MonObj.mul.unop = Bialgebra.comulAlgHom R A
-- Mathlib.Data.Int.GCD
Nat.exists_mul_mod_eq_one_of_coprime : ∀ {k n : ℕ}, n.Coprime k → 1 < k → ∃ m < k, n * m % k = 1
-- Lean.Level
_private.Lean.Level.0.Lean.Level.substParams.go : (Lean.Name → Option Lean.Level) → Lean.Level → Lean.Level
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.instSemilatticeInfClosedAddSubgroup.eq_1 : ∀ (G : Type u) [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  ClosedAddSubgroup.instSemilatticeInfClosedAddSubgroup G = Function.Injective.semilatticeInf SetLike.coe ⋯ ⋯ ⋯ ⋯
-- Init.Data.SInt.Lemmas
Int64.toInt_ofBitVec : ∀ (b : BitVec 64), (Int64.ofBitVec b).toInt = b.toInt
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsFraisse.jointEmbedding : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [self : FirstOrder.Language.IsFraisse K],
  FirstOrder.Language.JointEmbedding K
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.stdSimplex.spineId_vertex : ∀ (n : ℕ) (i : Fin (n + 1)), (SSet.stdSimplex.spineId n).vertex i = SSet.stdSimplex.obj₀Equiv.symm i
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Iterators.Types.FilterMap.instIterator.match_1.eq_2 : ∀ {β γ : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (Option γ)} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (out' : γ) (h' : (f out).Property (some out'))
  (h_1 : (h' : (f out).Property none) → motive ⟨none, h'⟩)
  (h_2 : (out' : γ) → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩),
  (match ⟨some out', h'⟩ with
    | ⟨none, h'⟩ => h_1 h'
    | ⟨some out', h'⟩ => h_2 out' h') =
    h_2 out' h'
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instMulOneClassOfMonoidHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → MulOneClass (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] → MulOneClass (DirectLimit G f)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_erase_eq_of_not_compare_maxKey!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → ¬cmp k t.maxKey! = Ordering.eq → (t.erase k).maxKey! = t.maxKey!
-- Mathlib.Order.Closure
LowerAdjoint.notMem_of_notMem_closure : ∀ {α : Type u_1} {β : Type u_4} [inst : SetLike α β] [inst_1 : Preorder α] (l : LowerAdjoint SetLike.coe) {s : Set β}
  {P : β}, P ∉ l.toFun s → P ∉ s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.forM_eq_forM_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → m PUnit.{w + 1}}, (forM t fun a => f a.1) = Array.forM f t.keysArray
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabRcc : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF → (Std.DTreeMap.Raw.Const.toArray t).size = t.size
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Converse to the mean value inequality: if `f` is differentiable at `x₀` and `C`-lipschitz
on a neighborhood of `x₀` then its derivative at `x₀` has norm bounded by `C`.  -/
HasDerivAt.le_of_lipschitzOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x₀ : 𝕜},
  HasDerivAt f f' x₀ → ∀ {s : Set 𝕜}, s ∈ nhds x₀ → ∀ {C : NNReal}, LipschitzOnWith C f s → ‖f'‖ ≤ ↑C
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.rel.inj : ∀ {L : FirstOrder.Language} {α : Type u'} {n l : ℕ} {R : L.Relations l} {ts : Fin l → L.Term (α ⊕ Fin n)} {l_1 : ℕ}
  {R_1 : L.Relations l_1} {ts_1 : Fin l_1 → L.Term (α ⊕ Fin n)},
  FirstOrder.Language.BoundedFormula.rel R ts = FirstOrder.Language.BoundedFormula.rel R_1 ts_1 →
    l = l_1 ∧ R ≍ R_1 ∧ ts ≍ ts_1
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instContainsIdentitiesScheme : CategoryTheory.MorphismProperty.ContainsIdentities @AlgebraicGeometry.IsFinite
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inlCompInlCompAssociator.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E],
  CategoryTheory.sum.inlCompInlCompAssociator C D E =
    (CategoryTheory.Sum.inl_ C D).isoWhiskerLeft (CategoryTheory.sum.inlCompAssociator C D E) ≪≫
      (CategoryTheory.Sum.inl_ C (D ⊕ E)).inlCompSum'
        ((CategoryTheory.Sum.inl_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E)))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.minKeyD_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : β → β},
  (Std.DTreeMap.Const.modify t k f).isEmpty = false →
    ∀ {fallback : α},
      (Std.DTreeMap.Const.modify t k f).minKeyD fallback =
        if cmp (t.minKeyD fallback) k = Ordering.eq then k else t.minKeyD fallback
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.evalList.match_1.eq_2 : ∀ (motive : List ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive []) (h_2 : (x : ℕ) → motive [x])
  (h_3 : (x : ℕ) → (xs : List ℕ) → motive (x :: xs)),
  (match [x] with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: xs => h_3 x xs) =
    h_2 x
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
/-- A category `HasFiniteWidePushouts` if it has all colimits of shape `WidePushoutShape J` for
finite `J`, i.e. if it has a wide pushout for every finite collection of morphisms with the same
domain.  -/
CategoryTheory.Limits.HasFiniteWidePushouts : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α} {fallback : β a} {v : β k},
  (t.insertIfNew k v).getD a fallback = if h : cmp k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.getD a fallback
-- Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
/-- There are permutations with cycleType `m` if and only if
its sum is at most `Fintype.card α` and its members are at least 2.  -/
Equiv.Perm.exists_with_cycleType_iff : ∀ (α : Type u_1) [inst : DecidableEq α] [inst_1 : Fintype α] {m : Multiset ℕ},
  (∃ g, g.cycleType = m) ↔ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
-- Mathlib.Order.WithBot
WithBot.decidableLT.eq_2 : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] (a : α), WithBot.decidableLT none (some a) = isTrue ⋯
-- Mathlib.Algebra.Group.Nat.Defs
Nat.instAddCancelCommMonoid : AddCancelCommMonoid ℕ
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgHom.equalizer_same : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), φ.equalizer φ = ⊤
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
AddEquiv.symm_toContinuousAddEquiv : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Add G] [inst_3 : Add H]
  {e : G ≃+ H} (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s),
  (e.toContinuousAddEquiv he).symm = e.symm.toContinuousAddEquiv ⋯
-- Mathlib.Topology.Separation.GDelta
instR0SpaceOfPerfectlyNormalSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PerfectlyNormalSpace X], R0Space X
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrum_eq_spectrum_union_zero : ∀ (R : Type u_3) {A : Type u_4} [inst : Semifield R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A),
  quasispectrum R a = spectrum R a ∪ {0}
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.sum_pow' : ∀ {κ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (s : Finset κ) (f : κ → R) (n : ℕ),
  (∑ a ∈ s, f a) ^ n = ∑ p ∈ Fintype.piFinset fun _i => s, ∏ i, f (p i)
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.mem_submoduleImage_of_le : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_10}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {O : Submodule R M} {ϕ : ↥O →ₗ[R] M'} {N : Submodule R M}
  (hNO : N ≤ O) {x : M'}, x ∈ ϕ.submoduleImage N ↔ ∃ y, ∃ (yN : y ∈ N), ϕ ⟨y, ⋯⟩ = x
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanQueryModuleParams.toJson : Lean.Lsp.LeanQueryModuleParams → Lean.Json
-- Mathlib.Algebra.Group.Basic
ite_zero_add : ∀ {M : Type u_4} [inst : AddZeroClass M] {P : Prop} [inst_1 : Decidable P] {a b : M},
  (if P then 0 else a + b) = (if P then 0 else a) + if P then 0 else b
-- Mathlib.Topology.Algebra.Module.LocallyConvex
Prod.locallyConvexSpace : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace E]
  [inst_7 : TopologicalSpace F] [LocallyConvexSpace 𝕜 E] [LocallyConvexSpace 𝕜 F], LocallyConvexSpace 𝕜 (E × F)
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
/-- The image of a Delone set under an isometry. This is a specialization of
`DeloneSet.mapBilipschitz` where the packing and covering radii are preserved because the
Lipschitz constants are both 1.  -/
Delone.DeloneSet.mapIsometry : {X : Type u_1} →
  {Y : Type u_2} → [inst : MetricSpace X] → [inst_1 : MetricSpace Y] → X ≃ᵢ Y → Delone.DeloneSet X ≃ Delone.DeloneSet Y
-- Mathlib.Order.Interval.Finset.Defs
LocallyFiniteOrder.toLocallyFiniteOrderTop : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → [OrderTop α] → LocallyFiniteOrderTop α
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the unit is an isomorphism, then the left adjoint is fully faithful.  -/
CategoryTheory.Adjunction.fullyFaithfulLOfIsIsoUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} → (h : L ⊣ R) → [CategoryTheory.IsIso h.unit] → L.FullyFaithful
-- Lean.Util.ForEachExprWhere
/-- `e.forEachWhere p f` applies `f` to each subterm that satisfies `p`.
If `stopWhenVisited` is `true`, the function doesn't visit subterms of terms
which satisfy `p`.
 -/
Lean.Expr.forEachWhere : {ω : Type} →
  {m : Type → Type} →
    [STWorld ω m] →
      [MonadLiftT (ST ω) m] →
        [Monad m] → (Lean.Expr → Bool) → (Lean.Expr → m Unit) → Lean.Expr → optParam Bool false → m Unit
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- See `inner_smul_right_eq_smul` for the case of a general algebra action.  -/
inner_smul_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E) (r : 𝕜), inner 𝕜 x (r • y) = r * inner 𝕜 x y
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.intCast_mul : ∀ {R : Type u_2} [inst : CommRing R] {b₁ b₃ : R} {a₁ a₃ : ℤ} (a₂ : ℕ),
  ↑a₁ = b₁ → ↑a₃ = b₃ → ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃
-- Mathlib.Data.TypeVec
/-- cases distinction for an arrow in the category of 0-length type vectors  -/
TypeVec.typevecCasesNil₃ : {β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v.Arrow v' → Sort u_1} →
  β Fin2.elim0 Fin2.elim0 TypeVec.nilFun →
    (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → (fs : v.Arrow v') → β v v' fs
-- Mathlib.Analysis.SpecialFunctions.Exp
Complex.exp_bound_sq : ∀ (x z : ℂ), ‖z‖ ≤ 1 → ‖Complex.exp (x + z) - Complex.exp x - z • Complex.exp x‖ ≤ ‖Complex.exp x‖ * ‖z‖ ^ 2
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionLiteralSupportValueSet.mk.sizeOf_spec : ∀ (valueSet : Array Lean.Lsp.CodeActionKind), sizeOf { valueSet := valueSet } = 1 + sizeOf valueSet
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arccos`, version subtracting vectors.  -/
Orientation.oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  o.oangle x y = ↑(Real.pi / 2) → o.oangle y (y - x) = ↑(Real.arccos (‖y‖ / ‖y - x‖))
-- Mathlib.Algebra.Group.Ideal
/-- In a monoid, the semigroup ideal generated by `s` is `Set.univ * s`.  -/
SemigroupIdeal.mem_closure'' : ∀ {M : Type u_1} [inst : Monoid M] {s : Set M} {x : M}, x ∈ SemigroupIdeal.closure s ↔ ∃ y, ∃ z ∈ s, y * z = x
-- Mathlib.Order.Defs.LinearOrder
_private.Mathlib.Order.Defs.LinearOrder.0.Ordering.Compares.match_1.eq_3 : ∀ {α : Type u_2} (motive : Ordering → α → α → Sort u_1) (a b : α) (h_1 : (a b : α) → motive Ordering.lt a b)
  (h_2 : (a b : α) → motive Ordering.eq a b) (h_3 : (a b : α) → motive Ordering.gt a b),
  (match Ordering.gt, a, b with
    | Ordering.lt, a, b => h_1 a b
    | Ordering.eq, a, b => h_2 a b
    | Ordering.gt, a, b => h_3 a b) =
    h_3 a b
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.ofSubmodules_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M₂] [inst_5 : TopologicalSpace M₂]
  {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃SL[σ₁₂] M₂) {p : Submodule R M} {q : Submodule R₂ M₂}
  (h : Submodule.map (↑↑e) p = q) (x : ↥q), ↑((e.ofSubmodules p q h).symm x) = e.symm ↑x
-- Mathlib.Topology.Category.TopCat.Limits.Basic
/-- The terminal object of `Top` is `PUnit`.  -/
TopCat.terminalIsoPUnit : ⊤_ TopCat ≅ TopCat.of PUnit.{u + 1}
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.leadingCoeff_finset_prod_le : ∀ {R : Type u} [inst : CommSemiring R] [NoZeroDivisors R] {ι : Type u_2} (s : Finset ι) (f : ι → Ideal (Polynomial R)),
  ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.iUnion_image_mk_leftRel : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  ⋃ q, Quot.mk ⇑(QuotientGroup.leftRel K) '' DoubleCoset.doubleCoset (Quotient.out q) ↑H ↑K = Set.univ
-- Mathlib.Algebra.Order.Group.Int.Sum
/-- Sharp upper bound for the sum of a finset of integers that is bounded above, `Ioc` version.  -/
Finset.sum_le_sum_Ioc : ∀ {s : Finset ℤ} {c : ℤ}, (∀ x ∈ s, x ≤ c) → ∑ x ∈ s, x ≤ ∑ x ∈ Finset.Ioc (c - ↑s.card) c, x
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instInv : {α : Type u_1} → [Inv α] → Inv αᵒᵈ
-- Mathlib.GroupTheory.Congruence.Hom
/-- The kernel of the quotient map induced by an additive congruence
relation `c` equals `c`.  -/
AddCon.ker_mkAddHom_eq : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M), AddCon.ker c.mkAddHom = c
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_sub : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddGroup R] (a b : QuaternionAlgebra R c₁ c₂ c₃), (a - b).imI = a.imI - b.imI
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.mul_nat : ∀ {p x : ℝ} {n : ℕ}, LiouvilleWith p x → n ≠ 0 → LiouvilleWith p (x * ↑n)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.gc_strictMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D), GaloisConnection (fun x => x.strictMap F) fun x => x.inverseImage F
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.liftRel_dropn_destruct : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {s : Stream'.WSeq α} {t : Stream'.WSeq β},
  Stream'.WSeq.LiftRel R s t →
    ∀ (n : ℕ),
      Computation.LiftRel (Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)) (s.drop n).destruct (t.drop n).destruct
-- Mathlib.Algebra.Group.EvenFunction
/-- The sum of values of an odd function over a symmetric finite set is zero.  -/
Function.Odd.finsetSum_eq_zero : ∀ {α : Type u_3} {β : Type u_4} [inst : AddCommGroup β] [IsAddTorsionFree β] [inst_2 : InvolutiveNeg α] {f : α → β},
  Function.Odd f → ∀ {s : Finset α}, Finset.map (Equiv.toEmbedding (Equiv.neg α)) s = s → s.sum f = 0
-- Std.Http.Data.URI.Basic
/-- Builds a `UserInfo` value from raw strings by applying userinfo percent-encoding.
 -/
Std.Http.URI.UserInfo.ofStrings : String → optParam (Option String) none → Std.Http.URI.UserInfo
-- Mathlib.Algebra.Module.Basic
Set.indicator_const_smul_apply : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : SMulZeroClass R M] (s : Set α) (r : R)
  (f : α → M) (a : α), s.indicator (fun x => r • f x) a = r • s.indicator f a
-- Init.GetElem
Array.get!Internal_eq_getElem! : ∀ {α : Type u_1} [inst : Inhabited α] (a : Array α) (i : ℕ), a.get!Internal i = a[i]!
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
/-- If `T` is `R`-flat, the canonical map `T ⊗[R] P.H1Cotangent →ₗ[T] (P.baseChange T).H1Cotangent`
is bijective.  -/
Algebra.Extension.tensorToH1Cotangent_bijective_of_flat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S) (T : Type u_3) [inst_3 : CommRing T] [inst_4 : Algebra R T] [Module.Flat R T],
  Function.Bijective ⇑(P.tensorToH1Cotangent T)