mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.preimage_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₁), ⇑f.symm ⁻¹' s = ⇑f '' s
-- Mathlib.RingTheory.WittVector.IsPoly
/-- The coefficients of `1 : 𝕎 R` as polynomials.  -/
WittVector.onePoly : ℕ → MvPolynomial ℕ ℤ
-- Mathlib.LinearAlgebra.InvariantBasisNumber
invariantBasisNumber_iff : ∀ (R : Type u) [inst : Semiring R], InvariantBasisNumber R ↔ ∀ {n m : ℕ} (a : (Fin n → R) ≃ₗ[R] Fin m → R), n = m
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.coe_bot : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], ↑⊥ = {0}
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Icc_add_one_sub_one_eq_Ioo : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [inst_4 : Sub α] [SuccAddOrder α] [PredSubOrder α] [Nontrivial α] (a b : α),
  Finset.Icc (a + 1) (b - 1) = Finset.Ioo a b
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.iff : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty},
  AlgebraicGeometry.HasAffineProperty P Q ↔
    AlgebraicGeometry.IsZariskiLocalAtTarget P ∧ Q = AlgebraicGeometry.AffineTargetMorphismProperty.of P
-- Mathlib.Topology.ContinuousOn
continuousOn_isOpen_of_generateFrom : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_5} {s : Set α} {T : Set (Set β)} {f : α → β},
  (∀ t ∈ T, IsOpen (s ∩ f ⁻¹' t)) → ContinuousOn f s
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.Walk.pathGraphHomToSubgraph.eq_1 : ∀ {V : Type u_3} {G : SimpleGraph V} {u v : V} (w : G.Walk u v),
  w.pathGraphHomToSubgraph = { toFun := fun n => ⟨w.support[n], ⋯⟩, map_rel' := ⋯ }
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.insert k).min? = some (t.min?.elim k fun k' => if cmp k k' = Ordering.lt then k else k')
-- Aesop.Index.Basic
Aesop.IndexMatchLocation.hyp.inj : ∀ {ldecl ldecl_1 : Lean.LocalDecl},
  Aesop.IndexMatchLocation.hyp ldecl = Aesop.IndexMatchLocation.hyp ldecl_1 → ldecl = ldecl_1
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.quotientKerRightHomEquivRight.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  (S : GroupExtension N E G), S.quotientKerRightHomEquivRight = QuotientGroup.quotientKerEquivOfSurjective S.rightHom ⋯
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- `sphere x ε` is the set of all points `y` with `dist y x = ε`  -/
Metric.sphere : {α : Type u} → [PseudoMetricSpace α] → α → ℝ → Set α
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousWithinAt.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  {r : α → β → Prop} {x : γ} {g : γ → α} {s : Set γ} {t : Set α},
  SemicontinuousWithinAt r t (g x) → ContinuousWithinAt g s x → Set.MapsTo g s t → SemicontinuousWithinAt (r ∘ g) s x
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.aut_one : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁],
  1 = AlgEquiv.refl
-- Mathlib.FieldTheory.PerfectClosure
_private.Mathlib.FieldTheory.PerfectClosure.0.PerfectClosure.mul_aux_right : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x y1 y2 : ℕ × K),
  PerfectClosure.R K p y1 y2 →
    PerfectClosure.mk K p (x.1 + y1.1, (⇑(frobenius K p))^[y1.1] x.2 * (⇑(frobenius K p))^[x.1] y1.2) =
      PerfectClosure.mk K p (x.1 + y2.1, (⇑(frobenius K p))^[y2.1] x.2 * (⇑(frobenius K p))^[x.1] y2.2)
-- Mathlib.Algebra.Group.Hom.Instances
/-- The expression `fun g m ↦ g (f m)` as a `MonoidHom`.
Equivalently, `(fun g ↦ MonoidHom.comp g f)` as a `MonoidHom`.  -/
MonoidHom.compHom' : {M : Type uM} →
  {N : Type uN} →
    {P : Type uP} →
      [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : CommMonoid P] → (M →* N) → (N →* P) →* M →* P
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.revMatchesAt_iff_revMatchesAt_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.RevMatchesAt p pos ↔ String.Slice.Pattern.Model.RevMatchesAt (fun x => decide (p x)) pos
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.ball_eq_or_disjoint : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x y : X) (r : ℝ),
  Metric.ball x r = Metric.ball y r ∨ Disjoint (Metric.ball x r) (Metric.ball y r)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isOpen_iff_of_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set (OnePoint X)},
  OnePoint.infty ∈ s → (IsOpen s ↔ IsClosed (OnePoint.some ⁻¹' s)ᶜ ∧ IsCompact (OnePoint.some ⁻¹' s)ᶜ)
