mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Restrict
CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] {iC : CategoryTheory.Functor C C'} {iD : CategoryTheory.Functor D D'}
  {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful)
  (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
  (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) (X : C) {Z : C'} (h : iC.obj (R.obj (L.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (iC.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).unit.app X)) h =
    CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X))
      (CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X))
        (CategoryTheory.CategoryStruct.comp (comm2.hom.app (L.obj X)) h))
-- Init.Data.BitVec.Lemmas
BitVec.toNat_rotateRight : ∀ {w : ℕ} {x : BitVec w} {r : ℕ}, (x.rotateRight r).toNat = x.toNat >>> (r % w) ||| x.toNat <<< (w - r % w) % 2 ^ w
-- Mathlib.Data.Nat.Find
/-- A weak version of `Nat.find_mono_of_le`, requiring `q` implies `p` everywhere.
 -/
Nat.find_mono : ∀ {p q : ℕ → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q],
  (∀ (n : ℕ), q n → p n) → ∀ {hp : ∃ n, p n} {hq : ∃ n, q n}, Nat.find hp ≤ Nat.find hq
-- Batteries.Logic
heq_of_cast_eq : ∀ {α β : Sort u_1} {a : α} {a' : β} (e : α = β), cast e a = a' → a ≍ a'
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K], NumberField.IsCMField K = NumberField.IsCMField K
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_nsmul : ∀ {α : Type u_1} {N : Type u_10} [inst : AddCommMonoid N] [inst_1 : Fintype α] (f : α →₀ ℕ) (g : α → N),
  (f.sum fun a b => b • g a) = ∑ a, f a • g a
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- Get the walk between two vertices in a connected component from a walk in the original graph.
This is used in `reachable_toSimpleGraph`.  -/
_private.Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected.0.SimpleGraph.ConnectedComponent.walk_toSimpleGraph : {V : Type u} →
  {G : SimpleGraph V} →
    (C : G.ConnectedComponent) →
      {u v : V} → (hu : u ∈ C) → (hv : v ∈ C) → G.Walk u v → C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨v, hv⟩
-- Lean.Meta.Tactic.Symm
/-- Return the symmetry lemmas that match the target type.  -/
Lean.Expr.getSymmLems : Lean.Expr → Lean.MetaM (Array Lean.Name)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A version of `Finset.sum_map` and `Finset.sum_image`, but we do not assume that `f` is
injective. Rather, we assume that the images of `f` are disjoint on `I`, and `g ⊥ = 0`. The
conclusion is the same as in `sum_image`.  -/
Finset.sum_image_of_disjoint : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι]
  [inst_2 : PartialOrder ι] [inst_3 : OrderBot ι] {f : κ → ι} {g : ι → M},
  g ⊥ = 0 → ∀ {I : Finset κ}, (↑I).PairwiseDisjoint f → ∑ s ∈ Finset.image f I, g s = ∑ i ∈ I, g (f i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.map_addX : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S)
  (P Q : Fin 3 → R), (W'.map f).addX (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addX P Q)
-- Mathlib.Algebra.GroupWithZero.Basic
zpow_one_add₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (i : ℤ), a ^ (1 + i) = a * a ^ i
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f}
  (e : (i : ι) → D₁.obj i ≅ D₂.obj i)
  (comm :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom)) =
          CategoryTheory.CategoryStruct.comp (e i₁).hom (D₂.hom i₁ i₂))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk._auto_1)
  (i : ι), (CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk e comm).hom.hom i = (e i).hom
-- Init.Data.Array.MapIdx
Array.mapFinIdx_eq_zipIdx_map : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β},
  xs.mapFinIdx f =
    Array.map
      (fun x =>
        match x with
        | ⟨(x, i), m⟩ => f i x ⋯)
      xs.zipIdx.attach
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.GetLsbD
Std.Sat.AIG.RefVec.getD.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} (s : aig.RefVec len) (idx : ℕ)
  (alt : aig.Ref), s.getD idx alt = if hidx : idx < len then s.get idx hidx else alt
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- A complement of an FG submodule is CoFG.  -/
Submodule.FG.cofg_of_isCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S T : Submodule R M},
  IsCompl S T → S.FG → T.CoFG
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CosimplicialObject.equivalenceRightToLeft_right_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  (F : CategoryTheory.Arrow C) (X : CategoryTheory.CosimplicialObject.Augmented C)
  (G : F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X) (x : SimplexCategory),
  (CategoryTheory.CosimplicialObject.equivalenceRightToLeft F X G).right.app x =
    CategoryTheory.Limits.WidePushout.desc
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left G) (X.hom.app x))
      (fun i =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right G) (X.right.map ({ len := 0 }.const x i)))
      ⋯
