mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Induced
Rep.instIsRightAdjointResFunctor : ∀ {k : Type u} {G : Type v} {H : Type v'} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H),
  (Rep.resFunctor φ).IsRightAdjoint
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instIsAddApplyMeasure : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β},
  IsAddApply (ProbabilityTheory.Kernel α β) α (MeasureTheory.Measure β)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smulCommClass_finset : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : SMul α γ] [inst_2 : SMul β γ]
  [SMulCommClass α β γ], SMulCommClass α β (Finset γ)
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_ofBitVec : ∀ (n : BitVec 64), { toBitVec := n }.toBitVec = n
-- Mathlib.Combinatorics.SetFamily.Shatter
/-- Pajor's variant of the **Sauer-Shelah lemma**.  -/
Finset.card_le_card_shatterer : ∀ {α : Type u_1} [inst : DecidableEq α] (𝒜 : Finset (Finset α)), 𝒜.card ≤ 𝒜.shatterer.card
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isCyclic_of_surjective : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] {F : Type u_4} [hH : IsCyclic G']
  [inst_2 : FunLike F G' G] [MonoidHomClass F G' G] (f : F), Function.Surjective ⇑f → IsCyclic G
-- Mathlib.NumberTheory.ZetaValues
bernoulliFun_eval_one : ∀ (k : ℕ), bernoulliFun k 1 = bernoulliFun k 0 + if k = 1 then 1 else 0
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom_assoc : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X : CategoryTheory.GradedObject I C} {p : I → J} {j : J} [inst_1 : X.HasMap p] {c : X.CofanMapObjFun p j}
  (hc : CategoryTheory.Limits.IsColimit c) (i : I) (hi : p i = j) {Z : C} (h : X.mapObj p j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj c ⟨i, hi⟩)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.CofanMapObjFun.iso hc).hom h) =
    CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) h
-- Lean.Meta.Tactic.Apply
Lean.MVarId.exfalso : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₃_app_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C),
  (((CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₃ C).app X).app Y).app Z =
    (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.comm₁₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂),
  CategoryTheory.CategoryStruct.comp sq₁.f₁₂ self.τ₂ = CategoryTheory.CategoryStruct.comp self.τ₁ sq₂.f₁₂
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.simp.injEq : ∀ (k₁ : ℤ) (c₁ : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon)
  (c₂ : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (k₁_1 : ℤ) (c₁_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (k₂_1 : ℤ)
  (m₂_1 : Lean.Grind.CommRing.Mon) (c₂_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.simp k₁ c₁ k₂ m₂ c₂ =
      Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.simp k₁_1 c₁_1 k₂_1 m₂_1 c₂_1) =
    (k₁ = k₁_1 ∧ c₁ = c₁_1 ∧ k₂ = k₂_1 ∧ m₂ = m₂_1 ∧ c₂ = c₂_1)
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.instSMulNat : {R : Type u_1} →
  {E₁ : Type u_2} →
    {E₂ : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E₁] →
          [inst_2 : PartialOrder E₁] →
            [inst_3 : AddCommMonoid E₂] →
              [inst_4 : PartialOrder E₂] →
                [inst_5 : Module R E₁] → [inst_6 : Module R E₂] → [IsOrderedAddMonoid E₂] → SMul ℕ (E₁ →ₚ[R] E₂)
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inverseAssociator_obj_inr_inl : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : D),
  (CategoryTheory.sum.inverseAssociator C D E).obj (Sum.inr (Sum.inl X)) = Sum.inl (Sum.inr X)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_union_of_contains_eq_false_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        m₂.contains k = false →
          Std.DHashMap.Internal.Raw₀.Const.get? (m₁.union m₂) k = Std.DHashMap.Internal.Raw₀.Const.get? m₁ k
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.zero_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (G H : CategoryTheory.AddGrp C), CategoryTheory.InducedCategory.Hom.hom 0 = 0
-- Lean.Language.Basic
/-- Recursively triggers all `SnapshotTask.cancelTk?` in the reachable tree, asynchronously.
 -/
Lean.Language.SnapshotTask.cancelRec : {α : Type} → [Lean.Language.ToSnapshotTree α] → Lean.Language.SnapshotTask α → BaseIO Unit
-- Lean.Compiler.ExportAttr
/-- Exports a function under the provided unmangled symbol name. This can be used to refer to Lean
functions from other programming languages like C.

Example:
```
@[export lean_color_from_map]
def colorValue (properties : @& Std.HashMap String String) : UInt32 :=
  match properties["color"]? with
  | some "red" => 0xff0000
  | some "green" => 0x00ff00
  | some "blue" => 0x0000ff
  | _ => -1
```
C code:
```c
#include <lean/lean.h>

uint32_t lean_color_from_map(b_lean_obj_arg properties);

void fill_rectangle_from_map(b_lean_obj_arg properties) {
    uint32_t color = lean_color_from_map(properties);
    // ...
}
```

The opposite of this is `@[extern]`, which allows Lean functions to refer to functions from other
programming languages.
 -/
Lean.exportAttr : Lean.ParametricAttribute Lean.Name
-- Mathlib.GroupTheory.Perm.Centralizer
/-- `k : Subgroup.centralizer {g}` belongs to the kernel of `toPermHom g`
iff it commutes with each cycle of `g`  -/
Equiv.Perm.OnCycleFactors.mem_ker_toPermHom_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α) (k : ↥(Subgroup.centralizer {g})),
  k ∈ (Equiv.Perm.OnCycleFactors.toPermHom g).ker ↔ ∀ c ∈ g.cycleFactorsFinset, Commute (↑k) c
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galRestrict_symm_algebraMap_apply : ∀ (A : Type u_1) (K : Type u_2) {L : Type u_3} {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra B L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : Algebra.IsAlgebraic K L]
  (σ : B ≃ₐ[A] B) (x : B), ((galRestrict A K L B).symm σ) ((algebraMap B L) x) = (algebraMap B L) (σ x)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
