mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Exponent
/-- If there exists an injective, addition-preserving map from `G` to `H`,
then the exponent of `G` divides the exponent of `H`.  -/
AddMonoid.exponent_dvd_of_addMonoidHom : ∀ {G : Type u} [inst : AddMonoid G] {H : Type u_1} [inst_1 : AddMonoid H] (e : G →+ H),
  Function.Injective ⇑e → AddMonoid.exponent G ∣ AddMonoid.exponent H
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.comp_zsmul_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X Y : C} [inst_2 : CategoryTheory.AddGrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) (n : ℤ) {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (n • g) h) =
    CategoryTheory.CategoryStruct.comp (n • CategoryTheory.CategoryStruct.comp f g) h
-- Mathlib.Data.Complex.Basic
Complex.ofReal_neg : ∀ (r : ℝ), ↑(-r) = -↑r
-- Mathlib.SetTheory.Cardinal.Embedding
Fin.Embedding.restrictSurjective_of_le_ENatCard : ∀ {α : Type u_1} {m n : ℕ} (hmn : m ≤ n), ↑n ≤ ENat.card α → Function.Surjective fun x => (Fin.castLEEmb hmn).trans x
-- Mathlib.RingTheory.RingHom.Flat
CommRingCat.flat.eq_1 : CommRingCat.flat = RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.Flat
-- Batteries.Data.String.Lemmas
String.Pos.Raw.offsetBy_eq : ∀ {p q : String.Pos.Raw}, p.offsetBy q = { byteIdx := q.byteIdx + p.byteIdx }
-- Mathlib.Data.Set.Image
Set.image_singleton : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α}, f '' {a} = {f a}
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfLax_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) (F' : F.PseudoCore) (a : B),
  (CategoryTheory.Pseudofunctor.mkOfLax F F').mapId a = F'.mapIdIso a
-- Lean.Elab.Do.Basic
/-- Register the given name as that of a `mut` variable if the syntax token `mut` is present.  -/
Lean.Elab.Do.declareMutVar? : {α : Type} → Option Lean.Syntax → Lean.Ident → Lean.Elab.Do.DoElabM α → Lean.Elab.Do.DoElabM α
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lim_lt : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : CauSeq.IsComplete α abs] {f : CauSeq α abs} {x : α}, f < CauSeq.const abs x → f.lim < x
-- Mathlib.RingTheory.Jacobson.Ideal
/-- An ideal equals its Jacobson radical iff it is the intersection of a set of maximal ideals.
Allowing the set to include ⊤ is equivalent, and is included only to simplify some proofs.  -/
Ideal.eq_jacobson_iff_sInf_maximal : ∀ {R : Type u} [inst : Ring R] {I : Ideal R}, I.jacobson = I ↔ ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.comp_eval₂ : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {φ : R →+* S} {a : S}
  [inst_2 : UniformSpace R] [inst_3 : UniformSpace S] [IsUniformAddGroup R] [IsTopologicalSemiring R]
  [IsUniformAddGroup S] [T2Space S] [CompleteSpace S] [IsTopologicalRing S] [IsLinearTopology S S],
  Continuous ⇑φ →
    PowerSeries.HasEval a →
      ∀ {T : Type u_3} [inst_11 : UniformSpace T] [CompleteSpace T] [T2Space T] [inst_14 : CommRing T]
        [IsTopologicalRing T] [IsLinearTopology T T] [IsUniformAddGroup T] {ε : S →+* T},
        Continuous ⇑ε → ⇑ε ∘ PowerSeries.eval₂ φ a = PowerSeries.eval₂ (ε.comp φ) (ε a)
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.comp_hom_assoc : ∀ {X Y Z : FintypeCat} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : Type u_1} (h : Z.obj ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h) =
    CategoryTheory.CategoryStruct.comp
      (TypeCat.ofHom (⇑(CategoryTheory.ConcreteCategory.hom g.hom) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f.hom))) h
