mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instIsGEObjSingleFunctor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : C) (n : ℤ), ((DerivedCategory.Plus.singleFunctor C n).obj X).IsGE n
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- Right-multiplying by `γ ∈ SL(2, ℤ)` sends `gammaSet N a` to `gammaSet N (a ᵥ* γ)`.  -/
EisensteinSeries.vecMul_SL2_mem_gammaSet : ∀ {N r : ℕ} {a : Fin 2 → ZMod N} [NeZero r] {v : Fin 2 → ℤ},
  v ∈ EisensteinSeries.gammaSet N r a →
    ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ),
      Matrix.vecMul v ↑γ ∈
        EisensteinSeries.gammaSet N r (Matrix.vecMul a ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ))
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.fiberInclusion_comp_eq_const : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮},
  CategoryTheory.Functor.Fiber.fiberInclusion.comp p = (CategoryTheory.Functor.const (p.Fiber S)).obj S
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.backend : Lean.ExternEntry → Lean.Name
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_lt_add_iff_of_right_lt_aleph0 : ∀ {a b c : Cardinal.{u_1}}, c < Cardinal.aleph0 → (a + c < b + c ↔ a < b)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_eq_get_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α} {h : a ∈ t}, Std.DTreeMap.Const.get t a h = (Std.DTreeMap.Const.get? t a).get ⋯
-- Init.Data.Float.Model.Float
/-- Converts a `UInt32` to a `Float.Model`, returning positive zero on zero.  -/
Float.Model.ofUInt32 : UInt32 → Float.Model
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.NewDecl.motive.sizeOf_spec : ∀ (decl : Lean.LocalDecl) (motiveIdx : ℕ) (vars : Array Lean.FVarId),
  sizeOf (Lean.Meta.IndPredBelow.NewDecl.motive✝ decl motiveIdx vars) = 1 + sizeOf decl + sizeOf motiveIdx + sizeOf vars
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_set_inter : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s t : Set β} {a : α},
  a +ᵥ s ∩ t = (a +ᵥ s) ∩ (a +ᵥ t)
-- Init.Data.BitVec.Lemmas
BitVec.getElem_zero_ofNat_one : ∀ {w : ℕ} (h : 0 < w), (1#w)[0] = true
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.FunctorialFactorizationData.hi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  (self : W₁.FunctorialFactorizationData W₂) (f : CategoryTheory.Arrow C), W₁ (self.i.app f)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.map_apply : ∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup H] (b : FreeAddGroupBasis ι G)
  (e : G ≃+ H) (x : ι), (b.map e) x = e (b x)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.toLp_smul : ∀ {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : NormedRing 𝕜] [inst_3 : Module 𝕜 E] [inst_4 : IsBoundedSMul 𝕜 E]
  (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.MemLp (⇑f) p μ) (c : 𝕜), (c • f).toLp ⋯ = c • f.toLp hf
-- Mathlib.Data.List.AList
AList.mem_mk : ∀ {α : Type u} {β : α → Type v} {l : List (Sigma β)} {h : l.NodupKeys} {x : α},
  x ∈ { entries := l, nodupKeys := h } ↔ x ∈ l.keys
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_X : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))) (n : α),
  (((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.obj P).X n).X = P.X.X n
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.alter.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (l' : Std.DTreeMap.Internal.Impl α fun x => β)
  (motive : Std.DTreeMap.Internal.Impl.SizedBalancedTree α (fun x => β) (l'.size - 1) (l'.size + 1) → Sort u_3)
  (d : Std.DTreeMap.Internal.Impl α fun x => β) (hd : d.Balanced) (hd'₁ : l'.size - 1 ≤ d.size)
  (hd'₂ : d.size ≤ l'.size + 1)
  (h_1 :
    (d : Std.DTreeMap.Internal.Impl α fun x => β) →
      (hd : d.Balanced) →
        (hd'₁ : l'.size - 1 ≤ d.size) →
          (hd'₂ : d.size ≤ l'.size + 1) →
            motive { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ }),
  (match { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ } with
    | { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ } => h_1 d hd hd'₁ hd'₂) =
    h_1 d hd hd'₁ hd'₂
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.splitMono_f_retraction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s : S.Splitting), s.splitMono_f.retraction = s.r
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.subset_pointwise_smul_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Group α] [inst_2 : MulDistribMulAction α G] {a : α}
  {S T : Subgroup G}, S ≤ a • T ↔ a⁻¹ • S ≤ T
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
/-- A recursor for `DegLex`. Use as `induction x`.  -/
DegLex.rec : {α : Type u_1} → {β : DegLex α → Sort u_2} → ((a : α) → β (toDegLex a)) → (a : DegLex α) → β a
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- If `P` is a sheaf for `R`, it is separated for `R`.  -/
CategoryTheory.Presieve.IsSheafFor.isSeparatedFor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X}, CategoryTheory.Presieve.IsSheafFor P R → CategoryTheory.Presieve.IsSeparatedFor P R
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_X_pow_add_one : ∀ {R : Type u} [inst : Semiring R] {n : ℕ}, 0 < n → (Polynomial.X ^ n + 1).leadingCoeff = 1
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.isGE_cokernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ),
  (∀ i < n, QuasiIsoAt f i) →
    ∀ [CategoryTheory.Mono f] [CategoryTheory.Mono (HomologicalComplex.homologyMap f n)],
      (CategoryTheory.Limits.cokernel f).IsGE n
