mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm_tmul : ∀ (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ}
  [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : Module B M]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
  [inst_12 : AddCommMonoid N] [inst_13 : Module R N] [inst_14 : AddCommMonoid P] [inst_15 : Module A P]
  [inst_16 : AddCommMonoid Q] [inst_17 : Module R Q] [inst_18 : Module R P] [inst_19 : IsScalarTower R A P]
  [inst_20 : Algebra A B] [inst_21 : IsScalarTower A B M] [inst_22 : CommSemiring S] [inst_23 : Algebra R S]
  [inst_24 : Algebra S B] [inst_25 : Module S M] [inst_26 : Module S N] [inst_27 : IsScalarTower R S M]
  [inst_28 : SMulCommClass A S M] [inst_29 : SMulCommClass S A M] [inst_30 : IsScalarTower S B M]
  [inst_31 : IsScalarTower R S N] (m : M) (n : N) (p : P) (q : Q),
  (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S A B M N P Q).symm (m ⊗ₜ[A] p ⊗ₜ[S] (n ⊗ₜ[R] q)) =
    m ⊗ₜ[S] n ⊗ₜ[A] (p ⊗ₜ[R] q)
-- Init.System.IOError
IO.Error.resourceExhausted.sizeOf_spec : ∀ (filename : Option String) (osCode : UInt32) (details : String),
  sizeOf (IO.Error.resourceExhausted filename osCode details) = 1 + sizeOf filename + sizeOf osCode + sizeOf details
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.sum_restrict : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ → (MeasureTheory.Measure.sum fun g => μ.restrict (g +ᵥ s)) = μ
-- Batteries.Data.List.Lemmas
List.findIdxNth_cons_of_neg : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} {n : ℕ} {a : α},
  p a = false → List.findIdxNth p (a :: xs) n = List.findIdxNth p xs n + 1
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.range_fst_comp : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S),
  Set.range ⇑(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) f) =
    Set.range ⇑f ∩ Set.range ⇑g
-- Mathlib.Logic.Equiv.Multiset
/-- `raise l n` is a non-decreasing sequence.  -/
Denumerable.raise_sorted : ∀ (l : List ℕ) (n : ℕ), (Denumerable.raise l n).SortedLE
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The inverse functor of `ofStructuredArrowProjEquivalence.functor`.  -/
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor D T) →
          (Y : T) →
            (X : D) →
              CategoryTheory.Functor (CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F))
                (CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F))
-- Mathlib.Algebra.Group.Graph
/-- **Line test** for group isomorphisms.

Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on both
factors and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` and every
"horizontal line" `{(h, i) | h : H}` at most once. Then the image of `f` is the graph of some group
isomorphism `f' : H ≃ I`.  -/
MonoidHom.exists_mulEquiv_range_eq_graph : ∀ {G : Type u_1} {H : Type u_2} {I : Type u_3} [inst : Group G] [inst_1 : Group H] [inst_2 : Group I] {f : G →* H × I},
  Function.Surjective (Prod.fst ∘ ⇑f) →
    Function.Surjective (Prod.snd ∘ ⇑f) →
      (∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) → ∃ e, f.range = e.toMonoidHom.graph
-- Mathlib.Algebra.Algebra.Tower
/-- If `A` is an `R`-algebra such that the induced morphism `R →+* A` is surjective, then the
`R`-module generated by a set `X` equals the `A`-module generated by `X`.  -/
Submodule.restrictScalars_span : ∀ (R : Type u) (A : Type w) {M : Type v₁} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M],
  Function.Surjective ⇑(algebraMap R A) →
    ∀ (X : Set M), Submodule.restrictScalars R (Submodule.span A X) = Submodule.span R X
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Finsupp.isAffineMap_eval : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {ι : Type u_3}
  {X : Type u_4} [inst_3 : Zero X] [inst_4 : Convexity.ConvexSpace R X] {i : ι}, Convexity.IsAffineMap R fun x => x i
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l →
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey?
            k' =
          some k
