mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}),
  ProfiniteGrp.instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap
      F =
    {
      mul :=
        ProfiniteGrp.instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap._aux_1
          F,
      mul_assoc := ⋯,
      one :=
        ProfiniteGrp.instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap._aux_4
          F,
      one_mul := ⋯, mul_one := ⋯,
      npow :=
        ProfiniteGrp.instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap._aux_8
          F,
      npow_zero := ⋯, npow_succ := ⋯,
      inv :=
        ProfiniteGrp.instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap._aux_12
          F,
      div :=
        ProfiniteGrp.instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap._aux_14
          F,
      zpow :=
        ProfiniteGrp.instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap._aux_16
          F,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.RingTheory.Kaehler.Basic
instIsScalarTowerTensorProductKaehlerDifferential : ∀ (R : Type u_2) (S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  IsScalarTower S (TensorProduct R S S) Ω[S⁄R]
-- Std.Data.TreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.TreeMap.getKey? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → Option α
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.toFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) {X Y : C} (i : X ⟶ Y),
  G.toFunctor.map i = TypeCat.ofHom fun x => ⟨(CategoryTheory.ConcreteCategory.hom (F.map i)) ↑x, ⋯⟩
-- Mathlib.Geometry.Manifold.Notation
/-- `CMDiff[s] n f` elaborates to `ContMDiffOn I J n f s`,
trying to determine `I` and `J` from the local context.
`n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported).  -/
Manifold.«termCMDiff[_]____» : Lean.ParserDescr
-- Std.Async.IO
Std.Async.IO.AsyncWrite.writeAll : {α β : Type} → [self : Std.Async.IO.AsyncWrite α β] → α → Array β → Std.Async.Async Unit
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.Monoidal.tensorHom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  {M₁ M₂ M₃ M₄ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄)
  (X : Cᵒᵖ),
  (PresheafOfModules.Monoidal.tensorHom f g).app X = CategoryTheory.MonoidalCategoryStruct.tensorHom (f.app X) (g.app X)
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- An additive action is `n`-multiply preprimitive if it is `n`-multiply pretransitive
and if, when `n ≥ 1`, for every set `s` of cardinality `n - 1`,
the action of `fixingAddSubgroup M s` on the complement of `s` is preprimitive.  -/
AddAction.IsMultiplyPreprimitive : (M : Type u_1) → (α : Type u_2) → [inst : AddGroup M] → [AddAction M α] → ℕ → Prop
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The Haar measure is a Haar measure, i.e., it is invariant and gives finite mass to compact
sets and positive mass to nonempty open sets.  -/
MeasureTheory.Measure.isHaarMeasure_haarMeasure : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G),
  (MeasureTheory.Measure.haarMeasure K₀).IsHaarMeasure
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.guard : Lean.Parser.Parser
-- Mathlib.GroupTheory.ArchimedeanDensely
instDenselyOrderedAdditive : ∀ {X : Type u_2} [inst : LT X] [DenselyOrdered X], DenselyOrdered (Additive X)
-- Mathlib.Algebra.Module.Torsion.Basic
Ideal.annihilator_span_singleton_eq_torsionOf : ∀ {R : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  (R ∙ x).annihilator = Ideal.torsionOf R M x
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Eta-expanded form of `MeromorphicOn.divisor_ball_comp_sub_const_eq_divisor_ball`

---

Divisors are invariant under translation, special case where the set is a ball..  -/
MeromorphicOn.divisor_ball_fun_comp_sub_const_eq_divisor_ball : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {z : 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {c : 𝕜} {R : ℝ} {f : 𝕜 → E},
  (MeromorphicOn.divisor (fun x => f (x - c)) (Metric.ball c R)) (z + c) = (MeromorphicOn.divisor f (Metric.ball 0 R)) z
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPower.beq.eq_def : ∀ (x x_1 : Lean.Grind.CommRing.Power),
  Lean.Grind.CommRing.instBEqPower.beq x x_1 =
    match x, x_1 with
    | { x := a, k := a_1 }, { x := b, k := b_1 } => a == b && a_1 == b_1
    | x, x_2 => false
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.prodAssoc_apply : ∀ (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) (P₃ : Type u_4) {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃] [inst_11 : AddTorsor V₃ P₃]
  [inst_12 : TopologicalSpace P₃] (p : (P₁ × P₂) × P₃),
  (ContinuousAffineEquiv.prodAssoc k P₁ P₂ P₃) p = (p.1.1, p.1.2, p.2)
-- Mathlib.LinearAlgebra.Dimension.Constructions
Subalgebra.finrank_bot : ∀ {F : Type u_2} {E : Type u_3} [inst : CommRing F] [IsDomain F] [inst_2 : Ring E] [inst_3 : Algebra F E]
  [StrongRankCondition F] [Module.IsTorsionFree F E] [Nontrivial E], Module.finrank F ↥⊥ = 1
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- The scalar recurrence initialized by array lookup agrees pointwise
with the matrix recurrence.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.iterate_stepEntry_get_eq_spec : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A : Array R) (hA : A.size = n * n) (t : ℕ) (i j : Fin n),
  (BirdDet.stepEntry n A)^[t] (BirdDet.get n A) ↑i ↑j =
    (BirdDet.Spec.stepEntry (Matrix.ofArray A hA))^[t] (Matrix.ofArray A hA) i j
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
/-- Tell `simp` what the entries are in a conjugate transposed matrix.

Compare with `mul_apply`, `diagonal_apply_eq`, etc.
 -/
Matrix.conjTranspose_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Star α] (M : Matrix m n α) (i : m) (j : n),
  M.conjTranspose j i = star (M i j)
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- The traditional `ε`-`δ` definition of absolutely continuous: A function `f` is
*absolutely continuous* on `uIcc a b` if for any `ε > 0`, there is `δ > 0` such that for
any finite disjoint collection of intervals `uIoc (a i) (b i)` for `i < n` where `a i`, `b i` are
all in `uIcc a b` for `i < n`, if `∑ i ∈ range n, dist (a i) (b i) < δ`, then
`∑ i ∈ range n, dist (f (a i)) (f (b i)) < ε`.  -/
absolutelyContinuousOnInterval_iff : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] (f : ℝ → X) (a b : ℝ),
  AbsolutelyContinuousOnInterval f a b ↔
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ E ∈ AbsolutelyContinuousOnInterval.disjWithin a b,
          ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
            ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.refl_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X], (PartialHomeomorph.refl X).symm = PartialHomeomorph.refl X
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- Construct an isomorphism of cospans from components.  -/
CategoryTheory.Limits.cospanExt : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z X' Y' Z' : C} →
      (iX : X ≅ X') →
        (iY : Y ≅ Y') →
          (iZ : Z ≅ Z') →
            {f : X ⟶ Z} →
              {g : Y ⟶ Z} →
                {f' : X' ⟶ Z'} →
                  {g' : Y' ⟶ Z'} →
                    CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom →
                      CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom →
                        (CategoryTheory.Limits.cospan f g ≅ CategoryTheory.Limits.cospan f' g')
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.rank_top : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], Module.rank (↥⊤) E = 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.of_forall_getKey_eq_of_forall_getElem?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF →
    t₂.WF →
      (∀ (k : α) (hk : k ∈ t₁) (hk' : k ∈ t₂), t₁.getKey k hk = t₂.getKey k hk') →
        (∀ (k : α), t₁[k]? = t₂[k]?) → t₁.Equiv t₂
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.rightCont_apply : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : PartialOrder ι] [inst_1 : TopologicalSpace ι]
  [OrderTopology ι] (𝓕 : MeasureTheory.Filtration ι m) (i : ι),
  ↑𝓕.rightCont i = if (nhdsWithin i (Set.Ioi i)).NeBot then ⨅ j, ⨅ (_ : j > i), ↑𝓕 j else ↑𝓕 i
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.mk.injEq : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit}
  (map : Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w)
  (hbound :
    ∀ {i : ℕ} (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ map) (h2 : i < k.w),
      (map.get k h1)[i].gate < aig.decls.size)
  (map_1 : Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w)
  (hbound_1 :
    ∀ {i : ℕ} (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ map_1) (h2 : i < k.w),
      (map_1.get k h1)[i].gate < aig.decls.size),
  ({ map := map, hbound := hbound } = { map := map_1, hbound := hbound_1 }) = (map = map_1)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.abs_integral_eq_abs_integral_uIoc : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (f : ℝ → ℝ), |∫ (x : ℝ) in a..b, f x ∂μ| = |∫ (x : ℝ) in Set.uIoc a b, f x ∂μ|
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `S ∈ 𝔖`, then the restriction to `S` is a uniformly continuous map from `α →ᵤ[𝔖] β` to
`↥S →ᵤ β`.  -/
UniformOnFun.uniformContinuous_restrict : ∀ (α : Type u_1) (β : Type u_2) {s : Set α} [inst : UniformSpace β] (𝔖 : Set (Set α)),
  s ∈ 𝔖 → UniformContinuous (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖))
-- Mathlib.AlgebraicGeometry.Gluing
_private.Mathlib.AlgebraicGeometry.Gluing.0.AlgebraicGeometry.Scheme.GlueData.termD_ : Lean.ParserDescr
-- Mathlib.Topology.Sheaves.Functors
/-- The pullback functor.
 -/
TopCat.Sheaf.pullback : {X Y : TopCat} →
  (A : Type u_1) →
    [inst : CategoryTheory.Category.{w, u_1} A] →
      {FA : A → A → Type u_2} →
        {CA : A → Type w} →
          [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory A FA] →
              [CategoryTheory.Limits.HasColimits A] →
                [CategoryTheory.Limits.HasLimits A] →
                  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] →
                    [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)] →
                      [(CategoryTheory.forget A).ReflectsIsomorphisms] →
                        (X ⟶ Y) → CategoryTheory.Functor (TopCat.Sheaf A Y) (TopCat.Sheaf A X)
-- Std.Do.SPred.SPred
/-- Disjunction in `SPred`: states that either satisfy `P` or satisfy `Q` satisfy `spred(P ∨ Q)`.  -/
Std.Do.SPred.or : {σs : List (Type u)} → Std.Do.SPred σs → Std.Do.SPred σs → Std.Do.SPred σs
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.comap_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {g : γ → α} (hg : Measurable g), ProbabilityTheory.Kernel.comap 0 g hg = 0
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- `A[x]` is a fractional ideal for every integral `x`.  -/
FractionalIdeal.isFractional_adjoin_integral : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [IsLocalization S P] (x : P), IsIntegral R x → IsFractional S (Subalgebra.toSubmodule R[x])
-- Lean.Data.KVMap
/-- Update a `String` entry based on its current value.  -/
Lean.KVMap.updateString : Lean.KVMap → Lean.Name → (String → String) → Lean.KVMap
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.norm_eq_zero_iff_eq_zero : ∀ {K : Type u_1} [inst : Field K] {a b : K} [Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)] {z : QuadraticAlgebra K a b},
  QuadraticAlgebra.norm z = 0 ↔ z = 0
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.l_u_eq : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : PartialOrder β]
  (gi : GaloisInsertion l u) (b : β), l (u b) = b
-- Mathlib.Data.Set.Lattice
Set.iUnion_univ_pi : ∀ {α : Type u_1} {π : α → Type u_12} {ι : α → Type u_13} (t : (a : α) → ι a → Set (π a)),
  (⋃ x, Set.univ.pi fun a => t a (x a)) = Set.univ.pi fun a => ⋃ j, t a j
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.exists_ne_ne_of_three_le : ∀ {α : Type u_1}, 3 ≤ Cardinal.mk α → ∀ (x y : α), ∃ z, z ≠ x ∧ z ≠ y
-- Mathlib.GroupTheory.CosetCover
AddSubgroup.leftCoset_cover_const_iff_surjOn : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {s : Finset ι} {H : AddSubgroup G} {g : ι → G},
  ⋃ i ∈ s, g i +ᵥ ↑H = Set.univ ↔ Set.SurjOn (fun x => ↑(g x)) (↑s) Set.univ
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ioi_mul_Ici_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] (a b : α),
  Set.Ioi a * Set.Ici b ⊆ Set.Ioi (a * b)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.toPoly'.go.match_1.eq_3 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (a b : Int.Internal.Linear.Expr)
  (h_1 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_2 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_3 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_4 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b))
  (h_5 : (k : ℤ) → (a : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k a))
  (h_6 : (a : Int.Internal.Linear.Expr) → (k : ℤ) → motive (a.mulR k))
  (h_7 : (a : Int.Internal.Linear.Expr) → motive a.neg),
  (match a.add b with
    | Int.Internal.Linear.Expr.num k => h_1 k
    | Int.Internal.Linear.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Int.Internal.Linear.Expr.mulL k a => h_5 k a
    | a.mulR k => h_6 a k
    | a.neg => h_7 a) =
    h_3 a b
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteIncidenceSet_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {x v₁ v₂ : V}, (G.deleteIncidenceSet x).Adj v₁ v₂ ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x
-- Mathlib.Combinatorics.Matroid.Rank.Finite
/-- An `IsRkFinite` set has a finite basis'  -/
Matroid.IsRkFinite.exists_finite_isBasis' : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.IsRkFinite X → ∃ I, M.IsBasis' I X ∧ I.Finite
-- Lean.DocString.Markdown
/-- Render the `i` and its contents to Markdown lines, given a recursive renderer
for ordinary inline content.
 -/
Lean.Doc.MarkdownInline.toMarkdown : {i : Type u} →
  [self : Lean.Doc.MarkdownInline i] →
    (Lean.Doc.Inline i → Lean.Doc.MarkdownM (Array String)) →
      i → Array (Lean.Doc.Inline i) → Lean.Doc.MarkdownM (Array String)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If `0 : X ⟶ Y` is a monomorphism, then `X ≅ 0`.  -/
CategoryTheory.Limits.isoZeroOfMonoZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → {X Y : C} → CategoryTheory.Mono 0 → (X ≅ 0)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.mk : (toGlueData : CategoryTheory.GlueData AlgebraicGeometry.Scheme) →
  (∀ (i j : toGlueData.J), AlgebraicGeometry.IsOpenImmersion (toGlueData.f i j)) → AlgebraicGeometry.Scheme.GlueData
-- Mathlib.Data.Set.Image
Set.preimage_singleton_false : ∀ {α : Type u_1} (p : α → Prop), p ⁻¹' {False} = {a | ¬p a}
-- Mathlib.Data.Matrix.Mul
Matrix.instMulOfFintypeOfAddCommMonoid : {n : Type u_3} → {α : Type v} → [Fintype n] → [Mul α] → [AddCommMonoid α] → Mul (Matrix n n α)
-- Mathlib.RingTheory.Ideal.Quotient.Defs
/-- **Quotient ring**: the quotient of a ring by a two-sided ideal is a ring.  -/
Ideal.Quotient.ring : {R : Type u} → [inst : Ring R] → (I : Ideal R) → [I.IsTwoSided] → Ring (R ⧸ I)
-- Mathlib.Lean.Expr.Basic
/-- Map binder names in a nested forall `(a₁ : α₁) → ... → (aₙ : αₙ) → _`  -/
Lean.Expr.mapForallBinderNames : Lean.Expr → (Lean.Name → Lean.Name) → Lean.Expr
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- **Alias** of `hasMFDerivWithinAt_sdiff_singleton`. -/
hasMFDerivWithinAt_diff_singleton : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)} (y : M), HasMFDerivAt[s \ {y}] f x f' ↔ HasMFDerivAt[s] f x f'
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.self_symm_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y), α ≪≫ α.symm = CategoryTheory.Iso.refl X
-- Aesop.RuleTac.ElabRuleTerm
Aesop.checkElabRuleTermForSimp : Lean.Term → Bool → Aesop.ElabM Unit
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Eta-expanded form of `MeasureTheory.StronglyMeasurable.pow` -/
MeasureTheory.StronglyMeasurable.fun_pow : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Monoid β]
  [ContinuousMul β], MeasureTheory.StronglyMeasurable f → ∀ (n : ℕ), MeasureTheory.StronglyMeasurable fun i => f i ^ n
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
MvPolynomial.scalarRTensorAlgEquiv.eq_1 : ∀ {R : Type u} {N : Type v} [inst : CommSemiring R] {σ : Type u_1} [inst_1 : CommSemiring N] [inst_2 : Algebra R N],
  MvPolynomial.scalarRTensorAlgEquiv = AddMonoidAlgebra.scalarTensorEquiv R N
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.commRingEquiv_single_single : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (m : M)
  (n : N) (r : R),
  MonoidAlgebra.commRingEquiv (MonoidAlgebra.single m (MonoidAlgebra.single n r)) =
    MonoidAlgebra.single n (MonoidAlgebra.single m r)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans F G) {a : B} {a' : C} (f : G.obj a ⟶ a')
  {Z : F.obj a ⟶ a'}
  (h :
    CategoryTheory.CategoryStruct.comp (η.app a)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (G.obj a)) f) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.id a)).hom f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.id a)) f).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapId a) f)) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (η.app a)) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom f)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv f)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (η.app a) (CategoryTheory.CategoryStruct.id (G.obj a)) f).hom h)))
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ext_iff : ∀ {numVarsSucc : ℕ} {x y : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula numVarsSucc},
  x = y ↔ x.clauses = y.clauses ∧ x.rupUnits = y.rupUnits ∧ x.ratUnits = y.ratUnits ∧ x.assignments = y.assignments
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_le_add_nnnorm_add : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖a‖₊ ≤ ‖a + b‖₊ + ‖b‖₊
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.star_mk : ∀ {d : ℤ} (x y : ℤ), star { re := x, im := y } = { re := x, im := -y }
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.SeparatingLeft.congr : ∀ {R : Type u_1} {M : Type u_5} {Mₗ₁ : Type u_9} {Mₗ₁' : Type u_10} {Mₗ₂ : Type u_11} {Mₗ₂' : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid Mₗ₁]
  [inst_4 : AddCommMonoid Mₗ₂] [inst_5 : AddCommMonoid Mₗ₁'] [inst_6 : AddCommMonoid Mₗ₂'] [inst_7 : Module R Mₗ₁]
  [inst_8 : Module R Mₗ₂] [inst_9 : Module R Mₗ₁'] [inst_10 : Module R Mₗ₂'] {B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M}
  (e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁') (e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'),
  B.SeparatingLeft → ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).SeparatingLeft
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_disjoint_iff : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {f : ι → M} {s : Set ι},
  Disjoint (Function.mulSupport f) s ↔ Set.EqOn f 1 s
-- Batteries.Recycling.RBTree.Basic
/-- `O(1)`. Construct a new empty tree.  -/
RBTree.RBSet.empty : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp
-- Mathlib.Algebra.Notation
PosPart.mk : {α : Type u_1} → (α → α) → PosPart α
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_map_nonneg_of_archimedean : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {S : Type u_3}
  [inst_3 : LinearOrder S] [inst_4 : CommRing S] [IsStrictOrderedRing S] [Archimedean S] (f : S →+*o R) (y : S),
  0 ≤ ArchimedeanClass.mk (f y)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.μ_naturalityᵣ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {m n n' : M}
  (g : n ⟶ n') (X : C) [inst_3 : F.LaxMonoidal],
  CategoryTheory.CategoryStruct.comp ((F.map g).app ((F.obj m).obj X))
      ((CategoryTheory.Functor.LaxMonoidal.μ F m n').app X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m n).app X)
      ((F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft m g)).app X)