mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_inv_π_π_assoc : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape K C] (k : K) (j : J) {Z : C} (h : (F.flip.obj k).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.flip.comp CategoryTheory.Limits.lim) k)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.flip.obj k) j) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.obj j) k) h)
-- Lean.Meta.Sym.Arith.Poly
/-- The computed S-polynomial.  -/
Lean.Grind.CommRing.SPolResult.spol : Lean.Grind.CommRing.SPolResult → Lean.Grind.CommRing.Poly
-- Mathlib.Order.Category.Preord
Preord.ofHom_comp : ∀ {X Y Z : Type u} [inst : Preorder X] [inst_1 : Preorder Y] [inst_2 : Preorder Z] (f : X →o Y) (g : Y →o Z),
  Preord.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (Preord.ofHom f) (Preord.ofHom g)
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.instLocallyOfFinitePresentationOfIsLocallyNoetherianOfLocallyOfFiniteType : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsLocallyNoetherian Y]
  [AlgebraicGeometry.LocallyOfFiniteType f], AlgebraicGeometry.LocallyOfFinitePresentation f
-- Mathlib.Topology.ContinuousMap.Polynomial
polynomialFunctions.eq_adjoin_X : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R] (s : Set R),
  polynomialFunctions s = R[(Polynomial.toContinuousMapOnAlgHom s) Polynomial.X]
-- Std.Http.Data.Status
/-- 202 Accepted
 -/
Std.Http.Status.accepted : Std.Http.Status
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_add_of_nonneg_of_le : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b c : α}, 0 ≤ a → b ≤ c → b ≤ a + c
-- Std.Time.DateTime
/-- Creates a new `DateTime` by adjusting the year to the given `year` value. The month and day are rolled
over to the next valid month and day if necessary.
 -/