-- Mathlib.Topology.Connected.Clopen
/-- Coercion from a topological space to the set of connected components of this space.  -/
ConnectedComponents.mk : {α : Type u} → [inst : TopologicalSpace α] → α → ConnectedComponents α
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap_op : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S),
  (Submodule.equivOpposite.symm (MulOpposite.op M)).mulMap (Submodule.equivOpposite.symm (MulOpposite.op N)) =
    ↑(MulOpposite.opLinearEquiv R) ∘ₗ
      N.mulMap M ∘ₗ
        ↑(TensorProduct.congr ((MulOpposite.opLinearEquiv R).symm.ofSubmodule' M)
              ((MulOpposite.opLinearEquiv R).symm.ofSubmodule' N) ≪≫ₗ
            TensorProduct.comm R ↥M ↥N)
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_ofFin : ∀ {n : Fin UInt16.size}, (UInt16.ofFin n).toUInt64 = UInt64.ofNatLT ↑n ⋯
-- Init.Data.List.Find
List.IsPrefix.findSome?_eq_none : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f : α → Option β},
  l₁ <+: l₂ → List.findSome? f l₂ = none → List.findSome? f l₁ = none
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.rankFinite_iff : ∀ {α : Type u_1} (M : Matroid α), M.RankFinite ↔ ∃ B, M.IsBase B ∧ B.Finite
-- Mathlib.Order.UpperLower.Closure
instDecidablePredMemLowerClosure : {α : Type u_1} →
  [inst : Preorder α] →
    {s : Set α} → [DecidablePred fun x => ∃ a ∈ s, x ≤ a] → DecidablePred fun x => x ∈ lowerClosure s
-- Init.Data.BitVec.Lemmas
BitVec.le_toInt : ∀ {w : ℕ} (x : BitVec w), -2 ^ (w - 1) ≤ x.toInt
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- `f₊ g` is the left Kan lift of `g` along `f`.
```
            b
          ◹ |
   f₊ g /   |
      /     | f
    /       ▽
  c - - - ▷ a
       g
```
 -/
CategoryTheory.Bicategory.«term_₊_» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.mk : ∀ {α : Type u_1} {β : Type u_2} {H G : Graph α β},
  H.IsInducedSubgraph G → (∀ ⦃e : β⦄ ⦃x : α⦄, G.Inc e x → x ∈ H.vertexSet → e ∈ H.edgeSet) → H.IsClosedSubgraph G
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.instMulAction : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      [DecidableEq ι] → [(i : ι) → DecidableEq (M i)] → MulAction (Monoid.CoprodI M) (Monoid.CoprodI.Word M)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.isZero_truncLE_obj_of_isGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ → ∀ (X : C) [t.IsGE X n₁], CategoryTheory.Limits.IsZero ((t.truncLE n₀).obj X)
-- Mathlib.Algebra.Order.Module.Synonym
OrderDual.instModule : {α : Type u_1} → {β : Type u_2} → [inst : Semiring α] → [inst_1 : AddCommMonoid β] → [Module α β] → Module αᵒᵈ β
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.add_isLittleO : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {l : Filter α}
  {f₁ f₂ : α → E'} {g : α → F}, f₁ =Θ[l] g → f₂ =o[l] g → (f₁ + f₂) =Θ[l] g
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (t.alter k f).maxKey? = some k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- If `G` preserves the product of `(X,Y)`, then the product comparison map for `G` at `(X,Y)` is
an isomorphism.
 -/
CategoryTheory.Limits.PreservesLimitPair.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          (X Y : C) →
            [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y] →
              [inst_3 : CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)] →
                [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G] →
                  G.obj (X ⨯ Y) ≅ G.obj X ⨯ G.obj Y
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instIsScalarTowerAdicCompletion : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [inst_2 : Field K]
  [inst_3 : CommSemiring S] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K]
  (v : IsDedekindDomain.HeightOneSpectrum R) [inst_6 : Algebra S K] {S₀ : Type u_4} [inst_7 : CommSemiring S₀]
  [inst_8 : Algebra S₀ S] [inst_9 : Algebra S₀ K] [IsScalarTower S₀ S K],
  IsScalarTower S₀ S (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Mathlib.Topology.UniformSpace.UniformConvergence
UniformContinuous₂.tendstoUniformly : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {x : α} [inst_1 : UniformSpace α]
  [inst_2 : UniformSpace γ] {f : α → β → γ}, UniformContinuous₂ f → TendstoUniformly f (f x) (nhds x)
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
LinearMap.linearProjOfIsCompl.congr_simp : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (q q_1 : Submodule R E)
  (e_q : q = q_1) {F : Type u_7} [inst_3 : AddCommGroup F] [inst_4 : Module R F] (i i_1 : F →ₗ[R] E) (e_i : i = i_1)
  (hi : Function.Injective ⇑i) (h : IsCompl i.range q),
  LinearMap.linearProjOfIsCompl q i hi h = LinearMap.linearProjOfIsCompl q_1 i_1 ⋯ ⋯
-- Mathlib.RingTheory.Coalgebra.GroupLike
GroupLike.val_inj : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] {a b : GroupLike R A}, ↑a = ↑b ↔ a = b
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Option.isSome.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (val : α) → motive (some val)) (h_2 : Unit → motive none),
  (match none with
    | some val => h_1 val
    | none => h_2 ()) =
    h_2 ()
