mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- If `F` preserves the terminal object and binary products, then it preserves products indexed by
`Fin n` for any `n`.
 -/
CategoryTheory.preservesFinOfPreservesBinaryAndTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F]
  [CategoryTheory.Limits.HasFiniteProducts C] (n : ℕ) (f : Fin n → C),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F
-- Mathlib.Order.Category.PartOrdEmb
/-- `OrderDual` as a functor.  -/
PartOrdEmb.dual : CategoryTheory.Functor PartOrdEmb PartOrdEmb
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.restrictRestrictAlgEquivMapHom_apply : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K L : IntermediateField F E)
  [inst_3 : Normal F ↥K] (φ : Gal(E/↥L)) (x : ↥K),
  ↑(((IntermediateField.restrictRestrictAlgEquivMapHom F (↥K) (↥L) E) φ) x) = φ ↑x
-- Init.Grind.Ring.Envelope
_private.Init.Grind.Ring.Envelope.0.Lean.Grind.Ring.OfSemiring.rel.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (h : Equivalence (Lean.Grind.Ring.OfSemiring.r α))
  (q₁ q₂ : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.rel✝ h q₁ q₂ = q₁.liftOn₂ q₂ (fun a₁ a₂ => Lean.Grind.Ring.OfSemiring.r α a₁ a₂) ⋯
-- Mathlib.Analysis.Convex.StrictConvexSpace
Real.instStrictConvexSpace : StrictConvexSpace ℝ ℝ
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} →
            (app : (a : B) → η.app a ⟶ θ.app a) →
              autoParam
                  (∀ {a b : B} (f : a ⟶ b),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f))
                        (θ.naturality f) =
                      CategoryTheory.CategoryStruct.comp (η.naturality f)
                        (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)))
                  CategoryTheory.Oplax.LaxTrans.Modification.naturality._autoParam →
                CategoryTheory.Oplax.LaxTrans.Modification η θ
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_add_restrict_compl : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [T2Space M] [inst_3 : ContinuousAdd M] {v : MeasureTheory.VectorMeasure α M} {i : Set α},
  MeasurableSet i → v.restrict i + v.restrict iᶜ = v
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.map_smul : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  {M₂ : Type u_6} [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₁ M₁]
  [inst_6 : Module R₁ M₂] (f : M₁ →L[R₁] M₂) (c : R₁) (x : M₁), f (c • x) = c • f x
