mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.enorm_comm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  (x : TensorProduct 𝕜 E F), ‖(TensorProduct.comm 𝕜 E F) x‖ₑ = ‖x‖ₑ
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.instIsStableUnderRetractsUnopOfOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty Cᵒᵖ)
  [P.IsStableUnderRetracts], P.unop.IsStableUnderRetracts
-- Mathlib.LinearAlgebra.Ray
/-- Any invertible action preserves the non-zeroness of rays. This is primarily of interest when
`G = Rˣ`  -/
instMulActionRay : {R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} →
          [inst_3 : AddCommMonoid M] →
            [inst_4 : Module R M] →
              {G : Type u_5} →
                [inst_5 : Group G] →
                  [inst_6 : DistribMulAction G M] → [SMulCommClass R G M] → MulAction G (Module.Ray R M)
-- Mathlib.RingTheory.Ideal.Over
Ideal.under_top : ∀ (A : Type u_2) [inst : CommSemiring A] (B : Type u_3) [inst_1 : Semiring B] [inst_2 : Algebra A B],
  Ideal.under A ⊤ = ⊤
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.haarScalarFactor_self : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ : MeasureTheory.Measure G) [inst_5 : μ.IsHaarMeasure],
  μ.haarScalarFactor μ = 1
-- Lean.Message
Lean.SerialMessage.mk.injEq : ∀ (toBaseMessage : Lean.BaseMessage String) (kind : Lean.Name) (toBaseMessage_1 : Lean.BaseMessage String)
  (kind_1 : Lean.Name),
  ({ toBaseMessage := toBaseMessage, kind := kind } = { toBaseMessage := toBaseMessage_1, kind := kind_1 }) =
    (toBaseMessage = toBaseMessage_1 ∧ kind = kind_1)
-- Mathlib.Order.WellFounded
WellFounded.asymm : ∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r → Std.Asymm r
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.zero : CategoryTheory.Limits.WalkingReflexivePair
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
EuclideanGeometry.angle.eq_1 : ∀ {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),
  EuclideanGeometry.angle p₁ p₂ p₃ = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
-- Mathlib.Algebra.Homology.CochainComplexOpposite
ComplexShape.embeddingDownIntUpInt_f : ∀ (n : ℤ), ComplexShape.embeddingDownIntUpInt.f n = -n
-- Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Complex.tan_arctan : ∀ {z : ℂ}, z ≠ Complex.I → z ≠ -Complex.I → Complex.tan z.arctan = z
-- Mathlib.Data.Sym.Sym2
Sym2.lift_smul_lift : ∀ {α : Type u_4} {R : Type u_5} {N : Type u_6} [inst : SMul R N] (f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ })
  (g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }), Sym2.lift f • Sym2.lift g = Sym2.lift ⟨↑f • ↑g, ⋯⟩
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.toSphere_apply_univ' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E], μ.toSphere Set.univ = ↑(Module.finrank ℝ E) * μ (Metric.ball 0 1 \ {0})
-- Init.Data.Array.Lemmas
Array.forall_mem_ne : ∀ {α : Type u_1} {a : α} {xs : Array α}, (∀ a' ∈ xs, ¬a = a') ↔ a ∉ xs
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C (Type w)}
  {x y : CategoryTheory.Subfunctor F}, x.obj = y.obj → x = y
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.toType_noMax_of_succ_lt : ∀ {o : Ordinal.{u_4}}, (∀ a < o, Order.succ a < o) → NoMaxOrder o.ToType
-- Mathlib.Data.Subtype
Subtype.coe_eta : ∀ {α : Sort u_1} {p : α → Prop} (a : { a // p a }) (h : p ↑a), ⟨↑a, h⟩ = a
-- Lean.MonadEnv
Lean.isInductive? : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Option Lean.InductiveVal)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.op_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂), ψ.op.right = ψ.left.op
-- Lean.Syntax
Lean.Syntax.hasMissing : Lean.Syntax → Bool
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.ext_iff : ∀ {d : ℤ} {a b : Pell.Solution₁ d}, a = b ↔ a.x = b.x ∧ a.y = b.y
-- Lean.Elab.Util
/-- Registers a macro expander for a given syntax node kind.

