mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_insertEntry_le_minKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {k : α} {v : β k} {fallback : α},
        (compare (Std.Internal.List.minKeyD (Std.Internal.List.insertEntry k v l) fallback)
              (Std.Internal.List.minKeyD l fallback)).isLE =
          true
-- Lean.Elab.Calc
Lean.Elab.Term.instInhabitedCalcStepView : Inhabited Lean.Elab.Term.CalcStepView
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit'.match_3.eq_2 : ∀ (motive : Lean.Expr → Sort u_1) (f x : Lean.Expr)
  (h_1 : (name : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const name us))
  (h_2 : (f x : Lean.Expr) → motive (f.app x))
  (h_3 :
    (binderName : Lean.Name) →
      (ty body : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName ty body binderInfo))
  (h_4 : Unit → motive (Lean.Expr.sort Lean.Level.zero)) (h_5 : (a : Lean.Level) → motive (Lean.Expr.sort a.succ))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (x : Lean.Expr) → motive x),
  (match f.app x with
    | Lean.Expr.const name us => h_1 name us
    | f.app x => h_2 f x
    | Lean.Expr.forallE binderName ty body binderInfo => h_3 binderName ty body binderInfo
    | Lean.Expr.sort Lean.Level.zero => h_4 ()
    | Lean.Expr.sort a.succ => h_5 a
    | Lean.Expr.sort u => h_6 u
    | x => h_7 x) =
    h_2 f x
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is the version for Banach spaces, see `charFun_eq_pi_iff`
for the Hilbert space version.  -/
MeasureTheory.charFunDual_eq_pi_iff : ∀ {ι : Type u_4} [inst : Fintype ι] [inst_1 : DecidableEq ι] {E : ι → Type u_5}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace ℝ (E i)]
  {mE : (i : ι) → MeasurableSpace (E i)} [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)]
  [∀ (i : ι), CompleteSpace (E i)] {μ : (i : ι) → MeasureTheory.Measure (E i)}
  {ν : MeasureTheory.Measure ((i : ι) → E i)} [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (L : StrongDual ℝ ((i : ι) → E i)),
      MeasureTheory.charFunDual ν L = ∏ i, MeasureTheory.charFunDual (μ i) (L ∘SL ContinuousLinearMap.single ℝ E i)) ↔
    ν = MeasureTheory.Measure.pi μ
-- Mathlib.Data.Set.Finite.Basic
/-- **Alias** of `Set.Finite.of_sdiff`. -/
Set.Finite.of_diff : ∀ {α : Type u} {s t : Set α}, (s \ t).Finite → t.Finite → s.Finite
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.opEquiv_inverse_obj_left_op : ∀ (C : Type u₁) {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (d : D),
  (CategoryTheory.Join.opEquiv C D).inverse.obj (CategoryTheory.Join.left (Opposite.op d)) =
    Opposite.op (CategoryTheory.Join.right d)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (a : X.I),
  X.coproductIsoSelf.inv.f a =
    (CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt X.I X.toFun).inv.f (X.cofanPtIsoSelf.inv.f a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Inhabited α] {k : α} {f : Option β → Option β} {hc : k ∈ Std.DTreeMap.Const.alter t k f},
  (Std.DTreeMap.Const.alter t k f).getKey k hc = k
-- Mathlib.NumberTheory.Modular
ModularGroup.abs_two_mul_re_lt_one_of_mem_fdo : ∀ {z : UpperHalfPlane}, z ∈ ModularGroup.fdo → |2 * z.re| < 1
-- Mathlib.Probability.Process.Filtration
/-- If `i` is not isolated on the right, then `𝓕₊ i = ⨅ j > i, 𝓕 j`. This is for instance the case
when `ι` is a densely ordered linear order with no maximal elements and equipped with the order
topology, see `rightCont_eq`.  -/
MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : PartialOrder ι] [inst_1 : TopologicalSpace ι]
  [OrderTopology ι] (𝓕 : MeasureTheory.Filtration ι m) (i : ι) [(nhdsWithin i (Set.Ioi i)).NeBot],
  ↑𝓕.rightCont i = ⨅ j, ⨅ (_ : j > i), ↑𝓕 j
