mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.star_apply : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : (i : α) → StarAddMonoid (E i)] [inst_2 : ∀ (i : α), NormedStarGroup (E i)] (f : ↥(lp E p)) (i : α),
  ↑(star f) i = star (↑f i)
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.exists_notMem_finite : ∀ {α : Type u} {s t : Set α}, s.Infinite → t.Finite → ∃ a ∈ s, a ∉ t
-- Mathlib.Data.PFun
/-- The range of a partial function is the set of values
`f x` where `x` is in the domain of `f`.  -/
PFun.ran : {α : Type u_1} → {β : Type u_2} → (α →. β) → Set β
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mem_toSubsemigroup : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Submonoid M} {x : M}, x ∈ s.toSubsemigroup ↔ x ∈ s
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_eval : ∀ (c : Turing.ToPartrec.Code) (v : List ℕ),
  StateTransition.eval (Turing.TM2.step Turing.PartrecToTM2.tr) (Turing.PartrecToTM2.init c v) =
    Turing.PartrecToTM2.halt <$> c.eval v
-- Mathlib.Order.Hom.Basic
OrderIso.conj_apply : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (a : α →o α),
  f.conj a = (↑f).comp (a.comp ↑f.symm)
-- Mathlib.Topology.Constructible
IsRetrocompact.finsetInf : ∀ {X : Type u_2} [inst : TopologicalSpace X] [T2Space X] {ι : Type u_4} {s : Finset ι} {t : ι → Set X},
  (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.inf t)
-- Mathlib.LinearAlgebra.Dimension.LinearMap
LinearMap.le_rank_iff_exists_linearIndependent_finset : ∀ {K : Type u} {V : Type v} {V' : Type v'} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V'] [inst_4 : Module K V'] {n : ℕ} {f : V →ₗ[K] V'},
  ↑n ≤ f.rank ↔ ∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.eq_X_sub_C' : ∀ {A : Type u_1} [inst : Field A] (a : A), minpoly A a = Polynomial.X - Polynomial.C a
-- Mathlib.RingTheory.LocalProperties.Exactness
bijective_of_localized_maximal : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  (∀ (J : Ideal R) [inst_5 : J.IsMaximal], Function.Bijective ⇑((LocalizedModule.map J.primeCompl) f)) →
    Function.Bijective ⇑f
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Finsupp.log_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β] (f : α →₀ β) (g : α → β → ℝ),
  (∀ (a : α), g a (f a) = 0 → f a = 0) → Real.log (f.prod g) = f.sum fun a b => Real.log (g a b)
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.smulZeroClass : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (P : Submodule R M) → SMulZeroClass R (M ⧸ P)
-- Mathlib.Topology.Metrizable.Uniformity
/-- A T₀ uniform space with countably generated `𝓤 X` is metrizable. This is not an instance to
avoid loops.  -/
UniformSpace.metrizableSpace : ∀ {X : Type u_1} [inst : UniformSpace X] [(uniformity X).IsCountablyGenerated] [T0Space X],
  TopologicalSpace.MetrizableSpace X
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tprod_pnat_eq_tprod_succ : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {f : ℕ → M},
  ∏' (n : ℕ+), f ↑n = ∏' (n : ℕ), f (n + 1)
