mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` preserves limits, then `F : Cᵒᵖ ⥤ D` preserves colimits.  -/
CategoryTheory.Limits.preservesColimits_of_rightOp : ∀ {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.Limits.PreservesLimits F.rightOp],
  CategoryTheory.Limits.PreservesColimits F
-- Mathlib.Algebra.Polynomial.GroupRingAction
Polynomial.smul_X : ∀ {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (m : M),
  m • Polynomial.X = Polynomial.X
-- Lean.Elab.DocString
/-- The name of the role to suggest.  -/
Lean.Doc.CodeSuggestion.role : Lean.Doc.CodeSuggestion → Lean.Name
-- Mathlib.Order.GameAdd
Prod.GameAdd.recursion_eq : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {C : α → β → Sort u_3} (hα : WellFounded rα)
  (hβ : WellFounded rβ)
  (IH : (a₁ : α) → (b₁ : β) → ((a₂ : α) → (b₂ : β) → Prod.GameAdd rα rβ (a₂, b₂) (a₁, b₁) → C a₂ b₂) → C a₁ b₁) (a : α)
  (b : β), Prod.GameAdd.recursion hα hβ IH a b = IH a b fun a' b' x => Prod.GameAdd.recursion hα hβ IH a' b'
-- Mathlib.Order.CompleteBooleanAlgebra
iInf₂_sup_eq : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : Order.Coframe α] {f : (i : ι) → κ i → α} (a : α),
  (⨅ i, ⨅ j, f i j) ⊔ a = ⨅ i, ⨅ j, f i j ⊔ a
-- Init.System.ST
STWorld.mk : {σ : outParam Type} → {m : Type → Type} → STWorld σ m
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
_private.Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic.0.ProfiniteGrp.Hom.mk.sizeOf_spec : ∀ {A B : ProfiniteGrp.{u}} (hom' : ↑A.toProfinite.toTop →ₜ* ↑B.toProfinite.toTop),
  sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Order.WithBot
Equiv.withTopCongr_symm : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), e.symm.withTopCongr = e.withTopCongr.symm
-- Mathlib.Topology.CompactOpen
Topology.IsQuotientMap.continuous_lift_prod_right : ∀ {X₀ : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X₀]
  [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Z] [LocallyCompactSpace Y]
  {f : X₀ → X}, Topology.IsQuotientMap f → ∀ {g : Y × X → Z}, (Continuous fun p => g (p.1, f p.2)) → Continuous g
-- Lean.Structure
Lean.instInhabitedStructureDescr.default : Lean.StructureDescr
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.IterM.step_takeWhileWithPostcondition.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (P out).Property → Sort u_3) (h' : (P out).Property { down := true })
  (h_1 : (h' : (P out).Property { down := true }) → motive ⟨{ down := true }, h'⟩)
  (h_2 : (h' : (P out).Property { down := false }) → motive ⟨{ down := false }, h'⟩),
  (match ⟨{ down := true }, h'⟩ with
    | ⟨{ down := true }, h'⟩ => h_1 h'
    | ⟨{ down := false }, h'⟩ => h_2 h') =
    h_1 h'
-- Mathlib.RingTheory.DividedPowers.Padic
PadicInt.dividedPowers.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)],
  PadicInt.dividedPowers p =
    DividedPowers.ofInjective (Ideal.span {↑p}) ⊤ PadicInt.Coe.ringHom ⋯ (DividedPowers.RatAlgebra.dividedPowers ⊤) ⋯ ⋯
-- Mathlib.Data.Vector.Zip
List.Vector.prod_mul_prod_eq_prod_zipWith : ∀ {α : Type u_1} {n : ℕ} [inst : CommMonoid α] (x y : List.Vector α n),
  x.toList.prod * y.toList.prod = (List.Vector.zipWith (fun x1 x2 => x1 * x2) x y).toList.prod
-- Lean.Server.FileWorker.Utils
/-- Construct a VersionedTextDocumentIdentifier from an EditableDocument - -/
Lean.Server.FileWorker.EditableDocument.versionedIdentifier : Lean.Server.FileWorker.EditableDocument → Lean.Lsp.VersionedTextDocumentIdentifier
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.ncard_le_ncard_sdiff_add_ncard`. -/
Set.ncard_le_ncard_diff_add_ncard : ∀ {α : Type u_1} (s t : Set α),
  autoParam t.Finite Set.ncard_le_ncard_sdiff_add_ncard._auto_1 → s.ncard ≤ (s \ t).ncard + t.ncard
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_apply_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type uE) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {ι : Type u_3} {ι' : Type u_4} [inst_3 : Fintype ι] [inst_4 : Fintype ι']
  (i : ι) (j : ι'), ContDiff 𝕜 n fun f => f i j
-- Lean.Level
Lean.Level.updateSucc! : Lean.Level → Lean.Level → Lean.Level
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.symm_dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] (g : CompleteLatticeHom βᵒᵈ γᵒᵈ) (f : CompleteLatticeHom αᵒᵈ βᵒᵈ),
  CompleteLatticeHom.dual.symm (g.comp f) = (CompleteLatticeHom.dual.symm g).comp (CompleteLatticeHom.dual.symm f)
