mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.preservesColimitsOfShape_eq_iSup : ∀ {J : Type u_1} {C : Type u_3} (K : Type u_5) [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} J] [inst_2 : CategoryTheory.Category.{v_5, u_3} C],
  CategoryTheory.ObjectProperty.preservesColimitsOfShape K = ⨅ F, CategoryTheory.ObjectProperty.preservesColimit F
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.le_topologicalClosure : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A] (s : StarSubalgebra R A), s ≤ s.topologicalClosure
-- Init.Data.Vector.Basic
/-- Extract the first `i` elements of a vector. If `i` is greater than or equal to the size of the
vector then the vector is returned unchanged.

We immediately simplify this to the `extract` operation, so there is no verification API for this function.
 -/
Vector.take : {α : Type u_1} → {n : ℕ} → Vector α n → (i : ℕ) → Vector α (min i n)
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.fiberPullbackEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] {X A B : C}
  (f : A ⟶ X) (g : B ⟶ X),
  CategoryTheory.PreGaloisCategory.fiberPullbackEquiv F f g =
    (CategoryTheory.Limits.PreservesPullback.iso (F.comp FintypeCat.incl) f g ≪≫
        CategoryTheory.Limits.Types.pullbackIsoPullback (F.map f).hom (F.map g).hom).toEquiv
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.isQuasicoherent_restrictFunctor : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  [SheafOfModules.IsQuasicoherent M],
  SheafOfModules.IsQuasicoherent ((AlgebraicGeometry.Scheme.Modules.restrictFunctor f).obj M)
-- Lean.Elab.Tactic.Induction
/-- Elaborates the `foo args` of `fun_induction` or `fun_cases`, returning the `ElabInfo` and targets.
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.elabFunTarget : Bool → Lean.Syntax → Lean.Elab.Tactic.TacticM (Lean.Meta.ElimInfo × Array Lean.Expr)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.freeGroupCongr_apply : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : FreeGroup α), (FreeGroup.freeGroupCongr e) a = (FreeGroup.map ⇑e) a
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.State.out : Std.Format.State✝ → String
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleMk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p n : ℤ}
  (α : CochainComplex.HomComplex.Cochain ((CochainComplex.singleFunctor C p).obj X) K n) (q : ℤ) (h : p + n = q),
  ∃ f, CochainComplex.HomComplex.Cochain.fromSingleMk f h = α
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.getAddThms : Lean.Meta.Grind.Arith.Cutsat.ToIntM Lean.Meta.Grind.Arith.Cutsat.ToIntThms
-- Mathlib.Algebra.Order.Module.Archimedean
FiniteArchimedeanClass.toAddSubgroup_ball : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (K : Type u_2)
  [inst_3 : Ring K] [inst_4 : LinearOrder K] [inst_5 : IsOrderedRing K] [inst_6 : Archimedean K] [inst_7 : Module K M]
  [inst_8 : PosSMulMono K M] (c : FiniteArchimedeanClass M),
  (FiniteArchimedeanClass.ball K c).toAddSubgroup = c.ballAddSubgroup
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the third quadrant. Let `f : ℂ → E` be a function such that

* `f` is differentiable in the open third quadrant and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open third quadrant
  for some `A`, `B`, and `c < 2`;
* `f` is equal to zero on the boundary of the third quadrant.

Then `f` is equal to zero on the closed third quadrant.  -/
PhragmenLindelof.eq_zero_on_quadrant_III : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E},
  DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Iio 0) →
    (∃ c < 2,
        ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Iio 0)] fun z => Real.exp (B * ‖z‖ ^ c)) →
      (∀ x ≤ 0, f ↑x = 0) → (∀ x ≤ 0, f (↑x * Complex.I) = 0) → Set.EqOn f 0 {z | z.re ≤ 0 ∧ z.im ≤ 0}
-- Lean.Util.Recognizers
/-- Recognize `α × β`  -/
Lean.Expr.prod? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializationOptions.mk.inj : ∀ {hasWidgets? : Option Bool} {logCfg? : Option Lean.Lsp.LogConfig} {hasWidgets?_1 : Option Bool}
  {logCfg?_1 : Option Lean.Lsp.LogConfig},
  { hasWidgets? := hasWidgets?, logCfg? := logCfg? } = { hasWidgets? := hasWidgets?_1, logCfg? := logCfg?_1 } →
    hasWidgets? = hasWidgets?_1 ∧ logCfg? = logCfg?_1
