mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.CompleteLattice.Basic
OrderIso.map_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β)
  (x : ι → α), f (⨆ i, x i) = ⨆ i, f (x i)
-- Mathlib.Algebra.Polynomial.Div
Irreducible.subsingleton_isRoot : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} [IsDomain R], Irreducible p → {x | p.IsRoot x}.Subsingleton
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.injective_pointReflection_left_of_module : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [Invertible 2] (y : P₁), Function.Injective fun x => (AffineEquiv.pointReflection k x) y
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.toList_rci : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.toList_rci._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap.Raw α β cmp},
  t.WF →
    ∀ {bound : α},
      Std.Slice.toList (Std.Rci.Sliceable.mkSlice t bound...*) = List.filter (fun e => (cmp e.1 bound).isGE) t.toList
-- Lean.Server.ServerTask
Lean.Server.ServerTask.IO.mapTaskCostly : {α : Type u_1} →
  {β : Type} → (α → IO β) → Lean.Server.ServerTask α → BaseIO (Lean.Server.ServerTask (Except IO.Error β))
-- Mathlib.Data.Set.Countable
/-- **Alias** of the reverse direction of `Set.Countable.sUnion_iff`. -/
Set.Countable.sUnion : ∀ {α : Type u} {s : Set (Set α)}, s.Countable → (∀ a ∈ s, a.Countable) → (⋃₀ s).Countable
-- Mathlib.Algebra.Group.Commute.Defs
Commute.mul_zpow : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a b → ∀ (n : ℤ), (a * b) ^ n = a ^ n * b ^ n
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.ae_le_condExp : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [inst_3 : LE E],
  MeasureTheory.Submartingale f ℱ μ → ∀ {i j : ι}, i ≤ j → f i ≤ᵐ[μ] μ[f j | ↑ℱ i]
-- Mathlib.Topology.Algebra.Group.CompactOpen
/-- `ContinuousMonoidHom f _` is a functor.  -/
ContinuousMonoidHom.compRight : (A : Type u_2) →
  {E : Type u_6} →
    [inst : Monoid A] →
      [inst_1 : CommGroup E] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace E] →
            [inst_4 : IsTopologicalGroup E] →
              {B : Type u_7} →
                [inst_5 : CommGroup B] →
                  [inst_6 : TopologicalSpace B] → [inst_7 : IsTopologicalGroup B] → (B →ₜ* E) → (A →ₜ* B) →ₜ* A →ₜ* E
-- Mathlib.Analysis.Polynomial.Order
Polynomial.zero_le_eval_of_roots_le_of_leadingCoeff_nonneg : ∀ {P : Polynomial ℝ} {x : ℝ}, (∀ (y : ℝ), P.IsRoot y → y ≤ x) → 0 ≤ P.leadingCoeff → 0 ≤ Polynomial.eval x P
-- Mathlib.CategoryTheory.Products.Unitor
/-- The right unitor functor `C × 1 ⥤ C`  -/
CategoryTheory.prod.rightUnitor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (C × CategoryTheory.Discrete PUnit.{w + 1}) C
-- Mathlib.Combinatorics.Additive.FreimanHom
isAddFreimanHom_id : ∀ {α : Type u_2} [inst : AddCommMonoid α] {A₁ A₂ : Set α} {n : ℕ}, A₁ ⊆ A₂ → IsAddFreimanHom n A₁ A₂ id
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- Every strongly measurable function is integrable with respect to a Dirac measure.
See `integrable_dirac` for a version which requires that singletons are measurable sets but has no
hypothesis on `f`.  -/
MeasureTheory.integrable_dirac' : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {a : α}
  {f : α → ε},
  MeasureTheory.StronglyMeasurable f → ‖f a‖ₑ < ⊤ → MeasureTheory.Integrable f (MeasureTheory.Measure.dirac a)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the sine of the opposite angle equals the
