mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Separation.Basic
inseparable_iff_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {x y : X}, Inseparable x y ↔ x = y
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.foldM_eq_foldlM_toList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'],
  m.WF →
    ∀ {f : δ → α → β → m' δ} {init : δ},
      Std.HashMap.Raw.foldM f init m = List.foldlM (fun a b => f a b.1 b.2) init m.toList
-- Mathlib.RingTheory.Extension.Cotangent.Basic
KaehlerDifferential.cotangentComplexBaseChange_tmul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] {P : Type u_2} {A : Type u_3}
  [inst_2 : CommRing P] [inst_3 : CommRing A] [inst_4 : Algebra P S] [inst_5 : Algebra P A] [inst_6 : Algebra R P]
  [inst_7 : Algebra S A] [inst_8 : IsScalarTower P S A] (a : A) (b : ↥(RingHom.ker (algebraMap P S))),
  (KaehlerDifferential.cotangentComplexBaseChange R S P A) (a ⊗ₜ[P] b) =
    a • (KaehlerDifferential.kerToTensor R P A) ⟨↑b, ⋯⟩
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_inv_hom_id_assoc : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantFrom i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (i₀ ⟶ i)) {Z : C} (h_1 : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (h.isoMap φ hφ).inv (CategoryTheory.CategoryStruct.comp (F.map φ) h_1) = h_1
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.isoImage_ι_inv_ι_assoc : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (V : (↑U).Opens) {Z : AlgebraicGeometry.Scheme} (h : ↑U ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage U.ι V).inv
      (CategoryTheory.CategoryStruct.comp V.ι h) =
    CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯) h
-- Batteries.Util.ProofWanted
/-- The trivial constructor; carries no information.  -/
DefWanted.mk : {α : Sort u} → DefWanted α
-- Lean.Server.FileWorker.RequestHandling
/-- Handles `completionItem/resolve` requests that are sent by the client after the user selects
a completion item that was provided by `textDocument/completion`. Resolving the item fills the
`detail?` field of the item with the pretty-printed type.
This control flow is necessary because pretty-printing the type for every single completion item
(even those never selected by the user) is inefficient.
 -/
Lean.Server.FileWorker.handleCompletionItemResolve : Lean.Lsp.CompletionItem → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.CompletionItem)
-- Init.Data.UInt.Lemmas
UInt8.ofNat_le_iff_le : ∀ {a b : ℕ}, a < UInt8.size → b < UInt8.size → (UInt8.ofNat a ≤ UInt8.ofNat b ↔ a ≤ b)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.isScalarTower_self : ∀ (k : Type u_1) (G : Type u_2) [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k]
  [IsScalarTower k k k], IsScalarTower k (SkewMonoidAlgebra k G) (SkewMonoidAlgebra k G)
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.simpMatch : Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.finite_effectiveEpiFamily_of_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  [F.ReflectsFiniteEffectiveEpiFamilies] {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B),
  (CategoryTheory.EffectiveEpiFamily (fun a => F.obj (X a)) fun a => F.map (π a)) →
    CategoryTheory.EffectiveEpiFamily X π
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_2 ()
-- Mathlib.Algebra.Algebra.Tower
AlgHom.comp_algebraMap_of_tower : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₐ[S] B),
  (↑f).comp (algebraMap R A) = algebraMap R B
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.quot_one : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat),
  Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) RingCat.Colimits.Prequotient.one = 1
-- Lean.Elab.PreDefinition.Basic
/-- Eliminate recursive application annotations containing syntax. These annotations are used by the well-founded recursion module
to produce better error messages.  -/
Lean.Elab.eraseRecAppSyntaxExpr : Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.Data.NNReal.Defs
NNReal.coe_injective : Function.Injective NNReal.toReal
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_apply : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F]
  (f : WithConv (E →ₗ[R] F)) (x : E), (star f).ofConv x = star (f.ofConv (star x))
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableWithinAt_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {x : E} {s : Set E} (c : F), DifferentiableWithinAt 𝕜 (fun x => c) s x
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_op : ∀ {M : Type u_2} [inst : MulOneClass M] (S : Submonoid M), S.op.unop = S
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.hcomp : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ x₂ : X} {p₀ p₁ : Path x₀ x₁} {q₀ q₁ : Path x₁ x₂},
  p₀.Homotopic p₁ → q₀.Homotopic q₁ → (p₀.trans q₀).Homotopic (p₁.trans q₁)