-- Init.Data.Float.Model.Float32
/-- The underlying bit pattern of the `Float32.Model`.  -/
Float32.Model.toBits : Float32.Model → UInt32
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.presheafEquivOfIso_inverse_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y)
  (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) {X_1 Y_1 : (TopologicalSpace.Opens ↑X)ᵒᵖ}
  (f : X_1 ⟶ Y_1),
  ((TopCat.Presheaf.presheafEquivOfIso C H).inverse.obj G).map f =
    G.map ((TopologicalSpace.Opens.map H.inv).map f.unop).op
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.antitone_arccos : Antitone Real.arccos
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.eq : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} {x y : R} [inst_1 : I.IsTwoSided],
  (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y ↔ x - y ∈ I
-- Init.Data.Iterators.Basic
Std.Iterators.FinitenessRelation.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {inst : Std.Iterator α m β}
  {Rel : Std.IterM m β → Std.IterM m β → Prop} {wf : WellFounded Rel}
  {subrelation : ∀ {it it' : Std.IterM m β}, it'.IsPlausibleSuccessorOf it → Rel it' it}
  {Rel_1 : Std.IterM m β → Std.IterM m β → Prop} {wf_1 : WellFounded Rel_1}
  {subrelation_1 : ∀ {it it' : Std.IterM m β}, it'.IsPlausibleSuccessorOf it → Rel_1 it' it},
  { Rel := Rel, wf := wf, subrelation := subrelation } = { Rel := Rel_1, wf := wf_1, subrelation := subrelation_1 } →
    Rel = Rel_1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.fold_eq_foldl_keysArray : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {δ : Type w} {f : δ → α → δ}
  {init : δ}, m.WF → Std.HashMap.Raw.fold (fun d a x => f d a) init m = Array.foldl f init m.keysArray
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.localTriv_apply : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι) (p : Z.TotalSpace),
  ↑(Z.localTriv i) p = (p.proj, Z.coordChange (Z.indexAt p.proj) i p.proj p.snd)
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.term_add_const : ∀ {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ) (x a k a' : α),
  a + k = a' → Mathlib.Tactic.Abel.term n x a + k = Mathlib.Tactic.Abel.term n x a'
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsG2.pairingIn_mem_zero_one_three : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] [Finite ι] [CharZero R] [IsDomain R] [P.IsG2]
  (i j : ι), P.root i ≠ P.root j → P.root i ≠ -P.root j → P.pairingIn ℤ i j ∈ {-3, -1, 0, 1, 3}
-- Mathlib.Algebra.Module.End
smulAddHom_apply : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r : R) (x : M),
  ((smulAddHom R M) r) x = r • x
-- Mathlib.Order.Heyting.Basic
sup_himp_distrib : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⊔ b ⇨ c = (a ⇨ c) ⊓ (b ⇨ c)
-- Mathlib.Algebra.Group.Units.Defs
Units.mul_inv_of_eq : ∀ {α : Type u} [inst : Monoid α] {u : αˣ} {a : α}, ↑u = a → a * ↑u⁻¹ = 1
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.hBinOpHeuristic : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
/-- An open partial homeomorphism defines a homeomorphism between its source and target.  -/
OpenPartialHomeomorph.toHomeomorphSourceTarget : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → (e : OpenPartialHomeomorph X Y) → ↑e.source ≃ₜ ↑e.target
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β),
  f.comp (CompleteLatticeHom.id α) = f
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The adjunction between `left` and `right`.  -/
CategoryTheory.Bicategory.LeftAdjoint.adj : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {right : b ⟶ a} →
        (self : CategoryTheory.Bicategory.LeftAdjoint right) → CategoryTheory.Bicategory.Adjunction self.left right
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.congr_of_eventuallyEq_insert : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s : Set M},
  MDiffAt[s] f x → f₁ =ᶠ[nhdsWithin x (insert x s)] f → MDiffAt[s] f₁ x
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffOn.of_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {m n : WithTop ℕ∞}, ContMDiffOn I I' n f s → m ≤ n → ContMDiffOn I I' m f s
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.prodComm_toAffineEquiv : ∀ (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂],
  ↑(ContinuousAffineEquiv.prodComm k P₁ P₂) = AffineEquiv.prodComm k P₁ P₂
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.point_mem_closedInterior : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] [ZeroLEOneClass k] {n : ℕ} (s : Affine.Simplex k P n)
  (i : Fin (n + 1)), s.points i ∈ s.closedInterior
