mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Frontend.Attribute
Aesop.Frontend.AttrConfig.mk : Array Aesop.Frontend.RuleExpr → Aesop.Frontend.AttrConfig
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_right_strictAnti₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} [PosMulStrictMono M₀],
  0 < a → a < 1 → StrictAnti fun x => a ^ x
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_pure_left : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {l : Filter β}, Filter.Tendsto f (pure a) l ↔ ∀ s ∈ l, f a ∈ s
-- Mathlib.Combinatorics.SimpleGraph.Partition
/-- A `Partition` of a simple graph `G` is a structure constituted by:
* `parts`: a set of subsets of the vertices `V` of `G`.
* `isPartition`: a proof that `parts` is a proper partition of `V`.
* `independent`: a proof that each element of `parts` doesn't have a pair of adjacent vertices.
 -/
SimpleGraph.Partition : {V : Type u} → SimpleGraph V → Type u
-- Mathlib.AlgebraicTopology.SingularSet
/-- The *geometric realization functor* is
the left Kan extension of `SimplexCategory.toTop` along the Yoneda embedding.

It is left adjoint to `TopCat.toSSet`, as witnessed by `sSetTopAdj`.  -/
SSet.toTop : CategoryTheory.Functor SSet TopCat
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.fvar.injEq : ∀ (a : Lean.FVarId) (a_1 : ℕ) (a_2 : Lean.FVarId) (a_3 : ℕ),
  (Lean.Meta.DiscrTree.Key.fvar a a_1 = Lean.Meta.DiscrTree.Key.fvar a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofSubmodule'_symm_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₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
  (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : ↥U), ↑((f.ofSubmodule' U).symm x) = f.symm ↑x
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsAddCyclic.exponent_eq_card : ∀ {α : Type u_1} [inst : AddGroup α] [IsAddCyclic α], AddMonoid.exponent α = Nat.card α
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isSome_getElem?_toArray_roo_eq : ∀ {m n : ℤ} {i : ℕ}, ((m<...n).toArray[i]?.isSome = true) = (i < (n - (m + 1)).toNat)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.activateNextGuard : Lean.Meta.Grind.EMatchTheorem →
  List Lean.Meta.Grind.TheoremGuard → ℕ → Lean.Meta.Grind.GoalM Lean.Meta.Grind.ActivateNextGuardResult
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.fibRec.eq_1 : ∀ {α : Type u_1} [inst : CommSemiring α], Real.fibRec = { order := 2, coeffs := ![1, 1] }
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
MvPowerSeries.WithPiTopology.tendsto_trunc_atTop : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : DecidableEq σ] [inst_2 : CommSemiring R]
  [Nonempty σ] (f : MvPowerSeries σ R), Filter.Tendsto (fun d => ↑((MvPowerSeries.trunc R d) f)) Filter.atTop (nhds f)
-- Mathlib.Algebra.Group.Pi.Lemmas
ZeroHom.coe_single : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → Zero (f i)] (i : I),
  ⇑(ZeroHom.single f i) = Pi.single i
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.ExprPair.mk : {w : ℕ} → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVPred.ExprPair
-- Mathlib.Logic.Small.Defs
small_congr : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), Small.{w, u_1} α ↔ Small.{w, u_2} β
-- Mathlib.Order.Heyting.Basic
BiheytingAlgebra.mk : {α : Type u_4} →
  [toHeytingAlgebra : HeytingAlgebra α] →
    [toSDiff : SDiff α] →
      (∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c) → [toHNot : HNot α] → (∀ (a : α), ⊤ \ a = ￢a) → BiheytingAlgebra α
-- Std.Time.Date.Basic
/-- Convert `Nanosecond.Offset` into `Day.Offset`.
 -/
