mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
WeakDual.CharacterSpace.ext : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : TopologicalSpace A]
  [inst_6 : Module 𝕜 A] {φ ψ : ↑(WeakDual.characterSpace 𝕜 A)}, (∀ (x : A), φ x = ψ x) → φ = ψ
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.rightUnitor_inv_apply : ∀ {X : Type u} {x : X},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv) x = (x, PUnit.unit)
-- Mathlib.Logic.Embedding.Set
Function.Embedding.coe_sigmaSet : ∀ {α : Type u_1} {ι : Type u_2} {s : ι → Set α} (h : Pairwise (Function.onFun Disjoint s)),
  ⇑(Function.Embedding.sigmaSet h) = fun x => ↑x.snd
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_map_iff : ∀ {α : Type u_1} {β : Type u_2} {n : Type u_4} [inst : Star α] [inst_1 : Star β] {A : Matrix n n α} {f : α → β},
  Function.Semiconj f star star → Function.Injective f → ((A.map f).IsHermitian ↔ A.IsHermitian)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The morphism `⦋2⦌ ⟶ ⦋n⦌` that picks out a specified composite of morphisms in `Fin (n+1)`.  -/
SimplexCategory.mkOfLeComp : {n : ℕ} → (i j k : Fin (n + 1)) → i ≤ j → j ≤ k → ({ len := 2 } ⟶ { len := n })
-- Mathlib.Order.SuccPred.Archimedean
antitoneOn_of_le_pred : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : PredOrder α]
  [IsPredArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMin a → a ∈ s → Order.pred a ∈ s → f a ≤ f (Order.pred a)) → AntitoneOn f s
-- Init.Data.Int.Order
Int.sign_natCast_add_one : ∀ (n : ℕ), (↑n + 1).sign = 1
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous : ∀ (R : Type u_1) (n : Type u_3) [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  ((MvPolynomial.optionEquivLeft R (n × n)).symm (Matrix.charpoly.univ R n)).IsHomogeneous (Fintype.card n)
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.instCanLiftForallCoeContinuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  CanLift (X → Y) C(X, Y) DFunLike.coe Continuous
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → ∀ {h : k' ∈ m.insertMany l}, (m.insertMany l).getKey k' h = k
-- Mathlib.Analysis.RCLike.Basic
RCLike.imCLM_coe : ∀ {K : Type u_1} [inst : RCLike K], ↑RCLike.imCLM = RCLike.imLm
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ext_chart_model_space_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x y : E}, ↑(extChartAt (modelWithCornersSelf 𝕜 E) x) y = y
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.imp_eq_cert.eq_1 : ∀ (p : Lean.Grind.Linarith.Poly) (x y : Lean.Grind.Linarith.Var),
  Lean.Grind.Linarith.imp_eq_cert p x y =
    (p == Lean.Grind.Linarith.Poly.add 1 x (Lean.Grind.Linarith.Poly.add (-1) y Lean.Grind.Linarith.Poly.nil))
-- Std.Do.WP.SimpLemmas
Std.Do.WP.OptionT_run : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {Q : Std.Do.PostCond (Option α) ps} [inst : Std.Do.WP m ps]
  (x : OptionT m α), (Std.Do.wp x.run).apply Q = (Std.Do.wp x).apply (fun a => Q.1 (some a), fun x => Q.1 none, Q.2)
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.isInducing_mk_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsInducing ⇑DomAddAct.mk.symm
-- Aesop.Rule.Basic
Aesop.Rule.pattern? : {α : Type} → Aesop.Rule α → Option Aesop.RulePattern
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
ContinuousMultilinearMap.hasStrictFDerivAt_uncurry : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)),
  HasStrictFDerivAt (fun fx => fx.1 fx.2)
    (ContinuousMultilinearMap.apply 𝕜 E F fa.2 ∘SL
        ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) +
      fa.1.linearDeriv fa.2 ∘SL ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i))
    fa
-- Mathlib.Algebra.Opposites
AddOpposite.instInv : {α : Type u_1} → [Inv α] → Inv αᵃᵒᵖ
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.isLittleO_congr_left : ∀ {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [inst : Norm G] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : SeminormedAddCommGroup F'] {k : α → G} {f' : α → E'} {g' : α → F'} {l : Filter α},
  f' =Θ[l] g' → (f' =o[l] k ↔ g' =o[l] k)
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory}
  {f g : X ⟶ Y}, f.hom = g.hom → f = g
