mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
ZMod.rootsOfUnityAddChar_val : ∀ (n : ℕ) [inst : NeZero n] (x : ZMod n), ↑↑((ZMod.rootsOfUnityAddChar n) x) = ZMod.toCircle x
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.neg_add : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M] (a b : M), -(a + b) = -a + -b
-- Std.Data.HashMap.IteratorLemmas
_private.Std.Data.HashMap.IteratorLemmas.0.Std.DHashMap.toList.eq_1 : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} (m : Std.DHashMap α β), m.toList = m.inner.toList
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_const_mul_iff : ∀ {α : Type u_1} {β : Type u_2} (l : Filter α) (k f : α → β) [inst : TopologicalSpace β] [inst_1 : Field β]
  [ContinuousMul β] {c : β},
  c ≠ 0 → ((Asymptotics.SuperpolynomialDecay l k fun n => c * f n) ↔ Asymptotics.SuperpolynomialDecay l k f)
-- Std.Time.DateTime
/-- Subtract `Hour.Offset` from a `DateTime`.
 -/
Std.Time.DateTime.subHours : Std.Time.DateTime → Std.Time.Hour.Offset → Std.Time.DateTime
-- Mathlib.Topology.NoetherianSpace
/-- In a Noetherian space, every closed set is a finite union of irreducible closed sets.  -/
TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] (s : TopologicalSpace.Closeds α),
  ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S
-- Init.Data.Vector.Basic
/-- Get an element of a vector using a `Nat` index. Returns the given default value if the index is out
of bounds.
 -/
Vector.getD : {α : Type u_1} → {n : ℕ} → Vector α n → ℕ → α → α
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.mk'_y : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x : ↥X) (y : ↥Y) (h : f x = g y),
  (AlgebraicGeometry.Scheme.Pullback.Triplet.mk' x y h).y = y
-- Lean.Parser.Extra
/-- The parser `many(p)`, or `p*`, repeats `p` until it fails, and returns the list of results.

The argument `p` is "auto-grouped", meaning that if the arity is greater than 1 it will be
automatically replaced by `group(p)` to ensure that it produces exactly 1 value.

This parser has arity 1: it produces a `nullKind` node containing one argument for each
invocation of `p` (or `group(p)`).  -/
Lean.Parser.many : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Probability.Kernel.Defs
/-- Notation for `Kernel` with respect to a non-standard σ-algebra in the domain.  -/
ProbabilityTheory.«termKernel[_]__» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.even_toSubmodule : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M), Subalgebra.toSubmodule (CliffordAlgebra.even Q) = CliffordAlgebra.evenOdd Q 0
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_obj_right_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.CostructuredArrow (CategoryTheory.Over.forget X.1) X.2),
  ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse X).obj Y).right.as = PUnit.unit
-- Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
contDiffOn_succ_of_fderiv_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {D : Type uD} [inst_1 : NormedAddCommGroup D]
  [inst_2 : NormedSpace 𝕜 D] {E : Type uE} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {n : WithTop ℕ∞}
  {f : D → E} {s : Set D} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 D],
  DifferentiableOn 𝕜 f s →
    (n = ⊤ → AnalyticOn 𝕜 f s) →
      (∀ (y : D), ContDiffOn 𝕜 n (fun x => (fderivWithin 𝕜 f s x) y) s) → ContDiffOn 𝕜 (n + 1) f s
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.left_mem_perpBisector : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ : P}, p₁ ∈ AffineSubspace.perpBisector p₁ p₂ ↔ p₁ = p₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- The (colimiting) `PushoutCocone f g` implicit in the statement
that we have an `IsPushout f g inl inr`.
 -/
