mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- The commutator of two Lie derivations on a Lie algebra is a Lie derivation.  -/
LieDerivation.instBracket : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Bracket (LieDerivation R L L) (LieDerivation R L L)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) (a : B),
  (CategoryTheory.CategoryStruct.id F).app a = CategoryTheory.CategoryStruct.id (F.obj a)
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.instFaithfulElementsπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)),
  (CategoryTheory.CategoryOfElements.π F).Faithful
-- Mathlib.Analysis.Normed.Field.Basic
/-- If `s` is a subfield of a normed field `F`, then `s` is equipped with an induced normed
field structure.
 -/
SubfieldClass.toNormedField : {S : Type u_5} →
  {F : Type u_6} → [inst : SetLike S F] → [inst_1 : NormedField F] → [SubfieldClass S F] → (s : S) → NormedField ↥s
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The closed subspace of vectors orthogonal to a given subspace, denoted `Kᗮ`.  -/
ClosedSubmodule.orthogonal : {𝕜 : Type u_4} →
  {E : Type u_5} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → ClosedSubmodule 𝕜 E → ClosedSubmodule 𝕜 E
-- Mathlib.Data.Vector3
/-- "Curried" forall, i.e. `∀ x₁ ... xₙ, f [x₁, ..., xₙ]`.  -/
VectorAll : {α : Type u_1} → (k : ℕ) → (Vector3 α k → Prop) → Prop
-- Plausible.Shrinkable
Plausible.Char.shrinkable : Plausible.Shrinkable Char
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.a'.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {α : Type u_2} {β : Type u_3}
  (a : Matrix α β (NumberField.RingOfIntegers K)) (k : α) (l : β) (r : K →+* ℂ),
  NumberField.house.a'✝ K a k l r = ⇑((NumberField.house.newBasis✝ K).repr (a k l * (NumberField.house.newBasis✝ K) r))
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.natCast_coeff_zero : ∀ {n : ℕ} {R : Type u_1} [inst : Semiring R], (↑n).coeff 0 = ↑n
-- Mathlib.NumberTheory.ModularForms.Cusps
CongruenceSubgroup.strictWidthInfty_Gamma0 : ∀ (N : ℕ), (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)).strictWidthInfty = 1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m₁ m₂ : M), (CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ ∈ CliffordAlgebra.evenOdd Q 0
-- Mathlib.Algebra.Lie.Weights.Killing
LieModule.Weight.coe_neg : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] [inst_4 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_5 : H.IsCartanSubalgebra] [inst_6 : LieModule.IsTriangularizable K (↥H) L] {α : LieModule.Weight K (↥H) L},
  ⇑(-α) = -⇑α
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
/-- If `f : X ⟶ Y` and `g : Y ⟶ Z` are composable morphisms, this
is the connecting homomorphism `kernel g ⟶ cokernel f`.  -/
CategoryTheory.kernelCokernelCompSequence.δ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y Z : C} → (f : X ⟶ Y) → (g : Y ⟶ Z) → CategoryTheory.Limits.kernel g ⟶ CategoryTheory.Limits.cokernel f
-- Lean.Attributes
Lean.ParametricAttribute.mk.injEq : ∀ {α : Type} (attr : Lean.AttributeImpl)
  (ext : Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (List Lean.Name × Lean.NameMap α))
  (preserveOrder : Bool) (attr_1 : Lean.AttributeImpl)
  (ext_1 : Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (List Lean.Name × Lean.NameMap α))
  (preserveOrder_1 : Bool),
  ({ attr := attr, ext := ext, preserveOrder := preserveOrder } =
      { attr := attr_1, ext := ext_1, preserveOrder := preserveOrder_1 }) =
    (attr = attr_1 ∧ ext = ext_1 ∧ preserveOrder = preserveOrder_1)
-- Aesop.Tree.Data
Aesop.Rapp.instBEq : BEq Aesop.Rapp
-- Mathlib.Order.Interval.Set.ProjIcc
/-- Projection of `α` to the closed interval `[a, b]`.  -/
Set.projIcc : {α : Type u_1} → [inst : LinearOrder α] → (a b : α) → a ≤ b → α → ↑(Set.Icc a b)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Subsingleton.measurableSet : ∀ {α : Type u_1} {m : MeasurableSpace α} [Subsingleton α] {s : Set α}, MeasurableSet s
-- Init.Tactics
/-- Transforms `let` expressions into `have` expressions when possible.
- `let_to_have` transforms `let`s in the target.
- `let_to_have at h` transforms `let`s in the given local hypothesis.
 -/
Lean.Parser.Tactic.letToHave : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- `K.homology j` is the cokernel of `K.toCycles i j : K.X i ⟶ K.cycles j`
when `c.prev j = i`.  -/
HomologicalComplex.homologyIsCokernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            (i j : ι) →
              c.prev j = i →
                [inst_2 : K.HasHomology j] →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (K.homologyπ j) ⋯)
