mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₁.ιLeft.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] {X Y : C} (f f_1 : X ⟶ Y)
  (e_f : f = f_1) (hf : W f) (g g_1 : X ⟶ Z),
  g = g_1 → CategoryTheory.OrthogonalReflection.D₁.ιLeft f hf g = CategoryTheory.OrthogonalReflection.D₁.ιLeft f_1 ⋯ g_1
-- Mathlib.MeasureTheory.Order.Group.Lattice
Measurable.oneLePart : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Group α] [inst_2 : MeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} [MeasurableSup α], Measurable f → Measurable fun x => (f x)⁺ᵐ
-- Mathlib.RingTheory.Finiteness.Finsupp
LinearMap.finsuppLinearMap_apply_apply_support : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} (S : Type u_5) [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N]
  [inst_5 : Semiring S] [inst_6 : Module S N] [inst_7 : SMulCommClass R S N] (m : ι →₀ M →ₗ[R] N) (m_1 : M),
  (((LinearMap.finsuppLinearMap S) m) m_1).support = Finsupp.onFinsetSupport m.support (⇑(LinearMap.id.flip m_1) ∘ ⇑m)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The canonical linear homeomorphism between `EuclideanSpace 𝕜 (ι ⊕ κ)` and
`EuclideanSpace 𝕜 ι × EuclideanSpace 𝕜 κ`.

See `PiLp.sumPiLpEquivProdLpPiLp` for the isometry version,
where the RHS is equipped with the Euclidean norm rather than the supremum norm.  -/
EuclideanSpace.sumEquivProd : {𝕜 : Type u_7} →
  [inst : RCLike 𝕜] →
    {ι : Type u_8} →
      {κ : Type u_9} →
        [Fintype ι] → [Fintype κ] → EuclideanSpace 𝕜 (ι ⊕ κ) ≃L[𝕜] EuclideanSpace 𝕜 ι × EuclideanSpace 𝕜 κ
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_cylinder : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {s : Finset ι} {S : Set ((i : ↥s) → X ↑i)},
  MeasurableSet S →
    (MeasureTheory.Measure.infinitePi μ) (MeasureTheory.cylinder s S) = (MeasureTheory.Measure.pi fun i => μ ↑i) S
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ιMulti.eq_1 : ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ),
  ExteriorAlgebra.ιMulti R n =
    { toFun := ⇑((MultilinearMap.mkPiAlgebraFin R n (ExteriorAlgebra R M)).compLinearMap fun x => ExteriorAlgebra.ι R),
      map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ }
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.JPDecl : Type
-- Mathlib.Data.List.Sigma
List.Perm.kunion : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {l₁ l₂ l₃ l₄ : List (Sigma β)},
  l₃.NodupKeys → l₁.Perm l₂ → l₃.Perm l₄ → (l₁.kunion l₃).Perm (l₂.kunion l₄)
-- Std.Http.Data.Version
Std.Http.instDecidableEqVersion : DecidableEq Std.Http.Version
-- Mathlib.Data.Set.Function
Set.InjOn.injective_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} (s : Set β),
  Set.InjOn g s → Set.range f ⊆ s → (Function.Injective (g ∘ f) ↔ Function.Injective f)
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabInfo.mk.sizeOf_spec : ∀ (toElabInfo : Lean.Elab.ElabInfo) (name : Lean.Name) (kind : Lean.Elab.DocElabKind),
  sizeOf { toElabInfo := toElabInfo, name := name, kind := kind } = 1 + sizeOf toElabInfo + sizeOf name + sizeOf kind
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBySet_iff_torsionBySet_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Module.IsTorsionBySet R M s ↔ Submodule.torsionBySet R M s = ⊤
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualRestrict_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (W : Submodule R M) (φ : Module.Dual R M) (x : ↥W), (W.dualRestrict φ) x = φ ↑x
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ArbitraryShiftTarget.n : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {m : ℕ} → aig.ArbitraryShiftTarget m → ℕ
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.orderIsoMapComap_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {σ₂₁ : R₂ →+* R} [inst_7 : RingHomInvPair σ₁₂ σ₂₁] [inst_8 : RingHomInvPair σ₂₁ σ₁₂]
  (f : M ≃ₛₗ[σ₁₂] M₂) (p : Submodule R₂ M₂), (Submodule.orderIsoMapComap f).symm p = Submodule.comap (↑f) p
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Monad.left_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R),
  L.comp (CategoryTheory.Monad.comparison h) = h.toMonad.free
