mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.SuccPred.Basic
/-- Order equipped with a sensible predecessor function.  -/
PredOrder : (α : Type u_3) → [Preorder α] → Type u_3
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
_private.Mathlib.GroupTheory.SpecificGroups.Dihedral.0.DihedralGroup.mul.eq_2 : ∀ {n : ℕ} (a a_1 : ZMod n), DihedralGroup.mul✝ (DihedralGroup.r a) (DihedralGroup.sr a_1) = DihedralGroup.sr (a_1 - a)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- The third left fraction.  -/
CategoryTheory.MorphismProperty.LeftFraction₃.thd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction₃ X Y → W.LeftFraction X Y
-- Mathlib.Topology.Connected.PathConnected
isPathConnected_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {F : Set X},
  IsPathConnected F ↔ F.Nonempty ∧ ∀ x ∈ F, ∀ y ∈ F, JoinedIn F x y
-- Mathlib.Algebra.Order.Group.Synonym
toColex_zero : ∀ {α : Type u_1} [inst : Zero α], toColex 0 = 0
-- Mathlib.Algebra.Free
/-- From a magma homomorphism `α →ₙ* β` to a semigroup homomorphism
`Magma.AssocQuotient α →ₙ* Magma.AssocQuotient β`.  -/
Magma.AssocQuotient.map : {α : Type u} →
  [inst : Mul α] → {β : Type v} → [inst_1 : Mul β] → (α →ₙ* β) → Magma.AssocQuotient α →ₙ* Magma.AssocQuotient β
