mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Divisible
/-- The root function  -/
RootableBy.root : {A : Type u_1} →
  {α : Type u_2} → {inst : Monoid A} → {inst_1 : Pow A α} → {inst_2 : Zero α} → [self : RootableBy A α] → A → α → A
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pos.ofEqAppend.congr_simp : ∀ {s : String.Slice} {t₁ t₁_1 : String} (e_t₁ : t₁ = t₁_1) {t₂ t₂_1 : String} (e_t₂ : t₂ = t₂_1)
  (h : s.copy = t₁ ++ t₂), String.Slice.Pos.ofEqAppend h = String.Slice.Pos.ofEqAppend ⋯
-- Init.Data.List.Sort.Basic
/-- Split a list in two equal parts. If the length is odd, the first part will be one element longer.

This is an implementation detail of `mergeSort`.
 -/
List.MergeSort.Internal.splitInTwo : {α : Type u_1} → {n : ℕ} → { l // l.length = n } → { l // l.length = (n + 1) / 2 } × { l // l.length = n / 2 }
-- Mathlib.MeasureTheory.Function.AEMeasurableOrder
/-- If a function `f : α → ℝ≥0∞` is such that the level sets `{f < p}` and `{q < f}` have measurable
supersets which are disjoint up to measure zero when `p` and `q` are finite numbers satisfying
`p < q`, then `f` is almost-everywhere measurable.  -/
ENNReal.aemeasurable_of_exist_almost_disjoint_supersets : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
  (∀ (p q : NNReal),
      p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < ↑p} ⊆ u ∧ {x | ↑q < f x} ⊆ v ∧ μ (u ∩ v) = 0) →
    AEMeasurable f μ
-- Batteries.Data.List.Basic
/-- `ofFnNthVal f i` returns `some (f i)` if `i < n` and `none` otherwise.  -/
List.ofFnNthVal : {α : Type u_1} → {n : ℕ} → (Fin n → α) → ℕ → Option α
-- Init.Data.Array.Lemmas
Array.filterMap_eq_empty_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {xs : Array α}, Array.filterMap f xs = #[] ↔ ∀ a ∈ xs, f a = none
-- Mathlib.Data.Finsupp.Single
Finsupp.support_single : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {b : M} (a : α), b ≠ 0 → (fun₀ | a => b).support = {a}
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.addSubgroup_eq_bot : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  FiniteArchimedeanClass.addSubgroup ⊤ = ⊥
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.subsingleton_iff : ∀ {G : Type u_1} [inst : AddGroup G], Subsingleton (AddSubgroup G) ↔ Subsingleton G
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.map_ne : ∀ {𝕜 : Type u_1} {V₁' : Type u_4} {V₂ : Type u_5} {P₁' : Type u_9} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V₁'] [inst_2 : NormedSpace 𝕜 V₁'] [inst_3 : MetricSpace P₁']
  [inst_4 : NormedAddTorsor V₁' P₁'] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f₁ : P₁' →ᵃⁱ[𝕜] P₂) {x y : P₁'}, x ≠ y → f₁ x ≠ f₁ y
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- If `p` is an independent family of submodules of an `R`-finite module `M`, then the
number of nontrivial subspaces in the family `p` is finite.  -/
iSupIndep.fintypeNeBotOfFiniteDimensional : {ι : Type w} →
  {R : Type u} →
    {M : Type v} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [IsDomain R] →
              [Module.IsTorsionFree R M] →
                [Module.Finite R M] →
                  [StrongRankCondition R] → {p : ι → Submodule R M} → iSupIndep p → Fintype { i // p i ≠ ⊥ }
-- Mathlib.Data.Set.Function
Set.eqOn_univ : ∀ {α : Type u_1} {β : Type u_2} (f₁ f₂ : α → β), Set.EqOn f₁ f₂ Set.univ ↔ f₁ = f₂
-- Mathlib.Algebra.Group.Basic
div_mul_eq_div_mul_one_div : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a / (b * c) = a / b * (1 / c)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.ofIso_II : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {Y : SSet} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom = B),
  (P.ofIso e hA).II = ⇑(SSet.Subcomplex.N.orderIsoOfIso e hA) ⁻¹' P.II
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
measurable_coe_ennreal_ereal : Measurable ENNReal.toEReal
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.instCoeForallParenthesizerAliasValue : Coe (Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer)
  Lean.PrettyPrinter.Parenthesizer.ParenthesizerAliasValue
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] {f g : BoundedLatticeHom α β}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
ufm_of_decomposition_of_wfDvdMonoid : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] [WfDvdMonoid α] [DecompositionMonoid α],
  UniqueFactorizationMonoid α
