mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.KrullDimension
/-- For an element of finite height there exists a series ending in that element of that height.  -/
Order.exists_series_of_height_eq_coe : ∀ {α : Type u_1} [inst : Preorder α] (a : α) {n : ℕ}, Order.height a = ↑n → ∃ p, RelSeries.last p = a ∧ p.length = n
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instSMul : {α : Type u} →
  {β : Type v} →
    {𝕜 : Type u_2} →
      [inst : PseudoMetricSpace 𝕜] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : PseudoMetricSpace β] →
            [inst_3 : Zero 𝕜] →
              [inst_4 : Zero β] → [inst_5 : SMul 𝕜 β] → [IsBoundedSMul 𝕜 β] → SMul 𝕜 (BoundedContinuousFunction α β)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_ι : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens),
  CategoryTheory.CategoryStruct.comp (f ∣_ U) U.ι =
    CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι f
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.integral_fun_sum : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {ι : Type u_2} {s : Finset ι} {f : ι → ℂ → E}
  {c : ℂ} {R : ℝ},
  (∀ i ∈ s, CircleIntegrable (f i) c R) → ∮ (z : ℂ) in C(c, R), ∑ i ∈ s, f i z = ∑ i ∈ s, ∮ (z : ℂ) in C(c, R), f i z
-- Init.Data.Bool
Bool.false_eq : ∀ (b : Bool), (false = b) = (b = false)
-- Mathlib.Topology.Algebra.OpenSubgroup
Subgroup.isClosed_of_isOpen : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousMul G] (U : Subgroup G),
  IsOpen ↑U → IsClosed ↑U
-- Init.Data.UInt.Basic
/-- Bitwise left shift for 64-bit unsigned integers. Usually accessed via the `<<<` operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.shiftLeft : UInt64 → UInt64 → UInt64
-- Mathlib.Data.DFinsupp.Interval
Finset.mem_dfinsupp_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (α i)] {s : Finset ι}
  {f : Π₀ (i : ι), α i} {t : (i : ι) → Finset (α i)} [inst_2 : (i : ι) → DecidableEq (α i)],
  f ∈ s.dfinsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
-- Init.Data.BitVec.Lemmas
/-- Non-overflowing signed division bounds when numerator is nonneg, denominator is nonneg.  -/
BitVec.toInt_ediv_toInt_lt_of_nonneg_of_nonneg : ∀ {w : ℕ} {x y : BitVec w}, 0 ≤ x.toInt → 0 ≤ y.toInt → x.toInt / y.toInt < 2 ^ (w - 1)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
/-- A walk in `G` which is fully contained in a set `s` of vertices lifts to a walk of `G[s]`.  -/
SimpleGraph.Walk.induce : {V : Type u} →
  {G : SimpleGraph V} →
    (s : Set V) →
      {u v : V} → (w : G.Walk u v) → (hw : ∀ x ∈ w.support, x ∈ s) → (SimpleGraph.induce s G).Walk ⟨u, ⋯⟩ ⟨v, ⋯⟩
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.aeval_injective_iff_of_isEmpty : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [IsEmpty σ] [inst_2 : CommSemiring S₁]
  [inst_3 : Algebra R S₁] {f : σ → S₁},
  Function.Injective ⇑(MvPolynomial.aeval f) ↔ Function.Injective ⇑(algebraMap R S₁)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.size_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β}
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.Internal.Impl.map f t).size = t.size
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstr.strict : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.HasZeroObject.from_zero_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C] {X : C}
  (f g : 0 ⟶ X), f = g
-- Lean.Meta.ProdN
/-- Given types `tᵢ`, return the tuple type `t₁ × t₂ × … × tₙ`.
For `n = 0`, return `PUnit` with the given level + 1.
 -/
Lean.Meta.mkProdN : Array Lean.Expr → Lean.Level → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.inter_subset_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] (self : Geometry.SimplicialComplex 𝕜 E) {s t : Finset E},
  s ∈ self.faces → t ∈ self.faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the sine of the opposite angle equals the
hypotenuse, version subtracting vectors.  -/
Orientation.norm_div_sin_oangle_sub_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → ‖y‖ / (o.oangle (x - y) x).sin = ‖x - y‖
-- Mathlib.Order.Lattice
Prod.instSemilatticeInf.eq_1 : ∀ (α : Type u) (β : Type v) [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β],
  Prod.instSemilatticeInf α β =
    { toPartialOrder := Prod.instPartialOrder α β, inf := fun a b => (a.1 ⊓ b.1, a.2 ⊓ b.2), inf_le_left := ⋯,
      inf_le_right := ⋯, le_inf := ⋯ }
