mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.forget₂Mon_obj_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.Grp C), ((CategoryTheory.Grp.forget₂Mon C).obj A).X = A.X
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : (a : α) → β a → Bool} {k : α} {h' : k ∈ Std.DTreeMap.filter f t},
  (Std.DTreeMap.filter f t).getKey k h' = t.getKey k ⋯
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_eq_zero_iff : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E] {f : k → E} {a b : k},
  slope f a b = 0 ↔ f a = f b
-- Aesop.Stats.Basic
Aesop.Stats.ruleSelection : Aesop.Stats → Aesop.Nanos
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_sub_singleton : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x y : E), Metric.ball x δ - {y} = Metric.ball (x - y) δ
-- Init.Data.Array.Basic
/-- Appends an array and a list.

Takes time proportional to the length of the list..

Examples:
* `#[1, 2, 3].appendList [4, 5] = #[1, 2, 3, 4, 5]`.
* `#[].appendList [4, 5] = #[4, 5]`.
* `#[1, 2, 3].appendList [] = #[1, 2, 3]`.
 -/
Array.appendList : {α : Type u} → Array α → List α → Array α
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.toLinearMap_mapL : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →L[𝕜] F) (g : G →L[𝕜] H),
  ↑(TensorProduct.mapL f g) = TensorProduct.map ↑f ↑g
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasurableSet.of_mem_measurableCylinders : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)] {s : Set ((i : ι) → α i)},
  s ∈ MeasureTheory.measurableCylinders α → MeasurableSet s
-- Mathlib.Analysis.Calculus.ImplicitContDiff
ContDiffAt.hasStrictFDerivAt_implicitFunction : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂] [inst_5 : NormedSpace 𝕜 E₂]
  [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F]
  [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {n : WithTop ℕ∞} (cdf : ContDiffAt 𝕜 n f u) (pn : n ≠ 0)
  (if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  HasStrictFDerivAt (cdf.implicitFunction pn if₂)
    (-(fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).inverse ∘SL fderiv 𝕜 f u ∘SL ContinuousLinearMap.inl 𝕜 E₁ E₂)
    u.1
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- The iteration on a successor element is the successor.  -/
CategoryTheory.SmallObject.SuccStruct.Iteration.arrowSucc_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j : J} (self : Φ.Iteration j)
  (i : J) (hi : i < j), CategoryTheory.SmallObject.SuccStruct.arrowSucc self.F i hi = Φ.toSuccArrow (self.F.obj ⟨i, ⋯⟩)
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- Condition that a presheaf with values in a concrete category is separated for
a Grothendieck topology.  -/
CategoryTheory.Presheaf.IsSeparated : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        CategoryTheory.GrothendieckTopology C →
          CategoryTheory.Functor Cᵒᵖ A →
            {FA : A → A → Type u_1} →
              {CA : A → Type u_2} →
                [inst : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] → [CategoryTheory.ConcreteCategory A FA] → Prop
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_bot' : ∀ {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [NeZero P] (X : Ω → ENNReal),
  P⁻[X | ⊥] = fun x => (P Set.univ)⁻¹ • ∫⁻ (ω : Ω), X ω ∂P
-- Mathlib.Order.Hom.Basic
/-- There is a unique monotone map from a subsingleton to itself.  -/
OrderHom.unique : {α : Type u_2} → [inst : Preorder α] → [Subsingleton α] → Unique (α →o α)
-- Mathlib.Order.Bounds.Image
/-- The image under a monotone function on a set `t` of a subset which has a lower bound
in `t` is bounded below.  -/
MonotoneOn.map_bddBelow : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α},
  MonotoneOn f t → s ⊆ t → (lowerBounds s ∩ t).Nonempty → BddBelow (f '' s)
-- Mathlib.AlgebraicGeometry.Artinian
/-- A scheme is Artinian if and only if it is Noetherian and has the discrete topology.  -/
AlgebraicGeometry.IsArtinianScheme.iff_isNoetherian_and_discreteTopology : ∀ {X : AlgebraicGeometry.Scheme},
  AlgebraicGeometry.IsArtinianScheme X ↔ AlgebraicGeometry.IsNoetherian X ∧ DiscreteTopology ↥X
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_ofNat_of_lt_two_pow_numBits : ∀ {n : ℕ}, n < 2 ^ (System.Platform.numBits - 1) → (ISize.ofNat n).toNatClampNeg = n
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- If `f` can be approximated by multiseries with negative leading exponent, then
it tends to zero.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.neg_leadingExp_tendsto_zero : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)},
  ms.leadingExp < 0 → ms.Approximates → Filter.Tendsto ms.toFun Filter.atTop (nhds 0)
