mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Bounding the Hausdorff distance by bounding the distance of any point
in each set to the other set  -/
Metric.hausdorffDist_le_of_infDist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {r : ℝ},
  0 ≤ r → (∀ x ∈ s, Metric.infDist x t ≤ r) → (∀ x ∈ t, Metric.infDist x s ≤ r) → Metric.hausdorffDist s t ≤ r
-- Mathlib.Order.Bounds.Basic
lowerBounds_le_upperBounds : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a b : α}, a ∈ lowerBounds s → b ∈ upperBounds s → s.Nonempty → a ≤ b
-- Mathlib.Topology.UniformSpace.Compact
unique_uniformity_of_compact : ∀ {γ : Type uc} [t : TopologicalSpace γ] [CompactSpace γ] {u u' : UniformSpace γ},
  u.toTopologicalSpace = t → u'.toTopologicalSpace = t → u = u'
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.HasUnifEigenvector.pow_apply : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {v : M}, f.HasUnifEigenvector μ 1 v → ∀ (n : ℕ), (f ^ n) v = μ ^ n • v
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- The Zariski topology on the prime spectrum of a commutative (semi)ring is defined
via the closed sets of the topology: they are exactly those sets that are the zero locus
of a subset of the ring.  -/
PrimeSpectrum.zariskiTopology : {R : Type u} → [inst : CommSemiring R] → TopologicalSpace (PrimeSpectrum R)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_leftUnitor_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X : C) {Z : D}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.ε F) (F.obj X))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) h))
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normalClosure_def' : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] (K : IntermediateField F L)
  [Normal F L], IntermediateField.normalClosure F (↥K) L = ⨆ f, IntermediateField.map f K
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.measure_Ioo_pos : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X] {m : MeasurableSpace X}
  (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [DenselyOrdered X] {a b : X}, 0 < μ (Set.Ioo a b) ↔ a < b
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.log_five_lt_d9 : Real.log 5 < 1.6094379126
-- Mathlib.RingTheory.WittVector.MulP
_private.Mathlib.RingTheory.WittVector.MulP.0.WittVector.wittMulN.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Control.Bitraversable.Basic
Bitraversable.bitraverse : {t : Type u → Type u → Type u} →
  [self : Bitraversable t] →
    {m : Type u → Type u} → [Applicative m] → {α α' β β' : Type u} → (α → m α') → (β → m β') → t α β → m (t α' β')
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.getTermOpIds : Lean.Expr → Lean.Meta.Grind.GoalM (List ℕ)
-- Lean.Meta.Sym.Pattern
/-- Returns `true` if `e` is an assigned metavariable.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isAssignedMVar : Lean.Expr → Lean.MetaM Bool
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.prod_le : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α]
  {a b : Associates.FactorSet α}, a.prod ≤ b.prod ↔ a ≤ b
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.methodNotFound.sizeOf_spec : sizeOf Lean.JsonRpc.ErrorCode.methodNotFound = 1
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Two pseudometric space structures with the same distance function coincide.  -/
PseudoMetricSpace.ext : ∀ {α : Type u_3} {m m' : PseudoMetricSpace α}, m.toDist = m'.toDist → m = m'
-- Mathlib.Data.Stream.Init
Stream'.nil_append_stream : ∀ {α : Type u} (s : Stream' α), [] ++ₛ s = s
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.π.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] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)],
  CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.π✝ f n₀ =
    CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ 0)
      ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op 0)).obj.π
-- Mathlib.Algebra.Module.Submodule.LinearMap
Submodule.subtype_apply : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} {p : Submodule R M}
  (x : ↥p), p.subtype x = ↑x
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
IsIntegral.smul : ∀ {B : Type u_3} {S : Type u_4} [inst : Ring B] [inst_1 : CommRing S] {R : Type u_5} [inst_2 : CommSemiring R]
  [inst_3 : Algebra R B] [inst_4 : Algebra S B] [inst_5 : Algebra R S] [IsScalarTower R S B] {x : B} (r : R),
  IsIntegral S x → IsIntegral S (r • x)
