mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- In a category with a terminal object and pullbacks,
a product of objects `X` and `Y` is isomorphic to a pullback.  -/
prodIsoPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasTerminal C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        (X Y : C) →
          [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y] →
            X ⨯ Y ≅
              CategoryTheory.Limits.pullback (CategoryTheory.Limits.terminal.from X)
                (CategoryTheory.Limits.terminal.from Y)
-- Mathlib.Algebra.Ring.CentroidHom
_private.Mathlib.Algebra.Ring.CentroidHom.0.CentroidHom.termL_1 : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.snd_mem_tail_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, ¬p.Nil → p.snd ∈ p.support.tail
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.X_ne_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [Nontrivial R] (s : σ), MvPolynomial.X s ≠ 0
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
IsBoundedBilinearMap.differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {b : E × F → G},
  IsBoundedBilinearMap 𝕜 b → ∀ (p : E × F), DifferentiableAt 𝕜 b p
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
/-- If `±‖T‖` are not in the spectrum, then `|T.rayleighQuotient x|` doesn't reach `‖T‖`.  -/
ContinuousLinearMap.abs_rayleighQuotient_le_of_norm_mem_resolventSet : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) [Nontrivial E],
  (algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T →
    -(algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T → ∃ ε > 0, ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - ε
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β k},
  (t.insertIfNew k v).minKey! = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integer.not_isUnit_iff_valuation_lt_one : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {x : ↥v.integer}, ¬IsUnit x ↔ v ↑x < 1
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.function.sizeOf_spec : ∀ (thm : Mathlib.Meta.FunProp.FunctionTheorem), sizeOf (Mathlib.Meta.FunProp.Theorem.function thm) = 1 + sizeOf thm
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.unzero.eq_1 : ∀ {α : Type u} (x_2 : α) (x_3 : ↑x_2 ≠ 0), WithZero.unzero x_3 = x_2
-- Mathlib.Topology.Defs.Basic
/-- A function between topological spaces is continuous if the preimage
of every open set is open. Registered as a structure to make sure it is not unfolded by Lean.  -/
Continuous : {X : Type u} → {Y : Type v} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop
-- Mathlib.Algebra.Group.Action.Defs
/-- An instance of `VAddAssocClass M N α` states that the additive action of `M` on `α` is
determined by the additive actions of `M` on `N` and `N` on `α`.  -/
VAddAssocClass : (M : Type u_9) → (N : Type u_10) → (α : Type u_11) → [VAdd M N] → [VAdd N α] → [VAdd M α] → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- The image of a binary bicone under a functor.  -/
CategoryTheory.Functor.mapBinaryBicone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              [F.PreservesZeroMorphisms] →
                {X Y : C} →
                  CategoryTheory.Limits.BinaryBicone X Y → CategoryTheory.Limits.BinaryBicone (F.obj X) (F.obj Y)
-- Mathlib.GroupTheory.GroupAction.FixedPoints
MulAction.minimalPeriod_eq_one_iff_fixedBy : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a : α} {g : G},
  Function.minimalPeriod (fun x => g • x) a = 1 ↔ a ∈ MulAction.fixedBy α g
