mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.instEvalExprReduceConfig.evalExpr : Lean.Expr → Lean.MetaM Lean.Meta.Command.ReduceConfig
-- Mathlib.Algebra.BigOperators.Ring.Finset
Nat.cast_prod : ∀ {R : Type u_4} {ι : Type u_5} [inst : CommSemiring R] (f : ι → ℕ) (s : Finset ι), ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.Topology.Semicontinuity.Defs
upperHemicontinuousAt_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α},
  UpperHemicontinuousAt f x ↔ ∀ t ∈ nhdsSet (f x), ∀ᶠ (x' : α) in nhds x, t ∈ nhdsSet (f x')
-- Mathlib.Data.NNReal.Defs
Real.natCastle_toNNReal' : ∀ {n : ℕ} {r : ℝ}, ↑n ≤ r.toNNReal ↔ ↑n ≤ r ∨ n = 0
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_nat : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddMonoidWithOne G]
  [inst_2 : AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ), f ↑n = f 0 + ↑n
-- Aesop.Rule.Name
Aesop.ScopeName.instToString : ToString Aesop.ScopeName
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- **Constructive Church-Rosser theorem** (compare `FreeAddGroup.Red.church_rosser`).  -/
FreeAddGroup.reduce.churchRosser : {α : Type u_1} →
  {L₁ L₂ L₃ : List (α × Bool)} →
    [DecidableEq α] →
      FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₁ L₃ → { L₄ // FreeAddGroup.Red L₂ L₄ ∧ FreeAddGroup.Red L₃ L₄ }
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux1.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Option (Computation α))) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (S' : Stream'.Seq (Option (Computation α))) → motive (some (none, S')))
  (h_3 : (c : Computation α) → (S' : Stream'.Seq (Option (Computation α))) → motive (some (some c, S'))),
  (match none with
    | none => h_1 ()
    | some (none, S') => h_2 S'
    | some (some c, S') => h_3 c S') =
    h_1 ()
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.isGrothendieckAbelian_sheaf_affineEtaleTopology : ∀ (S : AlgebraicGeometry.Scheme) (A : Type u') [inst : CategoryTheory.Category.{u, u'} A] {FA : A → A → Type u_1}
  {CD : A → Type u} [inst_1 : (X Y : A) → FunLike (FA X Y) (CD X) (CD Y)]
  [inst_2 : CategoryTheory.ConcreteCategory A FA]
  [inst_3 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
  [inst_4 : CategoryTheory.Limits.HasColimits A] [inst_5 : CategoryTheory.Limits.HasLimits A]
  [inst_6 : (CategoryTheory.forget A).ReflectsIsomorphisms]
  [inst_7 : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1} (CategoryTheory.forget A)]
  [inst_8 : CategoryTheory.Abelian A] [CategoryTheory.IsGrothendieckAbelian.{u, u, u'} A],
  CategoryTheory.IsGrothendieckAbelian.{u, u + 1, max (max u' (u + 1)) u}
    (CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.AffineEtale.topology S) A)
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.truncate.go : ℕ → Lean.Name → Lean.Name × ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map'_comp_map : ∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C} {g h : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g]
  [inst_3 : CategoryTheory.Limits.HasProduct h] (p : β → α) (q : (b : β) → f (p b) ⟶ g b) (q' : (b : β) → g b ⟶ h b),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.Limits.Pi.map q') =
    CategoryTheory.Limits.Pi.map' p fun b => CategoryTheory.CategoryStruct.comp (q b) (q' b)
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.Nonempty.zero_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : Zero α] [inst_2 : Zero β] [inst_3 : SMulWithZero α β]
  {t : Finset β}, t.Nonempty → 0 • t = 0
-- Mathlib.RingTheory.DualNumber
DualNumber.isNilpotent_iff_eps_dvd : ∀ {R : Type u_1} [inst : DivisionSemiring R] {x : DualNumber R}, IsNilpotent x ↔ DualNumber.eps ∣ x
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.AddMagmaCat.Hom.mk.inj : ∀ {A B : AddMagmaCat} {hom' hom'_1 : ↑A →ₙ+ ↑B}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Returns the maximum element of the tree, or panics if the tree is empty.  -/
RBTree.RBSet.max! : {α : Type u_1} → {cmp : α → α → Ordering} → [Inhabited α] → RBTree.RBSet α cmp → α
-- Mathlib.CategoryTheory.Join.Pseudofunctor
/-- The structural isomorphism for composition of `pseudofunctorLeft`.  -/
CategoryTheory.Join.mapCompLeft : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      (D : Type u_4) →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (F : CategoryTheory.Functor A B) →
                  (G : CategoryTheory.Functor B C) →
                    CategoryTheory.Join.mapPair (F.comp G) (CategoryTheory.Functor.id D) ≅
                      (CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id D)).comp
                        (CategoryTheory.Join.mapPair G (CategoryTheory.Functor.id D))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ \ t₂).getKey? k = none
-- Mathlib.Data.Finsupp.Order
Finsupp.sum_nonneg' : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ : ι → α → β}, (∀ (i : ι), 0 ≤ h₁ i (f i)) → 0 ≤ f.sum h₁
-- Init.Data.UInt.Bitwise
UInt32.toUSize_shiftLeft : ∀ (a b : UInt32), (a <<< b).toUSize = a.toUSize <<< (b % 32).toUSize % 4294967296
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the largest key that is less than the given key,
returning `none` if no such key exists.
 -/
Std.DTreeMap.Raw.getKeyLT? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → Option α
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.mk : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                [inst_6 : CategoryTheory.Pretriangulated C] →
                  (ω₁ : CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C) →
                    (δ' :
                        (CategoryTheory.ComposableArrows.functorArrows ι 1 2 2
                                CategoryTheory.Triangulated.SpectralObject._proof_2
                                CategoryTheory.Triangulated.SpectralObject._proof_4).comp
                            ω₁ ⟶
                          (CategoryTheory.ComposableArrows.functorArrows ι 0 1 2
                                CategoryTheory.Triangulated.SpectralObject._proof_6
                                CategoryTheory.Triangulated.SpectralObject._proof_2).comp
                            (ω₁.comp (CategoryTheory.shiftFunctor C 1))) →
                      (∀ (D : CategoryTheory.ComposableArrows ι 2),
                          CategoryTheory.Pretriangulated.Triangle.mk
                              (ω₁.map
                                ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2
                                      CategoryTheory.Triangulated.SpectralObject._proof_6
                                      CategoryTheory.Triangulated.SpectralObject._proof_8
                                      CategoryTheory.Triangulated.SpectralObject._proof_10
                                      CategoryTheory.Triangulated.SpectralObject._proof_2
                                      CategoryTheory.Triangulated.SpectralObject._proof_4).app
                                  D))
                              (ω₁.map
                                ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2
                                      CategoryTheory.Triangulated.SpectralObject._proof_8
                                      CategoryTheory.Triangulated.SpectralObject._proof_2
                                      CategoryTheory.Triangulated.SpectralObject._proof_6
                                      CategoryTheory.Triangulated.SpectralObject._proof_4
                                      CategoryTheory.Triangulated.SpectralObject._proof_4).app
                                  D))
                              (δ'.app D) ∈
                            CategoryTheory.Pretriangulated.distinguishedTriangles) →
                        CategoryTheory.Triangulated.SpectralObject C ι
-- Mathlib.Algebra.Star.Unitary
Unitary.isUnit_coe : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : ↥(unitary R)}, IsUnit ↑U
-- Init.Data.Nat.Lemmas
Nat.mul_lt_mul'' : ∀ {a b c d : ℕ}, a < c → b < d → a * b < c * d
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instReprZoneRules.repr : Std.Time.TimeZone.ZoneRules → ℕ → Std.Format
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- Every functor indexing a wide (co)equalizer is naturally isomorphic (actually, equal) to a
`parallelFamily`  -/
CategoryTheory.Limits.diagramIsoParallelFamily : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C) →
        F ≅ CategoryTheory.Limits.parallelFamily fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_roc : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : LE α]
  [inst_5 : DecidableLE α] [inst_6 : LT α] [inst_7 : Std.PRange.UpwardEnumerable α] [inst_8 : Std.Rxc.IsAlwaysFinite α]
  [inst_9 : Std.PRange.LawfulUpwardEnumerable α] [inst_10 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_11 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Roc α} {init : β} {f : α → β → m (ForInStep β)}
  (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instZero.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α], UpperSet.instZero = { zero := UpperSet.Ici 0 }
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.Receiver.mk : {α : Type} → Std.Bounded.Receiver✝ α → Std.Broadcast.Receiver α
-- Std.Data.ExtTreeMap.Basic
/-- Extensional tree maps.

