mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Submodule.Pointwise
/-- `Submodule.pointwiseNeg` as an order isomorphism.  -/
Submodule.negOrderIso : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Submodule R M ≃o Submodule R M
-- Mathlib.Data.Set.Prod
/-- The projection from the fiber product to the first factor.  -/
Function.Pullback.fst : {X : Type u_1} → {Y : Sort u_2} → {Z : Type u_3} → {f : X → Y} → {g : Z → Y} → Function.Pullback f g → X
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.instContextContext : Mathlib.Tactic.BicategoryLike.Context Mathlib.Tactic.Bicategory.Context
-- Init.Data.SInt.Bitwise
Int16.toUInt16_or : ∀ (a b : Int16), (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16
-- Mathlib.FieldTheory.RatFunc.Defs
/-- `RatFunc.mk (p q : K[X])` is `p / q` as a rational function.

If `q = 0`, then `mk` returns 0.

This is an auxiliary definition used to define an `Algebra` structure on `RatFunc`;
the `simp` normal form of `mk p q` is `algebraMap _ _ p / algebraMap _ _ q`.
 -/
RatFunc.mk : {K : Type u_1} → [inst : CommRing K] → [IsDomain K] → Polynomial K → Polynomial K → RatFunc K
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- The full level `N` congruence subgroup of `SL(2, ℤ)` of matrices that reduce to the identity
modulo `N`.  -/
CongruenceSubgroup.Gamma : ℕ → Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_one_le_of_pos : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : ℤ}, 0 < a → 1 ≤ ↑a
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanSingleton_pow : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] (x : P) (n : ℕ),
  FractionalIdeal.spanSingleton S x ^ n = FractionalIdeal.spanSingleton S (x ^ n)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Every Schwartz function is differentiable.  -/
