mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Field.WithAbs
WithAbs.instFiniteDimensional_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Field R] {T : Type u_3}
  [inst_3 : Field T] (v : AbsoluteValue R S) [inst_4 : Module T R] [FiniteDimensional T R],
  FiniteDimensional T (WithAbs v)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H1CoresCoinfOfTrivial_X₃ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal]
  [inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)],
  (groupHomology.H1CoresCoinfOfTrivial A S).X₃ = groupHomology.H1 (A.ofQuotient S)
-- Lean.Server.References
/-- Module name of the reference.  -/
Lean.Server.References.DocumentRefInfo.module : Lean.Server.References.DocumentRefInfo → Lean.Name
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_inverse_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma S' (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).inverse.obj X).hom =
    CategoryTheory.CategoryStruct.comp (i.hom.app X.left) X.hom
-- Mathlib.Topology.ContinuousOn
/-- **Alias** of the forward direction of `continuousOn_iff_continuous_domRestrict`. -/
ContinuousOn.domRestrict : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s → Continuous (s.domRestrict f)
-- Mathlib.Analysis.Normed.Module.Convex
/-- The set of nonzero vectors in the same ray as the nonzero vector `x` is connected.  -/
isConnected_setOfPred_sameRay_and_ne_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x : E},
  x ≠ 0 → IsConnected {y | SameRay ℝ x y ∧ y ≠ 0}
-- Lean.Meta.LazyDiscrTree
/-- Information about a failed import.  -/
Lean.Meta.LazyDiscrTree.ImportFailure : Type
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.normNatTrans_app : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : Group G] [inst_2 : Fintype G] (A : Rep.{u_1, u, v} k G),
  Rep.normNatTrans.app A = A.norm
-- Mathlib.Tactic.Linarith.Preprocessing
/-- `getNatComparisons e` returns a list of all subexpressions of `e` of the form `((t : ℕ) : C)`.
 -/
Mathlib.Tactic.Linarith.getNatComparisons : Lean.Expr → List (Lean.Expr × Lean.Expr)
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.continuous_aeval : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace A] [IsTopologicalSemiring A] (p : Polynomial R), Continuous fun x => (Polynomial.aeval x) p
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- `val_v(∏_{w ≠ v} w^{exps w}) = 0`.  -/
FractionalIdeal.count_finprod_coprime : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  (exps : IsDedekindDomain.HeightOneSpectrum R → ℤ),
  FractionalIdeal.count K v (∏ᶠ (w : IsDedekindDomain.HeightOneSpectrum R) (_ : w ≠ v), ↑w.asIdeal ^ exps w) = 0
-- Init.Classical
Classical.or_iff_not_imp_left : ∀ {a b : Prop}, a ∨ b ↔ ¬a → b
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_self_rpow_inv : ∀ {y : ℝ}, y ≠ 0 → ∀ (x : NNReal), (x ^ (1 / y)) ^ y = x
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.iInf_ker_weight_eq_bot : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L], ⨅ α, LieModule.Weight.ker = ⊥
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.toNat.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (a : ℕ) → motive (Int.negSucc a)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc a => h_2 a) =
    h_1 n
-- Init.Data.Float.Model.Unpacked.Operations.OfNat
/-- Converts a `UInt8` to an `UnpackedFloat`, returning positive zero on zero.  -/
Float.Model.UnpackedFloat.ofUInt8 : Float.Model.Format → UInt8 → Float.Model.UnpackedFloat
-- Lean.DocString.Markdown
_private.Lean.DocString.Markdown.0.Lean.Doc.MarkdownM.State.mk.inj : ∀ {footnotes footnotes_1 : Array (String × String)},
  { footnotes := footnotes } = { footnotes := footnotes_1 } → footnotes = footnotes_1
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.lift_embed_apply : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {I : Ideal A} (hI : DividedPowers I) {g : M →ₗ[R] A}
  (hg : ∀ (m : M), g m ∈ I) (m : M), (DividedPowerAlgebra.lift hI g hg) ((DividedPowerAlgebra.embed R M) m) = g m
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kronecker_assoc : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} {q : Type u_13} {r : Type u_14}
  [inst : Semigroup α] (A : Matrix l m α) (B : Matrix n p α) (C : Matrix q r α),
  (Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r))
      (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B) C) =
    Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) B C)
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_ofBitVec : ∀ (n : BitVec System.Platform.numBits) (h : System.Platform.numBits = 32),
  (ISize.ofBitVec n).toBitVec32 h = BitVec.cast h n
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ico_add_one_add_one_eq_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] [NoMaxOrder α] (a b : α),
  Set.Ico (a + 1) (b + 1) = Set.Ioc a b
