mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.ModularCharacter
MeasureTheory.Measure.addModularCharacterFun_map_zero : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : LocallyCompactSpace G], MeasureTheory.Measure.addModularCharacterFun 0 = 1
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.isLUB_Iio : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α], Order.IsSuccLimit a → IsLUB (Set.Iio a) a
-- Mathlib.CategoryTheory.Action.Basic
/-- The "restriction" functor along a monoid homomorphism `f : G →* H`,
taking actions of `H` to actions of `G`.

(This makes sense for any homomorphism, but the name is natural when `f` is a monomorphism.)
 -/
Action.res : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_3} →
      {H : Type u_4} →
        [inst_1 : Monoid G] → [inst_2 : Monoid H] → (G →* H) → CategoryTheory.Functor (Action V H) (Action V G)
-- Mathlib.RingTheory.Kaehler.Basic
instSMulKaehlerDifferentialOfSMulCommClass : (R : Type u_3) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {R' : Type u_1} → [inst_3 : CommRing R'] → [inst_4 : Algebra R' S] → [SMulCommClass R R' S] → SMul R' Ω[S⁄R]
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_actionHom : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {x y : D} {x' y' : C} (f : x ⟶ y) (g : x' ⟶ y')
  [inst_4 : CategoryTheory.IsIso f] [inst_5 : CategoryTheory.IsIso g],
  CategoryTheory.inv (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g) =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom (CategoryTheory.inv f) (CategoryTheory.inv g)
-- Mathlib.RingTheory.AdicCompletion.Basic
IsHausdorff.funext : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {N : Type u_5} [inst_1 : AddCommGroup N] [inst_2 : Module R N]
  {M : Type u_6} [IsHausdorff I N] {f g : M → N},
  (∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)) → f = g
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasurableEmbedding.integrableOn_range_iff_comap : ∀ {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] [inst_2 : MeasurableSpace β] {e : α → β},
  MeasurableEmbedding e →
    ∀ {f : β → ε} {μ : MeasureTheory.Measure β},
      MeasureTheory.IntegrableOn f (Set.range e) μ ↔ MeasureTheory.Integrable (f ∘ e) (MeasureTheory.Measure.comap e μ)
-- Mathlib.Order.Category.DistLat
DistLat.hom_ofHom : ∀ {X Y : Type u} [inst : DistribLattice X] [inst_1 : DistribLattice Y] (f : LatticeHom X Y),
  DistLat.Hom.hom (DistLat.ofHom f) = f
-- Init.Prelude
/-- Execute action in a new macro invocation context. This transformer should be
used at all places that morally qualify as the beginning of a "macro call",
e.g. `elabCommand` and `elabTerm` in the case of the elaborator. However, it
can also be used internally inside a "macro" if identifiers introduced by
e.g. different recursive calls should be independent and not collide. While
returning an intermediate syntax tree that will recursively be expanded by
the elaborator can be used for the same effect, doing direct recursion inside
the macro guarded by this transformer is often easier because one is not
restricted to passing a single syntax tree. Modelling this helper as a
transformer and not just a monadic action ensures that the current macro
scope before the recursive call is restored after it, as expected.
 -/
Lean.MonadQuotation.withFreshMacroScope : {m : Type → Type} → [self : Lean.MonadQuotation m] → {α : Type} → m α → m α
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.coe_restrictScalars : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] (V : Submodule R M),
  ↑(Submodule.restrictScalars S V) = ↑V
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.instCoeHTCUnitsRingOfIntegers : (K : Type u_1) → [inst : Field K] → CoeHTC (NumberField.RingOfIntegers K)ˣ K
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.yonedaEquiv_σ_comp : ∀ {X : SSet} {n : ℕ} (g : SSet.stdSimplex.obj { len := n } ⟶ X) (i : Fin (n + 1)),
  SSet.yonedaEquiv (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.σ i) g) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X i)) (SSet.yonedaEquiv g)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInlayHintOptions : Lean.FromJson Lean.Lsp.InlayHintOptions
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.rightUnitor_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : CategoryTheory.Grp C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor G).hom.hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor G.X).hom
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_eq_cfcₙ_coe_norm : ∀ (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A]
  [inst_2 : TopologicalSpace A] [inst_3 : Module 𝕜 A] [inst_4 : StarRing A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : IsScalarTower 𝕜 A A] [inst_8 : SMulCommClass 𝕜 A A]
  [inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] [inst_10 : Module ℝ A] [inst_11 : SMulCommClass ℝ A A]
  [inst_12 : IsScalarTower ℝ A A] [inst_13 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A]
  [inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A),
  autoParam (p a) CFC.abs_eq_cfcₙ_coe_norm._auto_1 → CFC.abs a = cfcₙ (fun z => ↑‖z‖) a
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.comap_map_le : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : α → β},
  MeasurableSpace.comap f (MeasurableSpace.map f m) ≤ m
