mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.awayι_preimage_basicOpen : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m'),
  0 < m' →
    (TopologicalSpace.Opens.map (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm).base).obj
        (AlgebraicGeometry.Proj.basicOpen 𝒜 g) =
      PrimeSpectrum.basicOpen (HomogeneousLocalization.Away.isLocalizationElem f_deg g_deg)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddMemClass.add_def : ∀ {M : Type u_1} {A : Type u_3} [inst : Add M] [inst_1 : SetLike A M] [hA : AddMemClass A M] (S' : A) (x y : ↥S'),
  x + y = ⟨↑x + ↑y, ⋯⟩
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_eq_empty : ∀ {V : Type u} {G : SimpleGraph V}, G.edgeSet = ∅ ↔ G = ⊥
-- Mathlib.Data.Complex.Basic
Complex.add_conj : ∀ (z : ℂ), z + (starRingEnd ℂ) z = ↑(2 * z.re)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.le_maxKey?_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : t.contains k = true), t.maxKey?.get ⋯ = km → (cmp k km).isLE = true
-- Init.Data.String.Defs
/-- `pos.IsAtEnd` is just shorthand for `pos = s.endPos` that is easier to write if `s` is long.
 -/
String.Slice.Pos.IsAtEnd : {s : String.Slice} → s.Pos → Prop
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_hom_hom_inv_inv_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z Z_1 : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj W X)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator W X
              (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).inv
        Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
        h)
-- Lean.Meta.Sym.Pattern
/-- Returns `true` and add `u =?= v` to pending list IF
- `u` is of the form `max .. ..` or `imax .. ..`, and
- `u` contains `UVars`
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.tryPostponeMaxCnstr : Lean.Level → Lean.Level → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_opow_omega0 : Ordinal.IsPrincipal (fun x1 x2 => x1 ^ x2) Ordinal.omega0
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.leadingCoeff_U_natCast : ∀ (R : Type u_1) [inst : CommRing R] [IsDomain R] [NeZero 2] (n : ℕ), (Polynomial.Chebyshev.U R ↑n).leadingCoeff = 2 ^ n
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.comp_apply : ∀ {X Y T : GrpCat} (f : X ⟶ Y) (g : Y ⟶ T) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.functorL₂_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y),
  CategoryTheory.ShortComplex.SnakeInput.functorL₂.map f = f.f₂
