mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.decompose_symm_mul : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring A]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜]
  (x y : DirectSum ι fun i => ↥(𝒜 i)),
  (DirectSum.decompose 𝒜).symm (x * y) = (DirectSum.decompose 𝒜).symm x * (DirectSum.decompose 𝒜).symm y
-- Mathlib.Order.Category.DistLat
DistLat.mk.inj : ∀ {carrier : Type u_1} {str : DistribLattice carrier} {carrier_1 : Type u_1} {str_1 : DistribLattice carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
Units.inv_pos : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [PosMulStrictMono R] {u : Rˣ},
  0 < ↑u⁻¹ ↔ 0 < ↑u
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- A reflexive quiver extends a quiver with a specified arrow `id X : X ⟶ X` for each `X` in its
type of objects. We denote these arrows by `id` since categories can be understood as an extension
of refl quivers.
 -/
CategoryTheory.ReflQuiver : Type u → Type (max u (v + 1))
-- Mathlib.Analysis.ODE.Gronwall
/-- A Grönwall-like inequality: if `f : ℝ → ℝ` is continuous on `[a, b]` and satisfies
the inequalities `f a ≤ δ` and
`∀ x ∈ [a, b), liminf_{z→x+0} (f z - f x)/(z - x) ≤ K * (f x) + ε`, then `f x`
is bounded by `gronwallBound δ K ε (x - a)` on `[a, b]`.

See also `norm_le_gronwallBound_of_norm_deriv_right_le` for a version bounding `‖f x‖`,
`f : ℝ → E`.  -/
le_gronwallBound_of_liminf_deriv_right_le : ∀ {f f' : ℝ → ℝ} {δ K ε a b : ℝ},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), (z - x)⁻¹ * (f z - f x) < r) →
      f a ≤ δ → (∀ x ∈ Set.Ico a b, f' x ≤ K * f x + ε) → ∀ x ∈ Set.Icc a b, f x ≤ gronwallBound δ K ε (x - a)
-- Lean.Server.FileWorker.SemanticHighlighting
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.collectVersoTokens.go : Lean.FileMap →
  (Lean.Syntax → Array Lean.Server.FileWorker.LeanSemanticToken) →
    Lean.Syntax → StateM (Array Lean.Server.FileWorker.LeanSemanticToken) Unit
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.leftAdjointSquareConjugate.vcomp.eq_1 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {g : a ⟶ c} {h : b ⟶ d} {l₁ : a ⟶ b} {l₂ l₃ : c ⟶ d}
  (α : CategoryTheory.CategoryStruct.comp g l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h) (β : l₃ ⟶ l₂),
  CategoryTheory.Bicategory.leftAdjointSquareConjugate.vcomp α β =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft g β) α
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.smul_naturality : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (f : M ⟶ N) (r : R),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).map f) (N.smul r) =
    CategoryTheory.CategoryStruct.comp (M.smul r) ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).map f)
