mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.tendsto_nhds_iff : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [DilationClass F α β] (f : F) {ι : Type u_5} {g : ι → α} {a : Filter ι} {b : α},
  Filter.Tendsto g a (nhds b) ↔ Filter.Tendsto (⇑f ∘ g) a (nhds (f b))
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
/-- On a compact space, locally uniform convergence is just uniform convergence.  -/
tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι} [CompactSpace α], TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.ofMon_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Mon (CategoryTheory.Functor C C)) (X : C),
  (CategoryTheory.Monad.ofMon M).obj X = M.X.obj X
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The ring homomorphism `R/(I ⊔ J) → (R/I)/J'` induced by `quotQuotMk`  -/
DoubleQuot.liftSupQuotQuotMk : {R : Type u} → [inst : CommRing R] → (I J : Ideal R) → R ⧸ I ⊔ J →+* (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J
-- Std.Http.Protocol.H1.Reader
/-- Checks if more input is needed to continue parsing.
 -/
Std.Http.Protocol.H1.Reader.needsMoreInput : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Bool
-- Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
CategoryTheory.MorphismProperty.HasCardinalLT.sup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P₁ P₂ : CategoryTheory.MorphismProperty C} {κ : Cardinal.{w}},
  P₁.HasCardinalLT κ → P₂.HasCardinalLT κ → Cardinal.aleph0 ≤ κ → (P₁ ⊔ P₂).HasCardinalLT κ
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.SatelliteConfig.hlast' : ∀ {α : Type u_1} [inst : MetricSpace α] {N : ℕ} {τ : ℝ} (a : Besicovitch.SatelliteConfig α N τ) (i : Fin N.succ),
  1 ≤ τ → a.r (Fin.last N) ≤ τ * a.r i
