mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiFamilyStruct.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B : C} {α : Type u_2} {X : α → C}
  {π : (a : α) → X a ⟶ B}
  (desc :
    {W : C} →
      (e : (a : α) → X a ⟶ W) →
        (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
            CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
              CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) →
          (B ⟶ W))
  (fac :
    ∀ {W : C} (e : (a : α) → X a ⟶ W)
      (h :
        ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
          CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
            CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
      (a : α), CategoryTheory.CategoryStruct.comp (π a) (desc e ⋯) = e a)
  (uniq :
    ∀ {W : C} (e : (a : α) → X a ⟶ W)
      (h :
        ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
          CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
            CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
      (m : B ⟶ W), (∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) → m = desc e ⋯)
  (desc_1 :
    {W : C} →
      (e : (a : α) → X a ⟶ W) →
        (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
            CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
              CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) →
          (B ⟶ W))
  (fac_1 :
    ∀ {W : C} (e : (a : α) → X a ⟶ W)
      (h :
        ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
          CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
            CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
      (a : α), CategoryTheory.CategoryStruct.comp (π a) (desc_1 e ⋯) = e a)
  (uniq_1 :
    ∀ {W : C} (e : (a : α) → X a ⟶ W)
      (h :
        ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
          CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
            CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
      (m : B ⟶ W), (∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) → m = desc_1 e ⋯),
  ({ desc := desc, fac := fac, uniq := uniq } = { desc := desc_1, fac := fac_1, uniq := uniq_1 }) = (desc = desc_1)
-- Aesop.Tree.Data
Aesop.RappData.mk.inj : ∀ {Goal MVarCluster : Type} {id : Aesop.RappId} {parent : IO.Ref Goal} {children : Array (IO.Ref MVarCluster)}
  {state : Aesop.NodeState} {isIrrelevant : Bool} {appliedRule : Aesop.RegularRule}
  {scriptSteps? : Option (Array Aesop.Script.LazyStep)} {originalSubgoals : Array Lean.MVarId}
  {successProbability : Aesop.Percent} {metaState : Lean.Meta.SavedState}
  {introducedMVars assignedMVars : Aesop.UnorderedArraySet Lean.MVarId} {id_1 : Aesop.RappId} {parent_1 : IO.Ref Goal}
  {children_1 : Array (IO.Ref MVarCluster)} {state_1 : Aesop.NodeState} {isIrrelevant_1 : Bool}
  {appliedRule_1 : Aesop.RegularRule} {scriptSteps?_1 : Option (Array Aesop.Script.LazyStep)}
  {originalSubgoals_1 : Array Lean.MVarId} {successProbability_1 : Aesop.Percent} {metaState_1 : Lean.Meta.SavedState}
  {introducedMVars_1 assignedMVars_1 : Aesop.UnorderedArraySet Lean.MVarId},
  { id := id, parent := parent, children := children, state := state, isIrrelevant := isIrrelevant,
        appliedRule := appliedRule, scriptSteps? := scriptSteps?, originalSubgoals := originalSubgoals,
        successProbability := successProbability, metaState := metaState, introducedMVars := introducedMVars,
        assignedMVars := assignedMVars } =
      { id := id_1, parent := parent_1, children := children_1, state := state_1, isIrrelevant := isIrrelevant_1,
        appliedRule := appliedRule_1, scriptSteps? := scriptSteps?_1, originalSubgoals := originalSubgoals_1,
        successProbability := successProbability_1, metaState := metaState_1, introducedMVars := introducedMVars_1,
        assignedMVars := assignedMVars_1 } →
    id = id_1 ∧
      parent = parent_1 ∧
        children = children_1 ∧
          state = state_1 ∧
            isIrrelevant = isIrrelevant_1 ∧
              appliedRule = appliedRule_1 ∧
                scriptSteps? = scriptSteps?_1 ∧
                  originalSubgoals = originalSubgoals_1 ∧
                    successProbability = successProbability_1 ∧
                      metaState = metaState_1 ∧ introducedMVars = introducedMVars_1 ∧ assignedMVars = assignedMVars_1
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.preimage_coe_Ico_top : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some ⁻¹' Set.Ico ↑a ⊤ = Set.Ici a
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.hom_ext_iff : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_4} [inst_3 : Semiring A] [inst_4 : Algebra R A] {f g : CliffordAlgebra Q →ₐ[R] A},
  f = g ↔ f.toLinearMap ∘ₗ CliffordAlgebra.ι Q = g.toLinearMap ∘ₗ CliffordAlgebra.ι Q
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.instFinite : ∀ {α : Type u} {β : α → Type v}, Std.Iterators.Finite (Std.DTreeMap.Internal.Zipper α β) Id
-- Mathlib.Data.List.Sym
List.sym_map : ∀ {α : Type u_1} {β : Type u_3} (f : α → β) (n : ℕ) (xs : List α),
  List.sym n (List.map f xs) = List.map (Sym.map f) (List.sym n xs)
-- Mathlib.Order.SymmDiff
le_symmDiff_iff_left : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b : α), a ≤ symmDiff a b ↔ Disjoint a b
-- Mathlib.Algebra.QuadraticDiscriminant
/-- A quadratic has roots if and only if its discriminant equals some square.
 -/
quadratic_eq_zero_iff_discrim_eq_sq : ∀ {R : Type u_1} [inst : CommRing R] {a b c : R} [NeZero 2] [NoZeroDivisors R],
  a ≠ 0 → ∀ (x : R), a * (x * x) + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2
-- Mathlib.Topology.UnitInterval
/-- The unit interval as a submonoid of ℝ.  -/
unitInterval.submonoid : Submonoid ℝ
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isSheafFor_over_map_op_comp_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B B' : C} (p : B ⟶ B')
  (P : CategoryTheory.Functor (CategoryTheory.Over B')ᵒᵖ (Type w)) {X : CategoryTheory.Over B}
  (R : CategoryTheory.Sieve X) {X' : CategoryTheory.Over B'} (e : (CategoryTheory.Over.map p).obj X ≅ X'),
  CategoryTheory.Presieve.IsSheafFor ((CategoryTheory.Over.map p).op.comp P) R.arrows ↔
    CategoryTheory.Presieve.IsSheafFor P
      (CategoryTheory.Sieve.pullback e.inv
          (CategoryTheory.Sieve.functorPushforward (CategoryTheory.Over.map p) R)).arrows
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_lt_rpow_of_exponent_gt : ∀ {x : ENNReal} {y z : ℝ}, 0 < x → x < 1 → z < y → x ^ y < x ^ z
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
Group.existsMulOfLE : ∀ (α : Type u) [inst : Group α] [inst_1 : LE α], ExistsMulOfLE α
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.mul_val_succ : ∀ {α : Type u} {m : ℕ} {n' : Type uₙ} {o' : Type uₒ} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n']
  (A : Matrix (Fin m.succ) n' α) (B : Matrix n' o' α) (i : Fin m) (j : o'),
  (A * B) i.succ j = (Matrix.of (Matrix.vecTail (Matrix.of.symm A)) * B) i j
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isUnitSubmonoid_eq_nonZeroDivisorsRight : ∀ (R : Type u_1) [inst : Ring R] [IsArtinianRing R], IsUnit.submonoid R = nonZeroDivisorsRight R
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateMulAct.instMulAction : {α : Type u_1} → {f : α → α} → MulAction (IterateMulAct f) α
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.Nonempty.smul_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset β} {a : α},
  s.Nonempty → (a • s).Nonempty
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.Context.mk.inj : ∀ {insideType insideType_1 : Bool},
  { insideType := insideType } = { insideType := insideType_1 } → insideType = insideType_1
-- Mathlib.Data.Fintype.BigOperators
Finset.prod_toFinset_eq_subtype : ∀ {α : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Fintype α] (p : α → Prop) [inst_2 : DecidablePred p]
  (f : α → M), ∏ a ∈ {x | p x}.toFinset, f a = ∏ a, f ↑a
-- Lean.Data.Lsp.Extra
/-- `$/lean/plainTermGoal` client->server request.

Returns the expected type at the specified position, pretty-printed as a string.  -/
Lean.Lsp.PlainTermGoalParams : Type
-- Init.Data.Vector.Lemmas
Vector.mk_toArray : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, Vector.mk xs.toArray ⋯ = xs
-- Mathlib.RingTheory.Unramified.Finite
Algebra.FormallyUnramified.one_tmul_sub_tmul_one_mul_elem : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Algebra.FormallyUnramified R S] [inst_4 : Algebra.EssFiniteType R S] (s : S),
  (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * Algebra.FormallyUnramified.elem R S = 0
-- Mathlib.Data.Vector.Defs
List.Vector.getElem_def : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n) (i : ℕ) {hi : i < n}, v[i] = v.toList[i]
-- Mathlib.AlgebraicGeometry.Morphisms.LocalIso
AlgebraicGeometry.IsLocalIso.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (∀ (x : ↥X), ∃ U, x ∈ U ∧ AlgebraicGeometry.IsOpenImmersion (CategoryTheory.CategoryStruct.comp U.ι f)) →
    AlgebraicGeometry.IsLocalIso f
-- Mathlib.Order.SupIndep
iSupIndep.mem_of_biSup_eq_top : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {f : ι → α} {s : Set ι},
  iSupIndep f → ⨆ i ∈ s, f i = ⊤ → ∀ {i : ι}, f i ≠ ⊥ → i ∈ s
-- Init.Data.Option.Lemmas
Option.all_eq_true_iff_get : ∀ {α : Type u_1} (p : α → Bool) (x : Option α), Option.all p x = true ↔ ∀ (h : x.isSome = true), p (x.get h) = true
-- Lean.Elab.App
/-- Elaborates the resolutions of a function. The `fns` array is the output of `resolveName'`.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.elabAppFnResolutions : Lean.Syntax →
  List (Lean.Expr × Lean.Syntax × List Lean.Syntax × List Lean.Level) →
    List Lean.Elab.Term.LVal →
      Array Lean.Elab.Term.NamedArg →
        Array Lean.Elab.Term.Arg →
          Option Lean.Expr →
            Bool →
              Bool →
                Bool →
                  Array (Lean.Elab.Term.TermElabResult Lean.Expr) →
                    optParam Bool false → Lean.Elab.TermElabM (Array (Lean.Elab.Term.TermElabResult Lean.Expr))
-- Mathlib.Algebra.Opposites
AddOpposite.op_bijective : ∀ {α : Type u_1}, Function.Bijective AddOpposite.op
-- Init.Data.String.PosRaw
String.Pos.Raw.unoffsetBy_lt_unoffsetBy_of_le_of_lt : ∀ {p₁ p₂ p₃ : String.Pos.Raw}, p₁ < p₂ → p₁ < p₃ → p₂.unoffsetBy p₃ < p₂.unoffsetBy p₁
-- Mathlib.Order.UpperLower.Basic
/-- **Alias** of `isLowerSet_setOfPred`. -/
isLowerSet_setOf : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop}, IsLowerSet {a | p a} ↔ Antitone p
-- Lean.Meta.LetToHave
/-- Finds `e` in the cache, or otherwise computes `m`.

If not in the cache, applies a cheap check to see if we can skip descending into the expression.
 -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.checkCache : Lean.Expr → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝ → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, t.isEmpty = t.toListModel.isEmpty
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblU_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R),
  W'.dblU P = W'.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W'.a₂ * P 0 * P 2 ^ 2 + W'.a₄ * P 2 ^ 4)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.intMul.injEq : ∀ (k : ℤ) (a : Lean.Grind.Linarith.Expr) (k_1 : ℤ) (a_1 : Lean.Grind.Linarith.Expr),
  (Lean.Grind.Linarith.Expr.intMul k a = Lean.Grind.Linarith.Expr.intMul k_1 a_1) = (k = k_1 ∧ a = a_1)
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Composition of `AffineIsometryEquiv`s as an `AffineIsometryEquiv`.  -/
AffineIsometryEquiv.trans : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {V₃ : Type u_6} →
        {P : Type u_10} →
          {P₂ : Type u_11} →
            {P₃ : Type u_12} →
              [inst : NormedField 𝕜] →
                [inst_1 : SeminormedAddCommGroup V] →
                  [inst_2 : NormedSpace 𝕜 V] →
                    [inst_3 : PseudoMetricSpace P] →
                      [inst_4 : NormedAddTorsor V P] →
                        [inst_5 : SeminormedAddCommGroup V₂] →
                          [inst_6 : NormedSpace 𝕜 V₂] →
                            [inst_7 : PseudoMetricSpace P₂] →
                              [inst_8 : NormedAddTorsor V₂ P₂] →
                                [inst_9 : SeminormedAddCommGroup V₃] →
                                  [inst_10 : NormedSpace 𝕜 V₃] →
                                    [inst_11 : PseudoMetricSpace P₃] →
                                      [inst_12 : NormedAddTorsor V₃ P₃] → (P ≃ᵃⁱ[𝕜] P₂) → (P₂ ≃ᵃⁱ[𝕜] P₃) → P ≃ᵃⁱ[𝕜] P₃
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.idemFst_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β] {p : ENNReal}
  (x : WithLp p (α × β)), WithLp.idemFst x = WithLp.toLp p (x.fst, 0)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagNode.mk.injEq : ∀ (origin : Lean.Meta.Grind.Origin) (proof : Lean.Expr) (origin_1 : Lean.Meta.Grind.Origin) (proof_1 : Lean.Expr),
  ({ origin := origin, proof := proof } = { origin := origin_1, proof := proof_1 }) =
    (origin = origin_1 ∧ proof = proof_1)
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.NatIso.pi_hom : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂}
  [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] {F G : (i : I) → CategoryTheory.Functor (C i) (D i)}
  (e : (i : I) → F i ≅ G i), (CategoryTheory.NatIso.pi e).hom = CategoryTheory.NatTrans.pi fun i => (e i).hom
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.abs_integral_mono_interval : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {c d : ℝ},
  Set.uIoc a b ⊆ Set.uIoc c d →
    0 ≤ᵐ[μ.restrict (Set.uIoc c d)] f →
      IntervalIntegrable f μ c d → |∫ (x : ℝ) in a..b, f x ∂μ| ≤ |∫ (x : ℝ) in c..d, f x ∂μ|
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Ordered.fill : ∀ {α : Type u_1} {cmp : α → α → Ordering} {path : RBTree.RBNode.Path α} {t : RBTree.RBNode α},
  RBTree.RBNode.Ordered cmp (path.fill t) ↔
    RBTree.RBNode.Path.Ordered cmp path ∧
      RBTree.RBNode.Ordered cmp t ∧ RBTree.RBNode.All (RBTree.RBNode.Path.RootOrdered cmp path) t
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.embDomain_of_notMem_range : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'}, b ∉ Set.range ⇑f → (HahnSeries.embDomain f x).coeff b = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects finite colimits, then `F : C ⥤ D` reflects finite limits.  -/
CategoryTheory.Limits.reflectsFiniteLimits_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFiniteColimits F.op],
  CategoryTheory.Limits.ReflectsFiniteLimits F
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- Corollary of `card_mul_finset_lt_two` in the case `A = S`, giving characterisation of sets of
doubling less than `2 - ε`.  -/
Finset.doubling_lt_two : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G} {ε : ℝ},
  0 < ε →
    ε ≤ 1 →
      A.Nonempty →
        ↑(A * A).card ≤ (2 - ε) * ↑A.card →
          ∃ H x Z, ↑(Fintype.card ↥H) ≤ (2 / ε - 1) * ↑A.card ∧ ↑Z.card ≤ 2 / ε - 1 ∧ ↑A ⊆ ↑H * ↑Z
