mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_inv_app_app_f : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D]
  (X : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D))
  (P : CategoryTheory.Idempotents.Karoubi C),
  (((CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso C D).inv.app X).app P).f = (X.map P.decompId_i).f
-- Mathlib.Algebra.Group.Conj
ConjClasses.instDecidableEqOfDecidableRelIsConj : {α : Type u} → [inst : Monoid α] → [DecidableRel IsConj] → DecidableEq (ConjClasses α)
-- Mathlib.Algebra.Order.UpperLower
LowerSet.Iic_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α], LowerSet.Iic 0 = 0
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.weightedSMul_congr : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (s t : Set α),
  μ s = μ t → MeasureTheory.weightedSMul μ s = MeasureTheory.weightedSMul μ t
-- Init.Data.Int.Lemmas
Int.negOfNat_mul_ofNat : ∀ (m n : ℕ), Int.negOfNat m * ↑n = Int.negOfNat (m * n)
-- Mathlib.Topology.MetricSpace.Defs
eq_of_dist_eq_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, dist x y = 0 → x = y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintParams.mk.injEq : ∀ (toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams) (textDocument : Lean.Lsp.TextDocumentIdentifier)
  (range : Lean.Lsp.Range) (toWorkDoneProgressParams_1 : Lean.Lsp.WorkDoneProgressParams)
  (textDocument_1 : Lean.Lsp.TextDocumentIdentifier) (range_1 : Lean.Lsp.Range),
  ({ toWorkDoneProgressParams := toWorkDoneProgressParams, textDocument := textDocument, range := range } =
      { toWorkDoneProgressParams := toWorkDoneProgressParams_1, textDocument := textDocument_1, range := range_1 }) =
    (toWorkDoneProgressParams = toWorkDoneProgressParams_1 ∧ textDocument = textDocument_1 ∧ range = range_1)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₃.X₁ = CategoryTheory.Limits.cokernel f
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_le_iff : ∀ {u : ℕ → ENNReal} {a : EReal}, ExpGrowth.expGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ (b * ↑n).exp
-- Init.Data.List.Scan.Lemmas
List.tail_scanr : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β},
  0 < l.length → (List.scanr f b l).tail = List.scanr f b l.tail
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_powerset_sdiff_elem : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : Set α → M} {s : Set α} {a : α},
  s.Finite →
    a ∈ s →
      ∑ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t =
        ∑ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t + ∑ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.π_comp_colimitOpIsoOpLimit_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j).op
      (CategoryTheory.Limits.colimitOpIsoOpLimit F).inv =
    CategoryTheory.Limits.colimit.ι F.op (Opposite.op j)
-- Init.Omega.Logic
Lean.Omega.Decidable.and_not_of_not_imp : ∀ {a b : Prop} [Decidable a], ¬(a → b) → a ∧ ¬b
-- Mathlib.Topology.Order.OrderClosed
Ico_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {a b x : α},
  b < x → x < a → Set.Ico b a ∈ nhds x
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.bijective : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N), Function.Bijective ⇑e
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.π_map : ∀ (M : Type u_1) [inst : Monoid M] (X : Type u) [inst_1 : MulAction M X] (p q : CategoryTheory.ActionCategory M X)
  (f : p ⟶ q), (CategoryTheory.ActionCategory.π M X).map f = ↑f
-- Mathlib.NumberTheory.Divisors
Nat.divisorsAntidiagonal_zero : Nat.divisorsAntidiagonal 0 = ∅
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.ofHom₂_compr₂ : ∀ {R : Type u} [inst : CommRing R] {M N P Q : ModuleCat R} (f : ↑M →ₗ[R] ↑N →ₗ[R] ↑P) (g : ↑P →ₗ[R] ↑Q),
  ModuleCat.ofHom₂ (f.compr₂ g) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom₂ f)
      (ModuleCat.ofHom (CategoryTheory.Linear.rightComp R N (ModuleCat.ofHom g)))
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.fastLegendreSym.eq : legendreSym = fastLegendreSym✝
-- Mathlib.Data.Fintype.Basic
seqOfForallFinsetExistsAux.eq_1 : ∀ {α : Type u_4} [inst : DecidableEq α] (P : α → Prop) (r : α → α → Prop)
  (h : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y) (x : ℕ),
  seqOfForallFinsetExistsAux P r h x = Classical.choose ⋯
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.ReducedWord.mk : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      G →
        (toList : List (ℤˣ × G)) →
          List.IsChain (fun a b => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) toList →
            HNNExtension.NormalWord.ReducedWord G A B
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.aevalDifferentialEquiv_apply : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) (x : σ → S),
  P.aevalDifferentialEquiv x = P.aevalDifferential x
