mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.least_le : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLeast? α] {a : α},
  Std.PRange.UpwardEnumerable.LE Std.PRange.UpwardEnumerable.least a
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.coe_inf : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
  [inst_3 : FaithfulSMul M X] (P Q : { P // IsLprojection X P }), ↑(P ⊓ Q) = ↑P * ↑Q
-- Mathlib.Data.Ordmap.Ordset
Ordset.mem.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLE α] (x : α) (s : Ordset α), Ordset.mem x s = decide (x ∈ ↑s)
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_top : ∀ (S : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M],
  Submodule.restrictScalars S ⊤ = ⊤
-- Mathlib.Data.Multiset.Lattice
Multiset.sup_zero : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α], Multiset.sup 0 = ⊥
-- Init.Data.Fin.Lemmas
Fin.lt_or_lt_of_ne : ∀ {n : ℕ} {a b : Fin n}, a ≠ b → a < b ∨ b < a
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- A copy of `Finsupp.distribMulActionHom_ext'` for `AddMonoidAlgebra`.  -/
AddMonoidAlgebra.distribMulActionHom_ext' : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] {N : Type u_7} [inst_1 : Monoid R]
  [inst_2 : AddMonoid N] [inst_3 : DistribMulAction R N] [inst_4 : DistribMulAction R S]
  {f g : AddMonoidAlgebra S M →+[R] N},
  (∀ (a : M),
      f.comp (AddMonoidAlgebra.singleDistribMulActionHom a) = g.comp (AddMonoidAlgebra.singleDistribMulActionHom a)) →
    f = g
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_comp : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X}
  {inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀} [self : 𝒰.LocallyDirected] {i j k : 𝒰.I₀} (hij : i ⟶ j)
  (hjk : j ⟶ k),
  AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans (CategoryTheory.CategoryStruct.comp hij hjk) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans hij)
      (AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans hjk)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_map_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) {X Y : G.Elements}
  (f : X ⟶ Y), ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).map f).base = ↑f
-- Mathlib.Data.Finset.Lattice.Prod
Finset.inf_prodMap : ∀ {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β]
  [inst_2 : OrderTop α] [inst_3 : OrderTop β] {s : Finset ι} {t : Finset κ},
  s.Nonempty → t.Nonempty → ∀ (f : ι → α) (g : κ → β), (s ×ˢ t).inf (Prod.map f g) = (s.inf f, t.inf g)
-- Mathlib.RingTheory.Algebraic.Denominator
IsAlgebraic.denominator_ne_zero : ∀ (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}, IsAlgebraic R x → Algebra.denominator R x ≠ 0
-- Mathlib.RingTheory.Unramified.LocalRing
/-- Let `A` be an essentially of finite type `R`-algebra, `q` be a prime over `p`.
Then `A` is unramified at `p` if and only if `κ(q)/κ(p)` is separable, and `pS_q = qS_q`.  -/
Algebra.isUnramifiedAt_iff_map_eq : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.EssFiniteType R S] (p : Ideal R) [inst_4 : p.IsPrime] (q : Ideal S) [inst_5 : q.IsPrime]
  [inst_6 : q.LiesOver p] [inst_7 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
  [inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q],
  Algebra.IsUnramifiedAt R q ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = IsLocalRing.maximalIdeal (Localization.AtPrime q)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_sum : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddCommMonoid α] [inst_1 : StarAddMonoid α] {ι : Type u_10}
  (s : Finset ι) (M : ι → Matrix m n α), (∑ i ∈ s, M i).conjTranspose = ∑ i ∈ s, (M i).conjTranspose
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- If `S` is an `R`-algebra, then `S[M]` is an `R[M]`-algebra.

Warning: This produces a diamond for `Algebra R[M] S[M][M]` and another one for `Algebra R[M] R[M]`.
That's why it is not a global instance.  -/
AddMonoidAlgebra.algebraAddMonoidAlgebra : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_7} →
      [inst : AddCommMonoid M] →
        [inst_1 : CommSemiring R] →
          [inst_2 : CommSemiring S] → [Algebra R S] → Algebra (AddMonoidAlgebra R M) (AddMonoidAlgebra S M)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.tan_sub_pi : ∀ (θ : Real.Angle), (θ - ↑Real.pi).tan = θ.tan
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.isPlot_sInf_iff : ∀ {X : Type u_1} {D : Set (DiffeologicalSpace X)} {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
  Diffeology.IsPlot p ↔ ∀ d ∈ D, Diffeology.IsPlot p
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.sub_const : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Sub G] {m : MeasurableSpace α} {f : α → G}
  [MeasurableSub G], Measurable f → ∀ (c : G), Measurable fun x => f x - c
