mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.map_congr : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} {f g : G →* H} {φ : A ⟶ Rep.res f B} {ψ : A ⟶ Rep.res g B},
  f = g →
    (Rep.Hom.hom φ).toLinearMap = (Rep.Hom.hom ψ).toLinearMap →
      ∀ (n : ℕ), groupHomology.map f φ n = groupHomology.map g ψ n
-- Mathlib.LinearAlgebra.Matrix.Action
Matrix.instModuleMulOppositeForall : {n : Type u_1} →
  {R : Type u_2} →
    [inst : Fintype n] → [inst_1 : DecidableEq n] → [inst_2 : Semiring R] → Module (Matrix n n R)ᵐᵒᵖ (n → R)
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientWithinAt_const : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (x : F) (s : Set F) (c : 𝕜), HasGradientWithinAt (fun x => c) 0 s x
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries.map : ∀ {G : Type u_1} [inst : Group G] {K : Type u_2} [inst_1 : Group K] (f : G →* K) (n : ℕ),
  Subgroup.map f (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Summable.tendsto_zero_of_even_summable_symmetricIcc : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [NormSMulClass ℤ F] {f : ℤ → F},
  Summable f (SummationFilter.symmetricIcc ℤ) → Function.Even f → Filter.Tendsto f Filter.atTop (nhds 0)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
SSet.Subcomplex.PairingCore.isRegular_iff_nonempty_weakRankFunction : ∀ {X : SSet} {A : X.Subcomplex} (P : A.PairingCore) [P.IsProper], P.IsRegular ↔ Nonempty (P.WeakRankFunction ℕ)
-- Mathlib.Tactic.ModCases
/-- `OnModCases n a lb p` represents a partial proof by cases that
there exists `0 ≤ z < n` such that `a ≡ z (mod n)`.
It asserts that if `∃ z, lb ≤ z < n ∧ a ≡ z (mod n)` holds, then `p`
(where `p` is the current goal).
 -/
Mathlib.Tactic.ModCases.IntMod.OnModCases : ℕ → ℤ → ℕ → Sort u_1 → Sort u_1
-- Init.System.IO
IO.Process.Output.mk.inj : ∀ {exitCode : UInt32} {stdout stderr : String} {exitCode_1 : UInt32} {stdout_1 stderr_1 : String},
  { exitCode := exitCode, stdout := stdout, stderr := stderr } =
      { exitCode := exitCode_1, stdout := stdout_1, stderr := stderr_1 } →
    exitCode = exitCode_1 ∧ stdout = stdout_1 ∧ stderr = stderr_1
-- Init.Data.Array.Lemmas
Array.getElem?_eq_some_getElem_iff : ∀ {α : Type u_1} (xs : Array α) (i : ℕ) (h : i < xs.size), xs[i]? = some xs[i] ↔ True
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.limitAddMonoid.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections],
  AddMonCat.limitAddMonoid F =
    {
      add := fun x y =>
        (equivShrink ↑(F.comp (CategoryTheory.forget AddMonCat)).sections).symm.invFun
          ((equivShrink ↑(F.comp (CategoryTheory.forget AddMonCat)).sections).symm.toFun x +
            (equivShrink ↑(F.comp (CategoryTheory.forget AddMonCat)).sections).symm.toFun y),
      add_assoc := ⋯, zero := (equivShrink ↑(F.comp (CategoryTheory.forget AddMonCat)).sections).symm.invFun 0,
      zero_add := ⋯, add_zero := ⋯, nsmul := fun n x => n • x, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.Data.Finset.Lattice.Fold
/-- A version of `Finset.inf'_map` with LHS and RHS reversed.
Also, this lemma assumes that `s` is nonempty instead of assuming that its image is nonempty.  -/
Finset.inf'_comp_eq_map : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] {s : Finset γ} {f : γ ↪ β} (g : β → α)
  (hs : s.Nonempty), s.inf' hs (g ∘ ⇑f) = (Finset.map f s).inf' ⋯ g
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
/-- This is the `n+1`st coefficient of our inverse.  -/
WittVector.succNthValUnits : {p : ℕ} →
  [hp : Fact (Nat.Prime p)] →
    {k : Type u_1} → [inst : CommRing k] → [CharP k p] → (n : ℕ) → kˣ → WittVector p k → (Fin (n + 1) → k) → k
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.finite : ∀ {α : Type u_1} {N M : Matroid α} [M.Finite], N.IsRestriction M → N.Finite
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.fix.injEq : ∀ (a : Turing.ToPartrec.Code) (a_1 : Turing.ToPartrec.Cont) (a_2 : Turing.ToPartrec.Code) (a_3 : Turing.ToPartrec.Cont),
  (Turing.ToPartrec.Cont.fix a a_1 = Turing.ToPartrec.Cont.fix a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.pair_preimage : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β)
  (g : MeasureTheory.SimpleFunc α γ) (s : Set β) (t : Set γ), ⇑(f.pair g) ⁻¹' s ×ˢ t = ⇑f ⁻¹' s ∩ ⇑g ⁻¹' t
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Dᵒᵖ A} (g : P ⟶ Q)
  (X : C) (x : Φ.fiber.obj X),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiberMap F K P X x) ((Φ.map F K).presheafFiber.map g) =
    CategoryTheory.CategoryStruct.comp (g.app (Opposite.op (F.obj X))) (Φ.toPresheafFiberMap F K Q X x)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformly.hasSumUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α], HasSumUniformly f g → HasSumUniformlyOn f g s
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.mk.injEq : ∀ {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]
  (functor functor_1 : CategoryTheory.Functor C V),
  ({ functor := functor } = { functor := functor_1 }) = (functor = functor_1)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- The set of fixed points of a normal subgroup is stable under the group action.  -/