-- Mathlib.Probability.Process.Stopping
/-- Given stopping times `τ` and `η` which are bounded below, `Set.piecewise s τ η` is also
a stopping time with respect to the same filtration.  -/
MeasureTheory.IsStoppingTime.piecewise_of_le : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {𝒢 : MeasureTheory.Filtration ι m}
  {τ η : Ω → WithTop ι} {i : ι} {s : Set Ω} [inst_1 : DecidablePred fun x => x ∈ s],
  MeasureTheory.IsStoppingTime 𝒢 τ →
    MeasureTheory.IsStoppingTime 𝒢 η →
      (∀ (ω : Ω), ↑i ≤ τ ω) → (∀ (ω : Ω), ↑i ≤ η ω) → MeasurableSet s → MeasureTheory.IsStoppingTime 𝒢 (s.piecewise τ η)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.productMap_eq_comp_map : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : CommSemiring S] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R S]
  (f : A →ₐ[R] S) (g : B →ₐ[R] S),
  Algebra.TensorProduct.productMap f g = (Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map f g)
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_ofNatLT : ∀ {n : ℕ} (hn : n < 2 ^ 16), { toBitVec := n#'hn } = UInt16.ofNatLT n hn
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductCone_snd : ∀ (X Y : Type u), (CategoryTheory.Limits.Types.binaryProductCone X Y).snd = TypeCat.ofHom Prod.snd
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.OptionsPerPos : Type
-- Mathlib.Algebra.Group.Pi.Basic
Pi.commMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → CommMonoid (f i)] → CommMonoid ((i : I) → f i)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the reverse direction of `Units.mul_inv_le_one`. -/
Units.mul_inv_le_one_of_le : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a : M} (u : Mˣ), a ≤ ↑u → a * ↑u⁻¹ ≤ 1
-- Mathlib.Probability.Distributions.Exponential
/-- The pdf of the exponential distribution integrates to 1  -/
ProbabilityTheory.lintegral_exponentialPDF_eq_one : ∀ {r : ℝ}, 0 < r → ∫⁻ (x : ℝ), ProbabilityTheory.exponentialPDF r x = 1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.isSome_succMany?_of_lt_size_toArray : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst : Std.Rxi.IsAlwaysFinite α] {i : ℕ}, i < r.toArray.size → (Std.PRange.succMany? (i + 1) r.lower).isSome = true
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic p K)` (in particular for `K = ℚ`) and `p` is an odd prime,
then the norm of `ζ - 1` is `p`.  -/
IsPrimitiveRoot.norm_sub_one_of_prime_ne_two' : ∀ {p : ℕ} {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L]
  [hpri : Fact (Nat.Prime p)] [hcyc : IsCyclotomicExtension {p} K L],
  IsPrimitiveRoot ζ p → Irreducible (Polynomial.cyclotomic p K) → p ≠ 2 → (Algebra.norm K) (ζ - 1) = ↑p
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.symm : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P}, s.IsDiameter p₁ p₂ → s.IsDiameter p₂ p₁
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂IdIso_inv_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {R : CategoryTheory.Functor C D} (T : D) (α : T ⟶ (CategoryTheory.Functor.id D).obj T)
  (β : R.comp (CategoryTheory.Functor.id D) ⟶ (CategoryTheory.Functor.id C).comp R)
  (hα : autoParam (α = CategoryTheory.CategoryStruct.id T) CategoryTheory.StructuredArrow.map₂IdIso._auto_1)
  (hβ :
    autoParam (β = CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv)
      CategoryTheory.StructuredArrow.map₂IdIso._auto_3)
  (X : CategoryTheory.StructuredArrow T R),
  ((CategoryTheory.StructuredArrow.map₂IdIso T α β hα hβ).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.symm_coordChangeL : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e]
  [inst_9 : Bundle.Trivialization.IsLinear R e'] {b : B},
  b ∈ e'.baseSet ∩ e.baseSet →
    (Bundle.Trivialization.coordChangeL R e e' b).symm = Bundle.Trivialization.coordChangeL R e' e b
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.moment_truncation_eq_intervalIntegral_of_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {A : ℝ} {n : ℕ},
      n ≠ 0 →
        0 ≤ f →
          ∫ (x : α), ProbabilityTheory.truncation f A x ^ n ∂μ = ∫ (y : ℝ) in 0..A, y ^ n ∂MeasureTheory.Measure.map f μ
-- Mathlib.NumberTheory.Chebyshev
Nat.lcmUpto_eq_prod : ∀ (n : ℕ), n.lcmUpto = ∏ p ∈ n.primesLE, p ^ n.lcmUpto.factorization p
-- Mathlib.Analysis.Calculus.Deriv.Abs
differentiableAt_abs : ∀ {x : ℝ}, x ≠ 0 → DifferentiableAt ℝ (fun x => |x|) x
-- Init.Data.Int.DivMod.Lemmas
Int.add_bmod : ∀ (a b : ℤ) (n : ℕ), (a + b).bmod n = (a.bmod n + b.bmod n).bmod n
-- Mathlib.Data.Multiset.Lattice
Multiset.sup_add : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s₁ s₂ : Multiset α), (s₁ + s₂).sup = s₁.sup ⊔ s₂.sup
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
/-- If `S` is a short exact short complex in a balanced category,
then `S.X₃` is the cokernel of `S.f`.  -/
CategoryTheory.ShortComplex.ShortExact.gIsCokernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Balanced C] →
        {S : CategoryTheory.ShortComplex C} →
          S.ShortExact → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
HomotopyCategory.singleFunctorsPostcompQuotientIso.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C],
  HomotopyCategory.singleFunctorsPostcompQuotientIso C = CategoryTheory.Iso.refl (HomotopyCategory.singleFunctors C)
-- Mathlib.Data.Fin.Basic
Fin.equivSubtype_symm_apply : ∀ {n : ℕ} (a : { i // i < n }), Fin.equivSubtype.symm a = ⟨↑a, ⋯⟩
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_zero : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] {f : Π₀ (i : ι), β i},
  (f.sum fun x x_1 => 0) = 0
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Catch.mk : Lean.Syntax → Lean.Syntax → Lean.Elab.Term.Do.CodeBlock → Lean.Elab.Term.Do.ToCodeBlock.Catch
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_mul_le : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.toSyn (m.degree (f * g)) ≤ m.toSyn (m.degree f + m.degree g)
-- Mathlib.Order.Hom.Lattice
OrderIsoClass.toLatticeHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : Lattice α] [inst_2 : Lattice β]
  [OrderIsoClass F α β], LatticeHomClass F α β
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_inv_atTop_atBot : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G],
  Filter.Tendsto Inv.inv Filter.atTop Filter.atBot
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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) {i j : EInt} (f : i ⟶ j) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj i).map ((t.eTruncLTι j).app X)) ((t.eTruncLT.map f).app X) =
    (t.eTruncLTι i).app ((t.eTruncLT.obj j).obj X)
-- Mathlib.Algebra.Group.Basic
left_eq_mul : ∀ {M : Type u_4} [inst : Monoid M] [IsLeftCancelMul M] {a b : M}, a = a * b ↔ b = 1
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instToJsonPosition.toJson : Lean.Lsp.Position → Lean.Json
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.SmallFilteredIntermediate.instFullInclusion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C),
  (CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion F).Full
-- Batteries.Data.Fin.Lemmas
Fin.find?_rev : ∀ {n : ℕ} {p : Fin n → Bool}, (Fin.find? fun x => p x.rev) = Option.map Fin.rev (Fin.findRev? p)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.containsThenInsertIfNew.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 →
    ∀ (a a_1 : α),
      a = a_1 → ∀ (b b_1 : β), b = b_1 → t.containsThenInsertIfNew a b = t_1.containsThenInsertIfNew a_1 b_1
-- Std.Data.String.ToNat
String.isNat_of_isDigit : ∀ {s : String}, s ≠ "" → (∀ c ∈ s.toList, c.isDigit = true) → s.isNat = true
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticRelatedInformation.mk.inj : ∀ {location : Lean.Lsp.Location} {message : String} {location_1 : Lean.Lsp.Location} {message_1 : String},
  { location := location, message := message } = { location := location_1, message := message_1 } →
    location = location_1 ∧ message = message_1
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- A point in a set is in its affine span.  -/
mem_spanPoints : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p : P) (s : Set P), p ∈ s → p ∈ spanPoints k s
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Icc_castAdd : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n),
  ∑ i ∈ Finset.Icc (Fin.castAdd m a) (Fin.castAdd m b), f i = ∑ i ∈ Finset.Icc a b, f (Fin.castAdd m i)
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.isUnit_toMatrix'_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  {f : (n → R) →ₗ[R] n → R}, IsUnit (LinearMap.toMatrix' f) ↔ IsUnit f
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A split mono `f` equalizes `(retraction f ≫ f)` and `(𝟙 Y)`.
Here we build the cone, and show in `isSplitMonoEqualizes` that it is a limit cone.
 -/
CategoryTheory.Limits.coneOfIsSplitMono : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.IsSplitMono f] →
          CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.id Y)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction f) f)
-- Init.Data.List.Lemmas
List.cons_append_fun : ∀ {α : Type u_1} {a : α} {as : List α}, (fun bs => a :: as ++ bs) = fun bs => a :: (as ++ bs)
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.coe_toIntAlgEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R ≃+* S), ⇑f.toIntAlgEquiv = ⇑f
-- Mathlib.Topology.Algebra.Support
mulTSupport_comp_subset_preimage : ∀ {X : Type u_1} {α : Type u_2} [inst : One α] [inst_1 : TopologicalSpace X] {Y : Type u_9}
  [inst_2 : TopologicalSpace Y] (g : Y → α) {f : X → Y}, Continuous f → mulTSupport (g ∘ f) ⊆ f ⁻¹' mulTSupport g
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The preceding piece of syntax, if available. It is not available if the cursor is
at the start of the next tactic. This is used for merging consecutive `rw` tactics.  -/
Mathlib.Tactic.ClickSuggestions.Context.stx : Mathlib.Tactic.ClickSuggestions.Context → Option (Lean.TSyntax `tactic)
-- Mathlib.Topology.Inseparable
SeparationQuotient.continuousOn_lift₂ : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y → Z}
  {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a c → Inseparable b d → f a b = f c d}
  {s : Set (SeparationQuotient X × SeparationQuotient Y)},
  ContinuousOn (Function.uncurry (SeparationQuotient.lift₂ f hf)) s ↔
    ContinuousOn (Function.uncurry f) (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s)
