mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.pullbackObjFreeIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
  [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_5 : CategoryTheory.HasWeakSheafify K AddCommGrpCat] [inst_6 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_7 : K.WEqualsLocallyBijective AddCommGrpCat] [inst_8 : F.Final] (I : Type u),
  SheafOfModules.pullbackObjFreeIso φ I =
    (CategoryTheory.asIso
          (CategoryTheory.Limits.sigmaComparison (SheafOfModules.pullback φ) fun x => SheafOfModules.unit S)).symm ≪≫
      CategoryTheory.Limits.Sigma.mapIso fun x => CategoryTheory.asIso (SheafOfModules.pullbackObjUnitToUnit φ)
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabPipeCompletion : Lean.Elab.Term.TermElab
-- Mathlib.RingTheory.Smooth.Flat
/-- Any smooth algebra is flat.  -/
Algebra.Smooth.flat : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [Algebra.Smooth R A],
  Module.Flat R A
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.constants_mem : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M} (c : L.Constants), ↑c ∈ S
-- Mathlib.Algebra.Group.TypeTags.Basic
ofAdd_add : ∀ {α : Type u} [inst : Add α] (x y : α), Multiplicative.ofAdd (x + y) = Multiplicative.ofAdd x * Multiplicative.ofAdd y
-- Mathlib.Topology.Order.Compact
/-- A compact set is bounded below  -/
IsCompact.bddBelow : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIicTopology α] [Nonempty α] {s : Set α},
  IsCompact s → BddBelow s
-- Mathlib.RingTheory.Localization.FractionRing
/-- Another version of unique to give two lift maps should be equal  -/
IsFractionRing.ringHom_ext : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] {L : Type u_7} [inst_2 : Field L]
  [inst_3 : Algebra A K] [IsFractionRing A K] {f1 f2 : K →+* L},
  (∀ (x : A), f1 ((algebraMap A K) x) = f2 ((algebraMap A K) x)) → f1 = f2
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w} [inst_3 : CategoryTheory.SmallCategory J]
  {Y : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone Y} (hc : CategoryTheory.Limits.IsColimit c)
  {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [CategoryTheory.IsCardinalFiltered J κ],
  HasCardinalLT (CategoryTheory.Subobject X) κ →
    ∀ (j₀ : J) (y₁ y₂ : X ⟶ Y.obj j₀),
      CategoryTheory.CategoryStruct.comp y₁ (c.ι.app j₀) = CategoryTheory.CategoryStruct.comp y₂ (c.ι.app j₀) →
        ∃ j φ, CategoryTheory.CategoryStruct.comp y₁ (Y.map φ) = CategoryTheory.CategoryStruct.comp y₂ (Y.map φ)
-- Init.Grind.AC
Lean.Grind.AC.Seq.union_k_eq_union : ∀ (s₁ s₂ : Lean.Grind.AC.Seq), s₁.union_k s₂ = s₁.union s₂
-- Mathlib.Dynamics.FixedPoints.Defs
Function.inter_subset_fixedPoints_comp : ∀ {α : Type u_1} {f g : α → α}, Function.fixedPoints f ∩ Function.fixedPoints g ⊆ Function.fixedPoints (f ∘ g)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.abs_lt_real_iff_infinitesimal : ∀ {x : ℝ*}, x.Infinitesimal ↔ ∀ (r : ℝ), r ≠ 0 → |x| < |↑r|
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.Pattern.mk : List Lean.Name →
  Array Lean.Expr →
    Option Lean.Meta.Sym.ProofInstInfo →
      Lean.Expr → Lean.AssocList Lean.Name Lean.Meta.Sym.ProofInstInfo → Option (Array Bool) → Lean.Meta.Sym.Pattern
-- Mathlib.Algebra.Order.Archimedean.Class
_private.Mathlib.Algebra.Order.Archimedean.Class.0.FiniteMulArchimedeanClass.lift.match_1.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M]
  (motive : FiniteMulArchimedeanClass M → Sort u_2) (A : MulArchimedeanClass M) (hA : A ≠ ⊤)
  (h_1 : (A : MulArchimedeanClass M) → (hA : A ≠ ⊤) → motive ⟨A, hA⟩),
  (match ⟨A, hA⟩ with
    | ⟨A, hA⟩ => h_1 A hA) =
    h_1 A hA
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.liftEquiv.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (N : Subgroup G) [nN : N.Normal] {φ : G →* H}
  (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker),
  QuotientGroup.liftEquiv N hφ HN = MulEquiv.ofBijective (QuotientGroup.lift N φ ⋯) ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_add_nat_mul_two_pi : ∀ (x : ℝ) (n : ℕ), Real.cos (x + ↑n * (2 * Real.pi)) = Real.cos x
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.forall_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] {x : G} {p : ↥(AddSubgroup.zmultiples x) → Prop},
  (∀ (g : ↥(AddSubgroup.zmultiples x)), p g) ↔ ∀ (m : ℤ), p ⟨m • x, ⋯⟩
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.addLeft.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableAdd G] (g : G),
  MeasurableEquiv.addLeft g = MeasurableEquiv.vadd g
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.Integrable.norm_integral_condDistrib_map : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F}
  [inst_5 : NormedSpace ℝ F],
  AEMeasurable Y μ →
    MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
      MeasureTheory.Integrable (fun x => ‖∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x‖)
        (MeasureTheory.Measure.map X μ)
-- Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerRight : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] {X Y : C} (f : X ⟶ Y) (Z : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z =
    CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id Z)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_add : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (x y : ↥H), ↑(x + y) = ↑x + ↑y
-- Mathlib.Topology.MetricSpace.Infsep
Set.Nontrivial.infsep_lt_iff : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} {d : ℝ},
  s.Nontrivial → (s.infsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d)
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.WPath.root : {n : ℕ} →
  {P : MvPFunctor.{u} (n + 1)} →
    (a : P.A) → (f : P.last.B a → P.last.W) → (i : Fin2 n) → P.drop.B a i → P.WPath (WType.mk a f) i
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
AlternatingMap.mkContinuousAlternating_apply : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  {ι' : Type u_1} [inst_8 : Fintype ι'] (f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G) {C : ℝ}
  (H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) (m : ι → E),
  ⇑((f.mkContinuousAlternating C H) m) = ⇑(f m)
-- Mathlib.GroupTheory.FiniteAbelian.Duality
/-- A finite commutative group `G` is (noncanonically) isomorphic to the group `G →* Mˣ`
when `M` is a commutative monoid with enough `n`th roots of unity, where `n` is the exponent
of `G`.  -/
CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity : ∀ (G : Type u_1) (M : Type u_2) [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)], Nonempty ((G →* Mˣ) ≃* G)
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.ContextualizedCompletionInfo.mk.inj : ∀ {hoverInfo : Lean.Server.Completion.HoverInfo} {ctx : Lean.Elab.ContextInfo} {info : Lean.Elab.CompletionInfo}
  {hoverInfo_1 : Lean.Server.Completion.HoverInfo} {ctx_1 : Lean.Elab.ContextInfo} {info_1 : Lean.Elab.CompletionInfo},
  { hoverInfo := hoverInfo, ctx := ctx, info := info } = { hoverInfo := hoverInfo_1, ctx := ctx_1, info := info_1 } →
    hoverInfo = hoverInfo_1 ∧ ctx = ctx_1 ∧ info = info_1
