mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- An orthonormal family of vectors whose span is dense in the whole module is a Hilbert basis.  -/
HilbertBasis.mk : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] →
      {E : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [CompleteSpace E] →
              {v : ι → E} →
                Orthonormal 𝕜 v → ⊤ ≤ (Submodule.span 𝕜 (Set.range v)).topologicalClosure → HilbertBasis ι 𝕜 E
-- Mathlib.Algebra.PresentedMonoid.Basic
/-- The extension of a map `f : α → M` that satisfies the given relations to a monoid homomorphism
from `PresentedMonoid rels → M`.  -/
PresentedMonoid.lift : {α : Type u_3} →
  {M : Type u_4} →
    [inst : Monoid M] →
      (f : α → M) →
        {rels : FreeMonoid α → FreeMonoid α → Prop} →
          (∀ (a b : FreeMonoid α), rels a b → (FreeMonoid.lift f) a = (FreeMonoid.lift f) b) → PresentedMonoid rels →* M
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrp_obj_grp_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.Braided] (A : CategoryTheory.CommGrp C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.MonObj.one)
-- Mathlib.Algebra.Group.Units.Basic
Units.mul_inv_cancel_right : ∀ {α : Type u} [inst : Monoid α] (a : α) (b : αˣ), a * ↑b * ↑b⁻¹ = a
-- Lean.Meta.Basic
Lean.Meta.shouldReduceAll : Lean.MetaM Bool
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.entries.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β]
  (es : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))),
  sizeOf (Lean.PersistentHashMap.Node.entries es) = 1 + sizeOf es
-- Mathlib.Topology.Order.Basic
/-- An order-theoretically left-continuous function is topologically left-continuous, assuming
the function is between conditionally complete linear orders with order topologies.  -/
LeftOrdContinuous.continuousWithinAt_Iic : ∀ {X : Type u_1} [inst : ConditionallyCompleteLinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X]
  {Y : Type u_2} [inst_3 : ConditionallyCompleteLinearOrder Y] [inst_4 : TopologicalSpace Y] [OrderTopology Y]
  {f : X → Y} {x : X}, LeftOrdContinuous f → ContinuousWithinAt f (Set.Iic x) x
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Const.maxEntryD.eq_def : ∀ {α : Type u} {β : Type v} (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : α × β),
  Std.DTreeMap.Internal.Impl.Const.maxEntryD x x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => (k, v)
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => Std.DTreeMap.Internal.Impl.Const.maxEntryD r fallback
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the coherence isomorphism `⊗𝟙 : f ⟶ g`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.coherenceHomM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ → Lean.Expr → m Mathlib.Tactic.BicategoryLike.CoherenceHom
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.MagmaCat.Hom.mk.inj : ∀ {A B : MagmaCat} {hom' hom'_1 : ↑A →ₙ* ↑B}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Quaternion.im_exp : ∀ (q : Quaternion ℝ), (NormedSpace.exp q).im = (NormedSpace.exp q.re * (Real.sin ‖q.im‖ / ‖q.im‖)) • q.im
-- Mathlib.Data.TypeVec
TypeVec.prod_fst_mk : ∀ {n : ℕ} {α β : TypeVec.{u_1} n} (i : Fin2 n) (a : α i) (b : β i), TypeVec.prod.fst i (TypeVec.prod.mk i a b) = a
-- Mathlib.Analysis.RCLike.Extend
Module.Dual.norm_extendRCLike_apply_sq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : AddCommGroup F] [inst_2 : Module ℝ F] [inst_3 : Module 𝕜 F]
  [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F) (x : F),
  ‖fr.extendRCLike x‖ ^ 2 = fr ((starRingEnd 𝕜) (fr.extendRCLike x) • x)
-- Mathlib.Data.Finset.Image
Finset.image_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq β] {f : α → β} {s : Finset α}
  [inst_1 : DecidableEq γ] {g : β → γ}, Finset.image g (Finset.image f s) = Finset.image (g ∘ f) s
