mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.SMulInvariantMeasure.measure_preimage_smul : ∀ {M : Type u_1} {α : Type u_2} {inst : SMul M α} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [self : MeasureTheory.SMulInvariantMeasure M α μ] (c : M) ⦃s : Set α⦄,
  MeasurableSet s → μ ((fun x => c • x) ⁻¹' s) = μ s
-- Mathlib.Data.ENat.Basic
/-- A version of `ENat.map` for `OneHom`s.  -/
OneHom.ENatMap : {N : Type u_2} → [inst : One N] → OneHom ℕ N → OneHom ℕ∞ (WithTop N)
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.Homotopy.smul_h₂ : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (a : R), (h.smul a).h₂ = a • h.h₂
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.length_toList : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.HasSize α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_6 : Std.Rxc.IsAlwaysFinite α] [Std.Rxc.LawfulHasSize α], r.toList.length = r.size
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.zero_mod : ∀ (b : Ordinal.{u_4}), 0 % b = 0
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- If a multilinear map in finitely many variables on normed spaces is continuous, then it
satisfies the inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖`, for some `C` which can be chosen to be
positive.  -/
MultilinearMap.exists_bound_of_continuous : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] (f : MultilinearMap 𝕜 E G),
  Continuous ⇑f → ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.op_i₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A),
  P.op.i₀ = P.p₀.op
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mem_nonZeroDivisors_iff : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {r : M₀},
  r ∈ nonZeroDivisors M₀ ↔ (∀ (x : M₀), r * x = 0 → x = 0) ∧ ∀ (x : M₀), x * r = 0 → x = 0
-- Init.Data.Nat.Lemmas
Nat.pow_pred_mul : ∀ {x w : ℕ}, 0 < w → x ^ (w - 1) * x = x ^ w
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- Given any other colimit cocone for `F`, the chosen `colimit F` is isomorphic to the cocone
point.  -/
CategoryTheory.Limits.colimit.isoColimitCocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            (t : CategoryTheory.Limits.ColimitCocone F) → CategoryTheory.Limits.colimit F ≅ t.cocone.pt
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.symm : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → v₂.IsEquiv v₁
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.lift_eq : ∀ {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) {Q : Type u_3}
  [inst_9 : AddCommMonoid Q] [inst_10 : Module S Q] [inst_11 : Module R Q] [inst_12 : IsScalarTower R S Q]
  (g : M →ₗ[R] Q) (x : M), (h.lift g) (f x) = g x
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.top_toSubalgebra : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A], ⊤.toSubalgebra = ⊤
-- Init.Data.SInt.Lemmas
Int32.add_left_inj : ∀ {a b : Int32} (c : Int32), a + c = b + c ↔ a = b
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Reorder a product.

The difference with `Finset.prod_bij'` is that the bijection is specified as a surjective injection,
rather than by an inverse function.

The difference with `Finset.prod_nbij` is that the bijection is allowed to use membership of the
domain of the product, rather than being a non-dependent function.  -/
Finset.prod_bij : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (i : (a : ι) → a ∈ s → κ),
  (∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) →
    (∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) →
      (∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b) →
        (∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) → ∏ x ∈ s, f x = ∏ x ∈ t, g x
-- Mathlib.Analysis.SpecialFunctions.Arsinh
HasStrictFDerivAt.arsinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : StrongDual ℝ E},
  HasStrictFDerivAt f f' a → HasStrictFDerivAt (fun x => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') a
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_3} (motive : (x : Option α) → ((a : α) → x = some a → β) → Sort u_2) (a : α)
  (f : (a_1 : α) → some a = some a_1 → β) (h_1 : (x : (a : α) → none = some a → β) → motive none x)
  (h_2 : (a : α) → (f : (a_1 : α) → some a = some a_1 → β) → motive (some a) f),
  (match some a, f with
    | none, x => h_1 x
    | some a, f => h_2 a f) =
    h_2 a f
