mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.descOfIsLeftKanExtension_fac_assoc : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [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]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] (G : CategoryTheory.Functor D H) (β : F ⟶ L.comp G)
  {Z : CategoryTheory.Functor C H} (h : L.comp G ⟶ Z),
  CategoryTheory.CategoryStruct.comp α
      (CategoryTheory.CategoryStruct.comp (L.whiskerLeft (F'.descOfIsLeftKanExtension α G β)) h) =
    CategoryTheory.CategoryStruct.comp β h
-- Mathlib.Topology.Order.Completion
Order.Fill.instTopologicalSpace : {α : Type u_1} → [inst : LinearOrder α] → TopologicalSpace (Order.Fill α)
-- Mathlib.Data.Finsupp.Weight
Finsupp.exists_le_degree_eq : ∀ {σ : Type u_5} (f : σ →₀ ℕ), ∀ n ≤ Finsupp.degree f, ∃ g ≤ f, Finsupp.degree g = n
-- Mathlib.Order.LiminfLimsup
Filter.limsInf_principal_eq_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α},
  BddBelow s → s.Nonempty → (Filter.principal s).limsInf = sInf s
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α}
  {fallback : β a} {v : β k},
  (m.insertIfNew k v).getD a fallback = if h : (k == a) = true ∧ k ∉ m then cast ⋯ v else m.getD a fallback
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
/-- (An auxiliary definition for `functorCategoryMonoidal`.)
Tensor product of natural transformations into `D`, when `D` is monoidal.
 -/
CategoryTheory.Monoidal.FunctorCategory.tensorHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          {F G F' G' : CategoryTheory.Functor C D} →
            (F ⟶ G) →
              (F' ⟶ G') →
                (CategoryTheory.Monoidal.FunctorCategory.tensorObj F F' ⟶
                  CategoryTheory.Monoidal.FunctorCategory.tensorObj G G')
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The sine of the angle between three points is 0 if and only if the angle is 0 or π.  -/
EuclideanGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 0 ↔
    EuclideanGeometry.angle p₁ p₂ p₃ = 0 ∨ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
RingHom.polyToMatrix.eq_1 : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] {n : Type w} [inst_2 : DecidableEq n]
  [inst_3 : Fintype n] (f : A →+* Matrix n n R),
  f.polyToMatrix = matPolyEquiv.symm.toRingEquiv.toRingHom.comp (Polynomial.mapRingHom f)
-- Mathlib.Order.BourbakiWitt
/-- The bottom admissible set with base point `x` and inflationary function `f`  -/
ChainCompletePartialOrder.bot : {α : Type u_1} → [ChainCompletePartialOrder α] → α → (α → α) → Set α
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
/-- The diagram used to define `P⁺`, composed with `F`, is isomorphic
to the diagram used to define `P ⋙ F`.  -/
CategoryTheory.GrothendieckTopology.diagramCompIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          {E : Type u_2} →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} E] →
              (F : CategoryTheory.Functor D E) →
                [inst_3 :
                    ∀ (J : CategoryTheory.Limits.MulticospanShape),
                      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D] →
                  [inst_4 :
                      ∀ (J : CategoryTheory.Limits.MulticospanShape),
                        CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E] →
                    [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
                          CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] →
                      (P : CategoryTheory.Functor Cᵒᵖ D) → (X : C) → (J.diagram P X).comp F ≅ J.diagram (P.comp F) X
-- Mathlib.Order.ModularLattice
/-- A lower modular lattice is a lattice where `a` and `b` both cover `a ⊓ b` if `a ⊔ b` covers
either `a` or `b`.  -/
IsLowerModularLattice : (α : Type u_2) → [Lattice α] → Prop
-- Mathlib.Order.Hom.Order
OrderHom.sSup_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : CompleteLattice β] (s : Set (α →o β)) (x : α),
  (sSup s) x = ⨆ f ∈ s, f x
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.instBiproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type v} (g : β → C)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasBiproduct g]
  [∀ (b : β), CategoryTheory.Projective (g b)], CategoryTheory.Projective (⨁ g)
-- Std.Async.Basic
/-- Block until the `AsyncTask` in `x` finishes.
 -/
Std.Async.AsyncTask.block : {α : Type} → Std.Async.AsyncTask α → IO α
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.add_zero : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S]
  (x : AddOreLocalization S R), x + 0 = x
