mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.MonadicRightAdjoint.eqv : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {R : CategoryTheory.Functor D C} [self : CategoryTheory.MonadicRightAdjoint R],
  (CategoryTheory.Monad.comparison CategoryTheory.MonadicRightAdjoint.adj).IsEquivalence
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.ofPermHom_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)),
  (a.ofPermHom τ).support = (↑τ).support.biUnion fun c => (↑c).support
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabFootnote.mk : Lean.StrLit → Lean.Doc.ElabFootnote✝
-- Lean.Environment
/-- Set the current state of the given extension in the given environment.  -/
Lean.PersistentEnvExtension.setState : {α β σ : Type} → Lean.PersistentEnvExtension α β σ → Lean.Environment → σ → Lean.Environment
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.instSliceableRooSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.instSliceableRooSlice._auto_1) →
      Std.Roo.Sliceable (Std.DTreeMap α β cmp) α (Std.DTreeMap.Internal.RooSlice α β)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.opFunctor_map_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : (CategoryTheory.Square C)ᵒᵖ} (φ : X ⟶ Y),
  (CategoryTheory.Square.opFunctor.map φ).τ₂ = φ.unop.τ₂.op
-- Mathlib.Data.ENNReal.Real
ENNReal.zero_eq_ofReal : ∀ {p : ℝ}, 0 = ENNReal.ofReal p ↔ p ≤ 0
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ioc_toDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (b a : α),
  Finset.Ioc (OrderDual.toDual b) (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ico a b)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
Eventually.le_linearGrowthInf : ∀ {u : ℕ → EReal} {a : EReal}, (∀ᶠ (n : ℕ) in Filter.atTop, a * ↑n ≤ u n) → a ≤ LinearGrowth.linearGrowthInf u
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The vector from a vertex to the corresponding `faceOppositeCentroid` equals the average of the
displacements to the other vertices.  -/
Affine.Simplex.faceOppositeCentroid_vsub_point_eq_smul_sum_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.faceOppositeCentroid i -ᵥ s.points i = (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i)
-- Mathlib.Algebra.Order.SuccPred
Order.IsPredLimit.lt_sub_natCast : ∀ {α : Type u_1} {x y : α} [inst : PartialOrder α] [inst_1 : AddCommGroupWithOne α] [PredSubOrder α],
  Order.IsPredLimit x → x < y → ∀ (n : ℕ), x < y - ↑n
-- Batteries.Data.Vector.Lemmas
Vector.scanr_map : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {n : ℕ} {init : γ} {f : β → γ → γ} {g : α → β} {as : Vector α n},
  Vector.scanr f init (Vector.map g as) = Vector.scanr (fun x acc => f (g x) acc) init as
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.im_inner_adjoint_mul_self_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (x : E), RCLike.im (inner 𝕜 x ((LinearMap.adjoint T) (T x))) = 0
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
SemiconjBy.tsum_left : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : TopologicalSpace α] [IsTopologicalSemiring α] {f : ι → α} [T2Space α] [L.NeBot] {a b : α},
  (∀ (i : ι), SemiconjBy (f i) a b) → SemiconjBy (∑'[L] (i : ι), f i) a b
-- Mathlib.Algebra.Group.Even
/-- **Alias** of the reverse direction of `even_neg`. -/
Even.neg : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {a : α}, Even a → Even (-a)
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.instInhabitedConfig.default : Lean.Meta.Sym.Simp.Config
-- Mathlib.Analysis.Asymptotics.TVS
/-- The definition of `IsBigOTVS` says that
for each neighborhood `U` of the origin in the codomain of `f`,
there exists a neighborhood `V` of the origin in the codomain of `g` such that
`egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)` eventually along `l`.

This lemma shows that it suffices to make this inequality work up to a constant multiplier.  -/
Asymptotics.IsBigOTVS.of_egauge_le_mul : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousConstSMul 𝕜 F]
  {ι : Sort u_7} {p : ι → Prop} {U : ι → Set E},
  (nhds 0).HasBasis p U →
    (∀ (i : ι), p i → ∃ C, ∃ V ∈ nhds 0, (fun x => egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x => ↑C * egauge 𝕜 V (g x)) →
      f =O[𝕜; l] g
-- Mathlib.GroupTheory.Perm.List
List.formPerm_rotate_one : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → (l.rotate 1).formPerm = l.formPerm
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasSeparator.hasCoseparator_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.HasSeparator C],
  CategoryTheory.HasCoseparator Cᵒᵖ
