mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Order.Lemmas
Std.instReflOfTotal : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Total r], Std.Refl r
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, derivative in the right endpoint.

If `f : ℝ → E` is continuous, then the derivative of `u ↦ ∫ x in a..u, f x` at `b` is `f b`.  -/
Continuous.deriv_integral : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (f : ℝ → E),
  Continuous f → ∀ (a b : ℝ), deriv (fun u => ∫ (x : ℝ) in a..u, f x) b = f b
-- Mathlib.Logic.Function.Iterate
Function.iterate_succ_apply : ∀ {α : Type u} (f : α → α) (n : ℕ) (x : α), f^[n.succ] x = f^[n] (f x)
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Measure.setIntegral_condKernel : ∀ {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (β × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ] {E : Type u_3}
  {f : β × Ω → E} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace ℝ E] {s : Set β},
  MeasurableSet s →
    ∀ {t : Set Ω},
      MeasurableSet t →
        MeasureTheory.IntegrableOn f (s ×ˢ t) ρ →
          ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- `MDifferentiableOn I I' f s` indicates that the function `f` between manifolds
has a derivative within `s` at all points of `s`.
This is a generalization of `DifferentiableOn` to manifolds.  -/
MDifferentiableOn : {𝕜 : 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] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                ModelWithCorners 𝕜 E' H' →
                                  {M' : Type u_7} →
                                    [inst : TopologicalSpace M'] → [ChartedSpace H' M'] → (M → M') → Set M → Prop
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.add_left : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : AddGroup α] [ContinuousConstVAdd α α] {s t : Set α},
  IsOpen t → IsOpen (s + t)
-- Mathlib.RingTheory.Smooth.Kaehler
tensorKaehlerQuotKerSqEquiv_tmul_D : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S] (s : S) (t : P),
  (tensorKaehlerQuotKerSqEquiv R P S)
      (s ⊗ₜ[P ⧸ RingHom.ker (algebraMap P S) ^ 2]
        (KaehlerDifferential.D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2))
          ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)) =
    s ⊗ₜ[P] (KaehlerDifferential.D R P) t
-- Lean.DocString.Parser
/-- Items like +  -/
Lean.Doc.Parser.UnorderedListType.plus : Lean.Doc.Parser.UnorderedListType
-- Mathlib.Topology.Algebra.Module.IsWeak
/-- Suppose `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜` and `B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜` are bilinear maps such that
`E ≃L[𝕜] E'` and `F ≃ₗ[𝕜] F'`. If `B.IsWeak`, then so also `B'.IsWeak`.  -/
LinearMap.IsWeak.congr : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {E' : Type u_5} {F' : Type u_6} [inst : CommSemiring 𝕜]
  [inst_1 : TopologicalSpace 𝕜] [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F]
  [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace E] [inst_7 : AddCommMonoid E'] [inst_8 : Module 𝕜 E']
  [inst_9 : AddCommMonoid F'] [inst_10 : Module 𝕜 F'] [inst_11 : TopologicalSpace E'] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)
  (B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜) (e : E ≃L[𝕜] E') (f : F ≃ₗ[𝕜] F'),
  ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B' → ∀ [hB : B.IsWeak], B'.IsWeak
-- Init.Data.Fin.Lemmas
Fin.val_castLT : ∀ {m n : ℕ} (i : Fin m) (h : ↑i < n), ↑(i.castLT h) = ↑i
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.refl_toLHom : ∀ (L : FirstOrder.Language), (FirstOrder.Language.LEquiv.refl L).toLHom = FirstOrder.Language.LHom.id L
-- Std.Data.DHashMap.Internal.AssocList.Iterator
Std.DHashMap.Internal.AssocList.AssocListIterator.mk.injEq : ∀ {α : Type u} {β : α → Type v} (l l_1 : Std.DHashMap.Internal.AssocList α β), ({ l := l } = { l := l_1 }) = (l = l_1)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.regularityReduced_mono : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [inst_4 : DecidableRel G.Adj]
  {δ ε₁ ε₂ : 𝕜}, ε₁ ≤ ε₂ → SimpleGraph.regularityReduced P G ε₁ δ ≤ SimpleGraph.regularityReduced P G ε₂ δ
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.tendsto_approx : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : TopologicalSpace β] {x : MeasurableSpace α}
  (hf : MeasureTheory.StronglyMeasurable f) (x_1 : α),
  Filter.Tendsto (fun n => (hf.approx n) x_1) Filter.atTop (nhds (f x_1))
