mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.pullback_addMonoidHom.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : R1Space α] [inst_2 : AddGroup α]
  [inst_3 : TopologicalSpace β] [inst_4 : R1Space β] [inst_5 : AddGroup β] [inst_6 : ContinuousAdd β]
  [inst_7 : NormedAddCommGroup γ] {φ : α →+ β} (hφ : Topology.IsClosedEmbedding ⇑φ)
  (f : CompactlySupportedContinuousMap β γ) (b : β),
  CompactlySupportedContinuousMap.pullback_addMonoidHom hφ f b =
    { toFun := fun a => f (b + φ a), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
-- Lean.Exception
/-- Tag used for `unknown identifier` messages.
This tag is used by the 'import unknown identifier' code action to detect messages that should
prompt the code action.
 -/
Lean.unknownIdentifierMessageTag : Lean.Name
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_rpow_inv_eq_iff : ∀ {x : ENNReal} {y : ℝ}, (x ^ y) ^ y⁻¹ = x ↔ y ≠ 0 ∨ x = 1
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.closure.eq_1 : ∀ {M : Type u_1} [inst : Mul M] (s : Set M), Subsemigroup.closure s = sInf {S | s ⊆ ↑S}
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.instReflectsFiniteEffectiveEpiFamiliesComp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.ReflectsFiniteEffectiveEpiFamilies]
  [G.ReflectsFiniteEffectiveEpiFamilies], (F.comp G).ReflectsFiniteEffectiveEpiFamilies
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonRenameOptions : Lean.ToJson Lean.Lsp.RenameOptions
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- See also `SkewPolynomial.sum_add`.  -/
SkewPolynomial.sum_add' : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : AddCommMonoid S] (p : SkewPolynomial R) (f g : ℕ → R → S),
  p.sum (f + g) = p.sum f + p.sum g
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left : ∀ {S : AlgebraicGeometry.Scheme} {X : CategoryTheory.Over S} (𝒰 : X.left.OpenCover)
  [inst : CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  {Y : CategoryTheory.Over S} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left)
  (h :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) (g j) = g i)
  (w : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.f i) X.hom)
  (i : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (𝒰.f i)
      (CategoryTheory.Over.Hom.left (𝒰.glueMorphismsOverOfLocallyDirected g ⋯ w)) =
    g i
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.toStarMonoidHom_coe : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Star A] [inst_3 : Star B] (f : A ≃⋆* B)
  (a : A), f.toStarMonoidHom a = f a
-- Std.Time.Date.Unit.Week
Std.Time.Week.OfYear.instLawfulEqOrdOrdinal : Std.LawfulEqOrd Std.Time.Week.OfYear.Ordinal
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.toAddMonoidHom_toContinuousAddMonoidHom : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {F : Type u_7} [inst_4 : FunLike F A B] [inst_5 : AddMonoidHomClass F A B]
  [inst_6 : ContinuousMapClass F A B] (f : F), ↑↑f = ↑f
-- Mathlib.Data.Multiset.Bind
Multiset.filterMap_bind : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (f : α → Multiset β) (g : β → Option γ),
  Multiset.filterMap g (m.bind f) = m.bind fun a => Multiset.filterMap g (f a)
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.map_comp : ∀ {M : Type u} {N : Type v} {P : Type w} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddMonoid P] (f : M →+ N)
  (g : N →+ P), AddUnits.map (g.comp f) = (AddUnits.map g).comp (AddUnits.map f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, t.getKeyD a fallback = (t.getKey? a).getD fallback
-- Mathlib.Combinatorics.Additive.CauchyDavenport
/-- The **Cauchy-Davenport theorem** for torsion-free groups. The size of `s + t` is lower-bounded
by `|s| + |t| - 1`.  -/
cauchy_davenport_of_isAddTorsionFree : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] [IsAddTorsionFree G] {s t : Finset G},
  s.Nonempty → t.Nonempty → s.card + t.card - 1 ≤ (s + t).card
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.fromOpcycles_op_cyclesOpIso_inv_assoc : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [inst_2 : K.HasHomology i]
  (j : ι) {Z : Vᵒᵖ} (h : K.op.cycles i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j).op
      (CategoryTheory.CategoryStruct.comp (K.cyclesOpIso i).inv h) =
    CategoryTheory.CategoryStruct.comp (K.op.toCycles j i) h
