mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.Iterators.Types.Zip.instIterator.match_3.splitter : {m : Type u_1 → Type u_2} →
  {α₁ β₁ : Type u_1} →
    [inst : Std.Iterator α₁ m β₁] →
      {α₂ β₂ : Type u_1} →
        [inst_1 : Std.Iterator α₂ m β₂] →
          (it : Std.IterM m (β₁ × β₂)) →
            (motive : it.internalState.right.Step → Sort u_3) →
              (x : it.internalState.right.Step) →
                ((it₂' : Std.IterM m β₂) →
                    (out₂ : β₂) →
                      (hp : it.internalState.right.IsPlausibleStep (Std.IterStep.yield it₂' out₂)) →
                        motive ⟨Std.IterStep.yield it₂' out₂, hp⟩) →
                  ((it₂' : Std.IterM m β₂) →
                      (hp : it.internalState.right.IsPlausibleStep (Std.IterStep.skip it₂')) →
                        motive ⟨Std.IterStep.skip it₂', hp⟩) →
                    ((hp : it.internalState.right.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩) →
                      motive x
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.isClosed_lattice : ∀ (L : PeriodPair), IsClosed ↑L.lattice
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instDecidableLE : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → DecidableLE (NonemptyInterval α)
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarAlgebra.elemental.star_self_mem : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] [inst_8 : TopologicalSpace A] [inst_9 : IsSemitopologicalSemiring A]
  [inst_10 : ContinuousConstSMul R A] [inst_11 : ContinuousStar A] (x : A), star x ∈ NonUnitalStarAlgebra.elemental R x
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
/-- Given a property `P` of objects for `F : Pseudofunctor B Cat` and
a `2`-morphism in `B`, this is the induced natural transformation between
the induced functors on the fullsubcategories of objects satisfying `P`.  -/
CategoryTheory.Pseudofunctor.ObjectProperty.map₂ : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} →
      (P : F.ObjectProperty) →
        [inst_1 : P.IsClosedUnderMapObj] → {X Y : B} → {f g : X ⟶ Y} → (f ⟶ g) → (P.map f ⟶ P.map g)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.star_apply : ∀ {n : Type u_3} {α : Type v} [inst : Star α] (M : Matrix n n α) (i j : n), star M i j = star (M j i)
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsBasis.isRkFinite_of_finite : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α}, M.IsBasis I X → I.Finite → M.IsRkFinite X
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal),
  ⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.equiv_symm_apply : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {f : M →ₗ[R] N} (h : IsBaseChange S f) (m : M),
  h.equiv.symm (f m) = 1 ⊗ₜ[R] m
-- Mathlib.Algebra.Ring.Parity
Nat.even_xor_odd' : ∀ (n : ℕ), ∃ k, Xor (n = 2 * k) (n = 2 * k + 1)
-- Mathlib.RingTheory.Regular.Flat
/-- Let `R` be a commutative ring, `M` be an `R`-module, `S` be a flat `R`-algebra, `N` be the base
change of `M` to `S`. If `[r₁, …, rₙ]` is a weakly regular `M`-sequence, then its image in `N` is
a weakly regular `N`-sequence.  -/
RingTheory.Sequence.IsWeaklyRegular.of_flat_of_isBaseChange : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] [Module.Flat R S] {f : M →ₗ[R] N},
  IsBaseChange S f →
    ∀ {rs : List R},
      RingTheory.Sequence.IsWeaklyRegular M rs → RingTheory.Sequence.IsWeaklyRegular N (List.map (⇑(algebraMap R S)) rs)
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int16.intCast_ofNat : ∀ (x : ℕ), ↑(OfNat.ofNat x) = OfNat.ofNat x
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.tensorTensorTensorComm_symm_tmul : ∀ {R : Type uR} {R' : Type u_1} {S : Type uS} {T : Type u_2} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD}
  [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A]
  [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B]
  [inst_9 : Semiring C] [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C]
  [inst_13 : Semiring D] [inst_14 : Algebra R D] [inst_15 : CommSemiring T] [inst_16 : Algebra R T]
  [inst_17 : Algebra T A] [inst_18 : IsScalarTower R T A] [inst_19 : SMulCommClass S T A] [inst_20 : Algebra S T]
  [inst_21 : IsScalarTower S T A] [inst_22 : CommSemiring R'] [inst_23 : Algebra R R'] [inst_24 : Algebra R' T]
  [inst_25 : Algebra R' A] [inst_26 : Algebra R' B] [inst_27 : IsScalarTower R R' A] [inst_28 : SMulCommClass S R' A]
  [inst_29 : SMulCommClass R' S A] [inst_30 : IsScalarTower R' T A] [inst_31 : IsScalarTower R R' B] (m : A) (n : C)
  (p : B) (q : D),
  (Algebra.TensorProduct.tensorTensorTensorComm R R' S T A B C D).symm (m ⊗ₜ[S] n ⊗ₜ[R'] (p ⊗ₜ[R] q)) =
    m ⊗ₜ[R'] p ⊗ₜ[S] (n ⊗ₜ[R] q)
-- Mathlib.Data.Set.MemPartition
memPartitionSet_zero : ∀ {α : Type u_1} (f : ℕ → Set α) (a : α), memPartitionSet f 0 a = Set.univ
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- A variant of `isConjRoot_of_algEquiv`.
Let `s` be an `R`-algebra isomorphism. Then `x` is a conjugate root of `s x`.
 -/
isConjRoot_of_algEquiv' : ∀ {R : Type u_1} {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (x : A) (s : A ≃ₐ[R] A),
  IsConjRoot R (s x) x
-- Std.Time.Date.Unit.Day
/-- Creates an ordinal from a natural number, ensuring the number is within the valid range
for days of a month (1 to 31).
 -/
Std.Time.Day.Ordinal.ofNat : (data : ℕ) → autoParam (data ≥ 1 ∧ data ≤ 31) Std.Time.Day.Ordinal.ofNat._auto_1 → Std.Time.Day.Ordinal
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_int8ToInt : ∀ (x : Int8), Int64.ofIntLE x.toInt ⋯ ⋯ = x.toInt64
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.exists_insert_of_ssubset : ∀ {α : Type u_1} {M : Matroid α} {B B' I : Set α}, M.IsBase B → I ⊂ B → M.IsBase B' → ∃ e ∈ B' \ I, M.Indep (insert e I)
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.Context.mctx₂ : Aesop.EqualUpToIdsM.Context → Lean.MetavarContext
-- Init.Data.Rat.Lemmas
Rat.div_lt_iff : ∀ {a b c : ℚ}, 0 < b → (a / b < c ↔ a < c * b)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.η_comp_isoPointwiseLeftKanExtension_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  (F G : CategoryTheory.MonoidalCategory.DayFunctor C V) (x y : C),
  CategoryTheory.CategoryStruct.comp ((F.η G).app (x, y))
      ((F.isoPointwiseLeftKanExtension G).hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
    CategoryTheory.Limits.colimit.ι
      ((CategoryTheory.CostructuredArrow.proj (CategoryTheory.MonoidalCategory.tensor C)
            (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)).comp
        (CategoryTheory.MonoidalCategory.externalProduct F.functor G.functor))
      (CategoryTheory.CostructuredArrow.mk
        (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)))
-- Mathlib.Data.List.Sort
/-- The list obtained from an antitone tuple is sorted.  -/
Antitone.sortedGE_ofFn : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin n → α}, Antitone f → (List.ofFn f).SortedGE
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_inf : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I J : FractionalIdeal S P), ↑(I ⊓ J) = ↑I ⊓ ↑J
-- Mathlib.Topology.Homotopy.Product
Path.Homotopic.pi.eq_1 : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {as bs : (i : ι) → X i}
  (γ : (i : ι) → Path.Homotopic.Quotient (as i) (bs i)),
  Path.Homotopic.pi γ = Quotient.map Path.pi ⋯ (Quotient.choice γ)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.subsemigroupComap_apply_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (N' : AddSubsemigroup N)
  (x : ↥(AddSubsemigroup.comap f N')), ↑((f.subsemigroupComap N') x) = f ↑x
-- Mathlib.NumberTheory.Padics.Complex
/-- `PadicAlgCl p` is a fixed algebraic closure of `ℚ_[p]`.  -/
PadicAlgCl : (p : ℕ) → [hp : Fact (Nat.Prime p)] → Type
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.ShouldCanonResult.canonImplicit.sizeOf_spec : sizeOf Lean.Meta.Sym.Canon.ShouldCanonResult.canonImplicit✝ = 1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toArray.eq_1 : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α] (r : Std.Roo α),
  r.toArray = (Std.Roo.Internal.iter r).toArray
-- Mathlib.Probability.CDF
/-- If two real probability distributions have the same cdf, they are equal.  -/
MeasureTheory.Measure.eq_of_cdf : ∀ (μ ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν],
  ProbabilityTheory.cdf μ = ProbabilityTheory.cdf ν → μ = ν
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- the induced map on cycles  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.φK : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.LeftHomologyData} →
            {h₂ : S₂.LeftHomologyData} → CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂ → (h₁.K ⟶ h₂.K)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndepOn.subset_span_extend : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s t : Set V}
  (hs : LinearIndepOn K id s) (hst : s ⊆ t), t ⊆ ↑(Submodule.span K (hs.extend hst))
-- Mathlib.Topology.Order.LeftRightLim
rightLim_eq_of_eq_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] (f : α → β) {a : α}, nhdsWithin a (Set.Ioi a) = ⊥ → Function.rightLim f a = f a
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.edges_toPath_subset_edges : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), (↑p.toPath).edges ⊆ p.edges
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiable.cle_arrowCongr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_17}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄},
  (MDiff fun x => ↑(f x).symm) → (MDiff fun x => ↑(g x)) → MDiff fun y => ↑((f y).arrowCongr (g y))