Std.Time.DateTime.withYearRollOver : Std.Time.DateTime → Std.Time.Year.Offset → Std.Time.DateTime
-- Mathlib.NumberTheory.NumberField.ClassNumber
/-- The class number of a number field is `1` iff the ring of integers is a PID.  -/
NumberField.classNumber_eq_one_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  NumberField.classNumber K = 1 ↔ IsPrincipalIdealRing (NumberField.RingOfIntegers K)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fundamentalSequence.eq_def : ∀ (x : ONote),
  x.fundamentalSequence =
    match x with
    | ONote.zero => Sum.inl none
    | a.oadd m b =>
      match b.fundamentalSequence with
      | Sum.inr f => Sum.inr fun i => a.oadd m (f i)
      | Sum.inl (some b') => Sum.inl (some (a.oadd m b'))
      | Sum.inl none =>
        match a.fundamentalSequence, m.natPred with
        | Sum.inl none, 0 => Sum.inl (some ONote.zero)
        | Sum.inl none, m.succ => Sum.inl (some (ONote.zero.oadd m.succPNat ONote.zero))
        | Sum.inl (some a'), 0 => Sum.inr fun i => a'.oadd i.succPNat ONote.zero
        | Sum.inl (some a'), m.succ => Sum.inr fun i => a.oadd m.succPNat (a'.oadd i.succPNat ONote.zero)
        | Sum.inr f, 0 => Sum.inr fun i => (f i).oadd 1 ONote.zero
        | Sum.inr f, m.succ => Sum.inr fun i => a.oadd m.succPNat ((f i).oadd 1 ONote.zero)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isSome_apply_of_contains_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ}
  {k : α} (h : (↑m).WF) (h' : (Std.DHashMap.Internal.Raw₀.filterMap f m).contains k = true),
  (f (m.getKey k ⋯) (Std.DHashMap.Internal.Raw₀.Const.get m k ⋯)).isSome = true
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instReprLeapSecond.repr : Std.Time.TimeZone.TZif.LeapSecond → ℕ → Std.Format
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.instIsRepresentableCompOppositeUliftFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v))
  [F.IsRepresentable], (F.comp CategoryTheory.uliftFunctor.{w, v}).IsRepresentable
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roc.toList_iter_eq_toList : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roc α}, r.iter.toList = r.toList
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_eq_diagonal_iff : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] {d₁ d₂ : n → α},
  Matrix.diagonal d₁ = Matrix.diagonal d₂ ↔ ∀ (i : n), d₁ i = d₂ i
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.cube_of_not_dvd : ∀ {n : ℤ}, ¬3 ∣ n → ↑n ^ 3 = 1 ∨ ↑n ^ 3 = 8
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
/-- The first function in a well-formed basis is eventually positive.  -/
Tactic.ComputeAsymptotics.WellFormedBasis.head_eventually_pos : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis (basis_hd :: basis_tl) → ∀ᶠ (x : ℝ) in Filter.atTop, 0 < basis_hd x
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_additive : ∀ {G : Type u} [inst : Monoid G], AddMonoid.exponent (Additive G) = Monoid.exponent G
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.val_mem_of_mem_addUnits : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M}, x ∈ S.addUnits → ↑x ∈ S
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k : α} {fallback : β},
      (List.map Prod.fst l).contains k = false →
        Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.Const.insertMany m l) k fallback =
          Std.DHashMap.Raw.Const.getD m k fallback
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- **Alias** of the reverse direction of `SimpleGraph.edgeFinset_subset_edgeFinset`. -/
SimpleGraph.edgeFinset_mono : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} [inst : Fintype ↑G₁.edgeSet] [inst_1 : Fintype ↑G₂.edgeSet],
  G₁ ≤ G₂ → G₁.edgeFinset ⊆ G₂.edgeFinset
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- An `AddGroup` homomorphism `f : G →+ H` induces a map `G/N →+ H/M` if `N ⊆ f⁻¹(M)`.  -/
QuotientAddGroup.map : {G : Type u_1} →
  {H : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddGroup H] →
        (N : AddSubgroup G) →
          [nN : N.Normal] →
            (M : AddSubgroup H) → [inst_2 : M.Normal] → (f : G →+ H) → N ≤ AddSubgroup.comap f M → G ⧸ N →+ H ⧸ M
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
MvQPF.Pi.instMvFunctor : {n : ℕ} → {A : Type u} → (F : A → TypeVec.{u} n → Type u) → [(α : A) → MvFunctor (F α)] → MvFunctor (MvQPF.Pi F)
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopyCategory.Plus.isIso_quotient_map_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex.Plus (CategoryTheory.InjectiveObject C)} (f : K ⟶ L),
  CategoryTheory.IsIso ((HomotopyCategory.Plus.quotient (CategoryTheory.InjectiveObject C)).map f) ↔
    CochainComplex.Plus.quasiIso C ((CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus.map f)
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
_private.Mathlib.GroupTheory.SpecificGroups.Quaternion.0.instDecidableEqQuaternionGroup.decEq.match_1.eq_4 : ∀ {n : ℕ} (motive : QuaternionGroup n → QuaternionGroup n → Sort u_1) (a b : ZMod (2 * n))
  (h_1 : (a b : ZMod (2 * n)) → motive (QuaternionGroup.a a) (QuaternionGroup.a b))
  (h_2 : (a a_1 : ZMod (2 * n)) → motive (QuaternionGroup.a a) (QuaternionGroup.xa a_1))
  (h_3 : (a a_1 : ZMod (2 * n)) → motive (QuaternionGroup.xa a) (QuaternionGroup.a a_1))
  (h_4 : (a b : ZMod (2 * n)) → motive (QuaternionGroup.xa a) (QuaternionGroup.xa b)),
  (match QuaternionGroup.xa a, QuaternionGroup.xa b with
    | QuaternionGroup.a a, QuaternionGroup.a b => h_1 a b
    | QuaternionGroup.a a, QuaternionGroup.xa a_1 => h_2 a a_1
    | QuaternionGroup.xa a, QuaternionGroup.a a_1 => h_3 a a_1
    | QuaternionGroup.xa a, QuaternionGroup.xa b => h_4 a b) =
    h_4 a b
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.pIntegral_pow_div : ∀ {p M N : ℕ} [inst : Fact (Nat.Prime p)], M ≠ 0 → M.factorization p ≤ N → Bernoulli.pIntegral✝ p (↑p ^ N / ↑M)
-- Mathlib.Data.Rat.Lemmas
Rat.den_div_eq_of_coprime : ∀ {a b : ℤ}, 0 < b → a.natAbs.Coprime b.natAbs → ↑(↑a / ↑b).den = b
-- Mathlib.GroupTheory.Exponent
AddSubgroup.exponent_toAddSubmonoid : ∀ {G : Type u} [inst : AddGroup G] (H : AddSubgroup G), AddMonoid.exponent ↥H.toAddSubmonoid = AddMonoid.exponent ↥H
-- Lean.Util.PtrSet
Lean.mkPtrMap : {α β : Type} → optParam ℕ 64 → Lean.PtrMap α β
-- Mathlib.Order.SuccPred.Basic
Order.Ico_succ_right_eq_insert : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  a ≤ b → Set.Ico a (Order.succ b) = insert b (Set.Ico a b)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.isCharNeTwoNF_of_isCharThreeJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF], W.IsCharNeTwoNF
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.image_coe_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithTop.some '' Set.Ico a b = Set.Ico ↑a ↑b
-- Mathlib.Algebra.Order.Group.End
RelIso.instGroup : {α : Type u_1} → {r : α → α → Prop} → Group (r ≃r r)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trNum.match_1.eq_2 : ∀ (motive : Num → Sort u_1) (n : PosNum) (h_1 : Unit → motive Num.zero) (h_2 : (n : PosNum) → motive (Num.pos n)),
  (match Num.pos n with
    | Num.zero => h_1 ()
    | Num.pos n => h_2 n) =
    h_2 n
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_inter_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} {fallback : β k}, m₂.contains k = false → (m₁.inter m₂).getD k fallback = fallback
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Choice.mk.injEq : ∀ (cnstrs : List Lean.Meta.Grind.EMatch.Cnstr) (gen : ℕ) (assignment : Array Lean.Expr)
  (sources : Lean.PHashSet Lean.Meta.Grind.EMatchDiagNode) (cnstrs_1 : List Lean.Meta.Grind.EMatch.Cnstr) (gen_1 : ℕ)
  (assignment_1 : Array Lean.Expr) (sources_1 : Lean.PHashSet Lean.Meta.Grind.EMatchDiagNode),
  ({ cnstrs := cnstrs, gen := gen, assignment := assignment, sources := sources } =
      { cnstrs := cnstrs_1, gen := gen_1, assignment := assignment_1, sources := sources_1 }) =
    (cnstrs = cnstrs_1 ∧ gen = gen_1 ∧ assignment = assignment_1 ∧ sources = sources_1)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.add : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c₁ c₂ : ℝ}
  {g : α → F} {l : Filter α} {f₁ f₂ : α → E'},
  Asymptotics.IsBigOWith c₁ l f₁ g →
    Asymptotics.IsBigOWith c₂ l f₂ g → Asymptotics.IsBigOWith (c₁ + c₂) l (fun x => f₁ x + f₂ x) g
-- Mathlib.Analysis.Fourier.AddCircle
/-- The subalgebra of `C(AddCircle T, ℂ)` generated by `fourier n` for `n ∈ ℤ` is dense.  -/
fourierSubalgebra_closure_eq_top : ∀ {T : ℝ} [hT : Fact (0 < T)], fourierSubalgebra.topologicalClosure = ⊤
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_sub : ∀ (a b : UInt32), (a - b).toUInt16 = a.toUInt16 - b.toUInt16
-- Mathlib.Algebra.Order.Ring.Defs
one_add_le_one_add_mul_one_sub : ∀ {R : Type u} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {a b c : R},
  a + c + b * c ≤ b → 1 + a ≤ (1 + b) * (1 - c)
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv2.oldAtom : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : ℕ}
  {map : Std.HashMap α ℕ} {a : α} {n : ℕ},
  Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map →
    ∀ (hlt : idx < decls.size),
      decls[idx] = Std.Sat.AIG.Decl.atom a → map[a]? = some n → Std.Sat.AIG.RelabelNat.State.Inv2 decls (idx + 1) map
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.DSimpArgs.mk.sizeOf_spec : ∀ (fvarIds : Array Lean.FVarId) (zetaDeltaAll : Bool),
  sizeOf { fvarIds := fvarIds, zetaDeltaAll := zetaDeltaAll } = 1 + sizeOf fvarIds + sizeOf zetaDeltaAll
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_comap_le : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] {f : F}
  {K : Ideal S} [inst_3 : RingHomClass F R S], Ideal.map f (Ideal.comap f K) ≤ K
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.pushoutObjIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D),
  CategoryTheory.Limits.pushoutObjIso f g d =
    CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation (CategoryTheory.Limits.span f g) d ≪≫
      CategoryTheory.Limits.HasColimit.isoOfNatIso
        (CategoryTheory.Limits.diagramIsoSpan
          ((CategoryTheory.Limits.span f g).comp ((CategoryTheory.evaluation D C).obj d)))
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The quotient map from `A` to `H₀(G, A)`.  -/
groupHomology.H0π : {k G : Type u} →
  [inst : CommRing k] → [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → ModuleCat.of k ↑A ⟶ groupHomology.H0 A
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.addMonoid : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (p : Submodule R M) → AddMonoid (M ⧸ p)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.nsmul_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → AddMonoid (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] (i : ι)
  (x : G i) (n : ℕ), n • ⟦⟨i, x⟩⟧ = ⟦⟨i, n • x⟩⟧
-- Mathlib.Order.SymmDiff
bihimp_le_iff_right : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), bihimp a b ≤ b ↔ Codisjoint a b
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_assoc : ∀ {R : Type u_1} [inst : CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) {Z : CommRingCat}
  (h_1 : (AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk R y)
      (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalkSpecializes h) h_1) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk R x) h_1
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- A splitting of a simplicial object `X` consists of the datum of a sequence
of objects `N`, a sequence of morphisms `ι : N n ⟶ X _⦋n⦌` such that
for all `Δ : SimplexCategoryᵒᵖ`, the canonical map `Splitting.map X ι Δ`
is an isomorphism.  -/
CategoryTheory.SimplicialObject.Splitting : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.SimplicialObject C → Type (max u_1 v_1)
-- Mathlib.Data.Set.MulAntidiagonal
Set.AddAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsCancelAdd α] [AddLeftMono α]
  [AddRightStrictMono α] (s t : Set α) (a : α) {x y : ↑(s.antidiagonal t a)}, (↑x).1 ≤ (↑y).1 → (↑x).2 ≤ (↑y).2 → x = y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionOptions.allCommitCharacters? : Lean.Lsp.CompletionOptions → Option (Array String)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim_hom_app : ∀ (α : Type w₂) {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape α C] (X : α → C),
  (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim α).hom.app X =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit (CategoryTheory.Discrete.functor X))
