mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The second part of the third simplicial identity  -/
CategoryTheory.SimplicialObject.δ_comp_σ_succ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 1)} {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (X.δ i.succ) h) = h
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.insertPerm.match_1.eq_1 : ∀ (motive : (x : ℕ) → Fin2 x → Fin2 x → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (n + 1) Fin2.fz Fin2.fz)
  (h_2 : (n : ℕ) → (j : Fin2 n) → motive (n + 1) Fin2.fz j.fs)
  (h_3 : (a : ℕ) → (a_1 : Fin2 a.succ) → motive (a.succ + 1) a_1.fs Fin2.fz)
  (h_4 : (a : ℕ) → (i : Fin2 a.succ) → (j : Fin2 (a + 1)) → motive (a.succ + 1) i.fs j.fs),
  (match n + 1, Fin2.fz, Fin2.fz with
    | .(n + 1), Fin2.fz, Fin2.fz => h_1 n
    | .(n + 1), Fin2.fz, j.fs => h_2 n j
    | .(a.succ + 1), a_1.fs, Fin2.fz => h_3 a a_1
    | .(a.succ + 1), i.fs, j.fs => h_4 a i j) =
    h_1 n
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.maxView.congr_simp : ∀ {α : Type u} {β : α → Type v} (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced) (hr : r.Balanced)
      (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size),
      Std.DTreeMap.Internal.Impl.maxView k v l r hl hr hlr = Std.DTreeMap.Internal.Impl.maxView k v_1 l r hl hr hlr
-- Lean.CoreM
Lean.diagnostics.threshold : Lean.Option ℕ
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.EqnInfo.mk : Lean.Name →
  List Lean.Name →
    Lean.Expr → Lean.Expr → ℕ → Array Lean.Name → Lean.Elab.FixedParamPerms → Lean.Elab.Structural.EqnInfo
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instAssociativeMeet : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l], Std.Associative fun x1 x2 => Lean.Order.meet x1 x2
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₂ → (t₁ ∪ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Std.Time.Time.Unit.Hour
/-- Creates an `Ordinal` from a natural number, ensuring the value is within the valid bounds for hours.
 -/
Std.Time.Hour.Ordinal.ofNat : (data : ℕ) → data ≤ 23 → Std.Time.Hour.Ordinal
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.rightAdjointUniq_trans_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D}
  {G G' G'' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') (x : D),
  CategoryTheory.CategoryStruct.comp ((adj1.rightAdjointUniq adj2).hom.app x) ((adj2.rightAdjointUniq adj3).hom.app x) =
    (adj1.rightAdjointUniq adj3).hom.app x