-- Mathlib.Order.Hom.Set
compl_antitone : ∀ (α : Type u_1) [inst : BooleanAlgebra α], Antitone compl
-- Std.Time.Zoned.Database.Basic
/-- A timezone database from which we can read the `ZoneRules` of some area by it's id.
 -/
Std.Time.Database : Type → Type
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffWithinAt.vadd : ∀ {𝕜 : 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} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {H'' : Type u_6} [inst_7 : TopologicalSpace H''] {E'' : Type u_7}
  [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {I'' : ModelWithCorners 𝕜 E'' H''} {G : Type u_8}
  [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H G] {M : Type u_9} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace H'' N]
  [inst_16 : VAdd G M] {n : WithTop ℕ∞} [ContMDiffVAdd I I' n G M] {f : N → G} {g : N → M} {s : Set N} {x : N},
  ContMDiffWithinAt I'' I n f s x → ContMDiffWithinAt I'' I' n g s x → ContMDiffWithinAt I'' I' n (f +ᵥ g) s x
-- Std.Do.SPred.SVal
Std.Do.SVal.instInhabited : {α : Type u_1} → {σs : List (Type u_1)} → [Inhabited α] → Inhabited (Std.Do.SVal σs α)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.eval_map : ∀ {ι : Type u_1} (V : Type u) [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (c : ComplexShape ι) (i : ι) {X Y : HomologicalComplex V c}
  (f : X ⟶ Y), (HomologicalComplex.eval V c i).map f = f.f i
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopObjFunctorTypeIsSheafGrothendieckTopologyStructureSheafInType : {R A : Type u} →
  [inst : CommRing R] →
    [inst_1 : CommRing A] →
      [inst_2 : Algebra R A] →
        (U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ) →
          Algebra R ((AlgebraicGeometry.structureSheafInType R A).obj.obj U)
-- Init.Grind.Module.Basic
/-- Addition is right-cancellative.  -/
Lean.Grind.AddRightCancel.add_right_cancel : ∀ {M : Type u} {inst : Add M} [self : Lean.Grind.AddRightCancel M] (a b c : M), a + c = b + c → a = b
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instHasFrameAndPure : ∀ {φ : Prop} (σs : List (Type u_1)) (P : Std.Do.SPred σs), Std.Do.SPred.Tactic.HasFrame spred(⌜φ⌝ ∧ P) P φ
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- A continuous linear map can be regarded as a continuous affine map.  -/
ContinuousLinearMap.toContinuousAffineMap : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module R V] →
            [inst_3 : TopologicalSpace V] →
              [inst_4 : AddCommGroup W] →
                [inst_5 : Module R W] → [inst_6 : TopologicalSpace W] → (V →L[R] W) → V →ᴬ[R] W
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.left_distrib : ∀ {n : ℕ} (a b c : Fin n), a * (b + c) = a * b + a * c
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.cos_le_one_sub_mul_cos_sq : ∀ {x : ℝ}, |x| ≤ Real.pi → Real.cos x ≤ 1 - 2 / Real.pi ^ 2 * x ^ 2
-- Aesop.Index.Basic
Aesop.IndexMatchLocation.target.sizeOf_spec : sizeOf Aesop.IndexMatchLocation.target = 1
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_one_div_add_atTop_nhds_zero_nat : ∀ {𝕜 : Type u_4} [inst : DivisionSemiring 𝕜] [inst_1 : CharZero 𝕜] [inst_2 : TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜],
  Filter.Tendsto (fun n => 1 / (↑n + 1)) Filter.atTop (nhds 0)
-- Mathlib.Order.CompleteLattice.Basic
Pi.infSet : {α : Type u_8} → {β : α → Type u_9} → [(i : α) → InfSet (β i)] → InfSet ((i : α) → β i)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.TriangleMorphism.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.HasShift C ℤ}
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} {x y : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂},
  x.hom₁ = y.hom₁ → x.hom₂ = y.hom₂ → x.hom₃ = y.hom₃ → x = y
