mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.comap` as an `AddMonoidHom`.  -/
LocallyConstant.comapAddMonoidHom : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {Z : Type u_6} → [inst_2 : AddZeroClass Z] → C(X, Y) → LocallyConstant Y Z →+ LocallyConstant X Z
-- Mathlib.Order.Filter.Pointwise
Filter.vsub_eq_bot_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f g : Filter β}, f -ᵥ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_subtype : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {p : ι → Prop} {f : Subtype p → α},
  BddAbove (Set.range f) → sSup ∅ ≤ iSup f → iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_neg : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : PartialOrder S] [IsOrderedRing S] [NoZeroDivisors S]
  [inst_4 : Ring R] (abv : R → S) [IsAbsoluteValue abv] (a : R), abv (-a) = abv a
-- Mathlib.RingTheory.Flat.Basic
/-- `M` is flat if and only if `f ⊗ 𝟙 M` is injective whenever `f` is an injective linear map.
See `Module.Flat.iff_rTensor_preserves_injective_linearMap` to specialize the universe of
`N, N', N''` to `Type (max u v)`.  -/
Module.Flat.iff_rTensor_preserves_injective_linearMap' : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Small.{v', u} R],
  Module.Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : Module R N] [inst_7 : Module R N']
      (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.rTensor M f)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A seminormed ring is a non-unital seminormed ring.  -/
SeminormedRing.toNonUnitalSeminormedRing : {α : Type u_2} → [β : SeminormedRing α] → NonUnitalSeminormedRing α
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_func : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} (v : α → M) {n : ℕ} (f : L.Functions n)
  (ts : Fin n → L.Term α),
  FirstOrder.Language.Term.realize v (FirstOrder.Language.func f ts) =
    FirstOrder.Language.Structure.funMap f fun i => FirstOrder.Language.Term.realize v (ts i)
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.matchesAt_iff_toSlice : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt pat pos ↔ String.Slice.Pattern.Model.MatchesAt pat.toSlice pos
-- Mathlib.Algebra.EuclideanDomain.Field
Field.gcd_zero_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] (b : K), EuclideanDomain.gcd 0 b = b
-- Mathlib.Order.Closure
LowerAdjoint.id_toFun : ∀ (α : Type u_1) [inst : Preorder α] (x : α), (LowerAdjoint.id α).toFun x = x
-- Mathlib.RepresentationTheory.Intertwining
/-- An underlying `A`-linear map of the underlying `A`-modules.  -/
Representation.IntertwiningMap.isIntertwining' : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (self : ρ.IntertwiningMap σ) (g : G),
  self.toLinearMap ∘ₗ ρ g = σ g ∘ₗ self.toLinearMap