Std.Time.Nanosecond.Offset.toDays : Std.Time.Nanosecond.Offset → Std.Time.Day.Offset
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mem_map_iff_mem : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Injective ⇑f → ∀ {S : AddSubmonoid M} {x : M}, f x ∈ AddSubmonoid.map f S ↔ x ∈ S
-- Mathlib.Data.Nat.Factorization.Basic
/-- Modified version of `factorization_prod` that accounts for inputs.  -/
Nat.factorization_prod_apply : ∀ {α : Type u_1} {p : ℕ} {S : Finset α} {g : α → ℕ},
  (∀ x ∈ S, g x ≠ 0) → (S.prod g).factorization p = ∑ x ∈ S, (g x).factorization p
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
summable_jacobiTheta₂'_term_iff : ∀ (z τ : ℂ), (Summable fun x => jacobiTheta₂'_term x z τ) ↔ 0 < τ.im
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.eq_or_edist_eq_top_of_fixedPoints : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α},
  ContractingWith K f → ∀ {x y : α}, Function.IsFixedPt f x → Function.IsFixedPt f y → x = y ∨ edist x y = ⊤
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- If a function is injective on a finset, sums over the original
finset or its image coincide.
See also `sum_image_of_pairwise_eq_zero` for a version with weaker assumptions.  -/
Finset.sum_image : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι]
  {s : Finset κ} {g : κ → ι}, Set.InjOn g ↑s → ∑ x ∈ Finset.image g s, f x = ∑ x ∈ s, f (g x)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_eq_head!_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.minKey! = t.keys.head!
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- Normalization as an equivalence of categories.  -/
CategoryTheory.FreeBicategory.normalizeEquiv : {B : Type u} →
  [inst : Quiver B] → (a b : B) → CategoryTheory.FreeBicategory.Hom a b ≌ CategoryTheory.Discrete (Quiver.Path a b)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_le_sub : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : Preorder α] [AddLeftMono α] {a b c d : α},
  a ≤ b → c ≤ d → a - d ≤ b - c