-- Mathlib.NumberTheory.FactorisationProperties
Nat.deficient_three : Nat.Deficient 3
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.holder.eq_1 : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {p q : ENNReal} (r : ENNReal) [hpqr : p.HolderTriple q r]
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G]
  (B : E →L[𝕜] F →L[𝕜] G) (f : ↥(MeasureTheory.Lp E p μ)) (g : ↥(MeasureTheory.Lp F q μ)),
  ContinuousLinearMap.holder r B f g = MeasureTheory.MemLp.toLp (fun x => (B (↑↑f x)) (↑↑g x)) ⋯
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertList.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)), Std.Internal.List.insertList l [] = l
-- Mathlib.NumberTheory.KummerDedekind
/-- The isomorphism of rings between `S / I` and `(R / I)[X] / minpoly x` when `I`
and `(conductor R x) ∩ R` are coprime.
 -/
KummerDedekind.quotMapEquivQuotQuotMap : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {x : S} →
            {I : Ideal R} →
              [IsDomain R] →
                [IsIntegrallyClosed R] →
                  [IsDedekindDomain S] →
                    [Module.IsTorsionFree R S] →
                      Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤ →
                        IsIntegral R x →
                          S ⧸ Ideal.map (algebraMap R S) I ≃+*
                            Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}
-- Mathlib.Data.Set.Card
Set.encard_preimage_of_bijective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Bijective f → ∀ (t : Set β), (f ⁻¹' t).encard = t.encard
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Finset.prod_lt_prod : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R]
  [PosMulStrictMono R] [Nontrivial R] {f g : ι → R} {s : Finset ι},
  (∀ i ∈ s, 0 < f i) → (∀ i ∈ s, f i ≤ g i) → (∃ i ∈ s, f i < g i) → ∏ i ∈ s, f i < ∏ i ∈ s, g i
-- Mathlib.Data.Finset.Insert
Finset.subset_singleton_iff : ∀ {α : Type u_1} {s : Finset α} {a : α}, s ⊆ {a} ↔ s = ∅ ∨ s = {a}
-- Mathlib.Combinatorics.Colex
/-- Initial segments are nested in some way. In particular, if they're the same size they're equal.
 -/
Finset.Colex.IsInitSeg.total : ∀ {α : Type u_1} [inst : LinearOrder α] {𝒜₁ 𝒜₂ : Finset (Finset α)} {r : ℕ},
  Finset.Colex.IsInitSeg 𝒜₁ r → Finset.Colex.IsInitSeg 𝒜₂ r → 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- An injective affine map from a finite-dimensional space is automatically anti-Lipschitz.  -/
AffineMap.antilipschitzWith_of_finiteDimensional : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  {PE : Type u_1} {PF : Type u_2} [inst_6 : MetricSpace PE] [inst_7 : NormedAddTorsor E PE] [inst_8 : MetricSpace PF]
  [inst_9 : NormedAddTorsor F PF] [FiniteDimensional 𝕜 E] {f : PE →ᵃ[𝕜] PF},
  Function.Injective ⇑f → ∃ K, AntilipschitzWith K ⇑f