-- Mathlib.LinearAlgebra.FreeModule.PID
Module.Basis.SmithNormalForm.le_ker_coord_of_notMem_range : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {n : ℕ} {N : Submodule R M} (snf : Module.Basis.SmithNormalForm N ι n) {i : ι},
  i ∉ Set.range ⇑snf.f → N ≤ (snf.bM.coord i).ker
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedInf_of_notMem : ∀ {α : Type u_1} [inst : SemilatticeInf α] {s : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : BoundedOrder α],
  a ∉ upperClosure ↑s → s.truncatedInf a = ⊥
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
CategoryTheory.Functor.instIsClosedUnderIsomorphismsIsDenseAt : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}, F.isDenseAt.IsClosedUnderIsomorphisms
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f)
  (X : ↑(F.obj b₀)),
  (F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp
        ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
        ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X))
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderProcessedSnapshot.mk.sizeOf_spec : ∀ (toSnapshot : Lean.Language.Snapshot) (metaSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf)
  (result? : Option Lean.Language.Lean.HeaderProcessedState),
  sizeOf { toSnapshot := toSnapshot, metaSnap := metaSnap, result? := result? } =
    1 + sizeOf toSnapshot + sizeOf metaSnap + sizeOf result?
-- Mathlib.Topology.Category.Stonean.Basic
/-- The forgetful functor `Stonean ⥤ CompHaus` is fully faithful.  -/
Stonean.fullyFaithfulToCompHaus : Stonean.toCompHaus.FullyFaithful
-- Mathlib.Order.Category.BddDistLat
/-- Construct a bundled `BddDistLat` from a `BoundedOrder` `DistribLattice`.  -/
BddDistLat.of : (α : Type u_1) → [inst : DistribLattice α] → [BoundedOrder α] → BddDistLat
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.comap_jacobson : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] {f : R →+* S} {K : Ideal S},
  Ideal.comap f K.jacobson = sInf (Ideal.comap f '' {J | K ≤ J ∧ J.IsMaximal})
-- Lean.Elab.Tactic.BuiltinTactic
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.getCaseGoals.notFound : List Lean.MVarId → Lean.Name → Lean.TSyntax `Lean.binderIdent → Lean.Elab.Tactic.TacticM Lean.MVarId
-- Std.Http.Transport
/-- Close the transport connection.
The default implementation is a no-op; override this for transports that require explicit teardown.
For `Socket.Client`, the runtime closes the file descriptor when the object is finalized.
 -/
Std.Http.Transport.close : {α : Type} → [self : Std.Http.Transport α] → α → IO Unit
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.isEquiv_iff_lt_one_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : Semifield S] [inst_2 : LinearOrder S]
  {v w : AbsoluteValue R S} [IsStrictOrderedRing S], v.IsEquiv w ↔ ∀ (x : R), v x < 1 ↔ w x < 1
-- Lean.Elab.MutualDef
/-- Runs `k` with a restricted local context where only section variables from `vars` are included that
* are directly referenced in any `headers`,
* are included in `sc.includedVars` (via the `include` command),
* are directly referenced in any variable included by these rules, OR
* are instance-implicit variables that only reference section variables included by these rules AND
  are not listed in `sc.omittedVars` (via `omit`; note that `omit` also subtracts from
  `sc.includedVars`).

If `check` is false, no exceptions will be produced.
 -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.withHeaderSecVars : {α : Type} →
  Array Lean.Expr →
    Lean.Elab.Command.Scope →
      Array Lean.Elab.DefViewElabHeader →
        (Array Lean.Expr → Lean.Elab.TermElabM α) → optParam Bool true → Lean.Elab.TermElabM α
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.id.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  AlgebraicTopology.DoldKan.MorphComponents.id X n =
    { a := AlgebraicTopology.DoldKan.PInfty.f (n + 1), b := fun i => X.σ i }
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.succ?_toFun' : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  (f : Std.PRange.UpwardEnumerable.Map α β), Std.PRange.succ? ∘ f.toFun = Option.map f.toFun ∘ Std.PRange.succ?
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.comm_from_apply : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁.Hom C₂) (i : ι) {F : V → V → Type uF} {carrier : V → Type w}
  {instFunLike : (X Y : V) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory V F]
  (x : carrier (C₁.X i)),
  (CategoryTheory.ConcreteCategory.hom (C₂.dFrom i)) ((CategoryTheory.ConcreteCategory.hom (f.f i)) x) =
    (CategoryTheory.ConcreteCategory.hom (f.next i)) ((CategoryTheory.ConcreteCategory.hom (C₁.dFrom i)) x)
-- Mathlib.Order.Lattice
inf_eq_minDefault : ∀ {α : Type u} [inst : SemilatticeInf α] [inst_1 : DecidableLE α] [Std.Total fun x1 x2 => x1 ≤ x2],
  (fun x1 x2 => x1 ⊓ x2) = minDefault
-- Mathlib.CategoryTheory.Category.TwoP
/-- Swaps the pointed elements of a two-pointed type. `TwoPointing.swap` as a functor.  -/
TwoP.swap : CategoryTheory.Functor TwoP TwoP
-- Mathlib.RingTheory.FilteredAlgebra.Basic
/-- A convenience constructor for `IsFiltration` when the index is the integers.  -/
IsFiltration.mk_int : ∀ {σ : Type u_3} [inst : Preorder σ] (F : ℤ → σ), Monotone F → IsFiltration F fun n => F (n - 1)
-- Mathlib.Order.Category.BddLat
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
BddLat.Hom.Simps.hom : (X Y : BddLat) → X.Hom Y → BoundedLatticeHom ↑X.toLat ↑Y.toLat
-- Init.Meta.Defs
/-- Takes a raw string literal, counts the number of `#`'s after the `r`, and interprets it as a string.
The position `i` should start at `1`, which is the character after the leading `r`.
The algorithm is simple: we are given `r##...#"...string..."##...#` with zero or more `#`s.
By counting the number of leading `#`'s, we can extract the `...string...`.
 -/