-- Init.Data.Vector.Extract
Vector.reverse_extract : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ},
  (xs.extract i j).reverse = Vector.cast ⋯ (xs.reverse.extract (n - j) (n - i))
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_preimage_mem_nhds_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {s : Set E} {x x' : M},
  x' ∈ (extChartAt I x).source →
    s ∈ nhdsWithin (↑(extChartAt I x) x') (Set.range ↑I) → ↑(extChartAt I x) ⁻¹' s ∈ nhds x'
-- Mathlib.RingTheory.Idempotents
Subsemigroup.mem_corner_iff_mul_left : ∀ {R : Type u_1} {e : R} [inst : Semigroup R],
  IsIdempotentElem e → IsMulCentral e → ∀ {r : R}, r ∈ Subsemigroup.corner e ↔ e * r = r
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- `Multiplicative (Additive H)` is just `H`.  -/
MulEquiv.multiplicativeAdditive : (H : Type u_3) → [inst : MulOneClass H] → Multiplicative (Additive H) ≃* H
-- Batteries.Data.List.Basic
List.dropSlice_zero₂ : ∀ {α : Type u_1} (n : ℕ) (l : List α), List.dropSlice n 0 l = l
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.induction_on : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {C : M ⧸ p → Prop} (x : M ⧸ p), (∀ (z : M), C (Submodule.Quotient.mk z)) → C x
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
/-- Coherence tactic for bicategories.  -/
Mathlib.Tactic.BicategoryCoherence.bicategoryCoherence : Lean.MVarId → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Order.Group.Action.End
/-- The tautological action by `r ≃r r` on `α`.  -/
RelIso.applyMulAction : {α : Type u_1} → {r : α → α → Prop} → MulAction (r ≃r r) α
-- Mathlib.Data.ENNReal.Holder
/-- An abbreviation for `ENNReal.HolderTriple p q 1`, this class states `p⁻¹ + q⁻¹ = 1`.  -/
ENNReal.HolderConjugate : ENNReal → ENNReal → Prop
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.SpecIso.eq_1 : ∀ (n : Type u) (R : CommRingCat),
  AlgebraicGeometry.AffineSpace.SpecIso n R =
    AlgebraicGeometry.AffineSpace.isoOfIsAffine n (AlgebraicGeometry.Spec R) ≪≫
      AlgebraicGeometry.Scheme.Spec.mapIso
        (MvPolynomial.mapEquiv n
              (AlgebraicGeometry.Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.op
-- Mathlib.Analysis.Real.Sqrt
Real.one_le_sqrt : ∀ {x : ℝ}, 1 ≤ √x ↔ 1 ≤ x
-- Mathlib.Topology.EMetricSpace.Defs
EMetricSpace.mk : {α : Type u} → [toPseudoEMetricSpace : PseudoEMetricSpace α] → (∀ {x y : α}, edist x y = 0 → x = y) → EMetricSpace α
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeDTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : ℕ → List α → Array α → Sort u_2) (x : List α) (acc : Array α)
  (h_1 : (n : ℕ) → (x : α) → (xs : List α) → (acc : Array α) → motive n.succ (x :: xs) acc)
  (h_2 : (x : List α) → (acc : Array α) → motive 0 x acc) (h_3 : (n : ℕ) → (acc : Array α) → motive n [] acc),
  (match 0, x, acc with
    | n.succ, x :: xs, acc => h_1 n x xs acc
    | 0, x, acc => h_2 x acc
    | n, [], acc => h_3 n acc) =
    h_2 x acc
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryD.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (k : α) (fallback : (a : α) × β a),
  t.getEntryD k fallback =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => fallback
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r =>
      match compare k k' with
      | Ordering.lt => l.getEntryD k fallback
      | Ordering.gt => r.getEntryD k fallback
      | Ordering.eq => ⟨k', v'⟩
-- Mathlib.Data.QPF.Univariate.Basic
QPF.comp_map : ∀ {F : Type u → Type v} [q : QPF F] {α β γ : Type u} (f : α → β) (g : β → γ) (x : F α), (g ∘ f) <$> x = g <$> f <$> x
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.hasInitial_of_hasTerminal_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal Cᵒᵖ],
  CategoryTheory.Limits.HasInitial C
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalAlgEquivClass.mk : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} [inst : Add A]
  [inst_1 : Mul A] [inst_2 : SMul R A] [inst_3 : Add B] [inst_4 : Mul B] [inst_5 : SMul R B] [inst_6 : EquivLike F A B]
  [toRingEquivClass : RingEquivClass F A B] [toMulActionSemiHomClass : MulActionSemiHomClass F id A B],
  NonUnitalAlgEquivClass F R A B
-- Init.Data.Nat.Lemmas
Nat.mod_mod : ∀ (a n : ℕ), a % n % n = a % n
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.i_mapZ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (data : W₁.FunctorialFactorizationData W₂) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'}
  (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g),
  CategoryTheory.CategoryStruct.comp (data.factorizationData f).i (data.mapZ φ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left φ) (data.factorizationData g).i
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Given a point on a sphere and a point inside it, the inner product between the difference of
those points and the radius vector is positive.  -/
EuclideanGeometry.inner_pos_of_dist_lt_radius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  p₁ ∈ s → dist p₂ s.center < s.radius → 0 < inner ℝ (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)
-- Mathlib.Algebra.Star.Pointwise
Set.star_mul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : StarMul α] (s t : Set α), star (s * t) = star t * star s
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- Extension for the `positivity` tactic: exponentiation by a real number is nonnegative when
the base is nonnegative and positive when the base is positive.
This is the `ENNReal` analogue of `evalRpow` for `Real`.  -/
Mathlib.Meta.Positivity.evalENNRealRpow : Mathlib.Meta.Positivity.PositivityExt
-- Init.Data.Array.Erase
Array.exists_or_eq_self_of_eraseP : ∀ {α : Type u_1} (p : α → Bool) (xs : Array α),
  xs.eraseP p = xs ∨ ∃ a ys zs, (∀ b ∈ ys, ¬p b = true) ∧ p a = true ∧ xs = ys.push a ++ zs ∧ xs.eraseP p = ys ++ zs
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [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} D]
  [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.Additive]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (x y : ℤ) [inst_8 : K₁.HasMapBifunctor K₂ F],
  K₁.mapBifunctorShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F x ≪≫
      (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).mapIso (K₁.mapBifunctorShift₂Iso K₂ F y) =
    (x * y).negOnePow •
      ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorShift₂Iso K₂ F y ≪≫
        (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).mapIso (K₁.mapBifunctorShift₁Iso K₂ F x) ≪≫
          (CategoryTheory.shiftFunctorComm (CochainComplex D ℤ) x y).app (K₁.mapBifunctor K₂ F)
