mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_sum : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} {ι : Type u_1} (f : ι → (M ⟶ N)) (s : Finset ι),
  ModuleCat.Hom.hom (∑ i ∈ s, f i) = ∑ i ∈ s, ModuleCat.Hom.hom (f i)
-- Lean.Compiler.InitAttr
Lean.declareBuiltin : Lean.Name → Lean.Expr → Lean.CoreM Unit
-- Mathlib.Analysis.CStarAlgebra.Classes
/-- The class of unital commutative (complex) C⋆-algebras.  -/
CommCStarAlgebra : Type u_1 → Type u_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
          k ∈ List.map Prod.fst l → ∀ {h' : k' ∈ t.insertMany l}, (t.insertMany l).getKey k' h' = k
-- Mathlib.Data.Nat.Factorization.Root
Nat.ceilRoot_zero_left : ∀ (a : ℕ), Nat.ceilRoot 0 a = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_union_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ ∪ t₂ ↔ k ∈ t₁ ∨ k ∈ t₂
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- This version of `rpow_le_rpow_of_exponent_ge` allows `x = 0` but requires `0 ≤ z`.
See also `rpow_le_rpow_of_exponent_ge_of_imp` for the most general version.  -/
Real.rpow_le_rpow_of_exponent_ge' : ∀ {x y z : ℝ}, 0 ≤ x → x ≤ 1 → 0 ≤ z → z ≤ y → x ^ y ≤ x ^ z
-- Lean.Parser.Do
Lean.Parser.Term.nestedAction : Lean.Parser.Parser
-- Mathlib.Topology.PartitionOfUnity
/-- If `X` is a normal topological space and `U i`, `i : ι`, is a locally finite open covering of a
closed set `s`, then there exists a `BumpCovering ι X s` that is subordinate to `U`. If `X` is a
paracompact space, then the assumption `hf : LocallyFinite U` can be omitted, see
`BumpCovering.exists_isSubordinate`. This version assumes that `p : (X → ℝ) → Prop` is a predicate
that satisfies Urysohn's lemma, and provides a `BumpCovering` such that each function of the
covering satisfies `p`.  -/
BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [NormalSpace X] (p : (X → ℝ) → Prop),
  (∀ (s t : Set X),
      IsClosed s →
        IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1) →
    IsClosed s →
      ∀ (U : ι → Set X),
        (∀ (i : ι), IsOpen (U i)) → LocallyFinite U → s ⊆ ⋃ i, U i → ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
-- Mathlib.Algebra.Group.Units.Hom
/-- If a map `g : M → Nˣ` agrees with a homomorphism `f : M →* N`, then
this map is a monoid homomorphism too.  -/
Units.liftRight : {M : Type u} →
  {N : Type v} →
    [inst : Monoid M] → [inst_1 : Monoid N] → (f : M →* N) → (g : M → Nˣ) → (∀ (x : M), ↑(g x) = f x) → M →* Nˣ
-- Init.PropLemmas
decide_implies : ∀ (u v : Prop) [duv : Decidable (u → v)] [du : Decidable u] {dv : u → Decidable v},
  decide (u → v) = if h : u then decide v else true
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.modifyKey : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [LawfulBEq α] → (k : α) → (β k → β k) → List ((a : α) × β a) → List ((a : α) × β a)
-- Mathlib.Data.FinEnum
FinEnum.card_ofList : ∀ {α : Type u} [inst : DecidableEq α] (xs : List α) (h : ∀ (x : α), x ∈ xs), FinEnum.card α = xs.dedup.length
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.leadingCoeff_top : ∀ {R : Type u} [inst : CommSemiring R], ⊤.leadingCoeff = ⊤
-- Mathlib.Analysis.Fourier.AddCircle
tsum_sq_fourierCoeff : ∀ {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)),
  ∑' (i : ℤ), ‖fourierCoeff (↑↑f) i‖ ^ 2 = ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂AddCircle.haarAddCircle
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_7} {n : ℕ} {x : 𝕜} {f : ι → 𝕜 → F} {I : Finset ι} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      (∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n) (f i) s x) →
        iteratedDerivWithin n (∑ i ∈ I, f i) s x = ∑ i ∈ I, iteratedDerivWithin n (f i) s x
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- The canonical relation on the path category of a category:
two paths are related if they compose to the same morphism.  -/
CategoryTheory.pathsHomRel : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → HomRel (CategoryTheory.Paths C)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
Std.IterM.toTake.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] [inst_1 : Std.Iterators.Finite α m]
  (it : Std.IterM m β), it.toTake = { internalState := { countdown := 0, inner := it, finite := ⋯ } }
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.instPartialOrder : (G : Type u) → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → PartialOrder (ClosedAddSubgroup G)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.map_pre : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] {G : CategoryTheory.Functor J C} (α : F ⟶ G)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape K C] (E : CategoryTheory.Functor K J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.lim.map α) (CategoryTheory.Limits.limit.pre G E) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.pre F E)
      (CategoryTheory.Limits.lim.map (E.whiskerLeft α))
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.degreewiseEpiWithInjectiveKernel_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K L : CochainComplex C ℤ) [inst_2 : CategoryTheory.EnoughInjectives C] (n₁ : ℤ),
  CochainComplex.degreewiseEpiWithInjectiveKernel (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.π✝ K L n₁)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g h : G) (a : ↑A),
  ((fun₀ | (h, 1) => (A.ρ g⁻¹) a) - fun₀ | (g * h, 1) => a) ∈ groupHomology.boundaries₂ A