A tree map stores an assignment of keys to values. It depends on a comparator function that
defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval
of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function `cmp` should satisfy
certain laws that ensure a consistent ordering:

* If `a` is less than (or equal) to `b`, then `b` is greater than (or equal) to `a`
and vice versa (see the `OrientedCmp` typeclass).
* If `a` is less than or equal to `b` and `b` is, in turn, less than or equal to `c`, then `a`
is less than or equal to `c` (see the `TransCmp` typeclass).

Keys for which `cmp a b = Ordering.eq` are considered the same, i.e., there can be only one entry
with key either `a` or `b` in a tree map. Looking up either `a` or `b` always yields the same entry,
if any is present.

To avoid expensive copies, users should make sure that the tree map is used linearly.

Internally, the tree maps are represented as size-bounded trees, a type of self-balancing binary
search tree with efficient order statistic lookups.

In contrast to regular tree maps, `Std.ExtTreeMap` offers several extensionality lemmas
and therefore has more lemmas about equality of tree maps. This doesn't affect the amount of
supported functions though: `Std.ExtTreeMap` supports all operations from `Std.TreeMap`.

In order to use most functions, a `TransCmp` instance is required. This is necessary to make sure
that the functions are congruent, i.e. equivalent tree maps as parameters produce equivalent return
values.

