mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.summable_eta_q : ∀ (z : UpperHalfPlane), Summable fun n => ‖-ModularForm.eta_q n ↑z‖
-- Std.Time.Format
/-- Parses a `String` in the `AscTime` or `LongDate` format and returns a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.parse : String → Except String Std.Time.PlainDateTime
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_prodCongrLeft : ∀ {α : Type u} [inst : DecidableEq α] {β : Type v} [inst_1 : Fintype α] [inst_2 : DecidableEq β] [inst_3 : Fintype β]
  (σ : α → Equiv.Perm β), Equiv.Perm.sign (Equiv.prodCongrLeft σ) = ∏ k, Equiv.Perm.sign (σ k)
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
MeasureTheory.integral_tsum_of_summable_integral_norm : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_4} [Countable ι] {F : ι → α → E},
  (∀ (i : ι), MeasureTheory.Integrable (F i) μ) →
    (Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ) → ∑' (i : ι), ∫ (a : α), F i a ∂μ = ∫ (a : α), ∑' (i : ι), F i a ∂μ
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Biprod.column_nonzero_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⊞ X ⟶ Y ⊞ Z) [CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.id W = 0 ∨
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
          (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst) ≠
        0 ∨
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
          (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd) ≠
        0
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.instInfSet : (ι : Type u_1) → InfSet (PreAbstractSimplicialComplex ι)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.rightOp_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) (X : C), F.rightOp.obj X = Opposite.op (F.obj (Opposite.op X))
-- Mathlib.Order.Filter.Pi
Filter.Tendsto.pi_map_coprodᵢ : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {β : ι → Type u_3} {m : (i : ι) → α i → β i}
  {g : (i : ι) → Filter (β i)},
  (∀ (i : ι), Filter.Tendsto (m i) (f i) (g i)) →
    Filter.Tendsto (fun k i => m i (k i)) (Filter.coprodᵢ f) (Filter.coprodᵢ g)
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.unsafeForwardRule.sizeOf_spec : ∀ (r₁ : Aesop.ForwardRule) (r₂ : Aesop.UnsafeRule),
  sizeOf (Aesop.BaseRuleSetMember.unsafeForwardRule r₁ r₂) = 1 + sizeOf r₁ + sizeOf r₂
-- Aesop.Script.Tactic
Aesop.Script.Tactic.unstructured : Aesop.Script.UTactic → Aesop.Script.Tactic
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.postcomp₂_app_toFunctor_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) (x : Bᵒᵖ) {X Y : Opposite.unop x ⟶ a}
  (x_1 : X ⟶ Y),
  ((CategoryTheory.Bicategory.postcomp₂ f).app x).toFunctor.map x_1 = CategoryTheory.Bicategory.whiskerRight x_1 f
-- Mathlib.Algebra.BigOperators.Expect
/-- Expectation over a product set equals the expectation of the fiberwise expectations.

For rewriting in the reverse direction, use `Finset.expect_product'`.  -/
Finset.expect_product : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] (s : Finset ι)
  (t : Finset κ) (f : ι × κ → M), ((s ×ˢ t).expect fun x => f x) = s.expect fun i => t.expect fun j => f (i, j)
-- Init.Data.Int.Lemmas
Int.mul_neg : ∀ (a b : ℤ), a * -b = -(a * b)
-- Mathlib.Data.Multiset.Filter
Multiset.count_eq_card_filter_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (a : α),
  Multiset.count a s = (Multiset.filter (fun x => a = x) s).card
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
/-- The Dirichlet convolution of two arithmetic functions `f` and `g` is another arithmetic function
such that `(f * g) n` is the sum of `f x * g y` over all `(x,y)` such that `x * y = n`.  -/
ArithmeticFunction.instSMul : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Zero R] → [inst_1 : AddCommMonoid M] → [SMul R M] → SMul (ArithmeticFunction R) (ArithmeticFunction M)
-- Mathlib.Logic.Equiv.Sum
/-- `α ⊕ β` is equivalent to a `Sigma`-type over `Bool`. Note that this definition assumes `α` and
`β` to be types from the same universe, so it cannot be used directly to transfer theorems about
sigma types to theorems about sum types. In many cases one can use `ULift` to work around this
difficulty.  -/
Equiv.sumEquivSigmaBool : (α β : Type u_9) → α ⊕ β ≃ (b : Bool) × bif b then β else α
-- Mathlib.Analysis.Convex.Between
/-- The closed interior of a 1-dimensional face of a simplex is a segment between its vertices.  -/
Affine.Simplex.closedInterior_face_eq_affineSegment : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {n : ℕ} (s : Affine.Simplex R P n)
  {i j : Fin (n + 1)} (h : i ≠ j), (s.face ⋯).closedInterior = affineSegment R (s.points i) (s.points j)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.lift_addConj_eq_add_add_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X G : C}
  [inst_2 : CategoryTheory.AddGrpObj G] (f₁ f₂ : X ⟶ G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂)
      (CategoryTheory.AddGrpObj.addConj G) =
    f₁ + f₂ + -f₁
