mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.flattenList.match_1.eq_2 : ∀ {n : ℕ} (motive : List (BitVec n) → Sort u_1) (x : BitVec n) (rest : List (BitVec n)) (h_1 : Unit → motive [])
  (h_2 : (x : BitVec n) → (rest : List (BitVec n)) → motive (x :: rest)),
  (match x :: rest with
    | [] => h_1 ()
    | x :: rest => h_2 x rest) =
    h_2 x rest
-- Mathlib.Analysis.Complex.ValueDistribution.Cartan
_private.Mathlib.Analysis.Complex.ValueDistribution.Cartan.0.ValueDistribution.log_trailingCoeff_eq_zero_on_unitSphere : ∀ {f : ℂ → ℂ} {a : ℂ},
  0 < meromorphicOrderAt f 0 → a ∈ Metric.sphere 0 |1| → Real.log ‖meromorphicTrailingCoeffAt (fun x => f x - a) 0‖ = 0
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The normal closure of the union of sets is the join of the normal closures of each set.  -/
Subgroup.normalClosure_union : ∀ {G : Type u_5} [inst : Group G] (s t : Set G),
  Subgroup.normalClosure (s ∪ t) = Subgroup.normalClosure s ⊔ Subgroup.normalClosure t
-- Mathlib.Topology.Algebra.FilterBasis
ModuleFilterBasis.smul_right' : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (self : ModuleFilterBasis R M) (m₀ : M) {U : Set M},
  U ∈ self.sets → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ U
-- Mathlib.Topology.Homeomorph.Lemmas
/-- If `h : X → Y` is a homeomorphism, `h(s)` is compact iff `s` is.  -/
Homeomorph.isCompact_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y),
  IsCompact (⇑h '' s) ↔ IsCompact s
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rio.length_iter : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] [inst_7 : Std.Rxo.HasSize α] [Std.Rxo.LawfulHasSize α] {r : Std.Rio α},
  r.iter.length = r.size
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.filterMapWithPostcondition_eq_toIter_filterMapWithPostcondition_toIterM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} [inst_1 : Monad m]
  {f : β → Std.Iterators.PostconditionT m (Option γ)},
  Std.Iter.filterMapWithPostcondition f it = Std.IterM.filterMapWithPostcondition f it.toIterM
-- Mathlib.Logic.Nontrivial.Defs
nontrivial_iff_exists_ne : ∀ {α : Type u_1} (x : α), Nontrivial α ↔ ∃ y, y ≠ x
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns `true` if the given key is contained in the map.  -/
Std.DTreeMap.Internal.Impl.contains : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Bool
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one_assoc : ∀ {Z : CategoryTheory.ObjectProperty.FullSubcategory fun a => a.len ≤ 2}
  (h : { obj := { len := 1 }, property := SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (SimplexCategory.Truncated.δ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1
        SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2)
      (CategoryTheory.CategoryStruct.comp
        (SimplexCategory.Truncated.σ₂ 1 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2
          SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1)
        h) =
    CategoryTheory.CategoryStruct.comp
      (SimplexCategory.Truncated.σ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3
        SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4)
      (CategoryTheory.CategoryStruct.comp
        (SimplexCategory.Truncated.δ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4
          SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3)
        h)
-- Lean.Meta.Match.MVarRenaming
/-- A mapping from MVarId to MVarId  -/
Lean.Meta.MVarRenaming : Type
-- Init.Internal.Order.Lemmas
Lean.Order.SeqLeft.monotone_seqLeft : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] [LawfulMonad m] (f : γ → m α) (g : γ → m β),
  Lean.Order.monotone g → Lean.Order.monotone f → Lean.Order.monotone fun x => g x <* f x
-- Mathlib.Algebra.Group.Action.Defs
/-- Type class for actions by additive semigroups, with notation `g +ᵥ p`.

The `AddSemigroupAction G P` typeclass says that the additive semigroup `G` acts additively on a
type `P`.  More precisely this means that the action satisfies the axiom
`(g₁ + g₂) +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)`.  A mathematician might simply say that the additive semigroup
`G` acts on `P`.

For example, if `A` is an additive semigroup and `X` is a type, if a mathematician says
say "let `A` act on the set `X`" they will usually mean `[AddSemigroupAction A X]`.  -/
AddSemigroupAction : (G : Type u_9) → Type u_10 → [AddSemigroup G] → Type (max u_10 u_9)
-- Mathlib.Topology.Order.HullKernel
/-- The pair of maps `kernel` and `hull` form an antitone Galois connection between the
subsets of `T` and `α`.  -/
PrimitiveSpectrum.gc : ∀ {α : Type u_1} [inst : CompleteLattice α] {T : Set α},
  GaloisConnection (fun S => OrderDual.toDual (PrimitiveSpectrum.kernel S)) fun a =>
    PrimitiveSpectrum.hull T (OrderDual.ofDual a)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.fold.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (match RBTree.RBNode.nil with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c l v r => h_2 c l v r) =
    h_1 ()
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanShape_L : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X), data.multicospanShape.L = data.I₀
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseFromSymbols : {α : Type} → Array (String × α) → Std.Internal.Parsec.String.Parser α
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNonUnitalnonAssocSemiring : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonUnitalNonAssocSemiring R] →
      [IsTopologicalSemiring R] → NonUnitalNonAssocSemiring (SeparationQuotient R)