-- Init.Data.Array.Basic
/-- Appends two arrays. Normally used via the `++` operator.

Appending arrays takes time proportional to the length of the second array.

Examples:
* `#[1, 2, 3] ++ #[4, 5] = #[1, 2, 3, 4, 5]`.
* `#[] ++ #[4, 5] = #[4, 5]`.
* `#[1, 2, 3] ++ #[] = #[1, 2, 3]`.
 -/
Array.append : {α : Type u} → Array α → Array α → Array α
-- Mathlib.Topology.Continuous
continuousAt_congr : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X}
  {g : X → Y}, f =ᶠ[nhds x] g → (ContinuousAt f x ↔ ContinuousAt g x)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.OverArrows.map₂_val : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A}
  {X Y : C} (f : X ⟶ Y) {s : CategoryTheory.yoneda.obj X ⟶ A} {t : CategoryTheory.yoneda.obj Y ⟶ A}
  (hst : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s)
  (u : CategoryTheory.OverPresheafAux.OverArrows η t),
  (u.map₂ f hst).val = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) u.val
-- Aesop.Forward.LevelIndex
Aesop.LevelIndex.mk.sizeOf_spec : ∀ (toNat : ℕ), sizeOf { toNat := toNat } = 1 + sizeOf toNat
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.MonCat.Hom.mk.sizeOf_spec : ∀ {A B : MonCat} (hom' : ↑A →* ↑B), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.RingTheory.Coprime.Lemmas
Fintype.prod_dvd_of_coprime : ∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {z : R} {s : I → R} [inst_1 : Fintype I],
  Pairwise (Function.onFun IsCoprime s) → (∀ (i : I), s i ∣ z) → ∏ x, s x ∣ z
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
/-- If `R` and `T` are isomorphic commutative rings and `S` is an `R`-algebra and a `T`-algebra in
a compatible way, then an element `a ∈ S` is integral over `R` if and only if it is integral
over `T`.  -/
RingEquiv.isIntegral_iff : ∀ {R : Type u_5} {S : Type u_6} {T : Type u_7} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra T S] (φ : R ≃+* T),
  (algebraMap T S).comp φ.toRingHom = algebraMap R S → ∀ (a : S), IsIntegral R a ↔ IsIntegral T a
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_eq_one : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : NonAssocSemiring α] [inst_2 : StarRing α]
  {M : Matrix n n α}, M.conjTranspose = 1 ↔ M = 1
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.ofEq_apply : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y) (a : X), (MulActionHom.ofEq h f) a = f a
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
/-- Two finite Borel measures are equal if the integrals of all bounded continuous functions with
respect to both agree.  -/
MeasureTheory.ext_of_forall_integral_eq_of_IsFiniteMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [HasOuterApproxClosed Ω] [BorelSpace Ω]
  {μ ν : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν],
  (∀ (f : BoundedContinuousFunction Ω ℝ), ∫ (x : Ω), f x ∂μ = ∫ (x : Ω), f x ∂ν) → μ = ν
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_cosh : ∀ (x : ℝ), ↑(Real.cosh x) = Complex.cosh ↑x
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.map_one : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) [IsDomain S] [Nontrivial R], abv 1 = 1
-- Mathlib.RingTheory.Algebraic.MvPolynomial
MvPolynomial.transcendental_polynomial_aeval_X_iff : ∀ {σ : Type u_1} (R : Type u_2) [inst : CommRing R] (i : σ) {f : Polynomial R},
  Transcendental R ((Polynomial.aeval (MvPolynomial.X i)) f) ↔ Transcendental R f
