mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_eq_of_eq_PosPart_sub : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A] [StarOrderedRing A]
  {a c : A}, a = a⁺ - c → autoParam (0 ≤ c) CFC.negPart_eq_of_eq_PosPart_sub._auto_1 → a⁻ = c
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.mk : {C : Type u₁} → C → CategoryTheory.Core C
-- Mathlib.Order.Interval.Multiset
/-- **Alias** of the reverse direction of `Multiset.Ico_eq_zero_iff`. -/
Multiset.Ico_eq_zero : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, ¬a < b → Multiset.Ico a b = 0
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.natCast_opow_omega0 : ∀ {n : ℕ}, 1 < n → ↑n ^ Ordinal.omega0 = Ordinal.omega0
-- Init.Data.UInt.Lemmas
/-- Note that on 32-bit machines we are doing a modulo by zero.  -/
UInt32.toUSize_add : ∀ (a b : UInt32), (a + b).toUSize = (a.toUSize + b.toUSize) % 4294967296
-- Init.System.ST
Void : Type → Type
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- **Alias** of `fderiv_fun_id`.

---

Eta-expanded form of `fderiv_id` -/
fderiv_id' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [T2Space E],
  fderiv 𝕜 (fun x => x) x = ContinuousLinearMap.id 𝕜 E
-- Mathlib.Analysis.MeanInequalitiesPow
ENNReal.rpow_add_rpow_le : ∀ {p q : ℝ} (a b : ENNReal), 0 < p → p ≤ q → (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n},
  i ∉ E.I n → Disjoint (Topology.RelCWComplex.openCell n i) ↑E
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.instLocallyOfFinitePresentationOverSchemeInferInstanceOverClassOfFinite : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) [Finite n],
  AlgebraicGeometry.LocallyOfFinitePresentation (AlgebraicGeometry.AffineSpace n S ↘ S)
-- Mathlib.Data.PNat.Basic
PNat.dvd_iff : ∀ {k m : ℕ+}, k ∣ m ↔ ↑k ∣ ↑m
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_eq_some_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.maxKey? = some t.maxKey!
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Functor.LaxMonoidal.whiskeringRight_ε_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory D] [inst_4 : CategoryTheory.MonoidalCategory E]
  (L : CategoryTheory.Functor D E) [inst_5 : L.LaxMonoidal] (X : C),
  (CategoryTheory.Functor.LaxMonoidal.ε ((CategoryTheory.Functor.whiskeringRight C D E).obj L)).app X =
    CategoryTheory.Functor.LaxMonoidal.ε L