-- Init.Data.SInt.Lemmas
Int16.toInt64_toISize : ∀ (n : Int16), n.toISize.toInt64 = n.toInt64
-- Mathlib.Algebra.Group.Defs
pow_three' : ∀ {M : Type u_2} [inst : Monoid M] (a : M), a ^ 3 = a * a * a
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.instReprTZSpec : Repr Std.Time.Database.TZdb.TZSpec
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_eq_sum : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m] (v : m → α)
  (M : Matrix m n α), Matrix.vecMul v M = ∑ i, v i • M i
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of a function `f` equals the order of `-f`.  -/
meromorphicOrderAt_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E}, meromorphicOrderAt f x = meromorphicOrderAt (-f) x
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- Two vector measures `v` and `w` are said to be mutually singular if there exists a measurable
set `s`, such that for all `t ⊆ s`, `v t = 0` and for all `t ⊆ sᶜ`, `w t = 0`.

We note that we do not require the measurability of `t` in the definition since this makes it easier
to use. This is equivalent to the definition which requires measurability. To prove
`MutuallySingular` with the measurability condition, use
`MeasureTheory.VectorMeasure.MutuallySingular.mk`.  -/
MeasureTheory.VectorMeasure.MutuallySingular : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : AddCommMonoid M] →
          [inst_1 : TopologicalSpace M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : TopologicalSpace N] → MeasureTheory.VectorMeasure α M → MeasureTheory.VectorMeasure α N → Prop
-- Mathlib.Order.Basic
Subtype.decidableLE : {α : Type u_2} → [inst : Preorder α] → [h : DecidableLE α] → {p : α → Prop} → DecidableLE (Subtype p)
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.needEscape.go.eq_def : ∀ (s : String) (i : ℕ),
  Lean.Json.needEscape.go✝ s i =
    if h : i < s.utf8ByteSize then
      let byte := s.getUTF8Byte { byteIdx := i } h;
      have h1 := ⋯;
      have h2 := Lean.Json.needEscape.go._proof_4✝;
      if ((↑Lean.Json.escapeTable✝).get byte.toNat ⋯ == 0) = true then Lean.Json.needEscape.go✝ s (i + 1) else true
    else false
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerMeasure_eq_iInf : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (A : Set G),
  μ.outerMeasure A = ⨅ U, ⨅ (hU : IsOpen U), ⨅ (_ : A ⊆ U), μ.innerContent { carrier := U, is_open' := hU }
-- Mathlib.RingTheory.Polynomial.GaussNorm
/-- If `v` is a nonnegative function with `v 0 = 0` and `c` is nonnegative, the Gauss norm of a
polynomial is equal to its Gauss norm as a power series.  -/
Polynomial.gaussNorm_coe_powerSeries : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) {c : ℝ} (p : Polynomial R)
  [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ], 0 ≤ c → PowerSeries.gaussNorm (⇑v) c ↑p = Polynomial.gaussNorm v c p
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.dropSuffix?_slice_of_isEmpty : ∀ {pat s : String.Slice}, pat.isEmpty = true → s.dropSuffix? pat = some s
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.neg_add_cancel_left : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α) (b : α), ↑(-a) + (↑a + b) = b
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- An affine combination with `affineCombinationSingleWeights` gives the specified point.  -/
Finset.affineCombination_affineCombinationSingleWeights : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] (p : ι → P) {i : ι},
  i ∈ s → (Finset.affineCombination k s p) (Finset.affineCombinationSingleWeights k i) = p i
-- Mathlib.RingTheory.Coalgebra.GroupLike
/-- The type of group-like elements in a coalgebra.  -/
GroupLike : (R : Type u_2) →
  (A : Type u_3) →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [Coalgebra R A] → Type u_3
