mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.d_comp_XIsoOfEq_hom_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₃ : ι}
  (h : p₂ = p₃) (p₁ : ι) {Z : V} (h_1 : K.X p₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.d p₁ p₂) (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).hom h_1) =
    CategoryTheory.CategoryStruct.comp (K.d p₁ p₃) h_1
-- Aesop.BuiltinRules.DestructProducts
_private.Aesop.BuiltinRules.DestructProducts.0.Aesop.BuiltinRules.destructProductHyp? : Lean.MVarId → Lean.FVarId → Lean.Meta.TransparencyMode → Lean.MetaM (Option (Aesop.Script.LazyStep × Lean.MVarId))
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.closure_pow_anti : ∀ {G : Type u_2} [inst : Group G] {s : Set G} {m n : ℕ}, m ∣ n → Subgroup.closure (s ^ n) ≤ Subgroup.closure (s ^ m)
-- Lean.Elab.Do.ForwardSyntax
/-- If `e` is a function application whose last argument effect-forwards into the enclosing `do`
block (its body bears a `do←` marker, possibly under `fun` binders), return the application
head sans the forwarding argument together with the `ForwardArg` description.
 -/
Lean.Elab.Do.Forward.matchApp? : Lean.Term → Option (Lean.Term × Lean.Elab.Do.ForwardArg)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanQueryModuleParams : Lean.FromJson Lean.Lsp.LeanQueryModuleParams
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.lift_cone : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F],
  CategoryTheory.Limits.limit.lift F (CategoryTheory.Limits.limit.cone F) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit F)
-- Mathlib.Data.Set.Card
Set.ncard_eq_three : ∀ {α : Type u_1} {s : Set α}, s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_strictMono_of_surjective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Surjective ⇑f → StrictMono (FirstOrder.Language.Substructure.comap f)
-- Mathlib.Data.Finset.Union
Finset.biUnion_subset : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [inst : DecidableEq β] {s' : Finset β},
  s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.colimitAdjunction_homEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.IsCofiltered C] [inst_3 : CategoryTheory.InitiallySmall C]
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R}
  (hcR : CategoryTheory.Limits.IsColimit cR) {F : PresheafOfModules R} {G : ModuleCat ↑cR.pt}
  (β : F ⟶ (PresheafOfModules.constFunctor cR).obj G) {X : Cᵒᵖ} (m : ↑(F.obj X)),
  (CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.colimitAdjunction hcR).homEquiv F G).symm β))
      (PresheafOfModules.ModuleColimit.ιM m) =
    (CategoryTheory.ConcreteCategory.hom (β.app X)) m
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
/-- A star projection is an element in a von Neumann algebra if and only if
its range is invariant under the commutant.  -/
VonNeumannAlgebra.IsStarProjection.mem_iff : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  {e : H →L[ℂ] H},
  IsStarProjection e → ∀ (S : VonNeumannAlgebra H), e ∈ S ↔ ∀ y ∈ S.commutant, (↑e).range ∈ Module.End.invtSubmodule ↑y
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_surjective : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  Function.Surjective ArchimedeanClass.mk
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β k}, a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.Data.NNRat.Defs
NNRat.num.eq_1 : ∀ (q : ℚ≥0), q.num = (↑q).num.natAbs
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.eq_of_xn_modEq' : ∀ {a : ℕ} (a1 : 1 < a) {i j n : ℕ},
  0 < i → i ≤ n → j ≤ 4 * n → Pell.xn a1 j ≡ Pell.xn a1 i [MOD Pell.xn a1 n] → j = i ∨ j + i = 4 * n
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.epi_of_epi_f : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L),
  (∀ (i : ι), CategoryTheory.Epi (φ.f i)) → CategoryTheory.Epi φ
-- Init.Data.ByteArray.Bootstrap
ByteArray.data_push : ∀ {a : ByteArray} {b : UInt8}, (a.push b).data = a.data.push b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.equiv_iff_toArray_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp},
  t₁.Equiv t₂ ↔ t₁.toArray.Perm t₂.toArray
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuous_empty : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] [IsEmpty ι]
  (F : ι → X → α), Equicontinuous F
