mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.UniformSpace
/-- The inclusion of a uniform space into its completion.  -/
UniformSpaceCat.completionHom : (X : UniformSpaceCat) →
  X ⟶ (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat).obj (UniformSpaceCat.completionFunctor.obj X)
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.enumOrd_lt_enumOrd : ∀ {s : Set Ordinal.{u}}, ¬BddAbove s → ∀ {a b : Ordinal.{u}}, Ordinal.enumOrd s a < Ordinal.enumOrd s b ↔ a < b
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
rTensor.inverse_comp_rTensor : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g),
  rTensor.inverse Q hfg hg ∘ₗ LinearMap.rTensor Q g = (LinearMap.rTensor Q f).range.mkQ
-- Mathlib.Data.Sym.Sym2
Sym2.toRel_fromRel : ∀ {α : Type u_1} {r : α → α → Prop} (sym : Std.Symm r), Sym2.ToRel (Sym2.fromRel sym) = r
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.ForgetEnrichment.equiv_counitIso : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {D : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} D] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D],
  (CategoryTheory.ForgetEnrichment.equiv V).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.ForgetEnrichment.equivInverse V D).comp
                (CategoryTheory.ForgetEnrichment.equivFunctor V D)).obj
            X))
      ⋯
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ⊆ u → t ⊆ u → s ∪ t ⊆ u
-- Init.Data.List.Zip
List.zipWithAll_map : ∀ {γ : Type u_1} {δ : Type u_2} {α : Type u_1} {β : Type u_2} {μ : Type u_3} {f : Option γ → Option δ → μ} {g : α → γ}
  {h : β → δ} {l₁ : List α} {l₂ : List β},
  List.zipWithAll f (List.map g l₁) (List.map h l₂) = List.zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.IsMonHom.monoidHom.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (f f_1 : M ⟶ N) (e_f : f = f_1)
  [inst_4 : CategoryTheory.IsMonHom f] (X : C),
  CategoryTheory.IsMonHom.monoidHom f X = CategoryTheory.IsMonHom.monoidHom f_1 X
-- Init.Data.Array.Lemmas
Array.foldl_map_hom : ∀ {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {xs : Array α},
  (∀ (x y : α), f' (g x) (g y) = g (f x y)) → Array.foldl f' (g a) (Array.map g xs) = g (Array.foldl f a xs)
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.WeaklyQuasiFiniteAt.congr_simp : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (q q_1 : Ideal S)
  (e_q : q = q_1) [inst_3 : q.IsPrime], Algebra.WeaklyQuasiFiniteAt R q = Algebra.WeaklyQuasiFiniteAt R q_1
-- Mathlib.GroupTheory.Perm.Fin
/-- Permutations of `Fin (n + 1)` are equivalent to fixing a single
`Fin (n + 1)` and permuting the remaining with a `Perm (Fin n)`.
The fixed `Fin (n + 1)` is swapped with `0`.  -/
Equiv.Perm.decomposeFin : {n : ℕ} → Equiv.Perm (Fin n.succ) ≃ Fin n.succ × Equiv.Perm (Fin n)
-- Aesop.BuiltinRules.Intros
Aesop.BuiltinRules.intros : Aesop.RuleTac
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.mapFreeIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u)
  [inst_6 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)),
  (SheafOfModules.mapFreeIso F I η).hom = SheafOfModules.mapFree F I η.hom
