mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Do.Internal.Ensures.Def
/-- `MayReturn x a` says `a` is in every postcondition of `x`, equivalently that `a`
is a value returnable from `x`. (The strongest postcondition, evaluated at `a`.)  -/
Std.Do.Internal.MayReturn : {m : Type u → Type v} → [Bind m] → {α : Type u} → m α → α → Prop
-- Mathlib.Logic.Equiv.Set
Equiv.Set.sumCompl_symm_apply_of_mem : ∀ {α : Type u} {s : Set α} [inst : DecidablePred fun x => x ∈ s] {x : α} (hx : x ∈ s),
  (Equiv.Set.sumCompl s).symm x = Sum.inl ⟨x, hx⟩
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.mem_prod : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {s : AddSubsemigroup M} {t : AddSubsemigroup N}
  {p : M × N}, p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
-- Mathlib.Data.Nat.Pairing
Nat.max_sq_add_min_le_pair : ∀ (m n : ℕ), max m n ^ 2 + min m n ≤ Nat.pair m n
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The conductor of the trivial character is 1.  -/
DirichletCharacter.conductor_one : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} [NeZero n], DirichletCharacter.conductor 1 = 1
-- Mathlib.Topology.Algebra.Module.Equiv
/-- A continuous equivalence from `M` to itself determines an invertible continuous linear map.  -/
ContinuousLinearEquiv.toUnit : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [inst_3 : TopologicalSpace M] → (M ≃L[R] M) → (M →L[R] M)ˣ
-- Lean.Meta.Tactic.Simp.Simproc
_private.Lean.Meta.Tactic.Simp.Simproc.0.Lean.Meta.Simp.addBuiltin : Lean.Name → Lean.Syntax → Lean.Name → Lean.AttrM Unit
-- Mathlib.Topology.MetricSpace.HausdorffDimension
dimH_bUnion : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {s : Set ι},
  s.Countable → ∀ (t : ι → Set X), dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_normEq0 : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (c : ℕ)
  (p₁ p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.eq_normEq0_cert c p₁ p₂ p = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ = 0 →
      Lean.Grind.CommRing.Poly.denote ctx p₂ = 0 → Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.toZeroHom_eq_coe : ∀ {E : Type u_3} [inst : AddGroup E] {p : NonarchAddGroupSeminorm E}, ⇑p.toZeroHom = ⇑p
-- Mathlib.Algebra.Ring.Semireal.Defs
isSemireal_iff : ∀ (R : Type u_1) [inst : Add R] [inst_1 : Mul R] [inst_2 : One R] [inst_3 : Zero R],
  IsSemireal R ↔ ∀ {s : R}, IsSumSq s → 1 + s ≠ 0
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.toMonoidWithZeroHom_eq_ofClass : ∀ {α : Type u_2} {β : Type u_3} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β}
  (f : α →*₀o β), f.toMonoidWithZeroHom = MonoidWithZeroHom.ofClass f
-- Mathlib.Logic.Equiv.Option
Equiv.optionSubtypeNe_none : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), (Equiv.optionSubtypeNe a) none = a
-- Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Finset.prod_intervalGapsWithin_mul_prod_eq_div : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : CommGroup β] (F : Finset (α × α)) {k : ℕ}
  (h : F.card = k) {a b : α} (g : α → β),
  (∏ i ∈ Finset.range (k + 1), g (F.intervalGapsWithin h a b ↑i).2 / g (F.intervalGapsWithin h a b ↑i).1) *
      ∏ z ∈ F, g z.2 / g z.1 =
    g b / g a
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instAddMonoid : {M : Type u_2} →
  {N : Type u_3} →
    {X : Type u_4} →
      {Y : Type u_5} →
        {σ : M → N} → [inst : SMul M X] → [inst_1 : AddMonoid Y] → [inst_2 : DistribSMul N Y] → AddMonoid (X →ₑ[σ] Y)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.π_descHomology_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} [inst_2 : S.HasHomology] (k : S.cycles ⟶ A)
  (hk : CategoryTheory.CategoryStruct.comp S.toCycles k = 0) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.homologyπ (CategoryTheory.CategoryStruct.comp (S.descHomology k hk) h) =
    CategoryTheory.CategoryStruct.comp k h
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.germ_comp_stalkToFiberRingHom : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)) (x : ↑(ProjectiveSpectrum.top 𝒜))
  (hx : x ∈ U),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.germ U x hx)
      (AlgebraicGeometry.stalkToFiberRingHom 𝒜 x) =
    AlgebraicGeometry.openToLocalization 𝒜 U x hx