-- Aesop.Tree.ExtractScript
Aesop.extractScript : Aesop.TreeM (Aesop.Script.UScript × Bool)
-- Lean.Meta.Tactic.Cases
Lean.Meta.ByCasesSubgoal.mk : Lean.MVarId → Lean.FVarId → Lean.Meta.ByCasesSubgoal
-- Mathlib.Topology.Semicontinuity.Defs
Semicontinuous.semicontinuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop},
  Semicontinuous r → ∀ (s : Set α), SemicontinuousOn r s
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `dist_triangle`.  -/
hammingDist_triangle : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] (x y z : (i : ι) → β i),
  hammingDist x z ≤ hammingDist x y + hammingDist y z
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyItem.kind : Lean.Lsp.CallHierarchyItem → Lean.Lsp.SymbolKind
-- Mathlib.FieldTheory.IsSepClosed
/-- If `K` is perfect and is a separable closure of `k`,
then it is also an algebraic closure of `k`.  -/
IsSepClosure.isAlgClosure_of_perfectField_top : ∀ (k : Type u) [inst : Field k] (K : Type v) [inst_1 : Field K] [inst_2 : Algebra k K] [IsSepClosure k K]
  [PerfectField K], IsAlgClosure k K
-- Mathlib.Order.Filter.ENNReal
/-- See also `limsup_mul_le'`  -/
ENNReal.limsup_mul_le : ∀ {α : Type u_1} {f : Filter α} [CountableInterFilter f] (u v : α → ENNReal),
  Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.post_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (X : CategoryTheory.StructuredArrow S F),
  (CategoryTheory.StructuredArrow.post S F G).obj X = CategoryTheory.StructuredArrow.mk (G.map X.hom)