A macro expander should have type `Lean.Macro` (which is `Lean.Syntax → Lean.MacroM Lean.Syntax`),
i.e. should take syntax of the given syntax node kind as a parameter and produce different syntax
in the same syntax category.

The `macro_rules` and `macro` commands should usually be preferred over using this attribute
directly.
 -/
Lean.Elab.macroAttribute : Lean.KeyedDeclsAttribute Lean.Macro
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- The property of preserving products expressed in terms of fans.  -/
CategoryTheory.Limits.isLimitFanMkObjOfIsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            (f : J → C) →
              [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] →
                {P : C} →
                  (g : (j : J) → P ⟶ f j) →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk P g) →
                      CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (G.obj P) fun j => G.map (g j))
-- Init.Data.UInt.Lemmas
UInt64.ofNat_toNat : ∀ {x : UInt64}, UInt64.ofNat x.toNat = x
-- Mathlib.Algebra.Lie.Prod
LieHom.snd_prod : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L : Type u_4} [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : LieRing L]
  [inst_6 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L₁) (g : L →ₗ⁅R⁆ L₂), (LieHom.snd R L₁ L₂).comp (f.prod g) = g
-- Mathlib.Data.Countable.Basic
instCountableProd : ∀ {α : Type u} {β : Type v} [Countable α] [Countable β], Countable (α × β)
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, panicking if no such key exists.
 -/
Std.TreeMap.Raw.getKeyLE! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap.Raw α β cmp → α → α
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.pow_inertiaDeg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R] [Module.Finite ℤ R]
  (p : ℕ) (P : Ideal R) [P.IsPrime] [P.LiesOver (Ideal.span {↑p})], p ^ P.inertiaDeg ℤ = Ideal.absNorm P
-- Init.Grind.AC
Lean.Grind.AC.instBEqExpr.beq : Lean.Grind.AC.Expr → Lean.Grind.AC.Expr → Bool
-- Mathlib.RingTheory.LocalProperties.Submodule
Module.eq_zero_of_localization_maximal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_5 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (m : M),
  (∀ (P : Ideal R) [inst_6 : P.IsMaximal], (f P) m = 0) → m = 0
-- Mathlib.Analysis.Fourier.Notation
FourierAdd.mk : ∀ {E : Type u_5} {F : outParam (Type u_6)} [inst : Add E] [inst_1 : Add F] [inst_2 : FourierTransform E F],
  (∀ (f g : E), FourierTransform.fourier (f + g) = FourierTransform.fourier f + FourierTransform.fourier g) →
    FourierAdd E F
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.IsComplete.realize_sentence_iff : ∀ {L : FirstOrder.Language} {T : L.Theory},
  T.IsComplete → ∀ (φ : L.Sentence) (M : Type u_1) [inst : L.Structure M] [M ⊨ T] [Nonempty M], M ⊨ φ ↔ T ⊨ᵇ φ
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.mkReturn : Lean.Elab.Do.ControlStack → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Combinatorics.Graph.Basic
Graph.bouquet_empty : ∀ {α : Type u_1} {β : Type u_2} (v : α), Graph.bouquet v ∅ = Graph.noEdge {v} β
-- Init.Control.Lawful.Instances
ExceptT.mk.eq_1 : ∀ {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)), ExceptT.mk x = x
-- Mathlib.Order.CompleteLattice.SetLike
Sublattice.setLike_mem_inf : ∀ {X : Type u_1} {L : Sublattice (Set X)} {S T : ↥L} {x : X}, x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
-- Mathlib.Topology.DiscreteSubset
/-- **Alias** of `Filter.codiscreteWithin_mono`.

---

