mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Rel
SetRel.isTrans_symmetrize : ∀ {α : Type u_1} {R : SetRel α α} [R.IsTrans], R.symmetrize.IsTrans
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- The composition of locally Lipschitz functions is locally Lipschitz.  -/
LocallyLipschitz.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {f : β → γ} {g : α → β},
  LocallyLipschitz f → LocallyLipschitz g → LocallyLipschitz (f ∘ g)
-- Batteries.Data.MLList.Basic
/-- Apply a function to every element of a `MLList`.  -/
MLList.map : {m : Type u_1 → Type u_1} → {α β : Type u_1} → [Monad m] → (α → β) → MLList m α → MLList m β
-- Mathlib.Algebra.Category.MonCat.Limits
/-- `limit.π (F ⋙ forget AddMonCat) j` as an `AddMonoidHom`.  -/
AddMonCat.limitπAddMonoidHom : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddMonCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections] →
        (j : J) →
          (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).pt →+ ↑(F.obj j)
-- Init.Data.Option.Lemmas
Option.elim_pfilter : ∀ {α : Type u_1} {β : Sort u_2} {o : Option α} {b : β} {f : α → β} {p : (a : α) → o = some a → Bool},
  (o.pfilter p).elim b f = o.pelim b fun a ha => if p a ha = true then f a else b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insertManyIfNewUnit_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} (h : t.WF) {l : List α} {k : α},
  Std.DTreeMap.Internal.Impl.Const.get! (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)) k = ()
-- Batteries.Control.LawfulMonadState
/-- Version of `modifyGet_eq` that preserves an call to `modify`.  -/
LawfulMonadStateOf.modifyGet_eq' : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (f : σ → α × σ),
  modifyGet f = do
    let s ← get
    modify (Prod.snd ∘ f)
    pure (f s).1
-- Mathlib.Data.Set.Restrict
Set.domRestrict₂.eq_1 : ∀ {α : Type u_1} {π : α → Type u_6} {s t : Set α} (hst : s ⊆ t) (f : (a : ↑t) → π ↑a) (x : ↑s),
  Set.domRestrict₂ hst f x = f ⟨↑x, ⋯⟩
