mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntryD.eq_3 : ∀ {α : Type u} {β : α → Type v} (x : (a : α) × β a) (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
  (l r r_1 : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).minEntryD x =
    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minEntryD x
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- The equivalence between an additive topological group `G` and `Gᵐᵒᵖ` as a uniform
equivalence when `G` is equipped with the right uniformity and `Gᵐᵒᵖ` with the left uniformity.  -/
AddOpposite.opUniformEquivRight : (G : Type u_2) → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [inst_2 : IsTopologicalAddGroup G] → G ≃ᵤ Gᵃᵒᵖ
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.linearEquiv.eq_1 : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Invertible R M], Module.Invertible.linearEquiv R M = LinearEquiv.ofBijective (contractLeft R M) ⋯
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.map_comp_lTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : AddCommMonoid S] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R S] [inst_9 : Module R P]
  [inst_10 : Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N),
  TensorProduct.map f g ∘ₗ LinearMap.lTensor M g' = TensorProduct.map f (g ∘ₗ g')
-- Std.Sync.StreamMap
/-- This is an existential wrapper for AsyncStream that is used for the `.ofArray` function
with `CoeDep` so it's easier and we keep StreamMap on `Type 0`.
 -/
Std.AnyAsyncStream : Type → Type 1
-- Init.Data.List.Perm
List.not_perm_nil_cons : ∀ {α : Type u_1} (x : α) (l : List α), ¬[].Perm (x :: l)
-- Aesop.Script.TacticState
Aesop.Script.TacticState.applyTactic : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      Aesop.Script.TacticState →
        Lean.MVarId → Array Aesop.GoalWithMVars → Lean.MetavarContext → Lean.MetavarContext → m Aesop.Script.TacticState