-- Lean.Meta.Closure
_private.Lean.Meta.Closure.0.Lean.Meta.Closure.TopoSort.tempMark : Lean.Meta.Closure.TopoSort✝ → Lean.FVarIdHashSet
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.lift.equiv_apply : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7)
  (N : Type u_8) (P₂ : Type u_17) [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] (f : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) (m : M) (n : N),
  ((TensorProduct.lift.equiv σ₁₂ M N P₂) f) (m ⊗ₜ[R] n) = (f m) n
-- Init.Data.List.Basic
List.sum_eq_foldr : ∀ {α : Type u} [inst : Add α] [inst_1 : Zero α] {l : List α}, l.sum = List.foldr (fun x1 x2 => x1 + x2) 0 l
-- Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
/-- If a monotone sequence of functions has an upper bound and the sequence of integrals of these
functions tends to the integral of the upper bound, then the sequence of functions converges
almost everywhere to the upper bound. Auxiliary version assuming moreover that the
functions in the sequence are ae measurable.  -/
MeasureTheory.tendsto_of_lintegral_tendsto_of_monotone_aux : ∀ {α : Type u_2} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {F : α → ENNReal} {μ : MeasureTheory.Measure α},
  (∀ (n : ℕ), AEMeasurable (f n) μ) →
    AEMeasurable F μ →
      Filter.Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (nhds (∫⁻ (a : α), F a ∂μ)) →
        (∀ᵐ (a : α) ∂μ, Monotone fun i => f i a) →
          (∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a) →
            ∫⁻ (a : α), F a ∂μ ≠ ⊤ → ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (nhds (F a))
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instBEqTheoremForm.beq : Mathlib.Meta.FunProp.TheoremForm → Mathlib.Meta.FunProp.TheoremForm → Bool
-- Mathlib.Data.Set.Monotone
MonotoneOn.monotone : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  MonotoneOn f s → Monotone (f ∘ Subtype.val)
-- Mathlib.Data.Num.Lemmas
Num.of_to_nat' : ∀ (n : Num), Num.ofNat' ↑n = n
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- The monomorphism `Injective.ι : X ⟶ Injective.under X`
from the arbitrarily chosen injective object under `X`.
 -/
CategoryTheory.Injective.ι : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.EnoughInjectives C] → (X : C) → X ⟶ CategoryTheory.Injective.under X
-- Mathlib.MeasureTheory.Function.UnifTight
/-- This lemma is less general than `MeasureTheory.unifTight_finite` which applies to
all sequences indexed by a finite type.  -/
_private.Mathlib.MeasureTheory.Function.UnifTight.0.MeasureTheory.unifTight_fin : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal},
  p ≠ ⊤ → ∀ {n : ℕ} {f : Fin n → α → β}, (∀ (i : Fin n), MeasureTheory.MemLp (f i) p μ) → MeasureTheory.UnifTight f p μ
-- Lean.Parser.Extension
Lean.Parser.mkInputContext : (input : String) →
  String →
    optParam Bool true →
      (endPos : optParam String.Pos.Raw input.rawEndPos) →
        autoParam (endPos ≤ input.rawEndPos) Lean.Parser.mkInputContext._auto_1 → Lean.Parser.InputContext
-- Mathlib.Algebra.CharP.Reduced
iterateFrobenius_inj : ∀ (R : Type u_1) [inst : CommRing R] [IsReduced R] (p n : ℕ) [inst_2 : ExpChar R p],
  Function.Injective ⇑(iterateFrobenius R p n)
-- Mathlib.Computability.Primrec.Basic
Primrec₂.ofNat_iff : ∀ {α : Type u_4} {β : Type u_5} {σ : Type u_6} [inst : Denumerable α] [inst_1 : Denumerable β] [inst_2 : Primcodable σ]
  {f : α → β → σ}, Primrec₂ f ↔ Primrec₂ fun m n => f (Denumerable.ofNat α m) (Denumerable.ofNat β n)
-- Mathlib.CategoryTheory.DifferentialObject
/-- The forgetful functor taking a differential object to its underlying object.  -/
CategoryTheory.DifferentialObject.forget : (S : Type u_1) →
  [inst : AddMonoidWithOne S] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) C