-- Mathlib.Order.Basic
LinearOrder.toPartialOrder_injective : ∀ {α : Type u_2}, Function.Injective (@LinearOrder.toPartialOrder α)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited γ] {f : α → β → γ} {k : α},
  t.WF → (Std.TreeMap.Raw.map f t)[k]! = (Option.map (f k) t[k]?).get!
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_reverse_zero_cons : ∀ {b : ℕ} (l : List ℕ), Nat.ofDigits b (0 :: l).reverse = Nat.ofDigits b l.reverse
-- Mathlib.Analysis.Normed.Group.Defs
/-- the `ℝ≥0∞`-valued norm function.  -/
ENorm.enorm : {E : Type u_8} → [self : ENorm E] → E → ENNReal
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.IsUniform.aemeasurable : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} {x : MeasurableSpace Ω}
  {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E},
  μ s ≠ 0 → μ s ≠ ⊤ → MeasureTheory.pdf.IsUniform X s ℙ μ → AEMeasurable X ℙ
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.and_right : ∀ (lhs rhs : Bool), (lhs && rhs) = true → rhs = true
-- Mathlib.Algebra.Quaternion
/-- Show the quaternion `⟨w, x, y, z⟩` as a string `"{ re := w, imI := x, imJ := y, imK := z }"`.

For the typical case of quaternions over ℝ, each component will show as a Cauchy sequence due to
the way Real numbers are represented.
 -/
Cardinal.instReprQuaternionAlgebra : {R : Type u_1} → [Repr R] → {a b c : R} → Repr (QuaternionAlgebra R a b c)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.insertEntryIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)),
  Std.Internal.List.insertEntryIfNew k v l = bif Std.Internal.List.containsKey k l then l else ⟨k, v⟩ :: l
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Div-mul-div version.  -/
Finset.ruzsa_triangle_inequality_div_mul_div : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : CommGroup G] (A B C : Finset G),
  (A / C).card * B.card ≤ (A * B).card * (B / C).card
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.sub_right : ∀ {R₁ : Type u_4} {M₁ : Type u_5} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B₁ : LinearMap.BilinForm R₁ M₁} (x y z : M₁), (B₁ x) (y - z) = (B₁ x) y - (B₁ x) z
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.sum.of : ∀ {α : Type u} [inst : AddGroup α] {x : α}, FreeAddGroup.sum (FreeAddGroup.of x) = x
-- Mathlib.Algebra.Homology.ComplexShape
/-- An arbitrary choice of index `j` such that `Rel i j`, if such exists.
Returns `i` otherwise.
 -/
ComplexShape.next : {ι : Type u_1} → ComplexShape ι → ι → ι
-- Mathlib.Logic.Small.Basic
/-- This can be seen as a version of `small_of_surjective` in which the function `f` doesn't
actually land in `β` but in some larger type `γ` related to `β` via an injective function `g`.
 -/
small_of_injective_of_exists : ∀ {α : Type v} {β : Type w} {γ : Type v'} [Small.{u, v} α] (f : α → γ) {g : β → γ},
  Function.Injective g → (∀ (b : β), ∃ a, f a = g b) → Small.{u, w} β
-- Mathlib.Data.Set.MulAntidiagonal
Set.AddAntidiagonal.eq_of_fst_eq_fst : ∀ {α : Type u_1} [inst : AddCommMonoid α] [IsCancelAdd α] {s t : Set α} {a : α} {x y : ↑(s.antidiagonal t a)},
  (↑x).1 = (↑y).1 → x = y
-- Init.Data.List.Count
List.countP_flatten : ∀ {α : Type u_1} {p : α → Bool} {l : List (List α)}, List.countP p l.flatten = (List.map (List.countP p) l).sum
-- Init.Data.Random
/-- The next value from a `StdGen`, paired with an updated generator state.
 -/
stdNext : StdGen → ℕ × StdGen
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyMapIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  (CategoryTheory.ShortComplex.homologyMapIso e).hom = CategoryTheory.ShortComplex.homologyMap e.hom
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange.zeroHom_apply : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N) (g : ι →₀ M),
  (Finsupp.mapRange.zeroHom f) g = Finsupp.mapRange ⇑f ⋯ g