-- Mathlib.Topology.Order.OrderClosed
frontier_gt_subset_eq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {g f : β → α}
  [inst_3 : TopologicalSpace β], Continuous g → Continuous f → frontier {b | g b < f b} ⊆ {b | f b = g b}
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.exists_config : ∀ {P : Type u_1} {L : Type u_2} {inst : Membership P L} [self : Configuration.ProjectivePlane P L],
  ∃ p₁ p₂ p₃ l₁ l₂ l₃, p₁ ∉ l₂ ∧ p₁ ∉ l₃ ∧ p₂ ∉ l₁ ∧ p₂ ∈ l₂ ∧ p₂ ∈ l₃ ∧ p₃ ∉ l₁ ∧ p₃ ∈ l₂ ∧ p₃ ∉ l₃
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.desc.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] (c : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Limits.colimit.desc F c = (CategoryTheory.Limits.colimit.isColimit F).desc c
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NFBelow.oadd' : ∀ {e : ONote} {n : ℕ+} {a : ONote} {eb b : Ordinal.{0}},
  e.NFBelow eb → a.NFBelow e.repr → e.repr < b → (e.oadd n a).NFBelow b
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₂ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ)
  (h : a + b = n) (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).hom.app X).hom₂ =
    (CategoryTheory.shiftFunctorAdd' C a b n h).hom.app X.obj₂
-- Lean.Meta.Sym.Arith.Types
/-- `Ring` instance for `type`  -/
Lean.Meta.Sym.Arith.Ring.ringInst : Lean.Meta.Sym.Arith.Ring → Lean.Expr
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.Std.Iter.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Algebra.Order.Positive.Field
Positive.coe_zpow : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K] (x : { x // 0 < x })
  (n : ℤ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_top : ∀ {G : Type u_1} [inst : Group G] (x : G), x ∈ ⊤
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.prodEquiv_symm_apply_snd : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃]
  [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃]
  (f : ContinuousMultilinearMap R M₁ (M₂ × M₃)),
  (ContinuousMultilinearMap.prodEquiv.symm f).2 = (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap f
-- Mathlib.GroupTheory.GroupAction.Period
/-- If for some `n`, `m ^ n • a = a`, then `0 < period m a`.  -/
MulAction.period_pos_of_fixed : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] {m : M} {a : α} {n : ℕ},
  0 < n → m ^ n • a = a → 0 < MulAction.period m a
-- Lean.Server.Completion.CompletionItemCompression
_private.Lean.Server.Completion.CompletionItemCompression.0.Lean.Lsp.ResolvableCompletionList.compressItemsFast.eq_def : ∀ (acc : String) (items : Array Lean.Lsp.ResolvableCompletionItem) (i : ℕ),
  Lean.Lsp.ResolvableCompletionList.compressItemsFast✝ acc items i =
    if h : i < items.size then
      have acc := Lean.Lsp.ResolvableCompletionList.compressItemFast✝ acc items[i];
      have acc := if i < items.size - 1 then acc ++ "," else acc;
      Lean.Lsp.ResolvableCompletionList.compressItemsFast✝ acc items (i + 1)
    else acc
-- Mathlib.Topology.Order.OrderClosed
ClosedIicTopology.mk : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α],
  (∀ (a : α), IsClosed (Set.Iic a)) → ClosedIicTopology α
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Specialization of `Finset.prod_nbij'` that automatically fills in most arguments.

See `Fintype.prod_equiv` for the version where `s` and `t` are `univ`.  -/
Finset.prod_equiv : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (e : ι ≃ κ), (∀ (i : ι), i ∈ s ↔ e i ∈ t) → (∀ i ∈ s, f i = g (e i)) → ∏ i ∈ s, f i = ∏ i ∈ t, g i
-- Mathlib.Algebra.Order.Floor.Defs
Nat.le_floor : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : FloorSemiring α] {a : α} {n : ℕ},
  ↑n ≤ a → n ≤ ⌊a⌋₊
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- If `f` is the pointwise limit of a bounded sequence in `lp E p`, then `f` is in `lp E p`.  -/
lp.memℓp_of_tendsto : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {ι : Type u_5}
  {l : Filter ι} [l.NeBot] [_i : Fact (1 ≤ p)] {F : ι → ↥(lp E p)},
  Bornology.IsBounded (Set.range F) → ∀ {f : (a : α) → E a}, Filter.Tendsto (id fun i => ↑(F i)) l (nhds f) → Memℓp f p
