mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.enorm_integral_le_lintegral_enorm_transpose : ∀ {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] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  ‖∫ᵛ (a : X), f a ∂[B; μ]‖ₑ ≤ ∫⁻ (a : X), ‖f a‖ₑ ∂(μ.transpose B).variation
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddLeftCancelMonoid : {α : Type u_1} → [AddLeftCancelMonoid α] → AddLeftCancelMonoid αᵒᵈ
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Precomp.map_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left) (i : Fin (n + 1 + 1)),
  CategoryTheory.ComposableArrows.Precomp.map F f i i ⋯ =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Precomp.obj F X i)
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.instIteratorIdSearchStepOfBackwardPattern.match_3.eq_2 : ∀ {ρ : Type} (pat : ρ) (s : String.Slice) (it : Std.IterM Id (String.Slice.Pattern.SearchStep s))
  (motive : Option (s.sliceTo it.internalState.currPos).Pos → Sort u_1)
  (h_1 : (pos : (s.sliceTo it.internalState.currPos).Pos) → none = some pos → motive (some pos))
  (h_2 : none = none → motive none),
  (match h' : none with
    | some pos => h_1 pos h'
    | none => h_2 h') =
    h_2 ⋯
-- Init.Notation
/-- The `run_cmd doSeq` command executes code in `CommandElabM Unit`.
This is the same as `#eval show CommandElabM Unit from discard do doSeq`.
 -/
Lean.runCmd : Lean.ParserDescr
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.foldl_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} {δ : Type w} [Std.TransCmp cmp]
  {f : δ → α → β → δ} {init : δ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.TreeMap.Raw.foldl f init t₁ = Std.TreeMap.Raw.foldl f init t₂
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_closure : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Set α} {x : α},
  x ∈ BooleanSubalgebra.closure s ↔ ∀ ⦃L : BooleanSubalgebra α⦄, s ⊆ ↑L → x ∈ L
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- A gcf terminated at position `n` if its sequence terminates at position `n`.  -/
GenContFract.TerminatedAt : {α : Type u_1} → GenContFract α → ℕ → Prop
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.iSup_map_mulSingle_le : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → MulOneClass (M i)] [inst_1 : DecidableEq ι] {I : Set ι}
  {S : (i : ι) → Submonoid (M i)}, ⨆ i, Submonoid.map (MonoidHom.mulSingle M i) (S i) ≤ Submonoid.pi I S
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.one_lt_rpow_of_pos_of_lt_one_of_neg : ∀ {x : ENNReal} {z : ℝ}, 0 < x → x < 1 → z < 0 → 1 < x ^ z
-- Init.Data.SInt.Lemmas
Int64.neg_mul_not_eq_add_mul : ∀ {a b : Int64}, -(a * ~~~b) = a + a * b
-- Mathlib.Data.Set.Image
Set.Nonempty.preimage' : ∀ {α : Type u_1} {β : Type u_2} {s : Set β}, s.Nonempty → ∀ {f : α → β}, s ⊆ Set.range f → (f ⁻¹' s).Nonempty
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_left_monotone : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → ∀ (a : Ordinal.{u}), Monotone fun x => Ordinal.veblenWith f x a
-- Init.Data.SInt.Lemmas
Int32.ofIntLE.eq_1 : ∀ (i : ℤ) (_hl : Int32.minValue.toInt ≤ i) (_hr : i ≤ Int32.maxValue.toInt), Int32.ofIntLE i _hl _hr = Int32.ofInt i
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedBuilder.default : Std.Http.URI.Builder
-- Lean.Elab.Tactic.Simp
/-- The elaborated simp arguments with syntax  -/
Lean.Elab.Tactic.ElabSimpArgsResult.simpArgs : Lean.Elab.Tactic.ElabSimpArgsResult → Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instIsStableUnderFilteredColimitsIsomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.{w, w', v, u}
    (CategoryTheory.MorphismProperty.isomorphisms C)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.coe_mk : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (s : Con R)
  (h : ∀ {w x y z : R}, s.toSetoid w x → s.toSetoid y z → s.toSetoid (w + y) (x + z)), ⇑{ toCon := s, add' := h } = ⇑s
-- Mathlib.Combinatorics.SimpleGraph.Maps
Equiv.simpleGraph_apply : ∀ {V : Type u_1} {W : Type u_2} (e : V ≃ W) (G : SimpleGraph V), e.simpleGraph G = SimpleGraph.comap (⇑e.symm) G
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_ofNat_add : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (n : ℕ)
  [inst_4 : n.AtLeastTwo] (a : R), ⌈OfNat.ofNat n + a⌉ = OfNat.ofNat n + ⌈a⌉
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Since `Truncated.inclusion` is fully faithful, so is right Kan extension along it.  -/
CategoryTheory.SimplicialObject.Truncated.cosk.fullyFaithful : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n : ℕ) →
      [inst_1 :
          ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
            (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] →
        [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
              (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F] →
          (CategoryTheory.SimplicialObject.Truncated.cosk n).FullyFaithful
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Poly.mulMon.go : ℕ → Nat.Internal.SOM.Mon → Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.baseChange_negY : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Projective R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P : Fin 3 → A), (W'.baseChange B).negY (⇑f ∘ P) = f ((W'.baseChange A).negY P)
-- Std.Data.DTreeMap.Internal.Balanced
/-- Leaf is balanced.  -/
Std.DTreeMap.Internal.Impl.Balanced.leaf : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.leaf.Balanced
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
/-- `recF` is used as a basis for defining the recursor on `Fix F α`. `recF`
traverses recursively the W-type generated by `q.P` using a function on `F`
as a recursive step  -/
MvQPF.recF : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} →
    [q : MvQPF F] → {α : TypeVec.{u} n} → {β : Type u} → (F (α ::: β) → β) → (MvQPF.P F).W α → β
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.fst_comp_inr : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W},
  (Representation.IntertwiningMap.fst A ρ σ).comp (Representation.IntertwiningMap.inr A ρ σ) = 0
