mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_const_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} (c : F), deriv (fun x => c + f x) x = deriv f x
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.lt_opow_succ_log_self : ∀ {b : Ordinal.{u_1}}, 1 < b → ∀ (x : Ordinal.{u_1}), x < b ^ Order.succ (Ordinal.log b x)
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.initial_mid : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
  CategoryTheory.Factorisation.initial.mid = X
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepNormal.eq_3 : Turing.ToPartrec.stepNormal Turing.ToPartrec.Code.tail = fun k v => Turing.ToPartrec.Cfg.ret k v.tail
-- Lean.HeadIndex
Lean.HeadIndex.fvar : Lean.FVarId → Lean.HeadIndex
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.isQuotientCoveringMap_npow : ∀ (n : ℕ) [NeZero n], IsQuotientCoveringMap (fun x => x ^ n) ↥(powMonoidHom n).ker
-- Mathlib.Algebra.GroupWithZero.Action.ConjAct
ConjAct.ofConjAct_zero : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀], ConjAct.ofConjAct 0 = 0
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
/-- If `it` is an iterator, then `it.filterMap f` is another iterator that applies a function `f` to all
values emitted by `it`. `f` is expected to return an `Option`. If it returns `none`, then nothing is
emitted; if it returns `some x`, then `x` is emitted.

In situations where `f` is monadic, use `filterMapM` instead.

**Marble diagram:**

```text
it               ---a --b--c --d-e--⊥
it.filterMap     ---a'-----c'-------⊥
```

(given that `f a = some a'`, `f c = c'` and `f b = f d = d e = none`)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be productive even though
no `Productive` instance is provided. For example, if `f` never returns `none`, then
this combinator will preserve productiveness. In such situations, the missing instance needs to
be proved manually.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
returned `Option` value.
 -/
Std.IterM.filterMap : {α β γ : Type w} →
  {m : Type w → Type w'} → [Std.Iterator α m β] → [inst : Monad m] → (f : β → Option γ) → Std.IterM m β → Std.IterM m γ
-- Mathlib.Order.Category.BddOrd
BddOrd.mk : (toPartOrd : PartOrd) → [isBoundedOrder : BoundedOrder ↑toPartOrd] → BddOrd
-- Lean.Util.PPExt
/-- A format tree with `Elab.Info` annotations.
Each `.tag n _` node is annotated with `infos[n]`.
This is used to attach semantic data such as expressions
to pretty-printer outputs.  -/
Lean.FormatWithInfos : Type
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory_whiskerLeft_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {x x_1 x_2 : CategoryTheory.Bicategory.InducedBicategory C F} (h : x ⟶ x_1) {x_3 x_4 : x_1 ⟶ x_2} (η : x_3 ⟶ x_4),
  (CategoryTheory.Bicategory.whiskerLeft h η).hom = CategoryTheory.Bicategory.whiskerLeft h.hom η.hom
-- Aesop.Util.UnorderedArraySet
/-- Precondition: `xs` contains no duplicates.  -/
Aesop.UnorderedArraySet.ofDeduplicatedArray : {α : Type u_1} → [inst : BEq α] → Array α → Aesop.UnorderedArraySet α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertManyIfNewUnit_list_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, Std.ExtDHashMap.Const.insertManyIfNewUnit m [k] = m.insertIfNew k ()
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- Map a cokernel cocone on the difference of two morphisms to the coequalizer cofork.  -/
CategoryTheory.Preadditive.coforkOfCokernelCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} → {f g : X ⟶ Y} → CategoryTheory.Limits.CokernelCofork (f - g) → CategoryTheory.Limits.Cofork f g
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.Hom.mk : {X : UniformSpaceCat} → {Y : UniformSpaceCat} → { f // UniformContinuous f } → X.Hom Y
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.map_eq_top_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
  f.range = ⊤ → ∀ {p : Submodule R M}, Submodule.map f p = ⊤ ↔ p ⊔ f.ker = ⊤
-- Mathlib.Algebra.Order.Module.Defs
smul_pos : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulStrictMono α β], 0 < a → 0 < b → 0 < a • b
-- Mathlib.Order.Filter.CountableSeparatingOn
Filter.exists_singleton_mem_of_mem_of_forall_separating : ∀ {α : Type u_1} {l : Filter α} [CountableInterFilter l] [Nonempty α] (p : Set α → Prop) {s : Set α}
  [HasCountableSeparatingOn α p s], s ∈ l → (∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l) → ∃ a, {a} ∈ l
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.norm_coe : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (x : WithAbs ↑v),
  ‖{ toCompletion := ↑x }‖ = v ((WithAbs.equiv ↑v) x)
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
SSet.horn.IsCompatible.exists_lift_of_kanComplex : ∀ {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)}
  [X.KanComplex],
  SSet.horn.IsCompatible f →
    ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) φ = f j hj
