mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.Module
ContinuousLinearMap.summable : ∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂}
  {L : SummationFilter ι} {f : ι → M} (φ : M →SL[σ] M₂), Summable f L → Summable (fun b => φ (f b)) L
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_insertManyIfNewUnit!_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List α} {k : α},
      k ∈ ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l) ↔ k ∈ t ∨ l.contains k = true
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_ric_eq_some : ∀ {n i : ℕ}, i ≤ n → (*...=n).toList[i]? = some i
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
OrderIso.map_ciSup_of_directed : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α]
  [inst_1 : ConditionallyCompletePartialOrderSup β] [Nonempty ι] (e : α ≃o β) {f : ι → α},
  Directed (fun x1 x2 => x1 ≤ x2) f → BddAbove (Set.range f) → e (⨆ i, f i) = ⨆ i, e (f i)
-- Mathlib.Order.Defs.Unbundled
antisymm_iff : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] [Std.Antisymm r] {a b : α}, r a b ∧ r b a ↔ a = b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a : α} {fallback v : β},
      (t.insert k v).getD a fallback = if cmp k a = Ordering.eq then v else t.getD a fallback
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.comapₗ.congr_simp : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u} [inst_3 : CommRing S]
  {N : Type u} [inst_4 : AddCommGroup N] [inst_5 : Module S N] {σ : R →+* S} (f f_1 : M →ₛₗ[σ] N),
  f = f_1 →
    ∀ (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
      (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
      (hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier),
      AlgebraicGeometry.StructureSheaf.comapₗ f U V hUV = AlgebraicGeometry.StructureSheaf.comapₗ f_1 U V hUV
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (X_1 : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)),
  ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso F U).inv.app X_1).hom =
    CategoryTheory.CategoryStruct.id X_1.pt
-- Mathlib.Order.WellFoundedSet
/-- `s.WellFoundedOn r` indicates that the relation `r` is `WellFounded` when restricted to `s`.  -/
Set.WellFoundedOn : {α : Type u_2} → Set α → (α → α → Prop) → Prop
-- Mathlib.Algebra.Group.Invertible.Basic
/-- If `x ^ n = 1` then `x` has an inverse, `x^(n - 1)`.  -/
invertibleOfPowEqOne : {α : Type u} → [inst : Monoid α] → (x : α) → (n : ℕ) → x ^ n = 1 → n ≠ 0 → Invertible x
-- Lean.Meta.ReduceEval
Lean.Meta.ReduceEval.reduceEval : {α : Type} → [self : Lean.Meta.ReduceEval α] → Lean.Expr → Lean.MetaM α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [Inhabited α] {k fallback : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).getKeyD k fallback = if (f (t.get? k)).isSome = true then k else fallback
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaAddGrp_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X Y : C} [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H]
  (α : CategoryTheory.yonedaAddGrpObj G ⟶ CategoryTheory.yonedaAddGrpObj H) (f : X ⟶ Y) (g : Y ⟶ G) {Z : C} (h : H ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) g) h)
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteAddGrp.instCategory.eq_1 : FiniteAddGrp.instCategory =
  { Hom := FiniteAddGrp.instCategory._aux_1, id := FiniteAddGrp.instCategory._aux_3,
    comp := @FiniteAddGrp.instCategory._aux_5, id_comp := @FiniteAddGrp.instCategory._proof_7,
    comp_id := @FiniteAddGrp.instCategory._proof_8, assoc := @FiniteAddGrp.instCategory._proof_9 }
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt32.reduceLT : Lean.Meta.Simp.Simproc
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Ico_left_eq_Ico_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  a ≤ b → insert (Order.pred a) (Set.Ico a b) = Set.Ico (Order.pred a) b
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor `F : C ⥤ D` reflects colimits if
whenever the image of a cocone over some `K : J ⥤ C` under `F` is a colimit cocone in `D`,
the cocone was already a colimit cocone in `C`.
Note that we do not assume a priori that `D` actually has any colimits.
 -/
