mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.restrict_carrier : ∀ {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)), ↑(X.restrict h).toPresheafedSpace = U
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_arrowProdEquivProdArrow : ∀ (α : Type u_4) (β : Type u_5) (γ : Type u_6) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : Fintype γ] (μ : γ → MeasureTheory.Measure α) (ν : γ → MeasureTheory.Measure β)
  [∀ (i : γ), MeasureTheory.SigmaFinite (μ i)] [∀ (i : γ), MeasureTheory.SigmaFinite (ν i)],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ))
    (MeasureTheory.Measure.pi fun i => (μ i).prod (ν i))
    ((MeasureTheory.Measure.pi fun i => μ i).prod (MeasureTheory.Measure.pi fun i => ν i))
-- Mathlib.Topology.Order.IntermediateValue
IsPreconnected.intermediate_value_Ici : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] {s : Set X},
  IsPreconnected s →
    ∀ {a : X} {l : Filter X},
      a ∈ s →
        ∀ [l.NeBot],
          l ≤ Filter.principal s →
            ∀ {f : X → α}, ContinuousOn f s → Filter.Tendsto f l Filter.atTop → Set.Ici (f a) ⊆ f '' s
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- A version of `smul_inv'` for groups with zero.  -/
smul_inv₀' : ∀ {α : Type u_10} {β : Type u_11} [inst : Group α] [inst_1 : GroupWithZero β] [inst_2 : MulDistribMulAction α β] (g : α)
  (x : β), g • x⁻¹ = (g • x)⁻¹
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.approx.eq_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (x : ℕ) (x_1 : Urysohns.CU P) (x_2 : X),
  Urysohns.CU.approx x x_1 x_2 =
    match x, x_1, x_2 with
    | 0, c, x => c.Uᶜ.indicator 1 x
    | n.succ, c, x => midpoint ℝ (Urysohns.CU.approx n c.left x) (Urysohns.CU.approx n c.right x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'] {Z_1 : C}
  (h : CategoryTheory.Limits.pushout f (CategoryTheory.CategoryStruct.comp g g') ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushout.inr f g) g')
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f (CategoryTheory.CategoryStruct.comp g g')) h
-- Std.Data.DTreeMap.Internal.Model
/-- General "update the mapping for a given key" function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.updateCell : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      (k : α) →
        (Std.DTreeMap.Internal.Cell α β (compare k) → Std.DTreeMap.Internal.Cell α β (compare k)) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            l.Balanced → Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (l.size - 1) (l.size + 1)
-- Std.Http.Data.Request
Std.Http.Request.Builder.mk : Std.Http.Request.Head → Std.Http.Extensions → Std.Http.Request.Builder
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.semiconj : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : Add G] [inst_2 : Add H]
  [AddConstMapClass F G H a b] (f : F), Function.Semiconj (⇑f) (fun x => x + a) fun x => x + b
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- The 'unopposite' of an additive monoid hom `αᵐᵒᵖ →+ βᵐᵒᵖ`. Inverse to
`AddMonoidHom.mul_op`.  -/
AddMonoidHom.mulUnop : {α : Type u_3} → {β : Type u_4} → [inst : AddZeroClass α] → [inst_1 : AddZeroClass β] → (αᵐᵒᵖ →+ βᵐᵒᵖ) ≃ (α →+ β)
-- Mathlib.Order.Filter.NAry
/-- Symmetric statement to `Filter.map_map₂_antidistrib_left`.  -/
Filter.map₂_map_left_anticomm : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : Filter α} {g : Filter β}
  {m : α' → β → γ} {n : α → α'} {m' : β → α → δ} {n' : δ → γ},
  (∀ (a : α) (b : β), m (n a) b = n' (m' b a)) → Filter.map₂ m (Filter.map n f) g = Filter.map n' (Filter.map₂ m' g f)