hypotenuse.  -/
Orientation.norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → ‖y‖ / (o.oangle x (x + y)).sin = ‖x + y‖
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.ε_one : ∀ {k : Type u} {G : Type v} [inst : Monoid G] [inst_1 : Semiring k],
  (Representation.LinearizeMonoidal.ε k G) 1 = MonoidAlgebra.single PUnit.unit 1
-- Lean.MetavarContext
Lean.MetavarContext.findLevelDepth? : Lean.MetavarContext → Lean.LMVarId → Option ℕ
-- Lean.Declaration
Lean.instBEqConstructor : BEq Lean.Constructor
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instDiv.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Div (G i)], Pi.instDiv = { div := fun f g i => f i / g i }
-- Mathlib.MeasureTheory.Integral.CircleTransform
Complex.continuous_circleTransformDeriv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ},
  0 < R →
    ∀ {f : ℂ → E} {z w : ℂ},
      ContinuousOn f (Metric.sphere z R) → w ∈ Metric.ball z R → Continuous (Complex.circleTransformDeriv R z w f)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.image_ofSnowflaking_image_toSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} (s : Set X),
  ⇑Metric.Snowflaking.ofSnowflaking '' ⇑Metric.Snowflaking.toSnowflaking '' s = s
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} {l : List α} {k : α}
  {h : k ∈ m.insertManyIfNewUnit l}, (m.insertManyIfNewUnit l)[k] = ()
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.IsOrtho.map_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F)
  {U V : Submodule 𝕜 E}, Submodule.map (↑↑↑f) U ⟂ Submodule.map (↑↑↑f) V ↔ U ⟂ V
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.descOpcycles_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A A' : C}
  (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : CategoryTheory.CategoryStruct.comp (K.d j i) k = 0) (α : A ⟶ A'),
  CategoryTheory.CategoryStruct.comp (K.descOpcycles k j hj hk) α =
    K.descOpcycles (CategoryTheory.CategoryStruct.comp k α) j hj ⋯
-- Init.System.IO
IO.AccessRight.mk.sizeOf_spec : ∀ (read write execution : Bool),
  sizeOf { read := read, write := write, execution := execution } = 1 + sizeOf read + sizeOf write + sizeOf execution
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
AlgebraicTopology.DoldKan.σ_comp_P_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) {n q : ℕ} (i : Fin (n + 1)),
  n + 1 ≤ ↑i + q → CategoryTheory.CategoryStruct.comp (X.σ i) ((AlgebraicTopology.DoldKan.P q).f (n + 1)) = 0
-- Mathlib.Algebra.Group.ModEq
/-- If `a ≡ b [PMOD p]`, then mod `n • p` there are `n` cases.  -/
AddCommGroup.modEq_nsmul_cases : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G} (n : ℕ),
  n ≠ 0 → (a ≡ b [PMOD p] ↔ ∃ i < n, a ≡ b + i • p [PMOD n • p])
-- Lean.DocString.Parser
/-- Succeeds when the parser is looking at an ordered list indicator.
 -/
Lean.Doc.Parser.lookaheadOrderedListIndicator : Lean.Doc.Parser.BlockCtxt → (Lean.Doc.Parser.OrderedListType → ℤ → Lean.Parser.ParserFn) → Lean.Parser.ParserFn
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_of_mem_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α}, l.contains k = false → k ∈ m.insertManyIfNewUnit l → k ∈ m
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negAddY_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q →
      W'.negAddY P Q * (P 2 * Q 2) ^ 2 =
        (P 1 * Q 2 - Q 1 * P 2) *
            ((P 1 * Q 2 - Q 1 * P 2) ^ 2 * P 2 * Q 2 +
                      W'.a₁ * (P 1 * Q 2 - Q 1 * P 2) * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) -
                    W'.a₂ * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 -
                  P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 -
                Q 0 * P 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 -
              P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2) +
          P 1 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 3
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_diff!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} [inst_1 : Inhabited (β k)],
        Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.diff! m₂).get! k = m₁.get! k
