mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- The reverse direction of `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`, since
`MeasurePreserving.symm` only works for `MeasurableEquiv`s.  -/
PiLp.volume_preserving_toLp : ∀ (ι : Type u_4) [inst : Fintype ι],
  MeasureTheory.MeasurePreserving (WithLp.toLp 2) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- Differentiability of `Θ z τ` in `z`, for fixed `τ`.  -/
differentiableAt_jacobiTheta₂_fst : ∀ (z : ℂ) {τ : ℂ}, 0 < τ.im → DifferentiableAt ℂ (fun x => jacobiTheta₂ x τ) z
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Given a functor `F` and an equivalence of categories `e` such that `e.functor` and `e.inverse ⋙ F`
are monoidal functors, `F` is monoidal as well.
 -/
CategoryTheory.Equivalence.monoidalOfPrecompInverse : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (e : C ≌ D) →
                    (F : CategoryTheory.Functor C E) →
                      {F' : CategoryTheory.Functor D E} →
                        (e.inverse.comp F ≅ F') → [e.functor.Monoidal] → [F'.Monoidal] → F.Monoidal
-- Mathlib.Topology.Constructions.SumProd
/-- Postcomposing `f` with `Prod.snd` is continuous  -/
Continuous.snd : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y × Z}, Continuous f → Continuous fun x => (f x).2
-- Mathlib.Condensed.Discrete.Module
/-- `LightCondMod.LocallyConstant.functor` is fully faithful.
 -/
LightCondMod.LocallyConstant.fullyFaithfulFunctor : (R : Type u) → [inst : Ring R] → (LightCondMod.LocallyConstant.functor R).FullyFaithful
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
/-- A finite product of functions nonnegative and antitone on `u` is antitone on `u`. See also
`AntitoneOn.finsetProd'` for the case of an ordered commutative multiplicative monoid.  -/
AntitoneOn.finsetProd : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {s : Finset ι} {γ : Type u_4} [inst_4 : Preorder γ] {u : Set γ} {f : ι → γ → R},
  (∀ i ∈ s, AntitoneOn (f i) u) → (∀ i ∈ s, ∀ x ∈ u, 0 ≤ f i x) → AntitoneOn (fun x => ∏ i ∈ s, f i x) u
-- Mathlib.Algebra.Category.MonCat.Basic
/-- additive equivalences between `AddCommMonoid`s are
the same as (isomorphic to) isomorphisms in `AddCommMonCat`  -/
addEquivIsoAddCommMonCatIso : {X Y : Type u} →
  [inst : AddCommMonoid X] → [inst_1 : AddCommMonoid Y] → X ≃+ Y ≅ AddCommMonCat.of X ≅ AddCommMonCat.of Y
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAt.scomp_hasDerivWithinAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F}
  {g₁' : F} {y : 𝕜'},
  HasDerivAt g₁ g₁' y → HasDerivWithinAt h h' s x → y = h x → HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₁.d₁₂_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (x : ↥(groupCohomology.cocycles₁ A)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.d₁₂ A)) ⇑x = 0
-- Mathlib.Tactic.DefEqTransformations
/-- `beta_reduce at loc` completely beta reduces the given location.
This also exists as a `conv`-mode tactic.

This means that whenever there is an applied lambda expression such as
`(fun x => f x) y` then the argument is substituted into the lambda expression
yielding an expression such as `f y`.
 -/
Mathlib.Tactic.convBeta_reduce : Lean.ParserDescr
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m β] →
      {it : Std.IterM m β} →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Lean.Data.AssocList
Lean.AssocList.replace : {α : Type u} → {β : Type v} → [BEq α] → α → β → Lean.AssocList α β → Lean.AssocList α β
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.pullbackObjIso_inv_comp_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D)
  {Z : C} (h : F.obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackObjIso f g d).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pullback.fst f g).app d) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f.app d) (g.app d)) h
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_hom_hom_inv_hom_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i)
      (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom
-- Mathlib.Algebra.Group.Basic
sub_eq_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a - b = 0 ↔ a = b
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_apply : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : (i : o) → Matrix (m' i) (n' i) α) (ik : (i : o) × m' i) (jk : (i : o) × n' i),
  Matrix.blockDiagonal' M ik jk = if h : ik.fst = jk.fst then M ik.fst ik.snd (cast ⋯ jk.snd) else 0