CategoryTheory.Limits.ReflectsColimitsOfSize : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.Products.Tail.eq_1 : ∀ {I : Type u} [inst : LinearOrder I] (l : Profinite.NobelingProof.Products I), l.Tail = ⟨(↑l).tail, ⋯⟩
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- If `ringChar F` is odd, then `quadraticCharFun F a` can be computed in
terms of `a ^ (Fintype.card F / 2)`.  -/
quadraticCharFun_eq_pow_of_char_ne_two : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 → ∀ {a : F}, a ≠ 0 → quadraticCharFun F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.integral_eq_integral : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] (f : ↥(α →₁ₛ[μ] E)),
  MeasureTheory.L1.SimpleFunc.integral f =
    MeasureTheory.SimpleFunc.integral μ (MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.id_mapMon_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) CategoryTheory.MonObj.one
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_subtype_support : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α),
  ∑' (x : ↑(Function.support f)), f ↑x = ∑' (x : β), f x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addXYZ_self : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R},
  W'.Equation P → W'.addXYZ P P = ![0, 0, 0]
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.instEmptyCollection : EmptyCollection AlgebraicGeometry.Scheme
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.right_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f g : a ⟶ b)
  [inst_1 : CategoryTheory.BicategoricalCoherence f g],
  CategoryTheory.BicategoricalCoherence.iso =
    CategoryTheory.Bicategory.rightUnitor f ≪≫ CategoryTheory.BicategoricalCoherence.iso
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.col.eq_1 : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α), A.col = A.transpose
-- Mathlib.Topology.UniformSpace.Defs
uniformContinuous_const : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {b : β}, UniformContinuous fun x => b
-- Mathlib.RepresentationTheory.Rep.Basic
/-- There is a `k`-linear isomorphism between the sets of representation morphisms `Hom(A ⊗ B, C)`
and `Hom(B, Homₖ(A, C))`.  -/
Rep.MonoidalClosed.linearHomEquiv : {k : Type u} →
  [inst : CommRing k] →
    {G : Type v} →
      [inst_1 : Group G] →
        (A B C : Rep.{u, u, v} k G) → (CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) ≃ₗ[k] B ⟶ A ⟹ C
-- Lean.Environment
_private.Lean.Environment.0.Lean.readModuleData.unsafe_1 : System.FilePath → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Mathlib.Topology.Constructions
IsClosed.image_val : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {t : Set ↑s},
  IsClosed t → ∃ c, IsClosed c ∧ Subtype.val '' t = c ∩ s
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- A morphism respecting addition, multiplication, and scalar multiplication
(denoted as `A →ₛₙₐ[φ] B`, or `A →ₙₐ[R] B` when `φ` is the identity on `R`).
When these arise from algebra structures, this is the same
as a not-necessarily-unital morphism of algebras.  -/
NonUnitalAlgHom : {R : Type u} →
  {S : Type u₁} →
    [inst : Monoid R] →
      [inst_1 : Monoid S] →
        (R →* S) →
          (A : Type v) →
            (B : Type w) →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [DistribMulAction R A] → [inst : NonUnitalNonAssocSemiring B] → [DistribMulAction S B] → Type (max v w)
-- Mathlib.Algebra.Polynomial.Sequence
/-- `S i` has `natDegree` `i`.  -/
Polynomial.Sequence.natDegree_eq : ∀ {R : Type u_1} [inst : Semiring R] (S : Polynomial.Sequence R) (i : ℕ), (↑S i).natDegree = i
-- Mathlib.Data.Int.Bitwise
Int.testBit_ldiff : ∀ (m n : ℤ) (k : ℕ), (m.ldiff n).testBit k = (m.testBit k && !n.testBit k)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShift.of_core : ∀ {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] {F₁ F₂ : CategoryTheory.Functor C D} {τ : F₁ ⟶ F₂} {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A],
  (∀ (a : A), CategoryTheory.NatTrans.CommShiftCore τ a) → CategoryTheory.NatTrans.CommShift τ A