-- Init.Data.Nat.Basic
Nat.le_succ_of_pred_le : ∀ {n : ℕ} {m : ℕ}, n.pred ≤ m → n ≤ m.succ
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.coe_units_zpow : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  (u : (Matrix n' n' R)ˣ) (n : ℤ), ↑(u ^ n) = ↑u ^ n
-- Batteries.Lean.Position
/-- Runs `x` with a synthetic ref that has position info locating the given `decl` if it is defined
in the current file, or else runs `x` without modifying the ref. This is useful for logging on a
declaration's name from within linters.

By default, this uses the "selection range" of the declaration, which is usually the declaration's
identifier or e.g. the `instance` token for an unnamed instance. (This is also the place that
receives hovers for the declaration.)

If `fullRange` is instead set to `true`, this uses the full declaration range, which includes the
modifiers (such as the docstring, if there is one) and the body of the declaration.

`canonical` applies to the synthetic syntax generated for the ref; see `Syntax.ofRange`.  -/
Lean.withDeclRef? : {α : Type} →
  {m : Type → Type} →
    [Monad m] →
      [Lean.MonadEnv m] →
        [MonadLiftT BaseIO m] →
          [Lean.MonadFileMap m] → [Lean.MonadRef m] → Lean.Name → m α → optParam Bool false → optParam Bool true → m α
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- An element can be compressed to any other element by removing/adding the differences.  -/
UV.compress_sdiff_sdiff : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  (a b : α), UV.compress (a \ b) (b \ a) b = a
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instCommSemigroup : CommSemigroup Complex.UnitDisc
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- Given a tagged partition `π` of `I` and a (not tagged) partition `πi J hJ` of each `J ∈ π`,
returns the tagged partition of `I` into all the boxes of all `πi J hJ`. The tag of a box `J`
is defined to be the `π.tag` of the box of the partition `π` that includes `J`.

Note that usually the result is not a Henstock partition.  -/
BoxIntegral.TaggedPrepartition.biUnionPrepartition : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} →
    BoxIntegral.TaggedPrepartition I →
      ((J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) → BoxIntegral.TaggedPrepartition I
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.toTopEdgeLabeling_labelGraph : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : DecidableRel G.Adj],
  SimpleGraph.EdgeLabeling.labelGraph G.toTopEdgeLabeling 1 = G
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.of_add_of : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Add α] (f g : m → n → α),
  Matrix.of f + Matrix.of g = Matrix.of (f + g)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
/-- The left inclusion in `Cochain K (mappingCocone φ) 0`.  -/
CochainComplex.mappingCocone.inl : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (φ : K ⟶ L) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            CochainComplex.HomComplex.Cochain K (CochainComplex.mappingCocone φ) 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_id' : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (a : A),
  autoParam (p a) cfc_id'._auto_1 → cfc (fun x => x) a = a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.comp_val_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {X Y Z : SheafOfModules R} (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : PresheafOfModules R.obj} (h : Z.val ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).val h =
    CategoryTheory.CategoryStruct.comp f.val (CategoryTheory.CategoryStruct.comp g.val h)
