mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepFun_self_left : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β}
  {mβ' : MeasurableSpace β'} {X : Ω → β} {Z : Ω → β'},
  Measurable X → ∀ (hZ : Measurable Z), ProbabilityTheory.CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ Z X μ
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffOn.nsmul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3} [inst_1 : TopologicalSpace H]
  {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5}
  [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G]
  {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7}
  [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H' M] {s : Set M} {g : M → G},
  ContMDiffOn I' I n g s → ∀ (m : ℕ), ContMDiffOn I' I n (fun x => m • g x) s
-- Std.Data.DTreeMap.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.DTreeMap.Const.toList : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → List (α × β)
-- Init.Data.String.Iterator
String.Legacy.instDecidableEqIterator : DecidableEq String.Legacy.Iterator
-- Init.Data.List.Perm
List.perm_singleton : ∀ {α : Type u_1} {a : α} {l : List α}, l.Perm [a] ↔ l = [a]
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
/-- The slice category over the terminal unit object is equivalent to the original category.  -/
CategoryTheory.equivToOverUnit : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≌ C
-- Mathlib.Topology.Inseparable
Inseparable.prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₁ x₂ : X} {y₁ y₂ : Y},
  Inseparable x₁ x₂ → Inseparable y₁ y₂ → Inseparable (x₁, y₁) (x₂, y₂)
-- Mathlib.Algebra.MvPolynomial.Derivation
MvPolynomial.derivation_eq_zero_of_forall_mem_vars : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] {D : Derivation R (MvPolynomial σ R) A} {f : MvPolynomial σ R},
  (∀ i ∈ f.vars, D (MvPolynomial.X i) = 0) → D f = 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.core : Lean.Expr →
  Lean.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mkHom.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M},
  Localization.mkHom = { toFun := fun x => Localization.mk x.1 x.2, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Order.CompleteLattice.Basic
sInf_Prop_eq : ∀ {s : Set Prop}, sInf s = ∀ p ∈ s, p
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.coe_sSup_of_directedOn : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {S : Set (NonUnitalSubring R)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ↑(sSup S) = ⋃ s ∈ S, ↑s
-- Lean.Meta.Tactic.Simp.Main
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.reduceFVar : Lean.Meta.Simp.Config → Lean.Meta.SimpTheoremsArray → Lean.Expr → Lean.Meta.SimpM Lean.Expr
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze : optParam Bool false → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α}, List.find? (fun x_2 => x_2.1 == k) (Std.DHashMap.Const.toList m) = none ↔ k ∉ m
-- Mathlib.Order.SuccPred.Limit
Order.not_isSuccLimit_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α], ¬Order.IsSuccLimit ⊥
-- Mathlib.Analysis.Complex.RealDeriv
Complex.differentiable_ofReal : Differentiable ℝ Complex.ofReal
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.LaxBraided.instComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {E : Type u₃} →
                  [inst_6 : CategoryTheory.Category.{v₃, u₃} E] →
                    [inst_7 : CategoryTheory.MonoidalCategory E] →
                      [inst_8 : CategoryTheory.BraidedCategory E] →
                        (F : CategoryTheory.Functor C D) →
                          (G : CategoryTheory.Functor D E) → [F.LaxBraided] → [G.LaxBraided] → (F.comp G).LaxBraided
