mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.dest_corec₁ : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u}
  (g : {X : Type u} → (MvQPF.Cofix F α → X) → (β → X) → β → F (α ::: X)) (x : β),
  (∀ (X Y : Type u) (f : MvQPF.Cofix F α → X) (f' : β → X) (k : X → Y),
      g (k ∘ f) (k ∘ f') x = MvFunctor.map (TypeVec.id ::: k) (g f f' x)) →
    (MvQPF.Cofix.corec₁ g x).dest = g id (MvQPF.Cofix.corec₁ g) x
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.eq_mk'_iff_add_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {x : M} {y : ↥S} {z : N}, z = f.mk' x y ↔ z + f ↑y = f x
-- Mathlib.Topology.UniformSpace.Pi
Cauchy.pi : ∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] [Nonempty ι] {l : (i : ι) → Filter (α i)},
  (∀ (i : ι), Cauchy (l i)) → Cauchy (Filter.pi l)
-- Mathlib.Analysis.Normed.Module.Completion
UniformSpace.Completion.coe_toComplₗᵢ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : UniformContinuousConstSMul 𝕜 E], ⇑UniformSpace.Completion.toComplₗᵢ = UniformSpace.Completion.coe'
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.cocone_pt : ∀ (R : Type) [inst : CommRing R] {X : LightCondMod R} {S T : LightProfinite}
  (π : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj S LightProfinite.NatUnionInfty)
  [inst_1 :
    CategoryTheory.Epi
      ((lightProfiniteToLightCondSet.comp (LightCondensed.free R)).map (InternalProjectivityProof.cover✝ π))]
  (g : (lightProfiniteToLightCondSet.comp (LightCondensed.free R)).obj T ⟶ X)
  (r_inf :
    T ⟶
      InternalProjectivityProof.LightProfinite.fibre✝ OnePoint.infty
        (CategoryTheory.CategoryStruct.comp π
          (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))
  (σ :
    S ⟶
      InternalProjectivityProof.LightProfinite.fibre✝ OnePoint.infty
        (CategoryTheory.CategoryStruct.comp π
          (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))
  (hr :
    CategoryTheory.CategoryStruct.comp
        (InternalProjectivityProof.LightProfinite.fibreIncl✝ OnePoint.infty
          (CategoryTheory.CategoryStruct.comp π
            (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))
        r_inf =
      CategoryTheory.CategoryStruct.id
        (InternalProjectivityProof.LightProfinite.fibre✝ OnePoint.infty
          (CategoryTheory.CategoryStruct.comp π
            (CategoryTheory.SemiCartesianMonoidalCategory.snd S LightProfinite.NatUnionInfty)))),
  (InternalProjectivityProof.cocone✝ R π g r_inf σ hr).pt = X
-- Mathlib.Analysis.Normed.Affine.MazurUlam
IsometryEquiv.coe_toRealLinearIsometryEquivOfMapZero : ∀ {E : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : E ≃ᵢ F) (h0 : f 0 = 0), ⇑(f.toRealLinearIsometryEquivOfMapZero h0) = ⇑f
-- Mathlib.Algebra.Module.Submodule.Map
MonoidHom.coe_toAdditive_map : ∀ {G : Type u_9} {G₂ : Type u_10} [inst : Group G] [inst_1 : Group G₂] (f : G →* G₂) (s : Subgroup G),
  AddSubgroup.map (MonoidHom.toAdditive f) (Subgroup.toAddSubgroup s) = Subgroup.toAddSubgroup (Subgroup.map f s)
-- Mathlib.Algebra.Homology.SpectralObject.Basic
/-- The connecting homomorphism of the spectral object.  -/
CategoryTheory.Abelian.SpectralObject.δ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (n₀ n₁ : ℤ) →
                    autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δ._auto_1 →
                      ((X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶
                        (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Lean.Util.CollectAxioms
/-- Collect axioms for `c` and return its sorted axiom list from the cache.  -/
_private.Lean.Util.CollectAxioms.0.Lean.CollectAxioms.collectAndGet : (Lean.Environment → Lean.Name → Option (Array Lean.Name)) → Lean.Name → Lean.CollectAxioms.M✝ (Array Lean.Name)
-- Mathlib.Algebra.Category.Grp.Basic
/-- Construct a bundled `AddGrpCat` from the underlying type and typeclass.  -/
AddGrpCat.of : (M : Type u) → [AddGroup M] → AddGrpCat
-- Lean.Parser.Do
Lean.Parser.Term.doReassignArrow : Lean.Parser.Parser
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.isEmpty_takeWhile_eq_true : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String}, s.startsWith pat = false → (s.takeWhile pat).isEmpty = true
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE._auto_3),
  (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₂ = X.opcycles f₁₂ f₃ n₁
-- Mathlib.Topology.Algebra.Group.Pointwise
compl_mul_closure_one_eq_iff : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {t : Set G},
  tᶜ * closure {1} = tᶜ ↔ t * closure {1} = t
-- Init.Data.List.MinMaxOn
List.apply_minOn_le_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} (h : xs ≠ []) {b : β}, f (List.minOn f xs h) ≤ b ↔ ∃ x ∈ xs, f x ≤ b
-- Mathlib.Order.Monotone.Basic
monotoneOn_toDual_comp_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  MonotoneOn (⇑OrderDual.toDual ∘ f) s ↔ AntitoneOn f s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.foldrM_eq_foldrM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ},
  Std.DTreeMap.foldrM f init t = List.foldrM (fun a b => f a.1 a.2 b) init (Std.DTreeMap.Const.toList t)
-- Mathlib.RepresentationTheory.Invariants
Rep.invariantsFunctor_map_hom : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B),
  ModuleCat.Hom.hom ((Rep.invariantsFunctor k G).map f) =
    LinearMap.codRestrict B.ρ.invariants ((Rep.Hom.hom f).toLinearMap ∘ₗ A.ρ.invariants.subtype) ⋯
-- Mathlib.Topology.Closure
/-- **Alias** of the forward direction of `dense_closure`.

---

The closure of a set `s` is dense if and only if `s` is dense.  -/
Dense.of_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, Dense (closure s) → Dense s
-- Mathlib.Analysis.Calculus.MeanValue
/-- Variant of the mean value inequality on a convex set, using a bound on the difference between
the derivative and a fixed linear map, rather than a bound on the derivative itself. Version with
`HasFDerivWithinAt`.  -/
Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x y : E}
  {f' : E → E →L[𝕜] G} {φ : E →L[𝕜] G},
  (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
    (∀ x ∈ s, ‖f' x - φ‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x - φ (y - x)‖ ≤ C * ‖y - x‖
-- Mathlib.Combinatorics.SimpleGraph.Dart
/-- A `Dart` is an oriented edge, implemented as an ordered pair of adjacent vertices.
This terminology comes from combinatorial maps, and they are also known as "half-edges"
or "bonds."  -/
SimpleGraph.Dart : {V : Type u_1} → SimpleGraph V → Type u_1
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.homInhabited.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.Mon C), M.homInhabited = { default := M.id }
-- Mathlib.Analysis.Normed.Module.RCLike.Real
interior_sphere : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ},
  r ≠ 0 → interior (Metric.sphere x r) = ∅
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_eq_default : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α}, a ∉ m → m[a]! = default
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonResolvableCompletionItemData : Lean.FromJson Lean.Lsp.ResolvableCompletionItemData
-- Mathlib.Logic.Relation
/-- The composition of two relations, yielding a new relation.  The result
relates a term of `α` and a term of `γ` if there is an intermediate
term of `β` related to both.
 -/
_private.Mathlib.Logic.Relation.0.Relation.«term_∘r_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst_map_prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {X : α → β} {Y : α → γ} {μ : MeasureTheory.Measure α},
  Measurable Y → (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).fst = MeasureTheory.Measure.map X μ
-- Mathlib.Analysis.Distribution.Distribution
Distribution.instLineDerivSMulRealTopENat : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2}
  [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousSMul ℝ F], LineDerivSMul ℝ E (Distribution Ω F ⊤) (Distribution Ω F ⊤)