-- Mathlib.FieldTheory.AbelRuffini
/-- **Alias** of `isIntegral_of_mem_solvableByRad`. -/
solvableByRad.isIntegral : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  x ∈ solvableByRad F E → IsIntegral F x
-- Lean.Meta.Tactic.Grind.AC.Util
_private.Lean.Meta.Tactic.Grind.AC.Util.0.Lean.Meta.Grind.AC.notAssoc : Std.HashSet Lean.Name
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.registerMatchEqns : Lean.Name → Lean.Meta.Match.MatchEqns → Lean.CoreM Unit
-- Init.Data.Vector.Attach
Vector.unattach_empty : ∀ {α : Type u_1} {p : α → Prop}, #v[].unattach = #v[]
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical_inf : ∀ {R : Type u} [inst : CommSemiring R] (I J : Ideal R), (I ⊓ J).radical = I.radical ⊓ J.radical
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.tendsto_nhds_iff : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜] {c : 𝕜},
  Filter.Tendsto (fun x => Polynomial.eval x P) Filter.atTop (nhds c) ↔ P.leadingCoeff = c ∧ P.degree ≤ 0
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePullbackShapeOpEquiv_functor : ∀ (J : Type w),
  (CategoryTheory.Limits.widePullbackShapeOpEquiv J).functor = CategoryTheory.Limits.widePullbackShapeUnop J
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoLeftHomology_hom_inv_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] (hf : S.f = 0) {Z : C} (h : S.cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.leftHomologyπ
      (CategoryTheory.CategoryStruct.comp (S.cyclesIsoLeftHomology hf).inv h) =
    h
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.one_mem_toNonUnitalSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  1 ∈ S.toNonUnitalSubalgebra
-- Mathlib.Algebra.Order.Field.Basic
div_nonpos_iff : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
ContinuousLinearMap.fderivWithin_of_bilinear : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {G' : Type u_5} [inst_7 : NormedAddCommGroup G']
  [inst_8 : NormedSpace 𝕜 G'] (B : E →L[𝕜] F →L[𝕜] G) {f : G' → E} {g : G' → F} {x : G'} {s : Set G'},
  DifferentiableWithinAt 𝕜 f s x →
    DifferentiableWithinAt 𝕜 g s x →
      UniqueDiffWithinAt 𝕜 s x →
        fderivWithin 𝕜 (fun y => (B (f y)) (g y)) s x =
          ((ContinuousLinearMap.precompR G' B) (f x)) (fderivWithin 𝕜 g s x) +
            ((ContinuousLinearMap.precompL G' B) (fderivWithin 𝕜 f s x)) (g x)
-- Mathlib.Algebra.Category.BialgCat.Monoidal
/-- `forget₂ (BialgCat R) (CoalgCat R)` as a monoidal functor.  -/
BialgCat.instMonoidalCoalgCatForget₂BialgHomCarrierCoalgHomCarrier : (R : Type u) → [inst : CommRing R] → (CategoryTheory.forget₂ (BialgCat R) (CoalgCat R)).Monoidal
-- Mathlib.Combinatorics.SetFamily.Intersecting
/-- A set family is intersecting if every pair of elements is non-disjoint.  -/
Set.Intersecting : {α : Type u_1} → [inst : SemilatticeInf α] → [OrderBot α] → Set α → Prop
-- Init.Grind.Norm
Lean.Grind.Int.sign_eq : ∀ (x : ℤ), x.sign = if x > 0 then 1 else if x < 0 then -1 else 0
-- Mathlib.Algebra.Torsor.Defs
vadd_right_cancel_iff : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {g₁ g₂ : G} (p : P), g₁ +ᵥ p = g₂ +ᵥ p ↔ g₁ = g₂
-- Mathlib.Order.Restriction
Preorder.restrictLe₂_comp_restrictLe₂ : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} {a b c : α} (hab : a ≤ b) (hbc : b ≤ c),
  Preorder.restrictLe₂ hab ∘ Preorder.restrictLe₂ hbc = Preorder.restrictLe₂ ⋯
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
/-- Relatively prime elements have disjoint prime factors (as multisets).  -/
UniqueFactorizationMonoid.disjoint_normalizedFactors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {a b : α},
  IsRelPrime a b →
    Disjoint (UniqueFactorizationMonoid.normalizedFactors a) (UniqueFactorizationMonoid.normalizedFactors b)
-- Lean.Util.ShareCommon
Lean.ShareCommon.PShareCommonT.monadShareCommon : {m : Type u_1 → Type u_2} → [Monad m] → MonadShareCommon (Lean.ShareCommon.PShareCommonT m)
-- Mathlib.Algebra.Module.Torsion.Basic
Module.IsTorsionBy.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  Module.IsTorsionBy R M a = ∀ ⦃x : M⦄, a • x = 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_inj : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r₁ r₂ : R} {m₁ m₂ : M},
  MonoidAlgebra.single m₁ r₁ = MonoidAlgebra.single m₂ r₂ ↔ m₁ = m₂ ∧ r₁ = r₂ ∨ r₁ = 0 ∧ r₂ = 0
-- Init.Data.Rat.Basic
instHashableRat.hash : ℚ → UInt64
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
/-- If two tangent lines to a sphere pass through the same point `q`,
then the distances from `q` to the tangent points are equal.  -/
EuclideanGeometry.Sphere.IsTangentAt.dist_eq_of_mem_of_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ q : P} {as₁ as₂ : AffineSubspace ℝ P},
  s.IsTangentAt p₁ as₁ → s.IsTangentAt p₂ as₂ → q ∈ as₁ → q ∈ as₂ → dist q p₁ = dist q p₂
-- Mathlib.Analysis.RCLike.Basic
RCLike.im_mul_ofReal : ∀ {K : Type u_1} [inst : RCLike K] (z : K) (r : ℝ), RCLike.im (z * ↑r) = RCLike.im z * r
-- Mathlib.Topology.ContinuousMap.Star
ContinuousMap.instStarRingOfContinuousStar : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalNonAssocSemiring β] →
          [inst_3 : IsTopologicalSemiring β] → [inst_4 : StarRing β] → [ContinuousStar β] → StarRing C(α, β)
-- Mathlib.Order.Filter.AtTopBot.Interval
Finset.tendsto_Ioo_neg_atTop_atTop : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : LocallyFiniteOrder α] [NoBotOrder α] [NoTopOrder α],
  Filter.Tendsto (fun a => Finset.Ioo (-a) a) Filter.atTop Filter.atTop
-- Lean.Server.GoTo
Lean.Server.GoToKind.type : Lean.Server.GoToKind
-- Init.Data.Array.Extract
Array.extract_set : ∀ {α : Type u_1} {as : Array α} {i j k : ℕ} (h : k < as.size) {a : α},
  (as.set k a h).extract i j =
    if x : k < i then as.extract i j
    else if x_1 : k < min j as.size then (as.extract i j).set (k - i) a ⋯ else as.extract i j
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.image_add_left_Icc : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] [inst_5 : DecidableEq α] (a b c : α),
  Finset.image (fun x => c + x) (Finset.Icc a b) = Finset.Icc (c + a) (c + b)