-- Lean.Environment
/-- Reported extension state eventually fulfilled by promise; may be missing for tasks (e.g. kernel
checking, synchronous decl addition) that can eagerly guarantee they will not report any state.
 -/
_private.Lean.Environment.0.Lean.AsyncConst.exts? : Lean.AsyncConst✝ → Option (Task (Array Lean.EnvExtensionState))
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.has_finite_products : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.NonPreadditiveAbelian C],
  CategoryTheory.Limits.HasFiniteProducts C
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.unitForward_unitBackward : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A)
  (X : C), CategoryTheory.OverPresheafAux.unitForward η X ∘ CategoryTheory.OverPresheafAux.unitBackward η X = id
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, (t₁ \ t₂).getKeyD k fallback = if k ∈ t₂ then fallback else t₁.getKeyD k fallback
-- Mathlib.Algebra.Algebra.Operations
Submodule.map_unop_pow : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (n : ℕ)
  (M : Submodule R Aᵐᵒᵖ),
  Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (M ^ n) =
    Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) M ^ n
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.toFinite_apply_eq_zero_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] {s : Set α},
  μ.toFinite s = 0 ↔ μ s = 0
-- Mathlib.Computability.Reduce
OneOneEquiv.congr_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, OneOneEquiv p q → (OneOneEquiv p r ↔ OneOneEquiv q r)
-- Mathlib.Algebra.Module.FinitePresentation
/-- Let `M` be a finitely presented `R`-module, `N` an `R`-module, `S : Submonoid R`.
The linear equivalence between the `M →ₗ[R] N` localized at `S` and
`LocalizedModule S M →ₗ[R] LocalizedModule S N`
 -/
Module.FinitePresentation.linearEquivMap : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] →
                (S : Submonoid R) →
                  [Module.FinitePresentation R M] →
                    LocalizedModule S (M →ₗ[R] N) ≃ₗ[R] LocalizedModule S M →ₗ[R] LocalizedModule S N