-- Mathlib.MeasureTheory.Measure.Prod
/-- A measure on a product space equals the product measure if they are equal on rectangles
with as sides sets that generate the corresponding σ-algebras.  -/
MeasureTheory.Measure.prod_eq_generateFrom : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {C : Set (Set α)} {D : Set (Set β)},
  MeasurableSpace.generateFrom C = inst →
    MeasurableSpace.generateFrom D = inst_1 →
      IsPiSystem C →
        IsPiSystem D →
          ∀ (h3C : μ.FiniteSpanningSetsIn C) (h3D : ν.FiniteSpanningSetsIn D) {μν : MeasureTheory.Measure (α × β)},
            (∀ s ∈ C, ∀ t ∈ D, μν (s ×ˢ t) = μ s * ν t) → μ.prod ν = μν
-- Mathlib.Data.Stream.Init
Stream'.tail_zip : ∀ {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (s₁ : Stream' α) (s₂ : Stream' β),
  (Stream'.zip f s₁ s₂).tail = Stream'.zip f s₁.tail s₂.tail
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.UniformIntegrable.memLp : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f : ι → α → β} {p : ENNReal},
  MeasureTheory.UniformIntegrable f p μ → ∀ (i : ι), MeasureTheory.MemLp (f i) p μ
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_map_hom : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  {j j' : J} (f : j ⟶ j'),
  ((CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F).map f).hom = CategoryTheory.Limits.lim.map (F.map f)
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.isChain_range_flag : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (b : Module.Basis (Fin n) R M), IsChain (fun x1 x2 => x1 ≤ x2) (Set.range b.flag)
-- Mathlib.Analysis.Normed.Affine.AddTorsor
AddMonoidHom.toRealLinearMap.congr_simp : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
  [inst_3 : ContinuousSMul ℝ E] {F : Type u_2} [inst_4 : AddCommGroup F] [inst_5 : Module ℝ F]
  [inst_6 : TopologicalSpace F] [inst_7 : ContinuousSMul ℝ F] [inst_8 : T2Space F] (f f_1 : E →+ F) (e_f : f = f_1)
  (hf : Continuous ⇑f), f.toRealLinearMap hf = f_1.toRealLinearMap ⋯
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The top additive subgroup is isomorphic to the additive group.

This is the additive group version of `AddSubmonoid.topEquiv`.  -/
AddSubgroup.topEquiv : {G : Type u_1} → [inst : AddGroup G] → ↥⊤ ≃+ G
-- Mathlib.Data.Option.Basic
Option.forall_mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {o : Option α} {p : β → Prop},
  (∀ y ∈ Option.map f o, p y) ↔ ∀ x ∈ o, p (f x)
-- Mathlib.LinearAlgebra.TensorProduct.Associator
/-- If the R- and A- action on A and M satisfy `CompatibleSMul` both ways,
then `A ⊗[R] M` is canonically isomorphic to `M`.  -/
TensorProduct.lidOfCompatibleSMul : (R : Type u_1) →
  [inst : CommSemiring R] →
    (A : Type u_4) →
      (M : Type u_5) →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : CommSemiring A] →
              [inst_4 : Module A M] →
                [inst_5 : Module R A] →
                  [inst_6 : SMulCommClass R A A] →
                    [TensorProduct.CompatibleSMul R A A M] →
                      [TensorProduct.CompatibleSMul A R A M] → TensorProduct R A M ≃ₗ[A] M
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- If two additive homomorphisms from `R[M]` are equal on each `single r m`,
then they are equal.  -/
AddMonoidAlgebra.addMonoidHom_ext : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddZeroClass N]
  ⦃f g : AddMonoidAlgebra R M →+ N⦄,
  (∀ (m : M) (r : R), f (AddMonoidAlgebra.single m r) = g (AddMonoidAlgebra.single m r)) → f = g
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.mem_completeTheory : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {φ : L.Sentence}, φ ∈ L.completeTheory M ↔ M ⊨ φ
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.coe_copy : ∀ {M : Type u_1} [inst : MulOneClass M] {S : Submonoid M} {s : Set M} (hs : s = ↑S), ↑(S.copy s hs) = s
-- Mathlib.Data.Nat.Digits.Defs
Nat.digitsAux.eq_def : ∀ (b : ℕ) (h : 2 ≤ b) (x : ℕ),
  b.digitsAux h x =
    match x with
    | 0 => []
    | n.succ => (n + 1) % b :: b.digitsAux h ((n + 1) / b)
