mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Defs
IsAddCommutative.mk : ∀ {M : Type u_2} [inst : Add M], (Std.Commutative fun x1 x2 => x1 + x2) → IsAddCommutative M
-- Init.Data.Option.Attach
_private.Init.Data.Option.Attach.0.Option.instDecidableEq.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (val : α) → motive (some val)),
  (match none with
    | none => h_1 ()
    | some val => h_2 val) =
    h_1 ()
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.const_algebraMap : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : CommSemiring K]
  [inst_2 : Semiring β] [inst_3 : Algebra K β] (k : K),
  MeasureTheory.SimpleFunc.const α ((algebraMap K β) k) = (algebraMap K (MeasureTheory.SimpleFunc α β)) k
-- Aesop.Util.EqualUpToIds
_private.Aesop.Util.EqualUpToIds.0.Aesop.EqualUpToIds.Unsafe.localContextsEqualUpToIdsCore.go : (decls₁ decls₂ : Array Lean.LocalDecl) →
  decls₁.size = decls₂.size →
    ℕ → Aesop.EqualUpToIds.GoalContext → Aesop.EqualUpToIdsM (Option Aesop.EqualUpToIds.GoalContext)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.Integrable.of_bound : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ] {f : α → E},
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (C : ℝ), (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) → MeasureTheory.Integrable f μ
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_neg_right : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ)
  (f g : (i : ι) → E i), ⟪f, -g⟫_[𝕜, w] = -⟪f, g⟫_[𝕜, w]
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.field.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.field = 1
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabInfo.name : Lean.Elab.DocElabInfo → Lean.Name
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.sum_Ioo_add_eq_sum_Ico : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a < b → ∑ x ∈ Finset.Ioo a b, f x + f a = ∑ x ∈ Finset.Ico a b, f x
-- Std.Time.Date.Unit.Week
Std.Time.Week.instInhabitedOffset : Inhabited Std.Time.Week.Offset
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsLocalization.instAlgebraAtPrimeLocalization : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) → (p : Ideal (Localization M)) → [inst_1 : p.IsPrime] → Algebra R (Localization.AtPrime p)
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Given tactic syntax `tac` that we want to paste into the editor, return it as a string.
This function respects the 100 character limit for long lines.  -/
Mathlib.Tactic.LibraryRewrite.tacticPasteString : Lean.TSyntax `tactic → Lean.Lsp.Range → Lean.CoreM String
-- Mathlib.Data.PNat.Factors
PNat.factorMultiset_lcm : ∀ (m n : ℕ+), (m.lcm n).factorMultiset = m.factorMultiset ⊔ n.factorMultiset
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_neg : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F), (-p).radius = p.radius
-- Std.Data.ExtHashSet.Lemmas
_private.Std.Data.ExtHashSet.Lemmas.0.Std.ExtHashSet.ext : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m m' : Std.ExtHashSet α}, m.inner = m'.inner → m = m'
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.centroid_eq_smul_sum_vsub_vadd : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.centroid = (↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) +ᵥ s.points i
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.swap.injEq : ∀ (c c_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.swap c = Lean.Meta.Grind.AC.EqCnstrProof.swap c_1) = (c = c_1)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.IsOrtho.starProjection_comp_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} [inst_3 : U.HasOrthogonalProjection] [inst_4 : V.HasOrthogonalProjection],
  U ⟂ V → U.starProjection ∘SL V.starProjection = 0
-- Std.Time.Zoned.TimeZone
/-- Gets the number of seconds in a timezone offset.
 -/
Std.Time.TimeZone.toSeconds : Std.Time.TimeZone → Std.Time.Second.Offset
-- Mathlib.Algebra.Homology.Opposite
Homotopy.unop_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {ι : Type u_2} {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Preadditive V] {F G : HomologicalComplex Vᵒᵖ c} {φ₁ φ₂ : F ⟶ G} (h : Homotopy φ₁ φ₂)
  (i j : ι), h.unop.hom i j = (h.hom j i).unop
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getValue?.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : List ((_ : α) × β) → Sort u_3) (h_1 : Unit → motive [])
  (h_2 : (k : α) → (v : β) → (l : List ((_ : α) × β)) → motive (⟨k, v⟩ :: l)),
  (match [] with
    | [] => h_1 ()
    | ⟨k, v⟩ :: l => h_2 k v l) =
    h_1 ()
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuousOn.mono : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s t : Set α},
  UniformContinuousOn f s → t ⊆ s → UniformContinuousOn f t
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.map_id : ∀ {R : CommRingCat} {M : ModuleCat ↑R},
  AlgebraicGeometry.tilde.map (CategoryTheory.CategoryStruct.id M) =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.tilde M)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
ValuativeRel.isDiscrete_trivialRel : ∀ {R Γ : Type} [inst : Ring R] [inst_1 : DecidableEq R] [inst_2 : IsDomain R]
  [inst_3 : LinearOrderedCommGroupWithZero Γ] [inst_4 : ValuativeRel R] [Valuation.Compatible 1],
  ValuativeRel.IsDiscrete R
-- Mathlib.GroupTheory.ArchimedeanDensely
instDenselyOrderedMultiplicative : ∀ {X : Type u_2} [inst : LT X] [DenselyOrdered X], DenselyOrdered (Multiplicative X)
-- Mathlib.RepresentationTheory.Basic
Representation.quotient_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Ring k] [inst_1 : Monoid G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (W : Submodule k V)
  (le_comap : ∀ (g : G), W ≤ Submodule.comap (ρ g) W) (g : G), (ρ.quotient W le_comap) g = W.mapQ W (ρ g) ⋯
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supportedEquivFinsupp_symm_apply_coe_apply : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set α) (a : ↑s →₀ M) (a_1 : α),
  ↑((Finsupp.supportedEquivFinsupp s).symm a) a_1 = if h : a_1 ∈ s then a ⟨a_1, h⟩ else 0
-- Mathlib.Order.Filter.Pointwise
Filter.pureMulHom.eq_1 : ∀ {α : Type u_2} [inst : Mul α], Filter.pureMulHom = { toFun := pure, map_mul' := ⋯ }
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Copy of a `LinearMap` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
LinearMap.copy : {R : Type u_1} →
  {S : Type u_5} →
    {M : Type u_8} →
      {M₃ : Type u_11} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M] →
                  [inst_5 : Module S M₃] → {σ : R →+* S} → (f : M →ₛₗ[σ] M₃) → (f' : M → M₃) → f' = ⇑f → M →ₛₗ[σ] M₃
-- Init.Data.Option.Lemmas
Option.forall : ∀ {α : Type u_1} {p : Option α → Prop}, (∀ (x : Option α), p x) ↔ p none ∧ ∀ (x : α), p (some x)
-- Init.Data.Vector.Lemmas
Vector.toList_reverse : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.reverse.toList = xs.toList.reverse
-- Mathlib.Algebra.Order.CauSeq.Basic
isCauSeq_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f : ℕ → β}, IsCauSeq abv (-f) ↔ IsCauSeq abv f
-- Init.Data.Rat.Lemmas
Rat.zero_divInt : ∀ (n : ℤ), Rat.divInt 0 n = 0
-- Mathlib.Data.List.TakeDrop
/-- `take_concat_get` in simp normal form  -/
List.take_concat_get' : ∀ {α : Type u} (l : List α) (i : ℕ) (h : i < l.length), List.take i l ++ [l[i]] = List.take (i + 1) l
-- Mathlib.Computability.EpsilonNFA
εNFA.eval_singleton : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) (a : α), M.eval [a] = M.stepSet (M.εClosure M.start) a
-- Mathlib.Data.Num.ZNum
ZNum.cast_one : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Add α] [inst_3 : Neg α], ↑1 = 1
-- Mathlib.Computability.TuringMachine.Tape
Turing.Dir.right.sizeOf_spec : sizeOf Turing.Dir.right = 1
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ioo_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a b : α) {c : α},
  c < 0 → (fun x => x * c) ⁻¹' Set.Ioo a b = Set.Ioo (b / c) (a / c)
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.monotone'_triangEnvelopeIter : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) {n m : ℕ},
  autoParam (n ≤ m) CategoryTheory.ObjectProperty.monotone'_triangEnvelopeIter._auto_1 →
    P.triangEnvelopeIter n ≤ P.triangEnvelopeIter m
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.of_rat : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  (∀ (t : ℝ), MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) (ν.bind ⇑κ)) →
    (∀ (q : ℚ), ∀ᵐ (ω' : Ω') ∂ν, ProbabilityTheory.mgf X (κ ω') ↑q ≤ Real.exp (↑c * ↑q ^ 2 / 2)) →
      ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- `usedCommRing` is `true` if the `CommRing` has been used to normalize expressions.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.usedCommRing : Lean.Meta.Grind.Arith.Cutsat.State → Bool
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t'_snd_snd_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀) {Z_1 : AlgebraicGeometry.Scheme} (h : 𝒰.X i ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)
          (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.snd
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
            (𝒰.f i))
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f j))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) h))
-- Batteries.Data.AssocList
Batteries.AssocList.mapVal.eq_def : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : α → β → δ) (x : Batteries.AssocList α β),
  Batteries.AssocList.mapVal f x =
    match x with
    | Batteries.AssocList.nil => Batteries.AssocList.nil
    | Batteries.AssocList.cons k v t => Batteries.AssocList.cons k (f k v) (Batteries.AssocList.mapVal f t)
-- Mathlib.Algebra.Ring.Int.Parity
Int.Odd.of_mul_right : ∀ {m n : ℤ}, Odd (m * n) → Odd n
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Set.smul_mem_center : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [IsScalarTower R A A] [SMulCommClass R A A] (r : R) {a : A}, a ∈ Set.center A → r • a ∈ Set.center A
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The forgetful functor from additive group objects to additive monoid objects.  -/
CategoryTheory.AddGrp.forget₂Mon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      CategoryTheory.Functor (CategoryTheory.AddGrp C) (CategoryTheory.AddMon C)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_union_Ioc_eq_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, b < a → c < b → Set.Ico b a ∪ Set.Ioc c b = Set.Ioo c a
-- Mathlib.Algebra.Algebra.Defs
/-- `mul_right_comm` for `Algebra`s when one element is from the base ring.  -/
Algebra.right_comm : ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) (r : R)
  (y : A), x * (algebraMap R A) r * y = x * y * (algebraMap R A) r
-- Mathlib.Data.Matrix.DMatrix
DMatrix.instAddCommGroup : {m : Type u_1} →
  {n : Type u_2} → {α : m → n → Type v} → [(i : m) → (j : n) → AddCommGroup (α i j)] → AddCommGroup (DMatrix m n α)
-- Lean.Meta.Sym.Arith.Types
/-- `AddRightCancel` instance for `type` if available.  -/
Lean.Meta.Sym.Arith.CommSemiring.addRightCancelInst? : Lean.Meta.Sym.Arith.CommSemiring → Option (Option Lean.Expr)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.disjoint_map_primeCompl_iff_comap_le : ∀ {R : Type u} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Semiring S] {f : R →+* S} {p : Ideal R} {I : Ideal S}
  [inst_2 : p.IsPrime], Disjoint ↑I ↑(Submonoid.map f p.primeCompl) ↔ Ideal.comap f I ≤ p
-- Mathlib.Condensed.TopCatAdjunction
_private.Mathlib.Condensed.TopCatAdjunction.0.CondensedSet.coinducingCoprod.match_1.splitter : (X : CondensedSet) →
  (motive : (i : (S : CompHaus) × X.obj.obj (Opposite.op S)) × ↑i.fst.toTop → Sort u_2) →
    (x : (i : (S : CompHaus) × X.obj.obj (Opposite.op S)) × ↑i.fst.toTop) →
      ((fst : CompHaus) → (i : X.obj.obj (Opposite.op fst)) → (s : ↑⟨fst, i⟩.fst.toTop) → motive ⟨⟨fst, i⟩, s⟩) →
        motive x
-- Mathlib.Tactic.DepRewrite
/-- The list of *value-less* binders (`cdecl`s and nondependent `ldecl`s)
that we have introduced.
Together with each binder, we store its type abstracted over `x` and `h`,
and with all occurrences of previous entries in `Δ`
casted along the abstracting equation.

E.g., if the local context is `a : T, b : U`,
we store `(a, Ma)` where `Ma := fun (x' : α) (h' : x = x') => T[x'/x, h'/h]`
and `(b, fun (x' : α) (h' : x = x') => U[x'/x, h'/h, (Eq.rec (motive := Ma) a h)/a])`
See the docstring on `visitAndCast`.  -/
Mathlib.Tactic.DepRewrite.Context.Δ : Mathlib.Tactic.DepRewrite.Context → Array (Lean.FVarId × Lean.Expr)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.minpoly_root : ∀ {K : Type u_5} [inst : Field K] {f : Polynomial K},
  f ≠ 0 → minpoly K (AdjoinRoot.root f) = f * Polynomial.C f.leadingCoeff⁻¹
-- Mathlib.Order.Interval.Set.Fin
Fin.image_val_Iic : ∀ {n : ℕ} (i : Fin n), Fin.val '' Set.Iic i = Set.Iic ↑i
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
BinaryTree.treesOfNumNodesEq.eq_2 : ∀ (n : ℕ),
  BinaryTree.treesOfNumNodesEq n.succ =
    (Finset.HasAntidiagonal.antidiagonal n).attach.biUnion fun ijh =>
      BinaryTree.pairwiseNode (BinaryTree.treesOfNumNodesEq (↑ijh).1) (BinaryTree.treesOfNumNodesEq (↑ijh).2)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.comp_mul_left_iff : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {f : ℝ → E} {c : ℝ},
  c ≠ 0 →
    autoParam (‖f (min a b)‖ₑ ≠ ⊤) IntervalIntegrable.comp_mul_left_iff._auto_1 →
      autoParam (‖f (c * min (a / c) (b / c))‖ₑ ≠ ⊤) IntervalIntegrable.comp_mul_left_iff._auto_3 →
        (IntervalIntegrable (fun x => f (c * x)) MeasureTheory.volume (a / c) (b / c) ↔
          IntervalIntegrable f MeasureTheory.volume a b)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.find?_toArray_eq_none_iff_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, Array.find? (fun x => cmp x.1 k == Ordering.eq) t.toArray = none ↔ k ∉ t
-- Mathlib.Computability.Language
Language.join_mem_kstar : ∀ {α : Type u_1} {l : Language α} {L : List (List α)}, (∀ y ∈ L, y ∈ l) → L.flatten ∈ KStar.kstar l
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} {fallback : γ},
  Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.filterMap f t) k fallback =
    ((Std.ExtDTreeMap.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Mathlib.NumberTheory.Real.Irrational
Irrational.intCast_add : ∀ {x : ℝ}, Irrational x → ∀ (m : ℤ), Irrational (↑m + x)
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_casesOn₁ : ∀ {α : Type u_1} [inst : Primcodable α] {f : ℕ → α} (a : α), Primrec f → Primrec fun n => Nat.casesOn n a f
-- Mathlib.Topology.ContinuousOn
ContinuousOn.continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousOn f s → x ∈ s → ContinuousWithinAt f s x
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Complex.measurable_sin : Measurable Complex.sin
-- Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
/-- If `f` is a nonconstant polynomial with coefficients in `R`, and `P` is a prime ideal in `R`,
then if every coefficient in `R` except the leading coefficient is in `P`, and
the trailing coefficient is not in `P^2` and no nonunits in `R` divide `f`, then `f` is
irreducible.  -/
Polynomial.irreducible_of_eisenstein_criterion : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {f : Polynomial R} {P : Ideal R},
  P.IsPrime →
    f.leadingCoeff ∉ P →
      (∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P) → 0 < f.degree → f.coeff 0 ∉ P ^ 2 → f.IsPrimitive → Irreducible f
-- Mathlib.Data.Fin.Tuple.Basic
Fin.tail_cons : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ), Fin.tail (Fin.cons x p) = p
-- Mathlib.Data.PFun
PFun.dom_coe : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), (↑f).Dom = Set.univ
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.PreservesLeast?.map_least? : ∀ {α : Type u_1} {β : Type u_2} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : Std.PRange.UpwardEnumerable β}
  {inst_2 : Std.PRange.Least? α} {inst_3 : Std.PRange.Least? β} {f : Std.PRange.UpwardEnumerable.Map α β}
  [self : f.PreservesLeast?], Option.map f.toFun Std.PRange.least? = Std.PRange.least?
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- The proposition that a bilinear form is symmetric  -/
LinearMap.BilinForm.IsSymm : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.BilinForm R M → Prop
-- Mathlib.Data.Num.Lemmas
PosNum.natSize_to_nat : ∀ (n : PosNum), n.natSize = (↑n).size
-- Init.Data.String.Lemmas.Splits
/-- You might want to invoke `Pos.Splits.exists_eq_singleton_append` to be able to apply this.  -/
String.Pos.Splits.next : ∀ {t₁ : String} {c : Char} {t₂ s : String} {p : s.Pos} (h : p.Splits t₁ (String.singleton c ++ t₂)),
  (p.next ⋯).Splits (t₁ ++ String.singleton c) t₂