-- Mathlib.RingTheory.Ideal.GoingDown
Algebra.HasGoingDown.mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (∀ {p : Ideal R} [p.IsPrime] (Q : Ideal S) [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p) →
    Algebra.HasGoingDown R S
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_one : ∀ {α : Type u_1} [inst : One α], SymAlg.sym 1 = 1
-- Mathlib.Order.Sublattice
Sublattice.subtype_apply : ∀ {α : Type u_2} [inst : Lattice α] (L : Sublattice α) (a : ↥L), L.subtype a = ↑a
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousLinearEquiv.coe_toContinuousAffineEquiv : ∀ {k : Type u_1} [inst : Ring k] {E : Type u_10} {F : Type u_11} [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module k F] [inst_6 : TopologicalSpace F]
  (e : E ≃L[k] F), ⇑e.toContinuousAffineEquiv = ⇑e
-- Batteries.Lean.EStateM
EStateM.run'_map : ∀ {α β ε σ : Type u_1} (f : α → β) (x : EStateM ε σ α) (s : σ), (f <$> x).run' s = Option.map f (x.run' s)
-- Init.Data.List.Range
List.range'_ne_nil_iff : ∀ (s : ℕ) {n step : ℕ}, List.range' s n step ≠ [] ↔ n ≠ 0
-- Mathlib.RingTheory.Congruence.Hom
RingCon.range_mkₐ : ∀ {M : Type u_1} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M] {c : RingCon M},
  (RingCon.mkₐ R c).range = ⊤
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.openCell_subset_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.openCell n j ⊆ C
-- Init.Data.Array.Attach
Array.filter_unattach : ∀ {α : Type u_1} {P : α → Prop} {xs : Array (Subtype P)} {f : α → Bool},
  Array.filter f xs.unattach =
    (Array.filter
        (fun x =>
          match x with
          | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
        xs).unattach
-- Lean.MetavarContext
/-- Depth is used to control whether an mvar can be assigned in unification.  -/
Lean.MetavarContext.depth : Lean.MetavarContext → ℕ
-- Mathlib.Computability.TuringMachine.Tape
/-- The n-th element of a `ListBlank` is well defined for all `n : ℕ`, unlike in a `List`.  -/
Turing.ListBlank.nth : {Γ : Type u_1} → [inst : Inhabited Γ] → Turing.ListBlank Γ → ℕ → Γ
-- Mathlib.CategoryTheory.NatTrans
/-- The component of a natural transformation.  -/
CategoryTheory.NatTrans.app : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} → CategoryTheory.NatTrans F G → (X : C) → F.obj X ⟶ G.obj X
-- Mathlib.MeasureTheory.SpecificCodomains.Pi
/-- **Alias** of the forward direction of `MeasureTheory.integrable_pi_iff`. -/
MeasureTheory.Integrable.eval : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {ι : Type u_2} [inst : Fintype ι]
  {E : ι → Type u_3} [inst_1 : (i : ι) → NormedAddCommGroup (E i)] {f : X → (i : ι) → E i},
  MeasureTheory.Integrable f μ → ∀ (i : ι), MeasureTheory.Integrable (fun x => f x i) μ
-- Batteries.Data.Char.AsciiCasing
/-- ASCII-case insensitive implementation comparison returning an `Ordering`. Useful for sorting.

```
#eval cmpCaseInsensitiveAsciiOnly 'a' 'A' -- eq
#eval cmpCaseInsensitiveAsciiOnly 'a' 'a' -- eq
#eval cmpCaseInsensitiveAsciiOnly '$' '$' -- eq
#eval cmpCaseInsensitiveAsciiOnly 'a' 'b' -- lt
#eval cmpCaseInsensitiveAsciiOnly 'γ' 'Γ' -- gt
#eval cmpCaseInsensitiveAsciiOnly 'ä' 'Ä' -- gt
```
 -/
Char.cmpCaseInsensitiveAsciiOnly : Char → Char → Ordering
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.fst_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.BinaryBicone X Y} (ht : CategoryTheory.Limits.IsColimit t.toCocone),
  t.fst = CategoryTheory.Limits.BinaryCofan.IsColimit.desc ht (CategoryTheory.CategoryStruct.id X) 0
-- Mathlib.Algebra.Ring.Basic
/-- Left multiplication by an element of a type with distributive multiplication is an `AddHom`.  -/
AddHom.mulLeft : {R : Type u_1} → [inst : Distrib R] → R → R →ₙ+ R
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.toIsNontrivial : ∀ {K : Type u_1} {inst : Field K} {inst_1 : ValuativeRel K} {inst_2 : TopologicalSpace K}
  [self : IsNonarchimedeanLocalField K], ValuativeRel.IsNontrivial K
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.range.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N),
  f.range = (AddSubgroup.map f ⊤).copy (Set.range ⇑f) ⋯
-- Mathlib.Topology.Order.LeftRightLim
Antitone.rightLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β}, Antitone f → Antitone (Function.rightLim f)
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.constantCoeff_subst_X_pow : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S] {k : ℕ},
  k ≠ 0 →
    ∀ (f : PowerSeries R),
      PowerSeries.constantCoeff (PowerSeries.subst (PowerSeries.X ^ k) f) =
        (algebraMap R S) (PowerSeries.constantCoeff f)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `Prod.fst` as a bundled `AddActionHom`.  -/