-- Std.Time.DateTime.WallTime
/-- Subtracts an `Hour.Offset` from the given `WallTime`.
 -/
Std.Time.WallTime.subHours : Std.Time.WallTime → Std.Time.Hour.Offset → Std.Time.WallTime
-- Lean.Meta.LetToHave
/-- Visits lambdas, lets, and haves.

Enters the entire telescope at once.
We do not check the cache at each step of the telescope since we assume that there are no unused variables.
 -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitLambdaLet : Lean.Expr → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Init.Data.String.Lemmas.Splits
/-- Given a slice `s` such that `s.copy = t₁ ++ t₂`, obtain the position sitting between `t₁` and `t₂`.
 -/
String.Slice.Pos.ofEqAppend : {s : String.Slice} → {t₁ t₂ : String} → s.copy = t₁ ++ t₂ → s.Pos
-- Mathlib.Order.Monotone.Defs
Function.update_mono : ∀ {ι : Type u_1} {π : ι → Type u_3} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)] {f : (i : ι) → π i}
  {i : ι}, Monotone (Function.update f i)
-- Mathlib.Algebra.Regular.Opposite
isRightRegular_unop : ∀ {R : Type u_1} [inst : Mul R] {a : Rᵐᵒᵖ}, IsRightRegular (MulOpposite.unop a) ↔ IsLeftRegular a
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMonFunctor_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (D : Type u₂) [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.LaxBraidedFunctor C D), (CategoryTheory.Functor.mapCommMonFunctor C D).obj F = F.mapCommMon
-- Std.Http.Data.Headers.Value
/-- The proof that it's a valid header value.
 -/