-- Mathlib.Probability.ConditionalProbability
/-- The conditional probability measure of measure `μ` on set `s` is `μ` restricted to `s`
and scaled by the inverse of `μ s` (to make it a probability measure):
`(μ s)⁻¹ • μ.restrict s`.  -/
ProbabilityTheory.«term__[_|_]» : Lean.TrailingParserDescr
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.unitOfList_nil : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.ExtDTreeMap.Const.unitOfList [] cmp = ∅
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.limitCone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [inst_2 :
    ∀ (X : Cᵒᵖ),
      Small.{v, max u₂ v}
        ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections],
  (PresheafOfModules.limitCone F).pt = PresheafOfModules.limitPresheafOfModules F
-- Aesop.Options.Public
/-- If `true`, print a warning when Aesop does not prove the goal.
This can also be turned off globally with the option `aesop.warn.nonterminal`.
 -/
Aesop.Options.warnOnNonterminal : Aesop.Options → Bool
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.isReal_comp_iff : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] {f : k ≃+* K} {φ : K →+* ℂ},
  NumberField.ComplexEmbedding.IsReal (φ.comp ↑f) ↔ NumberField.ComplexEmbedding.IsReal φ
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.projectiveFamilyContent_iUnion_le : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} (hP : MeasureTheory.IsProjectiveMeasureFamily P)
  {s : ℕ → Set ((i : ι) → α i)},
  (∀ (n : ℕ), s n ∈ MeasureTheory.measurableCylinders α) →
    ∀ (n : ℕ),
      (MeasureTheory.projectiveFamilyContent hP) (⋃ i, ⋃ (_ : i ≤ n), s i) ≤
        ∑ i ∈ Finset.range (n + 1), (MeasureTheory.projectiveFamilyContent hP) (s i)
-- Mathlib.CategoryTheory.Action
/-- A target vertex `t` and a scalar `g` determine a morphism in the action groupoid.  -/
CategoryTheory.ActionCategory.homOfPair : {X : Type u} →
  {G : Type u_2} → [inst : Group G] → [inst_1 : MulAction G X] → (t : X) → (g : G) → ⟨(), g⁻¹ • t⟩ ⟶ ⟨(), t⟩
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_sub_self_eq : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R} [IsOrderedRing R],
  Int.fract a ≠ 0 → ↑⌈a⌉ - a = 1 - Int.fract a
-- Mathlib.Topology.Algebra.Order.Module
instContinuousConstSMulSubtypeLeOfNat : ∀ {R : Type u_1} {α : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : SMul R α]
  [inst_3 : TopologicalSpace α] [ContinuousConstSMul R α], ContinuousConstSMul { r // 0 ≤ r } α
-- Std.Http.Internal.IndexMultiMap
/-- Updates all values associated with `key` by applying `f` to each one.
If the key is absent, returns the map unchanged.
 -/
Std.Internal.IndexMultiMap.update : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        [EquivBEq α] →
          [LawfulHashable α] → Std.Internal.IndexMultiMap α β → α → (β → β) → Std.Internal.IndexMultiMap α β
-- Init.Data.Order.ClassesExtra
Std.LawfulOrderOrd.mk : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α],
  (∀ (a b : α), (compare a b).isLE = true ↔ a ≤ b) →
    (∀ (a b : α), (compare a b).isGE = true ↔ b ≤ a) → Std.LawfulOrderOrd α
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.localization_away_isOpenEmbedding : ∀ {R : Type u} [inst : CommSemiring R] (S : Type v) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (r : R)
  [IsLocalization.Away r S], Topology.IsOpenEmbedding (PrimeSpectrum.comap (algebraMap R S))