-- Lean.Compiler.IR.Basic
/-- Partial application that creates a `pap` value (aka closure in our nonstandard terminology).  -/
Lean.IR.Expr.pap : Lean.IR.FunId → Array Lean.IR.Arg → Lean.IR.Expr
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a b : α},
  Std.Internal.List.containsKey a l = true → (a == b) = true → Std.Internal.List.containsKey b l = true
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.divLeft.eq_1 : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α] (a : α),
  OrderIso.divLeft a = { toEquiv := (Equiv.divLeft a).trans OrderDual.toDual, map_rel_iff' := ⋯ }
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.mul : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J RingCat} →
      RingCat.Colimits.Prequotient F → RingCat.Colimits.Prequotient F → RingCat.Colimits.Prequotient F
-- Mathlib.Order.Interval.Set.Monotone
AntitoneOn.Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  AntitoneOn f s → MonotoneOn (fun x => Set.Ici (f x)) s
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The principal unit group agrees with the kernel of the canonical map from
the units of `A` to the units of the residue field of `A`.  -/
ValuationSubring.principalUnitGroupEquiv : {K : Type u} →
  [inst : Field K] → (A : ValuationSubring K) → ↥A.principalUnitGroup ≃* ↥(Units.map ↑(IsLocalRing.residue ↥A)).ker