-- Init.Data.String.OrderInstances
String.Slice.Pos.instToIntCoOfNatIntHAddCastUtf8ByteSize : {s : String.Slice} → Lean.Grind.ToInt s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))
-- Mathlib.Order.Basic
Std.Irrefl.compl : ∀ {α : Type u_2} (r : α → α → Prop) [Std.Irrefl r], Std.Refl rᶜ
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange_hom_app_app_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type}
  [inst_1 : CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (X_1 : J)
  (a :
    ((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.functorToInterchange A
                K).flip.obj
          X).obj
      X_1),
  (CategoryTheory.ConcreteCategory.hom
        (((CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.flipFunctorToInterchange A
                    K).hom.app
              X).app
          X_1))
      a =
    a
-- Mathlib.Topology.Connected.Clopen
/-- In a preconnected space, any disjoint cover by non-empty open subsets has at most one
element.  -/
subsingleton_of_disjoint_isOpen_iUnion_eq_univ : ∀ {α : Type u} {ι : Type u_1} [inst : TopologicalSpace α] [PreconnectedSpace α] {s : ι → Set α},
  (∀ (i : ι), (s i).Nonempty) →
    Pairwise (Function.onFun Disjoint s) → (∀ (i : ι), IsOpen (s i)) → ⋃ i, s i = Set.univ → Subsingleton ι
-- Lean.Server.Requests
/-- `stateRef` is synchronized in `registerStatefulLspRequestHandler` by using `lastTaskMutex` to
ensure that stateful request tasks for the same handler are executed sequentially (in order of arrival).
 -/
Lean.Server.StatefulRequestHandler.stateRef : Lean.Server.StatefulRequestHandler → IO.Ref Dynamic
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.prop_iff_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y), P X ↔ P Y
-- Mathlib.Order.SuccPred.IntervalSucc
/-- Special case `a = ⊥` of `biUnion_Ici_Ioc_map_succ`.  -/
iUnion_Ioc_map_succ_eq_Ioi : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] [inst_4 : LinearOrder β] {f : α → β},
  (∀ (a : α), f ⊥ ≤ f a) → ¬BddAbove (Set.range f) → ⋃ a, Set.Ioc (f a) (f (Order.succ a)) = Set.Ioi (f ⊥)
-- Mathlib.Order.Sublattice
Sublattice.mem_carrier : ∀ {α : Type u_2} [inst : Lattice α] {L : Sublattice α} {a : α}, a ∈ L.carrier ↔ a ∈ L
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_top_eq_top_of_mul_eq_one : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (N P : Submodule R A), N * P = 1 → N * ⊤ = ⊤
-- Mathlib.Topology.Order.CountableSeparating
HasCountableSeparatingOn.range_Ioi : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X] [SecondCountableTopology X]
  {s : Set X}, HasCountableSeparatingOn X (fun x => x ∈ Set.range Set.Ioi) s
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMap.match_1.eq_1 : ∀ {C₀ : Type u_4} {C : Type u_5} [inst : CategoryTheory.Category.{u_2, u_4} C₀]
  [inst_1 : CategoryTheory.Category.{u_3, u_5} C] {F : CategoryTheory.Functor C₀ C} {X : C}
  (data : F.PreOneHypercoverDenseData X)
  (motive : CategoryTheory.Limits.WalkingMulticospan data.multicospanShape → Sort u_6) (i : data.multicospanShape.L)
  (h_1 : (i : data.multicospanShape.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i))
  (h_2 : (j : data.multicospanShape.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right j)),
  (match CategoryTheory.Limits.WalkingMulticospan.left i with
    | CategoryTheory.Limits.WalkingMulticospan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMulticospan.right j => h_2 j) =
    h_1 i
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
AEMeasurable.isGLB : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Sort u_5}
  {μ : MeasureTheory.Measure δ} [Countable ι] {f : ι → δ → α} {g : δ → α},
  (∀ (i : ι), AEMeasurable (f i) μ) → (∀ᵐ (b : δ) ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)) → AEMeasurable g μ
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg_ofNat_of_lt : ∀ {n : ℕ}, n < 2 ^ 63 → (Int64.ofNat n).toNatClampNeg = n
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_zero_of_antitone : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) (seq : ℕ → ℚ),
      Antitone seq →
        Filter.Tendsto seq Filter.atTop Filter.atBot →
          ∀ᵐ (c : β) ∂ν a, Filter.Tendsto (fun m => f (a, c) (seq m)) Filter.atTop (nhds 0)