-- Mathlib.Algebra.Homology.QuasiIso
quasiIsoAt_of_comp_left : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L)
  (φ' : L ⟶ M) (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : M.HasHomology i]
  [hφ : QuasiIsoAt φ i] [hφφ' : QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i], QuasiIsoAt φ' i
-- Mathlib.Order.CompleteLattice.Defs
sSup_le_sSup : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s t : Set α}, s ⊆ t → sSup s ≤ sSup t
-- Mathlib.Topology.SeparatedMap
discreteTopology_iff_locallyInjective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (y : Y), DiscreteTopology X ↔ IsLocallyInjective fun x => y
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The natural transformation induced by `Pi.π`.  -/
CategoryTheory.Limits.Pi.functorπ : {α : Type w₂} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] →
        (a : α) → CategoryTheory.Limits.Pi.functor α ⟶ CategoryTheory.Pi.eval (fun x => C) a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insertMany!_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] [inst : Inhabited β],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      Std.DTreeMap.Internal.Impl.Const.get! (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k =
        (List.findSomeRev?
              (fun x =>
                match x with
                | (a, b) => if compare a k = Ordering.eq then some b else none)
              l).getD
          (Std.DTreeMap.Internal.Impl.Const.get! t k)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
OrderIso.map_csSup : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
  (e : α ≃o β) {s : Set α}, s.Nonempty → BddAbove s → e (sSup s) = ⨆ x, e ↑x
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.one_ev : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ GrpCat) {I : Type w'}
  (U : I → C) (i j : I) {T : C} (a : T ⟶ U i) (b : T ⟶ U j), CategoryTheory.PresheafOfGroups.OneCochain.ev 1 i j a b = 1
-- Mathlib.FieldTheory.Differential.Basic
Differential.logDeriv_multisetProd : ∀ {R : Type u_1} [inst : Field R] [inst_1 : Differential R] {ι : Type u_2} (s : Multiset ι) {f : ι → R},
  (∀ x ∈ s, f x ≠ 0) →
    Differential.logDeriv (Multiset.map f s).prod = (Multiset.map (fun x => Differential.logDeriv (f x)) s).sum
-- Mathlib.RingTheory.Nakayama
Submodule.eq_bot_of_set_smul_eq_of_subset_jacobson_annihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s : Set R}
  {N : Submodule R M}, N.FG → N = s • N → s ⊆ ↑N.annihilator.jacobson → N = ⊥
-- Init.Core
Lean.Syntax.node.inj : ∀ {info : Lean.SourceInfo} {kind : Lean.SyntaxNodeKind} {args : Array Lean.Syntax} {info_1 : Lean.SourceInfo}
  {kind_1 : Lean.SyntaxNodeKind} {args_1 : Array Lean.Syntax},
  Lean.Syntax.node info kind args = Lean.Syntax.node info_1 kind_1 args_1 →
    info = info_1 ∧ kind = kind_1 ∧ args = args_1
-- Init.Data.Bool
Bool.cond_not : ∀ {α : Sort u_1} (b : Bool) (t e : α), (bif !b then t else e) = bif b then e else t
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : IsTopologicalAddGroup N] [inst_8 : Fintype ι] [inst_9 : DecidableEq ι]
  (f : ContinuousMultilinearMap R (fun x => M) N),
  (ContinuousMultilinearMap.alternatization f).toContinuousMultilinearMap =
    ∑ σ, Equiv.Perm.sign σ • ContinuousMultilinearMap.domDomCongr σ f
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains'.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → (Unit → motive Ordering.eq) → motive x
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.comp_s₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {X Y Z : CategoryTheory.PreOneHypercover S}
  (f : X.Hom Y) (g : Y.Hom Z) {i j : X.I₀} (a : X.I₁ i j), (CategoryTheory.CategoryStruct.comp f g).s₁ a = g.s₁ (f.s₁ a)
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.FundamentalSequenceProp.match_1.eq_3 : ∀ (motive : Option ONote ⊕ (ℕ → ONote) → Sort u_1) (f : ℕ → ONote) (h_1 : Unit → motive (Sum.inl none))
  (h_2 : (a : ONote) → motive (Sum.inl (some a))) (h_3 : (f : ℕ → ONote) → motive (Sum.inr f)),
  (match Sum.inr f with
    | Sum.inl none => h_1 ()
    | Sum.inl (some a) => h_2 a
    | Sum.inr f => h_3 f) =
    h_3 f
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandInfo.mk.sizeOf_spec : ∀ (toElabInfo : Lean.Elab.ElabInfo), sizeOf { toElabInfo := toElabInfo } = 1 + sizeOf toElabInfo
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.transpose_circulant : ∀ {α : Type u_1} {n : Type u_3} [inst : SubtractionMonoid n] (v : n → α),
  (Matrix.circulant v).transpose = Matrix.circulant fun i => v (-i)