-- Lean.Meta.TryThis
/-- Text to be used as a replacement via a code action.  -/
Lean.Meta.Tactic.TryThis.Suggestion.suggestion : Lean.Meta.Tactic.TryThis.Suggestion → Lean.Meta.Tactic.TryThis.SuggestionText
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version within a set at a point.  -/
ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} {y₀ : M'} [CompleteSpace E]
  [inst_12 : IsManifold I 1 M] [inst_13 : IsManifold I' 1 M'],
  ContMDiffWithinAt I' I'.tangent m (fun x => ⟨x, V x⟩) t y₀ →
    ContMDiffWithinAt I I' n f s x₀ →
      (mfderiv[s] f x₀).IsInvertible →
        x₀ ∈ s →
          UniqueMDiff[s] →
            m + 1 ≤ n →
              f ⁻¹' t ∈ nhdsWithin x₀ s →
                f x₀ = y₀ →
                  ContMDiffWithinAt I I.tangent m (fun x => ⟨x, VectorField.mpullbackWithin I I' f V s x⟩) s x₀
-- Mathlib.Data.PNat.Factors
instSemilatticeSupPrimeMultiset : SemilatticeSup PrimeMultiset
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.indiscrete_parts : ∀ {n : ℕ}, n ≠ 0 → (Nat.Partition.indiscrete n).parts = {n}
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_diff_le_size_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → (m₁ \ m₂).size ≤ m₁.size
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.congrLeft_apply : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y)
  (g : LocallyConstant X Z), (LocallyConstant.congrLeft e) g = LocallyConstant.comap (↑e.symm) g
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.ext_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N N' : LieSubmodule R L M}, N = N' ↔ ∀ (m : M), m ∈ N ↔ m ∈ N'
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_cWeight_eq_smul_wInner_one : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)]
  (f g : (i : ι) → E i), ⟪f, g⟫ₙ_[𝕜] = (↑(Fintype.card ι))⁻¹ • ⟪f, g⟫_[𝕜]
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.instSetLike : {L : FirstOrder.Language} → {M : Type u_1} → [inst : L.Structure M] → SetLike (L.ElementarySubstructure M) M
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CompletelyPositiveMapClass.map_cstarMatrix_nonneg' : ∀ {F : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {inst : NonUnitalCStarAlgebra A₁} {inst_1 : NonUnitalCStarAlgebra A₂}
  {inst_2 : PartialOrder A₁} {inst_3 : PartialOrder A₂} {inst_4 : StarOrderedRing A₁} {inst_5 : StarOrderedRing A₂}
  {inst_6 : FunLike F A₁ A₂} [self : CompletelyPositiveMapClass F A₁ A₂] (φ : F) (k : ℕ)
  (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑φ
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `HasStrictFDerivAt.mul'` -/
HasStrictFDerivAt.fun_mul' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a b : E → 𝔸}
  {a' b' : E →L[𝕜] 𝔸} {x : E},
  HasStrictFDerivAt a a' x →
    HasStrictFDerivAt b b' x → HasStrictFDerivAt (fun i => a i * b i) (a x • b' + MulOpposite.op (b x) • a') x
-- Mathlib.Data.Rel
SetRel.prod_comp_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set α) (t₁ t₂ : Set β) (u : Set γ)
  [inst : Decidable (Disjoint t₁ t₂)], SetRel.comp (s ×ˢ t₁) (t₂ ×ˢ u) = if Disjoint t₁ t₂ then ∅ else s ×ˢ u
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.map_iInf : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {ι : Sort u_2} [Nonempty ι] (f : F),
  Function.Injective ⇑f →
    ∀ (s : ι → NonUnitalSubsemiring R), NonUnitalSubsemiring.map f (iInf s) = ⨅ i, NonUnitalSubsemiring.map f (s i)
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.fromGeneratedByTopCat_obj : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] (Y : GeneratedByTopCat X),
  ContinuousGeneratedByCat.fromGeneratedByTopCat.obj Y = { carrier := ↑Y.obj, str := Y.obj.str }
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.coe_prod : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) (K : Subgroup N),
  ↑(H.prod K) = ↑H ×ˢ ↑K
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- A non-unital subring contains the ring's 0.  -/
NonUnitalSubring.zero_mem : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R), 0 ∈ s
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- If two open partial homeomorphisms are equivalent, so are their inverses.  -/
OpenPartialHomeomorph.EqOnSource.symm' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e e' : OpenPartialHomeomorph X Y}, e ≈ e' → e.symm ≈ e'.symm
-- Mathlib.Order.WithBot
WithTop.lt_ofDual_iff : ∀ {α : Type u_1} [inst : LT α] {x : WithTop αᵒᵈ} {y : WithBot α}, y < WithTop.ofDual x ↔ x < WithBot.toDual y
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If `(F', α)` is a right Kan extension of `F` along `L`, then `(F', α)` is a terminal object
in the category `RightExtension L F`.  -/
CategoryTheory.Functor.isUniversalOfIsRightKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : L.comp F' ⟶ F) →
                    [F'.IsRightKanExtension α] →
                      CategoryTheory.CostructuredArrow.IsUniversal (CategoryTheory.Functor.RightExtension.mk F' α)
-- Mathlib.Order.Filter.Defs
Filter.mem_top : ∀ {α : Type u_1} {s : Set α}, s ∈ ⊤ ↔ s = Set.univ
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.card_vadd_le : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset α} {t : Finset β},
  (s +ᵥ t).card ≤ s.card * t.card
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The property that a morphism between bimonoid objects is a bimonoid morphism.  -/
CategoryTheory.IsBimonHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {M N : C} → [CategoryTheory.BimonObj M] → [CategoryTheory.BimonObj N] → (M ⟶ N) → Prop
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypic.isotypicComponents : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : Submodule R M},
  m ∈ isotypicComponents R M → IsIsotypic R ↥m
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RoiSliceData.treeMap : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RoiSliceData α β → Std.DTreeMap.Internal.Impl α β
-- Lean.Compiler.InlineAttrs
_private.Lean.Compiler.InlineAttrs.0.Lean.Compiler.hasInlineAttrCore : Lean.Environment → Lean.Compiler.InlineAttributeKind → Lean.Name → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.cons : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k l = false →
    Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (⟨k, v⟩ :: l)
-- Mathlib.Analysis.InnerProductSpace.Coalgebra
InnerProductSpace.AlgebraOfCoalgebra.mul_def : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] [inst_4 : Coalgebra 𝕜 E] (x y : E),
  x * y = (LinearMap.adjoint CoalgebraStruct.comul) (x ⊗ₜ[𝕜] y)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.anyTR.loop : (n : ℕ) → ((i : ℕ) → i < n → Bool) → (i : ℕ) → i ≤ n → Bool
-- Aesop.Search.Expansion.Simp
Aesop.simpGoalWithAllHypotheses : Lean.MVarId →
  Lean.Meta.Simp.Context →
    Lean.Meta.Simp.SimprocsArray →
      optParam (Option Lean.Meta.Simp.Discharge) none →
        optParam Bool true → optParam Lean.Meta.Simp.Stats { } → Lean.MetaM Aesop.SimpResult