-- Mathlib.RingTheory.RegularLocalRing.Defs
instIsRegularRingOfIsDedekindDomain : ∀ (R : Type u_1) [inst : CommRing R] [IsDedekindDomain R], IsRegularRing R
-- Mathlib.Analysis.Convex.Cone.Dual
/-- Geometric interpretation of **Farkas' lemma**. Also stronger version of the
**Hahn-Banach separation theorem** for proper cones.  -/
ProperCone.hyperplane_separation_point : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [IsTopologicalAddGroup E] [inst_3 : Module ℝ E]
  [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {x₀ : E} (C : ProperCone ℝ E),
  x₀ ∉ C → ∃ f, (∀ x ∈ C, 0 ≤ f x) ∧ f x₀ < 0
-- Lean.Elab.PreDefinition.Basic
/-- Auxiliary method for (temporarily) adding pre definition as an axiom  -/
Lean.Elab.addAsAxiom : Lean.Elab.PreDefinition → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.whiskerEquiv_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C}
  (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [inst_1 : CategoryTheory.Limits.HasProduct f]
  [inst_2 : CategoryTheory.Limits.HasProduct g],
  (CategoryTheory.Limits.Pi.whiskerEquiv e w).inv = CategoryTheory.Limits.Pi.map' ⇑e fun j => (w j).hom
-- Mathlib.Order.Interval.Set.Basic
/-- **Alias** of the reverse direction of `Set.Ioi_eq_empty_iff`. -/
IsMax.Ioi_eq : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsMax a → Set.Ioi a = ∅
-- Mathlib.Data.Part
Part.mem_unique : ∀ {α : Type u_1} {a b : α} {o : Part α}, a ∈ o → b ∈ o → a = b
-- Mathlib.Data.Set.Function
/-- Construct the inverse for a function `f` on domain `s`. This function is a right inverse of `f`
on `f '' s`. For a computable version, see `Function.Embedding.invOfMemRange`.  -/
Function.invFunOn : {α : Type u_1} → {β : Type u_2} → [Nonempty α] → (α → β) → Set α → β → α
-- Mathlib.RingTheory.OrzechProperty
orzechProperty_iff : ∀ (R : Type u) [inst : Semiring R],
  OrzechProperty R ↔
    ∀ {M : Type u} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Finite R M] {N : Submodule R M}
      (f : ↥N →ₗ[R] M), Function.Surjective ⇑f → Function.Injective ⇑f
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImportKind.isPrivate : Lean.Lsp.LeanImportKind → Bool
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- **Alias** of `FractionalIdeal.extendedHom_eq_zero_iff`. -/
FractionalIdeal.extendedHomₐ_eq_zero_iff : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K},
  (FractionalIdeal.extendedHom L B) I = 0 ↔ I = 0