-- Mathlib.Tactic.FunProp.Types
/-- Log progress and failures messages that should be displayed to the user at the end.  -/
Mathlib.Meta.FunProp.State.msgLog : Mathlib.Meta.FunProp.State → List String
-- Mathlib.Topology.Instances.Matrix
Matrix.topologicalRing : ∀ {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : Fintype n] [inst_2 : NonUnitalNonAssocRing R]
  [IsTopologicalRing R], IsTopologicalRing (Matrix n n R)
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iio_strictMono : ∀ (α : Type u_1) [inst : Preorder α], StrictMono LowerSet.Iio
-- Mathlib.Topology.MetricSpace.Defs
instDistMultiplicative : {X : Type u_1} → [Dist X] → Dist (Multiplicative X)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableUniformlyOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] (f : ι → β → α) (s : Set β)
  [inst_1 : UniformSpace α], MultipliableUniformlyOn f s = Multipliable (⇑(UniformOnFun.ofFun {s}) ∘ f)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_hom_app_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} {mor₁ : obj₁ ⟶ obj₂}
  {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)}
  {obj₁' obj₂' obj₃' : CategoryTheory.Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'}
  {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (iso₁ : obj₁ ≅ obj₁') (iso₂ : obj₂ ≅ obj₂')
  (iso₃ : obj₃ ≅ obj₃')
  (comm₁ : CategoryTheory.CategoryStruct.comp mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom mor₁')
  (comm₂ : CategoryTheory.CategoryStruct.comp mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom mor₂')
  (comm₃ :
    CategoryTheory.CategoryStruct.comp mor₃
        (CategoryTheory.Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) =
      CategoryTheory.CategoryStruct.comp iso₃.hom mor₃')
  (j : J),
  ((CategoryTheory.Pretriangulated.Triangle.functorIsoMk' iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom.app j).hom₃ =
    iso₃.hom.app j
-- Lean.Environment
/-- Content of a .olean file.
We use `compact.cpp` to generate the image of this object in disk.  -/
Lean.ModuleData : Type
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], MeasureTheory.volume.IsAddHaarMeasure
-- Init.Data.SInt.Basic
instReprAtomInt32 : ReprAtom Int32
-- Mathlib.CategoryTheory.ObjectProperty.Ind
/-- `ind` is idempotent if `P` implies finitely presentable.  -/
CategoryTheory.ObjectProperty.ind_ind : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  P ≤ CategoryTheory.ObjectProperty.isFinitelyPresentable C →
    ∀ [CategoryTheory.LocallySmall.{w, v, u} C], P.ind.ind = P.ind
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.apply_symm_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Equiv M N)
  (a : N), f (f.symm a) = a
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.support_top : ∀ {X : AlgebraicGeometry.Scheme}, ⊤.support = ⊥
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_veblen_eq_veblen_iff : ∀ {o₁ o₂ a : Ordinal.{u}},
  o₂ ≤ o₁ → (Ordinal.veblen o₁ (Ordinal.veblen o₂ a) = Ordinal.veblen o₂ a ↔ Ordinal.veblen o₁ a = a)
-- Mathlib.AlgebraicGeometry.Sites.Small
/-- **Alias** of `AlgebraicGeometry.Scheme.smallGrothendieckTopology`.

---

If `P` and `Q` are morphism properties with `P ≤ Q`, this is the Grothendieck topology
induced via the forgetful functor `Q.Over ⊤ S ⥤ Over S` by the topology defined by `P`.  -/
AlgebraicGeometry.Scheme.smallGrothendieckTopologyOfLE : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme →
  {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
    (S : AlgebraicGeometry.Scheme) → CategoryTheory.GrothendieckTopology (Q.Over ⊤ S)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDerivWithin_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {x v : E},
  lineDerivWithin 𝕜 f Set.univ x v = lineDeriv 𝕜 f x v
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.cgf.eq_1 : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) (t : ℝ),
  ProbabilityTheory.cgf X μ t = Real.log (ProbabilityTheory.mgf X μ t)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Cache.mk.injEq : ∀ (backwardRuleName : Lean.PHashMap Lean.Name Lean.Meta.Sym.BackwardRule)
  (backwardRuleSyntax : Lean.PHashMap (ℕ × ℕ) Lean.Meta.Sym.BackwardRule)
  (simpState : Std.HashMap Lean.Elab.Tactic.Grind.SimpCacheKey Lean.Meta.Sym.Simp.State)
  (dsimpState : Std.HashMap Lean.Elab.Tactic.Grind.DSimpCacheKey Lean.Meta.Sym.DSimp.State)
  (backwardRuleName_1 : Lean.PHashMap Lean.Name Lean.Meta.Sym.BackwardRule)
  (backwardRuleSyntax_1 : Lean.PHashMap (ℕ × ℕ) Lean.Meta.Sym.BackwardRule)
  (simpState_1 : Std.HashMap Lean.Elab.Tactic.Grind.SimpCacheKey Lean.Meta.Sym.Simp.State)
  (dsimpState_1 : Std.HashMap Lean.Elab.Tactic.Grind.DSimpCacheKey Lean.Meta.Sym.DSimp.State),
  ({ backwardRuleName := backwardRuleName, backwardRuleSyntax := backwardRuleSyntax, simpState := simpState,
        dsimpState := dsimpState } =
      { backwardRuleName := backwardRuleName_1, backwardRuleSyntax := backwardRuleSyntax_1, simpState := simpState_1,
        dsimpState := dsimpState_1 }) =
    (backwardRuleName = backwardRuleName_1 ∧
      backwardRuleSyntax = backwardRuleSyntax_1 ∧ simpState = simpState_1 ∧ dsimpState = dsimpState_1)
-- Init.Data.String.Iterator
/-- The remaining characters in an iterator, as a string.
 -/
String.Legacy.Iterator.remainingToString : String.Legacy.Iterator → String
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.HasLeftDual.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {Y : C} → (leftDual : C) → [exact : CategoryTheory.ExactPairing leftDual Y] → CategoryTheory.HasLeftDual Y
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.unfold : Lean.Name → Lean.Name → Mathlib.Tactic.UnfoldBoundary.UnfoldEntry
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_inl : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (s : AddSubmonoid M),
  AddSubmonoid.map (AddMonoidHom.inl M N) s = s.prod ⊥
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.ofFinset_apply_of_notMem : ∀ {α : Type u_1} {f : α → ENNReal} {s : Finset α} (h : ∑ a ∈ s, f a = 1) (h' : ∀ a ∉ s, f a = 0) {a : α},
  a ∉ s → (PMF.ofFinset f s h h') a = 0
-- Mathlib.Geometry.Euclidean.Altitude
/-- An altitude is finite-dimensional.  -/
Affine.Simplex.finiteDimensional_direction_altitude : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  FiniteDimensional ℝ ↥(s.altitude i).direction
-- Mathlib.Data.Analysis.Topology
Ctop.mk : {α : Type u_1} →
  {σ : Type u_2} →
    (f : σ → Set α) →
      (top : α → σ) →
        (∀ (x : α), x ∈ f (top x)) →
          (inter : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ) →
            (∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (inter a b x h)) →
              (∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (inter a b x h) ⊆ f a ∩ f b) → Ctop α σ
-- Lean.Parser.Basic
Lean.Parser.RecoveryContext.mk.inj : ∀ {initialPos : String.Pos.Raw} {initialSize : ℕ} {initialPos_1 : String.Pos.Raw} {initialSize_1 : ℕ},
  { initialPos := initialPos, initialSize := initialSize } =
      { initialPos := initialPos_1, initialSize := initialSize_1 } →
    initialPos = initialPos_1 ∧ initialSize = initialSize_1
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : R)
  (p : Polynomial R), (Polynomial.aeval ((algebraMap R A) x)) p = (algebraMap R A) (Polynomial.eval x p)
-- Mathlib.NumberTheory.Cyclotomic.Gal
IsCyclotomicExtension.fromZetaAut_spec : ∀ {n : ℕ} [inst : NeZero n] {K : Type u_1} [inst_1 : Field K] {L : Type u_2} {μ : L} [inst_2 : CommRing L]
  [inst_3 : IsDomain L] (hμ : IsPrimitiveRoot μ n) [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L]
  (h : Irreducible (Polynomial.cyclotomic n K)),
  (IsCyclotomicExtension.fromZetaAut hμ h) (IsCyclotomicExtension.zeta n K L) = μ
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IsIndObject.nonempty_presentation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)},
  CategoryTheory.Limits.IsIndObject A → Nonempty (CategoryTheory.Limits.IndObjectPresentation A)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictMono.const_mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α}
  [MulLeftStrictMono α], StrictMono f → ∀ (c : α), StrictMono fun x => c * f x
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.of_zero : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S}, Algebra.Extension.Cotangent.of 0 = 0
-- Mathlib.Algebra.Lie.Basic
LieEquiv.instInhabited : {R : Type u} →
  {L₁ : Type v} → [inst : CommRing R] → [inst_1 : LieRing L₁] → [inst_2 : LieAlgebra R L₁] → Inhabited (L₁ ≃ₗ⁅R⁆ L₁)
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
/-- The naturality condition.  -/
CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G}
  (self : CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ) {a b : B} (f : a ⟶ b),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b))
      (θ.naturality f).hom =
    CategoryTheory.CategoryStruct.comp (η.naturality f).hom
      (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map f))
