mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.AC
_private.Init.Data.AC.0.Option.isSome.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (val : α) (h_1 : (val : α) → motive (some val))
  (h_2 : Unit → motive none),
  (match some val with
    | some val => h_1 val
    | none => h_2 ()) =
    h_1 val
-- Mathlib.Order.Bounds.Basic
OrderTop.upperBounds_univ : ∀ {γ : Type u_3} [inst : PartialOrder γ] [inst_1 : OrderTop γ], upperBounds Set.univ = {⊤}
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.length_eq_length_toIterM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  {it : Std.Iter β}, it.length = it.toIterM.length.run.down
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
/-- The functor `HomologicalComplex (Karoubi C) c ⥤ Karoubi (HomologicalComplex C c)`,
on objects  -/
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c →
            CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- The behaviour of `borelize α` depends on the existing assumptions on `α`.

- if `α` is a topological space with instances `[MeasurableSpace α] [BorelSpace α]`, then
  `borelize α` replaces the former instance by `borel α`;
- otherwise, `borelize α` adds instances `borel α : MeasurableSpace α` and `⟨rfl⟩ : BorelSpace α`.

Finally, `borelize α β γ` runs `borelize α; borelize β; borelize γ`.
 -/
Mathlib.Tactic.Borelize.tacticBorelize___ : Lean.ParserDescr
-- Init.Data.Array.Attach
Array.getElem?_attachWith : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {P : α → Prop} {H : ∀ a ∈ xs, P a},
  (xs.attachWith P H)[i]? = Option.pmap Subtype.mk xs[i]? ⋯
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.subtype_mk : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ {p : β → Prop} (hp : ∀ (x : α), p (f x)), LipschitzWith K fun x => ⟨f x, ⋯⟩
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonLogConfig : Lean.FromJson Lean.Lsp.LogConfig
-- Mathlib.Topology.Algebra.Module.LinearPMap
LinearPMap.HasCore.mk : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F} {S : Submodule R E},
  S ≤ f.domain → (f.domRestrict S).closure = f → f.HasCore S
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
MeasureTheory.Measure.sub_toSignedMeasure_eq_toSignedMeasure_sub : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν],
  μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
-- Std.Http.Data.Body.Full
Std.Http.Body.instCoeContextAsyncResponseFullAny : Coe (Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Full))
  (Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any))
-- Mathlib.Algebra.Polynomial.Roots
/-- To check a monic polynomial is irreducible, it suffices to check only for
divisors that have smaller degree.

See also: `Polynomial.Monic.irreducible_iff_natDegree`.
 -/
Polynomial.Monic.irreducible_iff_degree_lt : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {p : Polynomial R},
  p.Monic → p ≠ 1 → (Irreducible p ↔ ∀ (q : Polynomial R), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q)
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal_apply : ∀ (μ : ℝ) {v : NNReal},
  v ≠ 0 → ∀ (s : Set ℝ), (ProbabilityTheory.gaussianReal μ v) s = ∫⁻ (x : ℝ) in s, ProbabilityTheory.gaussianPDF μ v x
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- Given two adjunctions `l₁ ⊣ r₁` and `l₂ ⊣ r₂` both between objects `c`, `d`, there is a
bijection between 2-morphisms `l₂ ⟶ l₁` and 2-morphisms `r₁ ⟶ r₂`. This is
defined as a special case of `mateEquiv`, where the two "vertical" 1-morphisms are identities.
This bijection is `conjugateEquiv`; the image of a 2-morphism under it is called its conjugate.

Furthermore, this bijection preserves (and reflects) isomorphisms, i.e. a 2-morphism is an iso
iff its image under the bijection is an iso.
 -/