-- Mathlib.Algebra.Ring.Parity
Nat.odd_add_one : ∀ {n : ℕ}, Odd (n + 1) ↔ ¬Odd n
-- Init.ShareCommon
ShareCommon.StateFactoryBuilder.mkMap : (self : ShareCommon.StateFactoryBuilder) → {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → self.Map α β
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : Inhabited α] {a : α}, ∅.get! a = default
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- The natural map from a nonsingular projective point on a Weierstrass curve `W` to its
corresponding nonsingular point in affine coordinates.

If `hP` is the nonsingular condition underlying a nonsingular projective point `P` on `W`, then
`toAffineLift ⟨hP⟩` is definitionally equivalent to `toAffine W P`.  -/
WeierstrassCurve.Projective.Point.toAffineLift : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Projective F} → W.Point → W.toAffine.Point
-- Lean.SubExpr
/-- The coordinate deepest in the Pos.  -/
Lean.SubExpr.Pos.head : Lean.SubExpr.Pos → ℕ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocyclesIso₀_hom_comp_f_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : (groupCohomology.shortComplexH0 A).X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesIso₀ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH0 A).f h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 0) (groupCohomology.cochainsIso₀ A).hom) h
-- Lean.Meta.PPBinder
/-- Pretty-prints a local declaration and its type as a binder,
using the appropriate brackets given its `BinderInfo`. Example output: `{α : Type}`.

