mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Creates
/-- Any cocone lifts through the identity functor.  -/
CategoryTheory.idLiftsCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {K : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone (K.comp (CategoryTheory.Functor.id C))) →
            CategoryTheory.LiftableCocone K (CategoryTheory.Functor.id C) c
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonnegative, then
`f` is a monotone function.  -/
monotone_of_deriv_nonneg : ∀ {f : ℝ → ℝ}, Differentiable ℝ f → (∀ (x : ℝ), 0 ≤ deriv f x) → Monotone f
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {a : E} [inst_5 : CompleteSpace E] (hf : HasStrictFDerivAt f (↑f') a),
  a ∈ (HasStrictFDerivAt.toOpenPartialHomeomorph f hf).source
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.mkInv.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (f f_1 : Y ⟶ X) (e_f : f = f_1) (hf : W f) [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y],
  CategoryTheory.Localization.SmallHom.mkInv f hf = CategoryTheory.Localization.SmallHom.mkInv f_1 ⋯
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.exists_comap_evalRingHom_eq : ∀ {ι : Type u_3} {R : ι → Type u_4} [inst : (i : ι) → CommRing (R i)] [Finite ι] (p : PrimeSpectrum ((i : ι) → R i)),
  ∃ i q, PrimeSpectrum.comap (Pi.evalRingHom R i) q = p
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.map.match_1.eq_3 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3)
  (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1) →
        motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => h_2 a x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_3 x
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
/-- **Triangle Removal Lemma**. If there are not too many triangles (on the order of `(card α)^3`)
then they can all be removed by removing a few edges (on the order of `(card α)^2`).  -/
SimpleGraph.triangle_removal : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ},
  ↑(G.cliqueFinset 3).card < SimpleGraph.triangleRemovalBound ε * ↑(Fintype.card α) ^ 3 →
    ∃ G' ≤ G, ∃ x, ↑G.edgeFinset.card - ↑G'.edgeFinset.card < ε * ↑(Fintype.card α ^ 2) ∧ G'.CliqueFree 3
-- Mathlib.MeasureTheory.Constructions.Projective
MeasureTheory.IsProjectiveLimit.isProbabilityMeasure : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {μ : MeasureTheory.Measure ((i : ι) → α i)}
  [∀ (i : Finset ι), MeasureTheory.IsProbabilityMeasure (P i)],
  MeasureTheory.IsProjectiveLimit μ P → MeasureTheory.IsProbabilityMeasure μ
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_range_of_cauchy_map_cofinite : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : β → α},
  Cauchy (Filter.map f Filter.cofinite) → Bornology.IsBounded (Set.range f)