-- Lean.DocString.Types
Lean.Doc.Inline.code.inj : ∀ {i : Type u} {string string_1 : String},
  Lean.Doc.Inline.code string = Lean.Doc.Inline.code string_1 → string = string_1
-- Init.Data.AC
Lean.Data.AC.Context.arbitrary : {α : Sort u} → Lean.Data.AC.Context α → α
-- Mathlib.Topology.Category.Profinite.Limits
Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier : CompHausLike.HasExplicitPullbacks fun Y => TotallyDisconnectedSpace ↑Y
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.productUniqueIso_hom : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C),
  (CategoryTheory.Limits.productUniqueIso f).hom = CategoryTheory.Limits.Pi.π f default
-- Std.Internal.Do.Order.Basic
Lean.Order.CompleteLattice.ofProp_true : ∀ (l : Type v) [inst : Lean.Order.CompleteLattice l], Lean.Order.CompleteLattice.ofProp True = Lean.Order.top
-- Lean.LocalContext
Lean.LocalContext.getUnusedName : Lean.LocalContext → Lean.Name → Lean.Name
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.map_comp : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{vβ, uβ} β) {γ : Type uγ} [inst_2 : UniformSpace γ] (pkg'' : AbstractCompletion.{vγ, uγ} γ)
  {g : β → γ} {f : α → β},
  UniformContinuous g → UniformContinuous f → pkg'.map pkg'' g ∘ pkg.map pkg' f = pkg.map pkg'' (g ∘ f)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