CategoryTheory.IsPushout.cocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Z X Y P : C} →
      {f : Z ⟶ X} →
        {g : Z ⟶ Y} →
          {inl : X ⟶ P} → {inr : Y ⟶ P} → CategoryTheory.IsPushout f g inl inr → CategoryTheory.Limits.PushoutCocone f g
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.mk : {T : Type u_1} → (NT : Type) → NT → Finset (ContextFreeRule T NT) → ContextFreeGrammar T
-- Mathlib.Topology.FiberPartition
/-- The canonical map from the disjoint union induced by `f` to `S`.  -/
TopologicalSpace.Fiber.sigmaIsoHom : {S : Type u_1} → {Y : Type u_2} → (f : S → Y) → [inst : TopologicalSpace S] → C((x : Function.Fiber f) × ↑↑x, S)
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.isSymmetricProjection_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →ₗ[𝕜] E), T.IsSymmetricProjection ↔ IsIdempotentElem T ∧ T.IsSymmetric
-- Aesop.Rule.Name
Aesop.ScopeName.local.sizeOf_spec : sizeOf Aesop.ScopeName.local = 1
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- `prod F G` is a binary product for `F` and `G`.  -/
CategoryTheory.FunctorToTypes.binaryProductLimitCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G : CategoryTheory.Functor C (Type w)) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair F G)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_filter_key : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {f : α → Bool} {l : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKeyD k (List.filter (fun p => f p.fst) l) fallback =
      (Option.filter f (Std.Internal.List.getKey? k l)).getD fallback
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.next.eq_1 : ∀ {ι : Type u_1} (c : ComplexShape ι) (i : ι), c.next i = if h : ∃ j, c.Rel i j then h.choose else i
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.instHasCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.HasCoproducts (CategoryTheory.Limits.FormalCoproduct C)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.realSize.eq_def : ∀ {α : Type u_1} (x : Batteries.BinomialHeap.Imp.HeapNode α),
  x.realSize =
    match x with
    | Batteries.BinomialHeap.Imp.HeapNode.nil => 0
    | Batteries.BinomialHeap.Imp.HeapNode.node a c s => c.realSize + 1 + s.realSize
-- Std.Time.Time.Unit.Hour
/-- `Ordinal` represents a bounded value for hours, ranging from 0 to 23.
 -/
Std.Time.Hour.Ordinal : Type
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.isGroupoid_of_reflects_iso : ∀ {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) [F.ReflectsIsomorphisms]
  [CategoryTheory.IsGroupoid D], CategoryTheory.IsGroupoid C
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.smul_eq_mulAut_conj : ∀ {G : Type u_3} [inst : Group G] (g : ConjAct G) (h : G), g • h = (MulAut.conj (ConjAct.ofConjAct g)) h
-- Mathlib.Order.Closure
LowerAdjoint.closure_sup_closure_le : ∀ {α : Type u_1} {β : Type u_4} [inst : SemilatticeSup α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u)
  (x y : α), u (l.toFun x) ⊔ u (l.toFun y) ≤ u (l.toFun (x ⊔ y))
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
_private.Mathlib.Analysis.Distribution.SchwartzSpace.Basic.0.SchwartzMap.decay_smul_aux : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [SMulCommClass ℝ 𝕜 F] (k n : ℕ) (f : SchwartzMap E F) (c : 𝕜) (x : E),
  ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [Inhabited α] {k fallback : α} {f : β → β}, (m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback
-- Mathlib.FieldTheory.KummerExtension
X_pow_sub_C_irreducible_of_prime_pow : ∀ {K : Type u} [inst : Field K] {p : ℕ},
  Nat.Prime p → p ≠ 2 → ∀ (n : ℕ) {a : K}, (∀ (b : K), b ^ p ≠ a) → Irreducible (Polynomial.X ^ p ^ n - Polynomial.C a)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- The functions in the partition of unity add up to at most `1` everywhere.  -/
SmoothPartitionOfUnity.sum_le_one' : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : optParam (Set M) Set.univ} (self : SmoothPartitionOfUnity ι I M s) (x : M),
  ∑ᶠ (i : ι), (self.toFun i) x ≤ 1
-- Mathlib.Topology.Defs.Basic
/-- Delaborator for `IsClosed[_]`.  -/
Topology.delabIsClosed : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
/-- If `A` is a commutative ring of prime characteristic `p` and `I` is an ideal such that
`I^p = 0`, then `I` admits a divided power structure.  -/
DividedPowers.CharP.dividedPowers : (A : Type u_1) →
  [inst : CommRing A] →
    (p : ℕ) →
      [CharP A p] → [Fact (Nat.Prime p)] → {I : Ideal A} → [DecidablePred fun x => x ∈ I] → I ^ p = 0 → DividedPowers I
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (k : α) (v : β), (t₁.insertIfNew k v).Equiv (t₂.insertIfNew k v)
-- Mathlib.Algebra.Order.Star.Basic
star_nonneg_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x : R}, 0 ≤ star x ↔ 0 ≤ x
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (x y : CategoryTheory.Abelian.Ext X Y n),
  R.extEquivCohomologyClass (x - y) = R.extEquivCohomologyClass x - R.extEquivCohomologyClass y
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_11 : HAdd Std.Time.Millisecond.Offset Std.Time.Week.Offset Std.Time.Millisecond.Offset
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The closure by isomorphisms of a `MorphismProperty`  -/
CategoryTheory.MorphismProperty.isoClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Lean.Elab.App
/-- Try to synthesize metavariables are `instMVars` using type class resolution.
The ones that cannot be synthesized yet are registered.
 -/
Lean.Elab.Term.ElabAppArgs.synthesizeAppInstMVars : Lean.Elab.Term.ElabAppArgs.M Unit
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.toZFSet_succ : ∀ (o : Ordinal.{u_1}), (Order.succ o).toZFSet = insert o.toZFSet o.toZFSet
-- Aesop.Tree.State
Aesop.Rapp.isProvenNoCache : Aesop.Rapp → BaseIO Bool
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] (X Y : C) {Z : C}
  (h : e.inverse.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
      (CategoryTheory.CategoryStruct.comp (e.inverse.map (CategoryTheory.Functor.OplaxMonoidal.δ e.functor X Y)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y)) h)
