mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.all_eq_true_iff_forall_mem_getElem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {p : α → β → Bool},
  m.all p = true ↔ ∀ (a : α) (h : a ∈ m), p a m[a] = true
-- Batteries.Data.List.Perm
List.Subperm.cons_right : ∀ {α : Type u_1} {l l' : List α} (x : α), l.Subperm l' → l.Subperm (x :: l')
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- **Alias** of `PowerSeries.weierstrassDiv_zero_left`. -/
PowerSeries.zero_weierstrassDiv : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (g : PowerSeries A)
  [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A], 0 /ʷ g = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → (↑m).keys.isEmpty = (↑m).isEmpty
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (m.insertMany l).getD k' fallback = cast ⋯ v
-- Mathlib.GroupTheory.Sylow
Sylow.ext : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {P Q : Sylow p G}, ↑P = ↑Q → P = Q
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Function.locallyFinsuppWithin.toClosedBall_divisor : ∀ {r : ℝ} {f : ℂ → ℂ},
  Meromorphic f →
    MeromorphicOn.divisor f (Metric.closedBall 0 |r|) =
      (Function.locallyFinsuppWithin.toClosedBall r) (MeromorphicOn.divisor f Set.univ)
-- Mathlib.Algebra.Category.ModuleCat.Localization
ModuleCat.instPreservesFiniteColimitsLocalizationLocalizedModuleFunctor : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (S : Submonoid R),
  CategoryTheory.Limits.PreservesFiniteColimits (ModuleCat.localizedModuleFunctor S)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `right` co(ntra)variant.  -/
Right.inv_le_one_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a : α}, a⁻¹ ≤ 1 ↔ 1 ≤ a
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.zero_add : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.zero.add x) x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [Inhabited α] (h : t.WF) {k k' : α} {f : Option β → Option β} {hc : k' ∈ t.alter k f},
  (t.alter k f).getKey k' hc = if heq : cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