/-- The hyperbolic metric on the upper half plane. We ensure that the projection to
`TopologicalSpace` is definitionally equal to the subtype topology.  -/
UpperHalfPlane.instMetricSpace : MetricSpace UpperHalfPlane
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.instNormedAddTorsor : {𝕜 : Type u_1} →
  {V : Type u_3} →
    {W : Type u_4} →
      {Q : Type u_6} →
        [inst : SeminormedAddCommGroup V] →
          [inst_1 : SeminormedAddCommGroup W] →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : NormedSpace 𝕜 V] →
                [inst_4 : NormedSpace 𝕜 W] →
                  [inst_5 : PseudoMetricSpace Q] →
                    [inst_6 : NormedAddTorsor W Q] → NormedAddTorsor (V →ᴬ[𝕜] W) (V →ᴬ[𝕜] Q)
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.nonneg.hasMemOrNegMem : ∀ {T : Type u_2} [inst : Ring T] [inst_1 : LinearOrder T] [inst_2 : IsOrderedRing T], HasMemOrNegMem (RingCone.nonneg T)
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
EuclideanGeometry.Sphere.secondInter_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂]
  (s : EuclideanGeometry.Sphere P) (p : P) (v : V) (f : P →ᵃⁱ[ℝ] P₂),
  { center := f s.center, radius := s.radius }.secondInter (f p) (f.linearIsometry v) = f (s.secondInter p v)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Expand `⟪x + y, x + y⟫_ℝ`  -/
real_inner_add_add_self : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  inner ℝ (x + y) (x + y) = inner ℝ x x + 2 * inner ℝ x y + inner ℝ y y
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_mem_coeffs : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} (m : σ →₀ ℕ),
  MvPolynomial.coeff m p ≠ 0 → MvPolynomial.coeff m p ∈ p.coeffs
-- Batteries.Lean.Expr
/-- Like `withAppRev` but ignores metadata.  -/
Lean.Expr.withAppRev' : {α : Sort u_1} → Lean.Expr → (Lean.Expr → Array Lean.Expr → α) → α
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- A variant of `IsConjRoot.eq_of_isConjRoot_algebraMap`, only assuming `IsDomain R`,
`IsTorsionFree R A` and `Function.Injective (algebraMap R A)` instead of `Field R`. If `x` is a
conjugate root of some element `algebraMap R S r` in the image of the base ring, then
`x = algebraMap R S r`.
 -/
