mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Equivalence.map_projective_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : C ≌ D) (P : C), CategoryTheory.Projective (F.functor.obj P) ↔ CategoryTheory.Projective P
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid.eq_1 : ∀ (x : ℝ), x.sigmoid = (1 + Real.exp (-x))⁻¹
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.restrict_restrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) (V : X.Opens)
  (hV : Dense ↑V) (hV' : V ≤ U), (f.restrict U hU hU').restrict V hV hV' = f.restrict V hV ⋯
-- Mathlib.Algebra.Polynomial.Reverse
/-- We prefer to use the bundled `revAt` over unbundled `revAtFun`.  -/
Polynomial.revAtFun_eq : ∀ (N i : ℕ), Polynomial.revAtFun N i = (Polynomial.revAt N) i
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Γ'.consₗ : Turing.PartrecToTM2.Γ'
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabInclude : Lean.Elab.Command.CommandElab
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.IsAnd.mk : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs} {Q₁ Q₂ : outParam (Std.Do.SPred σs)},
  (P ⊣⊢ₛ Q₁ ∧ Q₂) → Std.Do.SPred.Tactic.IsAnd P Q₁ Q₂
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.preservesColimit_iff : ∀ {J : Type u_1} {C : Type u_3} (K : Type u_5) [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} J] [inst_2 : CategoryTheory.Category.{v_5, u_3} C]
  (F : CategoryTheory.Functor K J) (G : CategoryTheory.Functor J C),
  CategoryTheory.ObjectProperty.preservesColimit F G ↔ CategoryTheory.Limits.PreservesColimit F G
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_commutes : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R], ↑r * a = a * ↑r
-- Init.Data.SInt.Lemmas
Int64.add_right_neg : ∀ (a : Int64), a + -a = 0
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.mk.sizeOf_spec : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_4 : SizeOf ι] [inst_5 : SizeOf A]
  [inst_6 : SizeOf B] [inst_7 : SizeOf σ] [inst_8 : SizeOf τ] (toRingHom : A →+* B)
  (map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → toRingHom x ∈ ℬ i),
  sizeOf { toRingHom := toRingHom, map_mem := map_mem } = 1 + sizeOf toRingHom
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.mem_cons_of_mem : ∀ {α : Type u} {s : Stream'.WSeq α} (b : α) {a : α}, a ∈ s → a ∈ Stream'.WSeq.cons b s
-- Init.Data.Array.Extract
Array.getElem?_extract_of_lt : ∀ {α : Type u_1} {as : Array α} {i j k : ℕ} (h : k < min j as.size - i), (as.extract i j)[k]? = some as[i + k]
-- Mathlib.Data.Finset.Union
Finset.bind_toFinset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] (s : Multiset α) (t : α → Multiset β),
  (s.bind t).toFinset = s.toFinset.biUnion fun a => (t a).toFinset
-- Aesop.RuleSet
Aesop.LocalRuleSet.constForwardRuleMatches : Aesop.LocalRuleSet → Array Aesop.ForwardRuleMatch
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
MaximalSpectrum.mapPiLocalization_comp : ∀ {R : Type u_1} {S : Type u_2} (P : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring P] (f : R →+* S) (g : S →+* P) (hf : Function.Bijective ⇑f) (hg : Function.Bijective ⇑g),
  MaximalSpectrum.mapPiLocalization (g.comp f) ⋯ =
    (MaximalSpectrum.mapPiLocalization g hg).comp (MaximalSpectrum.mapPiLocalization f hf)