/-- The bilinear forms agree across the map.  -/
LinearMap.BilinForm.Isometry.map_app' : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} (self : B₁ →bᵢ B₂) (m m' : M₁), (B₂ (self.toFun m)) (self.toFun m') = (B₁ m) m'
-- Mathlib.CategoryTheory.Adjunction.Restrict
/-- If `C` is a full subcategory of `C'` and `D` is a full subcategory of `D'`, then we can restrict
an adjunction `L' ⊣ R'` where `L' : C' ⥤ D'` and `R' : D' ⥤ C'` to `C` and `D`.
The construction here is slightly more general, in that `C` is required only to have a full and
faithful "inclusion" functor `iC : C ⥤ C'` (and similarly `iD : D ⥤ D'`) which commute (up to
natural isomorphism) with the proposed restrictions.
 -/
CategoryTheory.Adjunction.restrictFullyFaithful : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C' : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] →
            {D' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] →
                {iC : CategoryTheory.Functor C C'} →
                  {iD : CategoryTheory.Functor D D'} →
                    {L' : CategoryTheory.Functor C' D'} →
                      {R' : CategoryTheory.Functor D' C'} →
                        (L' ⊣ R') →
                          iC.FullyFaithful →
                            iD.FullyFaithful →
                              {L : CategoryTheory.Functor C D} →
                                {R : CategoryTheory.Functor D C} →
                                  (iC.comp L' ≅ L.comp iD) → (iD.comp R' ≅ R.comp iC) → (L ⊣ R)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.gc_homogeneousIdeal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜],
  GaloisConnection (fun I => ProjectiveSpectrum.zeroLocus 𝒜 ↑I) fun t => ProjectiveSpectrum.vanishingIdeal t
-- Mathlib.Order.Filter.Finite
Filter.exists_iInter_of_mem_iInf : ∀ {ι : Sort u_2} {α : Type u_3} {f : ι → Filter α} {s : Set α},
  s ∈ ⨅ i, f i → ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i
-- Init.Data.String.Search
String.revPosOf : String → Char → Option String.Pos.Raw
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) (a b : ℤ) (h : a ≤ b) (X : C) {Z : C} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.natTransTruncLTOfLE a b h).app X)
      (CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) h_1) =
    CategoryTheory.CategoryStruct.comp ((t.truncLTι a).app X) h_1
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.Fibration.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C],
  HomotopicalAlgebra.fibrations C f → HomotopicalAlgebra.Fibration f
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.IsStarNormal.adjoint_apply_eq_zero_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E} [inst_3 : CompleteSpace E],
  IsStarNormal T → ∀ (x : E), (ContinuousLinearMap.adjoint T) x = 0 ↔ T x = 0
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ComputedFieldView : Type
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Over.instHasFiniteCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Limits.HasFiniteCoproducts (CategoryTheory.Over X)
-- Mathlib.Order.Partition.Finpartition
Finpartition.parts_top_subset : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] (a : α) [inst_2 : Decidable (a = ⊥)], ⊤.parts ⊆ {a}
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
/-- The identity span, where both legs are identity morphisms.  -/
CategoryTheory.Span.id : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} →
      [Wₗ.ContainsIdentities] → [Wᵣ.ContainsIdentities] → (c : C) → CategoryTheory.Span Wₗ Wᵣ c c
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
/-- The triangle in `CochainComplex C ℤ` attached to a degreewise split short exact sequence
of cochain complexes.  -/
CochainComplex.triangleOfDegreewiseSplit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) →
        ((n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) →
          CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.instCountableOrCountablyGeneratedProd : ∀ {β : Type u_2} {α : Type u_3} {γ : Type u_4} [inst : MeasurableSpace γ]
  [hα : MeasurableSpace.CountableOrCountablyGenerated α γ] [hβ : MeasurableSpace.CountableOrCountablyGenerated β γ],
  MeasurableSpace.CountableOrCountablyGenerated (α × β) γ
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.closure_union : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s t : Set R),
  NonUnitalSubring.closure (s ∪ t) = NonUnitalSubring.closure s ⊔ NonUnitalSubring.closure t
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
/-- Given `P : ObjectProperty C`, this is the equivalence between `P.op.FullSubcategory`
and `P.FullSubcategoryᵒᵖ`.  -/
CategoryTheory.ObjectProperty.opEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.ObjectProperty C) → P.op.FullSubcategory ≌ P.FullSubcategoryᵒᵖ
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_re : ∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6} [inst_1 : RCLike 𝕜]
  {f : X → 𝕜}, MeasureTheory.Integrable f μ → ∫ (x : X), RCLike.re (f x) ∂μ = RCLike.re (∫ (x : X), f x ∂μ)
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.opensDiagramι_app : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (i : I)
  (U : (D.obj i).Opens) (j : CategoryTheory.Over i),
  (AlgebraicGeometry.opensDiagramι D i U).app j = ((TopologicalSpace.Opens.map (D.map j.hom).base).obj U).ι
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addPrehaar_self : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G},
  (interior U).Nonempty → MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K₀.toCompacts = 1
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.homMk_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (u : f.left ⟶ g.left)
  (v : f.right ⟶ g.right)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp u g.hom = CategoryTheory.CategoryStruct.comp f.hom v)
      CategoryTheory.Arrow.homMk._auto_1),
  (CategoryTheory.Arrow.homMk u v w).right = v
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LocalPresentationAt.mk.inj : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} {inst : NontriviallyNormedField 𝕜}
  {inst_1 : NormedAddCommGroup E} {inst_2 : NormedSpace 𝕜 E} {inst_3 : NormedAddCommGroup F} {inst_4 : NormedSpace 𝕜 F}
  {inst_5 : TopologicalSpace H} {inst_6 : TopologicalSpace G} {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} {inst_7 : TopologicalSpace M} {inst_8 : ChartedSpace H M}
  {inst_9 : TopologicalSpace N} {inst_10 : ChartedSpace G N} {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} {domChart : OpenPartialHomeomorph M H}
  {codChart : OpenPartialHomeomorph N G} {mem_domChart_source : x ∈ domChart.source}
  {mem_codChart_source : f x ∈ codChart.source} {domChart_mem_maximalAtlas : domChart ∈ IsManifold.maximalAtlas I n M}
  {codChart_mem_maximalAtlas : codChart ∈ IsManifold.maximalAtlas J n N}
  {source_subset_preimage_source : domChart.source ⊆ f ⁻¹' codChart.source} {property : P f domChart codChart}
  {domChart_1 : OpenPartialHomeomorph M H} {codChart_1 : OpenPartialHomeomorph N G}
  {mem_domChart_source_1 : x ∈ domChart_1.source} {mem_codChart_source_1 : f x ∈ codChart_1.source}
  {domChart_mem_maximalAtlas_1 : domChart_1 ∈ IsManifold.maximalAtlas I n M}
  {codChart_mem_maximalAtlas_1 : codChart_1 ∈ IsManifold.maximalAtlas J n N}
  {source_subset_preimage_source_1 : domChart_1.source ⊆ f ⁻¹' codChart_1.source}
  {property_1 : P f domChart_1 codChart_1},
  { domChart := domChart, codChart := codChart, mem_domChart_source := mem_domChart_source,
        mem_codChart_source := mem_codChart_source, domChart_mem_maximalAtlas := domChart_mem_maximalAtlas,
        codChart_mem_maximalAtlas := codChart_mem_maximalAtlas,
        source_subset_preimage_source := source_subset_preimage_source, property := property } =
      { domChart := domChart_1, codChart := codChart_1, mem_domChart_source := mem_domChart_source_1,
        mem_codChart_source := mem_codChart_source_1, domChart_mem_maximalAtlas := domChart_mem_maximalAtlas_1,
        codChart_mem_maximalAtlas := codChart_mem_maximalAtlas_1,
        source_subset_preimage_source := source_subset_preimage_source_1, property := property_1 } →
    domChart = domChart_1 ∧ codChart = codChart_1
-- Std.Time.Format.Modifier
Std.Time.Modifier.u.inj : ∀ {presentation presentation_1 : Std.Time.Year},
  Std.Time.Modifier.u presentation = Std.Time.Modifier.u presentation_1 → presentation = presentation_1
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL.match_7.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l : Std.DTreeMap.Internal.Impl α β) →
      (motive :
          (r : Std.DTreeMap.Internal.Impl α β) →
            r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size → Sort u_3) →
        (r : Std.DTreeMap.Internal.Impl α β) →
          (hrb : r.Balanced) →
            (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size) →
              ((hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
                  (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size Std.DTreeMap.Internal.Impl.leaf.size) →
                    motive Std.DTreeMap.Internal.Impl.leaf hrb hlr) →
                ((rs : ℕ) →
                    (k : α) →
                      (v : β k) →
                        (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                          (hrb : (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).Balanced) →
                            (hlr :
                                Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size
                                  (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).size) →
                              motive (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r) hrb hlr) →
                  motive r hrb hlr
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.freeAddGroupCongr_symm : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β),
  (FreeAddGroup.freeAddGroupCongr e).symm = FreeAddGroup.freeAddGroupCongr e.symm
-- Mathlib.LinearAlgebra.Dual.Defs
Module.erange_coe : ∀ (R : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.IsReflexive R M], (Module.Dual.eval R M).range = ⊤
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_substFunc : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {β : Type v'}
  [inst_1 : L'.Structure M] {c : {n : ℕ} → L.Functions n → L'.Term (Fin n)},
  (∀ {n : ℕ} (g : L.Functions n) (y : Fin n → M),
      FirstOrder.Language.Term.realize y g.term = FirstOrder.Language.Term.realize y (c g)) →
    ∀ (v : β → M) (x : L.Term β),
      FirstOrder.Language.Term.realize v (x.substFunc fun {n} => c) = FirstOrder.Language.Term.realize v x
-- Mathlib.Data.Finmap
/-- `Finmap β` is the type of finite maps over a multiset. It is effectively
a quotient of `AList β` by permutation of the underlying list.  -/
Finmap : {α : Type u} → (α → Type v) → Type (max u v)
-- Batteries.Data.HashMap.Basic
Batteries.HashMap.mk.inj : ∀ {α : Type u} {β : Type v} {inst : BEq α} {inst_1 : Hashable α} {inner inner_1 : Std.HashMap α β},
  { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- If there is any isomorphism `G.obj ⊤ ≅ ⊤`, then `G` preserves terminal objects.  -/
CategoryTheory.Limits.preservesTerminal_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasTerminal D] (f : G.obj (⊤_ C) ≅ ⊤_ D),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G
-- Init.System.IO
IO.instDecidableEqTaskState : DecidableEq IO.TaskState
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBasis.isBase_restrict : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → (M.restrict X).IsBase I
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.prod_mono : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] {s₁ s₂ : AddSubmonoid M}
  {t₁ t₂ : AddSubmonoid N}, s₁ ≤ s₂ → t₁ ≤ t₂ → s₁.prod t₁ ≤ s₂.prod t₂
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongr_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {ι' : Type u_8} (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N)
  (v : ι' → M), (AlternatingMap.domDomCongr σ f) v = f (v ∘ ⇑σ)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
/-- `IntermediateField.adjoin` as an algebra over `Algebra.adjoin`.  -/
IntermediateField.algebraAdjoinAdjoin.instAlgebraSubtypeMemSubalgebraAdjoinAdjoin : (F : Type u_1) →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] → (S : Set E) → Algebra ↥(Algebra.adjoin F S) ↥(IntermediateField.adjoin F S)
-- Mathlib.Computability.Primrec.List
Primrec.nat_omega_rec' : ∀ {β : Type u_2} {σ : Type u_4} [inst : Primcodable β] [inst_1 : Primcodable σ] (f : β → σ) {m : β → ℕ} {l : β → List β}
  {g : β → List σ → Option σ},
  Primrec m →
    Primrec l →
      Primrec₂ g → (∀ (b b' : β), b' ∈ l b → m b' < m b) → (∀ (b : β), g b (List.map f (l b)) = some (f b)) → Primrec f
-- Mathlib.Topology.Specialization
/-- A recursor for `Specialization`. Use as `induction x`.  -/
Specialization.rec : {α : Type u_1} →
  {β : Specialization α → Sort u_4} → ((a : α) → β (Specialization.toEquiv a)) → (a : Specialization α) → β a
-- Mathlib.RingTheory.Algebraic.Denominator
Algebra.denominator_def : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : IsPrincipalIdealRing R] [inst_2 : CommRing S]
  [inst_3 : Algebra R S] (x : S),
  Algebra.denominator R x = Submodule.IsPrincipal.generator ((Subalgebra.toSubmodule (integralClosure R S)).colon {x})
-- Mathlib.Order.Interval.Finset.Defs
Set.instFintypeIic.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α),
  Set.instFintypeIic a = Fintype.ofFinset (Finset.Iic a) ⋯
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.algebraMap_eq : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (self : Algebra.Generators R S ι), algebraMap (MvPolynomial ι R) S = ↑(MvPolynomial.aeval self.val)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instIsIsoMapTruncLEAppTruncLEι : ∀ {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) [CategoryTheory.IsTriangulated C] (X : C) (n : ℤ),
  CategoryTheory.IsIso ((t.truncLE n).map ((t.truncLEι n).app X))
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
HomologicalComplex.stupidTruncMap.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c')
  [inst_3 : e.IsRelIff],
  HomologicalComplex.stupidTruncMap φ e = HomologicalComplex.extendMap (HomologicalComplex.restrictionMap φ e) e
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∉ t₁ → (t₁ ∪ t₂)[k]! = t₂[k]!
-- Mathlib.RingTheory.Noetherian.Basic
/-- In a module over a Noetherian ring, the submodule generated by finitely many vectors is
Noetherian.  -/
isNoetherian_span_of_finite : ∀ (R : Type u_1) {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherianRing R]
  {A : Set M}, A.Finite → IsNoetherian R ↥(Submodule.span R A)
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Balanced.below.red : ∀ {α : Type u_1} {motive : (a : RBTree.RBNode α) → (a_1 : RBTree.RBColor) → (a_2 : ℕ) → a.Balanced a_1 a_2 → Prop}
  {x : RBTree.RBNode α} {n : ℕ} {y : RBTree.RBNode α} {v : α} (a : x.Balanced RBTree.RBColor.black n)
  (a_1 : y.Balanced RBTree.RBColor.black n),
  RBTree.RBNode.Balanced.below a →
    motive x RBTree.RBColor.black n a →
      RBTree.RBNode.Balanced.below a_1 → motive y RBTree.RBColor.black n a_1 → RBTree.RBNode.Balanced.below ⋯
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.one_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulOneClass α] [inst_4 : MulOneClass β] [inst_5 : MulOneClass γ] (f : α →*o β), OrderMonoidHom.comp 1 f = 1
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.Path.child.injEq : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} (x : P.last.M) (a : P.A) (f : P.last.B a → P.last.M) (h : x.dest = ⟨a, f⟩)
  (j : P.last.B a) (i : Fin2 n) (c : MvPFunctor.M.Path P (f j) i) (a_1 : P.A) (f_1 : P.last.B a_1 → P.last.M)
  (h_1 : x.dest = ⟨a_1, f_1⟩) (j_1 : P.last.B a_1) (c_1 : MvPFunctor.M.Path P (f_1 j_1) i),
  (MvPFunctor.M.Path.child x a f h j i c = MvPFunctor.M.Path.child x a_1 f_1 h_1 j_1 i c_1) =
    (a = a_1 ∧ f ≍ f_1 ∧ j ≍ j_1 ∧ c ≍ c_1)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.instAlgEquivClass : ∀ {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₂], AlgEquivClass (A₁ ≃ₐ[R] A₂) R A₁ A₂
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.gc_map_comap : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S),
  GaloisConnection (Subring.map f) (Subring.comap f)
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.splitFromSteps.match_1.eq_1 : ∀ {s : String.Slice} (motive : List (String.Slice.Pattern.SearchStep s) → Sort u_1) (h_1 : Unit → motive [])
  (h_2 :
    (startPos endPos : s.Pos) →
      (l : List (String.Slice.Pattern.SearchStep s)) →
        motive (String.Slice.Pattern.SearchStep.rejected startPos endPos :: l))
  (h_3 :
    (p q : s.Pos) →
      (l : List (String.Slice.Pattern.SearchStep s)) → motive (String.Slice.Pattern.SearchStep.matched p q :: l)),
  (match [] with
    | [] => h_1 ()
    | String.Slice.Pattern.SearchStep.rejected startPos endPos :: l => h_2 startPos endPos l
    | String.Slice.Pattern.SearchStep.matched p q :: l => h_3 p q l) =
    h_1 ()
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple.0.RootPairing.GeckConstruction.termH : Lean.ParserDescr