mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Nilpotent
/-- An additive group `G` is nilpotent iff there exists a descending central series
which reaches the trivial group in a finite time.  -/
AddSubgroup.nilpotent_iff_finite_descending_central_series : ∀ (G : Type u_1) [inst : AddGroup G], AddGroup.IsNilpotent G ↔ ∃ n H, AddSubgroup.IsDescendingCentralSeries H ∧ H n = ⊥
-- Mathlib.AlgebraicGeometry.Stalk
/-- If `x` is a point of `X`, this is the canonical morphism from `Spec(O_x)` to `X`.
 -/
AlgebraicGeometry.Scheme.fromSpecStalk : (X : AlgebraicGeometry.Scheme) → (x : ↥X) → AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ X
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.QuasiFiniteAt.of_weaklyQuasiFiniteAt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FiniteType R S] (p : Ideal S) [inst_4 : p.IsPrime] [Algebra.WeaklyQuasiFiniteAt R p],
  Algebra.QuasiFiniteAt R p
-- Init.Data.Option.Lemmas
Option.pbind_none : ∀ {α : Type u_1} {α_1 : Type u_2} {f : (a : α) → none = some a → Option α_1}, none.pbind f = none
-- Init.Data.Vector.Lemmas
Vector.mem_or_eq_of_mem_set : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {a b : α} {hi : i < n}, a ∈ xs.set i b hi → a ∈ xs ∨ a = b
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.injective_constr_of_linearIndependent : ∀ {ι : Type u_1} {R : Type u_3} {R₂ : Type u_4} {M : Type u_5} {M' : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  (b : Module.Basis ι R M) [inst_5 : Semiring R₂] [inst_6 : Module R₂ M'] [inst_7 : SMulCommClass R R₂ M'] {v : ι → M'},
  LinearIndependent R v → Function.Injective ⇑((b.constr R₂) v)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.Hom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} {x y : M₁.Hom M₂}, x = y ↔ x.app = y.app
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF →
    ∀ {k : α} [inst : Inhabited β] {f : β → β},
      Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.Const.modify t k f) k =
        (Option.map f (Std.DTreeMap.Raw.Const.get? t k)).get!
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- The subgroup fixing a set under a `MulAction`.  -/
fixingSubgroup : (M : Type u_1) → {α : Type u_2} → [inst : Group M] → [MulAction M α] → Set α → Subgroup M
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lequivCongrLeft_lof : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {κ : Type u_1} [inst_3 : DecidableEq ι] [inst_4 : DecidableEq κ] {e : ι ≃ κ}
  {i : ι} {k : κ} (hik : i = e.symm k) (x : M i) (y : M (e.symm k)),
  cast ⋯ x = y →
    (DirectSum.lequivCongrLeft R e) ((DirectSum.lof R ι M i) x) = (DirectSum.lof R κ (fun i => M (e.symm i)) k) y
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The map `K.X i ⟶ K.cycles j` induced by the differential `K.d i j`.  -/
HomologicalComplex.toCycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) → (i j : ι) → [inst_2 : K.HasHomology j] → K.X i ⟶ K.cycles j
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Equivalence.mapHomologicalComplex_unitIso : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [inst_4 : e.functor.PreservesZeroMorphisms]
  (c : ComplexShape ι),
  (e.mapHomologicalComplex c).unitIso =
    (CategoryTheory.Functor.mapHomologicalComplexIdIso W₁ c).symm ≪≫
      CategoryTheory.NatIso.mapHomologicalComplex e.unitIso c
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wf_insertMany₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w}
  [inst_4 : ForIn Id ρ ((a : α) × β a)] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size} {l : ρ},
  m.WF → (↑↑(Std.DHashMap.Internal.Raw₀.insertMany ⟨m, h⟩ l)).WF
-- Mathlib.Algebra.FreeMonoid.Count
FreeAddMonoid.count_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (x : α) (l : FreeAddMonoid α),
  (FreeAddMonoid.count x) l = List.count x (FreeAddMonoid.toList l)
