mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.Primrec.List
_private.Mathlib.Computability.Primrec.List.0.prim : {β : Type u_2} →
  [inst : Primcodable β] → (Nat.Primrec fun n => Encodable.encode (Encodable.decode n)) → Primcodable (List β)
-- Mathlib.Data.Set.Prod
Set.range.eq_1 : ∀ {α : Type u} {ι : Sort u_1} (f : ι → α), Set.range f = {x | ∃ y, f y = x}
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.not_revMatchesAt_of_get_ne : ∀ {c : Char} {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.startPos},
  (pos.prev h).get ⋯ ≠ c → ¬String.Slice.Pattern.Model.RevMatchesAt c pos
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_sub : ∀ (x y : ℝ), Real.sin (x - y) = Real.sin x * Real.cos y - Real.cos x * Real.sin y
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.asStringAux : Bool → String.Pos.Raw → (String → String) → Lean.Parser.ParserFn
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr.eq_9 : ∀ (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret k.cons₂) =
    Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- The reflection associated to a coroot.  -/
RootPairing.coreflection : {ι : 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] → RootPairing ι R M N → ι → N ≃ₗ[R] N
-- Lean.Server.References
Lean.Server.RefInfo.mk : Option Lean.Server.Reference → Array Lean.Server.Reference → Lean.Server.RefInfo
-- Mathlib.Topology.Constructions.SumProd
Topology.IsInducing.sumElim_of_separatedNhds : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z},
  Topology.IsInducing f →
    Topology.IsInducing g → SeparatedNhds (Set.range f) (Set.range g) → Topology.IsInducing (Sum.elim f g)
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.foldl : {α : Type u} → {cmp : α → α → Ordering} → {δ : Type w} → (δ → α → δ) → δ → Std.TreeSet.Raw α cmp → δ
-- Init.Data.UInt.Lemmas
UInt32.toUSize_mod : ∀ (a b : UInt32), (a % b).toUSize = a.toUSize % b.toUSize
-- Mathlib.Algebra.CharP.Two
CharTwo.add_mul_self : ∀ {R : Type u_1} [inst : CommSemiring R] [CharP R 2] (x y : R), (x + y) * (x + y) = x * x + y * y
-- Mathlib.Analysis.InnerProductSpace.LinearMap
inner_map_polarization' : ∀ {V : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V) (x y : V),
  inner ℂ (T x) y =
    (inner ℂ (T (x + y)) (x + y) - inner ℂ (T (x - y)) (x - y) -
          Complex.I * inner ℂ (T (x + Complex.I • y)) (x + Complex.I • y) +
        Complex.I * inner ℂ (T (x - Complex.I • y)) (x - Complex.I • y)) /
      4
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.coe_toOpens : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Clopens α), ↑s.toOpens = ↑s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of two strictly monotone functions is strictly monotone.  -/
StrictMono.mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
  [MulLeftStrictMono α] [MulRightStrictMono α], StrictMono f → StrictMono g → StrictMono fun x => f x * g x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (Std.ExtTreeMap.ofList l cmp)[k]? = none
-- Mathlib.Computability.Reduce
OneOneEquiv.le_congr_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, OneOneEquiv q r → (p ≤₁ q ↔ p ≤₁ r)
-- Lean.Data.Lsp.Internal
Lean.Lsp.OpenNamespace.allExcept.sizeOf_spec : ∀ («namespace» : Lean.Name) (exceptions : Array Lean.Name),
  sizeOf (Lean.Lsp.OpenNamespace.allExcept «namespace» exceptions) = 1 + sizeOf «namespace» + sizeOf exceptions