-- Mathlib.Algebra.Group.End
AddAut.instAddGroup.eq_1 : ∀ (M : Type u_2) [inst : Add M],
  AddAut.instAddGroup M =
    { add := fun g h => AddEquiv.trans h g, add_assoc := ⋯, zero := AddEquiv.refl M, zero_add := ⋯, add_zero := ⋯,
      nsmul := nsmulRecAuto, nsmul_zero := ⋯, nsmul_succ := ⋯, neg := AddEquiv.symm, zsmul := zsmulRec,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.smulTower.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [inst_6 : IsScalarTower R S A] {ι : Type u_5}
  {ι' : Type u_6} (b : Module.Basis ι R S) (c : Module.Basis ι' S A),
  b.smulTower c =
    {
      repr :=
        LinearEquiv.restrictScalars R c.repr ≪≫ₗ
          (Finsupp.lcongr (Equiv.refl ι') b.repr ≪≫ₗ
            ((Finsupp.curryLinearEquiv R).symm ≪≫ₗ Finsupp.lcongr (Equiv.prodComm ι' ι) (LinearEquiv.refl R R))) }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_eq_get!_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, t.getKey! a = (t.getKey? a).get!
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.instDiscreteTopology : ∀ {α : Type u_1} [inst : TopologicalSpace α] [DiscreteTopology α], DiscreteTopology (TopologicalSpace.Compacts α)
-- Lean.Environment
Lean.mkEmptyEnvironment : optParam UInt32 0 → IO Lean.Environment
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- `σ k n` is the sum of the `k`th powers of the divisors of `n`  -/
ArithmeticFunction.sigma : ℕ → ArithmeticFunction ℕ
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.symm_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A), P.symm.π = P.π
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.exact_iff_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂), S₁.Exact ↔ S₂.Exact
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_iff_hasProd_of_ne_one_bij : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
  {g : γ → α} (i : ↑(Function.mulSupport g) → β),
  Function.Injective i →
    Function.mulSupport f ⊆ Set.range i →
      (∀ (x : ↑(Function.mulSupport g)), f (i x) = g ↑x) → (HasProd f a ↔ HasProd g a)
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.mem_cons_of_mem : ∀ {α : Type u_1} (y : α) {a : α} {l : List α}, a ∈ l → a ∈ y :: l
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- `centroidWeights` gives the weights for the centroid as a
constant function, which is suitable when summing over the points
whose centroid is being taken.  This function gives the weights in a
form suitable for summing over a larger set of points, as an indicator
function that is zero outside the set whose centroid is being taken.
In the case of a `Fintype`, the sum may be over `univ`.  -/
Finset.centroidWeightsIndicator : (k : Type u_1) → [DivisionRing k] → {ι : Type u_4} → Finset ι → ι → k
-- Mathlib.Data.Nat.Pairing
Nat.unpair_pair : ∀ (a b : ℕ), Nat.unpair (Nat.pair a b) = (a, b)
-- Mathlib.Algebra.Group.Units.Hom
IsUnit.of_map : ∀ {R : Type u_2} {S : Type u_3} {F : Type u_5} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : FunLike F R S] (f : F)
  [IsLocalHom f] (a : R), IsUnit (f a) → IsUnit a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Ult
Std.Tactic.BVDecide.BVPred.mkUlt.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (lhsRefs rhsRefs : aig.RefVec w),
  Std.Tactic.BVDecide.BVPred.mkUlt aig { lhs := lhsRefs, rhs := rhsRefs } =
    (Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit (Std.Tactic.BVDecide.BVExpr.bitblast.blastNot aig rhsRefs).aig
            { w := w,
              vec := { lhs := lhsRefs.cast ⋯, rhs := (Std.Tactic.BVDecide.BVExpr.bitblast.blastNot aig rhsRefs).vec },
              cin :=
                (Std.Tactic.BVDecide.BVExpr.bitblast.blastNot aig rhsRefs).aig.mkConstCached true }).aig.mkNotCached
      (Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit (Std.Tactic.BVDecide.BVExpr.bitblast.blastNot aig rhsRefs).aig
          { w := w,
            vec := { lhs := lhsRefs.cast ⋯, rhs := (Std.Tactic.BVDecide.BVExpr.bitblast.blastNot aig rhsRefs).vec },
            cin := (Std.Tactic.BVDecide.BVExpr.bitblast.blastNot aig rhsRefs).aig.mkConstCached true }).ref
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- `C₀(α, β)` is the type of continuous functions `α → β` which vanish at infinity from a
topological space to a metric space with a zero element.

When possible, instead of parametrizing results over `(f : C₀(α, β))`,
you should parametrize over `(F : Type*) [ZeroAtInftyContinuousMapClass F α β] (f : F)`.

When you extend this structure, make sure to extend `ZeroAtInftyContinuousMapClass`.  -/
ZeroAtInfty.«termC₀(_,_)» : Lean.ParserDescr
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.AltExpr.rhs : {σ : Type} → Lean.Elab.Term.Do.AltExpr σ → σ
-- Mathlib.Algebra.Group.Subgroup.Defs
zsmul_mem : ∀ {M : Type u_3} {S : Type u_4} [inst : SubNegMonoid M] [inst_1 : SetLike S M] [hSM : AddSubgroupClass S M] {K : S}
  {x : M}, x ∈ K → ∀ (n : ℤ), n • x ∈ K
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
/-- The term in `CofibrantBrownFactorization f` that is deduced from
a factorization of `prod.lift f (𝟙 X) : X ⟶ Y ⨯ X`
as a cofibration followed by a trivial fibration.  -/
HomotopicalAlgebra.FibrantBrownFactorization.mk' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [HomotopicalAlgebra.IsFibrant X] →
            [HomotopicalAlgebra.IsFibrant Y] →
              (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C)
                  (CategoryTheory.Limits.prod.lift f (CategoryTheory.CategoryStruct.id X)) →
                HomotopicalAlgebra.FibrantBrownFactorization f
-- Mathlib.Data.Set.Finite.Monad
Set.Finite.seq' : ∀ {α β : Type u} {f : Set (α → β)} {s : Set α}, f.Finite → s.Finite → (f <*> s).Finite
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
add_mem_upperBounds_add : ∀ {M : Type u_3} [inst : Add M] [inst_1 : Preorder M] [AddLeftMono M] [AddRightMono M] {s t : Set M} {a b : M},
  a ∈ upperBounds s → b ∈ upperBounds t → a + b ∈ upperBounds (s + t)
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X),
  CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) X.toSpecΓ =
    AlgebraicGeometry.Spec.map (X.presheaf.germ ⊤ x trivial)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.mk.injEq : ∀ {X : Type u_3} (as as_1 : X), ({ as := as } = { as := as_1 }) = (as = as_1)
-- Mathlib.Data.Finset.Prod
Finset.prodMap_image_product : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : DecidableEq β] [inst_1 : DecidableEq δ]
  (f : α → β) (g : γ → δ) (s : Finset α) (t : Finset γ),
  Finset.image (Prod.map f g) (s ×ˢ t) = Finset.image f s ×ˢ Finset.image g t