SchwartzMap.differentiable : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : SchwartzMap E F), Differentiable ℝ ⇑f
-- Mathlib.Data.List.TakeDrop
_private.Mathlib.Data.List.TakeDrop.0.List.reverseAux.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (l r : List α) (h_1 : (r : List α) → motive [] r)
  (h_2 : (a : α) → (l r : List α) → motive (a :: l) r),
  (match a :: l, r with
    | [], r => h_1 r
    | a :: l, r => h_2 a l r) =
    h_2 a l r
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false →
    Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.Const.ofList l) k fallback = fallback
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Complex.logTaylor_at_zero : ∀ (n : ℕ), Complex.logTaylor n 0 = 0
-- Mathlib.LinearAlgebra.Matrix.Basis
basis_toMatrix_mul : ∀ {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_9} [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : Fintype ι'] [inst_6 : Fintype κ] [inst_7 : Finite ι] [inst_8 : DecidableEq κ] (b₁ : Module.Basis ι R M)
  (b₂ : Module.Basis ι' R M) (b₃ : Module.Basis κ R N) (A : Matrix ι' κ R),
  b₁.toMatrix ⇑b₂ * A = (LinearMap.toMatrix b₃ b₁) ((Matrix.toLin b₃ b₂) A)
-- Init.Grind.Ordered.Linarith
/-- Normalizes the given polynomial by fusing monomial and constants.  -/
Lean.Grind.Linarith.Poly.norm : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_prod : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ι → MvPolynomial σ R)
  (g : σ → R), (MvPolynomial.eval g) (∏ i ∈ s, f i) = ∏ i ∈ s, (MvPolynomial.eval g) (f i)
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.card_edgeFinset_replaceVertex_of_not_adj : ∀ {V : Type u_1} (G : SimpleGraph V) {s t : V} [inst : DecidableEq V] [inst_1 : Fintype V]
  [inst_2 : DecidableRel G.Adj],
  ¬G.Adj s t → (G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_subLeft_nhdsLT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [IsTopologicalAddGroup H] [inst_3 : PartialOrder H]
  [IsOrderedAddMonoid H] {c a : H},
  Filter.map (fun x => c - x) (nhdsWithin a (Set.Iio a)) = nhdsWithin (c - a) (Set.Ioi (c - a))
-- Mathlib.Order.Types.Defs
/-- `ω` is the first infinite order type, defined as the order type of `ℕ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `ω` in identifiers is `omega0`. -/
OrderType.termω : Lean.ParserDescr
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressOptions.mk.injEq : ∀ (workDoneProgress workDoneProgress_1 : Bool),
  ({ workDoneProgress := workDoneProgress } = { workDoneProgress := workDoneProgress_1 }) =
    (workDoneProgress = workDoneProgress_1)
-- Mathlib.Algebra.Order.Round
round_sub_intCast : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α)
  (y : ℤ), round (x - ↑y) = round x - y
-- Mathlib.RingTheory.FreeCommRing
/-- **Alias** of `freeCommRingPEmptyEquivInt`.

---

The free commutative ring on the empty type is isomorphic to `ℤ`.  -/
freeCommRingPemptyEquivInt : FreeCommRing PEmpty.{u + 1} ≃+* ℤ
-- Mathlib.Data.Nat.Factorization.PrimePow
Nat.Coprime.isPrimePow_dvd_mul : ∀ {n a b : ℕ}, a.Coprime b → IsPrimePow n → (n ∣ a * b ↔ n ∣ a ∨ n ∣ b)
-- Init.Data.String.Defs
String.rawEndPos_eq_zero_iff : ∀ {b : String}, b.rawEndPos = 0 ↔ b = ""
-- Mathlib.Algebra.Order.Hom.Monoid
/-- See Note [custom simps projection].  -/
OrderAddMonoidIso.Simps.apply : {α : Type u_2} →
  {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Add α] → [inst_3 : Add β] → (α ≃+o β) → α → β
-- Mathlib.Order.RelSeries
RelSeries.append_apply_right : ∀ {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r) (i : Fin (q.length + 1)),
  (p.append q connect).toFun (Fin.cast ⋯ (Fin.natAdd (p.length + 1) i)) = q.toFun i
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.ofAbs_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S), Function.Bijective WithAbs.ofAbs
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_tsum : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {x : ℕ → MvPowerSeries σ R} [inst_3 : UniformSpace R]
  [DiscreteUniformity R] [inst_5 : UniformSpace S] [DiscreteUniformity S],
  Summable x →
    MvPowerSeries.HasSubst a → MvPowerSeries.subst a (∑' (i : ℕ), x i) = ∑' (i : ℕ), MvPowerSeries.subst a (x i)
-- Mathlib.LinearAlgebra.Dimension.Constructions
Module.finrank_finsupp : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Free R M] {ι : Type v} [inst_5 : Fintype ι], Module.finrank R (ι →₀ M) = Fintype.card ι * Module.finrank R M
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_mul_sphere_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), {x} * Metric.sphere 1 δ = Metric.sphere x δ
-- Mathlib.CategoryTheory.Comma.Basic
/-- The functor sending an object `X` in the comma category to `X.right`.  -/
CategoryTheory.Comma.snd : {B : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} B] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) → CategoryTheory.Functor (CategoryTheory.Comma L R) B
-- Init.Prelude
/-- The first element of a pair.  -/
PProd.fst : {α : Sort u} → {β : Sort v} → α ×' β → α
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.lintegral_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {f : α → ENNReal} {g : β → ENNReal},
  ProbabilityTheory.IdentDistrib f g μ ν → ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : β), g x ∂ν
-- Mathlib.Combinatorics.Quiver.Basic
/-- A type synonym for a quiver with no arrows.  -/
Quiver.Empty : Type u → Type u
-- Mathlib.CategoryTheory.Abelian.RightDerived
/-- The natural transformation between right-derived functors
induced by a natural transformation.  -/
CategoryTheory.NatTrans.rightDerived : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.HasInjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              {F G : CategoryTheory.Functor C D} →
                [inst_5 : F.Additive] → [inst_6 : G.Additive] → (F ⟶ G) → (n : ℕ) → F.rightDerived n ⟶ G.rightDerived n
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_neg : ∀ {α : Type u_1} {E : Type u_3} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (f : α → E) (m : MeasurableSpace α), μ[-f | m] =ᵐ[μ] -μ[f | m]
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to1.write.match_1.eq_1 : ∀ {Γ : Type u_3} {Λ : Type u_2} {σ : Type u_1}
  (motive : List Bool → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ → Sort u_4)
  (q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ)
  (h_1 : (q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) → motive [] q)
  (h_2 : (a : Bool) → (l : List Bool) → (q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) → motive (a :: l) q),
  (match [], q with
    | [], q => h_1 q
    | a :: l, q => h_2 a l q) =
    h_1 q
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- A finite sum of monotone functions is monotone.  -/
Monotone.finsetSum : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {s : Finset ι} [AddLeftMono N]
  {γ : Type u_9} [inst_3 : Preorder γ] {f : ι → γ → N}, (∀ i ∈ s, Monotone (f i)) → Monotone fun x => ∑ i ∈ s, f i x
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- We compute the absolute discriminant of a `p ^ k`-th cyclotomic field.
Beware that in the cases `p ^ k = 1` and `p ^ k = 2` the formula uses `1 / 2 = 0` and `0 - 1 = 0`.
See also the results below.  -/
IsCyclotomicExtension.Rat.discr_prime_pow : ∀ (p k : ℕ) (K : Type u) [inst : Field K] [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p ^ k} ℚ K],
  NumberField.discr K = (-1) ^ ((p ^ k).totient / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.mul_isBigO : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S},
  f₁ =o[l] g₁ → f₂ =O[l] g₂ → (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x
-- Mathlib.Order.UpperLower.Relative
instPartialOrderRelUpperSet : {α : Type u_1} → {P : α → Prop} → [inst : LE α] → PartialOrder (RelUpperSet P)
-- Mathlib.Topology.UnitInterval
/-- When `h : a ≤ b` and `δ > 0`, `addNSMul h δ` is a sequence of points in the closed interval
`[a,b]`, which is initially equally spaced but eventually stays at the right endpoint `b`.  -/
Set.Icc.addNSMul : {α : Type u_1} → [AddCommGroup α] → [inst : LinearOrder α] → {a b : α} → a ≤ b → α → ℕ → ↑(Set.Icc a b)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess.congr_simp : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] [inst_1 : LinearOrder ι] (u u_1 : ι → Ω → β),
  u = u_1 →
    ∀ (τ τ_1 : Ω → WithTop ι),
      τ = τ_1 →
        ∀ (a a_1 : ι),
          a = a_1 →
            ∀ (a_2 a_3 : Ω),
              a_2 = a_3 → MeasureTheory.stoppedProcess u τ a a_2 = MeasureTheory.stoppedProcess u_1 τ_1 a_1 a_3
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
ZMod.stdAddChar.eq_1 : ∀ {N : ℕ} [inst : NeZero N], ZMod.stdAddChar = Circle.coeHom.compAddChar ZMod.toCircle
-- Mathlib.Order.Filter.Extr
IsMinOn.inf : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf β] {f g : α → β} {a : α} {s : Set α},
  IsMinOn f s a → IsMinOn g s a → IsMinOn (fun x => f x ⊓ g x) s a
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_one : ↑1 = 1
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.linearEquivOfLeftInverse_apply : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : Module.Invertible R M] [inst_6 : Module.Invertible R N]
  {f : M →ₗ[R] N} {g : N →ₗ[R] M} (hfg : Function.LeftInverse ⇑f ⇑g) (x : M),
  (Module.Invertible.linearEquivOfLeftInverse hfg) x = f x
-- Init.Control.Option
/-- Adds the ability to fail to a monad. Unlike ordinary exceptions, there is no way to signal why a
failure occurred.
 -/
OptionT : (Type u → Type v) → Type u → Type v
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.mapCotangent_ker_of_surjective : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  Function.Surjective ⇑(algebraMap A B) →
    ∀ {I : Ideal B} {J : Ideal A} (eq : Ideal.comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J),
      (J.mapCotangent I (Algebra.ofId A B) ⋯).ker =
        Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))
-- Mathlib.Data.Num.Bitwise
SNum.zero.inj : ∀ {a a_1 : Bool}, SNum.zero a = SNum.zero a_1 → a = a_1
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q : ℕ) {Z : CochainComplex C ℤ}
  (h : L ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q)
      (CategoryTheory.CategoryStruct.comp
        ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op q)).obj.π h) =
    CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.π✝ f n₀) h
-- Aesop.Util.Unfold
_private.Aesop.Util.Unfold.0.Aesop.unfoldManyCore.pre : (Lean.Name → Option (Option Lean.Name)) →
  Lean.Expr → StateRefT' IO.RealWorld (Array Lean.Name) Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCocone_ι_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (j : J),
  (H.mapCocone c).ι.app j = H.map (c.ι.app j)
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.tryTacticElabAttribute.unsafe_1 : IO (Lean.KeyedDeclsAttribute Lean.Elab.Tactic.Try.TryTactic)
-- Mathlib.GroupTheory.DivisibleHull
/-- Coercion from `M` to `DivisibleHull M` as an `OrderAddMonoidHom`.  -/
DivisibleHull.coeOrderAddMonoidHom : (M : Type u_2) →
  [inst : AddCommGroup M] → [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → M →+o DivisibleHull M
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.orthogonal_span_coroot_eq_ker : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [inst_7 : CharZero K]
  (α : LieModule.Weight K (↥H) L),
  (LieModule.traceForm K (↥H) L).orthogonal (K ∙ LieAlgebra.IsKilling.coroot α) = LieModule.Weight.ker
-- Mathlib.Topology.Order.LeftRightLim
/-- A monotone function is continuous to the left at a point if and only if its left limit
coincides with the value of the function.  -/
Monotone.continuousWithinAt_Iio_iff_leftLim_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f →
    ∀ {x : α} [inst_4 : TopologicalSpace α] [OrderTopology α],
      ContinuousWithinAt f (Set.Iio x) x ↔ Function.leftLim f x = f x
-- Mathlib.RingTheory.HopfAlgebra.GroupLike
GroupLike.val_toUnits_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A]
  (a : GroupLike R A), ↑((GroupLike.toUnits R) a) = ↑a
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyMap'_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData),
  CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.id S) h h =
    CategoryTheory.CategoryStruct.id h.H
-- Init.Data.String.Decode
String.utf8EncodeChar.eq_1 : ∀ (c : Char),
  String.utf8EncodeChar c =
    if c.val.toNat ≤ 127 then [UInt8.ofNat c.val.toNat]
    else
      if c.val.toNat ≤ 2047 then [UInt8.ofNat (c.val.toNat / 64 % 32 + 192), UInt8.ofNat (c.val.toNat % 64 + 128)]
      else
        if c.val.toNat ≤ 65535 then
          [UInt8.ofNat (c.val.toNat / 4096 % 16 + 224), UInt8.ofNat (c.val.toNat / 64 % 64 + 128),
            UInt8.ofNat (c.val.toNat % 64 + 128)]
        else
          [UInt8.ofNat (c.val.toNat / 262144 % 8 + 240), UInt8.ofNat (c.val.toNat / 4096 % 64 + 128),
            UInt8.ofNat (c.val.toNat / 64 % 64 + 128), UInt8.ofNat (c.val.toNat % 64 + 128)]
-- Mathlib.Topology.Connected.TotallyDisconnected
Continuous.connectedComponentsLift_unique : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (g : ConnectedComponents α → β),
  g ∘ ConnectedComponents.mk = f → g = h.connectedComponentsLift
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.isUniformEmbedding_restrictScalars : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : UniformSpace F]
  [inst_7 : IsUniformAddGroup F] (𝕜' : Type u_5) [inst_8 : NontriviallyNormedField 𝕜'] [inst_9 : NormedAlgebra 𝕜' 𝕜]
  [inst_10 : (i : ι) → Module 𝕜' (E i)] [inst_11 : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [inst_12 : Module 𝕜' F]
  [inst_13 : IsScalarTower 𝕜' 𝕜 F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)],
  IsUniformEmbedding (ContinuousMultilinearMap.restrictScalars 𝕜')
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.tendsto_defaultRatCDF_atBot : Filter.Tendsto ProbabilityTheory.defaultRatCDF Filter.atBot (nhds 0)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.isNormal_derivFamily : ∀ {ι : Type u_1} [Small.{u, u_1} ι] (f : ι → Ordinal.{u} → Ordinal.{u}), Order.IsNormal (Ordinal.derivFamily f)
-- Mathlib.Algebra.Group.Invertible.Defs
mul_invOf_self : ∀ {α : Type u} [inst : Mul α] [inst_1 : One α] (a : α) [inst_2 : Invertible a], a * ⅟a = 1
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instStarModule : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] {𝕜 : Type u_5} [inst_1 : Zero 𝕜] [inst_2 : Star 𝕜]
  [inst_3 : AddMonoid β] [inst_4 : StarAddMonoid β] [inst_5 : TopologicalSpace β] [inst_6 : ContinuousStar β]
  [inst_7 : SMulWithZero 𝕜 β] [inst_8 : ContinuousConstSMul 𝕜 β] [StarModule 𝕜 β],
  StarModule 𝕜 (CompactlySupportedContinuousMap α β)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inr_smul : ∀ {S : Type u_2} (R : Type u_3) {A : Type u_4} [inst : Zero R] [inst_1 : SMulZeroClass S R] [inst_2 : SMul S A] (r : S)
  (m : A), ↑(r • m) = r • ↑m
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsCodetector.isCoseparator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasCoequalizers C] {G : C},
  CategoryTheory.IsCodetector G → CategoryTheory.IsCoseparator G
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.many1Unbox.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Complex.Circle
Circle.exp_zero : Circle.exp 0 = 1
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.add_comm : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (a b : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.add a b = Lean.Grind.IntModule.OfNatModule.add b a
-- Init.Sym.Lemmas
Lean.Sym.UInt32.le_eq_true : ∀ (a b : UInt32), decide (a ≤ b) = true → (a ≤ b) = True
-- Mathlib.Algebra.Free
FreeAddMagma.instAdd : {α : Type u} → Add (FreeAddMagma α)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.mk_coe : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S)
  (e' : S → R) (h₁ : Function.LeftInverse e' ⇑e) (h₂ : Function.RightInverse e' ⇑e)
  (h₃ :
    ∀ (x y : R),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) =
        { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x *
          { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y)
  (h₄ :
    ∀ (x y : R),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) =
        { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x +
          { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y),
  { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ } = e
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toAddSubmonoid_irrelevant_le : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] {P : AddSubmonoid A},
  (HomogeneousIdeal.irrelevant 𝒜).toAddSubmonoid ≤ P ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P
-- Mathlib.Algebra.Regular.Basic
/-- In a semigroup, the product of regular elements is regular.  -/
IsRegular.mul : ∀ {R : Type u_1} [inst : Semigroup R] {a b : R}, IsRegular a → IsRegular b → IsRegular (a * b)
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} [inst_5 : F.Additive] [inst_6 : G.Additive]
  (α : F ⟶ G) {X : C} (P : CategoryTheory.ProjectiveResolution X),
  (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α).app X =
    CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom
      (CategoryTheory.CategoryStruct.comp
        ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
          ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex))
        (P.isoLeftDerivedToHomotopyCategoryObj G).inv)