mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.CompactOpen
ContinuousMap.instT2Space : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y], T2Space C(X, Y)
-- Mathlib.Data.WSeq.Defs
/-- Apply a function to the elements of the sequence to produce a sequence
of partial results. (There is no `scanr` because this would require
working from the end of the sequence, which may not exist.)  -/
Stream'.WSeq.scanl : {α : Type u} → {β : Type v} → (α → β → α) → α → Stream'.WSeq β → Stream'.WSeq α
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.Kernel.indep_limsup_atTop_self : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω}
  {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} [inst : SemilatticeSup ι]
  [NoMaxOrder ι] [Nonempty ι],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.Kernel.iIndep s κ μα →
      ProbabilityTheory.Kernel.Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) κ μα
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_map : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {β : Type u_7} [inst_6 : MeasurableSpace β] {φ : X → β},
  Measurable φ →
    ∀ {f : β → E} {s : Set β},
      MeasurableSet s →
        MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map φ (μ.restrict (φ ⁻¹' s)).variation) →
          μ.Integrable (f ∘ φ) → ∫ᵛ (y : β) in s, f y ∂[B; μ.map φ] = ∫ᵛ (x : X) in φ ⁻¹' s, f (φ x) ∂[B; μ]
-- Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
CategoryTheory.injective_iff_rlp_monomorphisms_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (I : C),
  CategoryTheory.Injective I ↔ (CategoryTheory.MorphismProperty.monomorphisms C).rlp 0
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f` is invariant under negation of `x`, then so is `seminormFromBounded'`.  -/
seminormFromBounded_neg : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ},
  (∀ (x : R), f (-x) = f x) → ∀ (x : R), seminormFromBounded' f (-x) = seminormFromBounded' f x
-- Mathlib.Algebra.Group.Defs
/-- An `AddGroup` which `IsMulCommutative` is a `AddCommGroup`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsAddCommutative.instAddCommGroup : {G : Type u_2} → [inst : AddGroup G] → [IsAddCommutative G] → AddCommGroup G
-- Mathlib.RingTheory.Ideal.Span
Ideal.zero_ne_one_of_proper : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I ≠ ⊤ → 0 ≠ 1
-- Mathlib.Algebra.Star.Subalgebra
Subalgebra.starClosure_le : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {S₁ : Subalgebra R A}
  {S₂ : StarSubalgebra R A}, S₁ ≤ S₂.toSubalgebra → S₁.starClosure ≤ S₂
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.instTypeNameInteractiveMessage : TypeName Lean.Widget.InteractiveMessage
-- Mathlib.Algebra.Order.Group.CompleteLattice
mul_ciInf : ∀ {ι : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
  [MulLeftMono G], BddBelow (Set.range f) → ∀ (a : G), a * ⨅ i, f i = ⨅ i, a * f i
-- Mathlib.Data.Seq.Defs
/-- Destructor for a sequence, resulting in either `none` (for `nil`) or
`some (a, s)` (for `cons a s`).  -/
Stream'.Seq.destruct : {α : Type u} → Stream'.Seq α → Option (Stream'.Seq1 α)
-- Mathlib.Analysis.Complex.ReImTopology
Complex.frontier_setOfPred_le_re_and_im_le : ∀ (a b : ℝ), frontier {z | a ≤ z.re ∧ z.im ≤ b} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ z.im ≤ b}
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.Obj.inhabited : (P : PFunctor.{uA, uB}) → {α : Type v₁} → [Inhabited P.A] → [Inhabited α] → Inhabited (↑P α)
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
SubmodulesBasis.mk : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace R] {B : ι → Submodule R M},
  (∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j) → (∀ (m : M) (i : ι), ∀ᶠ (a : R) in nhds 0, a • m ∈ B i) → SubmodulesBasis B
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.uniqueLinearEquiv_symm_apply : ∀ (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : Zero M] [inst_4 : Subsingleton M] (s : S),
  (AddMonoidAlgebra.uniqueLinearEquiv R M).symm s = AddMonoidAlgebra.single 0 s
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.count_eq_count_toIterM : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  {it : Std.Iter β}, it.length = it.toIterM.length.run.down
-- Mathlib.Data.Complex.Basic
Complex.zero_re : Complex.re 0 = 0
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.exists_nnnorm_lt : ∀ (α : Type u_2) [inst : NontriviallyNormedField α] {r : NNReal}, 0 < r → ∃ x, 0 < ‖x‖₊ ∧ ‖x‖₊ < r
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.map_tsum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [L.NeBot] [inst_3 : AddCommMonoid γ] [inst_4 : TopologicalSpace γ] [T2Space γ],
  Summable f L →
    ∀ {G : Type u_4} [inst_6 : FunLike G α γ] [AddMonoidHomClass G α γ] (g : G),
      Continuous ⇑g → g (∑'[L] (i : β), f i) = ∑'[L] (i : β), g (f i)
-- Mathlib.Algebra.Order.CauSeq.Basic
/-- **Alias** of the reverse direction of `isCauSeq_neg`. -/
IsCauSeq.neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f : ℕ → β}, IsCauSeq abv f → IsCauSeq abv (-f)
-- Mathlib.Tactic.Module
/-- Given `l` of type `qNF R M`, i.e. a list of `(Q($R) × Q($M)) × ℕ`s (two `Expr`s and a natural
number), build an `Expr` representing an object of type `NF R M` (i.e. `List (R × M)`) in the
in the obvious way: by forgetting the natural numbers and gluing together the `Expr`s.  -/
Mathlib.Tactic.Module.qNF.toNF : {u v : Lean.Level} →
  {M : Q(Type v)} → {R : Q(Type u)} → Mathlib.Tactic.Module.qNF R M → Q(Mathlib.Tactic.Module.NF «$R» «$M»)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpoint_empty_mem_interior_faceOpposite : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  (i : Fin (n + 1)), s.touchpoint ∅ i ∈ (s.faceOpposite i).interior
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_Ioo_ae_eq_pi_Ioc : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)] {s : Set ι}
  {f g : (i : ι) → α i},
  (s.pi fun i => Set.Ioo (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] s.pi fun i => Set.Ioc (f i) (g i)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.IterM.step_intermediateDropWhileM.match_1.splitter : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    [inst : MonadAttach m] →
      {P : β → m (ULift.{u_1, 0} Bool)} →
        (out : β) →
          (motive : Subtype (MonadAttach.CanReturn (P out)) → Sort u_3) →
            (__do_lift : Subtype (MonadAttach.CanReturn (P out))) →
              ((hP : MonadAttach.CanReturn (P out) { down := true }) → motive ⟨{ down := true }, hP⟩) →
                ((hP : MonadAttach.CanReturn (P out) { down := false }) → motive ⟨{ down := false }, hP⟩) →
                  motive __do_lift
-- Mathlib.CategoryTheory.Abelian.Preradical.Basic
CategoryTheory.Abelian.Preradical.r_map_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) (X : C), Φ.r.map (Φ.ι.app X) = Φ.ι.app (Φ.r.obj X)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.cancelDen : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr →
  ℤ → Lean.Grind.Linarith.Var → Lean.Grind.Linarith.Var → Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom Y)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) h