Returns `none` for let decls.
 -/
Lean.LocalDecl.ppAsBinder : Lean.LocalDecl → Option Lean.MessageData
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.analyticOnNhd_cgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AnalyticOnNhd ℝ (ProbabilityTheory.cgf X μ) (interior (ProbabilityTheory.integrableExpSet X μ))
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.id.eq_1 : ∀ (M : Type u_10) [inst : Mul M], MulHom.id M = { toFun := fun x => x, map_mul' := ⋯ }
-- Mathlib.Algebra.DirectSum.Ring
/-- Each grade `A i` derives an `A 0`-module structure from `GSemiring A`. Note that this results
in an overall `Module (A 0) (⨁ i, A i)` structure via `DirectSum.module`.
 -/
DirectSum.instModuleOfNat : {ι : Type u_1} →
  [inst : DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst_1 : (i : ι) → AddCommMonoid (A i)] →
        [inst_2 : AddMonoid ι] → [inst_3 : DirectSum.GSemiring A] → {i : ι} → Module (A 0) (A i)
-- Mathlib.CategoryTheory.Sites.Finite
/-- The finite pretopology on a category consists of finite presieves, i.e. a presieve with finitely
many maps after uncurrying.  -/
CategoryTheory.Pretopology.finite : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.Pretopology C
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.includeRight_apply : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (b : B), Algebra.TensorProduct.includeRight b = 1 ⊗ₜ[R] b
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.comp_left_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β}
  {μc : MeasureTheory.Measure γ} {g : α → β} {e : β ≃ᵐ γ},
  MeasureTheory.MeasurePreserving (⇑e) μb μc →
    (MeasureTheory.MeasurePreserving (⇑e ∘ g) μa μc ↔ MeasureTheory.MeasurePreserving g μa μb)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_univ_add : ∀ {M : Type u_2} [inst : CommMonoid M] {a b : ℕ} (f : Fin (a + b) → M),
  ∏ i, f i = (∏ i, f (Fin.castAdd b i)) * ∏ i, f (Fin.natAdd a i)