-- Init.Data.SInt.Bitwise
Int32.toISize_xor : ∀ (a b : Int32), (a ^^^ b).toISize = a.toISize ^^^ b.toISize
-- Mathlib.Analysis.Convex.Star
StarConvex.is_linear_image : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] {x : E} {s : Set E},
  StarConvex 𝕜 x s → ∀ {f : E → F}, IsLinearMap 𝕜 f → StarConvex 𝕜 (f x) (f '' s)
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.of_subsingleton : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R],
  Subsingleton R → ∀ (M : Matrix n n R), M.PosDef
-- Lean.Server.References
/-- Direct imports of a module, containing an ordered representation and an index for fast lookups.
 -/
Lean.Server.DirectImports : Type
-- Mathlib.Algebra.Order.Nonneg.Module
Nonneg.instSMulWithZero : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : Zero S] → [SMulWithZero R S] → SMulWithZero { c // 0 ≤ c } S
-- Mathlib.Algebra.Field.Opposite
MulOpposite.instField : {α : Type u_1} → [Field α] → Field αᵐᵒᵖ
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- The continuous affine map sending `0` to `p₀` and `1` to `p₁`  -/
ContinuousAffineMap.lineMap : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module R V] →
            [inst_3 : TopologicalSpace P] →
              [inst_4 : AddTorsor V P] →
                P →
                  P →
                    [inst_5 : TopologicalSpace R] →
                      [inst_6 : TopologicalSpace V] → [ContinuousSMul R V] → [ContinuousVAdd V P] → R →ᴬ[R] P
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_single_of_neg : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] {a : α} {b : M},
  ¬p a → (Finsupp.filter p fun₀ | a => b) = 0
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.default_apply : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Subsingleton B] (x : A), default x = 0
-- Mathlib.Algebra.Group.AddChar
AddChar.map_sub_eq_div : ∀ {A : Type u_1} {M : Type u_2} [inst : AddCommGroup A] [inst_1 : DivisionCommMonoid M] (ψ : AddChar A M) (a b : A),
  ψ (a - b) = ψ a / ψ b
-- Mathlib.RingTheory.Unramified.Finite
Algebra.FormallyUnramified.comp_sec : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  [inst_7 : Algebra.FormallyUnramified R S] [inst_8 : Algebra.EssFiniteType R S],
  TensorProduct.AlgebraTensorModule.lift (↑R (Algebra.lsmul S S M).toLinearMap.flip).flip ∘ₗ
      Algebra.FormallyUnramified.sec R S M =
    LinearMap.id
-- Lean.Server.Completion.CompletionInfoSelection
_private.Lean.Server.Completion.CompletionInfoSelection.0.Lean.Server.Completion.findCompletionInfosAt.go : Lean.FileMap →
  String.Pos.Raw →
    ℕ →
      Lean.Elab.ContextInfo →
        Lean.Elab.Info →
          Array Lean.Server.Completion.ContextualizedCompletionInfo →
            Array Lean.Server.Completion.ContextualizedCompletionInfo
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_Ixx_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {Ixx : α → α → Set α} {p : α → α → Prop},
  (∀ {a b : α}, (Ixx a b).Nonempty → p a b) →
    (∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)) →
      ∀ (s t : Set α), IsPiSystem {S | ∃ l ∈ s, ∃ u ∈ t, p l u ∧ Ixx l u = S}
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- `associated'` is the `ℤ`-linear map that sends a quadratic form on a module `M` over `R` to its
associated symmetric bilinear form.  -/
QuadraticMap.associated' : {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] → [Invertible 2] → QuadraticMap R M N →ₗ[ℤ] LinearMap.BilinMap R M N
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcompose₂_obj_left_obj : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor H D')
  (X : CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F))
  (X_1 : D), ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj X).left.obj X_1 = G.obj (X.left.obj X_1)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- In a `StarAddMonoid` (i.e., an additive monoid with an additive involutive star operation), any