-- Init.Data.Array.BasicAux
_private.Init.Data.Array.BasicAux.0.List.toArrayAux.eq_def : ∀ {α : Type u_1} (x : List α) (x_1 : Array α),
  x.toArrayAux x_1 =
    match x, x_1 with
    | [], xs => xs
    | a :: as, xs => as.toArrayAux (xs.push a)
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.range_lift : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  {f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)} [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] {P : Type u₁} [inst_5 : L.Structure P]
  (g : (i : ι) → L.Embedding (G i) P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x),
  (FirstOrder.Language.DirectLimit.lift L ι G f g Hg).toHom.range = ⨆ i, (g i).toHom.range
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_eq_sum_genWeightSpaceOf : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsDomain R] [IsPrincipalIdealRing R] [inst_10 : Module.IsTorsionFree R M]
  [inst_11 : IsNoetherian R M] [LieModule.IsTriangularizable R L M] (z : L),
  LieModule.traceForm R L M = ∑ χ ∈ ⋯.toFinset, LieModule.traceForm R L ↥(LieModule.genWeightSpaceOf M χ z)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.ones_blocks : ∀ (n : ℕ), (Composition.ones n).blocks = List.replicate n 1
-- Lean.Meta.Constructions.BRecOn
Lean.mkBelow : Lean.Name → Lean.MetaM Unit
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_injective : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R], Function.Injective HahnSeries.coeff
-- Mathlib.CategoryTheory.Monoidal.Skeleton
/-- If `C` is braided and skeletal, it is a commutative monoid.  -/
CategoryTheory.commMonoidOfSkeletalBraided : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.Skeletal C → CommMonoid C
-- Mathlib.Computability.EpsilonNFA
εNFA.evalFrom_empty : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) (x : List α), M.evalFrom ∅ x = ∅
-- Init.Data.BitVec.Lemmas
BitVec.reverse_replicate : ∀ {w n : ℕ} {x : BitVec w}, (BitVec.replicate n x).reverse = BitVec.replicate n x.reverse
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_const_mul_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) (f : α → ENNReal),
  r * ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), r * f a ∂μ
-- Mathlib.Algebra.Module.GradedModule
/-- For graded monoid `A` and a graded module `M` over `A`. `Gmodule.smulAddMonoidHom` is the
`⨁ᵢ Aᵢ`-scalar multiplication on `⨁ᵢ Mᵢ` induced by `gsmul_hom`.  -/
DirectSum.Gmodule.smulAddMonoidHom : {ιA : Type u_1} →
  {ιB : Type u_2} →
    (A : ιA → Type u_3) →
      (M : ιB → Type u_4) →
        [inst : AddMonoid ιA] →
          [inst_1 : VAdd ιA ιB] →
            [inst_2 : (i : ιA) → AddCommMonoid (A i)] →
              [inst_3 : (i : ιB) → AddCommMonoid (M i)] →
                [DecidableEq ιA] →
                  [DecidableEq ιB] →
                    [inst_6 : GradedMonoid.GMonoid A] →
                      [DirectSum.Gmodule A M] →
                        (DirectSum ιA fun i => A i) →+ (DirectSum ιB fun i => M i) →+ DirectSum ιB fun i => M i