-- Mathlib.Analysis.Convex.Between
/-- Suppose lines from two vertices of a triangle to interior points of the opposite side meet at
`p`. Then `p` lies in the interior of the first (and by symmetry the other) segment from a
vertex to the point on the opposite side.  -/
sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] [Module.IsTorsionFree R V]
  {t : Affine.Triangle R P} {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    ∀ {p₁ p₂ p : P},
      Sbtw R (t.points i₂) p₁ (t.points i₃) →
        Sbtw R (t.points i₁) p₂ (t.points i₃) →
          p ∈ line[R, t.points i₁, p₁] → p ∈ line[R, t.points i₂, p₂] → Sbtw R (t.points i₁) p p₁
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.op_smul_finset_subset_mul : ∀ {α : Type u_2} [inst : Mul α] [inst_1 : DecidableEq α] {s t : Finset α} {a : α}, a ∈ t → MulOpposite.op a • s ⊆ s * t
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.instPartialOrder : {α : Type u_2} → [inst : TopologicalSpace α] → PartialOrder (TopologicalSpace.IrreducibleCloseds α)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.simplicialEvalσ_of_le_mem : ∀ (L : List ℕ) (j : ℕ), (∀ k ∈ L, j ≤ k) → SimplexCategoryGenRel.simplicialEvalσ L j = j
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_of_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G),
  (∀ (U : Cᵒᵖ), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.app U))) →
    CategoryTheory.Presheaf.IsLocallySurjective J f
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  {R : CategoryTheory.InjectiveResolution X} {X' : C} {R' : CategoryTheory.InjectiveResolution X'} {f : X ⟶ X'}
  (φ : R.Hom R' f),
  CategoryTheory.CategoryStruct.comp R.ι' φ.hom' =
    CategoryTheory.CategoryStruct.comp ((CochainComplex.singleFunctor C 0).map f) R'.ι'
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec_closedPoint : ∀ {R S : CommRingCat} [inst : IsLocalRing ↑R] [inst_1 : IsLocalRing ↑S] {f : R ⟶ S}
  [IsLocalHom (CommRingCat.Hom.hom f)],
  (AlgebraicGeometry.Spec.map f) (IsLocalRing.closedPoint ↑S) = IsLocalRing.closedPoint ↑R
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_exact : Bool → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Mathlib.Tactic.Attr.Register
/-- The simpset `zify_simps` is used by the tactic `zify` to move expressions from `ℕ` to `ℤ`
which gives a well-behaved subtraction.  -/
Parser.Attr.zify_simps : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.homOfLE_base : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (e : U ≤ V),
  (X.homOfLE e).base = (TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (CategoryTheory.homOfLE e)
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.salient_iff_not_flat : ∀ {R : Type u_2} {G : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup G]
  [inst_3 : SMul R G] {C : ConvexCone R G}, C.Salient ↔ ¬C.Flat
-- Mathlib.MeasureTheory.Measure.Tight
/-- In a compact space, every set of measures is tight.  -/
MeasureTheory.IsTightMeasureSet.of_compactSpace : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {S : Set (MeasureTheory.Measure 𝓧)} [inst : TopologicalSpace 𝓧]
  [CompactSpace 𝓧], MeasureTheory.IsTightMeasureSet S
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given left-open right-unbounded range as a list in ascending order.
 -/
Std.Roi.toList : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxi.IsAlwaysFinite α] → Std.Roi α → List α
-- Mathlib.Topology.ContinuousOn
Topology.IsInducing.continuousOn_image_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {g : β → γ} {s : Set α},
  Topology.IsInducing f → (ContinuousOn g (f '' s) ↔ ContinuousOn (g ∘ f) s)
-- Mathlib.Data.Set.Inclusion
Set.inclusion_le_inclusion : ∀ {α : Type u_1} [inst : LE α] {s t : Set α} (h : s ⊆ t) {x y : ↑s}, Set.inclusion h x ≤ Set.inclusion h y ↔ x ≤ y
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Computation.BisimO.match_1.eq_1 : ∀ {α : Type u_1} (motive : α ⊕ Computation α → α ⊕ Computation α → Sort u_2) (a a' : α)
  (h_1 : (a a' : α) → motive (Sum.inl a) (Sum.inl a')) (h_2 : (s s' : Computation α) → motive (Sum.inr s) (Sum.inr s'))
  (h_3 : (x x_1 : α ⊕ Computation α) → motive x x_1),
  (match Sum.inl a, Sum.inl a' with
    | Sum.inl a, Sum.inl a' => h_1 a a'
    | Sum.inr s, Sum.inr s' => h_2 s s'
    | x, x_1 => h_3 x x_1) =
    h_1 a a'
-- Std.Http.Data.Headers.Name
/-- Performs a case-insensitive comparison between a `Name` and a `String`. Returns `true` if they match.
 -/
Std.Http.Header.Name.is : Std.Http.Header.Name → String → Bool
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_toIocMod : ∀ (θ ψ : ℝ), ↑(toIocMod Real.two_pi_pos ψ θ) = ↑θ
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_one_div_one_add_sq : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, 1 / (1 + x ^ 2) = Real.arctan b - Real.arctan a
-- Mathlib.Order.Interval.Finset.Fin
Fin.attachFin_Iio : ∀ {n : ℕ} (a : Fin n), (Finset.Iio ↑a).attachFin ⋯ = Finset.Iio a
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.continuous_swapTrue : ∀ {I : Type u} [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u}),
  Continuous (Profinite.NobelingProof.SwapTrue o)
-- Batteries.Control.LawfulMonadState
liftM_get : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [inst : MonadStateOf σ m] [inst_1 : MonadLift m n],
  liftM get = get
-- Mathlib.Data.Set.Card
Set.ncard_inter_le_ncard_right : ∀ {α : Type u_1} (s t : Set α), autoParam t.Finite Set.ncard_inter_le_ncard_right._auto_1 → (s ∩ t).ncard ≤ t.ncard
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- The category of additive magmas and additive magma morphisms.  -/
AddMagmaCat : Type (u + 1)
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSESδ_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS₁ : S₁.ShortExact)
  (hS₂ : S₂.ShortExact) (f : S₁ ⟶ S₂) {Z : DerivedCategory C}
  (h : (CategoryTheory.shiftFunctor (DerivedCategory C) 1).obj (DerivedCategory.Q.obj S₂.X₁) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (DerivedCategory.triangleOfSESδ hS₁)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor (DerivedCategory C) 1).map (DerivedCategory.Q.map f.τ₁)) h) =
    CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map f.τ₃)
      (CategoryTheory.CategoryStruct.comp (DerivedCategory.triangleOfSESδ hS₂) h)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_Ioi : ∀ {a : ℝ}, MeasureTheory.volume (Set.Ioi a) = ⊤