-- Mathlib.Data.Fin.Basic
Fin.instNontrivial : ∀ {n : ℕ} [n.AtLeastTwo], Nontrivial (Fin n)
-- Std.Data.ExtDHashMap.Basic
/-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.ExtDHashMap.ofList : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → List ((a : α) × β a) → Std.ExtDHashMap α β
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → Std.DTreeMap.Raw.Const.get! (m₁ \ m₂) k = default
-- Lean.Environment
/-- Like `findRec?` but also returns the constant that has `declName` in its `consts`, if any.  -/
_private.Lean.Environment.0.Lean.AsyncConsts.findRecAndParent? : Lean.AsyncConsts✝ → Lean.Name → Option (Lean.AsyncConst✝ × Option Lean.AsyncConst✝)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C),
  CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A =
    (CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{w + 1})).obj A.X
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.cast_lt_ofNat : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {m n : ℕ} [inst_5 : n.AtLeastTwo], ↑m < OfNat.ofNat n ↔ m < OfNat.ofNat n
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_lt_aleph0 : ∀ {o : Ordinal.{u_1}}, o.card < Cardinal.aleph0 ↔ o < Ordinal.omega0
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.stateful.injEq : ∀ (h h_1 : Lean.TSyntax `Lean.binderIdent),
  (Lean.Parser.Tactic.MRefinePat.stateful h = Lean.Parser.Tactic.MRefinePat.stateful h_1) = (h = h_1)
-- Mathlib.Order.Minimal
maximal_and_iff_right_of_imp : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : LE α],
  (∀ ⦃x : α⦄, P x → Q x) → (Maximal (fun x => P x ∧ Q x) x ↔ Maximal P x ∧ Q x)
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofMkLE_comp_ofLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ : C} (f : A₁ ⟶ B) [inst_1 : CategoryTheory.Mono f]
  (X Y : CategoryTheory.Subobject B) (h₁ : CategoryTheory.Subobject.mk f ≤ X) (h₂ : X ≤ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X h₁) (X.ofLE Y h₂) =
    CategoryTheory.Subobject.ofMkLE f Y ⋯
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.objIsoOfEq_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) {i j : X.I}
  (hij : i = j), (X.objIsoOfEq hij).symm = X.objIsoOfEq ⋯
-- Std.Do.WP.Monad
/-- A monad with weakest preconditions (`WP`) that is also a monad morphism, preserving `pure` and
`bind`.

In practice, `mvcgen` is not useful for reasoning about programs in a monad that is without a
`WPMonad` instance. The specification lemmas for `Pure.pure` and `Bind.bind`, as well as those for
operators like `Functor.map`, require that their monad have a `WPMonad` instance.
 -/
Std.Do.WPMonad : (m : Type u → Type v) → outParam Std.Do.PostShape → [Monad m] → Type (max (u + 1) v)
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.bracket_apply : ∀ {ι : Type v} (L : ι → Type w) [inst : (i : ι) → LieRing (L i)] (x y : DirectSum ι fun i => L i) (i : ι),
  ⁅x, y⁆ i = ⁅x i, y i⁆
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.Cb : (X : Type u) → (Y : Type v) → [MetricSpace X] → [MetricSpace Y] → Type (max v u)
-- Mathlib.Order.Hom.Basic
OrderIso.lt_iff_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {x y : α}, e x < e y ↔ x < y
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.String.0.String.fromExpr? : Lean.Expr → Lean.Meta.SimpM (Option String)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.not_mem_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, k ∈ t₂ → k ∉ t₁ \ t₂
-- Mathlib.Data.Finsupp.Multiset
/-- The `n`th symmetric power of a type `α` is naturally equivalent to the subtype of
finitely-supported maps `α →₀ ℕ` with total mass `n`.

See also `Sym.equivNatSumOfFintype` when `α` is finite.  -/
Sym.equivNatSum : (α : Type u_1) → [DecidableEq α] → (n : ℕ) → Sym α n ≃ { P // (P.sum fun x => id) = n }
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `k.left` is a monomorphism, then `k` is a monomorphism. In other words, `Over.forget X` reflects
monomorphisms.
The converse of `CategoryTheory.Over.mono_left_of_mono`.

This lemma is not an instance, to avoid loops in type class inference.
 -/
CategoryTheory.Over.mono_of_mono_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (k : f ⟶ g)
  [hk : CategoryTheory.Mono (CategoryTheory.Over.Hom.left k)], CategoryTheory.Mono k
-- Mathlib.LinearAlgebra.Matrix.Polynomial
Polynomial.leadingCoeff_det_X_one_add_C : ∀ {n : Type u_1} {α : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
  (Polynomial.X • 1 + A.map ⇑Polynomial.C).det.leadingCoeff = 1
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIoc_continuous : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  {p a : 𝕜} [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜]
  [inst_6 : TopologicalSpace B] {f : 𝕜 → B},
  f a = f (a + p) → ContinuousOn f (Set.Icc a (a + p)) → Continuous (AddCircle.liftIoc p a f)
-- Mathlib.Tactic.Simproc.Factors
Mathlib.Meta.Simproc.FactorsHelper.nil : ∀ {a : ℕ}, Mathlib.Meta.Simproc.FactorsHelper 1 a []
-- Mathlib.Topology.Basic
IsClosed.sdiff : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], IsClosed s → IsOpen t → IsClosed (s \ t)
-- Batteries.Tactic.Lint.Frontend
Batteries.Tactic.Lint.LintVerbosity.medium.sizeOf_spec : sizeOf Batteries.Tactic.Lint.LintVerbosity.medium = 1
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_toContinuousMapₐ : ∀ {α : Type u} {γ : Type w} (𝕜 : Type u_1) [inst : NormedField 𝕜] [inst_1 : TopologicalSpace α] [inst_2 : NormedRing γ]
  [inst_3 : NormedAlgebra 𝕜 γ] (f : BoundedContinuousFunction α γ),
  ⇑((BoundedContinuousFunction.toContinuousMapₐ 𝕜) f) = ⇑f
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_bif_eq_bif' : ∀ {w : ℕ} (d : Bool) (a b c : BitVec w),
  ((~~~bif d then a else c) == bif d then b else c) = bif d then ~~~a == b else ~~~c == c
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyFunctorIso_inv_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C]
  (X : HomologicalComplex C c),
  (HomologicalComplex.homologyFunctorIso C c i).inv.app X = CategoryTheory.CategoryStruct.id (X.homology i)
-- Mathlib.Algebra.Group.Subgroup.Basic
MulAut.characteristic.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Characteristic],
  MulAut.characteristic H =
    {
      toFun := fun φ =>
        { toFun := fun h => ⟨φ ↑h, ⋯⟩, invFun := fun h => ⟨(MulEquiv.symm φ) ↑h, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
          map_mul' := ⋯ },
      map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- a second integer  -/
CochainComplex.HomComplex.Triplet.q : {n : ℤ} → CochainComplex.HomComplex.Triplet n → ℤ
-- Mathlib.GroupTheory.CoprodI
/-- A free group is a free product of copies of the `FreeGroup` over one generator.  -/
freeGroupEquivCoprodI : {ι : Type u_1} → FreeGroup ι ≃* Monoid.CoprodI fun x => FreeGroup Unit
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out h
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.sub`. -/
MeasureTheory.ProgMeasurable.sub : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u v : ι → Ω → β} [inst_2 : MeasurableSpace ι] [inst_3 : AddGroup β]
  [ContinuousSub β],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStronglyProgressive f v → MeasureTheory.IsStronglyProgressive f fun i ω => u i ω - v i ω
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.biSup_normal : ∀ {G : Type u_2} [inst : AddGroup G] {ι : Type u_5} (s : Set ι) (H : ι → AddSubgroup G),
  (∀ i ∈ s, (H i).Normal) → (⨆ i ∈ s, H i).Normal