-- Mathlib.Order.SupIndep
iSupIndep.le_iff_eq_of_iSup_eq_top : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] [IsModularLattice α] {f g : ι → α},
  iSupIndep g → iSup f = ⊤ → (f ≤ g ↔ f = g)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- The equivalence between characters and algebra homomorphisms into the base field.  -/
WeakDual.CharacterSpace.equivAlgHom : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NormedRing A] →
        [CompleteSpace A] → [inst_3 : NormedAlgebra 𝕜 A] → ↑(WeakDual.characterSpace 𝕜 A) ≃ (A →ₐ[𝕜] 𝕜)
-- Mathlib.Topology.MetricSpace.Completion
UniformSpace.Completion.edist_eq : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), edist ↑x ↑y = edist x y
-- Mathlib.Data.Finset.CastCard
Finset.cast_card_inter : ∀ {α : Type u_1} {R : Type u_2} {s t : Finset α} [inst : DecidableEq α] [inst_1 : AddGroupWithOne R],
  ↑(s ∩ t).card = ↑s.card + ↑t.card - ↑(s ∪ t).card
-- Mathlib.Algebra.Group.AddChar
AddChar.inv_apply' : ∀ {A : Type u_1} {M : Type u_2} [inst : AddCommGroup A] [inst_1 : DivisionCommMonoid M] (ψ : AddChar A M) (a : A),
  ψ⁻¹ a = (ψ a)⁻¹
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_closure_eq_of_disjoint : ∀ {α : Type u_1} (M : Matroid α) {D X : Set α}, Disjoint X D → (M.delete D).closure X = M.closure X \ D
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.instIsScalarTower : ∀ {G : Type u_1} {G' : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst_1 : Group G'] [inst_2 : SMul G G']
  [inst_3 : MulAction G β] [inst_4 : MulAction G' β] [IsScalarTower G G' β], IsScalarTower G G' (α ↪ β)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.AddConstAsyncResult.checkedEnvPromise : Lean.Environment.AddConstAsyncResult → IO.Promise Lean.Kernel.Environment
-- Mathlib.CategoryTheory.Yoneda
/-- Alternative constructor for `F.IsCorepresentable`, which takes as an input an
isomorphism `coyoneda.obj (op X) ≅ F`.  -/
CategoryTheory.Functor.IsCorepresentable.mk' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v₁)} {X : C}
  (e : CategoryTheory.coyoneda.obj (Opposite.op X) ≅ F), F.IsCorepresentable
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.pi.eq_1 : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → Group (f i)] (I : Set η) (H : (i : η) → Subgroup (f i)),
  Subgroup.pi I H = { toSubmonoid := Submonoid.pi I fun i => (H i).toSubmonoid, inv_mem' := ⋯ }
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.instToStringError : ToString Std.Internal.Parsec.Error
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.map_natCast : ∀ {α : Type u} {β : Type v} [inst : AddMonoidWithOne α] {f : α → β} (n : ℕ), WithTop.map f ↑n = ↑(f ↑n)
-- Mathlib.Order.WellFoundedSet
Set.IsStrictOrder.subset : ∀ {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α}, IsStrictOrder α fun a b => r a b ∧ a ∈ s ∧ b ∈ s
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H1AddEquivOfIsTrivial_symm_tmul : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial] (g : G) (a : ↑A),
  (groupHomology.H1AddEquivOfIsTrivial A).symm (Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.cycles₁IsoOfIsTrivial A).inv) fun₀ | g => a)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localRingHom_to_map : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
  (J : Ideal P) [inst_2 : J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) (x : R),
  (Localization.localRingHom I J f hIJ) ((algebraMap R (Localization.AtPrime I)) x) =
    (algebraMap P (Localization.AtPrime J)) (f x)