-- Mathlib.Tactic.Linter.Style
/-- `show t` finds the first goal whose target unifies with `t`. It makes that the main goal,
performs the unification, and replaces the target with the unified version of `t`.
 -/
Mathlib.Linter.Style.show : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_Δ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A),
  (W.map f).Δ = f W.Δ
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Icc_of_Icc : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α} [MeasureTheory.NullSingletonClass μ],
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Icc A B)) l fun i => Set.Icc (a i) (b i)
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableAt.sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {ι : Type u_4} {u : Finset ι} {A : ι → E → F},
  (∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) → DifferentiableAt 𝕜 (∑ i ∈ u, A i) x
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- The vertices `v, w₁, w₂` form an `IsPathGraph3Compl` in `G` iff `w₁w₂` is the only edge present
between these three vertices. It is a witness to the non-complete-multipartite-ness of `G` (see
`not_isCompleteMultipartite_iff_exists_isPathGraph3Compl`). This structure is an explicit way of
saying that the induced graph on `{v, w₁, w₂}` is the complement of `P3`.
 -/
SimpleGraph.IsPathGraph3Compl : {α : Type u} → SimpleGraph α → α → α → α → Prop
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_iff_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {k : α}, t.contains k = true ↔ k ∈ t
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- A valued CSP instance over the template `Γ` with variables indexed by `ι`.  -/
ValuedCSP.Instance : {D : Type u_1} →
  {C : Type u_2} →
    [inst : AddCommMonoid C] →
      [inst_1 : PartialOrder C] →
        [inst_2 : IsOrderedAddMonoid C] → ValuedCSP D C → Type u_3 → Type (max (max u_1 u_2) u_3)
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.sub_zmodRepr_mem : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), x - ↑x.zmodRepr ∈ IsLocalRing.maximalIdeal ℤ_[p]
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.InjectiveTheorem.origin : Lean.Meta.Grind.InjectiveTheorem → Lean.Meta.Grind.Origin
-- Mathlib.Logic.Equiv.Prod
Equiv.sumArrowEquivProdArrow_symm_apply_inr : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (f : α → γ) (g : β → γ) (b : β),
  (Equiv.sumArrowEquivProdArrow α β γ).symm (f, g) (Sum.inr b) = g b