-- Mathlib.Tactic.Order.Graph.Tarjan
/-- The Tarjan's algorithm.
See [Wikipedia](https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm).  -/
Mathlib.Tactic.Order.Graph.tarjanDFS : Mathlib.Tactic.Order.Graph → ℕ → StateM Mathlib.Tactic.Order.Graph.TarjanState Unit
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- For the versions of this lemma where `ν.withDensity (μ.rnDeriv ν)` or `μ.singularPart ν` are
isolated, see `MeasureTheory.Measure.measure_sub_singularPart` and
`MeasureTheory.Measure.measure_sub_rnDeriv`.  -/
MeasureTheory.Measure.singularPart_add_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν],
  μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = μ
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction.eq_2 : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β]
  (x : Std.Tactic.BVDecide.LRAT.Action β α),
  (∀ (id : ℕ) (c : β) (p : Std.Sat.Literal α) (rupHints : Array ℕ) (ratHints : Array (ℕ × Array ℕ)),
      x = Std.Tactic.BVDecide.LRAT.Action.addRat id c p rupHints ratHints → False) →
    Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction x = True
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `DifferentiableOn.finsetProd`. -/
DifferentiableOn.finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} {ι : Type u_2} {𝔸' : Type u_3}
  [inst_1 : NormedCommRing 𝔸'] [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableOn 𝕜 (f i) s) → DifferentiableOn 𝕜 (∏ i ∈ u, f i) s
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.hasCoeSubgroup : {G : Type u_1} → [inst : Group G] → [inst_1 : TopologicalSpace G] → CoeTC (OpenSubgroup G) (Subgroup G)
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.Functor.reflects_exact_of_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] [F.Faithful] (S : CategoryTheory.ShortComplex C), (S.map F).Exact → S.Exact
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.ext_to : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : i + 1 = j)
  {A : C} {f g : A ⟶ (CochainComplex.mappingCone φ).X i},
  CategoryTheory.CategoryStruct.comp f ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) =
      CategoryTheory.CategoryStruct.comp g ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) →
    CategoryTheory.CategoryStruct.comp f ((CochainComplex.mappingCone.snd φ).v i i ⋯) =
        CategoryTheory.CategoryStruct.comp g ((CochainComplex.mappingCone.snd φ).v i i ⋯) →
      f = g
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp},
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ (f : (a : α) → β a → Option (γ a)), (Std.DTreeMap.Raw.filterMap f t₁).Equiv (Std.DTreeMap.Raw.filterMap f t₂)
-- Std.Sat.AIG.RelabelNat
/-- This invariant says that we have already visited and inserted all nodes up to a certain index.
 -/
Std.Sat.AIG.RelabelNat.State.Inv2 : {α : Type} → [inst : DecidableEq α] → [inst_1 : Hashable α] → Array (Std.Sat.AIG.Decl α) → ℕ → Std.HashMap α ℕ → Prop
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero : ∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [inst_3 : TopologicalSpace α]
  [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α} [μ.Regular], μ ≠ 0 → IsOpen U → U.Nonempty → 0 < μ U
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.closure_eq_of_le : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M} {s : Set M},
  s ⊆ ↑S →
    S ≤ (FirstOrder.Language.Substructure.closure L).toFun s → (FirstOrder.Language.Substructure.closure L).toFun s = S
