mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Process.HittingTime
/-- Hitting time: given a stochastic process `u` and a set `s`, `hittingAfter u s n` is
the first time `u` is in `s` after time `n` (if `u` does not hit `s` after time `n` then the
hitting time is `⊤`).  -/
MeasureTheory.hittingAfter : {Ω : Type u_1} → {β : Type u_2} → {ι : Type u_3} → [Preorder ι] → [InfSet ι] → (ι → Ω → β) → Set β → ι → Ω → WithTop ι
-- Mathlib.Dynamics.Ergodic.Ergodic
/-- A map `f : α → α` is said to be quasi-ergodic with respect to a measure `μ` if it is
quasi-measure-preserving and pre-ergodic.  -/
QuasiErgodic : {α : Type u_1} → {m : MeasurableSpace α} → (α → α) → autoParam (MeasureTheory.Measure α) QuasiErgodic._auto_1 → Prop
-- Mathlib.LinearAlgebra.Complex.Module
mem_unitary_iff_isStarNormal_and_realPart_sq_add_imaginaryPart_sq_eq_one : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : Module ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A]
  [inst_5 : StarModule ℂ A] {x : A}, x ∈ unitary A ↔ IsStarNormal x ∧ ↑(realPart x) ^ 2 + ↑(imaginaryPart x) ^ 2 = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasDerivAt.ccosh : ∀ {f : ℂ → ℂ} {f' x : ℂ}, HasDerivAt f f' x → HasDerivAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) * f') x
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
CategoryTheory.Iso.toIsometryEquiv_trans : ∀ {R : Type u} [inst : CommRing R] {X Y Z : QuadraticModuleCat R} (e : X ≅ Y) (f : Y ≅ Z),
  (e ≪≫ f).toIsometryEquiv = e.toIsometryEquiv.trans f.toIsometryEquiv
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_keys : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, m.keys.contains k = m.contains k
-- Mathlib.Order.Filter.Pi
/-- The indexed product of a (possibly, infinite) family of pure filters `pure (f i)`
is generated by the sets of functions that are equal to `f` on a finite set.