AddActionHom.fst : (M : Type u_1) → (α : Type u_2) → (β : Type u_3) → [inst : VAdd M α] → [inst_1 : VAdd M β] → α × β →ₑ[id] α
-- Lean.EnvExtension
/-- Environment extension for mapping declarations to values.
Declarations must only be inserted into the mapping in the module where they were declared.  -/
Lean.MapDeclarationExtension : Type → Type
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicValued.uniformContinuousConstSMul : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [inst_2 : Field K]
  [inst_3 : CommSemiring S] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K]
  (v : IsDedekindDomain.HeightOneSpectrum R) [inst_6 : Algebra S K],
  UniformContinuousConstSMul S (WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v))
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzOnWith.norm_div_le_of_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedCommGroup E] [inst_1 : SeminormedCommGroup F] {f : E → F} {C : NNReal}
  {s : Set E} {a b : E} {r : ℝ}, LipschitzOnWith C f s → a ∈ s → b ∈ s → ‖a / b‖ ≤ r → ‖f a / f b‖ ≤ ↑C * r
-- Mathlib.Topology.Algebra.Module.PerfectPairing
/-- For a topological ring `R` and two topological modules `M` and `N`, a continuous perfect pairing
is a continuous bilinear map `M × N → R` that is bijective in both arguments.

We require continuity in the forward direction only so that we can put several different topologies
on the continuous dual: strong, weak, weak-\* topology...  -/
LinearMap.IsContPerfPair : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [TopologicalSpace R] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [TopologicalSpace M] →
                [inst_5 : AddCommGroup N] → [inst_6 : Module R N] → [TopologicalSpace N] → (M →ₗ[R] N →ₗ[R] R) → Prop
-- Mathlib.Logic.Function.Basic
/-- A function is involutive, if `f ∘ f = id`.  -/
Function.Involutive : {α : Sort u_1} → (α → α) → Prop
-- Init.Data.Int.Gcd
Int.lcm_pos_iff : ∀ {m n : ℤ}, 0 < m.lcm n ↔ m ≠ 0 ∧ n ≠ 0
-- Mathlib.RingTheory.Localization.Defs
/-- Surjectivity of a map descends to the map induced on localizations.  -/
IsLocalization.map_surjective_of_surjective : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  (Q : Type u_4) [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q],
  Function.Surjective ⇑g →
    ∀ [inst_7 : IsLocalization (Submonoid.map g M) Q], Function.Surjective ⇑(IsLocalization.map Q g ⋯)
-- Std.Sync.CancellationToken
Std.CancellationToken.State.mk.inj : ∀ {reason : Option Std.CancellationReason} {consumers : Std.Queue Std.CancellationToken.Consumer}
  {reason_1 : Option Std.CancellationReason} {consumers_1 : Std.Queue Std.CancellationToken.Consumer},
  { reason := reason, consumers := consumers } = { reason := reason_1, consumers := consumers_1 } →
    reason = reason_1 ∧ consumers = consumers_1
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.ex : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ : L.BoundedFormula α (n + 1)},
  T.Iff φ ψ → T.Iff φ.ex ψ.ex
-- Init.Data.Float.Model.Unpacked.Operations.OfNat
/-- Converts an `ISize` to an `UnpackedFloat`, returning positive zero on zero.  -/
Float.Model.UnpackedFloat.ofISize : Float.Model.Format → ISize → Float.Model.UnpackedFloat
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.subset_add_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddZeroClass α] (s : Finset α) {t : Finset α}, 0 ∈ t → s ⊆ s + t
-- Mathlib.Algebra.MonoidAlgebra.Support
MonoidAlgebra.support_coeff_mul_single : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : IsRightCancelMul G] (f : MonoidAlgebra k G)
  (r : k),
  (∀ (y : k), y * r = 0 ↔ y = 0) →
    ∀ (x : G), (f * MonoidAlgebra.single x r).coeff.support = Finset.map (mulRightEmbedding x) f.coeff.support
-- Mathlib.Data.Int.Range
Int.decidableLELT : (P : ℤ → Prop) → [DecidablePred P] → (m n : ℤ) → Decidable (∀ (r : ℤ), m ≤ r → r < n → P r)