-- Init.Control.Option
OptionT.instInhabitedOfPure : {α : Type u} → {m : Type u → Type v} → [Pure m] → Inhabited (OptionT m α)
-- Mathlib.Combinatorics.Hindman
Hindman.FP.tail' : ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M) (m : M), Hindman.FP a.tail m → Hindman.FP a m
-- Mathlib.RepresentationTheory.Coinvariants
/-- The quotient map from a representation to its coinvariants induces a natural transformation
from the forgetful functor `Rep k G ⥤ ModuleCat k` to the coinvariants functor.  -/
Rep.coinvariantsMk : (k : Type u) →
  (G : Type v) →
    [inst : CommRing k] →
      [inst_1 : Monoid G] → CategoryTheory.forget₂ (Rep.{u_1, u, v} k G) (ModuleCat k) ⟶ Rep.coinvariantsFunctor k G
-- Std.Http.Server
/-- The `Server` structure holds all state required to manage the lifecycle of an HTTP server, including
connection tracking and shutdown coordination.
 -/
Std.Http.Server : Type
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.inv_one_sub_inv' : ∀ {a : ENNReal}, 1 ≤ a → a.HolderConjugate (1 - a⁻¹)⁻¹
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The `a₁` coefficient of a Weierstrass curve.  -/
WeierstrassCurve.a₁ : {R : Type u} → WeierstrassCurve R → R
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.assoc_tmul : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} {D : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Semiring A] [inst_3 : Bialgebra S A] [inst_4 : Algebra R A] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring C] [inst_8 : Semiring D] [inst_9 : Bialgebra S C]
  [inst_10 : Bialgebra R D] [inst_11 : Algebra R C] [inst_12 : IsScalarTower R S C] (x : A) (y : C) (z : D),
  (Bialgebra.TensorProduct.assoc R S A C D) (x ⊗ₜ[S] y ⊗ₜ[R] z) = x ⊗ₜ[S] (y ⊗ₜ[R] z)
-- Mathlib.Data.Set.Prod
Membership.mem.hcongr_5 : ∀ (α α' : Type u),
  α = α' →
    ∀ (γ γ' : Type v),
      γ = γ' →
        ∀ (self : Membership α γ) (self' : Membership α' γ'),
          self ≍ self' → ∀ (a : γ) (a' : γ'), a ≍ a' → ∀ (a_1 : α) (a'_1 : α'), a_1 ≍ a'_1 → (a_1 ∈ a) ≍ (a'_1 ∈ a')
-- Init.Data.Iterators.Lemmas.Combinators.Append
Std.Iter.toList_append : ∀ {α₁ α₂ β : Type w} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] [Std.Iterators.Finite α₁ Id]
  [Std.Iterators.Finite α₂ Id] {it₁ : Std.Iter β} {it₂ : Std.Iter β}, (it₁.append it₂).toList = it₁.toList ++ it₂.toList
-- Mathlib.Analysis.Calculus.FDeriv.Pow
Differentiable.pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸},
  Differentiable 𝕜 f → ∀ (n : ℕ), Differentiable 𝕜 (f ^ n)
-- Mathlib.Dynamics.FixedPoints.Support
/-- A self-map `f : X → X` has compact fixed support if its fixed support is compact.  -/
Function.HasCompactFixedSupport : {X : Type u_1} → [TopologicalSpace X] → (X → X) → Prop
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Pairwise_nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {R :
    ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl →
      ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl → Prop},
  Stream'.Seq.Pairwise R Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.Control.Random
/-- Execute `RandT m α` using the global `stdGenRef` as RNG.

Note that:
- `stdGenRef` is not necessarily properly seeded on program startup
  as of now and will therefore be deterministic.
- `stdGenRef` is not thread local, hence two threads accessing it
  at the same time will get the exact same generator.
 -/
IO.runRand : {m : Type u_1 → Type u_2} →
  {m₀ : Type → Type} →
    [Monad m] → [MonadLiftT (ST IO.RealWorld) m₀] → [ULiftable m₀ m] → {α : Type u_1} → RandT m α → m α
-- Mathlib.CategoryTheory.Category.Cat
/-- The 2-morphism in `Cat` corresponding to a natural transformation between functors.  -/
CategoryTheory.NatTrans.toCatHom₂ : {C D : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Category.{v, u} D] →
      {F G : CategoryTheory.Functor C D} → (F ⟶ G) → (F.toCatHom ⟶ G.toCatHom)
-- Mathlib.Topology.Order.LeftRightNhds
/-- In a linearly ordered commutative group with the order topology,
if `f` tends to `atTop` and `g` tends to `C` then `f * g` tends to `atTop`.  -/
Filter.Tendsto.atTop_mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α]
  [IsOrderedMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α},
  Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Mathlib.RingTheory.Ideal.Over