-- Batteries.Classes.Order
Std.LawfulLTCmp.eq_gt_iff_gt : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [inst : LT α] [Std.LawfulLTCmp cmp], cmp x y = Ordering.gt ↔ y < x
-- Mathlib.Tactic.Translate.GuessName
/-- If `r` starts with an upper-case letter, return `s`, otherwise return `s` with the
initial sequence of upper-case letters lower-cased.  -/
Mathlib.Tactic.GuessName.decapitalizeLike : String → String → String
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.closedInterior_map : ∀ {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_4} {P₂ : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup V₂] [inst_5 : Module k V₂]
  [inst_6 : AddTorsor V₂ P₂] [inst_7 : PartialOrder k] {n : ℕ} (s : Affine.Simplex k P n) {f : P →ᵃ[k] P₂}
  (hf : Function.Injective ⇑f), (s.map f hf).closedInterior = ⇑f '' s.closedInterior
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.mk.sizeOf_spec : ∀ {α : Type u_4} [inst : SizeOf α] (vertexSet : Set α) (edgeSet : Set (Set α))
  (subset_vertexSet_of_mem_edgeSet' : ∀ ⦃e : Set α⦄, e ∈ edgeSet → e ⊆ vertexSet),
  sizeOf
      { vertexSet := vertexSet, edgeSet := edgeSet,
        subset_vertexSet_of_mem_edgeSet' := subset_vertexSet_of_mem_edgeSet' } =
    1
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.finite_of_mono : ∀ {X Y : SSet} [Y.Finite] (f : X ⟶ Y) [hf : CategoryTheory.Mono f], X.Finite
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.GammaAux.eq_def : ∀ (x : ℕ),
  Complex.GammaAux✝ x =
    match (motive := ℕ → ℂ → ℂ) x with
    | 0 => Complex.GammaIntegral
    | n.succ => fun s => Complex.GammaAux✝ n (s + 1) / s
-- Mathlib.Data.Finsupp.Option
Finsupp.optionElim_apply_eq_elim : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (y : M) (f : α →₀ M) (a : Option α),
  (Finsupp.optionElim y f) a = a.elim y ⇑f
-- Mathlib.LinearAlgebra.Eigenspace.Minpoly
/-- An endomorphism of a finite-dimensional vector space has a finite spectrum.  -/
Module.End.finite_spectrum : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  (f : Module.End K V), (spectrum K f).Finite
-- Mathlib.Order.Closure
/-- Every Galois connection induces a closure operator given by the composition. This is the partial
order version of the statement that every adjunction induces a monad.  -/
GaloisConnection.closureOperator : {α : Type u_1} →
  {β : Type u_4} →
    [inst : PartialOrder α] →
      [inst_1 : Preorder β] → {l : α → β} → {u : β → α} → GaloisConnection l u → ClosureOperator α
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainOfBialgHom_mapDomainBialgHom : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G]
  [inst_3 : Group H] (f : G →* H), MonoidAlgebra.mapDomainOfBialgHom (MonoidAlgebra.mapDomainBialgHom R f) = f
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffWithinAt.sub_section : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} {u : Set M} {x₀ : M},
  ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) u x₀ →
    ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t x⟩) u x₀ →
      ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (s - t) x⟩) u x₀
-- Mathlib.Algebra.Tropical.Basic
Tropical.instPowOfSMul : {R : Type u} → {α : Type u_1} → [SMul α R] → Pow (Tropical R) α
-- Mathlib.Algebra.Order.Group.PosPart
/-- See also `leOnePart_eq_inv`.  -/
leOnePart_eq_inv' : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] {a : α}, a⁻ᵐ = a⁻¹ ↔ 1 ≤ a⁻¹
-- Mathlib.Data.Fintype.Quotient
Quotient.eval_finChoice : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  (f : (i : ι) → Quotient (S i)), (Quotient.finChoice f).eval = f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_eq_default : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = true → t.maxKey! = default
-- Lean.Level
_private.Lean.Level.0.Lean.Level.PP.Result.formatLst : List Lean.Level.PP.Result → Std.Format
-- Mathlib.RingTheory.Nakayama
Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M]
  [Module.Finite R M] {I : Ideal R}, I ≤ (Module.annihilator R M).jacobson → ⊤ ≠ I • ⊤
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulEquiv.subsemigroupMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) (S : Subsemigroup M),
  e.subsemigroupMap S =
    { toFun := fun x => ⟨e ↑x, ⋯⟩, invFun := fun x => ⟨e.symm ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- The underlying object of `(Comonad.comparison L).obj X` is just `L.obj X`.
 -/
CategoryTheory.Comonad.comparisonForget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} →
            (h : L ⊣ R) → (CategoryTheory.Comonad.comparison h).comp h.toComonad.forget ≅ L
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
/-- The continuous `ℤ`-algebra isomorphism between `v.adicCompletionIntegers ℚ` and
`ℤ_[primesEquiv v]`.  -/
Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv : {R : Type u_2} →
  [inst : CommRing R] →
    [inst_1 : Algebra R ℚ] →
      [inst_2 : IsIntegralClosure R ℤ ℚ] →
        [inst_3 : IsDedekindDomain R] →
          [inst_4 : IsFractionRing R ℚ] →
            (v : IsDedekindDomain.HeightOneSpectrum R) →
              ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v) ≃A[ℤ]
                ℤ_[↑(Rat.HeightOneSpectrum.primesEquiv v)]
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.dropn_think : ∀ {α : Type u} (s : Stream'.WSeq α) (n : ℕ), s.think.drop n = (s.drop n).think
-- Lean.Meta.Check
/-- Return error message "has type{givenType}\nbut is expected to have type{expectedType}"
Adds the type’s types unless they are defeq.

If `trailing?` is non-`none`, it is appended to the end of the message. This requires modifying the
produced message, so prefer specifying `trailing?` over appending a message to the result of this
function. Any expressions appearing in the trailing message should be included in `trailingExprs`.
 -/
Lean.Meta.mkHasTypeButIsExpectedMsg : Lean.Expr →
  Lean.Expr → optParam (Option Lean.MessageData) none → optParam (Array Lean.Expr) #[] → Lean.MetaM Lean.MessageData
-- Mathlib.Data.Set.NAry
Set.mem_image2_iff : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β},
  Function.Injective2 f → (f a b ∈ Set.image2 f s t ↔ a ∈ s ∧ b ∈ t)