-- Mathlib.Order.GameAdd
Sym2.GameAdd.snd_fst : ∀ {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b : α}, rα a₁ a₂ → Sym2.GameAdd rα s(b, a₁) s(a₂, b)
-- Mathlib.Order.RelSeries
RelSeries.drop_length : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)), (p.drop i).length = p.length - ↑i
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The trifunctor `F ((- ⊗ -) ⊗ -)`  -/
CategoryTheory.MonoidalCategory.curriedTensorPostPost : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          CategoryTheory.Functor C D → CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C D))
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_div_Ici : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a / x) ⁻¹' Set.Ici b = Set.Iic (a / b)
-- Mathlib.Tactic.GRewrite.Core
/-- The rewrite lemma has not unified with anything yet.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.Progress.noMatch : Mathlib.Tactic.GRewrite.Progress✝
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.exists_measurable_superset_of_trim_eq_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {m : MeasureTheory.OuterMeasure α} {s : Set α},
  m.trim s = 0 → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = 0
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.le_sup_right : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {a b : CauSeq α abs},
  b ≤ a ⊔ b
-- Lean.Meta.Basic
/-- Track the number of nested `synthPending` invocations. Nested invocations can happen
when the type class resolution invokes `synthPending`.

Remark: `synthPending` fails if `synthPendingDepth > maxSynthPendingDepth`.
 -/
Lean.Meta.Context.synthPendingDepth : Lean.Meta.Context → ℕ
-- Mathlib.SetTheory.Ordinal.Basic
/-- The universe lift operation for ordinals, which embeds `Ordinal.{u}` as
a proper initial segment of `Ordinal.{v}` for `v > u`. For the initial segment version,
see `liftInitialSeg`.  -/
Ordinal.lift : Ordinal.{v} → Ordinal.{max v u}
-- Mathlib.Topology.ContinuousMap.Polynomial
/-- A polynomial as a continuous function,
with domain restricted to some subset of the semiring of coefficients.

(This is particularly useful when restricting to compact sets, e.g. `[0,1]`.)
 -/
Polynomial.toContinuousMapOn : {R : Type u_1} →
  [inst : Semiring R] →
    [inst_1 : TopologicalSpace R] → [IsTopologicalSemiring R] → Polynomial R → (X : Set R) → C(↑X, R)
-- Init.Data.List.Sort.Lemmas
List.map_merge : ∀ {α : Type u_2} {β : Type u_1} {f : α → β} {r : α → α → Bool} {s : β → β → Bool} {l l' : List α},
  (∀ a ∈ l, ∀ b ∈ l', r a b = s (f a) (f b)) → List.map f (l.merge l' r) = (List.map f l).merge (List.map f l') s
-- Mathlib.Order.CompleteLattice.Basic
Pi.supSet.eq_1 : ∀ {α : Type u_8} {β : α → Type u_9} [inst : (i : α) → SupSet (β i)], Pi.supSet = { sSup := fun s i => ⨆ f, ↑f i }
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.divLeft_symm_apply : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] (x b : G),
  (Homeomorph.divLeft x).symm b = b⁻¹ * x
-- Mathlib.Algebra.Polynomial.HasseDeriv
/-- The `k`th Hasse derivative of a polynomial `∑ a_i X^i` is `∑ (i.choose k) a_i X^(i-k)`.
It satisfies `k! * (hasse_deriv k f) = derivative^[k] f`.  -/
Polynomial.hasseDeriv : {R : Type u_1} → [inst : Semiring R] → ℕ → Polynomial R →ₗ[R] Polynomial R
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- The basic open set of a section, as an element of `AffineZariskiSite`.  -/
AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen : {X : AlgebraicGeometry.Scheme} →
  (U : X.AffineZariskiSite) → ↑(X.presheaf.obj (Opposite.op U.toOpens)) → X.AffineZariskiSite
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsStronglyCocartesian.isCocartesian_of_isStronglyCocartesian : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCocartesian f φ],
  p.IsCocartesian f φ
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair_obj_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B) (s : B ⟶ A)
  {sl : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B}
  {sr : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B},
  (CategoryTheory.Limits.reflexivePair f g s sl sr).obj CategoryTheory.Limits.WalkingReflexivePair.one = A
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_of_le_map_of_stronglyMeasurable : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {β : Type u_7}
  {x : MeasurableSpace β} {μ' : MeasureTheory.Measure β} {φ : α → β} {T' : Set β → E →L[ℝ] F}
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ' T' C') {f : β → E},
  MeasureTheory.Integrable (f ∘ φ) μ →
    MeasureTheory.StronglyMeasurable f →
      Measurable φ →
        μ' ≤ MeasureTheory.Measure.map φ μ →
          (∀ (s : Set β) (x_1 : E), MeasurableSet s → (T' s) x_1 = (T (φ ⁻¹' s)) x_1) →
            MeasureTheory.setToFun μ' T' hT' f = MeasureTheory.setToFun μ T hT (f ∘ φ)
