mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_inv_same : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f →
    (∀ᵐ (x : α) ∂μ, f x ≠ 0) → (∀ᵐ (x : α) ∂μ, f x ≠ ⊤) → ((μ.withDensity f).withDensity fun x => (f x)⁻¹) = μ
-- Mathlib.CategoryTheory.Category.Bipointed
/-- Turns a bipointing into a bipointed type.  -/
Bipointed.of : {X : Type u_1} → X × X → Bipointed
-- Mathlib.Algebra.Ring.CentroidHom
/-- The natural ring homomorphism from `R` into `CentroidHom α`.

This is a stronger version of `Module.toAddMonoidEnd`.  -/
Module.toCentroidHom : {α : Type u_5} →
  [inst : NonUnitalNonAssocSemiring α] →
    {R : Type u_6} →
      [inst_1 : CommSemiring R] →
        [inst_2 : Module R α] → [SMulCommClass R α α] → [IsScalarTower R α α] → R →+* CentroidHom α
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
IsTopologicallyNilpotent.eq_1 : ∀ {R : Type u_1} [inst : MonoidWithZero R] [inst_1 : TopologicalSpace R] (a : R),
  IsTopologicallyNilpotent a = Filter.Tendsto (fun x => a ^ x) Filter.atTop (nhds 0)
-- Mathlib.Analysis.Normed.Group.FunctionSeries
/-- An infinite sum of functions with summable sup norm is the uniform limit of its partial sums.
Version with index set `ℕ`.  -/
tendstoUniformly_tsum_nat : ∀ {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [CompleteSpace F] {f : ℕ → β → F} {u : ℕ → ℝ},
  Summable u →
    (∀ (n : ℕ) (x : β), ‖f n x‖ ≤ u n) →
      TendstoUniformly (fun N x => ∑ n ∈ Finset.range N, f n x) (fun x => ∑' (n : ℕ), f n x) Filter.atTop
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mulLECancellable_mul : ∀ {α : Type u_1} [inst : LE α] [inst_1 : CommSemigroup α] [MulLeftMono α] {a b : α},
  MulLECancellable (a * b) ↔ MulLECancellable a ∧ MulLECancellable b
-- Std.Net.Addr
Std.Net.instInhabitedInterfaceAddress.default : Std.Net.InterfaceAddress
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod.instNullSingletonClass_fst : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.NullSingletonClass μ], MeasureTheory.NullSingletonClass (μ.prod ν)
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
/-- The vector measure associated to a bounded variation function `f`, giving mass
`f.rightLim b - f.leftLim a` to closed intervals `[a, b]`, and similarly for other intervals.  -/
BoundedVariationOn.vectorMeasure : {α : Type u_1} →
  [inst : LinearOrder α] →
    [DenselyOrdered α] →
      [inst_2 : TopologicalSpace α] →
        [OrderTopology α] →
          [SecondCountableTopology α] →
            [CompactIccSpace α] →
              [hα : MeasurableSpace α] →
                [BorelSpace α] →
                  {E : Type u_2} →
                    [inst_7 : NormedAddCommGroup E] →
                      [CompleteSpace E] → {f : α → E} → BoundedVariationOn f Set.univ → MeasureTheory.VectorMeasure α E
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Struct.idempotentInst? : Lean.Meta.Grind.AC.Struct → Option Lean.Expr
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.mk.injEq : ∀ (X : Type u) (toTwoPointing : TwoPointing X) (X_1 : Type u) (toTwoPointing_1 : TwoPointing X_1),
  ({ X := X, toTwoPointing := toTwoPointing } = { X := X_1, toTwoPointing := toTwoPointing_1 }) =
    (X = X_1 ∧ toTwoPointing ≍ toTwoPointing_1)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformity_basis_dist_lt : ∀ {α : Type u} [inst : PseudoMetricSpace α] {R : ℝ},
  0 < R → (uniformity α).HasBasis (fun r => 0 < r ∧ r < R) fun r => {p | dist p.1 p.2 < r}
-- Mathlib.Order.Filter.FilterProduct
_private.Mathlib.Order.Filter.FilterProduct.0.Filter.«term∀*_,_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.comap_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (K : CategoryTheory.Precoverage C),
  CategoryTheory.Precoverage.comap (CategoryTheory.Functor.id C) K = K
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
/-- The image of a simplicial set by the involution `opFunctor : SSet ⥤ SSet`.  -/
SSet.op : SSet → SSet
-- Mathlib.Algebra.Quandle
Quandle.conj_swap : ∀ {G : Type u_2} [inst : Group G] (x y : Quandle.Conj G), Shelf.act x y = y ↔ Shelf.act y x = x
-- Lean.Compiler.ImplementedByAttr
/-- Instructs the compiler to use a different function as the implementation of a function. With the
exception of tactics that call native code such as `native_decide`, the kernel and type checking
are unaffected. When this attribute is used on a function, the function is not compiled and all
compiler-related attributes (e.g. `noncomputable`, `@[inline]`) are ignored. Calls to this
function are replaced by calls to its implementation.

The most common use cases of `@[implemented_by]` are to provide an efficient unsafe implementation
and to make an unsafe function accessible in safe code through an opaque function:

```
unsafe def testEqImpl (as bs : Array Nat) : Bool :=
  ptrEq as bs || as == bs

@[implemented_by testEqImpl]
def testEq (as bs : Array Nat) : Bool :=
  as == bs

unsafe def printAddrImpl {α : Type u} (x : α) : IO Unit :=
  IO.println s!"Address: {ptrAddrUnsafe x}"

@[implemented_by printAddrImpl]
opaque printAddr {α : Type u} (x : α) : IO Unit
```

The provided implementation is not checked to be equivalent to the original definition. This makes
it possible to prove `False` with `native_decide` using incorrect implementations. For a safer
variant of this attribute that however doesn't work for unsafe implementations, see `@[csimp]`,
which requires a proof that the two functions are equal.
 -/
Lean.Compiler.implementedByAttr : Lean.ParametricAttribute Lean.Name
-- Mathlib.Order.Atoms
/-- An upper-modular lattice that is atomistic is strongly atomic.
Not an instance to prevent loops.  -/
Lattice.isStronglyAtomic : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : OrderBot α] [IsUpperModularLattice α] [IsAtomistic α], IsStronglyAtomic α
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_union_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.Iio a ∪ Set.Ioi a = {a}ᶜ
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.coreMonoidalTransport_μIso_inv : ∀ {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 D]
  {F G : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (i : F ≅ G) (X Y : C),
  ((CategoryTheory.Functor.Monoidal.coreMonoidalTransport i).μIso X Y).inv =
    CategoryTheory.CategoryStruct.comp (i.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (i.hom.app X) (i.hom.app Y)))
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiffOn_of_subsingleton : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F}
  {n : WithTop ℕ∞} [Subsingleton F], ContDiffOn 𝕜 n f s
