mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.i.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.EnoughInjectives C] (n₁ : ℤ),
  CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.i✝ K n₁ =
    HomologicalComplex.mkHomToSingle
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K n₁)
        (CategoryTheory.Injective.ι (HomologicalComplex.opcycles K n₁)))
      ⋯
-- Mathlib.Probability.ProductMeasure
Preorder.frestrictLe₂.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] {a b : α} (hab : a ≤ b),
  Preorder.frestrictLe₂ hab = Finset.restrict₂ ⋯
-- Mathlib.Order.Filter.Prod
Filter.coprod_neBot_right : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} [g.NeBot] [Nonempty α], (f.coprod g).NeBot
-- Mathlib.RingTheory.NormalClosure
Ring.instIsDedekindDomainNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S] [Module.Finite R S] [PerfectField (FractionRing R)]
  [IsDedekindDomain S], IsDedekindDomain (Ring.NormalClosure R S)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- If the product comparison morphism is an iso, its inverse is natural in the left argument.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {A B A' : C}
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)] (f : A ⟶ A')
  [inst_5 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A' B)] {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj A' B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B))
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f B)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj B))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A' B)) h)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsTopologicalAddGroup.leftUniformSpace.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  IsTopologicalAddGroup.leftUniformSpace G =
    { toTopologicalSpace := inst_1, uniformity := Filter.comap (fun p => -p.1 + p.2) (nhds 0), symm := ⋯, comp := ⋯,
      nhds_eq_comap_uniformity := ⋯ }
