mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.centerToMulOpposite_apply_coe : ∀ (G : Type u_1) [inst : Group G] (r : ↥(Subsemigroup.center G)),
  ↑((Subgroup.centerToMulOpposite G) r) = MulOpposite.op ↑r
-- Mathlib.RingTheory.Jacobson.Semiprimary
IsSemiprimaryRing.isSemisimpleRing : ∀ {R : Type u_1} {inst : Ring R} [self : IsSemiprimaryRing R], IsSemisimpleRing (R ⧸ Ring.jacobson R)
-- Lean.MetavarContext
Lean.instInhabitedLocalInstance : Inhabited Lean.LocalInstance
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Measure.setLIntegral_condKernel_univ_right : ∀ {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (β × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ]
  {f : β × Ω → ENNReal},
  Measurable f →
    ∀ {s : Set β},
      MeasurableSet s →
        ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ
-- Mathlib.RingTheory.Ideal.Maps
Ideal.instIsTwoSidedComap : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  {K : Ideal S} [inst_3 : RingHomClass F R S] [K.IsTwoSided], (Ideal.comap f K).IsTwoSided
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instMulZeroClassOfContinuousMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : MulZeroClass β] → [ContinuousMul β] → MulZeroClass C(α, β)
-- Std.Data.HashMap.Raw
/-- Two hash maps are equivalent in the sense of `Equiv` iff
all the keys and values are equal.
 -/
Std.HashMap.Raw.«term_~m_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.inclusion_trans : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {R S T : CategoryTheory.Subgroupoid C} (k : R ≤ S) (h : S ≤ T),
  CategoryTheory.Subgroupoid.inclusion ⋯ =
    (CategoryTheory.Subgroupoid.inclusion k).comp (CategoryTheory.Subgroupoid.inclusion h)
-- Mathlib.Geometry.Euclidean.MongePoint
Affine.Simplex.mongePoint.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n),
  s.mongePoint = (↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ Finset.univ s.points -ᵥ s.circumcenter) +ᵥ s.circumcenter
-- Mathlib.Topology.Path
Path.extend_of_le_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) {t : ℝ}, t ≤ 0 → γ.extend t = a
-- Mathlib.Algebra.Group.Action.Hom
MonoidHom.smulOneHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : MulOneClass N] [inst_2 : MulAction M N]
  [inst_3 : IsScalarTower M N N], MonoidHom.smulOneHom = { toFun := fun x => x • 1, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_mul_le_one_of_le₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b : G₀}
  [ZeroLEOneClass G₀], a ≤ b → 0 ≤ b → b⁻¹ * a ≤ 1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ext_getKey?_unit : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {t₁ t₂ : Std.ExtTreeMap α Unit cmp},
  (∀ (k : α), t₁.getKey? k = t₂.getKey? k) → t₁ = t₂
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Presieve.CoverByImageStructure.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {G : CategoryTheory.Functor C D} {V U : D} {f : V ⟶ U} {obj : C}
  {lift : V ⟶ G.obj obj} {map : G.obj obj ⟶ U}
  {fac :
    autoParam (CategoryTheory.CategoryStruct.comp lift map = f)
      CategoryTheory.Presieve.CoverByImageStructure.fac._autoParam}
  {obj_1 : C} {lift_1 : V ⟶ G.obj obj_1} {map_1 : G.obj obj_1 ⟶ U}
  {fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp lift_1 map_1 = f)
      CategoryTheory.Presieve.CoverByImageStructure.fac._autoParam},
  { obj := obj, lift := lift, map := map, fac := fac } = { obj := obj_1, lift := lift_1, map := map_1, fac := fac_1 } →
    obj = obj_1 ∧ lift ≍ lift_1 ∧ map ≍ map_1
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto μs F (nhds μ) ↔
    ∀ (f : BoundedContinuousFunction Ω NNReal),
      Filter.Tendsto (fun i => (μs i).testAgainstNN f) F (nhds (μ.testAgainstNN f))
-- Mathlib.Lean.LocalContext
/-- Return the result of `f` on the last local declaration on which `f` succeeds.  -/
Lean.LocalContext.lastDeclM : {m : Type u → Type v} → [AlternativeMonad m] → {β : Type u} → Lean.LocalContext → (Lean.LocalDecl → m β) → m β
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffAt.clm_comp : ∀ {𝕜 : 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_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃}
  {f : M → F₂ →L[𝕜] F₁} {x : M},
  ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g x →
    ContMDiffAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n f x →
      ContMDiffAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n (fun x => g x ∘SL f x) x
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
/-- The final auxiliary construction for `CliffordAlgebra.even.lift`. This map is the forwards
direction of that equivalence, but not in the fully-bundled form.  -/
CliffordAlgebra.even.lift.aux : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {Q : QuadraticForm R M} →
            {A : Type u_3} →
              [inst_3 : Ring A] →
                [inst_4 : Algebra R A] → CliffordAlgebra.EvenHom Q A → ↥(CliffordAlgebra.even Q) →ₗ[R] A