-- Mathlib.Order.Interval.Set.Disjoint
Set.Iio_disjoint_Ioi_iff : ∀ {α : Type v} [inst : Preorder α] {a b : α} [DenselyOrdered α], Disjoint (Set.Iio a) (Set.Ioi b) ↔ ¬b < a
-- Batteries.Data.List.Lemmas
List.findIdxs_take : ∀ {α : Type u_1} {xs : List α} {n : ℕ} {p : α → Bool} {s : ℕ},
  List.findIdxs p (List.take n xs) s = List.take (List.countP p (List.take n xs)) (List.findIdxs p xs s)
-- Mathlib.GroupTheory.OrderOfElement
/-- A group element has finite additive order iff its order is positive.  -/
addOrderOf_pos_iff : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, 0 < addOrderOf x ↔ IsOfFinAddOrder x
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_zsmul : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (m : ℤ) (x : WittVector p R),
  WittVector.ghostFun✝ (m • x) = m • WittVector.ghostFun✝ x
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.HoCat.weakEquivalence_resolutionMap_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y),
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap f) ↔
    HomotopicalAlgebra.WeakEquivalence f
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_neg : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Neg α] (M : Matrix m n α), (-M).transpose = -M.transpose
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
_private.Mathlib.NumberTheory.DiophantineApproximation.Basic.0.Real.invariant : ∀ {ξ : ℝ} {u v : ℤ}, 2 ≤ v → Real.ContfracLegendre.Ass ξ u v → Real.ContfracLegendre.Ass (Int.fract ξ)⁻¹ v (u - ⌊ξ⌋ * v)
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.Equiv.symm : ∀ {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : LawfulMonad m] {ita itb : Std.BundledIterM m β},
  Std.BundledIterM.Equiv m β ita itb → Std.BundledIterM.Equiv m β itb ita
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.brecOn.eq : ∀ {R : Type u_1} {X : Type u_2} {motive : FreeAlgebra.Pre R X → Sort u} (t : FreeAlgebra.Pre R X)
  (F_1 : (t : FreeAlgebra.Pre R X) → FreeAlgebra.Pre.below t → motive t),
  FreeAlgebra.Pre.brecOn t F_1 = F_1 t (FreeAlgebra.Pre.brecOn.go t F_1).2
-- Mathlib.Data.Nat.WithBot
Nat.WithBot.coe_nonneg : ∀ {n : ℕ}, 0 ≤ ↑n
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
/-- The differential `E^{n}(f₃, f₄, f₅) ⟶ E^{n+1}(f₁, f₂, f₃)` that is
attached to a family of five composable morphisms `f₁`, `f₂`, `f₃`, `f₄`, `f₅`.  -/
CategoryTheory.Abelian.SpectralObject.d : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i₀ i₁ i₂ i₃ i₄ i₅ : ι} →
              (f₁ : i₀ ⟶ i₁) →
                (f₂ : i₁ ⟶ i₂) →
                  (f₃ : i₂ ⟶ i₃) →
                    (f₄ : i₃ ⟶ i₄) →
                      (f₅ : i₄ ⟶ i₅) →
                        (n₀ n₁ n₂ n₃ : ℤ) →
                          (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.d._auto_1) →
                            (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.d._auto_3) →
                              (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.d._auto_5) →
                                X.E f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mk : {α : Type u_2} → [inst : TopologicalSpace α] → (carrier : Set α) → IsOpen carrier → TopologicalSpace.Opens α
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_one_zero : Nat.testBit 1 0 = true
-- Mathlib.Tactic.NormNum.BigOperators
/-- If `s` unifies with `t`, convert a result for `s` to a result for `t`.

If `s` does not unify with `t`, this results in a type-incorrect proof.
 -/
Mathlib.Meta.List.ProveNilOrConsResult.uncheckedCast : {u v : Lean.Level} →
  {α : Q(Type u)} →
    {β : Q(Type v)} →
      (s : Q(List «$α»)) →
        (t : Q(List «$β»)) → Mathlib.Meta.List.ProveNilOrConsResult s → Mathlib.Meta.List.ProveNilOrConsResult t
