mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Limits
/-- `colimitCocone F` is colimit.  -/
CategoryTheory.ShortComplex.isColimitColimitCocone : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) →
            [inst_3 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] →
              [inst_4 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] →
                [inst_5 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.colimitCocone F)
-- Aesop.Tree.Data
Aesop.instInhabitedGoalId.default : Aesop.GoalId
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentRegistrationOptions.mk.injEq : ∀ (documentSelector? documentSelector?_1 : Option Lean.Lsp.DocumentSelector),
  ({ documentSelector? := documentSelector? } = { documentSelector? := documentSelector?_1 }) =
    (documentSelector? = documentSelector?_1)
-- Lean.Parser.Extension
Lean.Parser.getAlias : {α : Type} → IO.Ref (Lean.Parser.AliasTable α) → Lean.Name → IO (Option (Lean.Parser.AliasValue α))
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialTermInfo.mk : Lean.Elab.ElabInfo → Lean.LocalContext → Option Lean.Expr → Lean.Elab.PartialTermInfo
-- Init.Data.AC
Lean.Data.AC.ContextInformation.mk : {α : Sort u} → (α → ℕ → Bool) → (α → Bool) → (α → Bool) → Lean.Data.AC.ContextInformation α
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count.isFiniteMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Finite α], MeasureTheory.IsFiniteMeasure MeasureTheory.Measure.count
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_prod : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) {ι : Type u_1}
  (g : ι → Polynomial R) (s : Finset ι), Polynomial.map f (∏ i ∈ s, g i) = ∏ i ∈ s, Polynomial.map f (g i)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
IsLocalRing.specializes_closedPoint : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : IsLocalRing R] (x : PrimeSpectrum R), x ⤳ IsLocalRing.closedPoint R
-- Mathlib.Logic.Encodable.Basic
/-- Explicit encoding function for the sum of two encodable types.  -/
Encodable.encodeSum : {α : Type u_1} → {β : Type u_2} → [Encodable α] → [Encodable β] → α ⊕ β → ℕ
-- Batteries.Data.Vector.Lemmas
_private.Batteries.Data.Vector.Lemmas.0.Vector.scanlM.loop_toArray : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : ℕ} [inst : Monad m] [LawfulMonad m] (f : β → α → m β)
  (as : Vector α n) (h_stop : n ≤ as.toArray.size) (i : ℕ) (hi : i ≤ n) (cur : β) (acc_v : Vector β i)
  (acc_a : Array β),
  acc_v.toArray = acc_a →
    Vector.toArray <$> Vector.scanlM.loop f as cur i hi acc_v = Array.scanlM.loop f cur as.toArray i n h_stop acc_a
-- Mathlib.Order.Filter.CardinalInter
Filter.cardinalInterFilter_sup : ∀ {α : Type u} (l₁ l₂ : Filter α) {c₁ c₂ : Cardinal.{u}} [CardinalInterFilter l₁ c₁] [CardinalInterFilter l₂ c₂],
  CardinalInterFilter (l₁ ⊔ l₂) (min c₁ c₂)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.mono : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f s x → ∀ {t : Set E}, t ⊆ s → ContDiffWithinAt 𝕜 n f t x
-- Mathlib.Algebra.Group.Invertible.Basic
/-- An `Invertible` element is a unit.  -/
unitOfInvertible : {α : Type u} → [inst : Monoid α] → (a : α) → [Invertible a] → αˣ
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Append.0.Std.IterM.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.CategoryTheory.Monad.Basic
/-- An isomorphism of monads gives a natural isomorphism of the underlying functors.
 -/
CategoryTheory.MonadIso.toNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {M N : CategoryTheory.Monad C} → (M ≅ N) → (M.toFunctor ≅ N.toFunctor)
-- Mathlib.Control.Fix
_private.Mathlib.Control.Fix.0.Part.Fix.approx.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((i : ℕ) → motive i.succ) → motive x
-- Mathlib.LinearAlgebra.Complex.Module
imaginaryPart_smul : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  (z : ℂ) (a : A), imaginaryPart (z • a) = z.re • imaginaryPart a + z.im • realPart a
-- Mathlib.Algebra.Group.Action.Defs
AddSemigroupAction.mk : {G : Type u_9} →
  {P : Type u_10} →
    [inst : AddSemigroup G] →
      [toVAdd : VAdd G P] → (∀ (g₁ g₂ : G) (p : P), (g₁ + g₂) +ᵥ p = g₁ +ᵥ g₂ +ᵥ p) → AddSemigroupAction G P