If a set is codiscrete within `U`, then it is codiscrete within any subset of `U`.  -/
Filter.codiscreteWithin.mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U₁ U : Set X},
  U₁ ⊆ U → Filter.codiscreteWithin U₁ ≤ Filter.codiscreteWithin U
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutions.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V] {D : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} D]
  [inst_5 : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] (d d' : D),
  CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutions C V d d' =
    {
      convolution :=
        (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).obj
          (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObj C V d d'),
      unit :=
        {
          app := fun x =>
            CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutionUnitApp V d
              d' x.1 x.2,
          naturality := ⋯ },
      isPointwiseLeftKanExtensionUnit :=
        (CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionEquivOfIso
            (CategoryTheory.StructuredArrow.isoMk
              (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObjIsoConvolution
                  C V d d').symm
              ⋯))
          (CategoryTheory.MonoidalCategory.DayConvolution.isPointwiseLeftKanExtensionUnit
            ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).obj d)
            ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).obj d')) }
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).i =
    CategoryTheory.CategoryStruct.id S.X₂
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.SparseCasesOnKey.mk : Lean.Name → Array Lean.Name → Bool → Lean.Meta.SparseCasesOnKey✝
-- Std.Async.Process
/-- Gets the current process parent id.
 -/
Std.IO.Process.getParentId : IO Std.IO.Process.PId
-- Mathlib.Data.Finset.Sups
Finset.biUnion_image_inf_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] (s t : Finset α),
  (t.biUnion fun b => Finset.image (fun x => x ⊓ b) s) = s ⊼ t
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.le_nthRoot_iff : ∀ {n a b : ℕ}, n ≠ 0 → (a ≤ n.nthRoot b ↔ a ^ n ≤ b)
-- Init.Data.Nat.Lemmas
Nat.one_le_of_lt : ∀ {a b : ℕ}, a < b → 1 ≤ b
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.add.sizeOf_spec : ∀ {R : Type u_1} {X : Type u_2} [inst : SizeOf R] [inst_1 : SizeOf X] (a a_1 : FreeAlgebra.Pre R X),
  sizeOf (a.add a_1) = 1 + sizeOf a + sizeOf a_1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.var.sizeOf_spec : ∀ (i : Lean.Grind.CommRing.Var), sizeOf (Lean.Grind.CommRing.Expr.var i) = 1 + sizeOf i
-- Mathlib.Topology.UniformSpace.Real
ContinuousMap.coeNNRealReal_apply : ⇑ContinuousMap.coeNNRealReal = NNReal.toReal
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.del.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → RBTree.RBColor → Sort u_2) (c : RBTree.RBColor)
  (a : RBTree.RBNode α) (y : α) (parent : RBTree.RBNode.Path α) (b : RBTree.RBNode α)
  (h_1 : (t : RBTree.RBNode α) → (x : RBTree.RBColor) → motive RBTree.RBNode.Path.root t x)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a RBTree.RBColor.red)
  (h_3 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) →
          (parent : RBTree.RBNode.Path α) →
            (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b RBTree.RBColor.red)
  (h_4 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a RBTree.RBColor.black)
  (h_5 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) →
          (parent : RBTree.RBNode.Path α) →
            (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b RBTree.RBColor.black),
  (match RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.red with
    | RBTree.RBNode.Path.root, t, x => h_1 t x
    | RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.red => h_2 c parent y b a
    | RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.red => h_3 c a y parent b
    | RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.black => h_4 c parent y b a
    | RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.black => h_5 c a y parent b) =
    h_3 c a y parent b