-- Init.Data.Queue
Std.Queue.instInhabited : {α : Type u} → Inhabited (Std.Queue α)
-- Mathlib.Data.Real.Basic
Real.instAddCommSemigroup : AddCommSemigroup ℝ
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.inductionOn₂ : ∀ {α₁ : Type u_2} {α₂ : Type u_3} {rels₁ : FreeMonoid α₁ → FreeMonoid α₁ → Prop}
  {rels₂ : FreeMonoid α₂ → FreeMonoid α₂ → Prop} {δ : PresentedMonoid rels₁ → PresentedMonoid rels₂ → Prop}
  (q₁ : PresentedMonoid rels₁) (q₂ : PresentedMonoid rels₂),
  (∀ (a : FreeMonoid α₁) (b : FreeMonoid α₂), δ ((PresentedMonoid.mk rels₁) a) ((PresentedMonoid.mk rels₂) b)) → δ q₁ q₂
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- The `i`-th homology, as a functor from the homotopy category.  -/
HomotopyCategory.homologyFunctor : {ι : Type u_2} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        (c : ComplexShape ι) →
          [CategoryTheory.CategoryWithHomology V] → ι → CategoryTheory.Functor (HomotopyCategory V c) V
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.compatibility : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {d : F.WellOrderInductionData} [inst_2 : OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} [WellFoundedLT J] {j : J}
  (e : d.Extension val₀ j) {i : J} (e' : d.Extension val₀ i) (h : i ≤ j),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE h).op)) e.val = e'.val
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Measurable.sinc : ∀ {α : Type u_1} {x : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => Real.sinc (f x)
-- Init.Data.Fin.Lemmas
Fin.val_castSucc : ∀ {n : ℕ} (i : Fin n), ↑i.castSucc = ↑i
-- Mathlib.Algebra.Module.Torsion.Free
IsAddTorsionFree.of_isTorsionFree : ∀ (R : Type u_1) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.IsTorsionFree R M] [IsCancelMulZero R] [CharZero R], IsAddTorsionFree M
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.instAddCommGroup : {𝕜 : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : Ring 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : TopologicalSpace E] →
              [inst_4 : IsTopologicalAddGroup E] →
                [inst_5 : ContinuousConstSMul 𝕜 E] →
                  [inst_6 : AddCommGroup F] →
                    [inst_7 : Module 𝕜 F] →
                      [inst_8 : TopologicalSpace F] →
                        [inst_9 : IsTopologicalAddGroup F] →
                          [inst_10 : ContinuousConstSMul 𝕜 F] → AddCommGroup (FormalMultilinearSeries 𝕜 E F)
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedLitVal : Inhabited Lean.IR.LitVal
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.swap_map₂ : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {a b : B × C}
  {f g : a ⟶ b} (a_1 : f ⟶ g),
  (CategoryTheory.Bicategory.Prod.swap B C).map₂ a_1 = CategoryTheory.Prod.mkHom a_1.2 a_1.1
-- Lean.Parser.Do
Lean.Parser.Term.doSeqIndent.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Stream.Init
/-- Streams `s₁` and `s₂` are defined to be bisimulations if
their heads are equal and tails are bisimulations.  -/
Stream'.IsBisimulation : {α : Type u} → (Stream' α → Stream' α → Prop) → Prop
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_eq_iff : ∀ (n₁ n₂ : ℤ), n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_neg : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : AddGroup γ] [inst_3 : IsTopologicalAddGroup γ] (f : α →ₘ[μ] γ), ↑(-f) =ᵐ[μ] -↑f
-- Lean.Elab.Command
/-- Return the stack of all currently active scopes:
the base scope always comes last; new scopes are prepended in the front.
In particular, the current scope is always the first element.
 -/
Lean.Elab.Command.getScopes : Lean.Elab.Command.CommandElabM (List Lean.Elab.Command.Scope)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPullback_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve (F.obj X)),
  (CategoryTheory.Sieve.functorPullback F R).arrows = CategoryTheory.Presieve.functorPullback F R.arrows
-- Mathlib.Data.Fintype.BigOperators
Fintype.sum_extend_by_zero : ∀ {α : Type u_1} {ι : Type u_4} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : AddCommMonoid α] (s : Finset ι)
  (f : ι → α), (∑ i, if i ∈ s then f i else 0) = ∑ i ∈ s, f i