-- Mathlib.Topology.Constructions
Homeomorph.piCurry_apply : ∀ {X : Type u_9} {Y : Type u_10} {Z : Type u_11} [inst : TopologicalSpace Z] (a : X × Y → Z) (a_1 : X) (a_2 : Y),
  Homeomorph.piCurry a a_1 a_2 = Function.curry a a_1 a_2
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Given a fully faithful functor `ι : C ⥤ V ⥤ D`,
a family of Day convolutions, candidate functions for `tensorObj` and `tensorHom`,
suitable isomorphisms
`ι.obj (tensorObj d d') ≅ ι.obj (tensorObj d) ⊛ ι.obj (tensorObj d')`
that behave in a lawful way with respect to the chosen Day convolutions, we can
construct a `MonoidalCategoryStruct` on `D`.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.mkMonoidalCategoryStruct : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (V : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (D : Type u₃) →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} D] →
                [CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] →
                  [∀ (v : V) (d : C),
                        CategoryTheory.Limits.PreservesColimitsOfShape
                          (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
                          (CategoryTheory.MonoidalCategory.tensorLeft v)] →
                    [∀ (v : V) (d : C),
                          CategoryTheory.Limits.PreservesColimitsOfShape
                            (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
                            (CategoryTheory.MonoidalCategory.tensorRight v)] →
                      [∀ (v : V) (d : C),
                            CategoryTheory.Limits.PreservesColimitsOfShape
                              (CategoryTheory.CostructuredArrow
                                (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                d)
                              (CategoryTheory.MonoidalCategory.tensorRight v)] →
                        [∀ (v : V) (d : C),
                              CategoryTheory.Limits.PreservesColimitsOfShape
                                (CategoryTheory.CostructuredArrow
                                  (CategoryTheory.Functor.fromPUnit
                                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                  d)
                                (CategoryTheory.MonoidalCategory.tensorLeft v)] →
                          CategoryTheory.MonoidalCategoryStruct D
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- A type synonym for `Fintype`, which we will equip with a category structure
where the morphisms are matrices with components in `R`.  -/
CategoryTheory.Mat : Type u → Type (u + 1)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Small
CategoryTheory.StructuredArrow.essentiallySmall : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} [CategoryTheory.EssentiallySmall.{w, v₁, u₁} C]
  [CategoryTheory.LocallySmall.{w, v₂, u₂} D],
  CategoryTheory.EssentiallySmall.{w, v₁, max u₁ v₂} (CategoryTheory.StructuredArrow S T)
-- Mathlib.Probability.Moments.SubGaussian
/-- **Hoeffding inequality** for sub-Gaussian random variables.  -/
ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ},
  ProbabilityTheory.iIndepFun X μ →
    ∀ {c : NNReal} {n : ℕ},
      (∀ i < n, ProbabilityTheory.HasSubgaussianMGF (X i) c μ) →
        ∀ {ε : ℝ}, 0 ≤ ε → μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, X i ω} ≤ Real.exp (-ε ^ 2 / (2 * ↑n * ↑c))
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoOpPushout_hom_inl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f.unop g.unop)
      (CategoryTheory.Limits.pullbackIsoOpPushout f g).hom.unop =
    (CategoryTheory.Limits.pullback.fst f g).unop
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Introduce a function `inverse` from `M →L[R] M₂` to `M₂ →L[R] M`, which sends `f` to `f.symm` if
`f` is a continuous linear equivalence and to `0` otherwise.  This definition is somewhat ad hoc,
but one needs a fully (rather than partially) defined inverse function for some purposes, including
for calculus.  -/
ContinuousLinearMap.inverse : {R : Type u_1} →
  {M : Type u_2} →
    {M₂ : Type u_3} →
      [inst : TopologicalSpace M] →
        [inst_1 : TopologicalSpace M₂] →
          [inst_2 : Semiring R] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] → [inst_5 : AddCommMonoid M₂] → [inst_6 : Module R M₂] → (M →L[R] M₂) → M₂ →L[R] M
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne.match_1.congr_eq_2 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1)
  (x : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) (h_1 : Unit → motive none)
  (h_2 :
    (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      (nodupkey : ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l]) →
        (nodup : [l].Nodup) → motive (some { clause := [l], nodupkey := nodupkey, nodup := nodup }))
  (h_3 : (val : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some val))
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (nodupkey : ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l])
  (nodup : [l].Nodup),
  x = some { clause := [l], nodupkey := nodupkey, nodup := nodup } →
    (match x with
      | none => h_1 ()
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } => h_2 l nodupkey nodup
      | some val => h_3 val) ≍
      h_2 l nodupkey nodup
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The type of arrows for the diagram indexing a pushout.  -/
CategoryTheory.Limits.WalkingSpan.Hom : CategoryTheory.Limits.WalkingSpan → CategoryTheory.Limits.WalkingSpan → Type
-- Mathlib.Data.Rat.Cast.Lemmas
/-- Casting a scientific literal via `ℚ` is the same as casting directly.  -/
Rat.cast_ofScientific : ∀ {K : Type u_2} [inst : DivisionRing K] (m : ℕ) (s : Bool) (e : ℕ),
  ↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.MonadSetTermId.mk : {m : Type → Type} → (Lean.Expr → m Unit) → Lean.Meta.Grind.Arith.CommRing.MonadSetTermId m
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Pseudofunctor.StrongTrans.Modification.id η).app a = CategoryTheory.CategoryStruct.id (η.app a)
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- This definition allows to endow `Π i, α i` with the Lp distance with the uniformity and
bornology being defeq to the product ones. It is useful to endow a type synonym of `Π i, α i` with
the Lp distance.  -/
PiLp.pseudoMetricSpaceToPi : (p : ENNReal) →
  {ι : Type u_2} →
    (α : ι → Type u_3) →
      [Fact (1 ≤ p)] → [Fintype ι] → [(i : ι) → PseudoMetricSpace (α i)] → PseudoMetricSpace ((i : ι) → α i)
