mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instCofibrationOppositeOpOfFibration : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C] [HomotopicalAlgebra.Fibration f],
  HomotopicalAlgebra.Cofibration f.op
-- Mathlib.Algebra.Module.Torsion.Basic
Ideal.torsionOf_zero : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Ideal.torsionOf R M 0 = ⊤
-- Mathlib.Order.InitialSeg
InitialSeg.mk.injEq : ∀ {α : Type u_4} {β : Type u_5} {r : α → α → Prop} {s : β → β → Prop} (toRelEmbedding : r ↪r s)
  (mem_range_of_rel' : ∀ (a : α) (b : β), s b (toRelEmbedding a) → b ∈ Set.range ⇑toRelEmbedding)
  (toRelEmbedding_1 : r ↪r s)
  (mem_range_of_rel'_1 : ∀ (a : α) (b : β), s b (toRelEmbedding_1 a) → b ∈ Set.range ⇑toRelEmbedding_1),
  ({ toRelEmbedding := toRelEmbedding, mem_range_of_rel' := mem_range_of_rel' } =
      { toRelEmbedding := toRelEmbedding_1, mem_range_of_rel' := mem_range_of_rel'_1 }) =
    (toRelEmbedding = toRelEmbedding_1)
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.lex_iff_of_unique : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : Unique ι] [inst_2 : (i : ι) → LT (α i)]
  {r : ι → ι → Prop} [Std.Irrefl r] {x y : Π₀ (i : ι), α i},
  DFinsupp.Lex r (fun x x1 x2 => x1 < x2) x y ↔ x default < y default
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_le_one : ∀ {r : ℝ}, ENNReal.ofReal r ≤ 1 ↔ r ≤ 1
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_insert : ∀ {α : Type u} [inst : DecidableEq α] {s : Set α} {a : α} (hs : (insert a s).Finite), hs.toFinset = insert a ⋯.toFinset
-- Mathlib.Topology.Order.OrderClosed
Filter.Tendsto.min_left : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f : β → α}
  {l : Filter β} {a : α}, Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun i => min (f i) a) l (nhds a)
-- Mathlib.Data.Set.Image
/-- The image of a subsingleton is a subsingleton.  -/
Set.Subsingleton.image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Subsingleton → ∀ (f : α → β), (f '' s).Subsingleton
-- Init.Data.List.Lemmas
List.splitAt.go.eq_3 : ∀ {α : Type u} (l a : List α) (a_1 : ℕ) (a_2 : List α),
  (a = [] → False) →
    (∀ (x : α) (xs : List α) (n : ℕ), a = x :: xs → a_1 = n.succ → False) →
      List.splitAt.go l a a_1 a_2 = (a_2.reverse, a)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- `SpecialLinearGroup n R` is the group of `n` by `n` `R`-matrices with determinant equal to 1.
 -/
MatrixGroups.«termSL(_,_)» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
QuadraticMap.toBilin.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : LinearOrder ι] [inst_1 : CommRing R]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  (Q : QuadraticMap R M N) (bm : Module.Basis ι R M),
  Q.toBilin bm =
    (bm.constr R) fun i =>
      (bm.constr R) fun j => if i = j then Q (bm i) else if i < j then QuadraticMap.polar (⇑Q) (bm i) (bm j) else 0
