mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.isoEquivHomeo_apply : ∀ {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ≅ Y), CompHausLike.isoEquivHomeo f = CompHausLike.homeoOfIso f
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.coe_le_coe : ∀ {α : Type u} {f g : Ultrafilter α}, ↑f ≤ ↑g ↔ f = g
-- Lean.Parser.Extra
Lean.Parser.numLit.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- `equiv.subRight` as a `MeasurableEquiv`  -/
MeasurableEquiv.subRight : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : MeasurableSpace G] → [MeasurableAdd G] → G → G ≃ᵐ G
-- Mathlib.RingTheory.Noetherian.Defs
/-- For an endomorphism of a Noetherian module, any sufficiently large iterate has disjoint kernel
and range.  -/
Module.End.eventually_disjoint_ker_pow_range_pow : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsNoetherian R M]
  (f : Module.End R M), ∀ᶠ (n : ℕ) in Filter.atTop, Disjoint (f ^ n).ker (f ^ n).range
-- Mathlib.Topology.AlexandrovDiscrete
isClopen_iUnion₂ : ∀ {ι : Sort u_1} {κ : ι → Sort u_2} {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α]
  {f : (i : ι) → κ i → Set α}, (∀ (i : ι) (j : κ i), IsClopen (f i j)) → IsClopen (⋃ i, ⋃ j, f i j)
-- Mathlib.Algebra.Lie.Basic
lie_sum : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] {ι : Type u_1}
  (s : Finset ι) (f : ι → M) (a : L), ⁅a, ∑ i ∈ s, f i⁆ = ∑ i ∈ s, ⁅a, f i⁆
-- Mathlib.RingTheory.DedekindDomain.Instances
_private.Mathlib.RingTheory.DedekindDomain.Instances.0.termRₚ : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs_one : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S), WithAbs.toAbs v 1 = 1
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_inter_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ici a ∩ Set.Iic b = Set.Icc a b
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- A binary fan in the opposite category gives a binary cofan.  -/
CategoryTheory.Limits.BinaryFan.unop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → CategoryTheory.Limits.BinaryFan (Opposite.op X) (Opposite.op Y) → CategoryTheory.Limits.BinaryCofan X Y
-- Init.Grind.Order
Lean.Grind.Order.eq_trans_false' : ∀ {p q : Prop}, p = q → p = False → q = False
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instInv : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : DivisionRing R] → (v : Valuation R Γ₀) → Inv (WithVal v)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.isClosed_image : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) {S : Set A}, IsClosed (⇑e '' S) ↔ IsClosed S
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.isNClique_snd_right : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → G.IsNClique (r + 1) (insert w₂ t)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossings_lt_top_iff : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {ω : Ω},
  MeasureTheory.upcrossings a b f ω < ⊤ ↔ ∃ k, ∀ (N : ℕ), MeasureTheory.upcrossingsBefore a b f N ω ≤ k
-- Mathlib.Topology.LocallyFinsupp
LocallyFiniteSupport.finite_inter_support_of_isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} {W : Set X} [inst_1 : Zero Y] {f : X → Y},
  LocallyFiniteSupport f → IsCompact W → (W ∩ Function.support f).Finite
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The proposed colimit cocone is a colimit in `AddCommGroup`.  -/
AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J AddCommGrpCat) →
        CategoryTheory.Limits.IsColimit (AddCommGrpCat.FilteredColimits.colimitCocone F)
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- `Cocone.toCostructuredArrow` can be expressed in terms of `Functor.toCostructuredArrow`.  -/
CategoryTheory.Limits.Cocone.toCostructuredArrowIsoToCostructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone F) →
            c.toCostructuredArrow ≅ (CategoryTheory.Functor.id J).toCostructuredArrow F c.pt c.ι.app ⋯
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of `Relation.SymmGen.of_gt`. -/
LT.lt.symmGen_symm : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], b < a → Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.CategoryTheory.Shift.Basic
/-- When shifts are indexed by an additive commutative monoid, then shifts commute.  -/
CategoryTheory.shiftComm' : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] {X Y : C} (f : X ⟶ Y) (i j : A),
  (CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm X i j).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C i).map ((CategoryTheory.shiftFunctor C j).map f))
        (CategoryTheory.shiftComm Y j i).hom)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RccSliceData : (α : Type u) → (α → Type v) → [Ord α] → Type (max u v)