-- Mathlib.Topology.Homeomorph.Defs
HomeomorphClass.mk : ∀ {F : Type u_5} {A : outParam (Type u_6)} {B : outParam (Type u_7)} [inst : TopologicalSpace A]
  [inst_1 : TopologicalSpace B] [h : EquivLike F A B],
  (∀ (f : F), Continuous ⇑f) → (∀ (f : F), Continuous (EquivLike.inv f)) → HomeomorphClass F A B
-- Mathlib.Topology.Sequences
IsSeqCompact.exists_tendsto : ∀ {X : Type u_1} [inst : UniformSpace X] {s : Set X},
  IsSeqCompact s → ∀ {u : ℕ → X}, (∀ (n : ℕ), u n ∈ s) → CauchySeq u → ∃ x ∈ s, Filter.Tendsto u Filter.atTop (nhds x)
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.Heart.additive_ι : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Preadditive C}
  {inst_2 : CategoryTheory.Limits.HasZeroObject C} {inst_3 : CategoryTheory.HasShift C ℤ}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  {t : CategoryTheory.Triangulated.TStructure C} {H : Type u'} {inst_6 : CategoryTheory.Category.{v', u'} H}
  {inst_7 : CategoryTheory.Preadditive H} [self : t.Heart H],
  (CategoryTheory.Triangulated.TStructure.Heart.ι t).Additive
-- Std.Data.Iterators.Lemmas.Producers.Empty
Std.Iter.toArray_empty : ∀ {β : Type u_1}, (Std.Iter.empty β).toArray = #[]
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rio.toArray_iter_eq_toArray : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_5 : Std.Rxo.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rio α}, r.iter.toArray = r.toArray
-- Mathlib.Data.Part
Part.instAdd.eq_1 : ∀ {α : Type u_1} [inst : Add α], Part.instAdd = { add := fun a b => (fun x1 x2 => x1 + x2) <$> a <*> b }
-- Mathlib.MeasureTheory.Measure.Restrict
MeasurableEmbedding.comap_map : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f →
    ∀ (μ : MeasureTheory.Measure α), MeasureTheory.Measure.comap f (MeasureTheory.Measure.map f μ) = μ
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.Hom.birational : ∀ {X U : AlgebraicGeometry.Scheme} (f : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsDominant f],
  U.Birational X