-- Init.Data.Array.Lemmas
Array.ne_empty_of_size_pos : ∀ {α : Type u_1} {xs : Array α}, 0 < xs.size → xs ≠ #[]
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `upperSemicontinuous_iff_frequently`. -/
UpperSemicontinuous.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β},
  (∀ (x : α) (y : β), (∃ᶠ (x' : α) in nhds x, f x' ≥ y) → f x ≥ y) → UpperSemicontinuous f
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_smul : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c : ℕ → 𝕜) (x : 𝕜),
  FormalMultilinearSeries.ofScalars E (x • c) = x • FormalMultilinearSeries.ofScalars E c
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_eq_self_iff_zero_or_not_dvd : ∀ (n : ℕ) {p : ℕ}, Nat.Prime p → (n / p ^ n.factorization p = n ↔ n = 0 ∨ ¬p ∣ n)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instAddZeroClass : {R : Type u_3} → {A : Type u_4} → [AddZeroClass R] → [AddZeroClass A] → AddZeroClass (Unitization R A)
-- Mathlib.Data.List.Map2
List.zipLeft'.eq_1 : ∀ {α : Type u_1} {β : Type u_2}, List.zipLeft' = List.zipWithLeft' Prod.mk
-- Mathlib.Algebra.Homology.Embedding.Extend
ComplexShape.Embedding.instPreservesZeroMorphismsHomologicalComplexExtendFunctor : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (C : Type u_3)
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C], (e.extendFunctor C).PreservesZeroMorphisms
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_congr_uIoo : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f g : ℝ → E}
  {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ],
  Set.EqOn f g (Set.uIoo a b) → ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Function.Injective.tprod_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {g : γ → β},
  Function.Injective g → ∀ {f : β → α}, Function.mulSupport f ⊆ Set.range g → ∏' (c : γ), f (g c) = ∏' (b : β), f b
-- Mathlib.Analysis.Convex.Hull
convexHull_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (x : E), (convexHull 𝕜) {x} = {x}
-- Mathlib.Topology.Maps.Basic
IsOpenMap.preimage_closure_image : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → Function.Injective f → Continuous f → ∀ (s : Set X), IsClosed s → f ⁻¹' closure (f '' s) = s
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- **Alias** of `SimpleGraph.Coloring.ofIsEmpty`.

---

The coloring of an empty graph.  -/
SimpleGraph.coloringOfIsEmpty : {V : Type u} → {G : SimpleGraph V} → {α : Type u_2} → [IsEmpty V] → G.Coloring α
-- Mathlib.Algebra.Order.Floor.Extended
ENat.preimage_toENNReal_Ici : ∀ (a : ENNReal), ENat.toENNReal ⁻¹' Set.Ici a = Set.Ici ⌈a⌉ₑ
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.Hom.mk.injEq : ∀ {R : Type u} [inst : CommRing R] {V W : HopfAlgCat R} (toBialgHom' toBialgHom'_1 : V.carrier →ₐc[R] W.carrier),
  ({ toBialgHom' := toBialgHom' } = { toBialgHom' := toBialgHom'_1 }) = (toBialgHom' = toBialgHom'_1)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_injective_iff : ∀ {m n : ℕ} {α : Sort u_1} {xs : Fin m → α} {ys : Fin n → α},
  Function.Injective (Fin.append xs ys) ↔
    Function.Injective xs ∧ Function.Injective ys ∧ ∀ (i : Fin m) (j : Fin n), xs i ≠ ys j
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.mvars : Lean.Meta.AbstractMVars.State → Array Lean.Expr
-- Mathlib.Topology.OmegaCompletePartialOrder
Scott.IsOpen.eq_1 : ∀ (α : Type u) [inst : OmegaCompletePartialOrder α] (s : Set α),
  Scott.IsOpen α s = OmegaCompletePartialOrder.ωScottContinuous fun x => x ∈ s
-- Mathlib.Algebra.Group.Defs
two_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M), 2 • a = a + a
-- Init.Notation
/-- A pipe operator that feeds values from the left into functions on the right.

`x |> f` means the same as `f x`, and it chains such that `x |> f |> g` is interpreted as `g (f x)`.
 -/
«term_|>_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.GrothendieckTopology.toGrothendieck_toPrecoverage_le : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] (J : CategoryTheory.GrothendieckTopology C),
  J.toPrecoverage.toGrothendieck ≤ J
-- Mathlib.Analysis.Convex.Between
Sbtw.not_rotate : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] {x y z : P},
  Sbtw R x y z → ¬Wbtw R z x y
-- Mathlib.Data.Num.ZNum
ZNum.le_to_int : ∀ {m n : ZNum}, ↑m ≤ ↑n ↔ m ≤ n
-- Mathlib.Data.QPF.Univariate.Basic
/-- `recF` is insensitive to the representation  -/
QPF.recF_eq_of_Wequiv : ∀ {F : Type u → Type v} [q : QPF F] {α : Type u} (u : F α → α) (x y : (QPF.P F).W),
  QPF.Wequiv x y → QPF.recF u x = QPF.recF u y