-- Mathlib.CategoryTheory.Enriched.HomCongr
/-- `eHomCongr` respects composition of morphisms. Recall that for any
composable pair of arrows `f : X ⟶ Y` and `g : Y ⟶ Z` in `C`, the composite
`f ≫ g` in `C` defines a morphism `𝟙_ V ⟶ (X ⟶[V] Z)` in `V`. Composing with
the isomorphism `eHomCongr V α γ` yields a morphism in `V` that can be factored
through the enriched composition map as shown:
`𝟙_ V ⟶ 𝟙_ V ⊗ 𝟙_ V ⟶ (X₁ ⟶[V] Y₁) ⊗ (Y₁ ⟶[V] Z₁) ⟶ (X₁ ⟶[V] Z₁)`.  -/
CategoryTheory.Iso.eHomCongr_comp : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C]
  {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.Iso.eHomCongr V α γ).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) f) (CategoryTheory.Iso.eHomCongr V α β).hom)
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X₁ ⟶[V] Y₁)
            (CategoryTheory.CategoryStruct.comp ((CategoryTheory.eHomEquiv V) g)
              (CategoryTheory.Iso.eHomCongr V β γ).hom))
          (CategoryTheory.eComp V X₁ Y₁ Z₁)))
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintKind.noConfusionType : Sort v✝ → Lean.Elab.InlayHintKind → Lean.Elab.InlayHintKind → Sort v✝
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.radius_ne_zero_of_nontrivial : ∀ {α : Type u_1} {G : SimpleGraph α} [Nontrivial α], G.radius ≠ 0
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.homologyData'_right_p : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hk : c.next j = k) (h : (K.sc' i j k).HomologyData),
  (HomologicalComplex.extend.homologyData' K e hj' hi hk h).right.p =
    CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom h.right.p
-- Lean.Data.LOption
Lean.Option.toLOption : {α : Type u} → Option α → Lean.LOption α
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.filter_parts_partition_eq_cycleType : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α},
  Multiset.filter (fun n => 2 ≤ n) σ.partition.parts = σ.cycleType
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_index_coe : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [inst : h.IsProper] (s : h.ι) {d : ℕ} (hd : h.dim s = d),
  ↑(⋯.index hd) = ↑(h.index s)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k} {hc : k ∈ t.modify k f},
  (t.modify k f).get k hc = f (t.get k ⋯)
-- Mathlib.Algebra.Ring.GeomSum
RingHom.map_geom_sum : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (x : R) (n : ℕ) (f : R →+* S),
  f (∑ i ∈ Finset.range n, x ^ i) = ∑ i ∈ Finset.range n, f x ^ i
-- Mathlib.MeasureTheory.VectorMeasure.Prod
/-- If `ν` is a vector measure, and `s ⊆ X × Y` is measurable, then `x ↦ ν { y | (x, y) ∈ s }` is
a strongly measurable function.  -/
MeasureTheory.VectorMeasure.stronglyMeasurable_vectorMeasure_prodMk_left : ∀ {X : Type u_2} {Y : Type u_3} {F : Type u_5} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  [inst : NormedAddCommGroup F] {ν : MeasureTheory.VectorMeasure Y F} {s : Set (X × Y)},
  MeasurableSet s → MeasureTheory.StronglyMeasurable fun x => ν (Prod.mk x ⁻¹' s)
-- Mathlib.RingTheory.MvPowerSeries.Equiv
AdicCompletion.liftAlgHom.eq_1 : ∀ {S : Type u_5} [inst : CommRing S] (I : Ideal S) {R : Type u_6} {A : Type u_7} [inst_1 : CommRing R]
  [inst_2 : CommRing A] [inst_3 : Algebra R A] [inst_4 : Algebra R S] (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n)
  (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m),
  AdicCompletion.liftAlgHom I f hf =
    { toRingHom := AdicCompletion.liftRingHom I (fun n => (f n).toRingHom) ⋯, commutes' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_neg : ∀ {n : Type u_3} {R : Type u_6} [inst : Fintype n] [inst_1 : AddCommGroup R] (A : Matrix n n R), (-A).trace = -A.trace
-- Mathlib.Order.SuccPred.Basic
Order.pred_covBy_of_not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α}, ¬IsMin a → Order.pred a ⋖ a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k a : α} [inst_1 : Inhabited (β a)],
      (Std.DTreeMap.Internal.Impl.erase! k t).get! a = if compare k a = Ordering.eq then default else t.get! a
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
IsBoundedBilinearMap.toContinuousLinearMap.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f f_1 : E × F → G} (e_f : f = f_1)
  (hf : IsBoundedBilinearMap 𝕜 f), hf.toContinuousLinearMap = ⋯.toContinuousLinearMap