-- Init.Data.UInt.Lemmas
UInt8.zero_lt_one : 0 < 1
-- Mathlib.Topology.Algebra.Monoid
/-- A version of `Pi.continuousMul` for non-dependent functions. It is needed because sometimes
Lean 3 fails to use `Pi.continuousMul` for non-dependent functions.  -/
Pi.continuousMul' : ∀ {ι : Type u_1} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M], ContinuousMul (ι → M)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coordChange_same : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {b : B}, b ∈ e.baseSet → e.coordChange e b = id
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.IsSymmetric.one : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R], MvPolynomial.IsSymmetric 1
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.distribMulAction : {m : Type u_2} →
  {n : Type u_3} →
    {R : Type u_7} →
      {α : Type v} →
        [inst : Monoid R] → [inst_1 : AddMonoid α] → [DistribMulAction R α] → DistribMulAction R (Matrix m n α)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
Finset.card_inv_mul_of_doubling_lt_three_halves : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G},
  ↑(A * A).card < 3 / 2 * ↑A.card → (A⁻¹ * A).card = (A * A).card
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.PreservesCoequalizer.iso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G],
  CategoryTheory.Limits.PreservesCoequalizer.iso G f g = CategoryTheory.Limits.PreservesCoequalizer.iso G f g
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.lmapDomain_id : ∀ {α : Type u_1} (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Finsupp.lmapDomain M R id = LinearMap.id
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isIntTangentAt_center_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P},
  s₁.IsIntTangentAt s₂ s₁.center ↔ s₁.radius = 0 ∧ s₁.center ∈ s₂
-- Mathlib.Data.List.Basic
List.exists_of_length_succ : ∀ {α : Type u} {n : ℕ} (l : List α), l.length = n + 1 → ∃ h t, l = h :: t
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintParams.textDocument : Lean.Lsp.InlayHintParams → Lean.Lsp.TextDocumentIdentifier
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.coe_mapAlgEquiv : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A ≃ₐ[R] B), ⇑(Polynomial.mapAlgEquiv f) = Polynomial.map ↑f
-- Init.Data.List.Lemmas
/-- Variant of `foldl_flip_cons_eq_append` specalized to `f = id`.  -/
List.foldl_flip_cons_eq_append' : ∀ {α : Type u_1} {l l' : List α}, List.foldl (fun xs y => y :: xs) l' l = l.reverse ++ l'
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.span.congr_simp : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M} (hli : LinearIndependent R v), Module.Basis.span hli = Module.Basis.span hli
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.leftUnitor_inv_left_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Z : CategoryTheory.Over X) {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.fst (CategoryTheory.CategoryStruct.id X) Z.hom) h) =
    CategoryTheory.CategoryStruct.comp Z.hom h
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_alter_le_size : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.size ≤ t.size + 1
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.Array.filterMapM.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) →
    (__do_lift : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive __do_lift
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, if all binary products exist, then all binary biproducts exist.  -/
CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasBinaryProducts C], CategoryTheory.Limits.HasBinaryBiproducts C
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.and.sizeOf_spec : sizeOf Std.Tactic.BVDecide.BVBinOp.and = 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.RenameOptions.mk.sizeOf_spec : ∀ (prepareProvider : Bool), sizeOf { prepareProvider := prepareProvider } = 1 + sizeOf prepareProvider
-- Mathlib.Algebra.DirectSum.Algebra
DirectSum.toAlgebra_apply : ∀ {ι : Type uι} (R : Type uR) (A : ι → Type uA) {B : Type uB} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (A i)] [inst_2 : (i : ι) → Module R (A i)] [inst_3 : AddMonoid ι]
  [inst_4 : DirectSum.GSemiring A] [inst_5 : Semiring B] [inst_6 : DirectSum.GAlgebra R A] [inst_7 : Algebra R B]
  [inst_8 : DecidableEq ι] (f : (i : ι) → A i →ₗ[R] B) (hone : (f 0) GradedMonoid.GOne.one = 1)
  (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj)
  (a : DirectSum ι fun i => A i),
  (DirectSum.toAlgebra R A f hone hmul) a = (DirectSum.toSemiring (fun i => (f i).toAddMonoidHom) hone hmul) a
