mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.CharP.Frobenius
frobenius_def : ∀ {R : Type u_1} [inst : CommSemiring R] (p : ℕ) [inst_1 : ExpChar R p] (x : R), (frobenius R p) x = x ^ p
-- Mathlib.Topology.Order.LeftRightNhds
/-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `[l, a)`
with `l < a`.  -/
mem_nhdsLT_iff_exists_Ico_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMinOrder α]
  [DenselyOrdered α] {a : α} {s : Set α}, s ∈ nhdsWithin a (Set.Iio a) ↔ ∃ l ∈ Set.Iio a, Set.Ico l a ⊆ s
-- Mathlib.Analysis.Distribution.TemperedDistribution
MeasureTheory.Lp.toTemperedDistribution.eq_1 : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : CompleteSpace F] [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E]
  {μ : MeasureTheory.Measure E} [hμ : μ.HasTemperateGrowth] {p : ENNReal} [hp : Fact (1 ≤ p)]
  (f : ↥(MeasureTheory.Lp F p μ)),
  MeasureTheory.Lp.toTemperedDistribution f =
    (ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) (SchwartzMap E ℂ) F)
      ((ContinuousLinearMap.lpPairing μ p (1 - p⁻¹)⁻¹ (ContinuousLinearMap.lsmul ℂ ℂ).flip) f ∘SL
        SchwartzMap.toLpCLM ℂ ℂ (1 - p⁻¹)⁻¹ μ)
-- Mathlib.Order.WithBot
WithTop.toDual_le_toDual_iff : ∀ {α : Type u_1} [inst : LE α] {x y : WithTop α}, WithTop.toDual y ≤ WithTop.toDual x ↔ x ≤ y
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.hom_one : ∀ (X Y : MonCat), MonCat.Hom.hom 1 = 1
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.vars_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] [inst_1 : DecidableEq τ]
  (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R),
  ((MvPolynomial.bind₁ f) φ).vars ⊆ φ.vars.biUnion fun i => (f i).vars
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- Given a function on `𝕜`, return the unique function on `AddCircle p` agreeing with `f` on
`[a, a + p)`.  -/
AddCircle.liftIco : {𝕜 : Type u_1} →
  {B : Type u_2} →
    [inst : AddCommGroup 𝕜] →
      (p : 𝕜) →
        [inst_1 : LinearOrder 𝕜] →
          [IsOrderedAddMonoid 𝕜] → [hp : Fact (0 < p)] → 𝕜 → [Archimedean 𝕜] → (𝕜 → B) → AddCircle p → B
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalizer_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [h : H.Normal], AddSubgroup.normalizer ↑H = ⊤
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.dual_id : ∀ {α : Type u_2} [inst : InfSet α], sInfHom.dual (sInfHom.id α) = sSupHom.id αᵒᵈ
-- Mathlib.Logic.Nontrivial.Defs
/-- Pullback a `Nontrivial` instance along a surjective function.  -/
Function.Surjective.nontrivial : ∀ {α : Type u_1} {β : Type u_2} [Nontrivial β] {f : α → β}, Function.Surjective f → Nontrivial α
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_app' : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : TopologicalSpace.Opens ↥↑U),
  AlgebraicGeometry.Scheme.Hom.app (f ∣_ U) V =
    AlgebraicGeometry.Scheme.Hom.appLE f ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V)
      ((AlgebraicGeometry.Scheme.Hom.opensFunctor ((TopologicalSpace.Opens.map f.base).obj U).ι).obj
        ((TopologicalSpace.Opens.map (f ∣_ U).base).obj V))
      ⋯
-- Mathlib.Data.Nat.Choose.Basic
Nat.multichoose.eq_def : ∀ (x x_1 : ℕ),
  x.multichoose x_1 =
    match x, x_1 with
    | x, 0 => 1
    | 0, n.succ => 0
    | n.succ, k.succ => n.multichoose (k + 1) + (n + 1).multichoose k