-- Mathlib.Algebra.Ring.Associator
AddMonoidHom.mulRight₃_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (x y z : R), ((AddMonoidHom.mulRight₃ x) y) z = x * (y * z)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.instHasTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C],
  CategoryTheory.Limits.HasTerminal (CategoryTheory.Limits.FormalCoproduct C)
-- Mathlib.Logic.Equiv.Defs
Equiv.sumIsLeft_apply : ∀ {α : Type u_1} {β : Type u_2} (x : { x // x.isLeft = true }), Equiv.sumIsLeft x = (↑x).getLeft ⋯
-- Lean.Elab.ErrorUtils
_private.Lean.Elab.ErrorUtils.0.Lean.instHasOxfordStringsString : Lean.HasOxfordStrings✝ String
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.Quotient.mk_vadd_out : ∀ {G : Type u} {X : Type v} [inst : AddGroup G] [inst_1 : AddMonoid X] [inst_2 : AddAction X G] (H : AddSubgroup G)
  [inst_3 : AddAction.QuotientAction X H] (b : X) (q : G ⧸ H), ↑(b +ᵥ Quotient.out q) = b +ᵥ q
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.of_smul : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (r : R) (x : L × M),
  (LieAlgebra.ofProd c) (r • x) = r • (LieAlgebra.ofProd c) x
-- Init.Data.Array.Basic
/-- Replaces the element at the given index, if it exists, with the result of applying `f` to it. If the
index is invalid, the array is returned unmodified.

Examples:
 * `#[1, 2, 3].modifyOp 0 (· * 10) = #[10, 2, 3]`
 * `#[1, 2, 3].modifyOp 2 (· * 10) = #[1, 2, 30]`
 * `#[1, 2, 3].modifyOp 3 (· * 10) = #[1, 2, 3]`
 -/
Array.modifyOp : {α : Type u} → Array α → ℕ → (α → α) → Array α
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.AffineEtale.instIsOneHypercoverDenseEtaleSpecTopologySmallEtaleTopology : ∀ {S : AlgebraicGeometry.Scheme},
  (AlgebraicGeometry.Scheme.AffineEtale.Spec S).IsOneHypercoverDense (AlgebraicGeometry.Scheme.AffineEtale.topology S)
    S.smallEtaleTopology
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.HomologySequence.snakeInput_L₀ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j),
  (HomologicalComplex.HomologySequence.snakeInput hS i j hij).L₀ =
    (HomologicalComplex.homologyFunctor C c i).mapShortComplex.obj S
-- Std.Time.Format
/-- The SQLDate format, which follows the pattern `uuuu-MM-dd` and is commonly used
in SQL databases to represent dates.
 -/
Std.Time.Formats.sqlDate : Std.Time.GenericFormat Std.Time.Awareness.any
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.aeSeqSet_measurableSet : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} {hf : ∀ (i : ι), AEMeasurable (f i) μ},
  MeasurableSet (aeSeqSet hf p)