-- Lean.Meta.Basic
/-- Control projection reduction at `whnfCore`.  -/
Lean.Meta.Config.proj : Lean.Meta.Config → Lean.Meta.ProjReductionKind
-- Mathlib.Data.Finsupp.Order
Finsupp.instIsBotZeroClass : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsBotZeroClass α],
  IsBotZeroClass (ι →₀ α)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.identities_op_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.MorphismProperty.identities Cᵒᵖ f ↔ CategoryTheory.MorphismProperty.identities C f.unop
-- Mathlib.Order.Preorder.Finite
Finset.exists_minimalFor : ∀ {ι : Type u_1} {α : Type u_2} [inst : LE α] [IsTrans α fun a a_1 => a_1 ≤ a] (f : ι → α) (s : Finset ι),
  s.Nonempty → ∃ i, MinimalFor (fun x => x ∈ s) f i
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.cases.injEq : ∀ (eager eager_1 : Bool),
  (Lean.Meta.Grind.AttrKind.cases eager = Lean.Meta.Grind.AttrKind.cases eager_1) = (eager = eager_1)
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
/-- The anchor of a given Lie-Rinehart algebra `L` over `A` interpreted as a Lie-Rinehart morphism
to the module of derivations of `A`.  -/
LieRinehartAlgebra.anchor : (R : Type u_1) →
  (A₁ : Type u_2) →
    (L₁ : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing A₁] →
          [inst_2 : LieRing L₁] →
            [inst_3 : Module A₁ L₁] →
              [inst_4 : LieRingModule L₁ A₁] →
                [inst_5 : Algebra R A₁] →
                  [inst_6 : LieAlgebra R L₁] →
                    [inst_7 : LieRinehartRing A₁ L₁] →
                      [LieRinehartAlgebra R A₁ L₁] → LieRinehartAlgebra.Hom (AlgHom.id R A₁) L₁ (Derivation R A₁ A₁)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.contains_iff : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)), c.contains l = true ↔ l ∈ c.toList
-- Init.Ext
Prod.ext_iff : ∀ {α : Type u} {β : Type v} {x y : α × β}, x = y ↔ x.1 = y.1 ∧ x.2 = y.2
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- `X ×[Y] (Y ⨯ Z) ≅ X ⨯ Z`  -/
CategoryTheory.Limits.pullbackProdFstIsoProd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        (Z : C) →
          [inst_1 : CategoryTheory.Limits.HasBinaryProduct Y Z] →
            [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z] →
              [inst_3 : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] →
                CategoryTheory.Limits.pullback f CategoryTheory.Limits.prod.fst ≅ X ⨯ Z
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- The topology defined from a subgroups basis, admitting the given subgroups as a basis
of neighborhoods of zero.  -/
RingSubgroupsBasis.topology : {A : Type u_1} →
  {ι : Type u_2} → [inst : Ring A] → [Nonempty ι] → {B : ι → AddSubgroup A} → RingSubgroupsBasis B → TopologicalSpace A
