mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Path
/-- The path obtained from a map defined on `ℝ` by restriction to the unit interval.  -/
Path.ofLine : {X : Type u_1} →
  [inst : TopologicalSpace X] → {x y : X} → {f : ℝ → X} → ContinuousOn f unitInterval → f 0 = x → f 1 = y → Path x y
-- Mathlib.Order.Grade
/-- Lifts a graded order along a strictly monotone function.  -/
GradeOrder.liftLeft : {𝕆 : Type u_1} →
  {ℙ : Type u_2} →
    {α : Type u_3} →
      [inst : Preorder 𝕆] →
        [inst_1 : Preorder ℙ] →
          [inst_2 : Preorder α] →
            [GradeOrder 𝕆 α] → (f : 𝕆 → ℙ) → StrictMono f → (∀ (a b : 𝕆), a ⋖ b → f a ⋖ f b) → GradeOrder ℙ α
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.instIsIsoRightHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData)
  [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃],
  CategoryTheory.IsIso (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂)
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Add-add-negadd version.  -/
Finset.ruzsa_triangle_inequality_add_add_negAdd : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] (A B C : Finset G),
  (A + C).card * B.card ≤ (A + B).card * (-C + B).card
-- Init.Data.Option.Lemmas
Option.max_pfilter_right : ∀ {α : Type u_1} [inst : Max α] [Std.IdempotentOp max] {o : Option α} {p : (a : α) → o = some a → Bool},
  o ⊔ o.pfilter p = o
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image2_add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, Set.image2 (fun x1 x2 => x1 + x2) s t = s + t
-- Mathlib.Topology.Algebra.Group.Basic
ContinuousNeg.induced : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : FunLike F α β] [inst_1 : AddGroup α]
  [inst_2 : SubtractionMonoid β] [AddMonoidHomClass F α β] [tβ : TopologicalSpace β] [ContinuousNeg β] (f : F),
  ContinuousNeg α
-- Init.Data.Option.Monadic
Option.idRun_forIn_yield_eq_elim : ∀ {α : Type u_1} {β : Type u_2} (o : Option α) (f : α → β → Id β) (b : β),
  (forIn o b fun a b => ForInStep.yield <$> f a b).run = o.elim b fun a => (f a b).run
-- Mathlib.Topology.Path
Path.source_mem_range : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), x ∈ Set.range ⇑γ
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
SL_reduction_mod_hom_val : ∀ (N : ℕ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (i j : Fin 2),
  ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ) i j = ↑(↑γ i j)
-- Mathlib.Order.Interval.Multiset
Multiset.Iio.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (b : α), Multiset.Iio b = (Finset.Iio b).val
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- A `MonoidalRightAction C D` is the data of:
- For every object `c : C` and `d : D`, an object `c ⊙ᵣ d` of `D`.
- For every morphism `f : (c : C) ⟶ c'` and every `d : D`, a morphism
  `f ⊵ᵣ d : c ⊙ᵣ d ⟶ c' ⊙ᵣ d`.
- For every morphism `f : (d : D) ⟶ d'` and every `c : C`, a morphism
  `c ⊴ᵣ f : c ⊙ᵣ d ⟶ c ⊙ᵣ d'`.
- For every pair of morphisms `f : (c : C) ⟶ c'` and
  `f : (d : D) ⟶ d'`, a morphism `f ⊙ᵣₘ f' : c ⊙ᵣ d ⟶ c' ⊙ᵣ d'`.
- A structure isomorphism `αᵣ c c' d : c ⊗ c' ⊙ᵣ d ≅ c ⊙ᵣ c' ⊙ᵣ d`.
- A structure isomorphism `ρᵣ d : (𝟙_ C) ⊙ᵣ d ≅ d`.

