mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Submodule.reflection_singleton_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (u v : E), (𝕜 ∙ u).reflection v = 2 • (inner 𝕜 u v / ↑‖u‖ ^ 2) • u - v
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.pentagon_inv : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C)
  [inst_3 : X₁.HasTensor X₂] [inst_4 : X₂.HasTensor X₃] [inst_5 : X₃.HasTensor X₄]
  [inst_6 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃]
  [inst_7 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)]
  [inst_8 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃).HasTensor X₄]
  [inst_9 : X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_10 :
    (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃).HasTensor
      X₄]
  [inst_11 :
    (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)).HasTensor
      X₄]
  [inst_12 :
    X₁.HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄)]
  [inst_13 :
    X₁.HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))]
  [inst_14 :
    (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_15 : X₁.HasGoodTensor₁₂Tensor X₂ X₃] [inst_16 : X₁.HasGoodTensorTensor₂₃ X₂ X₃]
  [inst_17 : X₁.HasGoodTensor₁₂Tensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄]
  [inst_18 : X₁.HasGoodTensorTensor₂₃ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄]
  [inst_19 : X₂.HasGoodTensor₁₂Tensor X₃ X₄] [inst_20 : X₂.HasGoodTensorTensor₂₃ X₃ X₄]
  [inst_21 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄]
  [inst_22 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄]
  [inst_23 : X₁.HasGoodTensor₁₂Tensor X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_24 : X₁.HasGoodTensorTensor₂₃ X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [X₁.HasTensor₄ObjExt X₂ X₃ X₄],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id X₁)
        (CategoryTheory.GradedObject.Monoidal.associator X₂ X₃ X₄).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.Monoidal.associator X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)
            X₄).inv
        (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).inv
          (CategoryTheory.CategoryStruct.id X₄))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)).inv
      (CategoryTheory.GradedObject.Monoidal.associator (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ X₄).inv
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_sub : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Sub M] (a b : M), ↑(a - b) = ↑a - ↑b
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidSearchFrom.brecOn : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {motive :
    (a : s.Pos) →
      (a_1 : List (String.Slice.Pattern.SearchStep s)) → String.Slice.Pattern.Model.IsValidSearchFrom pat a a_1 → Prop}
  {a : s.Pos} {a_1 : List (String.Slice.Pattern.SearchStep s)}
  (t : String.Slice.Pattern.Model.IsValidSearchFrom pat a a_1),
  (∀ (a : s.Pos) (a_2 : List (String.Slice.Pattern.SearchStep s))
      (t : String.Slice.Pattern.Model.IsValidSearchFrom pat a a_2),
      String.Slice.Pattern.Model.IsValidSearchFrom.below t → motive a a_2 t) →
    motive a a_1 t