-- Mathlib.Data.EReal.Operations
/-- `-a < b` if and only if `-b < a` on `EReal`.  -/
EReal.neg_lt_comm : ∀ {a b : EReal}, -a < b ↔ -b < a
-- Mathlib.Data.Finset.Preimage
Finset.preimage_empty : ∀ {α : Type u} {β : Type v} {f : α → β}, ∅.preimage f ⋯ = ∅
-- Mathlib.Combinatorics.Colex
Finset.equivBitIndices_apply : ∀ (n : ℕ), Finset.equivBitIndices n = n.bitIndices.toFinset
-- Mathlib.Topology.Perfect
/-- Given a perfect nonempty set in a T2.5 space, we can find two disjoint perfect subsets.
This is the main inductive step in the proof of the Cantor-Bendixson Theorem.  -/
Perfect.splitting : ∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α} [T25Space α],
  Perfect C →
    C.Nonempty → ∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
/-- The support of `G.deleteIncidenceSet x` is at most `1` less than the support of the simple
graph `G`.  -/
SimpleGraph.card_support_deleteIncidenceSet : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] {x : V},
  x ∈ G.support → Fintype.card ↑(G.deleteIncidenceSet x).support ≤ Fintype.card ↑G.support - 1
-- Lean.Meta.WHNF
Lean.Meta.whnfUntil : Lean.Expr → Lean.Name → Lean.MetaM (Option Lean.Expr)
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.RecArgCandidate.group : Lean.Elab.Structural.RecArgCandidate → Lean.Elab.Structural.IndGroupInst
-- Init.Data.List.Basic
/-- Applies a function to the corresponding elements of two lists, stopping at the end of the shorter
list.

`O(min |xs| |ys|)`.

Examples:
* `[1, 2].zipWith (· + ·) [5, 6] = [6, 8]`
* `[1, 2, 3].zipWith (· + ·) [5, 6, 10] = [6, 8, 13]`
* `[].zipWith (· + ·) [5, 6] = []`
* `[x₁, x₂, x₃].zipWith f [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]`
 -/