fixedPointsSubMulOfNormal : {G : Type u_1} →
  [inst : Group G] → {α : Type u_2} → [inst_1 : MulAction G α] → {H : Subgroup G} → [hH : H.Normal] → SubMulAction G α
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.card_factors_of_irreducible : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α},
  Irreducible a → (UniqueFactorizationMonoid.factors a).card = 1
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.nodup_toCycle : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (f : Equiv.Perm α) (hf : f.IsCycle), (f.toCycle hf).Nodup
-- Mathlib.Computability.Partrec
/-- Computable functions `α → σ` between `Primcodable` types:
a function is computable if and only if it is partially recursive (as a partial function)  -/
Computable : {α : Type u_1} → {σ : Type u_2} → [Primcodable α] → [Primcodable σ] → (α → σ) → Prop
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap_id : ∀ {α : Type u_1} (x : Option α), (Std.Internal.List.Option.dmap✝ x fun a x => a) = x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k : α} {fallback : β k},
  (List.map Sigma.fst l).contains k = false → (m.insertMany l).getD k fallback = m.getD k fallback
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_mk : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (x : G) (hx : x ∈ H), ↑⟨x, hx⟩ = x
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivWithinAt.scomp_hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {s' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F},
  HasDerivWithinAt g₁ g₁' s' (h x) → HasDerivAt h h' x → (∀ (x : 𝕜), h x ∈ s') → HasDerivAt (g₁ ∘ h) (h' • g₁') x
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
/-- Any linearly ordered abelian group that is locally finite embeds to `Multiplicative ℤ`.  -/
LocallyFiniteOrder.orderMonoidEquiv : (G : Type u_3) →
  [inst : CommGroup G] →
    [inst_1 : LinearOrder G] → [IsOrderedMonoid G] → [LocallyFiniteOrder G] → [Nontrivial G] → G ≃*o Multiplicative ℤ
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find a model with corners on a Euclidean space, half-space or quadrant  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromEuclideanSpace : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Group.Center
Set.invOf_mem_center : ∀ {M : Type u_1} [inst : Monoid M] {a : M} [inst_1 : Invertible a], a ∈ Set.center M → ⅟a ∈ Set.center M
-- Mathlib.Data.Nat.Factorial.Basic
/-- `descFactorial` implemented using binary splitting.  -/
Nat.descFactorialBinary : ℕ → ℕ → ℕ
-- Mathlib.Analysis.Complex.Circle
Circle.normSq_coe : ∀ (z : Circle), Complex.normSq ↑z = 1
-- Init.Data.SInt.Lemmas
Int16.toInt64_ofIntLE : ∀ {n : ℤ} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt),
  (Int16.ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n ⋯ ⋯
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup contains the group's 1.  -/
Subgroup.one_mem : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), 1 ∈ H
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.op_pushoutMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z S T : C} (f₁ : S ⟶ W) (f₂ : S ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPushout f₁ f₂] (g₁ : T ⟶ Y) (g₂ : T ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPushout g₁ g₂] (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T)
  (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₁ = CategoryTheory.CategoryStruct.comp i₃ g₁)
  (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₂ = CategoryTheory.CategoryStruct.comp i₃ g₂),
  (CategoryTheory.Limits.pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoOpPushout g₁.op g₂.op).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯)
        (CategoryTheory.Limits.pullbackIsoOpPushout f₁.op f₂.op).hom)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasProd_mono : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α},
  HasProd f a₁ L → HasProd g a₂ L → f ≤ g → ∀ [L.NeBot], a₁ ≤ a₂