-- Lean.Elab.Do.Basic
/-- Information about `return`, `break` and `continue` continuations.  -/
Lean.Elab.Do.Context.contInfo : Lean.Elab.Do.Context → Lean.Elab.Do.ContInfoRef
-- Mathlib.Data.Fintype.Card
/-- `Fin` as a map from `ℕ` to `Type` is injective. Note that since this is a statement about
equality of types, using it should be avoided if possible.  -/
fin_injective : Function.Injective Fin
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.modifyNth.eq_1 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (f : Γ → Γ) (x : Turing.ListBlank Γ),
  Turing.ListBlank.modifyNth f 0 x = Turing.ListBlank.cons (f x.head) x.tail
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_one : ↑1 = 1
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addCommSemigroup : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddCommSemigroup (f i)] → AddCommSemigroup ((i : I) → f i)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.instInhabitedAlt.default : Lean.Meta.Match.Alt
-- Lean.Parser.Attr
Lean.Parser.Attr.export : Lean.Parser.Parser
-- Mathlib.Algebra.Group.TransferInstance
/-- An equivalence `e : α ≃ β` gives a multiplicative equivalence `α ≃* β` where
the multiplicative structure on `α` is the one obtained by transporting a multiplicative structure
on `β` back along `e`.  -/
Equiv.mulEquiv : {α : Type u_2} →
  {β : Type u_3} →
    (e : α ≃ β) →
      [inst : Mul β] →
        have x := e.mul;
        α ≃* β
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.memP_iff_upperBoundP? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut], RBTree.RBSet.MemP cut t ↔ ∃ x, t.upperBoundP? cut = some x ∧ cut x = Ordering.eq
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofZeros_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0),
  (CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg).iso =
    CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).H
-- Batteries.Control.Lemmas
StateT.run_failure : ∀ {m : Type u_1 → Type u_2} {α σ : Type u_1} [inst : Monad m] [inst_1 : Alternative m] (s : σ), failure.run s = failure
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep_precomp_of_bijective : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {ι' : Type u_6} {g : ι' → ι},
  Function.Bijective g → (ProbabilityTheory.iIndep (m ∘ g) μ ↔ ProbabilityTheory.iIndep m μ)
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.im_inner_apply_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ (x : E), RCLike.im (inner 𝕜 (T x) x) = 0
-- Std.Http.Data.Response
Std.Http.Response.Head.mk : Std.Http.Status → Std.Http.Version → Std.Http.Headers → Std.Http.Response.Head
-- Lean.Expr
/-- Return `true` if the given expression is a free variable with the given id.
Examples:
- `isFVarOf (.fvar id) id` is `true`
- ``isFVarOf (.fvar id) id'`` is `false`
- ``isFVarOf (.sort Level.zero) id`` is `false`
 -/
Lean.Expr.isFVarOf : Lean.Expr → Lean.FVarId → Bool
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ici_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α], UpperSet.Ici ⊥ = ⊥
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isNone_max?_eq_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t.max?.isNone = t.isEmpty
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.refl_apply : ∀ (X : Type u_4) [inst : PseudoEMetricSpace X], ⇑(DilationEquiv.refl X) = id
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.length_alterKey : ∀ {α : Type u} [inst : BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)},
  (Std.Internal.List.Const.alterKey k f l).length =
    if h : Std.Internal.List.containsKey k l = true then
      if (f (some (Std.Internal.List.getValue k l h))).isSome = true then l.length else l.length - 1
    else if (f none).isSome = true then l.length + 1 else l.length
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The trivial comonoid object. We later show this is terminal in `Comon C`.
 -/