-- Lean.Parser.Extra
Lean.Parser.withoutForbidden.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.BilinearMap
/-- Create a bilinear map from a function that is linear in each component.

This is a shorthand for `mk₂'` for the common case when `R = S`.  -/
LinearMap.mk₂ : (R : Type u_2) →
  [inst : CommSemiring R] →
    {M : Type u_5} →
      {Nₗ : Type u_8} →
        {Pₗ : Type u_9} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid Nₗ] →
              [inst_3 : AddCommMonoid Pₗ] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R Nₗ] →
                    [inst_6 : Module R Pₗ] →
                      (f : M → Nₗ → Pₗ) →
                        (∀ (m₁ m₂ : M) (n : Nₗ), f (m₁ + m₂) n = f m₁ n + f m₂ n) →
                          (∀ (c : R) (m : M) (n : Nₗ), f (c • m) n = c • f m n) →
                            (∀ (m : M) (n₁ n₂ : Nₗ), f m (n₁ + n₂) = f m n₁ + f m n₂) →
                              (∀ (c : R) (m : M) (n : Nₗ), f m (c • n) = c • f m n) → M →ₗ[R] Nₗ →ₗ[R] Pₗ
-- Mathlib.Algebra.Lie.Basic
/-- Every Lie algebra is a module over itself.  -/
lieAlgebraSelfModule : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L], LieModule R L L
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.HaveLebesgueDecomposition.lebesgue_decomposition : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [self : μ.HaveLebesgueDecomposition ν],
  ∃ p, Measurable p.2 ∧ p.1.MutuallySingular ν ∧ μ = p.1 + ν.withDensity p.2
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.getValueCast? k l = some v ↔
    ∃ (h : Std.Internal.List.containsKey k l = true), Std.Internal.List.getValueCast k l h = v
-- Mathlib.Data.Set.Lattice
Set.iUnion_or : ∀ {α : Type u_1} {p q : Prop} (s : p ∨ q → Set α), ⋃ (h : p ∨ q), s h = (⋃ (i : p), s ⋯) ∪ ⋃ (j : q), s ⋯
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_eq_bot_iff_of_injective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) {f : G →* N},
  Function.Injective ⇑f → (Subgroup.map f H = ⊥ ↔ H = ⊥)
-- Aesop.RuleTac.GoalDiff
/-- `FVarId`s that appear in the new goal, but not (or with a different type)
in the old goal.  -/
Aesop.GoalDiff.addedFVars : Aesop.GoalDiff → Std.HashSet Lean.FVarId
-- Mathlib.Order.Filter.Prod
Filter.EventuallyEq.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {la : Filter α} {fa ga : α → γ},
  fa =ᶠ[la] ga → ∀ {lb : Filter β} {fb gb : β → δ}, fb =ᶠ[lb] gb → Prod.map fa fb =ᶠ[la ×ˢ lb] Prod.map ga gb
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- The product of two continuous affine maps is a continuous affine map.  -/
ContinuousAffineMap.prod : {k : Type u_10} →
  {P₁ : Type u_11} →
    {P₂ : Type u_12} →
      {P₃ : Type u_13} →
        {V₁ : Type u_15} →
          {V₂ : Type u_16} →
            {V₃ : Type u_17} →
              [inst : Ring k] →
                [inst_1 : AddCommGroup V₁] →
                  [inst_2 : Module k V₁] →
                    [inst_3 : AddTorsor V₁ P₁] →
                      [inst_4 : TopologicalSpace P₁] →
                        [inst_5 : AddCommGroup V₂] →
                          [inst_6 : Module k V₂] →
                            [inst_7 : AddTorsor V₂ P₂] →
                              [inst_8 : TopologicalSpace P₂] →
                                [inst_9 : AddCommGroup V₃] →
                                  [inst_10 : Module k V₃] →
                                    [inst_11 : AddTorsor V₃ P₃] →
                                      [inst_12 : TopologicalSpace P₃] → (P₁ →ᴬ[k] P₂) → (P₁ →ᴬ[k] P₃) → P₁ →ᴬ[k] P₂ × P₃