-- Mathlib.Algebra.Regular.Basic
/-- A sum is add-regular if and only if the summands are.  -/
isAddRegular_add_iff : ∀ {R : Type u_1} [inst : AddCommSemigroup R] {a b : R}, IsAddRegular (a + b) ↔ IsAddRegular a ∧ IsAddRegular b
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The natural transformation `K.restriction e ⟶ K.truncGE' e` for all `K`.  -/
ComplexShape.Embedding.restrictionToTruncGE'NatTrans : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          [inst : e.IsTruncGE] →
            (C : Type u_4) →
              [inst_1 : CategoryTheory.Category.{v_2, u_4} C] →
                [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
                  [inst_3 : CategoryTheory.CategoryWithHomology C] → e.restrictionFunctor C ⟶ e.truncGE'Functor C
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.funLike.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N],
  ZeroHom.funLike = { coe := ZeroHom.toFun, coe_injective := ⋯ }
-- Mathlib.Algebra.Ring.Defs
/-- The canonical map `ℕ → R` sends `0 : ℕ` to `0 : R`.  -/
NonAssocRing.natCast_zero : ∀ {α : Type u_1} [self : NonAssocRing α], ↑0 = 0
-- Mathlib.Topology.ContinuousMap.Algebra
/-- The subring of continuous maps `α → β`.  -/
continuousSubring : (α : Type u_1) →
  (R : Type u_2) →
    [TopologicalSpace α] → [inst : TopologicalSpace R] → [inst_1 : Ring R] → [IsTopologicalRing R] → Subring (α → R)
-- Mathlib.Computability.Primrec.Basic
PrimrecRel.decide : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {R : α → β → Prop}
  [inst_2 : DecidableRel R], PrimrecRel R → Primrec₂ fun a b => decide (R a b)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_of_subsingleton : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  [Subsingleton E], MDiffAt[s] f x
-- Mathlib.GroupTheory.OreLocalization.OreSet
AddOreLocalization.addOreSetComm : {R : Type u_2} → [inst : AddCommMonoid R] → (S : AddSubmonoid R) → AddOreLocalization.AddOreSet S
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mem_map_equiv : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {f : R ≃+* S}
  {K : NonUnitalSubsemiring R} {x : S}, x ∈ NonUnitalSubsemiring.map (↑f) K ↔ f.symm x ∈ K
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- Given a closed embedding into a completely metrizable space,
the source space is also completely metrizable.  -/
Topology.IsClosedEmbedding.IsCompletelyMetrizableSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [TopologicalSpace.IsCompletelyMetrizableSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → TopologicalSpace.IsCompletelyMetrizableSpace X
-- Mathlib.Analysis.Normed.Group.Quotient
/-- An isometric version of `Submodule.quotientQuotientEquivQuotient`.  -/
Submodule.quotientQuotientLIEQuotient : {M : Type u_1} →
  [inst : SeminormedAddCommGroup M] →
    {R : Type u_3} →
      [inst_1 : Ring R] →
        [inst_2 : Module R M] → (S T : Submodule R M) → S ≤ T → (M ⧸ S) ⧸ Submodule.map S.mkQ T ≃ₗᵢ[R] M ⧸ T
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.sum_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {P Q : CategoryTheory.Idempotents.Karoubi C} {α : Type u_2} (s : Finset α) (f : α → (P ⟶ Q)),
  (∑ x ∈ s, f x).f = ∑ x ∈ s, (f x).f
-- Mathlib.Data.DFinsupp.Defs
/-- Equivalence between dependent functions with finite support `s : Finset ι` and functions
`∀ i, {x : β i // x ≠ 0}`.  -/
DFinsupp.subtypeSupportEqEquiv : {ι : Type u} →
  {β : ι → Type v} →
    [inst : DecidableEq ι] →
      [inst_1 : (i : ι) → Zero (β i)] →
        [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] →
          (s : Finset ι) → { f // f.support = s } ≃ ((i : ↥s) → { x // x ≠ 0 })
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.leftUnitor_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} {X : C},
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor F).hom.app X =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- The **Woodbury Identity** (`⁻¹` version).