-- Lean.Parser.Extra
Lean.Parser.ppHardLineUnlessUngrouped.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Batteries.Recycling.RBTree.Depth
RBTree.RBNode.depthLB.eq_1 : ∀ (x : ℕ), RBTree.RBNode.depthLB RBTree.RBColor.red x = x + 1
-- Mathlib.Data.Finset.Sups
Finset.sups_left_comm : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] (s t u : Finset α), s ⊻ (t ⊻ u) = t ⊻ (s ⊻ u)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- `stratum` and `FiniteArchimedeanClass.ball` are disjoint.  -/
HahnEmbedding.ArchimedeanStrata.disjoint_ball_stratum : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] (self : HahnEmbedding.ArchimedeanStrata K M)
  (c : FiniteArchimedeanClass M), Disjoint (FiniteArchimedeanClass.ball K c) (self.stratum c)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_filter_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool},
  (Std.DHashMap.filter f m).isEmpty = true ↔
    ∀ (k : α) (h : k ∈ m), f (m.getKey k h) (Std.DHashMap.Const.get m k h) = false
-- Mathlib.CategoryTheory.Generator.StrongGenerator
CategoryTheory.ObjectProperty.IsStrongGenerator.exists_of_subobject_ne_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  P.IsStrongGenerator → ∀ {X : C} {A : CategoryTheory.Subobject X}, A ≠ ⊤ → ∃ G, ∃ (_ : P G), ∃ f, ¬A.Factors f
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.refl_restr_source : ∀ {α : Type u_1} (s : Set α), ((PartialEquiv.refl α).restr s).source = s
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.finitary_of_rankFinite : ∀ {α : Type u_1} {M : Matroid α} [M.RankFinite], M.Finitary
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.of_injective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [Nontrivial R] [inst_2 : AddZeroClass M],
  Function.Injective ⇑(AddMonoidAlgebra.of R M)
-- Init.Data.UInt.Lemmas
UInt8.toUSize_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatClamp n).toUSize = USize.ofNatLT n ⋯
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Cases.mk.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {typeName : Lean.Name} {resultType : Lean.Expr} {discr : Lean.FVarId}
  {alts : Array (Lean.Compiler.LCNF.Alt pu)} {typeName_1 : Lean.Name} {resultType_1 : Lean.Expr} {discr_1 : Lean.FVarId}
  {alts_1 : Array (Lean.Compiler.LCNF.Alt pu)},
  Lean.Compiler.LCNF.Cases.mk typeName resultType discr alts =
      Lean.Compiler.LCNF.Cases.mk typeName_1 resultType_1 discr_1 alts_1 →
    typeName = typeName_1 ∧ resultType = resultType_1 ∧ discr = discr_1 ∧ alts = alts_1
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.restrict_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (p : CategoryTheory.Presieve.FamilyOfElements P R) (φ : P ⟶ Q)
  {R' : CategoryTheory.Presieve X} (h : R' ≤ R),
  (CategoryTheory.Presieve.FamilyOfElements.restrict h p).map φ =
    CategoryTheory.Presieve.FamilyOfElements.restrict h (p.map φ)
