mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- The canonical finitely-supported approximations to an element `f` of `lp` converge to it, in the
`lp` topology.  -/
lp.hasSum_single : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α]
  [inst_2 : Fact (1 ≤ p)], p ≠ ⊤ → ∀ (f : ↥(lp E p)), HasSum (fun i => lp.single p i (↑f i)) f
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The underlying `AddHom`.  -/
AddMagmaCat.Hom.hom' : {A B : AddMagmaCat} → A.Hom B → ↑A →ₙ+ ↑B
-- Mathlib.Topology.ContinuousMap.LocallyConstant
/-- The inclusion of locally-constant functions into continuous functions as a linear map.  -/
LocallyConstant.toContinuousMapLinearMap : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (R : Type u_3) →
          [inst_2 : Semiring R] →
            [inst_3 : AddCommMonoid Y] →
              [inst_4 : Module R Y] →
                [inst_5 : ContinuousAdd Y] → [inst_6 : ContinuousConstSMul R Y] → LocallyConstant X Y →ₗ[R] C(X, Y)
-- Init.System.CancelToken
_private.Init.System.CancelToken.0.IO.CancelToken.mk.inj : ∀ {promise : IO.Promise Unit} {setRef : IO.Ref Bool} {promise_1 : IO.Promise Unit} {setRef_1 : IO.Ref Bool},
  { promise := promise, setRef := setRef } = { promise := promise_1, setRef := setRef_1 } →
    promise = promise_1 ∧ setRef = setRef_1
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.precomp_map_left : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor C' C)
  {X Y :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)}
  (φ : X ⟶ Y),
  ((CategoryTheory.Functor.LeftExtension.precomp L F G).map φ).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_singletonAddHom : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α], ⇑Finset.singletonAddHom = singleton
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
/-- Convergence in probability (`TendstoInMeasure`) implies convergence in distribution
(`TendstoInDistribution`).  -/
MeasureTheory.TendstoInMeasure.tendstoInDistribution : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'}
  [inst : MeasureTheory.IsProbabilityMeasure μ'] {mE : MeasurableSpace E} {Z : Ω' → E} {l : Filter ι}
  [inst_1 : PseudoEMetricSpace E] [inst_2 : BorelSpace E] [l.IsCountablyGenerated] [l.NeBot] {X : ι → Ω' → E},
  MeasureTheory.TendstoInMeasure μ' X l Z →
    (∀ (i : ι), AEMeasurable (X i) μ') → MeasureTheory.TendstoInDistribution X l Z (fun x => μ') μ'
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.SameKeys.keys_eq : ∀ {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Std.DTreeMap.Internal.Impl α β}
  {t' : Std.DTreeMap.Internal.Impl α β'},
  t.SameKeys t' → List.map (fun x => x.fst) t.toListModel = List.map (fun x => x.fst) t'.toListModel
-- Init.Data.String.Lemmas.Basic
String.Slice.endPos.eq_1 : ∀ (s : String.Slice), s.endPos = { offset := s.rawEndPos, isValidForSlice := ⋯ }
-- Mathlib.Order.Restriction
Preorder.frestrictLe_updateFinset : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] [inst_2 : DecidableEq α]
  {a : α} (x : (a : α) → π a) (y : (b : ↥(Finset.Iic a)) → π ↑b),
  Preorder.frestrictLe a (Function.updateFinset x (Finset.Iic a) y) = y
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt32.reduceLE : Lean.Meta.Simp.Simproc
-- Mathlib.ModelTheory.Bundled
/-- An equivalence of types as a first-order equivalence to the bundled structure on the codomain.
 -/
Equiv.bundledInducedEquiv : (L : FirstOrder.Language) →
  {M : Type w} → [inst : L.Structure M] → {N : Type w'} → (g : M ≃ N) → L.Equiv M ↑(Equiv.bundledInduced L g)
-- Lean.Attributes
Lean.Attribute.add : Lean.Name → Lean.Name → Lean.Syntax → optParam Lean.AttributeKind Lean.AttributeKind.global → Lean.AttrM Unit
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.aux.sizeOf_spec : sizeOf Turing.PartrecToTM2.K'.aux = 1
-- Mathlib.Tactic.Simps.Basic
/-- Derive lemmas specifying the projections of the declaration.
`nm`: name of the lemma
If `todo` is non-empty, it will generate exactly the names in `todo`.
`toApply` is non-empty after a custom projection that is a composition of multiple projections
was just used. In that case we need to apply these projections before we continue changing `lhs`.
`simpLemmas`: names of the simp lemmas added so far.(simpLemmas : Array Name)
 -/
_private.Mathlib.Tactic.Simps.Basic.0.Simps.addProjections : Lean.Syntax →
  List Lean.Name →
    NameStruct✝ →
      Lean.Expr →
        Lean.Expr →
          Lean.Expr →
            Array Lean.Expr → Bool → Simps.Config → List (String × Lean.Syntax) → List ℕ → Lean.MetaM (Array Lean.Name)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_inr_image : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β},
  MeasurableSet (Sum.inr '' s) ↔ MeasurableSet s