star-closed subset which is also closed under addition and contains zero is itself a
`StarAddMonoid`.  -/
StarMemClass.instStarAddMonoid : {S : Type u_1} →
  {R : Type u_2} →
    [inst : AddMonoid R] →
      [inst_1 : StarAddMonoid R] →
        [inst_2 : SetLike S R] → [inst_3 : AddSubmonoidClass S R] → [StarMemClass S R] → (s : S) → StarAddMonoid ↥s
-- Lean.Level
Lean.instReprData : Repr Lean.Level.Data
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instSubgroupClass : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G], SubgroupClass (OpenNormalSubgroup G) G
-- Mathlib.Data.Finset.Prod
Finset.disjUnion_product : ∀ {α : Type u_1} {β : Type u_2} {s s' : Finset α} {t : Finset β} (hs : Disjoint s s'),
  s.disjUnion s' hs ×ˢ t = (s ×ˢ t).disjUnion (s' ×ˢ t) ⋯
-- Init.Data.Array.DecidableEq
Array.instLawfulBEq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α], LawfulBEq (Array α)
-- Mathlib.Algebra.BigOperators.Fin
_private.Mathlib.Algebra.BigOperators.Fin.0.Fin.prod_insertNth_go : ∀ {M : Type u_2} [inst : CommMonoid M] (n i : ℕ) (h : i < n + 1) (x : M) (p : Fin n → M),
  ∏ j, ⟨i, h⟩.insertNth x p j = x * ∏ j, p j
-- Mathlib.Data.Ordmap.Invariants
Ordnode.findMax'.eq_2 : ∀ {α : Type u_1} (x : α) (size : ℕ) (l : Ordnode α) (x_3 : α) (r : Ordnode α),
  Ordnode.findMax' x (Ordnode.node size l x_3 r) = Ordnode.findMax' x_3 r
-- Init.System.IO
/-- The file should be opened for reading.

The read/write cursor is positioned at the beginning of the file. It is an error if the file does
not exist.

* `open` flags: `O_RDONLY`
* `fdopen` mode: `r`
 -/
IO.FS.Mode.read : IO.FS.Mode
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Real.continuousAt_const_rpow' : ∀ {a b : ℝ}, b ≠ 0 → ContinuousAt (fun x => a ^ x) b
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.tensorObj_ext_iff : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ : CategoryTheory.GradedObject I C} [inst_3 : X₁.HasTensor X₂]
  {A : C} {j : I} {f g : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ j ⟶ A},
  f = g ↔
    ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ j hi) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ j hi) g
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f_assoc : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C]
  {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)} (f : P ⟶ Q) {Z : C} (h : Q.X.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp P.p.f (CategoryTheory.CategoryStruct.comp f.f.f h) =
    CategoryTheory.CategoryStruct.comp f.f.f (CategoryTheory.CategoryStruct.comp Q.p.f h)
-- Mathlib.Control.Monad.Cont
ContT.ext_iff : ∀ {r : Type u} {m : Type u → Type v} {α : Type w} {x y : ContT r m α}, x = y ↔ ∀ (f : α → m r), x.run f = y.run f
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isLimitOfCoconeOfConeUnop_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.unop}
  (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeUnop c))
  (s : CategoryTheory.Limits.Cone F.unop),
  (CategoryTheory.Limits.isLimitOfCoconeOfConeUnop F hc).lift s =
    (hc.desc (CategoryTheory.Limits.coconeOfConeUnop s)).unop