-- Mathlib.Topology.MetricSpace.Algebra
/-- Eta-expanded form of `TendstoLocallyUniformly.mul₀` -/
TendstoLocallyUniformly.fun_mul₀ : ∀ {X : Type u_3} {M : Type u_4} {ι : Type u_5} [inst : TopologicalSpace X] [inst_1 : PseudoMetricSpace M]
  [inst_2 : Zero M] [inst_3 : Mul M] [IsBoundedSMul M M] {F G : ι → X → M} {f g : X → M} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l →
      Continuous f → Continuous g → TendstoLocallyUniformly (fun i i_1 => F i i_1 * G i i_1) (fun i => f i * g i) l
-- Mathlib.Algebra.Ring.Prod
NonUnitalRingHom.coe_prodMap : ∀ {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] [inst_2 : NonUnitalNonAssocSemiring R'] [inst_3 : NonUnitalNonAssocSemiring S']
  (f : R →ₙ+* R') (g : S →ₙ+* S'), ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
-- Mathlib.SetTheory.Ordinal.Notation
ONote.opowAux2.eq_1 : ∀ (o₂ : ONote), o₂.opowAux2 (ONote.zero, 0) = if o₂ = 0 then 1 else 0
-- Mathlib.SetTheory.Cardinal.Ordinal
/-- **Alias** of `Ordinal.isPrincipal_opow_omega`. -/
Ordinal.principal_opow_omega : ∀ (o : Ordinal.{u_1}), Ordinal.IsPrincipal (fun x1 x2 => x1 ^ x2) (Ordinal.omega o)
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `NonAssocSemiring` across an `Equiv`  -/
Equiv.nonAssocSemiring : {α : Type u_1} → {β : Type u_2} → α ≃ β → [NonAssocSemiring β] → NonAssocSemiring α
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- The adjunction between the n-skeleton and n-truncation.  -/
SSet.skAdj : (n : ℕ) → SSet.Truncated.sk n ⊣ SSet.truncation n
-- Mathlib.Topology.Separation.Regular
/-- A topological space `X` is a *completely normal space* provided that for any two sets `s`, `t`
such that if both `closure s` is disjoint with `t`, and `s` is disjoint with `closure t`,
then there exist disjoint neighbourhoods of `s` and `t`.  -/
CompletelyNormalSpace : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.GroupTheory.GroupAction.Quotient
Subgroup.quotientCentralizerEmbedding_apply : ∀ {G : Type u_1} [inst : Group G] (g x : G), (Subgroup.quotientCentralizerEmbedding g) ↑x = ⟨⁅x, g⁆, ⋯⟩
-- Mathlib.Data.Finsupp.ToDFinsupp
sigmaFinsuppEquivDFinsupp_smul : ∀ {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} {R : Type u_6} [inst : Monoid R] [inst_1 : AddMonoid N]
  [inst_2 : DistribMulAction R N] (r : R) (f : (i : ι) × η i →₀ N),
  sigmaFinsuppEquivDFinsupp (r • f) = r • sigmaFinsuppEquivDFinsupp f