-- Mathlib.Data.SetLike.Basic
SetLike.coe_eq_coe : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {x y : ↥p}, ↑x = ↑y ↔ x = y
-- Init.Data.Dyadic.Basic
Int.trailingZeros.aux.match_1.congr_eq_1 : ∀ (i : ℤ) (motive : (k : ℕ) → k ≠ 0 → i.natAbs ≤ k → Sort u_1) (k : ℕ) (x : k ≠ 0) (hk : i.natAbs ≤ k)
  (h_1 : (k : ℕ) → (x : k + 1 ≠ 0) → (hk : i.natAbs ≤ k + 1) → motive k.succ x hk) (k_1 : ℕ) (x_1 : k_1 + 1 ≠ 0)
  (hk_1 : i.natAbs ≤ k_1 + 1),
  k = k_1.succ →
    x ≍ x_1 →
      hk ≍ hk_1 →
        (match k, x, hk with
          | k.succ, x, hk => h_1 k x hk) ≍
          h_1 k_1 x_1 hk_1
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_le_iff_le_exp : ∀ {x y : ℝ}, 0 < x → (Real.log x ≤ y ↔ x ≤ Real.exp y)
-- Mathlib.Data.Fintype.Basic
ULift.fintype : (α : Type u_4) → [Fintype α] → Fintype (ULift.{u_5, u_4} α)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.strictMono_gamma : StrictMono Ordinal.gamma
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- Note this is more general than `IsSelfAdjoint.star_mul_self` as `B` can be rectangular.  -/
Matrix.isHermitian_conjTranspose_mul_self : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : NonUnitalSemiring α] [inst_1 : StarRing α] [inst_2 : Fintype m]
  (A : Matrix m n α), (A.conjTranspose * A).IsHermitian
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_add_eq_of_lt_left : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  {x y : R}, v x < v y → v (x + y) = v x
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- Maps of simplicial sets induce maps of paths in a simplicial set.  -/
SSet.Path.map : {X Y : SSet} → {n : ℕ} → X.Path n → (X ⟶ Y) → Y.Path n
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.appIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} [inst_2 : G.IsCoverDense K] [inst_3 : G.IsLocallyFull K]
  {ℱ ℱ' : CategoryTheory.Sheaf K (Type v)} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) (X : D),
  (CategoryTheory.Functor.IsCoverDense.Types.appIso i X).hom = CategoryTheory.Functor.IsCoverDense.Types.appHom i.hom X
-- Mathlib.Data.Num.Basic
instDecidableEqZNum : DecidableEq ZNum
-- Mathlib.Analysis.Normed.Group.Uniform
dist_self_add_left : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] (a b : E), dist (b + a) b = ‖a‖
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformlyOn.mono : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s s' : Set α} {p : Filter ι},
  TendstoLocallyUniformlyOn F f p s → s' ⊆ s → TendstoLocallyUniformlyOn F f p s'
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f),
  (F.mapComp' f₀₂ f₂₃ f ⋯).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
          (F.mapComp' f₀₁ f₁₃ f ⋯).inv))
-- Mathlib.Data.Real.Basic
Real.mk_le : ∀ {f g : CauSeq ℚ abs}, Real.mk f ≤ Real.mk g ↔ f ≤ g
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
/-- Bundled additive functors.  -/
CategoryTheory.AdditiveFunctor : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.Preadditive C] → [CategoryTheory.Preadditive D] → Type (max (max (max u_1 u_2) v_1) v_2)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.equation_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R) {u : R},
  IsUnit u → (W'.Equation (u • P) ↔ W'.Equation P)
-- Init.Data.List.Basic
List.reverse.eq_1 : ∀ {α : Type u} (as : List α), as.reverse = as.reverseAux []
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Surjective.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}, Function.Surjective ⇑f → AlgebraicGeometry.Surjective f
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- given a point of `x : S`, `idx x` is the index of the component which contains `x`  -/
AlgebraicGeometry.Scheme.AffineCover.idx : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} → (self : AlgebraicGeometry.Scheme.AffineCover P S) → ↥S → self.I₀
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- If `g : M ⟶ N` is a `B`-linear morphism of `B`-modules, then it induces an
`A`-linear morphism when `M` and `N` have an `A`-module structure obtained
by restricting scalars along a monoid morphism `A ⟶ B`.  -/
CategoryTheory.Mod.scalarRestriction_hom : ∀ {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.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.MonObj A] [inst_5 : CategoryTheory.MonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsMonHom f] (M N : D) [inst_7 : CategoryTheory.ModObj B M]
  [inst_8 : CategoryTheory.ModObj B N] (g : M ⟶ N) [CategoryTheory.IsModHom B g], CategoryTheory.IsModHom A g
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- The epimorphism `free σ.I ⟶ M` given by `σ : M.GeneratingSections`.  -/
SheafOfModules.GeneratingSections.π : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} → (σ : M.GeneratingSections) → SheafOfModules.free σ.I ⟶ M
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_injective : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : InvolutiveStar α], Function.Injective Matrix.conjTranspose
-- Mathlib.Order.UpperLower.Relative
isRelLowerSet_true_iff_isLowerSet : ∀ {α : Type u_1} {s : Set α} [inst : LE α], (IsRelLowerSet s fun x => True) ↔ IsLowerSet s
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.instFullOppositeOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [F.Full], F.op.Full
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Filter.Tendsto.arccos : ∀ {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ},
  Filter.Tendsto f l (nhds x) → Filter.Tendsto (fun x => Real.arccos (f x)) l (nhds (Real.arccos x))