-- Mathlib.Combinatorics.Enumerative.DyckWord
instCoeDyckWordListDyckStep : Coe DyckWord (List DyckStep)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.State.symState : Lean.Elab.Tactic.Grind.State → Lean.Meta.Sym.State
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonal_succ_succ' : ∀ {n : ℕ},
  Finset.HasAntidiagonal.antidiagonal (n + 2) =
    Finset.cons (0, n + 2)
      (Finset.cons (n + 2, 0)
        (Finset.map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
          (Finset.HasAntidiagonal.antidiagonal n))
        ⋯)
      ⋯
-- Init.Coe
decPropToBool : (p : Prop) → [Decidable p] → CoeDep Prop p Bool
-- Init.Prelude
Nat.lt_trans : ∀ {n m k : ℕ}, n < m → m < k → n < k
-- Mathlib.Topology.Order.OrderClosed
SuccOrder.nhdsGT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a : α} [SuccOrder α],
  nhdsWithin a (Set.Ioi a) = ⊥
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- The injection map for a cofan of a functor to types.  -/
CategoryTheory.Limits.CofanTypes.inj : {C : Type u} → {F : C → Type v} → (c : CategoryTheory.Limits.CofanTypes F) → (i : C) → F i → c.pt
-- Mathlib.RingTheory.Localization.Defs
/-- Given a localization map `f : R →+* S` for a submonoid `M ⊆ R` and a map of `CommSemiring`s
`g : R →+* P` such that `g(M) ⊆ Units P`, `f x = f y → g x = g y` for all `x y : R`.  -/
IsLocalization.eq_of_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [IsLocalization M S] {g : R →+* P},
  (∀ (y : ↥M), IsUnit (g ↑y)) → ∀ {x y : R}, (algebraMap R S) x = (algebraMap R S) y → g x = g y
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- Evaluation at a single coordinate, as a continuous linear map on `lp E p`.  -/
lp.evalCLM : (𝕜 : Type u_1) →
  {α : Type u_3} →
    (E : α → Type u_4) →
      [inst : (i : α) → NormedAddCommGroup (E i)] →
        [inst_1 : NormedRing 𝕜] →
          [inst_2 : (i : α) → Module 𝕜 (E i)] →
            [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] →
              (p : ENNReal) → [inst_4 : Fact (1 ≤ p)] → (i : α) → ↥(lp E p) →L[𝕜] E i
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.ratio_of_subsingleton : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [Subsingleton α] [inst_4 : DilationClass F α β] (f : F), Dilation.ratio f = 1
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- A monad equipped with the ability to unfold `BicategoricalCoherence.iso`.  -/
Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom : (Type → Type) → Type
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- When `S.f = 0`, this is the canonical isomorphism `S.cycles ≅ S.leftHomology` induced
by `S.leftHomologyπ`.  -/
CategoryTheory.ShortComplex.cyclesIsoLeftHomology : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasLeftHomology] → S.f = 0 → (S.cycles ≅ S.leftHomology)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_W : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] {ι : Type w}
  (D : ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ)
  (hι : HasCardinalLT ι κ) (m : J),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁ D hι m).W =
    (⨆ i, (D i).W) ⊔ CategoryTheory.MorphismProperty.ofHoms fun x => CategoryTheory.CategoryStruct.id m
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.eq_iff_principalUnitGroup : ∀ {K : Type u} [inst : Field K] {A B : ValuationSubring K}, A = B ↔ A.principalUnitGroup = B.principalUnitGroup
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Pretrivialization.continuousLinearMap.congr_simp : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] (e₁ e₁_1 : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e_e₁ : e₁ = e₁_1)
  (e₂ e₂_1 : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) (e_e₂ : e₂ = e₂_1)
  [inst_13 : (x : B) → TopologicalSpace (E₁ x)] [inst_14 : FiberBundle F₁ E₁]
  [inst_15 : (x : B) → TopologicalSpace (E₂ x)] [inst_16 : FiberBundle F₂ E₂]
  [inst_17 : Bundle.Trivialization.IsLinear 𝕜₁ e₁] [inst_18 : Bundle.Trivialization.IsLinear 𝕜₂ e₂],
  Bundle.Pretrivialization.continuousLinearMap σ e₁ e₂ = Bundle.Pretrivialization.continuousLinearMap σ e₁_1 e₂_1
