mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.MonoidLocalization.Away
AddSubmonoid.LocalizationMap.AwayMap.lift_eq : ∀ {A : Type u_4} [inst : AddCommMonoid A] (x : A) {B : Type u_5} [inst_1 : AddCommMonoid B]
  (F : AddSubmonoid.LocalizationMap.AwayMap x B) {C : Type u_6} [inst_2 : AddCommMonoid C] {g : A →+ C}
  (hg : IsAddUnit (g x)) (a : A), (AddSubmonoid.LocalizationMap.AwayMap.lift x F hg) (F a) = g a
-- Mathlib.Data.List.Basic
List.foldrM_eq_foldr : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] [LawfulMonad m] (f : α → β → m β) (b : β)
  (l : List α), List.foldrM f b l = List.foldr (fun a mb => mb >>= f a) (pure b) l
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- For a topological space `X` the compact coherentification is defined as:
`A` is open iff for all compact sets `B`, the intersection `A ∩ B` is open in `B`.  -/
CompactCoherentification.instTopologicalSpace : {X : Type u_1} → [TopologicalSpace X] → TopologicalSpace (CompactCoherentification X)
-- Std.Data.TreeMap.Basic
Std.TreeMap.instForInProdOfMonad : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → {m : Type w → Type w₂} → [Monad m] → ForIn m (Std.TreeMap α β cmp) (α × β)
-- Mathlib.Tactic.CrossRefAttribute
/-- The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or
uppercase letters.  -/
Mathlib.CrossRef.stacksTagNoAntiquot : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.hasKernels : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  CategoryTheory.Limits.HasKernels D
-- Mathlib.Analysis.Fourier.Notation
FourierInvSMul.fourierInv_smul : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} {inst : SMul R E} {inst_1 : SMul R F}
  {inst_2 : FourierTransformInv E F} [self : FourierInvSMul R E F] (r : R) (f : E),
  FourierTransformInv.fourierInv (r • f) = r • FourierTransformInv.fourierInv f
-- Mathlib.Control.Traversable.Basic
instTraversableOption : Traversable Option
-- Init.Data.SInt.Basic
/-- Converts 16-bit signed integers to word-sized signed integers that denote the same number. This conversion is lossless, because
`ISize` is either `Int32` or `Int64`.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.toISize : Int16 → ISize
-- Mathlib.Algebra.Star.RingQuot
RingQuot.Rel.star : ∀ {R : Type u} [inst : Semiring R] (r : R → R → Prop) [inst_1 : StarRing R],
  (∀ (a b : R), r a b → r (star a) (star b)) → ∀ ⦃a b : R⦄, RingQuot.Rel r a b → RingQuot.Rel r (star a) (star b)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
CategoryTheory.yonedaCommGrpGrpObj_obj_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : CategoryTheory.CommGrp C) (H : (CategoryTheory.Grp C)ᵒᵖ),
  ↑((CategoryTheory.yonedaCommGrpGrpObj G).obj H) = (Opposite.unop H ⟶ G.toGrp)
-- Mathlib.Data.PFunctor.Univariate.M
/-- Corecursor for the M-type defined by `F`.  -/
PFunctor.M.corec : {F : PFunctor.{uA, uB}} → {X : Type u_1} → (X → ↑F X) → X → F.M
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- `completeEquipartiteGraph r t` contains no edges when `r ≤ 1` or `t = 0`.  -/
SimpleGraph.completeEquipartiteGraph_eq_bot_iff : ∀ {r t : ℕ}, SimpleGraph.completeEquipartiteGraph r t = ⊥ ↔ r ≤ 1 ∨ t = 0
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.coe_toInteger : ∀ {K : Type u} [inst : Field K] {ζ : K} {k : ℕ} [inst_1 : NeZero k] (hζ : IsPrimitiveRoot ζ k), ↑hζ.toInteger = ζ
-- Init.Data.UInt.Bitwise
UInt8.toUInt16_xor : ∀ (a b : UInt8), (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16
-- Mathlib.Tactic.Widget.StringDiagram
/-- The list of nodes at the top of a string diagram.  -/
Mathlib.Tactic.BicategoryLike.topNodes : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    Mathlib.Tactic.BicategoryLike.WhiskerLeft →
      Mathlib.Tactic.BicategoryLike.CoherenceM ρ (List Mathlib.Tactic.Widget.StringDiagram.Node)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_union : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {fallback : β},
  Std.ExtDTreeMap.Const.getD (t₁.union t₂) k fallback =
    Std.ExtDTreeMap.Const.getD t₂ k (Std.ExtDTreeMap.Const.getD t₁ k fallback)
-- Mathlib.Order.Cover
/-- A characterisation of the `CovBy` relation in products of preorders. See `Pi.covBy_iff` for the
(more common) version in products of partial orders.
 -/
Pi.covBy_iff_antisymmRel : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Preorder (α i)] {a b : (i : ι) → α i},
  a ⋖ b ↔ ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 => x1 ≤ x2) (a j) (b j)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.continuous_sin : Continuous Complex.sin