-- Mathlib.Logic.OpClass
instRightCommutativeOfCommutativeOfAssociative : ∀ {α : Sort u} {f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f], RightCommutative f
-- Mathlib.Order.BooleanAlgebra.Defs
Prop.instBooleanAlgebra : BooleanAlgebra Prop
-- Mathlib.Topology.Separation.Basic
t1Space_iff_t0Space_and_r0Space : ∀ {X : Type u_1} [inst : TopologicalSpace X], T1Space X ↔ T0Space X ∧ R0Space X
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.listProd_map_one : ∀ {α : Type u_1} {n : ℕ} {l : List α} {f : α → ℕ}, (∀ x ∈ l, f x ≡ 1 [MOD n]) → (List.map f l).prod ≡ 1 [MOD n]
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.toList.eq_def : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (x x_1 : ι) (x_2 : Monoid.CoprodI.NeWord M x x_1),
  x_2.toList =
    match x, x_1, x_2 with
    | i, .(i), Monoid.CoprodI.NeWord.singleton x a => [⟨i, x⟩]
    | x, x_3, w₁.append _hne w₂ => w₁.toList ++ w₂.toList
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.algebraMap_apply : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : ↥A), (algebraMap (↥A) K) a = ↑a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {c : ℕ},
  (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c)).isEmpty = true
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H0IsoOfIsTrivial_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  (groupCohomology.H0IsoOfIsTrivial A).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.H0Iso A).hom (groupCohomology.shortComplexH0 A).f
-- Mathlib.RingTheory.Binomial
Int.multichoose.eq_def : ∀ (n : ℤ) (k : ℕ),
  n.multichoose k =
    match n with
    | Int.ofNat n => ↑((n + k - 1).choose k)
    | Int.negSucc n => ↑(↑k).negOnePow * ↑((n + 1).choose k)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_inter : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveNeg α] (s t : Finset α), -(s ∩ t) = -s ∩ -t
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β),
  f.comp (RingHom.id α) = f
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.of_injective : ∀ {α : Type u}, Function.Injective FreeAbelianGroup.of
-- Mathlib.Combinatorics.HalesJewett
/-- One line in `ι → α` and one in `ι' → α` together determine a line in `ι ⊕ ι' → α`.  -/
Combinatorics.Line.prod : {α : Type u_5} →
  {ι : Type u_6} → {ι' : Type u_7} → Combinatorics.Line α ι → Combinatorics.Line α ι' → Combinatorics.Line α (ι ⊕ ι')
-- Mathlib.Algebra.Group.Units.Basic
AddRightCancelMonoid.eq_zero_of_add_right : ∀ {α : Type u} [inst : AddRightCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b = 0 → a = 0
-- Mathlib.ModelTheory.Basic
/-- The identity map from a structure to itself.  -/
FirstOrder.Language.Hom.id : (L : FirstOrder.Language) → (M : Type w) → [inst : L.Structure M] → L.Hom M M
-- Aesop.Rule
Aesop.instInhabitedSafeRuleInfo : Inhabited Aesop.SafeRuleInfo
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.IsIndContained.of_isEmpty : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [IsEmpty V], G.IsIndContained H
-- Lean.Meta.SynthInstance
/-- Result kind for `preprocess`  -/
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessKind : Type
-- Mathlib.CategoryTheory.EssentiallySmall
/-- The categorical equivalence between `C` and `Shrink C`, when `C` is small.  -/
CategoryTheory.Shrink.equivalence : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [inst_1 : Small.{w, u} C] → C ≌ Shrink.{w, u} C
-- Mathlib.LinearAlgebra.Dual.BaseChange
IsBaseChange.toDual.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommMonoid W] [inst_4 : Module R W] {A : Type u_4} [inst_5 : CommSemiring A] [inst_6 : Algebra R A]
  [inst_7 : Module A W] [inst_8 : IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j),
  ibc.toDual = ibc.linearMapLeftRightHom (Algebra.linearMap R A)
-- Mathlib.Analysis.Real.Sqrt
Real.lt_sqrt : ∀ {x y : ℝ}, 0 ≤ x → (x < √y ↔ x ^ 2 < y)
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.map_formula' : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (self : L.ElementaryEmbedding M N) ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M),
  φ.Realize (↑self ∘ x) ↔ φ.Realize x
-- Mathlib.LinearAlgebra.Projection
LinearMap.range_ofIsCompl : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (hpq : IsCompl p q) {φ : ↥p →ₗ[R] F}
  {ψ : ↥q →ₗ[R] F}, (LinearMap.ofIsCompl hpq φ ψ).range = φ.range ⊔ ψ.range
-- Mathlib.Order.Defs.Unbundled
asymm_def : ∀ {α : Sort u_1} {r : α → α → Prop}, Std.Asymm r ↔ ∀ ⦃a b : α⦄, r a b → ¬r b a
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_vadd_apply : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p : P1) (v : V1) (c : k), (AffineMap.lineMap p (v +ᵥ p)) c = c • v +ᵥ p
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ico_add_one_right_eq_Icc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] [NoMaxOrder α] (a b : α), Finset.Ico a (b + 1) = Finset.Icc a b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.contains_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  (Std.ExtDTreeMap.Const.alter t k f).contains k = (f (Std.ExtDTreeMap.Const.get? t k)).isSome
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_le_cons_iff : ∀ {α : Type u_1} {s t : Multiset α} (a : α), a ::ₘ s ≤ a ::ₘ t ↔ s ≤ t
-- Mathlib.Algebra.Group.Hom.Basic
OneHom.div_apply : ∀ {M : Type u_8} {N : Type u_9} [inst : One M] [inst_1 : DivisionMonoid N] (f g : OneHom M N) (x : M),
  (f / g) x = f x / g x