-- Init.GrindInstances.Ring.UInt
/-- Variant of `UInt32.ofNat_mod_size` replacing `2 ^ 32` with `4294967296`. -/
UInt32.ofNat_mod_size' : ∀ {x : ℕ}, UInt32.ofNat (x % 4294967296) = UInt32.ofNat x
-- Mathlib.Algebra.Lie.SerreConstruction
Matrix.instLieRingToLieAlgebra : (R : Type u_1) →
  {B : Type u_2} →
    [inst : CommRing R] → (CM : Matrix B B ℤ) → [inst_1 : DecidableEq B] → LieRing (Matrix.ToLieAlgebra R CM)
-- Mathlib.Data.Num.Lemmas
/-- This tactic tries to prove (in)equalities about `Num`s by transferring them to the `Nat` world and
then trying to call `simp`.
```lean
example (n : Num) (m : Num) : n ≤ n + m := by transfer
```
 -/
Num.transfer : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.symm_toAddEquiv : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ↑e.symm = (↑e).symm
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulToForwardSearcherModel.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {σ : String.Slice → Type}
  [inst_1 : String.Slice.Pattern.ToForwardSearcher pat σ]
  [inst_2 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_3 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id],
  (∀ (s : String.Slice),
      String.Slice.Pattern.Model.IsValidSearchFrom pat s.startPos
        (String.Slice.Pattern.ToForwardSearcher.toSearcher pat s).toList) →
    String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.superpose.injEq : ∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (c₁ : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (k₂ : ℤ)
  (m₂ : Lean.Grind.CommRing.Mon) (c₂ : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (k₁_1 : ℤ)
  (m₁_1 : Lean.Grind.CommRing.Mon) (c₁_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (k₂_1 : ℤ)
  (m₂_1 : Lean.Grind.CommRing.Mon) (c₂_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.superpose k₁ m₁ c₁ k₂ m₂ c₂ =
      Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.superpose k₁_1 m₁_1 c₁_1 k₂_1 m₂_1 c₂_1) =
    (k₁ = k₁_1 ∧ m₁ = m₁_1 ∧ c₁ = c₁_1 ∧ k₂ = k₂_1 ∧ m₂ = m₂_1 ∧ c₂ = c₂_1)
-- Mathlib.Analysis.Normed.Group.Bounded
Filter.hasBasis_cobounded_norm : ∀ {E : Type u_2} [inst : SeminormedAddGroup E],
  (Bornology.cobounded E).HasBasis (fun x => True) fun x => {x_1 | x ≤ ‖x_1‖}
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.map.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f f_1 : M₁ →ₗ[R] M₂ →ₗ[R] M} (e_f : f = f_1) {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8}
  [inst_7 : AddCommMonoid N₁] [inst_8 : AddCommMonoid N₂] [inst_9 : AddCommMonoid N] [inst_10 : Module R N₁]
  [inst_11 : Module R N₂] [inst_12 : Module R N] {g g_1 : N₁ →ₗ[R] N₂ →ₗ[R] N} (e_g : g = g_1) (hf : IsTensorProduct f)
  (hg : IsTensorProduct g) (i₁ i₁_1 : M₁ →ₗ[R] N₁),
  i₁ = i₁_1 → ∀ (i₂ i₂_1 : M₂ →ₗ[R] N₂), i₂ = i₂_1 → hf.map hg i₁ i₂ = ⋯.map ⋯ i₁_1 i₂_1
-- Mathlib.Data.Num.Bitwise
/-- Bitwise `not` for `NzsNum`.  -/
NzsNum.«term~_» : Lean.ParserDescr
-- Mathlib.Algebra.Free
/-- The unique additive magma homomorphism `FreeAddMagma α → FreeAddMagma β` that
sends each `of x` to `of (f x)`.  -/
FreeAddMagma.map : {α : Type u} → {β : Type v} → (α → β) → FreeAddMagma α →ₙ+ FreeAddMagma β
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Monoid β]
  [inst_3 : ContinuousMul β] (f : C(α, β)) (n : ℕ), ⇑(f ^ n) = ⇑f ^ n
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows.idx.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C}
  {f f_1 : (i : ι) → X i ⟶ S} (e_f : f = f_1) {Y : C} {g g_1 : Y ⟶ S} (e_g : g = g_1)
  (hf : CategoryTheory.Presieve.ofArrows X f g), hf.idx = ⋯.idx
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] [inst_1 : Nonempty ι] [inst_2 : IsDirectedOrder ι]
  {M : Type u_1} [inst_3 : L.Structure M] (S : ι →o L.Substructure M) (i : ι),
  (FirstOrder.Language.DirectLimit.Equiv_iSup S).symm.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion ⋯) =
    FirstOrder.Language.DirectLimit.of L ι (fun x => ↥(S x))
      (fun x x_1 h => FirstOrder.Language.Substructure.inclusion ⋯) i
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.setIntegral_preCDF_fst : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℚ) {s : Set α},
  MeasurableSet s →
    ∀ [MeasureTheory.IsFiniteMeasure ρ],
      ∫ (x : α) in s, (ProbabilityTheory.preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd ↑r).real s