-- Mathlib.Topology.Maps.Strict.Group
/-- An additive group homomorphism is strict if and only if the canonical isomorphism
`G ⧸ f.ker ≃ f.range` is a homeomorphism.  -/
AddMonoidHom.isStrictMap_iff_isHomeomorph_quotientKerEquivRange : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {f : G →+ H} [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace H], Topology.IsStrictMap ⇑f ↔ IsHomeomorph ⇑(QuotientAddGroup.quotientKerEquivRange f)
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.mor₁_πQ_assoc : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C} {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃}
  {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)},
  CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    ∀ {Q : A} (β : X₃ ⟶ ι.obj Q) [inst_7 : ι.Full] [inst_8 : CategoryTheory.Preadditive A] [ι.Faithful] {Z : A}
      (h : Q ⟶ Z),
      CategoryTheory.CategoryStruct.comp f₁
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Triangulated.AbelianSubcategory.πQ f₂ β) h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (j : C),
  ((t.triangleLTLTGELT a b h).obj j).mor₃ =
    CategoryTheory.CategoryStruct.comp ((t.truncGEδLT a).app ((t.truncLT b).obj j))
      ((CategoryTheory.shiftFunctor C 1).map ((t.truncLT a).map ((t.truncLTι b).app j)))
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instLawfulBEq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp] [inst_1 : Std.TransCmp cmp]
  [inst_2 : (k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)], LawfulBEq (Std.ExtDTreeMap α β cmp)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_single.eq_1 : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K),
  NumberField.mixedEmbedding.fundamentalCone.expMap_single w =
    { toFun := fun x => Real.exp ((↑w.mult)⁻¹ * x), invFun := fun x => ↑w.mult * Real.log x, source := Set.univ,
      target := Set.Ioi 0, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, continuousOn_toFun := ⋯,
      continuousOn_invFun := ⋯, open_source := NumberField.mixedEmbedding.fundamentalCone.expMap_single._proof_7,
      open_target := NumberField.mixedEmbedding.fundamentalCone.expMap_single._proof_8 }
-- Mathlib.CategoryTheory.Abelian.Images
CategoryTheory.Abelian.coimageImageComparisonFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  {f g : CategoryTheory.Arrow C} (η : f ⟶ g),
  CategoryTheory.Abelian.coimageImageComparisonFunctor.map η =
    CategoryTheory.Arrow.homMk
      (CategoryTheory.Limits.cokernel.map (CategoryTheory.Limits.kernel.ι f.hom) (CategoryTheory.Limits.kernel.ι g.hom)
        (CategoryTheory.Limits.kernel.map f.hom g.hom (CategoryTheory.Arrow.Hom.left η)
          (CategoryTheory.Arrow.Hom.right η) ⋯)
        (CategoryTheory.Arrow.Hom.left η) ⋯)
      (CategoryTheory.Limits.kernel.map (CategoryTheory.Limits.cokernel.π f.hom)
        (CategoryTheory.Limits.cokernel.π g.hom) (CategoryTheory.Arrow.Hom.right η)
        (CategoryTheory.Limits.cokernel.map f.hom g.hom (CategoryTheory.Arrow.Hom.left η)
          (CategoryTheory.Arrow.Hom.right η) ⋯)
        ⋯)
      ⋯