Std.Http.Header.Value.isValidHeaderValue : ∀ (self : Std.Http.Header.Value), Std.Http.Header.IsValidHeaderValue self.value
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F :
        CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
          (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} → CategoryTheory.Category.{max t v', max (max u' v') t} (F.DescentDataAsCoalgebra f)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_keys : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.keys.isEmpty = m.isEmpty
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceₘ.match_3.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      ¬r.size > Std.DTreeMap.Internal.delta * l.size → l.size > Std.DTreeMap.Internal.delta * r.size → Sort u_3)
  (l : Std.DTreeMap.Internal.Impl α β) (h : ¬r.size > Std.DTreeMap.Internal.delta * l.size)
  (h_1 : l.size > Std.DTreeMap.Internal.delta * r.size)
  (h_1_1 :
    (h : ¬r.size > Std.DTreeMap.Internal.delta * Std.DTreeMap.Internal.Impl.leaf.size) →
      (h_2 : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * r.size) →
        motive Std.DTreeMap.Internal.Impl.leaf h h_2)
  (h_2 :
    (size : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) →
            (h : ¬r.size > Std.DTreeMap.Internal.delta * (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size) →
              (h_2 : (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size > Std.DTreeMap.Internal.delta * r.size) →
                motive (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr) h h_2)
  (h_3 : ¬r.size > Std.DTreeMap.Internal.delta * Std.DTreeMap.Internal.Impl.leaf.size)
  (h_4 : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * r.size),
  l = Std.DTreeMap.Internal.Impl.leaf →
    h ≍ h_3 →
      h_1 ≍ h_4 →
        (match l, h, h_1 with
          | Std.DTreeMap.Internal.Impl.leaf, h, h_5 => h_1_1 h h_5
          | Std.DTreeMap.Internal.Impl.inner size lk lv ll lr, h, h_5 => h_2 size lk lv ll lr h h_5) ≍
          h_1_1 h_3 h_4
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.inverse.eq_1 : ∀ {M : Type u_2} {X : Type u_5} [inst : VAdd M X] {Y₁ : Type u_8} [inst_1 : VAdd M Y₁] (f : X →ₑ[id] Y₁) (g : Y₁ → X)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f), f.inverse g h₁ h₂ = { toFun := g, map_vadd' := ⋯ }
-- Mathlib.LinearAlgebra.Pi
LinearMap.compLeft_apply : ∀ {R : Type u} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₃] (f : M₂ →ₗ[R] M₃) (I : Type u_1) (h : I → M₂) (a : I),
  (f.compLeft I) h a = (⇑f ∘ h) a
-- Mathlib.Topology.Algebra.Indicator
ContinuousOn.continuousAt_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  [inst_2 : Zero β], ContinuousOn f (interior s) → ∀ {x : α}, x ∉ frontier s → ContinuousAt (s.indicator f) x
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_eq_zero_iff : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R}, ⌈a⌉ = 0 ↔ a ∈ Set.Ioc (-1) 0
-- Mathlib.Order.Bounds.Lattice
GaloisConnection.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (l : α → β) (u : β → α),
  GaloisConnection l u = ∀ (a : α) (b : β), l a ≤ b ↔ a ≤ u b
-- Mathlib.Algebra.Order.Group.Basic
/-- A nontrivial densely linear ordered additive commutative group can't be a cyclic group.  -/
not_isAddCyclic_of_denselyOrdered : ∀ (α : Type u_1) [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [DenselyOrdered α]
  [Nontrivial α], ¬IsAddCyclic α