-- Mathlib.Order.OrderDual
OrderDual.instLinearOrder : (α : Type u_2) → [LinearOrder α] → LinearOrder αᵒᵈ
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
SimpleGraph.UnitDistEmbedding.iso_p_apply : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {E : Type u_3} [inst : MetricSpace E]
  (U : G.UnitDistEmbedding E) (e : G ≃g H) (a : W), (U.iso e).p a = U.p (e.symm.toCopy.toEmbedding a)
-- Init.Omega.Constraint
/-- Dividing a constraint by a natural number, and tightened to integer bounds.
Thus the lower bound is rounded up, and the upper bound is rounded down.
 -/
Lean.Omega.Constraint.div : Lean.Omega.Constraint → ℕ → Lean.Omega.Constraint
-- Aesop.Rule.Name
Aesop.RuleName.name : Aesop.RuleName → Lean.Name
-- Init.Prelude
/-- Synthetic syntax is syntax that was produced by a metaprogram or by Lean itself (e.g. by a
quotation). Synthetic syntax is annotated with a source span from the original syntax, which
relates it to the source file.

The delaborator uses this constructor to store an encoded indicator of which core language
expression gave rise to the syntax.

The `canonical` flag on synthetic syntax is enabled for syntax that is not literally part of the
original input syntax but should be treated “as if” the user really wrote it for the purpose of
hovers and error messages. This is usually used on identifiers in order to connect the binding
site to the user's original syntax even if the name of the identifier changes during expansion, as
well as on tokens that should receive targeted messages.

Generally speaking, a macro expansion should only use a given piece of input syntax in a single
canonical token. An exception to this rule is when the same identifier is used to declare two
binders, as in the macro expansion for dependent if:
```
`(if $h : $cond then $t else $e) ~>
`(dite $cond (fun $h => $t) (fun $h => $t))
```
In these cases, if the user hovers over `h` they will see information about both binding sites.
 -/
Lean.SourceInfo.synthetic : String.Pos.Raw → String.Pos.Raw → optParam Bool false → Lean.SourceInfo
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.range_sigmoid : Set.range Real.sigmoid = Set.Ioo 0 1
-- Mathlib.Data.List.Rotate
List.rotate_zero : ∀ {α : Type u} (l : List α), l.rotate 0 = l
-- Mathlib.Probability.Density
/-- A real-valued random variable `X` `HasPDF X ℙ λ` (where `λ` is the Lebesgue measure) if and
only if the push-forward measure of `ℙ` along `X` is absolutely continuous with respect to `λ`.  -/
Real.hasPDF_iff_of_aemeasurable : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.SFinite ℙ],
  AEMeasurable X ℙ →
    (MeasureTheory.HasPDF X ℙ MeasureTheory.volume ↔
      (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous MeasureTheory.volume)
-- Mathlib.NumberTheory.Height.NumberField
NumberField.mem_multisetInfinitePlace : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {v : AbsoluteValue K ℝ},
  v ∈ NumberField.multisetInfinitePlace K ↔ NumberField.IsInfinitePlace v
-- Lean.Meta.Sym.LooseBVarsS
/-- Lifts loose bound variables `>= s` in `e` by `d`.
It assumes the input is maximally shared, and ensures the output is too.
 -/
Lean.Meta.Sym.liftLooseBVarsS' : Lean.Expr → ℕ → ℕ → Lean.Meta.Sym.Internal.AlphaShareBuilderM Lean.Expr
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.FunctionTheorems.mk.inj : ∀
  {theorems theorems_1 :
    Std.TreeMap Lean.Name (Std.TreeMap Lean.Name (Array Mathlib.Meta.FunProp.FunctionTheorem) Lean.Name.quickCmp)
      Lean.Name.quickCmp},
  { theorems := theorems } = { theorems := theorems_1 } → theorems = theorems_1
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.top_prod : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup N),
  ⊤.prod H = Subgroup.comap (MonoidHom.snd G N) H
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.isScalarTower_over_bot : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], IsScalarTower (↥⊥) F E
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_sumAlgEquiv : ∀ {R : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} [inst : CommSemiring R] (b : S₁) (p : MvPolynomial (S₁ ⊕ S₂) R),
  (MvPolynomial.pderiv b) ((MvPolynomial.sumAlgEquiv R S₁ S₂) p) =
    (MvPolynomial.sumAlgEquiv R S₁ S₂) ((MvPolynomial.pderiv (Sum.inl b)) p)
