mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Disintegration.Integral
ProbabilityTheory.setIntegral_condKernel_univ_right : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] {κ : ProbabilityTheory.Kernel α (β × Ω)}
  [inst_4 : ProbabilityTheory.IsFiniteKernel κ] {E : Type u_4} {f : β × Ω → E} [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℝ E] (a : α) {s : Set β},
  MeasurableSet s →
    MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) (κ a) →
      ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ a
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.mk.injEq : ∀ {α : Type} (inner inner_1 : Std.Bounded✝ α), ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.hom_map_lift : ∀ {α : Type u_1} {M : Type u_4} [inst : AddMonoid M] {N : Type u_5} [inst_1 : AddMonoid N] (g : M →+ N) (f : α → M)
  (x : FreeAddMonoid α), g ((FreeAddMonoid.lift f) x) = (FreeAddMonoid.lift (⇑g ∘ f)) x
-- Mathlib.Analysis.Fourier.AddCircle
/-- The elements of the Hilbert basis `fourierBasis` are the functions `fourierLp 2`, i.e. the
monomials `fourier n` on the circle considered as elements of `L²`.  -/
coe_fourierBasis : ∀ {T : ℝ} [hT : Fact (0 < T)], ⇑fourierBasis = fourierLp 2
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.congr_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℕ),
  TensorProduct.congr f g ^ n = TensorProduct.congr (f ^ n) (g ^ n)
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
/-- Variant of `hom_ext`.  -/
ComplexShape.Embedding.AreComplementary.hom_ext' : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c},
  e₁.AreComplementary e₂ →
    ∀ {K L : HomologicalComplex C c} (φ : K ⟶ L),
      K.IsStrictlySupportedOutside e₂ → L.IsStrictlySupportedOutside e₁ → φ = 0
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F}
  [inst_5 : NormedSpace ℝ F],
  AEMeasurable Y μ →
    MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
      MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x)
        (MeasureTheory.Measure.map X μ)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- A constructor for isomorphisms of `CatCospanTransform`'s.  -/