-- Mathlib.Algebra.Lie.UniversalEnveloping
UniversalEnvelopingAlgebra.eq_1 : ∀ (R : Type u₁) (L : Type u₂) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  UniversalEnvelopingAlgebra R L = (UniversalEnvelopingAlgebra.ringCon R L).Quotient
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.w_mul_φ_nonneg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (D : ℝ) (x y : E),
  0 ≤ ExistsContDiffBumpBase.w D y * ExistsContDiffBumpBase.φ (x - y)
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.coe_restrict_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {f : M →ₛₗ[σ₁₂] M₂} {p : Submodule R M} {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q) (x : ↥p),
  ↑((f.restrict hf) x) = f ↑x
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.HasFirstPageComputation.hi₂₃ : ∀ {ι : Type u_2} {κ : Type u_3} {inst : Preorder ι} {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  {data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀} [self : data.HasFirstPageComputation]
  (pq : κ), data.i₂ pq = data.i₃ r₀ pq ⋯
-- Std.Time.Date.Unit.Day
/-- Convert `Millisecond.Offset` into `Day.Offset`.
 -/
Std.Time.Day.Offset.ofMilliseconds : Std.Time.Millisecond.Offset → Std.Time.Day.Offset
-- Mathlib.Geometry.Manifold.ContMDiffMap
ContMDiffMap.ext_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {H' : Type u_5} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  {f g : ContMDiffMap I I' M M' n}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Preconnected.map : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {G'' : G'.coe.Subgraph} (f : G'.coe →g G),
  G''.Preconnected → (SimpleGraph.Subgraph.map f G'').Preconnected
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.alternatingSum_singleton : ∀ {G : Type u_7} [inst : Zero G] [inst_1 : Add G] [inst_2 : Neg G] (a : G), [a].alternatingSum = a
-- Mathlib.Data.Finset.Sort
Finset.sort_toFinset : ∀ {α : Type u_1} (s : Finset α) (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r] [inst_4 : DecidableEq α], (s.sort r).toFinset = s
-- Init.Data.String.TakeDrop
String.Slice.stripSuffix : String.Slice → String.Slice → String.Slice
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.le_sum_nonempty_of_subadditive_on_pred : ∀ {α : Type u_5} {β : Type u_6} [inst : AddMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β] (f : α → β) (p : α → Prop),
  (∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) →
    (∀ (a b : α), p a → p b → p (a + b)) → ∀ (l : List α), l ≠ [] → (∀ a ∈ l, p a) → f l.sum ≤ (List.map f l).sum
-- Mathlib.Algebra.Group.Action.End
AddAction.toPermHom_apply_apply : ∀ (G : Type u_1) (α : Type u_5) [inst : AddGroup G] [inst_1 : AddAction G α] (a : G) (x : α),
  ((AddAction.toPermHom G α) a) x = a +ᵥ x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.insert k v)[k]? = some v
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey!_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] [inst_2 : Inhabited α] {β : Type v} {γ : Type w}
  {f : α → β → Option γ} {l : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey! k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      ((Std.Internal.List.getKey? k l).pfilter fun x h => (f x (Std.Internal.List.getValue x l ⋯)).isSome).get!
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.delta.eq_1 : ∀ (n : ℕ), LSeries.delta n = if n = 1 then 1 else 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α},
  Std.DHashMap.Const.get? (m₁.inter m₂) k = if k ∈ m₂ then Std.DHashMap.Const.get? m₁ k else none
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.image_morphismRestrict_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : TopologicalSpace.Opens ↥↑U),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor ((TopologicalSpace.Opens.map f.base).obj U).ι).obj
      ((TopologicalSpace.Opens.map (f ∣_ U).base).obj V) =
    (TopologicalSpace.Opens.map f.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_truncLT : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : PartialOrder Γ] [inst_2 : DecidableLT Γ] (c : Γ)
  (x : HahnSeries Γ R) (i : Γ), ((HahnSeries.truncLT c) x).coeff i = if i < c then x.coeff i else 0
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.le_next : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.endPos}, p ≤ p.next h
-- Init.Data.List.BasicAux
/-- Auxiliary for `partitionM`:
`partitionM.go p l acc₁ acc₂` returns `(acc₁.toList ++ left, acc₂.toList ++ right)`
if `partitionM p l` returns `(left, right)`.  -/
_private.Init.Data.List.BasicAux.0.List.partitionM.go : {m : Type → Type u_1} → {α : Type} → [Monad m] → (α → m Bool) → List α → Array α → Array α → m (List α × List α)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.star_self_mem_adjoin_singleton : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (x : A), star x ∈ NonUnitalStarAlgebra.adjoin R {x}
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.cast_mul_floor_div_cancel : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  {n : ℕ}, n ≠ 0 → ∀ (a : R), ⌊↑n * a⌋₊ / n = ⌊a⌋₊
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- If `E / F` is an infinite algebraic extension, then there exists an intermediate field
`L / F` with arbitrarily large finite extension degree.  -/
IntermediateField.exists_lt_finrank_of_infinite_dimensional : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E],
  ¬FiniteDimensional F E → ∀ (n : ℕ), ∃ L, FiniteDimensional F ↥L ∧ n < Module.finrank F ↥L
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformAddGroup.ext_iff : ∀ {G : Type u_3} [inst : AddGroup G] {u v : UniformSpace G},
  IsUniformAddGroup G → IsUniformAddGroup G → (u = v ↔ nhds 0 = nhds 0)
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- A set `A` in a compactly coherent space is closed iff for every compact set `K`, the
intersection `K ∩ A` is closed in `K`.  -/
CompactlyCoherentSpace.isClosed_iff : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactlyCoherentSpace X] (A : Set X),
  IsClosed A ↔ ∀ (K : Set X), IsCompact K → IsClosed (Subtype.val ⁻¹' A)
-- Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
/-- Given two continuants `pconts` and `conts` and a value `fr`, this function returns
- `conts.a / conts.b` if `fr = 0`
- `exactConts.a / exactConts.b` where `exactConts = nextConts 1 fr⁻¹ pconts conts`
  otherwise.

This function can be used to compute the exact value approximated by a continued fraction
`GenContFract.of v` as described in lemma `compExactValue_correctness_of_stream_eq_some`.
 -/
GenContFract.compExactValue : {K : Type u_1} → [Field K] → [LinearOrder K] → GenContFract.Pair K → GenContFract.Pair K → K → K
-- Mathlib.NumberTheory.MulChar.Basic
MulCharClass.toMonoidHomClass : ∀ {F : Type u_3} {R : outParam (Type u_4)} {R' : outParam (Type u_5)} {inst : CommMonoid R}
  {inst_1 : CommMonoidWithZero R'} {inst_2 : FunLike F R R'} [self : MulCharClass F R R'], MonoidHomClass F R R'
-- Init.Data.Nat.Basic
Nat.add_sub_add_left : ∀ (k n m : ℕ), k + n - (k + m) = n - m
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)) (n : α),
  ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.obj K).p.f n = (K.X n).p
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop} (j : J),
  RingCat.Colimits.Relation.below ⋯