-- Mathlib.Topology.Algebra.Group.Basic
/-- Given a compact set `K` inside an open set `U`, there is an open neighborhood `V` of `1`
such that `V * K ⊆ U`.  -/
compact_open_separated_mul_left : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : MulOneClass G] [ContinuousMul G] {K U : Set G},
  IsCompact K → IsOpen U → K ⊆ U → ∃ V ∈ nhds 1, V * K ⊆ U
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is a division monoid under pointwise operations if `α` is.  -/
Set.divisionMonoid : {α : Type u_2} → [DivisionMonoid α] → DivisionMonoid (Set α)
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.dual.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α} (x : GaloisInsertion u l),
  x.dual = { choice := x.choice, gc := ⋯, u_l_le := ⋯, choice_eq := ⋯ }
-- Mathlib.Data.List.Rotate
List.rotate'_mod : ∀ {α : Type u} (l : List α) (n : ℕ), l.rotate' (n % l.length) = l.rotate' n
-- Batteries.Data.List.Lemmas
List.min!_eq_min_of_ne_nil : ∀ {α : Type u_1} [inst : Inhabited α] [inst_1 : Min α] (l : List α) (hl : l ≠ []), l.min! = l.min hl
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos.sizeOf_spec : sizeOf Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos = 1
-- Mathlib.NumberTheory.SelbergSieve
/-- `nu d` is an approximation to the proportion of elements of `support` that are a multiple of
`d`  -/
BoundingSieve.nu : BoundingSieve → ArithmeticFunction ℝ
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_Ico_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (b : α i), Pi.single i '' Set.Ico 0 b = Set.Ico 0 (Pi.single i b)
-- Mathlib.Data.LawfulXor.Basic
instLawfulXorUInt64 : LawfulXor UInt64
-- Mathlib.Data.List.NodupEquivFin
/-- An element `x : α` of `l : List α` is a duplicate iff it can be found
at two distinct indices `n m : ℕ` inside the list `l`.
 -/
List.duplicate_iff_exists_distinct_get : ∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x l ↔ ∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.finSuccEquiv_comp_C_eq_C : ∀ {R : Type u} [inst : CommSemiring R] (n : ℕ),
  (↑(MvPolynomial.finSuccEquiv R n).symm).comp (Polynomial.C.comp MvPolynomial.C) = MvPolynomial.C
-- Mathlib.Geometry.Euclidean.Inversion.Calculus
DifferentiableAt.inversion : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : InnerProductSpace ℝ F] {c x : E → F} {R : E → ℝ} {a : E},
  DifferentiableAt ℝ c a →
    DifferentiableAt ℝ R a →
      DifferentiableAt ℝ x a → x a ≠ c a → DifferentiableAt ℝ (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) a