-- Mathlib.Order.Std
/-- ≤ is decidable.  -/
LinearOrder.OfStdArgs.decidableLE : {α : Type u_1} → (self : LinearOrder.OfStdArgs α) → DecidableLE α
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldl_ι : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N)
  (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N) (m : M),
  ((CliffordAlgebra.foldl Q f hf) n) ((CliffordAlgebra.ι Q) m) = (f m) n
-- Mathlib.Topology.UniformSpace.Basic
entourageProd.eq_1 : ∀ {α : Type ua} {β : Type ub} (u : SetRel α α) (v : SetRel β β),
  entourageProd u v = {((a₁, b₁), a₂, b₂) | (a₁, a₂) ∈ u ∧ (b₁, b₂) ∈ v}
-- Mathlib.Data.ENNReal.Operations
ENNReal.mem_Ioo_self_sub_add : ∀ {x ε₁ ε₂ : ENNReal}, x ≠ ⊤ → x ≠ 0 → ε₁ ≠ 0 → ε₂ ≠ 0 → x ∈ Set.Ioo (x - ε₁) (x + ε₂)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
List.stronglyMeasurable_fun_sum : ∀ {α : Type u_1} {M : Type u_5} [inst : AddMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M]
  {m : MeasurableSpace α} (l : List (α → M)),
  (∀ f ∈ l, MeasureTheory.StronglyMeasurable f) →
    MeasureTheory.StronglyMeasurable fun x => (List.map (fun f => f x) l).sum
-- Batteries.Data.List.Matcher
List.Matcher.toMatcher : {α : Type u_1} → List.Matcher α → Array.Matcher α
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.commandElab_stx_quot_ : Lean.ParserDescr
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.span_gramSchmidtNormed : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E)
  (s : Set ι),
  Submodule.span 𝕜 (InnerProductSpace.gramSchmidtNormed 𝕜 f '' s) =
    Submodule.span 𝕜 (InnerProductSpace.gramSchmidt 𝕜 f '' s)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instFirstCountableTopology : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], FirstCountableTopology (SchwartzMap E F)
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.dirac_apply : ∀ {X : Type u_1} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : CommRing R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalRing R] (x : X) (f : C(X, R)), (AbstractMeasure.dirac R x) f = f x
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.eventually_atTop : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] {p : α → Prop} [Nonempty α],
  (∀ᶠ (x : α) in Filter.atTop, p x) ↔ ∃ a, ∀ (b : α), a ≤ b → p b
-- Mathlib.Logic.Function.Basic
Function.surjective_comp_right_iff_injective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {γ : Type u_4} [Nontrivial γ],
  (Function.Surjective fun g => g ∘ f) ↔ Function.Injective f
-- Lean.CompactedRegion
_private.Lean.CompactedRegion.0.Lean.CompactedRegion.baseAddr : Lean.CompactedRegion → USize
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_pi_div_thirty_two : Real.sin (Real.pi / 32) = √(2 - √(2 + √(2 + √2))) / 2
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourierInv_comp_linearIsometry : ∀ {V : Type u_1} {W : Type u_2} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E]
  [inst_2 : NormedAddCommGroup V] [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V]
  [inst_6 : NormedAddCommGroup W] [inst_7 : InnerProductSpace ℝ W] [inst_8 : MeasurableSpace W] [inst_9 : BorelSpace W]
  [inst_10 : FiniteDimensional ℝ W] [inst_11 : FiniteDimensional ℝ V] (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W),
  FourierTransformInv.fourierInv (f ∘ ⇑A) w = FourierTransformInv.fourierInv f (A w)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.isAddRightInvariant_smul_nnreal : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] {μ : MeasureTheory.Measure G} [μ.IsAddRightInvariant]
  (c : NNReal), (c • μ).IsAddRightInvariant
-- Mathlib.Topology.Sets.VietorisTopology
/-- When `Set` is equipped with the Vietoris topology, the powerset of an open set is open.  -/
IsOpen.powerset_vietoris : ∀ {α : Type u_1} [inst : TopologicalSpace α] {U : Set α}, IsOpen U → IsOpen (𝒫 U)
-- Mathlib.Algebra.Module.Submodule.Finsupp
Submodule.mem_set_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (sR : Set R)
  (N : Submodule R M) (x : M) [SMulCommClass R R ↥N], x ∈ sR • N ↔ ∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m => r • m)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
