mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.HNNExtension
/-- To avoid duplicating code, we define `toSubgroup A B u` and `toSubgroupEquiv u`
where `u : ℤˣ` is `1` or `-1`. `toSubgroup A B u` is `A` when `u = 1` and `B` when `u = -1`,
and `toSubgroupEquiv` is `φ` when `u = 1` and `φ⁻¹` when `u = -1`. `toSubgroup u` is the subgroup
such that for any `a ∈ toSubgroup u`, `t ^ (u : ℤ) * a = toSubgroupEquiv a * t ^ (u : ℤ)`.  -/
HNNExtension.toSubgroup : {G : Type u_1} → [inst : Group G] → Subgroup G → Subgroup G → ℤˣ → Subgroup G
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup L] [inst_2 : Module R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M) [inst_5 : Module.Free R M]
  [inst_6 : Module.Finite R M] [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] (x : L) [Nontrivial R],
  φ.IsNilRegular x ↔ (LinearMap.charpoly (φ x)).natTrailingDegree = φ.nilRank
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.ring : {α : Type u_1} →
  [inst : Ring α] →
    [inst_1 : UniformSpace α] → [IsTopologicalRing α] → [IsUniformAddGroup α] → Ring (UniformSpace.Completion α)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The index restriction function of a small `0`-hypercover.  -/
CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {S : C} →
        (E : J.ZeroHypercover S) → [inst_1 : E.Small] → CategoryTheory.Precoverage.ZeroHypercover.Small.Index E → E.I₀
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.coe_map_of_surjective : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L},
  Function.Surjective ⇑f → ↑(LieIdeal.map f I) = Submodule.map ↑f ↑I
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddMonoid.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → AddMonoid (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)],
  DirectLimit.instAddMonoid =
    { toAddSemigroup := DirectLimit.instAddSemigroupOfAddHomClass,
      toZero := DirectLimit.instAddZeroClassOfAddMonoidHomClass.toZero, zero_add := ⋯, add_zero := ⋯,
      nsmul := fun n => DirectLimit.map f f (fun x x_1 => n • x_1) ⋯, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Std.Http.Data.Extensions
_private.Std.Http.Data.Extensions.0.Std.Http.Extensions.data : Std.Http.Extensions → Std.TreeMap Lean.Name Dynamic Std.Http.Extensions.compareName
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- `AlgHom` to `⊤ : Subalgebra R A`.  -/
Algebra.toTop : {R : Type u} → {A : Type v} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → A →ₐ[R] ↥⊤
-- Mathlib.RingTheory.Finiteness.Defs
Submodule.fg_def : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M}, N.FG ↔ ∃ S, S.Finite ∧ Submodule.span R S = N
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.mul_star : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (x y : R),
  { re := x, im := y } * star { re := x, im := y } =
    (algebraMap R (QuadraticAlgebra R a b)) x * (algebraMap R (QuadraticAlgebra R a b)) x +
        (algebraMap R (QuadraticAlgebra R a b)) b * (algebraMap R (QuadraticAlgebra R a b)) x *
          (algebraMap R (QuadraticAlgebra R a b)) y -
      (algebraMap R (QuadraticAlgebra R a b)) a * (algebraMap R (QuadraticAlgebra R a b)) y *
        (algebraMap R (QuadraticAlgebra R a b)) y
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_gcd_cert : ℤ → ℤ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.Data.Fin.SuccPred
finCongr_apply_coe : ∀ {n m : ℕ} (h : m = n) (k : Fin m), ↑((finCongr h) k) = ↑k
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_natAbs_smul : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E) (n : ℤ), ‖n.natAbs • a‖₊ = ‖n • a‖₊
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  {X : CategoryTheory.SimplicialObject A} (n : ℕ),
  (AlgebraicTopology.NormalizedMooreComplex.objX X n).Factors (AlgebraicTopology.DoldKan.PInfty.f n)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coconeOfIsSplitEpi_π : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y) [inst_1 : CategoryTheory.IsSplitEpi f],
  (CategoryTheory.Limits.coconeOfIsSplitEpi f).π = f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSignatureHelpContext : Lean.ToJson Lean.Lsp.SignatureHelpContext
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_nsmul : ∀ (n : ℕ) (x : ENNReal), ↑(n • x) = n • ↑x
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.instIsStableUnderShiftIntUpPlus : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  (HomotopyCategory.plus C).IsStableUnderShift ℤ
-- Mathlib.Topology.Connected.Basic
IsIrreducible.isConnected : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsIrreducible s → IsConnected s
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrTheorem.argKinds : Lean.Meta.CongrTheorem → Array Lean.Meta.CongrArgKind
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.instCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Mon.instCategory =
    { Hom := fun M N => M.Hom N, id := CategoryTheory.Mon.id, comp := fun {X Y Z} f g => CategoryTheory.Mon.comp f g,
      id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsColoop.isCocircuit : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsColoop e → M.IsCocircuit {e}
-- Lean.Meta.GetUnfoldableConst
Lean.Meta.canUnfold : Lean.ConstantInfo → Lean.MetaM Bool
-- Mathlib.Topology.Instances.ENat
/-- Topology on `ℕ∞`.

Note: this is different from the `EMetricSpace` topology. The `EMetricSpace` topology has
`IsOpen {∞}`, but all neighborhoods of `∞` in `ℕ∞` contain infinite intervals.
 -/
ENat.instTopologicalSpace : TopologicalSpace ℕ∞
-- Mathlib.GroupTheory.Congruence.Defs
/-- Coercion from a type with a multiplication to its quotient by a congruence relation.

See Note [use has_coe_t].  -/
Con.instCoeTCQuotient : {M : Type u_1} → [inst : Mul M] → (c : Con M) → CoeTC M c.Quotient
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The underlying object of `C`.  -/
CategoryTheory.PreGaloisCategory.PointedGaloisObject.obj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} → CategoryTheory.PreGaloisCategory.PointedGaloisObject F → C
-- Plausible.Sampleable
Plausible.SampleableExt.interp : {α : Sort u} → [self : Plausible.SampleableExt α] → Plausible.SampleableExt.proxy α → α
-- Mathlib.Tactic.CrossRefAttribute
/-- The `#kerodon_tags` command retrieves all declarations that have the `kerodon` attribute.