-- Mathlib.Algebra.Field.Subfield.Basic
/-- Product of a multiset of elements in a subfield is in the subfield.  -/
Subfield.multiset_prod_mem : ∀ {K : Type u} [inst : Field K] (s : Subfield K) (m : Multiset K), (∀ a ∈ m, a ∈ s) → m.prod ∈ s
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.cast.injEq : ∀ (declName unfold refold unfold' refold' declName_1 unfold_1 refold_1 unfold'_1 refold'_1 : Lean.Name),
  (Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.cast declName unfold refold unfold' refold' =
      Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.cast declName_1 unfold_1 refold_1 unfold'_1 refold'_1) =
    (declName = declName_1 ∧ unfold = unfold_1 ∧ refold = refold_1 ∧ unfold' = unfold'_1 ∧ refold' = refold'_1)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpFunctor.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D],
  CategoryTheory.Functor.mapGrpFunctor =
    { obj := fun F => F.obj.mapGrp,
      map := fun {F G} α => { app := fun A => CategoryTheory.Grp.homMk'' (α.hom.app A.X) ⋯ ⋯, naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.quasiMeasurePreserving_neg_of_right_invariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddRightInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving Neg.neg μ μ
-- Mathlib.Algebra.Lie.Killing
/-- Given an equivalence `e` of Lie algebras from `L` to `L'`, and elements `x y : L`, the
respective Killing forms of `L` and `L'` satisfy `κ'(e x, e y) = κ(x, y)`.  -/
LieAlgebra.killingForm_of_equiv_apply : ∀ {R : Type u_1} {L : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L' : Type u_4}
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (e : L ≃ₗ⁅R⁆ L') (x y : L),
  ((killingForm R L') (e x)) (e y) = ((killingForm R L) x) y
-- Init.Tactics
/-- `cbv` performs simplification that closely mimics call-by-value evaluation.
It reduces terms by unfolding definitions using their defining equations and
applying matcher equations. The unfolding is propositional, so `cbv` also works
with functions defined via well-founded recursion or partial fixpoints.

`cbv` reduces the goal type (and optionally hypothesis types) using call-by-value
evaluation. For equation goals (`lhs = rhs`), `cbv` automatically attempts `refl`
after reduction to close the goal.

`cbv` supports the standard `at` location syntax:
- `cbv` — reduce the goal target
- `cbv at h` — reduce hypothesis `h`
- `cbv at h |-` — reduce hypothesis `h` and the goal target
- `cbv at *` — reduce all non-dependent propositional hypotheses and the goal target

`cbv` is not a finishing tactic in general: it may leave a new (simpler) goal.

The proofs produced by `cbv` only use the three standard axioms.
In particular, they do not require trust in the correctness of the code
generator.
 -/
Lean.Parser.Tactic.cbv : Lean.ParserDescr
-- Mathlib.Data.EReal.Operations
/-- Negation as an order reversing isomorphism on `EReal`.  -/
EReal.negOrderIso : EReal ≃o ERealᵒᵈ
-- Init.Data.Nat.Basic
Nat.lt_of_succ_lt_succ : ∀ {n m : ℕ}, n.succ < m.succ → n < m
-- Init.Data.List.Lemmas
List.flatten.eq_1 : ∀ {α : Type u_1}, [].flatten = []
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- `Multiplicative (∀ i : ι, K i)` is equivalent to `∀ i : ι, Multiplicative (K i)`.  -/
MulEquiv.piMultiplicative : {ι : Type u_1} →
  (K : ι → Type u_4) → [inst : (i : ι) → Add (K i)] → Multiplicative ((i : ι) → K i) ≃* ((i : ι) → Multiplicative (K i))
-- Init.Data.SInt.Bitwise
Int16.shiftRight_xor : ∀ {a b c : Int16}, (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
-- Mathlib.Order.JordanHolder
CompositionSeries.head_le : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X} (i : Fin (s.length + 1)),
  RelSeries.head s ≤ s.toFun i
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.tensorEquiv_symm_single_eq_tmul_single_zero : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] (mn : M × N) (r : R),
  (AddMonoidAlgebra.tensorEquiv R).symm (AddMonoidAlgebra.single mn r) =
    AddMonoidAlgebra.single mn.1 r ⊗ₜ[R] AddMonoidAlgebra.single mn.2 1
-- Mathlib.LinearAlgebra.DFinsupp
/-- `DFinsupp.mapRange` as a `LinearMap`.  -/
DFinsupp.mapRange.linearMap : {ι : Type u_1} →
  {R : Type u_3} →
    [inst : Semiring R] →
      {β₁ : ι → Type u_8} →
        {β₂ : ι → Type u_9} →
          [inst_1 : (i : ι) → AddCommMonoid (β₁ i)] →
            [inst_2 : (i : ι) → AddCommMonoid (β₂ i)] →
              [inst_3 : (i : ι) → Module R (β₁ i)] →
                [inst_4 : (i : ι) → Module R (β₂ i)] →
                  ((i : ι) → β₁ i →ₗ[R] β₂ i) → (Π₀ (i : ι), β₁ i) →ₗ[R] Π₀ (i : ι), β₂ i
-- Init.Data.Int.Order
Int.le.intro_sub : ∀ {a b : ℤ} (n : ℕ), b - a = ↑n → a ≤ b
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).inv.hom₃ =
    CategoryTheory.CategoryStruct.id (Opposite.op (F.obj T.obj₁))
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.decidableMemCenter : {R : Type u_1} → [inst : Semiring R] → [DecidableEq R] → [Fintype R] → DecidablePred fun x => x ∈ Subsemiring.center R
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_one_one_eq_X : ∀ {R : Type u} [inst : Semiring R], (Polynomial.monomial 1) 1 = Polynomial.X
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.nullSet.congr_simp : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ μ_1 : MeasureTheory.Measure α} (e_μ : μ = μ_1)
  {ν ν_1 : MeasureTheory.Measure α} (e_ν : ν = ν_1) (h : μ.MutuallySingular ν) (a a_1 : α),
  a = a_1 → h.nullSet a = ⋯.nullSet a_1
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.inner_rightAngleRotationAux₁_right : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), inner ℝ x (o.rightAngleRotationAux₁ y) = -(o.areaForm x) y
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
/-- The rank of `M × N` at `p` is equal to the sum of the ranks.  -/
Module.rankAtStalk_prod : ∀ {R : Type uR} (M : Type uM) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.Finite R M] (N : Type u_1) [inst_5 : AddCommGroup N] [inst_6 : Module R N] [Module.Flat R N]
  [Module.Finite R N], Module.rankAtStalk (M × N) = Module.rankAtStalk M + Module.rankAtStalk N
-- Lean.Elab.Term.TermElabM
/-- Return `true` if `e` reduces (by unfolding only `[reducible]` declarations) to `?m ...`  -/
Lean.Elab.Term.isMVarApp : Lean.Expr → Lean.Elab.TermElabM Bool
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- A multiplicative seminorm on a ring `R` is a function `f : R → ℝ` that preserves zero and
multiplication, takes nonnegative values, is subadditive and such that `f (-x) = f x` for all `x`.
 -/
MulRingSeminorm : (R : Type u_2) → [NonAssocRing R] → Type u_2
-- Init.Data.List.Impl
/-- Applies a function to the corresponding elements of two lists, stopping at the end of the shorter
list.

`O(min |xs| |ys|)`. This is a tail-recursive version of `List.zipWith` that's used at runtime.

Examples:
* `[1, 2].zipWithTR (· + ·) [5, 6] = [6, 8]`
* `[1, 2, 3].zipWithTR (· + ·) [5, 6, 10] = [6, 8, 13]`
* `[].zipWithTR (· + ·) [5, 6] = []`
* `[x₁, x₂, x₃].zipWithTR f [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]`
 -/
List.zipWithTR : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → β → γ) → List α → List β → List γ
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs.inj : ∀ {R : Type u_1} {S : Type u_2} {inst : Semiring S} {inst_1 : PartialOrder S} {inst_2 : Semiring R}
  {v : AbsoluteValue R S} {ofAbs ofAbs_1 : R}, WithAbs.toAbs v ofAbs = WithAbs.toAbs v ofAbs_1 → ofAbs = ofAbs_1
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrix_apply_same : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [CharZero R] (i : ↥b.support), b.cartanMatrix i i = 2
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
Complex.hasDerivAt_Gamma_one : HasDerivAt Complex.Gamma (-↑Real.eulerMascheroniConstant) 1
-- Mathlib.LinearAlgebra.LinearPMap
_private.Mathlib.LinearAlgebra.LinearPMap.0.LinearPMap.sup_aux : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f g : E →ₛₗ.[σ] F),
  (∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y) →
    ∃ fg, ∀ (x : ↥f.domain) (y : ↥g.domain) (z : ↥(f.domain ⊔ g.domain)), ↑x + ↑y = ↑z → fg z = ↑f x + ↑g y
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.one : Lean.TSyntax `Lean.binderIdent → Lean.Parser.Tactic.MRefinePat
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.units_mono : ∀ {M : Type u_1} [inst : Monoid M], Monotone Submonoid.units
-- Init.Data.String.Lemmas.Order
String.Pos.ne_endPos_of_lt : ∀ {s : String} {p q : s.Pos}, p < q → p ≠ s.endPos
-- Init.Data.Int.Compare
Int.compare_eq_gt : ∀ {a b : ℤ}, compare a b = Ordering.gt ↔ b < a
-- Mathlib.Data.Sigma.Interval
Sigma.Ici_mk : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] [inst_1 : (i : ι) → LocallyFiniteOrderTop (α i)]
  (i : ι) (a : α i), Finset.Ici ⟨i, a⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ici a)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.veq_mul_mul_mul_comm : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x y z w : R), x * y * (z * w) =ᵥ x * z * (y * w)
-- Init.Data.Format.Basic
/-- State for formatting a pretty string.  -/
_private.Init.Data.Format.Basic.0.Std.Format.State : Type
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_erase_mul : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] [inst_1 : DecidableEq α] (s : Finset α) {a : α},
  a ∈ s →
    ∀ (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f))
      (comm' : optParam (∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → Function.onFun Commute f x x_1) ⋯),
      (s.erase a).noncommProd f comm' * f a = s.noncommProd f comm
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opInverse_obj : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex Vᵒᵖ c.symm),
  (HomologicalComplex.opInverse V c).obj X = Opposite.op X.unopSymm
-- Mathlib.Analysis.Distribution.TemperateGrowth
MeasureTheory.Measure.integrable_pow_neg_integrablePower : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] (μ : MeasureTheory.Measure E)
  [h : μ.HasTemperateGrowth], MeasureTheory.Integrable (fun x => (1 + ‖x‖) ^ (-↑μ.integrablePower)) μ
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G)
  {X' X : C} {Y : D} (f : X' ⟶ X) (g : F.obj X ⟶ Y),
  (adj.homEquiv X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) =
    CategoryTheory.CategoryStruct.comp f ((adj.homEquiv X Y) g)
-- Mathlib.Topology.Compactness.Lindelof
Filter.coLindelof_eq_bot : ∀ {X : Type u} [inst : TopologicalSpace X] [LindelofSpace X], Filter.coLindelof X = ⊥
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.turanGraph_eq_top : ∀ {n r : ℕ}, SimpleGraph.turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r
-- Mathlib.Logic.Nonempty
Nonempty.congr : ∀ {α : Sort u_3} {β : Sort u_4} (f : α → β) (g : β → α), Nonempty α ↔ Nonempty β
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
FundamentalGroupoidFunctor.prodToProdTop_map : ∀ (A : TopCat) (B : TopCat) {x₀ x₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A)}
  {y₀ y₁ : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)} (p₀ : x₀ ⟶ x₁) (p₁ : y₀ ⟶ y₁),
  (FundamentalGroupoidFunctor.prodToProdTop A B).map (p₀, p₁) = Path.Homotopic.prod p₀ p₁
-- Mathlib.Tactic.Simps.Basic
/-- Arguments to `@[simps]` attribute.  -/
Lean.Parser.Attr.simpsArgsRest : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
ContDiffAt.rpow_const_of_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {p : ℝ} {m : ℕ},
  ContDiffAt ℝ (↑m) f x → ↑m ≤ p → ContDiffAt ℝ (↑m) (fun x => f x ^ p) x
-- Mathlib.CategoryTheory.Limits.Lattice
/-- The limit cone over any functor into a complete lattice.
 -/
CategoryTheory.Limits.CompleteLattice.limitCone : {α : Type u} →
  [inst : CompleteLattice α] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        (F : CategoryTheory.Functor J α) → CategoryTheory.Limits.LimitCone F
-- Mathlib.Probability.Moments.Variance
/-- **Chebyshev's inequality**: one can control the deviation probability of a real random variable
from its expectation in terms of the variance.  -/
ProbabilityTheory.meas_ge_le_variance_div_sq : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ},
  MeasureTheory.MemLp X 2 μ →
    ∀ {c : ℝ}, 0 < c → μ {ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ ENNReal.ofReal (ProbabilityTheory.variance X μ / c ^ 2)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sUnion_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] (S : Set (Set α)) (t : Set β), ⋃₀ S • t = ⋃ s ∈ S, s • t
-- Mathlib.RingTheory.Congruence.BigOperators
/-- Congruence relation of a ring preserves finite sum.  -/
RingCon.finsetSum : ∀ {ι : Type u_1} {S : Type u_2} [inst : AddCommMonoid S] [inst_1 : Mul S] (t : RingCon S) (s : Finset ι) {f g : ι → S},
  (∀ i ∈ s, t (f i) (g i)) → t (s.sum f) (s.sum g)
-- Mathlib.Order.Concept
lowerPolar_upperPolar_monotone : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop), Monotone (lowerPolar r ∘ upperPolar r)
-- Aesop.Forward.State
Aesop.VariableMap.instToMessageData : Lean.ToMessageData Aesop.VariableMap
-- Lean.Elab.Tactic.Config
Lean.Elab.Tactic.ConfigItemView.ref : Lean.Elab.Tactic.ConfigItemView → Lean.Syntax
-- Mathlib.Topology.Order.Completion
DedekindCut.continuous_principal : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : TopologicalSpace (DedekindCut α)] [OrderTopology (DedekindCut α)],
  Continuous fun a => DedekindCut.principal a
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.mapsTo : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : Topology.CWComplex C] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n),
  ∃ I,
    Set.MapsTo (↑(Topology.RelCWComplex.map n i)) (Metric.sphere 0 1)
      (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(Topology.RelCWComplex.map m j) '' Metric.closedBall 0 1)
-- Lean.Parser.Basic
/-- Optimized version of `mkAntiquot ... <|> p`.  -/
Lean.Parser.withAntiquot : Lean.Parser.Parser → Lean.Parser.Parser → Lean.Parser.Parser
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorKind.hole.sizeOf_spec : sizeOf Lean.Elab.Term.MVarErrorKind.hole = 1
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_const_left : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {g'' : α → F''} {l : Filter α} {c : E''}, (fun _x => c) =o[l] g'' ↔ c = 0 ∨ Filter.Tendsto (norm ∘ g'') l Filter.atTop
-- Lean.Meta.Tactic.Grind.Types
/-- Add a new lookahead candidate.  -/
Lean.Meta.Grind.addLookaheadCandidate : Lean.Meta.Grind.SplitInfo → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
CategoryTheory.FunctorToTypes.closed : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type (max w v u))) → CategoryTheory.Closed F
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
/-- The preimage of a closed submodule under a continuous linear map as a closed submodule.  -/
ClosedSubmodule.comap : {R : Type u_2} →
  {M : Type u_3} →
    {N : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : TopologicalSpace M] →
            [inst_3 : Module R M] →
              [inst_4 : AddCommMonoid N] →
                [inst_5 : TopologicalSpace N] →
                  [inst_6 : Module R N] → (M →L[R] N) → ClosedSubmodule R N → ClosedSubmodule R M
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_flip : ∀ {M : Type u_4} [inst : AddCommMonoid M] {n : ℕ} (f : ℕ → M),
  ∑ r ∈ Finset.range (n + 1), f (n - r) = ∑ k ∈ Finset.range (n + 1), f k
-- Mathlib.Probability.Kernel.Irreducible
ProbabilityTheory.Kernel.instIsIrreducibleIdOfSubsingleton : ∀ {α : Type u_1} {mα : MeasurableSpace α} {φ : MeasureTheory.Measure α} [Subsingleton α],
  ProbabilityTheory.Kernel.IsIrreducible φ ProbabilityTheory.Kernel.id
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.ringHom_ext'_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A]
  {f g : MvPolynomial σ R →+* A},
  f = g ↔ f.comp MvPolynomial.C = g.comp MvPolynomial.C ∧ ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)
-- Mathlib.Topology.Algebra.Algebra
Subalgebra.topologicalClosure_mono : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] {s t : Subalgebra R A},
  s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_range_eq : ∀ {α β : Type u} (f : α → β), Function.Injective f → Cardinal.mk ↑(Set.range f) = Cardinal.mk α
-- Mathlib.RingTheory.Etale.Finite
/-- Construct a term of `FiniteEtale R` from a finite étale `R`-algebra.  -/
CommAlgCat.FiniteEtale.of : (R : Type u) →
  [inst : CommRing R] →
    (S : Type v) →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → [Module.Finite R S] → [Algebra.Etale R S] → CommAlgCat.FiniteEtale R
-- Mathlib.RingTheory.Finiteness.Small
Submodule.FG.small : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Small.{u, u_1} R]
  (P : Submodule R M), P.FG → Small.{u, u_2} ↥P
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- A point lies in an affine subspace constructed from another point and a direction if and only
if their difference is in that direction.  -/
AffineSubspace.mem_mk' : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p q : P} {direction : Submodule k V},
  q ∈ AffineSubspace.mk' p direction ↔ q -ᵥ p ∈ direction
-- Mathlib.Tactic.GCongr.ForwardAttr
Mathlib.Tactic.GCongr.ForwardExt.mk.inj : ∀ {eval eval_1 : Lean.Expr → Lean.MVarId → Lean.MetaM Unit}, { eval := eval } = { eval := eval_1 } → eval = eval_1
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_fun_const_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {R : Type u_2} [inst_3 : Monoid R] [inst_4 : DistribMulAction R F]
  [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R),
  DifferentiableAt 𝕜 f x → deriv (fun y => c • f y) x = c • deriv f x
-- Init.Omega.IntList
Lean.Omega.IntList.mul_smul_left : ∀ {i : ℤ} {xs ys : Lean.Omega.IntList}, i * xs * ys = i * (xs * ys)
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.BinaryInput.rhs_cast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α} (input : aig1.BinaryInput)
  (h : aig1.decls.size ≤ aig2.decls.size), (input.cast h).rhs = input.rhs.cast h