-- Mathlib.Topology.Compactness.Paracompact
/-- Let `X` be a locally compact sigma compact Hausdorff topological space. Suppose that for each
`x` the sets `B x : ι x → Set X` with the predicate `p x : ι x → Prop` form a basis of the filter
`𝓝 x`. Then there exists a locally finite covering `fun i ↦ B (c i) (r i)` of `X` such that each
`r i` satisfies `p (c i)`.

The notation is inspired by the case `B x r = Metric.ball x r` but the theorem applies to
`nhds_basis_opens` as well. If the covering must be subordinate to some open covering of `s`, then
the user should use a basis obtained by `Filter.HasBasis.restrict_subset` or a similar lemma, see
the proof of `paracompact_of_locallyCompact_sigmaCompact` for an example.

The formalization is based on two [ncatlab](https://ncatlab.org/) proofs:
* [locally compact and sigma compact spaces are paracompact](https://ncatlab.org/nlab/show/locally+compact+and+sigma-compact+spaces+are+paracompact);
* [open cover of smooth manifold admits locally finite refinement by closed balls](https://ncatlab.org/nlab/show/partition+of+unity#ExistenceOnSmoothManifolds).

See also `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set` for a version of this lemma
dealing with a covering of a closed set.

In most cases (namely, if `B c r ∪ B c r'` is again a set of the form `B c r''`) it is possible
to choose `α = X`. This fact is not yet formalized in `mathlib`.  -/
refinement_of_locallyCompact_sigmaCompact_of_nhds_basis : ∀ {X : Type v} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X] [T2Space X]
  {ι : X → Type u} {p : (x : X) → ι x → Prop} {B : (x : X) → ι x → Set X},
  (∀ (x : X), (nhds x).HasBasis (p x) (B x)) →
    ∃ α c r, (∀ (a : α), p (c a) (r a)) ∧ ⋃ a, B (c a) (r a) = Set.univ ∧ LocallyFinite fun a => B (c a) (r a)
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapDomainNonUnitalAlgHom_apply : ∀ (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Mul M] [inst_4 : Mul N] (f : M →ₙ* N) (a : MonoidAlgebra A M),
  (MonoidAlgebra.mapDomainNonUnitalAlgHom R A f) a = (MonoidAlgebra.mapDomainNonUnitalRingHom A f).toFun a
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.coprodMap_apply_single : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} {N : Type u_6} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] [inst_5 : DecidableEq ι] (f : (i : ι) → M i →ₗ[R] N) (i : ι) (x : M i),
  ((DFinsupp.coprodMap f) fun₀ | i => x) = (f i) x
-- Mathlib.Algebra.Category.Grp.Basic
MulEquiv.toGrpIso.eq_1 : ∀ {X Y : GrpCat} (e : ↑X ≃* ↑Y),
  e.toGrpIso =
    { hom := GrpCat.ofHom e.toMonoidHom, inv := GrpCat.ofHom e.symm.toMonoidHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Analysis.Calculus.LHopital
/-- **L'Hôpital's rule** for approaching a real from within a convex set, `deriv` version  -/
deriv.lhopital_zero_nhdsWithin_convex : ∀ {a : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ} {s : Set ℝ},
  Convex ℝ s →
    (∀ᶠ (x : ℝ) in nhdsWithin a (s \ {a}), DifferentiableAt ℝ f x) →
      (∀ᶠ (x : ℝ) in nhdsWithin a (s \ {a}), deriv g x ≠ 0) →
        Filter.Tendsto f (nhdsWithin a (s \ {a})) (nhds 0) →
          Filter.Tendsto g (nhdsWithin a (s \ {a})) (nhds 0) →
            Filter.Tendsto (fun x => deriv f x / deriv g x) (nhdsWithin a (s \ {a})) l →
              Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (s \ {a})) l
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_eq_get!_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {a : α}, m[a]! = m[a]?.get!
-- Lean.MetavarContext
/-- Returns true iff `localDecl` depends on the free variable `fvarId`
- When `generalizeNondepLet := true` (the default), then values of nondependent lets are ignored,
  for computing dependencies from "within" a telescope.
 -/