-- Mathlib.Analysis.LocallyConvex.Basic
/-- Every neighbourhood of the origin is absorbent.  -/
absorbent_nhds_zero : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {A : Set E}
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E], A ∈ nhds 0 → Absorbent 𝕜 A
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.image_coe_preimage_inclusion_subset : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖)
  (U : Set (RestrictedProduct (fun i => R i) (fun i => A i) 𝓕)),
  DFunLike.coe '' RestrictedProduct.inclusion R A h ⁻¹' U ⊆ DFunLike.coe '' U
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst_self : ∀ (n : ℕ), n.stirlingFirst n = 1
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.Q_f_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (q n : ℕ)
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n })) ((AlgebraicTopology.DoldKan.Q q).f n) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n) (f.app (Opposite.op { len := n }))
-- Mathlib.Analysis.Calculus.Gradient.Basic
gradient_eq : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' : F → F}, (∀ (x : F), HasGradientAt f (f' x) x) → gradient f = f'
-- Lean.Server.Rpc.RequestHandling
_private.Lean.Server.Rpc.RequestHandling.0.Lean.Server.evalRpcProcedureUnsafe : Lean.Environment → Lean.Options → Lean.Name → Except String Lean.Server.RpcProcedure
-- Lean.Meta.Tactic.Contradiction
/-- Support for hypotheses such as
```
h : (x y : Nat) (ys : List Nat) → x = 0 → y::ys = [a, b, c] → False
```
This kind of hypotheses appear when proving conditional equation theorems for match expressions.  -/
Lean.Meta.Contradiction.Config.genDiseq : Lean.Meta.Contradiction.Config → Bool
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.isRightInversion_inv_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w t : W},
  cs.IsRightInversion w⁻¹ t ↔ cs.IsLeftInversion w t
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearEquiv.baseChange_symm_tmul : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] {e : M ≃ₗ[R] N} (a : A) (n : N),
  (LinearEquiv.baseChange R A M N e).symm (a ⊗ₜ[R] n) = a ⊗ₜ[R] e.symm n
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- The fibre of any presheaf `P : Cᵒᵖ ⥤ A` at `point J` is just `P` evaluated at
the terminal object.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
        [inst_2 : J.IsLocalSite] →
          {A : Type u'} →
            [inst_3 : CategoryTheory.Category.{v', u'} A] →
              [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                (P : CategoryTheory.Functor Cᵒᵖ A) →
                  (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).presheafFiber.obj P ≅
                    P.obj (Opposite.op (⊤_ C))
-- Mathlib.Algebra.Group.Hom.Defs
map_add : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [AddHomClass F M N] (f : F) (x y : M), f (x + y) = f x + f y
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.samePatternsVariables : ℕ → Lean.Elab.Term.CollectPatternVars.State → Lean.Elab.Term.CollectPatternVars.State → Bool
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.map_sub_left_ae : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableNeg G] [MeasurableAdd G]
  (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (x : G),
  Filter.map (fun t => x - t) (MeasureTheory.ae μ) = MeasureTheory.ae μ
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.feature__1 : Lean.ParserDescr
-- Init.Data.Int.Lemmas
Int.add_sub_add_right : ∀ (n k m : ℤ), n + k - (m + k) = n - m
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.isBigO : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =o[l] g → f =O[l] g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_maxKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {km : α}, t.maxKey? = some km → t.getKey! km = km
-- Mathlib.Analysis.Analytic.Order
/-- The set where an analytic function has zero or infinite order is discrete within its domain of
analyticity.
 -/
AnalyticOnNhd.codiscreteWithin_setOfPred_analyticOrderAt_eq_zero_or_top : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E},
  AnalyticOnNhd 𝕜 f U → {u | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤} ∈ Filter.codiscreteWithin U
-- Mathlib.Topology.Inseparable
SeparationQuotient.isOpenQuotientMap_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsOpenQuotientMap SeparationQuotient.mk
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.le_lt_combine : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α] (ctx : Lean.Grind.Linarith.Context α)
  (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.le_lt_combine_cert p₁ p₂ p₃ = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ ≤ 0 →
      Lean.Grind.Linarith.Poly.denote' ctx p₂ < 0 → Lean.Grind.Linarith.Poly.denote' ctx p₃ < 0
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.nodup_toList : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {a : α}, a...*.toList.Nodup
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_sub_lt_mk_left_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk (a - b) < ArchimedeanClass.mk a ↔ ArchimedeanClass.mk b < ArchimedeanClass.mk a
-- Mathlib.Topology.FiberBundle.Constructions
/-- Given trivializations `e₁`, `e₂` for bundle types `E₁`, `E₂` over a base `B`, the induced
trivialization for the fiberwise product of `E₁` and `E₂`, whose base set is
`e₁.baseSet ∩ e₂.baseSet`.  -/
Bundle.Trivialization.prod : {B : Type u_1} →
  [inst : TopologicalSpace B] →
    {F₁ : Type u_2} →
      [inst_1 : TopologicalSpace F₁] →
        {E₁ : B → Type u_3} →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
            {F₂ : Type u_4} →
              [inst_3 : TopologicalSpace F₂] →
                {E₂ : B → Type u_5} →
                  [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                    Bundle.Trivialization F₁ Bundle.TotalSpace.proj →
                      Bundle.Trivialization F₂ Bundle.TotalSpace.proj →
                        [(x : B) → Zero (E₁ x)] →
                          [(x : B) → Zero (E₂ x)] → Bundle.Trivialization (F₁ × F₂) Bundle.TotalSpace.proj
-- Std.Data.HashMap.Lemmas
Std.HashMap.forM_eq_forM_toList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α × β → m' PUnit.{w + 1}}, forM m f = forM m.toList f
-- Init.Data.List.Zip
_private.Init.Data.List.Zip.0.List.getElem?_zipWithAll.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (a? : Option α) (b? : Option β)
  (h_1 : Unit → motive none none) (h_2 : (a? : Option α) → (b? : Option β) → motive a? b?),
  (a? = none → b? = none → False) →
    (match a?, b? with
      | none, none => h_1 ()
      | a?, b? => h_2 a? b?) =
      h_2 a? b?
-- Lean.Elab.App
Lean.Elab.Term.ElabAppArgs.Context : Type
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.subst.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (x : α → L.Term β) (a : α),
  (FirstOrder.Language.var a).subst x = x a
-- Mathlib.CategoryTheory.MarkovCategory.Basic
CategoryTheory.MarkovCategory.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [toCopyDiscardCategory : CategoryTheory.CopyDiscardCategory C] →
        (∀ {X Y : C} (f : X ⟶ Y),
            CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit) →
          CategoryTheory.MarkovCategory C
-- Init.Data.List.MinMax
List.max?_eq_head? : ∀ {α : Type u} [inst : Max α] {l : List α}, List.Pairwise (fun a b => a ⊔ b = a) l → l.max? = l.head?
-- Lean.Meta.Match.SolveOverlap
_private.Lean.Meta.Match.SolveOverlap.0.Lean.Meta.Match.InjectionAnyResult.solved : Lean.Meta.Match.InjectionAnyResult✝
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {fallback : α}, t.getKeyD t.minKey! fallback = t.minKey!
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.pageHomologyNatIso_hom_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  (c : ℤ → ComplexShape κ) (r₀ r r' : ℤ) (pq : κ)
  (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.pageHomologyNatIso._auto_1)
  (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.pageHomologyNatIso._auto_3)
  (X : CategoryTheory.SpectralSequence C c r₀),
  (CategoryTheory.SpectralSequence.pageHomologyNatIso C c r₀ r r' pq hrr' hr).hom.app X = (X.iso r r' pq ⋯ ⋯).hom
-- Init.Data.Fin.Lemmas
Fin.coe_pred : ∀ {n : ℕ} (j : Fin (n + 1)) (h : j ≠ 0), ↑(j.pred h) = ↑j - 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_eq_getKeyD : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α} {h' : a ∈ m}, m.getKey a h' = m.getKeyD a fallback
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.Nonempty.smul_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β] [inst_1 : SMulZeroClass α β] {s : Set α}, s.Nonempty → s • 0 = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.instIsProperOfIso : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {Y : SSet} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom = B)
  [P.IsProper], (P.ofIso e hA).IsProper
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.map : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (f : R →+* S) (n ν : ℕ),
  Polynomial.map f (bernsteinPolynomial R n ν) = bernsteinPolynomial S n ν
-- Lean.Declaration
Lean.DefinitionSafety.safe : Lean.DefinitionSafety
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.isRatCondKernelCDF_preCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ],
  ProbabilityTheory.IsRatCondKernelCDF (fun p r => (ProbabilityTheory.preCDF ρ r p.2).toReal)
    (ProbabilityTheory.Kernel.const Unit ρ) (ProbabilityTheory.Kernel.const Unit ρ.fst)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_insert_of_notMem`. -/
Set.diff_insert_of_notMem : ∀ {α : Type u_1} {s t : Set α} {a : α}, a ∉ s → s \ insert a t = s \ t
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.gate : {α : Type} →
  Std.Tactic.BVDecide.Gate →
    Std.Tactic.BVDecide.BoolExpr α → Std.Tactic.BVDecide.BoolExpr α → Std.Tactic.BVDecide.BoolExpr α
-- Lean.Server.Requests
/-- Create a task which waits for the first snapshot matching `p`, handles various errors,
and if a matching snapshot was found executes `x` with it. If not found, the task executes
`notFoundX`.  -/
Lean.Server.RequestM.withWaitFindSnap : {β : Type} →
  Lean.Server.FileWorker.EditableDocument →
    (Lean.Server.Snapshots.Snapshot → Bool) →
      Lean.Server.RequestM β →
        (Lean.Server.Snapshots.Snapshot → Lean.Server.RequestM β) → Lean.Server.RequestM (Lean.Server.RequestTask β)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.instNormedField : {K : Type u_1} → [inst : Field K] → (v : NumberField.InfinitePlace K) → NormedField v.Completion
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.IsSkeletonOf.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor D C},
  CategoryTheory.Skeletal D →
    autoParam F.IsEquivalence CategoryTheory.IsSkeletonOf.eqv._autoParam → CategoryTheory.IsSkeletonOf C D F
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.mk.inj : ∀
  {transformed :
    Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)}
  {next : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)}
  {transformed_1 :
    Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)}
  {next_1 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)},
  { transformed := transformed, next := next } = { transformed := transformed_1, next := next_1 } →
    transformed = transformed_1 ∧ next = next_1
-- Mathlib.CategoryTheory.Generator.HomologicalComplex
/-- If `X : α → C` is a separating family, and `c : ComplexShape ι` has no loop,
then this is a separating family indexed by `α × ι` in `HomologicalComplex C c`,
which consists of homological complexes that are nonzero in at most
two (consecutive) degrees.  -/
HomologicalComplex.separatingFamily : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type w} →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [CategoryTheory.Limits.HasZeroObject C] → {α : Type t} → (α → C) → α × ι → HomologicalComplex C c
-- Mathlib.Order.Hom.Basic
/-- Notation for an `OrderHom`.  -/
«term_→o_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.coe_quotQuotMkₐ : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  ⇑(DoubleQuot.quotQuotMkₐ R I J) = ⇑(DoubleQuot.quotQuotMk I J)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.latticeBasis_zero : ∀ (L : PeriodPair), ↑(L.latticeBasis 0) = L.ω₁
-- Mathlib.Data.List.AList
AList.ext_iff : ∀ {α : Type u} {β : α → Type v} {s t : AList β}, s = t ↔ s.entries = t.entries
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.prod_top : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] [inst_7 : IsScalarTower R B B] [inst_8 : SMulCommClass R B B], ⊤.prod ⊤ = ⊤
-- Mathlib.RingTheory.Congruence.Defs
/-- The inductively defined smallest ring congruence relation containing a given binary
relation.  -/
RingConGen.Rel : {R : Type u_1} → [Add R] → [Mul R] → (R → R → Prop) → R → R → Prop
-- Mathlib.Topology.LocallyClosed
/-- A set `s` is locally closed if one of the equivalent conditions below hold
1. It is the intersection of some open set and some closed set.
2. The coborder `(closure s \ s)ᶜ` is open.
3. `s` is closed in some neighborhood of `x` for all `x ∈ s`.
4. Every `x ∈ s` has some open neighborhood `U` such that `U ∩ closure s ⊆ s`.
5. `s` is open in the closure of `s`.
 -/
isLocallyClosed_tfae : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X),
  [IsLocallyClosed s, IsOpen (coborder s), ∀ x ∈ s, ∃ U ∈ nhds x, IsClosed (Subtype.val ⁻¹' s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s, IsOpen (Subtype.val ⁻¹' s)].TFAE
-- Mathlib.Order.Minimal
not_minimal_subset_iff : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α}, P s → (¬Minimal P s ↔ ∃ t ⊂ s, P t)
-- Mathlib.Computability.Encoding
Computability.instDecidableEqΓ' : DecidableEq Computability.Γ'
-- Mathlib.Tactic.Linter.TextBased
/-- A unicode character was used that isn't allowed  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.unwantedUnicode : Char → Mathlib.Linter.TextBased.StyleError✝
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.toLinearEquiv_mulRight : ∀ {R : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] (u : ↥(unitary A)),
  (Unitary.mulRight R u).toLinearEquiv = Units.mulRightLinearEquiv R (Unitary.toUnits u)
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsAddTorsion.torsionAddEquiv_symm_apply_coe`. -/
AddMonoid.IsTorsion.torsionAddEquiv_symm_apply_coe : ∀ {G : Type u_1} [inst : AddCommMonoid G] (tG : IsAddTorsion G) (a : G), ↑(tG.torsionAddEquiv.symm a) = a
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pattern.ForwardSliceSearcher.isSome_skipPrefix? : ∀ {pat s : String.Slice},
  (String.Slice.Pattern.ForwardSliceSearcher.skipPrefix? pat s).isSome =
    String.Slice.Pattern.ForwardSliceSearcher.startsWith pat s
-- Init.Data.Sum.Basic
Sum.instBEq : {α : Type u_1} → {β : Type u_2} → [BEq α] → [BEq β] → BEq (α ⊕ β)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.equiv_empty_iff_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp}, t.Equiv Std.TreeSet.empty ↔ t.isEmpty = true
-- Lean.Elab.Do.Legacy
/-- Syntax representing the monad associated with the do notation.  -/
Lean.Elab.Term.Do.ToCodeBlock.Context.m : Lean.Elab.Term.Do.ToCodeBlock.Context → Lean.Syntax
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : t₁.WF)
  (h₂ : t₂.WF),
  t₁.Equiv t₂ →
    ∀ {k : α}, (Std.DTreeMap.Internal.Impl.erase k t₁ ⋯).impl.Equiv (Std.DTreeMap.Internal.Impl.erase k t₂ ⋯).impl