/-- Measure version of `sum_le_preVariationFun_of_subset`.  -/
MeasureTheory.VectorMeasure.le_variation : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] (μ : MeasureTheory.VectorMeasure X V) {s : Set X},
  MeasurableSet s →
    ∀ {P : Finset (Set X)}, (∀ t ∈ P, t ⊆ s) → (↑P).PairwiseDisjoint id → ∑ p ∈ P, ‖μ p‖ₑ ≤ μ.variation s
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The centralizer of a set as a subalgebra.  -/
Subalgebra.centralizer : (R : Type u) →
  {A : Type v} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Set A → Subalgebra R A
-- Mathlib.Data.Nat.SuccPred
Nat.instPredSubOrder : PredSubOrder ℕ
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.isSupported_zero : ∀ {α : Type u} {s : Set α}, FreeCommRing.IsSupported 0 s
-- Mathlib.Order.Basic
instLinearOrderPEmpty : LinearOrder PEmpty.{u_5 + 1}
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
/-- **Alias** of the reverse direction of `Matrix.fromCols_one_isTotallyUnimodular_iff`. -/
Matrix.IsTotallyUnimodular.fromCols_one : ∀ {m : Type u_1} {n : Type u_3} {R : Type u_5} [inst : CommRing R] [inst_1 : DecidableEq m] (A : Matrix m n R),
  A.IsTotallyUnimodular → (A.fromCols 1).IsTotallyUnimodular
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- Coercion of an open partial homeomorphisms to a function. We don't use `e.toFun` because it is
actually `e.toPartialEquiv.toFun`, so `simp` will apply lemmas about `toPartialEquiv`.  -/
OpenPartialHomeomorph.toFun' : {X : Type u_1} →
  {Y : Type u_3} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → OpenPartialHomeomorph X Y → X → Y