-- Mathlib.Data.Set.Semiring
SetSemiring.up_lt_up : ∀ {α : Type u_1} {s t : Set α}, Set.up s < Set.up t ↔ s ⊂ t
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.isTorsionBySet_cotangent : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R), Module.IsTorsionBySet R I.Cotangent ↑I
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- If a function is locally integrable, then it is integrable on an open neighborhood of any
compact set.  -/
MeasureTheory.LocallyIntegrable.integrableOn_nhds_isCompact : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε],
  MeasureTheory.LocallyIntegrable f μ →
    ∀ {k : Set X}, IsCompact k → ∃ u, IsOpen u ∧ k ⊆ u ∧ MeasureTheory.IntegrableOn f u μ
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.AbelNF.Config.mk.injEq : ∀ (toConfig : Mathlib.Tactic.AtomM.Recurse.Config) (mode : Mathlib.Tactic.Abel.AbelMode)
  (toConfig_1 : Mathlib.Tactic.AtomM.Recurse.Config) (mode_1 : Mathlib.Tactic.Abel.AbelMode),
  ({ toConfig := toConfig, mode := mode } = { toConfig := toConfig_1, mode := mode_1 }) =
    (toConfig = toConfig_1 ∧ mode = mode_1)
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.LawfulZipOperator.instMkImpCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.RefVec.LawfulZipOperator α Std.Sat.AIG.mkImpCached
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.coe_ne_zero : ∀ {α : Type u_1} (p : PMF α), ⇑p ≠ 0
-- Mathlib.Order.Filter.NAry
Filter.map₂_curry : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (m : α × β → γ) (f : Filter α) (g : Filter β),
  Filter.map₂ (Function.curry m) f g = Filter.map m (f ×ˢ g)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- diagonal arrow of the binary product in the category `fam I`  -/
CategoryTheory.Limits.diag : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) → [inst_1 : CategoryTheory.Limits.HasBinaryProduct X X] → X ⟶ X ⨯ X
-- Mathlib.Analysis.Distribution.FourierMultiplier
SchwartzMap.fourierMultiplierCLM_ofReal : ∀ (𝕜 : Type u_2) {E : Type u_3} {F : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace ℝ E] [inst_4 : NormedSpace ℂ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℂ 𝕜 F] [inst_7 : FiniteDimensional ℝ E] [inst_8 : MeasurableSpace E] [inst_9 : BorelSpace E]
  {g : E → ℝ},
  Function.HasTemperateGrowth g →
    ∀ (f : SchwartzMap E F),
      (SchwartzMap.fourierMultiplierCLM F fun x => ↑(g x)) f = (SchwartzMap.fourierMultiplierCLM F g) f
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.updateCell.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (l.size - 1) (l.size + 1) → Sort u_3)
  (newL : Std.DTreeMap.Internal.Impl α β) (h₁ : newL.Balanced) (h₂ : l.size - 1 ≤ newL.size)
  (h₃ : newL.size ≤ l.size + 1)
  (h_1 :
    (newL : Std.DTreeMap.Internal.Impl α β) →
      (h₁ : newL.Balanced) →
        (h₂ : l.size - 1 ≤ newL.size) →
          (h₃ : newL.size ≤ l.size + 1) →
            motive { impl := newL, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ }),
  (match { impl := newL, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ } with
    | { impl := newL, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ } => h_1 newL h₁ h₂ h₃) =
    h_1 newL h₁ h₂ h₃