-- Aesop.Builder.Basic
Aesop.PhaseSpec.norm.sizeOf_spec : ∀ (info : Aesop.NormRuleInfo), sizeOf (Aesop.PhaseSpec.norm info) = 1 + sizeOf info
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.of_eq : ∀ {n : ℕ} {f g : List.Vector ℕ n → ℕ}, Nat.Primrec' f → (∀ (i : List.Vector ℕ n), f i = g i) → Nat.Primrec' g
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousComponent_isHomogeneous : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (n : ℕ) (φ : MvPolynomial σ R),
  ((MvPolynomial.homogeneousComponent n) φ).IsHomogeneous n
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.map_zero : ∀ {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), F.map 0 = 0
-- Init.Data.String.Basic
/-- Advances a valid position on a slice to the next valid position, given a proof that the
position is not the past-the-end position, which guarantees that such a position exists.  -/
String.Slice.Pos.next : {s : String.Slice} → (pos : s.Pos) → pos ≠ s.endPos → s.Pos
-- Init.Data.String.Iterate
/-- Creates an iterator over the valid positions within `s`, starting at `p`.
 -/
String.Slice.positionsFrom : {s : String.Slice} → s.Pos → Std.Iter { p // p ≠ s.endPos }
-- Lean.Meta.Tactic.Grind.Arith.CommRing.PP
Lean.Meta.Grind.Arith.CommRing.pp? : Lean.Meta.Grind.Goal → Lean.MetaM (Option Lean.MessageData)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.entryAtIdx!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {i : ℕ}, t₁.Equiv t₂ → t₁.entryAtIdx! i = t₂.entryAtIdx! i
-- Init.Data.Ord.Basic
Ordering.gt_beq_lt : (Ordering.gt == Ordering.lt) = false
-- Mathlib.Data.Complex.Basic
Complex.div_intCast_im : ∀ (z : ℂ) (n : ℤ), (z / ↑n).im = z.im / ↑n
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.unop_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : F ⟶ G) (β : G ⟶ H) {Z : CategoryTheory.Functor C D} (h : F.unop ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.unop (CategoryTheory.CategoryStruct.comp α β)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.unop β)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.unop α) h)
-- Mathlib.CategoryTheory.Shift.ShiftSequence
/-- When `f : X ⟶ Y⟦m⟧`, `m + n = mn`, `n + a = a'` and `ha'' : m + a' = a''`, this lemma
relates the two morphisms `F.shiftMap f a' a'' ha''` and `(F.shift a).map (f⟦n⟧')`. Indeed,
via canonical isomorphisms, they both identify to morphisms
`(F.shift a').obj X ⟶ (F.shift a'').obj Y`.
 -/
CategoryTheory.Functor.shiftIso_hom_app_comp_shiftMap : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] {X Y : C} {m : M}
  (f : X ⟶ (CategoryTheory.shiftFunctor C m).obj Y) (n mn : M) (hnm : m + n = mn) (a a' a'' : M) (ha' : n + a = a')
  (ha'' : m + a' = a''),
  CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app X) (F.shiftMap f a' a'' ha'') =
    CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctor C n).map f))
      (CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app Y))
        ((F.shiftIso mn a a'' ⋯).hom.app Y))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inrCokernelCofork_π : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.biprod.inrCokernelCofork X Y) = CategoryTheory.Limits.biprod.fst
-- Mathlib.Algebra.Order.GroupWithZero.Lex
LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedCommGroupWithZero α] [inst_1 : LinearOrderedCommGroupWithZero β]
  {m : α} (hm : m ≠ 0), (LinearOrderedCommGroupWithZero.inl α β) m = ↑((OrderMonoidHom.inlₗ αˣ βˣ) (Units.mk0 m hm))