Lean.Syntax.decodeRawStrLitAux : String → String.Pos.Raw → ℕ → String
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The inclusion `Δ[2] ⟶ Λ[3, 2]` which avoids `3`.  -/
SSet.horn₃₂.ι₃ : SSet.stdSimplex.obj { len := 2 } ⟶ (SSet.horn 3 2).toSSet
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.true : Mathlib.Tactic.ITauto.IProp
-- Mathlib.Order.CountableSupClosed
countableSupClosure_mono : ∀ {α : Type u_2} [inst : Preorder α], Monotone ⇑countableSupClosure
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
parallelepiped.eq_1 : ∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] (v : ι → E),
  parallelepiped v = (fun t => ∑ i, t i • v i) '' Set.Icc 0 1
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right_split : Int.Internal.Linear.Context →
  Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℕ → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.condition_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (j₁ j₂ : J)
  (t : CategoryTheory.Limits.Trident f) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp t.ι (CategoryTheory.CategoryStruct.comp (f j₁) h) =
    CategoryTheory.CategoryStruct.comp t.ι (CategoryTheory.CategoryStruct.comp (f j₂) h)
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.instInhabited : {B : Type u₁} → [inst : CategoryTheory.Bicategory B] → Inhabited (CategoryTheory.PrelaxFunctor B B)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
MulEquiv.toContinuousMulEquiv_symm_apply : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Mul G] [inst_3 : Mul H]
  (e : G ≃* H) (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (a : H), (e.toContinuousMulEquiv he).symm a = e.symm a
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd_apply : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : Finset.HasMulAntidiagonal A]
  (x : (n : A) × ↥(Finset.HasMulAntidiagonal.mulAntidiagonal n)),
  Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd x = ↑x.snd
-- Mathlib.Topology.Category.UniformSpace
/-- The underlying space  -/
CpltSepUniformSpace.α : CpltSepUniformSpace → Type u
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.rel_sum : ∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N] {R : M → N → Prop},
  R 0 0 →
    (Relator.LiftFun R (Relator.LiftFun R R) (fun x1 x2 => x1 + x2) fun x1 x2 => x1 + x2) →
      Relator.LiftFun (List.Forall₂ R) R List.sum List.sum
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.inf_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (F G : M.Submodule) (X : Cᵒᵖ), (Lattice.inf F G).obj X = F.obj X ⊓ G.obj X
-- Mathlib.RingTheory.PowerSeries.Basic
/-- The ring homomorphism taking a power series `f(X)` to `f(aX)`.  -/
PowerSeries.rescale : {R : Type u_1} → [inst : CommSemiring R] → R → PowerSeries R →+* PowerSeries R
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.ofNat : ℕ → Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valuation.integer.eq_1 : ∀ {R : Type u} {Γ₀ : Type v} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀),
  v.integer = { carrier := {x | v x ≤ 1}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.Algebra.Group.Basic
add_zero_eq_id : ∀ {M : Type u_4} [inst : AddZeroClass M], (fun x => x + 0) = id
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.map_naturality : ∀ {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] {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : CategoryTheory.HasShift D M] {X Y : C} {a : M}
  (f : CategoryTheory.ShiftedHom X Y a) {F G : CategoryTheory.Functor C D} (τ : F ⟶ G) [inst_5 : F.CommShift M]
  [inst_6 : G.CommShift M] [CategoryTheory.NatTrans.CommShift τ M],
  (f.map F).comp (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ (τ.app Y)) ⋯ =
    (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ (τ.app X)).comp (f.map G) ⋯
-- Init.Data.SInt.Bitwise
ISize.toInt_not : ∀ (a : ISize), (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ System.Platform.numBits)
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.largeSchroder.eq_1 : Nat.largeSchroder 0 = 1
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.GoalContext.equalFVarIds : Aesop.EqualUpToIds.GoalContext → Std.HashMap Lean.FVarId Lean.FVarId
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.find?_eq_findM? : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  [Std.Iterators.Finite α m] {it : Std.IterM m β} {f : β → Bool}, it.find? f = it.findM? fun x => pure { down := f x }