Lean.localDeclDependsOn : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.LocalDecl → Lean.FVarId → optParam Bool true → m Bool
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addCancelCommMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Zero M₁] [inst_2 : SMul ℕ M₁]
  [inst_3 : AddCancelCommMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0)
  (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x),
  Function.Injective.addCancelCommMonoid f hf one mul npow =
    { toAddCommMonoid := Function.Injective.addCommMonoid f hf one mul npow, toIsLeftCancelAdd := ⋯ }
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.restrictVarLeft.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] {γ : Type u_2} (l : ℕ)
  (F : L.Functions l) (ts : Fin l → L.Term (α ⊕ γ)) (f : ↥(FirstOrder.Language.func F ts).varFinsetLeft → β),
  (FirstOrder.Language.func F ts).restrictVarLeft f =
    FirstOrder.Language.func F fun i => (ts i).restrictVarLeft (f ∘ Set.inclusion ⋯)
-- Init.Data.UInt.Lemmas
USize.toNat_ofNat_of_lt_32 : ∀ {n : ℕ}, n < 4294967296 → (USize.ofNat n).toNat = n
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
/-- If a functor preserves kernels and cokernels, it preserves abelian images.  -/
CategoryTheory.Abelian.PreservesImage.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              [F.PreservesZeroMorphisms] →
                {X Y : C} →
                  (f : X ⟶ Y) →
                    [inst_5 : CategoryTheory.Limits.HasCokernel f] →
                      [inst_6 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] →
                        [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] →
                          [CategoryTheory.Limits.PreservesLimit
                                (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F] →
                            [inst_9 : CategoryTheory.Limits.HasCokernel (F.map f)] →
                              [inst_10 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))] →
                                F.obj (CategoryTheory.Abelian.image f) ≅ CategoryTheory.Abelian.image (F.map f)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β} [inst_2 : Inhabited β],
      List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (Std.ExtHashMap.ofList l)[k']! = v
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.hasProjectiveDimensionLT_of_enoughInjectives : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] [CategoryTheory.EnoughInjectives C] (X : C) (n : ℕ),
  (∀ (Y : C), Subsingleton (CategoryTheory.Abelian.Ext X Y n)) → CategoryTheory.HasProjectiveDimensionLT X n
-- Init.Data.SInt.Lemmas
UInt64.toInt64_add : ∀ (a b : UInt64), (a + b).toInt64 = a.toInt64 + b.toInt64
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instMulAction_1 : {M : Type u_1} → {α : Type u_3} → [inst : Monoid M] → [MulAction M α] → MulAction M αᵒᵈ
-- Mathlib.NumberTheory.PythagoreanTriples
circleEquivGen_symm_apply : ∀ {K : Type u_1} [inst : Field K] (hk : ∀ (x : K), 1 + x ^ 2 ≠ 0) (v : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }),
  (circleEquivGen hk).symm v = (↑v).1 / ((↑v).2 + 1)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.instZeroHomOfHasZeroMorphisms : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] → (β : Type w) → (X Y : CategoryTheory.GradedObject β C) → Zero (X ⟶ Y)
-- Init.Data.List.Find
List.findFinIdx?_eq_none_iff : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, List.findFinIdx? p l = none ↔ ∀ x ∈ l, ¬p x = true
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_reverse_cons : ∀ {b : ℕ} (l : List ℕ) (d : ℕ), Nat.ofDigits b (d :: l).reverse = Nat.ofDigits b l.reverse + b ^ l.length * d
-- Mathlib.Algebra.Group.Action.Defs
/-- Acting on `0` by a scalar gives `0`  -/
AddDistribAddAction.vadd_zero : ∀ {M : Type u_9} {N : Type u_10} {inst : AddMonoid M} {inst_1 : AddMonoid N} [self : AddDistribAddAction M N] (r : M),
  r +ᵥ 0 = 0
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.topEmbedding_apply : ∀ {V : Type u_1} {α : Type u_4} {G : SimpleGraph V} (f : ⊤.Copy G) (a : α), f.topEmbedding a = f a
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- The connecting morphism `t.truncGE n ⟶ t.truncLT n ⋙ shiftFunctor C (1 : ℤ)`
when `t` is a t-structure on a pretriangulated category and `n : ℤ`.  -/
CategoryTheory.Triangulated.TStructure.truncGEδLT : {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) →
                (n : ℤ) → t.truncGE n ⟶ (t.truncLT n).comp (CategoryTheory.shiftFunctor C 1)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableLocallyUniformlyOn.comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] {γ : Type u_4} [inst_3 : TopologicalSpace γ] {t : Set γ},
  SummableLocallyUniformlyOn f s →
    ∀ (h' : γ → β), Set.MapsTo h' t s → ContinuousOn h' t → SummableLocallyUniformlyOn (fun i y => f i (h' y)) t