-- Mathlib.CategoryTheory.Action.Basic
Action.res_obj_ρ : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [inst_1 : Monoid G]
  [inst_2 : Monoid H] (f : G →* H) (M : Action V H), ((Action.res V f).obj M).ρ = M.ρ.comp f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_alter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k k' : α} {f : Option β → Option β},
  Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl k' =
    if compare k k' = Ordering.eq then f (Std.DTreeMap.Internal.Impl.Const.get? t k)
    else Std.DTreeMap.Internal.Impl.Const.get? t k'
-- Mathlib.RingTheory.Jacobson.Ring
/-- If `f : R → S` descends to an integral map in the localization at `x`,
and `R` is a Jacobson ring, then the intersection of all maximal ideals in `S` is trivial  -/
Polynomial.jacobson_bot_of_integral_localization : ∀ {S : Type u_2} [inst : CommRing S] [IsDomain S] {R : Type u_5} [inst_2 : CommRing R] [IsDomain R] [IsJacobsonRing R]
  (Rₘ : Type u_6) (Sₘ : Type u_7) [inst_5 : CommRing Rₘ] [inst_6 : CommRing Sₘ] (φ : R →+* S),
  Function.Injective ⇑φ →
    ∀ (x : R),
      x ≠ 0 →
        ∀ [inst_7 : Algebra R Rₘ] [inst_8 : IsLocalization.Away x Rₘ] [inst_9 : Algebra S Sₘ]
          [inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ],
          (IsLocalization.map Sₘ φ ⋯).IsIntegral → ⊥.jacobson = ⊥
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.point_finite : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s) (x : M),
  {i | ↑(fs.toFun i) x ≠ 0}.Finite
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.codExtend_toFun : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {s : Set B}
  (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Bundle.Pretrivialization F proj) (z : Z),
  ↑(Bundle.Pretrivialization.codExtend hs nonempty e).toPartialEquiv z = (↑(↑e z).1, (↑e z).2)
-- Mathlib.Algebra.Algebra.Basic
/-- A `Semiring` that is an `Algebra` over a commutative ring carries a natural `Ring` structure.
See note [reducible non-instances].  -/
Algebra.semiringToRing : {A : Type u_2} → (R : Type u_4) → [inst : CommRing R] → [inst_1 : Semiring A] → [Algebra R A] → Ring A
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The natural isomorphism of triangles `t.triangleLEGE a b h ≅ t.triangleLTGE b`
when `a + 1 = b`.  -/
CategoryTheory.Triangulated.TStructure.triangleLEGEIsoTriangleLTGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                (a b : ℤ) → (h : a + 1 = b) → t.triangleLEGE a b h ≅ t.triangleLTGE b
-- Mathlib.Data.Part
Part.map_eq_map : ∀ {α β : Type u_4} (f : α → β) (o : Part α), f <$> o = Part.map f o
-- Mathlib.Topology.Constructions.SumProd
isOpenMap_prodMap_iff : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] [Nonempty X] [Nonempty Z] {f : X → Y} {g : Z → W},
  IsOpenMap (Prod.map f g) ↔ IsOpenMap f ∧ IsOpenMap g