-- Mathlib.Topology.Convenient.OpenClosed
Topology.IsOpenEmbedding.isGeneratedBy : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type u_3}
  [inst_1 : TopologicalSpace Y] [∀ (i : ι) (U : TopologicalSpace.Opens (X i)), Topology.IsGeneratedBy X ↥U]
  [Topology.IsGeneratedBy X Y] {F : Type u_4} [inst_4 : TopologicalSpace F] {f : F → Y},
  Topology.IsOpenEmbedding f → Topology.IsGeneratedBy X F
-- Batteries.Tactic.Trans
Batteries.Tactic.TransRelation.implies.sizeOf_spec : ∀ (name : Lean.Name) (bi : Lean.BinderInfo),
  sizeOf (Batteries.Tactic.TransRelation.implies name bi) = 1 + sizeOf name + sizeOf bi
-- Init.Data.List.Basic
List.range'_one : ∀ {s step : ℕ}, List.range' s 1 step = [s]
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_self_eq_norm_mul_norm : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x : F), RCLike.re (inner 𝕜 x x) = ‖x‖ * ‖x‖
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isColoop_iff_mem_coloops : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsColoop e ↔ e ∈ M.coloops
-- Aesop.Search.SearchM
Aesop.incrementIteration : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q Unit
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- `AbstractMeasure.contractFst` bundled with continuity in the function argument.  -/
AbstractMeasure.contractFstCLM : {X : Type u_1} →
  {Y : Type u_2} →
    {R : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : CommRing R] →
            [inst_3 : TopologicalSpace R] →
              [inst_4 : IsTopologicalRing R] →
                [LocallyCompactSpace X] →
                  [inst_6 : LocallyCompactSpace Y] → AbstractMeasure X R R →ₗ[R] C(X × Y, R) →L[R] C(Y, R)
-- Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree
/-- The isomorphism between the zeroth cocycles and the kernel of the zeroth differential.  -/
ContinuousCohomology.cocycles₀Iso : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] →
            [inst_4 : IsTopologicalGroup G] →
              (X : TopRep k G) →
                ContinuousCohomology.cocycles X 0 ≅
                  TopModuleCat.of k ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) (i₁ i₂ i₃ : J) (h₁₂ : i₁ ≤ i₂) (h₂₃ : i₂ ≤ i₃) (h : i₃ ≤ Order.succ j),
  CategoryTheory.SmallObject.SuccStruct.extendToSucc.map hj F τ i₁ i₃ ⋯ h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.extendToSucc.map hj F τ i₁ i₂ h₁₂ ⋯)
      (CategoryTheory.SmallObject.SuccStruct.extendToSucc.map hj F τ i₂ i₃ h₂₃ h)
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- Let `X` be an extended metric space. Let `K : ι → Set X` be a locally finite family of closed
sets, let `U : ι → Set X` be a family of open sets such that `K i ⊆ U i` for all `i`. Then there
exists a positive continuous function `δ : C(X, ℝ)` such that for any `i` and `x ∈ K i`,
we have `Metric.closedEBall x (ENNReal.ofReal (δ x)) ⊆ U i`.  -/
Metric.exists_continuous_real_forall_closedEBall_subset : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K →
          ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedEBall x (ENNReal.ofReal (δ x)) ⊆ U i
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concat_dropLast : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : G.Adj p.penultimate v), p.dropLast.concat hp = p
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- There are `r * t` vertices in a complete equipartite subgraph with `r` parts of size `t`.  -/
SimpleGraph.CompleteEquipartiteSubgraph.card_verts : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (K : G.CompleteEquipartiteSubgraph r t), K.verts.card = r * t
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.Functor.commShiftOp_iso_eq : ∀ {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] (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] (F : CategoryTheory.Functor C D)
  [inst_5 : F.CommShift A] (a : A),
  CategoryTheory.Functor.commShiftIso (CategoryTheory.OppositeShift.functor A F) a =
    (CategoryTheory.NatIso.op (CategoryTheory.Functor.commShiftIso F a)).symm