-- Mathlib.Topology.Algebra.Monoid.Defs
continuous_mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M], Continuous fun p => p.1 * p.2
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.isCycleOn_empty : ∀ {α : Type u_2} {f : Equiv.Perm α}, f.IsCycleOn ∅
-- Batteries.Data.List.Perm
List.erase_cons_subperm_cons_erase : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a b : α) (l : List α), ((a :: l).erase b).Subperm (a :: l.erase b)
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
RingOfIntegers.exponent_eq_sInf : ∀ {K : Type u_1} [inst : Field K] {θ : NumberField.RingOfIntegers K},
  RingOfIntegers.exponent θ = sInf {d | 0 < d ∧ ↑d ∈ conductor ℤ θ}
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b}
  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (F.obj a)) (F.map f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (F.map f)) h =
    CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv
      (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv h))
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableDiv₂_of_add_neg : ∀ (G : Type u_2) [inst : MeasurableSpace G] [inst_1 : SubNegMonoid G] [MeasurableAdd₂ G] [MeasurableNeg G],
  MeasurableSub₂ G
-- Mathlib.Algebra.Category.Grp.Limits
/-- The category of additive commutative groups has all limits.  -/
AddCommGrpCat.hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} AddCommGrpCat
-- Lean.ResolveName
/-- Check `OpenDecl`s  -/
_private.Lean.ResolveName.0.Lean.ResolveName.resolveOpenDecls : Lean.Environment → Lean.Options → Lean.Name → List Lean.OpenDecl → List Lean.Name → List Lean.Name
-- Init.Data.Range.Polymorphic.PRange
Std.Ric.instDecidableMemOfDecidableLE : {α : Type u} → {r : Std.Ric α} → {a : α} → [inst : LE α] → [DecidableLE α] → Decidable (a ∈ r)
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.piIsoPi_inv_π_assoc : ∀ {ι : Type v} (α : ι → TopCat) (i : ι) {Z : TopCat} (h : α i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (TopCat.piIsoPi α).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π α i) h) =
    CategoryTheory.CategoryStruct.comp (TopCat.piπ α i) h