-- Init.Data.Array.Find
Array.findSome?_isSome_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α},
  (Array.findSome? f xs).isSome = true ↔ ∃ x ∈ xs, (f x).isSome = true
-- Mathlib.Algebra.Order.SuccPred
strictMono_of_lt_add_one : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : One α]
  [inst_4 : SuccAddOrder α] [IsSuccArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMax a → f a < f (a + 1)) → StrictMono f
-- Mathlib.CategoryTheory.Yoneda
/-- An isomorphism between a representable `F` and a functor of the
form `C(-, F.reprX)`.  Note the components `F.reprW.app X`
definitionally have type `(X.unop ⟶ F.reprX) ≅ F.obj X`.
 -/
CategoryTheory.Functor.reprW : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) → [inst_1 : F.IsRepresentable] → CategoryTheory.yoneda.obj F.reprX ≅ F
-- Lean.Language.Basic
Lean.Language.instInhabitedSnapshotLeaf : Inhabited Lean.Language.SnapshotLeaf
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.star_add_self : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R],
  star a + a = 2 * ↑a.re + ↑c₂ * ↑a.imI
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.simplex_snd_succ : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d} {l : Fin d},
  SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ → (x.cast hd).simplex.2 l.succ = (x.cast hd).simplex.2 l.castSucc
-- Mathlib.Topology.Category.TopCat.Opens
/-- If two continuous maps `f g : X ⟶ Y` are equal,
then the functors `Opens Y ⥤ Opens X` they induce are isomorphic.
 -/
TopologicalSpace.Opens.mapIso : {X Y : TopCat} → (f g : X ⟶ Y) → f = g → (TopologicalSpace.Opens.map f ≅ TopologicalSpace.Opens.map g)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.exists_le_of_tendsto_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsDirectedOrder α] {u : α → β} [inst_2 : Preorder β],
  Filter.Tendsto u Filter.atTop Filter.atTop → ∀ (a : α) (b : β), ∃ a', a ≤ a' ∧ b ≤ u a'
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateWithAnchor : Type
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.category.injEq : ∀ (catName declName : Lean.Name) (behavior : Lean.Parser.LeadingIdentBehavior) (catName_1 declName_1 : Lean.Name)
  (behavior_1 : Lean.Parser.LeadingIdentBehavior),
  (Lean.Parser.ParserExtension.Entry.category catName declName behavior =
      Lean.Parser.ParserExtension.Entry.category catName_1 declName_1 behavior_1) =
    (catName = catName_1 ∧ declName = declName_1 ∧ behavior = behavior_1)
-- Mathlib.Geometry.Convex.Cone.Dual
_private.Mathlib.Geometry.Convex.Cone.Dual.0.PointedCone.«termR≥0» : Lean.ParserDescr
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.trans : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {l : Filter α} {u v w : α → β},
  Asymptotics.IsEquivalent l u v → Asymptotics.IsEquivalent l v w → Asymptotics.IsEquivalent l u w
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.isIndex_succ : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d) (l : Fin d),
  SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ ↔
    (x.cast hd).simplex.1 l.castSucc = k.castSucc ∧
      (x.cast hd).simplex.1 l.succ = k.succ ∧ (x.cast hd).simplex.2 l.succ = (x.cast hd).simplex.2 l.castSucc
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.evalN_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (n : ℕ) {X Y : CategoryTheory.SimplicialObject.Split C}
  (Φ : X ⟶ Y), (CategoryTheory.SimplicialObject.Split.evalN C n).map Φ = Φ.f n