-- Mathlib.Algebra.Category.CommBialgCat
CommAlgCat.one_op_of_unop_hom : ∀ {R : Type u} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : Bialgebra R A],
  CommAlgCat.Hom.hom CategoryTheory.MonObj.one.unop = Bialgebra.counitAlgHom R A
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.IsUnifLocDoublingMeasure.volume_prod : ∀ {X : Type u_4} {Y : Type u_5} [inst : PseudoMetricSpace X] [inst_1 : MeasureTheory.MeasureSpace X]
  [inst_2 : PseudoMetricSpace Y] [inst_3 : MeasureTheory.MeasureSpace Y] [MeasureTheory.SFinite MeasureTheory.volume]
  [IsUnifLocDoublingMeasure MeasureTheory.volume] [IsUnifLocDoublingMeasure MeasureTheory.volume],
  IsUnifLocDoublingMeasure MeasureTheory.volume
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.eq_bot_of_card_eq : ∀ {M : Type u_1} [inst : Monoid M] {S : Submonoid M} [inst_1 : Fintype ↥S], Fintype.card ↥S = 1 → S = ⊥
-- Mathlib.Order.Lattice
inf_left_le_sup_left : ∀ {α : Type u} [inst : Lattice α] {a b c : α}, a ⊓ b ≤ c ⊔ b
-- Init.Data.Array.Lemmas
Array.foldl_filter : ∀ {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : β → α → β} {xs : Array α} {init : β},
  Array.foldl f init (Array.filter p xs) = Array.foldl (fun x y => if p y = true then f x y else x) init xs
-- Batteries.Data.Fin.Coding
Fin.decodeChar.eq_1 : ∀ (i : Fin Char.count),
  Fin.decodeChar i =
    if x : ↑i < Char.minSurrogate then Char.ofNatAux ↑i ⋯
    else Char.ofNatAux (↑i + (Char.maxSurrogate + 1 - Char.minSurrogate)) ⋯
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
/-- The algebra isomorphism `AdjoinRoot (minpoly R x) ≃ₐ[R] adjoin R x`  -/
minpoly.equivAdjoin : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [IsDomain R] →
          [inst_3 : Algebra R S] →
            [IsIntegrallyClosed R] →
              [IsDomain S] →
                [Module.IsTorsionFree R S] → {x : S} → IsIntegral R x → AdjoinRoot (minpoly R x) ≃ₐ[R] ↥R[x]