-- Init.Data.Option.Lemmas
Option.mem_unique : ∀ {α : Type u_1} {o : Option α} {a b : α}, a ∈ o → b ∈ o → a = b
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Eta-expanded form of `MeasureTheory.StronglyMeasurable.inv₀` -/
MeasureTheory.StronglyMeasurable.fun_inv₀ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β]
  [inst_1 : GroupWithZero β] [ContinuousInv₀ β] [TopologicalSpace.MetrizableSpace β],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun i => (f i)⁻¹
-- Init.Grind.Config
Lean.Grind.OrderConfig.mk : Lean.Grind.NoopConfig → Lean.Grind.OrderConfig
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.casesOnAdd : Int.Internal.Linear.Poly → (ℤ → Int.Internal.Linear.Var → Int.Internal.Linear.Poly → Bool) → Bool
-- Mathlib.Algebra.MvPolynomial.Nilpotent
_private.Mathlib.Algebra.MvPolynomial.Nilpotent.0.MvPolynomial.isNilpotent_iff_of_fintype : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] {P : MvPolynomial σ R} [Finite σ],
  IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (MvPolynomial.coeff i P)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mk'_eq_bot : ∀ {ι : Type u_1} {l u : ι → ℝ}, BoxIntegral.Box.mk' l u = ⊥ ↔ ∃ i, u i ≤ l i
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Filter.Tendsto.clog : ∀ {α : Type u_1} {l : Filter α} {f : α → ℂ} {x : ℂ},
  Filter.Tendsto f l (nhds x) →
    x ∈ Complex.slitPlane → Filter.Tendsto (fun t => Complex.log (f t)) l (nhds (Complex.log x))
-- Mathlib.Order.Basic
not_lt_iff_eq_or_lt : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ a = b ∨ b < a
-- Std.Async.System
/-- Represents the breakdown of CPU time usage in milliseconds.
 -/
Std.Async.System.CPUTimes : Type
-- Init.Data.List.Attach
List.pmap_nil : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β}, List.pmap f [] ⋯ = []
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.instBot : (ι : Type u_1) → Bot (PreAbstractSimplicialComplex ι)
-- Mathlib.Order.Partition.Basic
Partition.partOf_eq_empty_iff : ∀ {α : Type u_1} {x : α} {u : Set α} {P : Partition u}, P.partOf x = ∅ ↔ x ∉ u
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableWithinAt.rpow_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} {p : ℝ},
  DifferentiableWithinAt ℝ f s x → f x ≠ 0 ∨ 1 ≤ p → DifferentiableWithinAt ℝ (fun x => f x ^ p) s x
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instFullIndYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.Ind.yoneda.Full
-- Lean.Elab.PreDefinition.Structural.FindRecArg
/-- Precompute all candidate argument combinations for structural recursion.
This performs the analysis that may need function axioms in the environment
(via `isDefEq`, `inferType`, etc.) but does not run the callback that
attempts to eliminate mutual recursion.
 -/
Lean.Elab.Structural.findRecArgCandidates : Array Lean.Name →
  Lean.Elab.FixedParamPerms →
    Array Lean.Expr →
      Array Lean.Expr → Array (Option Lean.Elab.TerminationMeasure) → Lean.MetaM Lean.Elab.Structural.RecArgCandidates
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.limitBiconeOfUnique_bicone_ι : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : Unique J] (f : J → C) (j : J),
  (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.ι j = CategoryTheory.eqToHom ⋯