-- Mathlib.Algebra.Order.Hom.Basic
map_neg_add : ∀ {F : Type u_2} {β : Type u_4} [inst : AddCommMonoid β] [inst_1 : PartialOrder β] (f : F) {α : Type u_7}
  [inst_2 : FunLike F α β] [inst_3 : AddCommGroup α] [AddGroupSeminormClass F α β] (x y : α), f (-x + y) = f (x + -y)
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sumZeroHom.eq_1 : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : AddCommMonoid γ] (φ : (i : ι) → ZeroHom (β i) γ),
  DFinsupp.sumZeroHom φ =
    { toFun := fun f => (fun c => Trunc.lift (fun s => ∑ i ∈ (↑s).toFinset, (φ i) (f i)) c f.support') ⋯,
      map_zero' := ⋯ }
-- Lean.Elab.PreDefinition.TerminationMeasure
/-- A complete set of `TerminationMeasure`s, as applicable to a single clique.   -/
Lean.Elab.TerminationMeasures : Type
-- Mathlib.Data.Nat.Digits.Defs
Nat.digitsAux.congr_simp : ∀ (b b_1 : ℕ) (e_b : b = b_1) (h : 2 ≤ b) (a a_1 : ℕ), a = a_1 → b.digitsAux h a = b_1.digitsAux ⋯ a_1
-- Mathlib.Topology.Homeomorph.Lemmas
Topology.IsEmbedding.homeomorphOfSubsetRange_apply_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : Topology.IsEmbedding f) {s : Set Y} (hs : s ⊆ Set.range f) (x : ↑(f ⁻¹' s)),
  ↑((hf.homeomorphOfSubsetRange hs) x) = f ↑x
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vaddAssocClass : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α β] [inst_1 : VAdd α γ] [inst_2 : VAdd β γ]
  [VAddAssocClass α β γ], VAddAssocClass α β (Set γ)
-- Batteries.Data.Vector.Lemmas
Vector.toList_scanl : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {init : β} {f : β → α → β} {as : Vector α n},
  (Vector.scanl f init as).toList = List.scanl f init as.toList
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanImport : Lean.FromJson Lean.Lsp.LeanImport
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.toCoalgHom_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B], Function.Injective CoalgEquiv.toCoalgHom
-- Mathlib.Order.Filter.Partial
Filter.rmap_sets : ∀ {α : Type u} {β : Type v} (r : SetRel α β) (l : Filter α), (Filter.rmap r l).sets = r.core ⁻¹' l.sets
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_eq_getValueCast : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((_ : α) × β)} {a : α}
  {h : Std.Internal.List.containsKey a l = true},
  Std.Internal.List.getValue a l h = Std.Internal.List.getValueCast a l h
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_assoc : ∀ {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) {Z : CategoryTheory.Functor ↑X ↑Y} (h : G.toFunctor ⟶ Z),
  CategoryTheory.CategoryStruct.comp e.inv.toNatTrans (CategoryTheory.CategoryStruct.comp e.hom.toNatTrans h) = h
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Set.add_addSubgroupClosure : ∀ {G : Type u_2} [inst : AddGroup G] {s : Set G}, s.Nonempty → s + ↑(AddSubgroup.closure s) = ↑(AddSubgroup.closure s)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ico₀ : ∀ {G₀ : Type u_2} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {c : G₀} (a b : G₀),
  0 < c → (fun x => c * x) ⁻¹' Set.Ico a b = Set.Ico (a / c) (b / c)
-- Mathlib.CategoryTheory.Monoidal.Category
/-- We state it as a simp lemma, which is regarded as an involved version of
`id_whiskerRight X Y : 𝟙 X ▷ Y = 𝟙 (X ⊗ Y)`.
 -/
CategoryTheory.MonoidalCategory.leftUnitor_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom Y =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).hom
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- distinguished triangles in a pretriangulated category  -/
CategoryTheory.Pretriangulated.termDistTriang_ : Lean.ParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
PresheafOfModules.instAdditiveRestrictScalars : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R ⟶ R'),
  (PresheafOfModules.restrictScalars α).Additive
-- Std.Time.Zoned.ZoneRules
/-- Finds the index of the transition in effect at a given timestamp in `Array Transition`.
Returns the index of the most recent transition that started at or before the timestamp,
or `none` if the timestamp precedes all transitions.
 -/