-- Lean.Elab.InfoTree.Main
Lean.Elab.ContextInfo.ppGoals : Lean.Elab.ContextInfo → List Lean.MVarId → IO Std.Format
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.pOpcycles_opcyclesIsoSc'_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  CategoryTheory.CategoryStruct.comp (K.sc' i j k).pOpcycles (K.opcyclesIsoSc' i j k hi hk).inv = K.pOpcycles j
-- Mathlib.Data.Finset.Dedup
Multiset.isWellFounded_ssubset : ∀ {β : Type u_2}, IsWellFounded (Multiset β) fun x1 x2 => x1 ⊂ x2
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.nonneg : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν → ∀ (a : α), ∀ᵐ (c : β) ∂ν a, ∀ (q : ℚ), 0 ≤ f (a, c) q
-- Mathlib.Algebra.Group.Defs
zpow_two : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a : G), a ^ 2 = a * a
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.cof_preOmega_add_one : ∀ {o : Ordinal.{u_1}}, Ordinal.omega0 ≤ o → (Ordinal.preOmega (o + 1)).cof = Cardinal.preAleph (o + 1)
-- Mathlib.MeasureTheory.Integral.TorusIntegral
torusMap_sub_center : ∀ {n : ℕ} (c : Fin n → ℂ) (R θ : Fin n → ℝ), torusMap c R θ - c = torusMap 0 R θ
-- Mathlib.Topology.Constructions
continuous_toMul : ∀ {X : Type u} [inst : TopologicalSpace X], Continuous ⇑Additive.toMul
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- The neighbor finset of `w ∈ sᶜ` in `G.between s sᶜ` excludes the vertices in `sᶜ` adjacent to
`w` in `G`.  -/
SimpleGraph.neighborFinset_subset_between_union_compl : ∀ {V : Type u_1} {w : V} {G : SimpleGraph V} [inst : DecidableEq V] [inst_1 : Fintype V] {s : Finset V}
  [inst_2 : DecidableRel G.Adj], w ∈ sᶜ → G.neighborFinset w ⊆ (SimpleGraph.between (↑s) (↑s)ᶜ G).neighborFinset w ∪ sᶜ
-- Mathlib.Topology.Connected.TotallyDisconnected
isTotallyDisconnected_singleton : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, IsTotallyDisconnected {x}
-- Mathlib.Order.BooleanAlgebra.Defs
GeneralizedBooleanAlgebra.toBot : {α : Type u} → [self : GeneralizedBooleanAlgebra α] → Bot α
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.lift_bijective : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (self : StandardEtalePresentation R S), Function.Bijective ⇑(self.lift self.x ⋯)
-- Mathlib.Order.Filter.IsBounded
Antitone.frequently_ge_map_of_frequently_le : ∀ {R : Type u_5} {S : Type u_6} {F : Filter R} [inst : LinearOrder R] [inst_1 : LinearOrder S] {f : R → S},
  Antitone f → ∀ {l : R}, (∃ᶠ (x : R) in F, x ≤ l) → ∃ᶠ (y : S) in Filter.map f F, f l ≤ y
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_preservesPullback_of_left : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g)
    (AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.comp
      AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace)