CategoryTheory.Bicategory.conjugateEquiv : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {c d : B} →
      {l₁ l₂ : c ⟶ d} →
        {r₁ r₂ : d ⟶ c} →
          CategoryTheory.Bicategory.Adjunction l₁ r₁ →
            CategoryTheory.Bicategory.Adjunction l₂ r₂ → (l₂ ⟶ l₁) ≃ (r₁ ⟶ r₂)
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.coe_mk : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (f : R →* R')
  (hf : ∀ (a : R), ¬IsUnit a → (↑f).toFun a = 0), ⇑{ toMonoidHom := f, map_nonunit' := hf } = ⇑f
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (S : AddSubsemigroup M),
  AddSubsemigroup.map f S = { carrier := ⇑f '' ↑S, add_mem' := ⋯ }
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_eq_of_trailingDegree_eq : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] {q : Polynomial S},
  p.trailingDegree = q.trailingDegree → p.natTrailingDegree = q.natTrailingDegree
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.mk.sizeOf_spec : ∀ {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} [inst_4 : SizeOf R] [inst_5 : SizeOf B]
  [inst_6 : SizeOf F] [inst_7 : SizeOf ι] (baseSet : ι → Set B) (isOpen_baseSet : ∀ (i : ι), IsOpen (baseSet i))
  (indexAt : B → ι) (mem_baseSet_at : ∀ (x : B), x ∈ baseSet (indexAt x)) (coordChange : ι → ι → B → F →L[R] F)
  (coordChange_self : ∀ (i : ι), ∀ x ∈ baseSet i, ∀ (v : F), (coordChange i i x) v = v)
  (continuousOn_coordChange : ∀ (i j : ι), ContinuousOn (coordChange i j) (baseSet i ∩ baseSet j))
  (coordChange_comp :
    ∀ (i j k : ι),
      ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k,
        ∀ (v : F), (coordChange j k x) ((coordChange i j x) v) = (coordChange i k x) v),
  sizeOf
      { baseSet := baseSet, isOpen_baseSet := isOpen_baseSet, indexAt := indexAt, mem_baseSet_at := mem_baseSet_at,
        coordChange := coordChange, coordChange_self := coordChange_self,
        continuousOn_coordChange := continuousOn_coordChange, coordChange_comp := coordChange_comp } =
    1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_alter!_of_not_compare_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      ¬compare k k' = Ordering.eq →
        Std.DTreeMap.Internal.Impl.contains k' (Std.DTreeMap.Internal.Impl.Const.alter! k f t) =
          Std.DTreeMap.Internal.Impl.contains k' t
-- Mathlib.Topology.Algebra.WithZeroTopology
WithZeroTopology.instContinuousInv₀ : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀], ContinuousInv₀ Γ₀
-- Mathlib.Data.Rel
SetRel.image_empty_right : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, R.image ∅ = ∅
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
/-- If `forget C` preserves and reflects initials, then `X` is initial if and only if
`ToType X` is empty.  -/
CategoryTheory.Limits.Concrete.initial_iff_empty_of_preserves_of_reflects : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)]
  [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] (X : C),
  Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty (CategoryTheory.ToType X)
-- Std.Http.Data.URI.Encoding
/-- Encodes a raw string into an `EncodedString` with automatic proof construction. Unreserved characters
(alphanumeric, hyphen, period, underscore, tilde) are kept as-is, while all other characters are percent-encoded.
 -/