These tree maps contain a bundled well-formedness invariant, which means that they cannot
be used in nested inductive types. For these use cases, `Std.TreeMap.Raw` and
`Std.TreeMap.Raw.WF` unbundle the invariant from the tree map. When in doubt, prefer
`ExtTreeMap` over `TreeMap.Raw`.
 -/
Std.ExtTreeMap : (α : Type u) → Type v → autoParam (α → α → Ordering) Std.ExtTreeMap._auto_1 → Type (max u v)
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
/-- Given a functor `F : Jᵒᵖ ⥤ Type v` where `J` is a well-ordered type, this data
allows to construct a section of `F` from an element in `F.obj (op ⊥)`,
see `WellOrderInductionData.sectionsMk`.  -/
CategoryTheory.Functor.WellOrderInductionData : {J : Type u} → [inst : LinearOrder J] → [SuccOrder J] → CategoryTheory.Functor Jᵒᵖ (Type v) → Type (max u v)
-- Std.Http.Data.Response
/-- Creates a new HTTP Response builder with the 503 status code.
 -/
Std.Http.Response.serviceUnavailable : Std.Http.Response.Builder
-- Mathlib.Data.WSeq.Defs
/-- `union s1 s2` is a weak sequence which interleaves `s1` and `s2` in
some order (nondeterministically).  -/
Stream'.WSeq.union : {α : Type u} → Stream'.WSeq α → Stream'.WSeq α → Stream'.WSeq α
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.trans_eventuallyEq : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f : α → E}
  {g₁ g₂ : α → F}, f =O[l] g₁ → g₁ =ᶠ[l] g₂ → f =O[l] g₂
-- Mathlib.CategoryTheory.Elements
CategoryTheory.Functor.Elements.essentiallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w))
  [CategoryTheory.EssentiallySmall.{w, v, u} C], CategoryTheory.EssentiallySmall.{w, v, max u w} F.Elements
-- Mathlib.GroupTheory.FinitelyPresentedGroup
AddSubgroup.IsFinitelyNormallyGenerated.of_FG : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [N.Normal] [h : AddGroup.FG ↥N], N.IsFinitelyNormallyGenerated
-- Mathlib.Order.CompleteLattice.Basic
iSup_exists : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {p : ι → Prop} {f : Exists p → α},
  ⨆ (x : Exists p), f x = ⨆ i, ⨆ (h : p i), f ⋯