-- Mathlib.RepresentationTheory.FDRep
FDRep.instHasKernels : ∀ {k : Type u} {G : Type v} [inst : Field k] [inst_1 : Monoid G], CategoryTheory.Limits.HasKernels (FDRep k G)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDerivWithin_congr_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {s t : Set E} {x v : E}, s =ᶠ[nhds x] t → lineDerivWithin 𝕜 f s x v = lineDerivWithin 𝕜 f t x v
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.State.mk.sizeOf_spec : ∀ (numSteps : ℕ) (persistentCache transientCache : Lean.Meta.Sym.Simp.Cache)
  (funext : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Expr),
  sizeOf
      { numSteps := numSteps, persistentCache := persistentCache, transientCache := transientCache, funext := funext } =
    1 + sizeOf numSteps + sizeOf persistentCache + sizeOf transientCache + sizeOf funext
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.neg_of : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Neg α] (f : m → n → α), -Matrix.of f = Matrix.of (-f)
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroupClass.normedAddGroup.eq_1 : ∀ {E : Type u_1} [inst : NormedAddGroup E] {S : Type u_2} [inst_1 : SetLike S E] [inst_2 : AddSubgroupClass S E]
  (s : S),
  AddSubgroupClass.normedAddGroup s =
    { toNorm := (AddSubgroupClass.seminormedAddGroup s).toNorm, toAddGroup := AddSubgroupClass.toAddGroup s,
      toMetricSpace := Subtype.metricSpace, dist_eq := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {A : C},
  CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans (CategoryTheory.Functor.id C) A =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.MonoidalCategory.curriedTensor C).obj A).comp (CategoryTheory.Functor.id C))
-- Mathlib.Algebra.Star.StarRingHom
/-- Turn an element of a type `F` satisfying `StarRingEquivClass F A B` into an actual
`StarRingEquiv`. This is declared as the default coercion from `F` to `A ≃⋆+* B`.  -/
StarRingEquivClass.toStarRingEquiv : {F : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : Add A] →
        [inst_1 : Mul A] →
          [inst_2 : Star A] →
            [inst_3 : Add B] →
              [inst_4 : Mul B] →
                [inst_5 : Star B] → [inst_6 : EquivLike F A B] → [StarRingEquivClass F A B] → F → A ≃⋆+* B
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.freeGroupEmptyEquivUnit.eq_1 : FreeGroup.freeGroupEmptyEquivUnit = Equiv.ofUnique (FreeGroup Empty) Unit
-- Mathlib.Analysis.Real.Cardinality
Cardinal.cantorFunctionAux_zero : ∀ {c : ℝ} (f : ℕ → Bool), Cardinal.cantorFunctionAux c f 0 = bif f 0 then 1 else 0
-- Init.Data.Array.MinMax
Array.foldl_min : ∀ {α : Type u_1} [inst : Min α] [Std.IdempotentOp min] [Std.Associative min] {xs : Array α} {a : α},
  Array.foldl min a xs = a ⊓ xs.min?.getD a
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Suppose an indexed family of points is given, along with a subset
of the index type.  A vector can be expressed as `weightedVSub` using
a `Finset` lying within that subset and with sum of weights 0 if and
only if it can be expressed as `weightedVSub` with sum of weights 0
for the corresponding indexed family whose index type is the subtype
corresponding to that subset.  -/
Finset.eq_weightedVSub_subset_iff_eq_weightedVSub_subtype : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} {v : V} {s : Set ι} {p : ι → P},
  (∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 0 ∧ v = (fs.weightedVSub p) w) ↔
    ∃ fs w, ∑ i ∈ fs, w i = 0 ∧ v = (fs.weightedVSub fun i => p ↑i) w
-- Mathlib.RingTheory.Coalgebra.TensorProduct
Coalgebra.TensorProduct.rid_toLinearEquiv : ∀ {R : Type u_5} {S : Type u_6} {M : Type u_7} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  [inst_7 : Coalgebra S M],
  (Coalgebra.TensorProduct.rid R S M).toLinearEquiv = TensorProduct.AlgebraTensorModule.rid R S M