-- Lean.Server.References
/-- Kind of `meta` annotation on this import.  -/
Lean.Server.ModuleImport.metaKind : Lean.Server.ModuleImport → Lean.Lsp.LeanImportMetaKind
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_unitIso_inv_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).unitIso.inv.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Lean.Meta.Basic
Lean.Meta.maxSynthPendingDepth : Lean.Option ℕ
-- Lean.Parser.Command
Lean.Parser.Tactic.open.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.closure_pow : ∀ {G : Type u_2} [inst : Group G] {s : Set G} {n : ℕ}, 1 ∈ s → n ≠ 0 → Subgroup.closure (s ^ n) = Subgroup.closure s
-- Lean.Parser.Term
Lean.Parser.Term.matchAlt.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Module.Submodule.Lattice
AddSubgroup.toIntSubmodule_toAddSubgroup : ∀ {M : Type u_3} [inst : AddCommGroup M] (S : AddSubgroup M), (AddSubgroup.toIntSubmodule S).toAddSubgroup = S
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsRamified.comap_embedding : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K},
  NumberField.InfinitePlace.IsRamified k w → (w.comap (algebraMap k K)).embedding = w.embedding.comp (algebraMap k K)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₇_transpose : CartanMatrix.E₇.transpose = CartanMatrix.E₇
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.mk'_adj : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (Opposite.op X₁))
  (h :
    autoParam
      (∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) {X₂ : C₂} {X₃ : C₃} (g : (F.obj Y₁).obj X₂ ⟶ X₃),
        ((adj X₁).homEquiv X₂ X₃) (CategoryTheory.CategoryStruct.comp ((F.map f).app X₂) g) =
          CategoryTheory.CategoryStruct.comp (((adj Y₁).homEquiv X₂ X₃) g) ((G.map f.op).app X₃))
      CategoryTheory.ParametrizedAdjunction.mk'._auto_1)
  (X₁ : C₁), (CategoryTheory.ParametrizedAdjunction.mk' adj h).adj X₁ = adj X₁
-- Mathlib.Analysis.InnerProductSpace.MeanErgodic
/-- **Von Neumann Mean Ergodic Theorem** for an operator in a Hilbert space.
For a contracting continuous linear self-map `f : E →L[𝕜] E` of a Hilbert space, `‖f‖ ≤ 1`,
the Birkhoff averages
```
birkhoffAverage 𝕜 f id N x = (N : 𝕜)⁻¹ • ∑ n ∈ Finset.range N, f^[n] x
```
converge to the orthogonal projection of `x` to the subspace of fixed points of `f`.  -/
ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (f : E →L[𝕜] E),
  ‖f‖ ≤ 1 →
    ∀ (x : E),
      Filter.Tendsto (fun x_1 => birkhoffAverage 𝕜 (⇑f) id x_1 x) Filter.atTop
        (nhds ↑(((↑f).eqLocus ↑1).orthogonalProjectionOnto x))
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.sPolynomial_decomposition : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {d : m.syn} {ι : Type u_3} {B : Finset ι}
  {g : ι → MvPolynomial σ R},
  (∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < d →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negAddY_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2 →
            W.negAddY P Q / WeierstrassCurve.Jacobian.addZ P Q ^ 3 =
              W.toAffine.negAddY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3)
                (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → (Std.TreeMap.unitOfList l cmp).size = l.length
-- Mathlib.Algebra.Star.StarAlgHom
/-- `coe_mk'` below applies in more cases  -/
NonUnitalStarAlgHom.coe_mk : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] (f : A → B)
  (h₁ : ∀ (m : R) (x : A), f (m • x) = (MonoidHom.id R) m • f x) (h₂ : { toFun := f, map_smul' := h₁ }.toFun 0 = 0)
  (h₃ :
    ∀ (x y : A),
      { toFun := f, map_smul' := h₁ }.toFun (x + y) =
        { toFun := f, map_smul' := h₁ }.toFun x + { toFun := f, map_smul' := h₁ }.toFun y)
  (h₄ :
    ∀ (x y : A),
      { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
        { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
          { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y)
  (h₅ :
    ∀ (a : A),
      { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun (star a) =
        star ({ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun a)),
  ⇑{ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅ } = f
-- Lean.Meta.Tactic.Repeat
_private.Lean.Meta.Tactic.Repeat.0.Lean.Meta.repeat'Core.go.match_1.splitter : (motive : Option (List Lean.MVarId) → Sort u_1) →
  (__do_lift : Option (List Lean.MVarId)) →
    ((goals' : List Lean.MVarId) → motive (some goals')) → (Unit → motive none) → motive __do_lift
-- Mathlib.Algebra.Order.Monovary
Antivary.add_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {f₁ f₂ : ι → α} {g : ι → β}, Antivary f₁ g → Antivary f₂ g → Antivary (f₁ + f₂) g
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.apply_eq_prod_continuousLinearEquivAt : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] (b : B)
  (hb : b ∈ e.baseSet) (z : E b), ↑e ⟨b, z⟩ = (b, (Bundle.Trivialization.continuousLinearEquivAt R e b hb) z)
-- Mathlib.Control.Traversable.Equiv
/-- Like `Equiv.map`, a function `t' : Type u → Type u` can be given
the structure of a traversable functor using a traversable functor
`t'` and equivalences `t α ≃ t' α` for all α. See `Equiv.traversable`.  -/
Equiv.traverse : {t t' : Type u → Type u} →
  ((α : Type u) → t α ≃ t' α) →
    [Traversable t] → {m : Type u → Type u} → [Applicative m] → {α β : Type u} → (α → m β) → t' α → m (t' β)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.add_toSimpleFunc : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f g : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
  ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (f + g)) =ᵐ[μ]
    ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) + ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc g)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  k ∈ Std.DTreeMap.Const.insertManyIfNewUnit t l ↔ k ∈ t ∨ l.contains k = true
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRight_obj_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} (r : R₁ ⟶ R₂)
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRight L r hr).obj X).left = X.left
-- Mathlib.Tactic.NormNum.Eq
Mathlib.Meta.NormNum.isNat_eq_false : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [CharZero α] {a b : α} {a' b' : ℕ},
  Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.beq b' = false → ¬a = b
-- Mathlib.RingTheory.Flat.Localization
Module.flat_of_isLocalized_span : ∀ {R : Type u_1} (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [IsScalarTower R S M] (s : Set S),
  Ideal.span s = ⊤ →
    ∀ (Mₛ : ↑s → Type u_5) [inst_7 : (r : ↑s) → AddCommMonoid (Mₛ r)] [inst_8 : (r : ↑s) → Module R (Mₛ r)]
      [inst_9 : (r : ↑s) → Module S (Mₛ r)] [∀ (r : ↑s), IsScalarTower R S (Mₛ r)] (g : (r : ↑s) → M →ₗ[S] Mₛ r)
      [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)], (∀ (r : ↑s), Module.Flat R (Mₛ r)) → Module.Flat R M
-- Lean.Parser.Types
Lean.Parser.InputContext.mk'.injEq : ∀ (inputString fileName : String) (fileMap : Lean.FileMap) (endPos : String.Pos.Raw)
  (endPos_valid : autoParam (endPos ≤ inputString.rawEndPos) Lean.Parser.InputContext.endPos_valid._autoParam)
  (inputString_1 fileName_1 : String) (fileMap_1 : Lean.FileMap) (endPos_1 : String.Pos.Raw)
  (endPos_valid_1 : autoParam (endPos_1 ≤ inputString_1.rawEndPos) Lean.Parser.InputContext.endPos_valid._autoParam),
  ({ inputString := inputString, fileName := fileName, fileMap := fileMap, endPos := endPos,
        endPos_valid := endPos_valid } =
      { inputString := inputString_1, fileName := fileName_1, fileMap := fileMap_1, endPos := endPos_1,
        endPos_valid := endPos_valid_1 }) =
    (inputString = inputString_1 ∧ fileName = fileName_1 ∧ fileMap = fileMap_1 ∧ endPos = endPos_1)
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.appendTag : {α : Type u_1} → Lean.Widget.TaggedText α → α → Lean.Widget.TaggedText α → Lean.Widget.TaggedText α
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.HasPullbacksOfInclusions.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [hasPullbackInl :
    ∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inl f],
  CategoryTheory.HasPullbacksOfInclusions C
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.isoProd_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  (CategoryTheory.Limits.biprod.isoProd X Y).inv =
    CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.of_toNNReal : ∀ {p q : ENNReal}, p.toNNReal.HolderConjugate q.toNNReal → p.HolderConjugate q
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.link2.match_5.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.Balanced → Sort u_3) (szr : ℕ)
  (k'' : α) (v'' : β k'') (l'' r'' : Std.DTreeMap.Internal.Impl α β)
  (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced)
  (h_1 :
    (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'' = Std.DTreeMap.Internal.Impl.leaf →
        motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (szr_1 : ℕ) →
      (k''_1 : α) →
        (v''_1 : β k''_1) →
          (l''_1 r''_1 : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1).Balanced) →
              Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'' =
                  Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1 →
                motive (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1) hr),
  (match hr' : Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'', hr with
    | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr hr'
    | Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1, hr => h_2 szr_1 k''_1 v''_1 l''_1 r''_1 hr hr') =
    h_2 szr k'' v'' l'' r'' hr ⋯
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Slice.0.String.Slice.contains.match_1.congr_eq_1 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.SearchStep s → Sort u_1) (x : String.Slice.Pattern.SearchStep s)
  (h_1 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched startPos endPos))
  (h_2 : (x : String.Slice.Pattern.SearchStep s) → motive x) (startPos endPos : s.Pos),
  x = String.Slice.Pattern.SearchStep.matched startPos endPos →
    (match x with
      | String.Slice.Pattern.SearchStep.matched startPos endPos => h_1 startPos endPos
      | x => h_2 x) ≍
      h_1 startPos endPos
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.natDegree_notMem_eraseLead_support : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.natDegree ∉ f.eraseLead.support
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
DFinsupp.linearIndependent_single_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] {φ : ι → Type u_4} (f : (i : ι) → φ i → M i),
  (LinearIndependent R fun ix => fun₀ | ix.fst => f ix.fst ix.snd) ↔ ∀ (i : ι), LinearIndependent R (f i)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.toOrderHom_eq_coe : ∀ {α : Type u_2} {β : Type u_3} {x : Preorder α} {x_1 : Preorder β} {x_2 : MulOneClass α} {x_3 : MulOneClass β}
  (f : α →*o β), f.toOrderHom = ↑f