Std.Http.URI.EncodedString.encode : {r : UInt8 → Bool} → String → Std.Http.URI.EncodedString r
-- Mathlib.RingTheory.OreLocalization.NonZeroDivisors
OreLocalization.nontrivial : ∀ {R : Type u_1} [inst : MonoidWithZero R] [Nontrivial R] [inst_2 : OreLocalization.OreSet (nonZeroDivisors R)],
  Nontrivial (OreLocalization (nonZeroDivisors R) R)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).inv.toNatTrans.app X))
      ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv.toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp g h).inv.toNatTrans.app ((F.map f).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv.toNatTrans.app X)
        ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X))
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
Nat.doubleFactorial_add_one : ∀ (n : ℕ), (n + 1).doubleFactorial = (n + 1) * (n - 1).doubleFactorial
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Matrix.discr_of_card_eq_two : ∀ {R : Type u_1} {n : Type u_2} [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n R),
  Fintype.card n = 2 → A.discr = A.trace ^ 2 - 4 * A.det
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_cons_zero : ∀ {a : Bool} {w : ℕ} {x : BitVec w}, (BitVec.cons a x).getMsbD 0 = a
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.forget_createsLimitsOfShape : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] → CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget GrpCat)
-- Mathlib.Topology.AlexandrovDiscrete
Subtype.instAlexandrovDiscrete : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {p : α → Prop}, AlexandrovDiscrete { a // p a }
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isColocal_eq_inverseImage_isomorphisms : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : G ⊣ F) [G.Full] [G.Faithful],
  (CategoryTheory.ObjectProperty.isColocal fun x => x ∈ Set.range G.obj) =
    (CategoryTheory.MorphismProperty.isomorphisms D).inverseImage F
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map : ∀ {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] {J : CategoryTheory.GrothendieckTopology C}
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  (F : CategoryTheory.Sheaf J A) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F (G.map f) = F.obj.map f.op
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.lineDerivCLM_apply_of_gt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n k : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F]
  {v : E}, n < k + 1 → TestFunction.lineDerivCLM 𝕜 v = 0
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.hom_zsmul : ∀ {M N : AddCommGrpCat} (n : ℤ) (f : M ⟶ N), AddCommGrpCat.Hom.hom (n • f) = n • AddCommGrpCat.Hom.hom f
-- Init.Data.Rat.Lemmas
Rat.abs_pos_iff : ∀ {x : ℚ}, 0 < x.abs ↔ x ≠ 0
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold
mdifferentiable_jacobiTheta : MDiff (jacobiTheta ∘ UpperHalfPlane.coe)
-- Mathlib.Order.RelClasses
instIsStrictOrderGt : ∀ {α : Type u} [inst : Preorder α], IsStrictOrder α fun x1 x2 => x2 < x1
-- Init.Data.List.Erase
List.exists_of_eraseP : ∀ {α : Type u_1} {p : α → Bool} {l : List α} {a : α},
  a ∈ l → p a = true → ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ List.eraseP p l = l₁ ++ l₂
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.algHom_ext_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] {f : Polynomial R} [inst_1 : Semiring S] [inst_2 : Algebra R S]
  {g₁ g₂ : AdjoinRoot f →ₐ[R] S}, g₁ = g₂ ↔ g₁ (AdjoinRoot.root f) = g₂ (AdjoinRoot.root f)
-- Mathlib.Algebra.Group.Action.Pi
Pi.isCentralScalar : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)] [inst_1 : (i : ι) → SMul Mᵐᵒᵖ (α i)]
  [∀ (i : ι), IsCentralScalar M (α i)], IsCentralScalar M ((i : ι) → α i)
-- Init.Data.Range.Polymorphic.Basic
Std.Roc.lower_le_of_mem : ∀ {α : Type u} {r : Std.Roc α} {a : α} [inst : LE α] [inst_1 : LT α], a ∈ r → r.lower < a
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.isSigmaSubadditiveSetFun_zero : ∀ {X : Type u_1} [inst : MeasurableSpace X], MeasureTheory.IsSigmaSubadditiveSetFun 0
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.rightUnitor_inv_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : CategoryTheory.Grp C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor G).inv.hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor G.X).inv
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Constant terms at `∞`  -/
WeakFEPair.f₀ : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → E
-- Mathlib.RingTheory.WittVector.IsPoly
_private.Mathlib.RingTheory.WittVector.IsPoly.0.WittVector.term𝕎 : Lean.ParserDescr
-- Lean.Attributes
Lean.AttributeImpl.mk.inj : ∀ {toAttributeImplCore : Lean.AttributeImplCore} {add : Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit}
  {erase : Lean.Name → Lean.AttrM Unit} {toAttributeImplCore_1 : Lean.AttributeImplCore}
  {add_1 : Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit} {erase_1 : Lean.Name → Lean.AttrM Unit},
  { toAttributeImplCore := toAttributeImplCore, add := add, erase := erase } =
      { toAttributeImplCore := toAttributeImplCore_1, add := add_1, erase := erase_1 } →
    toAttributeImplCore = toAttributeImplCore_1 ∧ add = add_1 ∧ erase = erase_1