-- Mathlib.Logic.Equiv.Defs
Equiv.forall₃_congr : ∀ {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {γ₁ : Sort u_5} {γ₂ : Sort u_6}
  {p : α₁ → β₁ → γ₁ → Prop} {q : α₂ → β₂ → γ₂ → Prop} (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂) (eγ : γ₁ ≃ γ₂),
  (∀ {x : α₁} {y : β₁} {z : γ₁}, p x y z ↔ q (eα x) (eβ y) (eγ z)) →
    ((∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ↔ ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z)
-- Mathlib.Order.KrullDimension
Order.height_bot : ∀ (α : Type u_3) [inst : Preorder α] [inst_1 : OrderBot α], Order.height ⊥ = 0
-- Mathlib.Data.Ordmap.Invariants
Ordnode.rotateR.eq_1 : ∀ {α : Type u_1} (x : α) (x_1 : Ordnode α) (size : ℕ) (l : Ordnode α) (x_3 : α) (m : Ordnode α),
  (Ordnode.node size l x_3 m).rotateR x x_1 =
    if m.size < Ordnode.ratio * l.size then l.node3R x_3 m x x_1 else l.node4R x_3 m x x_1
-- Mathlib.Algebra.Category.MonCat.Adjunctions
/-- The `adjoinZero`-forgetful adjunction from `AddSemigrp` to `AddMonCat`  -/
AddMonCat.adjoinZeroAdj : AddMonCat.adjoinZero ⊣ CategoryTheory.forget₂ AddMonCat AddSemigrp
-- Mathlib.Order.Interval.Finset.Fin
Fin.card_Ioi : ∀ {n : ℕ} (a : Fin n), (Finset.Ioi a).card = n - 1 - ↑a
-- Lean.Meta.Sym.Arith.Types
/-- Non-commutative rings.  -/
Lean.Meta.Sym.Arith.State.ncRings : Lean.Meta.Sym.Arith.State → Array Lean.Meta.Sym.Arith.Ring
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.addCommSemigroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst_1 : AddCommSemigroup M₁] (f : M₁ → M₂)
  (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y),
  Function.Surjective.addCommSemigroup f hf mul =
    { toAddSemigroup := Function.Surjective.addSemigroup f hf mul, add_comm := ⋯ }
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.toNonUnitalSubsemiring_injective : ∀ {R : Type u} [inst : NonAssocSemiring R], Function.Injective Subsemiring.toNonUnitalSubsemiring
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF_iff_kernel : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X c μ ↔
    ProbabilityTheory.Kernel.HasSubgaussianMGF X c (ProbabilityTheory.Kernel.const Unit μ)
      (MeasureTheory.Measure.dirac ())
-- Mathlib.GroupTheory.Index
Subgroup.finiteIndex_toAddSubgroup_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, (Subgroup.toAddSubgroup H).FiniteIndex ↔ H.FiniteIndex
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_diff!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} [inst_1 : Inhabited (β k)],
        Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.diff! m₂).get! k = default
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measure_pos_iff_nonempty_of_isMulLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] [μ.Regular],
  μ ≠ 0 → ∀ {s : Set G}, IsOpen s → (0 < μ s ↔ s.Nonempty)
-- Aesop.Tree.Free
Aesop.GoalRef.free : Aesop.GoalRef → BaseIO Unit
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.instConcreteCategoryAlgHomCarrier : (R : Type u) → [inst : CommRing R] → CategoryTheory.ConcreteCategory (AlgCat R) fun x1 x2 => ↑x1 →ₐ[R] ↑x2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.nsmul_toReal_eq_mul : ∀ {n : ℕ},
  n ≠ 0 → ∀ {θ : Real.Angle}, (n • θ).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-Real.pi / ↑n) (Real.pi / ↑n)
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.ofIso_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {Y : C} (e : X ≅ Y),
  (P.ofIso e).ι = CategoryTheory.CategoryStruct.comp P.ι ((CategoryTheory.Functor.const J).map e.hom)
-- Mathlib.Data.Fintype.Card
set_fintype_card_le_univ : ∀ {α : Type u_1} [inst : Fintype α] (s : Set α) [inst_1 : Fintype ↑s], Fintype.card ↑s ≤ Fintype.card α
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
/-- In a Lie group, inversion is `C^n`.  -/
contMDiff_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] [LieGroup I n G],
  ContMDiff I I n fun x => x⁻¹
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.instIsCommMonObjTensorObj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] {M N : C} [inst_3 : CategoryTheory.MonObj M]
  [inst_4 : CategoryTheory.MonObj N] [CategoryTheory.IsCommMonObj M] [CategoryTheory.IsCommMonObj N],
  CategoryTheory.IsCommMonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
-- Mathlib.RingTheory.Algebraic.Defs
Algebra.transcendental_def : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  Algebra.Transcendental R A ↔ ∃ x, Transcendental R x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.toArray_eq_match_rci : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α],
  r.toArray =
    match Std.PRange.least? with
    | none => #[]
    | some init => init...*.toArray
-- Mathlib.Util.AtomM.Recurse
/-- A tactic in the `AtomM.RecurseM` monad which will simplify expression `parent` to a normal form, by
running a core operation `eval` (in the `AtomM` monad) on the maximal subexpression(s) on which
`eval` does not fail.

There is also a subsequent clean-up operation, governed by the context from the `AtomM.RecurseM`
monad.

* `root`: true if this is a direct call to the function.
  `AtomM.RecurseM.run` sets this to `false` in recursive mode.
 -/
Mathlib.Tactic.AtomM.onSubexpressions : (Lean.Expr → Mathlib.Tactic.AtomM Lean.Meta.Simp.Result) →
  Lean.Expr → Bool → optParam Bool true → Mathlib.Tactic.AtomM.RecurseM Lean.Meta.Simp.Result
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryLE!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α},
  t₁.Equiv t₂ → Std.DTreeMap.Const.getEntryLE! t₁ k = Std.DTreeMap.Const.getEntryLE! t₂ k
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A set `B` is a `G`-invariant block if `g • B ⊆ B` for all `g : G`.