-- Mathlib.Algebra.Algebra.Pi
/-- `Function.eval` as an `AlgHom`. The name matches `Pi.evalRingHom`, `Pi.evalMonoidHom`,
etc.  -/
Pi.evalAlgHom : {ι : Type u_1} →
  (R : Type u_2) →
    (A : ι → Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → Semiring (A i)] → [inst_2 : (i : ι) → Algebra R (A i)] → (i : ι) → ((i : ι) → A i) →ₐ[R] A i
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- for each `i : ι`, we shall attach a cell given by the morphism `g (π i)`.  -/
HomotopicalAlgebra.AttachCells.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} → {f : X₁ ⟶ X₂} → (self : HomotopicalAlgebra.AttachCells g f) → self.ι → α
-- Mathlib.Combinatorics.Graph.Subgraph
/-- `H ≤c G` (`Graph.IsClosedSubgraph`) is a union of components of `G`.  -/
Graph.IsClosedSubgraph : {α : Type u_1} → {β : Type u_2} → Graph α β → Graph α β → Prop
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.opNNNorm_subsingleton : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  [Subsingleton E] (f : E →SL[σ₁₂] F), ‖f‖₊ = 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
EReal.measurable_of_real_real : ∀ {β : Type u_6} {mβ : MeasurableSpace β} {f : EReal × EReal → β},
  (Measurable fun p => f (↑p.1, ↑p.2)) →
    (Measurable fun r => f (⊥, ↑r)) →
      (Measurable fun r => f (⊤, ↑r)) → (Measurable fun r => f (↑r, ⊥)) → (Measurable fun r => f (↑r, ⊤)) → Measurable f
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.supportedEquivFinsupp_apply_support_val : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M) (x : ↥(AddMonoidAlgebra.supported R S s)),
  ((AddMonoidAlgebra.supportedEquivFinsupp s) x).support.val =
    Multiset.map (fun x_1 => ⟨↑x_1, ⋯⟩) (Multiset.filter (fun x => x ∈ s) (↑x).coeff.support.val).attach
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f` is a submersion at `x`, then `f` is `C^n` on its domain chart's source,
in particular on an open neighbourhood of `x`.`

Prefer using `IsSubmersionAt.contMDiffAt` instead  -/
Manifold.IsSubmersionAt.contMDiffOn : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAt I J n f x), ContMDiffOn I J n f h.domChart.source
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_def : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] {s : Finset α}, s⁻¹ = Finset.image (fun x => x⁻¹) s
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app I.subschemeι ↑U))
-- Mathlib.GroupTheory.GroupAction.Support
AddAction.supports_of_mem : ∀ (G : Type u_1) {α : Type u_3} [inst : VAdd G α] {s : Set α} {a : α}, a ∈ s → AddAction.Supports G s a
-- Init.Data.Prod
Prod.swap_prod_mk : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β}, (a, b).swap = (b, a)
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.mk.sizeOf_spec : ∀ (toPartOrd : PartOrd) [isFintype : Fintype ↑toPartOrd],
  sizeOf { toPartOrd := toPartOrd, isFintype := isFintype } = 1 + sizeOf toPartOrd + sizeOf isFintype
-- Mathlib.Order.Hom.Lattice
SupHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Max α} {inst_1 : Max β} {toFun : α → β}
  {map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b} {toFun_1 : α → β}
  {map_sup'_1 : ∀ (a b : α), toFun_1 (a ⊔ b) = toFun_1 a ⊔ toFun_1 b},
  { toFun := toFun, map_sup' := map_sup' } = { toFun := toFun_1, map_sup' := map_sup'_1 } → toFun = toFun_1
-- Mathlib.Topology.Algebra.ConstMulAction
smul_closure_orbit_subset : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Monoid M] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α] (c : M) (x : α), c • closure (MulAction.orbit M x) ⊆ closure (MulAction.orbit M x)
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.mutuallySingular_dirac : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] (x : α) (μ : MeasureTheory.Measure α)
  [MeasureTheory.NullSingletonClass μ], (MeasureTheory.Measure.dirac x).MutuallySingular μ