Std.Time.TimeZone.Transition.findTransitionIndexForTimestamp : Array Std.Time.TimeZone.Transition → Std.Time.Timestamp → Option ℕ
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearEquiv.multilinearMapCongrRight_symm_apply : ∀ {R : Type uR} (S : Type uS) {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₂] [inst_7 : SMulCommClass R S M₂]
  [inst_8 : AddCommMonoid M₃] [inst_9 : Module S M₃] [inst_10 : Module R M₃] [inst_11 : SMulCommClass R S M₃]
  [inst_12 : LinearMap.CompatibleSMul M₂ M₃ S R] [inst_13 : LinearMap.CompatibleSMul M₃ M₂ S R] (g : M₂ ≃ₗ[R] M₃)
  (a : MultilinearMap R M₁ M₃), (LinearEquiv.multilinearMapCongrRight S g).symm a = (↑g.symm).compMultilinearMap a
-- Mathlib.Order.Interval.Finset.Nat
Nat.card_Iic : ∀ (b : ℕ), (Finset.Iic b).card = b + 1
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_pow : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] (n : ℕ) (x : R),
  ArchimedeanClass.mk (x ^ n) = n • ArchimedeanClass.mk x
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.toMonoid.unique : ∀ {α : Type u_3} {M : Type u_4} [inst : Monoid M] (f : α → M) {rels : FreeMonoid α → FreeMonoid α → Prop}
  (h : ∀ (a b : FreeMonoid α), rels a b → (FreeMonoid.lift f) a = (FreeMonoid.lift f) b)
  (g : (conGen rels).Quotient →* M), (∀ (a : α), g (PresentedMonoid.of rels a) = f a) → g = PresentedMonoid.lift f h
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_comp_tensorHom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ⟶ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z_1 : C} (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj W Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f h) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.comp g h)) h_1
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.AbsolutelyContinuous.prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ μ' : MeasureTheory.Measure α}
  {ν ν' : MeasureTheory.Measure β} [MeasureTheory.SFinite ν'],
  μ.AbsolutelyContinuous μ' → ν.AbsolutelyContinuous ν' → (μ.prod ν).AbsolutelyContinuous (μ'.prod ν')
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.toWeakDual_toStrongDual : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  (x : WeakDual 𝕜 E), StrongDual.toWeakDual (WeakDual.toStrongDual x) = x
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
Measurable.ennreal_log : ∀ {α : Type u_1} {x : MeasurableSpace α} {f : α → ENNReal}, Measurable f → Measurable fun x => (f x).log
-- Mathlib.Computability.ContextFreeGrammar
/-- Add extra postfix to context-free producing.  -/
ContextFreeGrammar.Produces.append_right : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)},
  g.Produces v w → ∀ (p : List (Symbol T g.NT)), g.Produces (v ++ p) (w ++ p)
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.map_unique : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{vβ, uβ} β) {f : α → β} {g : pkg.space → pkg'.space},
  UniformContinuous g → (∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)) → pkg.map pkg' f = g
-- Mathlib.Order.BoundedOrder.Lattice
inf_eq_top_iff : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {a b : α}, a ⊓ b = ⊤ ↔ a = ⊤ ∧ b = ⊤
-- Mathlib.Algebra.Quotient
HasQuotient.mk : {A : outParam (Type u)} → {B : Type v} → (B → Type (max u v)) → HasQuotient A B
-- Mathlib.GroupTheory.ArchimedeanDensely
Subgroup.isLeast_of_closure_iff_eq_mabs : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a b : G},
  IsLeast {y | y ∈ Subgroup.closure {a} ∧ 1 < y} b ↔ b = |a|ₘ ∧ 1 < b
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
AffineIndependent.card_le_finrank_succ : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] {p : ι → P},
  AffineIndependent k p → Fintype.card ι ≤ Module.finrank k ↥(vectorSpan k (Set.range p)) + 1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.ext_getVert_le_length : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v},
  p.length = q.length → (∀ k ≤ p.length, p.getVert k = q.getVert k) → p = q
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.instHasInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Limits.HasInitial (CategoryTheory.AddMon C)
-- Mathlib.Algebra.Order.Group.Defs
exists_one_lt' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] [Nontrivial α], ∃ a, 1 < a
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instCoeSortType : {k : Type u} → {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → CoeSort (Rep.{w, u, v} k G) (Type w)
-- Mathlib.Control.Bitraversable.Basic
LawfulBitraversable.id_bitraverse : ∀ {t : Type u → Type u → Type u} {inst : Bitraversable t} [self : LawfulBitraversable t] {α β : Type u} (x : t α β),
  bitraverse pure pure x = pure x
-- Lean.Parser.Term
Lean.Parser.Term.matchExprAlts.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.Ring.Limits
/-- We show that the forgetful functor `CommRingCat ⥤ RingCat` creates limits.

All we need to do is notice that the limit point has a `CommRing` instance available,
and then reuse the existing limit.
 -/
CommRingCat.instCreatesLimitRingCatForget₂RingHomCarrierCarrier : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommRingCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] →
        CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommRingCat RingCat)