-- Lean.Elab.App
/-- Auxiliary method for field notation. Tries to add `e` as a new argument to `args` or `namedArgs`.
This method first finds the parameter with a type of the form `(baseName ...)`.
When the parameter is found, if it an explicit one and `args` is big enough, we add `e` to `args`.
Otherwise, if there isn't another parameter with the same name, we add `e` to `namedArgs`.

Remark: `fullName` is the name of the resolved "field" access function. It is used for reporting errors
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.addLValArg : Lean.Name →
  Lean.Expr →
    Array Lean.Elab.Term.Arg →
      Array Lean.Elab.Term.NamedArg →
        Lean.Expr → Bool → Lean.MetaM (Array Lean.Elab.Term.Arg × Array Lean.Elab.Term.NamedArg)
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.NoetherianSpace.inter_of_left : ∀ {α : Type u_1} [inst : TopologicalSpace α] (W V : Set α) [TopologicalSpace.NoetherianSpace ↑W],
  TopologicalSpace.NoetherianSpace ↑(W ∩ V)
-- Mathlib.Data.List.Forall2
List.SublistForall₂.below : {α : Type u_1} →
  {β : Type u_2} →
    {R : α → β → Prop} →
      {motive : (a : List α) → (a_1 : List β) → List.SublistForall₂ R a a_1 → Prop} →
        {a : List α} → {a_1 : List β} → List.SublistForall₂ R a a_1 → Prop
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
/-- Lebesgue dominated convergence theorem for filters with a countable basis  -/
MeasureTheory.tendsto_integral_filter_of_dominated_convergence : ∀ {α : Type u_1} {G : Type u_3} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_4} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → α → G} {f : α → G}
  (bound : α → ℝ),
  (∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F n) μ) →
    (∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ →
        (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) l (nhds (f a))) →
          Filter.Tendsto (fun n => ∫ (a : α), F n a ∂μ) l (nhds (∫ (a : α), f a ∂μ))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- The type of sections of a presheaf of modules.  -/
PresheafOfModules.sections : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → PresheafOfModules R → Type (max u₁ v)
-- Init.Data.Array.Lex.Lemmas
Array.lt_of_le_of_lt' : ∀ {α : Type u_1} [inst : LT α] [i₁ : Std.Asymm fun x1 x2 => x1 < x2] [i₂ : Std.Trichotomous fun x1 x2 => x1 < x2]
  [i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2] {xs ys zs : Array α},
  xs ≤ ys → ys < zs → xs < zs
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Finset.mulIndicator_biUnion_apply : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [inst : CommMonoid β] (s : Finset ι) (t : ι → Set κ) {f : κ → β},
  (↑s).PairwiseDisjoint t → ∀ (x : κ), (⋃ i ∈ s, t i).mulIndicator f x = ∏ i ∈ s, (t i).mulIndicator f x
-- Init.Data.Range.Polymorphic.IntLemmas
Int.size_toArray_rco : ∀ {a b : ℤ}, (a...b).toArray.size = (b - a).toNat
-- Mathlib.Algebra.Algebra.Basic
IsDomain.of_faithfulSMul : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  [IsDomain A], IsDomain R
-- Mathlib.Geometry.Manifold.Instances.Icc
oneTangentSpaceIcc_def : ∀ {x y : ℝ} [h : Fact (x < y)] (z : ↑(Set.Icc x y)),
  oneTangentSpaceIcc z = (mfderiv[Set.Icc x y] (Set.projIcc x y ⋯) ↑z) 1
-- Mathlib.Algebra.GroupWithZero.Submonoid.Instances
MonoidWithZeroHom.instMonoidWithZeroSubtypeMemSubmonoidMrange : {G : Type u_1} →
  {H : Type u_2} →
    [inst : MulZeroOneClass G] → [inst_1 : MonoidWithZero H] → (f : G →*₀ H) → MonoidWithZero ↥(MonoidHom.mrange f)