-- Mathlib.Order.Category.FinBddDistLat
/-- Turn a morphism in `FinBddDistLat` back into a `BoundedLatticeHom`.  -/
FinBddDistLat.Hom.hom : {X Y : FinBddDistLat} → X.Hom Y → BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat
-- Mathlib.RingTheory.Ideal.Basic
Ideal.span.eq_1 : ∀ {α : Type u} [inst : Semiring α] (s : Set α), Ideal.span s = Submodule.span α s
-- Mathlib.Order.Lattice.Nat
Set.biInter_lt_succ : ∀ {α : Type u_1} (u : ℕ → Set α) (n : ℕ), ⋂ k, ⋂ (_ : k < n + 1), u k = (⋂ k, ⋂ (_ : k < n), u k) ∩ u n
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_sub : ∀ (a b : BitVec 64), { toBitVec := a - b } = { toBitVec := a } - { toBitVec := b }
-- Mathlib.Topology.UniformSpace.Defs
/-- The uniformity filter. Once `UniformSpace` is defined, `𝓤 α` (`_root_.uniformity`) becomes the
normal form.  -/
UniformSpace.Core.uniformity : {α : Type u} → UniformSpace.Core α → Filter (α × α)
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasStrictFDerivAt_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (c : F) (x : E), HasStrictFDerivAt (fun x => c) 0 x
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- The component 1-morphisms of a lax transformation.  -/
CategoryTheory.Oplax.LaxTrans.app : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} → CategoryTheory.Oplax.LaxTrans F G → (a : B) → F.obj a ⟶ G.obj a
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Spanning.closure_eq : ∀ {α : Type u_2} {M : Matroid α} {S : Set α}, M.Spanning S → M.closure S = M.E
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.limit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}),
  ProfiniteAddGrp.limit F = ProfiniteAddGrp.of ↥(ProfiniteAddGrp.limitConePtAux F)
-- Init.Tactics
/-- `withImplicit tacs` executes `tacs` using the `.implicit` transparency setting.
In this setting only definitions tagged as `[reducible]`, `[instance_reducible]` or
`[implicit_reducible]` are unfolded.
 -/
Lean.Parser.Tactic.withImplicit : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- **Alias** of `CategoryTheory.PreservesFiniteCoproducts.of_preserves_binary_and_initial`.

---

If `F` preserves the initial object and binary coproducts then it preserves finite products.  -/
CategoryTheory.preservesFiniteCoproductsOfPreservesBinaryAndInitial : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F]
  [CategoryTheory.Limits.HasFiniteCoproducts C] (J : Type u_1) [Finite J],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F
-- Mathlib.Algebra.Torsor.Defs
/-- Scalar division and multiplication with the same element cancels out.  -/
Torsor.sdiv_smul' : ∀ {G : outParam (Type u_1)} {P : Type u_2} {inst : Group G} [self : Torsor G P] (p₁ p₂ : P), (p₁ /ₛ p₂) • p₂ = p₁
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.Opposite.rotate_distinguished_triangle : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  T ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C ↔
    T.rotate ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_eq_some_getD : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α} {fallback : β}, a ∈ m → m[a]? = some (m.getD a fallback)
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.id_def : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  (X : CategoryTheory.ShrinkHoms.{u} C),
  CategoryTheory.CategoryStruct.id X =
    (equivShrink (X.fromShrinkHoms ⟶ X.fromShrinkHoms)) (CategoryTheory.CategoryStruct.id X.fromShrinkHoms)
-- Mathlib.Topology.Order.OrderClosed
nhdsWithin_Ioo_eq_nhdsLT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a < b → nhdsWithin b (Set.Ioo a b) = nhdsWithin b (Set.Iio b)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.mapRingHom.congr_simp : ∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : FunLike F (Polynomial R) (Polynomial S)] [inst_3 : RingHomClass F (Polynomial R) (Polynomial S)] (φ φ_1 : F)
  (e_φ : φ = φ_1) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))),
  RatFunc.mapRingHom φ hφ = RatFunc.mapRingHom φ_1 ⋯
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SimpCacheKey.mk : Lean.Name → Array Lean.Elab.Tactic.Grind.ExtraTheorem → Lean.Elab.Tactic.Grind.SimpCacheKey
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasProdUniformlyOn_univ_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α], HasProdUniformlyOn f g Set.univ ↔ HasProdUniformly f g
-- Mathlib.Algebra.GroupWithZero.Basic
left_ne_zero_of_mul : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] {a b : M₀}, a * b ≠ 0 → a ≠ 0
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousWithinAt.add_const : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ∀ (b : M), ContinuousWithinAt (fun x => f x + b) s x
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_update_of_notMem : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} {i : ι},
  i ∉ s → ∀ (f : ι → M) (b : M), ∏ x ∈ s, Function.update f i b x = ∏ x ∈ s, f x
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_ric_eq_zero : ∀ {n i : ℕ}, n < i → (*...=n).toList[i]! = 0
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.nullMeasurable_iff_eventuallyMeasurable : ∀ {α : Type u_2} {β : Type u_3} [m : MeasurableSpace α] [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  (f : α → β), MeasureTheory.NullMeasurable f μ ↔ EventuallyMeasurable m (MeasureTheory.ae μ) f
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result.simp : Lean.Meta.Grind.Result → Lean.Meta.Simp.Stats
-- Mathlib.Data.Finset.Pi
Finset.restrict_preimage_univ : ∀ {ι : Type u_2} {π : ι → Type u_3} {s : Finset ι} [inst : DecidablePred fun x => x ∈ s] (t : (i : ↥s) → Set (π ↑i)),
  s.restrict ⁻¹' Set.univ.pi t = (↑s).pi fun i => if h : i ∈ s then t ⟨i, h⟩ else Set.univ
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_add_compl : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet s → MeasureTheory.Integrable f μ → ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.factors_right_of_inf_factors : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A B : C}
  {X Y : CategoryTheory.Subobject B} {f : A ⟶ B}, (X ⊓ Y).Factors f → Y.Factors f