-- Init.Data.Array.Perm
Array.Perm.push : ∀ {α : Type u_1} (x : α) {xs ys : Array α}, xs.Perm ys → (xs.push x).Perm (ys.push x)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.equivSigma_symm_apply_right : ∀ (T : Type u) [inst : CategoryTheory.Category.{v, u} T] (x : (X : T) × (Y : T) × (X ⟶ Y)),
  ((CategoryTheory.Arrow.equivSigma T).symm x).right = x.snd.fst
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mk'_eq_coe : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {l u : ι → ℝ}, BoxIntegral.Box.mk' l u = ↑I ↔ l = I.lower ∧ u = I.upper
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.add_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [ContinuousAdd α]
  {s : Set β}, Summable (f ∘ Subtype.val) → Summable (f ∘ Subtype.val) → Summable f
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.isEmpty_dropEndWhile_takeEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String}, ((s.takeEndWhile pat).dropEndWhile pat).isEmpty = true
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.adjoinIntegral_coe : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] (x : P) (hx : IsIntegral R x),
  ↑(FractionalIdeal.adjoinIntegral S x hx) = Subalgebra.toSubmodule R[x]
-- Lean.Elab.DefView
Lean.Elab.DefParsed.mk : Lean.Syntax → Lean.Language.SnapshotTask (Option Lean.Elab.HeaderProcessedSnapshot) → Lean.Elab.DefParsed
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (x : Monoid.Coprod M N),
  (Monoid.Coprod.swap N M) ((Monoid.Coprod.swap M N) x) = x
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.Retract.projectiveDimension_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (h : CategoryTheory.Retract X Y), CategoryTheory.projectiveDimension X ≤ CategoryTheory.projectiveDimension Y
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.ext : ∀ {R : Type u_1} {inst : CommRing R} {x y : FormalGroup R}, x.toPowerSeries = y.toPowerSeries → x = y
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurable_of_Iic : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : δ → α},
  (∀ (x : α), MeasurableSet (f ⁻¹' Set.Iic x)) → Measurable f
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.dual_delete_dual : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), (M✶.delete X)✶ = M.contract X
-- Mathlib.Data.List.Sigma
/-- Determines whether the store uses a key several times.  -/
List.NodupKeys : {α : Type u} → {β : α → Type v} → List (Sigma β) → Prop
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.RotateRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {w : ℕ} → (aig : Std.Sat.AIG α) → aig.ShiftTarget w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Algebra.Group.Nat.Hom
AddMonoidHom.apply_nat : ∀ {M : Type u_1} [inst : AddMonoid M] (f : ℕ →+ M) (n : ℕ), f n = n • f 1
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
ChartedSpace.stalkMap_locallyRingedSpaceMap_evalHom_assoc : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {EM : Type u_1} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_2} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {M : Type u} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace HM M] {EN : Type u_3}
  [inst_6 : NormedAddCommGroup EN] [inst_7 : NormedSpace 𝕜 EN] {HN : Type u_4} [inst_8 : TopologicalSpace HN]
  {IN : ModelWithCorners 𝕜 EN HN} {N : Type u} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace HN N] (f : M → N)
  (hf : ContMDiff IM IN (↑⊤) f) (x : M) {Z : CommRingCat} (h : CommRingCat.of 𝕜 ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (ChartedSpace.locallyRingedSpaceMap f hf) x)
      (CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.evalHom IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜 x) h) =
    CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.evalHom IN (modelWithCornersSelf 𝕜 𝕜) N 𝕜 (f x)) h
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- relations  -/
SheafOfModules.Presentation.relations : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} →
              (self : M.Presentation) → (CategoryTheory.Limits.kernel self.generators.π).GeneratingSections
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.Equivalent.symm : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N}, Q₁.Equivalent Q₂ → Q₂.Equivalent Q₁
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `Differentiable.add` -/
Differentiable.fun_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F},
  Differentiable 𝕜 f → Differentiable 𝕜 g → Differentiable 𝕜 fun i => f i + g i