See `add_mul_mul_inv_eq_sub'` for the binomial inverse theorem.  -/
Matrix.add_mul_mul_inv_eq_sub : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α)
  (V : Matrix m n α),
  IsUnit A → IsUnit C → IsUnit (C⁻¹ + V * A⁻¹ * U) → (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.unoneD_eq_iff : ∀ {α : Type u} {d y : α} {x : WithOne α}, WithOne.unoneD d x = y ↔ x = ↑y ∨ x = 1 ∧ y = d
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- A version of `Set.pi` for `AddSubgroup`s. Given an index set `I` and a family
of submodules `s : Π i, AddSubgroup f i`, `pi I s` is the `AddSubgroup` of dependent functions
`f : Π i, f i` such that `f i` belongs to `pi I s` whenever `i ∈ I`.  -/
AddSubgroup.pi : {η : Type u_7} →
  {f : η → Type u_8} →
    [inst : (i : η) → AddGroup (f i)] → Set η → ((i : η) → AddSubgroup (f i)) → AddSubgroup ((i : η) → f i)
-- Mathlib.Order.Circular
sbtw_cyclic_right : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw c a b
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.modMonomial_X : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (i : σ), ((MvPolynomial.X i).modMonomial fun₀ | i => 1) = 0
-- Mathlib.Data.Int.Init
Int.div_le_div_iff_of_dvd_of_pos_of_neg : ∀ {a b c d : ℤ}, 0 < b → d < 0 → b ∣ a → d ∣ c → (a / b ≤ c / d ↔ c * b ≤ d * a)
-- Mathlib.Topology.DerivedSet
isClosed_iff_derivedSet_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] (A : Set X), IsClosed A ↔ derivedSet A ⊆ A
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.tan_eq_inv_of_two_zsmul_add_two_zsmul_eq_pi : ∀ {θ ψ : Real.Angle}, 2 • θ + 2 • ψ = ↑Real.pi → ψ.tan = θ.tan⁻¹
-- Mathlib.Analysis.SpecialFunctions.Sqrt
deriv_sqrt : ∀ {f : ℝ → ℝ} {x : ℝ}, DifferentiableAt ℝ f x → f x ≠ 0 → deriv (fun x => √(f x)) x = deriv f x / (2 * √(f x))
-- Mathlib.Algebra.Module.Presentation.Tautological
/-- The tautological presentation of any `A`-module `M` by generators and relations.
There is a generator `[m]` for any element `m : M`, and there are two types of relations:
* `[m₁] + [m₂] - [m₁ + m₂] = 0`
* `a • [m] - [a • m] = 0`.  -/
Module.Presentation.tautological : (A : Type u) →
  [inst : Ring A] → (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module A M] → Module.Presentation A M
-- Mathlib.Data.Seq.Basic
Stream'.Seq.set_cons_succ : ∀ {α : Type u} (hd x : α) (tl : Stream'.Seq α) (n : ℕ),
  (Stream'.Seq.cons hd tl).set (n + 1) x = Stream'.Seq.cons hd (tl.set n x)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_14} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_15}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_16} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {p : M × M'} {f : M → N} {g : M' → N'},
  MDiffAt f p.1 → MDiffAt g p.2 → mfderiv% (Prod.map f g) p = (mfderiv% f p.1).prodMap (mfderiv% g p.2)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getThenInsertIfNew?_snd : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {v : β}, (Std.DTreeMap.Const.getThenInsertIfNew? t k v).2 = t.insertIfNew k v
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
/-- The Cauchy product formula for the product of two infinite sums indexed by `ℕ`,
expressed by summing on `Finset.range`.
See also `tsum_mul_tsum_eq_tsum_sum_range` if `f` and `g` are
not absolutely summable, and `tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm'` when the
space is not complete.  -/
tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm : ∀ {R : Type u_1} [inst : NormedRing R] [CompleteSpace R] {f g : ℕ → R},
  (Summable fun x => ‖f x‖) →
    (Summable fun x => ‖g x‖) →
      (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ Finset.range (n + 1), f k * g (n - k)
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.mk'_mk_eq_div : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] {r s : A} (hs : s ∈ nonZeroDivisors A),
  IsLocalization.mk' K r ⟨s, hs⟩ = (algebraMap A K) r / (algebraMap A K) s
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- Register on the tangent space to a normed vector space the same `NormedAddCommGroup` structure
as in the vector space.

Should not be a global instance, as it does not coincide definitionally with the Riemannian
structure for inner product spaces, but can be activated locally.  -/
normedAddCommGroupTangentSpaceVectorSpace : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] → (x : E) → NormedAddCommGroup (TangentSpace (modelWithCornersSelf ℝ E) x)
-- Mathlib.Algebra.Order.Monovary
Antivary.mul_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : PartialOrder β] {f₁ f₂ : ι → α} {g : ι → β},
  0 ≤ f₁ → 0 ≤ f₂ → Antivary f₁ g → Antivary f₂ g → Antivary (f₁ * f₂) g
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₂₃ : ρ₂₃.I₂₃) (h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃),
  CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h =
    CategoryTheory.CategoryStruct.comp
      ((F.obj (X₁ i₁)).map (CategoryTheory.GradedObject.ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ i₂₃ h₂₃))
      (CategoryTheory.GradedObject.ιMapBifunctorMapObj F ρ₂₃.q X₁
        (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ i₂₃ j ⋯)
-- Lean.Meta.Basic
Lean.Meta.instMonadEnvMetaM : Lean.MonadEnv Lean.MetaM
-- Mathlib.Topology.Order.LeftRightNhds
nhdsGE_basis_Ico : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α),
  (nhdsWithin a (Set.Ici a)).HasBasis (fun u => a < u) (Set.Ico a)
