mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.property.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.property = 1
-- Std.Http.Data.Body.Full
/-- Builds a response body from raw bytes without setting any headers.
Use `bytes` instead if you want `Content-Type: application/octet-stream` set automatically.
 -/
Std.Http.Response.Builder.fromBytes : Std.Http.Response.Builder → ByteArray → Std.Async.Async (Std.Http.Response Std.Http.Body.Full)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_insert_congr : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α},
  e ∈ M.closure (insert f X) \ M.closure X → M.closure (insert e X) = M.closure (insert f X)
-- Mathlib.Condensed.Discrete.Module
/-- `CondensedMod.LocallyConstant.functor` is naturally isomorphic to the constant sheaf functor from
`R`-modules to condensed `R`-modules.
 -/
CondensedMod.LocallyConstant.functorIsoDiscrete : (R : Type (u + 1)) → [inst : Ring R] → CondensedMod.LocallyConstant.functor R ≅ Condensed.discrete (ModuleCat R)
-- Mathlib.Data.Sum.Order
OrderIso.sumAssoc_symm_apply_inr_inr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (c : γ),
  (OrderIso.sumAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.instFaithfulLocalizedFunctorOfIsLocalizedFullyFaithful : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₄, u₄} D₁]
  [inst_3 : CategoryTheory.Category.{v₅, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₂.IsLocalization W₂] [Φ.IsLocalizedFullyFaithful], (Φ.localizedFunctor L₁ L₂).Faithful
-- Init.Core
Subtype.eq : ∀ {α : Sort u} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inl_pushoutRightPushoutInlIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp f f') g)
      (CategoryTheory.Limits.pushoutRightPushoutInlIso f g f').inv =
    CategoryTheory.Limits.pushout.inl f' (CategoryTheory.Limits.pushout.inl f g)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.finTwoArrow_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α], ⇑MeasurableEquiv.finTwoArrow = fun f => (f 0, f 1)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.invFun_eq_symm : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {e : A₁ ≃ₐ[R] A₂}, e.invFun = ⇑e.symm
-- Mathlib.Data.List.Sigma
/-- Remove entries with duplicate keys from `l : List (Sigma β)`.  -/
List.dedupKeys : {α : Type u} → {β : α → Type v} → [DecidableEq α] → List (Sigma β) → List (Sigma β)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.isCompl_rootSpan_ker_rootForm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [P.IsAnisotropic], IsCompl (P.rootSpan R) (LinearMap.ker P.RootForm)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- Adding a one-form taking values in the endomorphisms of the vector bundle to a covariant
derivative gives a covariant derivative.  -/
IsCovariantDerivativeOn.add_one_form : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] {s : Set M}
  {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x},
  IsCovariantDerivativeOn F cov s →
    ∀ (A : (x : M) → V x →L[𝕜] TangentSpace I x →L[𝕜] V x),
      IsCovariantDerivativeOn F (fun σ x => cov σ x + (A x) (σ x)) s
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.neg : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : AddCommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedAddMonoid β] {f : α → β} {a : α} {s : Set α}, IsLocalMinOn f s a → IsLocalMaxOn (fun x => -f x) s a
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a colimit for `F : Jᵒᵖ ⥤ C` into a limit for `F.rightOp : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ C) →
          {c : CategoryTheory.Limits.Cone F.rightOp} →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeRightOp c) →
              CategoryTheory.Limits.IsLimit c
-- Mathlib.Data.Set.Insert
/-- **Alias** of `Set.ofPred_mem_list_eq_replicate`. -/
Set.setOf_mem_list_eq_replicate : ∀ {α : Type u_1} {l : List α} {a : α}, {x | x ∈ l} = {a} ↔ ∃ n > 0, l = List.replicate n a
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenRatio_pos : 0 < Real.goldenRatio
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {v : β k},
  (t.insert k v).minKey! = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Mathlib.Algebra.Algebra.Hom.Rat
RingEquiv.coe_toRatAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S]
  (f : R ≃+* S), ⇑f.toRatAlgEquiv = ⇑f
-- Mathlib.Dynamics.Ergodic.AddCircle
/-- If a null-measurable subset of the circle is almost invariant under rotation by a family of
rational angles with denominators tending to infinity, then it must be almost empty or almost full.
 -/
AddCircle.ae_empty_or_univ_of_forall_vadd_ae_eq_self : ∀ {T : ℝ} [hT : Fact (0 < T)] {s : Set (AddCircle T)},
  MeasureTheory.NullMeasurableSet s MeasureTheory.volume →
    ∀ {ι : Type u_1} {l : Filter ι} [l.NeBot] {u : ι → AddCircle T},
      (∀ (i : ι), u i +ᵥ s =ᵐ[MeasureTheory.volume] s) →
        Filter.Tendsto (addOrderOf ∘ u) l Filter.atTop →
          s =ᵐ[MeasureTheory.volume] ∅ ∨ s =ᵐ[MeasureTheory.volume] Set.univ
-- Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate
hasStrictFDerivAt_implicitFunctionOfBivariate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : IsRCLikeNormedField 𝕜] {E₁ : Type u_2}
  [inst_2 : NormedAddCommGroup E₁] [inst_3 : NormedSpace 𝕜 E₁] [inst_4 : CompleteSpace E₁] {E₂ : Type u_3}
  [inst_5 : NormedAddCommGroup E₂] [inst_6 : NormedSpace 𝕜 E₂] [inst_7 : CompleteSpace E₂] {F : Type u_4}
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ → E₂ → F}
  {f₁ : E₁ → E₂ → E₁ →L[𝕜] F} {f₂ : E₁ → E₂ → E₂ →L[𝕜] F}
  (df₁ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f x v.2) (f₁ v.1 v.2) v.1)
  (df₂ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f v.1 x) (f₂ v.1 v.2) v.2) (cf₁ : ContinuousAt (↿f₁) u)
  (cf₂ : ContinuousAt (↿f₂) u) (if₂u : (f₂ u.1 u.2).IsInvertible),
  HasStrictFDerivAt (implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u) (-(f₂ u.1 u.2).inverse ∘SL f₁ u.1 u.2) u.1
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a : α},
  t.contains a = false → t.get? a = none
-- Mathlib.Topology.LocallyClosed
closure_inter_coborder : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, closure s ∩ coborder s = s
-- Init.Data.Nat.Gcd
Nat.gcd_gcd_self_left_left : ∀ (m n : ℕ), (m.gcd n).gcd m = m.gcd n
-- Lean.Elab.Parallel
/-- Runs a list of MetaM computations in parallel and returns:
* a combined cancellation hook for all tasks, and
* an iterator that yields results in completion order (greedily).

The iterator runs in MetaM, and as it yields each result, it updates the MetaM state
to reflect the state when that particular task completed. This means the state is
threaded through the iteration in task completion order.

Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
Lean.Meta.MetaM.parIterGreedyWithCancel : {α : Type} → List (Lean.MetaM α) → Lean.MetaM (BaseIO PUnit.{1} × Std.IterM Lean.MetaM (Except Lean.Exception α))
-- Mathlib.Topology.Order.Lattice
ContinuousAt.finset_inf' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} {x : X} (hne : s.Nonempty),
  (∀ i ∈ s, ContinuousAt (f i) x) → ContinuousAt (s.inf' hne f) x
-- Std.Data.ExtTreeSet.Basic
/-- Inserts multiple elements into the tree set by iterating over the given collection and calling
`insert`. If the same element (with respect to `cmp`) appears multiple times, the first occurrence
takes precedence.

Note: this precedence behavior is true for `ExtTreeSet` and `ExtTreeSet.Raw`. The `insertMany` function on
`ExtTreeMap`, `ExtDTreeMap`, `ExtTreeMap.Raw` and `ExtDTreeMap.Raw` behaves differently: it will prefer the last
appearance.
 -/
Std.ExtTreeSet.insertMany : {α : Type u} →
  {cmp : α → α → Ordering} →
    [Std.TransCmp cmp] → {ρ : Type u_1} → [ForIn Id ρ α] → Std.ExtTreeSet α cmp → ρ → Std.ExtTreeSet α cmp
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonColor.toJson : Lean.Lsp.Color → Lean.Json
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.powerlt_succ : ∀ {a b : Cardinal.{u_1}}, a ≠ 0 → a ^< Order.succ b = a ^ b
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.cm1a : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C],
  CategoryTheory.Limits.HasFiniteLimits C
-- Mathlib.Order.Category.PartOrd
PartOrd.Iso.mk_inv : ∀ {α β : PartOrd} (e : ↑α ≃o ↑β), (PartOrd.Iso.mk e).inv = PartOrd.ofHom ↑e.symm
-- Mathlib.LinearAlgebra.Orientation
Orientation.map_of_isEmpty : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (ι : Type u_4) [IsEmpty ι] (x : Orientation R M ι) (f : M ≃ₗ[R] M),
  (Orientation.map ι f) x = x
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.zeros : ∀ {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i j : ℕ}, (i, j) ∉ μ → T i j = 0
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The norm of the image of `m : M` in the quotient by `S` is zero if and only if `m`
belongs to the closure of `S`.  -/
QuotientAddGroup.norm_mk_eq_zero_iff_mem_closure : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M} {m : M}, ‖↑m‖ = 0 ↔ m ∈ closure ↑S
-- Mathlib.Order.SuccPred.CompleteLinearOrder
exists_eq_ciInf_of_not_isPredLimit : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α},
  BddBelow (Set.range f) → ¬Order.IsPredLimit (⨅ i, f i) → ∃ i, f i = ⨅ i, f i
-- Mathlib.Analysis.InnerProductSpace.Calculus
HasDerivWithinAt.inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {f g : ℝ → E} {f' g' : E} {s : Set ℝ} {x : ℝ},
  HasDerivWithinAt f f' s x →
    HasDerivWithinAt g g' s x →
      HasDerivWithinAt (fun t => inner 𝕜 (f t) (g t)) (inner 𝕜 (f x) g' + inner 𝕜 f' (g x)) s x
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.isInducing : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
  IsDenseInducing i → Topology.IsInducing i
-- Mathlib.CategoryTheory.EqToHom
/-- `eqToHom h` is heterogeneously equal to the identity of its codomain.  -/
CategoryTheory.eqToHom_heq_id_cod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X Y : C) (h : X = Y),
  CategoryTheory.eqToHom h ≍ CategoryTheory.CategoryStruct.id Y
-- Init.Data.Option.Lemmas
Option.max_eq_none_iff : ∀ {α : Type u_1} [inst : Max α] {o o' : Option α}, o ⊔ o' = none ↔ o = none ∧ o' = none
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.image_coe_inj : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal] {s t : Set G},
  QuotientGroup.mk '' s = QuotientGroup.mk '' t ↔ ↑N * s = ↑N * t
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.instBoundedOrder : {α : Type u_1} → [inst : TopologicalSpace α] → [inst_1 : LE α] → BoundedOrder (ClopenUpperSet α)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.instEquivLike : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              {σ₂₁ : R₂ →+* R} →
                [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] → [inst_7 : Module R₂ E₂] → EquivLike (E ≃ₛₗᵢ[σ₁₂] E₂) E E₂
-- Mathlib.Algebra.Group.Defs
nsmulRec'.eq_2 : ∀ {M : Type u_2} [inst : Zero M] [inst_1 : Add M] (x : M), nsmulRec' 1 x = x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Ordered.upperBound?_exists : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut],
  RBTree.RBNode.Ordered cmp t → ((∃ x, RBTree.RBNode.upperBound? cut t = some x) ↔ ∃ x ∈ t, cut x ≠ Ordering.gt)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The canonical example of a normalised EDS `W : ℤ → R`, with initial values
`W(0) = 0`, `W(1) = 1`, `W(2) = b`, `W(3) = c`, and `W(4) = d * b`.

This is defined in terms of `preNormEDS` whose even terms differ by a factor of `b`.  -/
normEDS : {R : Type u_1} → [CommRing R] → R → R → R → ℤ → R
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_castPred_of_lt : ∀ {n : ℕ} (p i : Fin (n + 1)) (h : p < i), (p.castPred ⋯).predAbove i = i.pred ⋯
-- Mathlib.Algebra.Homology.Single
CochainComplex.toSingle₀Equiv_symm_apply_f_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {C : CochainComplex V ℕ} {X : V} (f : C.X 0 ⟶ X),
  ((C.toSingle₀Equiv X).symm f).f 0 = f
-- Mathlib.Tactic.ByCases
_private.Mathlib.Tactic.ByCases.0.Mathlib.Tactic.ByCases.tacticTry_push_neg_at__ : Lean.ParserDescr
-- Mathlib.Analysis.Complex.Liouville
/-- A corollary of Liouville's theorem where the function tends to a finite value at infinity
(i.e., along `Filter.cocompact`, which in proper spaces coincides with `Bornology.cobounded`).  -/
Differentiable.apply_eq_of_tendsto_cocompact : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [Nontrivial E] {f : E → F},
  Differentiable ℂ f → ∀ {c : F} (x : E), Filter.Tendsto f (Filter.cocompact E) (nhds c) → f x = c
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ici_nsmul_eq : ∀ {α : Type u_2} [inst : AddMonoid α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α] [AddRightMono α] {a : α} (n : ℕ),
  n ≠ 0 → n • Set.Ici a = Set.Ici (n • a)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.w_assoc : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g) {Z : T}
  (h : g.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) (CategoryTheory.CategoryStruct.comp g.hom h) =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right sq) h)
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.instCategoryI₀Pullback₁ : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    [inst : P.IsStableUnderBaseChange] →
      (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
        [CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] →
          {Y : AlgebraicGeometry.Scheme} →
            (f : Y ⟶ X) →
              CategoryTheory.Category.{v_2, u_1} (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
-- Mathlib.Order.Sublattice
Sublattice.inclusion_injective : ∀ {α : Type u_2} [inst : Lattice α] {L M : Sublattice α} (h : L ≤ M), Function.Injective ⇑(Sublattice.inclusion h)
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.IsDynCoverOf.closure : ∀ {X : Type u_1} {T : X → X} {F s : Set X} {U V : SetRel X X} {n : ℕ} [inst : UniformSpace X],
  Continuous T → V ∈ uniformity X → Dynamics.IsDynCoverOf T F U n s → Dynamics.IsDynCoverOf T (closure F) (V.comp U) n s
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_inv_hom_id_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : a ≤ b)
  (X : C) {Z : C} (h : (t.eTruncGE.obj b).obj ((t.eTruncGE.obj a).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncGEIsoGEGE a b hab).inv.app X)
      (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)) h) =
    h
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.single_mem_span_single : ∀ {α : Type u_1} (R : Type u_5) [inst : Semiring R] [Nontrivial R] {a : α} {s : Set α},
  (fun₀ | a => 1) ∈ Submodule.span R ((fun x => fun₀ | x => 1) '' s) ↔ a ∈ s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a k : α} {v : β k},
  (m.insert k v).getKey? a = if (k == a) = true then some k else m.getKey? a
-- Mathlib.Topology.Constructions
isOpenMap_sigma_map : ∀ {ι : Type u_5} {κ : Type u_6} {σ : ι → Type u_7} {τ : κ → Type u_8} [inst : (i : ι) → TopologicalSpace (σ i)]
  [inst_1 : (k : κ) → TopologicalSpace (τ k)] {f₁ : ι → κ} {f₂ : (i : ι) → σ i → τ (f₁ i)},
  IsOpenMap (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsOpenMap (f₂ i)
-- Mathlib.RingTheory.SimpleModule.Basic
LinearMap.bijective_of_ne_zero : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSimpleModule R M] [IsSimpleModule R N] {f : M →ₗ[R] N},
  f ≠ 0 → Function.Bijective ⇑f
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.cyclesMap_Ψ : ∀ {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 j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (f₂₃ : j ⟶ l),
  CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃ →
    ∀ (n₀ n₁ : ℤ) (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesMap_Ψ._auto_1),
      CategoryTheory.CategoryStruct.comp
          (X.cyclesMap f₁₂ f₃ f₂ f₃ (CategoryTheory.ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀)
          (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁) =
        0
-- Mathlib.Topology.Constructions.SumProd
isClosedMap_swap : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsClosedMap Prod.swap
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.instGroupSubtypeMemSubmonoidSpecialUnitaryGroup : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {α : Type v} → [inst_2 : CommRing α] → [inst_3 : StarRing α] → Group ↥(Matrix.specialUnitaryGroup n α)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.map_surjective : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid N']
  [inst_8 : Module R N] [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g] (h : M →ₗ[R] N),
  Function.Surjective ⇑h → Function.Surjective ⇑((IsLocalizedModule.map S f g) h)
-- Mathlib.GroupTheory.PushoutI
/-- Induction principle for `NormalWord`, that corresponds closely to inducting on
the underlying list.  -/
Monoid.PushoutI.NormalWord.consRecOn : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} →
              [inst_2 : DecidableEq ι] →
                [inst_3 : (i : ι) → DecidableEq (G i)] →
                  {motive : Monoid.PushoutI.NormalWord d → Sort u_5} →
                    (w : Monoid.PushoutI.NormalWord d) →
                      motive Monoid.PushoutI.NormalWord.empty →
                        ((i : ι) →
                            (g : G i) →
                              (w : Monoid.PushoutI.NormalWord d) →
                                (hmw : w.fstIdx ≠ some i) →
                                  g ∈ d.set i →
                                    (hgr : g ∉ (φ i).range) →
                                      w.head = 1 → motive w → motive (Monoid.PushoutI.NormalWord.cons g w hmw hgr)) →
                          ((h : H) →
                              (w : Monoid.PushoutI.NormalWord d) →
                                w.head = 1 → motive w → motive ((Monoid.PushoutI.base φ) h • w)) →
                            motive w
-- Mathlib.Data.PNat.Defs
/-- We define `m % k` in the same way as for `ℕ`
except that when `m = n * k` we take `m % k = k` This ensures that `m % k` is always positive.
 -/
PNat.mod : ℕ+ → ℕ+ → ℕ+
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List α} {k : α}, k ∉ t → l.contains k = false → (t.insertMany l).get? k = none
-- Mathlib.Order.SuccPred.Basic
Order.pred_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] (a : α), Order.pred a ≤ a
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarKind.postponed.sizeOf_spec : ∀ (ctx : Lean.Elab.Term.SavedContext), sizeOf (Lean.Elab.Term.SyntheticMVarKind.postponed ctx) = 1 + sizeOf ctx
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.of_isLocalization : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (M : Submonoid S)
  [IsLocalization M T] [Algebra.QuasiFinite R S], Algebra.QuasiFinite R T