-- Mathlib.Data.List.Cycle
/-- For `x : α`, `s : Cycle α`, `x ∈ s` indicates that `x` occurs at least once in `s`.  -/
Cycle.Mem : {α : Type u_1} → Cycle α → α → Prop
-- Plausible.Testable
Plausible.TestResult.failure.sizeOf_spec : ∀ {p : Prop} [inst : SizeOf p] (a : ¬p) (a_1 : List String) (a_2 : ℕ),
  sizeOf (Plausible.TestResult.failure a a_1 a_2) = 1 + sizeOf a_1 + sizeOf a_2
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- `Function.const` as an `AddHom`.  -/
Pi.constAddHom : (α : Type u_5) → (β : Type u_6) → [inst : Add β] → β →ₙ+ α → β
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.castLE.eq_5 : ∀ {L : FirstOrder.Language} {α : Type u'} (x x_1 : ℕ) (x_2 : x ≤ x_1) (f : L.BoundedFormula α (x + 1)),
  FirstOrder.Language.BoundedFormula.castLE x_2 f.all = (FirstOrder.Language.BoundedFormula.castLE ⋯ f).all
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.map_id : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R), Subring.map (RingHom.id R) s = s
-- Mathlib.Algebra.Order.Archimedean.Basic
exists_rat_lt : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] (x : K), ∃ q, ↑q < x
-- Init.Data.UInt.Lemmas
USize.zero_ne_one : 0 ≠ 1
-- Init.Data.Int.Order
Int.natAbs_pos : ∀ {a : ℤ}, 0 < a.natAbs ↔ a ≠ 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {k a : α} {v : β k}, (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ k ∉ m then some k else m.getKey? a
-- Mathlib.Data.Sym.Basic
_private.Mathlib.Data.Sym.Basic.0.SymOptionSuccEquiv.decode.match_1.splitter : {α : Type u_1} →
  {n : ℕ} →
    (motive : Sym (Option α) n ⊕ Sym α n.succ → Sort u_2) →
      (x : Sym (Option α) n ⊕ Sym α n.succ) →
        ((s : Sym (Option α) n) → motive (Sum.inl s)) → ((s : Sym α n.succ) → motive (Sum.inr s)) → motive x
-- Mathlib.Data.Countable.Basic
SetCoe.countable : ∀ {α : Type u} [Countable α] (s : Set α), Countable ↑s
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.sheafComposeNatTrans_app_uniq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B)
  {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)}
  (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A)
  {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)}
  (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [inst_3 : J.HasSheafCompose F] (P : CategoryTheory.Functor Cᵒᵖ A)
  (α : G₂.obj (P.comp F) ⟶ (CategoryTheory.sheafCompose J F).obj (G₁.obj P)),
  CategoryTheory.CategoryStruct.comp (adj₂.unit.app (P.comp F)) ((CategoryTheory.sheafToPresheaf J B).map α) =
      CategoryTheory.Functor.whiskerRight (adj₁.unit.app P) F →
    α = (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂).app P
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C),
  X.rightOpLeftOpIso.hom.right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Tactic.NormNum.IsSquare
Mathlib.Meta.NormNum.not_isSquare_of_isNNRat_rat_of_den : ∀ (a : ℚ) (n d : ℕ), ¬IsSquare d → n.Coprime d → Mathlib.Meta.NormNum.IsNNRat a n d → ¬IsSquare a
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- Evidence that `h` commutes with the left Kan lift `f₊ g`.  -/
CategoryTheory.Bicategory.LanLift.CommuteWith.isKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : b ⟶ a) →
        (g : c ⟶ a) →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] →
            {x : B} →
              (h : x ⟶ c) →
                [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] →
                  ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h).IsKan
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.injective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Function.Injective ⇑h
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_pow : ∀ {b : ENNReal}, (ExpGrowth.expGrowthInf fun n => b ^ n) = b.log
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- When `h : F.IsEventuallyConstantTo i₀`, the limit of `F` exists and is `F.obj i₀`.  -/
CategoryTheory.Functor.IsEventuallyConstantTo.isLimitCone : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {F : CategoryTheory.Functor J C} →
          {i₀ : J} →
            (h : F.IsEventuallyConstantTo i₀) →
              [inst_2 : CategoryTheory.IsCofiltered J] → CategoryTheory.Limits.IsLimit h.cone
-- Init.Data.Bool
Bool.or_comm : ∀ (x y : Bool), (x || y) = (y || x)
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.ringEquivOfRingEquivHom_apply : ∀ (A : Type u_8) (K : Type u_9) [inst : CommRing A] [inst_1 : CommRing K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] (f : A ≃+* A),
  (IsFractionRing.ringEquivOfRingEquivHom A K) f = IsFractionRing.ringEquivOfRingEquiv f
-- Init.Control.Basic
/-- Left-to-right composition of Kleisli arrows. 

Conventions for notations in identifiers:

 * The recommended spelling of `>=>` in identifiers is `kleisliRight`. -/