-- Mathlib.Data.Countable.Defs
not_countable : ∀ {α : Sort u} [Uncountable α], ¬Countable α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_alter_of_beq_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)}, (k == k') = false → (m.alter k f).contains k' = m.contains k'
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  (iso : E ≃ₗᵢ[𝕜] F), fderiv 𝕜 (⇑iso) x = ↑↑iso
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.eq_bot_iff_card : ∀ {M : Type u_1} [inst : Monoid M] {S : Submonoid M} [inst_1 : Fintype ↥S], S = ⊥ ↔ Fintype.card ↥S = 1
-- Mathlib.Topology.Connected.Basic
isConnected_connectedComponentIn_iff : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α} {F : Set α}, IsConnected (connectedComponentIn F x) ↔ x ∈ F
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
/-- If `Φ : LocalizerMorphism W₁ W₂` corresponds to a class `W₁` that is
induced by `W₂` via the fully faithful functor `Φ.functor` and we
have functorial right resolutions given by a functor `ρ : C₂ ⥤ C₁`, then
this is the natural transformation `𝟭 C₁ ⟶ Φ.functor ⋙ ρ` induced
by `i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor`.  -/
CategoryTheory.LocalizerMorphism.functorialRightResolutions.ι : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {ρ : CategoryTheory.Functor C₂ C₁} →
                (CategoryTheory.Functor.id C₂ ⟶ ρ.comp Φ.functor) →
                  [Φ.functor.Full] → [Φ.functor.Faithful] → CategoryTheory.Functor.id C₁ ⟶ Φ.functor.comp ρ
-- Mathlib.RingTheory.Perfection
Perfection.coeff_pow_p : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] (f : Perfection R p)
  (n : ℕ), (Perfection.coeff R p (n + 1)) (f ^ p) = (Perfection.coeff R p n) f
-- Lean.Widget.Diff
/-- Decorates the given goal `i₁` with a diff by comparing with goal `g₀`.
If `useAfter` is true then `i₁` is _after_ and `g₀` is _before_. Otherwise they are swapped.  -/
_private.Lean.Widget.Diff.0.Lean.Widget.diffInteractiveGoal : Bool → Lean.MVarId → Lean.Widget.InteractiveGoal → Lean.MetaM Lean.Widget.InteractiveGoal
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.centralizer_centralizer_centralizer : ∀ (M : Type u_1) [inst : AddMonoid M] {s : Set M},
  AddSubmonoid.centralizer s.addCentralizer.addCentralizer = AddSubmonoid.centralizer s
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.toMeasure_toOuterMeasure : ∀ {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms ≤ m.caratheodory),
  (m.toMeasure h).toOuterMeasure = m.trim
-- Init.Data.List.Lemmas
List.mem_append : ∀ {α : Type u_1} {a : α} {s t : List α}, a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_toReal : ∀ (r : NNReal), (↑r).toReal = ↑r
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.congr : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] [Module.Invertible R M] (e : M ≃ₗ[R] N), Module.Invertible R N
-- Mathlib.Data.Nat.Factorial.SuperFactorial
/-- `Nat.superFactorial n` is the superfactorial of `n`.  -/
Nat.superFactorial : ℕ → ℕ
-- Init.Data.Nat.Lemmas
Nat.mul_right_inj : ∀ {a b c : ℕ}, a ≠ 0 → (a * b = a * c ↔ b = c)
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.mem_supp_iff : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V} {v : V} {C : G.ComponentCompl K},
  v ∈ C ↔ ∃ (vK : v ∉ K), G.componentComplMk vK = C
-- Std.Http.Protocol.H1.Parser
/-- Parses a single ASCII hex digit and returns its numeric value (`0`–`15`).
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.hexDigit : Std.Internal.Parsec.ByteArray.Parser UInt8
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit.eq_1 : ∀ {n : ℕ} (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (foundContradiction : Bool)
  (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) (b : Bool),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) (l, b) =
    if Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b assignments[↑l]! = true then
      (units, assignments, foundContradiction)
    else
      have units := units.push (l, b);
      have assignments_1 := assignments.modify (↑l) (Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment b);
      have foundContradiction :=
        foundContradiction || assignments[↑l]! != Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned;
      (units, assignments_1, foundContradiction)