-- Mathlib.Algebra.Group.Defs
LeftCancelSemigroup.ext : ∀ {G : Type u} {x y : LeftCancelSemigroup G}, Mul.mul = Mul.mul → x = y
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.Context.mk.inj : ∀ {toInductiveVal : Lean.InductiveVal} {lparams : List Lean.Level} {params : Array Lean.Expr}
  {compFields : Array Lean.Name} {compFieldVars indices : Array Lean.Expr} {val : Lean.Expr}
  {toInductiveVal_1 : Lean.InductiveVal} {lparams_1 : List Lean.Level} {params_1 : Array Lean.Expr}
  {compFields_1 : Array Lean.Name} {compFieldVars_1 indices_1 : Array Lean.Expr} {val_1 : Lean.Expr},
  { toInductiveVal := toInductiveVal, lparams := lparams, params := params, compFields := compFields,
        compFieldVars := compFieldVars, indices := indices, val := val } =
      { toInductiveVal := toInductiveVal_1, lparams := lparams_1, params := params_1, compFields := compFields_1,
        compFieldVars := compFieldVars_1, indices := indices_1, val := val_1 } →
    toInductiveVal = toInductiveVal_1 ∧
      lparams = lparams_1 ∧
        params = params_1 ∧
          compFields = compFields_1 ∧ compFieldVars = compFieldVars_1 ∧ indices = indices_1 ∧ val = val_1
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.toList.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (tree : Std.DTreeMap.Internal.Impl α β)
  (next : Std.DTreeMap.Internal.Zipper α β),
  (Std.DTreeMap.Internal.Zipper.cons k v tree next).toList = ⟨k, v⟩ :: tree.toList ++ next.toList
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reduceOfList : Lean.Meta.Simp.DSimproc
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Var : Type
-- Init.Data.Int.DivMod.Lemmas
Int.lt_tmod_of_pos : ∀ (a : ℤ) {b : ℤ}, 0 < b → -b < a.tmod b
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- If `X : SSet`, this is the isomorphism of simplicial sets
from `⊤ : X.Subcomplex` to `X`.  -/
SSet.Subcomplex.topIso : (X : SSet) → ⊤.toSSet ≅ X
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.vadd_apply : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace W]
  [inst_10 : IsTopologicalAddGroup W] [inst_11 : IsTopologicalAddTorsor Q] (f : P →ᴬ[R] W) (g : P →ᴬ[R] Q) (p : P),
  (f +ᵥ g) p = f p +ᵥ g p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertMany!_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      compare k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
          k ∈ List.map Prod.fst l → (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).getKey? k' = some k
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toRing : {R : Type u_1} →
  {A : Type u_2} → [inst : CommRing R] → [inst_1 : Ring A] → [inst_2 : Algebra R A] → (S : Subalgebra R A) → Ring ↥S