-- Mathlib.Order.SupIndep
Finset.supIndep_empty : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] (f : ι → α), ∅.SupIndep f
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The action by a subsemiring is the action by the underlying semiring.  -/
Subsemiring.instSMulWithZeroSubtypeMem_1 : {R' : Type u_1} →
  {α : Type u_2} →
    [inst : NonAssocSemiring R'] → [inst_1 : Zero α] → [SMulWithZero R' α] → (S : Subsemiring R') → SMulWithZero (↥S) α
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instLawfulSingletonProd : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α],
  LawfulSingleton (α × β) (Std.ExtHashMap α β)
-- Mathlib.Combinatorics.Graph.Delete
Graph.restrict_restrict : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β), (G.restrict F₁).restrict F₂ = G.restrict (F₁ ∩ F₂)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
/-- Additive convolution: `(f ⋆₊[L] g) x = ∑' ab : addFiber x, L (f ab.1) (g ab.2)`.  -/
DiscreteConvolution.addConvolution : {M : Type u_1} →
  {S : Type u_2} →
    {E : Type u_3} →
      {E' : Type u_4} →
        {F : Type u_6} →
          [AddMonoid M] →
            [inst : CommSemiring S] →
              [inst_1 : AddCommMonoid E] →
                [inst_2 : AddCommMonoid E'] →
                  [inst_3 : AddCommMonoid F] →
                    [inst_4 : Module S E] →
                      [inst_5 : Module S E'] →
                        [inst_6 : Module S F] → [TopologicalSpace F] → (E →ₗ[S] E' →ₗ[S] F) → (M → E) → (M → E') → M → F
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The shape of a multicoequalizer diagram. It involves two types `L` and `R`,
and two maps `L → R`.  -/
CategoryTheory.Limits.MultispanShape : Type (max (w + 1) (w' + 1))
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_iff_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t ↔ t.contains k = true
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_mul_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {β : Type u_5} [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] (s t : Finset α) (f : α → β), (s * t).sup f = t.sup fun y => s.sup fun x => f (x * y)
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.rayleighQuotient_add : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T S : E →L[𝕜] E) {x : E}, (T + S).rayleighQuotient x = T.rayleighQuotient x + S.rayleighQuotient x
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.op_f₁₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.op.f₁₃ = sq.f₃₄.op
-- Mathlib.Util.AtLocation
/-- Use the procedure `m` to rewrite hypothesis `fvarId`.

The `simpTheorems` of the simp-context carried with `m` will be modified to remove `fvarId`;
this ensures that if the procedure `m` involves rewriting by this `SimpTheoremsArray`, then, e.g.,
`h : x = y` is not transformed (by rewriting `h`) to `True`.

Assumes `proc` is not surrounded by backticks.  -/
Mathlib.Tactic.transformAtLocalDecl : (Lean.Expr → ReaderT Lean.Meta.Simp.Context Lean.MetaM Lean.Meta.Simp.Result) →
  String →
    Mathlib.Tactic.BehaviorIfUnchanged →
      Bool → Lean.FVarId → Lean.MVarId → ReaderT Lean.Meta.Simp.Context Lean.MetaM (Option Lean.MVarId)
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
hasSum_sum_range_mul_of_summable_norm : ∀ {R : Type u_1} [inst : NormedRing R] [CompleteSpace R] {f g : ℕ → R},
  (Summable fun x => ‖f x‖) →
    (Summable fun x => ‖g x‖) →
      HasSum (fun n => ∑ k ∈ Finset.range (n + 1), f k * g (n - k)) ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_of_add_le_right : ∀ {α : Type u} [inst : Add α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α] {a b c : α}, a + b ≤ c → b ≤ c
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.addZeroClass.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddZeroClass α],
  Finset.addZeroClass = Function.Injective.addZeroClass SetLike.coe ⋯ ⋯ ⋯
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.sectionCotangent_eq_iff : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ)
  (x : P.toExtension.CotangentSpace) (y : P.toExtension.Cotangent),
  P.sectionCotangent x = y ↔ ∀ (i : σ), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i
-- Mathlib.Data.List.Sort
/-- The list obtained from a monotone tuple is sorted.  -/
Monotone.sortedLE_ofFn : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin n → α}, Monotone f → (List.ofFn f).SortedLE
-- Mathlib.Computability.DFA
DFA.accepts_reindex : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) {σ' : Type u_2} (g : σ ≃ σ'), ((DFA.reindex g) M).accepts = M.accepts
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.IsLocallyFiniteMeasure.withDensity_ofReal : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α]
  [OpensMeasurableSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → ℝ},
  Continuous f → MeasureTheory.IsLocallyFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.injective : ∀ {α : Type u} {β : Type v} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  (self : Std.PRange.UpwardEnumerable.Map α β), Function.Injective self.toFun
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RioSliceData.mk : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      (Std.DTreeMap.Internal.Impl α fun x => β) → Std.Rio α → Std.DTreeMap.Internal.Const.RioSliceData α β
-- Init.Data.Float.Float32
instBEqFloat32 : BEq Float32