-- Mathlib.Data.Set.Prod
Set.offDiag_singleton : ∀ {α : Type u_1} (a : α), {a}.offDiag = ∅
-- Mathlib.CategoryTheory.Limits.MorphismProperty
/-- If `Comma L R` has limits of shape `J` and `Comma L R` is closed under limits of shape
`J`, then `forget L R P ⊤ ⊤` creates limits of shape `J`.  -/
CategoryTheory.MorphismProperty.Comma.forgetCreatesLimitsOfShapeOfClosed : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      {A : Type u_2} →
        {B : Type u_3} →
          {J : Type u_4} →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} A] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} B] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} J] →
                  {L : CategoryTheory.Functor A T} →
                    {R : CategoryTheory.Functor B T} →
                      [CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.Comma L R)] →
                        [(CategoryTheory.MorphismProperty.commaObj L R P).IsClosedUnderLimitsOfShape J] →
                          CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.eq_loopyOn_or_rankPos : ∀ {α : Type u_1} (M : Matroid α), M = Matroid.loopyOn M.E ∨ M.RankPos
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.Iso.hom_inv_id_eval : ∀ {C : Type u_1} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : CategoryTheory.GradedObject J C}
  (e : X ≅ Y) (j : J), CategoryTheory.CategoryStruct.comp (e.hom j) (e.inv j) = CategoryTheory.CategoryStruct.id (X j)
