mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- `F.mapCone s` being limiting is the same as the induced binary fan being limiting.  -/
CategoryTheory.Limits.BinaryFan.isLimitMapConeEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {F : CategoryTheory.Functor C D} →
          {X Y : C} →
            {s : CategoryTheory.Limits.BinaryFan X Y} →
              CategoryTheory.Limits.IsLimit (F.mapCone s) ≃
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.map F s)
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
MonomialOrder.degLex_single_lt_iff : ∀ {σ : Type u_2} [inst : LinearOrder σ] [inst_1 : WellFoundedGT σ] {a b : σ},
  ((MonomialOrder.degLex.toSyn fun₀ | a => 1) < MonomialOrder.degLex.toSyn fun₀ | b => 1) ↔ b < a
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.mem_ptsOfPeriod : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, x ∈ Function.ptsOfPeriod f n ↔ Function.IsPeriodicPt f n x
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemView.mk.inj : ∀ {omitFields : Array (Lean.Ident × Lean.Name)} {handlers : Array Lean.Elab.ConfigEval.EvalConfigItemHandler}
  {omitFields_1 : Array (Lean.Ident × Lean.Name)} {handlers_1 : Array Lean.Elab.ConfigEval.EvalConfigItemHandler},
  { omitFields := omitFields, handlers := handlers } = { omitFields := omitFields_1, handlers := handlers_1 } →
    omitFields = omitFields_1 ∧ handlers = handlers_1
-- Mathlib.Analysis.Convex.Strong
UniformConvexOn.mono : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {φ ψ : ℝ → ℝ} {s : Set E} {f : E → ℝ},
  ψ ≤ φ → UniformConvexOn s φ f → UniformConvexOn s ψ f
-- Mathlib.Tactic.NormNum.RealSqrt
Mathlib.Meta.NormNum.isNat_realSqrt_of_isRat_negOfNat : ∀ {x : ℝ} {num denom : ℕ}, Mathlib.Meta.NormNum.IsRat x (Int.negOfNat num) denom → Mathlib.Meta.NormNum.IsNat (√x) 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstr.mk.sizeOf_spec : ∀ (p : Lean.Grind.CommRing.Poly) (h : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof),
  sizeOf { p := p, h := h } = 1 + sizeOf p + sizeOf h
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A totally bounded set is separable in countably generated uniform spaces. This can be obtained
from the more general `UniformSpace.subset_countable_closure_of_almost_dense_set`.  -/
TotallyBounded.isSeparable : ∀ {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] {s : Set α},
  TotallyBounded s → TopologicalSpace.IsSeparable s
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.opcyclesMap'_smul : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (a : R),
  CategoryTheory.ShortComplex.opcyclesMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂
-- Mathlib.Order.WithBot
WithBot.unbotD_eq_iff : ∀ {α : Type u_1} {d y : α} {x : WithBot α}, WithBot.unbotD d x = y ↔ x = ↑y ∨ x = ⊥ ∧ y = d
-- Mathlib.Topology.Category.TopCat.Limits.Basic
/-- Given a functor `F : J ⥤ TopCat` and a cone `c : Cone (F ⋙ forget)`
of the underlying functor to types, this is the type `c.pt`
with the infimum of the induced topologies by the maps `c.π.app j`.  -/
TopCat.conePtOfConeForget : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    {F : CategoryTheory.Functor J TopCat} → CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget TopCat)) → Type u
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.twoShortAddLongRoot_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R],
  RootPairing.EmbeddedG2.twoShortAddLongRoot P =
    2 • RootPairing.EmbeddedG2.shortRoot P + RootPairing.EmbeddedG2.longRoot P
