mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.LazyDiscrTree
/-- Allocate constants to tasks according to `constantsPerTask`.  -/
_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.createImportedDiscrTree.go : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadLiftT BaseIO m] →
        Lean.Core.Context →
          Lean.Environment →
            (Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) →
              ℕ →
                ℕ →
                  Lean.NameGenerator →
                    Array (Task (Lean.Meta.LazyDiscrTree.InitResults α)) →
                      ℕ → ℕ → ℕ → m (Array (Task (Lean.Meta.LazyDiscrTree.InitResults α)))
-- Mathlib.Topology.MetricSpace.Infsep
Set.Subsingleton.infsep_zero : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.Subsingleton → s.infsep = 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.mul_continuousOn : ∀ {A : Type u_7} [inst : NormedRing A] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f g : ℝ → A},
  IntervalIntegrable f μ a b → ContinuousOn g (Set.uIcc a b) → IntervalIntegrable (fun x => f x * g x) μ a b
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instNonemptyContInfoRef : Nonempty Lean.Elab.Do.ContInfoRef
-- Mathlib.CategoryTheory.Limits.Indization.Category
/-- The category of Ind-objects of `C`.  -/
CategoryTheory.Ind : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u (v + 1))
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is strictly positive,
then `f` is a strictly monotone function on `D`.  -/
strictAntiOn_of_hasDerivWithinAt_neg : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f f' : ℝ → ℝ},
      ContinuousOn f D →
        (∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) → (∀ x ∈ interior D, f' x < 0) → StrictAntiOn f D
-- Mathlib.RingTheory.DedekindDomain.Different
Ideal.quotientMulEquivQuotientProd.congr_simp : ∀ {R : Type u_2} [inst : CommRing R] (I J : Ideal R) (coprime : IsCoprime I J),
  I.quotientMulEquivQuotientProd J coprime = I.quotientMulEquivQuotientProd J coprime
-- Init.Data.Int.Order
Int.natAbs_mul_natAbs_eq : ∀ {a b : ℤ} {c : ℕ}, a * b = ↑c → a.natAbs * b.natAbs = c
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.coe_inj : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Zero 𝕜] [inst_1 : LE α] {f g : IncidenceAlgebra 𝕜 α}, ⇑f = ⇑g ↔ f = g
-- Std.Async.Basic
/-- Sequences two computations, allowing the second to depend on the value computed by the first.
 -/
Std.Async.BaseAsync.bind : {α β : Type} →
  Std.Async.BaseAsync α →
    (α → Std.Async.BaseAsync β) →
      optParam Task.Priority Task.Priority.default → optParam Bool false → Std.Async.BaseAsync β
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_def : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (σ : Equiv.Perm α),
  σ.cycleType = Multiset.map (Finset.card ∘ Equiv.Perm.support) σ.cycleFactorsFinset.val
-- Init.Data.Int.Linear
Int.Internal.Linear.cmod.eq_1 : ∀ (a b : ℤ), Int.Internal.Linear.cmod a b = -(-a % b)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R), CategoryTheory.CategoryStruct.comp M.toFreeYonedaCoproduct M.fromFreeYonedaCoproduct = 0
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_restriction : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) (X₀ : C₀) {Y₀ : C₀}
  (f : F.obj Y₀ ⟶ F.obj X₀),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv data G₀ X₀)
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction data G₀ f) =
    CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ f