-- Mathlib.Algebra.Group.Equiv.Defs
AddMonoid.End.equiv.eq_1 : ∀ (M : Type u_9) [inst : AddZero M],
  AddMonoid.End.equiv M = { toFun := id, invFun := id, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineEquiv.ofEq_symm : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (S₁ S₂ : AffineSubspace k P₁) [inst_4 : Nonempty ↥S₁] [inst_5 : Nonempty ↥S₂]
  (h : S₁ = S₂), (AffineEquiv.ofEq S₁ S₂ h).symm = AffineEquiv.ofEq S₂ S₁ ⋯
-- Mathlib.Data.Finsupp.Multiset
/-- Given a multiset `s`, `s.toFinsupp` returns the finitely supported function on `ℕ` given by
the multiplicities of the elements of `s`.  -/
Multiset.toFinsupp : {α : Type u_1} → [DecidableEq α] → Multiset α ≃+ (α →₀ ℕ)
-- Mathlib.Algebra.Order.Group.PosPart
instOneLePart.eq_1 : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α], instOneLePart = { oneLePart := fun a => a ⊔ 1 }
-- Mathlib.Data.Set.Operations
/-- `g` is a left inverse to `f` on `s` means that `g (f x) = x` for all `x ∈ s`.  -/
Set.LeftInvOn : {α : Type u} → {β : Type v} → (β → α) → (α → β) → Set α → Prop
-- Std.Net.Addr
Std.Net.instDecidableEqSocketAddressV6 : DecidableEq Std.Net.SocketAddressV6
-- Mathlib.Data.Nat.Log
/-- `log b n`, is the logarithm of natural number `n` in base `b`. It returns the largest `k : ℕ`
such that `b^k ≤ n`, so if `b^k = n`, it returns exactly `k`.  -/
Nat.log : ℕ → ℕ → ℕ
-- Mathlib.Data.Vector3
/-- Unexpander for `Vector3.nil`  -/
Vector3.unexpandNil : Lean.PrettyPrinter.Unexpander
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.Away.mk_surjective : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {f : A} {d : ι} (hf : f ∈ 𝒜 d) (x : HomogeneousLocalization.Away 𝒜 f),
  ∃ n a, ∃ (ha : a ∈ 𝒜 (n • d)), HomogeneousLocalization.Away.mk 𝒜 hf n a ha = x
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- A morphism of schemes `f : X ⟶ Y` is étale if for each affine `U ⊆ Y` and
`V ⊆ f ⁻¹' U`, The induced map `Γ(Y, U) ⟶ Γ(X, V)` is étale.  -/
AlgebraicGeometry.Etale : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.Order.Cover
/-- If `a ≤ b`, then `b` does not cover `a` iff there's an element in between.  -/
not_wcovBy_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → (¬a ⩿ b ↔ ∃ c, a < c ∧ c < b)
-- Mathlib.Data.Vector.Defs
/-- Map a vector under a partial function.  -/
List.Vector.pmap : {α : Type u_1} →
  {β : Type u_2} →
    {n : ℕ} → {p : α → Prop} → ((a : α) → p a → β) → (v : List.Vector α n) → (∀ x ∈ v.toList, p x) → List.Vector β n
-- Mathlib.Algebra.Order.IsBotOne
max_eq_zero : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Zero α] [IsBotZeroClass α] {a b : α}, max a b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.Topology.Constructions.SumProd
mem_nhds_prod_iff' : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x : X} {y : Y} {s : Set (X × Y)},
  s ∈ nhds (x, y) ↔ ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧ u ×ˢ v ⊆ s
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.op_reverse : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : CliffordAlgebra Q),
  MulOpposite.op (CliffordAlgebra.reverse x) = CliffordAlgebra.reverseOp x
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.and_or_right_inj : ∀ {m x y : ℕ}, x &&& m = y &&& m ∧ x ||| m = y ||| m ↔ x = y
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.npow.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S], OreLocalization.npow = npowRec
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_bijective : ∀ {m : Type u_3} {n : Type u_2} {R : Type u_1}, Function.Bijective Matrix.vec