-- Std.Time.DateTime.PlainDateTime
/-- Subtracts a `Day.Offset` from a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.subDays : Std.Time.PlainDateTime → Std.Time.Day.Offset → Std.Time.PlainDateTime
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving AlgebraicGeometry.IsOpenImmersion
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
HasFDerivWithinAt.exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E}
  {s : Set E}, HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => Real.exp (f x)) (Real.exp (f x) • f') s x
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
CategoryTheory.ShiftedHom.opEquiv'_zero_add_symm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y : C} (a : ℤ)
  (f : Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ 0).obj (Opposite.op X)),
  (CategoryTheory.ShiftedHom.opEquiv' 0 a a ⋯).symm f =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero Cᵒᵖ ℤ).hom.app (Opposite.op X)).unop f.unop
-- Init.Data.String.Basic
String.Slice.Pos.cast_eq_startPos : ∀ {s t : String.Slice} {p : s.Pos} {hst : s.copy = t.copy}, p.cast hst = t.startPos ↔ p = s.startPos
-- Mathlib.Algebra.GroupWithZero.Basic
pow_eq_zero_iff : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀], n ≠ 0 → (a ^ n = 0 ↔ a = 0)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_inv : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (e : P ≃ᵃⁱ[𝕜] P),
  ⇑e⁻¹ = ⇑e.symm
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.rightAdjointUniq_trans : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D}
  {G G' G'' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G''),
  CategoryTheory.CategoryStruct.comp (adj1.rightAdjointUniq adj2).hom (adj2.rightAdjointUniq adj3).hom =
    (adj1.rightAdjointUniq adj3).hom
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.goCache.match_3.eq_2 : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (motive : Option (aig.RefVec w) → Sort u_1)
  (h_1 : (vec : aig.RefVec w) → motive (some vec)) (h_2 : Unit → motive none),
  (match none with
    | some vec => h_1 vec
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.RingCat.Colimits.descFunLift.match_1.eq_5 : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (motive : RingCat.Colimits.Prequotient F → Sort u_2) (x y : RingCat.Colimits.Prequotient F)
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (RingCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive RingCat.Colimits.Prequotient.zero) (h_3 : Unit → motive RingCat.Colimits.Prequotient.one)
  (h_4 : (x : RingCat.Colimits.Prequotient F) → motive x.neg)
  (h_5 : (x y : RingCat.Colimits.Prequotient F) → motive (x.add y))
  (h_6 : (x y : RingCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match x.add y with
    | RingCat.Colimits.Prequotient.of j x => h_1 j x
    | RingCat.Colimits.Prequotient.zero => h_2 ()
    | RingCat.Colimits.Prequotient.one => h_3 ()
    | x.neg => h_4 x
    | x.add y => h_5 x y
    | x.mul y => h_6 x y) =
    h_5 x y
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_div : ∀ (a b : UInt64), a < 65536 → b < 65536 → (a / b).toUInt16 = a.toUInt16 / b.toUInt16
-- Mathlib.Order.RelIso.Basic
/-- If `f` is injective, then it is a relation embedding from the
preimage relation of `s` to `s`.  -/
RelEmbedding.preimage : {α : Type u_1} → {β : Type u_2} → (f : α ↪ β) → (s : β → β → Prop) → ⇑f ⁻¹'o s ↪r s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false →
    ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.find?_toArray_eq_none_iff_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, Array.find? (fun x => cmp x.fst k == Ordering.eq) t.toArray = none ↔ k ∉ t
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_union_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} (mem : k ∈ t₂), (t₁ ∪ t₂).getKey k ⋯ = t₂.getKey k mem
-- Mathlib.Order.Hom.Bounded
TopHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Top α] [inst_1 : Top β] [inst_2 : Top γ]
  [inst_3 : Top δ] (f : TopHom γ δ) (g : TopHom β γ) (h : TopHom α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.rightRelDecidable.eq_1 : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) [inst_1 : DecidablePred fun x => x ∈ s] (x y : α),
  QuotientGroup.rightRelDecidable s x y = ⋯.mpr (inst_1 (y * x⁻¹))
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_zero_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.covariance 0 Y μ = 0
-- Init.Data.Option.Lemmas
Option.merge_eq_or_eq : ∀ {α : Type u_1} {f : α → α → α},
  (∀ (a b : α), f a b = a ∨ f a b = b) → ∀ (o₁ o₂ : Option α), Option.merge f o₁ o₂ = o₁ ∨ Option.merge f o₁ o₂ = o₂
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.stalkMap_germ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y) (x : ↑↑X)
  (hx : (CategoryTheory.ConcreteCategory.hom α.base) x ∈ U),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom α.base) x) hx)
      (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x) =
    CategoryTheory.CategoryStruct.comp (α.c.app (Opposite.op U))
      (X.presheaf.germ ((TopologicalSpace.Opens.map α.base).obj U) x hx)
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.trans : ∀ {M : Type u_1} [inst : Monoid M] {x y z : M}, Associated x y → Associated y z → Associated x z
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_nsmul_add' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIocMod hp (m • p + a) b = m • p + toIocMod hp a b
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.mapRingEquiv_symm_apply : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] (e : K ≃+* L) (x : NumberField.RingOfIntegers L),
  ↑((NumberField.RingOfIntegers.mapRingEquiv e).symm x) = e.symm ↑x
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.skipPrefix?_char_eq_some_iff : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  s.skipPrefix? c = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ s.startPos.get h = c
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.FormallyUnramified.isStableUnderBaseChange : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
-- Std.Async.Signal
/-- Background read attempted from control terminal.
 -/