-- Init.Data.List.Zip
List.zipWith_map_left : ∀ {α : Type u_1} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} {l₁ : List α} {l₂ : List β} {f : α → α'}
  {g : α' → β → γ}, List.zipWith g (List.map f l₁) l₂ = List.zipWith (fun a b => g (f a) b) l₁ l₂
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.value.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.value = 1
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.brecOn_3.eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {motive_1 : Lean.PrefixTreeNode α β cmp → Sort u_1}
  {motive_2 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp → Sort u_1}
  {motive_3 : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp → Sort u_1}
  {motive_4 : (Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) → Sort u_1}
  (t : Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp)
  (F_1 : (t : Lean.PrefixTreeNode α β cmp) → t.below → motive_1 t)
  (F_2 : (t : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp) → Lean.PrefixTreeNode.below_1 t → motive_2 t)
  (F_3 :
    (t : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp) → Lean.PrefixTreeNode.below_2 t → motive_3 t)
  (F_4 :
    (t : Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) →
      Lean.PrefixTreeNode.below_3 t → motive_4 t),
  Lean.PrefixTreeNode.brecOn_3 t F_1 F_2 F_3 F_4 = F_4 t (Lean.PrefixTreeNode.brecOn_3.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Topology.Connected.LocallyConnected
isClopen_connectedComponent : ∀ {α : Type u} [inst : TopologicalSpace α] [LocallyConnectedSpace α] {x : α}, IsClopen (connectedComponent x)
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
/-- `lapMatrix_ker_basis G` is a basis of the nullspace indexed by its connected components,
the basis is made up of the functions `V → ℝ` which are `1` on the vertices of the given
connected component and `0` elsewhere.  -/
SimpleGraph.lapMatrix_ker_basis : {V : Type u_1} →
  [inst : Fintype V] →
    (G : SimpleGraph V) →
      [inst_1 : DecidableRel G.Adj] →
        [inst_2 : DecidableEq V] →
          [DecidableEq G.ConnectedComponent] →
            Module.Basis G.ConnectedComponent ℝ ↥(Matrix.toLin' (SimpleGraph.lapMatrix ℝ G)).ker
-- Mathlib.SetTheory.Ordinal.Notation
/-- Convert a natural number to an ordinal notation  -/
NONote.ofNat : ℕ → NONote
-- Mathlib.SetTheory.Ordinal.Notation
ONote.mul.eq_def : ∀ (x x_1 : ONote),
  x.mul x_1 =
    match x, x_1 with
    | ONote.zero, x => 0
    | x, ONote.zero => 0
    | o₁@h:(e₁.oadd n₁ a₁), e₂.oadd n₂ a₂ => if e₂ = 0 then e₁.oadd (n₁ * n₂) a₁ else (e₁ + e₂).oadd n₂ (o₁.mul a₂)
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.closure_le_centralizer_centralizer : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G),
  AddSubgroup.closure s ≤ AddSubgroup.centralizer ↑(AddSubgroup.centralizer s)
-- Batteries.Data.AssocList
Batteries.AssocList.mapKey.eq_2 : ∀ {α : Type u_1} {δ : Type u_2} {β : Type u_3} (f : α → δ) (a : α) (b : β) (es : Batteries.AssocList α β),
  Batteries.AssocList.mapKey f (Batteries.AssocList.cons a b es) =
    Batteries.AssocList.cons (f a) b (Batteries.AssocList.mapKey f es)
-- Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Matrix.IsHermitian.charpoly_cfc_eq : ∀ {n : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜}
  (hA : A.IsHermitian) (f : ℝ → ℝ), (cfc f A).charpoly = ∏ i, (Polynomial.X - Polynomial.C ↑(f (hA.eigenvalues i)))
-- Aesop.Tree.AddRapp
Aesop.AddRapp.mk.injEq : ∀ (toRuleApplication : Aesop.RuleApplication) (parent : Aesop.GoalRef) (appliedRule : Aesop.RegularRule)
  (successProbability : Aesop.Percent) (toRuleApplication_1 : Aesop.RuleApplication) (parent_1 : Aesop.GoalRef)
  (appliedRule_1 : Aesop.RegularRule) (successProbability_1 : Aesop.Percent),
  ({ toRuleApplication := toRuleApplication, parent := parent, appliedRule := appliedRule,
        successProbability := successProbability } =
      { toRuleApplication := toRuleApplication_1, parent := parent_1, appliedRule := appliedRule_1,
        successProbability := successProbability_1 }) =
    (toRuleApplication = toRuleApplication_1 ∧
      parent = parent_1 ∧ appliedRule = appliedRule_1 ∧ successProbability = successProbability_1)
-- Mathlib.Order.SymmDiff
compl_bihimp_self : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), bihimp aᶜ a = ⊥
-- Aesop.Rule
Aesop.UnsafeRuleInfo.successProbability : Aesop.UnsafeRuleInfo → Aesop.Percent
-- Lean.Meta.AbstractNestedProofs
/-- Abstracts the given proof into an auxiliary theorem, suitably pre-processing its type.  -/
Lean.Meta.abstractProof : {m : Type → Type} →
  [inst : Monad m] →
    [MonadLiftT Lean.MetaM m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [MonadFinally m] → Lean.Expr → optParam Bool true → optParam (Lean.Expr → m Lean.Expr) pure → m Lean.Expr
-- Mathlib.Data.Finset.Insert
Finset.consPiProd_fst : ∀ {α : Type u_1} {s : Finset α} {a : α} (f : α → Type u_3) (has : a ∉ s) (x : (i : α) → i ∈ Finset.cons a s has → f i),
  (Finset.consPiProd f has x).1 = x a ⋯
-- Mathlib.Analysis.Normed.Group.Basic
/-- The norm of a normed group as a group norm.  -/
normGroupNorm : (E : Type u_5) → [inst : NormedGroup E] → GroupNorm E
-- Mathlib.LinearAlgebra.Span.TensorProduct
Submodule.injective_tensorToSpan : ∀ {R : Type u_1} (A : Type u_2) {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  (p : Submodule R M) [Algebra.IsEpi R A] [Module.Flat R A], Function.Injective ⇑(Submodule.tensorToSpan A p)
-- Lean.Parser.Extra
Lean.Parser.ppAllowUngrouped.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.mem_think : ∀ {α : Type u} (s : Stream'.WSeq α) (a : α), a ∈ s.think ↔ a ∈ s
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.id_tsnd : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] [LawfulBitraversable t] {α β : Type u} (x : t α β),
  Bitraversable.tsnd pure x = pure x
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualLift_injective : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {W : Subspace K V},
  Function.Injective ⇑W.dualLift
-- Mathlib.Data.Finmap
Finmap.instDecidableMem : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → (s : Finmap β) → Decidable (a ∈ s)
-- Lean.Meta.Offset
/-- Quick function for converting `e` into `s + k` s.t. `e` is definitionally equal to `Nat.add s k`.
This function always succeeds in finding such `s` and `k`
(as a last resort it returns `e` and `0`).
 -/
_private.Lean.Meta.Offset.0.Lean.Meta.getOffset : Lean.Expr → Lean.MetaM (Lean.Expr × ℕ)
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Defining equation for the recursor of `W`  -/
MvPFunctor.wRec_eq : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {C : Sort u_1}
  (g : (a : P.A) → (P.drop.B a).Arrow α → (P.last.B a → P.W α) → (P.last.B a → C) → C) (a : P.A)
  (f' : (P.drop.B a).Arrow α) (f : P.last.B a → P.W α), P.wRec g (P.wMk a f' f) = g a f' f fun i => P.wRec g (f i)
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- Returns `some (a, b)` if `e` is of the form
```
@HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) a b
```
 -/
Lean.Meta.Grind.Arith.isNatAdd? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.merge? : Lean.TSyntax `tactic → Lean.TSyntax `tactic → Option (Lean.TSyntax `tactic)
-- Lean.Data.SMap
Lean.SMap.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (stage₁ : Bool) (map₁ : Std.HashMap α β)
  (map₂ : Lean.PHashMap α β) (stage₁_1 : Bool) (map₁_1 : Std.HashMap α β) (map₂_1 : Lean.PHashMap α β),
  ({ stage₁ := stage₁, map₁ := map₁, map₂ := map₂ } = { stage₁ := stage₁_1, map₁ := map₁_1, map₂ := map₂_1 }) =
    (stage₁ = stage₁_1 ∧ map₁ = map₁_1 ∧ map₂ = map₂_1)
-- Mathlib.Data.Finset.Sigma
Finset.mk_mem_sigmaLift : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [inst : DecidableEq ι]
  (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (i : ι) (a : α i) (b : β i) (x : γ i),
  ⟨i, x⟩ ∈ Finset.sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔ x ∈ f a b
-- Mathlib.Data.PNat.Factors
PrimeMultiset.coeNat : Coe PrimeMultiset (Multiset ℕ)
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.instBoundedOrderSubtypeSubmoduleMemSublattice : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (f : Module.End R M) → BoundedOrder ↥f.invtSubmodule
-- Mathlib.Data.Matrix.DMatrix
DMatrix.map_zero : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [inst : (i : m) → (j : n) → Zero (α i j)] {β : m → n → Type w}
  [inst_1 : (i : m) → (j : n) → Zero (β i j)] {f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j},
  (∀ (i : m) (j : n), f 0 = 0) → DMatrix.map 0 f = 0
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_surjective : ∀ {R : Type u_1} [inst : Semiring R] (x y : R), Function.Surjective (Polynomial.evalEval x y)
-- Mathlib.Topology.List
List.continuous_prod : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MulOneClass α] [ContinuousMul α], Continuous List.prod
-- Init.Data.Nat.Lemmas
/-- Shift right on successor with division moved inside.  -/
Nat.shiftRight_succ_inside : ∀ (m n : ℕ), m >>> (n + 1) = (m / 2) >>> n
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_14} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_15}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {x : M} {f : M → M'} {g : N → N'} {y : N},
  MDiffAt f x → MDiffAt g y → MDiffAt (Prod.map f g) (x, y)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.descCoconeMorphism.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t)
  (s : CategoryTheory.Limits.Cocone F), h.descCoconeMorphism s = { hom := h.desc s, w := ⋯ }
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
AddChar.starComp_apply : ∀ {R : Type u_1} [inst : CommRing R], 0 < ringChar R → ∀ {φ : AddChar R ℂ} (a : R), (starRingEnd ℂ) (φ a) = φ⁻¹ a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback fallback' : α}, t.getKeyD (t.maxKeyD fallback) fallback' = t.maxKeyD fallback
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] (v : Valuation A Γ)
  [inst_2 : v.IsRankOneDiscrete],
  Subgroup.zpowers (Valuation.IsRankOneDiscrete.generator v) = (MonoidWithZeroHom.ofClass v).valueGroup
-- Std.Http.Data.Status
/-- Checks if the status code indicates an error (either client error 4xx or server error 5xx).

Reference: https://httpwg.org/specs/rfc9110.html#status.codes
 -/
Std.Http.Status.isError : Std.Http.Status → Bool
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.epiComp_fst : ∀ {Δ₁ Δ₂ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ₁) (p : Δ₁ ⟶ Δ₂)
  [inst : CategoryTheory.Epi p.unop], (A.epiComp p).fst = A.fst
-- Mathlib.CategoryTheory.Abelian.Transfer
/-- No point making this an instance, as it requires `i`.  -/
CategoryTheory.AbelianOfAdjunction.hasKernels : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D C) [G.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteLimits G]
  (i : F.comp G ≅ CategoryTheory.Functor.id C), CategoryTheory.Limits.HasKernels C
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.mem_vadd_set_iff_neg_vadd_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {A : Set β} {a : α} {x : β},
  x ∈ a +ᵥ A ↔ -a +ᵥ x ∈ A
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuous_iInf_rng : ∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α' : Type u_7} [tX : TopologicalSpace X] {u : κ → UniformSpace α'}
  {F : ι → X → α'}, Equicontinuous F ↔ ∀ (k : κ), Equicontinuous F
-- Init.Prelude
/-- `SyntaxNodeKinds` is a set of `SyntaxNodeKind`, implemented as a list.

Singleton `SyntaxNodeKinds` are extremely common. They are written as name literals, rather than as
lists; list syntax is required only for empty or non-singleton sets of kinds.
 -/
Lean.SyntaxNodeKinds : Type
-- Lean.Environment
Lean.ModuleIdx.toNat : Lean.ModuleIdx → ℕ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.polynomial.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R),
  W'.polynomial =
    MvPolynomial.X 1 ^ 2 * MvPolynomial.X 2 +
          MvPolynomial.C W'.a₁ * MvPolynomial.X 0 * MvPolynomial.X 1 * MvPolynomial.X 2 +
        MvPolynomial.C W'.a₃ * MvPolynomial.X 1 * MvPolynomial.X 2 ^ 2 -
      (MvPolynomial.X 0 ^ 3 + MvPolynomial.C W'.a₂ * MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2 +
          MvPolynomial.C W'.a₄ * MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 +
        MvPolynomial.C W'.a₆ * MvPolynomial.X 2 ^ 3)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constModify : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {f : β → β},
          (Std.DTreeMap.Internal.Impl.Const.modify k f t₁).Equiv (Std.DTreeMap.Internal.Impl.Const.modify k f t₂)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
_private.Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet.0.«term_~ᵤ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Modification.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {app : (a : B) → η.app a ⟶ θ.app a}
  {naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)) (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
      CategoryTheory.Lax.OplaxTrans.Modification.naturality._autoParam}
  {app_1 : (a : B) → η.app a ⟶ θ.app a}
  {naturality_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app_1 b))
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerRight (app_1 a) (G.map f)))
      CategoryTheory.Lax.OplaxTrans.Modification.naturality._autoParam},
  { app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 } → app = app_1
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_eq_zero' : ∀ {E : Type u_5} [inst : NormedGroup E] {a : E}, ‖a‖₊ = 0 ↔ a = 1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  (Std.ExtDHashMap.Const.alter m k f).getKey? k =
    if (f (Std.ExtDHashMap.Const.get? m k)).isSome = true then some k else none
-- Init.Data.UInt.Bitwise
UInt16.toNat_xor : ∀ (a b : UInt16), (a ^^^ b).toNat = a.toNat ^^^ b.toNat
-- Init.Data.Vector.Find
Vector.findSome?_singleton : ∀ {α : Type u_1} {β : Type u_2} {a : α} {f : α → Option β}, Vector.findSome? f #v[a] = f a
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHomClass.toFrameHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [CompleteLatticeHomClass F α β], FrameHomClass F α β
-- Mathlib.Algebra.Order.Group.Basic
zpow_right_strictAnti : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {a : α},
  a < 1 → StrictAnti fun n => a ^ n