-- Mathlib.Algebra.Module.FinitePresentation
Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule : ∀ {R : Type u_1} {M : Type u_2} {N : 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] [inst_5 : AddCommGroup N']
  [inst_6 : Module R N'] (S : Submonoid R) (f : N →ₗ[R] N') [IsLocalizedModule S f] [hM : Module.Finite R M]
  (g₁ g₂ : M →ₗ[R] N), f ∘ₗ g₁ = f ∘ₗ g₂ → ∃ s, s • g₁ = s • g₂
-- Mathlib.Order.WithBot
WithBot.toDual_lt_iff : ∀ {α : Type u_1} [inst : LT α] {x : WithBot α} {y : WithTop αᵒᵈ}, WithBot.toDual x < y ↔ WithTop.ofDual y < x
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.comm₁₃_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂)
  {Z : C} (h : sq₂.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp sq₁.f₁₃ (CategoryTheory.CategoryStruct.comp self.τ₃ h) =
    CategoryTheory.CategoryStruct.comp self.τ₁ (CategoryTheory.CategoryStruct.comp sq₂.f₁₃ h)
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_int16 : ∀ (x : Int16), ↑x = x.toInt
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsAddTorsion.addGroup`.

---

Torsion additive monoids are really additive groups.  -/
IsTorsion.addGroup : {G : Type u_1} → [inst : AddMonoid G] → IsAddTorsion G → AddGroup G
-- Mathlib.Algebra.Order.Group.MinMax
max_inv_one : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] (a : α), max a⁻¹ 1 = a⁻¹ * max a 1
-- Mathlib.Data.Rel
SetRel.core_id : ∀ {β : Type u_2} (t : Set β), SetRel.id.core t = t
-- Mathlib.Data.List.Nodup
List.nodup_flatMap : ∀ {α : Type u} {β : Type v} {l₁ : List α} {f : α → List β},
  (List.flatMap f l₁).Nodup ↔ (∀ x ∈ l₁, (f x).Nodup) ∧ List.Pairwise (Function.onFun List.Disjoint f) l₁
-- Mathlib.Data.Set.Basic
Set.sep_mem_eq : ∀ {α : Type u} {s t : Set α}, {x | x ∈ s ∧ x ∈ t} = s ∩ t
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.instInhabitedHandlerTrie : Inhabited Lean.Elab.ConfigEval.HandlerTrie✝
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- The linear equivalence between `n`-fold alternating maps from `M` to `N` and linear maps from
`⋀[R]^n M` to `N`: this is the universal property of the `n`th exterior power of `M`.  -/
exteriorPower.alternatingMapLinearEquiv : {R : Type u} →
  [inst : CommRing R] →
    {n : ℕ} →
      {M : Type u_1} →
        {N : Type u_2} →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → M [⋀^Fin n]→ₗ[R] N ≃ₗ[R] ↥(⋀[R]^n M) →ₗ[R] N
-- Mathlib.RingTheory.Bialgebra.Hom
/-- Given `R`-algebras `A, B` with comultiplication maps `Δ_A, Δ_B` and counit maps
`ε_A, ε_B`, an `R`-bialgebra homomorphism `A →ₐc[R] B` is an `R`-algebra map `f` such that
`ε_B ∘ f = ε_A` and `(f ⊗ f) ∘ Δ_A = Δ_B ∘ f`.  -/
BialgHom : (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] → [CoalgebraStruct R A] → [CoalgebraStruct R B] → Type (max u_2 u_3)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_iUnion₂ : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_10}
  {κ : ι → Sort u_9} (s : (i : ι) → κ i → Set M),
  Submodule.span R (⋃ i, ⋃ j, s i j) = ⨆ i, ⨆ j, Submodule.span R (s i j)
-- Mathlib.Analysis.SpecialFunctions.FrullaniIntegral
Frullani.integral_comp_mul_inv_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {c ε r : ℝ},
  c ≠ 0 → ∫ (x : ℝ) in ε..r, x⁻¹ • f (c * x) = ∫ (x : ℝ) in c * ε..c * r, x⁻¹ • f x
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.instFaithfulToCompHausLike : ∀ {P P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop), (CompHausLike.toCompHausLike h).Faithful
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Version of `algebraMap_elemReduct_eq` using `ExpChar`.  -/
IsPurelyInseparable.algebraMap_elemReduct_eq' : ∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] (p : ℕ) [ExpChar K p] (a : L),
  (algebraMap K L) (IsPurelyInseparable.elemReduct K a) = a ^ p ^ IsPurelyInseparable.elemExponent K a
-- Mathlib.LinearAlgebra.ExteriorPower.Pairing
exteriorPower.pairingDual.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ),
  exteriorPower.pairingDual R M n = exteriorPower.alternatingMapLinearEquiv (exteriorPower.alternatingMapToDual R M n)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Truncated.whiskering_map_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y)
  (F : CategoryTheory.Functor (SimplexCategory.Truncated n) C) (c : SimplexCategory.Truncated n),
  (((CategoryTheory.CosimplicialObject.Truncated.whiskering C D).map τ).app F).app c = τ.app (F.obj c)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lt_add_iff_of_isSuccLimit : ∀ {a b c : Ordinal.{u_4}}, Order.IsSuccLimit c → (a < b + c ↔ ∃ d < c, a < b + d)
-- Init.Data.Nat.Div.Basic
Nat.modCore.go.congr_simp : ∀ (y y_1 : ℕ) (e_y : y = y_1) (hy : 0 < y) (fuel fuel_1 : ℕ) (e_fuel : fuel = fuel_1) (x x_1 : ℕ) (e_x : x = x_1)
  (hfuel : x < fuel), Nat.modCore.go y hy fuel x hfuel = Nat.modCore.go y_1 ⋯ fuel_1 x_1 ⋯
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sUnion_inv : ∀ {α : Type u_2} [inst : Inv α] (S : Set (Set α)), (⋃₀ S)⁻¹ = ⋃ s ∈ S, s⁻¹
-- Mathlib.Topology.Algebra.Algebra
/-- `Subalgebra.val` as a `ContinuousAlgHom`.  -/
Subalgebra.valA : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] → [inst_2 : TopologicalSpace A] → [inst_3 : Algebra R A] → (p : Subalgebra R A) → ↥p →A[R] A
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase_dup_rhs.sizeOf_spec : ∀ (c : Lean.Meta.Grind.AC.EqCnstr), sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.erase_dup_rhs c) = 1 + sizeOf c
-- Init.Coe
CoeTail.mk : {α : semiOutParam (Sort u)} → {β : Sort v} → (α → β) → CoeTail α β
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.instDecidableIsPathOfDecidableEq : {V : Type u} → {G : SimpleGraph V} → [DecidableEq V] → {u v : V} → (p : G.Walk u v) → Decidable p.IsPath
-- Mathlib.LinearAlgebra.Matrix.Ideal
Ideal.matrix_strictMono_of_nonempty : ∀ {R : Type u_1} [inst : Semiring R] (n : Type u_2) [inst_1 : Fintype n] [inst_2 : DecidableEq n] [Nonempty n],
  StrictMono (Ideal.matrix n)
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.instMul : (M : Type u_4) → [inst : MulOne M] → Mul (Monoid.End M)
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.liftOrderTop.eq_1 : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder β] [inst_1 : Preorder α] [inst_2 : OrderTop α]
  (gi : GaloisInsertion l u), gi.liftOrderTop = { top := gi.choice ⊤ ⋯, le_top := ⋯ }
-- Mathlib.RingTheory.TensorProduct.Free
Algebra.TensorProduct.basis_repr_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (b : Module.Basis ι R M) (a : A) (i : ι),
  ((Algebra.TensorProduct.basis A b).repr.symm fun₀ | i => a) = a ⊗ₜ[R] b.repr.symm fun₀ | i => 1
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvFunctor.supp.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} n → Type v} [inst : MvFunctor F] {α : TypeVec.{u} n} (x : F α) (i : Fin2 n),
  MvFunctor.supp x i = {y | ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, MvFunctor.LiftP P x → P i y}
-- Lean.Elab.WhereFinally
Lean.Elab.WhereFinallyView.isNone : Lean.Elab.WhereFinallyView → Bool
-- Mathlib.Topology.MetricSpace.MetricSeparated
/-- Two sets in an (extended) metric space are called *metric separated* if the (extended) distance
between `x ∈ s` and `y ∈ t` is bounded from below by a positive constant.  -/
Metric.AreSeparated : {X : Type u_1} → [PseudoEMetricSpace X] → Set X → Set X → Prop
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Ideal.minimalPrimes_map_of_surjective : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_3} [inst_1 : CommRing S] {f : R →+* S},
  Function.Surjective ⇑f →
    ∀ (I : Ideal R), (Ideal.map f I).minimalPrimes = Ideal.map f '' (I ⊔ RingHom.ker f).minimalPrimes
-- Mathlib.Topology.Separation.Basic
Ne.nhdsWithin_sdiff_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x y : X},
  x ≠ y → ∀ (s : Set X), nhdsWithin x (s \ {y}) = nhdsWithin x s
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.bind : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] {β γ : Type u_6} {f : α → Part β} {g : α → β → Part γ},
  OmegaCompletePartialOrder.ωScottContinuous f →
    OmegaCompletePartialOrder.ωScottContinuous g → OmegaCompletePartialOrder.ωScottContinuous fun x => f x >>= g x
-- Lean.Util.PPExt
Lean.pp.raw.showInfo : Lean.Option Bool
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.isClosed_eball_top`. -/
EMetric.isClosed_ball_top : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, IsClosed (Metric.eball x ⊤)
-- Init.Data.Nat.Gcd
Nat.gcd_left_comm : ∀ (m n k : ℕ), m.gcd (n.gcd k) = n.gcd (m.gcd k)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.eapprox.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α],
  MeasureTheory.SimpleFunc.eapprox = MeasureTheory.SimpleFunc.approx MeasureTheory.SimpleFunc.ennrealRatEmbed