-- Mathlib.Algebra.BigOperators.Finprod
prod_finprod_comm : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] (s : Finset α) (f : α → β → M),
  (∀ a ∈ s, Function.HasFiniteMulSupport (f a)) → ∏ a ∈ s, ∏ᶠ (b : β), f a b = ∏ᶠ (b : β), ∏ a ∈ s, f a b
-- Init.Data.Option.Basic
Option.max_some_some : ∀ {α : Type u_1} [inst : Max α] {a b : α}, some a ⊔ some b = some (a ⊔ b)
-- Mathlib.NumberTheory.ArithmeticFunction.Liouville
ArithmeticFunction.liouville_apply : ∀ {n : ℕ}, n ≠ 0 → ArithmeticFunction.liouville n = (-1) ^ ArithmeticFunction.cardFactors n
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.push_induction.append_singleton_induction : ∀ (l : List Char) (motive : List Char → Prop),
  motive [] → (∀ (l : List Char) (a : Char), motive l → motive (l ++ [a])) → motive l
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_lt : ∀ {m n : ℕ}, 0 < n → (n.factorial < m.factorial ↔ n < m)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_exClosure : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} [inst_1 : DecidableEq α]
  (φ : L.Formula α),
  M ⊨ φ.exClosure ↔ ∃ v, FirstOrder.Language.Formula.Realize (FirstOrder.Language.BoundedFormula.restrictFreeVar φ id) v
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.liftOn_mk : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α : Type u_3} {f : M × ↥S → α} (wd : ∀ (p p' : M × ↥S), p ≈ p' → f p = f p') (m : M) (s : ↥S),
  (LocalizedModule.mk m s).liftOn f wd = f (m, s)
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofBddAugment_indep : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n) (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E),
  (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).Indep = Indep
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- The n-ary version of `Set.image_mul_prod`.  -/
Set.image_finsetProd_pi : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (l : Finset ι) (S : ι → Set α),
  (fun f => ∏ i ∈ l, f i) '' (↑l).pi S = ∏ i ∈ l, S i
-- Lean.Syntax
Lean.Syntax.instForInTopDownOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForIn m Lean.Syntax.TopDown Lean.Syntax
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.isAddLeftInvariant_smul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant]
  (c : ENNReal), (c • μ).IsAddLeftInvariant
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.expr.sizeOf_spec : ∀ (a : Lean.Widget.CodeWithInfos), sizeOf (Lean.Widget.MsgEmbed.expr a) = 1 + sizeOf a
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- The inverse of a bijective morphism is a morphism.  -/
NonUnitalAlgHom.inverse : {R : Type u} →
  [inst : Monoid R] →
    {A : Type v} →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : DistribMulAction R A] →
          {B₁ : Type u_2} →
            [inst_3 : NonUnitalNonAssocSemiring B₁] →
              [inst_4 : DistribMulAction R B₁] →
                (f : A →ₙₐ[R] B₁) → (g : B₁ → A) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → B₁ →ₙₐ[R] A
-- Init.Data.Iterators.Combinators.Monadic.Take
/-- Internal implementation detail of the iterator library.
Caution: For `take n`, `countdown` is `n + 1`.
If `countdown` is zero, the combinator only terminates when `inner` terminates.
 -/