-- Init.Omega.IntList
Lean.Omega.IntList.sum_smul : ∀ (i : ℤ) (xs : Lean.Omega.IntList), (i * xs).sum = i * xs.sum
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.findSomeM?_eq_match_step.match_1.splitter : {γ : Type u_1} →
  (motive : Option γ → Sort u_2) →
    (__do_lift : Option γ) → (Unit → motive none) → ((fx : γ) → motive (some fx)) → motive __do_lift
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
CategoryTheory.PreservesImage.inv_comp_image_ι_map_assoc : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Limits.HasEqualizers A] [inst_3 : CategoryTheory.Limits.HasImages A]
  [inst_4 : CategoryTheory.StrongEpiCategory B] [inst_5 : CategoryTheory.Limits.HasImages B]
  (L : CategoryTheory.Functor A B)
  [inst_6 :
    ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L]
  [inst_7 :
    ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L]
  {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (L.map f)) h) =
    CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.image.ι f)) h
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If a function is countably sub-multiplicative then it is sub-multiplicative on countable
types  -/
rel_iSup_tprod : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {β : Type u_4} [Countable β]
  [inst_3 : CompleteLattice α] (m : α → M),
  m ⊥ = 1 →
    ∀ (R : M → M → Prop),
      (∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))) → ∀ (s : β → α), R (m (⨆ b, s b)) (∏' (b : β), m (s b))
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.ExprConfigCacheKey.mk.injEq : ∀ (expr : Lean.Expr) (configKey : UInt64) (expr_1 : Lean.Expr) (configKey_1 : UInt64),
  ({ expr := expr, configKey := configKey } = { expr := expr_1, configKey := configKey_1 }) =
    (expr = expr_1 ∧ configKey = configKey_1)
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.separableSpace_completion : ∀ {α : Type u_1} [inst : UniformSpace α] [TopologicalSpace.SeparableSpace α],
  TopologicalSpace.SeparableSpace (UniformSpace.Completion α)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.triangleOpEquivalence_inverse : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ],
  (CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse =
    CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderivWithin_subset : ∀ {𝕜 : 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] {f : E → F} {x : E} {s t : Set E},
  s ⊆ t →
    UniqueDiffWithinAt 𝕜 s x →
      ∀ [ContinuousAdd E] [ContinuousSMul 𝕜 E] [ContinuousAdd F] [ContinuousSMul 𝕜 F] [T2Space F],
        DifferentiableWithinAt 𝕜 f t x → fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
-- Mathlib.Data.ENNReal.Real
ENNReal.toNNReal_strict_mono : ∀ {a b : ENNReal}, b ≠ ⊤ → a < b → a.toNNReal < b.toNNReal
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instLatticeOfSeparatelyContinuousMul : {G : Type u} →
  [inst : Group G] → [inst_1 : TopologicalSpace G] → [SeparatelyContinuousMul G] → Lattice (OpenNormalSubgroup G)
-- Lean.Elab.Deriving.Basic
_private.Lean.Elab.Deriving.Basic.0.Lean.Elab.Term.MkInstResult.mk.injEq : ∀ (instType instVal instType_1 instVal_1 : Lean.Expr),
  ({ instType := instType, instVal := instVal } = { instType := instType_1, instVal := instVal_1 }) =
    (instType = instType_1 ∧ instVal = instVal_1)
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.rightDeriv_le_slope_of_mem_interior : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ},
  ConvexOn ℝ S f → ∀ {y : ℝ}, x ∈ interior S → y ∈ S → x < y → derivWithin f (Set.Ioi x) x ≤ slope f x y
-- Mathlib.Analysis.Normed.Module.Bases
/-- The `n`-th projection has rank `n`.  -/
SchauderBasis.RankOneDecomposition.finrank_range : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (self : SchauderBasis.RankOneDecomposition 𝕜 X) (n : ℕ),
  Module.finrank 𝕜 ↥(↑(self.P n)).range = n
-- Mathlib.Topology.Constructions
instCompactSpaceAdditive : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X], CompactSpace (Additive X)
-- Mathlib.Topology.Sheaves.Over
/-- If `X` is a topological space and `U : Opens X`,
then the category `Over U` is equivalent to `Opens ↥U`.  -/
TopologicalSpace.Opens.overEquivalence : {X : Type u} →
  [inst : TopologicalSpace X] → (U : TopologicalSpace.Opens X) → CategoryTheory.Over U ≌ TopologicalSpace.Opens ↥U
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.sumCoeffsExp_p_eq_one : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), ∑ i, a i * b i ^ AkraBazziRecurrence.p a b = 1
-- Init.Data.UInt.Lemmas
UInt64.ofFin_le_iff_le : ∀ {a b : Fin UInt64.size}, UInt64.ofFin a ≤ UInt64.ofFin b ↔ a ≤ b
-- Init.Data.SInt.IntToBitVec
ISize.lt_iff_toBitVec32_slt : ∀ {a b : ISize} (h : System.Platform.numBits = 32), a < b ↔ (a.toBitVec32 h).slt (b.toBitVec32 h) = true
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
SubMulAction.coe_pow : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : Monoid M]
  [inst_3 : IsScalarTower R M M] [inst_4 : SMulCommClass R M M] (p : SubMulAction R M) {n : ℕ},
  n ≠ 0 → ↑(p ^ n) = ↑p ^ n
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_of_forall_mem : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∀ {p : α → Prop}, (∀ x ∈ s, p x) → ∀ᵐ (x : α) ∂μ.restrict s, p x
-- Mathlib.Combinatorics.Graph.Basic
Graph.Inc.eq_of_isLink_of_ne_left : ∀ {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β}, G.Inc e x → G.IsLink e y z → x ≠ y → x = z
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_const_smul : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] {𝕜 : Type u_4} [inst_2 : SMul 𝕜 β] (c : 𝕜),
  MeasureTheory.stoppedProcess (c • u) τ = c • MeasureTheory.stoppedProcess u τ