-- Init.Data.Range.Polymorphic.Iterators
Std.Roo.Internal.iter.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (r : Std.Roo α),
  Std.Roo.Internal.iter r = { internalState := { next := Std.PRange.succ? r.lower, upperBound := r.upper } }
-- Init.Data.Ord.Basic
Ordering.isGE_eq_isGT_or_isEq : ∀ {o : Ordering}, o.isGE = (o.isGT || o.isEq)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget.mk.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {combined lw rw : ℕ}
  (lhs lhs_1 : aig.RefVec lw),
  lhs = lhs_1 →
    ∀ (rhs rhs_1 : aig.RefVec rw),
      rhs = rhs_1 →
        ∀ (h : combined = rw + lw),
          { lw := lw, rw := rw, lhs := lhs, rhs := rhs, h := h } =
            { lw := lw, rw := rw, lhs := lhs_1, rhs := rhs_1, h := h }
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.ofPred_subset_ofPred`. -/
Set.setOf_subset_setOf : ∀ {α : Type u} {p q : α → Prop}, {a | p a} ⊆ {a | q a} ↔ ∀ (a : α), p a → q a
-- Std.Http.Data.URI.Encoding
/-- Creates an `EncodedQueryString` from a `String`, panicking if the string is not a valid percent-encoded string.
 -/
Std.Http.URI.EncodedQueryString.ofString! : String → (r : optParam (UInt8 → Bool) Std.Http.Internal.Char.isQueryChar) → Std.Http.URI.EncodedQueryString r
-- Mathlib.AlgebraicGeometry.Restrict
/-- Restricting a morphism onto the image of an open immersion is isomorphic to the base change
along the immersion.  -/
AlgebraicGeometry.morphismRestrictOpensRange : {X Y U : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (g : U ⟶ Y) →
      [inst : AlgebraicGeometry.IsOpenImmersion g] →
        CategoryTheory.Arrow.mk (f ∣_ AlgebraicGeometry.Scheme.Hom.opensRange g) ≅
          CategoryTheory.Arrow.mk (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Order.Filter.Prod
Filter.prod_pure_pure : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β}, pure a ×ˢ pure b = pure (a, b)
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Stream.forIn.loop : {β : Type} → (Std.Http.Chunk → β → Std.Async.Async (ForInStep β)) → Std.Http.Body.Stream → β → Std.Async.Async β
-- Mathlib.CategoryTheory.Limits.Creates
/-- Transfer creation of colimits along a natural isomorphism in the diagram.  -/
CategoryTheory.createsColimitOfIsoDiagram : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K₁ K₂ : CategoryTheory.Functor J C} →
              (F : CategoryTheory.Functor C D) →
                (K₁ ≅ K₂) → [CategoryTheory.CreatesColimit K₁ F] → CategoryTheory.CreatesColimit K₂ F
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.a_zero : ∀ {n : ℕ}, QuaternionGroup.a 0 = 1
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- An array of matrix entry `Expr`s`  -/
Mathlib.Tactic.Determinant.Ctx.arrayEntries : {u : Lean.Level} → {α : Q(Type u)} → {rα : Q(CommRing «$α»)} → Mathlib.Tactic.Determinant.Ctx rα → Array Q(«$α»)
-- Mathlib.LinearAlgebra.Coevaluation
coevaluation.congr_simp : ∀ (K : Type u) [inst : Field K] (V : Type v) [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V], coevaluation K V = coevaluation K V
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₁_fst : ∀ (X : TopCat),
  CategoryTheory.CategoryStruct.comp TopCat.ι₁ (CategoryTheory.SemiCartesianMonoidalCategory.fst X TopCat.I) =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.isFlat_iff_isClosed : ∀ {α : Type u_2} {M : Matroid α} {F : Set α}, M.IsFlat F ↔ ∃ (h : F ⊆ M.E), M.subtypeClosure.IsClosed ⟨F, h⟩