-- Std.Async.TCP
/-- Creates a new TCP server socket.
 -/
Std.Async.TCP.Socket.Server.mk : IO Std.Async.TCP.Socket.Server
-- Mathlib.Data.NNReal.Defs
Real.coe_toNNReal_le : ∀ (x : ℝ), ↑x.toNNReal ≤ |x|
-- Init.Data.UInt.BasicAux
/-- Converts a 16-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.toNat : UInt16 → ℕ
-- Init.Data.Ord.Basic
Ordering.isEq_swap : ∀ {o : Ordering}, o.swap.isEq = o.isEq
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.toPresheafFiber_pointPresheafFiberIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_2 : J.IsLocalSite] {A : Type u'}
  [inst_3 : CategoryTheory.Category.{v', u'} A] [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  {P : CategoryTheory.Functor Cᵒᵖ A} (X : C) (x : (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).fiber.obj X)
  {Z : A} (h : P.obj (Opposite.op (⊤_ C)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.IsLocalSite.point J).toPresheafFiber X x P)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso J P).hom h) =
    CategoryTheory.CategoryStruct.comp (P.map (CategoryTheory.shrinkCoyonedaObjObjEquiv x).op) h
-- Mathlib.Topology.Connected.LocallyConnected
locallyConnectedSpace_of_connected_bases : ∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} (b : α → ι → Set α) (p : α → ι → Prop),
  (∀ (x : α), (nhds x).HasBasis (p x) (b x)) →
    (∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)) → LocallyConnectedSpace α
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.nthRoot_zero_left : ∀ (a : ℕ), Nat.nthRoot 0 a = 1
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- Construct a unit associated to the place `w₁`. The family, for `w₁ ≠ w₀`, formed by the
image by the `logEmbedding` of these units is `ℝ`-linearly independent, see
`unitLattice_span_eq_top`.  -/
NumberField.Units.dirichletUnitTheorem.exists_unit : ∀ (K : Type u_1) [inst : Field K] [NumberField K] (w₁ : NumberField.InfinitePlace K),
  ∃ u, ∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) < 0
-- Mathlib.Data.Fin.Fin2
_private.Mathlib.Data.Fin.Fin2.0.Fin2.add.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match k.succ with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_2 k
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt64.size ≤ n → (UInt64.ofNatClamp n).toBitVec = (UInt64.size - 1)#'UInt64.toBitVec_ofNatClamp_of_le._proof_1
-- Mathlib.Order.BooleanSubalgebra
/-- The preimage of a Boolean subalgebra along a bounded lattice homomorphism.  -/
BooleanSubalgebra.comap : {α : Type u_2} →
  {β : Type u_3} →
    [inst : BooleanAlgebra α] →
      [inst_1 : BooleanAlgebra β] → BoundedLatticeHom α β → BooleanSubalgebra β → BooleanSubalgebra α
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_le_of_support_subset : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R},
  p.support ⊆ q.support → p.totalDegree ≤ q.totalDegree
-- Mathlib.Analysis.Complex.Poisson
/-- Companion theorem to the Poisson Integral Formula: The real part of the Herglotz–Riesz kernel and
the Poisson kernel agree on the path of integration.
 -/