/-- `P` lies over `p` if `p` is the preimage of `P` by the `algebraMap`.  -/
Ideal.LiesOver : {A : Type u_2} →
  [inst : CommSemiring A] → {B : Type u_3} → [inst_1 : Semiring B] → [Algebra A B] → Ideal B → Ideal A → Prop
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
Function.Embedding.toEquivRange.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (f : α ↪ β),
  f.toEquivRange = { toFun := fun a => ⟨f a, ⋯⟩, invFun := f.invOfMemRange, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Unique
/-- `M₁(A)` is linearly equivalent to `A` as an `R`-module where `R` is a semiring.  -/
Matrix.uniqueLinearEquiv : {m : Type u_1} →
  {n : Type u_2} →
    {A : Type u_3} →
      {R : Type u_4} →
        [Unique m] →
          [Unique n] → [inst : Semiring R] → [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → Matrix m n A ≃ₗ[R] A
-- Mathlib.Tactic.FunProp.FunctionData
/-- Turn function data back to expression.  -/
Mathlib.Meta.FunProp.FunctionData.toExpr : Mathlib.Meta.FunProp.FunctionData → Lean.MetaM Lean.Expr
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.neg_lt_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommGroup M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] {a b : M}, -a < b ↔ -b < a
-- Mathlib.Data.DFinsupp.Module
DFinsupp.subtypeDomainLinearMap_apply : ∀ {ι : Type u} (γ : Type w) (β : ι → Type v) [inst : Semiring γ] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → Module γ (β i)] (p : ι → Prop) [inst_3 : DecidablePred p] (x : Π₀ (i : ι), β i),
  (DFinsupp.subtypeDomainLinearMap γ β p) x = DFinsupp.subtypeDomain p x
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inrRangeEquiv_apply_coe_snd : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : StarAddMonoid R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : Star A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A] (a : A),
  (↑((Unitization.inrRangeEquiv R A) a)).toProd.2 = a
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.mk_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cochain F G n) (m : ℤ) (hnm : n + 1 = m)
  (h : CochainComplex.HomComplex.δ n m z = 0), ↑(CochainComplex.HomComplex.Cocycle.mk z m hnm h) = z
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Given two forks with isomorphic components in such a way that the natural diagrams commute, then
one is a limit if and only if the other one is.
 -/