-- Init.Data.Nat.Div.Lemmas
Nat.div_eq_zero_iff_lt : ∀ {k x : ℕ}, 0 < k → (x / k = 0 ↔ x < k)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  k ∉ t → l.contains k = false → (Std.DTreeMap.Const.insertManyIfNewUnit t l).getKey? k = none
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Limit cones on `F` are unique up to isomorphism.  -/
CategoryTheory.Limits.IsLimit.uniqueUpToIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {s t : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit s → CategoryTheory.Limits.IsLimit t → (s ≅ t)
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.toAddGroupSeminorm : {R : Type u_2} → [inst : NonUnitalNonAssocRing R] → RingSeminorm R → AddGroupSeminorm R
-- Init.Data.UInt.Basic
/-- Multiplies two 32-bit unsigned integers, wrapping around on overflow.  Usually accessed via the `*`
operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.mul : UInt32 → UInt32 → UInt32
-- Lean.Server.References
/-- Gets the set of declarations of `mod`.  -/
Lean.Server.References.getDecls? : Lean.Server.References → Lean.Name → Option Lean.Lsp.Decls
-- Lean.Meta.Sym.Offset
Lean.Meta.Sym.Offset.num.injEq : ∀ (k k_1 : ℕ), (Lean.Meta.Sym.Offset.num k = Lean.Meta.Sym.Offset.num k_1) = (k = k_1)
-- Init.PropLemmas
exists₂_congr : ∀ {α : Sort u_1} {β : α → Sort u_2} {p q : (a : α) → β a → Prop},
  (∀ (a : α) (b : β a), p a b ↔ q a b) → ((∃ a b, p a b) ↔ ∃ a b, q a b)
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Typeclass for expressing that a type `M₀` with multiplication and a zero satisfies
`0 * a = 0` and `a * 0 = 0` for all `a : M₀`.  -/
MulZeroClass : Type u → Type u
-- Mathlib.Data.Finset.PiInduction
/-- General theorem for `Finset.induction_on_pi`-style induction principles.  -/
Finset.induction_on_pi_of_choice : ∀ {ι : Type u_1} {α : ι → Type u_2} [Finite ι] [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
  (r : (i : ι) → α i → Finset (α i) → Prop),
  (∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)) →
    ∀ {p : ((i : ι) → Finset (α i)) → Prop} (f : (i : ι) → Finset (α i)),
      (p fun x => ∅) →
        (∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
            r i x (g i) → p g → p (Function.update g i (insert x (g i)))) →
          p f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∪ t₂)[k]? = t₁[k]?
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.integrable_pair : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α E}
  {g : MeasureTheory.SimpleFunc α F},
  MeasureTheory.Integrable (⇑f) μ → MeasureTheory.Integrable (⇑g) μ → MeasureTheory.Integrable (⇑(f.pair g)) μ
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
/-- Restrict the codomain of a continuous linear map `f` to `f.range`.  -/
ContinuousLinearMap.rangeRestrict : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            {M₂ : Type u_5} →
              [inst_2 : TopologicalSpace M₁] →
                [inst_3 : AddCommMonoid M₁] →
                  [inst_4 : Module R₁ M₁] →
                    [inst_5 : TopologicalSpace M₂] →
                      [inst_6 : AddCommMonoid M₂] →
                        [inst_7 : Module R₂ M₂] →
                          [inst_8 : RingHomSurjective σ₁₂] → (f : M₁ →SL[σ₁₂] M₂) → M₁ →SL[σ₁₂] ↥(↑f).range
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
Std.Iterators.Types.DropWhile.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)}
  [inst : SizeOf α] [inst_1 : (a : Type w) → SizeOf (m a)] [inst_2 : SizeOf β] (dropping : Bool)
  (inner : Std.IterM m β), sizeOf { dropping := dropping, inner := inner } = 1 + sizeOf dropping + sizeOf inner