-- Mathlib.RingTheory.PowerSeries.Exp
/-- Shows that $e^{aX} * e^{bX} = e^{(a + b)X}$  -/
PowerSeries.exp_mul_exp_eq_exp_add : ∀ {A : Type u_4} [inst : CommRing A] [inst_1 : Algebra ℚ A] (a b : A),
  (PowerSeries.rescale a) (PowerSeries.exp A) * (PowerSeries.rescale b) (PowerSeries.exp A) =
    (PowerSeries.rescale (a + b)) (PowerSeries.exp A)
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.isOpenMap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsOpenEmbedding f → IsOpenMap f
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodCongr_symm_apply : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (e : M ≃+ N) (e' : M' ≃+ N'),
  ⇑(e.coprodCongr e').symm = ⇑(AddMonoid.Coprod.map ↑e.symm ↑e'.symm)
-- Mathlib.Algebra.GroupWithZero.Divisibility
dvd_antisymm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {a b : α} [Subsingleton αˣ], a ∣ b → b ∣ a → a = b
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_replaceEntry_of_key_ne : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [LawfulBEq α] {a : α} {b : β a} {l : List ((a : α) × β a)}
  (p : (a : α) × β a), p.fst ≠ a → (p ∈ Std.Internal.List.replaceEntry a b l ↔ p ∈ l)
-- Mathlib.Algebra.Homology.ModelCategory.Injective
CochainComplex.Plus.modelCategoryQuillen.instIsStableUnderRetractsFibrations : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopicalAlgebra.fibrations (CochainComplex.Plus C)).IsStableUnderRetracts
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Given a left adjoint functor between categories of cocones,
the image of a colimit cocone is a colimit cocone.
 -/
CategoryTheory.Limits.IsColimit.ofLeftAdjoint : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {D : Type u₄} →
                [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                  {G : CategoryTheory.Functor K D} →
                    {right : CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone G)} →
                      {left :
                          CategoryTheory.Functor (CategoryTheory.Limits.Cocone G) (CategoryTheory.Limits.Cocone F)} →
                        (left ⊣ right) →
                          {c : CategoryTheory.Limits.Cocone G} →
                            CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsColimit (left.obj c)
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.exists_smul_eq_mk_rep : ∀ (K : Type u_1) {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v : V)
  (hv : v ≠ 0), ∃ a, a • v = (Projectivization.mk K v hv).rep
-- Std.Data.TreeSet.Slice
Std.TreeSet.toList_rci : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.toList_rci._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet α cmp} {bound : α},
  Std.Slice.toList (Std.Rci.Sliceable.mkSlice t bound...*) = List.filter (fun e => (cmp e bound).isGE) t.toList
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vlt.trans : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, x <ᵥ y → y <ᵥ z → x <ᵥ z