-- Mathlib.Analysis.Complex.Convex
Complex.isConnected_of_upperHalfPlane : ∀ {r : ℝ} {s : Set ℂ}, {z | r < z.im} ⊆ s → s ⊆ {z | r ≤ z.im} → IsConnected s
-- Mathlib.Order.KrullDimension
Order.coheight_ofDual : ∀ {α : Type u_1} [inst : Preorder α] (x : αᵒᵈ), Order.coheight (OrderDual.ofDual x) = Order.height x
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsZeroOrMarkovKernel.isZeroOrProbabilityMeasure : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsZeroOrMarkovKernel κ] (a : α), MeasureTheory.IsZeroOrProbabilityMeasure (κ a)
-- Init.Data.Slice.Array.Lemmas
Array.toArray_mkSlice_rio : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ}, Std.Slice.toArray (Std.Rio.Sliceable.mkSlice xs *...hi) = xs.extract 0 hi
-- Mathlib.Order.Bounds.Basic
bddBelow_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, BddBelow (Set.Ioc b a)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.distinct_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) t.toList
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisionAt.eq_mul_add : ∀ {A : Type u_1} [inst : CommRing A] {f g q : PowerSeries A} {r : Polynomial A} {I : Ideal A},
  f.IsWeierstrassDivisionAt g q r I → f = g * q + ↑r
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.toFun_eq_coe : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (D : LieDerivation R L M), (↑D).toFun = ⇑D
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ker_algebraMap_residueField : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime], RingHom.ker (algebraMap R I.ResidueField) = I
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.opow_omega0 : ∀ {a : Ordinal.{u}}, 1 < a → a < Ordinal.omega0 → a ^ Ordinal.omega0 = Ordinal.omega0
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.shift.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] [inst_3 : W.IsCompatibleWithShift M] {X Y : C} {a : M}
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y]
  (f : CategoryTheory.Localization.SmallShiftedHom W X Y a) (n a' : M) (h : a + n = a'),
  f.shift n a' h =
    (CategoryTheory.Localization.SmallHom.shift f n).comp
      (CategoryTheory.Localization.SmallHom.mk W ((CategoryTheory.shiftFunctorAdd' C a n a' h).inv.app Y))
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.HasFiniteBiproducts.mk : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  (∀ (n : ℕ), CategoryTheory.Limits.HasBiproductsOfShape (Fin n) C) → CategoryTheory.Limits.HasFiniteBiproducts C
-- Init.Data.Vector.Basic
Vector.findRev? : {n : ℕ} → {α : Type} → (α → Bool) → Vector α n → Option α
-- Mathlib.Geometry.Manifold.Immersion
/-- A function `f : M → N` between `C^n` manifolds is `C^n` at `x` if and only if it is continuous
at `x` and its composition `φ ∘ f` with a `C^n` immersion `φ : N → N'` at `f x` is `C^n` at `x`.  -/
ContMDiffAt.iff_comp_isImmersionAtOfComplement : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E''' : Type u_4} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup E'''] [inst_6 : NormedSpace 𝕜 E''']
  [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F] {H : Type u_7} [inst_9 : TopologicalSpace H] {G : Type u_9}
  [inst_10 : TopologicalSpace G] {G' : Type u_10} [inst_11 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H M] {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {N' : Type u_14} [inst_16 : TopologicalSpace N'] [inst_17 : ChartedSpace G' N'] {n : WithTop ℕ∞} {x : M} {f : M → N}
  {φ : N → N'},
  Manifold.IsImmersionAtOfComplement F J J' n φ (f x) →
    (ContMDiffAt I J n f x ↔ ContinuousAt f x ∧ ContMDiffAt I J' n (φ ∘ f) x)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.AltExpr.pvars : {σ : Type} → Lean.Elab.Term.Do.AltExpr σ → Array Lean.Syntax
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃) {Z : CategoryTheory.Functor (CategoryTheory.Sheaf J A) A}
  (h : Φ₁.sheafFiber ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.Hom.sheafFiber f) h)
-- Batteries.Recycling.RBTree.WF
/-- If `x < y` then `f x < f y`.  -/
RBTree.RBNode.IsMonotone.lt_mono : ∀ {α : Type u_1} {β : Type u_2} {cmpα : α → α → Ordering} {cmpβ : β → β → Ordering} {f : α → β}
  [self : RBTree.RBNode.IsMonotone cmpα cmpβ f] {x y : α},
  RBTree.RBNode.cmpLT cmpα x y → RBTree.RBNode.cmpLT cmpβ (f x) (f y)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeExtension.mapPosSubmonoid.congr_simp : ∀ (A : Type u_1) (B : Type u_2) [inst : CommSemiring A] [inst_1 : Semiring B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B] [inst_5 : ValuativeExtension A B],
  ValuativeExtension.mapPosSubmonoid A B = ValuativeExtension.mapPosSubmonoid A B
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Ordering.swap.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_2 ()
-- Init.Data.Fin.Lemmas
Fin.val_ne_zero_iff : ∀ {n : ℕ} [inst : NeZero n] {a : Fin n}, ↑a ≠ 0 ↔ a ≠ 0
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inv_inv : ∀ {R : Type u} {M : Type v} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M] [inst_2 : Module Rᵐᵒᵖ M]
  [inst_3 : Module R M] [SMulCommClass R Rᵐᵒᵖ M] {x : TrivSqZeroExt R M}, x.fst ≠ 0 → x⁻¹⁻¹ = x
-- Mathlib.Analysis.Normed.Group.Basic
/-- A translated sphere is a sphere.  -/
setOf_sub_mem_sphere_eq_sphere : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a : E} {r : ℝ}, {x | x - a ∈ Metric.sphere 0 r} = Metric.sphere a r
-- Aesop.Tracing
Aesop.TraceOption.debug : Aesop.TraceOption
-- Batteries.Data.List.Basic
/-- Map each element of a `List` to an action, evaluate these actions in order,
and collect the results.
 -/
List.traverse : {F : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_1} → [Applicative F] → (α → F β) → List α → F (List β)
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.coe_toHom : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (f : A.Copy B), ⇑f.toHom = ⇑f
-- Std.Sat.CNF.RelabelFin
/-- Obtain the literal with the largest identifier in `c`.
 -/
Std.Sat.CNF.Clause.maxLiteral : Std.Sat.CNF.Clause ℕ → Option ℕ
-- Mathlib.Topology.ContinuousOn
/-- If a function is continuous within `s` at `x`, then it tends to `f x` within `s` by definition.
We register this fact for use with the dot notation, especially to use `Filter.Tendsto.comp` as
`ContinuousWithinAt.comp` will have a different meaning.  -/
ContinuousWithinAt.tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → Filter.Tendsto f (nhdsWithin x s) (nhds (f x))
-- Lean.Elab.Tactic.SolveByElim
_private.Lean.Elab.Tactic.SolveByElim.0.Lean.Elab.Tactic.SolveByElim.elabApplyRulesConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Lean.Meta.SolveByElim.ApplyRulesConfig
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- The explicit `Equiv` between maps from the constructed coproduct `cofan 𝒜 f` and families of
maps from each component, which is the universal property of coproducts.  -/
CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (𝒜 : Type w) →
      (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) →
        (t : CategoryTheory.Limits.FormalCoproduct C) →
          ((CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt ⟶ t) ≃ ((i : 𝒜) → f i ⟶ t)
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `bot_eq_zero`. -/
bot_eq_zero'' : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α] [inst_3 : OrderBot α], ⊥ = 0
-- Mathlib.Algebra.GCDMonoid.Basic
CommGroupWithZero.instStrongNormalizedGCDMonoid : (G₀ : Type u_2) → [inst : CommGroupWithZero G₀] → [DecidableEq G₀] → StrongNormalizedGCDMonoid G₀
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceBeqDiff : Lean.Meta.Simp.Simproc
-- Mathlib.Condensed.Discrete.Module
/-- `functorToPresheaves` as a functor to light condensed modules.  -/
LightCondMod.LocallyConstant.functor : (R : Type u) → [inst : Ring R] → CategoryTheory.Functor (ModuleCat R) (LightCondMod R)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- The inclusion from the subscheme associated to an ideal sheaf.  -/
AlgebraicGeometry.Scheme.IdealSheafData.subschemeι : {X : AlgebraicGeometry.Scheme} → (I : X.IdealSheafData) → I.subscheme ⟶ X
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arcsin`, version subtracting vectors.  -/
Orientation.oangle_sub_left_eq_arcsin_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  o.oangle x y = ↑(Real.pi / 2) → o.oangle (x - y) x = ↑(Real.arcsin (‖y‖ / ‖x - y‖))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.equiv_iff_toList_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ ↔ t₁.toList = t₂.toList
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom : {C : Type u} → (X : CategoryTheory.FreeMonoidalCategory C) → (X.tensor CategoryTheory.FreeMonoidalCategory.unit).Hom X
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.fundamentalFrontier_subset : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s : Set α},
  MeasureTheory.fundamentalFrontier G s ⊆ s
-- Mathlib.Logic.Encodable.Basic
Sigma.encodable : {α : Type u_1} → {γ : α → Type u_3} → [Encodable α] → [(a : α) → Encodable (γ a)] → Encodable (Sigma γ)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.liftRel_mk_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] {r : β → γ → Prop} {f : α → β} {g : α → γ}
  {hf : MeasureTheory.AEStronglyMeasurable f μ} {hg : MeasureTheory.AEStronglyMeasurable g μ},
  MeasureTheory.AEEqFun.LiftRel r (MeasureTheory.AEEqFun.mk f hf) (MeasureTheory.AEEqFun.mk g hg) ↔
    ∀ᵐ (a : α) ∂μ, r (f a) (g a)
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E / F` is a separable extension of exponential characteristic `q`, if `{ u_i }` is an
`F`-basis of `E`, then `{ u_i ^ (q ^ n) }` is also an `F`-basis of `E`
for any natural number `n`.  -/
Module.Basis.mapPowExpCharPowOfIsSeparable : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          (q : ℕ) →
            ℕ →
              [hF : ExpChar F q] → {ι : Type u_1} → [Algebra.IsSeparable F E] → Module.Basis ι F E → Module.Basis ι F E
-- Mathlib.Order.Heyting.Boundary
Coheyting.hnot_hnot_sup_boundary : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ￢￢a ⊔ Coheyting.boundary a = a
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.norm_cnstr_nc_cert.eq_1 : ∀ (lhs rhs lhs' rhs' : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.norm_cnstr_nc_cert lhs rhs lhs' rhs' = (rhs.sub lhs).toPoly_nc.beq' (rhs'.sub lhs').toPoly_nc
-- Mathlib.Data.Int.Init
Int.natCast_mod : ∀ (m n : ℕ), ↑(m % n) = ↑m % ↑n
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.le_retractClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C), P ≤ P.retractClosure
-- Mathlib.Algebra.CharP.Frobenius
RingHom.map_iterateFrobenius : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] (g : R →+* S) (p : ℕ)
  [inst_2 : ExpChar R p] [inst_3 : ExpChar S p] (x : R) (n : ℕ),
  g ((iterateFrobenius R p n) x) = (iterateFrobenius S p n) (g x)
-- Mathlib.Order.Antichain
IsStrongAntichain.image : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α},
  IsStrongAntichain r s →
    ∀ {f : α → β}, Function.Surjective f → (∀ (a b : α), r' (f a) (f b) → r a b) → IsStrongAntichain r' (f '' s)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.pairs : (σ : Type u_1) → [DecidableEq σ] → [Fintype σ] → ℕ → Finset (Finset σ × σ)
-- Mathlib.Order.SuccPred.Basic
Order.Ioc_pred_right_of_not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, ¬IsMin a → Set.Ioc b (Order.pred a) = Set.Ioo b a