-- Mathlib.CategoryTheory.Presentable.Presheaf
CategoryTheory.Presheaf.freeYoneda.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] (X X_1 : C),
  X = X_1 → ∀ (M M_1 : A), M = M_1 → CategoryTheory.Presheaf.freeYoneda X M = CategoryTheory.Presheaf.freeYoneda X_1 M_1
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.Truncated.sk.faithful : ∀ (n : ℕ), (SSet.Truncated.sk n).Faithful
-- Mathlib.Order.BooleanAlgebra.Defs
Bool.inf_eq_band : (fun x1 x2 => min x1 x2) = and
-- Mathlib.RingTheory.Derivation.MapCoeffs
Differential.coeff_mapCoeffs : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] (p : Polynomial A) (i : ℕ),
  (Differential.mapCoeffs p).coeff i = (p.coeff i)′
-- Std.Http.Data.URI.Basic
/-- Appends an already-encoded segment to the path.
 -/
Std.Http.URI.Path.appendEncoded : Std.Http.URI.Path → Std.Http.URI.EncodedSegment → Std.Http.URI.Path
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_toList_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, ⟨k, v⟩ ∈ m.toList ↔ m.get? k = some v
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.measurableSet : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
  {f : α → β} [inst_1 : Zero β] [inst_2 : T2Space β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ),
  MeasurableSet hf.sigmaFiniteSet
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_self : ∀ {E : Type v} [inst : Field E] (A : Subfield E), A.relfinrank A = 1
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.mkHom_hom : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {s t : CategoryTheory.Limits.Cotrident f} (k : s.pt ⟶ t.pt)
  (w : autoParam (CategoryTheory.CategoryStruct.comp s.π k = t.π) CategoryTheory.Limits.Cotrident.mkHom._auto_1),
  (CategoryTheory.Limits.Cotrident.mkHom k w).hom = k
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.modify.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp]
  (t t_1 : Std.DTreeMap.Raw α β cmp), t = t_1 → ∀ (a : α) (f f_1 : β a → β a), f = f_1 → t.modify a f = t_1.modify a f_1