-- Mathlib.Topology.CompactOpen
ContinuousMap.nhds_compactOpen : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)),
  nhds f =
    ⨅ K,
      ⨅ (_ : IsCompact K),
        ⨅ U, ⨅ (_ : IsOpen U), ⨅ (_ : Set.MapsTo (⇑f) K U), Filter.principal {g | Set.MapsTo (⇑g) K U}
-- Mathlib.Order.Interval.Multiset
Multiset.left_notMem_Ioc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, a ∉ Multiset.Ioc a b
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- Applying a pseudoelement to a composition of morphisms is the same as composing
with each morphism. Sadly, this is not a definitional equality, but at least it is true.  -/
CategoryTheory.Abelian.Pseudoelement.comp_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R) (a : CategoryTheory.Abelian.Pseudoelement P),
  CategoryTheory.Abelian.Pseudoelement.pseudoApply (CategoryTheory.CategoryStruct.comp f g) a =
    CategoryTheory.Abelian.Pseudoelement.pseudoApply g (CategoryTheory.Abelian.Pseudoelement.pseudoApply f a)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.points : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_5} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → {n : ℕ} → Affine.Simplex k P n → Fin (n + 1) → P
-- Batteries.Data.PairingHeap
/-- `O(n log n)`. Convert the heap to an array in increasing order.  -/
Batteries.PairingHeap.toArray : {α : Type u} → {le : α → α → Bool} → Batteries.PairingHeap α le → Array α
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ),
  (1 - Polynomial.X ^ 2) * Polynomial.derivative (Polynomial.Chebyshev.T R (n + 1)) =
    (↑n + 1) * (Polynomial.Chebyshev.T R n - Polynomial.X * Polynomial.Chebyshev.T R (n + 1))