-- Mathlib.Algebra.Group.Action.Defs
zero_vadd : ∀ (M : Type u_1) {α : Type u_5} [inst : AddMonoid M] [inst_1 : AddAction M α] (b : α), 0 +ᵥ b = b
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
/-- A non-cyclic multiplicative group is non-trivial.  -/
Nontrivial.of_not_isCyclic : ∀ {α : Type u_1} [inst : Group α], ¬IsCyclic α → Nontrivial α
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- A functor `F` preserves finite products if it reflects limits of shape `Discrete J` for finite `J`.
We require this for `J = Fin n` in the definition,
then generalize to `J : Type u` in the instance.
 -/
CategoryTheory.Limits.ReflectsFiniteProducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precomposeEquivalence_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G),
  (CategoryTheory.Limits.Cocone.precomposeEquivalence α).unitIso =
    CategoryTheory.NatIso.ofComponents'
      (fun s =>
        CategoryTheory.Limits.Cocone.extInv
          (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)).obj s).pt) ⋯)
      ⋯
-- Aesop.Script.UScriptToSScript
_private.Aesop.Script.UScriptToSScript.0.Aesop.Script.UScript.toStepTree.go : Std.HashMap Lean.MVarId (ℕ × Aesop.Script.Step) → Lean.MVarId → Aesop.Script.StepTree
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.foldl.match_1.splitter : {α : Type u_3} →
  {β : Type u_1} →
    (motive : α → List β → Sort u_2) →
      (x : α) →
        (x_1 : List β) → ((a : α) → motive a []) → ((a : α) → (b : β) → (l : List β) → motive a (b :: l)) → motive x x_1
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.leadingCoeff_eq : ∀ {R : Type u_1} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.IsMonicOfDegree n → p.leadingCoeff = 1
-- Mathlib.Data.Multiset.MapFold
Multiset.nodup_map_iff_of_injective : ∀ {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β}, Function.Injective f → ((Multiset.map f s).Nodup ↔ s.Nodup)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.rightExactFunctor_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D),
  CategoryTheory.rightExactFunctor C D F ↔ CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.Algebra.Order.Quantale
Quantale.instMulLeftMono : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : CompleteLattice α] [IsQuantale α], MulLeftMono α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isSome_maxKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : β → β}, (Std.DTreeMap.Const.modify t k f).maxKey?.isSome = !t.isEmpty
-- Mathlib.Data.Finmap
Finmap.keys_erase_toFinset : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : AList β),
  (AList.erase a s).toFinmap.keys = s.toFinmap.keys.erase a
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- `post (Over.forget X) : Over f ⥤ Over (forget.obj f)` is naturally isomorphic to the
functor `Over.iteratedSliceForward : Over f ⥤ Over f.left`.  -/
CategoryTheory.Over.iteratedSliceForwardIsoPost : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    (X : T) →
      (f : CategoryTheory.Over X) → CategoryTheory.Over.post (CategoryTheory.Over.forget X) ≅ f.iteratedSliceForward
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.instOrderBot : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : Ring 𝕜] →
      [inst_1 : PartialOrder 𝕜] →
        [inst_2 : AddCommGroup E] → [inst_3 : Module 𝕜 E] → OrderBot (Geometry.SimplicialComplex 𝕜 E)
-- Mathlib.Data.List.AList
AList.keys_replace : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) (s : AList β),
  (AList.replace a b s).keys = s.keys