Furthermore, we require identities that turn `- ⊙ᵣ -` into a bifunctor,
ensure naturality of `αᵣ` and `ρᵣ`, and ensure compatibilities with
the associator and unitor isomorphisms in `C`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.MonoidalCategory C] → Type (max (max (max u_1 u_2) v_1) v_2)
-- Mathlib.Topology.Instances.Rat
Nat.isClosedEmbedding_coe_rat : Topology.IsClosedEmbedding Nat.cast
-- Mathlib.Data.Set.Subsingleton
Set.Nontrivial.not_subset_empty : ∀ {α : Type u} {s : Set α}, s.Nontrivial → ¬s ⊆ ∅
-- Mathlib.Analysis.Calculus.Deriv.Prod
HasDerivAt.finCons : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℕ} {F' : Fin n.succ → Type u_1}
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : 𝕜 → F' 0} {φs : 𝕜 → (i : Fin n) → F' i.succ} {φ' : F' 0} {φs' : (i : Fin n) → F' i.succ},
  HasDerivAt φ φ' x → HasDerivAt φs φs' x → HasDerivAt (fun x => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Turn an element of a type `F` satisfying `MulActionSemiHomClass F φ X Y`
into an actual `MulActionHom`.
This is declared as the default coercion from `F` to `MulActionSemiHom φ X Y`.  -/
MulActionSemiHomClass.toMulActionHom : {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] →
              {F : Type u_8} → [inst_2 : FunLike F X Y] → [MulActionSemiHomClass F φ X Y] → F → X →ₑ[φ] Y
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- The canonical inclusion from the completion to the product.  -/
AdicCompletion.incl : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → AdicCompletion I M →ₗ[R] (n : ℕ) → M ⧸ I ^ n • ⊤
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.Position.character : Lean.Lsp.Position → ℕ
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.piCongrRight_toEquiv : ∀ {ι : Type u_4} {β₁ : ι → Type u_5} {β₂ : ι → Type u_6} [inst : (i : ι) → UniformSpace (β₁ i)]
  [inst_1 : (i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i),
  (UniformEquiv.piCongrRight F).toEquiv = Equiv.piCongrRight fun i => (F i).toEquiv
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.splits_iff_splits : ∀ {R : Type u_1} [inst : Field R] {f : Polynomial R},
  f.Splits ↔ f = 0 ∨ ∀ {g : Polynomial R}, Irreducible g → g ∣ f → g.degree = 1
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.opcyclesToCycles_iCycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι)
  [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (K.iCycles j) = K.fromOpcycles i j
-- Mathlib.Algebra.Module.ZLattice.Covolume
ZLattice.covolume_eq_det_mul_measureReal : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [inst_5 : DiscreteTopology ↥L] [IsZLattice ℝ L]
  (μ : autoParam (MeasureTheory.Measure E) _auto_31✝) [μ.IsAddHaarMeasure] {ι : Type u_2} [inst_8 : Fintype ι]
  [inst_9 : DecidableEq ι] (b : Module.Basis ι ℤ ↥L) (b₀ : Module.Basis ι ℝ E),
  ZLattice.covolume L μ = |b₀.det (Subtype.val ∘ ⇑b)| * μ.real (ZSpan.fundamentalDomain b₀)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.separatingLeft_toBilin'_iff : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {ι : Type u_6} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {M : Matrix ι ι R₂},
  LinearMap.SeparatingLeft (Matrix.toBilin' M) ↔ M.SeparatingLeft
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- `forbiddenImportDirs` relates module prefixes, specifying that modules with the first prefix
should not import modules with the second prefix (except if specifically allowed in
`overrideAllowedImportDirs`).

For example, ``(`Mathlib.Algebra.Notation, `Mathlib.Algebra)`` is in `forbiddenImportDirs` and
``(`Mathlib.Algebra.Notation, `Mathlib.Algebra.Notation)`` is in `overrideAllowedImportDirs`
because modules in `Mathlib/Algebra/Notation.lean` cannot import modules in `Mathlib.Algebra` that are
outside `Mathlib/Algebra/Notation.lean`.
 -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Mathlib.Linter.DirectoryDependency.forbiddenImportDirs : Mathlib.Linter.DirectoryDependency.NamePrefixRel✝
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_range_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → Nat.card ↑(Set.range f) = Nat.card α
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.HasAbsLeftKanLift.toHasLeftKanLift : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [self : CategoryTheory.Bicategory.HasAbsLeftKanLift f g], CategoryTheory.Bicategory.HasLeftKanLift f g
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_sInter : ∀ {x y : ZFSet.{u_1}}, x.Nonempty → (y ∈ x.sInter ↔ ∀ z ∈ x, y ∈ z)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.spanUnop_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z)
  (X_1 : CategoryTheory.Limits.WalkingSpan),
  (CategoryTheory.Limits.spanUnop f g).inv.app X_1 =
    (match X_1 with
      | none => CategoryTheory.Iso.refl (Opposite.unop Z)
      | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.unop X)
      | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.unop Y)).inv