-- Mathlib.Algebra.WithConv
WithConv.instAddAction.eq_1 : ∀ {R : Type u_1} {A : Type u_2} [inst : AddMonoid R] [inst_1 : AddAction R A],
  WithConv.instAddAction =
    { vadd := fun a a_1 => (WithConv.equiv A).2 (a +ᵥ (WithConv.equiv A).toFun a_1), add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.LinearAlgebra.Basis.Prod
Module.Free.prod : ∀ (R : Type u_7) (M : Type u_8) (N : Type u_9) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [Module.Free R M] [Module.Free R N], Module.Free R (M × N)
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_nonneg : ∀ {q : ℚ} {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K], 0 ≤ ↑q ↔ 0 ≤ q
-- Mathlib.Analysis.Calculus.ContDiff.Operations
OpenPartialHomeomorph.restrContDiff_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (f : OpenPartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ↑⊤) (a : E),
  ↑(OpenPartialHomeomorph.restrContDiff 𝕜 f n hn) a = ↑f a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_eq_some_getElem!_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {a : α}, m.contains a = true → m[a]? = some m[a]!
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotOfLEₐ_symm_toRingEquiv : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {I J : Ideal A}
  (h : I ≤ J), (DoubleQuot.quotQuotEquivQuotOfLEₐ R h).symm.toRingEquiv = (DoubleQuot.quotQuotEquivQuotOfLE h).symm
-- Mathlib.Order.Heyting.Basic
/-- `p → p → q ↔ p → q`  -/
le_himp_iff_left : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ≤ a ⇨ b ↔ a ≤ b
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- A Lipschitz function is locally Lipschitz.  -/
LipschitzWith.locallyLipschitz : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {K : NNReal},
  LipschitzWith K f → LocallyLipschitz f
-- Std.Tactic.Do.Syntax
/-- If `true` (the default), we will simplify every generated VC after trying
`mvcgen_trivial` by running `mleave`. (Note that this can be expensive.)
 -/
Lean.Elab.Tactic.Do.VCGen.Config.leave : Lean.Elab.Tactic.Do.VCGen.Config → Bool
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.LawfulForwardPattern.skipPrefixOfNonempty?_eq : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.ForwardPattern pat}
  [self : String.Slice.Pattern.LawfulForwardPattern pat] {s : String.Slice} (h : s.isEmpty = false),
  String.Slice.Pattern.ForwardPattern.skipPrefixOfNonempty? pat s h =
    String.Slice.Pattern.ForwardPattern.skipPrefix? pat s
-- Mathlib.Data.Num.Basic
/-- Modulus of `Num`s.  -/
Num.mod : Num → Num → Num
-- Std.Data.DTreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
less than or equal to the given key.
 -/
Std.DTreeMap.Const.getEntryLE : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [Std.TransCmp cmp] → (t : Std.DTreeMap α (fun x => β) cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isLE = true) → α × β
-- Mathlib.FieldTheory.Fixed
linearIndependent_toLinearMap : ∀ (R : Type u) (A : Type v) (B : Type w) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [IsDomain B] [inst_5 : Algebra R B], LinearIndependent B AlgHom.toLinearMap
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isInt_neg : ∀ {α : Type u_1} [inst : Ring α] {f : α → α} {a : α} {a' b : ℤ},
  f = Neg.neg → Mathlib.Meta.NormNum.IsInt a a' → a'.neg = b → Mathlib.Meta.NormNum.IsInt (-a) b
-- Mathlib.NumberTheory.Harmonic.Defs
harmonic_zero : harmonic 0 = 0
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MaybeFunctionData.data.inj : ∀ {fData fData_1 : Mathlib.Meta.FunProp.FunctionData},
  Mathlib.Meta.FunProp.MaybeFunctionData.data fData = Mathlib.Meta.FunProp.MaybeFunctionData.data fData_1 →
    fData = fData_1
-- Mathlib.Algebra.Category.ModuleCat.Localization
ModuleCat.isIso_of_isLocalizedModule_comp : ∀ {R : Type u} [inst : CommRing R] {S : Submonoid R} {M₁ M₂ M₃ : ModuleCat R} {f₁ : M₁ ⟶ M₂} {f₂ : M₂ ⟶ M₃},
  IsLocalizedModule S (ModuleCat.Hom.hom f₁) →
    IsLocalizedModule S (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp f₁ f₂)) → CategoryTheory.IsIso f₂
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
/-- If `0 < n`, then `QuaternionGroup n` is a finite group.
 -/