-- Mathlib.Algebra.Category.ModuleCat.Kernels
/-- The category of R-modules has cokernels, given by the projection onto the quotient.  -/
ModuleCat.hasCokernels_moduleCat : ∀ {R : Type u} [inst : Ring R], CategoryTheory.Limits.HasCokernels (ModuleCat R)
-- Std.Http.Data.Body.Any
/-- Returns `true` when the body stream is closed.
 -/
Std.Http.Body.Any.isClosed : Std.Http.Body.Any → Std.Async.Async Bool
-- Mathlib.Order.Closure
LowerAdjoint.closure_union_closure : ∀ {α : Type u_1} {β : Type u_4} [inst : SetLike α β] [inst_1 : Preorder α] (l : LowerAdjoint SetLike.coe) (x y : α),
  l.toFun (↑(l.toFun ↑x) ∪ ↑(l.toFun ↑y)) = l.toFun (↑x ∪ ↑y)
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.instDFunLikeFiniteAdeleRingHeightOneSpectrumAdicCompletion : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              DFunLike (IsDedekindDomain.FiniteAdeleRing R K) (IsDedekindDomain.HeightOneSpectrum R)
                (IsDedekindDomain.HeightOneSpectrum.adicCompletion K)
-- Mathlib.Data.Sym.Basic
Sym.ext : ∀ {α : Type u_1} {n : ℕ} {s₁ s₂ : Sym α n}, ↑s₁ = ↑s₂ → s₁ = s₂
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.instIsAddMonHomNegHomOfIsCommAddMonObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M G : C}
  [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddGrpObj G]
  [inst_4 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommAddMonObj G] {f : M ⟶ G}
  [CategoryTheory.IsAddMonHom f], CategoryTheory.IsAddMonHom (-f)
