mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapIsoWhiskerLeft_hom : ∀ {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] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (H : CategoryTheory.Functor C E) {Fᵣ Gᵣ : CategoryTheory.Functor D E'}
  (α : Fᵣ ≅ Gᵣ), (CategoryTheory.Join.mapIsoWhiskerLeft H α).hom = CategoryTheory.Join.mapWhiskerLeft H α.hom
-- Mathlib.Data.FunLike.IsApply
FunLike.intCast_eq_zsmul_one : ∀ {F' : Type u_4} {α : Type u_5} [inst : FunLike F' α α] [inst_1 : IntCast F'] [inst_2 : One F'] [inst_3 : SMul ℤ α]
  [inst_4 : SMul ℤ F'] [IsSMulApply ℤ F' α α] [IsIntCastApply F' α] [IsOneApplyEqSelf F' α] (n : ℤ), ↑n = n • 1
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MkEval.mk : {m : Type → Type} →
  [toMkEvalComp : Mathlib.Tactic.BicategoryLike.MkEvalComp m] →
    [toMkEvalWhiskerLeft : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft m] →
      [toMkEvalWhiskerRight : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight m] →
        [toMkEvalHorizontalComp : Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp m] →
          (Mathlib.Tactic.BicategoryLike.Mor₂ →
              Mathlib.Tactic.BicategoryLike.Mor₂ →
                Mathlib.Tactic.BicategoryLike.NormalExpr →
                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                    Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
            (Mathlib.Tactic.BicategoryLike.Mor₁ →
                Mathlib.Tactic.BicategoryLike.Mor₂ →
                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                    Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → m Lean.Expr) →
              (Mathlib.Tactic.BicategoryLike.Mor₂ →
                  Mathlib.Tactic.BicategoryLike.Mor₁ →
                    Mathlib.Tactic.BicategoryLike.NormalExpr →
                      Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → m Lean.Expr) →
                (Mathlib.Tactic.BicategoryLike.Mor₂ →
                    Mathlib.Tactic.BicategoryLike.Mor₂ →
                      Mathlib.Tactic.BicategoryLike.NormalExpr →
                        Mathlib.Tactic.BicategoryLike.NormalExpr →
                          Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
                  (Mathlib.Tactic.BicategoryLike.Atom → m Lean.Expr) →
                    (Mathlib.Tactic.BicategoryLike.Mor₂ →
                        Mathlib.Tactic.BicategoryLike.Mor₂ →
                          Mathlib.Tactic.BicategoryLike.Structural →
                            Mathlib.Tactic.BicategoryLike.NormalExpr →
                              Mathlib.Tactic.BicategoryLike.NormalExpr →
                                Mathlib.Tactic.BicategoryLike.NormalExpr →
                                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                                    Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
                      Mathlib.Tactic.BicategoryLike.MkEval m
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.tprod_eq_zero_mul : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {f : ℕ → G},
  Multipliable f → ∏' (b : ℕ), f b = f 0 * ∏' (b : ℕ), f (b + 1)
-- Init.Prelude
/-- Unpacks a `UInt8` into a `BitVec 8`. This function is overridden with a native implementation.
 -/
UInt8.toBitVec : UInt8 → BitVec 8
-- Mathlib.Algebra.Order.Group.PosPart
/-- The *negative part* of an element `a` in a lattice ordered group is `a⁻¹ ⊔ 1`, denoted `a⁻ᵐ `.
 -/
instLeOnePart : {α : Type u_1} → [Lattice α] → [DivInvMonoid α] → LeOnePart α
-- Lean.Parser.Basic
Lean.Parser.checkLinebreakBeforeFn : String → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.comp_assoc : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {𝒵 : CategoryTheory.BasedCategory 𝒮} {𝒜 : CategoryTheory.BasedCategory 𝒮}
  (F : CategoryTheory.BasedFunctor 𝒳 𝒴) (G : CategoryTheory.BasedFunctor 𝒴 𝒵) (H : CategoryTheory.BasedFunctor 𝒵 𝒜),
  (F.comp G).comp H = F.comp (G.comp H)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instOrdLocation.ord : Lean.Lsp.Location → Lean.Lsp.Location → Ordering
-- Mathlib.Data.SetLike.Fintype
/-- TODO: It should be possible to obtain a computable version of this for most
SetLike objects. If we add those instances, we should remove this one.  -/
SetLike.instFintype : {A : Type u_1} → {B : Type u_2} → [SetLike A B] → [Fintype B] → Fintype A
-- Mathlib.Analysis.Normed.MulAction
norm_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : Norm α] [inst_1 : Norm β] [inst_2 : SMul α β] [NormSMulClass α β] (r : α)
  (x : β), ‖r • x‖ = ‖r‖ * ‖x‖
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_succ : ∀ {n : ℕ}, (*...n + 1).toList = (*...n).toList ++ [n]
-- Mathlib.Data.Finset.Sups
Finset.sups_right_comm : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] (s t u : Finset α), s ⊻ t ⊻ u = s ⊻ u ⊻ t
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toArray_roc_eq_add : ∀ {m n fallback : ℤ} {i : ℕ}, i < (n - m).toNat → (m<...=n).toArray.getD i fallback = m + 1 + ↑i
-- Mathlib.Algebra.Polynomial.Bivariate
AdjoinRoot.evalEval.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {x y : R} {p : Polynomial (Polynomial R)} (h : Polynomial.evalEval x y p = 0),
  AdjoinRoot.evalEval h = AdjoinRoot.lift (Polynomial.evalRingHom x) y ⋯
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d}
  (h_1 : F.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h).inv)
      (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).inv (F.map h))
        (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv
          (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom) h_1)))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.leftUnitor_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M₁ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor M₁).hom.app X =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M₁.obj X)).hom
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} (not_mem : k ∉ t₂) {h' : k ∈ t₁.union t₂},
  Std.ExtDTreeMap.Const.get (t₁.union t₂) k h' = Std.ExtDTreeMap.Const.get t₁ k ⋯
-- Mathlib.Order.Comparable
instSymmCompRel : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Symm (CompRel r)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The 2-complement sequence `Wᶜ₂ : ℤ → R` for a normalised EDS `W : ℤ → R` that witnesses
`W(k) ∣ W(2 * k)`. In other words, `W(k) * Wᶜ₂(k) = W(2 * k)` for all `k ∈ ℤ`.

This is defined in terms of `preNormEDS`.  -/
complEDS₂ : {R : Type u_1} → [CommRing R] → R → R → R → ℤ → R
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.ι_chainComplexMap_f_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X Y : SSet) (f : X ⟶ Y) (R : C) {n : ℕ}
  (x : X.obj (Opposite.op { len := n })) {Z : C} (h : (Y.chainComplex R).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ιChainComplex x)
      (CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap f R).f n) h) =
    CategoryTheory.CategoryStruct.comp
      (Y.ιChainComplex ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x)) h
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.IsArtinianScheme.mk : ∀ {X : AlgebraicGeometry.Scheme} [toIsLocallyArtinian : AlgebraicGeometry.IsLocallyArtinian X]
  [toCompactSpace : CompactSpace ↥X], AlgebraicGeometry.IsArtinianScheme X
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**: if `f : ℝ → E` is integrable on `a..b` and `f` is
continuous at `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-f a` at `a`.  -/
intervalIntegral.integral_hasDerivAt_left : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
      ContinuousAt f a → HasDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-f a) a
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.ext'_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} {f g : E.Hom F},
  f = g ↔
    ∃ (hs : f.s₀ = g.s₀), ∀ (i : E.I₀), f.h₀ i = CategoryTheory.CategoryStruct.comp (g.h₀ i) (CategoryTheory.eqToHom ⋯)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.map_mk' : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (N : Subgroup G) [nN : N.Normal] (M : Subgroup H)
  [inst_2 : M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) (x : G),
  (QuotientGroup.map N M f h) ((QuotientGroup.mk' N) x) = ↑(f x)
-- Init.Data.SInt.Lemmas
Int8.mul_two : ∀ {a : Int8}, a * 2 = a + a
-- Mathlib.Data.Rat.Cast.Order
Rat.preimage_cast_Icc : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ),
  Rat.cast ⁻¹' Set.Icc ↑p ↑q = Set.Icc p q
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.comp_tendsto : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X} {ι' : Type u_4} {l' : Filter ι'} {φ : ι' → ι},
  IsFoelner G μ l F → Filter.Tendsto φ l' l → IsFoelner G μ l' (F ∘ φ)