CategoryTheory.Comon.trivial : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Comon C
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpOptions.mk.sizeOf_spec : ∀ (toWorkDoneProgressOptions : Lean.Lsp.WorkDoneProgressOptions)
  (triggerCharacters? retriggerCharacters? : Option (Array String)),
  sizeOf
      { toWorkDoneProgressOptions := toWorkDoneProgressOptions, triggerCharacters? := triggerCharacters?,
        retriggerCharacters? := retriggerCharacters? } =
    1 + sizeOf toWorkDoneProgressOptions + sizeOf triggerCharacters? + sizeOf retriggerCharacters?
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ModelWithCorners.extendCoordChange_target : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H},
  (ModelWithCorners.extendCoordChange e e').target = ↑I '' (e.symm.trans e').target
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
/-- Being a sheaf for a presieve `R` is local on the target in the following sense: If `E`
is a pre-`1`-hypercover for which `F` is separated and a sheaf for the `0`-components, then to
check that `F` is a sheaf for `R` it suffices to check:

- `F` is a sheaf for the pullbacks of `R` along the maps from the `0`-components.
- `F` is separated for the pullbacks of `R` along the maps from the `1`-components.
 -/
CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_of_pullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)},
  E.IsStronglySheafFor F →
    (∀ ⦃Y : C⦄ (f : Y ⟶ X),
        CategoryTheory.Presieve.IsSeparatedFor F (CategoryTheory.Sieve.pullback f E.sieve₀).arrows) →
      ∀ {R : CategoryTheory.Presieve X},
        (∀ (i : E.I₀),
            CategoryTheory.Presieve.IsSheafFor F
              (CategoryTheory.Sieve.pullback (E.f i) (CategoryTheory.Sieve.generate R)).arrows) →
          (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
              CategoryTheory.Presieve.IsSeparatedFor F
                (CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
                    (CategoryTheory.Sieve.generate R)).arrows) →
            CategoryTheory.Presieve.IsSheafFor F R
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.subterminalsEquivMonoOverTerminal_functor_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
  {X Y : CategoryTheory.Subterminals C} (f : X ⟶ Y),
  (CategoryTheory.subterminalsEquivMonoOverTerminal C).functor.map f = CategoryTheory.MonoOver.homMk f.hom ⋯
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.ofIsoLimit.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit r)
  (i : r ≅ t),
  P.ofIsoLimit i =
    CategoryTheory.Limits.IsLimit.mkConeMorphism
      (fun s => CategoryTheory.CategoryStruct.comp (P.liftConeMorphism s) i.hom) ⋯
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.densityProcess_mono_kernel_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ} {κ' : ProbabilityTheory.Kernel α (γ × β)},
  κ ≤ κ' → κ'.fst ≤ ν → ∀ (n : ℕ) (a : α) (x : γ) (s : Set β), κ.densityProcess ν n a x s ≤ κ'.densityProcess ν n a x s
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.evalCoeff_eq_zero : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  {x : M} {c : FiniteArchimedeanClass M}, (¬∃ y, ↑y - x ∈ FiniteArchimedeanClass.ball K c) → f.evalCoeff x c = 0
-- Mathlib.Probability.Moments.MGFAnalytic
/-- The cumulant-generating function is analytic on the interior of the interval
`integrableExpSet X μ`.  -/
ProbabilityTheory.analyticOn_cgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AnalyticOn ℝ (ProbabilityTheory.cgf X μ) (interior (ProbabilityTheory.integrableExpSet X μ))
-- Mathlib.Topology.Homeomorph.Defs
Equiv.toEquiv_toHomeomorph : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y)
  (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s), (e.toHomeomorph he).toEquiv = e