-- Lean.Elab.InfoTree.Main
/-- Runs `x`. The last info tree that is pushed while running `x` is assigned to `mvarId`. All other
pushed info trees are silently discarded.
 -/
Lean.Elab.withInfoHole : {m : Type → Type} → {α : Type} → [MonadFinally m] → [Monad m] → [Lean.Elab.MonadInfoTree m] → Lean.MVarId → m α → m α
-- Batteries.Util.ExtendedBinder
/-- The syntax `∀ᵉ (x < 2) (y < 3), p x y` is shorthand for `∀ x < 2, ∀ y < 3, p x y`.  -/
Batteries.ExtendedBinder.«term∀ᵉ_,_» : Lean.ParserDescr
-- Init.Control.Lawful.MonadAttach.Lemmas
WeaklyLawfulMonadAttach.bind_attach_of_nonempty : ∀ {m : Type u_1 → Type u_2} {β α : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Nonempty (m β)] {x : m α} {f : Subtype (MonadAttach.CanReturn x) → m β},
  MonadAttach.attach x >>= f = do
    let a ← x
    if ha : MonadAttach.CanReturn x a then f ⟨a, ha⟩ else Classical.ofNonempty
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkSpecializes_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {x y z : ↑X} (h : x ⤳ y) (h' : y ⤳ z),
  CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h') (F.stalkSpecializes h) = F.stalkSpecializes ⋯
-- Mathlib.Tactic.DepRewrite
_private.Mathlib.Tactic.DepRewrite.0.Mathlib.Tactic.DepRewrite.instEvalExprCastMode.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Tactic.DepRewrite.CastMode
-- Mathlib.Order.Hom.Basic
/-- Reinterpret a bundled monotone function as a monotone function between dual orders.  -/
OrderHom.dual : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) ≃ (αᵒᵈ →o βᵒᵈ)
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- Given a continuous group homomorphism `φ : H →ₜ* G`, a continuous intertwining map
`f : π.restrict φ →ⁱL π'` induces a continuous intertwining map
`π.coind₁.restrict φ →ⁱL π'.coind₁`, sending `F : C(G, V)` to `f ∘ F ∘ φ : C(H, W)`.  -/
ContRepresentation.coind₁ResMap : {R : Type u_1} →
  {V : Type u_3} →
    {W : Type u_4} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : TopologicalSpace V] →
            [inst_3 : IsTopologicalAddGroup V] →
              [inst_4 : Module R V] →
                [inst_5 : AddCommGroup W] →
                  [inst_6 : TopologicalSpace W] →
                    [inst_7 : IsTopologicalAddGroup W] →
                      [inst_8 : Module R W] →
                        {G : Type u_7} →
                          {H : Type u_8} →
                            [inst_9 : Group G] →
                              [inst_10 : TopologicalSpace G] →
                                [inst_11 : TopologicalSpace R] →
                                  [inst_12 : ContinuousSMul R V] →
                                    [inst_13 : ContinuousSMul R W] →
                                      [inst_14 : Group H] →
                                        [inst_15 : TopologicalSpace H] →
                                          {π : ContRepresentation R G V} →
                                            [inst_16 : IsTopologicalGroup G] →
                                              [inst_17 : IsTopologicalGroup H] →
                                                {π' : ContRepresentation R H W} →
                                                  (φ : H →ₜ* G) →
                                                    ContIntertwiningMap (π.restrict ↑φ) π' →
                                                      ContIntertwiningMap (π.coind₁.restrict ↑φ) π'.coind₁
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.mul_one : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.mul a (Lean.Grind.Ring.OfSemiring.natCast 1) = a
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Two intermediate fields are equal if they have the same elements.  -/
IntermediateField.ext : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {S T : IntermediateField K L}, (∀ (x : L), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.adjoin_primitive_root_eq_top : ∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {n : ℕ} [NeZero n]
  [IsDomain B] [h : IsCyclotomicExtension {n} A B] {ζ : B}, IsPrimitiveRoot ζ n → A[ζ] = ⊤
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.interior_map : ∀ {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_4} {P₂ : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup V₂] [inst_5 : Module k V₂]
  [inst_6 : AddTorsor V₂ P₂] [inst_7 : PartialOrder k] {n : ℕ} (s : Affine.Simplex k P n) {f : P →ᵃ[k] P₂}
  (hf : Function.Injective ⇑f), (s.map f hf).interior = ⇑f '' s.interior
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.toList_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {f : α → Bool},
  (Std.ExtTreeSet.filter f t).toList = List.filter f t.toList
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.Hom.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : CategoryTheory.SpectralSequence C c r₀} [inst_2 : SizeOf C]
  [inst_3 : SizeOf κ]
  (hom : (r : ℤ) → (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_1) → E.page r ⋯ ⟶ E'.page r ⋯)
  (comm :
    autoParam
      (∀ (r r' : ℤ) (pq : κ) (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.Hom._auto_5)
        (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_7),
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hom r ⋯) pq) (E'.iso r r' pq ⋯ ⋯).hom =
          CategoryTheory.CategoryStruct.comp (E.iso r r' pq ⋯ ⋯).hom ((hom r' ⋯).f pq))
      CategoryTheory.SpectralSequence.Hom.comm._autoParam),
  sizeOf { hom := hom, comm := comm } = 1
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.biUnion_congr : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I}
  {πi₁ πi₂ : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J},
  π₁ = π₂ → (∀ J ∈ π₁, πi₁ J = πi₂ J) → π₁.biUnion πi₁ = π₂.biUnion πi₂
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.asOverHom_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] (f : X ⟶ Y) [inst_3 : CategoryTheory.IsIso f]
  [inst_4 : CategoryTheory.HomIsOver f S],
  CategoryTheory.OverClass.asOverHom S (CategoryTheory.inv f) =
    CategoryTheory.inv (CategoryTheory.OverClass.asOverHom S f)