-- Init.Omega.IntList
Lean.Omega.IntList.instMul : Mul Lean.Omega.IntList
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Push forward a `MulZeroOneClass` instance along a surjective function.
See note [reducible non-instances].  -/
Function.Surjective.mulZeroOneClass : {M₀ : Type u_1} →
  {M₀' : Type u_3} →
    [inst : MulZeroOneClass M₀] →
      [inst_1 : Mul M₀'] →
        [inst_2 : Zero M₀'] →
          [inst_3 : One M₀'] →
            (f : M₀ → M₀') →
              Function.Surjective f → f 0 = 0 → f 1 = 1 → (∀ (a b : M₀), f (a * b) = f a * f b) → MulZeroOneClass M₀'
-- Mathlib.Order.Filter.Basic
Filter.instTransForallEventuallyEqEventuallyLE : {α : Type u} →
  {β : Type v} →
    [inst : Preorder β] →
      {l : Filter α} → Trans (fun x1 x2 => x1 =ᶠ[l] x2) (fun x1 x2 => x1 ≤ᶠ[l] x2) fun x1 x2 => x1 ≤ᶠ[l] x2
-- Mathlib.Data.Finsupp.Lex
Finsupp.toColex_monotone : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : LinearOrder α] [inst_2 : PartialOrder N], Monotone ⇑toColex
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_comap_eq_self_of_equiv : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {E : Type u_4} [inst_2 : EquivLike E R S]
  [inst_3 : RingEquivClass E R S] (e : E) (I : Ideal S), Ideal.map e (Ideal.comap e I) = I
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
_private.Mathlib.CategoryTheory.Sites.Hypercover.Zero.0.CategoryTheory.PreZeroHypercover.sumLift.match_1.splitter : {C : Type u_4} →
  [inst : CategoryTheory.Category.{u_3, u_4} C] →
    {S : C} →
      {E : CategoryTheory.PreZeroHypercover S} →
        {F : CategoryTheory.PreZeroHypercover S} →
          (motive : (E.sum F).I₀ → Sort u_5) →
            (x : (E.sum F).I₀) → ((i : E.I₀) → motive (Sum.inl i)) → ((i : F.I₀) → motive (Sum.inr i)) → motive x
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (E : CategoryTheory.PreZeroHypercover X) (f : Y ⟶ X)
  [E.presieve₀.HasPullbacks f] (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.mkRat_neg : ∀ {a : ℤ}, a < 0 → ∀ {b : ℕ}, b ≠ 0 → mkRat a b < 0
-- Lean.Elab.Tactic.Omega.OmegaM
/-- The `OmegaM` monad maintains two pieces of state:
* the linear atoms discovered while processing hypotheses
* a cache mapping subexpressions of one side of a linear inequality to `LinearCombo`s
  (and a proof that the `LinearCombo` evaluates at the atoms to the original expression).  -/
Lean.Elab.Tactic.Omega.OmegaM : Type → Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k a : α} {v : β},
  Std.DHashMap.Const.get! (m.insertIfNew k v) a = if (k == a) = true ∧ k ∉ m then v else Std.DHashMap.Const.get! m a
-- Mathlib.RingTheory.Polynomial.Quotient
Ideal.eval₂_C_mk_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R},
  ∀ f ∈ Ideal.map Polynomial.C I, (Polynomial.eval₂RingHom (Polynomial.C.comp (Ideal.Quotient.mk I)) Polynomial.X) f = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- `biprodComparison F X Y` is a split epi.  -/
CategoryTheory.Functor.splitEpiBiprodComparison : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              (X Y : C) →
                [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
                  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] →
                    [F.PreservesZeroMorphisms] → CategoryTheory.SplitEpi (F.biprodComparison X Y)
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
PiTensorProduct.dualDistribInvOfBasis.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [inst : CommRing R]
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Finite ι]
  [inst_4 : ∀ (i : ι), Finite (κ i)] (b : (i : ι) → Module.Basis (κ i) R (M i)),
  PiTensorProduct.dualDistribInvOfBasis b =
    ∑ p,
      (LinearMap.ringLmapEquivSelf R ℕ (PiTensorProduct R fun i => Module.Dual R (M i))).symm
          ((PiTensorProduct.tprod R) fun i => (b i).dualBasis (p i)) ∘ₗ
        LinearMap.applyₗ (⨂ₜ[R] (i : ι), (b i) (p i))
-- Mathlib.Data.PFunctor.Univariate.M
/-- corecursor where it is possible to return a fully formed value at any point
of the computation  -/
PFunctor.M.corec' : {P : PFunctor.{uA, uB}} → {α : Type u} → ({X : Type (max u uA uB)} → (α → X) → α → P.M ⊕ ↑P X) → α → P.M
-- Std.Data.HashSet.Basic
/-- Hash sets.

This is a simple separate-chaining hash table. The data of the hash set consists of a cached size
and an array of buckets, where each bucket is a linked list of keys. The number of buckets
is always a power of two. The hash set doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.

The hash table is backed by an `Array`. Users should make sure that the hash set is used linearly to
avoid expensive copies.

The hash set uses `==` (provided by the `BEq` typeclass) to compare elements and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if `a == b` implies `a = b`.

These hash sets contain a bundled well-formedness invariant, which means that they cannot
be used in nested inductive types. For these use cases, `Std.Data.HashSet.Raw` and
`Std.Data.HashSet.Raw.WF` unbundle the invariant from the hash set. When in doubt, prefer
`HashSet` over `HashSet.Raw`.
 -/
Std.HashSet : (α : Type u) → [BEq α] → [Hashable α] → Type u
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
/-- Measure version of `preVariation.exists_Finpartition_sum_gt`.  -/
MeasureTheory.VectorMeasure.exists_lt_sum_of_lt_variation : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] (μ : MeasureTheory.VectorMeasure X V) {s : Set X},
  MeasurableSet s →
    ∀ {a : ENNReal},
      a < μ.variation s →
        ∃ P, (∀ t ∈ P, t ⊆ s) ∧ (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ a < ∑ p ∈ P, ‖μ p‖ₑ
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
/-- The set that indexes roots and coroots.  -/
RootPairingCat.index : {R : Type u} → [inst : CommRing R] → RootPairingCat R → Type v
-- Mathlib.Order.IsNormal
/-- Restrict a normal function `α → β` to a normal function `Iio a → Iio (f a)`.  -/
Order.IsNormal.to_Iio : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : LinearOrder α] [inst_1 : LinearOrder β] (hf : Order.IsNormal f)
  (a : α), Order.IsNormal fun x => ⟨f ↑x, ⋯⟩
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.instUniformContinuousConstSMul : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : UniformSpace F]
  [inst_7 : IsUniformAddGroup F] {M : Type u_5} [inst_8 : Monoid M] [inst_9 : DistribMulAction M F]
  [inst_10 : SMulCommClass 𝕜 M F] [inst_11 : ContinuousConstSMul M F],
  UniformContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