-- Init.Data.Nat.Gcd
Nat.gcd_mul_right_sub_right : ∀ {m n k : ℕ}, n ≤ k * m → m.gcd (k * m - n) = m.gcd n
-- Init.Data.Fin.Lemmas
Fin.ofNat_zero : ∀ (n : ℕ) [inst : NeZero n], Fin.ofNat n 0 = 0
-- Mathlib.Algebra.Algebra.Spectrum.Basic
AlgHom.apply_mem_spectrum : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [inst_3 : FunLike F A R] [AlgHomClass F R A R] [Nontrivial R] (φ : F) (a : A), φ a ∈ spectrum R a
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.eq_1 : ∀ {α : Type u_1} (rels : FreeMonoid α → FreeMonoid α → Prop), PresentedMonoid rels = (conGen rels).Quotient
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_algebraMap : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : CommSemiring K]
  [inst_2 : Semiring β] [inst_3 : Algebra K β] (k : K) (x : α),
  ((algebraMap K (MeasureTheory.SimpleFunc α β)) k) x = (algebraMap K (α → β)) k x
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.homMk_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {f f' : CategoryTheory.StructuredArrow S T} (φ : f ⟶ f'),
  ∃ ψ,
    ∃ (hψ : CategoryTheory.CategoryStruct.comp f.hom (T.map ψ) = f'.hom), φ = CategoryTheory.StructuredArrow.homMk ψ hψ
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.val_mem_ofAddUnits_iff_mem : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup (AddUnits G)) (x : AddUnits G), ↑x ∈ H.ofAddUnits ↔ x ∈ H
-- Mathlib.Order.Filter.Pointwise
Filter.vsub_neBot_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f g : Filter β}, (f -ᵥ g).NeBot ↔ f.NeBot ∧ g.NeBot
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.instLocallySmallHoCat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  [CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.LocallySmall.{w, v, u} (HomotopicalAlgebra.BifibrantObject.HoCat C)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- Let `x` be a nondegenerate `d`-simplex of `Δ[m + 1] ⊗ Δ[n]` which
does not belong to `Λ[m + 1, k.castSucc].unionProd ∂Δ[n]`. This is
the finite subset of `Fin (d + 1)` consisting of those `l` such
that `x l` is of the form `(k.succ, _)`.  -/
SSet.prodStdSimplex.pairingCore.finset : {m : ℕ} →
  {k : Fin (m + 1)} →
    {n : ℕ} →
      (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) → {d : ℕ} → x.dim = d → Finset (Fin (d + 1))
-- Mathlib.Data.Sign.Defs
/-- This can't be a `CoeTail` or `Coe` instance because we don't want it to fire when `SignType` isn't
involved in the coercion (or `CoeHead` or `CoeOut` because of `outParam`s). The only other
user-exposed option is `CoeDep` then, which allows us to match on both given and expected type.
 -/
SignType.instCoeDep : {α : Type u_1} → [Zero α] → [One α] → [Neg α] → (s : SignType) → CoeDep SignType s α
-- Init.Data.Int.LemmasAux
Int.eq_natCast_toNat : ∀ {a : ℤ}, a = ↑a.toNat ↔ 0 ≤ a
-- Mathlib.Order.Heyting.Basic
/-- `p → q → r ↔ q → p → r`  -/
le_himp_comm : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b ⇨ c ↔ b ≤ a ⇨ c
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
sigNeg_neg : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommGroup M] [inst_1 : CommRing R] [inst_2 : LinearOrder R]
  [inst_3 : Module R M] {Q : QuadraticForm R M}, sigNeg (-Q) = sigPos Q
-- Mathlib.Order.Filter.Finite
Filter.frequently_exists : ∀ {α : Type u} {ι : Sort u_2} [Finite ι] {l : Filter α} {p : ι → α → Prop},
  (∃ᶠ (x : α) in l, ∃ i, p i x) ↔ ∃ i, ∃ᶠ (x : α) in l, p i x
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.uniformizingPolynomial_ne_zero : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [inst_2 : v.IsNontrivial] [inst_3 : Valuation.IsTrivialOn K v] (hle : v RatFunc.X ≤ 1),
  RatFunc.uniformizingPolynomial hle ≠ 0
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
aestronglyMeasurable_iff_nullMeasurable_separable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [BorelSpace β],
  MeasureTheory.AEStronglyMeasurable f μ ↔
    MeasureTheory.NullMeasurable f μ ∧ ∃ t, TopologicalSpace.IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
-- Init.Data.Slice.Array.Lemmas
Subarray.foldl_toList : ∀ {α : Type u_1} {init : α} {α_1 : Type u} {s : Subarray α_1} {f : α → α_1 → α},
  List.foldl f init (Std.Slice.toList s) = Std.Slice.foldl f init s