-- Mathlib.Order.Hom.Lattice
instCoeTCSupHomOfSupHomClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Max α] [inst_2 : Max β]
  [inst_3 : SupHomClass F α β], instCoeTCSupHomOfSupHomClass = { coe := fun f => { toFun := ⇑f, map_sup' := ⋯ } }
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.distribMulAction : {R : Type u} →
  [inst : Semiring R] →
    {S : Type u_1} → [inst_1 : Monoid S] → [DistribMulAction S R] → DistribMulAction S (Polynomial R)
-- Lean.Meta.MethodSpecs
/-- This function checks the `instName` for eligibility and collects the information to rewrite.
It is run twice: when setting the `@[specs]` attribute as a preflight check, and when actually realizing
the constants.
 -/
_private.Lean.Meta.MethodSpecs.0.Lean.getMethodSpecsInfo : Lean.Name → Lean.MetaM Lean.MethodSpecsInfo✝
-- Mathlib.Algebra.Module.Injective
Module.Baer.extension_property : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N],
  Module.Baer R Q → ∀ (f : M →ₗ[R] N), Function.Injective ⇑f → ∀ (g : M →ₗ[R] Q), ∃ h, h ∘ₗ f = g
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNonUnitalNonAssocSemiringQuotient : {R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → (c : RingCon R) → NonUnitalNonAssocSemiring c.Quotient
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.evalLinarith : Lean.Elab.Tactic.Tactic
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {a : α}, Std.Internal.List.getKey? a [] = none
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.DBuilderName.default : Aesop.Frontend.DBuilderName
-- Init.Data.UInt.Basic
/-- Adds two 8-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.add : UInt8 → UInt8 → UInt8
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.rangeRestrictFieldEquiv_apply_coe : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L) (a : K),
  ↑(f.rangeRestrictFieldEquiv a) = f a
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_comap_eq_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Surjective ⇑f → ∀ (p : Submodule R₂ M₂), Submodule.map f (Submodule.comap f p) = p
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.coe_orderIso : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), ⇑↑f = ⇑f
-- Mathlib.SetTheory.Ordinal.Notation
/-- **Alias** of the forward direction of `ONote.le_def`. -/
ONote.repr_le_repr : ∀ {x y : ONote}, x ≤ y → x.repr ≤ y.repr
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- If `χ` is a multiplicative function such that `J(a | p) = χ p` for all odd primes `p`,
then `J(a | b)` equals `χ b` for all odd natural numbers `b`.  -/
jacobiSym.value_at : ∀ (a : ℤ) {R : Type u_1} [inst : Semiring R] (χ : R →* ℤ),
  (∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p) → ∀ {b : ℕ}, Odd b → jacobiSym a b = χ ↑b
-- Mathlib.Probability.Moments.Variance
/-- The `ℝ≥0∞`-valued variance of a real-valued random variable defined as the Lebesgue integral of
`‖X - 𝔼[X]‖^2`.  -/
ProbabilityTheory.evariance : {Ω : Type u_1} → {mΩ : MeasurableSpace Ω} → (Ω → ℝ) → MeasureTheory.Measure Ω → ENNReal
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- To prove a property on morphisms of a path category with given source `a`, it suffices to
prove it for the identity and prove that the property is preserved under composition on the right
with length 1 paths.  -/
CategoryTheory.Paths.induction_fixed_source : ∀ {V : Type u₁} [inst : Quiver V] {a : CategoryTheory.Paths V} (P : {b : CategoryTheory.Paths V} → (a ⟶ b) → Prop),
  P (CategoryTheory.CategoryStruct.id a) →
    (∀ {u v : V} (p : a ⟶ (CategoryTheory.Paths.of V).obj u) (q : u ⟶ v),
        P p → P (CategoryTheory.CategoryStruct.comp p ((CategoryTheory.Paths.of V).map q))) →
      ∀ {b : CategoryTheory.Paths V} (f : a ⟶ b), P f
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.instDecidableLtKey : (a b : Lean.Meta.DiscrTree.Key) → Decidable (a < b)
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- One can bound the `k`-th derivative of the Fourier integral of `f`, multiplied by `(L v w) ^ n`,
in terms of integrals of iterated derivatives of `f` (of order up to `n`) multiplied by `‖v‖ ^ i`
(for `i ≤ k`).  -/
VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V]
  {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] {K N : ℕ∞},
  ContDiff ℝ (↑N) f →
    (∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ) →
      ∀ {k n : ℕ},
        ↑k ≤ K →
          ↑n ≤ N →
            ∀ (v : V) (w : W),
              |(L v) w| ^ n *
                  ‖iteratedFDeriv ℝ k
                      (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w‖ ≤
                ‖v‖ ^ n * (2 * Real.pi * ‖L‖) ^ k * (2 * ↑k + 2) ^ n *
                  ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
                    ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.exists_list_of_mem_closure : ∀ {R : Type u_1} [inst : Ring R] {s : Set R} {x : R},
  x ∈ Subring.closure s → ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff.eq_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m : σ →₀ ℕ) (p : MvPolynomial σ R),
  MvPolynomial.coeff m p = p.coeff m