-- Mathlib.Data.FinEnum
FinEnum.instUnique : {α : Type u} → [Unique α] → Unique (FinEnum α)
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.killCompl.congr_simp : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f f_1 : σ → τ} (e_f : f = f_1)
  (hf : Function.Injective f), MvPolynomial.killCompl hf = MvPolynomial.killCompl ⋯
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.toList_rio : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.toList_rio._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet.Raw α cmp},
  t.WF →
    ∀ {bound : α},
      Std.Slice.toList (Std.Rio.Sliceable.mkSlice t *...bound) = List.filter (fun e => (cmp e bound).isLT) t.toList
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_zpow : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (x : ↥H) (n : ℤ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `FunLike.coe_add`. -/
GroupSeminorm.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.mk.injEq : ∀ (toLinOrd : LinOrd) [nonempty : Nonempty ↑toLinOrd] [fintype : Fintype ↑toLinOrd] (toLinOrd_1 : LinOrd)
  (nonempty_1 : Nonempty ↑toLinOrd_1) (fintype_1 : Fintype ↑toLinOrd_1),
  ({ toLinOrd := toLinOrd, nonempty := nonempty, fintype := fintype } =
      { toLinOrd := toLinOrd_1, nonempty := nonempty_1, fintype := fintype_1 }) =
    (toLinOrd = toLinOrd_1 ∧ fintype ≍ fintype_1)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
integralClosure.AlgebraIsIntegral : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.IsIntegral R ↥(integralClosure R A)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_of_not_prime : ∀ (n p : ℕ), ¬Nat.Prime p → n / p ^ n.factorization p = n
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.lt_of_eq_of_lt : ∀ {α : Type u} [inst : Semiring α] [inst_1 : PartialOrder α] {a b : α}, a = 0 → b < 0 → a + b < 0
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor_obj_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) (K : HomologicalComplex C c),
  ((HomologicalComplex.shortComplexFunctor C c i).obj K).f = K.d (c.prev i) i
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzOnWith.div : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E} {s : Set α},
  LipschitzOnWith Kf f s → LipschitzOnWith Kg g s → LipschitzOnWith (Kf + Kg) (fun x => f x / g x) s
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonInitializeParams : Lean.FromJson Lean.Lsp.InitializeParams