mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- A pointwise left Kan extension is universal, i.e. it is a left Kan extension.  -/
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isUniversal : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                {E : L.LeftExtension F} → E.IsPointwiseLeftKanExtension → CategoryTheory.StructuredArrow.IsUniversal E
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
IsUnramifiedAtInfinitePlaces.isUnramified : ∀ {k : Type u_1} {inst : Field k} {K : Type u_2} {inst_1 : Field K} {inst_2 : Algebra k K}
  [self : IsUnramifiedAtInfinitePlaces k K] (w : NumberField.InfinitePlace K),
  NumberField.InfinitePlace.IsUnramified k w
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.of_iUnion_nonpos : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Countable β] {f : β → Set α} {M : Type u_4}
  [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M] [IsOrderedAddMonoid M]
  [OrderClosedTopology M] {v : MeasureTheory.VectorMeasure α M},
  (∀ (i : β), MeasurableSet (f i)) → Pairwise (Function.onFun Disjoint f) → (∀ (i : β), v (f i) ≤ 0) → v (⋃ i, f i) ≤ 0
-- Mathlib.Tactic.Ring.Basic
/-- Constructs the expression corresponding to `.const q h` for `q = -(n / d)`
and `h` a proof that `(d : α) ≠ 0`.
(The `.const` constructor does not check that the expression is correct.)
 -/
Mathlib.Tactic.Ring.ExProd.mkNegNNRat : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      Q(DivisionRing «$α») → ℚ → Q(ℕ) → Q(ℕ) → Lean.Expr → (e : Q(«$α»)) × Mathlib.Tactic.Ring.ExProd sα e
-- Mathlib.Analysis.Complex.RealDeriv
DifferentiableWithinAt.real_of_complex : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {s : Set ℂ} {z : ℂ},
  DifferentiableWithinAt ℂ f s z → DifferentiableWithinAt ℝ f s z
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.isoOfEq_rfl : ∀ (X : AlgebraicGeometry.Scheme) (U : X.Opens), X.isoOfEq ⋯ = CategoryTheory.Iso.refl ↑U
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
/-- Through the equivalence `(AugmentedSimplexCategory ⥤ C) ≌ CosimplicialObject.Augmented C`,
taking the point of the augmentation corresponds to evaluation at the initial object.  -/
AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompPointIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    AugmentedSimplexCategory.equivAugmentedSimplicialObject.functor.comp
        CategoryTheory.SimplicialObject.Augmented.point ≅
      (CategoryTheory.evaluation AugmentedSimplexCategoryᵒᵖ C).obj (Opposite.op CategoryTheory.WithInitial.star)
-- Mathlib.Combinatorics.HalesJewett
/-- The proposition that the underlying line of an almost monochromatic line assumes its main
color except possibly at the endpoints.  -/
Combinatorics.Line.AlmostMono.has_color : ∀ {α : Type u_5} {ι : Type u_6} {κ : Type u_7} {C : (ι → Option α) → κ} (self : Combinatorics.Line.AlmostMono C)
  (x : α), C (↑self.line (some x)) = self.color
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f g : FrameHom α β},
  f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_fst_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y : C},
  CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Algebra.BigOperators.Pi