-- Mathlib.CategoryTheory.Join.Sum
CategoryTheory.Join.inrCompFromSum_hom_app : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (X : D),
  (CategoryTheory.Join.inrCompFromSum C D).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right X)
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Circle averages do not change when shifting the angle.  -/
Real.circleAverage_eq_integral_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ} (η : ℝ),
  Real.circleAverage f c R = (2 * Real.pi)⁻¹ • ∫ (θ : ℝ) in 0..2 * Real.pi, f (circleMap c R (θ + η))
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.cyclotomic.dvd_X_pow_sub_one : ∀ (n : ℕ) (R : Type u_1) [inst : Ring R], Polynomial.cyclotomic n R ∣ Polynomial.X ^ n - 1
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.abs_sum_of_nonneg' : ∀ {ι : Type u_1} {G : Type u_9} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [AddLeftMono G] {f : ι → G}
  {s : Finset ι}, (∀ (i : ι), 0 ≤ f i) → |∑ i ∈ s, f i| = ∑ i ∈ s, f i
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_singleR : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {lk : α} {lv : β lk} {ll lr r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.singleR k v lk lv ll lr r).toListModel =
    ll.toListModel ++ ⟨lk, lv⟩ :: lr.toListModel ++ ⟨k, v⟩ :: r.toListModel
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instIsTriangulatedPlusQh : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], DerivedCategory.Plus.Qh.IsTriangulated
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureResult.mk.inj : ∀ {script : List Aesop.Script.Step} {postState : Lean.Meta.SavedState} {script_1 : List Aesop.Script.Step}
  {postState_1 : Lean.Meta.SavedState},
  { script := script, postState := postState } = { script := script_1, postState := postState_1 } →
    script = script_1 ∧ postState = postState_1
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.MethodsRef.toMethodsImpl : Lean.Meta.Sym.DSimp.MethodsRef → Lean.Meta.Sym.DSimp.Methods
-- Mathlib.ModelTheory.Encoding
/-- Decodes a list of symbols as a list of formulas.  -/
FirstOrder.Language.BoundedFormula.listDecode : {L : FirstOrder.Language} →
  {α : Type u'} →
    List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) → List ((n : ℕ) × L.BoundedFormula α n)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.revlexWF.eq_def : ∀ (m₁ m₂ : Lean.Grind.CommRing.Mon),
  m₁.revlexWF m₂ =
    match m₁, m₂ with
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => Ordering.eq
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.mult p m => Ordering.gt
    | Lean.Grind.CommRing.Mon.mult p m, Lean.Grind.CommRing.Mon.unit => Ordering.lt
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ =>
      bif pw₁.x == pw₂.x then (m₁.revlexWF m₂).then (Lean.Grind.CommRing.powerRevlex pw₁.k pw₂.k)
      else
        bif Nat.blt pw₁.x pw₂.x then (m₁.revlexWF (Lean.Grind.CommRing.Mon.mult pw₂ m₂)).then Ordering.lt
        else ((Lean.Grind.CommRing.Mon.mult pw₁ m₁).revlexWF m₂).then Ordering.gt
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.zero : Lean.Grind.Linarith.Expr
-- Mathlib.Data.String.Basic
_private.Mathlib.Data.String.Basic.0.String.le_iff_not_lt : ∀ {s₁ s₂ : String}, s₁ ≤ s₂ ↔ ¬s₂ < s₁
-- Mathlib.Algebra.Group.Action.TransferInstance
/-- Transfer `MulDistribMulAction` across an `Equiv`  -/
Equiv.mulDistribMulAction : (M : Type u_1) →
  {N : Type u_2} →
    {O : Type u_3} →
      [inst : Monoid M] → [inst_1 : Monoid O] → (e : N ≃ O) → [MulDistribMulAction M O] → MulDistribMulAction M N
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_le_of_le_add_int : ∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ}, f x ≤ x + ↑m → f.translationNumber ≤ ↑m
-- Mathlib.Algebra.GradedMonoid
SetLike.GradedMonoid.mk : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Monoid R] [inst_2 : AddMonoid ι]
  {A : ι → S} [toGradedOne : SetLike.GradedOne A] [toGradedMul : SetLike.GradedMul A], SetLike.GradedMonoid A
-- Mathlib.Algebra.GroupWithZero.Defs
GroupWithZero.toDiv : {G₀ : Type u} → [self : GroupWithZero G₀] → Div G₀
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_eq_of_subset_of_ae_sdiff_eq_zero : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s t : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G]
  {B : E →L[ℝ] F →L[ℝ] G},
  MeasurableSet s →
    MeasurableSet t →
      s ⊆ t →
        (∀ᵐ (x : X) ∂μ.variation.restrict (t \ s), f x = 0) →
          ∫ᵛ (x : X) in t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsStationary.univ : ∀ {α : Type v} [inst : LinearOrder α] [Nonempty α], IsStationary Set.univ
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.left_quotientAction : ∀ {G : Type u} [inst : Group G] (H : Subgroup G), MulAction.QuotientAction G H
-- Mathlib.Algebra.Lie.Rank
/-- Let `M` be a representation of a Lie algebra `L` over a nontrivial commutative ring `R`,
and assume that `L` and `M` are finite free as `R`-module.
Then the coefficients of the characteristic polynomial of `⁅x, ·⁆` are polynomial in `x`.
The *rank* of `M` is the smallest `n` for which the `n`-th coefficient is not the zero polynomial.
 -/