-- Mathlib.Data.Nat.Choose.Multinomial
Multiset.countPerms.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), m.countPerms = (Multiset.toFinsupp m).multinomial
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.lift_X_left : ∀ {R : Type u_1} [inst : CommRing R] (P : StandardEtalePair R), P.lift P.X ⋯ = AlgHom.id R P.Ring
-- Init.Data.BitVec.Basic
/-- Unsigned less-than-or-equal-to for bitvectors.

SMT-LIB name: `bvule`.
 -/
BitVec.ule : {n : ℕ} → BitVec n → BitVec n → Bool
-- Mathlib.Order.Lattice
inf_le_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, min b c ≤ a ↔ b ≤ a ∨ c ≤ a
-- Init.Data.Array.Find
Array.findFinIdx?_eq_none_iff : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, Array.findFinIdx? p xs = none ↔ ∀ x ∈ xs, ¬p x = true
-- Init.Data.SInt.Bitwise
Int32.xor_zero : ∀ {a : Int32}, a ^^^ 0 = a
-- Batteries.Util.ProofWanted
/-- The keyword used in the `Try this:` suggestion and in the error message when a body has
no `❰…❱` reference. `instance_wanted` → `instance`, `theorem_wanted` / `proof_wanted` → `theorem`,
`def_wanted` → `def`.  -/
_private.Batteries.Util.ProofWanted.0.WantedCmdKind.fallbackKeyword : WantedCmdKind✝ → String
-- Init.Grind.Norm
Lean.Grind.flip_bool_eq : ∀ (a b : Bool), (a = b) = (b = a)
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- `#rw?? e` gives all possible rewrites of `e`. It is a testing command for the `rw??` tactic  -/
Mathlib.Tactic.LibraryRewrite.rw??Command : Lean.ParserDescr
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.comm_trans_rTensorOne : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M : Submodule R S),
  TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne = M.lTensorOne
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m m_1 : Std.DHashMap.Raw α β),
  m = m_1 → ∀ (a : α) (fallback fallback_1 : β a), fallback = fallback_1 → m.getD a fallback = m_1.getD a fallback_1
-- Mathlib.Order.Hom.Basic
OrderIso.ofHomInv_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (g : β →o α)
  (h₁ : f.comp g = OrderHom.id) (h₂ : g.comp f = OrderHom.id) (a : β), (OrderIso.ofHomInv f g h₁ h₂).symm a = g a
-- Init.Data.BitVec.Basic
BitVec.getLsbD_eq_getElem : ∀ {w : ℕ} {x : BitVec w} {i : ℕ} (h : i < w), x.getLsbD i = x[i]
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fractRestrict_surjective : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι], Function.Surjective (ZSpan.fractRestrict b)
-- Init.Grind.Module.Basic
/-- Scalar multiplication is distributive over addition in the integers.  -/
Lean.Grind.IntModule.add_zsmul : ∀ {M : Type u} [self : Lean.Grind.IntModule M] (n m : ℤ) (a : M), (n + m) • a = n • a + m • a
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosure.isAlgClosed : ∀ (R : Type u) {K : Type v} {inst : CommRing R} {inst_1 : Field K} {inst_2 : Algebra R K}
  {inst_3 : Module.IsTorsionFree R K} [self : IsAlgClosure R K], IsAlgClosed K
-- Mathlib.Data.Nat.Multiplicity
/-- A lower bound on the multiplicity of `p` in `choose n k`.  -/
Nat.Prime.emultiplicity_le_emultiplicity_choose_add : ∀ {p : ℕ}, Nat.Prime p → ∀ (n k : ℕ), emultiplicity p n ≤ emultiplicity p (n.choose k) + emultiplicity p k
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.congr_simp : ∀ (L : Type u) [inst : CommRing L] [inst_1 : IsDomain L] {n : ℕ} [inst_2 : NeZero n]
  (hn : Nat.card ↥(rootsOfUnity n L) = n), modularCyclotomicCharacter L hn = modularCyclotomicCharacter L hn
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- If `μ` on `G ⧸ Γ` satisfies `AddQuotientMeasureEqMeasurePreimage` relative to a
both left- and right-invariant measure on `G` and `Γ` is a normal subgroup, then `μ` is a
left-invariant measure.  -/
MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addInvariantMeasure_quotient : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] [PolishSpace G] {Γ : AddSubgroup G} [inst_6 : Γ.Normal] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} (ν : MeasureTheory.Measure G)
  [ν.IsAddLeftInvariant] [hasFun : MeasureTheory.HasAddFundamentalDomain (↥Γ.op) G ν]
  [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ], μ.IsAddLeftInvariant
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Submodule.mem_toNonUnitalSubalgebra : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {p : Submodule R A} {h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p} {x : A},
  x ∈ p.toNonUnitalSubalgebra h_mul ↔ x ∈ p
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instZPow.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → DivInvMonoid (R i)] [inst_2 : ∀ (i : ι), SubgroupClass (S i) (R i)],
  RestrictedProduct.instZPow R = { pow := fun x n => ⟨fun i => x i ^ n, ⋯⟩ }
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.strictPeriods.eq_1 : ∀ {R : Type u_1} [inst : Ring R] (𝒢 : Subgroup (GL (Fin 2) R)),
  𝒢.strictPeriods = AddSubgroup.comap Matrix.GeneralLinearGroup.upperRightHom.toAddMonoidHom (Subgroup.toAddSubgroup 𝒢)