CategoryTheory.Limits.Fork.isLimitEquivOfIsos : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        {X' Y' : C} →
          (c : CategoryTheory.Limits.Fork f g) →
            {f' g' : X' ⟶ Y'} →
              (c' : CategoryTheory.Limits.Fork f' g') →
                (e₀ : X ≅ X') →
                  (e₁ : Y ≅ Y') →
                    (e : c.pt ≅ c'.pt) →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom)
                          CategoryTheory.Limits.Fork.isLimitEquivOfIsos._auto_1 →
                        autoParam
                            (CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom)
                            CategoryTheory.Limits.Fork.isLimitEquivOfIsos._auto_3 →
                          autoParam
                              (CategoryTheory.CategoryStruct.comp e.hom c'.ι =
                                CategoryTheory.CategoryStruct.comp c.ι e₀.hom)
                              CategoryTheory.Limits.Fork.isLimitEquivOfIsos._auto_5 →
                            CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsLimit c'
-- Init.Data.SInt.Lemmas
ISize.neg_ofInt : ∀ {n : ℤ}, -ISize.ofInt n = ISize.ofInt (-n)
-- Mathlib.CategoryTheory.Limits.Presentation
/-- The natural maps `sᵢ : Dᵢ ⟶ X`.  -/
CategoryTheory.Limits.ColimitPresentation.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          (self : CategoryTheory.Limits.ColimitPresentation J X) → self.diag ⟶ (CategoryTheory.Functor.const J).obj X
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.coe_bot : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M], ↑⊥ = ∅
-- Mathlib.CategoryTheory.Presentable.Directed
/-- Auxiliary definition for `isCardinalFiltered`.  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂ : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      [Fact κ.IsRegular] →
        {ι : Type w} →
          (D : ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ) →
            HasCardinalLT ι κ →
              {m : J} →
                ((i : ι) → (D i).top ⟶ m) → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ
-- Init.Data.Bool
Bool.false_le : ∀ (x : Bool), false ≤ x
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version within a set at a point, but with full pullback.  -/
MDifferentiableWithinAt.mpullback_vectorField_preimage : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} {t : Set M'} [inst_11 : IsManifold I 2 M]
  [inst_12 : IsManifold I' 2 M'] [CompleteSpace E],
  MDiffAt[t] (T% V) (f x₀) →
    ContMDiffAt I I' n f x₀ →
      (mfderiv% f x₀).IsInvertible → 2 ≤ n → (MDiffAt[f ⁻¹' t] fun x => ⟨x, VectorField.mpullback I I' f V x⟩) x₀
-- Aesop.Stats.Basic
Aesop.recordScriptGenerated : {m : Type → Type} → [Monad m] → [Aesop.MonadStats m] → Aesop.ScriptGenerated → m Unit
-- Mathlib.Analysis.SpecialFunctions.Arcosh
/-- The function `Real.arcosh` is real analytic.  -/
Real.analyticWithinAt_arcosh : ∀ {s : Set ℝ} {x : ℝ}, x ∈ Set.Ioi 1 → AnalyticWithinAt ℝ Real.arcosh s x
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.right : ∀ {O : Set (ℕ →. ℕ)}, Nat.RecursiveIn O fun n => ↑(some (Nat.unpair n).2)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Indep.indep_restrict_of_subset : ∀ {α : Type u_1} {M : Matroid α} {R I : Set α}, M.Indep I → I ⊆ R → (M.restrict R).Indep I
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.CancelResult.mk.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {mα : Q(Mul «$α»)} {e v : Q(«$α»)} (cancelled : Q(«$α»))
  (pf : Q(«$v» * «$e» = «$cancelled»)) (cancelled_1 : Q(«$α»)) (pf_1 : Q(«$v» * «$e» = «$cancelled_1»)),
  ({ cancelled := cancelled, pf := pf } = { cancelled := cancelled_1, pf := pf_1 }) =
    (cancelled = cancelled_1 ∧ pf = pf_1)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lift_type_eq : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s],
  Ordinal.lift.{max v w, u} (Ordinal.type r) = Ordinal.lift.{max u w, v} (Ordinal.type s) ↔ Nonempty (r ≃r s)
-- Mathlib.Algebra.Group.Support
Function.mulSupport_mul_inv : ∀ {α : Type u_1} {G : Type u_3} [inst : DivisionMonoid G] (f g : α → G),
  (Function.mulSupport fun x => f x * (g x)⁻¹) ⊆ Function.mulSupport f ∪ Function.mulSupport g
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Some types are unordered rings, so we do not process them in `linarith`.
When such types are detected in `getStructId?`, we add them to the set
`forbiddenNatModules` to avoid reprocessing them in `getNatStructId?`.
 -/
Lean.Meta.Grind.Arith.Linear.State.forbiddenNatModules : Lean.Meta.Grind.Arith.Linear.State → Lean.PHashSet Lean.Meta.Sym.ExprPtr
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_eq_one : ∀ {a : Cardinal.{v}}, Cardinal.lift.{u, v} a = 1 ↔ a = 1
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.boundedBy.eq_1 : ∀ {α : Type u_1} (m : Set α → ENNReal),
  MeasureTheory.OuterMeasure.boundedBy m = MeasureTheory.OuterMeasure.ofFunction (fun s => ⨆ (_ : s.Nonempty), m s) ⋯
-- Mathlib.CategoryTheory.Limits.Creates
/-- the lifted cone is limit  -/
CategoryTheory.LiftsToLimit.makesLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                {c : CategoryTheory.Limits.Cone (K.comp F)} →
                  {t : CategoryTheory.Limits.IsLimit c} →
                    (self : CategoryTheory.LiftsToLimit K F c t) → CategoryTheory.Limits.IsLimit self.liftedCone
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.toContinuousMap : {α : Type u} → {β : Type v} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → CocompactMap α β → C(α, β)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.eval₂_pUnitAlgEquiv : ∀ {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] {f : MvPolynomial PUnit.{u_4 + 1} R}
  {φ : R →+* S} {a : PUnit.{u_4 + 1} → S},
  Polynomial.eval₂ φ (a default) ((MvPolynomial.pUnitAlgEquiv R) f) = MvPolynomial.eval₂ φ a f
-- Init.Omega.Int
Lean.Omega.Int.natAbs_dichotomy : ∀ {a : ℤ}, 0 ≤ a ∧ ↑a.natAbs = a ∨ a < 0 ∧ ↑a.natAbs = -a
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
/-- A function `f : ℍ → α` is zero at infinity it is zero along `atImInfty`.  -/
UpperHalfPlane.IsZeroAtImInfty : {α : Type u_1} → [Zero α] → [TopologicalSpace α] → (UpperHalfPlane → α) → Prop
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
/-- **Alias** of the reverse direction of `Subgroup.normal_unop`. -/
Subgroup.Normal.unop : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup Gᵐᵒᵖ}, H.Normal → H.unop.Normal
-- Mathlib.CategoryTheory.Monad.Limits
/-- A comonadic functor creates limits if it preserves limits.  -/
CategoryTheory.comonadicCreatesLimitsOfPreservesLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (R : CategoryTheory.Functor D C) →
          [CategoryTheory.ComonadicLeftAdjoint R] →
            [CategoryTheory.Limits.PreservesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} R] →
              CategoryTheory.CreatesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} R