-- Mathlib.CategoryTheory.Groupoid.VertexGroup
/-- **Alias** of `CategoryTheory.Functor.mapVertexGroup`.

---

A functor defines a morphism of vertex groups.  -/
CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup : {C : Type u} →
  [inst : CategoryTheory.Groupoid C] →
    {D : Type v} →
      [inst_1 : CategoryTheory.Groupoid D] → (φ : CategoryTheory.Functor C D) → (c : C) → (c ⟶ c) →* (φ.obj c ⟶ φ.obj c)
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzOnWith.isBounded_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : PseudoMetricSpace γ] (f : α → β → γ) {K₁ K₂ : NNReal} {s : Set α} {t : Set β},
  Bornology.IsBounded s →
    Bornology.IsBounded t →
      (∀ b ∈ t, LipschitzOnWith K₁ (fun a => f a b) s) →
        (∀ a ∈ s, LipschitzOnWith K₂ (f a) t) → Bornology.IsBounded (Set.image2 f s t)
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- The terms of the sequence have norm bounded by `B`.  -/
NumberField.Units.dirichletUnitTheorem.seq_norm_le : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (w₁ : NumberField.InfinitePlace K) {B : ℕ}
  (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B)
  (n : ℕ), ((Algebra.norm ℤ) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n)).natAbs ≤ B
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- An auxiliary typeclass for the Fundamental theorem of calculus, part 1. It is used to formulate
theorems that work simultaneously for left and right one-sided derivatives of `∫ x in u..v, f x`.  -/
intervalIntegral.FTCFilter : outParam ℝ → Filter ℝ → outParam (Filter ℝ) → Prop
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.eq_top_pullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {S T : CategoryTheory.Sieve X},
  S ≤ T → ∀ (f : Y ⟶ X), S.arrows f → CategoryTheory.Sieve.pullback f T = ⊤
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instInfSet.eq_1 : ∀ {α : Type u_1} [inst : LE α], UpperSet.instInfSet = { sInf := fun S => { carrier := ⋃ s ∈ S, ↑s, upper' := ⋯ } }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_eq_get : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} {h : a ∈ t}, Std.DTreeMap.Const.get t a h = t.get a h
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Cases.and_3 : ∀ {σs : List (Type u_1)} {Q H₁ H₂ H T : Std.Do.SPred σs}, (H ⊣⊢ₛ H₁ ∧ H₂) → ((Q ∧ H₂) ∧ H₁ ⊢ₛ T) → Q ∧ H ⊢ₛ T
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.const_add : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f : α → M}
  [MeasurableAdd M], Measurable f → ∀ (c : M), Measurable fun x => c + f x
-- Mathlib.Algebra.Star.Basic
conj_trivial : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : StarRing R] [TrivialStar R] (a : R), (starRingEnd R) a = a
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.singleAddHom.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M),
  AddMonoidAlgebra.singleAddHom m = { toFun := AddMonoidAlgebra.single m, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.comul_hom : ∀ {X : SFinKer}, CategoryTheory.ComonObj.comul.hom = ProbabilityTheory.Kernel.copy X.carrier