-- Init.Data.Rat.Lemmas
Rat.add_nonneg : ∀ {a b : ℚ}, 0 ≤ a → 0 ≤ b → 0 ≤ a + b
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.restrict_empty : ∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α), (MeasureTheory.OuterMeasure.restrict ∅) m = 0
-- Mathlib.Tactic.ProdAssoc
Lean.Expr.instReprProdTree : Repr Lean.Expr.ProdTree
-- Mathlib.ModelTheory.ElementaryMaps
/-- Composition of elementary embeddings  -/
FirstOrder.Language.ElementaryEmbedding.comp : {L : FirstOrder.Language} →
  {M : Type u_1} →
    {N : Type u_2} →
      {P : Type u_3} →
        [inst : L.Structure M] →
          [inst_1 : L.Structure N] →
            [inst_2 : L.Structure P] → L.ElementaryEmbedding N P → L.ElementaryEmbedding M N → L.ElementaryEmbedding M P
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFree_one : ∀ {α : Type u_1} {G : SimpleGraph α}, G.CliqueFree 1 ↔ IsEmpty α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α}
  (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ Std.ExtDTreeMap.Const.insertMany t l},
  (Std.ExtDTreeMap.Const.insertMany t l).getKey k h' = t.getKey k ⋯
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddGroupWithOne : {ι : 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 ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → AddGroupWithOne (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] → AddGroupWithOne (DirectLimit G f)
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity holds if and only if all distances between points with different indices are
proportional.  -/
similar_iff_exists_pairwise_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Similar v₁ v₂ ↔ ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ => dist (v₁ i₁) (v₁ i₂) = ↑r * dist (v₂ i₁) (v₂ i₂)
-- Init.Data.Option.Basic
/-- Keeps an optional value only if it satisfies a monadic Boolean predicate.

If `Option` is thought of as a collection that contains at most one element, then `Option.filterM`
is analogous to `List.filterM`.
 -/
Option.filterM : {m : Type → Type u_1} → {α : Type} → [Applicative m] → (α → m Bool) → Option α → m (Option α)
-- Mathlib.MeasureTheory.Measure.Regular
/-- Any locally finite measure on a `σ`-compact pseudometrizable space is regular.  -/
MeasureTheory.Measure.Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure : ∀ {X : Type u_3} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] [SigmaCompactSpace X]
  [inst_3 : MeasurableSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsLocallyFiniteMeasure μ],
  μ.Regular
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_div : ∀ {Γ₀ : Type u_4} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_7} [inst_1 : DivisionRing R]
  (v : Valuation R Γ₀) (x y : R), v (x / y) = v x / v y
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) (n : ℕ),
  (AlgebraicTopology.DoldKan.N₁Γ₀.inv.app K).f.f n =
    (AlgebraicTopology.DoldKan.Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f n
-- Init.Data.Nat.Basic
Nat.repeat_eq_repeatTR : @Nat.repeat = @Nat.repeatTR
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The set of all Coxeter relations associated to the Coxeter matrix $M$.  -/
CoxeterMatrix.relationsSet : {B : Type u_1} → CoxeterMatrix B → Set (FreeGroup B)
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- Printable ASCII characters, not including whitespace.  -/
_private.Mathlib.Tactic.Linter.TextBased.UnicodeLinter.0.Mathlib.Linter.TextBased.UnicodeLinter.ASCII.printable : Char → Bool
-- Mathlib.Topology.Algebra.Monoid
tendsto_multiset_sum : ∀ {ι : Type u_1} {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] [ContinuousAdd M]
  {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι),
  (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) →
    Filter.Tendsto (fun b => (Multiset.map (fun c => f c b) s).sum) x (nhds (Multiset.map a s).sum)
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- The equivalence class of `μ`-almost-everywhere measurable functions associated to a continuous
map.  -/
ContinuousMap.toAEEqFun : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      (μ : MeasureTheory.Measure α) →
        [inst_1 : TopologicalSpace α] →
          [BorelSpace α] →
            [inst_3 : TopologicalSpace β] →
              [SecondCountableTopologyEither α β] → [TopologicalSpace.PseudoMetrizableSpace β] → C(α, β) → α →ₘ[μ] β
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {f : R}
  {p : PrimeSpectrum R},
  (PrimeSpectrum.basicOpen f).carrier = {p} → (IsLocalization.Away f S ↔ IsLocalization.AtPrime S p.asIdeal)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- Given a map `f : E [⋀^ι]→ₗ[𝕜] (F [⋀^ι']→ₗ[𝕜] G)` and an estimate
`H : ∀ m m', ‖f m m'‖ ≤ C * ∏ i, ‖m i‖ * ∏ i, ‖m' i‖`, upgrade all `AlternatingMap`s in the type
to `ContinuousAlternatingMap`s.  -/
AlternatingMap.mkContinuousAlternating : {𝕜 : Type u} →
  {E : Type wE} →
    {F : Type wF} →
      {G : Type wG} →
        {ι : Type v} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : SeminormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : SeminormedAddCommGroup G] →
                      [inst_6 : NormedSpace 𝕜 G] →
                        [inst_7 : Fintype ι] →
                          {ι' : Type u_1} →
                            [inst_8 : Fintype ι'] →
                              (f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G) →
                                (C : ℝ) →
                                  (∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) →
                                    E [⋀^ι]→L[𝕜] F [⋀^ι']→L[𝕜] G
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.sub : ∀ {x y : ℝ*} {r s : ℝ}, x.IsSt r → y.IsSt s → (x - y).IsSt (r - s)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.map.eq_1 : ∀ {R : Type u} [inst : CommRing R] (n : ℕ) {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  exteriorPower.map n f = exteriorPower.alternatingMapLinearEquiv ((exteriorPower.ιMulti R n).compLinearMap f)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Construct an isomorphism between categorical products (indexed by the same type)
from a family of isomorphisms between the factors.
 -/
CategoryTheory.Limits.Pi.mapIso : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : β → C} → [inst_1 : CategoryTheory.Limits.HasProductsOfShape β C] → ((b : β) → f b ≅ g b) → (∏ᶜ f ≅ ∏ᶜ g)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedSplitInfo : Inhabited Lean.Meta.Grind.SplitInfo
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_of_le_mul_left₀ : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [PosMulReflectLE α],
  0 < a → a ≤ a * b → 1 ≤ b
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.nsmul_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : AddCommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn f g s → ∀ (n : ℕ), AntivaryOn f (n • g) s
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft_shiftRight_eq_shiftLeft_of_le : ∀ {b c : ℕ}, c ≤ b → ∀ (a : ℤ), a <<< b >>> c = a <<< (b - c)
-- Mathlib.Topology.MetricSpace.Gluing
/-- A `Dist` instance on the disjoint union `Σ i, E i`.
We embed isometrically each factor, set the basepoints at distance 1, arbitrarily,
and say that the distance from `a` to `b` is the sum of the distances of `a` and `b` to
their respective basepoints, plus the distance 1 between the basepoints.
Since there is an arbitrary choice in this construction, it is not an instance by default.  -/
Metric.Sigma.instDist : {ι : Type u_1} → {E : ι → Type u_2} → [(i : ι) → MetricSpace (E i)] → Dist ((i : ι) × E i)
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination : ∀ (k : Type u) {G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] (g : G) [Finite G],
  (∀ (x : G), x ∈ Subgroup.zpowers g) →
    (Rep.Hom.hom ((Rep.leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (Rep.leftRegular k G))).range =
      ((Finsupp.linearCombination k fun x => 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
-- Std.Data.DHashMap.Raw
/-- Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of
`a ∈ m`.
 -/
Std.DHashMap.Raw.Const.get : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (m : Std.DHashMap.Raw α fun x => β) → (a : α) → a ∈ m → β
-- Mathlib.NumberTheory.Ostrowski
/-- If `f` is bounded and not trivial, then it is equivalent to a p-adic absolute value.  -/
Rat.AbsoluteValue.equiv_padic_of_bounded : ∀ {f : AbsoluteValue ℚ ℝ},
  f.IsNontrivial → (∀ (n : ℕ), f ↑n ≤ 1) → ∃! p, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (Rat.AbsoluteValue.padic p)
-- Mathlib.CategoryTheory.Triangulated.Rotate
/-- Given a triangle of the form:
```
      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
```
applying `invRotate` gives a triangle that can be thought of as:
```
        -h⟦-1⟧'     f       g
  Z⟦-1⟧  ───>  X  ───> Y  ───> Z
```
(note that this diagram doesn't technically fit the definition of triangle, as `Z⟦-1⟧⟦1⟧` is
not necessarily equal to `Z`, but it is isomorphic, by the `counitIso` of `shiftEquiv C 1`)
 -/
CategoryTheory.Pretriangulated.Triangle.invRotate : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        CategoryTheory.Pretriangulated.Triangle C → CategoryTheory.Pretriangulated.Triangle C
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- The bijection `h.ι ≃ h.I` when `h : A.PairingCore`.  -/
SSet.Subcomplex.PairingCore.equivI : {X : SSet} → {A : X.Subcomplex} → (h : A.PairingCore) → h.ι ≃ ↑h.I
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.instOne.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : One G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G],
  ContMDiffMap.instOne = { one := ContMDiffMap.const 1 }
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
/-- If the right cosets of `s` by elements of `t` are disjoint (but not necessarily distinct!), then
the size of `s` divides the size of `s * t`.  -/
Finset.card_dvd_card_mul_left : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] {s t : Finset α},
  ((fun b => Finset.image (fun a => a * b) s) '' ↑t).PairwiseDisjoint id → s.card ∣ (s * t).card
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.sizeLt : Lean.Parser.Parser
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.subset_union : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} [inst_1 : SetLike S G] [AddSubgroupClass S G] [inst : LE S]
  [IsConcreteLE S G] {H K L : S}, ↑H ⊆ ↑K ∪ ↑L ↔ H ≤ K ∨ H ≤ L
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.size_ric : ∀ {b : ℕ}, (*...=b).size = b + 1
-- Mathlib.CategoryTheory.Presentable.Type
/-- Given `X : Type u` and `κ : Cardinal.{u} X`, this is the preordered type
of subsets of `X` of cardinality `< κ`.  -/
HasCardinalLT.Set : Type u → Cardinal.{u} → Type (max 0 u)
-- Mathlib.Data.Finsupp.Option
/-- `Finsupp`s from `Option` are equivalent to
pairs of an element and a `Finsupp` on the original type.  -/
Finsupp.optionEquiv : {α : Type u_1} → {M : Type u_2} → [inst : Zero M] → (Option α →₀ M) ≃ M × (α →₀ M)
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.sSup_edge_eq : ∀ {V : Type u_1} (G : SimpleGraph V), sSup {x | ∃ u v, ∃ (_ : G.Adj u v), SimpleGraph.edge u v = x} = G
-- Mathlib.GroupTheory.Focal
/-- Lemma: The focal subgroup is contained in the commutator subgroup G'.  -/
Subgroup.focalSubgroup_le_commutator : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.focalSubgroup ≤ commutator G
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.rfindOpt : ∀ {n : ℕ} {f : List.Vector ℕ (n + 1) → ℕ},
  Nat.Partrec' ↑f → Nat.Partrec' fun v => Nat.rfindOpt fun a => Denumerable.ofNat (Option ℕ) (f (a ::ᵥ v))
-- Mathlib.Data.PNat.Factors
PNat.coeNat_factorMultiset : ∀ (n : ℕ+), n.factorMultiset.toNatMultiset = ↑(↑n).primeFactorsList
-- Lean.Level
Lean.Level.PP.Result.maxNode.injEq : ∀ (a a_1 : List Lean.Level.PP.Result), (Lean.Level.PP.Result.maxNode a = Lean.Level.PP.Result.maxNode a_1) = (a = a_1)
-- Mathlib.MeasureTheory.Integral.Average
/-- Average value of an `ℝ≥0∞`-valued function `f` w.r.t. the standard measure.

It is equal to `(volume univ)⁻¹ * ∫⁻ x, f x`, so it takes value zero if the space has infinite
measure. In a probability space, the average of any function is equal to its integral.

For the average on a set, use `⨍⁻ x in s, f x`, defined as `⨍⁻ x, f x ∂(volume.restrict s)`.  -/
MeasureTheory.«term⨍⁻_,_» : Lean.ParserDescr
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.mem_commutant_iff : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  {S : VonNeumannAlgebra H} {z : H →L[ℂ] H}, z ∈ S.commutant ↔ ∀ g ∈ S, g * z = z * g
-- Mathlib.Data.Num.Lemmas
PosNum.dvd : Dvd PosNum
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgEquiv.toAlgebraIso_hom : ∀ {R : Type u} [inst : CommRing R] {X₁ X₂ : Type v} {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁}
  {m₂ : Algebra R X₂} (e : X₁ ≃ₐ[R] X₂), e.toAlgebraIso.hom = AlgCat.ofHom ↑e
-- Mathlib.LinearAlgebra.Projection
LinearMap.isProj_iff_isIdempotentElem : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] (f : M →ₗ[S] M),
  (∃ p, LinearMap.IsProj p f) ↔ IsIdempotentElem f
-- Mathlib.Data.Finmap
Finmap.ext_iff : ∀ {α : Type u} {β : α → Type v} {s t : Finmap β}, s = t ↔ s.entries = t.entries
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- Generalized eigenspaces for exponents at least `finrank K V` are equal to each other.  -/
Module.End.genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  (f : Module.End R M) (μ : R) {k : ℕ},
  f.maxUnifEigenspaceIndex μ ≤ k → (f.genEigenspace μ) ↑k = (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_nat_add : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddCommMonoidWithOne G]
  [inst_2 : AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ) (x : G), f (↑n + x) = f x + ↑n
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.inf_N : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (F F' : I.Filtration M), (F ⊓ F').N = F.N ⊓ F'.N
-- Init.Data.List.Count
List.count_append : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l₁ l₂ : List α}, List.count a (l₁ ++ l₂) = List.count a l₁ + List.count a l₂
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map : ∀ {B : Type u₁} [inst : Quiver B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (F : B ⥤q C)
  {X Y : CategoryTheory.FreeBicategory B} (a : X ⟶ Y),
  (CategoryTheory.FreeBicategory.lift F).map a = CategoryTheory.FreeBicategory.liftHom F a
-- Mathlib.Data.ENNReal.Inv
OrderIso.invENNReal_symm_apply : ∀ (a : ENNRealᵒᵈ), OrderIso.invENNReal.symm a = (OrderDual.ofDual a)⁻¹
-- Mathlib.Data.Quot
/-- A version of `Quotient.liftOn₂` taking `{s₁ : Setoid α} {s₂ : Setoid β}` as implicit arguments
instead of instance arguments.  -/
Quotient.liftOn₂' : {α : Sort u_1} →
  {β : Sort u_2} →
    {γ : Sort u_3} →
      {s₁ : Setoid α} →
        {s₂ : Setoid β} →
          Quotient s₁ →
            Quotient s₂ →
              (f : α → β → γ) → (∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), s₁ a₁ b₁ → s₂ a₂ b₂ → f a₁ a₂ = f b₁ b₂) → γ
-- Mathlib.Logic.Function.Basic
/-- g factors through f : `f a = f b → g a = g b`  -/
Function.FactorsThrough : {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → (α → γ) → (α → β) → Prop
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.lim_le_one : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (x : X), c.lim x ≤ 1
-- Mathlib.CategoryTheory.Preadditive.Projective.Preserves
/-- See `Functor.projective_obj` for a variant taking `Projective X` as a typeclass argument.  -/
CategoryTheory.Functor.projective_obj_of_projective : ∀ {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.PreservesProjectiveObjects] {X : C},
  CategoryTheory.Projective X → CategoryTheory.Projective (F.obj X)
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.innerContent_pos_of_is_mul_left_invariant : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : Group G]
  [inst_2 : IsTopologicalGroup G],
  (∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g * x) ⋯ K) = μ K) →
    ∀ (K : TopologicalSpace.Compacts G),
      μ K ≠ 0 → ∀ (U : TopologicalSpace.Opens G), (↑U).Nonempty → 0 < μ.innerContent U
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.coordChange_apply : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
  (a : VectorPrebundle R F E) {e e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj}
  (he : e ∈ a.pretrivializationAtlas) (he' : e' ∈ a.pretrivializationAtlas) {b : B},
  b ∈ e.baseSet ∩ e'.baseSet → ∀ (v : F), (a.coordChange he he' b) v = (↑e' ⟨b, e.symm b v⟩).2
-- Mathlib.Analysis.Calculus.Deriv.Comp
derivWithin_comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {s' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'},
  DifferentiableWithinAt 𝕜' h₂ s' (h x) →
    DifferentiableWithinAt 𝕜 h s x →
      Set.MapsTo h s s' → derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
-- Lean.Structure
Lean.instInhabitedStructureDescr : Inhabited Lean.StructureDescr
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.subalgebraNontrivial : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [Nontrivial A],
  Nontrivial (Subalgebra R (Polynomial A))