-- Mathlib.Data.List.MinMax
List.maximum_mono : ∀ {α : Type u_1} [inst : LinearOrder α] {l₁ l₂ : List α}, l₁ ⊆ l₂ → l₁.maximum ≤ l₂.maximum
-- Mathlib.Data.FunLike.Equiv
/-- The coercion to a function in the forward direction.  -/
EquivLike.coe : {E : Sort u_1} → {α : outParam (Sort u_2)} → {β : outParam (Sort u_3)} → [self : EquivLike E α β] → E → α → β
-- Mathlib.LinearAlgebra.TensorProduct.Pi
/-- For any `R`-module `N` and index type `ι`, there is a natural
linear map `N ⊗[R] (ι → R) →ₗ (ι → N)`. This map is an isomorphism if `ι` is finite.  -/
TensorProduct.piScalarRightHom : (R : Type u_1) →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (N : Type u_3) →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                [inst_5 : Module S N] →
                  [inst_6 : IsScalarTower R S N] → (ι : Type u_4) → TensorProduct R N (ι → R) →ₗ[S] ι → N
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)),
  (F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((F.mapId b).hom.toNatTrans.app ((F.map f).toFunctor.obj X))
      ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv).toNatTrans.app X)
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.op_apply_symm_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A ≃ₐ[R] B) (a : Bᵐᵒᵖ),
  (AlgEquiv.op f).symm a = MulOpposite.op (f.symm (MulOpposite.unop a))
-- Std.Async.Basic
/-- Lifts an `EAsync` computation into an `ETask` that can be awaited and joined.
 -/
Std.Async.EAsync.asTask : {ε α : Type} → Std.Async.EAsync ε α → optParam Task.Priority Task.Priority.default → EIO ε (Std.Async.ETask ε α)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∉ t₂ → (t₁ ∪ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.Algebra.WithConv
WithConv.instCoeFunForall : {A : Type u_2} → {B : Type u_3} → {C : Type u_4} → [CoeFun A fun x => B → C] → CoeFun (WithConv A) fun x => B → C
-- Lean.Util.PtrSet
Lean.PtrMap.insert : {α β : Type} → Lean.PtrMap α β → α → β → Lean.PtrMap α β
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.getDₘ_eq_getValueD : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {fallback : β},
      Std.DHashMap.Internal.Raw₀.Const.getDₘ m a fallback =
        Std.Internal.List.getValueD a (Std.DHashMap.Internal.toListModel (↑m).buckets) fallback
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement'.card_mul_card : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsComplement' K → Nat.card ↥H * Nat.card ↥K = Nat.card G
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedSymbolKind : Inhabited Lean.Lsp.SymbolKind
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.sub_right : ∀ {n a b c : ℕ}, a ≤ b → a ≤ c → b ≡ c [MOD n] → b - a ≡ c - a [MOD n]
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.isoMk_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} (e : (i : ι) → D₁.obj i ≅ D₂.obj i)
  (comm :
    autoParam
      (∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
        (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
        (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
        CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom q f₁ f₂ ⋯ ⋯) =
          CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (e i₂).hom))
      CategoryTheory.Pseudofunctor.DescentData.isoMk._auto_1)
  (i : ι), (CategoryTheory.Pseudofunctor.DescentData.isoMk e comm).hom.hom i = (e i).hom
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_Iic : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] {l : ℝ},
  Filter.Tendsto (↑f) Filter.atBot (nhds l) → ∀ (x : R), f.measure (Set.Iic x) = ENNReal.ofReal (↑f x - l)