-- Mathlib.MeasureTheory.PiSystem
/-- Every element of the π-system generated by the union of a family of π-systems
is a finite intersection of elements from the π-systems.
For an indexed union version, see `mem_generatePiSystem_iUnion_elim'`.  -/
mem_generatePiSystem_iUnion_elim : ∀ {α : Type u_3} {β : Type u_4} {g : β → Set (Set α)},
  (∀ (b : β), IsPiSystem (g b)) → ∀ t ∈ generatePiSystem (⋃ b, g b), ∃ T f, t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.mk_left_unitor_inv : ∀ {B : Type u} [inst : Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b),
  Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv f) =
    (CategoryTheory.Bicategory.leftUnitor f).inv
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.natEnd.match_1.splitter : (motive : Turing.PartrecToTM2.Γ' → Sort u_1) →
  (x : Turing.PartrecToTM2.Γ') →
    (Unit → motive Turing.PartrecToTM2.Γ'.consₗ) →
      (Unit → motive Turing.PartrecToTM2.Γ'.cons) →
        ((x : Turing.PartrecToTM2.Γ') →
            (x = Turing.PartrecToTM2.Γ'.consₗ → False) → (x = Turing.PartrecToTM2.Γ'.cons → False) → motive x) →
          motive x
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.coe_smul_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] (a : α) (s : Finset β), ↑(a • s) = a • ↑s
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_leftUnitor_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) [inst_4 : F.Monoidal] (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.η F) (F.obj X))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h))
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.equiv_rootD_l : ∀ {self : Batteries.UnionFind} {a b : ℕ}, self.Equiv (self.rootD a) b ↔ self.Equiv a b
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instTop : {α : Type u_1} → [inst : LE α] → Top (LowerSet α)
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_const_smul_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} {c : 𝕜},
  DifferentiableWithinAt 𝕜 W s x →
    UniqueDiffWithinAt 𝕜 s x → VectorField.lieBracketWithin 𝕜 V (c • W) s x = c • VectorField.lieBracketWithin 𝕜 V W s x
-- Lean.Data.Position
/-- Content of a file together with precalculated positions of newlines.  -/
Lean.FileMap : Type
-- Init.Data.Nat.Lemmas
Nat.le_of_sub_le_sub_left : ∀ {n k m : ℕ}, n ≤ k → k - m ≤ k - n → n ≤ m
-- Mathlib.CategoryTheory.Localization.Resolution
/-- A localizer morphism has right resolutions when any object has a right resolution.  -/
CategoryTheory.LocalizerMorphism.HasRightResolutions : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} → CategoryTheory.LocalizerMorphism W₁ W₂ → Prop
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.forIn'_toList_eq_forIn' : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)},
  forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).minKey ⋯ = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Lean.Expr
Lean.instForInFVarIdSetFVarIdOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForIn m Lean.FVarIdSet Lean.FVarId
-- Mathlib.Topology.Order.LowerUpperTopology
sSupHom.continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] [inst_2 : TopologicalSpace α]
  [Topology.IsUpper α] [inst_4 : TopologicalSpace β] [Topology.IsUpper β] (f : sSupHom α β), Continuous ⇑f
-- Mathlib.Data.Fin.SuccPred
/-- Embedding `i : Fin n` into `Fin (n + 1)` using a pivot `p` that is greater
results in a value that is less than `p`.  -/
Fin.succAbove_lt_iff_castSucc_lt : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p.succAbove i < p ↔ i.castSucc < p
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.val_mk : ∀ {α : Type u} [inst : AddMonoid α] (a b : α) (h₁ : a + b = 0) (h₂ : b + a = 0),
  ↑{ val := a, neg := b, val_neg := h₁, neg_val := h₂ } = a