-- Mathlib.Order.SuccPred.Basic
/-- Proof of basic ordering with respect to `pred`  -/
PredOrder.pred_le : ∀ {α : Type u_3} {inst : Preorder α} [self : PredOrder α] (a : α), PredOrder.pred a ≤ a
-- Mathlib.GroupTheory.GroupAction.Iwasawa
MulAction.IwasawaStructure.mk.inj : ∀ {M : Type u_1} {inst : Group M} {α : Type u_2} {inst_1 : MulAction M α} {T : α → Subgroup M}
  {is_comm : ∀ (x : α), IsMulCommutative ↥(T x)} {is_conj : ∀ (g : M) (x : α), T (g • x) = MulAut.conj g • T x}
  {is_generator : iSup T = ⊤} {T_1 : α → Subgroup M} {is_comm_1 : ∀ (x : α), IsMulCommutative ↥(T_1 x)}
  {is_conj_1 : ∀ (g : M) (x : α), T_1 (g • x) = MulAut.conj g • T_1 x} {is_generator_1 : iSup T_1 = ⊤},
  { T := T, is_comm := is_comm, is_conj := is_conj, is_generator := is_generator } =
      { T := T_1, is_comm := is_comm_1, is_conj := is_conj_1, is_generator := is_generator_1 } →
    T = T_1
-- Mathlib.RingTheory.PrincipalIdealDomain
EuclideanDomain.to_principal_ideal_domain : ∀ {R : Type u} [inst : EuclideanDomain R], IsPrincipalIdealRing R
-- Mathlib.FieldTheory.Finite.GaloisField
/-- A finite field with `p ^ n` elements.
Every field with the same cardinality is (non-canonically)
isomorphic to this field.  -/
GaloisField : (p : ℕ) → [Fact (Nat.Prime p)] → ℕ → Type
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.Hom.fAddMonoidHom_apply : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c} (i : ι) (f : C₁ ⟶ C₂),
  (HomologicalComplex.Hom.fAddMonoidHom i) f = f.f i