-- Mathlib.Data.Multiset.ZeroCons
Multiset.exists_cons_of_mem : ∀ {α : Type u_1} {s : Multiset α} {a : α}, a ∈ s → ∃ t, s = a ::ₘ t
-- Mathlib.Algebra.Group.Prod
mulMulHom_apply : ∀ {α : Type u_6} [inst : CommSemigroup α] (a : α × α), mulMulHom a = a.1 * a.2
-- Lean.Parser.Do
Lean.Parser.Term.doAssert.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- To check equality of natural transformations `F ⟶ G`, it suffices to check it on
Galois objects.  -/
CategoryTheory.PreGaloisCategory.natTrans_ext_of_isGalois : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  {G : CategoryTheory.Functor C FintypeCat} {t s : F ⟶ G},
  (∀ (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X], t.app X = s.app X) → t = s
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The transitivity axiom in 'arrow' form: If `S` covers `f` and every arrow in `S` is covered by
`R`, then `R` covers `f`.
 -/
CategoryTheory.GrothendieckTopology.arrow_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C)
  (f : Y ⟶ X) (S R : CategoryTheory.Sieve X),
  J.Covers S f → (∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g) → J.Covers R f
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.all_eq_match_step : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {p : β → Bool},
  Std.Iter.all p it =
    match ↑it.step with
    | Std.IterStep.yield it' x => if p x = true then Std.Iter.all p it' else false
    | Std.IterStep.skip it' => Std.Iter.all p it'
    | Std.IterStep.done => true
-- Mathlib.Data.Set.Lattice
Set.union_iUnion : ∀ {β : Type u_2} {ι : Sort u_5} [Nonempty ι] (s : Set β) (t : ι → Set β), s ∪ ⋃ i, t i = ⋃ i, s ∪ t i
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Functor.sections_ext_iff : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w)} {x y : ↑F.sections},
  x = y ↔ ∀ (j : J), ↑x j = ↑y j
-- Init.Data.BitVec.Lemmas
BitVec.toNat_intMin_of_pos : ∀ {w : ℕ}, 0 < w → (BitVec.intMin w).toNat = 2 ^ (w - 1)
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
IicProdIoc_self : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : LocallyFiniteOrderBot ι] (a : ι), IicProdIoc a a = Prod.fst
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_sup : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s t : TopologicalSpace.Opens α), ↑(s ⊔ t) = ↑s ∪ ↑t
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.apply_ne_top : ∀ {α : Type u_1} (p : PMF α) (a : α), p a ≠ ⊤
-- Mathlib.Data.Set.Function
Set.exists_image_eq_and_injOn : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (f : α → β), ∃ u, f '' u = f '' s ∧ Set.InjOn f u
-- Mathlib.Order.Types.Defs
OrderType.lift_lift : ∀ (o : OrderType.{u_1}), OrderType.lift.{u, max v u_1} (OrderType.lift.{v, u_1} o) = OrderType.lift.{max v u, u_1} o
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_le_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, k ∈ t → (cmp t.min! k).isLE = true
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
/-- The first projection.  -/
CategoryTheory.PreZeroHypercover.Relation.fst : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S : C} → {E : CategoryTheory.PreZeroHypercover S} → {i j : E.I₀} → (self : E.Relation i j) → self.obj ⟶ E.X i
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- A topological space `X` is compactly generated if its topology is finer than (and thus equal to)
the compactly generated topology, i.e. it is coinduced by the continuous maps from compact
Hausdorff spaces to `X`.

In this version, intended for topological purposes, the compact spaces are taken
in the same universe as `X`. See `UCompactlyGeneratedSpace` for a version with an explicit
universe parameter, intended for categorical purposes.
 -/
CompactlyGeneratedSpace : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.evalN_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (n : ℕ) (S : CategoryTheory.SimplicialObject.Split C),
  (CategoryTheory.SimplicialObject.Split.evalN C n).obj S = S.s.N n
-- Batteries.Data.UInt
UInt8.compare_eq_toNat_compare_toNat : ∀ (x y : UInt8), compare x y = compare x.toNat y.toNat
-- Mathlib.Topology.UnitInterval
unitInterval.symm.eq_1 : ∀ (t : ↑unitInterval), unitInterval.symm t = ⟨1 - ↑t, ⋯⟩
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurablePow.mk : ∀ {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ] [inst_2 : Pow β γ],
  (Measurable fun p => p.1 ^ p.2) → MeasurablePow β γ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