-- Mathlib.Topology.MetricSpace.IsometricSMul
isometry_add_left : ∀ {M : Type u} [inst : Add M] [inst_1 : PseudoEMetricSpace M] [IsIsometricVAdd M M] (a : M), Isometry fun x => a + x
-- Mathlib.Topology.MetricSpace.IsometricSMul
Pi.isIsometricSMul'' : ∀ {ι : Type u_3} {M : ι → Type u_2} [inst : Fintype ι] [inst_1 : (i : ι) → Mul (M i)]
  [inst_2 : (i : ι) → PseudoEMetricSpace (M i)] [∀ (i : ι), IsIsometricSMul (M i)ᵐᵒᵖ (M i)],
  IsIsometricSMul ((i : ι) → M i)ᵐᵒᵖ ((i : ι) → M i)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.braiding_inv_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ X Y).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd Y X) h
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.isoOfHomotopyEquiv_inv : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D),
  (HomotopyCategory.isoOfHomotopyEquiv f).inv = (HomotopyCategory.quotient V c).map f.inv
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero : ∀ {R : Type u} {A : Type u_1} [inst : CommRing R] [inst_1 : CommRing A] {f : R →+* A},
  Function.Injective ⇑f →
    ∀ {p : Polynomial R},
      p.Monic → ∀ (x y : R) (z : A), Polynomial.eval₂ f z p = 0 → f x * z = f y → x ∣ y ^ p.natDegree
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The data part of a continuation is a list of lists, which is encoded on the `stack` stack
using `trLList`.  -/
Turing.PartrecToTM2.trContStack : Turing.ToPartrec.Cont → List Turing.PartrecToTM2.Γ'
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {X Y Z : CategoryTheory.Limits.ColimitPresentation.Total P} (f : X.Hom Y) (g : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n log n)`. Convert the heap to an array in increasing order.  -/
Batteries.BinomialHeap.Imp.Heap.toArray : {α : Type u_1} → (α → α → Bool) → Batteries.BinomialHeap.Imp.Heap α → Array α
-- Mathlib.Algebra.Quandle
ShelfHom.ext_iff : ∀ {S₁ : Type u_1} {S₂ : Type u_2} {inst : Shelf S₁} {inst_1 : Shelf S₂} {x y : ShelfHom S₁ S₂},
  x = y ↔ x.toFun = y.toFun
-- Mathlib.Analysis.Convex.Between
Sbtw.right_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P}, Sbtw R x y z → z ≠ y
-- Mathlib.CategoryTheory.Shift.Quotient
/-- The functor `Quotient.functor r : C ⥤ Quotient r` commutes with the shift.  -/
CategoryTheory.Quotient.functor_commShift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (r : HomRel C) →
      (A : Type w) →
        [inst_1 : AddMonoid A] →
          [inst_2 : CategoryTheory.HasShift C A] →
            [inst_3 : r.IsCompatibleWithShift A] → (CategoryTheory.Quotient.functor r).CommShift A
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_emptyWithCapacity : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {a : α} {c : ℕ},
  (Std.HashSet.Raw.emptyWithCapacity c).contains a = false
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.addEquivOfLocalizations_symm_eq_addEquivOfLocalizations : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {k : S.LocalizationMap P},
  (k.addEquivOfLocalizations f).symm = f.addEquivOfLocalizations k
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.ker_apply : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {f : M →+ P} {x y : M},
  (AddCon.ker f) x y ↔ f x = f y
-- Mathlib.Data.Set.Functor
Set.eq_univ_of_image_val_eq : ∀ {α : Type u} {β : Set α} {γ : Set ↑β}, Subtype.val '' γ = β → γ = Set.univ
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_η : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X),
  CategoryTheory.CategoryStruct.comp
      (Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor Cᵒᵖ A)))
      (CategoryTheory.Functor.OplaxMonoidal.η Φ.presheafFiber) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)
-- Mathlib.Tactic.Algebra.Basic
/-- This cache contains typeclasses required during `algebra`'s execution. These assumptions
are stronger than `ring` because `algebra` occasionally requires commutativity to move between
the base ring and the algebra.  -/
Mathlib.Tactic.Algebra.Cache : {u : Lean.Level} → {A : Q(Type u)} → Q(CommSemiring «$A») → Type
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLT_map_app_eTruncLTι_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {i j : EInt} (f : i ⟶ j) (X : C) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.map f).app X)
      (CategoryTheory.CategoryStruct.comp ((t.eTruncLTι j).app X) h) =
    CategoryTheory.CategoryStruct.comp ((t.eTruncLTι i).app X) h
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.pairwise_toList_ne : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α], List.Pairwise (fun a b => a ≠ b) r.toList
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_append_of_containsKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l l' : List ((a : α) × β a)} {a : α}
  {h : Std.Internal.List.containsKey a (l ++ l') = true} (hl' : Std.Internal.List.containsKey a l' = false),
  Std.Internal.List.getEntry a (l ++ l') h = Std.Internal.List.getEntry a l ⋯
-- Mathlib.Algebra.Quaternion
Quaternion.instModule : {S : Type u_1} → {R : Type u_3} → [inst : CommRing R] → [inst_1 : Semiring S] → [Module S R] → Module S (Quaternion R)
-- Mathlib.Algebra.Group.Shrink
equivShrink_symm_sub : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Sub α] (x y : Shrink.{v, u_2} α),
  (equivShrink α).symm (x - y) = (equivShrink α).symm x - (equivShrink α).symm y
-- Init.Data.List.Erase
List.erase_eq_eraseP' : ∀ {α : Type u_1} [inst : BEq α] (a : α) (l : List α), l.erase a = List.eraseP (fun x => x == a) l
-- Mathlib.Data.Finset.SDiff
Finset.insert_sdiff_insert' : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ≠ b → a ∉ s → insert a s \ insert b s = {a}