-- Init.Grind.Ordered.Module
Lean.Grind.ExistsAddOfLT.mk : ∀ {α : Type u} [inst : LT α] [inst_1 : Zero α] [inst_2 : Add α],
  (∀ {a b : α}, a < b → ∃ c, 0 < c ∧ b = a + c) → Lean.Grind.ExistsAddOfLT α
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
CategoryTheory.Limits.instIsIsoSigmaComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [inst_2 : CategoryTheory.Limits.HasCoproduct f]
  [inst_3 : CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G],
  CategoryTheory.IsIso (CategoryTheory.Limits.sigmaComparison G f)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.zip_nil_left : ∀ {α : Type u} {s : Stream'.Seq α}, Stream'.Seq.nil.zip s = Stream'.Seq.nil
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.«grind_filter_&&_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Measure.GiryMonad
AEMeasurable.ae_of_join : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {m : MeasureTheory.Measure (MeasureTheory.Measure α)} {f : α → β},
  AEMeasurable f m.join → ∀ᵐ (μ : MeasureTheory.Measure α) ∂m, AEMeasurable f μ
-- Mathlib.Analysis.Analytic.Constructions
FormalMultilinearSeries.radius_pi_eq_iInf : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)]
  {p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)}, (FormalMultilinearSeries.pi p).radius = ⨅ i, (p i).radius