-- Lean.Parser.Do
Lean.Parser.Term.termTry.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k₁ k₂ : α}
  (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t), t.get k₁ h₁ = t.get k₂ ⋯
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- (Implementation)
The canonical map `(W ×[X] Uᵢ) ×[W] (Uⱼ ×[Z] Y) ⟶ (Uⱼ ×[Z] Y) ×[X] Uᵢ = V j i` where `W` is
the glued fibred product.

This is used in `lift_comp_ι`.  -/
AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV : {X Y Z : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (f : X ⟶ Z) →
      (g : Y ⟶ Z) →
        [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] →
          (i j : 𝒰.I₀) →
            CategoryTheory.Limits.pullback
                (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
                ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι j) ⟶
              AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g j i
-- Mathlib.NumberTheory.NumberField.AdeleRing
/-- `𝔸[R, K]` is notation for `NumberField.AdeleRing R K`.  -/
NumberField.AdeleRing.«term𝔸[_,_]» : Lean.ParserDescr
-- Init.Prelude
/-- `Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 -/
Nonempty : Sort u → Prop
-- Mathlib.Order.SymmDiff
/-- **Alias** of `symmDiff_top`. -/
symmDiff_top' : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), symmDiff a ⊤ = ￢a
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_in_normalizer : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, (H.subgroupOf (Subgroup.normalizer ↑H)).Normal
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.recOnSingleAppend.eq_def : ∀ {motive : (n : ℕ) → Composition n → Sort u_1} {n : ℕ} (c : Composition n) (zero : motive 0 (Composition.ones 0))
  (single_append :
    (k n : ℕ) → (c : Composition n) → motive n c → motive (k + 1 + n) ((Composition.single (k + 1) ⋯).append c)),
  Composition.recOnSingleAppend c zero single_append =
    match n, c with
    | .(blocks.sum), { blocks := blocks, blocks_pos := blocks_pos, blocks_sum := ⋯ } =>
      match blocks, blocks_pos with
      | [], blocks_pos => zero
      | 0 :: tail, blocks_pos => ⋯.elim
      | k.succ :: l, blocks_pos =>
        single_append k l.sum { blocks := l, blocks_pos := ⋯, blocks_sum := ⋯ }
          (Composition.recOnSingleAppend { blocks := l, blocks_pos := ⋯, blocks_sum := ⋯ } zero single_append)
-- Mathlib.Order.Bounds.Image
/-- The image under an antitone function of a set which is bounded above is bounded below.  -/
AntitoneOn.map_bddAbove : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α},
  AntitoneOn f t → s ⊆ t → (upperBounds s ∩ t).Nonempty → BddBelow (f '' s)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_zero_right : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.singularPart 0 = μ
-- Init.Coe
/-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
or by double type ascription `((x : α) : β)`.  -/
CoeHTC.coe : {α : Sort u} → {β : Sort v} → [self : CoeHTC α β] → α → β
-- Lean.Parser.Extension
Lean.Parser.evalParserConstUnsafe : Lean.Name → optParam (Option Lean.Parser.ParserFn) none → Lean.Parser.ParserFn
-- Mathlib.AlgebraicTopology.ModelCategory.Opposite
HomotopicalAlgebra.instModelCategoryOpposite : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.ModelCategory C] → HomotopicalAlgebra.ModelCategory Cᵒᵖ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = (t.isEmpty || t.size == 1 && t.contains k)
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- `UnfoldBoundaries` stores abstraction boundaries for definitions that shouldn't be unfolded.  -/
Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries : Type
-- Init.Sym.Lemmas
Lean.Sym.and_eq_false_left : ∀ (a b : Prop), a = False → (a ∧ b) = False
-- Init.Data.UInt.Bitwise
UInt64.toUInt16_shiftLeft_mod : ∀ (a b : UInt64), (a <<< (b % 16)).toUInt16 = a.toUInt16 <<< b.toUInt16
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_val_zero' : ∀ {α : Type u} {m : ℕ} (h : 0 < m.succ) (x : α) (u : Fin m → α), Matrix.vecCons x u ⟨0, h⟩ = x
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_noncommProd : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {ι : Type u_2} {k : ι → Equiv.Perm α} {s : Finset ι}
  (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i => (k i).support
-- Lean.Meta.Sym.Simp.SimpM
/-- Runs a `SimpM` computation with the given methods and configuration.  -/
Lean.Meta.Sym.Simp.SimpM.run' : {α : Type} →
  Lean.Meta.Sym.Simp.SimpM α →
    optParam Lean.Meta.Sym.Simp.Methods { } → optParam Lean.Meta.Sym.Simp.Config { } → Lean.Meta.Sym.SymM α
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.iff.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ ψ : L.BoundedFormula α n), φ.iff ψ = φ.imp ψ ⊓ ψ.imp φ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_union! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁.union! m₂).get? k = (m₂.get? k).or (m₁.get? k)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- We can partition the square `s ×ˢ s` into shifted diagonals as such:
```
01234
40123
34012
23401
12340
```

The diagonals are given by the cycle `f`.
 -/
Finset.product_self_eq_disjiUnion_perm : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Finset α} (hf : f.IsCycleOn ↑s),
  s ×ˢ s = (Finset.range s.card).disjiUnion (fun k => Finset.map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s) ⋯
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
GenContFract.of_h_eq_intFractPair_seq1_fst_b : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K},
  (GenContFract.of v).h = ↑(GenContFract.IntFractPair.seq1 v).1.b
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `⊔` distributes over `⨅`.  -/
sup_sInf_eq : ∀ {α : Type u} [inst : Order.Coframe α] {s : Set α} {a : α}, a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.instIsStableUnderRetractsRetractClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  P.retractClosure.IsStableUnderRetracts
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt16.size ≤ n →
    (UInt16.ofNatClamp n).toUInt32 = UInt32.ofNatLT (UInt16.size - 1) UInt16.toUInt32_ofNatClamp_of_le._proof_1
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.instFintypeColoring : {V : Type u} → {G : SimpleGraph V} → {α : Type u_2} → [Fintype V] → [Fintype α] → Fintype (G.Coloring α)
-- Init.Data.UInt.BasicAux
/-- Converts a `UInt8` into the corresponding `Fin UInt8.size`.  -/
UInt8.toFin : UInt8 → Fin UInt8.size
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.arrows_eq_top_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}, S.arrows = ⊤ ↔ S = ⊤
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
/-- A bounded measurable function with compact support is in L^p.
This is the `ENNReal`-valued version of `HasCompactSupport.memLp_of_bound`.  -/
HasCompactSupport.memLp_of_enorm_bound : ∀ {E : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup E] {X : Type u_3} [inst_1 : TopologicalSpace X]
  [inst_2 : MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → E},
  HasCompactSupport f →
    MeasureTheory.AEStronglyMeasurable f μ →
      ∀ {C : ENNReal}, (∀ᵐ (x : X) ∂μ, ‖f x‖ₑ ≤ C) → C ≠ ⊤ → MeasureTheory.MemLp f p μ
-- Mathlib.Order.Category.OmegaCompletePartialOrder
/-- The pi-type is a limit cone for the product.  -/
ωCPO.HasProducts.isProduct : (J : Type v) → (f : J → ωCPO) → CategoryTheory.Limits.IsLimit (ωCPO.HasProducts.product f)
-- Mathlib.Order.Filter.Pi
Filter.coprodᵢ_neBot_iff' : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)},
  (Filter.coprodᵢ f).NeBot ↔ (∀ (i : ι), Nonempty (α i)) ∧ ∃ d, (f d).NeBot
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.backward.split : Lean.Option Bool
-- Mathlib.RingTheory.KrullDimension.Basic
Ring.krullDimLE_one_iff_of_isPrime_bot : ∀ {R : Type u_1} [inst : CommSemiring R] [⊥.IsPrime],
  Ring.KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- The restriction of a Cartesian-monoidal category along an object property that's closed under
finite products is Cartesian-monoidal.  -/
CategoryTheory.CartesianMonoidalCategory.fullSubcategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.CartesianMonoidalCategory C] →
      {P : CategoryTheory.ObjectProperty C} →
        [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] →
          [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)] →
            CategoryTheory.CartesianMonoidalCategory P.FullSubcategory
-- Lean.Meta.Tactic.Grind.AC.PP
_private.Lean.Meta.Tactic.Grind.AC.PP.0.Lean.Meta.Grind.AC.ppDiseqs? : Lean.Meta.Grind.AC.M✝ (Option Lean.MessageData)
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then for all `n : ℕ`,
`X ^ n * exp (v * X)` is integrable.  -/
ProbabilityTheory.integrable_pow_mul_exp_of_integrable_exp_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v : ℝ},
  t ≠ 0 →
    MeasureTheory.Integrable (fun ω => Real.exp ((v + t) * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp ((v - t) * X ω)) μ →
        ∀ (n : ℕ), MeasureTheory.Integrable (fun ω => X ω ^ n * Real.exp (v * X ω)) μ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.io.injEq : ∀ (hi hi_1 : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound),
  (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.io hi = Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.io hi_1) =
    (hi = hi_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∈ m₂ → (m₁ ∩ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.representative_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (Y : CategoryTheory.Subobject X),
  (CategoryTheory.Subobject.representative.obj Y).obj.left = CategoryTheory.Subobject.underlying.obj Y
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
algebraicIndependent_equiv : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (e : ι ≃ ι') {f : ι' → A}, AlgebraicIndependent R (f ∘ ⇑e) ↔ AlgebraicIndependent R f
-- Mathlib.LinearAlgebra.AffineSpace.Restrict
AffineMap.restrict.bijective : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] {E : AffineSubspace k P₁} [inst_7 : Nonempty ↥E]
  {φ : P₁ →ᵃ[k] P₂}, Function.Injective ⇑φ → Function.Bijective ⇑(φ.restrict ⋯)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_ofList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  l.contains k = false → (Std.HashSet.Raw.ofList l).get? k = none
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.eq_coroot_of_mem_corootSpace_of_two : ∀ {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] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K]
  (α : LieModule.Weight K (↥H) L) {x : ↥H}, x ∈ LieAlgebra.corootSpace ⇑α → α x = 2 → x = LieAlgebra.IsKilling.coroot α