-- Mathlib.Data.PNat.Factors
PrimeMultiset.coe_prod : ∀ (v : PrimeMultiset), ↑v.prod = v.toNatMultiset.prod
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.toWord_mul : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : FreeGroup α), (x * y).toWord = FreeGroup.reduce (x.toWord ++ y.toWord)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Y ⟶ W) {Z_1 : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj W Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight h Z) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f h) g) h_1
-- Mathlib.ModelTheory.LanguageMap
/-- The composition of two language homomorphisms.  -/
_private.Mathlib.ModelTheory.LanguageMap.0.FirstOrder.Language.LHom.«term_∘ᴸ_» : Lean.TrailingParserDescr
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k a : α}, (t.erase k).getKey! a = if cmp k a = Ordering.eq then default else t.getKey! a
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] [inst_1 : CommSemiring β] (l : Filter α) (k : α → β),
  Asymptotics.SuperpolynomialDecay l k 0
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.weights_nonneg : ∀ (self : BoundingSieve) (n : ℕ), 0 ≤ self.weights n
-- Lean.Meta.LetToHave
/-- Like `findMCache?` but checks that `e` doesn't have any loose bvars.  -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.findCacheNoBVars? : Lean.Expr → Lean.Meta.LetToHave.M✝ (Option Lean.Meta.LetToHave.Result✝)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
/-- Fold a bilinear map along the generators of a term of the clifford algebra, with the rule
given by `foldr Q f hf n (ι Q m * x) = f m (foldr Q f hf n x)`.

For example, `foldr f hf n (r • ι R u + ι R v * ι R w) = r • f u n + f v (f w n)`.  -/
CliffordAlgebra.foldr : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                (Q : QuadraticForm R M) →
                  (f : M →ₗ[R] N →ₗ[R] N) →
                    (∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) → N →ₗ[R] CliffordAlgebra Q →ₗ[R] N