Note: It is not necessarily a block when the action is not by a group.  -/
MulAction.IsInvariantBlock : (G : Type u_1) → {X : Type u_2} → [SMul G X] → Set X → Prop
-- Lean.Data.Lsp.TextSync
/-- NOTE: This is defined twice in the spec. The latter version has more fields.  -/
Lean.Lsp.TextDocumentSyncOptions : Type
-- Mathlib.Data.Sym.Sym2
Sym2.map_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β}, Sym2.map (g ∘ f) = Sym2.map g ∘ Sym2.map f
-- Init.Data.Rat.Lemmas
Rat.intCast_nonneg : ∀ {a : ℤ}, 0 ≤ ↑a ↔ 0 ≤ a
-- Mathlib.NumberTheory.ZetaValues
/-- The function `x ↦ Bₖ(x) : ℝ → ℝ`.  -/
bernoulliFun : ℕ → ℝ → ℝ
-- Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
/-- Similar to `geom_sum_isUnit`, but instead of assuming `2 ≤ n` we assume that `j` is a unit in
`A`.  -/
IsPrimitiveRoot.geom_sum_isUnit' : ∀ {n j : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [IsDomain A],
  IsPrimitiveRoot ζ n → j.Coprime n → IsUnit ↑j → IsUnit (∑ i ∈ Finset.range j, ζ ^ i)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instModule : {α : Type u} →
  {β : Type v} →
    {𝕜 : Type u_2} →
      [inst : PseudoMetricSpace 𝕜] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : PseudoMetricSpace β] →
            [inst_3 : Semiring 𝕜] →
              [inst_4 : AddCommMonoid β] →
                [inst_5 : Module 𝕜 β] →
                  [IsBoundedSMul 𝕜 β] →
                    [inst : BoundedAdd β] → [inst_6 : ContinuousAdd β] → Module 𝕜 (BoundedContinuousFunction α β)
-- Init.Core
/-- A dependent recursion principle for `Quot`. It is analogous to the
[recursor](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=recursors) for a structure, and can be used when the resulting type
is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may
be easier to use:
 * `Quot.lift` is useful for defining non-dependent functions.
 * `Quot.ind` is useful for proving theorems about quotients.
 * `Quot.recOnSubsingleton` can be used whenever the target type is a `Subsingleton`.
 * `Quot.hrecOn` uses [heterogeneous equality](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=HEq) instead of rewriting with
   `Quot.sound`.

`Quot.recOn` is a version of this recursor that takes the quotient parameter first.
 -/
Quot.rec : {α : Sort u} →
  {r : α → α → Prop} →
    {motive : Quot r → Sort v} →
      (f : (a : α) → motive (Quot.mk r a)) → (∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) → (q : Quot r) → motive q
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.commMap_canonical_eq_mixed : ∀ (K : Type u_1) [inst : Field K] (x : K),
  (NumberField.mixedEmbedding.commMap K) ((NumberField.canonicalEmbedding K) x) = (NumberField.mixedEmbedding K) x
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `fallback` if no such pair exists.
 -/
Std.ExtDTreeMap.getEntryLTD : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Sigma β → (a : α) × β a
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.range_incl : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M), N.incl.range = N
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeOption.match_1.eq_2 : ∀ {n : ℕ} (motive : Fin (n + 1) → Sort u_1) (i : ℕ) (h : i + 1 < n + 1) (h_1 : Unit → motive ⟨0, ⋯⟩)
  (h_2 : (i : ℕ) → (h : i + 1 < n + 1) → motive ⟨i.succ, h⟩),
  (match ⟨i.succ, h⟩ with
    | ⟨0, ⋯⟩ => h_1 ()
    | ⟨i.succ, h⟩ => h_2 i h) =
    h_2 i h
-- Mathlib.LinearAlgebra.Matrix.Ideal
/-- The two-sided ideal of matrices with entries in `I ≤ R`.  -/
TwoSidedIdeal.matrix : {R : Type u_1} →
  (n : Type u_2) →
    [inst : NonUnitalNonAssocRing R] → [inst_1 : Fintype n] → TwoSidedIdeal R → TwoSidedIdeal (Matrix n n R)
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- If two functions agree on the circle, then their circle averages agree.  -/
Real.circleAverage_congr_sphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E},
  Set.EqOn f₁ f₂ (Metric.sphere c |R|) → Real.circleAverage f₁ c R = Real.circleAverage f₂ c R
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.range_const_subset : ∀ {β : Type u_2} (α : Type u_5) [inst : MeasurableSpace α] (b : β), (MeasureTheory.SimpleFunc.const α b).range ⊆ {b}
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_nonempty : ∀ {α : Type u_1} [inst : Fintype α] [Nonempty α], Finset.univ.Nonempty
-- ProofWidgets.Component.PenroseDiagram
/-- Assemble the diagram using the provided domain and style programs.