LieModule.rank : (R : Type u_1) →
  (L : Type u_3) →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [Module.Finite R L] →
              [Module.Free R L] →
                [inst_5 : AddCommGroup M] →
                  [inst_6 : Module R M] →
                    [inst_7 : LieRingModule L M] → [LieModule R L M] → [Module.Finite R M] → [Module.Free R M] → ℕ
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
/-- Given `P : ObjectProperty C`, and a presentation `P.ColimitOfShape J X`
of an object `X : C`, this is the induced functor `J ⥤ CostructuredArrow P.ι X`.  -/
CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {J : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} J] →
          {X : C} → P.ColimitOfShape J X → CategoryTheory.Functor J (CategoryTheory.CostructuredArrow P.ι X)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_beq : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, Option.all (fun x => x == k) (m.getKey? k) = true
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_eq_some_iff : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {k : α} {v : β},
  Std.Internal.List.getValue? k l = some v ↔
    ∃ (h : Std.Internal.List.containsKey k l = true), Std.Internal.List.getValue k l h = v
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.neg : ∀ {f : ℝ → ℝ}, AkraBazziRecurrence.GrowsPolynomially f → AkraBazziRecurrence.GrowsPolynomially (-f)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H1IsoOfIsTrivial_inv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} [inst_2 : A.IsTrivial]
  (f : Additive G →+ ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.H1IsoOfIsTrivial A).inv) f =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.H1π A))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cocycles₁IsoOfIsTrivial A).inv) f)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
PiTensorProduct.toDualContinuousMultilinearMap_apply_apply : ∀ {ι : Type uι} [inst : Fintype ι] {𝕜 : Type u𝕜} [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type uE}
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (F : Type u_1)
  [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] (x : PiTensorProduct 𝕜 fun i => E i)
  (x_1 : ContinuousMultilinearMap 𝕜 E F),
  ((PiTensorProduct.toDualContinuousMultilinearMap F) x) x_1 = (PiTensorProduct.lift x_1.toMultilinearMap) x
-- Mathlib.Tactic.Linarith.Frontend
_private.Mathlib.Tactic.Linarith.Frontend.0.Mathlib.Tactic.instEvalExprLinarithConfig.unsafe_1 : Lean.Expr → Lean.MetaM Mathlib.Tactic.Linarith.LinarithConfig
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_filter!_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filter! f t).isEmpty = true ↔
      ∀ (k : α) (h : Std.DTreeMap.Internal.Impl.contains k t = true), f k (t.get k h) = false)
-- Mathlib.SetTheory.ZFC.Basic
/-- The range of a type-indexed family of sets.  -/
ZFSet.range : {α : Type u_1} → [Small.{u, u_1} α] → (α → ZFSet.{u}) → ZFSet.{u}
-- Lean.Elab.Command
/-- If `hint?` is `some hint`, establishes a new context for macro scope naming and runs `act` in it,
otherwise runs `act` directly without changes.

Context names as documented in Note `Macro Scope Representation` help with avoiding rebuilds and
`prefer_native` lookup misses from macro scopes in declaration names and other exported information.
This function establishes a new context with a globally unique name by combining the name of the
current module with `hint` while also checking for previously used `hint`s in the same module.
Thus `hint` does not need to be unique but ensuring it is usually unique helps with keeping the
context name stable.

In the current implementation, we call `withInitQuotContext` once in `elabCommandTopLevel` using the
source input of the command as the hint. This helps with keeping macro scopes stable on changes to
other parts of the file but not on changes to the command itself. Thus in each *declaration*
elaborator we call `withInitQuotContext` again with the declaration name(s) as a hint so that
changes to any other part of the declaration do not change the context name.
 -/
Lean.Elab.Command.withInitQuotContext : Option UInt64 → Lean.Elab.Command.CommandElabM Unit → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- A binary cofan in `Under X` is a colimit if its corresponding pushout cocone from `X` is a
colimit.  -/
CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          {c : CategoryTheory.Limits.PushoutCocone f g} →
            CategoryTheory.Limits.IsColimit c →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.functor.obj c)
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.sum_const : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable ι]
  (μ : ι → MeasureTheory.Measure β),
  (ProbabilityTheory.Kernel.sum fun n => ProbabilityTheory.Kernel.const α (μ n)) =
    ProbabilityTheory.Kernel.const α (MeasureTheory.Measure.sum μ)