-- Mathlib.Algebra.Group.Hom.Defs
/-- Makes an additive inverse from a bijection which preserves addition.  -/
AddHom.inverse : {M : Type u_4} →
  {N : Type u_5} →
    [inst : Add M] →
      [inst_1 : Add N] → (f : M →ₙ+ N) → (g : N → M) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → N →ₙ+ M
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instOrderBotOfIsBotZeroClass : {ι : Type u_1} →
  (α : ι → Type u_2) →
    [inst : (i : ι) → AddCommMonoid (α i)] →
      [inst_1 : (i : ι) → PartialOrder (α i)] → [∀ (i : ι), IsBotZeroClass (α i)] → OrderBot (Π₀ (i : ι), α i)
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.Equiv.mk : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.DTreeMap α β cmp},
  m₁.inner.Equiv m₂.inner → m₁.Equiv m₂
-- Mathlib.Algebra.Lie.Basis.Base
/-- The support of `LieAlgebra.Basis.base` is in one-to-one correspondence with the indexing
set of the basis.  -/
LieAlgebra.Basis.baseSupportEquiv : {ι : Type u_1} →
  {K : Type u_2} →
    {L : Type u_3} →
      [inst : Fintype ι] →
        [inst_1 : Field K] →
          [inst_2 : CharZero K] →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra K L] →
                [inst_5 : FiniteDimensional K L] →
                  {H : LieSubalgebra K L} →
                    (b : LieAlgebra.Basis ι H) →
                      [inst_6 : LieModule.IsTriangularizable K (↥H) L] →
                        [inst_7 : LieAlgebra.IsKilling K L] → ι ≃ ↥b.base.support
-- Std.Http.Internal.ChunkedBuffer
Std.Http.Internal.ChunkedBuffer.mk.injEq : ∀ (data : Array ByteArray) (size : ℕ) (data_1 : Array ByteArray) (size_1 : ℕ),
  ({ data := data, size := size } = { data := data_1, size := size_1 }) = (data = data_1 ∧ size = size_1)
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_univ : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M), ∏ᶠ (i : α) (_ : i ∈ Set.univ), f i = ∏ᶠ (i : α), f i
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.φ_def : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R],
  SkewPolynomial.φ = MulSemiringAction.toRingHom (Multiplicative ℕ) R (Multiplicative.ofAdd 1)
-- Mathlib.Logic.Function.Defs
Function.bijective_id : ∀ {α : Sort u₁}, Function.Bijective id
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.Iso.mk_inv : ∀ {α β : AlexDisc} (e : ↑α.toTopCat ≃ₜ ↑β.toTopCat),
  (AlexDisc.Iso.mk e).inv = CategoryTheory.ConcreteCategory.ofHom ↑e.symm
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_piecewise : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s t : Finset ι) (f g : ι → M),
  ∑ x ∈ s, t.piecewise f g x = ∑ x ∈ s ∩ t, f x + ∑ x ∈ s \ t, g x
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.eq : ∀ {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄ : String}, p.Splits t₁ t₂ → p.Splits t₃ t₄ → t₁ = t₃ ∧ t₂ = t₄
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.mem_nhds_one : ∀ {G : Type u} [inst : Group G] (B : GroupFilterBasis G) {U : Set G}, U ∈ B → U ∈ nhds 1
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.isMulCommutative_iSup : ∀ {G : Type u_1} [inst : Group G] {ι : Sort u_2} [Nonempty ι] {S : ι → Subgroup G}
  [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], Directed (fun x1 x2 => x1 ≤ x2) S → IsMulCommutative ↥(⨆ i, S i)