-- Mathlib.Order.Lattice
Pi.instDistribLattice : {ι : Type u_1} → {α' : ι → Type u_2} → [(i : ι) → DistribLattice (α' i)] → DistribLattice ((i : ι) → α' i)
-- Init.Data.Fin.Bitwise
Fin.or_val_of_uInt8Size : ∀ (a b : Fin UInt8.size), ↑(a ||| b) = ↑a ||| ↑b
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.invEquivalence_functor_map : ∀ (C : Type u) [inst : CategoryTheory.Groupoid C] {x x_1 : C} (f : x ⟶ x_1),
  (CategoryTheory.Groupoid.invEquivalence C).functor.map f = (CategoryTheory.Groupoid.inv f).op
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.integrable_condExp : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E], MeasureTheory.Integrable μ[f | m] μ
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indepSets_iff_singleton_indepSets : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒜 ℬ : Set (Set Ω)},
  ProbabilityTheory.IndepSets 𝒜 ℬ μ ↔ ∀ A ∈ 𝒜, ProbabilityTheory.IndepSets {A} ℬ μ
-- Mathlib.Data.Num.ZNum
ZNum.commRing : CommRing ZNum
-- Batteries.Util.Pickle
pickle.unsafe_impl_2 : {α : Type} → α → Lean.ModuleData
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.instCoeSortType : CoeSort CommRingCat (Type u)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_one_of_one_lt_of_neg : ∀ {x z : ℝ}, 1 < x → z < 0 → x ^ z < 1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKey?.eq_2 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxKey? = some k
-- Mathlib.Algebra.Tropical.Basic
/-- Tropical multiplication is the addition in the underlying `R`.  -/
Tropical.instMulOfAdd : {R : Type u} → [Add R] → Mul (Tropical R)
-- Mathlib.Data.FunLike.Group
FunLike.group.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : One F]
  [inst_3 : Pow F ℕ] [inst_4 : Inv F] [inst_5 : Div F] [inst_6 : Pow F ℤ] [inst_7 : Group β] [inst_8 : IsOneApply F α β]
  [inst_9 : IsMulApply F α β] [inst_10 : IsInvApply F α β] [inst_11 : IsDivApply F α β] [inst_12 : IsPowApply ℕ F α β]
  [inst_13 : IsPowApply ℤ F α β], FunLike.group = Function.Injective.group (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.MeasureTheory.Measure.Hausdorff
IsometryEquiv.hausdorffMeasure_image : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] (e : X ≃ᵢ Y) (d : ℝ) (s : Set X),
  (MeasureTheory.Measure.hausdorffMeasure d) (⇑e '' s) = (MeasureTheory.Measure.hausdorffMeasure d) s
-- Mathlib.LinearAlgebra.Quotient.Defs
/-- The map from a module `M` to the quotient of `M` by a submodule `p` as a linear map.  -/
Submodule.mkQ : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (p : Submodule R M) → M →ₗ[R] M ⧸ p
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_inv_natCast_smul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : StarAddMonoid α] [inst_3 : Module R α] (c : ℕ) (M : Matrix m n α),
  ((↑c)⁻¹ • M).conjTranspose = (↑c)⁻¹ • M.conjTranspose