poissonKernel_eq_re_herglotzRieszKernel : ∀ {c w : ℂ}, poissonKernel c w = Complex.re ∘ herglotzRieszKernel c w
-- Mathlib.Topology.Algebra.Group.Torsor
Continuous.sdiv : ∀ {V : Type u_1} {P : Type u_2} {α : Type u_3} [inst : Group V] [inst_1 : TopologicalSpace V] [inst_2 : Torsor V P]
  [inst_3 : TopologicalSpace P] [IsTopologicalTorsor P] [inst_5 : TopologicalSpace α] {f g : α → P},
  Continuous f → Continuous g → Continuous fun x => f x /ₛ g x
-- Lean.Elab.Deriving.Basic
_private.Lean.Elab.Deriving.Basic.0.Lean.Elab.elabDefDeriving : Array Lean.Elab.DerivingClassView →
  Array Lean.Syntax → optParam Bool false → optParam (Option Lean.Syntax) none → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.monadToMon_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Monad C),
  (CategoryTheory.Monad.monadToMon C).obj M = M.toMon
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.instHasTensorTensorUnit_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive]
  [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2}
  [inst_6 : AddMonoid I] {c : ComplexShape I} [inst_7 : c.TensorSigns] (K : HomologicalComplex C c)
  [inst_8 : DecidableEq I]
  [∀ (X₁ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)],
  K.HasTensor (HomologicalComplex.tensorUnit C c)
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.«termρ⁻¹_» : Lean.ParserDescr
-- Init.Data.UInt.Lemmas
UInt8.toNat_sub : ∀ (a b : UInt8), (a - b).toNat = (2 ^ 8 - b.toNat + a.toNat) % 2 ^ 8
-- Mathlib.Topology.Compactness.LocallyCompact
instWeaklyLocallyCompactSpaceOfLocallyCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X], WeaklyLocallyCompactSpace X
-- Mathlib.Algebra.Star.Basic
/-- A type endowed with `star` and `*` is a star magma if it admits an injective map that
preserves `star` and `*` to star magma.  See note [reducible non-instances].  -/
Function.Injective.starMul : {R : Type u} →
  {S : Type v} →
    (f : R → S) →
      [inst : Star R] →
        [inst_1 : Mul R] →
          [inst_2 : Mul S] →
            [inst_3 : StarMul S] →
              Function.Injective f →
                (∀ (x : R), f (star x) = star (f x)) → (∀ (x y : R), f (x * y) = f x * f y) → StarMul R
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.trans_conjAut : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (β : Y ≅ Z)
  (f : CategoryTheory.Aut X), (α ≪≫ β).conjAut f = β.conjAut (α.conjAut f)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.leSigmaOfOrd : {α : Type u} → {β : α → Type v} → [Ord α] → LE ((a : α) × β a)
-- Mathlib.CategoryTheory.Sites.Continuous
/-- SGA 4 III 1.2 (i) => (iii)  -/
CategoryTheory.Functor.W_map_of_adjunction_of_isContinuous : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u} [inst_2 : CategoryTheory.Category.{t, u} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (F : CategoryTheory.Functor C D)
  (H : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Functor Dᵒᵖ A))
  (adj : H ⊣ (CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj F.op) [F.IsContinuous J K]
  {G G' : CategoryTheory.Functor Cᵒᵖ A} (f : G ⟶ G'), J.W f → K.W (H.map f)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivWithinAt_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] (x : E) (s : Set E), HasFDerivWithinAt id (ContinuousLinearMap.id 𝕜 E) s x
-- Mathlib.LinearAlgebra.Ray
units_smul_eq_neg_iff : ∀ {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] [Module.IsTorsionFree R M] {u : Rˣ} {v : Module.Ray R M},
  u • v = -v ↔ ↑u < 0
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.measurable_measure_stieltjesOfMeasurableRat : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : Measurable f),
  Measurable fun a => (ProbabilityTheory.stieltjesOfMeasurableRat f hf a).measure
-- Lean.Elab.App
/-- Position of the next argument to be processed. We use it to decide whether the argument is the motive or a discriminant.  -/
Lean.Elab.Term.ElabElim.State.idx : Lean.Elab.Term.ElabElim.State → ℕ
-- Mathlib.Combinatorics.Matroid.Loop
/-- **Alias** of the reverse direction of `Matroid.singleton_isCircuit`. -/
Matroid.IsLoop.isCircuit : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsLoop e → M.IsCircuit {e}
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mk_zero : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] {s : Finset ι},
  DFinsupp.mk s 0 = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.minKey_modify_eq_minKey : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {he : Std.ExtDTreeMap.Const.modify t k f ≠ ∅},
  (Std.ExtDTreeMap.Const.modify t k f).minKey he = t.minKey ⋯