fderiv_cos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → fderiv ℝ (fun x => Real.cos (f x)) x = -Real.sin (f x) • fderiv ℝ f x
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.equivIccQuot_comp_mk_eq_toIcoMod : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜] (p a : 𝕜)
  [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜],
  ⇑(AddCircle.equivIccQuot p a) ∘ Quotient.mk'' = fun x => Quot.mk (AddCircle.EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩
-- Mathlib.Analysis.CStarAlgebra.Basic
_private.Mathlib.Analysis.CStarAlgebra.Basic.0.«term_⋆» : Lean.TrailingParserDescr
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_two_pi_mul_int : ∀ (n : ℤ), Circle.exp (2 * Real.pi * ↑n) = 1
-- Init.Data.List.Sort.Lemmas
/-- The elements of `merge le xs ys` are exactly the elements of `xs` and `ys`.
 -/
List.mem_merge : ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {xs ys : List α}, a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁'_map_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (h : X ⟶ Y) (X_1 Y_1 : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁' C).map h).app X_1).app Y_1 =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X_1 (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y_1 h)
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Down.erase_mem_compression : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α},
  s ∈ 𝒜 → s.erase a ∈ Down.compression a 𝒜
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.basisKaehlerOfIsCompl.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P P_1 : Algebra.SubmersivePresentation R S ι σ) (e_P : P = P_1)
  {κ : Type u_5} {f f_1 : κ → ι} (e_f : f = f_1) (hf : Function.Injective f)
  (hcompl : IsCompl (Set.range f) (Set.range P.map)), P.basisKaehlerOfIsCompl hf hcompl = P_1.basisKaehlerOfIsCompl ⋯ ⋯
-- Mathlib.Analysis.Normed.Group.Real
enorm_norm : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (x : E), ‖‖x‖‖ₑ = ‖x‖ₑ
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Limits.WeightedCone.IsLimit.fac_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W : CategoryTheory.Functor J (Type w)} {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.WeightedCone W F}
  (hc : c.IsLimit) {Z : C} (π : ⦃j : J⦄ → W.obj j → (Z ⟶ F.obj j))
  (hπ :
    ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂),
      CategoryTheory.CategoryStruct.comp (π x) (F.map f) = π ((CategoryTheory.ConcreteCategory.hom (W.map f)) x))
  {j : J} (x : W.obj j) {Z_1 : C} (h : F.obj j ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (hc.lift π hπ) (CategoryTheory.CategoryStruct.comp (c.π x) h) =
    CategoryTheory.CategoryStruct.comp (π x) h
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- The elements of the atlas belong to the maximal atlas for any structure groupoid.  -/
StructureGroupoid.subset_maximalAtlas : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (G : StructureGroupoid H) [HasGroupoid M G], atlas H M ⊆ StructureGroupoid.maximalAtlas M G
-- Mathlib.Topology.Algebra.Monoid
continuousOn_finsetSum : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Finset ι) {t : Set X},
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => ∑ i ∈ s, f i a) t
-- Mathlib.Logic.Basic
apply_ite_left : ∀ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (f : α → β → γ) (P : Prop) [inst : Decidable P] (x y : α) (z : β),
  f (if P then x else y) z = if P then f x z else f y z
-- Mathlib.Data.ENNReal.Inv
ENNReal.zpow_sub : ∀ {x : ENNReal}, x ≠ 0 → x ≠ ⊤ → ∀ (m n : ℤ), x ^ (m - n) = x ^ m * (x ^ n)⁻¹
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.mk.inj : ∀ {toProfinite : Profinite} {addGroup : AddGroup ↑toProfinite.toTop}
  {topologicalAddGroup : IsTopologicalAddGroup ↑toProfinite.toTop} {toProfinite_1 : Profinite}
  {addGroup_1 : AddGroup ↑toProfinite_1.toTop} {topologicalAddGroup_1 : IsTopologicalAddGroup ↑toProfinite_1.toTop},
  { toProfinite := toProfinite, addGroup := addGroup, topologicalAddGroup := topologicalAddGroup } =
      { toProfinite := toProfinite_1, addGroup := addGroup_1, topologicalAddGroup := topologicalAddGroup_1 } →
    toProfinite = toProfinite_1 ∧ addGroup ≍ addGroup_1