-- Batteries.Util.ProofWanted
/-- `proof_wanted` is a synonym for `theorem_wanted`; only the command keyword used in error
messages differs.  -/
_private.Batteries.Util.ProofWanted.0.proofWantedCmd : WantedCmdKind✝
-- Mathlib.RingTheory.PicardGroup
/-- Given an invertible `R`-submodule `I` in an `R`-algebra `A`, the `R`-linear map
from `I ⊗[R] I⁻¹` to `R` induced by multiplication is an isomorphism.  -/
Submodule.tensorInvEquiv : {R : Type u} →
  {A : Type u_4} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] → [FaithfulSMul R A] → (I : (Submodule R A)ˣ) → TensorProduct R ↥↑I ↥↑I⁻¹ ≃ₗ[R] R
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.instMonoidWithZero : {α : Type u_2} → [inst : NonUnitalNonAssocSemiring α] → MonoidWithZero (α →ₙ+* α)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₂ → (m₁ ∪ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Std.Http.Data.URI.Basic
/-- Authority-form request target (used for CONNECT requests).
Example: `example.com:443`
 -/
Std.Http.RequestTarget.authorityForm : Std.Http.URI.Authority → Std.Http.RequestTarget
-- Aesop.Util.Basic
Aesop.instMonadCacheStateRefT'_aesop : {α β : Type} → {m : Type → Type} → {ω σ : Type} → [Lean.MonadCache α β m] → Lean.MonadCache α β (StateRefT' ω σ m)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.refl_toRingHom : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁],
  ↑AlgEquiv.refl = RingHom.id A₁