-- Mathlib.Order.SuccPred.Basic
Order.le_succ_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : PredOrder α] (a : α),
  a ≤ Order.succ (Order.pred a)
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_le_iff_le : ∀ {a b : ℕ} (ha : a < UInt16.size) (hb : b < UInt16.size), UInt16.ofNatLT a ha ≤ UInt16.ofNatLT b hb ↔ a ≤ b
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mem_mrange : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {y : N}, y ∈ AddMonoidHom.mrange f ↔ ∃ x, f x = y
-- Mathlib.Data.ENNReal.Basic
ENNReal.iUnion_Iic_coe_nat : ⋃ n, Set.Iic ↑n = {⊤}ᶜ
-- Mathlib.Algebra.Group.Irreducible.Lemmas
addIrreducible_add_addUnits : ∀ {M : Type u_2} [inst : AddMonoid M] {y : M} (u : AddUnits M), AddIrreducible (y + ↑u) ↔ AddIrreducible y
-- Mathlib.Algebra.MonoidAlgebra.Support
MonoidAlgebra.support_coeff_single_mul_subset : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : DecidableEq G] (x : MonoidAlgebra k G)
  (r : k) (a : G), (MonoidAlgebra.single a r * x).coeff.support ⊆ Finset.image (fun x => a * x) x.coeff.support
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Isomorphic monads give equivalent categories of algebras. Furthermore, they are equivalent as
categories over `C`, that is, we have `algebraEquivOfIsoMonads h ⋙ forget = forget`.
 -/
CategoryTheory.Monad.algebraEquivOfIsoMonads : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {T₁ T₂ : CategoryTheory.Monad C} → (T₁ ≅ T₂) → (T₁.Algebra ≌ T₂.Algebra)
-- Init.Data.BitVec.Bitblast
BitVec.toInt_smod : ∀ {w : ℕ} {x y : BitVec w}, (x.smod y).toInt = x.toInt.fmod y.toInt
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α},
  t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.RingTheory.Norm.Basic
Algebra.norm_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [Nontrivial S]
  [Module.Free R S] [Module.Finite R S], (Algebra.norm R) 0 = 0