-- Mathlib.Algebra.Order.Module.Defs
PosSMulReflectLT.toPosSMulReflectLE : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : AddCommGroup β] [inst_2 : Module α β] [IsDomain α]
  [Module.IsTorsionFree α β] [inst_5 : Preorder α] [inst_6 : PartialOrder β] [PosSMulReflectLT α β],
  PosSMulReflectLE α β
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
Std.Tactic.BVDecide.Return.cache : {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
  (self : Std.Tactic.BVDecide.Return aig) → Std.Tactic.BVDecide.BVExpr.Cache (↑self.result).aig
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- The data of generating sections of the restriction of a sheaf of modules
over a covering of the terminal object.  -/
SheafOfModules.LocalGeneratorsData : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        SheafOfModules R →
          [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
            [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] → Type (max (max (max (u + 1) u') v') (w + 1))
-- Init.Data.Vector.Lemmas
Vector.getElem?_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} {size : xs.size = n} {i : ℕ}, (Vector.mk xs size)[i]? = xs[i]?
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.toRatCDF_unit_prod : ∀ {α : Type u_1} {f : α → ℚ → ℝ} (a : α),
  ProbabilityTheory.toRatCDF (fun p => f p.2) ((), a) = ProbabilityTheory.toRatCDF f a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for the unsigned modulo operation on `BitVec`s.  -/
BitVec.reduceUMod : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- If `P₁ : Cᵒᵖ ⥤ Type w` and `P₂  : Cᵒᵖ ⥤ Type w` are two naturally equivalent
presheaves, and `P₁` is a sheaf for a presieve `R`, then `P₂` is also a sheaf for `R`.  -/
CategoryTheory.Presieve.isSheafFor_of_nat_equiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P₁ : CategoryTheory.Functor Cᵒᵖ (Type w)}
  {P₂ : CategoryTheory.Functor Cᵒᵖ (Type w')} (e : ⦃X : C⦄ → P₁.obj (Opposite.op X) ≃ P₂.obj (Opposite.op X)),
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (Opposite.op Y)),
      e ((CategoryTheory.ConcreteCategory.hom (P₁.map f.op)) x) =
        (CategoryTheory.ConcreteCategory.hom (P₂.map f.op)) (e x)) →
    ∀ {X : C} {R : CategoryTheory.Presieve X},
      CategoryTheory.Presieve.IsSheafFor P₁ R → CategoryTheory.Presieve.IsSheafFor P₂ R
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Scalar multiples of harmonic functions are harmonic.
 -/
InnerProductSpace.HarmonicAt.const_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {x : E} {c : ℝ},
  InnerProductSpace.HarmonicAt f x → InnerProductSpace.HarmonicAt (c • f) x
-- Init.System.IO
/-- `IO` specialization of `EIO.mapTasks`.  -/
IO.mapTasks : {α : Type u_1} →
  {β : Type} →
    (List α → IO β) →
      List (Task α) →
        optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO (Task (Except IO.Error β))
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.lift_injective_iff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)),
  Function.Injective ⇑(f.lift hg) ↔ ∀ (x y : M), f x = f y ↔ g x = g y
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.Γ_obj_op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : AlgebraicGeometry.SheafedSpace C),
  AlgebraicGeometry.SheafedSpace.Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op ⊤)
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
/-- A simplicial complex in a `𝕜`-module is a collection of simplices which glue nicely together.
Note that the textbook meaning of "glue nicely" is given in
`Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull`. It is mostly useless, as
`Geometry.SimplicialComplex.convexHull_inter_convexHull` is enough for all purposes.  -/
Geometry.SimplicialComplex : (𝕜 : Type u_1) →
  (E : Type u_2) → [inst : Ring 𝕜] → [PartialOrder 𝕜] → [inst_2 : AddCommGroup E] → [Module 𝕜 E] → Type u_2
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The presentation of `S` over `R` obtained from composing the naive presentation of
`T = R[X₁, ..., Xₙ]/(b₁, ..., bᵣ)` with the presentation of the localization away from `g`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.pres : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b →
                    Algebra.Presentation R S (Unit ⊕ ι) (Unit ⊕ σ)
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ord_neg : ∀ {R : Type u_1} [inst : CommRing R] (x : R), Ring.ord R (-x) = Ring.ord R x
-- Std.Tactic.Do.ProofMode
/-- This is only used for delaboration purposes, so that we can render context variables that appear
to have type `A : PROP` even though `PROP` is not a type.  -/
Std.Tactic.Do.MGoalHypMarker : {σs : List (Type u)} → Std.Do.SPred σs → Prop
-- Mathlib.Algebra.CharZero.Defs
OfNat.zero_ne_ofNat : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ) [inst_2 : n.AtLeastTwo], 0 ≠ OfNat.ofNat n
-- Mathlib.Data.Finsupp.Basic
Finsupp.sigmaFinsuppEquivPiFinsupp_apply : ∀ {α : Type u_1} {η : Type u_13} [inst : Fintype η] {ιs : η → Type u_14} [inst_1 : Zero α] (f : (j : η) × ιs j →₀ α)
  (j : η) (i : ιs j), (Finsupp.sigmaFinsuppEquivPiFinsupp f j) i = f ⟨j, i⟩
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- A variant of `of_isLimit` that is more useful with `apply`.  -/
CategoryTheory.IsPullback.of_isLimit' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (w : CategoryTheory.CommSq fst snd f g) (h : CategoryTheory.Limits.IsLimit w.cone),
  CategoryTheory.IsPullback fst snd f g