-- Lean.CoreM
Lean.MonadRuntimeException.tryCatchRuntimeEx : {m : Type → Type} → [self : Lean.MonadRuntimeException m] → {α : Type} → m α → (Lean.Exception → m α) → m α
-- Lean.Environment
Lean.Kernel.instNonemptyException : Nonempty Lean.Kernel.Exception
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.toWeightBasisInt.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : CharZero R], b.toWeightBasisInt = Module.Basis.mk ⋯ ⋯
-- Mathlib.Algebra.Group.Basic
add_sub_left_comm : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a + (b - c) = b + (a - c)
-- Mathlib.CategoryTheory.Topos.Sheaf
/-- The sheaf of closed sieves w/r/t `J`. See also `Functor.closedSieves` and `Sheaf.classifier`  -/
CategoryTheory.Sheaf.Ω : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) → CategoryTheory.Sheaf J (Type (max u v))
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_neg_iff : ∀ {x : ℝ}, 0 < x → (Real.log x < 0 ↔ x < 1)
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.subProdXSubC.eq_1 : ∀ {k : Type u} [inst : Field k] (f : AlgebraicClosure.Monics k),
  AlgebraicClosure.subProdXSubC f =
    Polynomial.map (algebraMap k (MvPolynomial (AlgebraicClosure.Vars k) k)) ↑f -
      ∏ i, (Polynomial.X - Polynomial.C (MvPolynomial.X ⟨f, i⟩))