-- Init.Data.SInt.Lemmas
Int8.sub_sub : ∀ (a b c : Int8), a - b - c = a - (b + c)
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem_append_left : ∀ {i : ℕ} {a b : ByteArray} {h : i < (a ++ b).size} (hlt : i < a.size), (a ++ b)[i] = a[i]
-- Mathlib.Data.List.Sort
List.Perm.eq_of_sortedLE : ∀ {α : Type u_1} [inst : PartialOrder α] {l₁ l₂ : List α}, l₁.SortedLE → l₂.SortedLE → l₁.Perm l₂ → l₁ = l₂
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀] (x : R)
  (y : MvPolynomial ι R₀),
  (Algebra.Presentation.tensorModelOfHasCoeffsEquiv R₀)
      (x ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (Algebra.Presentation.relationOfHasCoeffs R₀)))) y) =
    (algebraMap R S) x * (MvPolynomial.aeval P.val) y
-- Lean.Parser.Types
Lean.Parser.ParserInfo.mk.injEq : ∀ (collectTokens : List Lean.Parser.Token → List Lean.Parser.Token)
  (collectKinds : Lean.Parser.SyntaxNodeKindSet → Lean.Parser.SyntaxNodeKindSet) (firstTokens : Lean.Parser.FirstTokens)
  (collectTokens_1 : List Lean.Parser.Token → List Lean.Parser.Token)
  (collectKinds_1 : Lean.Parser.SyntaxNodeKindSet → Lean.Parser.SyntaxNodeKindSet)
  (firstTokens_1 : Lean.Parser.FirstTokens),
  ({ collectTokens := collectTokens, collectKinds := collectKinds, firstTokens := firstTokens } =
      { collectTokens := collectTokens_1, collectKinds := collectKinds_1, firstTokens := firstTokens_1 }) =
    (collectTokens = collectTokens_1 ∧ collectKinds = collectKinds_1 ∧ firstTokens = firstTokens_1)
-- Mathlib.Topology.EMetricSpace.Defs
Metric.nhdsWithin_basis_closedEBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α},
  (nhdsWithin x s).HasBasis (fun ε => 0 < ε) fun ε => Metric.closedEBall x ε ∩ s