-- Mathlib.RingTheory.Congruence.Hom
RingCon.Quotient.hom_extₐ_iff : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] {c : RingCon M} {f g : c.Quotient →ₐ[R] P},
  f = g ↔ f.comp (RingCon.mkₐ R c) = g.comp (RingCon.mkₐ R c)
-- Mathlib.Algebra.Prime.Lemmas
not_prime_pow : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {a : M} {n : ℕ}, n ≠ 1 → ¬Prime (a ^ n)
-- Mathlib.Data.Nat.Basic
Nat.pow_right_injective : ∀ {a : ℕ}, 2 ≤ a → Function.Injective fun x => a ^ x
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.isLocalizing_iff_of_iso : ∀ {R : CommRingCat} {M N : TopCat.Sheaf (ModuleCat ↑R) ↑(AlgebraicGeometry.Spec R).toPresheafedSpace} (φ : M ≅ N),
  AlgebraicGeometry.IsLocalizing M ↔ AlgebraicGeometry.IsLocalizing N
-- Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Polynomial.IsDistinguishedAt.mk : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} {I : Ideal R},
  f.IsWeaklyEisensteinAt I → f.Monic → f.IsDistinguishedAt I
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIic_surjOn : ∀ {α : Type u_1} [inst : LinearOrder α] {b : α}, Set.SurjOn (Set.projIic b) (Set.Iic b) Set.univ
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {p : ENNReal} (f : ↥(MeasureTheory.Lp E p μ)),
  p ≠ 0 →
    p ≠ ⊤ →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑f) s μ) →
        (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0) → ↑↑f =ᵐ[μ] 0
-- Init.Data.Float.Model.Float
/-- Converts a `UInt16` to a `Float.Model`, returning positive zero on zero.  -/
Float.Model.ofUInt16 : UInt16 → Float.Model
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.height_eq_sum : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  [inst_5 : CharZero R] {i : ι} {f : ι → ℤ},
  P.root i = ∑ j ∈ b.support, f j • P.root j → b.height i = ∑ j ∈ b.support, f j
-- Mathlib.Lean.Expr.Basic
/-- Find the largest prefix `n` of a `Name` such that `f n != none`, then replace this prefix
with the value of `f n`.  -/
Lean.Name.mapPrefix : (Lean.Name → Option Lean.Name) → Lean.Name → Lean.Name
-- Mathlib.Algebra.Lie.Subalgebra
/-- The Lie subalgebra of a Lie algebra `L` generated by a subset `s ⊆ L`.  -/
LieSubalgebra.lieSpan : (R : Type u) →
  (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Set L → LieSubalgebra R L
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.contains_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α] {k : α},
  m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.contains k = m₂.contains k
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] {a b : α},
  a ≤ b → ¬IsMax b → insert (Order.succ b) (Finset.Ioc a b) = Finset.Ioc a (Order.succ b)
-- Mathlib.Order.BoundedOrder.Basic
not_bot_lt_iff : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, ¬⊥ < a ↔ a = ⊥
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.order_ne_zero_iff_constCoeff_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R},
  f.order ≠ 0 ↔ MvPowerSeries.constantCoeff f = 0
-- Init.Data.Vector.InsertIdx
Vector.insertIdx_eraseIdx : ∀ {α : Type u} {a : α} {n i j : ℕ} {as : Vector α n} (h₁ : i < n) (h₂ : j ≤ n - 1),
  (as.eraseIdx i h₁).insertIdx j a h₂ =
    if h : i ≤ j then Vector.cast ⋯ ((as.insertIdx (j + 1) a ⋯).eraseIdx i ⋯)
    else Vector.cast ⋯ ((as.insertIdx j a ⋯).eraseIdx (i + 1) ⋯)