-- Mathlib.Tactic.Tauto
/-- Matches propositions where we want to apply the `cases` tactic
in the core loop of `tauto`.  -/
Mathlib.Tactic.Tauto.casesMatcher : Q(Prop) → Lean.MetaM Bool
-- Mathlib.LinearAlgebra.Multilinear.Curry
/-- Given a multilinear map `f` in `n+1` variables, split the last variable to obtain
a multilinear map in `n` variables taking values in linear maps from `M (last n)` to `M₂`, given by
`m ↦ (x ↦ f (snoc m x))`.  -/
MultilinearMap.curryRight : {R : Type uR} →
  {n : ℕ} →
    {M : Fin n.succ → Type v} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : Fin n.succ) → Module R (M i)] →
                [inst_4 : Module R M₂] →
                  MultilinearMap R M M₂ → MultilinearMap R (fun i => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)
-- Mathlib.Algebra.Homology.SpectralObject.Basic
/-- The (exact) sequence
`H^n₀(f) ⟶ H^n₀(fg) ⟶ H^n₀(g) ⟶ H^n₁(f) ⟶ H^n₁(fg) ⟶ H^n₁(g)`
of a spectral object, when `f ≫ g = fg` and `n₀ + 1 = n₁`.  -/
CategoryTheory.Abelian.SpectralObject.composableArrows₅ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (fg : i ⟶ k) →
                    CategoryTheory.CategoryStruct.comp f g = fg →
                      (n₀ n₁ : ℤ) →
                        autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.composableArrows₅._auto_1 →
                          CategoryTheory.ComposableArrows C 5
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.orthogonalDecomposition_apply : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (x : E),
  K.orthogonalDecomposition x = WithLp.toLp 2 (K.orthogonalProjectionOnto x, Kᗮ.orthogonalProjectionOnto x)
-- Mathlib.RingTheory.AdicCompletion.Functoriality
/-- A linear map induces a map on adic completions.  -/
AdicCompletion.map : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {M : Type u_2} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {N : Type u_3} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] → (M →ₗ[R] N) → AdicCompletion I M →ₗ[AdicCompletion I R] AdicCompletion I N
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instIsTrivialObjModuleCatTrivialFunctor : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : Monoid G] (X : ModuleCat k),
  ((Rep.trivialFunctor k G).obj X).IsTrivial
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.liftHom₂WhiskerLeft : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        [inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
          {g h : b ⟶ c} →
            (η : g ⟶ h) →
              [inst_2 : Mathlib.Tactic.BicategoryCoherence.LiftHom g] →
                [inst_3 : Mathlib.Tactic.BicategoryCoherence.LiftHom h] →
                  [Mathlib.Tactic.BicategoryCoherence.LiftHom₂ η] →
                    Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.whiskerLeft f η)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.mem_support_iff_exists_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v}, w ∈ p.support ↔ ∃ q r, p = q.append r
-- Init.Data.Fin.Basic
Fin.instXorOp : {n : ℕ} → XorOp (Fin n)
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.mem_inf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {A : Set M} {α : Type u₁} {s t : L.DefinableSet A α}
  {x : α → M}, x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t
-- Mathlib.Order.CompleteLattice.SetLike
Sublattice.setLike_mem_coe : ∀ {X : Type u_1} {L : Sublattice (Set X)} {T : ↥L} {x : X}, x ∈ ↑T ↔ x ∈ T
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countable_countableGeneratingSet : ∀ {α : Type u_1} [inst : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α],
  (MeasurableSpace.countableGeneratingSet α).Countable
-- Lean.Expr
/-- Same as `mkApp f args` but reversing `args`.  -/
Lean.mkAppRev : Lean.Expr → Array Lean.Expr → Lean.Expr
-- Std.Do.PostCond
Std.Do.ExceptConds.snd_false : ∀ {ε : Type u} {ps : Std.Do.PostShape}, Std.Do.ExceptConds.false.2 = Std.Do.ExceptConds.false
-- Mathlib.Data.NNRat.Defs
NNRat.coe_pow : ∀ (q : ℚ≥0) (n : ℕ), ↑(q ^ n) = ↑q ^ n
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toSubring_inj : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {S U : Subalgebra R A},
  S.toSubring = U.toSubring ↔ S = U