-- Mathlib.Topology.MetricSpace.CoveringNumbers
/-- The external covering number of a set `A` in `X` for radius `ε` is the minimal cardinality
(in `ℕ∞`) of an `ε`-cover by points in `X` (not necessarily in `A`).  -/
Metric.externalCoveringNumber : {X : Type u_1} → [PseudoEMetricSpace X] → NNReal → Set X → ℕ∞
-- Lean.Meta.Tactic.NormCast
/-- Counts how many coercions are inside the expression, excluding the head ones.  -/
Lean.Meta.NormCast.countInternalCoes : Lean.Expr → Lean.MetaM ℕ
-- Mathlib.Algebra.Order.Group.OrderIso
le_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] [AddRightMono α] {a b : α}, a ≤ -b ↔ b ≤ -a
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.reindex_simple : ∀ {B : Type u_1} {B' : Type u_2} (e : B ≃ B') {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B}
  (cs : CoxeterSystem M W) (i' : B'), (cs.reindex e).simple i' = cs.simple (e.symm i')
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.rescaleAlgHom_mul : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (a b : σ → R),
  MvPowerSeries.rescaleAlgHom (a * b) = (MvPowerSeries.rescaleAlgHom b).comp (MvPowerSeries.rescaleAlgHom a)
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.hom_neg_apply : ∀ {X Y : AddGrpCat} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.Topology.Order.Hom.Basic
/-- Composition of `ContinuousOrderHom`s as a `ContinuousOrderHom`.  -/
ContinuousOrderHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : TopologicalSpace α] →
        [inst_1 : Preorder α] →
          [inst_2 : TopologicalSpace β] →
            [inst_3 : Preorder β] →
              [inst_4 : TopologicalSpace γ] → [inst_5 : Preorder γ] → (β →Co γ) → (α →Co β) → α →Co γ
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.symm_toMulEquiv : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ↑e.symm = (↑e).symm
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_eq_empty_iff : ∀ {m n : ℕ}, (m...=n).toArray = #[] ↔ n < m
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)),
  (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj F U c).pt = c.pt
-- Mathlib.Topology.Algebra.Group.Basic
ContinuousAt.zsmul : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G} {x : α}, ContinuousAt f x → ∀ (z : ℤ), ContinuousAt (z • f) x
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.subset_dual_flip_iff_subset_dual : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {s : Set M} {t : Set N}, s ⊆ ↑(PointedCone.dual p.flip t) ↔ t ⊆ ↑(PointedCone.dual p s)
-- Init.Data.SInt.Bitwise
ISize.not_or_self : ∀ {a : ISize}, ~~~a ||| a = -1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.size_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp}, t₁.Equiv t₂ → t₁.size = t₂.size
-- Init.Data.SInt.Lemmas
ISize.zero_lt_one : 0 < 1
-- Lean.Compiler.IR.Basic
Lean.IR.DeclInfo.mk.injEq : ∀ (sorryDep? sorryDep?_1 : Option Lean.Name),
  ({ sorryDep? := sorryDep? } = { sorryDep? := sorryDep?_1 }) = (sorryDep? = sorryDep?_1)
-- Mathlib.Data.Sym.Sym2
/-- Multiplication as a function from `Sym2`.
 -/