/-- The natural transformation `L ⋙ (L.lan).obj G ⟶ L`.  -/
CategoryTheory.Functor.ranCounit : {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] →
        (L : CategoryTheory.Functor C D) →
          {H : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] →
                L.ran.comp ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) ⟶
                  CategoryTheory.Functor.id (CategoryTheory.Functor C H)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatch.State.mk.sizeOf_spec : ∀ (thmMap : Lean.Meta.Grind.EMatchTheoremsArray) (gmt : ℕ) (thms newThms : Lean.PArray Lean.Meta.Grind.EMatchTheorem)
  (numInstances numDelayedInstances num : ℕ) (preInstances : Lean.Meta.Grind.PreInstanceSet) (nextThmIdx : ℕ)
  (matchEqNames : Lean.PHashSet Lean.Name)
  (delayedThmInsts : Lean.PHashMap Lean.Meta.Sym.ExprPtr (List Lean.Meta.Grind.DelayedTheoremInstance)),
  sizeOf
      { thmMap := thmMap, gmt := gmt, thms := thms, newThms := newThms, numInstances := numInstances,
        numDelayedInstances := numDelayedInstances, num := num, preInstances := preInstances, nextThmIdx := nextThmIdx,
        matchEqNames := matchEqNames, delayedThmInsts := delayedThmInsts } =
    1 + sizeOf thmMap + sizeOf gmt + sizeOf thms + sizeOf newThms + sizeOf numInstances + sizeOf numDelayedInstances +
              sizeOf num +
            sizeOf preInstances +
          sizeOf nextThmIdx +
        sizeOf matchEqNames +
      sizeOf delayedThmInsts
-- Mathlib.Topology.Sheaves.EtaleSpace
TopCat.Presheaf.EtaleSpace.mk.sizeOf_spec : ∀ {X : TopCat} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {CC : C → Type v} {FC : C → C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {F : TopCat.Presheaf C X} [inst_4 : SizeOf C]
  [inst_5 : (a : C) → SizeOf (CC a)] [inst_6 : (a a_1 : C) → SizeOf (FC a a_1)] (base : ↑X)
  (germ : CategoryTheory.ToType (F.stalk base)), sizeOf { base := base, germ := germ } = 1 + sizeOf base + sizeOf germ
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- The naturality for the associator.  -/
Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality.mkNaturalityAssociator : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality m] →
    Mathlib.Tactic.BicategoryLike.NormalizedHom →
      Mathlib.Tactic.BicategoryLike.NormalizedHom →
        Mathlib.Tactic.BicategoryLike.NormalizedHom →
          Mathlib.Tactic.BicategoryLike.NormalizedHom →
            Mathlib.Tactic.BicategoryLike.Mor₁ →
              Mathlib.Tactic.BicategoryLike.Mor₁ →
                Mathlib.Tactic.BicategoryLike.Mor₁ →
                  Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                    Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Lean.Expr
-- Mathlib.Algebra.Group.Action.Opposite
MulOpposite.unop_smul_eq_unop_smul_unop : ∀ {M : Type u_1} {α : Type u_3} [inst : SMul M α] [inst_1 : SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (r : Mᵐᵒᵖ) (a : αᵐᵒᵖ),
  MulOpposite.unop (r • a) = MulOpposite.unop r • MulOpposite.unop a
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.baseSet : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] → {ι : Type u_5} → VectorBundleCore R B F ι → ι → Set B
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Functor.zero_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [inst_2 : CategoryTheory.Limits.HasZeroObject D] (X : C),
  CategoryTheory.Limits.IsZero (CategoryTheory.Functor.obj 0 X)
-- Init.Data.List.Attach
List.attachWith.congr_simp : ∀ {α : Type u_1} (l l_1 : List α) (e_l : l = l_1) (P : α → Prop) (H : ∀ x ∈ l, P x),
  l.attachWith P H = l_1.attachWith P ⋯
-- Std.Async.System
/-- Information about the current user.
 -/
Std.Async.System.SystemUser : Type
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Function.locallyFinsuppWithin.toClosedBall.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (r : ℝ),
  Function.locallyFinsuppWithin.toClosedBall r = Function.locallyFinsuppWithin.restrictMonoidHom ⋯
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.mem_toSubgroup_iff : ∀ {G : Type u_1} [inst : Group G] {H : FiniteIndexNormalSubgroup G} {g : G}, g ∈ H.toSubgroup ↔ g ∈ H
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Extension of scalars is a functor where an `R`-module `M` is sent to `S ⊗ M` and
`l : M1 ⟶ M2` is sent to `s ⊗ m ↦ s ⊗ l m`
 -/