«term_>=>_» : Lean.TrailingParserDescr
-- Init.Data.SInt.Lemmas
Int64.toInt8_sub : ∀ (a b : Int64), (a - b).toInt8 = a.toInt8 - b.toInt8
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁_obj_obj_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁ C).obj X₁).obj X₂).obj X₃ =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃) X₁
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Ineq.WithStrictness.lt.sizeOf_spec : ∀ (strict : Bool), sizeOf (Mathlib.Ineq.WithStrictness.lt strict) = 1 + sizeOf strict
-- Mathlib.Algebra.Homology.HomotopyFiber
/-- The property that a homological complex `K` has a path object,
i.e. that the morphism `K ⟶ K ⊞ K` induced by `𝟙 K` and `-𝟙 K`
has a homotopy fiber.  -/
HomologicalComplex.HasPathObject : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {α : Type u_2} →
        {c : ComplexShape α} →
          (K : HomologicalComplex C c) → [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] → Prop
-- Mathlib.Topology.IndicatorConstPointwise
tendsto_indicator_const_apply_iff_eventually' : ∀ {α : Type u_1} {A : Set α} {β : Type u_2} [inst : Zero β] [inst_1 : TopologicalSpace β] {ι : Type u_3} (L : Filter ι)
  {As : ι → Set α} (b : β),
  {0}ᶜ ∈ nhds b →
    {b}ᶜ ∈ nhds 0 →
      ∀ (x : α),
        Filter.Tendsto (fun i => (As i).indicator (fun x => b) x) L (nhds (A.indicator (fun x => b) x)) ↔
          ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instVAdd.eq_1 : ∀ (M : Type v) (X : Type x) [inst : UniformSpace X] [inst_1 : VAdd M X],
  UniformSpace.Completion.instVAdd M X = { vadd := fun c => UniformSpace.Completion.map fun x => c +ᵥ x }
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.Fun.mk.injEq : ∀ {X : Type u_1} {Y : Type u_2} (toFun toFun_1 : X → Y), ({ toFun := toFun } = { toFun := toFun_1 }) = (toFun = toFun_1)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Functor.isRightAdjoint_comp_iff_left : ∀ {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 : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [G.IsEquivalence], (F.comp G).IsRightAdjoint ↔ F.IsRightAdjoint
-- Mathlib.Order.Category.DistLat
DistLat.hom_ext_iff : ∀ {X Y : DistLat} {f g : X ⟶ Y}, f = g ↔ DistLat.Hom.hom f = DistLat.Hom.hom g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_filterMap! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → Option γ} {k fallback : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap! f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => (f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯)).isSome).getD fallback
-- Mathlib.RingTheory.Derivation.Basic
/-- Define `Derivation R A M` from a linear map when `M` is cancellative by verifying the Leibniz
rule.  -/
Derivation.mk' : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : CommSemiring A] →
        [inst_2 : Algebra R A] →
          {M : Type u_3} →
            [inst_3 : AddCancelCommMonoid M] →
              [inst_4 : Module R M] →
                [inst_5 : Module A M] →
                  (D : A →ₗ[R] M) → (∀ (a b : A), D (a * b) = a • D b + b • D a) → Derivation R A M
-- Init.Data.Nat.Lemmas
Nat.div_lt_one_iff : ∀ {b a : ℕ}, 0 < b → (a / b < 1 ↔ a < b)
-- Mathlib.Analysis.Normed.Ring.Lemmas
/-- Non-unital seminormed ring structure on the product of finitely many non-unital seminormed
rings, using the sup norm.  -/
Pi.nonUnitalSeminormedRing : {ι : Type u_3} →
  {R : ι → Type u_4} → [Fintype ι] → [(i : ι) → NonUnitalSeminormedRing (R i)] → NonUnitalSeminormedRing ((i : ι) → R i)
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.opEquiv_inverse_map_inclRight_op : ∀ (C : Type u₁) {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {c c' : C} (f : c ⟶ c'),
  (CategoryTheory.Join.opEquiv C D).inverse.map ((CategoryTheory.Join.inclRight Dᵒᵖ Cᵒᵖ).map f.op) =
    Opposite.op ((CategoryTheory.Join.inclLeft C D).map f)
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.coe_toEquiv_symm : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), e.toEquiv.symm = ↑e.symm
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- Given a submonoid `s` of `M`, we say that `s` is **saturated** if it satisfies
`x * y ∈ s → x ∈ s ∧ y ∈ s`.