-- Mathlib.Order.Fin.Basic
Fin.succAbove_lt_succAbove_iff : ∀ {n : ℕ} {p : Fin (n + 1)} {i j : Fin n}, p.succAbove i < p.succAbove j ↔ i < j
-- Init.Data.Int.Lemmas
Int.neg_ofNat_eq_negSucc_add_one_iff : ∀ {a b : ℕ}, -↑a = Int.negSucc b + 1 ↔ a = b
-- Mathlib.Data.PFunctor.Univariate.M
/-- `CofixA F n` is an `n` level approximation of an M-type  -/
PFunctor.Approx.CofixA : PFunctor.{uA, uB} → ℕ → Type (max uA uB)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.WithCache.mk.injEq : ∀ {α : Type u} {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} (val : α) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig)
  (val_1 : α) (cache_1 : Std.Tactic.BVDecide.BVExpr.Cache aig),
  ({ val := val, cache := cache } = { val := val_1, cache := cache_1 }) = (val = val_1 ∧ cache = cache_1)
-- Std.Data.DTreeMap.Lemmas
/-- Variant of `get?_map` that holds without `LawfulEqCmp`.  -/
Std.DTreeMap.Const.get?_map' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k : α},
  Std.DTreeMap.Const.get? (Std.DTreeMap.map f t) k =
    Option.pmap (fun v h' => f (t.getKey k h') v) (Std.DTreeMap.Const.get? t k) ⋯
-- Mathlib.Algebra.CharP.Invertible
invertibleThree : {K : Type u_2} → [inst : DivisionSemiring K] → [CharZero K] → Invertible 3
-- Mathlib.NumberTheory.Real.Irrational
instDecidableIrrationalSqrtCastReal_1 : (z : ℤ) → Decidable (Irrational √↑z)
-- Lean.Data.NameMap.Basic
Lean.NameMap.instForInProdNameOfMonad : {α : Type} → {m : Type u_1 → Type u_2} → [Monad m] → ForIn m (Lean.NameMap α) (Lean.Name × α)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [inst_3 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A]
  (G₀ : CategoryTheory.Sheaf J₀ A) (X : C) (i i' : (data X).I₀) (j : (data X).I₁ i i'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i)
      (G₀.obj.map ((data X).p₁ j).op) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i')
      (G₀.obj.map ((data X).p₂ j).op)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.func.sizeOf_spec : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : SizeOf α] {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α),
  sizeOf (FirstOrder.Language.func _f _ts) = 1 + sizeOf l + sizeOf _f