List.zipWith : {α : Type u} → {β : Type v} → {γ : Type w} → (α → β → γ) → List α → List β → List γ
-- Mathlib.Computability.PartrecCode
/-- There are only countably many partial recursive partial functions `ℕ →. ℕ`.  -/
Nat.Partrec.Code.instCountableSubtypePFunPartrec : Countable { f // Partrec f }
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A ⊗[R] B` is a field, then `A` and `B` are linearly disjoint.  -/
Subalgebra.LinearDisjoint.of_isField : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  IsField (TensorProduct R ↥A ↥B) → A.LinearDisjoint B
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_apply_eq' : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (x : 𝔸),
  (fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = fun n => (↑n.factorial)⁻¹ • x ^ n
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.exists_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] {x : G} {p : ↥(AddSubgroup.zmultiples x) → Prop}, (∃ g, p g) ↔ ∃ m, p ⟨m • x, ⋯⟩
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.hasInjectiveDimensionLT_of_ge : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n m : ℕ),
  n ≤ m → ∀ [CategoryTheory.HasInjectiveDimensionLT X n], CategoryTheory.HasInjectiveDimensionLT X m
-- Init.Data.Nat.Gcd
Nat.gcd_self_add_left : ∀ (m n : ℕ), (m + n).gcd m = n.gcd m
-- Mathlib.Algebra.Group.Hom.Defs
/-- Given a monoid homomorphism `f : M →* N` and an element `x : M`, if `x` has a right inverse,
then `f x` has a right inverse too. For elements invertible on both sides see `IsUnit.map`.  -/
MonoidHom.map_exists_right_inv : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : FunLike F M N]
  [MonoidHomClass F M N] (f : F) {x : M}, (∃ y, x * y = 1) → ∃ y, f x * y = 1
-- Init.Grind.Ring.Basic
Lean.Grind.CommSemiring.toSemiring : {α : Type u} → [self : Lean.Grind.CommSemiring α] → Lean.Grind.Semiring α
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- A linearly independent family of vectors `f` remains linearly independent when we substitute one
of the terms with a vector `m` provided there exists a non-zero divisor `r`, such that `r • m`
belongs to the span of `f` with non-zero-divisor coefficients.  -/
LinearIndependent.update : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : DecidableEq ι] [inst_1 : CommRing R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {f : ι → M},
  LinearIndependent R f →
    ∀ (i : ι) (m : M),
      (∃ r ∈ nonZeroDivisors R, ∃ l, l i ∈ nonZeroDivisors R ∧ r • m = (Finsupp.linearCombination R f) l) →
        LinearIndependent R (Function.update f i m)
-- Mathlib.Analysis.Complex.Liouville
_private.Mathlib.Analysis.Complex.Liouville.0.«term_̂» : Lean.TrailingParserDescr
-- Lean.Level
Lean.Level.PP.Result.imaxNode.inj : ∀ {a a_1 : List Lean.Level.PP.Result}, Lean.Level.PP.Result.imaxNode a = Lean.Level.PP.Result.imaxNode a_1 → a = a_1
-- Mathlib.Order.DirSupClosed
dirSupClosed_iff_forall_sSup : ∀ {α : Type u_1} {s : Set α} [inst : CompleteLattice α],
  DirSupClosed s ↔ ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → sSup d ∈ s
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- An embedding of a complete graph that witnesses the fact that the graph is not clique-free.  -/
SimpleGraph.topEmbeddingOfNotCliqueFree : {α : Type u_1} → {G : SimpleGraph α} → {n : ℕ} → ¬G.CliqueFree n → SimpleGraph.completeGraph (Fin n) ↪g G
-- Std.Data.ExtTreeMap.Basic
/-- Returns an array of all keys present in the tree map in ascending  order.  -/
Std.ExtTreeMap.keysArray : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → Array α
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.hasDimensionLT_of_epi : ∀ {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Epi f] (d : ℕ) [X.HasDimensionLT d], Y.HasDimensionLT d
-- Mathlib.Tactic.Sat.FromLRAT
/-- If `f` is unsatisfiable, and every `v` which agrees with `ps` implies `¬⟦f⟧_v → p`, then `p`.
Equivalently, there exists a valuation `v` which agrees with `ps`,
and every such valuation yields `¬⟦f⟧_v` because `f` is unsatisfiable.  -/
Sat.Fmla.refute : ∀ {p : Prop} {ps : List Prop} (f : Sat.Fmla),
  f.proof [] → (∀ (v : Sat.Valuation), v.implies (Sat.Fmla.reify v f p) ps 0) → p
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.unwantedUnicode.sizeOf_spec : ∀ (c : Char), sizeOf (Mathlib.Linter.TextBased.StyleError.unwantedUnicode✝ c) = 1 + sizeOf c
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.rangeRestrict_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), Function.Surjective ⇑f.rangeRestrict
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The `n`-th iterated derivative of a function from `𝕜` to `F`, as a function from `𝕜` to `F`.  -/
iteratedDeriv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type u_2} → [inst_1 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → ℕ → (𝕜 → F) → 𝕜 → F
-- Init.Data.List.Sort.Impl
/-- Variant of `splitAt`, that does not reverse the first list, i.e
`splitRevAt n l = ((l.take n).reverse, l.drop n)`.

This exists solely as an optimization for `mergeSortTR` and `mergeSortTR₂`,
and should not be used elsewhere.
 -/
List.MergeSort.Internal.splitRevAt : {α : Type u_1} → ℕ → List α → List α × List α
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.eq_of_notMem_uIoc_of_notMem_uIoc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ≤ c → b ≤ c → a ∉ Set.uIoc b c → b ∉ Set.uIoc a c → a = b
-- Mathlib.Data.Set.MulAntidiagonal
Set.AddAntidiagonal.finite_of_isPWO : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsCancelAdd α] [AddLeftMono α]
  [AddRightStrictMono α] {s t : Set α}, s.IsPWO → t.IsPWO → ∀ (a : α), (s.antidiagonal t a).Finite
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType : Type
-- Mathlib.Data.Finset.Insert
Finset.cons_induction : ∀ {α : Type u_3} {motive : Finset α → Prop},
  motive ∅ → (∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)) → ∀ (s : Finset α), motive s
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- The standard Riemannian metric on a vector space with an inner product, given by this inner
product on each tangent space.  -/
riemannianMetricVectorSpace : (F : Type u_4) →
  [inst : NormedAddCommGroup F] →
    [inst_1 : InnerProductSpace ℝ F] →
      Bundle.ContMDiffRiemannianMetric (modelWithCornersSelf ℝ F) ⊤ F fun x => TangentSpace (modelWithCornersSelf ℝ F) x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
/-- A binary coproduct of free sheaves of modules is the free sheaf
of modules on the sum type.  -/
SheafOfModules.freeSumIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            (I J_1 : Type u) → SheafOfModules.free I ⨿ SheafOfModules.free J_1 ≅ SheafOfModules.free (I ⊕ J_1)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.domCongr_toAlgHom : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (e : M ≃+ N),
  ↑(AddMonoidAlgebra.domCongr R A e) = AddMonoidAlgebra.mapDomainAlgHom R A ↑e
-- Mathlib.ModelTheory.Satisfiability
/-- A theory is `κ`-categorical if all models of size `κ` are isomorphic.  -/
Cardinal.Categorical : {L : FirstOrder.Language} → Cardinal.{w} → L.Theory → Prop
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Given a map `f : A →ₐ[R] B` and an element `a : A`, we may construct a map `Aₐ →ₐ[R] Bₐ`.  -/
Localization.awayMapₐ : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_4} →
      [inst_1 : CommSemiring A] →
        [inst_2 : Algebra R A] →
          {B : Type u_5} →
            [inst_3 : CommSemiring B] →
              [inst_4 : Algebra R B] → (f : A →ₐ[R] B) → (a : A) → Localization.Away a →ₐ[R] Localization.Away (f a)
-- Mathlib.Data.W.Cardinal
WType.cardinalMk_eq_sum_lift : ∀ {α : Type u} {β : α → Type v},
  Cardinal.mk (WType β) = Cardinal.sum fun a => Cardinal.mk (WType β) ^ Cardinal.lift.{u, v} (Cardinal.mk (β a))
-- Mathlib.RingTheory.Trace.Basic
/-- Given an `A`-algebra `B` and `b`, a `κ`-indexed family of elements of `B`, we define
`traceMatrix A b` as the matrix whose `(i j)`-th element is the trace of `b i * b j`.  -/
Algebra.traceMatrix : {κ : Type w} →
  (A : Type u) → {B : Type v} → [inst : CommRing A] → [inst_1 : CommRing B] → [Algebra A B] → (κ → B) → Matrix κ κ A
-- Mathlib.Computability.Primrec.List
_private.Mathlib.Computability.Primrec.List.0.List.lookup.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : α → List (α × β) → Sort u_3) →
      (x : α) →
        (x_1 : List (α × β)) →
          ((x : α) → motive x []) → ((a k : α) → (b : β) → (as : List (α × β)) → motive a ((k, b) :: as)) → motive x x_1
-- Init.System.Uri
/-- Replaces special characters in the given Uri with %HH Uri escapings.  -/
System.Uri.escapeUri : String → String
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The additive submonoid `M` of the `AddMonoid M`.  -/
AddSubmonoid.instTop : {M : Type u_1} → [inst : AddZeroClass M] → Top (AddSubmonoid M)
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.ofUpperSet_toUpperSet : ∀ {α : Type u_1} (a : α), Topology.WithUpperSet.ofUpperSet (Topology.WithUpperSet.toUpperSet a) = a
-- Lean.Elab.Tactic.Induction
/-- Returns `some #[alt_1, ..., alt_n]` if `alt` has multiple LHSs or if `alt` has no RHS.
If there is no RHS, it is filled in with a hole.
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.expandAlt? : Lean.Syntax → Option (Array Lean.Syntax)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofIsInitialRight_pt : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂)
  [inst_3 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.obj X₁)]
  [inst_4 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.obj Y₁)]
  (h : CategoryTheory.Limits.IsInitial X₂),
  (CategoryTheory.Functor.PushoutObjObj.ofIsInitialRight F f₁ f₂ h).pt = (F.obj X₁).obj Y₂
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_orthogonal_apply_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : Kᗮ.HasOrthogonalProjection] {v : E}, v ∈ K → Kᗮ.starProjection v = 0
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeriesAux.eq_2 : ∀ (G : Type u_1) [inst : Group G] (n : ℕ),
  Subgroup.upperCentralSeriesAux G n.succ = ⟨(Subgroup.upperCentralSeriesAux G n).fst.upperCentralSeriesStep, ⋯⟩
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.instHashableStained : Hashable Mathlib.Linter.Flexible.Stained✝
-- Lean.Elab.DefView
/-- Elaboration result, unless fatal exception occurred.  -/
Lean.Elab.DefParsed.headerProcessedSnap : Lean.Elab.DefParsed → Lean.Language.SnapshotTask (Option Lean.Elab.HeaderProcessedSnapshot)
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_symm_powMulEquiv : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} (f : Perfection M p) (n : ℕ),
  (Perfection.coeffMonoidHom M p n) ((powMulEquiv (Perfection M p) p).symm f) =
    (Perfection.coeffMonoidHom M p (n + 1)) f
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.mem_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {x : P}, x ∈ 0 ↔ x = 0
-- Mathlib.Algebra.Module.Injective
Module.injective_iff : ∀ (R : Type u) [inst : Ring R] (Q : Type v) [inst_1 : AddCommGroup Q] [inst_2 : Module R Q],
  Module.Injective R Q ↔
    ∀ ⦃X Y : Type v⦄ [inst_3 : AddCommGroup X] [inst_4 : AddCommGroup Y] [inst_5 : Module R X] [inst_6 : Module R Y]
      (f : X →ₗ[R] Y), Function.Injective ⇑f → ∀ (g : X →ₗ[R] Q), ∃ h, ∀ (x : X), h (f x) = g x
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Some other origin. `name` should not collide with the other types
for erasure to work correctly, and simp trace will ignore this lemma.
The other origins should be preferred if possible.
 -/