-- Mathlib.Data.NNReal.Defs
/-- Extension for the `positivity` tactic: `Real.toNNReal`  -/
Mathlib.Meta.Positivity.evalRealToNNReal : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- The canonical isomorphism relating `parallelPair f.op g.op` and `(parallelPair f g).op`  -/
CategoryTheory.Limits.parallelPairOpIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (f g : X ⟶ Y) →
        CategoryTheory.Limits.parallelPair f.op g.op ≅
          CategoryTheory.Limits.walkingParallelPairOpEquiv.functor.comp (CategoryTheory.Limits.parallelPair f g).op
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- **Alias** of `AddMonoidAlgebra.sup_support_coeff_add_le`. -/
AddMonoidAlgebra.sup_support_add_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : SemilatticeSup B] [inst_1 : OrderBot B] [inst_2 : Semiring R]
  (degb : A → B) (f g : AddMonoidAlgebra R A),
  (f + g).coeff.support.sup degb ≤ f.coeff.support.sup degb ⊔ g.coeff.support.sup degb
-- Mathlib.Analysis.Convex.Cone.Dual
LinearMap.toContPerfPair.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : TopologicalSpace R]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : TopologicalSpace M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : TopologicalSpace N] (p p_1 : M →ₗ[R] N →ₗ[R] R) (e_p : p = p_1)
  [inst_8 : p.IsContPerfPair] [inst_9 : IsTopologicalRing R], p.toContPerfPair = p_1.toContPerfPair
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.delabHtmlElement : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Order.Lattice
sup_eq_inf : ∀ {α : Type u} [inst : Lattice α] {a b : α}, a ⊔ b = a ⊓ b ↔ a = b
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instMulAction.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α],
  Lex.instMulAction = { toSMul := Lex.instSMul', mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
minSmoothness_of_isRCLikeNormedField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [h : IsRCLikeNormedField 𝕜] {n : WithTop ℕ∞}, minSmoothness 𝕜 n = n
-- Mathlib.Order.BooleanGenerators
/-- The elements in a collection of Boolean generators are all atoms.  -/
IsCompactlyGenerated.BooleanGenerators.isAtom : ∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α}, IsCompactlyGenerated.BooleanGenerators S → ∀ I ∈ S, IsAtom I
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtTarget.of_forall_source_exists_preimage : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  {X Y : AlgebraicGeometry.Scheme} [P.RespectsRight AlgebraicGeometry.IsOpenImmersion]
  [P.HasOfPostcompProperty AlgebraicGeometry.IsOpenImmersion] (f : X ⟶ Y),
  (∀ (x : ↥X), ∃ U, f x ∈ U ∧ P (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι f)) →
    P f
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.contDiff_rpow_const_of_le : ∀ {p : ℝ} {n : ℕ}, ↑n ≤ p → ContDiff ℝ ↑n fun x => x ^ p
-- Lean.Parser.Do
Lean.Parser.Term.doIfLetPure.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.bitblast_le_size : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (input : Std.Tactic.BVDecide.BVExpr.WithCache (Std.Tactic.BVDecide.BVExpr w) aig),
  aig.decls.size ≤ (↑(Std.Tactic.BVDecide.BVExpr.bitblast aig input).result).aig.decls.size
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.iteratedFDeriv_right' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {m : WithTop ℕ∞}
  {i : ℕ}, ContDiff 𝕜 (m + ↑i) f → ContDiff 𝕜 m (iteratedFDeriv 𝕜 i f)