-- Mathlib.Data.Finsupp.Notation
Finsupp.fun₀.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Setoid.Basic
Setoid.comap_map_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (r : Setoid α), Function.Injective f → Setoid.comap f (r.map f) = r
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddAbove.add : ∀ {M : Type u_3} [inst : Add M] [inst_1 : Preorder M] [AddLeftMono M] [AddRightMono M] {s t : Set M},
  BddAbove s → BddAbove t → BddAbove (s + t)
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.isNNRat_eq_rawCast : ∀ {R : Type u_1} {A : Type u_2} [inst : Semifield R] [inst_1 : Semifield A] [inst_2 : Algebra R A] {a : A} {n d : ℕ},
  Mathlib.Meta.NormNum.IsNNRat a n d → a = (algebraMap R A) (NNRat.rawCast n d + 0) + 0
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- Any non-trivial linearly ordered mul-archimedean group is either cyclic, or densely ordered,
exclusively.  -/
LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] [Nontrivial G],
  IsCyclic G ↔ ¬DenselyOrdered G
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.isScalarTower_of_injective : ∀ {M : Type u_8} {M₂ : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] (R : Type u_14) {S : Type u_15}
  [inst_2 : Semiring S] [inst_3 : SMul R M] [inst_4 : Module S M] [inst_5 : SMul R M₂] [inst_6 : Module S M₂]
  [inst_7 : SMul R S] [LinearMap.CompatibleSMul M M₂ R S] [IsScalarTower R S M₂] (f : M →ₗ[S] M₂),
  Function.Injective ⇑f → IsScalarTower R S M
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
isMIntegralCurve_comp_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {dt : ℝ}, IsMIntegralCurve (γ ∘ fun x => x + dt) v ↔ IsMIntegralCurve γ v
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.mapRingEquiv_apply : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] (e : K ≃+* L) (x : NumberField.RingOfIntegers K),
  ↑((NumberField.RingOfIntegers.mapRingEquiv e) x) = e ↑x
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- For every nonzero ideal `I` of `v`, there are finitely many maximal ideals `v` such that
`v^(val_v(I))` is not the unit ideal.  -/
Ideal.hasFiniteMulSupport : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R},
  I ≠ 0 → Function.HasFiniteMulSupport fun v => v.maxPowDividing I
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.aleph_univ : Cardinal.aleph Ordinal.univ.{u, v} = Cardinal.univ.{u, v}
-- Lean.Linter.Util
/-- Get the names of declarations introduced by elaborating `t`.

A declaration introduces a `TermInfo` with `isBinder := true` whose `expr` is the constant
being declared. This covers `def`/`theorem`/`axiom`, inductive types and their constructors,
and structure fields and parent projections — including mutual blocks where each member
emits its own binder.
 -/
Lean.Linter.getNewDecls : Lean.Elab.InfoTree → List Lean.Name
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_neg_Ioo : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  Neg.neg '' Set.Ioo a b = Set.Ioo (-b) (-a)
-- Mathlib.Data.Set.SMulAntidiagonal
Set.VAddAntidiagonal.eq_of_fst_eq_fst : ∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [inst : VAdd G P] {x y : ↑(s.vaddAntidiagonal t a)}
  [IsLeftCancelVAdd G P], (↑x).1 = (↑y).1 → x = y
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.add_smul : ∀ {R : Type u_1} {R'' : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring R''] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R'' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : SMulCommClass R R'' M] (r s : R'') (x : TensorProduct R M N),
  (r + s) • x = r • x + s • x
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.state : {α : Type} → Std.Bounded✝ α → Std.Mutex (Std.Bounded.State✝ α)
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- A root datum is a root pairing with coefficients in the integers and for which the root and
coroot spaces are finitely-generated free Abelian groups.