-- Mathlib.Topology.Compactness.Lindelof
hasBasis_coLindelof : ∀ {X : Type u} [inst : TopologicalSpace X], (Filter.coLindelof X).HasBasis IsLindelof compl
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.ofList_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k : α}
  {v : β k} {tl : List ((a : α) × β a)}, Std.ExtDHashMap.ofList (⟨k, v⟩ :: tl) = (∅.insert k v).insertMany tl
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.State.congrCache : Lean.Meta.Simp.State → Lean.Meta.Simp.CongrCache
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_getModify_StateT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ : Type u}
  {post : σ → σ → Pred} {epost : EPred} (f : σ → σ),
  Std.Internal.Do.wp (getModify f) post epost = Std.Internal.Do.wp (MonadStateOf.modifyGet fun s => (s, f s)) post epost
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.Submartingale.eLpNorm_stoppedAbove_le' : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {r : ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    0 ≤ r →
      f 0 = 0 →
        (∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) →
          ∀ (i : ℕ),
            MeasureTheory.eLpNorm (MeasureTheory.stoppedAbove f r i) 1 μ ≤
              ↑(2 * μ Set.univ * ENNReal.ofReal (r + ↑R)).toNNReal
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.mul.go.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (m₁ : Lean.Grind.CommRing.Mon)
  (h_1 : (m₁ : Lean.Grind.CommRing.Mon) → motive m₁ Lean.Grind.CommRing.Mon.unit)
  (h_2 : (m₂ : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit m₂)
  (h_3 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)),
  (match m₁, Lean.Grind.CommRing.Mon.unit with
    | m₁, Lean.Grind.CommRing.Mon.unit => h_1 m₁
    | Lean.Grind.CommRing.Mon.unit, m₂ => h_2 m₂
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_3 pw₁ m₁ pw₂ m₂) =
    h_1 m₁