-- Init.Data.Nat.Lemmas
Nat.succ_max_succ : ∀ (x y : ℕ), max x.succ y.succ = (max x y).succ
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.sum.sigmaFinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ι : Type u_4} [Finite ι] (μ : ι → MeasureTheory.Measure α)
  [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)], MeasureTheory.SigmaFinite (MeasureTheory.Measure.sum μ)
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_6.go : {i : Type u} →
  {b : Type v} →
    {motive_1 : Lean.Doc.Block i b → Sort u_1} →
      {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
        {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
          {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1} →
            {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
              {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
                {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} →
                  {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1} →
                    {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1} →
                      (t : List (Lean.Doc.Block i b)) →
                        ((t : Lean.Doc.Block i b) → t.below → motive_1 t) →
                          ((t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                              Lean.Doc.Block.below_1 t → motive_2 t) →
                            ((t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                Lean.Doc.Block.below_2 t → motive_3 t) →
                              ((t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t) →
                                ((t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                                    Lean.Doc.Block.below_4 t → motive_5 t) →
                                  ((t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                      Lean.Doc.Block.below_5 t → motive_6 t) →
                                    ((t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t) →
                                      ((t : Lean.Doc.ListItem (Lean.Doc.Block i b)) →
                                          Lean.Doc.Block.below_7 t → motive_8 t) →
                                        ((t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) →
                                            Lean.Doc.Block.below_8 t → motive_9 t) →
                                          motive_7 t ×' Lean.Doc.Block.below_6 t
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The map on valuation subrings to their nonunits is a dual order embedding.  -/
ValuationSubring.nonunitsOrderEmbedding : {K : Type u} → [inst : Field K] → ValuationSubring K ↪o (NonUnitalSubring K)ᵒᵈ
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMkSucc_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C (n + 1)}
  (α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯) (β : F.δ₀ ≅ G.δ₀)
  (w :
    CategoryTheory.CategoryStruct.comp (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯)
        (CategoryTheory.ComposableArrows.app' β.hom 0 ⋯) =
      CategoryTheory.CategoryStruct.comp α.hom (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⋯)),
  (CategoryTheory.ComposableArrows.isoMkSucc α β w).hom = CategoryTheory.ComposableArrows.homMkSucc α.hom β.hom w
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- The topological sum of `ZetaAsymptotics.term (n + 1) 1` over all `n : ℕ` is `1 - γ`. This is
proved by directly evaluating the sum of the first `N` terms and using the limit definition of `γ`.
 -/
ZetaAsymptotics.term_tsum_one : HasSum (fun n => ZetaAsymptotics.term (n + 1) 1) (1 - Real.eulerMascheroniConstant)
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_sdiff_eq_of_le : ∀ {V : Type u_1} {G H : SimpleGraph V}, H ≤ G → G.deleteEdges (G.edgeSet \ H.edgeSet) = H
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rankD_lt_rankMax : ∀ (self : Batteries.UnionFind) (i : ℕ), Batteries.UnionFind.rankD self.arr i < self.rankMax
-- Mathlib.NumberTheory.Real.Irrational
Irrational.ne_rat : ∀ {x : ℝ}, Irrational x → ∀ (q : ℚ), x ≠ ↑q
-- Mathlib.Order.Basic
/-- **Alias** of `Decidable.eq_or_lt_of_le`. -/
LE.le.eq_or_lt_dec : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α} [DecidableLE α], a ≤ b → a = b ∨ a < b
-- Init.Data.UInt.BasicAux
/-- Converts 16-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.toUInt64 : UInt16 → UInt64
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.geometricMeasure_singleton : ∀ {p : ↑unitInterval},
  p ≠ 0 → ∀ (n : ℕ), (ProbabilityTheory.geometricMeasure p) {n} = ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.zero_sub : ∀ (a : Ordinal.{u_4}), 0 - a = 0
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.left_tensor_tensorObj₃_ext : ∀ {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₃ : CategoryTheory.GradedObject I C} [inst_3 : X₂.HasTensor X₃]
  [inst_4 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] {j : I} {A : C} (Z : C)
  (f g :
    CategoryTheory.MonoidalCategoryStruct.tensorObj Z
        (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) j) ⟶
      A)
  [H : X₁.HasGoodTensorTensor₂₃ X₂ X₃] [hZ : CategoryTheory.GradedObject.HasLeftTensor₃ObjExt Z X₁ X₂ X₃ j],
  (∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z
            (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h))
          f =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z
            (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h))
          g) →
    f = g
-- Aesop.Builder.Unfold
Aesop.RuleBuilder.hasConst : Lean.Name → Lean.Expr → Bool
-- Mathlib.GroupTheory.IsPerfect
/-- A group `G` is perfect if `G` equals its commutator subgroup `⁅G, G⁆`.  -/
Group.IsPerfect : (G : Type u_1) → [Group G] → Prop
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_ratCast : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : Field R] [inst_2 : IsOrderedRing R] {q : ℚ},
  q ≠ 0 → ArchimedeanClass.mk ↑q = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {km : α},
        Std.Internal.List.minKey! l = km ↔
          Std.Internal.List.getKey? km l = some km ∧
            ∀ (k : α), Std.Internal.List.containsKey k l = true → (compare km k).isLE = true
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.map_C_leadingCoeff : ∀ {R : Type u} [inst : CommSemiring R] (p : Ideal R), (Ideal.map Polynomial.C p).leadingCoeff = p
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.IsReduced.red_iff_eq : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.IsReduced L₁ → (FreeAddGroup.Red L₁ L₂ ↔ L₂ = L₁)
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.instBEqIndGroupInfo.beq : Lean.Elab.Structural.IndGroupInfo → Lean.Elab.Structural.IndGroupInfo → Bool
-- Mathlib.RingTheory.Bezout
IsBezout.TFAE : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] [IsDomain R],
  [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.map_id : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n), s.map (AffineMap.id k P) ⋯ = s
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The natural degree of `cyclotomic n` is at most `totient n`.

If the base ring is nontrivial, then the degree is exactly `φ n`,
otherwise it's zero.  -/
Polynomial.natDegree_cyclotomic_le : ∀ {R : Type u_1} [inst : Ring R] {n : ℕ}, (Polynomial.cyclotomic n R).natDegree ≤ n.totient
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_left : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x z → IsCoprime y z → IsCoprime (x * y) z
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_unitOfList_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α},
  (Std.DHashMap.Const.unitOfList l).size ≤ l.length
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.ofLinearEquiv.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsAdicComplete I M], AdicCompletion.ofLinearEquiv I M = AdicCompletion.ofLinearEquiv I M
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.join.match_3.eq_1 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Stream'.Seq1 α)) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (a : α) → (s : Stream'.Seq α) → (S' : Stream'.Seq (Stream'.Seq1 α)) → motive (some ((a, s), S'))),
  (match none with
    | none => h_1 ()
    | some ((a, s), S') => h_2 a s S') =
    h_1 ()
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.powers_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R], HahnSeries.SummableFamily.powers 0 = HahnSeries.SummableFamily.single 0 1
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v))
  (X : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ),
  ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj X).fst = Opposite.op (Opposite.unop X).left
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_of_lt_of_one_le : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b c : α}, b < c → 1 ≤ a → b < c * a
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
_private.Mathlib.CategoryTheory.Abelian.FreydMitchell.0.CategoryTheory.Abelian.FreydMitchell.G : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.AsSmall C) (CategoryTheory.Ind (CategoryTheory.AsSmall C)ᵒᵖ)ᵒᵖ
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.PosNum.sub'.match_1.splitter : (motive : PosNum → PosNum → Sort u_1) →
  (x x_1 : PosNum) →
    ((a : PosNum) → motive a PosNum.one) →
      ((b : PosNum) → (b = PosNum.one → False) → motive PosNum.one b) →
        ((a b : PosNum) → motive a.bit0 b.bit0) →
          ((a b : PosNum) → motive a.bit0 b.bit1) →
            ((a b : PosNum) → motive a.bit1 b.bit0) → ((a b : PosNum) → motive a.bit1 b.bit1) → motive x x_1