-- Init.Data.Slice.Array.Iterator
SubarrayIterator.mk.inj : ∀ {α : Type u} {xs xs_1 : Subarray α}, { xs := xs } = { xs := xs_1 } → xs = xs_1
-- Mathlib.LinearAlgebra.Lagrange
/-- `basisDivisor x y` is the unique linear or constant polynomial such that
when evaluated at `x` it gives `1` and `y` it gives `0` (where when `x = y` it is identically `0`).
Such polynomials are the building blocks for the Lagrange interpolants.  -/
Lagrange.basisDivisor : {F : Type u_1} → [inst : Field F] → F → F → Polynomial F
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.IsocrystalEquiv.mk.injEq : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {k : Type u_1} [inst_1 : CommRing k] [inst_2 : CharP k p]
  [inst_3 : PerfectRing k p] {V : Type u_2} [inst_4 : AddCommGroup V] [inst_5 : WittVector.Isocrystal p k V]
  {V₂ : Type u_3} [inst_6 : AddCommGroup V₂] [inst_7 : WittVector.Isocrystal p k V₂]
  (toLinearEquiv : V ≃ₗ[FractionRing (WittVector p k)] V₂)
  (frob_equivariant :
    ∀ (x : V),
      (WittVector.Isocrystal.frobenius p k) (toLinearEquiv x) = toLinearEquiv ((WittVector.Isocrystal.frobenius p k) x))
  (toLinearEquiv_1 : V ≃ₗ[FractionRing (WittVector p k)] V₂)
  (frob_equivariant_1 :
    ∀ (x : V),
      (WittVector.Isocrystal.frobenius p k) (toLinearEquiv_1 x) =
        toLinearEquiv_1 ((WittVector.Isocrystal.frobenius p k) x)),
  ({ toLinearEquiv := toLinearEquiv, frob_equivariant := frob_equivariant } =
      { toLinearEquiv := toLinearEquiv_1, frob_equivariant := frob_equivariant_1 }) =
    (toLinearEquiv = toLinearEquiv_1)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.unit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.unit = e.unitIso.hom
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_left_iff : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime (x * y) z ↔ IsCoprime x z ∧ IsCoprime y z
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mk.sizeOf_spec : ∀ {G : Type u_3} [inst : AddGroup G] [inst_1 : SizeOf G] (toAddSubmonoid : AddSubmonoid G)
  (neg_mem' : ∀ {x : G}, x ∈ toAddSubmonoid.carrier → -x ∈ toAddSubmonoid.carrier),
  sizeOf { toAddSubmonoid := toAddSubmonoid, neg_mem' := neg_mem' } = 1 + sizeOf toAddSubmonoid
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.piCongrLeft'_symm_apply : ∀ (R : Type u) {ι : Type x} {ι' : Type x'} [inst : Semiring R] (φ : ι → Type u_1)
  [inst_1 : (i : ι) → AddCommMonoid (φ i)] [inst_2 : (i : ι) → Module R (φ i)] (e : ι ≃ ι')
  (a : (b : ι') → φ (e.symm b)) (a_1 : ι),
  (LinearEquiv.piCongrLeft' R φ e).symm a a_1 = (Equiv.piCongrLeft' φ e).symm a a_1
-- Init.Data.SInt.Bitwise
Bool.toBitVec_toInt8 : ∀ {b : Bool}, b.toInt8.toBitVec = BitVec.setWidth 8 (BitVec.ofBool b)
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.geom_sum_X_comp_X_add_one_eq_sum : ∀ {R : Type u} [inst : Semiring R] (n : ℕ),
  (∑ i ∈ Finset.range n, Polynomial.X ^ i).comp (Polynomial.X + 1) =
    ∑ i ∈ Finset.range n, ↑(n.choose (i + 1)) * Polynomial.X ^ i
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.measurableInv : ∀ {ι : Type u_4} {α : ι → Type u_5} [inst : (i : ι) → Inv (α i)] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  [∀ (i : ι), MeasurableInv (α i)], MeasurableInv ((i : ι) → α i)
-- Mathlib.LinearAlgebra.CrossProduct
cross_apply : ∀ {R : Type u_1} [inst : CommRing R] (a b : Fin 3 → R),
  (crossProduct a) b = ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]
-- Init.Core
UInt8.ofBitVec.inj : ∀ {toBitVec toBitVec_1 : BitVec 8}, { toBitVec := toBitVec } = { toBitVec := toBitVec_1 } → toBitVec = toBitVec_1
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_union_compl_neighborSet_eq : ∀ {V : Type u} (G : SimpleGraph V) (v : V), G.neighborSet v ∪ Gᶜ.neighborSet v = {v}ᶜ
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.instFiniteCarrierToAddGrp : ∀ (G : FiniteAddGrp.{u_1}), Finite ↑G.toAddGrp
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.eq_zero_of_mem_of_neg_mem : ∀ {F : Type u_2} [inst : Field F] {P : RingPreordering F} {x : F}, x ∈ P → -x ∈ P → x = 0
-- Mathlib.Algebra.Order.Floor.Ring
natCast_ceil_eq_intCast_ceil_of_neg_one_lt : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R}, -1 < a → ↑⌈a⌉₊ = ↑⌈a⌉
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.ofSigmaCofork_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} {c : CategoryTheory.Limits.Cofan I.left}
  {hc : CategoryTheory.Limits.IsColimit c} {d : CategoryTheory.Limits.Cofan I.right}
  (a : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)),
  (CategoryTheory.Limits.Multicofork.ofSigmaCofork a).pt = a.pt
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.vadd_apply : ∀ {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [inst : (i : ι) → VAdd α (M i)] (a : α) (f : (i : ι) → M i) (i : ι),
  (a +ᵥ f) i = a +ᵥ f i
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_center_homothety : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  dist p₁ ((AffineMap.homothety p₁ c) p₂) = ‖c‖ * dist p₁ p₂
-- Mathlib.Data.Finset.Insert
Finset.nonempty_iff_eq_singleton_default : ∀ {α : Type u_1} [inst : Unique α] {s : Finset α}, s.Nonempty ↔ s = {default}
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.single_add : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α] (p : ENNReal)
  (i : α) (a b : E i), lp.single p i (a + b) = lp.single p i a + lp.single p i b
-- Mathlib.GroupTheory.Perm.Centralizer
/-- The conjugation action of `Subgroup.centralizer {g}` on `g.cycleFactorsFinset`  -/
Equiv.Perm.OnCycleFactors.instMulActionSubtypeMemSubgroupCentralizerSingletonSetFinsetCycleFactorsFinset : {α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] → (g : Equiv.Perm α) → MulAction ↥(Subgroup.centralizer {g}) ↥g.cycleFactorsFinset
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coxeterWeight_flip : ∀ {ι : Type u_1} {R : Type u_2} {M : 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] (P : RootPairing ι R M N) (i j : ι),
  P.flip.coxeterWeight i j = P.coxeterWeight i j
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- The `k`-th Mahler basis function, i.e. the unique continuous function `ℤ_[p] → ℤ_[p]`
agreeing with `n ↦ n.choose k` for `n ∈ ℕ`. See [colmez2010], §1.2.1.
 -/
mahler : {p : ℕ} → [hp : Fact (Nat.Prime p)] → ℕ → C(ℤ_[p], ℤ_[p])