IsLUB.sub : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s t : Set G} {a b : G},
  IsLUB s a → IsGLB t b → IsLUB (s - t) (a - b)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Group.mulRightReflectLT_of_mulRightStrictMono : ∀ {N : Type u_2} [inst : Group N] [inst_1 : LT N] [MulRightStrictMono N], MulRightReflectLT N
-- Mathlib.NumberTheory.Height.Projectivization
_private.Mathlib.NumberTheory.Height.Projectivization.0.Projectivization.logHeight_aux : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι]
  (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → Height.logHeight ↑a = Height.logHeight ↑b
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Auxiliary function to expand a pattern containing forbidden application symbols
into a multi-pattern.

This function enhances the usability of the `[grind =]` attribute by automatically handling
forbidden pattern symbols. For example, consider the following theorem tagged with this attribute:
```
getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a]
```
Here, the selected pattern is `xs.getLast? = some a`, but `Eq` is a forbidden pattern symbol.
Instead of producing an error, this function converts the pattern into a multi-pattern,
allowing the attribute to be used conveniently.

The function recursively expands patterns with forbidden symbols by splitting them
into their sub-components. If the pattern does not contain forbidden symbols,
it is returned as-is.
 -/
Lean.Meta.Grind.splitWhileForbidden : Lean.Expr → List Lean.Expr
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- A continuous alternating map from `ι → M` to `N`, denoted `M [⋀^ι]→L[R] N`,
is a continuous map that is

- multilinear : `f (update m i (c • x)) = c • f (update m i x)` and
  `f (update m i (x + y)) = f (update m i x) + f (update m i y)`;
- alternating : `f v = 0` whenever `v` has two equal coordinates.
 -/
«term_[⋀^_]→L[_]_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeAddSemigroup.toFreeAddMonoid_mk_eq_cons : ∀ {α : Type u_1} (x : α) (xs : List α),
  FreeAddSemigroup.toFreeAddMonoid { head := x, tail := xs } = FreeAddMonoid.ofList (x :: xs)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Filter.inf_isMeasurablyGenerated : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f g : Filter α) [f.IsMeasurablyGenerated] [g.IsMeasurablyGenerated],
  (f ⊓ g).IsMeasurablyGenerated
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
/-- **Alias** of `WfDvdMonoid.not_isUnit_iff_exists_factors_eq`. -/
WfDvdMonoid.not_unit_iff_exists_factors_eq : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [WfDvdMonoid α] (a : α),
  a ≠ 0 → (¬IsUnit a ↔ ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅)