-- Mathlib.Data.Analysis.Filter
/-- Construct a realizer for filter bind  -/
Filter.Realizer.bind : {α : Type u_1} →
  {β : Type u_2} → {f : Filter α} → {m : α → Filter β} → f.Realizer → ((i : α) → (m i).Realizer) → (f.bind m).Realizer
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.toSubsemiring_top : ∀ {R : Type u} [inst : NonAssocRing R], ⊤.toSubsemiring = ⊤
-- Init.Data.Order.Ord
Std.OrientedCmp.opposite : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp], Std.OrientedCmp fun a b => cmp b a
-- Std.Time.Date.Unit.Month
/-- `Quarter` represents a value between 1 and 4, inclusive, corresponding to the four quarters of a year.
 -/
Std.Time.Month.Quarter : Type
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.generate_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X) (Z : C) (f : Z ⟶ X),
  (CategoryTheory.Sieve.generate R).arrows f = ∃ Y h g, R g ∧ CategoryTheory.CategoryStruct.comp h g = f
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.descFunLift.eq_2 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (s : CategoryTheory.Limits.Cocone F), CommRingCat.Colimits.descFunLift F s CommRingCat.Colimits.Prequotient.zero = 0
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- If a group `G` acts on `α` by measurable maps, then each element `c : G` defines a measurable
automorphism of `α`.  -/
MeasurableEquiv.smul : {G : Type u_1} →
  {α : Type u_3} →
    [inst : MeasurableSpace α] → [inst_1 : Group G] → [inst_2 : MulAction G α] → [MeasurableConstSMul G α] → G → α ≃ᵐ α
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNonUnitalRing : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [NonUnitalRing R] → NonUnitalRing (l.Germ R)
-- Mathlib.Topology.CompactOpen
ContinuousMap.nhds_compactOpen_eq_iInf_nhds_induced : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)),
  nhds f = ⨅ s, ⨅ (_ : IsCompact s), Filter.comap (ContinuousMap.restrict s) (nhds (ContinuousMap.restrict s f))
-- Mathlib.Data.ENat.Basic
ENat.ofNat_ne_top : ∀ (a : ℕ) [inst : a.AtLeastTwo], OfNat.ofNat a ≠ ⊤
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The universal property of a limit cone: a map `W ⟶ t.pt` is the same as
a cone on `F` with cone point `W`.  -/
CategoryTheory.Limits.IsLimit.homEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit t → {W : C} → (W ⟶ t.pt) ≃ ((CategoryTheory.Functor.const J).obj W ⟶ F)
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.extend_unique : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [inst_2 : TopologicalSpace γ] [T2Space γ] {f : α → γ} {g : β → γ} (di : IsDenseInducing i),
  (∀ (x : α), g (i x) = f x) → Continuous g → di.extend f = g
-- Mathlib.RingTheory.Coprime.Lemmas
Nat.Coprime.cast : ∀ {R : Type u_1} [inst : CommRing R] {a b : ℕ}, a.Coprime b → IsCoprime ↑a ↑b
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsLeftUniformGroup.mk : ∀ {G : Type u_7} [inst : UniformSpace G] [inst_1 : Group G] [toIsTopologicalGroup : IsTopologicalGroup G],
  uniformity G = Filter.comap (fun x => x.1⁻¹ * x.2) (nhds 1) → IsLeftUniformGroup G
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.entryAtIdx! : {α : Type u} → {β : α → Type v} → [Inhabited ((a : α) × β a)] → Std.DTreeMap.Internal.Impl α β → ℕ → (a : α) × β a
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.isLE_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (e : X ≅ Y) (n : ℤ) [t.IsLE X n], t.IsLE Y n
-- Lean.Elab.InfoTree.Types
Lean.Elab.ErrorNameInfo.mk.sizeOf_spec : ∀ (stx : Lean.Syntax) (errorName : Lean.Name),
  sizeOf { stx := stx, errorName := errorName } = 1 + sizeOf stx + sizeOf errorName
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.rel_imp_rel : ∀ {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] {a b c d : α}, r c a → r b d → r a b → r c d
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.addLeftMono : ∀ {α : Type u_1} {N : Type u_2} [inst : LinearOrder α] [inst_1 : AddMonoid N] [inst_2 : LinearOrder N]
  [AddLeftStrictMono N], AddLeftMono (Colex (α →₀ N))