-- Mathlib.Tactic.CongrExclamation
/-- Returns whether or not it's reasonable to consider an equality between types `ty1` and `ty2`.
The heuristic is the following:

- If `ty1` and `ty2` are in `Prop`, then yes.
- If in whnf both `ty1` and `ty2` have the same head and if (recursively) it's reasonable to
  consider an equality between corresponding type arguments, then yes.
- Otherwise, no.

This helps keep congr from going too far and generating hypotheses like `ℝ = ℤ`.

To keep things from going out of control, there is a `maxDepth`. Additionally, if we do the check
with `maxDepth = 0` then the heuristic answers "no".  -/
Congr!.plausiblyEqualTypes : Lean.Expr → Lean.Expr → optParam ℕ 5 → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.rightOpLeftOpIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) (X : Cᵒᵖ),
  F.rightOpLeftOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.congr_fun : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] {f g : P →ᴬ[R] Q},
  f = g → ∀ (x : P), f x = g x
-- Init.Prelude
instInhabitedUInt8 : Inhabited UInt8
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Functor.pi'_map : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (f : (i : I) → CategoryTheory.Functor A (C i)) {X Y : A} (h : X ⟶ Y)
  (i : I), (CategoryTheory.Functor.pi' f).map h i = (f i).map h
-- Mathlib.Topology.MetricSpace.Bounded
Metric.tendsto_dist_left_atTop_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] (c : α) {f : β → α} {l : Filter β},
  Filter.Tendsto (fun x => dist c (f x)) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded α)
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.not_bddAbove_setOfPred_isPrincipal`.

---

Principal ordinals under any operation are unbounded.  -/
Ordinal.not_bddAbove_setOf_isPrincipal : ∀ (op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}), ¬BddAbove {o | Ordinal.IsPrincipal op o}
-- Mathlib.Algebra.Free
FreeAddSemigroup.lift_symm_apply : ∀ {α : Type u} {β : Type v} [inst : AddSemigroup β] (f : FreeAddSemigroup α →ₙ+ β) (a : α),
  FreeAddSemigroup.lift.symm f a = (⇑f ∘ FreeAddSemigroup.of) a
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the second morphism of a `ShortComplex`  -/
CategoryTheory.ShortComplex.g : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (self : CategoryTheory.ShortComplex C) → self.X₂ ⟶ self.X₃
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsAddCyclic.image_range_card : ∀ {α : Type u_1} {a : α} [inst : AddGroup α] [inst_1 : Fintype α] [inst_2 : DecidableEq α],
  (∀ (x : α), x ∈ AddSubgroup.zmultiples a) → Finset.image (fun i => i • a) (Finset.range (Nat.card α)) = Finset.univ
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.congr_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D),
  (CategoryTheory.MonoOver.congr X e).inverse =
    (CategoryTheory.MonoOver.lift (CategoryTheory.Over.post e.inverse) ⋯).comp
      (CategoryTheory.MonoOver.mapIso (e.unitIso.symm.app X)).functor
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
/-- The natural transformation in each degree that is induced by `natTransPInfty`.  -/
AlgebraicTopology.DoldKan.natTransPInfty_f : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (n : ℕ) →
        (AlgebraicTopology.alternatingFaceMapComplex C).comp (HomologicalComplex.eval C (ComplexShape.down ℕ) n) ⟶
          (AlgebraicTopology.alternatingFaceMapComplex C).comp (HomologicalComplex.eval C (ComplexShape.down ℕ) n)
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.mem_subgroup_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a : M}
  {s : UpperSet (FiniteMulArchimedeanClass M)},
  a ∈ FiniteMulArchimedeanClass.subgroup s ↔ ∀ (h : a ≠ 1), FiniteMulArchimedeanClass.mk a h ∈ s
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
/-- The canonical rank function with values in `ℕ` of a regular pairing.  -/
SSet.Subcomplex.Pairing.rankFunction : {X : SSet} → {A : X.Subcomplex} → (P : A.Pairing) → [P.IsRegular] → P.RankFunction ℕ
-- Init.Internal.Order.Basic
/-- The transfinite iteration of a function `f` is a set that is `⊥ ` and is closed under application
of `f` and `csup`.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.iterates : {α : Sort u} → [Lean.Order.CCPO α] → (α → α) → α → Prop
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_comp_whiskerLeft_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (F.obj Z))
          (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom))
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instEssSurjCochainComplexIntQ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], DerivedCategory.Q.EssSurj
-- Mathlib.GroupTheory.Congruence.Defs
Con.mk : {M : Type u_1} →
  [inst : Mul M] →
    (toSetoid : Setoid M) → (∀ {w x y z : M}, toSetoid w x → toSetoid y z → toSetoid (w * y) (x * z)) → Con M
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) (groupHomology.opcyclesIso₀ A).inv =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₀ A).inv
      (HomologicalComplex.pOpcycles (groupHomology.inhomogeneousChains A) 0)
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.toUpperSetAddArchimedeanClass.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  FiniteArchimedeanClass.toUpperSetAddArchimedeanClass =
    OrderEmbedding.ofStrictMono (fun s => { carrier := {a | ∀ (h : a ≠ ⊤), ⟨a, h⟩ ∈ s}, upper' := ⋯ }) ⋯
-- Mathlib.Algebra.Ring.Commute
neg_pow' : ∀ {R : Type u} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R) (n : ℕ), (-a) ^ n = a ^ n * (-1) ^ n
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getKey?ₘ_eq_getKey? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α}, m.getKey?ₘ a = Std.Internal.List.getKey? a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.Hom.partialIso_iso : ∀ {X U : AlgebraicGeometry.Scheme} (f : U ⟶ X) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsDominant f],
  (AlgebraicGeometry.Scheme.Hom.partialIso f).iso =
    U.topIso ≪≫
      AlgebraicGeometry.Scheme.Hom.isoOpensRange f ≪≫
        (↑(AlgebraicGeometry.Scheme.Hom.opensRange f)).topIso.symm ≪≫
          (↑(AlgebraicGeometry.Scheme.Hom.opensRange f)).isoOfEq ⋯ ≪≫
            ((AlgebraicGeometry.Scheme.Hom.opensRange f).partialIsoOfDense ⋯).iso
-- Aesop.Index
_private.Aesop.Index.0.Aesop.Index.applicableByTargetRules : {α : Type} →
  Aesop.Index α →
    Lean.MVarId → (Aesop.Rule α → Bool) → Lean.MetaM (Array (Aesop.Rule α × Array Aesop.IndexMatchLocation))
-- Mathlib.Order.Defs.Unbundled
trichotomous : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Trichotomous r] (a b : α), r a b ∨ a = b ∨ r b a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.valuesArray_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.valuesArray = t₂.valuesArray
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.SavedState.term : Lean.Elab.Tactic.SavedState → Lean.Elab.Term.SavedState
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Filter.IsIncreasingApproximateUnit.closedBall_mem : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {l : Filter A},
  l.IsIncreasingApproximateUnit → Metric.closedBall 0 1 ∈ l
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.Nonempty.csInf_eq_min' : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Finset α} (h : s.Nonempty), sInf ↑s = s.min' h
-- Init.Data.BitVec.Basic
/-- Returns the absolute value of a signed bitvector.
 -/
BitVec.abs : {n : ℕ} → BitVec n → BitVec n
-- Mathlib.Topology.Sheaves.PresheafOfFunctions
TopCat.presheafToType_obj : ∀ (X : TopCat) {T : Type u_1} {U : (TopologicalSpace.Opens ↑X)ᵒᵖ}, (X.presheafToType T).obj U = (↥(Opposite.unop U) → T)
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivAt.fun_sum : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F} {A' : ι → F},
  (∀ i ∈ u, HasDerivAt (A i) (A' i) x) → HasDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_4.congr_eq_7 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (a : Lean.Grind.CommRing.Expr),
  x = a.neg →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.intCast k => h_2 k
      | Lean.Grind.CommRing.Expr.natCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_7 a
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.app_η_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C}
  (self : CategoryTheory.MonadHom T₁ T₂) (X : C) {Z : C} (h : T₂.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (T₁.η.app X) (CategoryTheory.CategoryStruct.comp (self.app X) h) =
    CategoryTheory.CategoryStruct.comp (T₂.η.app X) h
-- Mathlib.Algebra.Ring.Parity
odd_add_self_one' : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Odd (a + (a + 1))
-- Lean.Elab.DeclUtil
Lean.Elab.expandOptDeclSig : Lean.Syntax → Lean.Syntax × Option Lean.Syntax
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.mk.inj : ∀ {toLinOrd : LinOrd} {nonempty : Nonempty ↑toLinOrd} {fintype : Fintype ↑toLinOrd} {toLinOrd_1 : LinOrd}
  {nonempty_1 : Nonempty ↑toLinOrd_1} {fintype_1 : Fintype ↑toLinOrd_1},
  { toLinOrd := toLinOrd, nonempty := nonempty, fintype := fintype } =
      { toLinOrd := toLinOrd_1, nonempty := nonempty_1, fintype := fintype_1 } →
    toLinOrd = toLinOrd_1 ∧ fintype ≍ fintype_1
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep.iIndepSets' : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.iIndep m κ μ → ProbabilityTheory.Kernel.iIndepSets (fun x => {s | MeasurableSet s}) κ μ
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- Auxiliary construction for `desc`.  -/
CategoryTheory.InjectiveResolution.descFZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Y Z : C} →
          (Z ⟶ Y) →
            (I : CategoryTheory.InjectiveResolution Y) →
              (J : CategoryTheory.InjectiveResolution Z) → J.cocomplex.X 0 ⟶ I.cocomplex.X 0
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
CategoryTheory.IsSplitEqualizer.map_rightRetraction : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X} (q : CategoryTheory.IsSplitEqualizer f g ι)
  (F : CategoryTheory.Functor C D), (q.map F).rightRetraction = F.map q.rightRetraction
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.exists_iso_of_arrow_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C),
  T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
      ∀ (e : CategoryTheory.Arrow.mk T₁.mor₁ ≅ CategoryTheory.Arrow.mk T₂.mor₁),
        ∃ e', e'.hom.hom₁ = CategoryTheory.Arrow.Hom.left e.hom ∧ e'.hom.hom₂ = CategoryTheory.Arrow.Hom.right e.hom
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)),
  (F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).hom.toNatTrans.app X =
    (F.map f).toFunctor.map ((F.mapId b₀).inv.toNatTrans.app X)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.toList_roi : ∀ {α : Type u} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => Unit),
  t.Ordered →
    ∀ (lowerBound : α),
      Std.Slice.toList (Std.Roi.Sliceable.mkSlice t lowerBound<...*) =
        List.filter (fun e => (compare e lowerBound).isGT) t.keys
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- `centroidWeights` equals a constant function.  -/
Finset.centroidWeights_eq_const : ∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι),
  Finset.centroidWeights k s = Function.const ι (↑s.card)⁻¹
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- multivariate polynomial functors
 -/
MvPFunctor : ℕ → Type (u + 1)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.HasRightKanExtension.mk : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α], L.HasRightKanExtension F
-- Mathlib.Data.List.TakeWhile
List.takeWhile_eq_nil_iff : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.takeWhile p l = [] ↔ ∀ (hl : 0 < l.length), ¬p (l.get ⟨0, hl⟩) = true
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- Given a morphism of rings `f : R ⟶ S`, the stalk map of `Spec S ⟶ Spec R` at
a prime of `S` is isomorphic to the localized ring homomorphism.  -/
AlgebraicGeometry.Scheme.arrowStalkMapSpecIso : {R S : CommRingCat} →
  (f : R ⟶ S) →
    (p : PrimeSpectrum ↑S) →
      CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap (AlgebraicGeometry.Spec.map f) p) ≅
        CategoryTheory.Arrow.mk
          (CommRingCat.ofHom
            (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
              (CommRingCat.Hom.hom f) ⋯))
-- Std.Time.Format.DateFormat
/-- Short quarter names (4 elements, index 0 = Q1).
 -/
Std.Time.DateFormatSymbols.quarterShort : Std.Time.DateFormatSymbols → Vector String 4