-- Init.Data.SInt.Lemmas
Int8.toInt32_toInt16 : ∀ (n : Int8), n.toInt16.toInt32 = n.toInt32
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.equivOfNatIso_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : F ≅ G),
  (CategoryTheory.Endofunctor.Algebra.equivOfNatIso α).inverse =
    CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α.hom
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.uliftFunctor_faithful : CategoryTheory.uliftFunctor.{v, u}.Faithful
-- Init.Grind.Config
Lean.Grind.CutsatConfig.mk : Lean.Grind.NoopConfig → Lean.Grind.CutsatConfig
-- Mathlib.Algebra.Order.Nonneg.Basic
/-- Coercion `{x : α // 0 ≤ x} → α` as a `RingHom`.  -/
Nonneg.coeRingHom : {α : Type u_1} →
  [inst : Semiring α] →
    [inst_1 : PartialOrder α] →
      [inst_2 : ZeroLEOneClass α] → [inst_3 : AddLeftMono α] → [inst_4 : PosMulMono α] → { x // 0 ≤ x } →+* α
-- Mathlib.LinearAlgebra.Semisimple
Module.End.isSemisimple_id : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsSemisimpleModule R M], Module.End.IsSemisimple LinearMap.id
-- Mathlib.Logic.Function.Basic
Function.onFun_comp_eq : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (f : α → α → γ) (g : β → α) (h : δ → β),
  Function.onFun f (g ∘ h) = Function.onFun (Function.onFun f g) h
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mk : {G : Type u_3} →
  [inst : AddGroup G] →
    (toAddSubmonoid : AddSubmonoid G) →
      (∀ {x : G}, x ∈ toAddSubmonoid.carrier → -x ∈ toAddSubmonoid.carrier) → AddSubgroup G
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- Type-alias for modifications between lax transformations of oplax functors. This is the type
used for the 2-homomorphisms in the bicategory of oplax functors equipped with lax
transformations.  -/
CategoryTheory.Oplax.LaxTrans.Hom : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} → (F ⟶ G) → (F ⟶ G) → Type (max u₁ w₂)
-- Batteries.Lean.PersistentHashSet
/-- Returns `true` if `f` returns `true` for any element of the set.
 -/
Lean.PersistentHashSet.any : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashSet α → (α → Bool) → Bool
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.w_mk_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : T} {f : X ⟶ Y} {g : CategoryTheory.Arrow T}
  (sq : CategoryTheory.Arrow.mk f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) g.hom =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Arrow.Hom.right sq)
-- Init.Data.UInt.Lemmas
UInt16.toNat_one : UInt16.toNat 1 = 1
-- Init.Data.List.Lemmas
List.set_getElem_self : ∀ {α : Type u_1} {as : List α} {i : ℕ} (h : i < as.length), as.set i as[i] = as
-- Mathlib.Topology.Algebra.Monoid
continuousOn_list_prod : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : Monoid M] [ContinuousMul M] {f : ι → X → M} (l : List ι) {t : Set X},
  (∀ i ∈ l, ContinuousOn (f i) t) → ContinuousOn (fun a => (List.map (fun i => f i a) l).prod) t
-- Std.Time.Zoned.Database.TzIf
/-- The number of leap second records.
 -/
Std.Time.TimeZone.TZif.Header.leapcnt : Std.Time.TimeZone.TZif.Header → UInt32
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tprod_int_eq_zero_mul_tprod_pnat : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : UniformSpace G] [IsUniformGroup G] [CompleteSpace G] [T2Space G]
  {f : ℤ → G}, Multipliable f → ∏' (n : ℤ), f n = (f 0 * ∏' (n : ℕ+), f ↑↑n) * ∏' (n : ℕ+), f (-↑↑n)
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.deterministic_parallelComp_deterministic : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {f : α → γ} {g : β → δ} (hf : Measurable f) (hg : Measurable g),
  (ProbabilityTheory.Kernel.deterministic f hf).parallelComp (ProbabilityTheory.Kernel.deterministic g hg) =
    ProbabilityTheory.Kernel.deterministic (Prod.map f g) ⋯