-- Mathlib.Logic.Equiv.Basic
Equiv.coe_subtypeEquivCodomain_symm : ∀ {X : Sort u_9} {Y : Sort u_10} [inst : DecidableEq X] {x : X} (f : { x' // x' ≠ x } → Y),
  ⇑(Equiv.subtypeEquivCodomain f).symm = fun y => ⟨fun x' => if h : x' ≠ x then f ⟨x', h⟩ else y, ⋯⟩
-- Mathlib.Analysis.Complex.SqrtDeriv
Complex.deriv_sqrt : ∀ {z : ℂ}, z ∈ Complex.slitPlane → deriv Complex.sqrt z = z ^ (-1 / 2) / 2
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.instSMulCommClass : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {G : Type u_5} {G' : Type u_6} [inst_3 : Group G] [inst_4 : Group G'] [inst_5 : DistribMulAction G M]
  [inst_6 : DistribMulAction G' M] [inst_7 : SMulCommClass G R M] [inst_8 : SMulCommClass G' R M]
  [SMulCommClass G G' M], SMulCommClass G G' (Module.Basis ι R M)
-- Mathlib.FieldTheory.CardinalEmb
_private.Mathlib.FieldTheory.CardinalEmb.0.Field.Emb.Cardinal.termX_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorMk_map_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} (mor₁ : obj₁ ⟶ obj₂)
  (mor₂ : obj₂ ⟶ obj₃) (mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)) {X Y : J} (φ : X ⟶ Y),
  ((CategoryTheory.Pretriangulated.Triangle.functorMk mor₁ mor₂ mor₃).map φ).hom₁ = obj₁.map φ
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.lie_le_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  (I : LieIdeal R L), ⁅I, N⁆ ≤ N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'
-- Mathlib.Analysis.Calculus.MeanValue
eq_of_fderiv_eq : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace 𝕜 G] {E : Type u_5} [inst_4 : NormedAddCommGroup E]
  [inst_5 : NormedSpace 𝕜 E] {f g : E → G},
  Differentiable 𝕜 f → Differentiable 𝕜 g → (∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x) → ∀ (x : E), f x = g x → f = g