-- Mathlib.RingTheory.Henselian
instHenselianRingMaximalIdeal : ∀ (R : Type u_1) [inst : CommRing R] [hR : HenselianLocalRing R], HenselianRing R (IsLocalRing.maximalIdeal R)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aevalTower_algebraMap : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S : Type u_2} {A : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring A] [inst_3 : Algebra S R] [inst_4 : Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (x : R),
  (MvPolynomial.aevalTower g y) ((algebraMap R (MvPolynomial σ R)) x) = g x
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R],
  (IsDiscreteValuationRing.addVal R) 0 = ⊤
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.Measure.setIntegral_comp_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {F : Type u_2}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace ℝ F] (f : E → F) {R : ℝ} (s : Set E),
  R ≠ 0 → ∫ (x : E) in s, f (R • x) ∂μ = |(R ^ Module.finrank ℝ E)⁻¹| • ∫ (x : E) in R • s, f x ∂μ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.MonObj M] (f : X ⟶ M) {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul f)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id M) f)
          CategoryTheory.MonObj.mul))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.subset_nsmul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s : Finset α} {n : ℕ}, 0 ∈ s → n ≠ 0 → s ⊆ n • s
-- Mathlib.RingTheory.Valuation.Basic
Valuation.leAddSubgroup_monotone : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀),
  Monotone v.leAddSubgroup
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_eq_contract_apply : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] (x : TensorProduct R (Module.Dual R M) M),
  (LinearMap.trace R M) ((dualTensorHom R M M) x) = (contractLeft R M) x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