isConjRoot_iff_eq_algebraMap_of_injective : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain S]
  [IsDomain R] [Module.IsTorsionFree R S] {r : R} {x : S},
  Function.Injective ⇑(algebraMap R S) → (IsConjRoot R ((algebraMap R S) r) x ↔ x = (algebraMap R S) r)
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Functor.sections.eq_1 : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w)),
  F.sections = {u | ∀ {j j' : J} (f : j ⟶ j'), (CategoryTheory.ConcreteCategory.hom (F.map f)) (u j) = u j'}
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_forall_exists_isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.RespectsIso],
  (∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g],
      P g → ∃ T fst snd, CategoryTheory.IsPullback fst snd f g ∧ P fst) →
    P.IsStableUnderBaseChange
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
/-- the (weak) rank function  -/
SSet.Subcomplex.Pairing.WeakRankFunction.rank : {X : SSet} →
  {A : X.Subcomplex} → {P : A.Pairing} → {α : Type v} → [inst : PartialOrder α] → P.WeakRankFunction α → ↑P.II → α
-- Mathlib.Order.SuccPred.Limit
PredOrder.colimitRecOn_pred_of_not_isMin : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : PredOrder α]
  [inst_2 : WellFoundedGT α] (isMax : (a : α) → IsMax a → motive a)
  (pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
  (isPredLimit : (a : α) → Order.IsPredLimit a → ((b : α) → a < b → motive b) → motive a) (hb : ¬IsMin b),
  PredOrder.colimitRecOn (Order.pred b) isMax pred isPredLimit =
    pred b hb (PredOrder.colimitRecOn b isMax pred isPredLimit)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.erase_eq_empty_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  t.erase k = ∅ ↔ t = ∅ ∨ t.size = 1 ∧ k ∈ t
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.mk : {R : Type u_1} →
  [inst : Semiring R] →
    (vle : R → R → Prop) →
      (∀ (x y : R), vle x y ∨ vle y x) →
        (∀ {z y x : R}, vle x y → vle y z → vle x z) →
          (∀ {x y z : R}, vle x z → vle y z → vle (x + y) z) →
            (∀ {x y : R}, vle x y → ∀ (z : R), vle (x * z) (y * z)) →
              (∀ {x y z : R}, ¬vle z 0 → vle (x * z) (y * z) → vle x y) →
                ¬vle 1 0 → (∀ {x y : R}, vle (x * y) (y * x)) → ValuativeRel R
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.curry_inj : ∀ {c₁ c₂ : Nat.Partrec.Code} {n₁ n₂ : ℕ}, c₁.curry n₁ = c₂.curry n₂ → c₁ = c₂ ∧ n₁ = n₂
-- Mathlib.Topology.Order.LeftRightLim
/-- An antitone function is continuous to the left at a point if and only if its left limit
coincides with the value of the function.  -/
Antitone.continuousWithinAt_Iio_iff_leftLim_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Antitone f →
    ∀ {x : α} [inst_4 : TopologicalSpace α] [OrderTopology α],
      ContinuousWithinAt f (Set.Iio x) x ↔ Function.leftLim f x = f x
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.instFullUnderTopUnderForget : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T),
  (CategoryTheory.MorphismProperty.Under.forget P ⊤ X).Full
-- Mathlib.Computability.TuringMachine.Tape
_private.Mathlib.Computability.TuringMachine.Tape.0.Turing.ListBlank.append.match_1.splitter : {Γ : Type u_1} →
  [inst : Inhabited Γ] →
    (motive : List Γ → Turing.ListBlank Γ → Sort u_2) →
      (x : List Γ) →
        (x_1 : Turing.ListBlank Γ) →
          ((L : Turing.ListBlank Γ) → motive [] L) →
            ((a : Γ) → (l : List Γ) → (L : Turing.ListBlank Γ) → motive (a :: l) L) → motive x x_1
-- Mathlib.Algebra.Group.Action.Units
/-- If an action `G` associates and commutes with multiplication on `M`, then it lifts to an
action on `Mˣ`. Notably, this provides `MulAction Mˣ Nˣ` under suitable conditions.  -/
Units.mulAction' : {G : Type u_1} →
  {M : Type u_3} →
    [inst : Group G] →
      [inst_1 : Monoid M] → [inst_2 : MulAction G M] → [SMulCommClass G M M] → [IsScalarTower G M M] → MulAction G Mˣ