-- Init.Data.UInt.Basic
/-- Bitwise left shift for 8-bit unsigned integers. Usually accessed via the `<<<` operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.shiftLeft : UInt8 → UInt8 → UInt8
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  (t₁ ∪ t₂).getKeyD k fallback = t₂.getKeyD k (t₁.getKeyD k fallback)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMap.eq_2 : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Zipper α β) (size : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Zipper.prependMap (Std.DTreeMap.Internal.Impl.inner size k v l r) x =
    Std.DTreeMap.Internal.Zipper.prependMap l (Std.DTreeMap.Internal.Zipper.cons k v r x)
-- Init.Core
/-- If `a → b` and `b → a` then `a` and `b` are equivalent.  -/
Iff.intro : ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.toAddSubgroup_injective : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], Function.Injective NonUnitalSubring.toAddSubgroup
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.instIsMarkovKernelId : ∀ {α : Type u_1} {mα : MeasurableSpace α}, ProbabilityTheory.IsMarkovKernel ProbabilityTheory.Kernel.id
-- Mathlib.MeasureTheory.Measure.Map
/-- We can evaluate the pushforward on measurable sets. For non-measurable sets, see
`MeasureTheory.Measure.le_map_apply` and `MeasurableEquiv.map_apply`.  -/
MeasureTheory.Measure.map_apply_of_aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β}, AEMeasurable f μ → ∀ {s : Set β}, MeasurableSet s → (MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
-- Mathlib.Algebra.Order.Group.Action.End
RelEmbedding.smul_def : ∀ {α : Type u_1} {r : α → α → Prop} (f : r ↪r r) (a : α), f • a = f a
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.multifork_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.Functor Cᵒᵖ A) (i : E.I₀),
  (E.multifork F).ι i = F.map (E.f i).op
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toStructuredArrow_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.Cocone.toStructuredArrow F).obj c = CategoryTheory.StructuredArrow.mk c.ι
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalStarRing.hom_ext_iff : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : (i : ι) → StarRing (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [inst_8 : Nonempty ι] {P : Type u_7}
  [inst_9 : NonUnitalNonAssocSemiring P] [inst_10 : StarRing P] {g₁ g₂ : DirectLimit G f →⋆ₙ+* P},
  g₁ = g₂ ↔
    ∀ (i : ι), g₁.comp (DirectLimit.NonUnitalStarRing.of G f i) = g₂.comp (DirectLimit.NonUnitalStarRing.of G f i)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.coe_toEmbedding : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), ⇑f.toEmbedding = ⇑f
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.instBEqUnpackedFloat : BEq Float.Model.UnpackedFloat
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_pow : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (n : ℕ), (x ^ n).fst = x.fst ^ n
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.self_trans_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N), e.trans e.symm = ContinuousMulEquiv.refl M
-- Init.ShareCommon
ShareCommon.StateFactoryBuilder.mapInsert : (self : ShareCommon.StateFactoryBuilder) →
  {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → self.Map α β → α → β → self.Map α β
-- Mathlib.Algebra.Order.Floor.Ring
Int.lt_floor_add_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (a : R), a < ↑⌊a⌋ + 1
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.toPrefunctor.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D),
  F.toPrefunctor = { obj := F.obj, map := @CategoryTheory.Functor.map C inst D inst_1 F }
-- Mathlib.GroupTheory.GroupAction.Quotient
_private.Mathlib.GroupTheory.GroupAction.Quotient.0.MulAction.termΩ : Lean.ParserDescr
-- Mathlib.Data.Seq.Basic
Stream'.Seq.fold_cons : ∀ {α : Type u} {β : Type v} (init : β) (f : β → α → β) (x : α) (s : Stream'.Seq α),
  (Stream'.Seq.cons x s).fold init f = Stream'.Seq.cons init (s.fold (f init x) f)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_map : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] {L : BooleanSubalgebra α}
  {f : BoundedLatticeHom α β} {b : β}, b ∈ BooleanSubalgebra.map f L ↔ ∃ a ∈ L, f a = b