-- Mathlib.Probability.ProductMeasure
MeasureTheory.piContent.congr_simp : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)}
  (μ μ_1 : (i : ι) → MeasureTheory.Measure (X i)) (e_μ : μ = μ_1)
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)], MeasureTheory.piContent μ = MeasureTheory.piContent μ_1
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.lift_self_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {f : Polynomial R}
  (h : IsAdjoinRoot S f) (x : S), (h.lift (algebraMap R S) h.root ⋯) x = x
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
/-- The identity isometric equivalence between a quadratic form and itself.  -/
QuadraticMap.IsometryEquiv.refl : {R : Type u_2} →
  {M : Type u_4} →
    {N : Type u_9} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → (Q : QuadraticMap R M N) → Q.IsometryEquiv Q
-- Mathlib.Order.Interval.Basic
Interval.coe_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] [inst_1 : DecidableLE α] (f : ι → Interval α),
  ↑(⨅ i, f i) = ⋂ i, ↑(f i)
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The type of objects of the opposite (or "reverse") monoidal category.
Use the notation `Cᴹᵒᵖ`.  -/
CategoryTheory.MonoidalOpposite : Type u₁ → Type u₁
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.ofClass.eq_1 : ∀ {S : Type u_3} {G : Type u_4} [inst : Group G] [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] (s : S),
  Subgroup.ofClass s = { carrier := ↑s, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableInTime.mk.inj : ∀ {α β αΓ βΓ : Type} {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β}
  {toTM2ComputableAux : Turing.TM2ComputableAux αΓ βΓ} {time : ℕ → ℕ}
  {outputsFun :
    (a : α) →
      Turing.TM2OutputsInTime toTM2ComputableAux.tm (List.map toTM2ComputableAux.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux.outputAlphabet.invFun (eb (f a)))) (time (ea a).length)}
  {toTM2ComputableAux_1 : Turing.TM2ComputableAux αΓ βΓ} {time_1 : ℕ → ℕ}
  {outputsFun_1 :
    (a : α) →
      Turing.TM2OutputsInTime toTM2ComputableAux_1.tm (List.map toTM2ComputableAux_1.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux_1.outputAlphabet.invFun (eb (f a)))) (time_1 (ea a).length)},
  { toTM2ComputableAux := toTM2ComputableAux, time := time, outputsFun := outputsFun } =
      { toTM2ComputableAux := toTM2ComputableAux_1, time := time_1, outputsFun := outputsFun_1 } →
    toTM2ComputableAux = toTM2ComputableAux_1 ∧ time = time_1 ∧ outputsFun ≍ outputsFun_1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightShift_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n' + a = n)
  (p q : ℤ) (hpq : p + n' = q) (p' : ℤ) (hp' : p + n = p'),
  (γ.rightShift a n' hn').v p q hpq =
    CategoryTheory.CategoryStruct.comp (γ.v p p' hp') (L.shiftFunctorObjXIso a q p' ⋯).inv
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonInitializeParams.toJson : Lean.Lsp.InitializeParams → Lean.Json
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.topology.eq_1 : ∀ (S : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.ProEt.topology S = (AlgebraicGeometry.Scheme.ProEt.precoverage S).toGrothendieck
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_eq_get!_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a : α}, Std.DTreeMap.Raw.Const.get! t a = (Std.DTreeMap.Raw.Const.get? t a).get!
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- `minIndexable := true`  -/
Lean.Meta.Grind.MinIndexableMode.yes : Lean.Meta.Grind.MinIndexableMode
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toNonUnitalSubring_injective : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing A] [inst_2 : Module R A],
  Function.Injective NonUnitalSubalgebra.toNonUnitalSubring
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.compl_sdiff`. -/
Set.compl_diff : ∀ {α : Type u_1} {s t : Set α}, (t \ s)ᶜ = s ∪ tᶜ
-- Mathlib.Topology.Defs.Induced
WithTopology.equiv_symm_apply_ofTopology : ∀ (X : Type u_1) (t : TopologicalSpace X) (ofTopology : X),
  ((WithTopology.equiv X t).symm ofTopology).ofTopology = ofTopology
-- Mathlib.Tactic.ITauto
/-- A comparator for `AndKind`. (There should really be a derive handler for this.)  -/
Mathlib.Tactic.ITauto.AndKind.cmp : Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.AndKind → Ordering
-- Lean.CoreM
Lean.Core.instMonadRefCoreM : Lean.MonadRef Lean.CoreM
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_iff_eventually_bddAbove : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {f : Filter β} {u : β → α},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u ↔ ∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_ι_image_ι_isoImage_inv_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : (↑U).Opens) {Z : AlgebraicGeometry.Scheme}
  (h : ↑V ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f ∣_ (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage U.ι V).inv h) =
    CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Hom.isoImage ((TopologicalSpace.Opens.map f.base).obj U).ι
            ((TopologicalSpace.Opens.map (f ∣_ U).base).obj V)).inv
        (CategoryTheory.CategoryStruct.comp (f ∣_ U ∣_ V) h))
-- Lean.Server.GoTo
Lean.Server.locationLinksFromCommandInfo : Lean.Elab.CommandInfo → Lean.Server.GoToM (Array Lean.Lsp.LeanLocationLink)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.CustomEliminators.mk.sizeOf_spec : ∀ (map : Lean.SMap (Bool × Array Lean.Name) Lean.Name), sizeOf { map := map } = 1 + sizeOf map
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.instBEqSign.beq.eq_def : ∀ (x y : Float.Model.UnpackedFloat.Sign), Float.Model.UnpackedFloat.instBEqSign.beq x y = (x.ctorIdx == y.ctorIdx)
-- Std.Http.Data.Status
/-- The reason phrase associated with the status code.
 -/
Std.Http.CustomStatus.phrase : Std.Http.CustomStatus → String
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instFromJsonRange.fromJson : Lean.Json → Except String Lean.Lsp.Range
-- Lean.Elab.MacroArgUtil
_private.Lean.Elab.MacroArgUtil.0.Lean.Elab.Command.expandMacroArg.mkSplicePat : Lean.SyntaxNodeKind → Lean.TSyntax `stx → Lean.Term → String → Lean.Elab.Command.CommandElabM Lean.Term
-- Mathlib.CategoryTheory.Action.Monoidal
Action.tensor_ρ : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] {X Y : Action V G} {g : G},
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ρ g =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (X.ρ g) (Y.ρ g)