-- Mathlib.Algebra.Group.Action.Pi
Set.piecewise_vadd : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] (s : Set ι)
  [inst_1 : (i : ι) → Decidable (i ∈ s)] (c : M) (f₁ g₁ : (i : ι) → α i),
  s.piecewise (c +ᵥ f₁) (c +ᵥ g₁) = c +ᵥ s.piecewise f₁ g₁
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousWithinAt.add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (f + g) s x
-- Mathlib.Data.Ordmap.Invariants
/-- `Bounded t lo hi` says that every element `x ∈ t` is in the range `lo < x < hi`, and also this
property holds recursively in subtrees, making the full tree a BST. The bounds can be set to
`lo = ⊥` and `hi = ⊤` if we care only about the internal ordering constraints.  -/
Ordnode.Bounded : {α : Type u_1} → [Preorder α] → Ordnode α → WithBot α → WithTop α → Prop
-- Lean.Parser.Extension
Lean.Parser.ParserAttributeHook.mk : (Lean.Name → Lean.Name → Bool → Lean.AttrM Unit) → Lean.Parser.ParserAttributeHook
-- Mathlib.Algebra.Algebra.Subalgebra.Directed
Subalgebra.inclusion.congr_simp : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A}
  (h : S ≤ T), Subalgebra.inclusion h = Subalgebra.inclusion h
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- The right homotopy relation is symmetric.
 -/
SSet.Truncated.HomotopicR.symm : ∀ {X : SSet.Truncated 2} [X.Quasicategory₂]
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f g : SSet.Truncated.Edge x y}, SSet.Truncated.HomotopicR f g → SSet.Truncated.HomotopicR g f
-- Mathlib.Tactic.Module
/-- Given a goal parseable as a linear combination `⊢ a • x + ... + b • y = c • x + ... + d • y`,
`module` proves the equalities of the scalars for each respective atom, by ring normalization.
This means the example goal above is solved if `ring` can prove `⊢ a = c` (from `x`), ..., `⊢ b = d`
(from `y`).

`module` is equivalent to `match_scalars <;> ring1`. If `ring1` fails to prove one of the
equalities, you can instead use `match_scalars` followed by specialized proofs for each scalar.

Examples:
```
example [AddCommMonoid M] [CommSemiring R] [Module R M] (a b : R) (x : M) :
    a • x + b • x = (b + a) • x := by
  module

example [AddCommMonoid M] [Field K] [CharZero K] [Module K M] (x : M) :
    (2:K)⁻¹ • x + (3:K)⁻¹ • x + (6:K)⁻¹ • x = x := by
  module

example [AddCommGroup M] [CommRing R] [Module R M] (a : R) (v w : M) :
    (1 + a ^ 2) • (v + w) - a • (a • v - w) = v + (1 + a + a ^ 2) • w := by
  module

example [AddCommGroup M] [CommRing R] [Module R M] (a b μ ν : R) (x y : M) :
    (μ - ν) • a • x = (a • μ • x + b • ν • y) - ν • (a • x + b • y) := by
  module
```
 -/