`none` is returned iff nothing was added to the diagram.  -/
ProofWidgets.Penrose.DiagramBuilderM.buildDiagram : String → String → optParam ℕ 500 → ProofWidgets.Penrose.DiagramBuilderM (Option ProofWidgets.Html)
-- Mathlib.RingTheory.DedekindDomain.SInteger
/-- The subgroup of `S`-units of `Kˣ`.  -/
Set.unit : {R : Type u} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      Set (IsDedekindDomain.HeightOneSpectrum R) →
        (K : Type v) → [inst_2 : Field K] → [inst_3 : Algebra R K] → [IsFractionRing R K] → Subgroup Kˣ
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.refl_toContinuousLinearEquiv : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A], ↑(ContinuousAlgEquiv.refl R A) = ContinuousLinearEquiv.refl R A
-- Init.Data.Array.Lemmas
Array.filter_append : ∀ {α : Type u_1} {p : α → Bool} {xs ys : Array α} {stop : ℕ},
  stop = xs.size + ys.size → Array.filter p (xs ++ ys) 0 stop = Array.filter p xs ++ Array.filter p ys
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
UpgradedStandardBorel.toMeasurableSpace : {α : Type u_1} → [self : UpgradedStandardBorel α] → MeasurableSpace α
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor'_obj_X₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) (K : HomologicalComplex C c),
  ((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).X₃ = K.X k
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.induction_on₂ : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {β : LocalizedModule S M → LocalizedModule S M → Prop},
  (∀ (m m' : M) (s s' : ↥S), β (LocalizedModule.mk m s) (LocalizedModule.mk m' s')) →
    ∀ (x y : LocalizedModule S M), β x y
-- Mathlib.Data.Vector.Defs
/-- Runs a function over a pair of vectors returning the intermediate results and a
final result.
 -/
List.Vector.mapAccumr₂ : {α : Type u_1} →
  {β : Type u_2} →
    {σ : Type u_3} →
      {φ : Type u_4} → {n : ℕ} → (α → β → σ → σ × φ) → List.Vector α n → List.Vector β n → σ → σ × List.Vector φ n
-- Mathlib.Order.RelIso.Basic
RelIso.ofSurjective_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) (H : Function.Surjective ⇑f) (a : α),
  (RelIso.ofSurjective f H) a = f a
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.map_mul_right_inv_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : DivisionMonoid G] [MeasurableMul G] [MeasurableInv G]
  (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G),
  MeasureTheory.Measure.map (fun t => (g * t)⁻¹) μ = μ
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.cofilteredClosure.min : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  {f : α → C} {j j' : C},
  CategoryTheory.IsCofiltered.cofilteredClosure f j →
    CategoryTheory.IsCofiltered.cofilteredClosure f j' →
      CategoryTheory.IsCofiltered.cofilteredClosure f (CategoryTheory.IsCofiltered.min j j')
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.StAct.inhabited : {K : Type u_1} → {Γ : K → Type u_2} → {σ : Type u_4} → {k : K} → Inhabited (Turing.TM2to1.StAct K Γ σ k)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.comp.eq_1 : ∀ {E : Type u_3} {F : Type u_4} [inst : Group E] [inst_1 : Group F] (p : GroupSeminorm E) (f : F →* E),
  p.comp f = { toFun := fun x => p (f x), map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ }
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.ext : ∀ {α : Type u} ⦃f g : Ultrafilter α⦄, (∀ (s : Set α), s ∈ f ↔ s ∈ g) → f = g
-- Mathlib.Order.Hom.WithTopBot
Function.Embedding.coeWithBot.eq_1 : ∀ {α : Type u_1}, Function.Embedding.coeWithBot = { toFun := WithBot.some, inj' := ⋯ }
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.copy_eq : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) (s : Set G) (hs : s = ↑K), K.copy s hs = K
-- Lean.Linter.UnusedVariables
/-- Information regarding an `FVarId` definition.  -/
Lean.Linter.UnusedVariables.FVarDefinition : Type
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.toZFSet.eq_1 : ∀ (o : Ordinal.{u}), o.toZFSet = ZFSet.mk o.toPSet
-- Mathlib.Order.Atoms
/-- Every simple lattice is isomorphic to `Bool`, regardless of order.  -/
IsSimpleOrder.equivBool : {α : Type u_4} → [DecidableEq α] → [inst : LE α] → [inst_1 : BoundedOrder α] → [IsSimpleOrder α] → α ≃ Bool
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- The isomorphism `E ⧸ S.inl.range ≃+ G` induced by `S.rightHom`  -/
AddGroupExtension.quotientRangeInlEquivRight : {N : Type u_1} →
  {G : Type u_2} →
    [inst : AddGroup N] →
      [inst_1 : AddGroup G] →
        {E : Type u_3} → [inst_2 : AddGroup E] → (S : AddGroupExtension N E G) → E ⧸ S.inl.range ≃+ G
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.H1InfRes_f : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  (groupCohomology.H1InfRes A S).f =
    groupCohomology.map (QuotientGroup.mk' S) (Rep.ofHom (A.ρ.quotientToInvariants_lift S)) 1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.filterMap_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ},
  Std.ExtDHashMap.filterMap f m = ∅ ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) (Std.ExtDHashMap.Const.get m k h) = none
-- Mathlib.Topology.Connected.LocallyPathConnected
pathConnected_subset_basis : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} [LocallyPathConnectedSpace X] {U : Set X},
  IsOpen U → x ∈ U → (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsPathConnected s ∧ s ⊆ U) id
-- Mathlib.Data.List.Forall2
List.forall₂_same : ∀ {α : Type u_1} {Rₐ : α → α → Prop} {l : List α}, List.Forall₂ Rₐ l l ↔ ∀ x ∈ l, Rₐ x x
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.hasNoNatZeroDivisors : Lean.Meta.Grind.Arith.Linear.LinearM Bool
-- Mathlib.Data.Int.Basic
Int.ofNat_injective : Function.Injective Int.ofNat
-- Init.Data.UInt.Bitwise
UInt8.ofFin_shiftRight_mod : ∀ (a b : Fin UInt8.size), UInt8.ofFin (a >>> (b % 8)) = UInt8.ofFin a >>> UInt8.ofFin b
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.BinaryRefVec : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- `CartesianMonoidalCategory` implies `BraidedCategory`.
This is not an instance to prevent diamonds.  -/
CategoryTheory.BraidedCategory.ofCartesianMonoidalCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.BraidedCategory C
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.addMonoid.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X : C} [inst_2 : CategoryTheory.AddMonObj M],
  CategoryTheory.Hom.addMonoid =
    {
      add := fun f₁ f₂ =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂)
          CategoryTheory.AddMonObj.add,
      add_assoc := ⋯,
      zero :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
          CategoryTheory.AddMonObj.zero,
      zero_add := ⋯, add_zero := ⋯, nsmul := nsmulRecAuto, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