-- Std.Time.DateTime.PlainDateTime
/-- Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.atDate : Std.Time.PlainTime → Std.Time.PlainDate → Std.Time.PlainDateTime
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_sum : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] (S₁ : AddSubgroup G₁)
  (S₂ : AddSubgroup G₂) (n : ℕ),
  (S₁.prod S₂).lowerCentralSeries n = (S₁.lowerCentralSeries n).prod (S₂.lowerCentralSeries n)
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.WithGeneratedByTopology.continuous_from_iff : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {Z : Type v'} [inst_1 : TopologicalSpace Z] (g : Topology.WithGeneratedByTopology X Y → Z),
  Continuous g ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous (g ∘ ⇑Topology.WithGeneratedByTopology.equiv.symm ∘ ⇑f)
-- Mathlib.RingTheory.Nilpotent.Lemmas
Matrix.isNilpotent_toLin'_iff : ∀ {R : Type u_1} {ι : Type u_3} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommSemiring R]
  (A : Matrix ι ι R), IsNilpotent (Matrix.toLin' A) ↔ IsNilpotent A
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.instIsCancelMulZero : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] [NoZeroDivisors R],
  IsCancelMulZero ↑(Set.Icc 0 1)
-- Lean.Data.Json.Basic
Lean.Json.brecOn_3.go : {motive_1 : Lean.Json → Sort u} →
  {motive_2 : Array Lean.Json → Sort u} →
    {motive_3 : Std.TreeMap.Raw String Lean.Json compare → Sort u} →
      {motive_4 : List Lean.Json → Sort u} →
        {motive_5 : Std.DTreeMap.Raw String (fun x => Lean.Json) compare → Sort u} →
          {motive_6 : (Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Sort u} →
            (t : List Lean.Json) →
              ((t : Lean.Json) → t.below → motive_1 t) →
                ((t : Array Lean.Json) → Lean.Json.below_1 t → motive_2 t) →
                  ((t : Std.TreeMap.Raw String Lean.Json compare) → Lean.Json.below_2 t → motive_3 t) →
                    ((t : List Lean.Json) → Lean.Json.below_3 t → motive_4 t) →
                      ((t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) → Lean.Json.below_4 t → motive_5 t) →
                        ((t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) →
                            Lean.Json.below_5 t → motive_6 t) →
                          motive_4 t ×' Lean.Json.below_3 t
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- The map ground assigning a function `M → N` to a polynomial map `f : M →ₚₗ[R] N` as a
linear map.  -/
PolynomialLaw.lground : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → (M →ₚₗ[R] N) →ₗ[R] M → N
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux2 : {α : Type u} → List (Computation α) → α ⊕ List (Computation α)
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.mul_swap_of_ne : ∀ {R : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Semiring R] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  {i j b : n} {a : m}, b ≠ i → b ≠ j → ∀ (g : Matrix m n R), (g * Matrix.swap R i j) a b = g a b
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonTextDocumentIdentifier : Lean.FromJson Lean.Lsp.TextDocumentIdentifier
-- Mathlib.Data.Vector.Snoc
/-- Define `C v w` by *reverse* induction on a pair of vectors `v : Vector α n` and
`w : Vector β n`.  -/
List.Vector.revInductionOn₂ : {α : Type u_1} →
  {β : Type u_2} →
    {C : {n : ℕ} → List.Vector α n → List.Vector β n → Sort u_5} →
      {n : ℕ} →
        (v : List.Vector α n) →
          (w : List.Vector β n) →
            C List.Vector.nil List.Vector.nil →
              ({n : ℕ} →
                  (xs : List.Vector α n) →
                    (ys : List.Vector β n) → (x : α) → (y : β) → C xs ys → C (xs.snoc x) (ys.snoc y)) →
                C v w
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
mulRightReflectLT_of_mulRightMono : ∀ (N : Type u_2) [inst : Mul N] [inst_1 : LinearOrder N] [MulRightMono N], MulRightReflectLT N
-- Mathlib.NumberTheory.Padics.PadicNumbers
instDivPadic : (p : ℕ) → [inst : Fact (Nat.Prime p)] → Div ℚ_[p]
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- If all the elements of a set `s` commute, then `closure s` is a non-unital commutative
ring.  -/
NonUnitalSubring.closureNonUnitalCommRingOfComm : {R : Type u_1} →
  [inst : NonUnitalRing R] →
    {s : Set R} → (∀ x ∈ s, ∀ y ∈ s, x * y = y * x) → NonUnitalCommRing ↥(NonUnitalSubring.closure s)
-- Mathlib.CategoryTheory.Localization.StructuredArrow
CategoryTheory.Localization.structuredArrowEquiv_symm_apply : ∀ {C : Type u_1} {D : Type u_2} {D' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} D']
  (W : CategoryTheory.MorphismProperty C) (L : CategoryTheory.Functor C D) (L' : CategoryTheory.Functor C D')
  [inst_3 : L.IsLocalization W] [inst_4 : L'.IsLocalization W] {X : C}
  (f : CategoryTheory.StructuredArrow (L'.obj X) L'),
  (CategoryTheory.Localization.structuredArrowEquiv W L L').symm f =
    CategoryTheory.StructuredArrow.mk ((CategoryTheory.Localization.homEquiv W L' L) f.hom)
-- Mathlib.Analysis.Normed.Order.Hom.Basic
GroupSeminormClass.toSeminormedCommGroup_norm_eq : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : CommGroup α] [inst_2 : GroupSeminormClass F α ℝ]
  (f : F) (x : α), ‖x‖ = f x
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'),
  T = T' →
    ∀ (f : ↥(α →₁ₛ[μ] E)),
      (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.biUnion_coe_eq_coe : ∀ {ι : Type u_1} (I : WithBot (BoxIntegral.Box ι)), ⋃ J, ⋃ (_ : ↑J = I), ↑J = ↑I
-- Mathlib.Geometry.Manifold.Submersion
/-- `f : M → N` is a `C^n` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
around `x` and `f x`, respectively such that in these charts, `f` looks like `(u, v) ↦ u`.
This version does not assume that `f` maps `φ.source` to `ψ.source`,
but that `f` is continuous at `x`.  -/
Manifold.IsSubmersionAt.mk_of_continuousAt : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M},
  ContinuousAt f x →
    ∀ (equiv : E ≃L[𝕜] E'' × F) (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G),
      x ∈ domChart.source →
        f x ∈ codChart.source →
          domChart ∈ IsManifold.maximalAtlas I n M →
            codChart ∈ IsManifold.maximalAtlas J n N →
              Set.EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (Prod.fst ∘ ⇑equiv)
                  (domChart.extend I).target →
                Manifold.IsSubmersionAt I J n f x
-- Mathlib.Order.Max
Subsingleton.isTop : ∀ {α : Type u_1} [inst : Preorder α] [Subsingleton α] (a : α), IsTop a
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors.eq_1 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  (a : α), UniqueFactorizationMonoid.normalizedFactors a = Multiset.map normalize (UniqueFactorizationMonoid.factors a)
-- Mathlib.Analysis.SpecialFunctions.Bernstein
/-- Extension of the `positivity` tactic for Bernstein polynomials: they are always non-negative.  -/
Mathlib.Meta.Positivity.evalBernstein : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.one : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j : J),
  RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.of j 1) RingCat.Colimits.Prequotient.one
-- Mathlib.RingTheory.Multiplicity
multiplicity_lt_of_emultiplicity_lt : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {n : ℕ}, emultiplicity a b < ↑n → multiplicity a b < n
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enrichedId_π : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₁] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedId V F₁)
      (CategoryTheory.Limits.end_.π (CategoryTheory.Enriched.FunctorCategory.diagram V F₁ F₁) j) =
    CategoryTheory.eId V (F₁.obj j)
-- Init.Data.List.MapIdx
List.exists_of_mem_mapIdx : ∀ {β : Type u_1} {α : Type u_2} {f : ℕ → α → β} {b : β} {l : List α},
  b ∈ List.mapIdx f l → ∃ i, ∃ (h : i < l.length), f i l[i] = b
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isRamified_iff : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K},
  NumberField.InfinitePlace.IsRamified k w ↔ w.IsComplex ∧ (w.comap (algebraMap k K)).IsReal
-- Init.Data.UInt.Lemmas
UInt8.toNat_ofNat_of_lt : ∀ {n : ℕ}, n < UInt8.size → UInt8.toNat (OfNat.ofNat n) = n
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.isNat_not_prime : ∀ {n n' : ℕ}, Mathlib.Meta.NormNum.IsNat n n' → ¬Nat.Prime n' → ¬Nat.Prime n
-- Lean.Meta.Tactic.Try.Collect
/-- All constant symbols occurring in the gal.  -/
Lean.Meta.Try.Collector.Result.allConsts : Lean.Meta.Try.Collector.Result → Lean.Meta.Try.Collector.OrdSet Lean.Name
-- Init.Data.Int.Order
Int.pos_of_mul_pos_left : ∀ {a b : ℤ}, 0 < a * b → 0 < b → 0 < a
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.restrict_compl_singleton : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ] (a : α),
  μ.restrict {a}ᶜ = μ
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.ofFunction_eq_sSup : ∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0},
  MeasureTheory.OuterMeasure.ofFunction m m_empty = sSup {μ | ∀ (s : Set α), μ s ≤ m s}
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minEntry?.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k : α) →
                (v : β k) →
                  (r : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r)) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (size_1 : ℕ) →
                      (k_1 : α) →
                        (v_1 : β k_1) →
                          (l r r_1 : Std.DTreeMap.Internal.Impl α β) →
                            motive
                              (Std.DTreeMap.Internal.Impl.inner size k v
                                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)) →
              motive x