If the index type is finite, then the indexed product of pure filters is a pure filter,
see `pi_pure`.  -/
Filter.hasBasis_pi_pure : ∀ {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → α i),
  (Filter.pi fun i => pure (f i)).HasBasis Set.Finite fun I => {g | ∀ i ∈ I, g i = f i}
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.closedCell_zero_eq_singleton`. -/
Topology.CWComplex.closedCell_zero_eq_singleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  {j : Topology.RelCWComplex.cell C 0}, Topology.RelCWComplex.closedCell 0 j = {↑(Topology.RelCWComplex.map 0 j) ![]}
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitStatus.resolved.sizeOf_spec : sizeOf Lean.Meta.Grind.SplitStatus.resolved = 1
-- Batteries.Data.Array.Basic
/-- Fold a function `f` over the array from the right, returning the array of partial results.
```
scanr (· + ·) 0 #[1, 2, 3] = #[6, 5, 3, 0]
```
 -/
Array.scanr : {α : Type u_1} → {β : Type u_2} → (α → β → β) → β → (as : Array α) → optParam ℕ as.size → optParam ℕ 0 → Array β
-- Mathlib.Data.ENat.Basic
ENat.ne_top_iff_exists : ∀ {n : ℕ∞}, n ≠ ⊤ ↔ ∃ m, ↑m = n
-- Mathlib.Analysis.Normed.Group.Defs
NormedGroup.toSeminormedGroup : {E : Type u_5} → [NormedGroup E] → SeminormedGroup E
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
/-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is a principal ring
and `L` has no zero smul divisors by `A`, the integral closure `C` of `A` in `L` is
a free `A`-module.  -/
IsIntegralClosure.module_free : ∀ (A : Type u_1) (K : Type u_2) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  (L : Type u_3) [inst_4 : Field L] (C : Type u_4) [inst_5 : CommRing C] [inst_6 : Algebra K L] [inst_7 : Algebra A L]
  [IsScalarTower A K L] [inst_9 : Algebra C L] [IsIntegralClosure C A L] [inst_11 : Algebra A C] [IsScalarTower A C L]
  [FiniteDimensional K L] [IsDomain A] [Algebra.IsSeparable K L] [Module.IsTorsionFree A L] [IsPrincipalIdealRing A],
  Module.Free A C
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_insertIfNew_le_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α} {v : β}
  {he : t.isEmpty = false}, (cmp ((t.insertIfNew k v).minKey ⋯) (t.minKey he)).isLE = true
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.State.mk.inj : ∀ {cache : Lean.Meta.Simp.Cache} {congrCache : Lean.Meta.Simp.CongrCache} {dsimpCache : Lean.ExprStructMap Lean.Expr}
  {usedTheorems : Lean.Meta.Simp.UsedSimps} {numSteps : ℕ} {diag : Lean.Meta.Simp.Diagnostics}
  {cache_1 : Lean.Meta.Simp.Cache} {congrCache_1 : Lean.Meta.Simp.CongrCache}
  {dsimpCache_1 : Lean.ExprStructMap Lean.Expr} {usedTheorems_1 : Lean.Meta.Simp.UsedSimps} {numSteps_1 : ℕ}
  {diag_1 : Lean.Meta.Simp.Diagnostics},
  { cache := cache, congrCache := congrCache, dsimpCache := dsimpCache, usedTheorems := usedTheorems,
        numSteps := numSteps, diag := diag } =
      { cache := cache_1, congrCache := congrCache_1, dsimpCache := dsimpCache_1, usedTheorems := usedTheorems_1,
        numSteps := numSteps_1, diag := diag_1 } →
    cache = cache_1 ∧
      congrCache = congrCache_1 ∧
        dsimpCache = dsimpCache_1 ∧ usedTheorems = usedTheorems_1 ∧ numSteps = numSteps_1 ∧ diag = diag_1
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.apply_coe_mem_map : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) (x : ↥S), f ↑x ∈ Submonoid.map f S
-- Mathlib.Data.Option.Defs
/-- Traverse an object of `Option α` with a function `f : α → F β` for an applicative `F`.  -/
Option.traverse : {F : Type u → Type v} → [Applicative F] → {α : Type u_1} → {β : Type u} → (α → F β) → Option α → F (Option β)
-- Mathlib.Algebra.Group.Basic
zpow_natCast_sub_natCast : ∀ {G : Type u_3} [inst : Group G] (a : G) (m n : ℕ), a ^ (↑m - ↑n) = a ^ m / a ^ n
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_toAddSubgroup : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f : M →ₛₗ[τ₁₂] M₂), f.ker.toAddSubgroup = f.toAddMonoidHom.ker
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_eq_iff : ∀ {a : ℤ} {b : ℕ} {c : ℤ}, 0 < b → (a.bmod b = c ↔ -(↑b / 2) ≤ c ∧ c < (↑b + 1) / 2 ∧ ↑b ∣ c - a)
-- Mathlib.Computability.DFA
DFA.reindex_apply_accept : ∀ {α : Type u} {σ : Type v} {σ' : Type u_2} (g : σ ≃ σ') (M : DFA α σ),
  ((DFA.reindex g) M).accept = ⇑g.symm ⁻¹' M.accept
-- Mathlib.Algebra.Group.Subsemigroup.Membership
Subsemigroup.mem_iSup_prop : ∀ {M : Type u_2} [inst : Mul M] {p : Prop} {S : p → Subsemigroup M} {x : M}, x ∈ ⨆ (h : p), S h ↔ ∃ (h : p), x ∈ S h
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.toList_eq_toList_roi : ∀ {α : Type u} {r : Std.Rci α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α], r.toList = r.lower :: r.lower<...*.toList
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.RatAlgebra.dpow.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (I : Ideal R) [inst_1 : DecidablePred fun x => x ∈ I],
  DividedPowers.RatAlgebra.dpow I = DividedPowers.OfInvertibleFactorial.dpow I
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- To check whether two maps are coequalized by both maps of a cotrident, it suffices to check it
for the second map  -/
CategoryTheory.Limits.Cotrident.coequalizer_ext : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J]
  (s : CategoryTheory.Limits.Cotrident f) {W : C} {k l : s.pt ⟶ W},
  CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l →
    ∀ (j : CategoryTheory.Limits.WalkingParallelFamily J),
      CategoryTheory.CategoryStruct.comp (s.ι.app j) k = CategoryTheory.CategoryStruct.comp (s.ι.app j) l
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.extractBind : Option Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Term.ExtractMonadResult
-- Mathlib.Data.Seq.Defs
/-- Applies `f` to the `n`th element of the sequence, if it exists, replacing that element
with the result.  -/
Stream'.Seq.update : {α : Type u} → Stream'.Seq α → ℕ → (α → α) → Stream'.Seq α
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun_iff : ∀ {Ω : Type u_1} {x : MeasurableSpace Ω} {β : Type u_7} {γ : Type u_8} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ]
  (f : Ω → β) (g : Ω → γ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.IndepFun f g μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv_apply' : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (i j : n),
  (LinearMap.toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i
-- Mathlib.Algebra.Algebra.Operations
Submodule.mapHom_apply : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {A' : Type u_1}
  [inst_3 : Semiring A'] [inst_4 : Algebra R A'] (f : A →ₐ[R] A') (p : Submodule R A),
  (Submodule.mapHom f) p = Submodule.map f.toLinearMap p
-- Mathlib.Analysis.Complex.Positivity
/-- An entire function whose iterated derivatives at `c` are all nonnegative real (except
possibly the value itself) has values of the form `f c + nonneg. real` on the set `c + ℝ≥0`.  -/
Differentiable.apply_le_of_iteratedDeriv_nonneg : ∀ {f : ℂ → ℂ} {c : ℂ}, Differentiable ℂ f → (∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c) → ∀ ⦃z : ℂ⦄, c ≤ z → f c ≤ f z
-- Mathlib.CategoryTheory.Limits.Sifted
CategoryTheory.IsSifted.toFinal : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsSifted C],
  (CategoryTheory.Functor.diag C).Final
-- Init.Data.Array.GetLit
_private.Init.Data.Array.GetLit.0.Array.toArrayLit_eq.go : ∀ {α : Type u_1} (xs : Array α) (n : ℕ) (hsz : xs.size = n) (i : ℕ) (hi : i ≤ xs.size),
  xs.toListLitAux n hsz i hi (List.drop i xs.toList) = xs.toList
-- Init.Data.Vector.Lex
_private.Init.Data.Vector.Lex.0.Break.runK.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.id : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {k : ℕ} {α : ↑unitInterval} {a : E},
  ContDiffPointwiseHolderAt k α id a
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Enriched.Functor.whiskerRight_app_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (K L M N : CategoryTheory.Functor C D)
  (f : CategoryTheory.MonoidalCategoryStruct.tensorObj (K.functorHom L) (L.functorHom M) ⟶ K.functorHom M) {X : C}
  (a :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (K.functorHom L) (L.functorHom M)) (M.functorHom N)).obj
      X),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (f.app X)
          ((M.homObjFunctor N).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X))))))
      a =
    ((CategoryTheory.ConcreteCategory.hom (f.app X)) a.1, a.2)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.Indep.eq_empty_of_subset_loops : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → I ⊆ M.loops → I = ∅
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- The center of a special linear group of degree `n` is the subgroup of scalar matrices, for which
the scalars are the `n`-th roots of unity.  -/
Matrix.SpecialLinearGroup.mem_center_iff : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  {A : Matrix.SpecialLinearGroup n R},
  A ∈ Subgroup.center (Matrix.SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (Matrix.scalar n) r = ↑A
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isCoboundary₁_of_mem_coboundaries₁ : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A],
  ∀ f ∈ groupCohomology.coboundaries₁ (Rep.ofDistribMulAction k G A), groupCohomology.IsCoboundary₁ f
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- **Alias** of `OpenPartialHomeomorph.replacePartialEquiv`.

---

Replace `toPartialEquiv` field to provide better definitional equalities.  -/
OpenPartialHomeomorph.replaceEquiv : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e : OpenPartialHomeomorph X Y) → (e' : PartialEquiv X Y) → e.toPartialEquiv = e' → OpenPartialHomeomorph X Y
-- Mathlib.Analysis.Calculus.Deriv.Add
hasDerivAt_add_const_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F),
  HasDerivAt (fun x => f x + c) f' x ↔ HasDerivAt f f' x
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatMarkerShort : Std.Time.DateFormatSymbols → Std.Time.HourMarker → String
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.whiskerLeft_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} (f : G ⟶ H) (I : CategoryTheory.Grp C),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f I).hom.hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom.hom I.X
-- Mathlib.Order.Category.Frm
Frm.hom_comp : ∀ {X Y Z : Frm} (f : X ⟶ Y) (g : Y ⟶ Z),
  Frm.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Frm.Hom.hom g).comp (Frm.Hom.hom f)
-- Init.Data.Nat.ToString
Nat.digitChar_eq_eight : ∀ {n : ℕ}, n.digitChar = '8' ↔ n = 8
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.max?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.max? = t₂.max?
-- Batteries.Recycling.RBTree.Basic
/-- Returns `black` if the node is black, otherwise `red`.
(Nil nodes are treated as `red`, which is not the usual convention but useful for deletion.)
 -/
RBTree.RBNode.isBlack : {α : Type u_1} → RBTree.RBNode α → RBTree.RBColor
-- Mathlib.Order.Filter.Map
Filter.neBot_inf_comap_iff_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {F : Filter α} {G : Filter β},
  (F ⊓ Filter.comap f G).NeBot ↔ (Filter.map f F ⊓ G).NeBot
-- Mathlib.Tactic.Ring.Common
/-- Returns whether two coefficients are equal  -/
Mathlib.Tactic.Ring.Common.RingCompare.eq : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      Mathlib.Tactic.Ring.Common.RingCompare BaseType → {x y : Q(«$α»)} → BaseType x → BaseType y → Bool
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_last : ∀ {w : ℕ} (x : BitVec w), x.getLsbD (w - 1) = decide (2 ^ (w - 1) ≤ x.toNat)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace_zero : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R}, (f.genEigenspace μ) 0 = ⊥
-- Mathlib.Order.Filter.Map
Filter.comap_id' : ∀ {α : Type u_1} {f : Filter α}, Filter.comap (fun x => x) f = f
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toComon_map_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.Comon (CategoryTheory.Mon C)} (f : X ⟶ Y),
  ((CategoryTheory.Bimon.toComon C).map f).hom = f.hom.hom
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mk_eq_monoidOf_mk'_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (x : M) (y : ↥S),
  Localization.mk x y = (Localization.monoidOf S).mk' x y
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.get? (t.maxD fallback) = some (t.maxD fallback)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftUnitorNatIso_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategory.leftUnitorNatIso C).inv.app X =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.eval.eq_3 : Std.Tactic.BVDecide.Gate.beq.eval = fun x1 x2 => x1 == x2
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.mk.inj : ∀ {recursorName typeName : Lean.Name} {univLevelPos : List Lean.Meta.RecursorUnivLevelPos} {depElim recursive : Bool}
  {numArgs majorPos : ℕ} {paramsPos : List (Option ℕ)} {indicesPos : List ℕ} {produceMotive : List Bool}
  {recursorName_1 typeName_1 : Lean.Name} {univLevelPos_1 : List Lean.Meta.RecursorUnivLevelPos}
  {depElim_1 recursive_1 : Bool} {numArgs_1 majorPos_1 : ℕ} {paramsPos_1 : List (Option ℕ)} {indicesPos_1 : List ℕ}
  {produceMotive_1 : List Bool},
  { recursorName := recursorName, typeName := typeName, univLevelPos := univLevelPos, depElim := depElim,
        recursive := recursive, numArgs := numArgs, majorPos := majorPos, paramsPos := paramsPos,
        indicesPos := indicesPos, produceMotive := produceMotive } =
      { recursorName := recursorName_1, typeName := typeName_1, univLevelPos := univLevelPos_1, depElim := depElim_1,
        recursive := recursive_1, numArgs := numArgs_1, majorPos := majorPos_1, paramsPos := paramsPos_1,
        indicesPos := indicesPos_1, produceMotive := produceMotive_1 } →
    recursorName = recursorName_1 ∧
      typeName = typeName_1 ∧
        univLevelPos = univLevelPos_1 ∧
          depElim = depElim_1 ∧
            recursive = recursive_1 ∧
              numArgs = numArgs_1 ∧
                majorPos = majorPos_1 ∧
                  paramsPos = paramsPos_1 ∧ indicesPos = indicesPos_1 ∧ produceMotive = produceMotive_1
-- Init.Data.BitVec.Lemmas
BitVec.xor_right_inj : ∀ {w : ℕ} {x y : BitVec w} (z : BitVec w), z ^^^ x = z ^^^ y ↔ x = y
-- Std.Http.Data.Method
Std.Http.Method.mkredirectref.sizeOf_spec : sizeOf Std.Http.Method.mkredirectref = 1
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.exp_injective : ∀ {M : Type u_4}, Function.Injective WithZero.exp
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.mkD_apply_of_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {g : C(α, β)}
  {x : α}, Continuous f → (ContinuousMap.mkD f g) x = f x
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.homEquiv'_app_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R}
  {cM : CategoryTheory.Limits.Cocone M.presheaf} (hcM : CategoryTheory.Limits.IsColimit cM) {N : ModuleCat ↑cR.pt}
  (α : PresheafOfModules.ModuleColimit hcR hcM →+ ↑N) {X : Cᵒᵖ} (x : ↑(M.obj X)),
  (CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.ModuleColimit.homEquiv' hcR hcM) α).app X)) x =
    α ((CategoryTheory.ConcreteCategory.hom (cM.ι.app X)) x)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionList.items : Lean.Lsp.ResolvableCompletionList → Array Lean.Lsp.ResolvableCompletionItem
-- Mathlib.Order.Atoms
GaloisCoinsertion.isAtom_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α]
  [inst_3 : OrderBot β] [IsAtomic β] {l : α → β} {u : β → α} (gi : GaloisCoinsertion l u),
  (∀ (b : β), IsAtom b → l (u b) = b) → ∀ (a : α), IsAtom (l a) ↔ IsAtom a
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanIso.comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid γ] {A : Set α} {B : Set β} {C : Set γ} {f : α → β} {g : β → γ} {n : ℕ},
  IsAddFreimanIso n B C g → IsAddFreimanIso n A B f → IsAddFreimanIso n A C (g ∘ f)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLE.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.eq) → (Unit → motive Ordering.gt) → motive x
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.subtype_comp_inclusion : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂),
  S₂.subtype.comp (StarSubalgebra.inclusion h) = S₁.subtype
-- Aesop.Tree.Check
Aesop.MVarClusterRef.checkAcyclic : Aesop.MVarClusterRef → Lean.CoreM Unit
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `𝔖 : Set (Set α)` is nonempty and directed, then the uniformity of `α →ᵤ[𝔖] β` admits the
family `{(f, g) | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and `V ∈ 𝓤 β` as a filter basis.  -/
UniformOnFun.hasBasis_uniformity : ∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      (uniformity (UniformOnFun α β 𝔖)).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ uniformity β) fun SV =>
        UniformOnFun.gen 𝔖 SV.1 SV.2