-- Mathlib.RingTheory.Jacobson.Ideal
/-- The Jacobson radical of a two-sided ideal is two-sided.  -/
Ideal.instIsTwoSidedJacobson : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} [I.IsTwoSided], I.jacobson.IsTwoSided
-- Aesop.Tree.Data
Aesop.Goal.setId : Aesop.GoalId → Aesop.Goal → Aesop.Goal
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.zsmul_period_add_vadd : ∀ {α : Type v} {G : Type u} [inst : AddGroup G] [inst_1 : AddAction G α] (i : ℤ) (g : G) (a : α),
  (↑(AddAction.period g a) + i) • g +ᵥ a = i • g +ᵥ a
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_sPolynomial : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
  m.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g) ∨ m.sPolynomial f g = 0
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.toCocone_ι_app : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J] {A : Type w} [inst_2 : AddCommGroup A] (f : AddCommGrpCat.Colimits.Quot F →+ A) (j : J),
  (AddCommGrpCat.Colimits.toCocone F f).ι.app j = AddCommGrpCat.ofHom (f.comp (AddCommGrpCat.Colimits.Quot.ι F j))
-- Mathlib.RingTheory.KrullDimension.Regular
/-- If `M` is a finite module over a Noetherian local ring `R`, then `dim M ≤ dim M/xM + 1`
for every `x` in the maximal ideal of the local ring `R`.  -/
Module.supportDim_le_supportDim_quotSMulTop_succ : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {M : Type u_2} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.Finite R M] [inst_5 : IsLocalRing R] {x : R},
  x ∈ IsLocalRing.maximalIdeal R → Module.supportDim R M ≤ Module.supportDim R (QuotSMulTop x M) + 1
-- Lean.Attributes
Lean.instBEqAttributeApplicationTime : BEq Lean.AttributeApplicationTime
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.p.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ),
  CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.p✝ f n =
    HomologicalComplex.mkHomToSingle (CategoryTheory.Injective.ι (((CategoryTheory.Limits.cokernel f).truncGE n).X n)) ⋯
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.foldl_eq_foldl_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {δ : Type w} {f : δ → α → δ} {init : δ},
  Std.TreeSet.Raw.foldl f init t = List.foldl f init t.toList
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
AlgEquiv.map_det : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type w}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] {T : Type z} [inst_5 : CommRing T] [inst_6 : Algebra R T] (f : S ≃ₐ[R] T)
  (M : Matrix n n S), f M.det = (f.mapMatrix M).det
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.retractClosure_extensionProductIter_retractClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) {n : ℕ},
  (P.retractClosure.extensionProductIter n).retractClosure = (P.extensionProductIter n).retractClosure
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableAt.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E → F) (x : E), DifferentiableAt 𝕜 f x = ∃ f', HasFDerivAt f f' x
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- An operator is positive iff it is symmetric and `0 ≤ ⟪T x, x⟫`.