-- Init.Data.List.MinMaxOn
List.max?_eq_min? : ∀ {α : Type u_1} {max : Max α} {xs : List α}, xs.max? = xs.min?
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_union!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β k},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.union! m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The isomorphism between `W` and the Coxeter group associated to `M`.  -/
CoxeterSystem.mulEquiv : {B : Type u_1} → {M : CoxeterMatrix B} → {W : Type u_2} → [inst : Group W] → CoxeterSystem M W → W ≃* M.Group
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
/-- A family of `indicatorConstLp` functions tends to an `indicatorConstLp`,
if the underlying sets tend to the set in the sense of the measure of the symmetric difference.  -/
MeasureTheory.tendsto_indicatorConstLp_set : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} [hp₁ : Fact (1 ≤ p)]
  {β : Type u_3} {l : Filter β} {t : β → Set α} {ht : ∀ (b : β), MeasurableSet (t b)} {hμt : ∀ (b : β), μ (t b) ≠ ⊤},
  p ≠ ⊤ →
    Filter.Tendsto (fun b => μ (symmDiff (t b) s)) l (nhds 0) →
      Filter.Tendsto (fun b => MeasureTheory.indicatorConstLp p ⋯ ⋯ c) l
        (nhds (MeasureTheory.indicatorConstLp p hs hμs c))
-- Mathlib.Algebra.Group.Finsupp
Finsupp.erase_sub : ∀ {ι : Type u_1} {G : Type u_6} [inst : AddGroup G] (a : ι) (f₁ f₂ : ι →₀ G),
  Finsupp.erase a (f₁ - f₂) = Finsupp.erase a f₁ - Finsupp.erase a f₂