It is called `MulSaturated` here to be distinguished from `Submonoid.PowSaturated` or
`AddSubmonoid.NSMulSaturated`, which is also called "saturated" in the literature.  -/
Submonoid.MulSaturated : {M : Type u_1} → [inst : MulOneClass M] → Submonoid M → Prop
-- Mathlib.CategoryTheory.Limits.Cones
/-- The isomorphism between a cone on `F` and an element of the functor `F.cones`.  -/
CategoryTheory.Limits.Cone.equiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) →
          CategoryTheory.Limits.Cone F ≅ (X : Cᵒᵖ) × ((CategoryTheory.Functor.const J).obj (Opposite.unop X) ⟶ F)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintTextEdit.mk : Lean.Syntax.Range → String → Lean.Elab.InlayHintTextEdit
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.tensorHom_comp_tensorHom : ∀ {C : Type u} {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : CategoryTheory.FreeMonoidalCategory C} (f₁ : X₁.Hom Y₁) (f₂ : X₂.Hom Y₂)
  (g₁ : Y₁.Hom Z₁) (g₂ : Y₂.Hom Z₂),
  CategoryTheory.FreeMonoidalCategory.HomEquiv ((f₁.tensor f₂).comp (g₁.tensor g₂)) ((f₁.comp g₁).tensor (f₂.comp g₂))
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.HasCokernels.has_colimit : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  [self : CategoryTheory.Limits.HasCokernels C] {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasCokernel f
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.mk.injEq : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (toIntermediateField : IntermediateField k K) [finiteDimensional : FiniteDimensional k ↥toIntermediateField]
  [isGalois : IsGalois k ↥toIntermediateField] (toIntermediateField_1 : IntermediateField k K)
  (finiteDimensional_1 : FiniteDimensional k ↥toIntermediateField_1) (isGalois_1 : IsGalois k ↥toIntermediateField_1),
  ({ toIntermediateField := toIntermediateField, finiteDimensional := finiteDimensional, isGalois := isGalois } =
      { toIntermediateField := toIntermediateField_1, finiteDimensional := finiteDimensional_1,
        isGalois := isGalois_1 }) =
    (toIntermediateField = toIntermediateField_1)
-- Mathlib.Topology.Order.LeftRight
nhdsWithinGE_sup_nhdsWithinLT : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {s : Set α} (a : α),
  nhdsWithin a (s ∩ Set.Ici a) ⊔ nhdsWithin a (s ∩ Set.Iio a) = nhdsWithin a s
-- Mathlib.Data.Subtype
/-- A version of `x.property` or `x.2` where `p` is syntactically applied to the coercion of `x`
instead of `x.1`. A similar result is `Subtype.mem` in `Mathlib/Data/Set/Basic.lean`.  -/
Subtype.prop : ∀ {α : Sort u_1} {p : α → Prop} (x : Subtype p), p ↑x
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.lowerCentralSeries_map_eq_lcs : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (k : ℕ) (N : LieSubmodule R L M)
  [LieModule R L M], LieSubmodule.map N.incl (LieModule.lowerCentralSeries R L (↥N) k) = LieSubmodule.lcs k N
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_subset_uIcc : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α},
  a₁ ∈ Finset.uIcc a₂ b₂ → b₁ ∈ Finset.uIcc a₂ b₂ → Finset.uIcc a₁ b₁ ⊆ Finset.uIcc a₂ b₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Complex.cos_eq_tsum : ∀ (z : ℂ), Complex.cos z = ∑' (n : ℕ), (-1) ^ n * z ^ (2 * n) / ↑(2 * n).factorial
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.instCategory : CategoryTheory.Category.{u, u + 1} AddMagmaCat
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.localRingHom.eq_1 : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {B : Type u_4} {τ : Type u_5} [inst_6 : CommRing B] [inst_7 : SetLike τ B]
  [inst_8 : AddSubgroupClass τ B] {ℬ : ι → τ} [inst_9 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (I : Ideal A) [inst_10 : I.IsPrime]
  (J : Ideal B) [inst_11 : J.IsPrime] (hIJ : I = Ideal.comap f J),
  HomogeneousLocalization.localRingHom f I J hIJ = HomogeneousLocalization.map f ⋯
-- Std.Data.DTreeMap.Internal.Operations
/-- Transforms a list of mappings into a tree map.  -/
Std.DTreeMap.Internal.Impl.Const.ofArray : {α : Type u} → {β : Type v} → [Ord α] → Array (α × β) → Std.DTreeMap.Internal.Impl α fun x => β
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.rnDeriv_posterior : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω] [inst_4 : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧],
  (∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)) →
    ∀ᵐ (ω : Ω) ∂μ,
      ∀ᵐ (x : 𝓧) ∂μ.bind ⇑κ,
        (ProbabilityTheory.posterior κ μ).rnDeriv (ProbabilityTheory.Kernel.const 𝓧 μ) x ω =
          κ.rnDeriv (ProbabilityTheory.Kernel.const Ω (μ.bind ⇑κ)) ω x
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.mkTermInfo : Lean.Name →
  Lean.Syntax →
    Lean.Expr →
      optParam (Option Lean.Expr) none →
        optParam (Option Lean.LocalContext) none →
          optParam Bool false → optParam Bool false → Lean.Elab.TermElabM (Lean.Elab.Info ⊕ Lean.MVarId)