-- Mathlib.AlgebraicGeometry.Sites.Etale
/-- The pretopology generating the small étale site.  -/
AlgebraicGeometry.Scheme.smallEtalePretopology : (X : AlgebraicGeometry.Scheme) → CategoryTheory.Pretopology X.Etale
-- Mathlib.CategoryTheory.Category.PartialFun
/-- Constructs a partial function isomorphism between types from an equivalence between them.  -/
PartialFun.Iso.mk : {α β : PartialFun} → α ≃ β → (α ≅ β)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_injective : ∀ (k : Type u_1) {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] [IsDomain k] [Module.IsTorsionFree k V1] {p₀ p₁ : P1},
  p₀ ≠ p₁ → Function.Injective ⇑(AffineMap.lineMap p₀ p₁)
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitude_restrict_eq_comap_subtype : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)),
  (s.restrict S hS).altitude i = AffineSubspace.comap S.subtype (s.altitude i)
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.trans_transPartialEquiv : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : α ≃ β) (e' : β ≃ γ) (f'' : PartialEquiv γ δ),
  (e.trans e').transPartialEquiv f'' = e.transPartialEquiv (e'.transPartialEquiv f'')
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.modifyTop : (Lean.Meta.SynthInstance.GeneratorNode → Lean.Meta.SynthInstance.GeneratorNode) → Lean.Meta.SynthInstance.SynthM Unit
-- Mathlib.Topology.Maps.Basic
/-- **Alias** of the reverse direction of `Topology.isCoinducing_iff_isClosed`. -/
Topology.IsCoinducing.of_isClosed_preimage_iff_isClosed : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  (∀ (s : Set Y), IsClosed (f ⁻¹' s) ↔ IsClosed s) → Topology.IsCoinducing f
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α} {k : α}, k ∈ m.insertMany l ↔ k ∈ m ∨ l.contains k = true
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.finite_setOfPred_isRestriction : ∀ {α : Type u_1} (M : Matroid α) [M.Finite], {N | N.IsRestriction M}.Finite
-- Init.Data.Option.Basic
/-- Applies a function to a two optional values if both are present. Otherwise, if one value is present,
it is returned and the function is not used.

The value is `some (fn a b)` if the inputs are `some a` and `some b`. Otherwise, the behavior is
equivalent to `Option.orElse`: if only one input is `some x`, then the value is `some x`, and if
both are `none`, then the value is `none`.

Examples:
 * `Option.merge (· + ·) none (some 3) = some 3`
 * `Option.merge (· + ·) (some 2) (some 3) = some 5`
 * `Option.merge (· + ·) (some 2) none = some 2`
 * `Option.merge (· + ·) none none = none`
 -/
Option.merge : {α : Type u_1} → (α → α → α) → Option α → Option α → Option α
-- Init.Data.List.Basic
List.append.eq_2 : ∀ {α : Type u_1} (x : List α) (a : α) (as : List α), (a :: as).append x = a :: as.append x
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_roc_eq_mkSlice_roo : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Roo.Sliceable.mkSlice xs lo<...hi + 1
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.integral_zero : ∀ (α : Type u_1) (E : Type u_2) [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E], MeasureTheory.L1.integral 0 = 0
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.surjective_toQuotient : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A), Function.Surjective ⇑relations.toQuotient
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.frequently_filterAt_iff : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) {x : X} {P : Set X → Prop},
  (∃ᶠ (t : Set X) in v.filterAt x, P t) ↔ ∀ ε > 0, ∃ t ∈ v.setsAt x, t ⊆ Metric.closedBall x ε ∧ P t
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.Limits.PullbackCone.mk.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X)
  (snd : W ⟶ Y) (eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g),
  CategoryTheory.Limits.PullbackCone.mk fst snd eq =
    { pt := W,
      π :=
        {
          app := fun j =>
            Option.casesOn j (CategoryTheory.CategoryStruct.comp fst f) fun j' =>
              CategoryTheory.Limits.WalkingPair.casesOn j' fst snd,
          naturality := ⋯ } }
