mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.standardComplex.d_comp_ε : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G],
  CategoryTheory.CategoryStruct.comp ((Rep.standardComplex k G).d 1 0) (Rep.standardComplex.ε k G) = 0
-- Mathlib.Algebra.Category.MonCat.Basic
AddEquiv.toAddCommMonCatIso.eq_1 : ∀ {X Y : Type u} [inst : AddCommMonoid X] [inst_1 : AddCommMonoid Y] (e : X ≃+ Y),
  e.toAddCommMonCatIso =
    { hom := AddCommMonCat.ofHom e.toAddMonoidHom, inv := AddCommMonCat.ofHom e.symm.toAddMonoidHom, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_sub : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t : Finset α} {a : α},
  a ∈ s - t ↔ ∃ b ∈ s, ∃ c ∈ t, b - c = a
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_3_comp_chainsIso₃ : ∀ {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 →* H) (φ : A ⟶ Rep.res f B),
  CategoryTheory.CategoryStruct.comp ((groupHomology.chainsMap f φ).f 3) (groupHomology.chainsIso₃ B).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₃ A).hom (groupHomology.chainsMap₃ f φ)
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.tensor : ∀ {R : Type u_7} {S : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_9)
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (M : Submonoid R) [IsLocalization M A],
  IsLocalization (Algebra.algebraMapSubmonoid S M) (TensorProduct R S A)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- The pre-`1`-hypercover induced by a `PreOneHypercoverDenseData` structure.  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} → {X : C} → F.PreOneHypercoverDenseData X → CategoryTheory.PreOneHypercover X
-- Mathlib.Data.Set.Sups
Set.singleton_infs_singleton : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a b : α}, {a} ⊼ {b} = {a ⊓ b}
-- Init.Data.Float.Float
/-- Splits the given float `x` into a significand/exponent pair `(s, i)` such that `x = s * 2^i` where
`s ∈ (-1;-0.5] ∪ [0.5; 1)`. Returns an undefined value if `x` is not finite.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`frexp`.
 -/
Float.frExp : Float → Float × ℤ
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_inverse : ∀ {V : Type u'} [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {W : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} W] [inst_3 : CategoryTheory.MonoidalCategory W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.LaxMonoidal] (D : Type u) [inst_5 : CategoryTheory.EnrichedCategory V D]
  (e :
    (v : V) →
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v))
  (h :
    ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
      (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)),
  (CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv F D e h).inverse =
    CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse F D e h
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.equivalence.additive_inverse : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).inverse.Additive
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
/-- The adic ring filter basis associated to an ideal `I` is made of powers of `I`.  -/
Ideal.ringFilterBasis : {R : Type u_1} → [inst : CommRing R] → Ideal R → RingFilterBasis R
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Rep.FiniteCyclicGroup.groupHomologyIsoEven.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  [inst_3 : DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [h₀ : NeZero i] (hi : Even i),
  Rep.FiniteCyclicGroup.groupHomologyIsoEven A g hg i hi = Rep.FiniteCyclicGroup.groupHomologyIsoEven A g hg i hi
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.coe_comp : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Monoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (g : B →ₜ* C) (f : A →ₜ* B),
  ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsRegular.cof_ord : ∀ {c : Cardinal.{u_1}}, c.IsRegular → c.ord.cof = c
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- `G.killCopies H` has no effect on `G` if and only if `G` already contained no copies of `H`. See
`Free.killCopies_eq_left` for the reverse implication with no assumption on `H`.  -/
SimpleGraph.killCopies_eq_left : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}, H ≠ ⊥ → (G.killCopies H = G ↔ H.Free G)
-- Init.System.ST
instInhabitedST : {σ α : Type} → [Inhabited α] → Inhabited (ST σ α)
-- Lean.Server.Rpc.Basic
/-- Unique `RpcRef` for the ID of an object that is being referenced through RPC.
We store this mapping so that we can reuse `RpcRef`s for the same object.
Reusing `RpcRef`s is helpful because it enables clients to reuse their UI state.
 -/