-- Mathlib.Order.Filter.Map
Filter.canLift : ∀ {α : Type u_1} {β : Type u_2} (c : β → α) (p : α → Prop) [CanLift α β c p],
  CanLift (Filter α) (Filter β) (Filter.map c) fun f => ∀ᶠ (x : α) in f, p x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Elimination stack. For every variable in `elimStack`. If `x` in `elimStack`, then `elimEqs[x]` is not `none`.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.elimStack : Lean.Meta.Grind.Arith.Cutsat.State → List Int.Internal.Linear.Var
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsImmersion f]
  (U : (↑(AlgebraicGeometry.Scheme.Hom.coborderRange f)).Opens),
  (TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.liftCoborder f).base).obj U =
    (TopologicalSpace.Opens.map f.base).obj
      ((AlgebraicGeometry.Scheme.Hom.opensFunctor (AlgebraicGeometry.Scheme.Hom.coborderRange f).ι).obj U)
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.ofIterM : {m : Type u_1 → Type u_2} → {β α : Type u_1} → [Std.Iterator α m β] → Std.IterM m β → Std.BundledIterM m β
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_le_iff_le_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {T : Submonoid N},
  Submonoid.map f S ≤ T ↔ S ≤ Submonoid.comap f T
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.mult_coe_ne_zero : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K}, ↑w.mult ≠ 0
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Inverse if `fieldInst?` is `some inst`  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.invFn? : Lean.Meta.Grind.Arith.CommRing.CommRing → Option Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.BinaryBiconeMorphism.winl : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B),
  CategoryTheory.CategoryStruct.comp A.inl self.hom = B.inl
-- Mathlib.Order.Max
isMax_toDual_iff : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMax (OrderDual.toDual a) ↔ IsMin a
-- Mathlib.Data.List.Basic
List.reverse_bijective : ∀ {α : Type u}, Function.Bijective List.reverse
-- Mathlib.Data.Multiset.UnionInter
Multiset.Nodup.inter_left : ∀ {α : Type u_1} {s : Multiset α} [inst : DecidableEq α] (t : Multiset α), s.Nodup → (s ∩ t).Nodup
-- Mathlib.Algebra.Group.Action.Faithful
FaithfulVAdd.tower_bot : ∀ (R : Type u_4) (S : Type u_5) (T : Type u_6) [inst : AddMonoid S] [inst_1 : AddZeroClass T] [inst_2 : VAdd R S]
  [inst_3 : VAdd R T] [inst_4 : AddAction S T] [VAddAssocClass R S S] [VAddAssocClass R T T] [VAddAssocClass R S T]
  [FaithfulVAdd R T], FaithfulVAdd R S
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.finiteDimensional_quot_dualCoannihilator_iff : ∀ {K : Type u_4} {V : Type u_5} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {W : Submodule K (Module.Dual K V)}, FiniteDimensional K (V ⧸ W.dualCoannihilator) ↔ FiniteDimensional K ↥W
-- Init.Data.Array.Lemmas
Array.flatten_push : ∀ {α : Type u_1} {xss : Array (Array α)} {xs : Array α}, (xss.push xs).flatten = xss.flatten ++ xs
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- Multiplication with a temperate growth function as a continuous linear map on `𝓢'(E, F)`.  -/
TemperedDistribution.smulLeftCLM : {E : Type u_3} →
  (F : Type u_4) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : AddCommGroup F] →
          [inst_3 : Module ℂ F] →
            [inst_4 : TopologicalSpace F] →
              [inst_5 : IsTopologicalAddGroup F] →
                [inst_6 : ContinuousConstSMul ℂ F] → (E → ℂ) → TemperedDistribution E F →L[ℂ] TemperedDistribution E F
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.reindexEquiv.eq_1 : ∀ {n : Type u_1} {p : Type u_2} {R : Type u₂} (e : n ≃ p) (t : Matrix.TransvectionStruct n R),
  Matrix.TransvectionStruct.reindexEquiv e t = { i := e t.i, j := e t.j, hij := ⋯, c := t.c }
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.quot_mk_eq_quotient_map : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : C ⟶ D),
  Quot.mk (CategoryTheory.HomRel.CompClosure (homotopic V c)) f = (HomotopyCategory.quotient V c).map f
-- Mathlib.Algebra.Order.Ring.Basic
/-- **Alias** of the reverse direction of `Odd.pow_nonpos_iff`. -/
Odd.pow_nonpos : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R],
  Odd n → a ≤ 0 → a ^ n ≤ 0
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ofLp_smul : ∀ (p : ENNReal) {K : Type u_1} {V : Type u_4} [inst : SMul K V] (c : K) (x : WithLp p V), (c • x).ofLp = c • x.ofLp
-- Lean.ErrorExplanation
/-- An explanation of a named error message.