-- Mathlib.Order.Bounds.Image
IsLUB.of_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  (∀ {x y : α}, f y ≤ f x ↔ y ≤ x) → ∀ {s : Set α} {x : α}, IsLUB (f '' s) (f x) → IsLUB s x
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Commutative semirings. We support them using the envelope `OfCommRing.Q`  -/
Lean.Meta.Grind.Arith.CommRing.State.semirings : Lean.Meta.Grind.Arith.CommRing.State → Array Lean.Meta.Grind.Arith.CommRing.CommSemiring
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_smul_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (c : ℝ) (f : α → E),
  MeasureTheory.setToFun μ (fun s => c • T s) ⋯ f = c • MeasureTheory.setToFun μ T hT f
-- Mathlib.Order.CompleteLatticeIntervals
Set.Icc.coe_iSup : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) [Nonempty ι]
  {S : ι → ↑(Set.Icc a b)},
  have this := ⋯;
  ↑(iSup S) = ⨆ i, ↑(S i)
-- Mathlib.Algebra.Order.UpperLower
upperClosure_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] (s t : Set α),
  ↑(upperClosure s) + t = ↑(upperClosure (s + t))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_nat_mul_two_pi : ∀ (n : ℕ), Real.cos (↑n * (2 * Real.pi)) = 1
-- Lean.Server.FileWorker.InlayHints
Lean.Elab.InlayHintLabel.toLspInlayHintLabel : Lean.FileMap → Lean.Elab.InlayHintLabel → IO Lean.Lsp.InlayHintLabel
-- Mathlib.Algebra.Ring.Units
Units.divp_add_divp : ∀ {α : Type u} [inst : CommSemiring α] (a b : α) (u₁ u₂ : αˣ), a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_div_right₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Div β] [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) → ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.IndepFun (f i) (f j / f k) μ
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_mem_matrix_iff : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] {S : Set α},
  0 ∈ S → ∀ {d : n → α}, Matrix.diagonal d ∈ S.matrix ↔ ∀ (i : n), d i ∈ S
-- Std.Data.DTreeMap.Internal.Cell
/-- If there is a mapping, then it has a matching key.  -/
Std.DTreeMap.Internal.Cell.property : ∀ {α : Type u} [inst : Ord α] {β : α → Type v} {k : α → Ordering} (self : Std.DTreeMap.Internal.Cell α β k)
  [Std.OrientedOrd α] (p : (a : α) × β a), self.inner = some p → k p.fst = Ordering.eq
-- Init.Data.String.Lemmas.Basic
String.Slice.slice_startPos : ∀ {s : String.Slice} {p : s.Pos}, s.slice s.startPos p ⋯ = s.sliceTo p
-- Mathlib.Algebra.Group.Pointwise.Finset.Density
Finset.dens_smul_finset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] [inst_3 : Fintype β]
  (a : α) (s : Finset β), (a • s).dens = s.dens
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
CategoryTheory.Limits.hasColimitsOfShape_discrete : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteCoproducts C] (ι : Type w)
  [Finite ι], CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ι) C
-- Mathlib.Analysis.Calculus.FDeriv.Linear
ContinuousLinearMap.differentiableAt : ∀ {𝕜 : 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 →L[𝕜] F) {x : E}, DifferentiableAt 𝕜 (⇑f) x
-- Init.Data.SInt.Bitwise
instIdempotentOpInt64HOr : Std.IdempotentOp fun x1 x2 => x1 ||| x2
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.decidableMemNSMul : {α : Type u_2} →
  [inst : AddMonoid α] →
    {s : Set α} →
      [Fintype α] → [DecidableEq α] → [DecidablePred fun x => x ∈ s] → (n : ℕ) → DecidablePred fun x => x ∈ n • s
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.isoMk_inv_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {x y : CategoryTheory.Core C} (e : x.of ≅ y.of),
  (CategoryTheory.Core.isoMk e).inv.iso = e.symm