-- Lean.Elab.MutualDef
Lean.Elab.Term.elabMutualDef : Array Lean.Expr → Lean.Elab.Command.Scope → Array Lean.Elab.DefView → Lean.Elab.TermElabM Unit
-- Mathlib.Analysis.Convex.GaugeRescale
continuous_gaugeRescale : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E] [T1Space E] {s t : Set E},
  Convex ℝ s → s ∈ nhds 0 → Convex ℝ t → t ∈ nhds 0 → Bornology.IsVonNBounded ℝ t → Continuous (gaugeRescale s t)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
instNonemptyUniformOnFun : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Nonempty β], Nonempty (UniformOnFun α β 𝔖)
-- Init.Prelude
/-- Unsigned integers that are the size of a word on the platform's architecture.

On a 32-bit architecture, `USize` is equivalent to `UInt32`. On a 64-bit machine, it is equivalent
to `UInt64`.
 -/
USize : Type
-- Mathlib.CategoryTheory.Generator.Preadditive
CategoryTheory.Preadditive.isCoseparating_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (P : CategoryTheory.ObjectProperty C),
  P.IsCoseparating ↔
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), P G → ∀ (h : Y ⟶ G), CategoryTheory.CategoryStruct.comp f h = 0) → f = 0
-- Mathlib.Order.DirSupClosed
DirSupInacc.empty : ∀ {α : Type u_1} [inst : Preorder α], DirSupInacc ∅
-- Std.Async.Select
Std.Async.Selector.mk.inj : ∀ {α : Type} {tryFn : Std.Async.Async (Option α)} {registerFn : Std.Async.Waiter α → Std.Async.Async Unit}
  {unregisterFn : Std.Async.Async Unit} {tryFn_1 : Std.Async.Async (Option α)}
  {registerFn_1 : Std.Async.Waiter α → Std.Async.Async Unit} {unregisterFn_1 : Std.Async.Async Unit},
  { tryFn := tryFn, registerFn := registerFn, unregisterFn := unregisterFn } =
      { tryFn := tryFn_1, registerFn := registerFn_1, unregisterFn := unregisterFn_1 } →
    tryFn = tryFn_1 ∧ registerFn = registerFn_1 ∧ unregisterFn = unregisterFn_1
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mem_ballSubgroup_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a : M}
  {c : MulArchimedeanClass M}, c ≠ ⊤ → (a ∈ c.ballSubgroup ↔ c < MulArchimedeanClass.mk a)
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_add_emod_self_right : ∀ (a b c : ℤ), (a * b + c) % b = c % b
-- Mathlib.Combinatorics.SimpleGraph.Density
/-- If `s₂ ⊆ s₁`, `t₂ ⊆ t₁` and they take up all but a `δ`-proportion, then the difference in edge
densities is at most `2 * δ`.  -/
Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul : ∀ {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  (r : α → β → Prop) [inst_3 : (a : α) → DecidablePred (r a)] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} {δ : 𝕜},
  s₂ ⊆ s₁ →
    t₂ ⊆ t₁ →
      0 ≤ δ →
        (1 - δ) * ↑s₁.card ≤ ↑s₂.card →
          (1 - δ) * ↑t₁.card ≤ ↑t₂.card → |↑(Rel.edgeDensity r s₂ t₂) - ↑(Rel.edgeDensity r s₁ t₁)| ≤ 2 * δ