-- Mathlib.RingTheory.Frobenius
/-- Let `G` be a finite group acting on `S`, and `R` be the fixed subring.
If `Q` is a prime of `S` with finite residue field,
then there exists a Frobenius element `σ : G` at `Q`.  -/
IsArithFrobAt.exists_of_isInvariant : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (G : Type u_3)
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [inst_5 : SMulCommClass G R S] (Q : Ideal S) [Finite G]
  [Algebra.IsInvariant R S G] [Q.IsPrime] [Finite (S ⧸ Q)], ∃ σ, IsArithFrobAt R σ Q
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.ofCommaMorphism_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {c c' :
    CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D))}
  (φ : c ⟶ c') (x : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.ofCommaMorphism φ).app x =
    match x with
    | CategoryTheory.WithInitial.of x => φ.right.app x
    | CategoryTheory.WithInitial.star => φ.left
-- Mathlib.Topology.Maps.Strict.Basic
/-- An embedding is strict. See also `isEmbedding_iff_isStrictMap_injective`.  -/
Topology.IsEmbedding.isStrictMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsEmbedding f → Topology.IsStrictMap f
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_map_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) {X Y : CategoryTheory.MorphismProperty.Comma L₂ R P Q W} (f : X ⟶ Y),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).inverse.map f).left =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f).left
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.finite : ∀ {α : Type u_1} {M : Matroid α} {B : Set α} [M.RankFinite], M.IsBase B → B.Finite
-- Mathlib.Logic.Equiv.Defs
/-- An equivalence `e : α ≃ β` generates an equivalence between quotient spaces,
if `ra a₁ a₂ ↔ rb (e a₁) (e a₂)`.  -/
Quotient.congr : {α : Sort u} →
  {β : Sort v} →
    {ra : Setoid α} →
      {rb : Setoid β} → (e : α ≃ β) → (∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)) → Quotient ra ≃ Quotient rb
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_eq_empty : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, ¬a < b → Set.Ioo a b = ∅
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_toSubsemigroup : ∀ {M : Type u_2} [inst : MulOneClass M] (H : Submonoid Mᵐᵒᵖ), H.unop.toSubsemigroup = H.unop
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.homeomorph_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] (x : ↥X),
  (AlgebraicGeometry.Scheme.Hom.homeomorph f) x = f x
-- Mathlib.RingTheory.Coprime.Lemmas
IsRelPrime.prod_right_iff : ∀ {α : Type u_1} {I : Type u_2} [inst : CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I},
  IsRelPrime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsRelPrime x (s i)
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), ¬a < b → ¬b < a → a = b
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], (m₁ \ m₂).get! k = if k ∈ m₂ then default else m₁.get! k
-- Mathlib.Analysis.Calculus.FDeriv.Comp
HasFDerivAtFilter.comp : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {f' : E →L[𝕜] F} {L : Filter (E × E)}
  {g : F → G} {g' : F →L[𝕜] G} {L' : Filter (F × F)},
  HasFDerivAtFilter g g' L' →
    HasFDerivAtFilter f f' L → Filter.Tendsto (Prod.map f f) L L' → HasFDerivAtFilter (g ∘ f) (g' ∘SL f') L
-- Mathlib.CategoryTheory.Abelian.Basic
/-- the inclusion of the image  -/
CategoryTheory.Abelian.AbelianStruct.imageι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} → {f : X ⟶ Y} → (self : CategoryTheory.Abelian.AbelianStruct f) → self.image ⟶ Y
-- Mathlib.Order.ConditionallyCompleteLattice.Group
le_ciInf_add : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst_1 : AddGroup α]
  [AddRightMono α] {a : α} {g : ι → α} {h : α}, (∀ (i : ι), a ≤ g i + h) → a ≤ iInf g + h
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.Pos.Raw.utf8GetAux.match_1.eq_2 : ∀ (motive : List Char → String.Pos.Raw → String.Pos.Raw → Sort u_1) (c : Char) (cs : List Char) (i p : String.Pos.Raw)
  (h_1 : (x x_1 : String.Pos.Raw) → motive [] x x_1)
  (h_2 : (c : Char) → (cs : List Char) → (i p : String.Pos.Raw) → motive (c :: cs) i p),
  (match c :: cs, i, p with
    | [], x, x_1 => h_1 x x_1
    | c :: cs, i, p => h_2 c cs i p) =
    h_2 c cs i p
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The centroid lies on the median from any vertex.  -/
Affine.Simplex.centroid_mem_median : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.centroid ∈ s.median i
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Submodule.isOpenQuotientMap_mkQL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_3} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (S : Submodule R M) [ContinuousAdd M], IsOpenQuotientMap ⇑S.mkQL
-- Mathlib.Analysis.RCLike.Extend
/-- **Alias** of `Module.Dual.extendRCLike_apply`. -/
LinearMap.extendTo𝕜'_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : AddCommGroup F] [inst_2 : Module ℝ F] [inst_3 : Module 𝕜 F]
  [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F) (x : F),
  fr.extendRCLike x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- The isomorphism `Γ(Y, f(U)) ≅ Γ(X, U)` induced by an open immersion `f : X ⟶ Y`.  -/