-- Init.Data.ByteArray.Basic
ByteArray.instGetElemNatUInt8LtSize : GetElem ByteArray ℕ UInt8 fun xs i => i < xs.size
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.ext : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  ⦃η η' : ApplicativeTransformation F G⦄,
  (∀ (α : Type u) (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x) → η = η'
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
/-- The `Z`-coordinate of a representative of `P + Q` for two distinct projective point
representatives `P` and `Q` on a Weierstrass curve.

If the representatives of `P` and `Q` are equal, then this returns the value `0`.  -/
WeierstrassCurve.Projective.addZ : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → (Fin 3 → R) → R
-- Init.Data.String.Lemmas.FindPos
String.Slice.posGE_eq_iff : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos},
  s.posGE p h = q ↔ p ≤ q.offset ∧ ∀ (q' : s.Pos), p ≤ q'.offset → q ≤ q'
-- Init.Data.List.Find
List.findFinIdx?.eq_1 : ∀ {α : Type u} (p : α → Bool) (l : List α), List.findFinIdx? p l = List.findFinIdx?.go p l l 0 ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.preservesLimitIso_hom_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesLimit F G]
  [inst_4 : CategoryTheory.Limits.HasLimit F] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).hom
      (CategoryTheory.Limits.limit.π (F.comp G) j) =
    G.map (CategoryTheory.Limits.limit.π F j)
-- Init.Internal.Order.Lemmas
Lean.Order.SeqRight.monotone_seqRight : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] [LawfulMonad m] (f : γ → m α) (g : γ → m β),
  Lean.Order.monotone g → Lean.Order.monotone f → Lean.Order.monotone fun x => g x *> f x
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedCtorInfo : Inhabited Lean.IR.CtorInfo
-- Batteries.Data.List.Lemmas
List.erase_eq_self_iff_forall_bne : ∀ {α : Type u_1} [inst : BEq α] (a : α) (xs : List α), xs.erase a = xs ↔ ∀ x ∈ xs, ¬(x == a) = true
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_right_inj : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r₁ r₂ : R} {m : M},
  MonoidAlgebra.single m r₁ = MonoidAlgebra.single m r₂ ↔ r₁ = r₂
-- Init.Data.Rat.Lemmas
Rat.den_normalize : ∀ {num : ℤ} {den : ℕ} (den_nz : den ≠ 0), (Rat.normalize num den den_nz).den = den / num.natAbs.gcd den
-- Mathlib.Algebra.Group.Defs
AddCancelCommMonoid.toAddCancelMonoid.eq_1 : ∀ (M : Type u) [inst : AddCancelCommMonoid M],
  AddCancelCommMonoid.toAddCancelMonoid M =
    { toAddLeftCancelMonoid := inst.toAddLeftCancelMonoid, toIsRightCancelAdd := ⋯ }
-- Mathlib.Data.TypeVec
TypeVec.typevecCasesCons₂_appendFun : ∀ (n : ℕ) (t : Type u_1) (t' : Type u_2) (v : TypeVec.{u_1} n) (v' : TypeVec.{u_2} n)
  {β : (v ::: t).Arrow (v' ::: t') → Sort u_3} (F : (f : t → t') → (fs : v.Arrow v') → β (fs ::: f)) (f : t → t')
  (fs : v.Arrow v'), TypeVec.typevecCasesCons₂ n t t' v v' F (fs ::: f) = F f fs
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
trdeg_eq_zero : ∀ {R : Type u_3} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsAlgebraic R A], Algebra.trdeg R A = 0
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- If `g : ι → G × G` converges to the uniformity, then any `f : ι → G × G`
converges to the uniformity iff `f + g` does. This is often useful when `g` is valued in the
diagonal, in which case its convergence is automatic.  -/
Filter.Tendsto.uniformity_add_iff_left : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {f g : ι → α × α}
  {l : Filter ι},
  Filter.Tendsto g l (uniformity α) → (Filter.Tendsto (f + g) l (uniformity α) ↔ Filter.Tendsto f l (uniformity α))
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure.eq_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  (f : α → C) (x : ℕ),
  CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure✝ f x =
    match x with
    | 0 => ⟨ULift.{v, w} α, f ∘ ULift.down⟩
    | n.succ =>
      ⟨CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep✝ (n + 1) fun m x =>
          CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure✝ f m,
        CategoryTheory.IsFiltered.FilteredClosureSmall.inductiveStepRealization✝ (n + 1) fun m x =>
          CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure✝ f m⟩
-- Mathlib.Algebra.Algebra.Unitization
Unitization.starLift_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : StarRing C]
  [inst_10 : StarModule R C] (φ : Unitization R A →⋆ₐ[R] C),
  Unitization.starLift.symm φ = φ.toNonUnitalStarAlgHom.comp (Unitization.inrNonUnitalStarAlgHom R A)