-- Lean.Data.Lsp.Diagnostics
/-- Diagnostics representing an "unsolved goals" error.
Corresponds to `MessageData.tagged `Tactic.unsolvedGoals ..`.
 -/
Lean.Lsp.LeanDiagnosticTag.unsolvedGoals : Lean.Lsp.LeanDiagnosticTag
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.IsDPMorphism.of_comp : ∀ {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : CommSemiring A] [inst_1 : CommSemiring B]
  [inst_2 : CommSemiring C] {I : Ideal A} {J : Ideal B} {K : Ideal C} (hI : DividedPowers I) (hJ : DividedPowers J)
  (hK : DividedPowers K) (f : A →+* B) (g : B →+* C),
  J = Ideal.map f I → hI.IsDPMorphism hJ f → hI.IsDPMorphism hK (g.comp f) → hJ.IsDPMorphism hK g
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
/-- The canonical map `Φ.X₀ ⟶ Φ.iteration J` which is the `J`th-transfinite composition
of maps `Φ.toSucc`.  -/
CategoryTheory.SmallObject.SuccStruct.ιIteration : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Φ : CategoryTheory.SmallObject.SuccStruct C) →
      (J : Type w) →
        [inst_1 : LinearOrder J] →
          [inst_2 : OrderBot J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : WellFoundedLT J] →
                [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] → Φ.X₀ ⟶ Φ.iteration J
-- Mathlib.Data.Bundle
/-- `Bundle.TotalSpace.proj` is the canonical projection `Bundle.TotalSpace F E → B` from the
total space to the base space.  -/
Bundle.TotalSpace.proj : {B : Type u_1} → {F : Type u_4} → {E : B → Type u_5} → Bundle.TotalSpace F E → B
-- Init.Data.Array.Extract
Array.extract_of_size_lt : ∀ {α : Type u_1} {as : Array α} {i j : ℕ}, as.size < j → as.extract i j = as.extract i
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- The action of `gal p` on the roots of `p` in `E`.  -/
Polynomial.Gal.galAction : {F : Type u_1} →
  [inst : Field F] →
    (p : Polynomial F) →
      (E : Type u_2) →
        [inst_1 : Field E] →
          [inst_2 : Algebra F E] → [Fact (Polynomial.map (algebraMap F E) p).Splits] → MulAction p.Gal ↑(p.rootSet E)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S),
  E.presieve₀ = CategoryTheory.Presieve.ofArrows E.X E.f
-- Mathlib.Data.Finsupp.Basic
Finsupp.uncurry_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α →₀ β →₀ M) (x : α × β), f.uncurry x = (f x.1) x.2
-- Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
/-- Given an endomorphism `S` of a normed space that's a closed embedding but not surjective, we can
find a sequence of vectors `f n`, living inside a shell, such that `f n` is in the
range of `S ^ n` but is at least `1` away from any vector in the range of `S ^ (n + 1)`.
This is a useful construction for the proof of the Fredholm alternative for compact operators.
The conditions about `c` and `R` are to mimic those in Riesz's lemma.
 -/
_private.Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative.0.IsCompactOperator.exists_seq : ∀ {𝕜 : Type u_1} {X : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {S : Module.End 𝕜 X},
  ¬Function.Surjective ⇑S →
    Topology.IsClosedEmbedding ⇑S →
      ∀ {c : 𝕜},
        1 < ‖c‖ →
          ∀ {R : ℝ},
            ‖c‖ < R →
              ∃ f,
                (∀ (n : ℕ), 1 ≤ ‖f n‖) ∧
                  (∀ (n : ℕ), ‖f n‖ ≤ R) ∧
                    (∀ (n : ℕ), f n ∈ LinearMap.range (S ^ n)) ∧
                      ∀ (n : ℕ), ∀ y ∈ LinearMap.range (S ^ (n + 1)), 1 ≤ ‖f n - y‖
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.sub_apply : ∀ {α : Type u} [inst : TopologicalSpace α] {R : Type u_2} [inst_1 : PseudoMetricSpace R] [inst_2 : Sub R]
  [inst_3 : BoundedSub R] [inst_4 : ContinuousSub R] (f g : BoundedContinuousFunction α R) {x : α},
  (f - g) x = f x - g x
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.Grpd.instReflectiveCatForgetToCat : CategoryTheory.Reflective CategoryTheory.Grpd.forgetToCat
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.dvd_of_mk_le_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {a b : M}, Associates.mk a ≤ Associates.mk b → a ∣ b
-- Mathlib.Order.BoundedOrder.Lattice
inf_bot_eq : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] (a : α), a ⊓ ⊥ = ⊥
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.ball_eq_of_symmetry : ∀ {β : Type ub} {V : SetRel β β} [V.IsSymm] {x : β}, UniformSpace.ball x V = {y | (y, x) ∈ V}
-- Mathlib.Data.Sym.Basic
Sym.inhabitedSym : {α : Type u_1} → [Inhabited α] → (n : ℕ) → Inhabited (Sym α n)
-- Mathlib.RingTheory.Localization.Basic
/-- **Alias** of `IsLocalization.of_le_isUnit`. -/
IsLocalization.at_units : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R}, S ≤ IsUnit.submonoid R → IsLocalization S R
-- Init.Omega.Logic
Lean.Omega.ite_disjunction : ∀ {α : Type u} {P : Prop} [inst : Decidable P] {a b : α}, P ∧ (if P then a else b) = a ∨ ¬P ∧ (if P then a else b) = b
-- Mathlib.Analysis.Normed.Ring.Lemmas
SeparationQuotient.instNormOneClass : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] [inst_1 : One α] [NormOneClass α],
  NormOneClass (SeparationQuotient α)
-- Mathlib.Algebra.Order.Sub.Basic
tsub_tsub_eq_min : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] [AddLeftReflectLE α] (a b : α), a - (a - b) = min a b
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.unop.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F.op),
  c.unop = { pt := Opposite.unop c.pt, ι := CategoryTheory.NatTrans.removeOp c.π }
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_limit_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  {i j : K} (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (f : i ⟶ j) {Z : C}
  (h : (CategoryTheory.Limits.limit F).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F i).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit F).map f) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limMap (F.whiskerLeft ((CategoryTheory.evaluation K C).map f)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F j).inv h)
-- Mathlib.Data.Set.Lattice
Set.coe_unionEqSigmaOfDisjoint_symm_apply : ∀ {α : Type u_12} {β : Type u_13} {t : α → Set β} (h : Pairwise (Function.onFun Disjoint t)) (x : (i : α) × ↑(t i)),
  ↑((Set.unionEqSigmaOfDisjoint h).symm x) = ↑x.snd
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.varsToConstants.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} (x : L.Term (γ ⊕ α)),
  x.varsToConstants =
    match x with
    | FirstOrder.Language.var (Sum.inr a) => FirstOrder.Language.var a
    | FirstOrder.Language.var (Sum.inl c) => FirstOrder.Language.Constants.term (Sum.inr c)
    | FirstOrder.Language.func f ts => FirstOrder.Language.func (Sum.inl f) fun i => (ts i).varsToConstants
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.normal_unop : ∀ {G : Type u_2} [inst : AddGroup G] {H : AddSubgroup Gᵃᵒᵖ}, H.unop.Normal ↔ H.Normal
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.groupPowers.eq_1 : ∀ {G : Type u_1} [inst : Monoid G] {x : G} (hx : IsOfFinOrder x),
  hx.groupPowers = And.casesOn ⋯ fun hpos hx_1 => Submonoid.groupPowers hpos hx_1
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.FunPropDeclsExt : Type
-- Lean.Parser.Do
Lean.Parser.Term.doCatch : Lean.Parser.Parser
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.UnpackedFloat.notANumber.sizeOf_spec : sizeOf Float.Model.UnpackedFloat.notANumber = 1
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.mk : {V : Type u} →
  {G : SimpleGraph V} →
    (verts : Set V) →
      (Adj : V → V → Prop) →
        (∀ {v w : V}, Adj v w → G.Adj v w) →
          (∀ {v w : V}, Adj v w → v ∈ verts) →
            autoParam (Std.Symm Adj) SimpleGraph.Subgraph.symm._autoParam → G.Subgraph
-- Mathlib.NumberTheory.AbelSummation
_private.Mathlib.NumberTheory.AbelSummation.0.abelSummationProof.ineqofmemIco' : ∀ {a b : ℝ} {k : ℕ}, k ∈ Finset.Ico (⌊a⌋₊ + 1) ⌊b⌋₊ → a ≤ ↑k ∧ ↑k + 1 ≤ b
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.divisionCommMonoid.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DivisionCommMonoid α],
  Finset.divisionCommMonoid = Function.Injective.divisionCommMonoid SetLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Topology.Separation.Basic
/-- A weakly locally compact R₁ space is locally compact.  -/
WeaklyLocallyCompactSpace.locallyCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X], LocallyCompactSpace X