Std.Iterators.Types.Take.countdown : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → [inst : Std.Iterator α m β] → Std.Iterators.Types.Take α m → ℕ
-- Mathlib.GroupTheory.OreLocalization.Cardinality
OreLocalization.cardinalMk_le_max : ∀ {R : Type u} [inst : Monoid R] (S : Submonoid R) [inst_1 : OreLocalization.OreSet S] (X : Type v)
  [inst_2 : MulAction R X],
  Cardinal.mk (OreLocalization S X) ≤ max (Cardinal.lift.{v, u} (Cardinal.mk ↥S)) (Cardinal.lift.{u, v} (Cardinal.mk X))
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instHasPushoutsAlongOfHasPushoutsAlong : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Limits.HasPushoutsAlong f], P.HasPushoutsAlong f
-- Init.PropLemmas
dite_eq_left_iff : ∀ {α : Sort u_1} {p : Prop} [inst : Decidable p] {x : α} {y : ¬p → α},
  (if h : p then x else y h) = x ↔ ∀ (h : ¬p), y h = x
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.topology_eq : ∀ (α : Type u_1) [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLowerSet α], inst_1 = Topology.lowerSet α
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The right distributivity isomorphism of the a left distributive symmetric monoidal category
is given by `(β_ (Y ⨿ Z) X).hom ≫ (∂L X Y Z).inv ≫ (coprod.map (β_ X Y).hom (β_ X Z).hom)`.  -/
CategoryTheory.SymmetricCategory.rightDistrib_of_leftDistrib : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.SymmetricCategory C]
  [inst_4 : CategoryTheory.IsMonoidalDistrib C] {X Y Z : C},
  ∂R X Y Z = CategoryTheory.Limits.coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ CategoryTheory.leftDistrib X Y Z ≪≫ β_ X (Y ⨿ Z)
-- Mathlib.Topology.Algebra.Group.Basic
/-- Given two compact sets in a noncompact additive topological group, there is a
translate of the second one that is disjoint from the first one.  -/
exists_disjoint_vadd_of_isCompact : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] [NoncompactSpace G]
  {K L : Set G}, IsCompact K → IsCompact L → ∃ g, Disjoint K (g +ᵥ L)
-- Batteries.Data.List.Lemmas
List.foldrIdx_start : ∀ {α : Type u_1} {xs : List α} {α_1 : Type u_2} {f : ℕ → α → α_1 → α_1} {i : α_1} {s : ℕ},
  List.foldrIdx f i xs s = List.foldrIdx (fun x => f (x + s)) i xs
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.MultispanIndex.toLinearOrderMultispanIso.match_1.eq_1 : ∀ {ι : Type u_1} [inst : LinearOrder ι]
  (motive : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι) → Sort u_2)
  (a : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).L)
  (h_1 :
    (a : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).L) →
      motive (CategoryTheory.Limits.WalkingMultispan.left a))
  (h_2 :
    (a : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).R) →
      motive (CategoryTheory.Limits.WalkingMultispan.right a)),
  (match CategoryTheory.Limits.WalkingMultispan.left a with
    | CategoryTheory.Limits.WalkingMultispan.left a => h_1 a
    | CategoryTheory.Limits.WalkingMultispan.right a => h_2 a) =
    h_1 a
-- Init.Data.BitVec.Lemmas
BitVec.instLawfulCommIdentityHMulOfNatOfNatNat : ∀ {w : ℕ}, Std.LawfulCommIdentity (fun x y => x * y) 1#w
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon_nc : ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Tactic.Abel
/-- Evaluate an expression into its `abel` normal form.

This is a variant of `Mathlib.Tactic.Abel.eval`, the main driver of the `abel` tactic.
It differs in
* outputting a `Simp.Result`, rather than a `NormalExpr × Expr`;
* throwing an error if the expression `e` is an atom for the `abel` tactic.
 -/