-- Mathlib.Combinatorics.Quiver.Push
Quiver.Push.of_obj : ∀ {V : Type u_1} [inst : Quiver V] {W : Type u_2} (σ : V → W), (Quiver.Push.of σ).obj = σ
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
CategoryTheory.Preadditive.epi_iff_surjective' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [(CategoryTheory.forget₂ C Ab).PreservesHomology]
  [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Topology.UniformSpace.Completion
/-- The map from a uniform space to its completion.  -/
UniformSpace.Completion.coe' : {α : Type u_1} → [inst : UniformSpace α] → α → UniformSpace.Completion α
-- Init.Data.Option.Lemmas
Option.get!_eq_getD : ∀ {α : Type u_1} [inst : Inhabited α] (o : Option α), o.get! = o.getD default
-- Init.Data.SInt.Bitwise
Int8.neg_one_xor : ∀ {a : Int8}, -1 ^^^ a = ~~~a
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.category_id_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.CategoryStruct.id sq).τ₂ = CategoryTheory.CategoryStruct.id sq.X₂
-- Mathlib.Data.Rel
SetRel.isSymm_comp_inv : ∀ {α : Type u_1} {R : SetRel α α}, (R.comp R.inv).IsSymm
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.ω₁_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (D : CategoryTheory.ComposableArrows EInt 1),
  t.ω₁.obj D = (t.eTruncLT.obj (D.obj 1)).comp (t.eTruncGE.obj (D.obj 0))
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.nullMeasurableSet : ∀ {G : Type u_1} {α : Type u_2} [inst : One G] [inst_1 : SMul G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : autoParam (MeasureTheory.Measure α) MeasureTheory.IsFundamentalDomain._auto_1},
  MeasureTheory.IsFundamentalDomain G s μ → MeasureTheory.NullMeasurableSet s μ
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- Borel-measurable sets are measurable.  -/
OpensMeasurableSpace.borel_le : ∀ {α : Type u_6} {inst : TopologicalSpace α} {h : MeasurableSpace α} [self : OpensMeasurableSpace α], borel α ≤ h
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.coe_singletonZeroHom : ∀ {α : Type u_2} [inst : Zero α], ⇑Set.singletonZeroHom = singleton
-- Lean.Server.GoTo
Lean.Server.GoToKind.declaration : Lean.Server.GoToKind
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalClosure_eq_self : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [H.Normal], Subgroup.normalClosure ↑H = H
-- Mathlib.Algebra.BigOperators.Ring.Finset
Int.cast_list_prod : ∀ {R : Type u_4} [inst : Ring R] (s : List ℤ), ↑s.prod = (List.map Int.cast s).prod
-- Mathlib.Data.Fin.Embedding
/-- `Fin.natAdd_castLEEmb` as an `Embedding` from `Fin n` to `Fin m`, by appending the former
at the end of the latter.
`natAdd_castLEEmb hmn i` maps `i : Fin m` to `i + (m - n) : Fin n` by adding `m - n` to `i`  -/
Fin.natAdd_castLEEmb : {n m : ℕ} → n ≤ m → Fin n ↪ Fin m
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.smul_left_def : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : Semiring R]
  (v : AbsoluteValue R S) [inst_3 : SMul R T] (x : WithAbs v) (t : T), x • t = x.ofAbs • t
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- The compatibility morphisms after pullbacks. It follows from the conditions
`hom_self` and `hom_comp` that these are isomorphisms, see
`CategoryTheory.Pseudofunctor.DescentData.iso` below.  -/
CategoryTheory.Pseudofunctor.DescentData.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              (self : F.DescentData f) →
                ⦃Y : C⦄ →
                  (q : Y ⟶ S) →
                    ⦃i₁ i₂ : ι⦄ →
                      (f₁ : Y ⟶ X i₁) →
                        (f₂ : Y ⟶ X i₂) →
                          autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                              CategoryTheory.Pseudofunctor.DescentData._auto_1 →
                            autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
                                CategoryTheory.Pseudofunctor.DescentData._auto_3 →
                              ((F.map f₁.op.toLoc).toFunctor.obj (self.obj i₁) ⟶
                                (F.map f₂.op.toLoc).toFunctor.obj (self.obj i₂))
-- Mathlib.Data.PEquiv
PEquiv.symm_injective : ∀ {α : Type u} {β : Type v}, Function.Injective PEquiv.symm
-- Init.Data.Array.BasicAux
_private.Init.Data.Array.BasicAux.0.List.toArrayAux.eq_1 : ∀ {α : Type u_1} (x : Array α), [].toArrayAux x = x
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.tendsto_exp_atBot_nhdsGT : Filter.Tendsto Real.exp Filter.atBot (nhdsWithin 0 (Set.Ioi 0))
-- Lean.Meta.LazyDiscrTree
/-- Get the results of each task and merge using combining function  -/
Lean.Meta.LazyDiscrTree.combineGet : {α : Type u_1} → [Append α] → α → Array (Task α) → α