Note that the latter assumptions `[Finite ℤ X₁] [Finite ℤ X₂]` should be supplied as mixins, and
that freeness follows automatically since two finitely-generated Abelian groups in perfect pairing
are necessarily free. Moreover Lean knows this, e.g., via `PerfectPairing.reflexive_left`,
`IsReflexive.to_isTorsionFree`, `Module.free_of_finite_type_torsion_free'`.  -/
RootDatum : Type u_1 →
  (X₁ : Type u_5) → (X₂ : Type u_6) → [AddCommGroup X₁] → [AddCommGroup X₂] → Type (max (max (max u_1 0) u_5) u_6)
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluing_t : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j : 𝒰.I₀), (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).t i j = AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.annotateCurPos : Lean.Term → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Data.Seq.Computation
Computation.eq_of_pure_mem : ∀ {α : Type u} {a a' : α}, a' ∈ Computation.pure a → a' = a
-- Std.Data.Internal.List.Associative
Std.Internal.List.foldlM_eq_foldlM_toProd : ∀ {α : Type u} {β : Type v} {δ : Type w} {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m']
  {l : List ((_ : α) × β)} {f : δ → α → β → m' δ} {init : δ},
  List.foldlM (fun a b => f a b.fst b.snd) init l =
    List.foldlM (fun a b => f a b.1 b.2) init (List.map (fun x => (x.fst, x.snd)) l)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.map_Φ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ),
  (W.map f).Φ n = Polynomial.map f (W.Φ n)
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.lratProofToBinary.startDelete : ByteArray → ByteArray
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Supported predicates on `BVExpr`.
 -/
Std.Tactic.BVDecide.BVPred : Type
-- Mathlib.CategoryTheory.Category.RelCat
/-- The category of types with binary relations as morphisms.  -/
CategoryTheory.RelCat.instLargeCategory : CategoryTheory.LargeCategory CategoryTheory.RelCat
-- Mathlib.RepresentationTheory.Maschke
/-- In fact, the sum over `g : G` of the conjugate of `π` by `g` is a `k[G]`-linear map.
 -/
LinearMap.sumOfConjugatesEquivariant : {k : Type u_1} →
  [inst : CommRing k] →
    (G : Type u_2) →
      [inst_1 : Group G] →
        {V : Type u_3} →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              [inst_4 : Module (MonoidAlgebra k G) V] →
                [IsScalarTower k (MonoidAlgebra k G) V] →
                  {W : Type u_4} →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : Module k W] →
                        [inst_8 : Module (MonoidAlgebra k G) W] →
                          [IsScalarTower k (MonoidAlgebra k G) W] →
                            (W →ₗ[k] V) → [Fintype G] → W →ₗ[MonoidAlgebra k G] V
-- Mathlib.RingTheory.PolynomialLaw.Basic
_private.Mathlib.RingTheory.PolynomialLaw.Basic.0.PolynomialLaw.π.match_1.splitter : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_3) →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (S : Type u_2) →
            (motive : PolynomialLaw.lifts R M S → Sort u_4) →
              (x : PolynomialLaw.lifts R M S) →
                ((s : Finset S) → (p : TensorProduct R (MvPolynomial (Fin s.card) R) M) → motive ⟨s, p⟩) → motive x
-- Mathlib.Order.Filter.Prod
Filter.Tendsto.prodMap_coprod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {f : α → γ} {g : β → δ} {a : Filter α} {b : Filter β}
  {c : Filter γ} {d : Filter δ},
  Filter.Tendsto f a c → Filter.Tendsto g b d → Filter.Tendsto (Prod.map f g) (a.coprod b) (c.coprod d)
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- We can define an additive character on `ZMod n` when we have an `n`th root of unity `ζ : C`.  -/
AddChar.zmodChar : {C : Type v} → [inst : CommMonoid C] → (n : ℕ) → [NeZero n] → {ζ : C} → ζ ^ n = 1 → AddChar (ZMod n) C
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Ioc_succ_left_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] {a b : α},
  a < b → insert (Order.succ a) (Finset.Ioc (Order.succ a) b) = Finset.Ioc a b
-- Lean.Elab.Command
Lean.Elab.Command.mkState : Lean.Environment → optParam Lean.MessageLog { } → optParam Lean.Options ∅ → Lean.Elab.Command.State
-- Mathlib.LinearAlgebra.Complex.Module
realPart_imaginaryPart : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  {x : A}, realPart ↑(imaginaryPart x) = imaginaryPart x
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- **Alias** of the reverse direction of `hasDerivAtFilter_const_add_iff`. -/
HasDerivAtFilter.const_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)} (c : F),
  HasDerivAtFilter f f' L → HasDerivAtFilter (fun x => c + f x) f' L
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.mk.injEq : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (map : X ⟶ Y)
  (comm :
    autoParam (CategoryTheory.CategoryStruct.comp A.ι map = CategoryTheory.CategoryStruct.comp φ B.ι)
      SSet.RelativeMorphism.comm._autoParam)
  (map_1 : X ⟶ Y)
  (comm_1 :
    autoParam (CategoryTheory.CategoryStruct.comp A.ι map_1 = CategoryTheory.CategoryStruct.comp φ B.ι)
      SSet.RelativeMorphism.comm._autoParam),
  ({ map := map, comm := comm } = { map := map_1, comm := comm_1 }) = (map = map_1)
-- Mathlib.Topology.Spectral.Hom
/-- statement that `F` is a type of spectral maps  -/
SpectralMapClass.map_spectral : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : TopologicalSpace α} {inst_1 : TopologicalSpace β}
  {inst_2 : FunLike F α β} [self : SpectralMapClass F α β] (f : F), IsSpectralMap ⇑f