Sym2.mul : {M : Type u_4} → [CommMagma M] → Sym2 M → M
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.reverse_balance1 : ∀ {α : Type u_1} (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  (l.balance1 v r).reverse = r.reverse.balance2 v l.reverse
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_congr : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  {t : Finset ι} {w : ι → R} {z : ι → E} [inst_3 : DecidableEq ι] {t' : Finset ι} {w' : ι → R} {z' : ι → E},
  (∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i) →
    t.centerMass w z = t'.centerMass w' z'
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.equiv_iff_keys_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.TreeMap α Unit cmp},
  t₁.Equiv t₂ ↔ t₁.keys = t₂.keys
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∈ t₂ → (t₁ ∩ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppScalarRight_symm_apply_single : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {ι : Type u_5}
  [inst_7 : DecidableEq ι] (i : ι) (m : M),
  ((TensorProduct.finsuppScalarRight R S M ι).symm fun₀ | i => m) = m ⊗ₜ[R] fun₀ | i => 1
-- Mathlib.Topology.Homotopy.Contractible
ContractibleSpace.hequiv : ∀ (X : Type u_1) (Y : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [ContractibleSpace X]
  [ContractibleSpace Y], Nonempty (ContinuousMap.HomotopyEquiv X Y)
-- Lean.Meta.Tactic.Cases
_private.Lean.Meta.Tactic.Cases.0.Lean.Meta.Cases.unifyCasesEqs : ℕ → Array Lean.Meta.CasesSubgoal → Lean.MetaM (Array Lean.Meta.CasesSubgoal)
-- Init.Prelude
Nat.mod_lt : ∀ (x : ℕ) {y : ℕ}, 0 < y → x % y < y
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Cell.getEntry?.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (p : (a : α) × β a) → motive (some p)),
  (match none with
    | none => h_1 ()
    | some p => h_2 p) =
    h_1 ()
-- Mathlib.LinearAlgebra.Ray
sameRay_neg_smul_left_iff_of_ne : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [Module.IsTorsionFree R M] {v : M} {r : R},
  v ≠ 0 → r ≠ 0 → (SameRay R (r • v) (-v) ↔ r < 0)
-- Lean.Elab.Do.Switch
Lean.Elab.Term.backward.do.legacy : Lean.Option Bool
-- Mathlib.Topology.Separation.Regular
/-- The `SeparationQuotient` of a completely normal R₀ space is a T₅ space.  -/
instT5SpaceSeparationQuotientOfCompletelyNormalSpaceOfR0Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompletelyNormalSpace X] [R0Space X], T5Space (SeparationQuotient X)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.equivProd_inverse_map_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X Y : A × B} (f : X ⟶ Y),
  ((CategoryTheory.Comma.equivProd L R).inverse.map f).right = f.2
-- Mathlib.ModelTheory.Bundled
/-- The reduct of any model of `φ.onTheory T` is a model of `T`.  -/
FirstOrder.Language.Theory.ModelType.reduct : {L : FirstOrder.Language} →
  {T : L.Theory} → {L' : FirstOrder.Language} → (φ : L →ᴸ L') → (φ.onTheory T).ModelType → T.ModelType
-- Init.Data.Int.Gcd
Int.lcm_dvd_lcm_of_dvd_right : ∀ {a b : ℤ} (c : ℤ), a ∣ b → c.lcm a ∣ c.lcm b
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.hausdorffMeasure_vadd : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {α : Type u_4}
  [inst_3 : VAdd α X] [IsIsometricVAdd α X] {d : ℝ} (c : α),
  (0 ≤ d ∨ Function.Surjective fun x => c +ᵥ x) →
    ∀ (s : Set X), (MeasureTheory.Measure.hausdorffMeasure d) (c +ᵥ s) = (MeasureTheory.Measure.hausdorffMeasure d) s
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- A multiplicative algebra norm on an `R`-algebra norm `S` is a multiplicative ring norm on `S`
compatible with the action of `R`.  -/
MulAlgebraNorm : (R : Type u_1) → [inst : SeminormedCommRing R] → (S : Type u_2) → [inst_1 : Ring S] → [Algebra R S] → Type u_2
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_arg : ∀ (z : Circle), Circle.exp (↑z).arg = z
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.sZMod.eq_def : ∀ (p x : ℕ),
  LucasLehmer.sZMod p x =
    match x with
    | 0 => 4
    | i.succ => LucasLehmer.sZMod p i ^ 2 - 2