-- Aesop.Search.SearchM
Aesop.SearchM.instMonadStateState : {Q : Type} → [inst : Aesop.Queue Q] → MonadState (Aesop.SearchM.State Q) (Aesop.SearchM Q)
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.mulLeft_zero_eq_zero` for matrix multiplication.  -/
mulLeftLinearMap_zero_eq_zero : ∀ {l : Type u_1} {m : Type u_2} (n : Type u_3) (R : Type u_5) {A : Type u_6} [inst : Fintype m] [inst_1 : Semiring R]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : SMulCommClass R A A],
  mulLeftLinearMap n R 0 = 0
-- Mathlib.Analysis.Calculus.ParametricIntegral
/-- Differentiation under integral of `x ↦ ∫ x in a..b, F x a` at a given point `x₀`, assuming
`F x₀` is integrable on `(a,b)`, `x ↦ F x a` is differentiable on a neighborhood of `x₀` for ae `a`
with derivative norm uniformly bounded by an integrable function (the neighborhood is independent
of `a`), and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`.  -/
hasFDerivAt_integral_of_dominated_of_fderiv_le'' : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_4} [inst_2 : NormedAddCommGroup H]
  {x₀ : H} {s : Set H} [inst_3 : NormedSpace ℝ H] {μ : MeasureTheory.Measure ℝ} {F : H → ℝ → E} {F' : H → ℝ → H →L[ℝ] E}
  {a b : ℝ} {bound : ℝ → ℝ},
  s ∈ nhds x₀ →
    (∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) →
      IntervalIntegrable (F x₀) μ a b →
        MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Set.uIoc a b)) →
          (∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ∀ x ∈ s, ‖F' x t‖ ≤ bound t) →
            IntervalIntegrable bound μ a b →
              (∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ∀ x ∈ s, HasFDerivAt (fun x => F x t) (F' x t) x) →
                HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
-- Init.Data.Rat.Lemmas
Rat.natCast_nonneg : ∀ {a : ℕ}, 0 ≤ ↑a
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
/-- Typeclass for formulas. An instance `[Formula α β σ]` indicates that `σ` is the type of a formula
with variables of type `α`, clauses of type `β`, and clause ids of type `Nat`.
 -/
Std.Tactic.BVDecide.LRAT.Internal.Formula : (α : outParam (Type u)) →
  (β : outParam (Type v)) →
    [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] →
      (σ : Type w) → [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] → Type (max (max u v) w)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {k a : α},
  Std.ExtDTreeMap.Const.get! (t.erase k) a = if cmp k a = Ordering.eq then default else Std.ExtDTreeMap.Const.get! t a
-- Mathlib.Tactic.CrossRefAttribute
/-- Append a cross-reference link to the docstring of `decl` and record it in `tagExt`.
This is the database-agnostic core of every cross-reference attribute's `add` handler.  -/
Mathlib.CrossRef.addCrossRefDoc : Mathlib.CrossRef.Database → Lean.Name → String → String → Lean.CoreM Unit
-- Mathlib.Topology.Order.OrderClosed
Ico_mem_nhdsLE_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b c : α},
  b ∈ Set.Ioo a c → Set.Ico a c ∈ nhdsWithin b (Set.Iic b)
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- `t` is in the shadow of `𝒜` iff we can add an element to it so that the resulting finset is in
`𝒜`.  -/
Finset.mem_shadow_iff_insert_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α}, t ∈ 𝒜.shadow ↔ ∃ a ∉ t, insert a t ∈ 𝒜
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.insert_sdiff_of_notMem`. -/
Set.insert_diff_of_notMem : ∀ {α : Type u_1} {t : Set α} {a : α} (s : Set α), a ∉ t → insert a s \ t = insert a (s \ t)
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left_assoc : ∀ {S : AlgebraicGeometry.Scheme} {X : CategoryTheory.Over S} (𝒰 : X.left.OpenCover)
  [inst : CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  {Y : CategoryTheory.Over S} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left)
  (h :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) (g j) = g i)
  (w : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.f i) X.hom)
  (i : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h_1 : Y.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp (𝒰.f i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (𝒰.glueMorphismsOverOfLocallyDirected g ⋯ w))
        h_1) =
    CategoryTheory.CategoryStruct.comp (g i) h_1
-- Mathlib.Algebra.Order.Group.Synonym
isAddRightRegular_toLex : ∀ {α : Type u_1} [inst : AddMonoid α] {a : α}, IsAddRightRegular (toLex a) ↔ IsAddRightRegular a
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.opEquivOpUnder_functor_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T) {Z Y : CategoryTheory.Over (Opposite.op X)}
  (f : Z ⟶ Y),
  (CategoryTheory.Over.opEquivOpUnder X).functor.map f =
    Opposite.op (CategoryTheory.Under.homMk (CategoryTheory.Over.Hom.left f).unop ⋯)
-- Mathlib.Topology.Bases
/-- In a topological space with second countable topology, if `f` is a function that sends each
point `x` to a neighborhood of `x`, then for some countable set `s`, the neighborhoods `f x`,
`x ∈ s`, cover the whole space.  -/
TopologicalSpace.countable_cover_nhds : ∀ {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {f : α → Set α},
  (∀ (x : α), f x ∈ nhds x) → ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = Set.univ
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.pullback_symm_apply_proj : ∀ {B : Type u} {F : Type v} {E : B → Type w₁} {B' : Type w₂} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : TopologicalSpace F] [inst_3 : TopologicalSpace B]
  [inst_4 : ∀ (_b : B), Nonempty (E _b)] {K : Type U} [inst_5 : FunLike K B' B] [inst_6 : ContinuousMapClass K B' B]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) (f : K) (y : B' × F), (↑(e.pullback f).symm y).proj = y.1
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.topCat_hasLimits : CategoryTheory.Limits.HasLimits TopCat
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
/-- Restrict codomain of a continuous linear map.  -/
ContinuousLinearMap.restrict : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            {M₂ : Type u_5} →
              [inst_2 : TopologicalSpace M₁] →
                [inst_3 : AddCommMonoid M₁] →
                  [inst_4 : Module R₁ M₁] →
                    [inst_5 : TopologicalSpace M₂] →
                      [inst_6 : AddCommMonoid M₂] →
                        [inst_7 : Module R₂ M₂] →
                          (f : M₁ →SL[σ₁₂] M₂) →
                            {p : Submodule R₁ M₁} → {q : Submodule R₂ M₂} → (∀ x ∈ p, f x ∈ q) → ↥p →SL[σ₁₂] ↥q
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.coe_positive : ∀ (R : Type u_2) (M : Type u_4) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : PartialOrder M] [inst_4 : IsOrderedAddMonoid M] [inst_5 : Module R M] [inst_6 : PosSMulMono R M],
  ↑(ConvexCone.positive R M) = Set.Ici 0
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.inv_neg_iff : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a : R}, a⁻¹ < 0 ↔ a < 0
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.ext_iff : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s t : TopologicalSpace.IrreducibleCloseds α}, s = t ↔ ↑s = ↑t
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
/-- A multifork `c : Multifork I` in the category of types is limit iff the
map `c.toSections : c.pt → I.sections` is a bijection.  -/
CategoryTheory.Limits.Multifork.isLimit_types_iff : ∀ {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)}
  (c : CategoryTheory.Limits.Multifork I), Nonempty (CategoryTheory.Limits.IsLimit c) ↔ Function.Bijective c.toSections
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.subtype_isoBaseOfIsPrincipal_eq_mul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {I : Ideal R} [hprinc : Submodule.IsPrincipal I] (h : I ≠ ⊥),
  Submodule.subtype I ∘ₗ ↑(Ideal.isoBaseOfIsPrincipal h) = (LinearMap.mul R R) (Submodule.IsPrincipal.generator I)
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The right action of this bimodule object  -/
Bimod.actRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {A B : CategoryTheory.Mon C} →
        (self : Bimod A B) → CategoryTheory.MonoidalCategoryStruct.tensorObj self.X B.X ⟶ self.X
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.ι_isOpenImmersion : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J), AlgebraicGeometry.IsOpenImmersion (D.ι i)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (R : Type u_1)
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n)
  (a_1 : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'),
  (CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv R K L n a n' hn').symm a_1 = a_1.rightUnshift n hn'
-- Mathlib.Data.Finsupp.Defs
Finsupp.embDomain.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_4} [inst : Zero M] (f : α ↪ β) (v : α →₀ M),
  Finsupp.embDomain f v =
    { support := Finset.map f v.support,
      toFun := fun b =>
        match Multiset.find? (fun a => f a = b) v.support.val ⋯ with
        | some a => v a
        | none => 0,
      mem_support_toFun := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.instAddCommGroupModuleColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {cR : CategoryTheory.Limits.Cocone R} →
        (hcR : CategoryTheory.Limits.IsColimit cR) →
          {M : PresheafOfModules R} →
            {cM : CategoryTheory.Limits.Cocone M.presheaf} →
              (hcM : CategoryTheory.Limits.IsColimit cM) → AddCommGroup (PresheafOfModules.ModuleColimit hcR hcM)
-- Init.Data.String.Iterate
/-- Creates an iterator over all bytes in {name}`s`.

Examples:
* {lean}`"abc".toSlice.bytes.toList = [97, 98, 99]`
* {lean}`"ab∀c".toSlice.bytes.toList = [97, 98, 226, 136, 128, 99]`
 -/
String.Slice.bytes : String.Slice → Std.Iter UInt8
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.tendsto_nhdsWithin_nhds : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {s : Set α} [inst_1 : PseudoMetricSpace β] {f : α → β} {a : α}
  {b : β},
  Filter.Tendsto f (nhdsWithin a s) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommFoldr.eq_1 : ∀ {α : Type u_3} {β : Type u_4} (f : α → β → β) (s : Multiset α)
  (comm : {x | x ∈ s}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)) (b : β),
  Multiset.noncommFoldr f s comm b = Multiset.foldr (f ∘ Subtype.val) b s.attach