-- Lean.Meta.LazyDiscrTree
/-- Module with constant that import failed on.  -/
Lean.Meta.LazyDiscrTree.ImportFailure.module : Lean.Meta.LazyDiscrTree.ImportFailure → Lean.Name
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.L2.eLpNorm_rpow_two_norm_lt_top : ∀ {α : Type u_1} {F : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
  (f : ↥(MeasureTheory.Lp F 2 μ)), MeasureTheory.eLpNorm (fun x => ‖↑↑f x‖ ^ 2) 1 μ < ⊤
-- Init.Data.BitVec.Basic
/-- Checks whether addition of `x` and `y` results in *unsigned* overflow.

SMT-LIB name: `bvuaddo`.
 -/
BitVec.uaddOverflow : {w : ℕ} → BitVec w → BitVec w → Bool
-- Std.Data.ByteSlice
/-- The underlying byte array.
 -/
ByteSlice.byteArray : ByteSlice → ByteArray
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.instInhabitedWithTerminal : {a : Type u_1} → Inhabited (CategoryTheory.WithTerminal a)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.range_fst : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S], (RingHom.fst R S).rangeS = ⊤
-- Mathlib.Control.Traversable.Instances
_private.Mathlib.Control.Traversable.Instances.0.Sum.traverse.match_1.eq_1 : ∀ {σ : Type u_1} {α : Type u_2} (motive : σ ⊕ α → Sort u_3) (x : σ) (h_1 : (x : σ) → motive (Sum.inl x))
  (h_2 : (x : α) → motive (Sum.inr x)),
  (match Sum.inl x with
    | Sum.inl x => h_1 x
    | Sum.inr x => h_2 x) =
    h_1 x
-- Init.Data.List.ToArray
List.push_toArray : ∀ {α : Type u_1} (l : List α) (a : α), l.toArray.push a = (l ++ [a]).toArray
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
returning `fallback` if no such key exists.
 -/
Std.ExtTreeMap.getKeyGTD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → α → α
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.isEmpty : ∀ {s : Substring.Raw}, s.Valid → (s.isEmpty = true ↔ s.toString = "")
-- Mathlib.Data.Finset.Sups
Finset.mem_infs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t : Finset α} {c : α},
  c ∈ s ⊼ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ b = c
-- Mathlib.Analysis.Convex.Basic
convex_iff_add_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E},
  Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
-- Mathlib.Analysis.Normed.Group.Basic
enorm_div_le : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a b : E}, ‖a / b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  (t.erase k).getD k fallback = fallback
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The type of morphisms in the category `Φ.RightResolution X₂`.  -/
CategoryTheory.LocalizerMorphism.RightResolution.Hom : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂} → Φ.RightResolution X₂ → Φ.RightResolution X₂ → Type v_1
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- A `w`-`0`-hypercover `E` is `w'`-small if there exists an indexing type `ι` in `Type w'` and a
restriction map `ι → E.I₀` such that the restriction of `E` to `ι` is still covering.

Note: This is weaker than `E.I₀` being `w'`-small. For example, every Zariski cover of
`X : Scheme.{u}` is `u`-small, because `X` itself suffices as indexing type.
 -/
CategoryTheory.Precoverage.ZeroHypercover.Small : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {J : CategoryTheory.Precoverage C} → {S : C} → J.ZeroHypercover S → Prop
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.id_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
  (CategoryTheory.Profunctor.id.obj X).map f = TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp f.unop g
-- Mathlib.Tactic.FieldSimp
/-- If the user provided a discharger, elaborate it. If not, we will use the `field_simp_discharge`
default discharger, which (among other things) includes a simp-run for the specified argument list,
so we elaborate those arguments.  -/
Mathlib.Tactic.FieldSimp.parseDischarger : Option (Lean.TSyntax `Lean.Parser.Tactic.discharger) →
  Option (Lean.TSyntax `Lean.Parser.Tactic.simpArgs) →
    Lean.Elab.Tactic.TacticM ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»))
-- Lean.Data.Options
Lean.getOptionDefaultValue : Lean.Name → IO Lean.DataValue
-- Mathlib.Data.ENat.Lattice
ENat.iSup_add_iSup_le : ∀ {ι : Sort u_2} {κ : Sort u_3} {f : ι → ℕ∞} {a : ℕ∞} [Nonempty ι] [Nonempty κ] {g : κ → ℕ∞},
  (∀ (i : ι) (j : κ), f i + g j ≤ a) → iSup f + iSup g ≤ a
-- Mathlib.Order.DirSupClosed
DirSupClosedOn.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (D : Set (Set α)) (s : Set α),
  DirSupClosedOn D s =
    ∀ ⦃d : Set α⦄, d ∈ D → d ⊆ s → d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