-- Mathlib.CategoryTheory.Galois.Action
CategoryTheory.PreGaloisCategory.instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  (CategoryTheory.PreGaloisCategory.functorToAction F).ReflectsIsomorphisms
-- Init.Data.Array.Lemmas
Array.exists_mem_of_size_pos : ∀ {α : Type u_1} {xs : Array α}, 0 < xs.size → ∃ a, a ∈ xs
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_mul_unit_left_right : ∀ {R : Type u_1} [inst : CommSemiring R] {x : R}, IsUnit x → ∀ (y z : R), IsCoprime y (x * z) ↔ IsCoprime y z
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.id_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (f : α →ᵈ β),
  (Dilation.id β).comp f = f
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.ofComonObjCoalgebraStruct_counit : ∀ {R : Type u} [inst : CommRing R] (X : ModuleCat R) [inst_1 : CategoryTheory.ComonObj X],
  CoalgebraStruct.counit = ModuleCat.Hom.hom CategoryTheory.ComonObj.counit
-- Mathlib.Order.Antisymmetrization
OrderHom.antisymmetrization_apply_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (a : α),
  f.antisymmetrization (toAntisymmetrization (fun x1 x2 => x1 ≤ x2) a) =
    toAntisymmetrization (fun x1 x2 => x1 ≤ x2) (f a)
-- Mathlib.RingTheory.Spectrum.Prime.Chevalley
PrimeSpectrum.isConstructible_comap_C : ∀ {R : Type u_1} [inst : CommRing R] {s : Set (PrimeSpectrum (Polynomial R))},
  Topology.IsConstructible s → Topology.IsConstructible (PrimeSpectrum.comap Polynomial.C '' s)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ} (φ : T₁ ⟶ T₂),
  (CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C).map φ =
    Quiver.Hom.op { hom₁ := φ.hom₃.unop, hom₂ := φ.hom₂.unop, hom₃ := φ.hom₁.unop, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
-- Mathlib.Analysis.Convex.Radon
/-- **Helly's theorem** for finite sets of convex sets.

If `F` is a finite set of convex sets in a vector space of finite dimension `d`, and any `k ≤ d + 1`
sets from `F` intersect nontrivially, then all sets from `F` intersect nontrivially.  -/
Convex.helly_theorem_set' : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [FiniteDimensional 𝕜 E] {F : Finset (Set E)},
  (∀ X ∈ F, Convex 𝕜 X) → (∀ G ⊆ F, G.card ≤ Module.finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty) → (⋂₀ ↑F).Nonempty
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.instDeterministicHomLeftUnitor : ∀ {X : SFinKer}, CategoryTheory.Deterministic (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.jdecl.injEq : ∀ (j : Lean.IR.JoinPointId) (xs : Array Lean.IR.Param) (v b : Lean.IR.FnBody) (j_1 : Lean.IR.JoinPointId)
  (xs_1 : Array Lean.IR.Param) (v_1 b_1 : Lean.IR.FnBody),
  (Lean.IR.FnBody.jdecl j xs v b = Lean.IR.FnBody.jdecl j_1 xs_1 v_1 b_1) = (j = j_1 ∧ xs = xs_1 ∧ v = v_1 ∧ b = b_1)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le : ∀ {𝕜 : 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] {n : ℕ} (c : OrderedFinpartition n)
  (f₁ f₂ : F [×c.length]→L[𝕜] G) (g₁ g₂ : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F),
  ‖c.compAlongOrderedFinpartition f₁ g₁ - c.compAlongOrderedFinpartition f₂ g₂‖ ≤
    ‖f₁‖ * ↑c.length * max ‖g₁‖ ‖g₂‖ ^ (c.length - 1) * ‖g₁ - g₂‖ + ‖f₁ - f₂‖ * ∏ i, ‖g₂ i‖
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_filter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Bool} {k : α} [inst_3 : Inhabited (β k)],
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.filter f m).get! k = (Option.filter (f k) (m.get? k)).get!
-- Mathlib.Topology.KrullDimension
/-- The topological Krull dimension is invariant under homeomorphisms  -/
IsHomeomorph.topologicalKrullDim_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  IsHomeomorph f → topologicalKrullDim X = topologicalKrullDim Y
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.whiskering_map_app_left : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u') [inst_1 : CategoryTheory.Category.{v', u'} D]
  {X Y : CategoryTheory.Functor C D} (η : X ⟶ Y) (A : CategoryTheory.CosimplicialObject.Augmented C),
  (((CategoryTheory.CosimplicialObject.Augmented.whiskering C D).map η).app A).left =
    η.app (CategoryTheory.CosimplicialObject.Augmented.point.obj A)