-- Mathlib.Order.Filter.Cocardinal
Filter.mem_cocardinal : ∀ {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α}, s ∈ Filter.cocardinal α hreg ↔ Cardinal.mk ↑sᶜ < c
-- Mathlib.Algebra.Category.AlgCat.Symmetric
AlgCat.instBraidedCategory : {R : Type u} → [inst : CommRing R] → CategoryTheory.BraidedCategory (AlgCat R)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.toOplax_mapId' : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {b : B} (f : b ⟶ b)
  (hf : autoParam (f = CategoryTheory.CategoryStruct.id b) CategoryTheory.Pseudofunctor.toOplax_mapId'._auto_1),
  F.toOplax.mapId' f hf = (F.mapId' f hf).hom
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsPrincipalIdealRingLocalizationAlgebraMapSubmonoidPrimeComplOfIsDedekindDomainOfFiniteOfNeZeroIdeal : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [IsDomain S]
  [inst_4 : Algebra R S] {P : Ideal R} [inst_5 : P.IsPrime] [FaithfulSMul R S] [IsDedekindDomain R] [IsDedekindDomain S]
  [Module.Finite R S] [hP : NeZero P], IsPrincipalIdealRing (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_erase_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {k : α}, (m.erase k).get? k = none
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
/-- A unit in `ArithmeticFunction R` that evaluates to `ζ`, with inverse `μ`.  -/
ArithmeticFunction.zetaUnit : {R : Type u_1} → [inst : CommRing R] → (ArithmeticFunction R)ˣ
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trNormal.eq_7 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4},
  Turing.TM2to1.trNormal Turing.TM2.Stmt.halt = Turing.TM1.Stmt.halt
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.startsWith_char_eq_startsWith_beq : ∀ {c : Char} {s : String.Slice}, s.startsWith c = s.startsWith fun x => x == c
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_alter_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k : α}
  (h : t.WF) {f : Option β → Option β},
  Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl =
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome
-- Init.Data.Ord.Basic
_private.Init.Data.Ord.Basic.0.Ordering.then.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (a : Ordering) (h_1 : Unit → motive Ordering.eq) (h_2 : (a : Ordering) → motive a),
  (a = Ordering.eq → False) →
    (match a with
      | Ordering.eq => h_1 ()
      | a => h_2 a) =
      h_2 a
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (x : M),
  (AddMonoid.Coprod.swap M N) (AddMonoid.Coprod.inl x) = AddMonoid.Coprod.inr x
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.natTransEquiv_apply_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}
  (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C (Type (max v' v u))) ⟶ F.functorHom G)
  (X : C),
  (CategoryTheory.Functor.natTransEquiv f).app X =
    ((CategoryTheory.ConcreteCategory.hom (f.app X)) PUnit.unit).app X
      (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op X)))
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.toMonoidHom : {α : Type u_7} → {β : Type u_8} → [inst : MulZeroOneClass α] → [inst_1 : MulZeroOneClass β] → (α →*₀ β) → α →* β
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.op_comp_isSheaf_of_preservesOneHypercovers : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {A : Type u} [inst_2 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  [F.PreservesOneHypercovers J K] [J.IsGeneratedByOneHypercovers] (P : CategoryTheory.Functor Dᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf K P → CategoryTheory.Presheaf.IsSheaf J (F.op.comp P)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.pow_prod_atom : ∀ {R : Type u_1} [inst : CommSemiring R] (a : R) (b : ℕ) {e : R}, (a + 0) ^ b * Nat.rawCast 1 = e → a ^ b = e
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.le_comap_of_map_le : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup M) {T : Subsemigroup N} {f : M →ₙ* N},
  Subsemigroup.map f S ≤ T → S ≤ Subsemigroup.comap f T
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_union' : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  Disjoint s t → MeasurableSet s → μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
/-- The center of `GL n R` is the image of `Rˣ`.  -/
Matrix.GeneralLinearGroup.center_eq_range_scalar : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R],
  Subgroup.center (GL n R) = (Matrix.GeneralLinearGroup.scalar n).range
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- The canonical isomorphism `W ×[X] (X ×[Z] Y) ≅ W ×[Z] Y`  -/
CategoryTheory.Limits.pullbackRightPullbackFstIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          (f' : W ⟶ X) →
            [inst_1 : CategoryTheory.Limits.HasPullback f g] →
              [inst_2 : CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)] →
                CategoryTheory.Limits.pullback f' (CategoryTheory.Limits.pullback.fst f g) ≅
                  CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp f' f) g
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.instNeBotValFilterCauchy : ∀ {α : Type u} [inst : UniformSpace α] (f : CauchyFilter α), (↑f).NeBot
-- Lean.Compiler.IR.Format
_private.Lean.Compiler.IR.Format.0.Lean.IR.formatCtorInfo : Lean.IR.CtorInfo → Std.Format
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Wrapper around `Expr.nat?` that also allows `Nat.cast`.  -/
Lean.Elab.Tactic.Omega.natCast? : Lean.Expr → Option ℕ
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` is purely inseparable, then for any reduced `F`-algebra `L`, there exists at most one
`F`-algebra homomorphism from `E` to `L`.  -/
instSubsingletonAlgHomOfIsPurelyInseparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E]
  (L : Type w) [inst_4 : CommRing L] [IsReduced L] [inst_6 : Algebra F L], Subsingleton (E →ₐ[F] L)
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.LawfulOperator.lt_size_of_lt_aig_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → Type}
  {f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α} [Std.Sat.AIG.LawfulOperator α β f] {x : ℕ}
  (aig : Std.Sat.AIG α) (input : β aig), x < aig.decls.size → x < (f aig input).aig.decls.size
-- Init.Data.List.Scan.Lemmas
List.scanr_reverse : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : List α},
  List.scanr f init as.reverse = (List.scanl (flip f) init as).reverse
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.getKey? a =
    if compare k a = Ordering.eq ∧ k ∉ t then some k else t.getKey? a
-- Mathlib.Data.List.Defs
/-- Runs a function over a list returning the intermediate results and a final result.  -/
List.mapAccumr : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → γ → γ × β) → List α → γ → γ × List β
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.changeInverse_counitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : D),
  (e.changeInverse iso).counitIso.hom.app X =
    CategoryTheory.CategoryStruct.comp (e.functor.map (iso.inv.app X)) (e.counitIso.hom.app X)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.opFunctorCompFst_hom_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : (CategoryTheory.Comma L R)ᵒᵖ),
  (CategoryTheory.Comma.opFunctorCompFst L R).hom.app X =
    CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).right)
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
/-- `γ` is an integral curve for `v` at `t₀` iff `γ` is an integral curve on some interval
containing `t₀`.  -/
isMIntegralCurveAt_iff' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {t₀ : ℝ},
  IsMIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
-- Batteries.Data.List.Basic
/-- If `a` relates to `b` and `b::l` is a chain, then `a :: b :: l` is also a chain.  -/
List.IsChain.cons_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α},
  R a b → List.IsChain R (b :: l) → List.IsChain R (a :: b :: l)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_minKey?_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, k ∈ t → t.minKey?.isSome = true
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.sumArrowHomeomorphProdArrow_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_7} {ι' : Type u_8} (f : ι ⊕ ι' → X),
  Homeomorph.sumArrowHomeomorphProdArrow f = (f ∘ Sum.inl, f ∘ Sum.inr)
-- Mathlib.Analysis.Convex.Cone.Dual
ProperCone.dual.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : ClosedIciTopology R] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : TopologicalSpace M] [inst_8 : AddCommGroup N] [inst_9 : Module R N] [inst_10 : TopologicalSpace N]
  (p p_1 : M →ₗ[R] N →ₗ[R] R) (e_p : p = p_1) [inst_11 : p.IsContPerfPair] (s s_1 : Set M),
  s = s_1 → ProperCone.dual p s = ProperCone.dual p_1 s_1
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piEquivalenceFunctorDiscrete_functor_comp_colim : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape α C],
  (CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.comp CategoryTheory.Limits.colim =
    CategoryTheory.Limits.Sigma.functor α
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.map.eq_1 : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (R' : Type u_6)
  {M' : Type u_7} [inst_3 : CommRing R'] [inst_4 : AddCommGroup M'] [inst_5 : Module R' M'] [inst_6 : Module R M']
  (f : M →ₗ[R] M'),
  PolynomialModule.map R' f =
    ↑(PolynomialModule.coeffLinearEquiv R' R).symm ∘ₗ
      Finsupp.mapRange.linearMap f ∘ₗ ↑(PolynomialModule.coeffLinearEquiv R R)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_le_of_le_add_nat : ∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℕ}, f x ≤ x + ↑m → f.translationNumber ≤ ↑m
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.forIn'_eq_foldlM.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.done b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_2 b
-- Mathlib.Order.Interval.Finset.Defs
/-- Left-closed right-open interval  -/
LocallyFiniteOrder.finsetIco : {α : Type u_1} → {inst : Preorder α} → [self : LocallyFiniteOrder α] → α → α → Finset α
-- Init.Data.Option.Attach
Option.attach_toList : ∀ {α : Type u_1} (o : Option α),
  o.toList.attach =
    (Option.map
        (fun x =>
          match x with
          | ⟨a, h⟩ => ⟨a, ⋯⟩)
        o.attach).toList