-- Mathlib.Order.Defs.PartialOrder
gt_trans : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, b < a → c < b → c < a
-- Mathlib.Order.Monotone.Defs
instDecidableStrictAntiOfForallForallForallLt : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → {f : α → β} → [i : Decidable (∀ (a b : α), a < b → f b < f a)] → Decidable (StrictAnti f)
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.val_injective : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {d : F.WellOrderInductionData} [inst_2 : OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J}
  {e e' : d.Extension val₀ j}, e.val = e'.val → e = e'
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Collects additional binder/Finset pairs for the given `bigOpBinder`.

Note: this is not extensible at the moment, unlike the usual `bigOpBinder` expansions.  -/
BigOperators.processBigOpBinder : Array (Lean.Term × Lean.Term) → Lean.TSyntax `BigOperators.bigOpBinder → Lean.MacroM (Array (Lean.Term × Lean.Term))
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.hom_inv_h₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  {i j : E.I₀} (k : E.I₁ i j),
  CategoryTheory.CategoryStruct.comp (e.hom.h₁ k) (e.inv.h₁ (e.hom.s₁ k)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ k).inv
      (CategoryTheory.eqToHom ⋯)
-- Mathlib.Data.List.NodupEquivFin
List.SortedLT.coe_getIso_apply : ∀ {α : Type u_1} [inst : Preorder α] {l : List α} [inst_1 : DecidableEq α] (H : l.SortedLT) {i : Fin l.length},
  ↑((List.SortedLT.getIso l H) i) = l.get i
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.prop₂_of_degHom_eq_deg_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y}, r.degHom f = r.deg X → W₂ f
-- Mathlib.Analysis.Normed.Group.Quotient
/-- An isometric version of `Subgroup.quotientEquivOfEq`.  -/
Subgroup.quotientIsometryEquivOfEq : {M : Type u_1} → [inst : SeminormedCommGroup M] → {S T : Subgroup M} → S = T → M ⧸ S ≃ᵢ M ⧸ T
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.unitsEquivAut_apply_symm : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : ContinuousMul R] (u : Rˣ) (x : R),
  ((ContinuousLinearEquiv.unitsEquivAut R) u).symm x = x * ↑u⁻¹
-- Mathlib.Combinatorics.SetFamily.Shatter
/-- Down-compressing decreases the VC-dimension.  -/
Finset.vcDim_compress_le : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 : Finset (Finset α)), (Down.compression a 𝒜).vcDim ≤ 𝒜.vcDim
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonClientCapabilities : Lean.FromJson Lean.Lsp.ClientCapabilities
-- Mathlib.Topology.Algebra.Group.Basic
continuousAt_inv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [ContinuousInv G] {x : G}, ContinuousAt Inv.inv x
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dense_compl_of_dimH_lt_finrank : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E},
  dimH s < ↑(Module.finrank ℝ E) → Dense sᶜ
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.imp_congr : ∀ {σs : List (Type u)} {P P' Q Q' : Std.Do.SPred σs}, (P ⊣⊢ₛ Q) → (P' ⊣⊢ₛ Q') → (P → P') ⊣⊢ₛ Q → Q'
-- Mathlib.Logic.IsEmpty.Basic
isEmpty_plift : ∀ {α : Sort u_4}, IsEmpty (PLift α) ↔ IsEmpty α
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If a category `C` has 0-morphisms, there is a canonical inclusion from the second component `Y`
into any product of objects `X ⨯ Y`.  -/
CategoryTheory.Limits.prod.inr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) → [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y] → Y ⟶ X ⨯ Y
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_incl_le : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N : LieSubmodule R L M} {N' : LieSubmodule R L ↥N},
  LieSubmodule.map N.incl N' ≤ N
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.categoryOfGradedObjects_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (β : Type w) (X : (i : β) → (fun x => C) i) (i : β),
  CategoryTheory.CategoryStruct.id X i = CategoryTheory.CategoryStruct.id (X i)
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_bot : ∀ {R : Type u_2} [inst : NonAssocRing R], ⊥.op = ⊥
-- Init.Data.SInt.Basic
/-- Converts an arbitrary-precision natural number to a word-sized signed integer, wrapping around on
overflow.

This function is overridden at runtime with an efficient implementation.
 -/
Nat.toISize : ℕ → ISize
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.toList_rcc : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.toList_rcc._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet.Raw α cmp},
  t.WF →
    ∀ {lowerBound upperBound : α},
      Std.Slice.toList (Std.Rcc.Sliceable.mkSlice t lowerBound...=upperBound) =
        List.filter (fun e => decide ((cmp e lowerBound).isGE = true ∧ (cmp e upperBound).isLE = true)) t.toList