-- Init.Data.String.Decode
ByteArray.eq_of_utf8DecodeChar?_eq_some : ∀ {b : ByteArray} {c : Char},
  b.utf8DecodeChar? 0 = some c → b = (String.utf8EncodeChar c).toByteArray ++ b.extract c.utf8Size b.size
-- Init.Data.Ord.Basic
instOrdOrdering : Ord Ordering
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.botCharacteristic : ∀ {G : Type u_1} [inst : Group G], ⊥.Characteristic
-- Mathlib.GroupTheory.NoncommPiCoprod
/-- The canonical homomorphism from a family of additive subgroups where elements from
different subgroups commute  -/
AddSubgroup.noncommPiCoprod : {G : Type u_1} →
  [inst : AddGroup G] →
    {ι : Type u_2} →
      {H : ι → AddSubgroup G} →
        [Fintype ι] → (Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y) → ((i : ι) → ↥(H i)) →+ G
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- If `F : C ⥤ D` is an equivalence of categories and `C` is a `SplitEpiCategory`,
then `D` also is.  -/
CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsEquivalence] [CategoryTheory.SplitEpiCategory C],
  CategoryTheory.SplitEpiCategory D
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.equiv_refl : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  TopologicalSpace.Compacts.equiv (Homeomorph.refl α) = Equiv.refl (TopologicalSpace.Compacts α)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionalIdeal.one_mem_inv_coe_ideal : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] [inst_4 : IsDomain A] {I : Ideal A}, I ≠ ⊥ → 1 ∈ (↑I)⁻¹
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.comp_continuousLinearEquivAt_eq_coord_change : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e]
  [inst_10 : Bundle.Trivialization.IsLinear R e'] {b : B} (hb : b ∈ e.baseSet ∩ e'.baseSet),
  (Bundle.Trivialization.continuousLinearEquivAt R e b ⋯).symm.trans
      (Bundle.Trivialization.continuousLinearEquivAt R e' b ⋯) =
    Bundle.Trivialization.coordChangeL R e e' b
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.coe_coe_symm_apply_coe_apply : ∀ {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₂] {F : Type u_1} [inst_5 : EquivLike F A₁ A₂]
  [inst_6 : AlgEquivClass F R A₁ A₂] (f : F) (x : A₁), (↑f).symm (f x) = x
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSpanningSubgraph.le : ∀ {α : Type u_1} {β : Type u_2} {H G : Graph α β}, H ≤s G → H.IsSubgraph G
-- Mathlib.Data.Int.GCD
gcd_nsmul_eq_zero : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {m n : ℕ}, m.gcd n • a = 0 ↔ m • a = 0 ∧ n • a = 0
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_nsmul : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [inst : SMul M G] (a : G) (n : M), ↑(n • a) = n • ↑a
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_eq_zero_of_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E},
  V x = 0 → W x = 0 → VectorField.lieBracketWithin 𝕜 V W s x = 0
-- Mathlib.Analysis.Complex.Norm
Complex.abs_im_le_norm : ∀ (z : ℂ), |z.im| ≤ ‖z‖
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.hasDerivAt_inv_log : ∀ {x : ℝ}, x ≠ 0 → x ≠ 1 → x ≠ -1 → HasDerivAt (fun x => (Real.log x)⁻¹) (-x⁻¹ / Real.log x ^ 2) x
-- Mathlib.RingTheory.Coalgebra.TensorProduct
Coalgebra.TensorProduct.rid_symm_apply : ∀ {R : Type u_5} {S : Type u_6} {M : Type u_7} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  [inst_7 : Coalgebra S M] (a : M), (Coalgebra.TensorProduct.rid R S M).symm a = a ⊗ₜ[R] 1
-- Mathlib.Data.PFun
PFun.image_union : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : Set α), f.image (s ∪ t) = f.image s ∪ f.image t
-- Aesop.Builder.Unfold
Aesop.RuleBuilder.unfoldCore : Lean.Name → Lean.MetaM Aesop.LocalRuleSetMember
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- The sign of the horizontal differential in the total complex.  -/
ComplexShape.ε₁ : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) → (c₁₂ : ComplexShape I₁₂) → [TotalComplexShape c₁ c₂ c₁₂] → I₁ × I₂ → ℤˣ