-- Mathlib.Order.UpperLower.Closure
coe_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α), ↑(lowerClosure s) = ⋃ a ∈ s, Set.Iic a
-- Lean.Elab.Command
Lean.Elab.Command.runLintersAsync : Lean.Syntax → Array Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.regularSpace_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], RegularSpace (TopologicalSpace.NonemptyCompacts α) ↔ RegularSpace α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_of_mul_lt_mul_left' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α] [MulLeftReflectLT α] {a b c : α}, a * b < a * c → b < c
-- Mathlib.Order.RelClasses
IsOrderConnected.neg_trans : ∀ {α : Type u} {r : α → α → Prop} [IsOrderConnected α r] {a b c : α}, ¬r a b → ¬r b c → ¬r a c
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.unifIntegrable_zero_meas : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : NormedAddCommGroup β] [inst_1 : MeasurableSpace α] {p : ENNReal}
  {f : ι → α → β}, MeasureTheory.UnifIntegrable f p 0
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsSemilinearSet.biUnion_finset : ∀ {M : Type u_1} {ι : Type u_3} [inst : AddCommMonoid M] {s : Finset ι} {t : ι → Set M},
  (∀ i ∈ s, IsSemilinearSet (t i)) → IsSemilinearSet (⋃ i ∈ s, t i)
-- Init.Data.String.Basic
String.Slice.Pos.ofSliceTo_startPos : ∀ {s : String.Slice} {pos : s.Pos}, String.Slice.Pos.ofSliceTo (s.sliceTo pos).startPos = s.startPos
-- Mathlib.Data.List.Defs
List.map₂Left'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (x : List β), List.map₂Left' f [] x = ([], x)
-- Init.Data.List.MinMaxIdx
List.get_minIdxOn?_eq_minIdxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α}
  (h : (List.minIdxOn? f xs).isSome = true), (List.minIdxOn? f xs).get h = List.minIdxOn f xs ⋯
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.instIsLieTowerSubtypeMem : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) {M : Type u_3} [inst_3 : AddCommGroup M] [inst_4 : LieRingModule L M],
  IsLieTower (↥L') L M
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- The `RelStruct f g i` deduced from an equality `f = g`.  -/
SSet.PtSimplex.RelStruct.ofEq : {X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} → {f g : X.PtSimplex n x} → f = g → (i : Fin (n + 1)) → f.RelStruct g i
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- Coalgebras of an endofunctor `F` form a category  -/
CategoryTheory.Endofunctor.Coalgebra.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C C) → CategoryTheory.Category.{v, max u v} (CategoryTheory.Endofunctor.Coalgebra F)
-- Mathlib.Algebra.Order.Field.Pointwise
LinearOrderedField.smul_Iio : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {a r : K},
  0 < r → r • Set.Iio a = Set.Iio (r * a)
-- Mathlib.Logic.Function.Basic
/-- Composition by an injective function on the left is itself injective.  -/
Function.Injective.comp_left : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : β → γ}, Function.Injective g → Function.Injective fun x => g ∘ x
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits, then `F : C ⥤ D` preserves limits.  -/
CategoryTheory.Limits.preservesLimits_of_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.PreservesColimits F.op],
  CategoryTheory.Limits.PreservesLimits F
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.preimage_coe_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some ⁻¹' Set.Ici ↑a = Set.Ici a
-- Mathlib.RingTheory.TensorProduct.Maps
LinearMap.tensorProductEnd_apply : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (a : TensorProduct R A (Module.End R M)),
  (LinearMap.tensorProductEnd R A M) a =
    (TensorProduct.liftAux
        (↑R { toFun := fun a => a • LinearMap.baseChangeHom R A M M, map_add' := ⋯, map_smul' := ⋯ }))
      a
-- Mathlib.CategoryTheory.Galois.Examples
/-- The `G`-action on a connected finite `G`-set is transitive.  -/
CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected : ∀ (G : Type u) [inst : Group G] (X : Action FintypeCat G) [CategoryTheory.PreGaloisCategory.IsConnected X],
  MulAction.IsPretransitive G X.V.obj