/-- **Alias** of the reverse direction of `Unitization.inr_nonneg_iff`. -/
Unitization.LE.le.inr : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : A}, 0 ≤ a → 0 ≤ ↑a
-- Mathlib.Algebra.Lie.BaseChange
/-- The Lie algebra homomorphism induced by an algebra map.  -/
LieAlgebra.ExtendScalars.map : {R : Type u_5} →
  {A : Type u_6} →
    {B : Type u_7} →
      {L : Type u_8} →
        {L' : Type u_9} →
          [inst : CommRing R] →
            [inst_1 : CommRing A] →
              [inst_2 : Algebra R A] →
                [inst_3 : CommRing B] →
                  [inst_4 : Algebra R B] →
                    [inst_5 : LieRing L] →
                      [inst_6 : LieAlgebra R L] →
                        [inst_7 : LieRing L'] →
                          [inst_8 : LieAlgebra R L'] →
                            (A →ₐ[R] B) → (L →ₗ⁅R⁆ L') → TensorProduct R A L →ₗ⁅R⁆ TensorProduct R B L'
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableAt_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_6} {F' : ι → Type u_7} [inst_3 : (i : ι) → NormedAddCommGroup (F' i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  DifferentiableAt 𝕜 Φ x ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun x => Φ x i) x
-- Batteries.Lean.Util.EnvSearch
/-- Find constants in current environment that match find options and predicate.
 -/
Lean.getMatchingConstants : {m : Type → Type} →
  [Monad m] → [Lean.MonadEnv m] → (Lean.ConstantInfo → m Bool) → optParam Bool true → m (Array Lean.ConstantInfo)
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.IsCyclicallyReduced.isReduced : ∀ {α : Type u} {L : List (α × Bool)}, FreeAddGroup.IsCyclicallyReduced L → FreeAddGroup.IsReduced L
-- Std.Http.Internal.ChunkedBuffer
/-- A structure that accumulates multiple `ByteArray`s efficiently by tracking them in an array and
maintaining the total size. This allows building large buffers without repeated allocations and copies.
 -/
Std.Http.Internal.ChunkedBuffer : Type
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.instInverseImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {P : CategoryTheory.MorphismProperty D} [P.IsMultiplicative] (F : CategoryTheory.Functor C D),
  (P.inverseImage F).IsMultiplicative
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.isoNerve_inv_app_apply : ∀ {n d : ℕ} (F : (CategoryTheory.nerve (ULift.{u, 0} (Fin (n + 1)))).obj (Opposite.op { len := d })) (i : Fin (d + 1)),
  ((CategoryTheory.ConcreteCategory.hom ((SSet.stdSimplex.isoNerve.{u} n).inv.app (Opposite.op { len := d }))) F) i =
    (F.obj i).down
-- Std.Async.System
Std.Async.System.instReprOSInfo : Repr Std.Async.System.OSInfo
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequenceδ.eq_1 : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) [inst_3 : F.ShiftSequence ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
  F.homologySequenceδ T n₀ n₁ h = F.shiftMap T.mor₃ n₀ n₁ ⋯
-- Mathlib.Algebra.Order.ToIntervalMod
iUnion_Ioc_add_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] {p : α},
  0 < p → ∀ (a : α), ⋃ n, Set.Ioc (a + n • p) (a + (n + 1) • p) = Set.univ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Actual value.  -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.Literal.value : (self : BitVec.Literal✝) → BitVec (BitVec.Literal.n✝ self)
-- Mathlib.Data.Set.Lattice
Set.iInter_subset : ∀ {β : Type u_2} {ι : Sort u_5} (s : ι → Set β) (i : ι), ⋂ i, s i ⊆ s i
-- Init.Data.Int.DivMod.Lemmas
Int.mul_bmod_bmod : ∀ {x y : ℤ} {n : ℕ}, (x * y.bmod n).bmod n = (x * y).bmod n
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Iio_add_one_eq_Iic : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] [NoMaxOrder α] (b : α),
  Set.Iio (b + 1) = Set.Iic b
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt8.reduceGE : Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.pushforwardId_hom_counit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : C)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id I)]
  [inst_2 : CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.id I)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.ExponentiableMorphism.pushforwardId I).hom
        (CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.CategoryStruct.id I)))
      (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.id I)).counit =
    (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.id I)).counit
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.encoding_encode : ∀ {L : FirstOrder.Language} {α : Type u'} (φ : (n : ℕ) × L.BoundedFormula α n),
  FirstOrder.Language.BoundedFormula.encoding.encode φ = φ.snd.listEncode
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instInhabited : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → Inhabited (FractionalIdeal S P)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_comap_eq_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f → ∀ (S : AddSubmonoid N), AddSubmonoid.map f (AddSubmonoid.comap f S) = S
-- Init.Data.UInt.Lemmas
UInt8.toFin_add : ∀ (a b : UInt8), (a + b).toFin = a.toFin + b.toFin
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.ofPermHomFun_apply_of_cycleOf_mem : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)) {x : α} {c : ↥g.cycleFactorsFinset},
  x ∈ (↑c).support → ∀ {m : ℤ}, (g ^ m) (a c) = x → a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))
-- Mathlib.Algebra.Group.Submonoid.BigOperators
AddSubmonoidClass.coe_multiset_sum : ∀ {B : Type u_3} {S : B} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : SetLike B M] [inst_2 : AddSubmonoidClass B M]
  (m : Multiset ↥S), ↑m.sum = (Multiset.map Subtype.val m).sum
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
MeasureTheory.Measure.IsFiniteMeasureOnCompacts.comap : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [mα : MeasurableSpace α] [BorelSpace α]
  {mβ : TopologicalSpace β} [inst_2 : MeasurableSpace β] [BorelSpace β] (μ : MeasureTheory.Measure β)
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : α ≃ₜ β),
  MeasureTheory.IsFiniteMeasureOnCompacts (MeasureTheory.Measure.comap (⇑f) μ)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mod_self : ∀ (a : Ordinal.{u_4}), a % a = 0