Lean.Meta.Origin.other : Lean.Name → Lean.Meta.Origin
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instLawfulEqOrdOffset : Std.LawfulEqOrd Std.Time.Minute.Offset
-- Lean.Server.InfoUtils
Lean.Elab.Info.tailPos? : Lean.Elab.Info → Option String.Pos.Raw
-- Mathlib.Order.CompactlyGenerated.Basic
/-- An element `k` is compact if any directed set with `LUB` (least upper bound) above
`k` has already got above `k` at some point in the set.
Such an element is also called "finite" or "S-compact".  -/
IsCompactElement : {α : Type u_1} → [PartialOrder α] → α → Prop
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.Integrable.of_integral_ne_zero : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → G}, ∫ (a : α), f a ∂μ ≠ 0 → MeasureTheory.Integrable f μ
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.orElse_ExceptT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [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}
  (x : ExceptT ε m α) (h : Unit → ExceptT ε m α) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred),
  ⦃ Std.Internal.Do.wp x post (EPost.Cons.mk✝ (fun x => Std.Internal.Do.wp (h ()) post epost) epost.tail) ⦄
    OrElse.orElse x h ⦃ post; epost ⦄
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsAEKolmogorovProcess.mk.congr_simp : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p p_1 : ℝ} (e_p : p = p_1) {q q_1 : ℝ} (e_q : q = q_1) {M M_1 : NNReal}
  (e_M : M = M_1) {P P_1 : MeasureTheory.Measure Ω} (e_P : P = P_1) (X X_1 : T → Ω → E) (e_X : X = X_1)
  (h : ProbabilityTheory.IsAEKolmogorovProcess X P p q M) (a a_1 : T),
  a = a_1 →
    ∀ (a_2 a_3 : Ω),
      a_2 = a_3 →
        ProbabilityTheory.IsAEKolmogorovProcess.mk X h a a_2 = ProbabilityTheory.IsAEKolmogorovProcess.mk X_1 ⋯ a_1 a_3
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.continuousAt_equivIco : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜]
  {x : AddCircle p}, x ≠ ↑a → ContinuousAt (⇑(AddCircle.equivIco p a)) x