-- Init.Data.Array.MinMax
List.min_eq_min_toArray : ∀ {α : Type u_1} [inst : Min α] {l : List α} {h : l ≠ []}, l.min h = l.toArray.min ⋯
-- Mathlib.MeasureTheory.Group.Measure
/-- If a left-invariant measure gives finite mass to a nonempty open set, then it gives finite mass
to any compact set.  -/
MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] (U : Set G),
  IsOpen U → U.Nonempty → μ U ≠ ⊤ → ∀ {K : Set G}, IsCompact K → μ K < ⊤
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItem.sortText? : Lean.Lsp.CompletionItem → Option String
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAgainst.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.MorphismProperty C},
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), P' f → P.IsStableUnderCobaseChangeAlong f) → P.IsStableUnderCobaseChangeAgainst P'
-- Mathlib.Tactic.ApplyFun
/-- Given a metavariable `ginj` of type `Injective f`, try to prove it.
Returns whether it was successful.  -/
Mathlib.Tactic.maybeProveInjective : Lean.Expr → Option Lean.Expr → Lean.MetaM Bool
-- Mathlib.SetTheory.Lists
Lists'.nil.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf Lists'.nil = 1
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.ext_iff : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} {α β : CategoryTheory.BasedNatTrans F G},
  α = β ↔ α.toNatTrans = β.toNatTrans
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `r` is a negative constant, `fun x ↦ f x / r` tends to negative infinity along a filter `l`
if and only if `f` tends to infinity along `l`.  -/
Filter.tendsto_div_const_atBot_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, r < 0 → (Filter.Tendsto (fun x => f x / r) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop)
-- Std.Data.ExtDTreeMap.Basic
/-- Inserts multiple mappings into the tree map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `TreeMap`, `DTreeMap`, `TreeMap.Raw` and `DTreeMap.Raw`.
The `insertMany` function on `TreeSet` and `TreeSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.ExtDTreeMap.Const.insertMany : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [Std.TransCmp cmp] →
        {ρ : Type u_1} →
          [ForIn Id ρ (α × β)] → Std.ExtDTreeMap α (fun x => β) cmp → ρ → Std.ExtDTreeMap α (fun x => β) cmp
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- Evaluates expressions of the form `a ^ b` when `a : ℝ≥0` and `b : ℝ`.
Works if `a`, `b`, and `a ^ b` are in fact rational numbers.
 -/
Mathlib.Meta.NormNum.evalNNRealRPow : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.instFunLikeSubtypeDualMemDualAnnihilator : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (W : Submodule R M) → FunLike (↥W.dualAnnihilator) M R
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 :
    ∀ {X S : C} (πX : X ⟶ S),
      CategoryTheory.Limits.HasColimitsOfShape
        (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
  (π : CategoryTheory.Arrow C),
  (CategoryTheory.SmallObject.functor f).obj π =
    CategoryTheory.Arrow.mk (CategoryTheory.SmallObject.πFunctorObj f π.hom)
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.lintegral_conv_eq_lintegral_sum : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] {μ ν : MeasureTheory.Measure M}
  {f : M → ENNReal}, Measurable f → ∫⁻ (z : M), f z ∂μ.conv ν = ∫⁻ (z : M × M), f (z.1 + z.2) ∂μ.prod ν
-- Mathlib.Order.Filter.Map
Filter.comap_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {φ : α → β} {θ : α → γ} {ψ : β → δ} {ρ : γ → δ},
  ψ ∘ φ = ρ ∘ θ → ∀ (G : Filter δ), Filter.comap φ (Filter.comap ψ G) = Filter.comap θ (Filter.comap ρ G)
-- Mathlib.Algebra.FreeAlgebra
/-- Noncommutative version of `Algebra.adjoin_range_eq_range_aeval`.  -/
Algebra.adjoin_range_eq_range_freeAlgebra_lift : ∀ (R : Type u_1) (X : Type u_2) [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (f : X → A), Algebra.adjoin R (Set.range f) = ((FreeAlgebra.lift R) f).range
-- Init.Data.BitVec.Lemmas
BitVec.instLawfulCommIdentityHXorOfNatOfNatNat : ∀ {n : ℕ}, Std.LawfulCommIdentity (fun x1 x2 => x1 ^^^ x2) 0#n
-- Init.Data.Vector.OfFn
Vector.ofFnM_add : ∀ {k : ℕ} {α : Type u_1} {n : ℕ} {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m] {f : Fin (n + k) → m α},
  Vector.ofFnM f = do
    let as ← Vector.ofFnM fun i => f (Fin.castLE ⋯ i)
    let bs ← Vector.ofFnM fun i => f (Fin.natAdd n i)
    pure (as ++ bs)
-- Mathlib.Topology.Order.LeftRight
continuousWithinAt_iff_continuous_left_right : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace β]
  {s : Set α} {a : α} {f : α → β},
  ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Set.Iic a) a ∧ ContinuousWithinAt f (s ∩ Set.Ici a) a
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lmarginal_le_of_subset : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] {s t : Finset δ} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)]
  {f g : ((i : δ) → X i) → ENNReal},
  s ⊆ t → Measurable f → Measurable g → ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ → ∫⋯∫⁻_t, f ∂μ ≤ ∫⋯∫⁻_t, g ∂μ
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesAt.eventually_hasSum : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E},
  HasFPowerSeriesAt f p x → ∀ᶠ (y : E) in nhds 0, HasSum (fun n => (p n) fun x => y) (f (x + y))
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `FunLike.coe_add`. -/
QuadraticMap.coeFn_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.isScalarField : Lean.Name → Lean.CoreM Bool
-- Std.Data.TreeMap.Raw.Iterator
Std.TreeMap.Raw.toList.eq_1 : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap.Raw α β cmp),
  t.toList = Std.DTreeMap.Raw.Const.toList t.inner
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.le_sin : ∀ {x : ℝ}, x ≤ 0 → x ≤ Real.sin x
-- Lean.Util.LeanOptions
Lean.instToJsonLeanOptionValue : Lean.ToJson Lean.LeanOptionValue
-- Plausible.Testable
/-- Once a property fails to hold on an example, look for smaller counter-examples
to show the user.  -/
Plausible.Testable.minimize : {α : Sort u_1} →
  [inst : Plausible.SampleableExt α] →
    {β : α → Prop} →
      [(x : α) → Plausible.Testable (β x)] →
        Plausible.Configuration →
          String →
            (x : Plausible.SampleableExt.proxy α) →
              Plausible.TestResult (β (Plausible.SampleableExt.interp x)) →
                Plausible.Gen
                  ((x : Plausible.SampleableExt.proxy α) × Plausible.TestResult (β (Plausible.SampleableExt.interp x)))
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.dist_eq_dist_add_one_of_adj_of_reachable : ∀ {V : Type u_1} {G : SimpleGraph V},
  G.IsAcyclic →
    ∀ (u : V) {v w : V}, G.Adj v w → G.Reachable u v → G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1
-- Mathlib.Tactic.FunProp.FunctionData
/-- local context where `mainVar` exists  -/
Mathlib.Meta.FunProp.FunctionData.lctx : Mathlib.Meta.FunProp.FunctionData → Lean.LocalContext
-- Mathlib.Data.Finset.Sum
Finset.subset_map_inl : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {u : Finset (α ⊕ β)},
  u ⊆ Finset.map Function.Embedding.inl s ↔ u.toLeft ⊆ s ∧ u.toRight = ∅
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.derivative_coe : ∀ {R : Type u_1} [inst : CommSemiring R] (f : Polynomial R), (PowerSeries.derivative R) ↑f = ↑(Polynomial.derivative f)
-- Std.Async.Basic
/-- Runs all computations in an `Array` concurrently and returns all results as an array.
 -/
Std.Async.BaseAsync.concurrentlyAll : {α : Type} →
  Array (Std.Async.BaseAsync α) → optParam Task.Priority Task.Priority.default → Std.Async.BaseAsync (Array α)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeExtension.mapPosSubmonoid_apply_coe : ∀ (A : Type u_1) (B : Type u_2) [inst : CommSemiring A] [inst_1 : Semiring B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B] [inst_5 : ValuativeExtension A B]
  (x : ↥(ValuativeRel.posSubmonoid A)), ↑((ValuativeExtension.mapPosSubmonoid A B) x) = (algebraMap A B) ↑x
-- Init.Data.Option.Basic
Option.getM_some : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Alternative m] {a : α}, (some a).getM = pure a
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.Ordering.Compares.match_1.splitter : {α : Type u_2} →
  (motive : Ordering → α → α → Sort u_1) →
    (x : Ordering) →
      (x_1 x_2 : α) →
        ((a b : α) → motive Ordering.lt a b) →
          ((a b : α) → motive Ordering.eq a b) → ((a b : α) → motive Ordering.gt a b) → motive x x_1 x_2
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)} {he : t.alter k f ≠ ∅},
  (t.alter k f).maxKey he = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.Cells.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w'} {inst_1 : LinearOrder J} {inst_2 : OrderBot J}
  {inst_3 : SuccOrder J} {inst_4 : WellFoundedLT J} {α : J → Type t} {A B : (j : J) → α j → C}
  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y}
  {c : HomotopicalAlgebra.RelativeCellComplex basicCell f} {j : J} {hj : ¬IsMax j} {k : (c.attachCells j hj).ι}
  {j_1 : J} {hj_1 : ¬IsMax j_1} {k_1 : (c.attachCells j_1 hj_1).ι},
  { j := j, hj := hj, k := k } = { j := j_1, hj := hj_1, k := k_1 } → j = j_1 ∧ k ≍ k_1
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.centralizer_centralizer_centralizer : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A},
  Subalgebra.centralizer R s.centralizer.centralizer = Subalgebra.centralizer R s
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.largeSchroder_two : Nat.largeSchroder 2 = 6