-- Mathlib.Logic.Equiv.Option
Equiv.optionIsSomeEquiv_symm_apply_coe : ∀ (α : Type u_4) (x : α), ↑((Equiv.optionIsSomeEquiv α).symm x) = some x
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Poly.toExpr.goTerm : ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Expr
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLinkLocation : Type
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles._auto_3) {Z : C}
  (h : (X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₁) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom
      (CategoryTheory.CategoryStruct.comp (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂) h) =
    CategoryTheory.CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles h
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.forget₂_commBialgCat_obj : ∀ {R : Type u} [inst : CommRing R] (A : CommHopfAlgCat R),
  (CategoryTheory.forget₂ (CommHopfAlgCat R) (CommBialgCat R)).obj A = CommBialgCat.of R ↑A
-- Mathlib.RingTheory.Binomial
Polynomial.ascPochhammer_smeval_eq_eval : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (n : ℕ),
  (ascPochhammer ℕ n).smeval r = Polynomial.eval r (ascPochhammer R n)
-- Std.Http.Data.Status
Std.Http.Status.badGateway.sizeOf_spec : sizeOf Std.Http.Status.badGateway = 1
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_subset_iff : ∀ {α : Type u_1} {s t u : Set α}, s \ t ⊆ u ↔ s ⊆ t ∪ u
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
RootPairingCat.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] [inst_1 : SizeOf R] (weight : Type v) [weightIsAddCommGroup : AddCommGroup weight]
  [weightIsModule : Module R weight] (coweight : Type v) [coweightIsAddCommGroup : AddCommGroup coweight]
  [coweightIsModule : Module R coweight] (index : Type v) (pairing : RootPairing index R weight coweight),
  sizeOf
      { weight := weight, weightIsAddCommGroup := weightIsAddCommGroup, weightIsModule := weightIsModule,
        coweight := coweight, coweightIsAddCommGroup := coweightIsAddCommGroup, coweightIsModule := coweightIsModule,
        index := index, pairing := pairing } =
    1 + sizeOf weight + sizeOf weightIsAddCommGroup + sizeOf weightIsModule + sizeOf coweight +
            sizeOf coweightIsAddCommGroup +
          sizeOf coweightIsModule +
        sizeOf index +
      sizeOf pairing
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.Simps.symm_apply.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (h : α ≃*o β), OrderMonoidIso.Simps.symm_apply h = ⇑h.symm
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- Imaginary part of a point of the unit disc.  -/
Complex.UnitClosedDisc.im : Complex.UnitClosedDisc → ℝ
-- Init.Data.List.Lemmas
List.mem_insert_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {b a : α} {l : List α}, a ∈ List.insert b l ↔ a = b ∨ a ∈ l
-- Mathlib.CategoryTheory.Preadditive.Transfer
/-- The preadditive structure on `C` induced by an equivalence `e : C ≌ D` makes `e.inverse` an
additive functor.  -/
CategoryTheory.Equivalence.additive_inverse_of_FullyFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive D] (e : C ≌ D), e.inverse.Additive
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Two affine maps are equal if they have equal linear maps and are equal at some point.  -/
AffineMap.ext_linear : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] {f g : P1 →ᵃ[k] P2},
  f.linear = g.linear → ∀ {p : P1}, f p = g p → f = g
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- If `G` acts freely on `X`, `X` is equivalent to the product of the quotient of `X` by `G` and
`G`.  -/
MulAction.selfEquivOrbitsQuotientProd : {G : Type u} →
  {X : Type v} →
    [inst : Group G] →
      [inst_1 : MulAction G X] → (∀ (b : X), MulAction.stabilizer G b = ⊥) → X ≃ Quotient (MulAction.orbitRel G X) × G
-- Lean.Elab.DefView
Lean.Elab.DefView.kind : Lean.Elab.DefView → Lean.Elab.DefKind
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reducePow : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.monotone_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N}, Monotone (Subsemigroup.comap f)
-- Std.Data.ExtDHashMap.Lemmas
/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the proof obligation
in the statement of `get_insertIfNew`.  -/
Std.ExtDHashMap.mem_of_mem_insertIfNew' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k}, a ∈ m.insertIfNew k v → ¬((k == a) = true ∧ k ∉ m) → a ∈ m
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.preimage_Ico : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a b : R},
  Nat.cast ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉₊ ⌈b⌉₊
-- Init.Data.String.Lemmas.Splits
String.Slice.splits_prev_endPos : ∀ {s : String.Slice} {h : s.endPos ≠ s.startPos},
  (s.endPos.prev h).Splits (s.sliceTo (s.endPos.prev h)).copy (String.singleton ((s.endPos.prev h).get ⋯))
-- Init.Data.Sum.Lemmas
Sum.elim_eq_iff : ∀ {α : Type u_1} {γ : Sort u_2} {β : Type u_3} {u u' : α → γ} {v v' : β → γ},
  Sum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v'
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.BohrMollerup.logGammaSeq_add_one : ∀ (x : ℝ) (n : ℕ),
  Real.BohrMollerup.logGammaSeq (x + 1) n =
    Real.BohrMollerup.logGammaSeq x (n + 1) + Real.log x - (x + 1) * (Real.log (↑n + 1) - Real.log ↑n)
-- Mathlib.Combinatorics.SimpleGraph.Prod
_private.Mathlib.Combinatorics.SimpleGraph.Prod.0.SimpleGraph.Walk.ofBoxProdLeft.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    {G : SimpleGraph α} →
      {H : SimpleGraph β} →
        {x : α × β} →
          (motive : (y : α × β) → (G □ H).Walk x y → Sort u_3) →
            (y : α × β) →
              (x_1 : (G □ H).Walk x y) →
                (Unit → motive x SimpleGraph.Walk.nil) →
                  ((y v : α × β) →
                      (h : (G □ H).Adj x v) → (w : (G □ H).Walk v y) → motive y (SimpleGraph.Walk.cons h w)) →
                    motive y x_1