-- Mathlib.Order.WithBot
WithTop.eq_top_iff_forall_ne : ∀ {α : Type u_1} {x : WithTop α}, x = ⊤ ↔ ∀ (a : α), ↑a ≠ x
-- Init.System.IO
/-- Converts `s` to a string using its `ToString α` instance, and prints it with a trailing newline to
the current standard output (as determined by `IO.getStdout`).
 -/
IO.println : {α : Type u_1} → [ToString α] → α → IO Unit
-- Mathlib.NumberTheory.NumberField.EquivReindex
/-- The basis matrix for the embeddings of `K` into `ℂ`. This matrix is formed by
taking the lattice basis vectors of `K` and reindexing them according to the
equivalence `equivReindex`, then transposing the resulting matrix.  -/
NumberField.basisMatrix : (K : Type u_1) → [inst : Field K] → [NumberField K] → Matrix (K →+* ℂ) (K →+* ℂ) ℂ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_erase_eq_iff_not_compare_eq_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, (t.erase k).minKey he = t.minKey ⋯ ↔ ¬cmp k (t.minKey ⋯) = Ordering.eq
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Truncated.instHasColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} [CategoryTheory.Limits.HasColimits C],
  CategoryTheory.Limits.HasColimits (CategoryTheory.CosimplicialObject.Truncated C n)
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_top_right_le_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, ⁅H, ⊤⁆ ≤ H ↔ H.Normal
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffAt_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E}, ContDiffAt 𝕜 0 f x ↔ ∃ u ∈ nhds x, ContinuousOn f u
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.relabelAux.eq_1 : ∀ {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) (k : ℕ),
  FirstOrder.Language.BoundedFormula.relabelAux g k =
    Sum.map id ⇑finSumFinEquiv ∘ ⇑(Equiv.sumAssoc β (Fin n) (Fin k)) ∘ Sum.map g id
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- For every vertex `a`, there is a canonical hom from the root, given by the path in the tree.  -/
IsFreeGroupoid.SpanningTree.treeHom : {G : Type u} →
  [inst : CategoryTheory.Groupoid G] →
    [inst_1 : IsFreeGroupoid G] →
      (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) →
        [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] →
          (a : G) → IsFreeGroupoid.SpanningTree.root'✝ T ⟶ a
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.id_apply : ∀ {α : Type u_2} [inst : SupSet α] (a : α), (sSupHom.id α) a = a
-- Mathlib.Tactic.Module
/-- Given two terms `l₁`, `l₂` of type `qNF R M`, i.e. lists of `(Q($R) × Q($M)) × ℕ`s (two `Expr`s
and a natural number), recursively construct a proof that in the `$R`-module `$M`, the difference
of the "linear combinations" represented by `l₁` and `l₂` is the linear combination represented by
`Module.qNF.sub iR l₁ l₁`.  -/
Mathlib.Tactic.Module.qNF.mkSubProof : {u v : Lean.Level} →
  {M : Q(Type v)} →
    {R : Q(Type u)} →
      (iR : Q(Ring «$R»)) →
        (iM : Q(AddCommGroup «$M»)) →
          (iRM : Q(Module «$R» «$M»)) →
            (l₁ l₂ : Mathlib.Tactic.Module.qNF R M) →
              have a := (Mathlib.Tactic.Module.qNF.sub iR l₁ l₂).toNF;
              have a_1 := l₂.toNF;
              have a_2 := l₁.toNF;
              Q(«$a_2».eval - «$a_1».eval = «$a».eval)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.id.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (X : CategoryTheory.Grothendieck F),
  X.id = { base := CategoryTheory.CategoryStruct.id X.base, fiber := CategoryTheory.eqToHom ⋯ }
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.Commute.self_zpow : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  (A : Matrix n' n' R) (n : ℤ), Commute A (A ^ n)
-- Lean.Parser.Basic
Lean.Parser.manyNoAntiquot : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.linearOrderedCommGroupWithZero : {α : Type u_1} →
  [inst : Field α] → [inst_1 : LinearOrder α] → [IsStrictOrderedRing α] → LinearOrderedCommGroupWithZero { x // 0 ≤ x }
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneRightOpOfCoconeEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C},
  CategoryTheory.Limits.coneRightOpOfCoconeEquiv =
    CategoryTheory.Equivalence.mk''
      { obj := fun c => CategoryTheory.Limits.coneRightOpOfCocone (Opposite.unop c),
        map := fun {Y X} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }
      { obj := fun c => Opposite.op (CategoryTheory.Limits.coconeOfConeRightOp c),
        map := fun {Y X} f => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }
      (CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)ᵒᵖ))
      (CategoryTheory.Iso.refl
        ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coconeOfConeRightOp c),
              map := fun {Y X} f => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp
          { obj := fun c => CategoryTheory.Limits.coneRightOpOfCocone (Opposite.unop c),
            map := fun {Y X} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }))
      ⋯