ModuleCat.extendScalars : {R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → CategoryTheory.Functor (ModuleCat R) (ModuleCat S)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.bot_isClosedSubgraph : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β), ⊥.IsClosedSubgraph G
-- Init.Data.SInt.Lemmas
ISize.toInt_bmod_18446744073709551616 : ∀ (x : ISize), x.toInt.bmod 18446744073709551616 = x.toInt
-- Mathlib.Algebra.Category.Grp.EpiMono
CommGrpCat.mono_iff_ker_eq_bot : ∀ {A B : CommGrpCat} (f : A ⟶ B), CategoryTheory.Mono f ↔ (CommGrpCat.Hom.hom f).ker = ⊥
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.inv_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g)
  [inst_1 : CategoryTheory.IsIso sq],
  CategoryTheory.Arrow.Hom.left (CategoryTheory.inv sq) = CategoryTheory.inv (CategoryTheory.Arrow.Hom.left sq)
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Circle averages commute with scalar multiplication.  -/
Real.circleAverage_fun_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} [inst_2 : NormedDivisionRing 𝕜]
  [inst_3 : Module 𝕜 E] [NormSMulClass 𝕜 E] [SMulCommClass ℝ 𝕜 E] {f : ℂ → E} {c : ℂ} {R : ℝ} {a : 𝕜},
  Real.circleAverage (fun z => a • f z) c R = a • Real.circleAverage f c R
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ 1 ≤ 1` and `μ x ≠ 0`, then `smoothingFun μ x` is the limit of
`smoothingSeminormSeq μ x`.  -/
tendsto_smoothingFun_of_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R),
  μ 1 ≤ 1 → ∀ {x : R}, μ x ≠ 0 → Filter.Tendsto (smoothingSeminormSeq μ x) Filter.atTop (nhds (smoothingFun μ x))
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.feature__4 : Lean.ParserDescr
-- Std.Http.Data.Chunk
Std.Http.Chunk.ExtensionName.mk.inj : ∀ {value : String}
  {isValidExtensionName :
    autoParam (Std.Http.Chunk.IsValidExtensionName value) Std.Http.Chunk.ExtensionName.isValidExtensionName._autoParam}
  {value_1 : String}
  {isValidExtensionName_1 :
    autoParam (Std.Http.Chunk.IsValidExtensionName value_1)
      Std.Http.Chunk.ExtensionName.isValidExtensionName._autoParam},
  { value := value, isValidExtensionName := isValidExtensionName } =
      { value := value_1, isValidExtensionName := isValidExtensionName_1 } →
    value = value_1
-- Lean.Attributes
Lean.AttributeImplCore.name : Lean.AttributeImplCore → Lean.Name
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    Std.DTreeMap.Internal.Impl.Const.get? (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k =
      Std.DTreeMap.Internal.Impl.Const.get? t k
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
/-- `count p s` is the multiplicity of the irreducible `p` in the FactorSet `s`.

If `p` is not irreducible, `count p s` is defined to be `0`.  -/
Associates.count : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [DecidableEq (Associates α)] →
      [(p : Associates α) → Decidable (Irreducible p)] → Associates α → Associates.FactorSet α → ℕ
-- Mathlib.Analysis.Distribution.Sobolev
/-- Schwartz functions are in every Sobolev space.  -/
SchwartzMap.memSobolev : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] [inst_7 : CompleteSpace F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (f : SchwartzMap E F),
  TemperedDistribution.MemSobolev s p ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) f)
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- Applying `P` to a morphism of `Type`  -/
MvPFunctor.map : {n : ℕ} → (P : MvPFunctor.{u} n) → {α β : TypeVec.{u} n} → α.Arrow β → ↑P α → ↑P β
-- Mathlib.Analysis.InnerProductSpace.NormPow
norm_fderiv_norm_rpow_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {F : Type u_2}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {f : F → E},
  Differentiable ℝ f →
    ∀ {x : F} {p : ℝ}, 1 < p → ‖fderiv ℝ (fun x => ‖f x‖ ^ p) x‖ ≤ p * ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