Mathlib.Tactic.Abel.evalExpr : Lean.Expr → Mathlib.Tactic.AtomM Lean.Meta.Simp.Result
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (∃ n, Nonempty (S ≃ₐ[R] Fin n → R)) → Algebra.IsFiniteSplit R S
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.evalCompCoyonedaCorepresentableBySingle_homEquiv_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_3 : DecidableEq ι]
  (hi : ∀ (j : ι), ¬c.Rel i j) (X : C) {K : HomologicalComplex C c} (g : (HomologicalComplex.single C c i).obj X ⟶ K),
  (HomologicalComplex.evalCompCoyonedaCorepresentableBySingle c i hi X).homEquiv g =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c i X).inv (g.f i)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combine : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Init.Data.Vector.Lemmas
Vector.mk_zipWith_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → β → γ} {as : Array α} {bs : Array β} (h : as.size = n)
  (h' : bs.size = n), Vector.zipWith f (Vector.mk as h) (Vector.mk bs h') = Vector.mk (Array.zipWith f as bs) ⋯
-- Lean.Server.Requests
Lean.Server.StatefulRequestHandler.mk.inj : ∀ {fileSource : Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri}
  {pureHandle : Lean.Json → Dynamic → Lean.Server.RequestM (Lean.Server.SerializedLspResponse × Dynamic)}
  {handle : Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse)}
  {pureOnDidChange : Lean.Lsp.DidChangeTextDocumentParams → StateT Dynamic Lean.Server.RequestM Unit}
  {onDidChange : Lean.Lsp.DidChangeTextDocumentParams → Lean.Server.RequestM Unit}
  {lastTaskMutex : Std.Mutex (Lean.Server.ServerTask Unit)} {initState : Dynamic} {stateRef : IO.Ref Dynamic}
  {completeness : Lean.Server.RequestHandlerCompleteness}
  {fileSource_1 : Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri}
  {pureHandle_1 : Lean.Json → Dynamic → Lean.Server.RequestM (Lean.Server.SerializedLspResponse × Dynamic)}
  {handle_1 : Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse)}
  {pureOnDidChange_1 : Lean.Lsp.DidChangeTextDocumentParams → StateT Dynamic Lean.Server.RequestM Unit}
  {onDidChange_1 : Lean.Lsp.DidChangeTextDocumentParams → Lean.Server.RequestM Unit}
  {lastTaskMutex_1 : Std.Mutex (Lean.Server.ServerTask Unit)} {initState_1 : Dynamic} {stateRef_1 : IO.Ref Dynamic}
  {completeness_1 : Lean.Server.RequestHandlerCompleteness},
  { fileSource := fileSource, pureHandle := pureHandle, handle := handle, pureOnDidChange := pureOnDidChange,
        onDidChange := onDidChange, lastTaskMutex := lastTaskMutex, initState := initState, stateRef := stateRef,
        completeness := completeness } =
      { fileSource := fileSource_1, pureHandle := pureHandle_1, handle := handle_1,
        pureOnDidChange := pureOnDidChange_1, onDidChange := onDidChange_1, lastTaskMutex := lastTaskMutex_1,
        initState := initState_1, stateRef := stateRef_1, completeness := completeness_1 } →
    fileSource = fileSource_1 ∧
      pureHandle = pureHandle_1 ∧
        handle = handle_1 ∧
          pureOnDidChange = pureOnDidChange_1 ∧
            onDidChange = onDidChange_1 ∧
              lastTaskMutex = lastTaskMutex_1 ∧
                initState = initState_1 ∧ stateRef = stateRef_1 ∧ completeness = completeness_1
-- Mathlib.Topology.Algebra.Monoid.Defs
/-- A type class encoding that addition is continuous in each argument. This is weaker than
`ContinuousMul`.  -/
SeparatelyContinuousMul : (M : Type u_1) → [TopologicalSpace M] → [Mul M] → Prop
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace Y]
  [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace Z],
  Topology.IsInducing g → Topology.IsInducing f → Topology.IsInducing (g ∘ f)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_hom : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_hom._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.p_opcyclesIso_hom._auto_3),
  CategoryTheory.CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).pOpcycles
      (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom =
    X.pOpcycles f₂ f₃ n₁
-- Mathlib.Combinatorics.Hindman
Ultrafilter.continuous_add_left : ∀ {M : Type u_1} [inst : Add M] (V : Ultrafilter M), Continuous fun x => x + V