CategoryTheory.Limits.CatCospanTransform.mkIso : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {A' : Type u₄} →
        {B' : Type u₅} →
          {C' : Type u₆} →
            [inst : CategoryTheory.Category.{v₁, u₁} A] →
              [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                  {F : CategoryTheory.Functor A B} →
                    {G : CategoryTheory.Functor C B} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} →
                                  (left : ψ.left ≅ ψ'.left) →
                                    (right : ψ.right ≅ ψ'.right) →
                                      (base : ψ.base ≅ ψ'.base) →
                                        autoParam
                                            (CategoryTheory.CategoryStruct.comp
                                                (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
                                                (CategoryTheory.Functor.whiskerRight left.hom F') =
                                              CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom)
                                                (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
                                            CategoryTheory.Limits.CatCospanTransform.mkIso._auto_1 →
                                          autoParam
                                              (CategoryTheory.CategoryStruct.comp
                                                  (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
                                                  (CategoryTheory.Functor.whiskerRight right.hom G') =
                                                CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom)
                                                  (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom)
                                              CategoryTheory.Limits.CatCospanTransform.mkIso._auto_3 →
                                            (ψ ≅ ψ')
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.sum_sigma_eq_sum : ∀ {n : ℕ} (c : OrderedFinpartition n) {α : Type u_5} [inst : AddCommMonoid α] (v : Fin n → α),
  ∑ m, ∑ r, v (c.emb m r) = ∑ i, v i
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- Thus conjugation defines an equivalence between natural isomorphisms.  -/
CategoryTheory.conjugateIsoEquiv : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L₁ L₂ : CategoryTheory.Functor C D} →
          {R₁ R₂ : CategoryTheory.Functor D C} → (L₁ ⊣ R₁) → (L₂ ⊣ R₂) → (L₂ ≅ L₁) ≃ (R₁ ≅ R₂)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
CategoryTheory.Functor.instIsDenseSubsiteRestrictedTopologyOfIsCoverDense : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K]
  [G.IsCoverDense K], CategoryTheory.Functor.IsDenseSubsite (G.restrictedTopology K) K G
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IicExtend_of_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {b x : α} (f : ↑(Set.Iic b) → β) (hx : x ∈ Set.Iic b),
  Set.IicExtend f x = f ⟨x, hx⟩
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂_inv_hom_isIso : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (η : f ⟶ g) [inst_2 : CategoryTheory.IsIso η],
  CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.inv η)) (F.map₂ η) =
    CategoryTheory.CategoryStruct.id (F.map g)
-- Mathlib.MeasureTheory.Measure.Sub
/-- This application lemma only works in special circumstances. Given knowledge of
when `μ ≤ ν` and `ν ≤ μ`, a more general application lemma can be written.  -/
MeasureTheory.Measure.sub_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsFiniteMeasure ν],
  MeasurableSet s → ν ≤ μ → (μ - ν) s = μ s - ν s
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.sInf_carrier_def : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (S : Set hI.SubDPIdeal),
  (sInf S).carrier = ⨅ s ∈ insert ⊤ S, s.carrier
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.colimit_one_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat) (j : J), 1 = GrpCat.FilteredColimits.G.mk F ⟨j, 1⟩
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.mapBiprod_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : F.PreservesZeroMorphisms] [inst_6 : CategoryTheory.Limits.PreservesBinaryBiproduct X Y F],
  (F.mapBiprod X Y).inv =
    CategoryTheory.Limits.biprod.desc (F.map CategoryTheory.Limits.biprod.inl) (F.map CategoryTheory.Limits.biprod.inr)
-- Mathlib.Algebra.Group.Action.Opposite
MulOpposite.instMulAction.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α],
  MulOpposite.instMulAction = { toSMul := MulOpposite.instSMul, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.coe_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] (s : Finset α) (t : Finset β),
  ↑(s +ᵥ t) = ↑s +ᵥ ↑t
-- Mathlib.Control.Monad.Cont
ExceptT.goto_mkLabel : ∀ {m : Type u → Type v} [inst : Monad m] {α β ε : Type u} (x : MonadCont.Label (Except ε α) m β) (i : α),
  MonadCont.goto (ExceptT.mkLabel x) i = ExceptT.mk (Except.ok <$> MonadCont.goto x (Except.ok i))
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- A partial Hahn embedding is strictly monotone.  -/
HahnEmbedding.IsPartial.strictMono : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R}
  {f : M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)}, HahnEmbedding.IsPartial seed f → StrictMono ↑f
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.mapIso_refl : ∀ {X Y : TopCat} (f : X ⟶ Y) (h : f = f),
  TopologicalSpace.Opens.mapIso f f h = CategoryTheory.Iso.refl (TopologicalSpace.Opens.map f)
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.addContent_le_sum_of_subset_sUnion : ∀ {α : Type u_1} {C : Set (Set α)} {t : Set α} {G : Type u_2} [inst : AddCommMonoid G] [inst_1 : PartialOrder G]
  [CanonicallyOrderedAdd G] {m : MeasureTheory.AddContent G C},
  MeasureTheory.IsSetSemiring C → ∀ {J : Finset (Set α)}, ↑J ⊆ C → t ∈ C → t ⊆ ⋃₀ ↑J → m t ≤ ∑ u ∈ J, m u
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.isRationalOver_iff : ∀ {S X : AlgebraicGeometry.Scheme} (sX : X ⟶ S),
  AlgebraicGeometry.Scheme.IsRationalOver sX ↔
    ∃ n, AlgebraicGeometry.Scheme.BirationalOver sX (AlgebraicGeometry.AffineSpace n S ↘ S)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_neg_eq_arg_add_pi_iff : ∀ {x : ℂ}, (-x).arg = x.arg + Real.pi ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsEisensteinAt.leading : ∀ {R : Type u} [inst : CommSemiring R] {f : Polynomial R} {𝓟 : Ideal R}, f.IsEisensteinAt 𝓟 → f.leadingCoeff ∉ 𝓟
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
TensorAlgebra.SymRel.mul_comm : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x y : M),
  TensorAlgebra.SymRel R M ((TensorAlgebra.ι R) x * (TensorAlgebra.ι R) y)
    ((TensorAlgebra.ι R) y * (TensorAlgebra.ι R) x)
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_eq_empty : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, ¬b < a → Set.Ioc b a = ∅
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.prop_hom_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (self : X.Hom Y), Q self.left
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α} [inst_3 : Inhabited (β k)], k ∉ m₂ → (m₁ ∩ m₂).get! k = default
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- Given a submodule, restrict to the pairing on `W` by
simultaneously corestricting to `Module.Dual R M ⧸ W.dualAnnihilator`.
This is `Submodule.dualRestrict` factored through the quotient by its kernel (which
is `W.dualAnnihilator` by definition).