eqOn_fun_finsetProd : ∀ {ι : Type u_8} {α : Type u_9} {β : Type u_10} [inst : CommMonoid α] {s : Set β} {f f' : ι → β → α},
  (∀ (i : ι), Set.EqOn (f i) (f' i) s) →
    ∀ (v : Finset ι), Set.EqOn (fun b => ∏ i ∈ v, f i b) (fun b => ∏ i ∈ v, f' i b) s
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version within a set at a point, but with full pullback.  -/
ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} [CompleteSpace E] [inst_12 : IsManifold I 1 M]
  [inst_13 : IsManifold I' 1 M'],
  ContMDiffWithinAt I' I'.tangent m (fun x => ⟨x, V x⟩) t (f x₀) →
    ContMDiffAt I I' n f x₀ →
      (mfderiv% f x₀).IsInvertible →
        m + 1 ≤ n →
          f ⁻¹' t ∈ nhdsWithin x₀ s →
            ContMDiffWithinAt I I.tangent m (fun x => ⟨x, VectorField.mpullback I I' f V x⟩) s x₀
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- A sub-ideal `J` of a divided power ideal `(I, hI)` is a sub-dp-ideal if for all `n > 0` and
all `x ∈ J`, `hI.dpow n j ∈ J`.  -/
DividedPowers.IsSubDPIdeal : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → DividedPowers I → Ideal A → Prop
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.mk_eq : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f g : CauSeq β abv},
  CauSeq.Completion.mk f = CauSeq.Completion.mk g ↔ (f - g).LimZero
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAtFilter.isBigO_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L → (fun p => f p.1 - f p.2) =O[L] fun p => p.1 - p.2
-- Mathlib.Data.Setoid.Partition
/-- The quotient associated to an indexed partition.  -/
IndexedPartition.Quotient : {ι : Type u_1} → {α : Type u_2} → {s : ι → Set α} → IndexedPartition s → Type u_2
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMap₂_apply : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] [inst_7 : Fintype n] [inst_8 : Fintype m]
  [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂)
  (M : Matrix n m N₂) (x : M₁) (y : M₂),
  (((Matrix.toLinearMap₂ b₁ b₂) M) x) y = ∑ i, ∑ j, (b₁.repr x) i • (b₂.repr y) j • M i j
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.exact : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β},
  Std.ExtDHashMap.mk m₁ = Std.ExtDHashMap.mk m₂ → m₁.Equiv m₂
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.toAddSubmonoid : {G : Type u_1} → [inst : AddCommGroup G] → AddGroupCone G → AddSubmonoid G
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.coe_unop : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup Gᵐᵒᵖ), ↑H.unop = MulOpposite.op ⁻¹' ↑H
-- Mathlib.Algebra.Ring.Prod
/-- Given non-unital semirings `R`, `S`, the natural projection homomorphism from `R × S` to `S`.  -/
NonUnitalRingHom.snd : (R : Type u_1) →
  (S : Type u_3) → [inst : NonUnitalNonAssocSemiring R] → [inst_1 : NonUnitalNonAssocSemiring S] → R × S →ₙ+* S
-- Mathlib.Data.Set.Image
/-- The range of a function from a `Unique` type contains just the
function applied to its single value.  -/
Set.range_unique : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} [inst : Unique ι], Set.range f = {f default}
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeSemigroup.range_toFreeMonoid : ∀ {α : Type u_1}, Set.range ⇑FreeSemigroup.toFreeMonoid = {1}ᶜ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β},
  m.WF →
    Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.Const.modify m k f) k' =
      if (k == k') = true then Option.map f (Std.DHashMap.Raw.Const.get? m k) else Std.DHashMap.Raw.Const.get? m k'
-- Mathlib.CategoryTheory.EssentiallySmall
/-- An essentially small category is equivalent to some small category.  -/
CategoryTheory.EssentiallySmall.equiv_smallCategory : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.EssentiallySmall.{w, v, u} C],
  ∃ S x, Nonempty (C ≌ S)
-- Mathlib.Algebra.Module.Projective
/-- A module which satisfies the universal property is projective.  -/
Module.Projective.of_lifting_property' : ∀ {R : Type u} [inst : Semiring R] {P : Type v} [inst_1 : AddCommMonoid P] [inst_2 : Module R P] [Small.{v, u} R],
  (∀ {M N : Type v} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : Module R M] [inst_7 : Module R N]
      (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g) →
    Module.Projective R P
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H1CoresCoinf_f : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  (groupHomology.H1CoresCoinf A S).f =
    groupHomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype A)) 1
-- Mathlib.Topology.Separation.Hausdorff
lim_nhdsWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {x : X} {s : Set X}, x ∈ closure s → (nhdsWithin x s).lim = x
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddMonoid (f i)],
  Pi.addMonoid =
    { toAddSemigroup := Pi.addSemigroup, toZero := Pi.addZeroClass.toZero, zero_add := ⋯, add_zero := ⋯,
      nsmul := fun n x i => n • x i, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] [inst_3 : (k : α) → BEq (β k)] [∀ (k : α), ReflBEq (β k)],
  m₁.WF → m₂.WF → m₁.Equiv m₂ → (m₁ == m₂) = true
-- Mathlib.RingTheory.Localization.Integer
/-- A choice of a common multiple of the denominators of a `Finset`-indexed family of fractions.  -/
IsLocalization.commonDenom : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      {S : Type u_2} →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] → [IsLocalization M S] → {ι : Type u_4} → Finset ι → (ι → S) → ↥M
-- Init.MethodSpecsSimp
ShiftLeft.shiftLeft_hShiftLeft : ∀ {α : Type u_1} [inst : ShiftLeft α], ShiftLeft.shiftLeft = HShiftLeft.hShiftLeft
-- Lean.AuxRecursor
Lean.instInhabitedNoConfusionInfo : Inhabited Lean.NoConfusionInfo
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_prod : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] (S : NonUnitalSubalgebra R A) [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B]
  (S₁ : NonUnitalSubalgebra R B), ↑(S.prod S₁) = ↑S ×ˢ ↑S₁