-- Mathlib.Data.Finset.Preimage
Finset.preimage_compl' : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Fintype α] [inst_3 : Fintype β]
  {f : α → β} (s : Finset β) (hfc : Set.InjOn f (f ⁻¹' ↑sᶜ)) (hf : Set.InjOn f (f ⁻¹' ↑s)),
  sᶜ.preimage f hfc = (s.preimage f hf)ᶜ
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.comap_comap_center : ∀ {G : Type u} [inst : AddGroup G] {H₁ : AddSubgroup G} [inst_1 : H₁.Normal] {H₂ : AddSubgroup (G ⧸ H₁)}
  [inst_2 : H₂.Normal],
  AddSubgroup.comap (QuotientAddGroup.mk' H₁)
      (AddSubgroup.comap (QuotientAddGroup.mk' H₂) (AddSubgroup.center ((G ⧸ H₁) ⧸ H₂))) =
    AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.comap (QuotientAddGroup.mk' H₁) H₂))
      (AddSubgroup.center (G ⧸ AddSubgroup.comap (QuotientAddGroup.mk' H₁) H₂))
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffAt.restrict_scalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {n : WithTop ℕ∞} {𝕜' : Type u_3} [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜']
  [inst_7 : NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [inst_9 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F],
  ContDiffAt 𝕜' n f x → ContDiffAt 𝕜 n f x
-- Std.Data.ExtTreeMap.Lemmas
/-- Simpler variant of `getElem?_filter` when `LawfulEqCmp` is available.  -/
Std.ExtTreeMap.getElem?_filter' : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Bool} {k : α}, (Std.ExtTreeMap.filter f t)[k]? = Option.filter (f k) t[k]?
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Relations.isUniversal_total : ∀ {L : FirstOrder.Language} (r : L.Relations 2), FirstOrder.Language.BoundedFormula.IsUniversal r.total