-- Mathlib.Algebra.Ring.Prod
/-- Combine two ring homomorphisms `f : R →+* S`, `g : R →+* T` into `f.prod g : R →+* S × T`
given by `(f.prod g) x = (f x, g x)`  -/
RingHom.prod : {R : Type u_1} →
  {S : Type u_3} →
    {T : Type u_5} →
      [inst : NonAssocSemiring R] →
        [inst_1 : NonAssocSemiring S] → [inst_2 : NonAssocSemiring T] → (R →+* S) → (R →+* T) → R →+* S × T
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_X_sub_C_pow_left : ∀ {R : Type u_1} [inst : CommRing R] (r : R) (g : Polynomial R) (m n : ℕ),
  g.natDegree ≤ n → ((Polynomial.X - Polynomial.C r) ^ m).resultant g m n = Polynomial.eval r g ^ m
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.node.inj : ∀ {α : Type u} {a : α} {child sibling : Batteries.PairingHeapImp.Heap α} {a_1 : α}
  {child_1 sibling_1 : Batteries.PairingHeapImp.Heap α},
  Batteries.PairingHeapImp.Heap.node a child sibling = Batteries.PairingHeapImp.Heap.node a_1 child_1 sibling_1 →
    a = a_1 ∧ child = child_1 ∧ sibling = sibling_1
-- Mathlib.CategoryTheory.Sites.Coherent.Comparison
CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.FinitaryPreExtensive C]
  [CategoryTheory.Preregular C], CategoryTheory.Precoherent C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- Extension for the `positivity` tactic: `π` is always positive.  -/
Mathlib.Meta.Positivity.evalRealPi : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Data.List.ToFinsupp
List.toFinsupp_cons_eq_single_add_embDomain : ∀ {R : Type u_2} [inst : AddZeroClass R] (x : R) (xs : List R)
  [inst_1 : DecidablePred fun x_1 => (x :: xs).getD x_1 0 ≠ 0] [inst_2 : DecidablePred fun x => xs.getD x 0 ≠ 0],
  (x :: xs).toFinsupp = (fun₀ | 0 => x) + Finsupp.embDomain (addRightEmbedding 1) xs.toFinsupp
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β} (h : (↑m).WF),
  Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.filter f m) k fallback =
    ((Std.DHashMap.Internal.Raw₀.Const.get? m k).pfilter fun x h' => f (m.getKey k ⋯) x).getD fallback
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofNatNonneg : Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- The integral of a function lifted to AddCircle from an interval `(t, t + T]` to `AddCircle T`
is equal to the intervalIntegral over the interval.  -/
AddCircle.integral_liftIoc_eq_intervalIntegral : ∀ (T : ℝ) [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {t : ℝ}
  {f : ℝ → E}, ∫ (a : AddCircle T), AddCircle.liftIoc T t f a = ∫ (a : ℝ) in t..t + T, f a
-- Std.Data.HashMap.Lemmas
Std.HashMap.instLawfulGetElemMemOfEquivBEqOfLawfulHashable : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α],
  LawfulGetElem (Std.HashMap α β) α β fun m a => a ∈ m
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_maxKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.getKey! t.maxKey! = t.maxKey!
-- Mathlib.Algebra.Quaternion
Quaternion.re_intCast : ∀ {R : Type u_3} [inst : CommRing R] (z : ℤ), (↑z).re = ↑z
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
/-- Given a family of opens `U` and an open `Y` equal to the union of opens in `U`, we may
take the presieve on `Y` associated to `U` and the sieve generated by it, and form the
full subcategory (subposet) of opens contained in `Y` (`over Y`) consisting of arrows
in the sieve. This full subcategory is equivalent to `OpensLeCover U`, the (poset)
category of opens contained in some `U i`.  -/
TopCat.Presheaf.generateEquivalenceOpensLe_functor' : {X : TopCat} →
  {ι : Type u_2} →
    (U : ι → TopologicalSpace.Opens ↑X) →
      {Y : TopologicalSpace.Opens ↑X} →
        CategoryTheory.Functor
          (CategoryTheory.ObjectProperty.FullSubcategory fun f =>
            (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows f.hom)
          (TopCat.Presheaf.SheafCondition.OpensLeCover U)
-- Mathlib.GroupTheory.OrderOfElement
pow_inj_mod : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] {x : G} {n m : ℕ}, x ^ n = x ^ m ↔ n % orderOf x = m % orderOf x
-- Mathlib.Combinatorics.Schnirelmann
/-- The Schnirelmann density of `A` is `1` if and only if `A` contains all the positive naturals.  -/
schnirelmannDensity_eq_one_iff : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A], schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
WittVector.fontaineThetaModPPow_teichmuller : ∀ {R : Type u} [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [inst_3 : IsAdicComplete (Ideal.span {↑p}) R] (n : ℕ) (x : PreTilt R p),
  (WittVector.fontaineThetaModPPow R p n) ((WittVector.teichmuller p) x) =
    (Ideal.Quotient.mk (Ideal.span {↑p} ^ (n + 1))) (PreTilt.untilt x)
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.chosenCoend.ι_apply : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))} (j : J)
  (x : (F.obj (Opposite.op j)).obj j),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.chosenCoend.ι F j)) x =
    Quot.mk (CategoryTheory.Limits.Types.coendRel F) ⟨j, x⟩