-- Mathlib.Data.Set.Basic
Set.not_subset : ∀ {α : Type u} {s t : Set α}, ¬s ⊆ t ↔ ∃ a ∈ s, a ∉ t
-- Mathlib.Topology.ContinuousOn
ContinuousOn.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] {f : α → γ} {g : β → δ} {s : Set α} {t : Set β},
  ContinuousOn f s → ContinuousOn g t → ContinuousOn (Prod.map f g) (s ×ˢ t)
-- Std.Time.Zoned.Database.TzIf
/-- Indicates if this local time type observes daylight saving time.
 -/
Std.Time.TimeZone.TZif.LocalTimeType.isDst : Std.Time.TimeZone.TZif.LocalTimeType → Bool
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X₁ X₂ X₃ X₄ : C} {f₁₂ : X₁ ⟶ X₂} {f₁₃ : X₁ ⟶ X₃}
  {f₂₄ : X₂ ⟶ X₄} {f₃₄ : X₃ ⟶ X₄}
  {fac : CategoryTheory.CategoryStruct.comp f₁₂ f₂₄ = CategoryTheory.CategoryStruct.comp f₁₃ f₃₄}
  {X₁_1 X₂_1 X₃_1 X₄_1 : C} {f₁₂_1 : X₁_1 ⟶ X₂_1} {f₁₃_1 : X₁_1 ⟶ X₃_1} {f₂₄_1 : X₂_1 ⟶ X₄_1} {f₃₄_1 : X₃_1 ⟶ X₄_1}
  {fac_1 : CategoryTheory.CategoryStruct.comp f₁₂_1 f₂₄_1 = CategoryTheory.CategoryStruct.comp f₁₃_1 f₃₄_1},
  { X₁ := X₁, X₂ := X₂, X₃ := X₃, X₄ := X₄, f₁₂ := f₁₂, f₁₃ := f₁₃, f₂₄ := f₂₄, f₃₄ := f₃₄, fac := fac } =
      { X₁ := X₁_1, X₂ := X₂_1, X₃ := X₃_1, X₄ := X₄_1, f₁₂ := f₁₂_1, f₁₃ := f₁₃_1, f₂₄ := f₂₄_1, f₃₄ := f₃₄_1,
        fac := fac_1 } →
    X₁ = X₁_1 ∧ X₂ = X₂_1 ∧ X₃ = X₃_1 ∧ X₄ = X₄_1 ∧ f₁₂ ≍ f₁₂_1 ∧ f₁₃ ≍ f₁₃_1 ∧ f₂₄ ≍ f₂₄_1 ∧ f₃₄ ≍ f₃₄_1
-- Mathlib.Probability.StrongLaw
/-- If a function is integrable, then the integral of its truncated versions converges to the
integral of the whole function.  -/
ProbabilityTheory.tendsto_integral_truncation : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ →
    Filter.Tendsto (fun A => ∫ (x : α), ProbabilityTheory.truncation f A x ∂μ) Filter.atTop (nhds (∫ (x : α), f x ∂μ))
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- An intermediate field of `E / F` is contained in the relative perfect closure of `F` in `E`
if it is purely inseparable over `F`.  -/
le_perfectClosure : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E)
  [h : IsPurelyInseparable F ↥L], L ≤ perfectClosure F E
-- Mathlib.RingTheory.PowerSeries.Catalan
/-- The Catalan generating function as a power series.  -/
PowerSeries.catalanSeries : PowerSeries ℕ
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- A function is continuously differentiable up to order `n` within a set `s` at a point `x` if
it admits continuous derivatives up to order `n` in a neighborhood of `x` in `s ∪ {x}`.
The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
number, `∞`, or `ω`.
For `n = ∞`, we only require that this holds up to any finite order (where the neighborhood may
depend on the finite order we consider).
For `n = ω`, we require the function to be analytic within `s` at `x`. The precise definition we
give (all the derivatives should be analytic) is more involved to work around issues when the space
is not complete, but it is equivalent when the space is complete.