-- Std.Tactic.BVDecide.Syntax
Lean.Elab.Tactic.BVDecide.BVDecideConfig.mk.inj : ∀ {timeout : ℕ}
  {trimProofs binaryProofs acNf andFlattening embeddedConstraintSubst structures fixedInt enums graphviz : Bool}
  {maxSteps : ℕ} {shortCircuit : Bool} {solverMode : Lean.Elab.Tactic.BVDecide.SolverMode} {timeout_1 : ℕ}
  {trimProofs_1 binaryProofs_1 acNf_1 andFlattening_1 embeddedConstraintSubst_1 structures_1 fixedInt_1 enums_1
    graphviz_1 : Bool}
  {maxSteps_1 : ℕ} {shortCircuit_1 : Bool} {solverMode_1 : Lean.Elab.Tactic.BVDecide.SolverMode},
  { timeout := timeout, trimProofs := trimProofs, binaryProofs := binaryProofs, acNf := acNf,
        andFlattening := andFlattening, embeddedConstraintSubst := embeddedConstraintSubst, structures := structures,
        fixedInt := fixedInt, enums := enums, graphviz := graphviz, maxSteps := maxSteps, shortCircuit := shortCircuit,
        solverMode := solverMode } =
      { timeout := timeout_1, trimProofs := trimProofs_1, binaryProofs := binaryProofs_1, acNf := acNf_1,
        andFlattening := andFlattening_1, embeddedConstraintSubst := embeddedConstraintSubst_1,
        structures := structures_1, fixedInt := fixedInt_1, enums := enums_1, graphviz := graphviz_1,
        maxSteps := maxSteps_1, shortCircuit := shortCircuit_1, solverMode := solverMode_1 } →
    timeout = timeout_1 ∧
      trimProofs = trimProofs_1 ∧
        binaryProofs = binaryProofs_1 ∧
          acNf = acNf_1 ∧
            andFlattening = andFlattening_1 ∧
              embeddedConstraintSubst = embeddedConstraintSubst_1 ∧
                structures = structures_1 ∧
                  fixedInt = fixedInt_1 ∧
                    enums = enums_1 ∧
                      graphviz = graphviz_1 ∧
                        maxSteps = maxSteps_1 ∧ shortCircuit = shortCircuit_1 ∧ solverMode = solverMode_1
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_eq_add_conj : ∀ {K : Type u_1} [inst : RCLike K] (z : K), ↑(RCLike.re z) = (z + (starRingEnd K) z) / 2
-- Mathlib.Algebra.Order.Round
round_add_intCast : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α)
  (y : ℤ), round (x + ↑y) = round x + y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp},
  (Std.DTreeMap.Const.toArray t).size = t.size
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
/-- Pull an opposite additive submonoid back to a submonoid along
`AddOpposite.op`  -/
AddSubmonoid.unop : {M : Type u_2} → [inst : AddZeroClass M] → AddSubmonoid Mᵃᵒᵖ → AddSubmonoid M
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.Equiv.refl : ∀ {α : Type u} (s : Stream'.WSeq α), s ~ʷ s
-- Std.Data.ExtTreeSet.Basic
/-- Erases multiple items from the tree set by iterating over the given collection and calling erase.
 -/
Std.ExtTreeSet.eraseMany : {α : Type u} →
  {cmp : α → α → Ordering} →
    [Std.TransCmp cmp] → {ρ : Type u_1} → [ForIn Id ρ α] → Std.ExtTreeSet α cmp → ρ → Std.ExtTreeSet α cmp
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, k ∈ t₂ → (t₁ \ t₂).getKey! k = default
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- The canonical map `K ⟶ K.truncGE n` for `K : CochainComplex C ℤ`.  -/
CochainComplex.πTruncGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (K : CochainComplex C ℤ) →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] → (n : ℤ) → K ⟶ K.truncGE n
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.comp_liftOfSurjective : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_1}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] {C : Type u_4} [inst_5 : CommRing C] [inst_6 : Algebra R C]
  [inst_7 : Algebra.FormallySmooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : Function.Surjective ⇑g)
  (hg' : IsNilpotent (RingHom.ker ↑g)), g.comp (Algebra.FormallySmooth.liftOfSurjective f g hg hg') = f
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr.eq_1 : ∀ (p : Turing.PartrecToTM2.Γ' → Bool) (k₁ k₂ : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) =
    Turing.PartrecToTM2.pop' k₁
      (Turing.TM2.Stmt.branch (fun s => s.elim true p) (Turing.TM2.Stmt.goto fun x => q)
        (Turing.PartrecToTM2.push' k₂ (Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.Λ'.move p k₁ k₂ q)))
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C}
  (t : CategoryTheory.Limits.IsTerminal T),
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso X i t).hom.right =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.right
        (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from T))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.right).hom
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.cases'.match_1.splitter : {n : ℕ} →
  (motive : Fin2 n.succ → Sort u_1) →
    (x : Fin2 n.succ) → (Unit → motive Fin2.fz) → ((n_1 : Fin2 n) → motive n_1.fs) → motive x
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : CommRing K] [inst_2 : Algebra R K]
  [ifr : IsFractionRing R K] [IsIntegrallyClosed R] {x : K} {n : ℕ},
  0 < n → IsIntegral R (x ^ n) → ∃ y, (algebraMap R K) y = x