-- Mathlib.Util.Notation3
/-- Variant of `matchScoped` after some number of `binders` have already been captured.  -/
_private.Mathlib.Util.Notation3.0.Mathlib.Notation3.matchScoped.go : Lean.Name →
  Lean.Name →
    Mathlib.Notation3.Matcher →
      Array (Lean.TSyntax `Batteries.ExtendedBinder.extBinderParenthesized) →
        Mathlib.Notation3.MatchState → Lean.PrettyPrinter.Delaborator.DelabM Mathlib.Notation3.MatchState
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) {Z : C} (h : X.obj (Opposite.op { len := n + 1 }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.σ j) (CategoryTheory.CategoryStruct.comp (X.δ i) h) =
    CategoryTheory.CategoryStruct.comp (X.δ (i.pred ⋯)) (CategoryTheory.CategoryStruct.comp (X.σ (j.castLT ⋯)) h)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the auxiliary object of left fractions  -/
CategoryTheory.MorphismProperty.LeftFraction₃.Y' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction₃ X Y → C
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_eq_head!_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t.minKey! = t.keys.head!
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The ring isomorphism between multivariable polynomials in no variables
and the ground ring.  -/
MvPolynomial.isEmptyRingEquiv : (R : Type u) → (σ : Type u_1) → [inst : CommSemiring R] → [IsEmpty σ] → MvPolynomial σ R ≃+* R
-- Mathlib.Data.FunLike.IsApply
/-- `IsInvApply F α β` states for all `f : F` and `x : α`, `f⁻¹ x = (f x)⁻¹`.  -/
IsInvApply : (F : Type u_1) → (α : outParam (Type u_2)) → (β : outParam (Type u_3)) → [FunLike F α β] → [Inv β] → [Inv F] → Prop
-- Mathlib.ModelTheory.Encoding
/-- An encoding of terms as lists.  -/
FirstOrder.Language.Term.encoding : {L : FirstOrder.Language} → {α : Type u'} → Computability.Encoding (L.Term α) (α ⊕ (i : ℕ) × L.Functions i)
-- Mathlib.Algebra.RingQuot
RingQuot.liftAlgHom_unique : ∀ (S : Type uS) [inst : CommSemiring S] {A : Type uA} [inst_1 : Semiring A] [inst_2 : Algebra S A] {B : Type u₄}
  [inst_3 : Semiring B] [inst_4 : Algebra S B] (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y : A⦄, s x y → f x = f y)
  (g : RingQuot s →ₐ[S] B), g.comp (RingQuot.mkAlgHom S s) = f → g = (RingQuot.liftAlgHom S) ⟨f, w⟩
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveMessageProps.mk : Lean.Server.WithRpcRef Lean.MessageData → ProofWidgets.InteractiveMessageProps
-- Init.Data.String.Basic
String.copy_comp_toSlice : String.Slice.copy ∘ String.toSlice = id
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.toInt'.processSub : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Lean.Expr × Lean.Expr)
-- Aesop.Tree.Data
Aesop.Goal.successProbability : Aesop.Goal → Aesop.Percent
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.isCompl_ker : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (self : ImplicitFunctionData 𝕜 E F G),
  IsCompl (↑self.leftDeriv).ker (↑self.rightDeriv).ker
-- Lean.Parser.Basic
Lean.Parser.optionalInfo : Lean.Parser.ParserInfo → Lean.Parser.ParserInfo
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.toRatVec_inj : ∀ {ι : Type u_3} (x y : ι → ℕ), toRatVec✝ x = toRatVec✝ y ↔ x = y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_le_size_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t.size ≤ (t.erase k).size + 1
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.hasSum : ∀ {α : Type u_1} {f : α → ENNReal}, HasSum f (⨆ s, ∑ a ∈ s, f a)
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂)
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)]
  [h₁ : HomotopicalAlgebra.Cofibration f₁] [h₂ : HomotopicalAlgebra.Cofibration f₂]
  [inst_5 : CategoryTheory.Limits.HasBinaryCoproduct X₁ X₂] [inst_6 : CategoryTheory.Limits.HasBinaryCoproduct Y₁ Y₂],
  HomotopicalAlgebra.Cofibration (CategoryTheory.Limits.coprod.map f₁ f₂)
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.Factors.finrank_pow_ramificationIdx : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : IsDedekindDomain S] [p.IsMaximal]
  (P : ↥(UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset),
  Module.finrank (R ⧸ p) (S ⧸ ↑P ^ p.ramificationIdx' ↑P) = p.ramificationIdx' ↑P * p.inertiaDeg' ↑P
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.fold_eq_foldl_keys : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {δ : Type w},
  m.WF → ∀ {f : δ → α → δ} {init : δ}, Std.DHashMap.Raw.fold (fun d a x => f d a) init m = List.foldl f init m.keys
-- Mathlib.Algebra.Lie.Rank
LieAlgebra.isRegular_def : ∀ (R : Type u_1) {L : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] (x : L),
  LieAlgebra.IsRegular R x ↔ (LinearMap.charpoly ((LieAlgebra.ad R L) x)).coeff (LieAlgebra.rank R L) ≠ 0
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.leAtTop_of_not_NeBot : ∀ {β : Type u_2} (L : SummationFilter β), ¬L.NeBot → L.LeAtTop
-- Mathlib.RingTheory.Algebraic.Integral
/-- An element of an algebra over a field is algebraic if and only if it is integral.  -/
isAlgebraic_iff_isIntegral : ∀ {K : Type u} {A : Type v} [inst : Field K] [inst_1 : Ring A] [inst_2 : Algebra K A] {x : A},
  IsAlgebraic K x ↔ IsIntegral K x
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv : ∀ (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) (i : D.J),
  CategoryTheory.CategoryStruct.comp (D.toSheafedSpaceGlueData.ι i) D.isoSheafedSpace.inv =
    AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom (D.ι i)
-- Mathlib.Order.Filter.Prod
Filter.tendsto_prodAssoc_symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ},
  Filter.Tendsto (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) ((f ×ˢ g) ×ˢ h)
-- Mathlib.Order.RelSeries
/-- In a non-trivial series `p`, the last element of `p.eraseLast` is related to `p.last`  -/
RelSeries.eraseLast_last_rel_last : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.length ≠ 0 → (p.eraseLast.last, p.last) ∈ r
-- Mathlib.RingTheory.Valuation.Basic
Valuation.ofAddValuation_apply : ∀ {R : Type u_3} {Γ₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  (v : AddValuation R (Additive Γ₀)ᵒᵈ) (r : R), (Valuation.ofAddValuation v) r = Additive.toMul (OrderDual.ofDual (v r))
-- Mathlib.Topology.Category.LightProfinite.AsLimit
/-- An abbreviation for the `n`th component of `S.diagram`.  -/
LightProfinite.component : LightProfinite → ℕ → LightProfinite
-- Mathlib.Algebra.Field.ULift
ULift.down_nnratCast : ∀ {α : Type u} [inst : NNRatCast α] (q : ℚ≥0), (↑q).down = ↑q
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForILeansParams.uri? : Lean.Lsp.WaitForILeansParams → Option Lean.Lsp.DocumentUri
-- Mathlib.Data.List.Sort
List.orderedInsert_cons : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] (a b : α) (l : List α),
  List.orderedInsert r a (b :: l) = if r a b then a :: b :: l else b :: List.orderedInsert r a l
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
Lean.Elab.Structural.instReprRecArgInfo : Repr Lean.Elab.Structural.RecArgInfo
-- Mathlib.CategoryTheory.Action.Limits
Action.sub_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {X Y : Action V G} (f g : X ⟶ Y), (f - g).hom = f.hom - g.hom
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.mk_inv_tmul : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} {W : Type u_9} [inst : CommRing k] [inst_1 : Group G]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  (ρ : Representation k G V) (τ : Representation k G W) (x : V) (y : W) (g : G),
  (Representation.Coinvariants.mk (ρ.tprod τ)) ((ρ g⁻¹) x ⊗ₜ[k] y) =
    (Representation.Coinvariants.mk (ρ.tprod τ)) (x ⊗ₜ[k] (τ g) y)
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- `R` is a right adjoint  -/
CategoryTheory.MonadicRightAdjoint.adj : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {R : CategoryTheory.Functor D C} →
          [self : CategoryTheory.MonadicRightAdjoint R] → CategoryTheory.MonadicRightAdjoint.L R ⊣ R
-- Std.Http.Data.Body.Stream
/-- Creates a body from a producer function.
Returns the stream immediately and runs `gen` in a detached task.
The channel is always closed when `gen` returns or throws.
Errors from `gen` are not rethrown here; consumers observe end-of-stream via `recv = none`.
 -/
Std.Http.Body.stream : (Std.Http.Body.Stream → Std.Async.Async Unit) → Std.Async.Async Std.Http.Body.Stream
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.homeoOfIso_apply : ∀ {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ≅ Y) (a : ↑X.toTop),
  (CompHausLike.homeoOfIso f) a = (CategoryTheory.ConcreteCategory.hom f.hom.hom) a
-- Mathlib.Data.Finsupp.ToDFinsupp
DFinsupp.toFinsupp_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddZeroClass M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f g : Π₀ (x : ι), M), (f + g).toFinsupp = f.toFinsupp + g.toFinsupp
-- Mathlib.RingTheory.EssentialFiniteness
RingHom.FiniteType.essFiniteType : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, f.FiniteType → f.EssFiniteType
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.isPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} (f : Y ⟶ X) (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g],
  CategoryTheory.IsPullback (CategoryTheory.ChosenPullbacksAlong.fst f g) (CategoryTheory.ChosenPullbacksAlong.snd f g)
    f g
-- Std.Time.Format.Modifier
/-- `X`: Zone offset with 'Z' for zero (e.g., Z, -08, -0830, -08:30).
 -/
Std.Time.Modifier.X : Std.Time.OffsetX → Std.Time.Modifier
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasDerivAt.cpow_const : ∀ {f : ℂ → ℂ} {f' x c : ℂ},
  HasDerivAt f f' x → f x ∈ Complex.slitPlane → HasDerivAt (fun x => f x ^ c) (c * f x ^ (c - 1) * f') x
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.convexOn_Gamma : ConvexOn ℝ (Set.Ioi 0) Real.Gamma
-- Mathlib.RingTheory.Flat.Equalizer
/-- (Implementation): Inverse for `LinearMap.tensorEqLocusEquiv`.  -/
LinearMap.tensorEqLocusInv : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    {N : Type u_4} →
                      {P : Type u_5} →
                        [inst_7 : AddCommGroup N] →
                          [inst_8 : AddCommGroup P] →
                            [inst_9 : Module R N] →
                              [inst_10 : Module R P] →
                                (f g : N →ₗ[R] P) →
                                  [Module.Flat R M] →
                                    ↥(((TensorProduct.AlgebraTensorModule.lTensor S M) f).eqLocus
                                          ((TensorProduct.AlgebraTensorModule.lTensor S M) g)) →ₗ[S]
                                      TensorProduct R M ↥(f.eqLocus g)
-- Mathlib.Order.GaloisConnection.Basic
Nat.galoisConnection_mul_div : ∀ {k : ℕ}, 0 < k → GaloisConnection (fun n => n * k) fun n => n / k
-- Init.Data.Vector.Lemmas
Vector.decide_forall_mem : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Prop} [inst : DecidablePred p],
  decide (∀ x ∈ xs, p x) = xs.all fun b => decide (p b)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.mem_cliqueFinset_iff : ∀ {α : Type u_1} {G : SimpleGraph α} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : DecidableRel G.Adj] {n : ℕ}
  {s : Finset α}, s ∈ G.cliqueFinset n ↔ G.IsNClique n s
-- Mathlib.RingTheory.DiscreteValuationRing.TFAE
IsDedekindDomain.isPrincipalIdealRing : ∀ (R : Type u_1) [inst : CommRing R] [IsLocalRing R] [IsDedekindDomain R], IsPrincipalIdealRing R
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPullback.flip : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square C},
  sq.IsPullback → sq.flip.IsPullback
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.modifyState.unsafe_4 : {σ : Type} → Lean.EnvExtension σ → Lean.Environment → (σ → σ) → Array Lean.EnvExtensionState
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
ModelWithCorners.mdifferentiableOn_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H),
  MDiff[Set.range ↑I] ↑I.symm
-- Init.Data.Bool
Bool.eq_self_and : ∀ {a b : Bool}, a = (a && b) ↔ a = true → b = true
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.coordinate_eval_3 : ∀ {a0 a1 a2 a3 : ℤ} {t : List ℤ},
  (Lean.Omega.LinearCombo.coordinate 3).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: t)) = a3