-- Init.Core
equivalence_true : ∀ (α : Sort u), Equivalence fun x x_1 => True
-- Mathlib.Analysis.RCLike.Sqrt
sqrt_eq_exp : ∀ {z : ℂ}, z ≠ 0 → z.sqrt = Complex.exp (Complex.log z / 2)
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.comp_over_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (S : C)
  [inst_1 : CategoryTheory.OverClass X S] [inst_2 : CategoryTheory.OverClass Y S] [CategoryTheory.HomIsOver f S] {Z : C}
  (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (Y ↘ S) h) =
    CategoryTheory.CategoryStruct.comp (X ↘ S) h
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)),
  ↑↑((NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv K) a).1 =
    Ideal.span {↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet a)}
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.GoodProducts.smaller.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u}),
  Profinite.NobelingProof.GoodProducts.smaller C o =
    ⇑(Profinite.NobelingProof.πs C o) ''
      Profinite.NobelingProof.GoodProducts.range
        (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)
-- Mathlib.Algebra.MonoidAlgebra.Ideal
/-- If `x` belongs to the ideal generated by generators in `s`, then every element of the support of
`x` factors through an element of `s`.

We could spell `∃ d, m = d * m` as `MulOpposite.op m' ∣ MulOpposite.op m` but this would be worse.
 -/
MonoidAlgebra.mem_ideal_span_of_image : ∀ {k : Type u_1} {G : Type u_3} [inst : Monoid G] [inst_1 : Semiring k] {s : Set G} {x : MonoidAlgebra k G},
  x ∈ Ideal.span (⇑(MonoidAlgebra.of k G) '' s) ↔ ∀ m ∈ x.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_finsetSum_cbm : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F)
  (B : ι → E →L[ℝ] F →L[ℝ] G) (s : Finset ι), μ.transpose (∑ i ∈ s, B i) = ∑ i ∈ s, μ.transpose (B i)
-- Std.Internal.Do.PredTrans
/-- Unfolding `<$>` through `apply`.  -/
Std.Internal.Do.PredTrans.apply_map : ∀ {β : Type w} {Pred : Type u} {EPred : Type v} {α : Type w} (trans : Std.Internal.Do.PredTrans Pred EPred α)
  (f : α → β) (post : β → Pred) (epost : EPred), (f <$> trans).apply post epost = trans.apply (post ∘ f) epost
-- Mathlib.Algebra.Order.Group.Lattice
inf_add : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddRightMono α] (a b c : α), a ⊓ b + c = (a + c) ⊓ (b + c)
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.dropEndWhile.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  s.dropEndWhile pat = s.sliceTo (s.skipSuffixWhile pat)
-- Init.Data.BitVec.Lemmas
BitVec.msb_eq_toNat : ∀ {w : ℕ} {x : BitVec w}, x.msb = decide (x.toNat ≥ 2 ^ (w - 1))
-- Mathlib.Order.Filter.AtTopBot.Finite
Filter.strictMono_subseq_of_tendsto_atTop : ∀ {β : Type u_4} [inst : LinearOrder β] [NoMaxOrder β] {u : ℕ → β},
  Filter.Tendsto u Filter.atTop Filter.atTop → ∃ φ, StrictMono φ ∧ StrictMono (u ∘ φ)
-- Std.Time.Format.DateFormat
/-- English (US) locale symbols.
 -/
Std.Time.DateFormatSymbols.enUS : Std.Time.DateFormatSymbols
-- Std.Internal.Do.ExceptPost
Std.Internal.Do.EPost.Cons.mk : {eh : Type u} → {et : Type v} → eh → et → EPost.Cons✝ eh et
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.toZFSet_monotone : Monotone Ordinal.toZFSet
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_mul_unit_right : ∀ {R : Type u_1} [inst : CommSemiring R] {x : R}, IsUnit x → ∀ (y z : R), IsCoprime (y * x) (z * x) ↔ IsCoprime y z
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- An additive group object in a Cartesian monoidal category.  -/
CategoryTheory.AddGrp : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.CartesianMonoidalCategory C] → Type (max u₁ v₁)
-- Init.Data.ByteArray.Basic
/-- Replaces the byte at the given index.

No bounds check is performed, but the function requires a proof that the index is in bounds. This
proof can usually be omitted, and will be synthesized automatically.

The array is modified in-place if there are no other references to it.
 -/