-- Mathlib.Algebra.Algebra.Subalgebra.Pi
Subalgebra.center_pi : ∀ {ι : Type u_1} {R : Type u_2} {S : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (S i)]
  [inst_2 : (i : ι) → Algebra R (S i)],
  Subalgebra.center R ((i : ι) → S i) = Subalgebra.pi Set.univ fun i => Subalgebra.center R (S i)
-- Mathlib.Tactic.DuplicateDecls
/-- Clear all universe levels from an expression, so that they are ignored.  -/
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.eraseUnivs : Lean.Expr → Lean.Expr
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ π : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι]
  (hτ : MeasureTheory.IsStoppingTime f τ), MeasureTheory.IsStoppingTime f π → MeasurableSet {ω | τ ω = π ω}
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- An affine isomorphism between the domains of affine spaces induces a linear isomorphism over
another ring between the two function spaces.  -/
AffineEquiv.congrLeftₗ : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] →
                      [inst_6 : AddTorsor V₂ P₂] →
                        (R : Type u_10) →
                          (W : Type u_11) →
                            [inst_7 : Ring R] →
                              [inst_8 : AddCommGroup W] →
                                [inst_9 : Module k W] →
                                  [inst_10 : Module R W] →
                                    [inst_11 : SMulCommClass k R W] → (P₁ ≃ᵃ[k] P₂) → (P₁ →ᵃ[k] W) ≃ₗ[R] P₂ →ᵃ[k] W
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.mem_smul_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset β} {a : α} {x : β},
  x ∈ a • s ↔ ∃ y ∈ s, a • y = x
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_add_le : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), (p + q).natDegree ≤ max p.natDegree q.natDegree
-- Mathlib.Topology.Homotopy.HomotopyGroup
Cube.boundary_sum_iff : ∀ {N : Type u_1} {M : Type u_3} {y : M ⊕ N → ↑unitInterval},
  y ∈ Cube.boundary (M ⊕ N) ↔ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N
-- Mathlib.LinearAlgebra.Matrix.Permutation
/-- The l2-operator norm of a permutation matrix is bounded above by 1.
See `Matrix.permMatrix_l2_opNorm_eq` for the equality statement assuming the matrix is nonempty.
 -/
Matrix.permMatrix_l2_opNorm_le : ∀ {n : Type u_1} [inst : DecidableEq n] (σ : Equiv.Perm n) [inst_1 : Fintype n] {𝕜 : Type u_3} [inst_2 : RCLike 𝕜],
  ‖Equiv.Perm.permMatrix 𝕜 σ‖ ≤ 1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RccSlice : (α : Type u_1) → [Ord α] → Type u_1
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.comp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N O : CategoryTheory.Comon C} (f : M.Hom N) (g : N.Hom O),
  (CategoryTheory.Comon.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Composition of morphisms of additive monoid objects.  -/
CategoryTheory.AddMon.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → {M N O : CategoryTheory.AddMon C} → M.Hom N → N.Hom O → M.Hom O
-- Init.Data.SInt.Lemmas
ISize.div_zero : ∀ {a : ISize}, a / 0 = 0
-- Lean.Parser.Command
Lean.Parser.Command.synth.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.dvd_le_tight' : ∀ {d p b₁ b₂ : ℤ}, d > 0 → d ∣ p + b₁ → p + b₂ ≤ 0 → p + (b₁ - d * ((b₁ - b₂) / d)) ≤ 0
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.toAddEquiv_eq_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (f : M ≃ₜ+ N), f.toAddEquiv = ↑f
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalize.eq_1 : ∀ (C : Type u),
  CategoryTheory.FreeMonoidalCategory.normalize C =
    { obj := fun X => X.normalizeObj',
      map := fun {X Y} => Quotient.lift CategoryTheory.FreeMonoidalCategory.normalizeMapAux ⋯, map_id := ⋯,
      map_comp := ⋯ }