For instance, a real function which is `C^m` on `(-1/m, 1/m)` for each natural `m`, but not
better, is `C^∞` at `0` within `univ`.
 -/
ContDiffWithinAt : (𝕜 : Type u) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type uE} →
      [inst_1 : NormedAddCommGroup E] →
        [NormedSpace 𝕜 E] →
          {F : Type uF} → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → WithTop ℕ∞ → (E → F) → Set E → E → Prop
-- Init.Data.Slice.Array.Lemmas
Array.stop_mkSlice_roo : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, (Std.Roo.Sliceable.mkSlice xs lo<...hi).stop = min hi xs.size
-- Mathlib.Control.Functor
/-- `Const.mk'` is `Const.mk` but specialized to map `α` to
`Const α PUnit`, where `PUnit` is the terminal object in `Type*`.  -/
Functor.Const.mk' : {α : Type u_1} → α → Functor.Const α PUnit.{u_2 + 1}
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_map_toList : ∀ {ι : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] (s : Multiset ι) (f : ι → M),
  (List.map f s.toList).sum = (Multiset.map f s).sum
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNeg : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddGroup β] → [IsTopologicalAddGroup β] → Neg (ZeroAtInftyContinuousMap α β)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
IsOpen.contDiffOn_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞}, IsOpen s → (ContDiffOn 𝕜 n f s ↔ ∀ ⦃a : E⦄, a ∈ s → ContDiffAt 𝕜 n f a)
-- Mathlib.Analysis.Seminorm
Seminorm.instZero : {𝕜 : Type u_3} →
  {E : Type u_7} → [inst : SeminormedRing 𝕜] → [inst_1 : AddGroup E] → [inst_2 : SMul 𝕜 E] → Zero (Seminorm 𝕜 E)
-- Mathlib.Order.Category.PartOrd
_private.Mathlib.Order.Category.PartOrd.0.PartOrd.Hom.mk : {X Y : PartOrd} → (↑X →o ↑Y) → X.Hom Y
-- Mathlib.LinearAlgebra.Complex.Module
selfAdjoint.submodule.congr_simp : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A],
  selfAdjoint.submodule R A = selfAdjoint.submodule R A
-- Mathlib.Data.Fintype.Quotient
List.Pi.tail.congr_simp : ∀ {ι : Type u_1} {α : ι → Sort u_2} {i : ι} {l : List ι} (f f_1 : (j : ι) → j ∈ i :: l → α j),
  f = f_1 → ∀ (j : ι) (a : j ∈ l), List.Pi.tail f j a = List.Pi.tail f_1 j a
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_bot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D), ⊥.inverseImage F = ⊥
-- Mathlib.Algebra.Lie.Basic
LieHom.instCoeLinearMapId : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieAlgebra R L₁] →
            [inst_3 : LieRing L₂] → [inst_4 : LieAlgebra R L₂] → Coe (L₁ →ₗ⁅R⁆ L₂) (L₁ →ₗ[R] L₂)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.map_map : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} {N : Type u_10} {P : Type u_11}
  [inst_2 : IsStrictOrderedRing R] (f : Convexity.StdSimplex R M) (g₁ : M → N) (g₂ : N → P),
  Convexity.StdSimplex.map g₂ (Convexity.StdSimplex.map g₁ f) = Convexity.StdSimplex.map (fun x => g₂ (g₁ x)) f
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.le_induce_top_verts : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph}, G' ≤ ⊤.induce G'.verts
-- Mathlib.Data.Finsupp.Single
Finsupp.nontrivial_iff : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M], Nontrivial (α →₀ M) ↔ Nonempty α ∧ Nontrivial M
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_div_sub : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
  c ≠ 0 → ∀ (d : ℝ), ∫ (x : ℝ) in a..b, f (x / c - d) = c • ∫ (x : ℝ) in a / c - d..b / c - d, f x
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
_private.Mathlib.Topology.Algebra.InfiniteSum.NatInt.0.cond.match_1.splitter : (motive : Bool → Sort u_1) → (c : Bool) → (Unit → motive true) → (Unit → motive false) → motive c
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.comap_comap : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {N : Type u_2} [inst_2 : AddGroup N]
  [inst_3 : TopologicalSpace N] {P : Type u_3} [inst_4 : AddGroup P] [inst_5 : TopologicalSpace P]
  (K : OpenAddSubgroup P) (f₂ : N →+ P) (hf₂ : Continuous ⇑f₂) (f₁ : G →+ N) (hf₁ : Continuous ⇑f₁),
  OpenAddSubgroup.comap f₁ hf₁ (OpenAddSubgroup.comap f₂ hf₂ K) = OpenAddSubgroup.comap (f₂.comp f₁) ⋯ K
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- To show a category is an `InitialMonoClass` it suffices to show the unique morphism from an
initial object to a terminal object is a monomorphism.  -/
CategoryTheory.Limits.InitialMonoClass.of_isTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I T : C} (hI : CategoryTheory.Limits.IsInitial I)
  (hT : CategoryTheory.Limits.IsTerminal T), CategoryTheory.Mono (hI.to T) → CategoryTheory.Limits.InitialMonoClass C