-- Lean.Meta.Instances
Lean.Meta.InstanceEntry.mk : Array Lean.Meta.InstanceKey → Lean.Expr → ℕ → Option Lean.Name → Array ℕ → Lean.AttributeKind → Lean.Meta.InstanceEntry
-- Mathlib.NumberTheory.AbelSummation
/-- Specialized version of `sum_mul_eq_sub_integral_mul` when the first coefficient of the sequence
`c` is equal to `0`.  -/
sum_mul_eq_sub_integral_mul₀ : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜},
  c 0 = 0 →
    ∀ (b : ℝ),
      (∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t) →
        MeasureTheory.IntegrableOn (deriv f) (Set.Icc 1 b) MeasureTheory.volume →
          ∑ k ∈ Finset.Icc 0 ⌊b⌋₊, f ↑k * c k =
            f b * ∑ k ∈ Finset.Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k
-- Mathlib.CategoryTheory.Limits.Final
/-- If `colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit` for all `d : D`, then `F` is final.
 -/
CategoryTheory.Functor.final_of_colimit_comp_coyoneda_iso_pUnit : ∀ {C : Type v} [inst : CategoryTheory.Category.{v, v} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v, u₁} D]
  (F : CategoryTheory.Functor C D)
  (I : (d : D) → CategoryTheory.Limits.colimit (F.comp (CategoryTheory.coyoneda.obj (Opposite.op d))) ≅ PUnit.{v + 1}),
  F.Final
-- Mathlib.Topology.Algebra.Affine
Continuous.lineMap : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : AddCommGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : Ring R]
  [inst_6 : Module R V] [inst_7 : TopologicalSpace R] [ContinuousSMul R V] {X : Type u_6} [inst_9 : TopologicalSpace X]
  {f₁ f₂ : X → P} {g : X → R},
  Continuous f₁ → Continuous f₂ → Continuous g → Continuous fun x => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)
-- Init.Data.String.Basic
/-- Copies a region of a slice to a new string.

The region of `s` from `b` (inclusive) to `e` (exclusive) is copied to a newly-allocated `String`.

If `b`'s offset is greater than or equal to that of `e`, then the resulting string is `""`.

If possible, prefer `Slice.slice`, which avoids the allocation.
 -/
String.Slice.extract : (s : String.Slice) → s.Pos → s.Pos → String
-- Mathlib.Topology.Constructions.SumProd
/-- Postcomposing `f` with `Prod.snd` is continuous at `x`  -/
ContinuousAt.snd : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y × Z} {x : X}, ContinuousAt f x → ContinuousAt (fun x => (f x).2) x
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- commutation with `i`  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.commi_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) {Z : C} (h : S₂.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.φK (CategoryTheory.CategoryStruct.comp h₂.i h) =
    CategoryTheory.CategoryStruct.comp h₁.i (CategoryTheory.CategoryStruct.comp φ.τ₂ h)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.transnumAuxSeq_dist_lt : ∀ (f : CircleDeg1Lift) (n : ℕ), dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 / 2 ^ n
-- Mathlib.Tactic.IntervalCases
/-- Construct the canonical numeral for integer `z`, or fail if `z` is out of range.  -/
Mathlib.Tactic.IntervalCases.Methods.mkNumeral : Mathlib.Tactic.IntervalCases.Methods → ℤ → Lean.MetaM Lean.Expr
-- Init.Data.Option.Lemmas
Option.get_guard : ∀ {α : Type u_1} {p : α → Bool} {a : α} {h : (Option.guard p a).isSome = true}, (Option.guard p a).get h = a
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
hasFTaylorSeriesUpToOn_empty : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F}, HasFTaylorSeriesUpToOn n f p ∅
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.contains_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List α} {k : α}, (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).contains k = (t.contains k || l.contains k)
-- Mathlib.Topology.Separation.Regular
/-- A T₃ space is a T₀ space which is a regular space. Any T₃ space is a T₁ space, a T₂ space, and
a T₂.₅ space.  -/
T3Space : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Spanning.subset_ground : ∀ {α : Type u_2} {M : Matroid α} {S : Set α}, M.Spanning S → S ⊆ M.E
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_inter_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α], (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = false → (m₁.inter m₂).get? k = none
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
isAlmostIntegral_iff_isIntegral : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsNoetherianRing R]
  [IsDomain R] [IsFractionRing R S] {s : S}, IsAlmostIntegral R s ↔ IsIntegral R s