-- Mathlib.Data.Quot
/-- Map a function `f : α → β → γ` that sends equivalent elements to equivalent elements
to a function `f : Quotient sa → Quotient sb → Quotient sc`.
Useful to define binary operations on quotients.  -/
Quotient.map₂ : {α : Sort u_1} →
  {β : Sort u_2} →
    {sa : Setoid α} →
      {sb : Setoid β} →
        {γ : Sort u_4} →
          {sc : Setoid γ} →
            (f : α → β → γ) →
              (∀ ⦃a₁ a₂ : α⦄, a₁ ≈ a₂ → ∀ ⦃b₁ b₂ : β⦄, b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂) →
                Quotient sa → Quotient sb → Quotient sc
-- Init.Data.BitVec.Lemmas
BitVec.toNat_lt_of_msb_false : ∀ {w : ℕ} {x : BitVec w}, x.msb = false → x.toNat < 2 ^ (w - 1)
-- Mathlib.RingTheory.Coalgebra.Basic
Prod.counit_apply : ∀ (R : Type u) (A : Type v) (B : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : AddCommMonoid B]
  [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : Coalgebra R A] [inst_6 : Coalgebra R B] (r : A × B),
  CoalgebraStruct.counit r = CoalgebraStruct.counit r.1 + CoalgebraStruct.counit r.2
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Step.continue.injEq : ∀ (e? e?_1 : Option Lean.Meta.Simp.Result),
  (Lean.Meta.Simp.Step.continue e? = Lean.Meta.Simp.Step.continue e?_1) = (e? = e?_1)
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.finCons : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ} {X : Fin (n + 1) → Type u_5}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (X i)] {f : α → X 0} {g : α → (j : Fin n) → X j.succ} {a : α}
  {s : Set α},
  ContinuousWithinAt f s a → ContinuousWithinAt g s a → ContinuousWithinAt (fun a => Fin.cons (f a) (g a)) s a
-- Mathlib.Algebra.BigOperators.Ring.List
List.dvd_sum : ∀ {R : Type u_5} [inst : NonUnitalSemiring R] {a : R} {l : List R}, (∀ x ∈ l, a ∣ x) → a ∣ l.sum
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_functor_obj_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (x : C),
  (CategoryTheory.WithTerminal.equivComma.functor.obj F).hom.app x =
    F.map (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of x))