-- Mathlib.GroupTheory.Perm.Sign
_private.Mathlib.GroupTheory.Perm.Sign.0.Equiv.Perm.signAux_swap_zero_one' : ∀ (n : ℕ), (Equiv.swap 0 1).signAux = -1
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R],
  CanLift (Set R) (NonUnitalSubring R) SetLike.coe fun s =>
    0 ∈ s ∧
      (∀ {x y : R}, x ∈ s → y ∈ s → x + y ∈ s) ∧ (∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x : R}, x ∈ s → -x ∈ s
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- If `L/K`, `ψ : K →+* ℂ`, and `φ : L →+* ℂ`, then `φ` lies over `ψ` if the restriction of
`φ` to `K` is `ψ`.  -/
NumberField.ComplexEmbedding.LiesOver : {K : Type u_3} → {L : Type u_4} → [inst : Field K] → [inst_1 : Field L] → [Algebra K L] → (L →+* ℂ) → (K →+* ℂ) → Prop
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- `WithLp.equiv` as a homeomorphism.  -/
PiLp.homeomorph : (p : ENNReal) →
  {ι : Type u_2} → (β : ι → Type u_4) → [inst : (i : ι) → TopologicalSpace (β i)] → PiLp p β ≃ₜ ((i : ι) → β i)