-- Mathlib.Algebra.GradedMonoid
/-- Build a `GCommMonoid` instance for a collection of subobjects.  -/
SetLike.gCommMonoid : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      [inst : SetLike S R] →
        [inst_1 : CommMonoid R] →
          [inst_2 : AddCommMonoid ι] → (A : ι → S) → [SetLike.GradedMonoid A] → GradedMonoid.GCommMonoid fun i => ↥(A i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.leadingCoeff_Ψ₃ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 3 ≠ 0 → W.Ψ₃.leadingCoeff = 3
-- Mathlib.Algebra.Group.AddChar
AddChar.ext_iff : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] {f g : AddChar A M},
  f = g ↔ ∀ (x : A), f x = g x
-- Lean.Meta.Tactic.Grind.Types
/-- Sets methods/handlers for solver extension `ext`.
Solver extension methods can only be registered during initialization.
Reason: We do not use any synchronization primitive to access `solverExtensionsRef`.
 -/
Lean.Meta.Grind.SolverExtension.setMethods : {σ : Type} →
  Lean.Meta.Grind.SolverExtension σ →
    (optParam (Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM Unit) fun x x_1 => pure ()) →
      (optParam (Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit) fun x x_1 => pure ()) →
        (optParam (Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit) fun x x_1 => pure ()) →
          optParam (Lean.Meta.Grind.GoalM Bool) (pure false) →
            optParam Lean.Meta.Grind.Action Lean.Meta.Grind.Action.notApplicable →
              optParam (Lean.Meta.Grind.GoalM Bool) (pure false) →
                optParam (Lean.Meta.Grind.GoalM Unit) (pure ()) → IO Unit
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.forget_map : ∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y), CategoryTheory.Quiv.forget.map F = F.toFunctor.toPrefunctor
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.forIn'_eq_forIn'_toList : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.Rxc.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toList init fun a ha acc => f a ⋯ acc
-- Mathlib.Order.Category.Frm
Frm.id_apply : ∀ (X : Frm) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.smooth_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Smooth f ↔
    ∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Smooth
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.hasProducts_of_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasCoproducts Cᵒᵖ],
  CategoryTheory.Limits.HasProducts C
-- Mathlib.Topology.Algebra.Valued.NormedValued
/-- The valued field structure on a nonarchimedean normed field `K`, determined by the norm.  -/
NormedField.toValued : {K : Type u_1} → [hK : NormedField K] → [IsUltrametricDist K] → Valued K NNReal
-- Batteries.Classes.Order
/-- `cmp x y = .lt` holds iff `x < y` is true.  -/
Std.LawfulBCmp.eq_lt_iff_lt : ∀ {α : Type u_1} {inst : LE α} {inst_1 : LT α} {inst_2 : BEq α} {cmp : α → α → Ordering} [self : Std.LawfulBCmp cmp]
  {x y : α}, cmp x y = Ordering.lt ↔ x < y
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_alter_of_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {f : Option (β k) → Option (β k)},
  m.WF → (k == k') = true → (k' ∈ m.alter k f ↔ (f (m.get? k)).isSome = true)
-- Std.Data.DHashMap.Raw
/-- Folds the given function over the mappings in the hash map in the reverse order used
by `foldM`.  -/
Std.DHashMap.Raw.foldRev : {α : Type u} → {β : α → Type v} → {δ : Type w} → (δ → (a : α) → β a → δ) → δ → Std.DHashMap.Raw α β → δ
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.instCompleteLatticeNonUnitalStarSubalgebra : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : NonUnitalSemiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Module R A] →
              [IsScalarTower R A A] →
                [SMulCommClass R A A] → [StarModule R A] → CompleteLattice (NonUnitalStarSubalgebra R A)