-- Mathlib.Algebra.Algebra.Subalgebra.Operations
/-- The set of fixed points under a group action, as a subalgebra.  -/
FixedPoints.subalgebra : (A : Type u_1) →
  (B' : Type u_3) →
    [inst : CommSemiring A] →
      [inst_1 : Semiring B'] →
        [inst_2 : Algebra A B'] →
          (G : Type u_4) →
            [inst_3 : Monoid G] → [inst_4 : MulSemiringAction G B'] → [SMulCommClass G A B'] → Subalgebra A B'
-- Init.Data.String.Lemmas.Order
String.Pos.ofSlice_next : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {h' : p ≠ (s.slice p₀ p₁ h).endPos},
  String.Pos.ofSlice (p.next h') = (String.Pos.ofSlice p).next ⋯
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opFunctor_map_f : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {X Y : (HomologicalComplex V c)ᵒᵖ} (f : X ⟶ Y) (i : ι),
  ((HomologicalComplex.opFunctor V c).map f).f i = (f.unop.f i).op
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.eq_gcd_cert.match_1.splitter : (motive : Lean.Grind.CommRing.Poly → Sort u_1) →
  (p : Lean.Grind.CommRing.Poly) →
    ((k : ℤ) →
        (v : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k v p)) →
      ((g : ℤ) → motive (Lean.Grind.CommRing.Poly.num g)) → motive p
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionSemiHomClass.mk : ∀ {F : Type u_15} {M : outParam (Type u_16)} {N : outParam (Type u_17)} [inst : Monoid M] [inst_1 : Monoid N]
  {φ : outParam (M → N)} {R : outParam (Type u_18)} {S : outParam (Type u_19)} [inst_2 : Semiring R]
  [inst_3 : Semiring S] [inst_4 : DistribMulAction M R] [inst_5 : DistribMulAction N S] [inst_6 : FunLike F R S]
  [toDistribMulActionSemiHomClass : DistribMulActionSemiHomClass F φ R S] [toMonoidHomClass : MonoidHomClass F R S],
  MulSemiringActionSemiHomClass F φ R S
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstr.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.Linear.RingEqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof → Sort u} →
    (t : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) →
      ((t : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) → t.below → motive_1 t) →
        ((t : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof) → t.below → motive_2 t) → motive_1 t ×' t.below
-- Lean.Meta.PProdN
_private.Lean.Meta.PProdN.0.Lean.Meta.PProdN.unpack.go : Lean.Expr → ℕ → Array Lean.Expr → Lean.MetaM (Array Lean.Expr)
-- Batteries.Data.String.Lemmas
String.Pos.Raw.extract.go₂.eq_def : ∀ (a : List Char) (a_1 a_2 : String.Pos.Raw),
  String.Pos.Raw.extract.go₂ a a_1 a_2 =
    match a, a_1, a_2 with
    | [], x, x_1 => []
    | c :: cs, i, e => if i = e then [] else c :: String.Pos.Raw.extract.go₂ cs (i + c) e
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_swapEquiv_apply : ∀ {R : Type u_3} (c₁ c₃ : R) [inst : CommRing R] (t : QuaternionAlgebra R c₁ 0 c₃),
  ((QuaternionAlgebra.swapEquiv c₁ c₃) t).re = t.re
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabelPart.mk.sizeOf_spec : ∀ (value : String) (tooltip? : Option String) (location? : Option Lean.Elab.InlayHintLinkLocation),
  sizeOf { value := value, tooltip? := tooltip?, location? := location? } =
    1 + sizeOf value + sizeOf tooltip? + sizeOf location?
-- Mathlib.Data.Fin.Basic
Fin.lt_last_iff_ne_last : ∀ {n : ℕ} {a : Fin (n + 1)}, a < Fin.last n ↔ a ≠ Fin.last n
-- Mathlib.Topology.Algebra.Group.Extension
TopologicalAddGroup.IsSES.exact : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : AddGroup A] [inst_1 : AddGroup B] [inst_2 : AddGroup C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C},
  TopologicalAddGroup.IsSES φ ψ → Function.Exact ⇑φ ⇑ψ
-- Mathlib.Data.Sum.Interval
Sum.Iic_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : LocallyFiniteOrderBot β] (a : α), Finset.Iic (Sum.inl a) = Finset.map Function.Embedding.inl (Finset.Iic a)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instMax.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : SeparatelyContinuousMul G],
  OpenSubgroup.instMax = { max := fun U V => { toSubgroup := ↑U ⊔ ↑V, isOpen' := ⋯ } }
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.prod_range_natCast_sub : ∀ {R : Type u_4} [inst : CommRing R] (n k : ℕ), ∏ i ∈ Finset.range k, (↑n - ↑i) = ↑(∏ i ∈ Finset.range k, (n - i))
-- Mathlib.SetTheory.Lists
Lists'.ofList_subset : ∀ {α : Type u_1} {l₁ l₂ : List (Lists α)}, l₁ ⊆ l₂ → Lists'.ofList l₁ ⊆ Lists'.ofList l₂
-- Std.Data.TreeMap.Raw.Iterator
Std.DTreeMap.Raw.Const.toList.eq_1 : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Std.DTreeMap.Raw α (fun x => β) cmp),
  Std.DTreeMap.Raw.Const.toList t = Std.DTreeMap.Internal.Impl.Const.toList t.inner
-- Mathlib.Probability.Distributions.Gaussian.Fernique
/-- **Fernique's theorem**: for a Gaussian measure, there exists `C > 0` such that the function
`x ↦ exp (C * ‖x‖ ^ 2)` is integrable.  -/
ProbabilityTheory.IsGaussian.exists_integrable_exp_sq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [SecondCountableTopology E] [CompleteSpace E] (μ : MeasureTheory.Measure E) [ProbabilityTheory.IsGaussian μ],
  ∃ C, 0 < C ∧ MeasureTheory.Integrable (fun x => Real.exp (C * ‖x‖ ^ 2)) μ
-- Mathlib.Geometry.Manifold.StructureGroupoid
Pregroupoid.mk.injEq : ∀ {H : Type u_2} [inst : TopologicalSpace H] (property : (H → H) → Set H → Prop)
  (comp :
    ∀ {f g : H → H} {u v : Set H},
      property f u → property g v → IsOpen u → IsOpen v → IsOpen (u ∩ f ⁻¹' v) → property (g ∘ f) (u ∩ f ⁻¹' v))
  (id_mem : property id Set.univ)
  (locality :
    ∀ {f : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, ∃ v, IsOpen v ∧ x ∈ v ∧ property f (u ∩ v)) → property f u)
  (congr : ∀ {f g : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, g x = f x) → property f u → property g u)
  (property_1 : (H → H) → Set H → Prop)
  (comp_1 :
    ∀ {f g : H → H} {u v : Set H},
      property_1 f u → property_1 g v → IsOpen u → IsOpen v → IsOpen (u ∩ f ⁻¹' v) → property_1 (g ∘ f) (u ∩ f ⁻¹' v))
  (id_mem_1 : property_1 id Set.univ)
  (locality_1 :
    ∀ {f : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, ∃ v, IsOpen v ∧ x ∈ v ∧ property_1 f (u ∩ v)) → property_1 f u)
  (congr_1 : ∀ {f g : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, g x = f x) → property_1 f u → property_1 g u),
  ({ property := property, comp := comp, id_mem := id_mem, locality := locality, congr := congr } =
      { property := property_1, comp := comp_1, id_mem := id_mem_1, locality := locality_1, congr := congr_1 }) =
    (property = property_1)
-- Mathlib.ModelTheory.Order
/-- Any structure in an ordered language can be ordered correspondingly.  -/
FirstOrder.Language.leOfStructure : (L : FirstOrder.Language) → (M : Type w') → [L.IsOrdered] → [L.Structure M] → LE M
-- Init.Data.BitVec.Lemmas
BitVec.zero_append_zero : ∀ {v w : ℕ}, 0#v ++ 0#w = 0#(v + w)
-- Mathlib.Order.Defs.Unbundled
IsTrans.decide : ∀ {α : Sort u_1} {r : α → α → Prop} [inst : DecidableRel r] [IsTrans α r], IsTrans α fun a b => decide (r a b) = true
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFunDual_eq_charFun_map_one : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure E} [OpensMeasurableSpace E] (L : StrongDual ℝ E),
  MeasureTheory.charFunDual μ L = MeasureTheory.charFun (MeasureTheory.Measure.map (⇑L) μ) 1
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.leftComm_tmul : ∀ (R : Type uR) (A : Type uA) {M : Type uM} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid P] [inst_8 : Module A P]
  [inst_9 : AddCommMonoid Q] [inst_10 : Module R Q] [inst_11 : Module R P] [inst_12 : IsScalarTower R A P] (m : M)
  (p : P) (q : Q), (TensorProduct.AlgebraTensorModule.leftComm R A M P Q) (m ⊗ₜ[A] (p ⊗ₜ[R] q)) = p ⊗ₜ[A] (m ⊗ₜ[R] q)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instTopologicalSpace : {A : Type u_1} → [NonUnitalCStarAlgebra A] → {m : Type u_2} → {n : Type u_3} → TopologicalSpace (CStarMatrix m n A)
-- Mathlib.Algebra.Group.TransferInstance
Equiv.mul_def : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Mul β] (x y : α), x * y = e.symm (e x * e y)
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
/-- The bijection between `K ⟶ L.extend e` and the subtype of `K.restriction e ⟶ L`
consisting of morphisms `φ` such that `e.HasLift φ`.  -/
ComplexShape.Embedding.homEquiv : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          {C : Type u_3} →
            [inst : CategoryTheory.Category.{v_1, u_3} C] →
              [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
                [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                  (K : HomologicalComplex C c') →
                    (L : HomologicalComplex C c) → [inst_3 : e.IsRelIff] → (K ⟶ L.extend e) ≃ { φ // e.HasLift φ }
-- Mathlib.Order.Booleanisation
Booleanisation.liftLatticeHom_injective : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α], Function.Injective ⇑Booleanisation.liftLatticeHom
-- Mathlib.RingTheory.Nilpotent.GeometricallyReduced
Algebra.isGeometricallyReduced_field_iff : ∀ (k : Type u_3) (A : Type u_4) [inst : Field k] [inst_1 : Ring A] [inst_2 : Algebra k A],
  Algebra.IsGeometricallyReduced k A ↔ IsReduced (TensorProduct k (AlgebraicClosure k) A)
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.nearestPt_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α] [inst_2 : OpensMeasurableSpace α]
  (e : ℕ → α), MeasureTheory.SimpleFunc.nearestPt e 0 = MeasureTheory.SimpleFunc.const α (e 0)
-- Lean.Data.PersistentArray
Lean.PersistentArray.mul2Shift : USize → USize → USize
-- Mathlib.Order.WellFoundedSet
Set.isPWO_empty : ∀ {α : Type u_2} [inst : Preorder α], ∅.IsPWO
-- Aesop.Rule.Name
Aesop.instHashableScopeName : Hashable Aesop.ScopeName
-- Mathlib.Algebra.Homology.DerivedCategory.Linear
DerivedCategory.instLinearCochainComplexIntQ : ∀ (R : Type t) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : HasDerivedCategory C],
  CategoryTheory.Functor.Linear R DerivedCategory.Q
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.of_forall_constGet?_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [LawfulBEq α],
  (∀ (k : α), Std.DHashMap.Const.get? m₁ k = Std.DHashMap.Const.get? m₂ k) → m₁.Equiv m₂
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.sup_ker_aeval_le_ker_aeval_mul : ∀ {R : Type u} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : M →ₗ[R] M}
  {p q : Polynomial R}, ((Polynomial.aeval f) p).ker ⊔ ((Polynomial.aeval f) q).ker ≤ ((Polynomial.aeval f) (p * q)).ker
-- Mathlib.Algebra.BigOperators.Associated
Prod.associated_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] {x z : M × N},
  Associated x z ↔ Associated x.1 z.1 ∧ Associated x.2 z.2