-- Mathlib.Data.Matrix.Basic
Matrix.scalar_apply : ∀ {n : Type u_3} {α : Type u_11} [inst : Semiring α] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (a : α),
  (Matrix.scalar n) a = Matrix.diagonal fun x => a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], Array.map Sigma.fst (↑m).toArray = (↑m).keysArray
-- Mathlib.Order.BooleanAlgebra.Basic
hnot_eq_compl : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α], ￢x = xᶜ
-- Mathlib.LinearAlgebra.Matrix.Orthogonal
/-- `Aᵀ` has orthogonal rows iff `A` has orthogonal columns.  -/
Matrix.transpose_hasOrthogonalRows_iff_hasOrthogonalCols : ∀ {α : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Mul α] [inst_1 : AddCommMonoid α] (A : Matrix m n α)
  [inst_2 : Fintype m], A.transpose.HasOrthogonalRows ↔ A.HasOrthogonalCols
-- Lean.MetavarContext
Lean.exprDependsOn : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.Expr → Lean.FVarId → m Bool
-- Init.Data.SInt.Bitwise
Int64.toBitVec_or : ∀ (a b : Int64), (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.basisProd_castAdd : ∀ {R : Type u_1} [inst : Semiring R] (m n : ℕ) (i : Fin m),
  (Polynomial.degreeLT.basisProd R m n) (Fin.castAdd n i) = ((Polynomial.degreeLT.basis R m) i, 0)
-- Mathlib.Data.Finset.Sort
Finset.orderEmbOfFin.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k),
  s.orderEmbOfFin h = RelEmbedding.trans (s.orderIsoOfFin h).toOrderEmbedding (OrderEmbedding.subtype fun x => x ∈ s)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` reflects colimits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits.  -/
CategoryTheory.Limits.reflectsLimitsOfSize_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_ofNatLT : ∀ {n : ℕ} (hn : n < UInt64.size), (UInt64.ofNatLT n hn).toUInt8 = UInt8.ofNat n
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.refl_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {P : C(X, Y) → Prop} (f : C(X, Y))
  (hf : P f) (x : ↑unitInterval × X), (ContinuousMap.HomotopyWith.refl f hf) x = f x.2
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPoly.beq.eq_2 : ∀ (a : ℤ) (a_1 : Lean.Grind.CommRing.Mon) (a_2 : Lean.Grind.CommRing.Poly) (b : ℤ) (b_1 : Lean.Grind.CommRing.Mon)
  (b_2 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.instBEqPoly.beq (Lean.Grind.CommRing.Poly.add a a_1 a_2)
      (Lean.Grind.CommRing.Poly.add b b_1 b_2) =
    (a == b && (a_1 == b_1 && Lean.Grind.CommRing.instBEqPoly.beq a_2 b_2))
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `⊓` distributes over `⨆`.  -/
inf_sSup_eq : ∀ {α : Type u} [inst : Order.Frame α] {s : Set α} {a : α}, a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instNonUnitalRing : {R : Type u_1} → [NonUnitalRing R] → NonUnitalRing Rᵒᵈ
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.ofNat_eq_zero_iff : ∀ {α : Type u_1} (p : ℕ) [inst : Lean.Grind.Semiring α] [Lean.Grind.IsCharP α p] (x : ℕ), OfNat.ofNat x = 0 ↔ x % p = 0