-- Init.Data.String.Decode
ByteArray.isUTF8FirstByte_of_isSome_utf8DecodeChar? : ∀ {b : ByteArray} {i : ℕ} (h : (b.utf8DecodeChar? i).isSome = true), b[i].IsUTF8FirstByte
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_pi_apply : ∀ {A : Type u_2} {ι : Type u_3} {E : ι → Type u_4} (x : WithCStarModule A ((i : ι) → E i)) (i : ι),
  (WithCStarModule.equiv A ((i : ι) → E i)) x i = x i
-- Mathlib.GroupTheory.Coset.Basic
/-- An equivalence between any two fibers of a surjective `AddMonoidHom`.  -/
AddMonoidHom.fiberEquivOfSurjective : {α : Type u_1} →
  [inst : AddGroup α] →
    {H : Type u_2} →
      [inst_1 : AddGroup H] → {f : α →+ H} → Function.Surjective ⇑f → (h h' : H) → ↑(⇑f ⁻¹' {h}) ≃ ↑(⇑f ⁻¹' {h'})
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.derivFamily_lt_ord_lift : ∀ {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}} {c : Cardinal.{max u v}},
  c.IsRegular →
    Cardinal.lift.{v, u} (Cardinal.mk ι) < c →
      c ≠ Cardinal.aleph0 →
        (∀ (i : ι), ∀ b < c.ord, f i b < c.ord) → ∀ {a : Ordinal.{max u v}}, a < c.ord → Ordinal.derivFamily f a < c.ord
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.toWord_of : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), (FreeGroup.of a).toWord = [(a, true)]
-- Mathlib.NumberTheory.Dioph
IsPoly.below.const : ∀ {α : Type u_1} {motive : (a : (α → ℕ) → ℤ) → IsPoly a → Prop} (n : ℤ), IsPoly.below ⋯
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsClosed.completeSpace_coe : ∀ {α : Type u} [inst : UniformSpace α] [CompleteSpace α] {s : Set α} [hs : IsClosed s], CompleteSpace ↑s
-- Mathlib.Data.Finset.Attach
Finset.mem_attach : ∀ {α : Type u_1} (s : Finset α) (x : ↥s), x ∈ s.attach
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getD_eq_getValueCastD : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {fallback : β a},
      m.getD a fallback = Std.Internal.List.getValueCastD a (Std.DHashMap.Internal.toListModel (↑m).buckets) fallback