-- Mathlib.Data.Part
Part.inv_mem_inv : ∀ {α : Type u_1} [inst : Inv α] (a : Part α), ∀ ma ∈ a, ma⁻¹ ∈ a⁻¹
-- Std.Time.DateTime.Timestamp
/-- Subtracts a `Week.Offset` from the given `Timestamp`.
 -/
Std.Time.Timestamp.subWeeks : Std.Time.Timestamp → Std.Time.Week.Offset → Std.Time.Timestamp
-- Mathlib.Algebra.Colimit.Finiteness
Module.fgSystem.equiv_comp_of : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq (Submodule R M)] (N : { N // N.FG }),
  ↑(Module.fgSystem.equiv R M) ∘ₗ Module.DirectLimit.of R { N // N.FG } (fun i => ↥↑i) (Module.fgSystem R M) N =
    (↑N).subtype
-- Mathlib.NumberTheory.Dioph
Dioph.reindex_dioph : ∀ {α : Type u} (β : Type u) {S : Set (α → ℕ)} (f : α → β), Dioph S → Dioph {v | v ∘ f ∈ S}
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.drain_eq_map_toList : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  it.drain = (fun x => PUnit.unit) <$> it.toList
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G], (groupHomology.chainsFunctor k G).PreservesZeroMorphisms
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.IntFractPair.mapFr.eq_1 : ∀ {K : Type u_1} {β : Type u_2} (f : K → β) (gp : GenContFract.IntFractPair K),
  GenContFract.IntFractPair.mapFr f gp = { b := gp.b, fr := f gp.fr }
-- Mathlib.Analysis.Normed.Field.Basic
/-- A normed field is nontrivially normed
provided that the norm of some nonzero element is not one.  -/
NontriviallyNormedField.ofNormNeOne : {𝕜 : Type u_5} → [h' : NormedField 𝕜] → (∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1) → NontriviallyNormedField 𝕜
-- Mathlib.Tactic.Linarith.Verification
/-- If `prf` is a proof of `t R s`, `leftOfIneqProof prf` returns `t`.  -/
Mathlib.Tactic.Linarith.leftOfIneqProof : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.all_slice_iff : ∀ {pat s : String.Slice}, s.all pat = true ↔ ∃ n, s.copy = String.join (List.replicate n pat.copy)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularWRT.eq_of_innerRegularWRT_of_forall_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q : Set α → Prop}
  {ν : MeasureTheory.Measure α},
  μ.InnerRegularWRT p q → ν.InnerRegularWRT p q → (∀ (U : Set α), p U → μ U = ν U) → ∀ {U : Set α}, q U → μ U = ν U
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.congr_var : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution solution' : relations.Solution M},
  solution = solution' → ∀ (g : relations.G), solution.var g = solution'.var g
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.HasPairwisePullbacks.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Presieve X},
  (∀ {Y Z : C} {f : Y ⟶ X}, R f → ∀ {g : Z ⟶ X}, R g → CategoryTheory.Limits.HasPullback f g) → R.HasPairwisePullbacks
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- The indicators of δ-thickenings of a set tend pointwise to the indicator of the
set, as δ>0 tends to zero.  -/
tendsto_indicator_thickening_indicator_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
  (f : α → β) (E : Set α),
  Filter.Tendsto (fun δ => (Metric.thickening δ E).indicator f) (nhdsWithin 0 (Set.Ioi 0))
    (nhds ((closure E).indicator f))
-- Mathlib.Algebra.Group.Center
Set.centralizer.eq_1 : ∀ {M : Type u_1} (S : Set M) [inst : Mul M], S.centralizer = {c | ∀ m ∈ S, m * c = c * m}
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isColocal_iff_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {X Y : C}
  (f : X ⟶ Y), P X → P Y → (P.isColocal f ↔ CategoryTheory.IsIso f)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.CohomologyClass.mk_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n : ℤ), CochainComplex.HomComplex.CohomologyClass.mk 0 = 0
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- **Alias** of `Finsupp.prod_finsetSum_index`. -/
Finsupp.prod_finset_sum_index : ∀ {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [inst : AddCommMonoid M] [inst_1 : CommMonoid N]
  {s : Finset ι} {g : ι → α →₀ M} {h : α → M → N},
  (∀ (a : α), h a 0 = 1) →
    (∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂) → ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
-- Mathlib.Tactic.Push.Attr
Mathlib.Tactic.Push.instBEqHead : BEq Mathlib.Tactic.Push.Head
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.instUniqueI₀Singleton : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S T : C} → (f : S ⟶ T) → Unique (CategoryTheory.PreZeroHypercover.singleton f).I₀
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_eq_integral_klFun : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  InformationTheory.klDiv μ ν =
    if μ.AbsolutelyContinuous ν ∧ MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ then
      ENNReal.ofReal (∫ (x : α), InformationTheory.klFun (μ.rnDeriv ν x).toReal ∂ν)
    else ⊤
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.triangle : ∀ {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] {L : CategoryTheory.Functor C D}
  {W : CategoryTheory.MorphismProperty C} [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} {ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit}
  (X Y : CategoryTheory.LocalizedMonoidal L W ε),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.LocalizedMonoidal L W ε)) Y).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom Y
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α]
  {f : (a : α) → β a → γ a} {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey! k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) = Std.Internal.List.getKey! k l