-- Init.Core
UInt16.ofBitVec.inj : ∀ {toBitVec toBitVec_1 : BitVec 16}, { toBitVec := toBitVec } = { toBitVec := toBitVec_1 } → toBitVec = toBitVec_1
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {S : C}
  {toPreZeroHypercover : CategoryTheory.PreZeroHypercover S}
  {I₁ : toPreZeroHypercover.I₀ → toPreZeroHypercover.I₀ → Type w} {Y : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → I₁ i₁ i₂ → C}
  {p₁ : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ toPreZeroHypercover.X i₁}
  {p₂ : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ toPreZeroHypercover.X i₂}
  {w :
    ∀ ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ (j : I₁ i₁ i₂),
      CategoryTheory.CategoryStruct.comp (p₁ j) (toPreZeroHypercover.f i₁) =
        CategoryTheory.CategoryStruct.comp (p₂ j) (toPreZeroHypercover.f i₂)}
  {toPreZeroHypercover_1 : CategoryTheory.PreZeroHypercover S}
  {I₁_1 : toPreZeroHypercover_1.I₀ → toPreZeroHypercover_1.I₀ → Type w}
  {Y_1 : ⦃i₁ i₂ : toPreZeroHypercover_1.I₀⦄ → I₁_1 i₁ i₂ → C}
  {p₁_1 : ⦃i₁ i₂ : toPreZeroHypercover_1.I₀⦄ → (j : I₁_1 i₁ i₂) → Y_1 j ⟶ toPreZeroHypercover_1.X i₁}
  {p₂_1 : ⦃i₁ i₂ : toPreZeroHypercover_1.I₀⦄ → (j : I₁_1 i₁ i₂) → Y_1 j ⟶ toPreZeroHypercover_1.X i₂}
  {w_1 :
    ∀ ⦃i₁ i₂ : toPreZeroHypercover_1.I₀⦄ (j : I₁_1 i₁ i₂),
      CategoryTheory.CategoryStruct.comp (p₁_1 j) (toPreZeroHypercover_1.f i₁) =
        CategoryTheory.CategoryStruct.comp (p₂_1 j) (toPreZeroHypercover_1.f i₂)},
  { toPreZeroHypercover := toPreZeroHypercover, I₁ := I₁, Y := Y, p₁ := p₁, p₂ := p₂, w := w } =
      { toPreZeroHypercover := toPreZeroHypercover_1, I₁ := I₁_1, Y := Y_1, p₁ := p₁_1, p₂ := p₂_1, w := w_1 } →
    toPreZeroHypercover = toPreZeroHypercover_1 ∧ I₁ ≍ I₁_1 ∧ Y ≍ Y_1 ∧ p₁ ≍ p₁_1 ∧ p₂ ≍ p₂_1
-- Mathlib.Tactic.Ring.Basic
/-- `ExBase BaseType sα e` stores the structure of a normalized expression `e`, which appears
as the base of an exponent expression `e^n`. The `sum` constructor is only used when the exponent
`n` is not a constant.  -/
Mathlib.Tactic.Ring.ExBase : {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.forget₂_preservesEpimorphisms : ∀ (C : Type u) (D : Type u') [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FC : C → C → Type u_2} {CC : C → Type w} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [inst_3 : CategoryTheory.ConcreteCategory C FC] {FD : D → D → Type u_3} {CD : D → Type w}
  [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [inst_6 : CategoryTheory.HasForget₂ C D] [(CategoryTheory.forget C).PreservesEpimorphisms],
  (CategoryTheory.forget₂ C D).PreservesEpimorphisms
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_sInf : ∀ {V : Type u} {s : Set (SimpleGraph V)}, s.Nonempty → (sInf s).edgeSet = ⋂₀ (SimpleGraph.edgeSet '' s)
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.isMeta : Lean.Elab.Modifiers → Bool