For the version with `IsSelfAdjoint` instead of `IsSymmetric`, see
`ContinuousLinearMap.isPositive_iff'`.  -/
ContinuousLinearMap.isPositive_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E), T.IsPositive ↔ (↑T).IsSymmetric ∧ ∀ (x : E), 0 ≤ inner 𝕜 (T x) x
-- Std.Data.ExtDTreeMap.Basic
/-- Implementation detail of the tree map  -/
Std.ExtDTreeMap.pliftOn : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {γ : Sort w} →
        (t : Std.ExtDTreeMap α β cmp) →
          (f : (x : Std.DTreeMap α β cmp) → t = Std.ExtDTreeMap.mk x → γ) →
            (∀ (a b : Std.DTreeMap α β cmp) (h₁ : t = Std.ExtDTreeMap.mk a) (h₂ : t = Std.ExtDTreeMap.mk b),
                a.Equiv b → f a h₁ = f b h₂) →
              γ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], MeasureTheory.volume.IsAddHaarMeasure
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `f` is an antitone function taking values in a conditionally complete linear order
and `g` tends to `atTop` along a nontrivial filter,
then the indexed infimum of `f ∘ g` is equal to the indexed infimum of `f`.  -/
Antitone.ciInf_comp_tendsto_atTop_of_linearOrder : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : ConditionallyCompleteLinearOrder γ]
  {l : Filter α} [l.NeBot] {f : β → γ},
  Antitone f → ∀ {g : α → β}, Filter.Tendsto g l Filter.atTop → ⨅ a, f (g a) = ⨅ b, f b
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.args : Lean.Elab.Term.CollectPatternVars.Context → List Lean.Elab.Term.Arg
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.varLt : Lean.Grind.CommRing.Power → Lean.Grind.CommRing.Power → Bool
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M`, if a `CommMonoid` map
`g : M →* P` induces a map `f.lift hg : N →* P` then for all `z : N`, we have
`g y * f.lift hg z = g x`, where `x : M, y ∈ S` are such that `z * f y = f x`.  -/
Submonoid.LocalizationMap.lift_mul_left : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (z : N),
  g ↑(f.sec z).2 * (f.lift hg) z = g (f.sec z).1
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.Clause.relabel_id' : ∀ {α : Type u_1}, Std.Sat.CNF.Clause.relabel id = id
-- Lean.Util.PPExt
Lean.PPFns.mk : (Lean.PPContext → Lean.Expr → IO Lean.FormatWithInfos) →
  (Lean.PPContext → Lean.Name → IO Lean.FormatWithInfos) →
    (Lean.PPContext → Lean.Term → IO Std.Format) →
      (Lean.PPContext → Lean.Level → IO Std.Format) → (Lean.PPContext → Lean.MVarId → IO Std.Format) → Lean.PPFns
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.ι_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ),
  CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.ι✝ f n)
      (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.π✝ f n) =
    f
-- Std.Time.Time.Unit.Second
Std.Time.Second.instOfNatOrdinal : {leap : Bool} → {n : ℕ} → OfNat (Std.Time.Second.Ordinal leap) n
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.copy_H : ∀ {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) {Q' H' : C} (eQ : Q' ≅ h.Q) (eH : H' ≅ h.H),
  (h.copy eQ eH).H = H'
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- Do not use this. Use `MeasurableSet.of_discrete` instead.  -/
DiscreteMeasurableSpace.forall_measurableSet : ∀ {α : Type u_7} {inst : MeasurableSpace α} [self : DiscreteMeasurableSpace α] (s : Set α), MeasurableSet s
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
/-- `nearestPt e N x` is the nearest point to `x` among the points `e 0`, ..., `e N`. If more than
one point are at the same distance from `x`, then `nearestPt e N x` returns the point with the
least possible index.  -/
MeasureTheory.SimpleFunc.nearestPt : {α : Type u_1} →
  [inst : MeasurableSpace α] →
    [inst_1 : PseudoEMetricSpace α] → [OpensMeasurableSpace α] → (ℕ → α) → ℕ → MeasureTheory.SimpleFunc α α
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.hom_neg_apply : ∀ {M N : AddMonCat} (e : M ≅ N) (s : ↑N),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.Combinatorics.Derangements.Basic
/-- The set of derangements on `Option α` is equivalent to the union over `a : α`
of "permutations with `a` the only possible fixed point".  -/
derangements.derangementsOptionEquivSigmaAtMostOneFixedPoint : {α : Type u_1} → [DecidableEq α] → ↑(derangements (Option α)) ≃ (a : α) × ↑{f | Function.fixedPoints ⇑f ⊆ {a}}
-- Lean.Data.Name
/-- Returns true if the name has any numeric components.  -/
Lean.Name.hasNum : Lean.Name → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushoutShape.hom_id : ∀ {J : Type w} (X : CategoryTheory.Limits.WidePushoutShape J),
  CategoryTheory.Limits.WidePushoutShape.Hom.id X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFiniteFPowerSeriesOnBall.fderiv_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E},
  HasFiniteFPowerSeriesOnBall f p x n r →
    ∀ {y : E}, ↑‖y‖₊ < r → fderiv 𝕜 f (x + y) = (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.instIsLocalizationCompιWeakEquivalences : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] (L : CategoryTheory.Functor C D)
  [L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)],
  (HomotopicalAlgebra.BifibrantObject.ι.comp L).IsLocalization
    (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.BifibrantObject C))
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.out_one : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α], Associates.out 1 = 1
-- Std.Http.Data.Extensions
/-- A dynamically typed map for optional metadata that can be attached to HTTP requests and responses.
Extensions allow storing arbitrary typed data keyed by type name, useful for metadata such as socket
information or custom processing data.
 -/
Std.Http.Extensions : Type
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts_functor : ∀ {C : Type (u₁ + 1)} [inst : CategoryTheory.LargeCategory C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C],
  (CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts C).functor =
    CategoryTheory.Mat_.lift (CategoryTheory.Functor.id C)