QuaternionGroup.instFintypeOfNeZeroNat : {n : ℕ} → [NeZero n] → Fintype (QuaternionGroup n)
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_natCast : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (n : ℕ), ↑↑n = ↑n
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flip_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.flip.X₁ = sq.X₁
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
CategoryTheory.Functor.over_forget_locallyCoverDense : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (X : C),
  (CategoryTheory.Over.forget X).LocallyCoverDense J
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffOn.finsum_section_of_locallyFinite : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {u : Set M} {ι : Type u_7} {t : ι → (x : M) → V x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) →
    (∀ (i : ι), ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t i x⟩) u) →
      ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, ∑ᶠ (i : ι), t i x⟩) u
-- Mathlib.LinearAlgebra.FreeModule.Norm
/-- For a nonzero element `f` in an algebra `S` over a principal ideal domain `R` that is finite and
free as an `R`-module, the norm of `f` relative to `R` is associated to the product of the Smith
coefficients of the ideal generated by `f`.  -/
associated_norm_prod_smith : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : IsPrincipalIdealRing R] [inst_3 : CommRing S] [inst_4 : IsDomain S] [inst_5 : Algebra R S]
  [inst_6 : Fintype ι] (b : Module.Basis ι R S) {f : S} (hf : f ≠ 0),
  Associated ((Algebra.norm R) f) (∏ i, Ideal.smithCoeffs b (Ideal.span {f}) ⋯ i)
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.measure.eq_1 : ∀ {α : Type u_1} {β : Type u_2}, Lean.PersistentHashMap.Zipper.done.measure = 0
-- Lean.Environment
/-- Environment extension, can only be generated by `registerEnvExtension` that allocates a unique index
for this extension into each environment's extension state's array.
 -/
Lean.EnvExtension : Type → Type
-- Mathlib.CategoryTheory.Core
CategoryTheory.CoreHom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.Core C} [inst_1 : SizeOf C]
  (iso : X.of ≅ Y.of), sizeOf { iso := iso } = 1 + sizeOf iso
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_comp_equiv : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : κ → M} (e : ι ≃ κ),
  s.sum (f ∘ ⇑e) = (Finset.map e.toEmbedding s).sum f
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.ShiftMkCore.mk.sizeOf_spec : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A] [inst_2 : SizeOf C]
  [inst_3 : SizeOf A] (F : A → CategoryTheory.Functor C C) (zero : F 0 ≅ CategoryTheory.Functor.id C)
  (add : (n m : A) → F (n + m) ≅ (F n).comp (F m))
  (assoc_hom_app :
    autoParam
      (∀ (m₁ m₂ m₃ : A) (X : C),
        CategoryTheory.CategoryStruct.comp ((add (m₁ + m₂) m₃).hom.app X) ((F m₃).map ((add m₁ m₂).hom.app X)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp ((add m₁ (m₂ + m₃)).hom.app X) ((add m₂ m₃).hom.app ((F m₁).obj X))))
      CategoryTheory.ShiftMkCore.assoc_hom_app._autoParam)
  (zero_add_hom_app :
    autoParam
      (∀ (n : A) (X : C),
        (add 0 n).hom.app X =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((F n).map (zero.inv.app X)))
      CategoryTheory.ShiftMkCore.zero_add_hom_app._autoParam)
  (add_zero_hom_app :
    autoParam
      (∀ (n : A) (X : C),
        (add n 0).hom.app X =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (zero.inv.app ((F n).obj X)))
      CategoryTheory.ShiftMkCore.add_zero_hom_app._autoParam),
  sizeOf
      { F := F, zero := zero, add := add, assoc_hom_app := assoc_hom_app, zero_add_hom_app := zero_add_hom_app,
        add_zero_hom_app := add_zero_hom_app } =
    1 + sizeOf zero
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.dvd_add_iff : ∀ {a b c : Ordinal.{u_4}}, a ∣ b → (a ∣ b + c ↔ a ∣ c)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.isReal_of_mk_isReal : ∀ {K : Type u_1} [inst : Field K] {φ : K →+* ℂ},
  (NumberField.InfinitePlace.mk φ).IsReal → NumberField.ComplexEmbedding.IsReal φ
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
/-- **Alias** of the forward direction of `AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff`. -/
AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative]
  {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.Sieve X},
  S ∈ (AlgebraicGeometry.Scheme.grothendieckTopology P) X → ∃ 𝒰, CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.comp_continuous : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β}
  [inst_2 : TopologicalSpace δ] {g : δ → α} {b : δ}, IsLocalMax f (g b) → ContinuousAt g b → IsLocalMax (f ∘ g) b