-- Mathlib.GroupTheory.Sylow
/-- Sylow subgroups are Hall subgroups.  -/
Sylow.card_coprime_index : ∀ {G : Type u} [inst : Group G] [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)] (P : Sylow p G),
  (Nat.card ↥↑P).Coprime (↑P).index
-- Init.Data.SInt.Lemmas
Int64.mul_one : ∀ (a : Int64), a * 1 = a
-- Mathlib.Topology.MetricSpace.Closeds
/-- **Alias** of `TopologicalSpace.Closeds.continuous_infEDist`.

---

The edistance to a closed set depends continuously on the point and the set  -/
EMetric.continuous_infEdist_hausdorffEdist : ∀ {α : Type u_1} [inst : EMetricSpace α], Continuous fun p => Metric.infEDist p.1 ↑p.2
-- Aesop.Index
Aesop.Index.trace : {α : Type} → [ToString (Aesop.Rule α)] → Aesop.Index α → Aesop.TraceOption → Lean.CoreM Unit
-- Aesop.Tree.Data
Aesop.treeImpl : Aesop.TreeSpec
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.regularityReduced.congr_simp : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  (P P_1 : Finpartition A),
  P = P_1 →
    ∀ (G G_1 : SimpleGraph α),
      G = G_1 →
        ∀ {inst_3 : DecidableRel G.Adj} [inst_4 : DecidableRel G_1.Adj] (ε ε_1 : 𝕜),
          ε = ε_1 →
            ∀ (δ δ_1 : 𝕜),
              δ = δ_1 → SimpleGraph.regularityReduced P G ε δ = SimpleGraph.regularityReduced P_1 G_1 ε_1 δ_1
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_zero_one : ∀ {R : Type u_1} [inst : Semiring R], (SkewPolynomial.monomial 0) 1 = 1
-- Mathlib.Order.UpperLower.Fibration
Relation.fibration_iff_isLowerSet_image_Iic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : LE β],
  Relation.Fibration (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) f ↔ ∀ (x : α), IsLowerSet (f '' Set.Iic x)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- An arbitrary choice of weak limit cone for a functor.  -/
CategoryTheory.Limits.weakLimit.cone : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        (F : CategoryTheory.Functor J C) → [CategoryTheory.Limits.HasWeakLimit F] → CategoryTheory.Limits.Cone F
-- Mathlib.Data.Finset.Empty
Finset.Nonempty.eq_1 : ∀ {α : Type u_1} (s : Finset α), s.Nonempty = ∃ x, x ∈ s
-- Mathlib.NumberTheory.LegendreSymbol.Complex
/-- A primitive additive character on the finite field `F` with values in `ℂ`.  -/
AddChar.FiniteField.primitiveChar_to_Complex : (F : Type u_1) → [inst : Field F] → [Finite F] → AddChar F ℂ
-- Mathlib.Analysis.Normed.Group.Continuity
/-- In a normed group, the pullback under the norm of `𝓝[>] 0` is the punctured neighborhood
of `1`.  -/
comap_norm_nhdsGT_zero' : ∀ (E : Type u_4) [inst : NormedGroup E], Filter.comap norm (nhdsWithin 0 (Set.Ioi 0)) = nhdsWithin 1 {1}ᶜ
-- Lean.Compiler.BorrowedAnnotation
Lean.markBorrowed : Lean.Expr → Lean.Expr
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon.go : ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.CategoryTheory.Action.Basic
/-- (implementation) The forgetful functor from bundled actions to the underlying objects.

Use the `CategoryTheory.forget` API provided by the `ConcreteCategory` instance below,
rather than using this directly.
 -/