-- Mathlib.Topology.Algebra.Ring.Basic
/-- The product topology on the Cartesian product of two semitopological rings
makes the product into a semitopological ring.  -/
instIsSemitopologicalRingProd : ∀ {R : Type u_1} {S : Type u_2} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace S]
  [inst_2 : NonUnitalNonAssocRing R] [inst_3 : NonUnitalNonAssocRing S] [IsSemitopologicalRing R]
  [IsSemitopologicalRing S], IsSemitopologicalRing (R × S)
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : LatticeHom α β) (hf : f.toFun ⊤ = ⊤) (hf' : f.toFun ⊥ = ⊥),
  ⇑{ toLatticeHom := f, map_top' := hf, map_bot' := hf' } = ⇑f
-- Mathlib.Data.FunLike.Equiv
EquivLike.comp_injective : ∀ {F : Sort u_2} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [inst : EquivLike F β γ] (f : α → β) (e : F),
  Function.Injective (⇑e ∘ f) ↔ Function.Injective f
-- Mathlib.Order.Closure
ClosureOperator.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SizeOf α] (toOrderHom : α →o α)
  (le_closure' : ∀ (x : α), x ≤ toOrderHom.toFun x)
  (idempotent' : ∀ (x : α), toOrderHom.toFun (toOrderHom.toFun x) = toOrderHom.toFun x) (IsClosed : α → Prop)
  (isClosed_iff : autoParam (∀ {x : α}, IsClosed x ↔ toOrderHom.toFun x = x) ClosureOperator.isClosed_iff._autoParam),
  sizeOf
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
        isClosed_iff := isClosed_iff } =
    1 + sizeOf toOrderHom
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- An injective equivariant map `α →ₑ[σ] β` induces
an equivariant map on embedding types `(ι ↪ α) → (ι ↪ β)`.  -/
Function.Injective.mulActionHom_embedding : {G : Type u_1} →
  {α : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G α] →
        {H : Type u_3} →
          {β : Type u_4} →
            [inst_2 : Group H] →
              [inst_3 : MulAction H β] →
                {σ : G → H} → {f : α →ₑ[σ] β} → (ι : Type u_5) → Function.Injective ⇑f → (ι ↪ α) →ₑ[σ] ι ↪ β
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- A morphism property `P` satisfies `P.Respects Q` if it is stable under composition on the
left and right by morphisms satisfying `Q`.  -/
CategoryTheory.MorphismProperty.Respects : {C : Type u} →
  [inst : CategoryTheory.CategoryStruct.{v, u} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.CategoryTheory.SingleObj
CategoryTheory.SingleObj.functor_map : ∀ {M : Type u} [inst : Monoid M] {C : Type v} [inst_1 : CategoryTheory.Category.{w, v} C] {X : C}
  (f : M →* CategoryTheory.End X) {X_1 Y : CategoryTheory.SingleObj M} (a : X_1 ⟶ Y),
  (CategoryTheory.SingleObj.functor f).map a = f a
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.toFiniteMeasure_nonzero : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω), μ.toFiniteMeasure ≠ 0
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.Tag.mk.injEq : ∀ (declName : Lean.Name) (database : Mathlib.CrossRef.Database) (tag comment : String) (declName_1 : Lean.Name)
  (database_1 : Mathlib.CrossRef.Database) (tag_1 comment_1 : String),
  ({ declName := declName, database := database, tag := tag, comment := comment } =
      { declName := declName_1, database := database_1, tag := tag_1, comment := comment_1 }) =
    (declName = declName_1 ∧ database = database_1 ∧ tag = tag_1 ∧ comment = comment_1)
-- Mathlib.Order.Fin.Tuple
antitone_vecEmpty : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Antitone ![a]
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.lift_post : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasLimit F] (G : CategoryTheory.Functor C D)
  [inst_4 : CategoryTheory.Limits.HasLimit (F.comp G)] (c : CategoryTheory.Limits.Cone F),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.limit.lift F c))
      (CategoryTheory.Limits.limit.post F G) =
    CategoryTheory.Limits.limit.lift (F.comp G) (G.mapCone c)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The `C`-composition morphism
  `hom(x, y) ⊗ hom(y, z) ⟶ hom(x, z)`
used to equip `C` with the structure of a `C`-category  -/
CategoryTheory.MonoidalClosed.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (x y z : C) →
        [inst_2 : CategoryTheory.Closed x] →
          [inst_3 : CategoryTheory.Closed y] → CategoryTheory.MonoidalCategoryStruct.tensorObj (x ⟹ y) (y ⟹ z) ⟶ x ⟹ z
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f₁ : E →L[𝕜] F) (f₂ : H →L[𝕜] E),
  ContinuousLinearMap.rTensor G (f₁ ∘SL f₂) = ContinuousLinearMap.rTensor G f₁ ∘SL ContinuousLinearMap.rTensor G f₂