-- Lean.Compiler.IR.Basic
/-- Join point identifier  -/
Lean.IR.JoinPointId : Type
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.limitIsoOfIsRightKanExtension_inv_π : ∀ {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) [inst_3 : F'.IsRightKanExtension α] [inst_4 : CategoryTheory.Limits.HasLimit F]
  [inst_5 : CategoryTheory.Limits.HasLimit F'] (i : C),
  CategoryTheory.CategoryStruct.comp (F'.limitIsoOfIsRightKanExtension α).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F' (L.obj i)) (α.app i)) =
    CategoryTheory.Limits.limit.π F i
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.isInducing : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsClosedEmbedding f → Topology.IsInducing f
-- Mathlib.Combinatorics.SimpleGraph.Partition
SimpleGraph.Partition.partOfVertex_mem : ∀ {V : Type u} {G : SimpleGraph V} (P : G.Partition) (v : V), P.partOfVertex v ∈ P.parts
-- Mathlib.MeasureTheory.Measure.Restrict
/-- Restrict a measure `μ` to a set `s`.  -/
MeasureTheory.Measure.restrict : {α : Type u_2} → {_m0 : MeasurableSpace α} → MeasureTheory.Measure α → Set α → MeasureTheory.Measure α
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardPushforwardAdj_unit_app_val_app : ∀ {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} {G : CategoryTheory.Functor D C} {S : CategoryTheory.Sheaf J RingCat}
  {R : CategoryTheory.Sheaf K RingCat} [inst_2 : F.IsContinuous J K] [inst_3 : G.IsContinuous K J] (adj : F ⊣ G)
  (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S)
  (H₁ :
    CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.counit) R.obj =
      CategoryTheory.CategoryStruct.comp ψ.hom (G.op.whiskerLeft φ.hom))
  (H₂ :
    CategoryTheory.CategoryStruct.comp φ.hom
        (CategoryTheory.CategoryStruct.comp (F.op.whiskerLeft ψ.hom)
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.unit) S.obj)) =
      CategoryTheory.CategoryStruct.id S.obj)
  (M : SheafOfModules R) (U : Dᵒᵖ) (x : ↑(((CategoryTheory.Functor.id (SheafOfModules R)).obj M).val.obj U)),
  (CategoryTheory.ConcreteCategory.hom
        (((SheafOfModules.pushforwardPushforwardAdj adj φ ψ H₁ H₂).unit.app M).val.app U))
      x =
    (CategoryTheory.ConcreteCategory.hom (M.val.map (adj.counit.app (Opposite.unop U)).op)) x
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.isNilpotent_of_top_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [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] [LieModule R L M],
  LieModule.IsNilpotent (↥⊤) M ↔ LieModule.IsNilpotent L M
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.instFromJsonAbsoluteLspSemanticToken.fromJson : Lean.Json → Except String Lean.Server.FileWorker.AbsoluteLspSemanticToken
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- The isomorphism between homology groups induced by a group isomorphism `e : G ≃* H` and a
isomorphism between representations (restricted by `e`).  -/
groupHomology.mapIso : {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} →
            (e : G ≃* H) →
              (e' : ↑A ≃ₗ[k] ↑B) →
                (∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e') → (n : ℕ) → groupHomology A n ≅ groupHomology B n
-- Mathlib.CategoryTheory.Functor.OfSequence
/-- The functor `ℕᵒᵖ ⥤ C` constructed from a sequence of
morphisms `f : X (n + 1) ⟶ X n` for all `n : ℕ`.  -/
CategoryTheory.Functor.ofOpSequence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : ℕ → C} → ((n : ℕ) → X (n + 1) ⟶ X n) → CategoryTheory.Functor ℕᵒᵖ C
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.hurwitzZetaEven.eq_1 : ∀ (a : UnitAddCircle),
  HurwitzZeta.hurwitzZetaEven a =
    Function.update (fun s => HurwitzZeta.completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_truncLT_of_le : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] {c i : Γ},
  c ≤ i → ∀ (x : HahnSeries Γ R), ((HahnSeries.truncLT c) x).coeff i = 0
-- Mathlib.Analysis.Normed.Module.RCLike.Real
closure_ball : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ},
  r ≠ 0 → closure (Metric.ball x r) = Metric.closedBall x r
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
/-- Combine two `OpenPartialHomeomorph`s using `Set.piecewise`. The source of the new
`OpenPartialHomeomorph` is `s.ite e.source e'.source = e.source ∩ s ∪ e'.source \ s`, and similarly
for target.  The function sends `e.source ∩ s` to `e.target ∩ t` using `e` and
`e'.source \ s` to `e'.target \ t` using `e'`, and similarly for the inverse function.
To ensure the maps `toFun` and `invFun` are inverse of each other on the new `source` and `target`,
the definition assumes that the sets `s` and `t` are related both by `e.is_image` and `e'.is_image`.
To ensure that the new maps are continuous on `source`/`target`, it also assumes that `e.source` and
`e'.source` meet `frontier s` on the same set and `e x = e' x` on this intersection.  -/
OpenPartialHomeomorph.piecewise : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e e' : OpenPartialHomeomorph X Y) →
          (s : Set X) →
            (t : Set Y) →
              [(x : X) → Decidable (x ∈ s)] →
                [(y : Y) → Decidable (y ∈ t)] →
                  e.IsImage s t →
                    e'.IsImage s t →
                      e.source ∩ frontier s = e'.source ∩ frontier s →
                        Set.EqOn (↑e) (↑e') (e.source ∩ frontier s) → OpenPartialHomeomorph X Y
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_pow : ∀ {R : Type u_1} [inst : Semiring R] (s : Subsemiring R) (x : ↥s) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_zsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIcoDiv hp (a + m • p) b = toIcoDiv hp a b - m
-- Mathlib.Data.Set.Sups
Set.sups_empty : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s : Set α}, s ⊻ ∅ = ∅
-- Mathlib.Order.Closure
GaloisConnection.closureOperator_apply : ∀ {α : Type u_1} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (gc : GaloisConnection l u) (x : α), gc.closureOperator x = u (l x)
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.AsSmall.down_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : CategoryTheory.AsSmall C),
  CategoryTheory.AsSmall.down.obj X = X.down
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- The sequence with `n`-th term `n ^ s * n! / (s * (s + 1) * ... * (s + n))`, for complex `s`.
We will show that this tends to `Γ(s)` as `n → ∞`.  -/
Complex.GammaSeq : ℂ → ℕ → ℂ
-- Aesop.RuleSet
/-- Safe rules registered in this rule set.
 -/
Aesop.BaseRuleSet.safeRules : Aesop.BaseRuleSet → Aesop.Index Aesop.SafeRuleInfo
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.instIsFiniteTypeOfEpi : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N)
  [inst_3 : CategoryTheory.Epi p] [σ.IsFiniteType], (σ.ofEpi p).IsFiniteType
-- Init.Data.BitVec.Lemmas
/-- Variant of `toNat_cons` using `+` instead of `|||`.  -/
BitVec.toNat_cons' : ∀ {w : ℕ} {a : Bool} {x : BitVec w}, (BitVec.cons a x).toNat = a.toNat <<< w + x.toNat