-- Batteries.Data.List.Perm
List.Subperm.trans : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁.Subperm l₂ → l₂.Subperm l₃ → l₁.Subperm l₃
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a : α},
  m.contains a = false → m.get? a = none
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
IsStrictlyPositive.commute_iff : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : PartialOrder A] [inst_2 : StarRing A] [StarOrderedRing A]
  [inst_4 : TopologicalSpace A] [inst_5 : Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [NonnegSpectrumClass ℝ A] {a b : A},
  IsStrictlyPositive a → IsStrictlyPositive b → (Commute a b ↔ IsStrictlyPositive (a * b))
-- Lean.Parser.Types
Lean.Parser.SyntaxStack.size : Lean.Parser.SyntaxStack → ℕ
-- Lean.Elab.Tactic.BuiltinTactic
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goOdd : Lean.Syntax → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Connected.of_isUniversal : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, G.IsUniversal v → G.Connected
-- Init.Data.Nat.Lemmas
Nat.sub_mul_mod : ∀ {x k n : ℕ}, n * k ≤ x → (x - n * k) % n = x % n
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.isPublic : Lean.Elab.Modifiers → Bool
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.List.toArrayAux.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (a : α) (as : List α) (xs : Array α)
  (h_1 : (xs : Array α) → motive [] xs) (h_2 : (a : α) → (as : List α) → (xs : Array α) → motive (a :: as) xs),
  (match a :: as, xs with
    | [], xs => h_1 xs
    | a :: as, xs => h_2 a as xs) =
    h_2 a as xs
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicones.functoriality_obj_ι : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] (A : CategoryTheory.Limits.Bicone F) (j : J),
  ((CategoryTheory.Limits.Bicones.functoriality F G).obj A).ι j = G.map (A.ι j)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.contains (t.minKeyD fallback) = true