-- Mathlib.RepresentationTheory.Equiv
Representation.freeLift_toLinearMap : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {k : Type u} [inst_2 : CommSemiring k]
  [inst_3 : Module k V] (σ : Representation k G V) {α : Type w'} (f : α → V),
  (σ.freeLift f).toLinearMap =
    (Finsupp.linearCombination k fun x => (σ x.2) (f x.1)) ∘ₗ
      ↑(Finsupp.curryLinearEquiv k).symm ∘ₗ Finsupp.mapRange.linearMap ↑(MonoidAlgebra.coeffLinearEquiv k)
-- Mathlib.Logic.Lemmas
dite_dite_distrib_left : ∀ {α : Sort u_1} {p q : Prop} [inst : Decidable p] [inst_1 : Decidable q] {a : p → α} {b : ¬p → q → α}
  {c : ¬p → ¬q → α},
  (dite p a fun hp => dite q (b hp) (c hp)) = if hq : q then dite p a fun hp => b hp hq else dite p a fun hp => c hp hq
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonRpcReleaseParams.toJson : Lean.Lsp.RpcReleaseParams → Lean.Json
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_fin_one : ∀ {R : Type u_6} [inst : AddCommMonoid R] (A : Matrix (Fin 1) (Fin 1) R), A.trace = A 0 0
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
CategoryTheory.Limits.colimitQuotientCoproduct_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C] (F : CategoryTheory.Functor J C),
  CategoryTheory.Epi (CategoryTheory.Limits.colimitQuotientCoproduct F)
-- Mathlib.Analysis.Complex.Norm
Complex.norm_ratCast : ∀ (q : ℚ), ‖↑q‖ = |↑q|
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.interSmallerFn.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l sofar : List ((a : α) × β a)) (k : α),
  Std.Internal.List.interSmallerFn l sofar k =
    match Std.Internal.List.getEntry? k l with
    | some kv' => Std.Internal.List.insertEntry kv'.fst kv'.snd sofar
    | none => sofar