-- Lean.Elab.Tactic.Doc
Lean.Elab.Tactic.Doc.TacticDoc.mk.inj : ∀ {internalName : Lean.Name} {userName : String} {tags : Lean.NameSet} {docString : Option String}
  {extensionDocs : Array String} {internalName_1 : Lean.Name} {userName_1 : String} {tags_1 : Lean.NameSet}
  {docString_1 : Option String} {extensionDocs_1 : Array String},
  { internalName := internalName, userName := userName, tags := tags, docString := docString,
        extensionDocs := extensionDocs } =
      { internalName := internalName_1, userName := userName_1, tags := tags_1, docString := docString_1,
        extensionDocs := extensionDocs_1 } →
    internalName = internalName_1 ∧
      userName = userName_1 ∧ tags = tags_1 ∧ docString = docString_1 ∧ extensionDocs = extensionDocs_1
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.re : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : RCLike 𝕜] {f : α → 𝕜},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun x => RCLike.re (f x)) μ
-- Mathlib.Geometry.Euclidean.Triangle
/-- If `B` lies on the same ray from `P` as a point `X` strictly between `A` and `C`,
then `∠ A P B + ∠ B P C = ∠ A P C`.  -/
EuclideanGeometry.angle_add_angle_eq_of_sbtw_of_sameRay : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {a b c p x : P},
  Sbtw ℝ a x c →
    SameRay ℝ (x -ᵥ p) (b -ᵥ p) →
      b ≠ p → EuclideanGeometry.angle a p b + EuclideanGeometry.angle b p c = EuclideanGeometry.angle a p c
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.ShouldCanonResult.noConfusionType : Sort v✝ → Lean.Meta.Sym.Canon.ShouldCanonResult✝ → Lean.Meta.Sym.Canon.ShouldCanonResult✝ → Sort v✝
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.isClosedEmbedding_toContinuousMultilinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] [T2Space F],
  Topology.IsClosedEmbedding ContinuousAlternatingMap.toContinuousMultilinearMap
-- Mathlib.Data.List.Sort
List.SortedLT.sortedLE : ∀ {α : Type u_1} [inst : Preorder α] {l : List α}, l.SortedLT → l.SortedLE
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.pairing_smul_coroot_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j k : ι),
  P.reflectionPerm i = P.reflectionPerm j → P.pairing i k • P.coroot i = P.pairing j k • P.coroot j
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- A diagram `WalkingCospan ⥤ C` is isomorphic to some `PullbackCone.mk` after
composing with `diagramIsoCospan`.  -/
CategoryTheory.Limits.PullbackCone.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} →
      (t : CategoryTheory.Limits.Cone F) →
        (CategoryTheory.Limits.Cone.postcompose (CategoryTheory.Limits.diagramIsoCospan F).hom).obj t ≅
          CategoryTheory.Limits.PullbackCone.mk (t.π.app CategoryTheory.Limits.WalkingCospan.left)
            (t.π.app CategoryTheory.Limits.WalkingCospan.right) ⋯
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.hasLimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C)
  [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₁, max u₁ v₁} (CategoryTheory.Over X)],
  CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₁, max u₁ v₁} (CategoryTheory.MonoOver X)
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.oneLE.eq_1 : ∀ (H : Type u_1) [inst : CommGroup H] [inst_1 : PartialOrder H] [inst_2 : IsOrderedMonoid H],
  GroupCone.oneLE H = { toSubmonoid := Submonoid.oneLE H, eq_one_of_mem_of_inv_mem' := ⋯ }
-- Mathlib.NumberTheory.LSeries.RiemannZeta
analyticOn_riemannZeta : AnalyticOnNhd ℂ riemannZeta {1}ᶜ
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.induction_on₃ : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
  [inst_2 : UniformSpace γ]
  {p : UniformSpace.Completion α → UniformSpace.Completion β → UniformSpace.Completion γ → Prop}
  (a : UniformSpace.Completion α) (b : UniformSpace.Completion β) (c : UniformSpace.Completion γ),
  IsClosed {x | p x.1 x.2.1 x.2.2} → (∀ (a : α) (b : β) (c : γ), p ↑a ↑b ↑c) → p a b c
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.mk.sizeOf_spec : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} [inst_2 : SizeOf G] [inst_3 : SizeOf X] [inst_4 : SizeOf ιₚ] (index : ιₚ)
  (groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries),
  sizeOf { index := index, groupElts := groupElts } = 1 + sizeOf index + sizeOf groupElts