-- Mathlib.Algebra.Ring.Fin
/-- The product over `Fin 2` of some rings is just the Cartesian product of these rings.  -/
RingEquiv.piFinTwo : (R : Fin 2 → Type u_1) → [inst : (i : Fin 2) → Semiring (R i)] → ((i : Fin 2) → R i) ≃+* R 0 × R 1
-- Mathlib.Algebra.Group.Defs
IsAddRightRegular.add_eq_zero_symm : ∀ {M : Type u_2} [inst : AddMonoid M] {a b : M}, IsAddRightRegular a → b + a = 0 → a + b = 0
-- Mathlib.RingTheory.HahnSeries.Multiplication
Finset.VAddAntidiagonal.congr_simp : ∀ {G : Type u_1} {P : Type u_2} [inst : VAdd G P] {s s_1 : Set G} (e_s : s = s_1) {t t_1 : Set P} (e_t : t = t_1)
  (a a_1 : P) (e_a : a = a_1) (h : (s.vaddAntidiagonal t a).Finite),
  Finset.VAddAntidiagonal a h = Finset.VAddAntidiagonal a_1 ⋯
-- Init.Control.MonadAttach
/-- A `MonadAttach` instance where all return values are possible and `attach` adds no
information to the return value, except a trivial proof of `True`.

This instance is used whenever no more useful `MonadAttach` instance can be implemented.
It always has a `WeaklyLawfulMonadAttach`, but usually no `LawfulMonadAttach` instance.
 -/
MonadAttach.trivial : {m : Type u → Type v} → [Monad m] → MonadAttach m
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableMul.measurable_mul_const : ∀ {M : Type u_2} {inst : MeasurableSpace M} {inst_1 : Mul M} [self : MeasurableMul M] (c : M), Measurable fun x => x * c
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.presheaf_mono_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [(CategoryTheory.forget D).ReflectsIsomorphisms] {F G : CategoryTheory.Sheaf J D} (f : F ⟶ G) [CategoryTheory.Mono f],
  CategoryTheory.Mono f.hom
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.hasLimits : CategoryTheory.Limits.HasLimits AddCommMonCat
-- Lean.Elab.Do.Control
_private.Lean.Elab.Do.Control.0.Lean.Elab.Do.mkInstMonad : Lean.Elab.Do.MonadInfo → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_restrict₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s (μ.restrict t) → (μ.restrict t).restrict s = μ.restrict (s ∩ t)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.op_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P),
  (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).op = CategoryTheory.Limits.BinaryFan.mk ι₁.op ι₂.op
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_neg_neg : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : AddGroup N] (f g : α →₀ N),
  (-f).neLocus (-g) = f.neLocus g
-- Mathlib.Order.Interval.Basic
/-- `{a}` as an interval.  -/
NonemptyInterval.pure : {α : Type u_1} → [inst : Preorder α] → α → NonemptyInterval α
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
tendsto_uniformity_iff_dist_tendsto_zero : ∀ {α : Type u} {ι : Type u_2} [inst : PseudoMetricSpace α] {f : ι → α × α} {p : Filter ι},
  Filter.Tendsto f p (uniformity α) ↔ Filter.Tendsto (fun x => dist (f x).1 (f x).2) p (nhds 0)
-- Mathlib.Algebra.Star.MonoidHom
/-- Construct a `StarMulEquiv` from an equivalence in some type which preserves `*` and `star`.  -/
StarMulEquiv.ofClass : {F : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : Mul A] →
        [inst_1 : Mul B] →
          [inst_2 : Star A] →
            [inst_3 : Star B] → [inst_4 : EquivLike F A B] → [MulEquivClass F A B] → [StarHomClass F A B] → F → A ≃⋆* B
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.isEmbedding_coe_ennreal : Topology.IsEmbedding ENNReal.toEReal
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isLittleO_abs_abs`. -/
Asymptotics.IsLittleO.abs_abs : ∀ {α : Type u_1} {l : Filter α} {u v : α → ℝ}, u =o[l] v → (fun x => |u x|) =o[l] fun x => |v x|
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- A real function whose derivative tends to minus infinity from the left at a point is not
differentiable on the left at that point  -/
not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio : ∀ (f : ℝ → ℝ) {a : ℝ},
  Filter.Tendsto (deriv f) (nhdsWithin a (Set.Iio a)) Filter.atBot → ¬DifferentiableWithinAt ℝ f (Set.Iio a) a
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.map_neg : ∀ {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) (a : L), D (-a) = -D a