-- Init.Data.Char.Basic
/-- True for natural numbers that are valid [Unicode scalar
values](https://www.unicode.org/glossary/#unicode_scalar_value).
 -/
Char.isValidCharNat : ℕ → Prop
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.Expanded.const.injEq : ∀ (c c_1 : Lean.Term),
  (Mathlib.Tactic.LinearCombinationPrime.Expanded.const c = Mathlib.Tactic.LinearCombinationPrime.Expanded.const c_1) =
    (c = c_1)
-- Mathlib.Computability.NFA
NFA.Path.nil : {α : Type u} → {σ : Type v} → {M : NFA α σ} → (s : σ) → M.Path s s []
-- Mathlib.RingTheory.Extension.ExtendScalars
/-- The canonical homomorphism from `P` to `P.extendScalars` induced by the identity map
on the underlying extension rings.  -/
Algebra.Extension.toExtendScalars : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Extension R S) → P.Hom P.extendScalars
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.PointsWithCircumcenterIndex.pointIndex : {n : ℕ} → Fin (n + 1) → Affine.Simplex.PointsWithCircumcenterIndex n
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.instIsPushout : ∀ {R : Type u_1} {M : Type u_2} {S : Type u_4} {A : Type u_5} {B : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : AddCommMonoid M] [inst_8 : Algebra S B] [inst_9 : Algebra A B]
  [inst_10 : IsScalarTower R A B] [inst_11 : IsScalarTower R S B] [Algebra.IsPushout R S A B],
  Algebra.IsPushout R S (AddMonoidAlgebra A M) (AddMonoidAlgebra B M)
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.ediv_ediv_of_pos : ∀ {x y z : ℤ}, 0 < y → 0 < z → x / y / z = x / (y * z)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_uIcc_castLE : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n),
  ∑ i ∈ Finset.uIcc (Fin.castLE h a) (Fin.castLE h b), f i = ∑ i ∈ Finset.uIcc a b, f (Fin.castLE h i)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
_private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.example_localization_eq_localizedModule : ∀ {R : Type u_3} [inst : CommSemiring R] (S : Submonoid R), Localization S = LocalizedModule S R
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_le_mk : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b ↔ ∃ n, |b| ≤ n • |a|
-- Mathlib.Order.BoundedOrder.Lattice
min_top_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderTop α] (a : α), min a ⊤ = a
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
StrictMono.orderIsoOfRightInverse.congr_simp : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Preorder β] (f f_1 : α → β) (e_f : f = f_1)
  (h_mono : StrictMono f) (g g_1 : β → α) (e_g : g = g_1) (hg : Function.RightInverse g f),
  StrictMono.orderIsoOfRightInverse f h_mono g hg = StrictMono.orderIsoOfRightInverse f_1 ⋯ g_1 ⋯
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instBEqSplitInfo : BEq Lean.Meta.Grind.SplitInfo
-- Mathlib.Topology.Order
continuous_induced_rng : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {f : α → β} {g : γ → α} {t₂ : TopologicalSpace β} {t₁ : TopologicalSpace γ},
  Continuous g ↔ Continuous (f ∘ g)
-- Mathlib.Order.Filter.Pointwise
Filter.mem_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α} {g : Filter β} {t : Set β},
  t ∈ f • g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ • t₂ ⊆ t
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.le_prefixFunction_iff : ∀ {k : ℕ} {pat : ByteArray} {stackPos : ℕ} {hst : stackPos < pat.size},
  k ≤ String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat stackPos hst ↔
    ∃ k',
      k ≤ k' ∧ k' ≤ stackPos ∧ String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat pat k' (stackPos + 1)
-- Lean.Elab.Tactic.Omega.Core
/-- Folding `addInequality` over a list.  -/
Lean.Elab.Tactic.Omega.Problem.addInequalities : Lean.Elab.Tactic.Omega.Problem →
  List (ℤ × Lean.Omega.Coeffs × Option Lean.Elab.Tactic.Omega.Proof) → Lean.Elab.Tactic.Omega.Problem
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.Path.inhabited : {F : PFunctor.{uA, uB}} → Inhabited (PFunctor.Approx.Path F)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.MemBaseSet.distortion_le : ∀ {ι : Type u_1} [inst : Fintype ι] {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {c : NNReal}
  {r : (ι → ℝ) → ↑(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I},
  l.MemBaseSet I c r π → l.bDistortion = true → π.distortion ≤ c
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.instIsZeroOrProbabilityMeasureProdCompProdOfIsZeroOrMarkovKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.IsZeroOrProbabilityMeasure μ]
  [ProbabilityTheory.IsZeroOrMarkovKernel κ], MeasureTheory.IsZeroOrProbabilityMeasure (μ.compProd κ)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.inf_eq_right : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {a b : CauSeq α abs},
  b ≤ a → a ⊓ b ≈ b
-- Init.Data.UInt.Lemmas
UInt64.sub_add_cancel : ∀ (a b : UInt64), a - b + b = a
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.preimageDiagram : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preregular C] →
      [inst_2 : CategoryTheory.FinitaryExtensive C] →
        {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))} →
          (∀ (n : ℕ), CategoryTheory.Sheaf.IsLocallySurjective (F.map (CategoryTheory.homOfLE ⋯).op)) →
            (X : C) → (F.obj (Opposite.op 0)).obj.obj (Opposite.op X) → CategoryTheory.Functor ℕᵒᵖ C