-- Mathlib.Dynamics.Ergodic.Ergodic
Ergodic.ae_empty_or_univ_of_preimage_ae_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ],
  Ergodic f μ → MeasureTheory.NullMeasurableSet s μ → f ⁻¹' s ≤ᵐ[μ] s → s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.support_neg : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddGroup R] {x : HahnSeries Γ R},
  (-x).support = x.support
-- Lean.Meta.Tactic.Clear
/-- Try to erase the given free variable from the goal `mvarId`. It is no-op if the free variable
cannot be erased due to forward dependencies.
 -/
Lean.MVarId.tryClear : Lean.MVarId → Lean.FVarId → Lean.MetaM Lean.MVarId
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.nat.inj : ∀ {val val_1 : ℕ}, Lean.Compiler.LCNF.LitValue.nat val = Lean.Compiler.LCNF.LitValue.nat val_1 → val = val_1
-- Mathlib.Logic.Unique
Unique.instInhabited : {α : Sort u_1} → [Unique α] → Inhabited α
-- Mathlib.Topology.UniformSpace.Ultra.Completion
CauchyFilter.isSymm_gen : ∀ {X : Type u_1} [inst : UniformSpace X] {s : SetRel X X} [s.IsSymm], (CauchyFilter.gen s).IsSymm
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
/-- The transition maps in the sequential limit of products  -/
CategoryTheory.Limits.SequentialProduct.functorMap : {C : Type u_1} →
  {M N : ℕ → C} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      ((n : ℕ) → M n ⟶ N n) →
        [inst_1 : CategoryTheory.Limits.HasCountableProducts C] →
          (n : ℕ) →
            CategoryTheory.Limits.SequentialProduct.functorObj M N (n + 1) ⟶
              CategoryTheory.Limits.SequentialProduct.functorObj M N n
-- Mathlib.Topology.UniformSpace.UniformEmbedding
isUniformInducing_val : ∀ {α : Type u_1} [inst : UniformSpace α] (s : Set α), IsUniformInducing Subtype.val
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The image of `𝒱 i j₁ ×[𝒰 i] 𝒱 i j₂` in `diagonalCover` with `j₁ = j₂`  -/
AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (𝒰 : Y.OpenCover) →
      ((i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
          ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover) →
        (CategoryTheory.Limits.pullback.diagonalObj f).Opens
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.measurable_countableFiltration_densityProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (n : ℕ) (a : α) {s : Set β},
  MeasurableSet s → Measurable fun x => κ.densityProcess ν n a x s
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgHom.mem_range : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (φ : F) {y : B}, y ∈ NonUnitalAlgHom.range φ ↔ ∃ x, φ x = y
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight_swap : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x y : K),
  Height.logHeight ![x, y] = Height.logHeight ![y, x]
-- Mathlib.Topology.Algebra.Group.Basic
continuousAt_neg_iff : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G]
  [inst_3 : TopologicalSpace α] {f : α → G} {x : α}, ContinuousAt (-f) x ↔ ContinuousAt f x
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_toAddMonoidHom : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (f : α →ₙ+* β), ⇑f.toAddMonoidHom = ⇑f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.equation_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R) {u : R},
  IsUnit u → (W'.Equation (u • P) ↔ W'.Equation P)