-- Mathlib.Computability.TuringMachine.Tape
Turing.instInhabitedPointedMap : {Γ : Type u_1} → {Γ' : Type u_2} → [inst : Inhabited Γ] → [inst_1 : Inhabited Γ'] → Inhabited (Turing.PointedMap Γ Γ')
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- For finite intervals, see: `intervalIntegral.integral_deriv_mul_eq_sub`.  -/
MeasureTheory.integral_Iic_deriv_mul_eq_sub : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] {a : ℝ} {a' b' : A} {u v u' v' : ℝ → A}
  [CompleteSpace A],
  (∀ x ∈ Set.Iio a, HasDerivAt u (u' x) x) →
    (∀ x ∈ Set.Iio a, HasDerivAt v (v' x) x) →
      MeasureTheory.IntegrableOn (u' * v + u * v') (Set.Iic a) MeasureTheory.volume →
        Filter.Tendsto (u * v) (nhdsWithin a (Set.Iio a)) (nhds a') →
          Filter.Tendsto (u * v) Filter.atBot (nhds b') → ∫ (x : ℝ) in Set.Iic a, u' x * v x + u x * v' x = a' - b'
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mu_mul_zeta : ∀ (𝕜 : Type u_2) (α : Type u_5) [inst : AddCommGroup 𝕜] [inst_1 : MulOneClass 𝕜] [inst_2 : PartialOrder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] [inst_5 : DecidableLE α],
  IncidenceAlgebra.mu 𝕜 * IncidenceAlgebra.zeta 𝕜 = 1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k a : α} {v : β k},
  (t.insertIfNew k v).getKey! a = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKey! a
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.homEquiv_unop_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {Y : C}
  (h : F.RepresentableBy Y) {X : Cᵒᵖ} {X' : C} (f : Opposite.op X' ⟶ X) (g : X' ⟶ Y),
  h.homEquiv (CategoryTheory.CategoryStruct.comp f.unop g) =
    (CategoryTheory.ConcreteCategory.hom (F.map f)) (h.homEquiv g)
-- Mathlib.CategoryTheory.Limits.Lattice
/-- The limit cone over any functor from a finite diagram into a `SemilatticeInf` with `OrderTop`.
 -/
CategoryTheory.Limits.CompleteLattice.finiteLimitCone : {α : Type u} →
  {J : Type w} →
    [inst : CategoryTheory.SmallCategory J] →
      [CategoryTheory.FinCategory J] →
        [inst_2 : SemilatticeInf α] →
          [OrderTop α] → (F : CategoryTheory.Functor J α) → CategoryTheory.Limits.LimitCone F
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_target' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
  (e.trans e').target = e'.target ∩ ↑e'.symm ⁻¹' (e'.source ∩ e.target)
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Presieve.Arrows.FirstObj.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type t}
  [inst_1 : Small.{w, t} I] {X : I → C} {z₁ z₂ : CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X},
  z₁ = z₂ ↔
    ∀ (i : I),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun i => P.obj (Opposite.op (X i))) i)) z₁ =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun i => P.obj (Opposite.op (X i))) i)) z₂
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasure.mk.sizeOf_spec : ∀ {α : Type u_2} [inst : SizeOf α] (measureOf : Set α → ENNReal) (empty : measureOf ∅ = 0)
  (mono : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf s₁ ≤ measureOf s₂)
  (iUnion_nat :
    ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → measureOf (⋃ i, s i) ≤ ∑' (i : ℕ), measureOf (s i)),
  sizeOf { measureOf := measureOf, empty := empty, mono := mono, iUnion_nat := iUnion_nat } = 1 + sizeOf empty
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.isSuccLimit_omega : ∀ (o : Ordinal.{u_1}), Order.IsSuccLimit (Ordinal.omega o)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
/-- For vector spaces `E`, there is a canonical map `WeakDual 𝕜 E → StrongDual 𝕜 E` (the "identity"
mapping). It is a linear equivalence. Here it is implemented as the inverse of the linear
equivalence `StrongDual.toWeakDual` in the other direction.  -/
WeakDual.toStrongDual : {𝕜 : Type u_2} →
  {E : Type u_4} →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] →
              [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → WeakDual 𝕜 E ≃ₗ[𝕜] StrongDual 𝕜 E
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- **Alias** of `CategoryTheory.MorphismProperty.RespectsIso.inf`. -/
CategoryTheory.MorphismProperty.inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.MorphismProperty C) [P.RespectsIso]
  [Q.RespectsIso], (P ⊓ Q).RespectsIso
-- Mathlib.Algebra.Group.Prod
MulEquiv.uniqueProd_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Unique N] (a : N × M),
  MulEquiv.uniqueProd a = a.2
-- Init.Data.Range.Polymorphic.SInt
Int64.instRxiLawfulHasSize : Std.Rxi.LawfulHasSize Int64
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_comp : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂)
  (g : NormedAddGroupHom V₂ V₃), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The `LSeries` of the constant sequence `1` converges at `s` if and only if `re s > 1`.  -/
LSeriesSummable_one_iff : ∀ {s : ℂ}, LSeriesSummable 1 s ↔ 1 < s.re
-- Mathlib.Data.Nat.BitIndices
Nat.sum_map_two_pow_bitIndices : ∀ (n : ℕ), (List.map (fun i => 2 ^ i) n.bitIndices).sum = n
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.congr : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P → ∀ {s : Set H} {x : H} {f g : H → H'}, f =ᶠ[nhds x] g → P f s x → P g s x
-- Init.Data.Vector.Lemmas
Vector.foldl_toList : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} (f : β → α → β) {init : β} {xs : Vector α n},
  List.foldl f init xs.toList = Vector.foldl f init xs
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.markRecDecls.go : {pu : Lean.Compiler.LCNF.Purity} → Array (Lean.Compiler.LCNF.Decl pu) → StateM Lean.NameSet Unit