-- Mathlib.RingTheory.Smooth.Kaehler
/-- Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`,
and a section `g : S →ₐ[R] P` (as an algebra homomorphism),
we get an `R`-derivation `P → I` via `x ↦ x - g (f x)`.
 -/
derivationOfSectionOfKerSqZero : {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 R S] →
                (f : P →ₐ[R] S) →
                  RingHom.ker f ^ 2 = ⊥ → (g : S →ₐ[R] P) → f.comp g = AlgHom.id R S → Derivation R P ↥(RingHom.ker f)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- Proof that `g(p) = H(1 ⟶ 1, p)`, with the appropriate casts  -/
ContinuousMap.Homotopy.apply_one_path : ∀ {X Y : TopCat} {f g : C(↑X, ↑Y)} (H : f.Homotopy g) {x₀ x₁ : ↑X}
  (p : FundamentalGroupoid.fromTop x₀ ⟶ FundamentalGroupoid.fromTop x₁),
  (FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom g)).map p =
    CategoryTheory.CategoryStruct.comp (ContinuousMap.Homotopy.hcast ⋯)
      (CategoryTheory.CategoryStruct.comp
        ((FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom H.uliftMap)).map
          (ContinuousMap.Homotopy.prodToProdTopI
            (CategoryTheory.CategoryStruct.id (FundamentalGroupoid.fromTop { down := 1 })) p))
        (ContinuousMap.Homotopy.hcast ⋯))
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.containsThenInsert_fst : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.containsThenInsert k).1 = t.contains k
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_eq : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (μ : MeasureTheory.Measure α) (f : α → E), ⨍ (x : α), f x ∂μ = (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffWithinAt.smulRight : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x : E} {n : WithTop ℕ∞}
  {f : E → StrongDual 𝕜 F} {g : E → G},
  ContDiffWithinAt 𝕜 n f s x →
    ContDiffWithinAt 𝕜 n g s x → ContDiffWithinAt 𝕜 n (fun x => ContinuousLinearMap.smulRight (f x) (g x)) s x
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.monotone_extensionProduct_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C} (Q : CategoryTheory.ObjectProperty C) {P' : CategoryTheory.ObjectProperty C},
  P ≤ P' → P.extensionProduct Q ≤ P'.extensionProduct Q
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.fun_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ],
  ProbabilityTheory.HasSubgaussianMGF (fun x => 0) 0 μ
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def
ProbabilityTheory.IsGaussianProcess.mk : ∀ {Ω : Type u_1} {E : Type u_2} {T : Type u_3} {mΩ : MeasurableSpace Ω} [inst : MeasurableSpace E]
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommMonoid E] [inst_3 : Module ℝ E] {X : T → Ω → E}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsGaussianProcess._auto_1},
  (∀ (I : Finset T), ProbabilityTheory.HasGaussianLaw (fun ω => I.restrict fun x => X x ω) P) →
    ProbabilityTheory.IsGaussianProcess X P
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.comp₂_iso_hom_assoc : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} {x y z : a ⟶ b}
  {f : x ⟶ y} {g : y ⟶ z} {Z : a.as ⟶ b.as} (h : z.of ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).iso.hom h =
    CategoryTheory.CategoryStruct.comp f.iso.hom (CategoryTheory.CategoryStruct.comp g.iso.hom h)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_hom_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.op =
    (CategoryTheory.MonoidalCategoryStruct.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).inv
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.iff_of_isPullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {A X Y Z : C}
  {fst : A ⟶ X} {snd : A ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} [P.IsStableUnderBaseChange] [P.DescendsAlong Q],
  CategoryTheory.IsPullback fst snd f g → Q f → (P fst ↔ P g)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- A functor between based categories is a functor between the underlying categories that commutes
with the projections.  -/
CategoryTheory.BasedFunctor : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    CategoryTheory.BasedCategory 𝒮 → CategoryTheory.BasedCategory 𝒮 → Type (max (max (max u₂ u₃) v₂) v₃)
-- Lean.Compiler.InlineAttrs
Lean.Compiler.InlineAttributeKind.inline.sizeOf_spec : sizeOf Lean.Compiler.InlineAttributeKind.inline = 1
-- Mathlib.NumberTheory.LSeries.Convergence
LSeries.abscissaOfAbsConv_congr : ∀ {f g : ℕ → ℂ}, (∀ {n : ℕ}, n ≠ 0 → f n = g n) → LSeries.abscissaOfAbsConv f = LSeries.abscissaOfAbsConv g
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flippingEquiv_apply_map_app : ∀ {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 (CategoryTheory.Functor D E)) {X Y : D} (f : X ⟶ Y) (j : C),
  ((CategoryTheory.Functor.flippingEquiv F).map f).app j = (F.obj j).map f
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.allCombinations : {α : Type u_1} → Array (Array α) → Option (Array (Array α))
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.natTrans_app : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor ((i : I) × C i) D}
  (h : (i : I) → (CategoryTheory.Sigma.incl i).comp F ⟶ (CategoryTheory.Sigma.incl i).comp G) (i : I) (X : C i),
  (CategoryTheory.Sigma.natTrans h).app ⟨i, X⟩ = (h i).app X
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on `ℝ`, and `f''` is strictly positive on `ℝ`,
then `f` is strictly convex on `ℝ`.
Note that we don't require twice differentiability explicitly as it is already implied by the second
derivative being strictly positive, except at at most one point.  -/
strictConvexOn_univ_of_deriv2_pos : ∀ {f : ℝ → ℝ}, Continuous f → (∀ (x : ℝ), 0 < deriv^[2] f x) → StrictConvexOn ℝ Set.univ f
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.support_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f g : Equiv.Perm α},
  f.Disjoint g → (f * g).support = f.support ∪ g.support
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrixₛₗ₂'.eq_1 : ∀ (R : Type u_1) {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11}
  {m : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring R₁]
  [inst_4 : Semiring R₂] [inst_5 : Semiring S₁] [inst_6 : Semiring S₂] [inst_7 : Module S₁ N₂] [inst_8 : Module S₂ N₂]
  [inst_9 : SMulCommClass S₁ R N₂] [inst_10 : SMulCommClass S₂ R N₂] [inst_11 : SMulCommClass S₂ S₁ N₂] {σ₁ : R₁ →+* S₁}
  {σ₂ : R₂ →+* S₂} [inst_12 : Fintype n] [inst_13 : Fintype m] [inst_14 : DecidableEq n] [inst_15 : DecidableEq m],
  LinearMap.toMatrixₛₗ₂' R =
    { toFun := ⇑(LinearMap.toMatrix₂Aux R (fun i => Pi.single i 1) fun j => Pi.single j 1), map_add' := ⋯,
      map_smul' := ⋯, invFun := Matrix.toLinearMap₂'Aux σ₁ σ₂, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Int.LemmasAux
Int.toNat_le : ∀ {m : ℤ} {n : ℕ}, m.toNat ≤ n ↔ m ≤ ↑n
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.coe_toEquiv : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y), ⇑h.toEquiv = ⇑h
-- Mathlib.Algebra.Order.Ring.Cone
/-- Construct a partially ordered ring by designating a cone in a ring.  -/
IsOrderedRing.mkOfCone : ∀ {S : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : SetLike S R] (C : S) [inst_2 : RingConeClass S R],
  IsOrderedRing R
-- Lean.Elab.Do.Legacy
/-- Syntax to reference the result of the monadic computation performed by the do notation.  -/
Lean.Elab.Term.Do.ToTerm.Context.returnType : Lean.Elab.Term.Do.ToTerm.Context → Lean.Syntax
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_toUInt16 : ∀ (n : USize) (h : System.Platform.numBits = 64), n.toUInt16.toBitVec = BitVec.setWidth 16 (n.toBitVec64 h)
-- Mathlib.Order.Filter.Cofinite
/-- **Alias** of the reverse direction of `Filter.cofinite_inf_principal_neBot_iff`. -/
Set.Infinite.cofinite_inf_principal_neBot : ∀ {α : Type u_2} {s : Set α}, s.Infinite → (Filter.cofinite ⊓ Filter.principal s).NeBot
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.eval_soln : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2),
  (Polynomial.aeval (soln_gen✝ hnorm)) F = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) {Z_1 : C} (h_1 : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.IsLimit.lift ht h k w)
      (CategoryTheory.CategoryStruct.comp t.snd h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.Data.PNat.Interval
PNat.map_subtype_embedding_uIcc : ∀ (a b : ℕ+), Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.uIcc a b) = Finset.uIcc ↑a ↑b
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.le_add_lt : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α] {a b : α}, a ≤ 0 → b < 0 → a + b < 0
-- Mathlib.Util.Notation3
/-- Like `Expr.isType`, but uses logic that normalizes the universe level.
Mirrors the core `Sort` delaborator logic.
 -/
Mathlib.Notation3.isType' : Lean.Expr → Bool