-- Init.Data.Nat.Lcm
Nat.lcm_mul_right_right_eq_mul_of_lcm_eq_mul : ∀ {n m k : ℕ}, n.lcm m = n * m → n.lcm (m * k) = n.lcm k * m
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rxc.Iterator.toList_eq_match.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : Unit → motive none) (h_2 : (a : α) → motive (some a)),
  (match some a with
    | none => h_1 ()
    | some a => h_2 a) =
    h_2 a
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.add_domain : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f g : E →ₛₗ.[σ] F),
  (f + g).domain = f.domain ⊓ g.domain
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.enorm_toL1 : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β} (hf : MeasureTheory.Integrable f μ), ‖MeasureTheory.Integrable.toL1 f hf‖ₑ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The ring equiv between the top element of `Subfield K` and `K`.  -/
Subfield.topEquiv : {K : Type u} → [inst : DivisionRing K] → ↥⊤ ≃+* K
-- Mathlib.RingTheory.Polynomial.UniqueFactorization
Polynomial.wfDvdMonoid : ∀ {R : Type u_1} [inst : CommSemiring R] [NoZeroDivisors R] [WfDvdMonoid R], WfDvdMonoid (Polynomial R)
-- Mathlib.Algebra.Field.Defs
/-- The inverse of `0` is `0` by convention.  -/
Field.inv_zero : ∀ {K : Type u} [self : Field K], 0⁻¹ = 0
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instVAdd : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → VAdd (E →ₛₗ[σ] F) (E →ₛₗ.[σ] F)
-- Init.System.IO
/-- Marks given value and its object graph closure as persistent. This will remove
reference counter updates but prevent the closure from being deallocated until
the end of the process! It can still be useful to do eagerly when the value
will be marked persistent later anyway and there is available time budget to
mark it now or it would be unnecessarily marked multi-threaded in between.

This function is only safe to use on objects (in the full closure) which are
not used concurrently or which are already persistent.
 -/
Runtime.markPersistent : {α : Type} → α → BaseIO α
-- Mathlib.Topology.Semicontinuity.Basic
UpperSemicontinuousWithinAt.sup : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α} {a : α},
  UpperSemicontinuousWithinAt f s a →
    UpperSemicontinuousWithinAt g s a → UpperSemicontinuousWithinAt (fun x => max (f x) (g x)) s a
-- Init.Data.Array.Attach
Array.foldr_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {P : α → Prop} {f : (a : α) → P a → β} (H : ∀ a ∈ xs, P a)
  (g : β → γ → γ) (x : γ), Array.foldr g x (Array.pmap f xs H) = Array.foldr (fun a acc => g (f ↑a ⋯) acc) x xs.attach
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.smul : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : SeminormedAddCommGroup Y] {C r : NNReal}
  {f : X → Y} {α : Type u_4} [inst_2 : SeminormedAddCommGroup α] [inst_3 : SMulZeroClass α Y] [IsBoundedSMul α Y]
  (a : α), HolderWith C r f → HolderWith (C * ‖a‖₊) r (a • f)
-- Mathlib.Data.Complex.Basic
/-- The "imaginary part" map, considered as an additive group homomorphism.  -/
Complex.imAddGroupHom : ℂ →+ ℝ
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftCoyonedaEquiv_symm_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
  {F : CategoryTheory.Functor C (Type (max w v₁))} (t : F.obj X),
  CategoryTheory.uliftCoyonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.map f.op)
      (CategoryTheory.uliftCoyonedaEquiv.symm t)
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.IsAddConj.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (S : AddGroupExtension N E G) (s s' : S.Splitting), S.IsAddConj s s' = ∃ n, ⇑s = fun g => S.inl n + s' g + -S.inl n
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.whiskering_obj_obj_δ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) (X : CategoryTheory.SimplicialObject C) {n : ℕ} (i : Fin (n + 2)),
  (((CategoryTheory.SimplicialObject.whiskering C D).obj F).obj X).δ i = F.map (X.δ i)