ByteArray.set : (a : ByteArray) → (i : ℕ) → UInt8 → autoParam (i < a.size) ByteArray.set._auto_1 → ByteArray
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsSingular.pos : ∀ {c : Cardinal.{u_1}}, c.IsSingular → 0 < c
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
/-- **Alias** of `infEDist_thickening`. -/
infEdist_thickening : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ : ℝ},
  0 < δ → ∀ (s : Set E) (x : E), Metric.infEDist x (Metric.thickening δ s) = Metric.infEDist x s - ENNReal.ofReal δ
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.instSMulAutFintypeCatObjObjFinite : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) → (X : C) → SMul (CategoryTheory.Aut (F.obj X)) (F.obj X).obj
-- Init.Data.Int.DivMod.Lemmas
Int.sign_eq_ediv_natAbs : ∀ (a : ℤ), a.sign = a / ↑a.natAbs
-- Mathlib.Analysis.Normed.Operator.Banach
/-- The bound `C` so that `‖inverse x‖ ≤ C * ‖x‖` for all `x`.  -/
ContinuousLinearMap.NonlinearRightInverse.nnnorm : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NontriviallyNormedField 𝕜'] →
        {σ : 𝕜 →+* 𝕜'} →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {F : Type u_4} →
                  [inst_4 : NormedAddCommGroup F] →
                    [inst_5 : NormedSpace 𝕜' F] → {f : E →SL[σ] F} → f.NonlinearRightInverse → NNReal
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_read : ∀ (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.read q) = Turing.TM2.Stmt.goto q
-- Mathlib.Algebra.Group.Opposite
AddOpposite.pow : {α : Type u_1} → {β : Type u_2} → [Pow α β] → Pow αᵃᵒᵖ β
-- Mathlib.Algebra.Group.Pi.Lemmas
AddHom.coeFn.eq_1 : ∀ (α : Type u_5) (β : Type u_6) [inst : Add α] [inst_1 : AddCommSemigroup β],
  AddHom.coeFn α β = { toFun := fun g => ⇑g, map_add' := ⋯ }
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.le_def : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C},
  P ≤ Q ↔ ∀ (X : C), P X → Q X
-- Init.Data.BitVec.Basic
/-- Increases the width of a bitvector to one that is at least as large by zero-extending it.

This is a constant-time operation because the underlying `Nat` is unmodified; because the new width
is at least as large as the old one, no overflow is possible.
 -/
BitVec.setWidth' : {n w : ℕ} → n ≤ w → BitVec n → BitVec w
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.dual_isColoop : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsLoop e → M✶.IsColoop e
-- Mathlib.Algebra.Algebra.Subalgebra.Directed
/-- Define an algebra homomorphism on a directed supremum of subalgebras by defining
it on each subalgebra, and proving that it agrees on the intersection of subalgebras.  -/
Subalgebra.iSupLift : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra R B] →
                {ι : Type u_4} →
                  [Nonempty ι] →
                    (K : ι → Subalgebra R A) →
                      Directed (fun x1 x2 => x1 ≤ x2) K →
                        (f : (i : ι) → ↥(K i) →ₐ[R] B) →
                          (∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (Subalgebra.inclusion h)) →
                            (T : Subalgebra R A) → T ≤ iSup K → ↥T →ₐ[R] B
-- Init.Data.SInt.Basic
/-- Bitwise and for 32-bit signed integers. Usually accessed via the `&&&` operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set,
according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.land : Int32 → Int32 → Int32
-- Mathlib.Order.WithBot
WithBot.coe_ne_bot : ∀ {α : Type u_1} {a : α}, ↑a ≠ ⊥
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.exists_mem_basis : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α} {ι : Sort u_18} {p : ι → Prop} {s : ι → Set α},
  f =O[l] g' → l.HasBasis p s → ∃ c > 0, ∃ i, p i ∧ ∀ x ∈ s i, ‖f x‖ ≤ c * ‖g' x‖
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.instSubsingleton : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [Subsingleton Y],
  Subsingleton C(X, Y)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.minKey_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β} {he : Std.ExtDTreeMap.Const.alter t k f ≠ ∅},
  (Std.ExtDTreeMap.Const.alter t k f).minKey he = k ↔
    (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true