-- Mathlib.Data.Multiset.FinsetOps
Multiset.attach_ndinsert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α),
  (Multiset.ndinsert a s).attach = Multiset.ndinsert ⟨a, ⋯⟩ (Multiset.map (fun p => ⟨↑p, ⋯⟩) s.attach)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
/-- **Markov's inequality** also known as **Chebyshev's first inequality**.  -/
MeasureTheory.mul_meas_ge_le_lintegral₀ : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → ∀ (ε : ENNReal), ε * μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ
-- Mathlib.Data.List.ModifyLast
List.modifyLast.go.eq_def : ∀ {α : Type u_1} (f : α → α) (a : List α) (a_1 : Array α),
  List.modifyLast.go f a a_1 =
    match a, a_1 with
    | [], x => []
    | [x], acc => acc.toListAppend [f x]
    | x :: xs, acc => List.modifyLast.go f xs (acc.push x)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instSupSet : {α : Type u_1} → [inst : LE α] → SupSet (UpperSet α)
-- Lean.AddDecl
/-- If `warn.sorry` is set to true, then, so long as the message log does not already have any errors,
declarations with `sorryAx` generate the "declaration uses `sorry`" warning.  -/
Lean.warn.sorry : Lean.Option Bool
-- Mathlib.RingTheory.WittVector.MulCoeff
/-- `remainder p n` represents the remainder term from `mul_polyOfInterest_aux3`.
`wittPolyProd p (n+1)` will have variables up to `n+1`,
but `remainder` will only have variables up to `n`.
 -/