-- Mathlib.Topology.Semicontinuity.Defs
lowerHemicontinuousAt_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α},
  LowerHemicontinuousAt f x ↔ ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, f x' ⊆ t) → f x ⊆ t
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.dp.eq_1 : ∀ (R : Type u_2) {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ)
  (m : M), DividedPowerAlgebra.dp R n m = ↑(MvPolynomial.X (n, m))
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ModuleCat k}
  (h : ModuleCat.of k ↥(groupHomology.cycles₁ B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.cyclesMap f φ 1)
      (CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₁ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₁ A).hom
      (CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₁ f φ) h)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {f : σ → R} (a : R), (MvPolynomial.eval f) (MvPolynomial.C a) = a
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.unitIsoAddEquiv.eq_1 : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {V : Rep.{w, u, v} k G},
  Rep.unitIsoAddEquiv =
    id (V.ρ.asModuleEquiv.symm.toAddEquiv.trans (RestrictScalars.addEquiv k (MonoidAlgebra k G) V.ρ.asModule).symm)
-- Aesop.Stats.File
Aesop.StatsFileRecord.position : Aesop.StatsFileRecord → Option Lean.Position
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualRestrict_comp_dualLift : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (W : Subspace K V),
  Submodule.dualRestrict W ∘ₗ W.dualLift = 1
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b),
  CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom
      (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv)
        (F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom)
-- Init.Data.Nat.Lemmas
Nat.shiftLeft_shiftRight : ∀ (x n : ℕ), x <<< n >>> n = x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_le_pi_div_two : ∀ {x : ℝ}, Real.arccos x ≤ Real.pi / 2 ↔ 0 ≤ x
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.continuous : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), Continuous ⇑e
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.sumTransform_def : ∀ {p : ℝ} {g : ℝ → ℝ} {n₀ n : ℕ},
  AkraBazziRecurrence.sumTransform p g n₀ n = ↑n ^ p * ∑ u ∈ Finset.Ico n₀ n, g ↑u / ↑u ^ (p + 1)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.mkEqTransOptProofResult : Option Lean.Expr → Bool → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.prod_Ioo_mul_eq_prod_Ico : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a < b → (∏ x ∈ Finset.Ioo a b, f x) * f a = ∏ x ∈ Finset.Ico a b, f x
-- Mathlib.RingTheory.Derivation.Basic
/-- For a tower `R → A → B` and an `R`-derivation `B → M`, we may compose with `A → B` to obtain an
`R`-derivation `A → M`.  -/
Derivation.compAlgebraMap : {R : Type u_1} →
  (A : Type u_2) →
    {B : Type u_3} →
      {M : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : CommSemiring B] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Algebra R B] →
                    [inst_6 : Module A M] →
                      [inst_7 : Module B M] →
                        [inst_8 : Module R M] →
                          [inst_9 : Algebra A B] →
                            [IsScalarTower R A B] → [IsScalarTower A B M] → Derivation R B M → Derivation R A M
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.adjoin_simple_le_iff : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  {x : K} {L : FiniteGaloisIntermediateField k K},
  FiniteGaloisIntermediateField.adjoin k {x} ≤ L ↔ x ∈ L.toIntermediateField
-- Lean.Util.CollectFVars
Lean.CollectFVars.State.mk.sizeOf_spec : ∀ (visitedExpr : Lean.ExprSet) (fvarSet : Lean.FVarIdSet) (fvarIds : Array Lean.FVarId),
  sizeOf { visitedExpr := visitedExpr, fvarSet := fvarSet, fvarIds := fvarIds } =
    1 + sizeOf visitedExpr + sizeOf fvarSet + sizeOf fvarIds