-- Mathlib.Algebra.Algebra.Equiv
/-- Reinterpret a `RingEquiv` as an `ℕ`-algebra isomorphism.  -/
RingEquiv.toNatAlgEquiv : {R : Type u_1} → {S : Type u_2} → [inst : Semiring R] → [inst_1 : Semiring S] → R ≃+* S → R ≃ₐ[ℕ] S
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.entryAtIdx?.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → ℕ → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (x_1 : ℕ) →
          ((x : ℕ) → motive Std.DTreeMap.Internal.Impl.leaf x) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
                      (n : ℕ) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n) →
              motive x x_1
-- Mathlib.Data.Sym.Sym2
Sym2.exists : ∀ {α : Type u_4} {f : Sym2 α → Prop}, (∃ x, f x) ↔ ∃ x y, f s(x, y)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_pow_mul_cancel : ∀ {R : Type u_1} [inst : Semiring R] {k : ℕ} {φ ψ : PowerSeries R},
  PowerSeries.X ^ k * φ = PowerSeries.X ^ k * ψ → φ = ψ
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.range_path_inter_range_path : ∀ {x y : Circle}, x ≠ y → Set.range ⇑(x.path y) ∩ Set.range ⇑(y.path x) = {x, y}
-- Mathlib.AlgebraicTopology.Quasicategory.Basic
SSet.Quasicategory.hasLiftingProperty : ∀ (S : SSet) [S.Quasicategory] {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) {n : ℕ} {i : Fin (n + 1)},
  0 < i → i < Fin.last n → CategoryTheory.HasLiftingProperty (SSet.horn n i).ι (t.from S)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map : ∀ {X : AlgebraicGeometry.Scheme} (U V : X.Opens) (h : U ≤ V),
  CategoryTheory.CategoryStruct.comp U.toSpecΓ
      (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.homOfLE h).op)) =
    CategoryTheory.CategoryStruct.comp (X.homOfLE h) V.toSpecΓ
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The map `pr₁*` of the Stacks entry.  -/
CategoryTheory.Equalizer.Presieve.secondMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) →
      {X : C} →
        (R : CategoryTheory.Presieve X) →
          [inst_1 : R.HasPairwisePullbacks] →
            CategoryTheory.Equalizer.FirstObj P R ⟶ CategoryTheory.Equalizer.Presieve.SecondObj P R
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.toListRev_zip_of_finite : ∀ {α₁ α₂ β₁ β₂ : Type u_1} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂] {it₁ : Std.Iter β₁}
  {it₂ : Std.Iter β₂} [Std.Iterators.Finite α₁ Id] [Std.Iterators.Finite α₂ Id],
  (it₁.zip it₂).toListRev = (it₁.toList.zip it₂.toList).reverse
-- Mathlib.Analysis.SpecialFunctions.Bernstein
bernstein.variance : ∀ {n : ℕ}, n ≠ 0 → ∀ (x : ↑unitInterval), ∑ k, (↑x - ↑(bernstein.z k)) ^ 2 * (bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoal.toInteractiveGoalCore : Lean.Widget.InteractiveGoal → Lean.Widget.InteractiveGoalCore
-- Std.Data.HashMap.Lemmas
Std.HashMap.any_toList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {p : α → β → Bool},
  (m.toList.any fun x => p x.1 x.2) = m.any p
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.centralizer_toNonUnitalSubsemiring : ∀ {R : Type u_1} [inst : NonUnitalRing R] (s : Set R),
  (NonUnitalSubring.centralizer s).toNonUnitalSubsemiring = NonUnitalSubsemiring.centralizer s
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_homologyπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.f = 0 → ∀ [inst_2 : S.HasHomology], CategoryTheory.IsIso S.homologyπ
-- Mathlib.CategoryTheory.GlueData
/-- (Implementation) The diagram to take colimit of.  -/
CategoryTheory.GlueData.diagram : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (D : CategoryTheory.GlueData C) →
      CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod D.J) C
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the associator `α_ f g h`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.associatorM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.StructuralAtom
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.keys_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool},
  (Std.ExtDTreeMap.filter f t).keys =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (t.get x ⋯))
        t.keys.attach).unattach
-- Lean.Server.CodeActions.Basic
Lean.Server.LazyCodeAction.mk.inj : ∀ {eager : Lean.Lsp.CodeAction} {lazy? : Option (IO Lean.Lsp.CodeAction)} {eager_1 : Lean.Lsp.CodeAction}
  {lazy?_1 : Option (IO Lean.Lsp.CodeAction)},
  { eager := eager, lazy? := lazy? } = { eager := eager_1, lazy? := lazy?_1 } → eager = eager_1 ∧ lazy? = lazy?_1