Mathlib.Tactic.Module.tacticModule : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.map_injective : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Affine R} {f : R →+* S},
  Function.Injective ⇑f → Function.Injective ⇑(WeierstrassCurve.Affine.CoordinateRing.map W' f)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toArray.eq_1 : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Impl α β),
  t.toArray = Std.DTreeMap.Internal.Impl.foldl (fun l k v => l.push ⟨k, v⟩) (Array.emptyWithCapacity t.size) t
-- Mathlib.Analysis.Calculus.VectorField
/-- If vector fields coincide on a neighborhood of a point within a set, then the Lie brackets
also coincide on a neighborhood of this point within this set. Version where one considers the Lie
bracket within a subset.  -/
Filter.EventuallyEq.lieBracketWithin_vectorField' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {s t : Set E} {x : E},
  V₁ =ᶠ[nhdsWithin x s] V →
    W₁ =ᶠ[nhdsWithin x s] W →
      t ⊆ s → VectorField.lieBracketWithin 𝕜 V₁ W₁ t =ᶠ[nhdsWithin x s] VectorField.lieBracketWithin 𝕜 V W t
-- Mathlib.Topology.Algebra.Group.Basic
Filter.Tendsto.zsmul : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {α : Type u_1} {l : Filter α}
  {f : α → G} {x : G}, Filter.Tendsto f l (nhds x) → ∀ (z : ℤ), Filter.Tendsto (fun x => z • f x) l (nhds (z • x))
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.mk : {P : Type u_2} →
  [inst : Preorder P] → (I : Order.Ideal P) → (F : Order.PFilter P) → IsCompl ↑I ↑F → Order.Ideal.PrimePair P
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_toNNReal_le_self : ∀ {a : ENNReal}, ↑a.toNNReal ≤ a
-- Mathlib.Algebra.Polynomial.Laurent
/-- The ring homomorphism, taking a polynomial with coefficients in `R` to a Laurent polynomial
with coefficients in `R`.  -/
Polynomial.toLaurent : {R : Type u_1} → [inst : Semiring R] → Polynomial R →+* LaurentPolynomial R
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
WeakDual.CharacterSpace.compContinuousMap_apply : ∀ {A : Type u_1} {B : Type u_2} {𝕜 : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A]
  [inst_2 : NormedAlgebra 𝕜 A] [inst_3 : CompleteSpace A] [inst_4 : StarRing A] [inst_5 : NormedRing B]
  [inst_6 : NormedAlgebra 𝕜 B] [inst_7 : CompleteSpace B] [inst_8 : StarRing B] (ψ : A →⋆ₐ[𝕜] B)
  (φ : ↑(WeakDual.characterSpace 𝕜 B)),
  (WeakDual.CharacterSpace.compContinuousMap ψ) φ =
    WeakDual.CharacterSpace.equivAlgHom.symm ((WeakDual.CharacterSpace.equivAlgHom φ).comp ↑ψ)
-- Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2 : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} {W : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  [inst_6 : NormedAddCommGroup W] [inst_7 : NormedSpace ℝ W] [inst_8 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] {μ : MeasureTheory.Measure (E × ℝ)} [μ.IsAddHaarMeasure] {f f' : E × ℝ → F} {g g' : E × ℝ → G}
  {B : F →L[ℝ] G →L[ℝ] W},
  MeasureTheory.Integrable (fun x => (B (f' x)) (g x)) μ →
    MeasureTheory.Integrable (fun x => (B (f x)) (g' x)) μ →
      MeasureTheory.Integrable (fun x => (B (f x)) (g x)) μ →
        (∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)) →
          (∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)) →
            ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- If `s` is a colimit cotrident over `f`, then a morphism `k : Y ⟶ W` satisfying
`∀ j₁ j₂, f j₁ ≫ k = f j₂ ≫ k` induces a morphism `l : s.X ⟶ W` such that
`Cotrident.π s ≫ l = k`.  -/
CategoryTheory.Limits.Cotrident.IsColimit.desc' : {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} →
              CategoryTheory.Limits.IsColimit s →
                {W : C} →
                  (k : Y ⟶ W) →
                    (∀ (j₁ j₂ : J),
                        CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k) →
                      { l // CategoryTheory.CategoryStruct.comp s.π l = k }
-- Mathlib.RingTheory.Regular.RegularSequence
LinearEquiv.isRegular_congr' : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] {σ : R →+* S}
  {σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ] (e : M ≃ₛₗ[σ] M₂) (rs : List R),
  RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.IsRegular M₂ (List.map (⇑σ) rs)
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_coe : ∀ {x : ENNReal}, (↑x).toENNReal = x
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.inf : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SemilatticeInf β] {f g : α → β} {a : α},
  IsLocalMax f a → IsLocalMax g a → IsLocalMax (fun x => f x ⊓ g x) a
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functorObj_isPushout : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  CategoryTheory.IsPushout (CategoryTheory.SmallObject.functorObjTop f πX)
    (CategoryTheory.SmallObject.functorObjLeft f πX) (CategoryTheory.SmallObject.ιFunctorObj f πX)
    (CategoryTheory.SmallObject.ρFunctorObj f πX)
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X),
  TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U =
    CategoryTheory.Limits.Pi.lift fun p =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => F.obj (Opposite.op (U i))) p.1)
        (F.map ((U p.1).infLELeft (U p.2)).op)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Functor
CategoryTheory.leftDualFunctor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.LeftRigidCategory C] (X : C),
  (CategoryTheory.leftDualFunctor C).obj X = { unmop := Opposite.op ᘁX }