WittVector.remainder : ℕ → ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
-- Std.Data.HashMap.Lemmas
Std.HashMap.foldM_eq_foldlM_toArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : δ → α → β → m' δ} {init : δ},
  Std.HashMap.foldM f init m = Array.foldlM (fun a b => f a b.1 b.2) init m.toArray
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
/-- The `Y`-coordinate of a representative of `-P` for a projective point representative `P` on a
Weierstrass curve.  -/
WeierstrassCurve.Projective.negY : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → R
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
instContMDiffVectorBundleSomeENatTopTangentSpaceOfIsManifold : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] [h : IsManifold I (↑⊤) M],
  ContMDiffVectorBundle (↑⊤) E (TangentSpace I) I
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The morphism from the (right) homology attached to a morphism
`k : S.X₂ ⟶ A` such that `S.f ≫ k = 0`.  -/
CategoryTheory.ShortComplex.RightHomologyData.descH : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.RightHomologyData) → {A : C} → (k : S.X₂ ⟶ A) → CategoryTheory.CategoryStruct.comp S.f k = 0 → (h.H ⟶ A)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_op_iff_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.IsClosedUnderColimitsOfShape Jᵒᵖ ↔ P.op.IsClosedUnderLimitsOfShape J
-- Mathlib.LinearAlgebra.Orientation
/-- The orientations given by two bases are equal if and only if the determinant of one basis
with respect to the other is positive.  -/
Module.Basis.orientation_eq_iff_det_pos : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (e₁ e₂ : Module.Basis ι R M), e₁.orientation = e₂.orientation ↔ 0 < e₁.det ⇑e₂