conformalAt_const_smul : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] [inst_1 : NormedSpace ℝ X] {c : ℝ},
  c ≠ 0 → ∀ (x : X), ConformalAt (fun x' => c • x') x
-- Mathlib.Order.Lattice
Pi.sup_def : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Max (α' i)] (f g : (i : ι) → α' i), f ⊔ g = fun i => f i ⊔ g i
-- Mathlib.Data.List.Induction
List.bidirectionalRec.eq_3 : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a])
  (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) (a b : α) (l : List α),
  List.bidirectionalRec nil singleton cons_append (a :: b :: l) =
    ⋯ ▸
      cons_append a (b :: l).dropLast ((b :: l).getLast ⋯)
        (List.bidirectionalRec nil singleton cons_append (b :: l).dropLast)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.multiset_sum : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {s : Multiset A},
  (∀ x ∈ s, IsIntegral R x) → IsIntegral R s.sum
-- Mathlib.Order.Types.Arithmetic
OrderType.instAddMonoid : AddMonoid OrderType.{u}
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.subset_closure_of_subset : ∀ {α : Type u_2} {X Y : Set α} (M : Matroid α),
  X ⊆ Y → autoParam (Y ⊆ M.E) Matroid.subset_closure_of_subset._auto_1 → X ⊆ M.closure Y
-- Init.Data.UInt.Basic
/-- Converts 64-bit unsigned integers to word-sized unsigned integers. On 32-bit machines, this may
overflow, which results in the value wrapping around (that is, it is reduced modulo `USize.size`).

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.toUSize : UInt64 → USize