-- Mathlib.Algebra.Order.Hom.Basic
le_map_add_map_sub : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α] [inst_2 : AddCommMagma β]
  [inst_3 : LE β] [SubadditiveHomClass F α β] (f : F) (a b : α), f a ≤ f b + f (a - b)
-- Mathlib.Data.ENNReal.Inv
ENNReal.sub_half : ∀ {a : ENNReal}, a ≠ ⊤ → a - a / 2 = a / 2
-- Mathlib.Data.Num.ZNum
ZNum.ofInt'_eq : ∀ (n : ℤ), ZNum.ofInt' n = ↑n
-- Lean.Environment
/-- Environment extension for overriding the height that `getMaxHeight` assigns to a definition.
This is consulted for all definitions regardless of their reducibility hints. Currently used by
structural recursion to ensure that parent definitions get the correct height even though the
`_f` helper definitions are marked as `.abbrev` (which `getMaxHeight` would otherwise ignore).  -/
Lean.defHeightOverrideExt : Lean.EnvExtension (Lean.NameMap UInt32)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_foldr_inf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {n : ℕ} (l : List (L.BoundedFormula α n))
  (v : α → M) (xs : Fin n → M), (List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ l).Realize v xs ↔ ∀ φ ∈ l, φ.Realize v xs
-- Mathlib.Algebra.Group.PUnit
PUnit.instOne_mathlib.eq_1 : PUnit.instOne_mathlib = { one := PUnit.unit }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyItem.name : Lean.Lsp.CallHierarchyItem → String
-- Init.Data.Rat.Lemmas
Rat.le_of_mul_le_mul_left : ∀ {a b c : ℚ}, c * a ≤ c * b → 0 < c → a ≤ b
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
/-- `Measure.compProd` is associative. We have to insert `MeasurableEquiv.prodAssoc`
because the products of types `α × β × γ` and `(α × β) × γ` are different.  -/
MeasureTheory.Measure.compProd_assoc : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} {γ : Type u_3} {mγ : MeasurableSpace γ} {η : ProbabilityTheory.Kernel (α × β) γ},
  MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc.symm) (μ.compProd (κ.compProd η)) = (μ.compProd κ).compProd η
-- Mathlib.Topology.ContinuousMap.Sigma
ContinuousMap.sigmaCodHomeomorph_symm_apply : ∀ (X : Type u_1) {ι : Type u_2} (Y : ι → Type u_3) [inst : TopologicalSpace X]
  [inst_1 : (i : ι) → TopologicalSpace (Y i)] [inst_2 : ConnectedSpace X] (a : (i : ι) × C(X, Y i)),
  (ContinuousMap.sigmaCodHomeomorph X Y).symm a = (ContinuousMap.sigmaMk a.fst).comp a.snd
-- Lean.ParserCompiler.Attribute
Lean.ParserCompiler.CombinatorAttribute.runDeclFor : {α : Type} → Lean.ParserCompiler.CombinatorAttribute → Lean.Name → Lean.CoreM α
-- Mathlib.MeasureTheory.Group.Convolution
/-- Convolution of the dirac measure at 1 with a measure μ returns μ.  -/
MeasureTheory.Measure.dirac_one_mconv : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] (μ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ], (MeasureTheory.Measure.dirac 1).mconv μ = μ
-- Init.Data.Option.Lemmas
Option.mem_some : ∀ {α : Type u_1} {a b : α}, a ∈ some b ↔ b = a
-- Mathlib.Order.ScottContinuity
ScottContinuousOn.monotone : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} (D : Set (Set α)),
  (∀ (a b : α), a ≤ b → {a, b} ∈ D) → ScottContinuousOn D f → Monotone f
-- Std.Http.Data.Method
Std.Http.instReprMethod : Repr Std.Http.Method
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpMax.eq_1 : CommGrpMax = CommGrpCat
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_keys : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k : α}, k ∈ m.keys ↔ k ∈ m