-- Mathlib.CategoryTheory.Localization.Opposite
CategoryTheory.Localization.isLocalization_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C},
  W.Q.op.IsLocalization W.op
-- Mathlib.Algebra.Regular.Defs
isAddRegular_iff : ∀ {R : Type u_1} [inst : Add R] {c : R}, IsAddRegular c ↔ IsAddLeftRegular c ∧ IsAddRightRegular c
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_diff!_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false →
          Std.DTreeMap.Internal.Impl.Const.get! (m₁.diff! m₂) k = Std.DTreeMap.Internal.Impl.Const.get! m₁ k
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piOptionEquivProd_symm_apply : ∀ {ι : Type u_7} {R : Option ι → Type u_8} [inst : (i : Option ι) → NonUnitalNonAssocSemiring (R i)]
  (x : R none × ((a : ι) → R (some a))) (a : Option ι),
  RingEquiv.piOptionEquivProd.symm x a = Option.rec x.1 (fun val => x.2 val) a
-- Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
/-- `AlternatingMap.alternatizeUncurryFin` as a linear map.  -/
AlternatingMap.alternatizeUncurryFinLM : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] → {n : ℕ} → (M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) →ₗ[R] M [⋀^Fin (n + 1)]→ₗ[R] N
-- Mathlib.Algebra.Homology.HomologySequence
CategoryTheory.ShortComplex.ShortExact.δ_eq' : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j) {A : C} (x₃ : A ⟶ S.X₃.homology i) (x₂ : A ⟶ S.X₂.opcycles i) (x₁ : A ⟶ S.X₁.cycles j),
  CategoryTheory.CategoryStruct.comp x₂ (HomologicalComplex.opcyclesMap S.g i) =
      CategoryTheory.CategoryStruct.comp x₃ (S.X₃.homologyι i) →
    CategoryTheory.CategoryStruct.comp x₁ (HomologicalComplex.cyclesMap S.f j) =
        CategoryTheory.CategoryStruct.comp x₂ (S.X₂.opcyclesToCycles i j) →
      CategoryTheory.CategoryStruct.comp x₃ (hS.δ i j hij) = CategoryTheory.CategoryStruct.comp x₁ (S.X₁.homologyπ j)
-- Lean.Message
Lean.NamingContext.currNamespace : Lean.NamingContext → Lean.Name
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piUnique_apply : ∀ {ι : Type u_7} (R : ι → Type u_8) [inst : Unique ι] [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (R i)],
  ⇑(RingEquiv.piUnique R) = fun f => f default
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- Type class for manifold without boundary. This differs from `ModelWithCorners.Boundaryless`,
which states that the `ModelWithCorners` maps to the whole model vector space.  -/
BoundarylessManifold : {𝕜 : Type u_5} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_6} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_7} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H → (M : Type u_8) → [inst : TopologicalSpace M] → [ChartedSpace H M] → Prop
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.lhomWithConstants_onRelation : ∀ (L : FirstOrder.Language) (α : Type w') (_n : ℕ) (val : L.Relations _n),
  (L.lhomWithConstants α).onRelation val = Sum.inl val
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalFrontier : ∀ {G : Type u_1} {α : Type u_3} [Countable G] [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.IsAddFundamentalDomain G s μ → μ (MeasureTheory.addFundamentalFrontier G s) = 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInlayHintKind : Lean.ToJson Lean.Lsp.InlayHintKind
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.id_right : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C),
  (CategoryTheory.CategoryStruct.id X).right = CategoryTheory.CategoryStruct.id X.right