-- Mathlib.Analysis.Normed.Group.Basic
/-- The norm of a seminormed group as a group seminorm.  -/
normGroupSeminorm : (E : Type u_5) → [inst : SeminormedGroup E] → GroupSeminorm E
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- The `BifunctorComp₁₂IndexData r` attached to a `TriangleIndexData r π`.  -/
CategoryTheory.GradedObject.TriangleIndexData.ρ₁₂ : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₃ : Type u_3} →
      {J : Type u_4} →
        [inst : Zero I₂] →
          {r : I₁ × I₂ × I₃ → J} →
            {π : I₁ × I₃ → J} →
              CategoryTheory.GradedObject.TriangleIndexData r π → CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r
-- Mathlib.Algebra.BigOperators.Finprod
/-- Product of `f x` as `x` ranges over the elements of the multiplicative support of `f`, if it's
finite. One otherwise.  -/
finprod : {M : Type u_7} → {α : Sort u_8} → [CommMonoid M] → (α → M) → M
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.addZeroClass.eq_1 : ∀ {α : Type u_2} [inst : AddZeroClass α],
  Set.addZeroClass = { toZero := Set.zero, toAdd := Set.add, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_lt_sqrt_iff : ∀ {x y : ℝ}, 0 ≤ x → (√x < √y ↔ x < y)
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instInvCauchy : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : DivisionRing β] →
            {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → Inv (CauSeq.Completion.Cauchy abv)
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.dValue_pos : ∀ {N : ℕ}, 8 ≤ N → 0 < Behrend.dValue N
-- Mathlib.Order.Antichain
IsAntichain.subsingleton : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Trichotomous r], IsAntichain r s → s.Subsingleton
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comapOn_finitary : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {E : Set α} [N.Finitary], (N.comapOn E f).Finitary
-- Mathlib.Data.Finsupp.Single
Finsupp.card_support_eq_one' : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M}, f.support.card = 1 ↔ ∃ a b, b ≠ 0 ∧ f = fun₀ | a => b
-- Mathlib.CategoryTheory.Sites.Monoidal
/-- The monoidal category structure on `Sheaf J A` that is obtained
by localization of the monoidal category structure on the category
of presheaves.  -/
CategoryTheory.Sheaf.monoidalCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₃) →
        [inst_1 : CategoryTheory.Category.{v₃, u₃} A] →
          [inst_2 : CategoryTheory.MonoidalCategory A] →
            [J.W.IsMonoidal] →
              [CategoryTheory.HasWeakSheafify J A] → CategoryTheory.MonoidalCategory (CategoryTheory.Sheaf J A)
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.compr₂_linearEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} {M' : Type u_5}
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M']
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M] [inst_8 : Module R M'] {f : M₁ →ₗ[R] M₂ →ₗ[R] M},
  IsTensorProduct f → ∀ (e : M ≃ₗ[R] M'), IsTensorProduct (f.compr₂ ↑e)
-- Init.Data.Bool
Bool.or_right_comm : ∀ (x y z : Bool), (x || y || z) = (x || z || y)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.foldl_filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.norm_toLp_le_seminorm : ∀ (𝕜 : Type u_2) {E : Type u_5} (F : Type u_6) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E]
  [inst_5 : OpensMeasurableSpace E] [inst_6 : NormedField 𝕜] [inst_7 : NormedSpace 𝕜 F] [inst_8 : SMulCommClass ℝ 𝕜 F]
  [inst_9 : SecondCountableTopologyEither E F] (p : ENNReal)
  (μ : autoParam (MeasureTheory.Measure E) SchwartzMap.norm_toLp_le_seminorm._auto_1) [hμ : μ.HasTemperateGrowth],
  ∃ k C, 0 ≤ C ∧ ∀ (f : SchwartzMap E F), ‖f.toLp p μ‖ ≤ C * ((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f
-- Mathlib.Order.SuccPred.Basic
pred_notMem_iff_isMin : ∀ {α : Type u_3} [inst : PartialOrder α] {s : Set α} [s.OrdConnected] [inst_2 : PredOrder α] [NoMinOrder α] {a : ↑s},
  Order.pred ↑a ∉ s ↔ IsMin a
-- Mathlib.RingTheory.Conductor
_private.Mathlib.RingTheory.Conductor.0.«term_<_>» : Lean.TrailingParserDescr