Lean.Server.RpcObjectStore.refsById : Lean.Server.RpcObjectStore → Lean.PersistentHashMap USize Lean.Lsp.RpcRef
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.mul_prod_Iio_eq_prod_Iic : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] {f : α → M} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrderBot α] (a : α), f a * ∏ x < a, f x = ∏ x ≤ a, f x
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instFibrationOppositeOpOfCofibration : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.Cofibration f],
  HomotopicalAlgebra.Fibration f.op
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
/-- The isometry between two weighted sum of squares, give that each weight is scaled by the square
of a unit.  -/
QuadraticForm.isometryEquivWeightedSumSquaresWeightedSumSquares : {ι : Type u_10} →
  {S : Type u_11} →
    {R : Type u_12} →
      [inst : Fintype ι] →
        [inst_1 : CommSemiring R] →
          [inst_2 : Monoid S] →
            [inst_3 : DistribMulAction S R] →
              [inst_4 : SMulCommClass S R R] →
                [IsScalarTower S R R] →
                  {w w' : ι → S} →
                    (u : ι → Sˣ) →
                      (∀ (i : ι), w' i * ↑(u i) ^ 2 = w i) →
                        (QuadraticMap.weightedSumSquares R w).IsometryEquiv (QuadraticMap.weightedSumSquares R w')
-- Mathlib.Topology.MetricSpace.Bounded
tendsto_dist_right_cocompact_atTop : ∀ {α : Type u} [inst : PseudoMetricSpace α] [ProperSpace α] (x : α),
  Filter.Tendsto (fun x_1 => dist x_1 x) (Filter.cocompact α) Filter.atTop
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.appendCore.loop.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (i' : ℕ) → motive i'.succ),
  (match 0 with
    | 0 => h_1 ()
    | i'.succ => h_2 i') =
    h_1 ()
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_subset_sdiff_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} (u : Finset α), s ⊆ t → u \ t ⊆ u \ s
-- Mathlib.RingTheory.MvPolynomial.Ideal
MvPolynomial.C_mem_pow_idealOfVars_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (n : ℕ) (r : R),
  MvPolynomial.C r ∈ MvPolynomial.idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0
-- Mathlib.Order.RelIso.Basic
RelEmbedding.instCoeRelHom : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → Coe (r ↪r s) (r →r s)
-- Mathlib.Topology.Compactness.Lindelof
/-- The comap of the coLindelöf filter on `Y` by a continuous function `f : X → Y` is less than or
equal to the coLindelöf filter on `X`.
This is a reformulation of the fact that images of Lindelöf sets are Lindelöf.  -/
Filter.comap_coLindelof_le : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → Filter.comap f (Filter.coLindelof Y) ≤ Filter.coLindelof X
-- Mathlib.Topology.Algebra.Affine
eventually_homothety_mem_of_mem_interior : ∀ (R : Type u_1) {W : Type u_4} {Q : Type u_5} [inst : AddCommGroup W] [inst_1 : TopologicalSpace W]
  [inst_2 : AddTorsor W Q] [inst_3 : TopologicalSpace Q] [IsTopologicalAddTorsor Q] [inst_5 : CommRing R]
  [inst_6 : TopologicalSpace R] [inst_7 : Module R W] [ContinuousSMul R W] (x : Q) {s : Set Q} {y : Q},
  y ∈ interior s → ∀ᶠ (δ : R) in nhds 1, (AffineMap.homothety x δ) y ∈ s
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
/-- The rank of an isomorphism is `1`.  -/
AlgebraicGeometry.Scheme.Hom.finrank_eq_one_of_isIso : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f], AlgebraicGeometry.Scheme.Hom.finrank f = 1
-- Mathlib.Order.PiLex
Pi.instNoMaxOrderColexForallOfWellFoundedGTOfNonempty : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] [WellFoundedGT ι] [Nonempty ι]
  [inst_3 : (i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMaxOrder (β i)], NoMaxOrder (Colex ((i : ι) → β i))
-- Mathlib.Topology.Convenient.Category
/-- Constructor for objects in `ContinuousGeneratedByCat X`.  -/
ContinuousGeneratedByCat.of : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      (carrier : Type v) → [str : TopologicalSpace carrier] → ContinuousGeneratedByCat X
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.fromNondegComplex_toNondegComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.CategoryStruct.comp s.fromNondegComplex s.toNondegComplex =
    CategoryTheory.CategoryStruct.id s.nondegComplex
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.iterToSum_X : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (b : S₁),
  (MvPolynomial.iterToSum R S₁ S₂) (MvPolynomial.X b) = MvPolynomial.X (Sum.inl b)
-- Mathlib.RingTheory.Polynomial.Dickson
_private.Mathlib.RingTheory.Polynomial.Dickson.0.Polynomial.dickson.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match n.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_3 n
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.generateFrom_toPlots : ∀ {X : Type u_1} (d : DiffeologicalSpace X), DiffeologicalSpace.generateFrom d.toPlots = d
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] (f : α →Co β), f.comp (ContinuousOrderHom.id α) = f
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_hom_fac_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesLeftKanExtension F L] [inst_5 : L.HasLeftKanExtension F]
  {Z : CategoryTheory.Functor A D} (h : L.comp (L.leftKanExtension (F.comp G)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L.leftKanExtensionUnit F) G)
      (CategoryTheory.CategoryStruct.comp (L.associator (L.leftKanExtension F) G).hom
        (CategoryTheory.CategoryStruct.comp (L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).hom) h)) =
    CategoryTheory.CategoryStruct.comp (L.leftKanExtensionUnit (F.comp G)) h