-- Mathlib.AlgebraicGeometry.GluingOneHypercover
AlgebraicGeometry.Scheme.GlueData.sheafValGluedMk_val : ∀ (D : AlgebraicGeometry.Scheme.GlueData) {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type v)}
  (s : (j : D.J) → F.obj.obj (Opposite.op (D.U j)))
  (h :
    ∀ (i j : D.J),
      (CategoryTheory.ConcreteCategory.hom (F.obj.map (D.f i j).op)) (s i) =
        (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.CategoryStruct.comp (D.f j i).op (D.t i j).op)))
          (s j))
  (j : D.J), (CategoryTheory.ConcreteCategory.hom (F.obj.map (D.ι j).op)) (D.sheafValGluedMk s h) = s j
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.dgoToHomologicalComplex_obj_d : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i j : β),
  ((HomologicalComplex.dgoToHomologicalComplex b V).obj X).d i j =
    if h : i + b = j then CategoryTheory.CategoryStruct.comp (X.d i) (X.objEqToHom ⋯) else 0
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_algebraMap : ∀ {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₁) (x : R),
  (LinearMap.toMatrix v₁ v₁) ((algebraMap R (Module.End R M₁)) x) = (Matrix.scalar n) x
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.smul_le : ∀ {R : Type u_2} {A : Type u_3} [inst : AddMonoid R] [inst_1 : AddMonoid A] [inst_2 : DistribSMul R A]
  {M : AddSubmonoid R} {N P : AddSubmonoid A}, M • N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m • n ∈ P
-- Mathlib.Algebra.Order.Hom.Basic
/-- The map is invariant under negation of its argument.  -/
AddGroupSeminormClass.map_neg_eq_map : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : AddGroup α} {inst_1 : AddCommMonoid β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : AddGroupSeminormClass F α β] (f : F) (a : α), f (-a) = f a
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- Polynomial evaluation on a pair is a product of the evaluations on the components.  -/
Polynomial.aeval_prod : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (x : A × B),
  Polynomial.aeval x = (Polynomial.aeval x.1).prod (Polynomial.aeval x.2)
-- Std.Data.Iterators.Combinators.Zip
/-- Given two iterators `left` and `right`, `left.zip right` is an iterator that yields pairs of
outputs of `left` and `right`. When one of them terminates,
the `zip` iterator will also terminate.

**Marble diagram:**

```text
left               --a        ---b        --c
right                 --x         --y        --⊥
left.zip right     -----(a, x)------(b, y)-----⊥
```

**Termination properties:**

* `Finite` instance: only if either `left` or `right` is finite and the other is productive
* `Productive` instance: only if `left` and `right` are productive

There are situations where `left.zip right` is finite (or productive) but none of the instances
above applies. For example, if `left` immediately terminates but `right` always skips, then
`left.zip.right` is finite even though no `Finite` (or even `Productive`) instance is available.
Such instances need to be proved manually.

**Performance:**

This combinator incurs an additional O(1) cost with each step taken by `left` or `right`.

Right now, the compiler does not unbox the internal state, leading to worse performance than
theoretically possible.
 -/
Std.Iter.zip : {α₁ β₁ α₂ β₂ : Type w} →
  [inst : Std.Iterator α₁ Id β₁] → [Std.Iterator α₂ Id β₂] → Std.Iter β₁ → Std.Iter β₂ → Std.Iter (β₁ × β₂)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.toLinearMap_rTensor : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (f : σ.IntertwiningMap τ),
  (Representation.IntertwiningMap.rTensor ρ f).toLinearMap = LinearMap.rTensor V f.toLinearMap