-- Mathlib.Topology.UniformSpace.UniformConvergence
tendstoUniformly_iff_tendstoUniformlyOnFilter : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι},
  TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_union : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} {fallback : β k}, (m₁.union m₂).getD k fallback = m₂.getD k (m₁.getD k fallback)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_eq_some_maxKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.maxKey? = some t.maxKey!
-- Mathlib.Data.FinEnum
FinEnum.mk : {α : Sort u_1} → (card : ℕ) → α ≃ Fin card → [decEq : DecidableEq α] → FinEnum α
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_rev : ∀ {w : ℕ} (x : BitVec w) (i : Fin w), x.getLsbD ↑i.rev = x.getMsbD ↑i
-- Mathlib.Analysis.Analytic.CPolynomial
HasFiniteFPowerSeriesOnBall.sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {pf pg : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n m : ℕ},
  HasFiniteFPowerSeriesOnBall f pf x n r →
    HasFiniteFPowerSeriesOnBall g pg x m r → HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (max n m) r
-- Mathlib.LinearAlgebra.LinearPMap
/-- The domain of the (semi)linear map.  -/
LinearPMap.domain : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_3} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_4} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → (E →ₛₗ.[σ] F) → Submodule R E
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instNeg : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommGroup M] →
        [inst_1 : TopologicalSpace M] → [IsTopologicalAddGroup M] → Neg (MeasureTheory.VectorMeasure α M)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_lt_one_of_one_lt_of_neg : ∀ {x : NNReal} {z : ℝ}, 1 < x → z < 0 → x ^ z < 1
-- Lean.Language.Basic
/-- Converts a typed snapshot to a `SnapshotTree` using the default (identity) transformation.

`toSnapshotTreeM` must be used instead when in context of a transformation, e.g. when implementing
`ToSnapshotTree`.
 -/
Lean.Language.toSnapshotTree : {α : Type} → [Lean.Language.ToSnapshotTree α] → α → Lean.Language.SnapshotTree
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.mkParserSeq : Array (Lean.Term × ℕ) → Lean.Elab.TermElabM (Lean.Term × ℕ)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- Reindex an additive free group basis through a bijection of the indexing sets.  -/
FreeAddGroupBasis.reindex : {ι : Type u_1} →
  {ι' : Type u_2} → {G : Type u_3} → [inst : AddGroup G] → FreeAddGroupBasis ι G → ι ≃ ι' → FreeAddGroupBasis ι' G
-- Init.Data.SInt.Lemmas
Int64.toISize_add : ∀ (a b : Int64), (a + b).toISize = a.toISize + b.toISize
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_ofDigits : ∀ (b : ℕ),
  1 < b → ∀ (L : List ℕ), (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (Nat.ofDigits b L) = L
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.aeval_iterate_derivative_self : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A] (p : Polynomial R)
  (q : ℕ) (r : A) {p' : Polynomial A},
  Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ q * p' →
    (Polynomial.aeval r) ((⇑Polynomial.derivative)^[q] p) = q.factorial • Polynomial.eval r p'
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.isOpenEmbedding_of_le : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U V : TopologicalSpace.Opens α} (i : U ≤ V),
  Topology.IsOpenEmbedding (Set.inclusion ⋯)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instMul.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [inst_2 : ContinuousMul M],
  SeparationQuotient.instMul = { mul := Quotient.map₂ (fun x1 x2 => x1 * x2) ⋯ }
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The endomorphisms of `F` are isomorphic to the limit over the fibers of `F` on all
Galois objects.  -/
CategoryTheory.PreGaloisCategory.endEquivSectionsFibers : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          CategoryTheory.End F ≃
            ↑((CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).comp (F.comp FintypeCat.incl)).sections
-- Init.Core
/-- Constructs a new thunk that forces `x` and then applies `x` to the result. Upon forcing, the result
of `f` is cached and the reference to the thunk `x` is dropped.
 -/
Thunk.map : {α : Type u_1} → {β : Type u_2} → (α → β) → Thunk α → Thunk β
-- Init.Data.Fin.Basic
Fin.val_ne_of_ne : ∀ {n : ℕ} {i j : Fin n}, i ≠ j → ↑i ≠ ↑j