-- Aesop.Check
Aesop.Check.script.steps : Aesop.Check
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_map_eq_of_isEquivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty C) [P.RespectsIso] (F : CategoryTheory.Functor C D) [F.IsEquivalence],
  (P.map F).inverseImage F = P
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.minKeyD_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).isEmpty = false →
        ∀ {fallback : α},
          (Std.DTreeMap.Raw.Const.alter t k f).minKeyD fallback = k ↔
            (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.iSup_subcomplex_eq_top : ∀ (X : SSet), ⨆ s, s.subcomplex = ⊤
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_lt_ediv_iff_of_dvd_of_neg_of_neg : ∀ {a b c d : ℤ}, b < 0 → d < 0 → b ∣ a → d ∣ c → (a / b < c / d ↔ d * a < c * b)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (f : ↑(X.presheaf.obj (Opposite.op U))) {V : X.Opens} (i : V ⟶ U),
      V = X.basicOpen f → IsLocalization.Away f ↑(X.presheaf.obj (Opposite.op V))
-- Mathlib.Algebra.Star.Basic
/-- `star` as a `RingEquiv` from `R` to `Rᵐᵒᵖ`  -/
starRingEquiv : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → [StarRing R] → R ≃+* Rᵐᵒᵖ
-- Mathlib.Data.Finsupp.Defs
Finsupp.embDomain_refl : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M], Finsupp.embDomain (Function.Embedding.refl α) = id
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_eq_default : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a : α}, a ∉ t → Std.DTreeMap.Raw.Const.get! t a = default
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticOn.log : ∀ {f : ℝ → ℝ} {s : Set ℝ}, AnalyticOn ℝ f s → (∀ x ∈ s, 0 < f x) → AnalyticOn ℝ (fun z => Real.log (f z)) s
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.algebraMap_ringEquiv_apply : ∀ (G : Type u_1) (A : Type u_2) (A' : Type u_3) (B : Type u_4) [inst : Group G] [inst_1 : CommSemiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B] [hA : IsGaloisGroup G A B]
  [inst_5 : FaithfulSMul A B] [inst_6 : CommSemiring A'] [inst_7 : Algebra A' B] [inst_8 : FaithfulSMul A' B]
  [hA' : IsGaloisGroup G A' B] (x : A), (algebraMap A' B) ((IsGaloisGroup.ringEquiv G A A' B) x) = (algebraMap A B) x
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
/-- There is a unique `GoodProducts` for the singleton `{fun _ ↦ false}`.  -/
Profinite.NobelingProof.instUniqueSubtypeProductsIsGoodSingletonForallBoolSetFalse : {I : Type u} → [inst : LinearOrder I] → Unique { l // Profinite.NobelingProof.Products.isGood {fun x => false} l }
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.entryAtIdxD.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → ℕ → α × β → Sort u_3) (size : ℕ)
  (k : α) (v : β) (l r : Std.DTreeMap.Internal.Impl α fun x => β) (n : ℕ) (fallback : α × β)
  (h_1 : (x : ℕ) → (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf x fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (n : ℕ) → (fallback : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l r, n, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, x, fallback => h_1 x fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n, fallback => h_2 size k v l r n fallback) =
    h_2 size k v l r n fallback
-- Mathlib.Algebra.QuaternionBasis
/-- The third imaginary unit  -/
QuaternionAlgebra.Basis.k : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] → [inst_2 : Algebra R A] → {c₁ c₂ c₃ : R} → QuaternionAlgebra.Basis A c₁ c₂ c₃ → A
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- The vertex set  -/
Hypergraph.vertexSet : {α : Type u_4} → Hypergraph α → Set α
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.u : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Year.Offset
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_minKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : l.isEmpty = false}, Std.Internal.List.containsKey (Std.Internal.List.minKey l he) l = true
-- Mathlib.RingTheory.WittVector.MulP
WittVector.wittMulN.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] (a a_1 : ℕ),
  a = a_1 → ∀ (a_2 a_3 : ℕ), a_2 = a_3 → WittVector.wittMulN p a a_2 = WittVector.wittMulN p_1 a_1 a_3
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_permCongr : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  (e : α ≃ β) (p : Equiv.Perm α), Equiv.Perm.sign (e.permCongr p) = Equiv.Perm.sign p
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_neg' : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (f : α → G), ∫ (a : α), (-f) a ∂μ = -∫ (a : α), f a ∂μ