-- Init.Data.UInt.Lemmas
USize.toNat_mod_size : ∀ (n : USize), n.toNat % USize.size = n.toNat
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_of_mem_keys : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {k : α}, m.WF → k ∈ m.keys → k ∈ m
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
FiberBundle.exists_mdifferentiableOn_extend : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (F : Type u_5) [inst_6 : NormedAddCommGroup F]
  {V : M → Type u_6} [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → AddCommGroup (V x)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : NormedSpace 𝕜 F]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [inst_13 : VectorBundle 𝕜 F V] [ContMDiffVectorBundle 1 F V I] {x₀ : M}
  (σ₀ : V x₀), ∃ s ∈ nhds x₀, MDiff[s] fun x' => ⟨x', FiberBundle.extend F σ₀ x'⟩
-- Init.Data.SInt.Bitwise
Int8.xor_right_inj : ∀ {a b : Int8} (c : Int8), c ^^^ a = c ^^^ b ↔ a = b
-- Init.Data.Nat.Fold
/-- Checks whether a predicate holds for all natural numbers in a range.

In particular, `(start, stop).allI f` returns true if `f` is true for all natural numbers from
`start` (inclusive) to `stop` (exclusive).

Examples:
 * `(5, 8).allI (fun j _ _ => j < 10) = (5 < 10) && (6 < 10) && (7 < 10)`
 * `(5, 8).allI (fun j _ _ => j % 2 = 0) = false`
 * `(6, 7).allI (fun j _ _ => j % 2 = 0) = true`
 -/
Prod.allI : (i : ℕ × ℕ) → ((j : ℕ) → i.1 ≤ j → j < i.2 → Bool) → Bool
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
quasispectrum_realPart' : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [inst_6 : StarModule ℂ A]
  [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A),
  autoParam (IsStarNormal a) quasispectrum_realPart'._auto_1 →
    quasispectrum ℝ ↑(realPart a) = Complex.re '' quasispectrum ℂ a
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
/-- The colimit cocone expressing that `Φ.iteration J` is the colimit
of `Φ.iterationFunctor J`.  -/
CategoryTheory.SmallObject.SuccStruct.iterationCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Φ : CategoryTheory.SmallObject.SuccStruct C) →
      (J : Type w) →
        [inst_1 : LinearOrder J] →
          [inst_2 : OrderBot J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : WellFoundedLT J] →
                [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] →
                  CategoryTheory.Limits.Cocone (Φ.iterationFunctor J)