-- Mathlib.Topology.Algebra.StarSubalgebra
/-- If a star subalgebra of a topological star algebra is commutative, then so is its topological
closure. See note [reducible non-instances].  -/
StarSubalgebra.commRingTopologicalClosure : {R : Type u_4} →
  {A : Type u_5} →
    [inst : CommRing R] →
      [inst_1 : StarRing R] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : Ring A] →
            [inst_4 : Algebra R A] →
              [inst_5 : StarRing A] →
                [inst_6 : StarModule R A] →
                  [inst_7 : IsSemitopologicalRing A] →
                    [inst_8 : ContinuousStar A] →
                      [T2Space A] →
                        (s : StarSubalgebra R A) → (∀ (x y : ↥s), x * y = y * x) → CommRing ↥s.topologicalClosure
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.convMul_bialgHom_single_one : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Bialgebra R A] [inst_3 : CommMonoid M] (f g : WithConv (MonoidAlgebra R M →ₐc[R] A)) (x : M),
  (f * g).ofConv (MonoidAlgebra.single x 1) = f.ofConv (MonoidAlgebra.single x 1) * g.ofConv (MonoidAlgebra.single x 1)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.add' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε' : Type u_8} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddMonoid ε'] {f g : α → ε'},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → MeasureTheory.HasFiniteIntegral (f + g) μ
-- Init.System.IO
/-- Iterates an `IO` action. Starting with an initial state, the action is applied repeatedly until it
returns a final value in `Sum.inr`. Each time it returns `Sum.inl`, the returned value is treated as
a new state.
 -/
IO.iterate : {α β : Type} → α → (α → IO (α ⊕ β)) → IO β
-- Mathlib.Geometry.Manifold.ContMDiffMap
/-- Bundled `n` times continuously differentiable maps,
denoted as `C^n(I, M; I', M')` and `C^n(I, M; k)` (when the target is a normed space `k` with
the trivial model) in the `Manifold` namespace.  -/
ContMDiffMap : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_5} →
                      [inst_6 : TopologicalSpace H'] →
                        ModelWithCorners 𝕜 E H →
                          ModelWithCorners 𝕜 E' H' →
                            (M : Type u_6) →
                              [inst : TopologicalSpace M] →
                                [ChartedSpace H M] →
                                  (M' : Type u_7) →
                                    [inst : TopologicalSpace M'] →
                                      [ChartedSpace H' M'] → WithTop ℕ∞ → Type (max 0 u_6 u_7)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddAbove.range_inv : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {α : Type u_4} {f : α → G},
  BddAbove (Set.range f) → BddBelow (Set.range fun x => (f x)⁻¹)
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
_private.Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum.0.ZMod.χ₄.match_1.eq_2 : ∀ (motive : ZMod 4 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 2) (h_3 : Unit → motive 1)
  (h_4 : Unit → motive 3),
  (match 2 with
    | 0 => h_1 ()
    | 2 => h_2 ()
    | 1 => h_3 ()
    | 3 => h_4 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {G H : CategoryTheory.OplaxFunctor B CategoryTheory.Cat}
  (θ : CategoryTheory.Oplax.StrongTrans G H) {a b : B} {a' : CategoryTheory.Cat} (f : a' ⟶ G.obj a) {g h : a ⟶ b}
  (β : g ⟶ h) (X : ↑a'),
  CategoryTheory.CategoryStruct.comp ((θ.app b).toFunctor.map ((G.map₂ β).toNatTrans.app (f.toFunctor.obj X)))
      ((θ.naturality h).hom.toNatTrans.app (f.toFunctor.obj X)) =
    CategoryTheory.CategoryStruct.comp ((θ.naturality g).hom.toNatTrans.app (f.toFunctor.obj X))
      ((H.map₂ β).toNatTrans.app ((θ.app a).toFunctor.obj (f.toFunctor.obj X)))