Std.Async.Signal.sigttin : Std.Async.Signal
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesLE_eq_filter_Icc_zero : ∀ (n : ℕ), n.primesLE = Finset.filter Nat.Prime (Finset.Icc 0 n)
-- Init.Data.Vector.Lemmas
Vector.toList_emptyWithCapacity : ∀ {α : Type u_1} {cap : ℕ}, (Vector.emptyWithCapacity cap).toList = []
-- Init.Data.UInt.Lemmas
USize.ofNat_bitVecToNat : ∀ (n : BitVec System.Platform.numBits), USize.ofNat n.toNat = { toBitVec := n }
-- Init.Data.List.ToArray
List.zipWithMAux_toArray_succ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u} {m : Type u → Type v} [inst : Monad m] (as : List α) (bs : List β)
  (f : α → β → m γ) (i : ℕ) (xs : Array γ),
  as.toArray.zipWithMAux bs.toArray f (i + 1) xs = as.tail.toArray.zipWithMAux bs.tail.toArray f i xs
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The cosine of the angle between three points is 1 if and only if the angle is 0.  -/
EuclideanGeometry.cos_eq_one_iff_angle_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  Real.cos (EuclideanGeometry.angle p₁ p₂ p₃) = 1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = 0
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The bottom left map in the forward hexagon identity.  -/
CategoryTheory.BraidedCategory.ofBifunctor.Forward.firstMap₃ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁ C ⟶ CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁' C
-- Batteries.Recycling.RBTree.WF
/-- The `ins` function preserves the ordering invariants.  -/
RBTree.RBNode.Ordered.ins : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBTree.RBNode α},
  RBTree.RBNode.Ordered cmp t → RBTree.RBNode.Ordered cmp (RBTree.RBNode.ins cmp x t)
-- Mathlib.Algebra.Order.AddGroupWithTop
add_right_injective_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommMonoidWithTop α] (b : α), b ≠ ⊤ → Function.Injective fun x => b + x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.eq_of_revlex : ∀ {m₁ m₂ : Lean.Grind.CommRing.Mon}, m₁.revlex m₂ = Ordering.eq → m₁ = m₂
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Generate a suggestion for inserting `tac`, with message `html`.
The button is `[apply]` if the tactic does not close the goal, and `[done]` if it is closing.  -/
Mathlib.Tactic.ClickSuggestions.mkSuggestion : Lean.TSyntax `tactic →
  ProofWidgets.Html → optParam Bool false → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM ProofWidgets.Html
-- Mathlib.Algebra.Category.Grp.FiniteGrp
/-- The category of finite additive groups.  -/
FiniteAddGrp : Type (u + 1)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom'' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)),
  (∀ (i₁ i₂ i₃ : ι),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯
            ⋯)
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯
            ⋯) =
        CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯
          ⋯) →
    ∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃)
      (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
      (hf₃ : CategoryTheory.CategoryStruct.comp f₃ (f i₃) = q),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q f₁ f₂ ⋯ ⋯)
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q f₂ f₃ ⋯ ⋯) =
        CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom q f₁ f₃ ⋯ ⋯
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.vecMulVec_empty : ∀ {α : Type u} {m' : Type uₘ} [inst : NonUnitalNonAssocSemiring α] (v : m' → α) (w : Fin 0 → α),
  Matrix.vecMulVec v w = Matrix.of fun x => ![]
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.cons : ∀ {V : Type u} {G : SimpleGraph V} {u u' v : V} {w : G.Walk u' v},
  w.IsTrail → ∀ (hu : G.Adj u u'), s(u, u') ∉ w.edges → (SimpleGraph.Walk.cons hu w).IsTrail
-- Mathlib.Analysis.Calculus.FDeriv.Norm
fderiv_norm_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : E) (t : ℝ),
  fderiv ℝ (fun x => ‖x‖) (t • x) = ↑(SignType.sign t) • fderiv ℝ (fun x => ‖x‖) x
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lim_mul : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [inst_5 : CauSeq.IsComplete β abv] (f : CauSeq β abv)
  (x : β), f.lim * x = (f * CauSeq.const abv x).lim
-- Std.Async.Basic
Std.Async.MonadAsync.mk : {t m : Type → Type} →
  ({α : Type} → m α → optParam Task.Priority Task.Priority.default → m (t α)) → Std.Async.MonadAsync t m
-- Mathlib.Algebra.Module.Equiv.Basic
Units.symm_mulRightLinearEquiv_apply : ∀ (R : Type u_9) {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (a : Aˣ) (x : A), (Units.mulRightLinearEquiv R a).symm x = x * ↑a⁻¹