-- Mathlib.Analysis.Calculus.FDeriv.Defs
hasFDerivWithinAt_iff_isLittleO : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {s : Set E} {x : E},
  HasFDerivWithinAt f f' s x ↔ (fun x' => f x' - f x - f' (x' - x)) =o[nhdsWithin x s] fun x' => x' - x
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.mem_torsion'_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_3)
  [inst_3 : CommMonoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M] (x : M),
  x ∈ Submodule.torsion' R M S ↔ ∃ a, a • x = 0
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `iteratedFDerivWithin_sub_apply`

---

The iterated derivative of the difference of two functions is the difference of the iterated
derivatives.
 -/
fun_iteratedFDerivWithin_sub_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] {s : Set E}
  {x : E} {i : ℕ} {f g : E → F},
  ContDiffWithinAt 𝕜 (↑i) f s x →
    ContDiffWithinAt 𝕜 (↑i) g s x →
      UniqueDiffOn 𝕜 s →
        x ∈ s →
          iteratedFDerivWithin 𝕜 i (fun i => f i - g i) s x =
            iteratedFDerivWithin 𝕜 i f s x - iteratedFDerivWithin 𝕜 i g s x
-- Batteries.Lean.Except
_private.Batteries.Lean.Except.0.ExceptT.bindCont.match_1.eq_1 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_1 a
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j)
  {D₁ D₂ : F.DescentData f}
  (φ :
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂)
  ⦃i : ι⦄ {Z : C} (q : Z ⟶ X i) ⦃j : ι'⦄ (a : Z ⟶ X' j)
  (fac : CategoryTheory.CategoryStruct.comp a (f' j) = CategoryTheory.CategoryStruct.comp q (f i)) (q' : Z ⟶ S)
  (a' : Z ⟶ X (α j))
  (hq' :
    autoParam (CategoryTheory.CategoryStruct.comp q (f i) = q')
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_eq._auto_1✝)
  (ha' :
    autoParam (CategoryTheory.CategoryStruct.comp a (p' j) = a')
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor_eq._auto_3✝),
  CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor✝ w φ q a fac =
    CategoryTheory.CategoryStruct.comp (D₁.hom q' q a' ⋯ ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (φ.hom j) a a' a' ⋯ ⋯) (D₂.hom q' a' q ⋯ ⋯))
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- An algebra of an endofunctor; `str` stands for "structure morphism"  -/
CategoryTheory.Endofunctor.Algebra : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C C → Type (max u v)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited γ] {f : α → β → Option γ} {k k' : α},
  t.getKey? k = some k' → (Std.TreeMap.filterMap f t)[k]! = (t[k]?.bind (f k')).get!
-- Mathlib.Topology.Algebra.Module.Cardinality
/-- In a topological vector space over a nontrivially normed field, any neighborhood of zero has
the same cardinality as the whole space.

See also `cardinal_eq_of_mem_nhds`.  -/
cardinal_eq_of_mem_nhds_zero : ∀ {E : Type u_1} (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : Zero E] [inst_2 : MulActionWithZero 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E}, s ∈ nhds 0 → Cardinal.mk ↑s = Cardinal.mk E
-- Mathlib.LinearAlgebra.Matrix.Reindex
/-- Reindexing both indices along the same equivalence preserves the determinant.

For the `simp` version of this lemma, see `det_submatrix_equiv_self`.
 -/
Matrix.det_reindexAlgEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) (B : Type u_13) [inst : CommSemiring R] [inst_1 : CommRing B]
  [inst_2 : Algebra R B] [inst_3 : Fintype m] [inst_4 : DecidableEq m] [inst_5 : Fintype n] [inst_6 : DecidableEq n]
  (e : m ≃ n) (A : Matrix m m B), ((Matrix.reindexAlgEquiv R B e) A).det = A.det
-- Mathlib.Data.Num.ZNum
ZNum.bit1.eq_1 : ZNum.zero.bit1 = 1