-- Mathlib.Order.Interval.Multiset
Multiset.Iic.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (b : α), Multiset.Iic b = (Finset.Iic b).val
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.ctor.inj : ∀ {info : Lean.IR.CtorInfo} {b : Lean.IR.FnBody} {info_1 : Lean.IR.CtorInfo} {b_1 : Lean.IR.FnBody},
  Lean.IR.Alt.ctor info b = Lean.IR.Alt.ctor info_1 b_1 → info = info_1 ∧ b = b_1
-- Std.Sat.AIG.CNF
/-- The CNF returned by `go` will always be SAT at `cnfSatAssignment`.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.go_sat : ∀ (aig : Std.Sat.AIG ℕ) (start : ℕ) (h1 : start < aig.decls.size) (assign1 : ℕ → Bool)
  (state : Std.Sat.AIG.toCNF.State✝ aig),
  Std.Sat.AIG.toCNF.State.Sat✝ (Std.Sat.AIG.toCNF.cnfSatAssignment✝ aig assign1)
    ↑(Std.Sat.AIG.toCNF.go✝ aig start h1 state)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.equivHomShift_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (a : CochainComplex.HomComplex.Cocycle K L n),
  CochainComplex.HomComplex.Cocycle.equivHomShift.symm a = (a.rightShift n 0 ⋯).homOf
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_rightDistributor_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (X : C) (f : J → C) (Y : C),
  CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.leftDistributor X f)
        (CategoryTheory.asIso (CategoryTheory.CategoryStruct.id Y)) ≪≫
      CategoryTheory.rightDistributor (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) Y =
    CategoryTheory.MonoidalCategoryStruct.associator X (⨁ f) Y ≪≫
      CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.asIso (CategoryTheory.CategoryStruct.id X))
          (CategoryTheory.rightDistributor f Y) ≪≫
        (CategoryTheory.leftDistributor X fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) Y) ≪≫
          CategoryTheory.Limits.biproduct.mapIso fun x =>
            (CategoryTheory.MonoidalCategoryStruct.associator X (f x) Y).symm
-- Mathlib.RingTheory.WittVector.InitTail
_private.Mathlib.RingTheory.WittVector.InitTail.0.term𝕎 : Lean.ParserDescr
-- Mathlib.Order.Cover
covBy_of_eq_or_eq : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → (∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b) → a ⋖ b
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instOfNatOffset : {n : ℕ} → OfNat Std.Time.Millisecond.Offset n
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
Lex.instCommMonoidWithZero : {α : Type u_1} → [CommMonoidWithZero α] → CommMonoidWithZero (Lex α)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.HasBinaryBiproduct.mk : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (d : CategoryTheory.Limits.BinaryBiproductData P Q), CategoryTheory.Limits.HasBinaryBiproduct P Q
-- Mathlib.Order.KrullDimension
_private.Mathlib.Order.KrullDimension.0.Order.exists_eq_iSup_of_iSup_eq_coe : ∀ {α : Type u_3} [Nonempty α] {f : α → ℕ∞} {n : ℕ}, ⨆ x, f x = ↑n → ∃ x, f x = ↑n
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.handleSemanticTokensDidChange : Lean.Lsp.DidChangeTextDocumentParams → StateT Lean.Server.FileWorker.SemanticTokensState Lean.Server.RequestM Unit