-- Std.Data.Iterators.Lemmas.Producers.Repeat
Std.Iter.isSome_atIdxSlow?_repeat : ∀ {α : Type w} {f : α → α} {init : α} {k : ℕ}, (Std.Iter.atIdxSlow? k (Std.Iter.repeat f init)).isSome = true
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.HasOfPostcompProperty.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W W' : CategoryTheory.MorphismProperty C},
  (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W' g → W (CategoryTheory.CategoryStruct.comp f g) → W f) →
    W.HasOfPostcompProperty W'
-- Mathlib.Data.Set.Image
/-- The preimage of a nontrivial set under a surjective map is nontrivial.  -/
Set.Nontrivial.preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, s.Nontrivial → Function.Surjective f → (f ⁻¹' s).Nontrivial
-- Mathlib.Algebra.Order.Sub.Defs
tsub_tsub_le_tsub_add : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] [AddLeftMono α]
  {a b c : α}, a - (b - c) ≤ a - b + c
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.proofWidgetsJsxAttrVal_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Types.Images
CategoryTheory.Limits.Types.instHasImageMapsType : CategoryTheory.Limits.HasImageMaps (Type u)
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.instAddCommGroupHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (M N : CategoryTheory.Mat_ C) → AddCommGroup (M ⟶ N)
-- Std.Data.TreeMap.Basic
Std.TreeMap.instEmptyCollection : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → EmptyCollection (Std.TreeMap α β cmp)
-- Mathlib.Algebra.Group.Basic
div_div_div_cancel_left : ∀ {G : Type u_3} [inst : CommGroup G] (a b c : G), c / a / (c / b) = b / a
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContextEntry.param.injEq : ∀ (a a_1 : Lean.IR.IRType), (Lean.IR.LocalContextEntry.param a = Lean.IR.LocalContextEntry.param a_1) = (a = a_1)
-- Std.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.Equiv.foldM_eq : ∀ {α₁ α₂ β γ : Type w} {m : Type w → Type w'} [Std.Iterator α₁ Id β] [Std.Iterator α₂ Id β]
  [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] [Std.Iterators.Finite α₁ Id]
  [Std.Iterators.Finite α₂ Id] [inst_4 : Monad m] [LawfulMonad m] [inst_6 : Std.IteratorLoop α₁ Id m]
  [Std.LawfulIteratorLoop α₁ Id m] [inst_8 : Std.IteratorLoop α₂ Id m] [Std.LawfulIteratorLoop α₂ Id m] {init : γ}
  {f : γ → β → m γ} {ita : Std.Iter β} {itb : Std.Iter β},
  ita.Equiv itb → Std.Iter.foldM f init ita = Std.Iter.foldM f init itb
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_subsingleton : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} [inst : Subsingleton m] (A : Matrix m n R) (i : m) (b : n → R),
  A.updateRow i b = (Matrix.replicateRow (Fin 1) b).submatrix (Function.const m 0) id
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.subgroupOf_map_powMonoidHom_eq_range : ∀ {M : Type u_6} [inst : CommGroup M] (S : Subgroup M) (n : ℕ),
  (Subgroup.map (powMonoidHom n) S).subgroupOf S = (powMonoidHom n).range
-- Mathlib.Algebra.Regular.Basic
IsAddRegular.nsmul : ∀ {R : Type u_1} [inst : AddMonoid R] {a : R} (n : ℕ), IsAddRegular a → IsAddRegular (n • a)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The bijection between the elements of the height one prime spectrum of `B` that divide the lift
of the maximal ideal `p` in `B` and the primes over `p` in `B`.
 -/
IsDedekindDomain.HeightOneSpectrum.equivPrimesOver : {A : Type u_4} →
  [inst : CommRing A] →
    {p : Ideal A} →
      [hpm : p.IsMaximal] →
        (B : Type u_5) →
          [inst_1 : CommRing B] →
            [IsDedekindDomain B] →
              [inst_3 : Algebra A B] →
                [IsDomain A] →
                  [Module.IsTorsionFree A B] →
                    p ≠ 0 → { v // v.asIdeal ∣ Ideal.map (algebraMap A B) p } ≃ ↑(p.primesOver B)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coe_inv : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Inv Y] (f : LocallyConstant X Y), ⇑f⁻¹ = (⇑f)⁻¹
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instCStarAlgebraComplex : {A : Type u_1} → [inst : NonUnitalCStarAlgebra A] → CStarAlgebra (DoubleCentralizer ℂ A)
-- Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
/-- The given sum is the number of integer points in the triangle formed by the diagonal of the
rectangle `(0, p/2) × (0, q/2)`.  -/
_private.Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas.0.ZMod.sum_Ico_eq_card_lt : ∀ {p q : ℕ},
  ∑ a ∈ Finset.Ico 1 (p / 2).succ, a * q / p =
    {x ∈ Finset.Ico 1 (p / 2).succ ×ˢ Finset.Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q}.card
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.set_bind_modifyGet_bind : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α β : Type u_1} (s : σ) (f : σ → α × σ) (mx : α → m β),
  (do
      set s
      let x ← modifyGet f
      mx x) =
    do
    set (f s).2
    mx (f s).1