-- Mathlib.Combinatorics.Graph.Basic
Graph.copy_eq : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) {V : Set α} {E : Set β} {IsLink : β → α → α → Prop}
  (hV : G.vertexSet = V) (hE : G.edgeSet = E) (h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y),
  G.copy hV hE h_isLink = G
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mk_eq_top_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N : Submodule R M}
  {h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier}, { toSubmodule := N, lie_mem := h } = ⊤ ↔ N = ⊤
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- An element of the atlas in a charted space without topology becomes an open partial
homeomorphism for the topology constructed from this atlas. The `OpenPartialHomeomorph` version is
given in this definition.  -/
ChartedSpaceCore.openPartialHomeomorph : {H : Type u} →
  {M : Type u_2} →
    [inst : TopologicalSpace H] →
      (c : ChartedSpaceCore H M) → (e : PartialEquiv M H) → e ∈ c.atlas → OpenPartialHomeomorph M H
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovary_inv_right`. -/
Antivary.inv_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : CommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedMonoid β] {f : ι → α} {g : ι → β}, Antivary f g → Monovary f g⁻¹
-- Std.Tactic.BVDecide.Syntax
/-- Whether to run the trimming algorithm on LRAT proofs.  -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig.trimProofs : Lean.Elab.Tactic.BVDecide.BVDecideConfig → Bool
-- Init.While
_private.Init.While.0.repeatM.impl.congr_simp : ∀ {α : Type u} {m : Type u → Type v} [inst : Monad m] {β : Type u} [inst_1 : Nonempty β] (f : α → m (α ⊕ β)) (a : α),
  repeatM.impl✝ f a = repeatM.impl✝ f a
-- Mathlib.Order.Heyting.Hom
map_symmDiff : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : CoheytingAlgebra α]
  [inst_2 : CoheytingAlgebra β] [CoheytingHomClass F α β] (f : F) (a b : α), f (symmDiff a b) = symmDiff (f a) (f b)
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- The morphism `triangleh φ₁ ⟶ triangleh φ₂` that is induced by a square that
is commutative up to homotopy.  -/
CochainComplex.mappingCone.trianglehMapOfHomotopy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} →
          {φ₁ : K₁ ⟶ L₁} →
            {φ₂ : K₂ ⟶ L₂} →
              {a : K₁ ⟶ K₂} →
                {b : L₁ ⟶ L₂} →
                  Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂) →
                    (CochainComplex.mappingCone.triangleh φ₁ ⟶ CochainComplex.mappingCone.triangleh φ₂)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- Given a `2`-truncated simplicial set `X` and a category `C`,
this is the bijection between morphism `X.HomotopyCategory ⥤ C`
and `X ⟶ (truncation 2).obj (nerve C)` which is part of the adjunction
`SSet.Truncated.nerve₂Adj`.  -/
SSet.Truncated.HomotopyCategory.functorEquiv : {X : SSet.Truncated 2} →
  {C : Type u} →
    [inst : CategoryTheory.SmallCategory C] →
      CategoryTheory.Functor X.HomotopyCategory C ≃ (X ⟶ (SSet.truncation 2).obj (CategoryTheory.nerve C))
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- For a ring homomorphism `f : R →+* S` and open sets `U` and `V` of the prime spectra of `R` and
`S` such that `V ⊆ (comap f) ⁻¹ U`, the induced ring homomorphism from the structure sheaf of `R`
at `U` to the structure sheaf of `S` at `V`.

Explicitly, this map is given as follows: For a point `p : V`, if the section `s` evaluates on `p`
to the fraction `a / b`, its image on `V` evaluates on `p` to the fraction `f(a) / f(b)`.
 -/
AlgebraicGeometry.StructureSheaf.comap : {R : Type u} →
  [inst : CommRing R] →
    {S : Type u} →
      [inst_1 : CommRing S] →
        (f : R →+* S) →
          (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
            (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)) →
              V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier →
                ↑((AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op U)) →+*
                  ↑((AlgebraicGeometry.Spec.structureSheaf S).obj.obj (Opposite.op V))
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.map_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C} (F : CategoryTheory.Functor C D) [F.Full], Function.Surjective F.map
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiff_infty : ∀ {𝕜 : 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'},
  ContMDiff I I' (↑⊤) f ↔ ∀ (n : ℕ), ContMDiff I I' (↑n) f
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.eq_inv : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : α) (v : ℚ) (d : ℕ),
  (v.num == 1 && v.den == d) = true → a = Lean.Grind.Field.NormNum.ofRat v → a = (↑d)⁻¹
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformAddGroup.ext : ∀ {G : Type u_3} [inst : AddGroup G] {u v : UniformSpace G},
  IsUniformAddGroup G → IsUniformAddGroup G → nhds 0 = nhds 0 → u = v
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.add_apply : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] (f g : P →ᴬ[R] W) (x : P),
  (f + g) x = f x + g x
-- Mathlib.Data.Set.Basic
Set.ofPred_top : ∀ {α : Type u}, {_x | ⊤} = Set.univ
-- Std.Time.DateTime.Timestamp
Std.Time.instInhabitedTimestamp : Inhabited Std.Time.Timestamp
-- Mathlib.GroupTheory.PushoutI
/-- The equivalence that is part of the universal property of the pushout. A hom out of
the pushout is just a morphism out of all groups in the pushout that satisfies a commutativity
condition.  -/
Monoid.PushoutI.homEquiv : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      {K : Type u_4} →
        [inst : Monoid K] →
          [inst_1 : (i : ι) → Monoid (G i)] →
            [inst_2 : Monoid H] →
              {φ : (i : ι) → H →* G i} → (Monoid.PushoutI φ →* K) ≃ { f // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs
/-- `IsIntegralClosure A R B` is the characteristic predicate stating `A` is
the integral closure of `R` in `B`,
i.e. that an element of `B` is integral over `R` iff it is an element of (the image of) `A`.
 -/
IsIntegralClosure : (A : Type u_1) →
  (R : Type u_2) →
    (B : Type u_3) →
      [inst : CommRing R] → [inst_1 : CommSemiring A] → [inst_2 : CommRing B] → [Algebra R B] → [Algebra A B] → Prop
-- Mathlib.Tactic.FunProp.Core
/-- Get candidate theorems from the local context for function property `funPropDecl` and
function `funName`.  -/
Mathlib.Meta.FunProp.getLocalTheorems : Mathlib.Meta.FunProp.FunPropDecl →
  Mathlib.Meta.FunProp.Origin → Array ℕ → ℕ → Mathlib.Meta.FunProp.FunPropM (Array Mathlib.Meta.FunProp.FunctionTheorem)
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.limitCone_π_app : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type (max v u))) (j : J),
  (CategoryTheory.Limits.Types.limitCone F).π.app j = TypeCat.ofHom fun u => ↑u j
-- Mathlib.RingTheory.AdjoinRoot
/-- If `R` is a field and `f` is irreducible, then `AdjoinRoot f` is a field  -/
AdjoinRoot.instField : {K : Type u_5} → [inst : Field K] → {f : Polynomial K} → [Fact (Irreducible f)] → Field (AdjoinRoot f)
-- Mathlib.Order.Heyting.Basic
/-- `p → q → r ↔ p ∧ q → r`  -/
le_himp_iff : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b ⇨ c ↔ a ⊓ b ≤ c
-- Mathlib.Computability.Ackermann
ack.induct : ∀ (motive : ℕ → ℕ → Prop),
  (∀ (n : ℕ), motive 0 n) →
    (∀ (m : ℕ), motive m 1 → motive m.succ 0) →
      (∀ (m n : ℕ), motive (m + 1) n → motive m (ack (m + 1) n) → motive m.succ n.succ) → ∀ (a a_1 : ℕ), motive a a_1
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_mul_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G]
  {a : G}, ContMDiff I I n fun x => x * a
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.PreZeroHypercoverFamily C} {X : C}
  {E : CategoryTheory.PreZeroHypercover X}, E.presieve₀ ∈ P.precoverage.coverings X ↔ P.property E
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.getD.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (a : α) (fallback : β) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.Const.getD ⟨{ size := size, buckets := buckets }, hm⟩ a fallback =
    Std.DHashMap.Internal.AssocList.getD a fallback buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))]
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientKerEquivOfRightInverse.eq_1 : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H) (ψ : H → G)
  (hφ : Function.RightInverse ψ ⇑φ),
  QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ hφ =
    { toFun := ⇑(QuotientAddGroup.kerLift φ), invFun := QuotientAddGroup.mk ∘ ψ, left_inv := ⋯, right_inv := hφ,
      map_add' := ⋯ }
-- Init.Data.Vector.Range
Vector.mem_range' : ∀ {s step m n : ℕ}, m ∈ Vector.range' s n step ↔ ∃ i < n, m = s + step * i
-- Init.Data.Array.Lemmas
Array.mem_of_mem_filter : ∀ {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α}, a ∈ Array.filter p xs → a ∈ xs
-- Mathlib.Analysis.SpecificLimits.Basic
/-- **Alias** of `NNReal.tsum_geometric`. -/
tsum_geometric_nnreal : ∀ {r : NNReal}, r < 1 → ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
-- Init.Data.Range.Basic
/-- The number of elements in the range.  -/
Std.Legacy.Range.size : Std.Legacy.Range → ℕ