-- Mathlib.Topology.Algebra.OpenSubgroup
Subgroup.isOpen_of_openSubgroup : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousMul G] (H : Subgroup G)
  {U : OpenSubgroup G}, ↑U ≤ H → IsOpen ↑H
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.Preprocessor.toPreprocessorBase : Mathlib.Tactic.Linarith.Preprocessor → Mathlib.Tactic.Linarith.PreprocessorBase
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.instInhabitedHom : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} →
      (X : F.Grothendieck) → Inhabited (X.Hom X)
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxEntry?.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k : α) →
                (v : β k) →
                  (l : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf)) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (l : Std.DTreeMap.Internal.Impl α β) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β k_1) →
                            (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                              motive
                                (Std.DTreeMap.Internal.Impl.inner size k v l
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))) →
              motive x
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_freeOn : ∀ {α : Type u_1} {β : Type u_2} {E : Set α} (f : α → β) (hf : Set.InjOn f (Matroid.freeOn E).E),
  (Matroid.freeOn E).map f hf = Matroid.freeOn (f '' E)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
commGroupOfCyclicCenterQuotient.eq_1 : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] [inst_2 : IsCyclic G'] (f : G →* G')
  (hf : f.ker ≤ Subgroup.center G), commGroupOfCyclicCenterQuotient f hf = { toGroup := inst, mul_comm := ⋯ }
-- Mathlib.Order.OmegaCompletePartialOrder
/-- Eta-expanded form of `OmegaCompletePartialOrder.ωScottContinuous.comp` -/
OmegaCompletePartialOrder.ωScottContinuous.fun_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : OmegaCompletePartialOrder α]
  [inst_1 : OmegaCompletePartialOrder β] [inst_2 : OmegaCompletePartialOrder γ] {f : α → β} {g : β → γ},
  OmegaCompletePartialOrder.ωScottContinuous g →
    OmegaCompletePartialOrder.ωScottContinuous f → OmegaCompletePartialOrder.ωScottContinuous fun x => g (f x)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.surjOn_logb : ∀ {b : ℝ}, 0 < b → b ≠ 1 → Set.SurjOn (Real.logb b) (Set.Ioi 0) Set.univ
-- Lean.Elab.Do.Legacy
/-- Return a code block that executes `terminal` and then `k` with the value produced by `terminal`.
This method assumes `terminal` is a terminal  -/
Lean.Elab.Term.Do.concat : Lean.Elab.Term.Do.CodeBlock →
  Lean.Syntax →
    Option Lean.Elab.Term.Do.Var → Lean.Elab.Term.Do.CodeBlock → Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock
-- Mathlib.Algebra.Group.TypeTags.Hom
AddMonoidHom.toMultiplicative_add : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddCommMonoid N] (f g : M →+ N),
  AddMonoidHom.toMultiplicative (f + g) = AddMonoidHom.toMultiplicative f * AddMonoidHom.toMultiplicative g