For each found declaration, it prints a line
```
'declaration_name' corresponds to tag 'declaration_tag'.
```
The variant `#kerodon_tags!` also adds the theorem statement (for theorems)
or declaration type (for definitions, structures, instances, etc.) after each summary line.
 -/
Mathlib.CrossRef.kerodonTags : Lean.ParserDescr
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig.mk : Array Aesop.Frontend.RuleExpr →
  Array Aesop.Frontend.RuleExpr →
    Std.HashSet Aesop.RuleSetName →
      Aesop.Options → Lean.Meta.Simp.Config → Option Lean.Term → Aesop.Frontend.TacticConfig
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.minKey? = some km → t.getKey? km = some km
-- Mathlib.Data.DFinsupp.Lex
/-- Auxiliary helper to case split computably. There is no need for this to be public, as it
can be written with `Or.by_cases` on `lt_trichotomy` once the instances below are constructed.  -/
_private.Mathlib.Data.DFinsupp.Lex.0.DFinsupp.lt_trichotomy_rec : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      [inst_1 : LinearOrder ι] →
        [inst_2 : (i : ι) → LinearOrder (α i)] →
          {P : Lex (Π₀ (i : ι), α i) → Lex (Π₀ (i : ι), α i) → Sort u_3} →
            ({f g : Π₀ (i : ι), α i} → toLex f < toLex g → P (toLex f) (toLex g)) →
              ({f g : Π₀ (i : ι), α i} → toLex f = toLex g → P (toLex f) (toLex g)) →
                ({f g : Π₀ (i : ι), α i} → toLex g < toLex f → P (toLex f) (toLex g)) →
                  (f g : Lex (Π₀ (i : ι), α i)) → P f g
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.inv_mul_cancel : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] (φ : MvPowerSeries σ k),
  MvPowerSeries.constantCoeff φ ≠ 0 → φ⁻¹ * φ = 1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.IsPath.ncard_neighborSet_toSubgraph_internal_eq_two : ∀ {V : Type u} {G : SimpleGraph V} {v u : V} {i : ℕ} {p : G.Walk u v},
  p.IsPath → i ≠ 0 → i < p.length → (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2
-- Mathlib.RingTheory.Ideal.Span
Ideal.mem_span_singleton_self : ∀ {α : Type u} [inst : Semiring α] (x : α), x ∈ Ideal.span {x}
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.ι_totalShift₁Iso_hom_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (a b n : ℤ) (h : a + b = n) (a' : ℤ) (ha' : a' = a + x) (n' : ℤ) (hn' : n' = n + x),
  CategoryTheory.CategoryStruct.comp
      (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).ιTotal (ComplexShape.up ℤ) a b n h)
      ((K.totalShift₁Iso x).hom.f n) =
    CategoryTheory.CategoryStruct.comp (K.shiftFunctor₁XXIso a x a' ha' b).hom
      (CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a' b n' ⋯)
        (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) x n n' hn').inv)
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.instPreservesFiniteCoproductsOfPreservesFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F],
  CategoryTheory.Limits.PreservesFiniteCoproducts F
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.mapQ_pow : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {f : M →ₗ[R] M} (h : p ≤ Submodule.comap f p) (k : ℕ) (h' : optParam (p ≤ Submodule.comap (f ^ k) p) ⋯),
  p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.lintegral_rnDeriv_lt_top_of_measure_ne_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (ν : MeasureTheory.Measure α) {s : Set α},
  μ s ≠ ⊤ → ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ⊤
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.Util.0.Int.Internal.Linear.Poly.isSorted.go : Option Int.Internal.Linear.Var → Int.Internal.Linear.Poly → Bool
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.halt : Turing.PartrecToTM2.Cont'
-- Mathlib.Order.CompleteBooleanAlgebra
compl_iInf : ∀ {α : Type u} {ι : Sort w} [inst : CompleteBooleanAlgebra α] {f : ι → α}, (iInf f)ᶜ = ⨆ i, (f i)ᶜ
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.MonoOver.bot_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.InitialMonoClass C] (X : C), ⊥.obj.left = ⊥_ C
-- Mathlib.Analysis.Normed.Group.Pointwise
closedBall_mul_singleton : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x y : E),
  Metric.closedBall x δ * {y} = Metric.closedBall (x * y) δ