-- Mathlib.Tactic.ApplyCongr
Lean.Parser.Tactic.applyCongr : Lean.ParserDescr
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.bot_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β]
  (a : α), ⊥ a = ⊥
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
ChainComplex.isoHomologyι₀_inv_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : ChainComplex C ℕ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomology K 0]
  [inst_3 : HomologicalComplex.HasHomology L 0],
  CategoryTheory.CategoryStruct.comp K.isoHomologyι₀.inv (HomologicalComplex.homologyMap φ 0) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ 0) L.isoHomologyι₀.inv
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → t.maxKey? = t_1.maxKey?
-- Mathlib.FieldTheory.RatFunc.Luroth
RatFunc.Luroth.algEquiv_algebraMap : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥) (g : Polynomial K),
  ↑((RatFunc.Luroth.algEquiv h) ((algebraMap (Polynomial K) (RatFunc K)) g)) =
    (Polynomial.aeval (RatFunc.Luroth.generator E)) g
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.aemeasurable : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X c μ → AEMeasurable X μ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyIncomingCall.mk.injEq : ∀ («from» : Lean.Lsp.CallHierarchyItem) (fromRanges : Array Lean.Lsp.Range) (from_1 : Lean.Lsp.CallHierarchyItem)
  (fromRanges_1 : Array Lean.Lsp.Range),
  ({ «from» := «from», fromRanges := fromRanges } = { «from» := from_1, fromRanges := fromRanges_1 }) =
    («from» = from_1 ∧ fromRanges = fromRanges_1)
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.mul_le_mul : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] {M N P Q : AddSubmonoid R}, M ≤ P → N ≤ Q → M * N ≤ P * Q
-- Mathlib.Data.Matrix.Basis
Matrix.liftLinear_single : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} (S : Type u_6) {α : Type u_7} {β : Type u_8} [inst : DecidableEq m]
  [inst_1 : DecidableEq n] [inst_2 : Fintype m] [inst_3 : Fintype n] [inst_4 : Semiring R] [inst_5 : Semiring S]
  [inst_6 : AddCommMonoid α] [inst_7 : AddCommMonoid β] [inst_8 : Module R α] [inst_9 : Module R β]
  [inst_10 : Module S β] [inst_11 : SMulCommClass R S β] (f : m → n → α →ₗ[R] β) (i : m) (j : n) (a : α),
  ((Matrix.liftLinear S) f) (Matrix.single i j a) = (f i j) a
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.card_Ico : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [inst_3 : (i : ι) → Zero (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)]
  (f g : Π₀ (i : ι), α i), (Finset.Ico f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 1
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioc_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Ioc a b)), Subtype.val '' Set.Iio c = Set.Ioo a ↑c
-- Init.Data.List.Lemmas
List.filter_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α} {p : α → Bool},
  List.filter p (List.replicate n a) = if p a = true then List.replicate n a else []
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin.0.Fin.reduceBoolPred : Lean.Name → ℕ → (ℕ → ℕ → Bool) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Order.Basic
/-- **Alias** of `lt_of_lt_of_eq''`. -/
LT.lt.trans_eq' : ∀ {α : Type u_1} {a b c : α} [inst : LT α], b < a → b = c → c < a
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.uniqueHomToTrivial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : CategoryTheory.Comon C) → Unique (A ⟶ CategoryTheory.Comon.trivial C)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  (h : t.WF) {k : α} {f : β → β} {hc : k ∈ Std.DTreeMap.Raw.Const.modify t k f},
  Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.Const.modify t k f) k hc = f (Std.DTreeMap.Raw.Const.get t k ⋯)
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.mem_inv_pointwise_smul_iff₀ : ∀ {M : Type u_1} {R : Type u_2} [inst : GroupWithZero M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {a : M},
  a ≠ 0 → ∀ (S : Subring R) (x : R), x ∈ a⁻¹ • S ↔ a • x ∈ S
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.instIsMultiplicativeLocalEpi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C},
  P.localEpi.IsMultiplicative
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instIsDomain : ∀ {R : Type u_1} [inst : Ring R] [IsDomain R], IsDomain Rᵃᵒᵖ
-- Mathlib.Algebra.Group.Units.Hom
isAddUnit_map_of_leftInverse : ∀ {F : Type u_1} {G : Type u_2} {M : Type u_3} {N : Type u_4} [inst : FunLike F M N] [inst_1 : FunLike G N M]
  [inst_2 : AddMonoid M] [inst_3 : AddMonoid N] [AddMonoidHomClass F M N] [AddMonoidHomClass G N M] {f : F} {x : M}
  (g : G), Function.LeftInverse ⇑g ⇑f → (IsAddUnit (f x) ↔ IsAddUnit x)
-- Mathlib.CategoryTheory.EpiMono
/-- `IsSplitEpi f` is the assertion that `f` admits a section  -/
CategoryTheory.IsSplitEpi : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (X ⟶ Y) → Prop