-- Mathlib.GroupTheory.OrderOfElement
/-- The backward direction of `addOrderOf_eq_prime_iff`.  -/
addOrderOf_eq_prime : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)], p • x = 0 → x ≠ 0 → addOrderOf x = p
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `Pow` across an `Equiv`  -/
Equiv.pow : (M : Type u_1) → {α : Type u_2} → {β : Type u_3} → α ≃ β → [Pow β M] → Pow α M
-- Init.Meta.Defs
/-- Whether to support offset constraints such as `?x + 1 =?= e`  -/
Lean.Meta.Rewrite.Config.offsetCnstrs : Lean.Meta.Rewrite.Config → Bool
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_sdiff_left : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Ico a b \ {a} = Set.Ioo a b
-- Lean.Meta.InferType
Lean.Meta.throwTypeExpected : {α : Type} → Lean.Expr → Lean.MetaM α
-- Mathlib.Order.IsNormal
Order.isNormal_iff' : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] (f : α → β),
  Order.IsNormal f ↔ StrictMono f ∧ ∀ {a : α}, Order.IsSuccLimit a → f a ∈ lowerBounds (upperBounds (f '' Set.Iio a))
-- Mathlib.RingTheory.Localization.Free
/-- If `M` is a finitely presented `R`-module,
then any `Rₛ`-basis of `Mₛ` for some `S : Submonoid R` can be lifted to
a `Rᵣ`-basis of `Mᵣ` for some `r ∈ S`.
 -/
Module.FinitePresentation.exists_basis_localizedModule_powers : ∀ {R : Type u_4} {M : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submonoid R)
  {M' : Type u_1} [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') [inst_5 : IsLocalizedModule S f]
  (Rₛ : Type u_3) [inst_6 : CommRing Rₛ] [inst_7 : Algebra R Rₛ] [inst_8 : Module Rₛ M'] [IsScalarTower R Rₛ M']
  [IsLocalization S Rₛ] [Module.FinitePresentation R M] {I : Type u_6} [Finite I] (b : Module.Basis I Rₛ M'),
  ∃ r, ∃ (hr : r ∈ S), ∃ b', ∀ (i : I), (LocalizedModule.lift (Submonoid.powers r) f ⋯) (b' i) = b i
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.isFiniteMeasure_trim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
  [MeasureTheory.IsFiniteMeasure μ], MeasureTheory.IsFiniteMeasure (μ.trim hm)
-- Mathlib.Analysis.InnerProductSpace.Basic
_private.Mathlib.Analysis.InnerProductSpace.Basic.0.«term⟪_,_⟫_1» : Lean.ParserDescr
-- Mathlib.Topology.AlexandrovDiscrete
Finite.toAlexandrovDiscrete : ∀ {α : Type u_3} [inst : TopologicalSpace α] [Finite α], AlexandrovDiscrete α
-- Std.Async.System
Std.Async.System.SystemUser.mk : String →
  Option Std.Async.System.UserId →
    Option Std.Async.System.GroupId → Option String → Option System.FilePath → Std.Async.System.SystemUser
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.entries.inj : ∀ {α : Type u} {β : Type v} {es es_1 : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))},
  Lean.PersistentHashMap.Node.entries es = Lean.PersistentHashMap.Node.entries es_1 → es = es_1