-- Mathlib.Order.LatticeIntervals
Set.Icc.coe_inf : ∀ {α : Type u_1} {a b : α} [inst : SemilatticeInf α] {x y : ↑(Set.Icc a b)}, ↑(x ⊓ y) = ↑x ⊓ ↑y
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instLocallyCompactSpace : ∀ {M : Type u_1} [inst : TopologicalSpace M] [LocallyCompactSpace M], LocallyCompactSpace Mᵈᵐᵃ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.mkIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : CategoryTheory.Grp C} (e e_1 : G.X ≅ H.X) (e_e : e = e_1)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
        CategoryTheory.MonObj.mul),
  CategoryTheory.Grp.mkIso e one_f mul_f = CategoryTheory.Grp.mkIso e_1 ⋯ ⋯
-- Mathlib.Order.CompleteLattice.Basic
biSup_prod' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ},
  ⨆ x ∈ s ×ˢ t, f x.1 x.2 = ⨆ a ∈ s, ⨆ b ∈ t, f a b
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.map_id_comp_H0Iso_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (groupHomology.map (MonoidHom.id G) f 0) (groupHomology.H0Iso B).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.H0Iso A).hom ((Rep.coinvariantsFunctor k G).map f)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.ext : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {f g : X →ₑ[φ] Y}, (∀ (x : X), f x = g x) → f = g
-- Init.Data.Slice.Array.Lemmas
Array.start_mkSlice_rii : ∀ {α : Type u_1} {xs : Array α}, (Std.Rii.Sliceable.mkSlice xs *...*).start = 0
-- Mathlib.Logic.Equiv.Sum
Equiv.sumCompl_symm_apply_of_neg : ∀ {α : Type u_9} {p : α → Prop} [inst : DecidablePred p] {a : α} (h : ¬p a), (Equiv.sumCompl p).symm a = Sum.inr ⟨a, h⟩
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Given a family of points, if we use a member of the family as a base point, the
`weightedVSubOfPoint` does not depend on the value of the weights at this point.  -/
Finset.weightedVSubOfPoint_eq_of_weights_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P) (j : ι) (w₁ w₂ : ι → k),
  (∀ (i : ι), i ≠ j → w₁ i = w₂ i) → (s.weightedVSubOfPoint p (p j)) w₁ = (s.weightedVSubOfPoint p (p j)) w₂
-- Mathlib.Computability.Partrec
Nat.Partrec.of_eq_tot : ∀ {f : ℕ →. ℕ} {g : ℕ → ℕ}, Nat.Partrec f → (∀ (n : ℕ), g n ∈ f n) → Nat.Partrec ↑g
-- Mathlib.Algebra.Group.Equiv.Defs
/-- The identity equivalence between the additive monoid of endomorphisms
`AddMonoid.End M` and the type `M →+ M` of additive monoid homomorphisms from `M` to itself.
`AddMonoid.End M` is definitionally (but not reducibly) equal to `M →+ M`.  -/
AddMonoid.End.equiv : (M : Type u_9) → [inst : AddZero M] → AddMonoid.End M ≃ (M →+ M)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
NonUnitalIsometricContinuousFunctionalCalculus.isometric : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst : CommSemiring R} {inst_1 : Nontrivial R}
  {inst_2 : StarRing R} {inst_3 : MetricSpace R} {inst_4 : IsTopologicalSemiring R} {inst_5 : ContinuousStar R}
  {inst_6 : NonUnitalRing A} {inst_7 : StarRing A} {inst_8 : MetricSpace A} {inst_9 : Module R A}
  {inst_10 : IsScalarTower R A A} {inst_11 : SMulCommClass R A A}
  [self : NonUnitalIsometricContinuousFunctionalCalculus R A p] (a : A) (ha : p a), Isometry ⇑(cfcₙHom ha)