Action.forget : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) → [inst_1 : Monoid G] → CategoryTheory.Functor (Action V G) V
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousMul.mk : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M], (Continuous fun p => p.1 * p.2) → ContinuousMul M
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.instIsSFiniteKernelSectROfProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : α) [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.IsSFiniteKernel (κ.sectR a)
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerivedNatTrans_comp_assoc : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (RF RF' RF'' : CategoryTheory.Functor D H) {F F' F'' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (α'' : F'' ⟶ L.comp RF'') (W : CategoryTheory.MorphismProperty C)
  [inst_3 : L.IsLocalization W] [inst_4 : RF.IsRightDerivedFunctor α W] [inst_5 : RF'.IsRightDerivedFunctor α' W]
  (τ : F ⟶ F') (τ' : F' ⟶ F'') {Z : CategoryTheory.Functor D H} (h : RF'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (RF.rightDerivedNatTrans RF' α α' W τ)
      (CategoryTheory.CategoryStruct.comp (RF'.rightDerivedNatTrans RF'' α' α'' W τ') h) =
    CategoryTheory.CategoryStruct.comp (RF.rightDerivedNatTrans RF'' α α'' W (CategoryTheory.CategoryStruct.comp τ τ'))
      h
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.HasRightDerivedFunctor.mk' : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (RF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) {W : CategoryTheory.MorphismProperty C} [inst_3 : L.IsLocalization W]
  [RF.IsRightDerivedFunctor α W], F.HasRightDerivedFunctor W
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.intCast_def : ∀ (R : Type u_1) {N₁ : Type u_8} [inst : Semiring R] (z : ℤ) [inst_1 : AddCommGroup N₁] [inst_2 : Module R N₁],
  ↑z = (Module.toModuleEnd R N₁) z
-- Mathlib.Algebra.Quaternion
Quaternion.re_ratCast : ∀ {R : Type u_1} [inst : Field R] (q : ℚ), (↑q).re = ↑q
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.leftRel.eq_1 : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), QuotientGroup.leftRel s = MulAction.orbitRel (↥s.op) α
-- Mathlib.Algebra.Order.CauSeq.Basic
IsCauSeq.add : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f g : ℕ → β},
  IsCauSeq abv f → IsCauSeq abv g → IsCauSeq abv (f + g)
-- Mathlib.RingTheory.Flat.Equalizer
AlgHom.tensorEqualizerAux_mul : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {A : Type u_4}
  {B : Type u_5} [inst_7 : CommRing A] [inst_8 : CommRing B] [inst_9 : Algebra R A] [inst_10 : Algebra R B]
  (f g : A →ₐ[R] B) (x y : TensorProduct R T ↥(f.equalizer g)),
  (AlgHom.tensorEqualizerAux S T f g) (x * y) =
    (AlgHom.tensorEqualizerAux S T f g) x * (AlgHom.tensorEqualizerAux S T f g) y
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.add_mem_cancel_left : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {x y : G}, x ∈ H → (x + y ∈ H ↔ y ∈ H)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
EuclideanGeometry.oangle_pointReflection_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  p₁ ≠ p₂ →
    p₃ ≠ p₂ →
      EuclideanGeometry.oangle ((AffineEquiv.pointReflection ℝ p₂) p₁) p₂ p₃ =
        EuclideanGeometry.oangle p₁ p₂ p₃ + ↑Real.pi
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.smul_apply : ∀ {M : Type u_2} {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Monoid M] [inst_2 : DistribMulAction M α]
  [inst_3 : SMulCommClass M α α] [inst_4 : IsScalarTower M α α] (n : M) (f : CentroidHom α) (a : α), (n • f) a = n • f a
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_le_pow_of_le_one : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [PosMulMono M₀],
  0 ≤ a → a ≤ 1 → ∀ {m n : ℕ}, m ≤ n → a ^ n ≤ a ^ m
-- Mathlib.Algebra.Ring.Basic
/-- Right multiplication by an element of a (semi)ring is an `AddMonoidHom`  -/
AddMonoidHom.mulRight : {R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → R → R →+ R
-- Mathlib.RingTheory.Spectrum.Maximal.Topology
MaximalSpectrum.toPrimeSpectrum_range : ∀ {R : Type u} [inst : CommRing R], Set.range MaximalSpectrum.toPrimeSpectrum = {x | IsClosed {x}}