-- Init.Data.Order.Lemmas
Std.instAntisymmLeOfIsPartialOrder : ∀ {α : Type u} [inst : LE α] [Std.IsPartialOrder α], Std.Antisymm fun x1 x2 => x1 ≤ x2
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonReferenceParams.fromJson : Lean.Json → Except String Lean.Lsp.ReferenceParams
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivary_inv_left`. -/
Monovary.inv_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Monovary f g → Antivary f⁻¹ g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] {l : List α}
  {k k' : α},
  cmp k k' = Ordering.eq →
    k ∉ t →
      List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
        k ∈ l → (Std.DTreeMap.Const.insertManyIfNewUnit t l).getKey? k' = some k
-- Mathlib.Algebra.Group.Action.Opposite
op_smul_mul : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid α] [inst_1 : MulAction αᵐᵒᵖ β] (b : β) (a₁ a₂ : α),
  MulOpposite.op (a₁ * a₂) • b = MulOpposite.op a₂ • MulOpposite.op a₁ • b
-- Mathlib.LinearAlgebra.Dual.Defs
/-- A direct summand of a reflexive module is reflexive.  -/
Module.IsReflexive.of_split : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] [Module.IsReflexive R M] (i : N →ₗ[R] M)
  (s : M →ₗ[R] N), s ∘ₗ i = LinearMap.id → Module.IsReflexive R N
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.scMap_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i : ℕ)
  (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.scMap._auto_1),
  (CategoryTheory.ComposableArrows.scMap φ h₁ h₂ i hi).τ₂ = φ.app ⟨i + 1, ⋯⟩
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
associatedPrimes.nonempty : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [IsNoetherianRing R] [Nontrivial M], (associatedPrimes R M).Nonempty
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- A monotone map between preorders spaces induces a continuous map between themselves considered
with the upper set topology.  -/
Topology.WithUpperSet.map : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → C(Topology.WithUpperSet α, Topology.WithUpperSet β)
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.map_mk_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : M), Filter.map (⇑DomMulAct.mk) (nhds x) = nhds (DomMulAct.mk x)
-- Mathlib.CategoryTheory.CopyDiscardCategory.Cartesian
/-- Cartesian categories have copy-discard structure.  -/
CategoryTheory.CartesianCopyDiscard.ofCartesianMonoidalCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.CopyDiscardCategory C
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.instIsTorsionFree : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M],
  Module.IsTorsionFree R M
-- Mathlib.Logic.Small.Defs
small_plift : ∀ (α : Type u) [Small.{v, u} α], Small.{v, u + 1} (PLift α)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.Hom.right : CategoryTheory.Limits.WalkingReflexivePair.one.Hom CategoryTheory.Limits.WalkingReflexivePair.zero
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.zigzag_equivalence : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J], Equivalence CategoryTheory.Zigzag
-- Init.Grind.Ring.Basic
/-- Zero is the right identity for addition.  -/
Lean.Grind.Semiring.add_zero : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (a : α), a + 0 = a
-- Mathlib.Order.Hom.Basic
OrderIso.refl_apply : ∀ {α : Type u_2} [inst : LE α] (x : α), (OrderIso.refl α) x = x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.of_add_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α}, (s + t).Nonempty → t.Nonempty
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_fn_injective : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  Function.Injective DFunLike.coe
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.nsmul_eq_nsmul : ∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddCommMonoid X] [inst_3 : Module R X] (n : ℕ) (x : OreLocalization S X), n • x = n • x
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop}
  {U : TopologicalSpace.Opens M'} (f : M → ↥U) (s : Set M) (x : M),
  ChartedSpace.LiftPropWithinAt P (Subtype.val ∘ f) s x ↔ ChartedSpace.LiftPropWithinAt P f s x
-- Init.Data.UInt.Basic
instModUSize : Mod USize
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `UniformCauchySeqOn.sub` -/
UniformCauchySeqOn.fun_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {s : Set β},
  UniformCauchySeqOn f l s → UniformCauchySeqOn f' l s → UniformCauchySeqOn (fun i i_1 => f i i_1 - f' i i_1) l s
-- Mathlib.Data.Finset.NAry
/-- A common special case of `image₂_congr`  -/
Finset.image₂_congr' : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f f' : α → β → γ} {s : Finset α} {t : Finset β},
  (∀ (a : α) (b : β), f a b = f' a b) → Finset.image₂ f s t = Finset.image₂ f' s t
-- Batteries.Data.List.Scan
List.getElem?_partialProds : ∀ {α : Type u_1} {i : ℕ} [inst : Mul α] [inst_1 : One α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1] {l : List α},
  l.partialProds[i]? = if i ≤ l.length then some (List.take i l).prod else none
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.coneOfConeForget_pt : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat}
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget TopCat))),
  (TopCat.coneOfConeForget c).pt = TopCat.of (TopCat.conePtOfConeForget c)
-- Batteries.Data.Vector.Lemmas
Vector.toArray_injective : ∀ {α : Type u_1} {n : ℕ} {v w : Vector α n}, v.toArray = w.toArray → v = w
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_unitIso_hom_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).unitIso.hom.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.oneTruncation₂_obj : ∀ (S : SSet.Truncated 2), SSet.oneTruncation₂.obj S = CategoryTheory.ReflQuiv.of (SSet.OneTruncation₂ S)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- The region between two a.e.-measurable functions on a null-measurable set is null-measurable;
a version for the region together with the graphs of both functions.  -/
nullMeasurableSet_region_between_cc : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f g : α → ℝ},
  AEMeasurable f μ →
    AEMeasurable g μ →
      ∀ {s : Set α},
        MeasureTheory.NullMeasurableSet s μ →
          MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Icc (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.homeomorphCircle'_apply : ∀ (θ : Real.Angle), AddCircle.homeomorphCircle' θ = θ.toCircle
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.find?_toArray_eq_some_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {v : β k}, Array.find? (fun x => cmp x.fst k == Ordering.eq) t.toArray = some ⟨k, v⟩ ↔ t.get? k = some v
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instInvolutiveStar : InvolutiveStar Complex.UnitDisc
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.mainCore : Lean.Expr →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.State { } →
      optParam Lean.Meta.Simp.Methods { } → Lean.MetaM (Lean.Meta.Simp.Result × Lean.Meta.Simp.State)
-- Std.Http.Internal.IndexMultiMap
Option.get.hcongr_3 : ∀ (α α' : Type u),
  α = α' →
    ∀ (o : Option α) (o' : Option α'),
      o ≍ o' → ∀ (a : o.isSome = true) (a' : o'.isSome = true), a ≍ a' → o.get a ≍ o'.get a'
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- Turn an element of a type `F` satisfying `NonUnitalAlgHomClass F R A B` into an actual
@[coe]
`NonUnitalAlgHom`. This is declared as the default coercion from `F` to `A →ₛₙₐ[R] B`.  -/
NonUnitalAlgHomClass.toNonUnitalAlgHom : {F : Type u_3} →
  {R : Type u_4} →
    [inst : Monoid R] →
      {A : Type u_5} →
        {B : Type u_6} →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : DistribMulAction R A] →
              [inst_3 : NonUnitalNonAssocSemiring B] →
                [inst_4 : DistribMulAction R B] →
                  [inst_5 : FunLike F A B] → [NonUnitalAlgHomClass F R A B] → F → A →ₙₐ[R] B
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.next.eq_1 : ∀ (s : String) (i : String.Pos.Raw), { s := s, i := i }.next = { s := s, i := String.Pos.Raw.next s i }
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
/-- The sum of two functions that are majorized with exponents `f_exp` and `g_exp` is
majorized with exponent `exp` whenever `exp ≥ max f_exp g_exp`.  -/
Tactic.ComputeAsymptotics.Majorized.add : ∀ {f g b : ℝ → ℝ} {exp f_exp g_exp : ℝ},
  Tactic.ComputeAsymptotics.Majorized f b f_exp →
    Tactic.ComputeAsymptotics.Majorized g b g_exp →
      f_exp ≤ exp → g_exp ≤ exp → Tactic.ComputeAsymptotics.Majorized (f + g) b exp
-- Init.Data.Vector.Perm
Vector.swap_perm : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} (h₁ : i < n) (h₂ : j < n), (xs.swap i j h₁ h₂).Perm xs
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.congrHom_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X ⟶ Z} {g₁ g₂ : Y ⟶ Z} (h₁ : f₁ = f₂)
  (h₂ : g₁ = g₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ g₁] [inst_2 : CategoryTheory.Limits.HasPullback f₂ g₂],
  (CategoryTheory.Limits.pullback.congrHom h₁ h₂).inv =
    CategoryTheory.Limits.pullback.map f₂ g₂ f₁ g₁ (CategoryTheory.CategoryStruct.id X)
      (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯
-- Mathlib.Data.Num.ZNum
ZNum.neg_of_int : ∀ (n : ℤ), ↑(-n) = -↑n
-- Mathlib.Computability.RegularExpressions
RegularExpression.deriv_star : ∀ {α : Type u_1} [inst : DecidableEq α] (P : RegularExpression α) (a : α), P.star.deriv a = P.deriv a * P.star
-- Mathlib.Analysis.Convex.Body
ConvexBody.instAdd : {V : Type u_1} →
  [inst : TopologicalSpace V] →
    [inst_1 : AddCommGroup V] → [inst_2 : Module ℝ V] → [ContinuousAdd V] → Add (ConvexBody V)
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_le_abs : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {f : Filter β}
  {u : β → α},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => |u a|) ↔
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u ∧ Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f u
-- Mathlib.Order.SupClosed
IsSublattice.image : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] {s : Set α}
  [inst_2 : FunLike F α β] [LatticeHomClass F α β], IsSublattice s → ∀ (f : F), IsSublattice (⇑f '' s)
-- Mathlib.Algebra.Lie.TensorProduct
/-- Given Lie submodules `M' ⊆ M` and `N' ⊆ N`, this is the natural map: `M' ⊗ N' → M ⊗ N`.  -/
TensorProduct.LieModule.mapIncl : {R : Type u} →
  [inst : CommRing R] →
    {L : Type v} →
      {M : Type w} →
        {N : Type w₁} →
          [inst_1 : LieRing L] →
            [inst_2 : LieAlgebra R L] →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module R M] →
                  [inst_5 : LieRingModule L M] →
                    [inst_6 : LieModule R L M] →
                      [inst_7 : AddCommGroup N] →
                        [inst_8 : Module R N] →
                          [inst_9 : LieRingModule L N] →
                            [inst_10 : LieModule R L N] →
                              (M' : LieSubmodule R L M) →
                                (N' : LieSubmodule R L N) → TensorProduct R ↥M' ↥N' →ₗ⁅R,L⁆ TensorProduct R M N
-- Mathlib.Order.ScottContinuity
ScottContinuous.prodMk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {g : α → γ}, ScottContinuous f → ScottContinuous g → ScottContinuous fun x => (f x, g x)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_antiperiodic : Function.Antiperiodic Real.sin Real.pi
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.notification.injEq : ∀ (method method_1 : String),
  (Lean.JsonRpc.MessageMetaData.notification method = Lean.JsonRpc.MessageMetaData.notification method_1) =
    (method = method_1)
-- Std.Do.Triple.SpecLemmas
List.Cursor.ext : ∀ {α : Type u} {l : List α} {x y : l.Cursor}, x.prefix = y.prefix → x.suffix = y.suffix → x = y
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
/-- An element of an `m`-admissible list, as an element of the appropriate `Fin`  -/
SimplexCategoryGenRel.IsAdmissible.getElemAsFin : {m : ℕ} → {L : List ℕ} → SimplexCategoryGenRel.IsAdmissible m L → (k : ℕ) → k < L.length → Fin (m + k + 1)
-- Mathlib.Data.List.Defs
/-- `orM xs` runs the actions in `xs`, returning true if any of them returns
true. `orM` short-circuits, so if an action returns true, later actions are
not run.  -/
List.orM : {m : Type → Type v} → [Monad m] → List (m Bool) → m Bool
-- Mathlib.Algebra.Module.Projective
Module.Projective.of_shrink : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Small.{w, u_3} M] [Module.Projective R (Shrink.{w, u_3} M)], Module.Projective R M
-- Init.System.ST
EST.Out.error.injEq : ∀ {ε σ α : Type} (a : ε) (a_1 : Void σ) (a_2 : ε) (a_3 : Void σ),
  (EST.Out.error a a_1 = EST.Out.error a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.SetTheory.Ordinal.Notation
/-- `scale x o` is the ordinal notation for `ω ^ x * o`.  -/
ONote.scale : ONote → ONote → ONote
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.comap_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {g : γ → α} (κ : ProbabilityTheory.Kernel α β) (hg : Measurable g) (c : γ),
  (κ.comap g hg) c = κ (g c)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_alter!_of_not_compare_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      ¬compare k k' = Ordering.eq → (k' ∈ Std.DTreeMap.Internal.Impl.Const.alter! k f t ↔ k' ∈ t)
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
/-- **Alias** of `MeasureTheory.ae_norm_ofReal_f_le_bound`. -/
MeasureTheory.all_ae_ofReal_f_le_bound : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {F : ℕ → α → β} {f : α → β} {bound : α → ℝ},
  (∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) →
    (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) →
      ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.instLieRing : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → (ψ : L →ₗ⁅R⁆ LieDerivation R K K) → LieRing (K ⋊⁅ψ⁆ L)
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.insert_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α}
  {b : β a}, m.insert a b = ↑(Std.DHashMap.Internal.Raw₀.insert ⟨m, ⋯⟩ a b)
-- Mathlib.SetTheory.ZFC.Basic
/-- `ZFSet.powerset` is equivalent to `Set.powerset`.  -/
ZFSet.powersetEquiv : (x : ZFSet.{u}) → ↥x.powerset ≃ ↑(𝒫 ↑x)