-- Aesop.Stats.Basic
Aesop.instToJsonRuleStats.toJson : Aesop.RuleStats → Lean.Json
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientAt_const : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (x : F) (c : 𝕜), HasGradientAt (fun x => c) 0 x
-- Lean.Meta.Tactic.Simp.SimpTheorems
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.mkSimpTheoremCore : Lean.Meta.Origin →
  Lean.Expr → Array Lean.Name → Lean.Expr → Bool → ℕ → Bool → optParam Bool false → Lean.MetaM Lean.Meta.SimpTheorem
-- Init.System.FilePath
System.FilePath.mk : String → System.FilePath
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.coe_injective : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N],
  Function.Injective DFunLike.coe
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.equivWeakDual_apply : ∀ (𝕜 : Type u_3) [inst : NormedField 𝕜] (E : Type u_7) [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] (x : E →L[𝕜] 𝕜), (PointwiseConvergenceCLM.equivWeakDual 𝕜 E) x = x
-- Mathlib.RingTheory.Congruence.Basic
RingCon.instIsCentralScalarQuotient : ∀ {α : Type u_1} {R : Type u_3} [inst : Add R] [inst_1 : MulOneClass R] [inst_2 : SMul α R]
  [inst_3 : IsScalarTower α R R] (c : RingCon R) [inst_4 : SMul αᵐᵒᵖ R] [inst_5 : IsCentralScalar α R],
  IsCentralScalar α c.Quotient
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_3.splitter : {n : ℕ} →
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1) →
    (acc : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth) →
        (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty) →
          ((l' : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
              motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l')) →
            (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit) → motive acc
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.SheafedSpace.sheaf.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : AlgebraicGeometry.SheafedSpace C),
  X.sheaf = { obj := X.presheaf, property := ⋯ }
-- Mathlib.Algebra.Divisibility.Basic
one_dvd : ∀ {α : Type u_1} [inst : Monoid α] (a : α), 1 ∣ a
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instPartialOrder : {ι : Type u_1} →
  {α : ι → Type u_2} → [inst : (i : ι) → Zero (α i)] → [(i : ι) → PartialOrder (α i)] → PartialOrder (Π₀ (i : ι), α i)
-- Mathlib.Topology.WithTopology
WithTopology.toTopology_injective : ∀ {X : Type u_1} (t : TopologicalSpace X), Function.Injective (WithTopology.toTopology t)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc : ∀ {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : NormedRing 𝕜] [inst_3 : Module 𝕜 E] [inst_4 : IsBoundedSMul 𝕜 E] (k : 𝕜)
  (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
  ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (k • f)) =ᵐ[μ] k • ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Normed space (which is actually a seminorm in general) structure constructed from a
`PreInnerProductSpace.Core` structure  -/
InnerProductSpace.Core.toNormedSpace : {𝕜 : Type u_1} →
  {F : Type u_3} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] → [inst_2 : Module 𝕜 F] → [c : PreInnerProductSpace.Core 𝕜 F] → NormedSpace 𝕜 F
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.map : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing A'] [inst_3 : Algebra R A] [inst_4 : Algebra R A'],
  AlgebraicIndependent R x →
    ∀ {f : A →ₐ[R] A'}, Set.InjOn ⇑f ↑(Algebra.adjoin R (Set.range x)) → AlgebraicIndependent R (⇑f ∘ x)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_nonneg : ∀ {d : ℤ}, d ≤ 0 → ∀ (n : ℤ√d), 0 ≤ n.norm
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro
/-- Shapiro's lemma: given a subgroup `S ≤ G` and an `S`-representation `A`, we have
`Hₙ(G, Ind_S^G(A)) ≅ Hₙ(S, A).`  -/
groupHomology.indIso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (S : Subgroup G) →
        [DecidableEq G] → (A : Rep.{u, u, u} k ↥S) → (n : ℕ) → groupHomology (Rep.ind S.subtype A) n ≅ groupHomology A n
-- Mathlib.Algebra.FreeMonoid.Basic
/-- Recursor for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of `[]` and `x :: xs`.  -/
FreeMonoid.recOn : {α : Type u_1} →
  {motive : FreeMonoid α → Sort u_6} →
    (xs : FreeMonoid α) →
      motive 1 → ((x : α) → (xs : FreeMonoid α) → motive xs → motive (FreeMonoid.of x * xs)) → motive xs
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stmts₁_self : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {q : Turing.TM1.Stmt Γ Λ σ}, q ∈ Turing.TM1.stmts₁ q
-- Mathlib.Data.Vector.Snoc
List.Vector.replicate_succ_to_snoc : ∀ {α : Type u_1} {n : ℕ} (val : α), List.Vector.replicate (n + 1) val = (List.Vector.replicate n val).snoc val
-- Mathlib.Data.Sym.Sym2
/-- A type `α` is naturally included in the diagonal of `α × α`, and this function gives the image
of this diagonal in `Sym2 α`.
 -/
Sym2.diag : {α : Type u_1} → α → Sym2 α
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.mem_lpMeas_indicatorConstLp : ∀ {α : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {p : ENNReal} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} (hm : m ≤ m0) {μ : MeasureTheory.Measure α} {s : Set α}
  (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) {c : F},
  MeasureTheory.indicatorConstLp p ⋯ hμs c ∈ MeasureTheory.lpMeas F 𝕜 m p μ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushout_inr_inv_inl_of_right_isIso_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g] {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pushout.inl f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Tactic.Sat.FromLRAT
/-- Returns `a` and `pr : reify v c a` given a clause `c`  -/
Mathlib.Tactic.Sat.buildReify.reifyClause : ℕ → Lean.Expr → Lean.Expr × Lean.Expr
-- Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
MeasureTheory.pow_mul_meas_ge_le_eLpNorm : ∀ {α : Type u_1} {ε' : Type u_3} {m0 : MeasurableSpace α} [inst : TopologicalSpace ε'] [inst_1 : ContinuousENorm ε']
  {p : ENNReal} (μ : MeasureTheory.Measure α),
  p ≠ 0 →
    p ≠ ⊤ →
      ∀ {f : α → ε'},
        MeasureTheory.AEStronglyMeasurable f μ →
          ∀ (ε : ENNReal), (ε * μ {x | ε ≤ ‖f x‖ₑ ^ p.toReal}) ^ (1 / p.toReal) ≤ MeasureTheory.eLpNorm f p μ
-- Mathlib.Algebra.Star.Module
IsSelfAdjoint.selfAdjointPart_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] {x : A} (hx : IsSelfAdjoint x), (selfAdjointPart R) x = ⟨x, hx⟩
-- Mathlib.Analysis.ODE.Basic
/-- `IsIntegralCurveOn γ v s` means `γ t` is tangent to `v t (γ t)` within `s` for all `t ∈ s`.  -/
IsIntegralCurveOn : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (ℝ → E) → (ℝ → E → E) → Set ℝ → Prop
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_equiv' : ∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (e : ι ≃ ι') {f : ι' → M} {g : ι → M},
  f ∘ ⇑e = g → (LinearIndependent R g ↔ LinearIndependent R f)
-- Init.Data.String.Iterate
String.Slice.length : String.Slice → ℕ
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.curryAddEquiv.eq_1 : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N],
  AddMonoidAlgebra.curryAddEquiv =
    AddMonoidAlgebra.coeffAddEquiv.trans
      (Finsupp.curryAddEquiv.trans
        ((Finsupp.mapRange.addEquiv AddMonoidAlgebra.coeffAddEquiv.symm).trans AddMonoidAlgebra.coeffAddEquiv.symm))
-- Mathlib.Data.Set.Image
Set.image_inter_subset : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α), f '' (s ∩ t) ⊆ f '' s ∩ f '' t
-- Lean.Elab.Do.Basic
/-- Elaborate the `DoElemCont` with the `deadCode` flag set to `deadSyntactically` to emit warnings.  -/
Lean.Elab.Do.DoElemCont.elabAsSyntacticallyDeadCode : Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Unit
-- Init.Data.Nat.Basic
Nat.add_succ : ∀ (n m : ℕ), n + m.succ = (n + m).succ
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_nonpos_iff : ∀ {x : ℝ}, Real.arsinh x ≤ 0 ↔ x ≤ 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- Two finite measures on a Borel space are equal if they agree on all open-closed intervals.  If
`α` is a conditionally complete linear order with no top element,
`MeasureTheory.Measure.ext_of_Ioc` is an extensionality lemma with weaker assumptions on `μ` and
`ν`.  -/
MeasureTheory.Measure.ext_of_Ioc_finite : ∀ {α : Type u_5} [inst : TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α]
  [inst_2 : LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure μ],
  μ Set.univ = ν Set.univ → (∀ ⦃a b : α⦄, a < b → μ (Set.Ioc a b) = ν (Set.Ioc a b)) → μ = ν
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- For `f : 𝕜 → 𝕜` continuous on a compact set `s`, `cfc f` is continuous on the set of `a : A`
satisfying the predicate `p` (associated to `𝕜`) and whose `𝕜`-spectrum is contained in `s`.  -/
continuousOn_cfc : ∀ {𝕜 : Type u_2} (A : Type u_3) {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜),
      autoParam (ContinuousOn f s) continuousOn_cfc._auto_1 → ContinuousOn (cfc f) {a | p a ∧ spectrum 𝕜 a ⊆ s}
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.coe_neLocus : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → Zero (N a)] (f g : Π₀ (a : α), N a), ↑(f.neLocus g) = {x | f x ≠ g x}
-- Init.Data.Int.Order
Int.neg_nonpos_of_nonneg : ∀ {a : ℤ}, 0 ≤ a → -a ≤ 0
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- **Alias** of `sub_apply`. -/
SchwartzMap.sub_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Sub β}
  {inst_2 : Sub F} [self : IsSubApply F α β] (f g : F) (x : α), (f - g) x = f x - g x
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.stdPart_epsilon : ArchimedeanClass.stdPart Hyperreal.epsilon = 0
-- Mathlib.NumberTheory.LSeries.Dirichlet
ArithmeticFunction.const_one_eq_zeta : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] {n : ℕ}, n ≠ 0 → 1 n = ↑((fun x => ArithmeticFunction.zeta x) n)
-- Mathlib.GroupTheory.Index
AddSubgroup.finite_quotient_of_finiteIndex : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} [H.FiniteIndex], Finite (G ⧸ H)
-- Lean.Meta.Basic
/-- `nargs? = some n` if the cached information was computed assuming the function has arity `n`.
  If `nargs? = none`, then the cache information consumed the arrow type as much as possible
  using the current transparency setting.
X -/
Lean.Meta.InfoCacheKey.nargs? : Lean.Meta.InfoCacheKey → Option ℕ
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsIsoAppTruncLTιObjTruncGETruncLT : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C),
  CategoryTheory.IsIso ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))