-- Mathlib.Algebra.Group.Commute.Units
/-- If the product of two commuting elements is a unit, then the left multiplier is a unit.  -/
Units.leftOfMul : {M : Type u_1} → [inst : Monoid M] → (u : Mˣ) → (a b : M) → a * b = ↑u → Commute a b → Mˣ
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.map_monotone : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {P Q : CategoryTheory.ObjectProperty C}, P ≤ Q → ∀ (F : CategoryTheory.Functor C D), P.map F ≤ Q.map F
-- Init.Data.Vector.Lemmas
Vector.countP_mk : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Array α} (h : xs.size = n),
  Vector.countP p (Vector.mk xs h) = Array.countP p xs
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- If the arrow set for a family of elements is actually a sieve (i.e. it is downward closed) then the
consistency condition can be simplified.
This is an equivalent condition, see `compatible_iff_sieveCompatible`.

This is the notion of "matching" given for families on sieves given in [MM92], Chapter III,
Section 4, Equation 1, and nlab: https://ncatlab.org/nlab/show/matching+family.
See also the discussion before Lemma C2.1.4 of [Elephant].
 -/
CategoryTheory.Presieve.FamilyOfElements.SieveCompatible : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} → {S : CategoryTheory.Sieve X} → CategoryTheory.Presieve.FamilyOfElements P S.arrows → Prop
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_toAddSubgroup : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  (Subgroup.toAddSubgroup H).relIndex (Subgroup.toAddSubgroup K) = H.relIndex K
-- Init.Data.List.Basic
List.erase.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (x : α), [].erase x = []
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.pairwise_toList_le : ∀ {α : Type u} {r : Std.Rci α} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α], List.Pairwise (fun a b => a ≤ b) r.toList
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_le_size_insertMany_list : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {l : List ((a : α) × β a)}, m.size ≤ (m.insertMany l).size
-- Mathlib.Analysis.Convex.Star
starConvex_iInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {x : E} {ι : Sort u_4} {s : ι → Set E},
  (∀ (i : ι), StarConvex 𝕜 x (s i)) → StarConvex 𝕜 x (⋂ i, s i)
-- Mathlib.Analysis.Matrix.Spectrum
/-- Unitary diagonalization of a Hermitian matrix.  -/
Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian),
  ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) (star hA.eigenvectorUnitary)) A =
    Matrix.diagonal (RCLike.ofReal ∘ hA.eigenvalues)
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.apply_eq_iff_symm_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) {x : M} {y : N}, e x = y ↔ x = e.symm y
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.cofinite_le_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.cofinite ≤ MeasureTheory.ae μ
-- Mathlib.Algebra.CharP.Lemmas
exists_add_pow_prime_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ},
  Nat.Prime p → ∀ (x y : R), ∃ r, (x + y) ^ p = x ^ p + y ^ p + ↑p * x * y * r
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Orientation.rotation_apply : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (x : V), (o.rotation θ) x = θ.cos • x + θ.sin • o.rightAngleRotation x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the sign of the angle between two vectors is nonzero, the vectors are not equal.  -/
Orientation.ne_of_oangle_sign_ne_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, (o.oangle x y).sign ≠ 0 → x ≠ y
-- Mathlib.Logic.Equiv.Sum
/-- Sum of types is commutative up to an equivalence. This is `Sum.swap` as an equivalence.  -/
Equiv.sumComm : (α : Type u_9) → (β : Type u_10) → α ⊕ β ≃ β ⊕ α
-- Mathlib.Order.Bounds.Basic
bddBelow_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, BddBelow (Set.Ioo b a)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.foldl_eq_foldl_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {δ : Type w} {f : δ → α → δ} {init : δ},
  Std.TreeSet.foldl f init t = Array.foldl f init t.toArray
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf_div_right : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Div α] [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] (s t : Finset α) (f : α → β), (s / t).inf f = t.inf fun y => s.inf fun x => f (x / y)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- A pushout cone is a colimit cocone if and only if the corresponding pullback cone
in the opposite category is a limit cone.  -/
CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          (c : CategoryTheory.Limits.PushoutCocone f g) →
            CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsLimit c.op
-- Mathlib.RingTheory.HopfAlgebra.Convolution
_private.Mathlib.RingTheory.HopfAlgebra.Convolution.0.LinearMap.«term𝑭» : Lean.ParserDescr