-- Lean.Expr
Lean.instBEqMVarId.beq : Lean.MVarId → Lean.MVarId → Bool
-- Mathlib.Data.Nat.Squarefree
Nat.minSqFac_has_prop : ∀ (n : ℕ), n.MinSqFacProp n.minSqFac
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- This is the `Finset` version of `incidenceSet`.  -/
SimpleGraph.incidenceFinset : {V : Type u_1} → (G : SimpleGraph V) → (v : V) → [Fintype ↑(G.neighborSet v)] → [DecidableEq V] → Finset (Sym2 V)
-- Mathlib.Data.Finset.Prod
Finset.Nonempty.fst : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, (s ×ˢ t).Nonempty → s.Nonempty
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.op_r : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (h : S.Splitting), h.op.r = h.s.op
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- The First-Derivative Test from calculus, minima version.  -/
isLocalMin_of_deriv_Ioo : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  a < b →
    b < c →
      ContinuousAt f b →
        DifferentiableOn ℝ f (Set.Ioo a b) →
          DifferentiableOn ℝ f (Set.Ioo b c) →
            (∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) → (∀ x ∈ Set.Ioo b c, 0 ≤ deriv f x) → IsLocalMin f b
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.toLinearMap_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E ≃ₗ[𝕜] E}, (↑T).IsSymmetric → (↑T.symm).IsSymmetric
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeAddGroup.nonempty_basis : ∀ {G : Type u} {inst : AddGroup G} [self : IsFreeAddGroup G], ∃ ι, Nonempty (FreeAddGroupBasis ι G)
-- Mathlib.RepresentationTheory.Coinvariants
/-- The coinvariants of a representation, `V ⧸ ⟨{ρ g x - x | g ∈ G, x ∈ V}⟩`.  -/
Representation.Coinvariants : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] → [inst_2 : AddCommGroup V] → [inst_3 : Module k V] → Representation k G V → Type u_3
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.w_prod_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : D) (S' : D') (T : CategoryTheory.Functor C D)
  (T' : CategoryTheory.Functor C' D') {X Y : CategoryTheory.StructuredArrow (S, S') (T.prod T')} (f : X ⟶ Y) {Z : D}
  (h : T.obj Y.right.1 ⟶ Z),
  CategoryTheory.CategoryStruct.comp X.hom.1
      (CategoryTheory.CategoryStruct.comp (T.map (CategoryTheory.StructuredArrow.Hom.right f).1) h) =
    CategoryTheory.CategoryStruct.comp Y.hom.1 h
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.measure_eq_measure_larger_of_between_null_sdiff`. -/
MeasureTheory.measure_eq_measure_larger_of_between_null_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α},
  s₁ ⊆ s₂ → s₂ ⊆ s₃ → μ (s₃ \ s₁) = 0 → μ s₂ = μ s₃
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.snd_pow : ∀ {α : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α]
  (s : NonemptyInterval α) (n : ℕ), (s ^ n).toProd.2 = s.toProd.2 ^ n
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addLeftReflectLT : ∀ {α : Type u} [inst : Add α] [inst_1 : LT α] [AddLeftReflectLT α], AddLeftReflectLT (WithTop α)
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Split the tree into those smaller than `x` and those greater than it.
If an element equivalent to `x` is in the set, it is discarded.

```
split 2 {1, 2, 4} = ({1}, {4})
split 3 {1, 2, 4} = ({1, 2}, {4})
split 4 {1, 2, 4} = ({1, 2}, ∅)
```

Using a preorder on `ℕ × ℕ` that only compares the first coordinate:

```
split (1, 1) {(0, 1), (1, 2)} = ({(0, 1)}, ∅)
split (3, 1) {(0, 1), (1, 2)} = ({(0, 1), (1, 2)}, ∅)
```  -/
Ordnode.split : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → Ordnode α × Ordnode α
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.ofClass_coe : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B]
  [inst_4 : FunLike F A B] [inst_5 : MonoidHomClass F A B] [inst_6 : StarHomClass F A B] (f : F) (a : A),
  (StarMonoidHom.ofClass f) a = f a
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithBot.unbot.match_1.splitter : {α : Type u_1} →
  (motive : (x : WithBot α) → x ≠ ⊥ → Sort u_2) →
    (x : WithBot α) → (x_1 : x ≠ ⊥) → ((x : α) → (x_2 : ↑x ≠ ⊥) → motive (some x) x_2) → motive x x_1
-- Std.Sat.AIG.Basic
/-- Get the value of `ref` if it is constant.
 -/
Std.Sat.AIG.getConstant : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → aig.Ref → Option Bool
-- Init.Data.Float.Model.Unpacked.Operations.OfNat
/-- Converts an `Int` to an `UnpackedFloat`, returning positive zero on zero.  -/
Float.Model.UnpackedFloat.ofInt : Float.Model.Format → ℤ → Float.Model.UnpackedFloat
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_eq_push : ∀ {n : ℕ}, 0 < n → (*...n).toArray = (*...n - 1).toArray.push (n - 1)
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
AddAction.isPreprimitive_fixingAddSubgroup_insert_iff : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {a : α}
  {t : Set ↥(SubAddAction.ofStabilizer G a)},
  AddAction.IsPreprimitive ↥(fixingAddSubgroup G (insert a (Subtype.val '' t)))
      ↥(SubAddAction.ofFixingAddSubgroup G (insert a (Subtype.val '' t))) ↔
    AddAction.IsPreprimitive ↥(fixingAddSubgroup (↥(AddAction.stabilizer G a)) t)
      ↥(SubAddAction.ofFixingAddSubgroup (↥(AddAction.stabilizer G a)) t)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.toList.eq_1 : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n), c.toList = c.clause
-- Init.Data.SInt.Lemmas
Int8.iSizeMinValue_le_toInt : ∀ (x : Int8), ISize.minValue.toInt ≤ x.toInt
-- Mathlib.Algebra.Free
FreeSemigroup.map_of : ∀ {α : Type u} {β : Type v} (f : α → β) (x : α), (FreeSemigroup.map f) (FreeSemigroup.of x) = FreeSemigroup.of (f x)
-- Mathlib.Topology.Order.OrderClosed
eventually_gt_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  b < a → ∀ᶠ (x : α) in nhds a, b < x
-- Mathlib.Algebra.CharP.Frobenius
frobenius.congr_simp : ∀ (R : Type u_3) [inst : CommSemiring R] (p p_1 : ℕ) (e_p : p = p_1) [inst_1 : ExpChar R p],
  frobenius R p = frobenius R p_1
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.of_eq : ∀ {f g : ℕ →. ℕ} {O : Set (ℕ →. ℕ)}, Nat.RecursiveIn O f → (∀ (n : ℕ), f n = g n) → Nat.RecursiveIn O g
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
AlgebraicGeometry.Proj.instIsProperToSpecZeroOfFiniteTypeSubtypeMemOfNatNat : ∀ {σ : Type u_1} {A : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A],
  AlgebraicGeometry.IsProper (AlgebraicGeometry.Proj.toSpecZero 𝒜)
-- Mathlib.Algebra.Free
FreeSemigroup.lift.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Semigroup β],
  FreeSemigroup.lift =
    { toFun := fun f => { toFun := fun x => List.foldl (fun a b => a * f b) (f x.head) x.tail, map_mul' := ⋯ },
      invFun := fun f => ⇑f ∘ FreeSemigroup.of, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.instHomIsOverLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {X Y : CategoryTheory.Over S} (f : X ⟶ Y),
  CategoryTheory.HomIsOver (CategoryTheory.Over.Hom.left f) S
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instAddZeroClass : {α : Type u} → [Add α] → AddZeroClass (WithZero α)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ),
  X.leftOpRightOpIso.hom.left = CategoryTheory.CategoryStruct.id X.left
-- Lean.Meta.LazyDiscrTree
/-- Exception that triggers error.  -/
Lean.Meta.LazyDiscrTree.ImportFailure.exception : Lean.Meta.LazyDiscrTree.ImportFailure → Lean.Exception
-- Mathlib.Data.EReal.Basic
EReal.coe_nnreal_ne_top : ∀ (x : NNReal), ↑↑x ≠ ⊤
-- Mathlib.RingTheory.Smooth.Kaehler
/-- Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`.
Let `σ` be an arbitrary (set-theoretic) section of `f`.
Suppose we have a retraction `l` of the injection `I →ₗ[P] S ⊗[P] Ω[P/R]`, then
`x ↦ σ x - l (1 ⊗ D (σ x))` is an algebra homomorphism and a section to `f`.
 -/
sectionOfRetractionKerToTensorAux : {R : Type u_1} →
  {P : Type u_2} →
    {S : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing P] →
          [inst_2 : CommRing S] →
            [inst_3 : Algebra R P] →
              [inst_4 : Algebra P S] →
                (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))) →
                  l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id →
                    (σ : S → P) →
                      (∀ (x : S), (algebraMap P S) (σ x) = x) →
                        [inst_5 : Algebra R S] →
                          [IsScalarTower R P S] → RingHom.ker (algebraMap P S) ^ 2 = ⊥ → S →ₐ[R] P
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.coe_mk : ∀ (z : ℂ) (hz : ‖z‖ < 1), ↑(Complex.UnitDisc.mk z hz) = z
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigOWith.right_le_add_of_lt_one : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {c : ℝ} {l : Filter α} {f₁ f₂ : α → E'},
  Asymptotics.IsBigOWith c l f₁ f₂ → c < 1 → Asymptotics.IsBigOWith (1 / (1 - c)) l f₂ fun x => f₁ x + f₂ x
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.sumEquiv_unitIso_inv_app : ∀ {J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete (J ⊕ K)),
  CategoryTheory.Discrete.sumEquiv.unitIso.inv.app X =
    (match X.as with
      | Sum.inl x => CategoryTheory.Iso.refl { as := Sum.inl x }
      | Sum.inr x => CategoryTheory.Iso.refl { as := Sum.inr x }).inv
-- Init.Data.Int.OfNat
Nat.ToInt.add_congr : ∀ {a b : ℕ} {a' b' : ℤ}, ↑a = a' → ↑b = b' → ↑(a + b) = a' + b'
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_sub_const_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Integrable X μ →
    ∀ (c : ℝ), ProbabilityTheory.covariance (fun ω => X ω - c) Y μ = ProbabilityTheory.covariance X Y μ
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.map_σ : ∀ {α : Type u_1} {β : Type u_2} (m : α → β) {f : Filter α} (F : f.Realizer), (Filter.Realizer.map m F).σ = F.σ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.coe_mapCycles₂ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : ↑(ModuleCat.of k ↥(groupHomology.cycles₂ A))),
  ↑((CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₂ f φ)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsMap₂ f φ)) ↑x
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.recordCongrTheorem : Lean.Name → Lean.Meta.SimpM Unit
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listDecode_encode_list : ∀ {L : FirstOrder.Language} {α : Type u'} (l : List ((n : ℕ) × L.BoundedFormula α n)),
  FirstOrder.Language.BoundedFormula.listDecode (List.flatMap (fun φ => φ.snd.listEncode) l) = l
-- Mathlib.RingTheory.PowerSeries.WellKnown
_private.Mathlib.RingTheory.PowerSeries.WellKnown.0.PowerSeries.invOneSubPow.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((d : ℕ) → motive d.succ) → motive x
-- Mathlib.Data.Multiset.Replicate
Multiset.card_replicate : ∀ {α : Type u_1} (n : ℕ) (a : α), (Multiset.replicate n a).card = n
-- Mathlib.Computability.Ackermann
_private.Mathlib.Computability.Ackermann.0.ack.match_1.eq_3 : ∀ (motive : ℕ → ℕ → Sort u_1) (m n : ℕ) (h_1 : (n : ℕ) → motive 0 n) (h_2 : (m : ℕ) → motive m.succ 0)
  (h_3 : (m n : ℕ) → motive m.succ n.succ),
  (match m.succ, n.succ with
    | 0, n => h_1 n
    | m.succ, 0 => h_2 m
    | m.succ, n.succ => h_3 m n) =
    h_3 m n
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instToJsonDiagnosticRelatedInformation : Lean.ToJson Lean.Lsp.DiagnosticRelatedInformation
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (h : S.Splitting) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct S.X₁ S.X₃],
  h.isoBinaryBiproduct.inv = CategoryTheory.Limits.biprod.desc S.f h.s
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.hasInv : {R : Type u_1} → [inst : CommMonoid R] → {R' : Type u_2} → [inst_1 : CommMonoidWithZero R'] → Inv (MulChar R R')
-- Mathlib.Topology.MetricSpace.TransferInstance
/-- Transfer a `PseudoMetricSpace` across an `Equiv`  -/
Equiv.pseudometricSpace : {α : Type u_1} → {β : Type u_2} → [PseudoMetricSpace β] → α ≃ β → PseudoMetricSpace α
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.isInvertedBy₂ : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit),
  W.IsInvertedBy₂ W
    ((CategoryTheory.MonoidalCategory.curriedTensor C).comp
      ((CategoryTheory.Functor.whiskeringRight C C D).obj
        (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)))
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.mul_one : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : (i : ι) → NonAssocSemiring (A i)]
  [inst_2 : (i : ι) → Module R (A i)] [inst_3 : ∀ (i : ι), SMulCommClass R (A i) (A i)]
  [inst_4 : ∀ (i : ι), IsScalarTower R (A i) (A i)] (x : PiTensorProduct R fun i => A i),
  (PiTensorProduct.mul x) ((PiTensorProduct.tprod R) 1) = x
-- Std.Sync.SharedMutex
/-- Attempts to lock a `BaseSharedMutex` for shared read access. If the mutex is not available
return `false`, otherwise lock it and return `true`.

The current thread must not have already locked the mutex.
Reentrant locking is undefined behavior (inherited from the C++ implementation).
 -/
Std.BaseSharedMutex.tryRead : Std.BaseSharedMutex → BaseIO Bool