AlgebraicGeometry.Scheme.Hom.appIso : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [H : AlgebraicGeometry.IsOpenImmersion f] →
      (U : X.Opens) →
        Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)) ≅
          X.presheaf.obj (Opposite.op U)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet_map_hom_hom_apply_coe : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J : CategoryTheory.CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop)
  [inst_1 : ∀ (S : Subtype P), CategoryTheory.IsCardinalFiltered (↑↑S) κ] {X Y : Subtype P} (f : X ⟶ Y) (x : ↑↑X),
  ↑((PartOrdEmb.Hom.hom ((CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet P).map f).hom) x) = ↑x
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.naturality_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  {F G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (Z : D) {X Y : C} (f : X ⟶ Y) {Z_1 : E}
  (h : (G.obj Y).obj Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((F.map f).app Z) (CategoryTheory.CategoryStruct.comp ((T.app Y).app Z) h) =
    CategoryTheory.CategoryStruct.comp ((T.app X).app Z) (CategoryTheory.CategoryStruct.comp ((G.map f).app Z) h)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- A kernel fork for `f` is mapped to a kernel fork for `G.map f` if `G` is a functor
which preserves zero morphisms.  -/
CategoryTheory.Limits.KernelFork.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {X Y : C} →
              {f : X ⟶ Y} →
                CategoryTheory.Limits.KernelFork f →
                  (G : CategoryTheory.Functor C D) →
                    [G.PreservesZeroMorphisms] → CategoryTheory.Limits.KernelFork (G.map f)
-- Init.Internal.Order.Basic
/-- A complete lattice is a partial order where every subset has a least upper bound.
 -/
Lean.Order.CompleteLattice : Sort u → Sort (max 1 u)
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.natPair : Nat.Primrec' fun v => Nat.pair v.head v.tail.head
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.ofHom_comp : ∀ {M N O : Type u} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
  [inst_2 : SeminormedAddCommGroup O] (f : NormedAddGroupHom M N) (g : NormedAddGroupHom N O),
  SemiNormedGrp.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (SemiNormedGrp.ofHom f) (SemiNormedGrp.ofHom g)
-- Mathlib.Data.List.Permutation
List.permutationsAux2.eq_def : ∀ {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (x : List α) (x_1 : List α → β),
  List.permutationsAux2 t ts r x x_1 =
    match x, x_1 with
    | [], x => (ts, r)
    | y :: ys, f =>
      match List.permutationsAux2 t ts r ys fun x => f (y :: x) with
      | (us, zs) => (y :: us, f (t :: y :: us) :: zs)
-- Mathlib.AlgebraicGeometry.SpreadingOut
AlgebraicGeometry.injective_germ_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (x : ↥X) (hx : x ∈ U) (f : ↑(X.presheaf.obj (Opposite.op U))) (hf : x ∈ X.basicOpen f),
      Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) →
        Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
-- Mathlib.Data.NNReal.Defs
NNReal.coe_mk : ∀ (a : ℝ) (ha : 0 ≤ a), ↑(NNReal.mk a ha) = a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The flip of a pushout square is a pushout square.  -/
CategoryTheory.Limits.PushoutCocone.flipIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          {t : CategoryTheory.Limits.PushoutCocone f g} →
            CategoryTheory.Limits.IsColimit t → CategoryTheory.Limits.IsColimit t.flip
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_add_ofNat' : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddMonoidWithOne G]
  [inst_2 : AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℕ) [inst_4 : n.AtLeastTwo],
  f (x + OfNat.ofNat n) = f x + OfNat.ofNat n • b
-- Mathlib.Topology.ContinuousMap.Ideals
/-- The natural continuous map from a locally compact topological space `X` to the
`WeakDual.characterSpace 𝕜 C(X, 𝕜)` which sends `x : X` to point evaluation at `x`.  -/
WeakDual.CharacterSpace.continuousMapEval : (X : Type u_1) →
  (𝕜 : Type u_2) →
    [inst : TopologicalSpace X] →
      [inst_1 : CommRing 𝕜] →
        [inst_2 : TopologicalSpace 𝕜] →
          [inst_3 : IsTopologicalRing 𝕜] →
            [Nontrivial 𝕜] → [NoZeroDivisors 𝕜] → C(X, ↑(WeakDual.characterSpace 𝕜 C(X, 𝕜)))
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- One direction of `le_div_iff₀` where `c` is allowed to be `0` (but `b` must be nonnegative).  -/
mul_le_of_le_div₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  0 ≤ b → 0 ≤ c → a ≤ b / c → a * c ≤ b
-- Init.Data.Array.Range
Array.count_range : ∀ {a n : ℕ}, Array.count a (Array.range n) = if a < n then 1 else 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.zero_rpow : ∀ {x : ℝ}, x ≠ 0 → 0 ^ x = 0
-- Std.Http.Data.Request
Std.Http.instInhabitedRequest.default : {t : Type} → [Inhabited t] → Std.Http.Request t
-- Init.Data.Array.MinMax
Array.max_eq_max_toList : ∀ {α : Type u_1} [inst : Max α] {xs : Array α} {h : xs ≠ #[]}, xs.max h = xs.toList.max ⋯
-- Mathlib.Computability.NFA
NFA.instInhabited : {α : Type u} → {σ : Type v} → Inhabited (NFA α σ)
-- Mathlib.Topology.Sets.Opens
/-- The coercion from open sets to sets as a `FrameHom`.  -/
TopologicalSpace.Opens.frameHom : {α : Type u_2} → [inst : TopologicalSpace α] → FrameHom (TopologicalSpace.Opens α) (Set α)
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.toFun_one : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : One β], (UniformOnFun.toFun 𝔖) 1 = 1
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.instSMulMemClass : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R], SMulMemClass (TwoSidedIdeal R) R R
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainGoalParams.mk.injEq : ∀ (toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1)
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₃.eq_def : ∀ (w x y : UInt8),
  ByteArray.utf8DecodeChar?.assemble₃ w x y =
    if
        (ByteArray.utf8DecodeChar?.isInvalidContinuationByte x ||
            ByteArray.utf8DecodeChar?.isInvalidContinuationByte y) =
          true then
      none
    else
      let r := ByteArray.utf8DecodeChar?.assemble₃Unchecked w x y;
      if r < 2048 then none else if hr : 55296 ≤ r ∧ r ≤ 57343 then none else some { val := r, valid := ⋯ }
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.instAddLeftMono : AddLeftMono Ordinal.{u}