-- Mathlib.Data.Finset.Union
Finset.singleton_disjiUnion : ∀ {α : Type u_1} {β : Type u_2} {t : α → Finset β} (a : α) {h : (↑{a}).PairwiseDisjoint t}, {a}.disjiUnion t h = t a
-- Mathlib.Analysis.Normed.Field.UnitBall
unitSphereToUnits_injective : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜], Function.Injective ⇑(unitSphereToUnits 𝕜)
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has derivative `1` at zero.  -/
hasDerivAt_exp_zero : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂], HasDerivAt NormedSpace.exp 1 0
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffAt.continuousAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {n : WithTop ℕ∞},
  ContMDiffAt I I' n f x → ContinuousAt f x
-- Mathlib.RingTheory.PrincipalIdealDomain
exists_associated_pow_of_associated_pow_mul : ∀ {R : Type u} [inst : CommRing R] [IsBezout R] [IsDomain R] {a b c : R},
  IsCoprime a b → ∀ {k : ℕ}, Associated (c ^ k) (a * b) → ∃ d, Associated (d ^ k) a
-- Lean.Meta.Tactic.Grind.Types
/-- Return `true` if the goal is inconsistent.  -/
Lean.Meta.Grind.isInconsistent : Lean.Meta.Grind.GoalM Bool
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSlice_le_iff : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos},
  String.Slice.Pos.ofSlice p ≤ q ↔ ∀ (h₁ : q ≤ p₁), ∃ (h₀ : p₀ ≤ q), p ≤ q.slice p₀ p₁ h₀ h₁
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.not_tendsto_const_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [NoBotOrder α] (x : α) (l : Filter β) [l.NeBot],
  ¬Filter.Tendsto (fun x_1 => x) l Filter.atBot
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.toHomeomorphSourceTarget_apply_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (a : ↑e.source), ↑(e.toHomeomorphSourceTarget a) = ↑e ↑a
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.pure.injEq : ∀ (h h_1 : Lean.TSyntax `Lean.binderIdent),
  (Lean.Parser.Tactic.MCasesPat.pure h = Lean.Parser.Tactic.MCasesPat.pure h_1) = (h = h_1)
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_f : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰)
  [inst_2 : Small.{u, u_1} 𝒰.I₀] [inst_3 : Quiver.IsThin 𝒰.I₀] (j : 𝒰.I₀),
  d.cover.f j = CategoryTheory.Limits.colimit.ι d.functor j
-- Mathlib.Analysis.Analytic.Linear
/-- `snd` is entire  -/
analyticOnNhd_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {t : Set (E × F)}, AnalyticOnNhd 𝕜 (fun p => p.2) t
-- Init.Prelude
/-- A `MacroScopesView` represents a parsed hygienic name. `extractMacroScopes`
will decode it from a `Name`, and `.review` will re-encode it. The grammar of a
hygienic name is:
```
<name>._@.(<module_name>.<scopes>)*.<mainModule>._hyg.<scopes>
```
 -/
Lean.MacroScopesView : Type