-- Mathlib.Data.Multiset.MapFold
Multiset.erase_attach_map_val : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (x : { x // x ∈ s }),
  Multiset.map Subtype.val (s.attach.erase x) = s.erase ↑x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β},
      (t.insert k v).maxKey? = some (t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k')
-- Mathlib.Topology.ClusterPt
MapClusterPt.frequently : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X},
  MapClusterPt x F u → ∀ {p : X → Prop}, (∀ᶠ (y : X) in nhds x, p y) → ∃ᶠ (a : α) in F, p (u a)
-- Mathlib.RingTheory.Localization.Finiteness
Module.Finite.of_isLocalization : ∀ (R : Type u_3) (S : Type u_4) {Rₚ : Type u_1} {Sₚ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring Rₚ] [inst_3 : CommSemiring Sₚ] [inst_4 : Algebra R S] [inst_5 : Algebra R Rₚ]
  [inst_6 : Algebra R Sₚ] [inst_7 : Algebra S Sₚ] [inst_8 : Algebra Rₚ Sₚ] [IsScalarTower R S Sₚ]
  [IsScalarTower R Rₚ Sₚ] (M : Submonoid R) [IsLocalization M Rₚ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ]
  [hRS : Module.Finite R S], Module.Finite Rₚ Sₚ
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Mapping from variables to their denotations.
Remark each variable can be in only one ring.
 -/
Lean.Meta.Grind.Arith.CommRing.Semiring.vars : Lean.Meta.Grind.Arith.CommRing.Semiring → Lean.PArray Lean.Expr
-- Mathlib.LinearAlgebra.LinearPMap
/-- The unique `LinearPMap` on `R ∙ x` that sends `x` to `y`. This version works for modules
over rings, and requires a proof of `∀ c, c • x = 0 → c • y = 0`.  -/
LinearPMap.mkSpanSingleton' : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module S F] → (x : E) → (y : F) → (∀ (c : R), c • x = 0 → σ c • y = 0) → E →ₛₗ.[σ] F
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.sum_sin : ∀ (n : ℕ) {a : ℂ},
  (∀ (k : ℤ), a ≠ ↑k * (2 * ↑Real.pi)) →
    ∀ (b : ℂ),
      ∑ i ∈ Finset.range n, Complex.sin (a * ↑i + b) =
        Complex.sin (↑n * a / 2) * Complex.sin ((↑n - 1) * a / 2 + b) / Complex.sin (a / 2)
-- Lean.Meta.Tactic.Grind.Arith.Util
_private.Lean.Meta.Tactic.Grind.Arith.Util.0.Lean.Meta.Grind.Arith.resize.go : ℕ → Lean.PArray ℚ → Lean.PArray ℚ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiff.csin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {n : WithTop ℕ∞},
  ContDiff ℂ n f → ContDiff ℂ n fun x => Complex.sin (f x)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Braided
/-- If a braided category is left-rigid, then it is right-rigid.
Not registered as an instance as this is not canonical enough.  -/
CategoryTheory.BraidedCategory.rightRigidCategoryOfLeftRigidCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → [CategoryTheory.LeftRigidCategory C] → CategoryTheory.RightRigidCategory C
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.mkIntCast : ℤ → Lean.Meta.Grind.Arith.FieldNormNum.M✝ Lean.Expr
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- The fiber of the terminal object is a terminal object in `Type w`.  -/
CategoryTheory.GrothendieckTopology.Point.isTerminalFiberObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        [CategoryTheory.LocallySmall.{w, v, u} C] →
          (T : C) → CategoryTheory.Limits.IsTerminal T → CategoryTheory.Limits.IsTerminal (Φ.fiber.obj T)
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.isPositive_iff_complex : ∀ {E' : Type u_4} [inst : NormedAddCommGroup E'] [inst_1 : InnerProductSpace ℂ E'] (T : E' →ₗ[ℂ] E'),
  T.IsPositive ↔ ∀ (x : E'), ↑(RCLike.re (inner ℂ (T x) x)) = inner ℂ (T x) x ∧ 0 ≤ RCLike.re (inner ℂ (T x) x)
-- Init.Data.UInt.Lemmas
USize.toUInt32_ofNat' : ∀ (n : ℕ), (USize.ofNat n).toUInt32 = UInt32.ofNat n
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_range_right : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {f : Quotient (QuotientGroup.rightRel H) → G},
  (∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q) → Subgroup.IsComplement (↑H) (Set.range f)
-- Mathlib.Algebra.MvPolynomial.Derivation
MvPolynomial.derivation_C : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] (D : Derivation R (MvPolynomial σ R) A) (a : R), D (MvPolynomial.C a) = 0
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Subgraph.IsInduced.isIndContained : ∀ {V : Type u_1} {G : SimpleGraph V} {G' : G.Subgraph}, G'.IsInduced → G'.coe.IsIndContained G