-- Mathlib.Data.Finset.Basic
Finset.erase_cons_of_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Finset α} (ha : a ∉ s),
  a ≠ b → (Finset.cons a s ha).erase b = Finset.cons a (s.erase b) ⋯
-- Lean.Data.KVMap
Lean.DataValue.ofName.sizeOf_spec : ∀ (v : Lean.Name), sizeOf (Lean.DataValue.ofName v) = 1 + sizeOf v
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsMaxOn.hasLineDerivAt_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E} {f' : ℝ},
  IsMaxOn f s a → HasLineDerivAt ℝ f f' a b → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → f' = 0
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.eraseListₘ.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (l : List α),
  m.eraseListₘ l =
    match l with
    | [] => m
    | hd :: tl => (m.erase hd).eraseListₘ tl
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Sieve.generate.hcongr_4 : ∀ (C C' : Type u₁),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v₁, u₁} C) (inst' : CategoryTheory.Category.{v₁, u₁} C'),
      inst ≍ inst' →
        ∀ (X : C) (X' : C'),
          X ≍ X' →
            ∀ (R : CategoryTheory.Presieve X) (R' : CategoryTheory.Presieve X'),
              R ≍ R' → CategoryTheory.Sieve.generate R ≍ CategoryTheory.Sieve.generate R'
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.minKeyD fallback ∈ t
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_sdiff_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a b \ Set.Iic c = Set.Ioc (max a c) b
-- Mathlib.RingTheory.LocalRing.Pullback
/-- The first projection from the pullback of `f` and `g` to `A`.  -/
AlgHom.pullbackFst : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R B] →
                  [inst_5 : Semiring C] →
                    [inst_6 : Algebra R C] → (f : A →ₐ[R] C) → (g : B →ₐ[R] C) → ↥(f.pullback g) →ₐ[R] A
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccAboveEquiv_symm_apply_last : ∀ {n : ℕ} (x : { x // x ≠ Fin.last n }), (finSuccAboveEquiv (Fin.last n)).symm x = (↑x).castLT ⋯
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.CCPOProdProjs : ℕ → Lean.Expr → Array Lean.Expr
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compQuasiMeasurePreserving_comp : ∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} {γ : Type u_5}
  {mγ : MeasurableSpace γ} {ξ : MeasureTheory.Measure γ} (g : γ →ₘ[ξ] δ) {f : β → γ}
  (hf : MeasureTheory.Measure.QuasiMeasurePreserving f ν ξ) {f' : α → β}
  (hf' : MeasureTheory.Measure.QuasiMeasurePreserving f' μ ν),
  g.compQuasiMeasurePreserving (f ∘ f') ⋯ = (g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf'
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.inftyValuation_of_nonzero : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] {x : RatFunc F},
  x ≠ 0 → RatFunc.inftyValuationDef F x = WithZero.exp x.intDegree
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardFactors_eq_zero_iff_eq_zero_or_one : ∀ {n : ℕ}, ArithmeticFunction.cardFactors n = 0 ↔ n = 0 ∨ n = 1
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.instFunLike : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → FunLike (LocallyConstant X Y) X Y
-- Mathlib.Algebra.Order.Group.Equiv
toEquiv_toLexAddEquiv : ∀ (α : Type u_1) [inst : Add α], ↑(toLexAddEquiv α) = toLex
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.lift_prod : ∀ {ι : Type u} (c : ι → Cardinal.{v}),
  Cardinal.lift.{w, max v u} (Cardinal.prod c) = Cardinal.prod fun i => Cardinal.lift.{w, v} (c i)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The relation itself.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} {I₁ I₂ : S.Arrow} (self : I₁.Relation I₂) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.g₁ (CategoryTheory.CategoryStruct.comp I₁.f h) =
    CategoryTheory.CategoryStruct.comp self.g₂ (CategoryTheory.CategoryStruct.comp I₂.f h)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.not_infinite_of_exists_st : ∀ {x : ℝ*}, (∃ r, x.IsSt r) → ¬x.Infinite
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.evalAddHom_apply : ∀ {I : Type u} (f : I → Type v) [inst : (i : I) → Add (f i)] (i : I) (g : (i : I) → f i), (Pi.evalAddHom f i) g = g i
-- Lean.EnvExtension
Lean.SimplePersistentEnvExtensionDescr.exportEntriesFnEx? : {α σ : Type} →
  Lean.SimplePersistentEnvExtensionDescr α σ → Option (Lean.Environment → σ → List α → Lean.OLeanEntries (Array α))
-- Mathlib.Tactic.Widget.SelectPanelUtils
/-- Helper function to create a widget allowing to select parts of the main goal
and then display a link that will insert some tactic call.

The main argument is `mkCmdStr` which is a function creating the link text and the tactic call text.
The `helpMsg` argument is displayed when nothing is selected and `title` is used as a panel title.
The `onlyGoal` argument says whether the selected has to be in the goal. Otherwise it
can be in the local context.
The `onlyOne` argument says whether one should select only one sub-expression.
In every cases, all selected subexpressions should be in the main goal or its local context.

The last arguments `params` should not be provided so that the output
has type `Params → RequestM (RequestTask Html)` and can be fed to the `mk_rpc_widget%`
elaborator.

Note that the `pos` and `goalType` arguments to `mkCmdStr` could be extracted for the `Params`
argument but that extraction would happen in every example, hence it is factored out here.
We also make sure `mkCmdStr` is executed in the right context.
 -/
mkSelectionPanelRPC : {Params : Type} →
  [SelectInsertParamsClass Params] →
    (Array Lean.SubExpr.GoalsLocation →
        Lean.Expr → Params → Lean.MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw))) →
      String →
        String →
          optParam Bool true →
            optParam Bool false → Params → Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)
-- Init.System.IO
IO.FS.Stream.Buffer.mk : ByteArray → ℕ → IO.FS.Stream.Buffer