-- Mathlib.Data.List.Basic
/-- The images of disjoint lists under an injective map are disjoint  -/
List.disjoint_map : ∀ {α : Type u} {β : Type v} {f : α → β} {s t : List α},
  Function.Injective f → s.Disjoint t → (List.map f s).Disjoint (List.map f t)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.isOpenImmersion_glueDataObjMap : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {V : ↑X.affineOpens} (f : ↑(X.presheaf.obj (Opposite.op ↑V))),
  AlgebraicGeometry.IsOpenImmersion (I.glueDataObjMap ⋯)
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.eball_subset_eball`. -/
EMetric.ball_subset_ball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε₁ ε₂ : ENNReal}, ε₁ ≤ ε₂ → Metric.eball x ε₁ ⊆ Metric.eball x ε₂
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.ext_iff₂ : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}, f = g ↔ ∀ (m : M) (n : N), (f m) n = (g m) n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ofList_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {k : α} {v : β},
  Std.ExtDTreeMap.Const.ofList [(k, v)] cmp = ∅.insert k v
-- Std.Data.DTreeMap.Internal.Balancing
/-- A single right rotation.  -/
Std.DTreeMap.Internal.Impl.singleR : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        (lk : α) →
          β lk →
            Std.DTreeMap.Internal.Impl α β →
              Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.ofAlgEquiv_algEquiv : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : Ring T] [inst_4 : Algebra R T] {U : Type u_2} [inst_5 : Ring U]
  [inst_6 : Algebra R U] (h'' : IsAdjoinRoot U f) (e : S ≃ₐ[R] T),
  (h.ofAlgEquiv e).algEquiv h'' = e.symm.trans (h.algEquiv h'')
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.ext : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {s t : MeasureTheory.VectorMeasure α M}, (∀ (i : Set α), MeasurableSet i → s i = t i) → s = t
-- Lean.Meta.Tactic.Grind.AC.Util
/-- Returns `true` if `op` is an arithmetic operator supported in other modules.
Remark: `f == op.getAppFn!`
 -/
_private.Lean.Meta.Tactic.Grind.AC.Util.0.Lean.Meta.Grind.AC.isArithOpInOtherModules : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lt_aleph0_iff_subtype_finite : ∀ {α : Type u} {p : α → Prop}, Cardinal.mk { x // p x } < Cardinal.aleph0 ↔ {x | p x}.Finite
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform.0.EisensteinSeries.δ_eq : EisensteinSeries.δ✝ ![0, 0] = 1
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.kind : Lean.SyntaxNodeKind → Lean.Parser.ParserExtension.Entry
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Arithmetic progressions are preserved under 2-Freiman isos.  -/
IsMulFreimanIso.mulRothNumber_congr : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : CommMonoid α] [inst_2 : CommMonoid β]
  [inst_3 : DecidableEq β] {A : Finset α} {B : Finset β} {f : α → β},
  IsMulFreimanIso 2 (↑A) (↑B) f → mulRothNumber A = mulRothNumber B
-- Std.Time.Format.DateFormat
/-- `DateFormatSymbols` contains locale-specific strings needed for date/time formatting and parsing.
 -/
Std.Time.DateFormatSymbols : Type
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalIntExpr : Lean.Expr → Lean.MetaM ℤ
-- Mathlib.Analysis.Calculus.ContDiff.WithLp
contDiff_piLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [inst_5 : Fintype ι] (p : ENNReal) [inst_6 : Fact (1 ≤ p)] {n : WithTop ℕ∞}
  {f : H → PiLp p E}, ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => (f x).ofLp i
-- Mathlib.Analysis.Fourier.LpSpace
MeasureTheory.Lp.instFourierAdd : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E],
  FourierAdd ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs.0.BirdDet.sumFrom.eq_def : ∀ {R : Type u_1} [inst : CommRing R] (n lo : ℕ) (f : ℕ → R),
  BirdDet.sumFrom n lo f = if lo < n then f lo + BirdDet.sumFrom n (lo + 1) f else 0
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.dfinsuppFamily_apply_support' : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : Semiring R]
  [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)]
  [inst_5 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_6 : (p : (i : ι) → κ i) → Module R (N p)]
  (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)) (x : (i : ι) → Π₀ (j : κ i), M i j),
  ((MultilinearMap.dfinsuppFamily f) x).support' =
    Trunc.map (fun s => ⟨Multiset.map (fun f i => f i ⋯) (Finset.univ.val.pi fun i => ↑(s i)), ⋯⟩)
      (Trunc.finChoice fun i => (x i).support')
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_union_of_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∈ m₁ → k ∈ m₁ ∪ m₂
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.map_fun_eq_pi_map : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : Fintype ι]
  {β : ι → Type u_11} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  (∀ (i : ι), AEMeasurable (f i) μ) →
    ProbabilityTheory.iIndepFun f μ →
      MeasureTheory.Measure.map (fun ω i => f i ω) μ =
        MeasureTheory.Measure.pi fun i => MeasureTheory.Measure.map (f i) μ
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.val_mkOfAddEqZero : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : IsDedekindFiniteAddMonoid α] {a b : α} (h : a + b = 0),
  ↑(AddUnits.mkOfAddEqZero a b h) = a
-- Std.Net.Addr
Std.Net.AddressFamily.ofNat : ℕ → Std.Net.AddressFamily
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Free.killCopies_eq_left : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}, H.Free G → G.killCopies H = G