See `Subspace.dualPairing_nondegenerate`.  -/
Submodule.dualPairing : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (W : Submodule R M) → Module.Dual R M ⧸ W.dualAnnihilator →ₗ[R] ↥W →ₗ[R] R
-- Init.Data.Float.Float32
/-- Checks whether a floating point number is `NaN` ("not a number") value.

`NaN` values result from operations that might otherwise be errors, such as dividing zero by zero.

This function has a logical model in terms of `Float32.Model`. It is compiled to the C operator `isnan`.
 -/
Float32.isNaN : Float32 → Bool
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkGrindStx : Lean.Meta.Try.Info → Lean.MetaM (Lean.TSyntax `tactic)
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.ins.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_2 ()
-- Batteries.Data.BitVec.Lemmas
BitVec.toNat_ofFnLE : ∀ {n : ℕ} (f : Fin n → Bool), (BitVec.ofFnLE f).toNat = Nat.ofBits f
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.unit_app_unit_comp_map_η_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.OplaxMonoidal]
  [inst_5 : G.LaxMonoidal] [adj.IsMonoidal] {Z : C}
  (h : G.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (adj.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.OplaxMonoidal.η F)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε G) h
-- Init.Data.Float.Float32
/-- Computes the cube root of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`cbrtf`.
 -/
Float32.cbrt : Float32 → Float32
-- Lean.Meta.DiscrTree.Main
/-- When `noIndexAtArgs := true`, `pushArgs` assumes function application arguments have a `no_index` annotation.
That is, `f a b` is indexed as it was `f (no_index a) (no_index b)`.
This feature is used when indexing local proofs in the simplifier. This is useful in examples like the one described on issue #2670.
In this issue, we have a local hypotheses `(h : ∀ p : α × β, f p p.2 = p.2)`, and users expect it to be applicable to
`f (a, b) b = b`. This worked in Lean 3 since no indexing was used. We can retrieve Lean 3 behavior by writing
`(h : ∀ p : α × β, f p (no_index p.2) = p.2)`, but this is very inconvenient when the hypotheses was not written by the user in first place.
For example, it was introduced by another tactic. Thus, when populating the discrimination tree explicit arguments provided to `simp` (e.g., `simp [h]`),
we use `noIndexAtArgs := true`. See comment: https://github.com/leanprover/lean4/issues/2670#issuecomment-1758889365
 -/
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.pushArgs : Bool → Array Lean.Expr → Lean.Expr → Bool → Lean.MetaM (Lean.Meta.DiscrTree.Key × Array Lean.Expr)
-- Init.Core
/-- A dependent recursion principle for `Quotient`. 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:

 * `Quotient.lift` is useful for defining non-dependent functions.
 * `Quotient.ind` is useful for proving theorems about quotients.
 * `Quotient.recOnSubsingleton` can be used whenever the target type is a `Subsingleton`.
 * `Quotient.hrecOn` uses heterogeneous equality instead of rewriting with `Quotient.sound`.

`Quotient.rec` is a version of this recursor that takes the quotient parameter last.
 -/
Quotient.recOn : {α : Sort u} →
  {s : Setoid α} →
    {motive : Quotient s → Sort v} →
      (q : Quotient s) → (f : (a : α) → motive ⟦a⟧) → (∀ (a b : α) (p : a ≈ b), ⋯ ▸ f a = f b) → motive q
-- Mathlib.Data.Nat.Log
_private.Mathlib.Data.Nat.Log.0.Nat.log.go.match_1.splitter : (motive : ℕ × ℕ → Sort u_1) → (x : ℕ × ℕ) → ((q e : ℕ) → motive (q, e)) → motive x
-- Mathlib.Algebra.Group.Shrink
Shrink.instOne : {α : Type u_2} → [inst : Small.{v, u_2} α] → [One α] → One (Shrink.{v, u_2} α)
-- Init.Data.ByteArray.Basic
/-- Copies the slice at `[srcOff, srcOff + len)` in `src` to `[destOff, destOff + len)` in
`dest`, growing `dest` if necessary. If `exact` is `false`, the capacity
will be doubled when grown.
 -/
ByteArray.copySlice : ByteArray → ℕ → ByteArray → ℕ → ℕ → optParam Bool true → ByteArray
-- Mathlib.Tactic.FunProp.Theorems
/-- Apply theorem e.g. `Continuous fun (f : (x : X) → Y x ↦ f x)`  -/
Mathlib.Meta.FunProp.LambdaTheoremArgs.apply : Mathlib.Meta.FunProp.LambdaTheoremArgs
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
CliffordAlgebra.ι_mem_evenOdd_one : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M), (CliffordAlgebra.ι Q) m ∈ CliffordAlgebra.evenOdd Q 1
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.isStableUnderColimitsOfShape_iff_colimitsOfShape_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J], W.IsStableUnderColimitsOfShape J ↔ W.colimitsOfShape J ≤ W
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  (t t_1 : Std.ExtTreeMap α β cmp), t = t_1 → ∀ (a a_1 : α), a = a_1 → t.getKey! a = t_1.getKey! a_1
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The circumcenter of a 1-simplex equals its centroid.  -/
Affine.Simplex.circumcenter_eq_centroid : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : Affine.Simplex ℝ P 1), s.circumcenter = Finset.centroid ℝ Finset.univ s.points
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.StableUnderCompositionWithLocalizationAway.respectsIso : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.MeasureTheory.PiSystem
/-- Induction principle for measurable sets.
If `s` is a π-system that generates the product `σ`-algebra on `α`
and a predicate `C` defined on measurable sets is true

- on the empty set;
- on each set `t ∈ s`;
- on the complement of a measurable set that satisfies `C`;
- on the union of a sequence of pairwise disjoint measurable sets that satisfy `C`,

then it is true on all measurable sets in `α`.  -/
MeasurableSpace.induction_on_inter : ∀ {α : Type u_3} {m : MeasurableSpace α} {C : (s : Set α) → MeasurableSet s → Prop} {s : Set (Set α)}
  (h_eq : m = MeasurableSpace.generateFrom s),
  IsPiSystem s →
    C ∅ ⋯ →
      (∀ (t : Set α) (ht : t ∈ s), C t ⋯) →
        (∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯) →
          (∀ (f : ℕ → Set α),
              Pairwise (Function.onFun Disjoint f) →
                ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯) →
            ∀ (t : Set α) (ht : MeasurableSet t), C t ht
-- Mathlib.Data.Finset.Sym
Finset.sym2_mono : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → s.sym2 ⊆ t.sym2
-- Std.Time.Zoned.RecurringRule
/-- Returns the `Day.Offset` (days since epoch) for a `TransitionSpec.julian` in the given year.

`Jn`: Julian day 1–365. Feb 29 is never counted, so in a leap year days ≥ 60 are shifted by one.
 -/
Std.Time.TimeZone.TransitionSpec.toEpochDayJulian : Std.Time.Year.Offset → Std.Time.Internal.Bounded.LE 1 365 → Std.Time.Day.Offset
-- Lean.Compiler.IR.Basic
Lean.IR.push : Array Lean.IR.FnBody → Lean.IR.FnBody → Array Lean.IR.FnBody
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_zero : ∀ {x : ENNReal}, x ^ 0 = 1
-- Mathlib.CategoryTheory.Shift.Quotient
/-- Auxiliary definition for `Quotient.liftCommShift`.  -/
CategoryTheory.Quotient.LiftCommShift.iso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        (F : CategoryTheory.Functor C D) →
          (r : HomRel C) →
            {A : Type w} →
              [inst_2 : AddMonoid A] →
                [inst_3 : CategoryTheory.HasShift C A] →
                  [inst_4 : CategoryTheory.HasShift D A] →
                    [inst_5 : r.IsCompatibleWithShift A] →
                      [F.CommShift A] →
                        (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) →
                          (a : A) →
                            (CategoryTheory.shiftFunctor (CategoryTheory.Quotient r) a).comp
                                (CategoryTheory.Quotient.lift r F hF) ≅
                              (CategoryTheory.Quotient.lift r F hF).comp (CategoryTheory.shiftFunctor D a)
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOf.le : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  {i : M →ₗ[R] N} {f : M →ₗ[R] Q} (self : Module.Baer.ExtensionOf i f), i.range ≤ self.domain
-- Mathlib.Topology.AlexandrovDiscrete
DiscreteTopology.toAlexandrovDiscrete : ∀ {α : Type u_3} [inst : TopologicalSpace α] [DiscreteTopology α], AlexandrovDiscrete α
-- Mathlib.CategoryTheory.Limits.Presentation
/-- `X` is the limit of the `Dᵢ` via `sᵢ`.  -/
CategoryTheory.Limits.LimitPresentation.isLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          (self : CategoryTheory.Limits.LimitPresentation J X) → CategoryTheory.Limits.IsLimit { pt := X, π := self.π }