-- Mathlib.Algebra.Homology.Augment
CochainComplex.truncate_obj_d : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : CochainComplex V ℕ) (i j : ℕ), (CochainComplex.truncate.obj C).d i j = C.d (i + 1) (j + 1)
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.mul_left : ∀ {D : Type u_1} {Q : Type u_2} [inst : Group D] [inst_1 : Group Q] (a b : D ≀ᵣ Q),
  (a * b).left = a.left * fun x => b.left (a.right⁻¹ * x)
-- Mathlib.Topology.WithTopology
WithTopology.isClosed_iff : ∀ {X : Type u_1} (t : TopologicalSpace X) {s : Set (WithTopology X t)},
  IsClosed s ↔ IsClosed (WithTopology.toTopology t ⁻¹' s)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.tendsto_atTop : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] {u v : α → β}
  {l : Filter α} [OrderTopology β],
  Asymptotics.IsEquivalent l u v → Filter.Tendsto u l Filter.atTop → Filter.Tendsto v l Filter.atTop
-- Mathlib.Algebra.Group.Center
Set.units_inv_mem_center : ∀ {M : Type u_1} [inst : Monoid M] {a : Mˣ}, ↑a ∈ Set.center M → ↑a⁻¹ ∈ Set.center M
-- Aesop.Script.StructureDynamic
/-- Given a bijective map `map` from new `MVarId`s to old `MVarId`s, update the
`steps` of the context `c` such that each entry whose key is an old `MVarId` `m`
is replaced with an entry whose key is the corresponding new `MVarId`
`map⁻¹ m`.
 -/
Aesop.Script.DynStructureM.Context.updateMVarIds : Aesop.Script.DynStructureM.Context → Std.HashMap Lean.MVarId Lean.MVarId → Aesop.Script.DynStructureM.Context
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
aemeasurable_congr : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {f g : α → β}
  {μ : MeasureTheory.Measure α}, f =ᵐ[μ] g → (AEMeasurable f μ ↔ AEMeasurable g μ)
-- Mathlib.Order.PropInstances
Prop.le_total : Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_add : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : AddGroup α] [ContinuousConstVAdd α α] {s t : Set α},
  interior s + interior t ⊆ interior (s + t)
-- Mathlib.Order.CountableSupClosed
/-- Every set generates a set closed under countable supremum.  -/
countableSupClosure : {α : Type u_2} → [Preorder α] → ClosureOperator (Set α)
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.hom_bijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C},
  Function.Bijective CategoryTheory.ConcreteCategory.hom
-- Mathlib.Data.Set.Basic
Set.mem_of_mem_inter_left : ∀ {α : Type u} {x : α} {a b : Set α}, x ∈ a ∩ b → x ∈ a
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- Generalization of `Finsupp.mul_prod_erase`: if `g` maps a second argument of 0 to 1,
then its product over `f : α →₀ M` is the same as multiplying the value on any element
`y : α` by the product over `erase y f`.  -/
Finsupp.mul_prod_erase' : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] (f : α →₀ M) (y : α)
  (g : α → M → N), (∀ (i : α), g i 0 = 1) → g y (f y) * (Finsupp.erase y f).prod g = f.prod g
-- Mathlib.Algebra.Group.Defs
CommMagma.toMul : {G : Type u} → [self : CommMagma G] → Mul G
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Postcomposition with a continuous linear map is a continuous linear map on Schwartz
functions.  -/
SchwartzMap.postcompCLM : {𝕜 : Type u_2} →
  {E : Type u_5} →
    {F : Type u_6} →
      {G : Type u_7} →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace ℝ E] →
            [inst_2 : NormedAddCommGroup F] →
              [inst_3 : NormedSpace ℝ F] →
                [inst_4 : RCLike 𝕜] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    [inst_6 : NormedAddCommGroup G] →
                      [inst_7 : NormedSpace ℝ G] →
                        [inst_8 : NormedSpace 𝕜 G] → (F →L[𝕜] G) → SchwartzMap E F →L[𝕜] SchwartzMap E G