-- Mathlib.Algebra.Category.BoolRing
BoolRing.Iso.mk_hom_hom' : ∀ {α β : BoolRing} (e : ↑α ≃+* ↑β), (BoolRing.Iso.mk e).hom.hom' = ↑e
-- Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
CategoryTheory.Monoidal.functorHasRightDual : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Groupoid C] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          [CategoryTheory.RightRigidCategory D] → (F : CategoryTheory.Functor C D) → CategoryTheory.HasRightDual F
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.hom_id : ∀ (X : UniformSpaceCat), UniformSpaceCat.Hom.hom (CategoryTheory.CategoryStruct.id X) = ⟨id, ⋯⟩
-- Mathlib.Order.ScottContinuity.Complete
scottContinuous_inf_left : ∀ {β : Type u_2} [inst : CompleteLinearOrder β] (b : β), ScottContinuous fun a => min a b
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` preserves colimits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves
limits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.preservesLimit_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesColimit K.leftOp F.unop],
  CategoryTheory.Limits.PreservesLimit K F
-- Mathlib.RingTheory.Localization.Module
Module.Basis.ofIsLocalizedModule.eq_1 : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ]
  [inst_2 : Algebra R Rₛ] [inst_3 : IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid Mₛ] [inst_7 : Module R Mₛ] [inst_8 : Module Rₛ Mₛ]
  [inst_9 : IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [inst_10 : IsLocalizedModule S f] {ι : Type u_5}
  (b : Module.Basis ι R M), Module.Basis.ofIsLocalizedModule Rₛ S f b = Module.Basis.mk ⋯ ⋯
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.op_Z : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) {X Y : C}
  {f : X ⟶ Y} (hf : W₁.MapFactorizationData W₂ f),
  (CategoryTheory.MorphismProperty.MapFactorizationData.op W₁ W₂ hf).Z = Opposite.op hf.Z
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.Nondegenerate.ker_eq_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.Nondegenerate → LinearMap.ker B = ⊥
-- Mathlib.Algebra.Homology.Double
/-- If `i` has no successor for the complex shape `c`,
then for any `X : C`, the functor which sends `K : HomologicalComplex C c`
to `X ⟶ K.X i` is corepresentable by `(single C c i).obj X`.  -/
HomologicalComplex.evalCompCoyonedaCorepresentableBySingle : {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 ι] →
                (∀ (j : ι), ¬c.Rel i j) →
                  (X : C) →
                    ((HomologicalComplex.eval C c i).comp
                          (CategoryTheory.coyoneda.obj (Opposite.op X))).CorepresentableBy
                      ((HomologicalComplex.single C c i).obj X)