Error explanations are rendered in the manual; a link to the resulting manual page is displayed at
the bottom of corresponding error messages thrown using `throwNamedError` or `throwNamedErrorAt`.
 -/
Lean.ErrorExplanation : Type
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidRevSearchFrom.mismatched : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {l : List (String.Slice.Pattern.SearchStep s)} {startPos endPos : s.Pos},
  startPos < endPos →
    (∀ (pos : s.Pos), startPos < pos → pos ≤ endPos → ¬String.Slice.Pattern.Model.RevMatchesAt pat pos) →
      String.Slice.Pattern.Model.IsValidRevSearchFrom pat startPos l →
        String.Slice.Pattern.Model.IsValidRevSearchFrom pat endPos
          (String.Slice.Pattern.SearchStep.rejected startPos endPos :: l)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.instIsAddMonHomId : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M], CategoryTheory.IsAddMonHom (CategoryTheory.CategoryStruct.id M)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.center_eq_bot_of_odd_ne_one : ∀ {n : ℕ}, Odd n → n ≠ 1 → Subgroup.center (DihedralGroup n) = ⊥
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.norm_num_ext.sModNat.eq_2 : ∀ (q i : ℕ), LucasLehmer.norm_num_ext.sModNat q i.succ = (LucasLehmer.norm_num_ext.sModNat q i ^ 2 + (q - 2)) % q
-- Lean.Elab.DeclarationRange
/-- Derives and adds declaration ranges from given syntax trees. If `rangeStx` does not have a range,
nothing is added. If `selectionRangeStx` does not have a range, it is defaulted to that of
`rangeStx`.
 -/
Lean.Elab.addDeclarationRangesFromSyntax : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadFileMap m] → Lean.Name → Lean.Syntax → optParam Lean.Syntax Lean.Syntax.missing → m Unit
-- Mathlib.Algebra.Ring.Int.Defs
Int.instDistrib : Distrib ℤ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, (t.erase k).getKey! k = default
-- Std.Data.Iterators.Producers.Repeat
Std.Iterators.Types.RepeatIterator.mk.injEq : ∀ {α : Type u} {f : α → α} (next next_1 : α), ({ next := next } = { next := next_1 }) = (next = next_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m m_1 : Std.DHashMap.Raw α β) (e_m : m = m_1)
  (a a_1 : α) (e_a : a = a_1) (h : a ∈ m), m.getKey a h = m_1.getKey a_1 ⋯
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.RightLinear.inv_μᵣ : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] [inst_6 : F.RightLinear C] (c : C) (d : D),
  CategoryTheory.inv (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c) = CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c
-- Mathlib.Algebra.Algebra.Hom
RingHom.toNatAlgHom_coe : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S), ⇑f.toNatAlgHom = ⇑f
-- Mathlib.Data.Finset.Basic
/-- Given a finset `l` and a predicate `p`, associate to a proof that there is a unique element of
`l` satisfying `p` this unique element, as an element of the corresponding subtype.  -/
Finset.chooseX : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → (l : Finset α) → (∃! a, a ∈ l ∧ p a) → { a // a ∈ l ∧ p a }
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.id_comp : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴),
  (CategoryTheory.BasedFunctor.id 𝒳).comp F = F
-- Mathlib.Order.BooleanAlgebra.Basic
inf_compl_eq_bot' : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α], x ⊓ xᶜ = ⊥
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.coe_addMonoidHom_symm_comp_coe_addMonoidHom : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (e : M ≃+ N),
  (↑e.symm).comp ↑e = AddMonoidHom.id M
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
/-- The tensor algebra is isomorphic to a direct sum of tensor powers.  -/
TensorAlgebra.equivDirectSum : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → TensorAlgebra R M ≃ₐ[R] DirectSum ℕ fun n => TensorPower R n M
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.subtype_apply : ∀ {R : Type u_1} [inst : Ring R] (I : TwoSidedIdeal R) (x : ↥I), I.subtype x = ↑x
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.of_forall_contains_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [LawfulBEq α],
  (∀ (k : α), m₁.contains k = m₂.contains k) → m₁.Equiv m₂
-- Mathlib.Data.ENNReal.Basic
ENNReal.iUnion_Iio_coe_nat : ⋃ n, Set.Iio ↑n = {⊤}ᶜ