-- Mathlib.Util.Notation3
Mathlib.Notation3.MatchState.mk.sizeOf_spec : ∀ (vars : Std.HashMap Lean.Name (Lean.SubExpr × Lean.LocalContext × Lean.LocalInstances))
  (scopeState : Option (Array (Lean.TSyntax `Batteries.ExtendedBinder.extBinderParenthesized)))
  (foldState : Std.HashMap Lean.Name (Array Lean.Term)),
  sizeOf { vars := vars, scopeState := scopeState, foldState := foldState } =
    1 + sizeOf vars + sizeOf scopeState + sizeOf foldState
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.desc.multicofork_π_one : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁),
  (SSet.horn₃₂.desc.multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).π ⟨1, SSet.horn₃₂.desc.multicofork_π_one._proof_1⟩ =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso 1).inv f₁
-- Mathlib.Condensed.Discrete.Module
CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf : (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology CompHaus) (Type (u + 1))).Faithful
-- Init.MethodSpecsSimp
Mul.mul_eq_smul : ∀ {α : Type u_1} [inst : Mul α], Mul.mul = SMul.smul
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.RightAdjointCommShift.iso_inv_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] (a b : A) (h : b + a = 0) [inst_5 : F.CommShift A] (Y : D) {Z : C}
  (h_1 : G.obj ((CategoryTheory.shiftFunctor D a).obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a).inv.app Y) h_1 =
    CategoryTheory.CategoryStruct.comp (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj (G.obj Y)))
      (CategoryTheory.CategoryStruct.comp
        (G.map
          ((CategoryTheory.shiftFunctorCompIsoId D b a h).inv.app
            (F.obj ((CategoryTheory.shiftFunctor C a).obj (G.obj Y)))))
        (CategoryTheory.CategoryStruct.comp
          (G.map
            ((CategoryTheory.shiftFunctor D a).map
              ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).hom.app (G.obj Y)))))
          (CategoryTheory.CategoryStruct.comp
            (G.map
              ((CategoryTheory.shiftFunctor D a).map
                ((CategoryTheory.shiftFunctorCompIsoId D a b ⋯).hom.app (F.obj (G.obj Y)))))
            (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.shiftFunctor D a).map (adj.counit.app Y)))
              h_1))))
-- Init.Data.Char.Lemmas
Char.lt_def : ∀ {a b : Char}, a < b ↔ a.val < b.val
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Two equal maps on scalars give rise to an equivariant map for identity  -/
AddActionHom.ofEq : {M : Type u_2} →
  {N : Type u_3} →
    {φ : M → N} →
      {X : Type u_5} →
        [inst : VAdd M X] → {Y : Type u_6} → [inst_1 : VAdd N Y] → {φ' : M → N} → φ = φ' → (X →ₑ[φ] Y) → X →ₑ[φ'] Y
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_one_add : ∀ (f : CircleDeg1Lift) (x : ℝ), f (1 + x) = 1 + f x
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Iio_succ_eq_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : SuccOrder α] [NoMaxOrder α]
  (b : α), Finset.Iio (Order.succ b) = Finset.Iic b
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.mk_le_mk : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x y : R) (t s : ↥(ValuativeRel.posSubmonoid R)),
  ValuativeRel.ValueGroupWithZero.mk x t ≤ ValuativeRel.ValueGroupWithZero.mk y s ↔ x * ↑s ≤ᵥ y * ↑t
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The open cells are pairwise disjoint. Use `CWComplex.pairwiseDisjoint` or
`CWComplex.disjoint_openCell_of_ne` instead.  -/
Topology.CWComplex.pairwiseDisjoint' : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} [self : Topology.CWComplex C],
  Set.univ.PairwiseDisjoint fun ni => ↑(Topology.CWComplex.map ni.fst ni.snd) '' Metric.ball 0 1
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- If `{ xᵢ }` are homogeneous and span `A` as an `A₀` algebra, then `D₊(xᵢ)` covers `Proj A`.  -/
AlgebraicGeometry.Proj.iSup_basicOpen_eq_top' : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {ι : Type u_2} (f : ι → A),
  (∀ (i : ι), ∃ n, f i ∈ 𝒜 n) →
    Algebra.adjoin (↥(𝒜 0)) (Set.range f) = ⊤ → ⨆ i, AlgebraicGeometry.Proj.basicOpen 𝒜 (f i) = ⊤
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity follows from pairwise scaled non-negative distance. Backward direction of
`similar_iff_exists_pairwise_nndist_eq`.  -/
Similar.of_exists_pairwise_nndist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  (∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ => nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)) → Similar v₁ v₂
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.of_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace Y]
  [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace Z],
  Continuous f → Continuous g → Topology.IsInducing (g ∘ f) → Topology.IsInducing f
-- Init.Data.String.Basic
String.Slice.Pos.offset_copy : ∀ {s : String.Slice} {pos : s.Pos}, pos.copy.offset = pos.offset
-- Mathlib.Topology.Algebra.Module.IsWeak
/-- Typeclass expressing that the topology on `E` is the weak topology induced
by the bilinear form `B`.  -/
LinearMap.IsWeak : {𝕜 : Type u_2} →
  {E : Type u_3} →
    {F : Type u_4} →
      [inst : CommSemiring 𝕜] →
        [TopologicalSpace 𝕜] →
          [inst_2 : AddCommMonoid E] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : AddCommMonoid F] → [inst_5 : Module 𝕜 F] → [t : TopologicalSpace E] → (E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → Prop
-- Mathlib.Order.Category.BddOrd
BddOrd.isBoundedOrder : (self : BddOrd) → BoundedOrder ↑self.toPartOrd
-- Init.Data.UInt.Basic
instDivUInt32 : Div UInt32
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom_assoc : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) (d : D) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).hom d)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) c d).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso
            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)).hom
        h)
-- Init.Data.Bool
Bool.ite_eq_false_distrib : ∀ (p : Prop) [h : Decidable p] (t f : Bool), ((if p then t else f) = false) = if p then t = false else f = false
-- Mathlib.Algebra.Polynomial.Div
Polynomial.degree_modByMonic_lt : ∀ {R : Type u} [inst : Ring R] [Nontrivial R] (p : Polynomial R) {q : Polynomial R},
  q.Monic → (p %ₘ q).degree < q.degree
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.mul_card_image_le_card_of_maps_to : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
  (∀ a ∈ s, f a ∈ t) → ∀ (n : ℕ), (∀ b ∈ t, n ≤ {a ∈ s | f a = b}.card) → n * t.card ≤ s.card
-- Mathlib.Data.Num.Lemmas
PosNum.one_add : ∀ (n : PosNum), 1 + n = n.succ
-- Mathlib.FieldTheory.Galois.Basic
/-- If `K / k` is a Galois extension, `L` is an intermediate field of `K / k`, then `[L : k]`
as a natural number is equal to the index of the fixing subgroup of `L`.  -/
IntermediateField.finrank_eq_fixingSubgroup_index : ∀ {F : Type u_1} (E' : Type u_3) [inst : Field F] [inst_1 : Field E'] [inst_2 : Algebra F E']
  (L : IntermediateField F E') [IsGalois F E'], Module.finrank F ↥L = L.fixingSubgroup.index
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.smul_def : ∀ {R : Type u_1} {ι : 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 ι]
  [inst_4 : (i : ι) → SMul R (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] (i : ι)
  (x : G i) (r : R), r • ⟦⟨i, x⟩⟧ = ⟦⟨i, r • x⟩⟧
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.verifyBVExpr.eq_1 : ∀ (bv : Std.Tactic.BVDecide.BVLogicalExpr) (cert : String),
  Std.Tactic.BVDecide.Reflect.verifyBVExpr bv cert =
    Std.Tactic.BVDecide.Reflect.verifyCert (Std.Sat.AIG.toCNF bv.bitblast.relabelNat) cert
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instNatCast : {α : Type u} →
  [inst : TopologicalSpace α] →
    {β : Type u_2} → [inst_1 : PseudoMetricSpace β] → [NatCast β] → NatCast (BoundedContinuousFunction α β)
-- Mathlib.RingTheory.Regular.IsSMulRegular
isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  (r : R), IsSMulRegular (↥N) r ↔ Disjoint ((LinearMap.lsmul R M) r).ker N
-- Lean.Parser.Syntax
Lean.Parser.Command.elab : Lean.Parser.Parser
-- Mathlib.MeasureTheory.Group.AEStabilizer
MeasureTheory.neg_vadd_ae_eq_self : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {x_1 : G} {s : Set α},
  x_1 +ᵥ s =ᵐ[μ] s → -x_1 +ᵥ s =ᵐ[μ] s
-- Mathlib.Analysis.RCLike.Basic
RCLike.toAlgHom_ofRealStarAlgHom : ∀ {K : Type u_1} [inst : RCLike K], ↑(RCLike.ofRealStarAlgHom K) = RCLike.ofRealAm
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Add a lazy entry to an existing trie.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.addLazyEntryToTrie : {α : Type} →
  Lean.Meta.RefinedDiscrTree.TrieIndex →
    Lean.Meta.RefinedDiscrTree.LazyEntry × α → Lean.Meta.RefinedDiscrTree.TreeM✝ α Unit
-- Mathlib.Data.List.Sort
List.Subset.antisymm_of_pairwise : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Antisymm r] [Std.Irrefl r] {l₁ l₂ : List α},
  List.Pairwise r l₁ → List.Pairwise r l₂ → l₁ ⊆ l₂ → l₂ ⊆ l₁ → l₁ = l₂
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_unique : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Unique α], Finset.univ = {default}
-- Lean.Meta.RecursorInfo
_private.Lean.Meta.RecursorInfo.0.Lean.Meta.checkMotive : Lean.Name → Lean.Expr → Array Lean.Expr → Lean.MetaM Unit
-- Lean.Meta.Tactic.Grind.ProveEq
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.abstractGroundMismatches?.go : Lean.Expr → Lean.Expr → Lean.Meta.Grind.AbstractM✝ Lean.Expr
-- Aesop.RuleTac.RuleTerm
Aesop.RuleTerm : Type
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_alter!_of_compare_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      compare k k' = Ordering.eq → (k' ∈ Std.DTreeMap.Internal.Impl.alter! k f t ↔ (f (t.get? k)).isSome = true)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.instEmptyCollection : EmptyCollection Batteries.UnionFind
-- Lean.Meta.Tactic.Grind.ReflCmp
/-- If `op` implements `ReflCmp`, then returns the proof term for
`∀ a b, a = b → op a b = .eq`
 -/
Lean.Meta.Grind.getReflCmpThm? : Lean.Expr → Lean.Meta.Grind.GrindM (Option Lean.Expr)
-- Mathlib.Order.RelClasses
/-- Set notation form of `LT.lt.not_ge` -/
LT.lt.not_superset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊂ b → ¬b ⊆ a
-- Lean.Environment
_private.Lean.Environment.0.Lean.mkInitialExtensionStates : IO (Array Lean.EnvExtensionState)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer reflection of limits along an equivalence in the shape.  -/
CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv : ∀ {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] {J' : Type w₂}
  [inst_3 : CategoryTheory.Category.{w₂', w₂} J'] (e : J ≌ J') (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.ReflectsLimitsOfShape J F], CategoryTheory.Limits.ReflectsLimitsOfShape J' F
-- Mathlib.Topology.Order.OrderClosed
nhds_inf_atTop : ∀ {α : Type u} [inst : Preorder α] [NoTopOrder α] [inst_2 : TopologicalSpace α] [ClosedIciTopology α] (a : α),
  nhds a ⊓ Filter.atTop = ⊥
-- Mathlib.Algebra.Order.Monoid.Associated
Associates.instIsOrderedMonoid : ∀ {M : Type u_1} [inst : CommMonoidWithZero M], IsOrderedMonoid (Associates M)
-- Mathlib.GroupTheory.PGroup
IsPGroup.of_bot : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], IsPGroup p ↥⊥
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map₀_algebraMap : ∀ {R : Type u_1} {ι : 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 ι] [inst_4 : Nonempty ι]
  [inst_5 : CommSemiring R] [inst_6 : (i : ι) → Semiring (G i)] [inst_7 : (i : ι) → Algebra R (G i)]
  [∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] (i : ι) (r : R),
  (DirectLimit.map₀ f fun i => (algebraMap R (G i)) r) = ⟦⟨i, (algebraMap R (G i)) r⟩⟧
-- Mathlib.RingTheory.Flat.Equalizer
_private.Mathlib.RingTheory.Flat.Equalizer.0.instAddHomClassAlgHom : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_4} {B : Type u_5} [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B], AddHomClass (A →ₐ[R] B) A B
-- Mathlib.Data.Finset.Empty
Finset.forall_mem_empty_iff : ∀ {α : Type u_1} (p : α → Prop), (∀ x ∈ ∅, p x) ↔ True
-- Init.Data.Array.Lex.Lemmas
Array.le_trans' : ∀ {α : Type u_1} [inst : LT α] [i₁ : Std.Asymm fun x1 x2 => x1 < x2] [i₂ : Std.Trichotomous fun x1 x2 => x1 < x2]
  [i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2] {xs ys zs : Array α},
  xs ≤ ys → ys ≤ zs → xs ≤ zs
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.volume_Ioo : ∀ (x y : ↑unitInterval), MeasureTheory.volume (Set.Ioo x y) = ENNReal.ofReal (↑y - ↑x)
-- Mathlib.NumberTheory.MulChar.Lemmas
MulChar.ofRootOfUnity.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : Fintype M] [inst_2 : DecidableEq M] {R : Type u_2}
  [inst_3 : CommMonoidWithZero R] {ζ : Rˣ} (hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R) {g : Mˣ}
  (hg : ∀ (x : Mˣ), x ∈ Subgroup.zpowers g),
  MulChar.ofRootOfUnity hζ hg = MulChar.ofUnitHom (monoidHomOfForallMemZpowers hg ⋯)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_erase_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).size ≤ t.size
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Equivariant monoid homomorphisms.  -/
«MulDistribMulActionHomIdLocal≺» : Lean.TrailingParserDescr
-- Mathlib.Data.Nat.Nth
Nat.nth_le_nth_of_lt_card : ∀ {p : ℕ → Prop} (hf : (Set.ofPred p).Finite) {m n : ℕ}, m ≤ n → n < hf.toFinset.card → Nat.nth p m ≤ Nat.nth p n
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.ι_coproductUniqueIso_hom_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C) (b : β) {Z : C}
  (h : f default ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coproductUniqueIso f).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
-- Mathlib.Combinatorics.Additive.CovBySMul
CovBySMul.subset_left : ∀ {M : Type u_1} {X : Type u_3} [inst : Monoid M] [inst_1 : MulAction M X] {K : ℝ} {A₁ A₂ B : Set X},
  A₁ ⊆ A₂ → CovBySMul M K A₂ B → CovBySMul M K A₁ B
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_bind_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.minKey?.bind t.getKey? = t.minKey?
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
/-- Lemma 3.3 (a) from [Geck](Geck2017).  -/
RootPairing.GeckConstruction.lie_h_e : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : IsDomain R] [inst_3 : CharZero R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {b : P.Base} [inst_9 : Fintype ι]
  (i j : ↥b.support),
  ⁅RootPairing.GeckConstruction.h j, RootPairing.GeckConstruction.e i⁆ =
    b.cartanMatrix i j • RootPairing.GeckConstruction.e i
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.coeffs_map : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (p : MvPolynomial σ R) [inst_2 : DecidableEq S₁], ((MvPolynomial.map f) p).coeffs ⊆ Finset.image (⇑f) p.coeffs
-- Lean.ResolveName
/-- Interprets the syntax `n` as an identifier for a global constant, and return a resolved
constant name. If there are multiple possible interpretations it will throw.

Consider using `realizeGlobalConstNoOverload` if you need to handle reserved names, and
`realizeGlobalConstNoOverloadWithInfo` if you
want the syntax to show the resulting name's info on hover.

## Example:
```
def Boo.x   := 1
def Foo.x   := 2
def Foo.x.y := 3
```
After `open Foo`, we have
- `resolveGlobalConstNoOverload x`     => `Foo.x`
- `resolveGlobalConstNoOverload x.y`   => `Foo.x.y`
- `resolveGlobalConstNoOverload x.z.w` => error: unknown constant

After `open Foo open Boo`, we have
- `resolveGlobalConstNoOverload x`     => error: ambiguous identifier
- `resolveGlobalConstNoOverload x.y`   => `Foo.x.y`
- `resolveGlobalConstNoOverload x.z.w` => error: unknown constant
 -/
Lean.resolveGlobalConstNoOverload : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadError m] → Lean.Syntax → m Lean.Name
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
/-- A morphism is proper if it is separated, universally closed and locally of finite type.  -/
AlgebraicGeometry.IsProper : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.instCountableSymbolsConstantsOn : ∀ {α : Type u'} [Countable α], Countable (FirstOrder.Language.constantsOn α).Symbols
-- Mathlib.Data.Matrix.Basic
Matrix.algebraMap_eq_diagonal : ∀ {n : Type u_3} {R : Type u_7} {α : Type u_11} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  [inst_3 : Semiring α] [inst_4 : Algebra R α] (r : R),
  (algebraMap R (Matrix n n α)) r = Matrix.diagonal ((algebraMap R (n → α)) r)
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instSubtractionMonoid : {α : Type u_1} → [SubtractionMonoid α] → SubtractionMonoid αᵃᵒᵖ
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.map_id_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat},
  CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.id F) =
    CategoryTheory.Functor.id (CategoryTheory.Grothendieck F)
-- Std.Http.Data.Body.Stream
/-- Gets the known size if available.
 -/
Std.Http.Body.Stream.getKnownSize : Std.Http.Body.Stream → Std.Async.Async (Option Std.Http.Body.Length)