-- Batteries.Tactic.GeneralizeProofs
/-- Abstract proofs occurring in the expression.
A proof is *abstracted* if it is of the form `f a b ...` where `a b ...` are bound variables
(that is, they are variables that are not present in the initial local context)
and where `f` contains no bound variables.
In this form, `f` can be immediately lifted to be a local variable and generalized.
The abstracted proofs are recorded in the state.

This function is careful to track the type of `e` based on where it's used,
since the inferred type might be different.
For example, `(by simp : 1 < [1, 2].length)` has `1 < Nat.succ 1` as the inferred type,
but from knowing it's an argument to `List.nthLe` we can deduce `1 < [1, 2].length`.
 -/
Batteries.Tactic.GeneralizeProofs.abstractProofs : Lean.Expr → Option Lean.Expr → Batteries.Tactic.GeneralizeProofs.MAbs Lean.Expr
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.zero.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} [inst_1 : SizeOf J],
  sizeOf RingCat.Colimits.Prequotient.zero = 1
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.mk.inj : ∀ {views : Array Lean.Elab.Command.InductiveView} {elabs' : Array Lean.Elab.Command.InductiveElabStep2}
  {indFVars vars : Array Lean.Expr} {levelParams : List Lean.Name} {numVars numParams : ℕ}
  {indTypes : List Lean.InductiveType} {isUnsafe : Bool} {rs : Array Lean.Elab.Command.ElabHeaderResult}
  {params : Array Lean.Expr} {isCoinductive : Bool} {views_1 : Array Lean.Elab.Command.InductiveView}
  {elabs'_1 : Array Lean.Elab.Command.InductiveElabStep2} {indFVars_1 vars_1 : Array Lean.Expr}
  {levelParams_1 : List Lean.Name} {numVars_1 numParams_1 : ℕ} {indTypes_1 : List Lean.InductiveType}
  {isUnsafe_1 : Bool} {rs_1 : Array Lean.Elab.Command.ElabHeaderResult} {params_1 : Array Lean.Expr}
  {isCoinductive_1 : Bool},
  { views := views, elabs' := elabs', indFVars := indFVars, vars := vars, levelParams := levelParams,
        numVars := numVars, numParams := numParams, indTypes := indTypes, isUnsafe := isUnsafe, rs := rs,
        params := params, isCoinductive := isCoinductive } =
      { views := views_1, elabs' := elabs'_1, indFVars := indFVars_1, vars := vars_1, levelParams := levelParams_1,
        numVars := numVars_1, numParams := numParams_1, indTypes := indTypes_1, isUnsafe := isUnsafe_1, rs := rs_1,
        params := params_1, isCoinductive := isCoinductive_1 } →
    views = views_1 ∧
      elabs' = elabs'_1 ∧
        indFVars = indFVars_1 ∧
          vars = vars_1 ∧
            levelParams = levelParams_1 ∧
              numVars = numVars_1 ∧
                numParams = numParams_1 ∧
                  indTypes = indTypes_1 ∧
                    isUnsafe = isUnsafe_1 ∧ rs = rs_1 ∧ params = params_1 ∧ isCoinductive = isCoinductive_1
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.toSubsemiring_injective : ∀ {R : Type u_1} [inst : CommRing R], Function.Injective RingPreordering.toSubsemiring
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro
/-- Given a projective resolution `P` of `k` as a `k`-linear `G`-representation, a subgroup
`S ≤ G`, and a `k`-linear `S`-representation `A`, this is an isomorphism of complexes
`Hom(Res(S)(P), A) ≅ Hom(P, Coind_S^G(A)).`  -/
groupCohomology.linearYonedaObjResProjectiveResolutionIso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {S : Subgroup G} →
        (P : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)) →
          (A : Rep.{u, u, u} k ↥S) →
            ((Rep.resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A ≅
              P.complex.linearYonedaObj k (Rep.coind.{u, u, u, u} S.subtype A)
-- Mathlib.RingTheory.PowerSeries.Substitution
Polynomial.toPowerSeries_toMvPowerSeries : ∀ {R : Type u_2} [inst : CommRing R] (p : Polynomial R), ↑p = ↑((Polynomial.aeval (MvPolynomial.X ())) p)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
normEDS_four : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), normEDS b c d 4 = d * b
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- This is `Orthonormal.isHilbertSum` in the case of actual inclusions from subspaces.  -/
IsHilbertSum.mkInternal : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] (F : ι → Submodule 𝕜 E) [∀ (i : ι), CompleteSpace ↥(F i)],
  (OrthogonalFamily 𝕜 (fun i => ↥(F i)) fun i => (F i).subtypeₗᵢ) →
    ⊤ ≤ (⨆ i, F i).topologicalClosure → IsHilbertSum 𝕜 (fun i => ↥(F i)) fun i => (F i).subtypeₗᵢ
-- Mathlib.Algebra.CharP.Two
CharTwo.add_self_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] [CharP R 2] (x : R), x + x = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp] {k : α}, k ∉ t₁ → (t₁ ∪ t₂).getKey! k = t₂.getKey! k
-- Mathlib.Topology.MetricSpace.IsometricSMul
isometry_mul_right : ∀ {M : Type u} [inst : Mul M] [inst_1 : PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a : M), Isometry fun x => x * a
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.ofFun_div : ∀ {α : Type u_1} {β : Type u_2} [inst : Div β] (f g : α → β),
  UniformFun.ofFun (f / g) = UniformFun.ofFun f / UniformFun.ofFun g
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.condIndep_limsup_atTop_self : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] [inst_3 : StandardBorelSpace Ω] (hm : m ≤ m0)
  [inst_4 : MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iCondIndep m hm s μ →
      ProbabilityTheory.CondIndep m (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) hm μ
-- Init.Data.Nat.Basic
Nat.instAntisymmLe : Std.Antisymm fun x1 x2 => x1 ≤ x2
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.val_compl : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} (a : ↥L), ↑aᶜ = (↑a)ᶜ
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Poly.denote.match_1.splitter : (motive : Nat.Internal.Linear.Poly → Sort u_1) →
  (p : Nat.Internal.Linear.Poly) →
    (Unit → motive []) →
      ((k : ℕ) → (v : Nat.Internal.Linear.Var) → (p : List (ℕ × Nat.Internal.Linear.Var)) → motive ((k, v) :: p)) →
        motive p
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_erase : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF →
    ∀ {k a : α},
      Std.DHashMap.Raw.Const.get! (m.erase k) a = if (k == a) = true then default else Std.DHashMap.Raw.Const.get! m a
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- The stalk of `Proj A` at `x` is the degree `0` part of the localization of `A` at `x`.  -/
AlgebraicGeometry.Proj.stalkIso : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (x : ↥(AlgebraicGeometry.Proj 𝒜)) →
                (AlgebraicGeometry.Proj 𝒜).presheaf.stalk x ≅
                  CommRingCat.of (HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.Selector : Type
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.map_toSubring : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Nontrivial S] (f : R →+* S)
  (s : LocalSubring R), (LocalSubring.map f s).toSubring = Subring.map f s.toSubring
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
/-- A mutually inductive group, identified by the `all` array of the `InductiveVal` of its
constituents.
 -/
Lean.Elab.Structural.IndGroupInfo : Type
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.toArray_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  {f : (a : α) → β a → Option (γ a)},
  t.WF →
    (Std.DTreeMap.Raw.filterMap f t).toArray =
      Array.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toArray
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertNumber : Std.Time.Number → Lean.MacroM (Lean.TSyntax `term)
-- Init.Data.List.Impl
/-- Replaces the value at (zero-based) index `n` in `l` with `a`. If the index is out of bounds, then
the list is returned unmodified.

This is a tail-recursive version of `List.set` that's used at runtime.

Examples:
* `["water", "coffee", "soda", "juice"].set 1 "tea" = ["water", "tea", "soda", "juice"]`
* `["water", "coffee", "soda", "juice"].set 4 "tea" = ["water", "coffee", "soda", "juice"]`
 -/
List.setTR : {α : Type u_1} → List α → ℕ → α → List α