mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Polynomial
AnalyticOnNhd.eval_polynomial : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {A : Type u_5} [inst_1 : NormedCommRing A]
  [inst_2 : NormedAlgebra 𝕜 A] (p : Polynomial A), AnalyticOnNhd 𝕜 (fun x => Polynomial.eval x p) Set.univ
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} [inst_2 : SizeOf C] [inst_3 : SizeOf ι]
  (Hₚ : ι → CategoryTheory.Functor TopPair C) (H : ι → CategoryTheory.Functor TopCat C)
  (iso : (i : ι) → H i ≅ TopPair.incl.comp (Hₚ i)) (δ : (i j : ι) → Hₚ i ⟶ TopPair.proj₂.comp (H j))
  (shape_δ : autoParam (∀ (i j : ι), ¬c.Rel i j → δ i j = 0) TopPair.HomologyPretheory.shape_δ._autoParam),
  sizeOf { Hₚ := Hₚ, H := H, iso := iso, δ := δ, shape_δ := shape_δ } = 1
-- Init.Data.Rat.Lemmas
Rat.mkRat_ne_zero : ∀ {d : ℕ} {n : ℤ}, d ≠ 0 → (mkRat n d ≠ 0 ↔ n ≠ 0)
-- Lean.Elab.Command
Lean.Elab.Command.State.maxRecDepth : Lean.Elab.Command.State → ℕ
-- Mathlib.LinearAlgebra.TensorProduct.Opposite
Algebra.TensorProduct.opAlgEquiv_apply : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] (x : TensorProduct R Aᵐᵒᵖ Bᵐᵒᵖ),
  (Algebra.TensorProduct.opAlgEquiv R S A B) x =
    MulOpposite.op ((TensorProduct.map ↑(MulOpposite.opLinearEquiv R).symm ↑(MulOpposite.opLinearEquiv R).symm) x)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.SupportsStmt.match_1.splitter : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4) →
        (x : Turing.TM1.Stmt Γ Λ σ) →
          ((a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.move a q)) →
            ((a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.write a q)) →
              ((a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.load a q)) →
                ((a : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.branch a q₁ q₂)) →
                  ((l : Γ → σ → Λ) → motive (Turing.TM1.Stmt.goto l)) → (Unit → motive Turing.TM1.Stmt.halt) → motive x
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
right_le_lineMap_iff_one_le : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] {a b : E} {r : k}, a < b → (b ≤ (AffineMap.lineMap a b) r ↔ 1 ≤ r)
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorPower.toTensorAlgebra_gMul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {i j : ℕ}
  (a : TensorPower R i M) (b : TensorPower R j M),
  TensorPower.toTensorAlgebra (GradedMonoid.GMul.mul a b) =
    TensorPower.toTensorAlgebra a * TensorPower.toTensorAlgebra b
-- Mathlib.NumberTheory.Rayleigh
beattySeq'.eq_1 : ∀ (r : ℝ) (k : ℤ), beattySeq' r k = ⌈↑k * r⌉ - 1
-- Mathlib.Data.Multiset.Filter
Multiset.filterMap_cons : ∀ {α : Type u_1} {β : Type v} (f : α → Option β) (a : α) (s : Multiset α),
  Multiset.filterMap f (a ::ₘ s) = (Option.map singleton (f a)).getD 0 + Multiset.filterMap f s
-- Lean.Parser.Command
Lean.Parser.Command.definition.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_add_eq_left_of_degree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.degree < p.degree → (p + q).degree = p.degree
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinAlgEquiv'_toMatrixAlgEquiv' : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (f : (n → R) →ₗ[R] n → R), Matrix.toLinAlgEquiv' (LinearMap.toMatrixAlgEquiv' f) = f
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.toMeasure_pure : ∀ {α : Type u_1} (a : α) [inst : MeasurableSpace α], (PMF.pure a).toMeasure = MeasureTheory.Measure.dirac a
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- We say that a functor creates finite products if it creates all limits of shape `Discrete J`
where `J : Type` is finite.  -/
CategoryTheory.Limits.CreatesFiniteProducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → Type (max (max (max (max 1 u₁) u₂) v₁) v₂)
-- Std.Http.Data.Status
Std.Http.Status.paymentRequired.sizeOf_spec : sizeOf Std.Http.Status.paymentRequired = 1
-- Lean.Parser.Command
Lean.Parser.Command.declaration.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.mkHom.congr_simp : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {s t : CategoryTheory.Limits.Cotrident f} (k k_1 : s.pt ⟶ t.pt) (e_k : k = k_1)
  (w : CategoryTheory.CategoryStruct.comp s.π k = t.π),
  CategoryTheory.Limits.Cotrident.mkHom k w = CategoryTheory.Limits.Cotrident.mkHom k_1 ⋯
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instInhabitedExpr : Inhabited Lean.Grind.CommRing.Expr
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).maxKey? = some (t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k')
-- Lean.Level
/-- Auxiliary function for `normalize`. See `isExplicitSubsumedAux`  -/
_private.Lean.Level.0.Lean.Level.isExplicitSubsumed : Array Lean.Level → ℕ → Bool
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- An alternative way to provide the argument to `CliffordAlgebra.lift` when `2` is invertible.

To show a function squares to the quadratic form, it suffices to show that
`f x * f y + f y * f x = algebraMap _ _ (polar Q x y)`  -/
CliffordAlgebra.forall_mul_self_eq_iff : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_4} [inst_3 : Ring A] [inst_4 : Algebra R A],
  IsUnit 2 →
    ∀ (f : M →ₗ[R] A),
      (∀ (x : M), f x * f x = (algebraMap R A) (Q x)) ↔
        (LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f =
          LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.allLTTR.loop.eq_2 : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool) (i_1 : ℕ) (h : i_1 + 1 ≤ n),
  Nat.allLTTR.loop✝ n f i_1.succ h = (f (n - (i_1 + 1)) ⋯ && Nat.allLTTR.loop✝ n f i_1 ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularMono.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y},
  Nonempty (CategoryTheory.RegularMono f) → CategoryTheory.IsRegularMono f
-- Mathlib.Topology.Defs.Filter
/-- `X` is a noncompact topological space if it is not a compact space.  -/
NoncompactSpace : (X : Type u_1) → [TopologicalSpace X] → Prop
-- Init.Data.Int.Order
Int.natAbs_of_nonneg : ∀ {a : ℤ}, 0 ≤ a → ↑a.natAbs = a
-- Mathlib.Order.RelIso.Basic
RelIso.instInhabited : {α : Type u_1} → (r : α → α → Prop) → Inhabited (r ≃r r)
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isRat_inv_pos : ∀ {α : Type u_1} [inst : DivisionRing α] [CharZero α] {a : α} {n d : ℕ},
  Mathlib.Meta.NormNum.IsRat a (Int.ofNat n.succ) d → Mathlib.Meta.NormNum.IsRat a⁻¹ (Int.ofNat d) n.succ
-- Mathlib.ModelTheory.Substructures
/-- The equivalence between the maximal substructure of a structure and the structure itself.  -/
FirstOrder.Language.Substructure.topEquiv : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → L.Equiv (↥⊤) M
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_nonpos_of_nonpos_of_neg_pi_div_two_le : ∀ {x : ℝ}, x ≤ 0 → -(Real.pi / 2) ≤ x → Real.tan x ≤ 0
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toSpanSingleton_zero : ∀ (R₁ : Type u_1) [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₁],
  ContinuousLinearMap.toSpanSingleton R₁ 0 = 0
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ)
  (hi : n + i = i') (X : CochainComplex C ℤ),
  ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₃ =
    (n.negOnePow •
        (CochainComplex.shiftEval C n ((ComplexShape.up ℤ).next i) ((ComplexShape.up ℤ).next i') ⋯).app X).hom
-- Init.Prelude
/-- A reader monad that additionally allows the value to be locally overridden.

In this class, `ρ` is an `outParam`, which means that it is inferred from `m`. `MonadWithReaderOf ρ`
provides the same operations, but allows `ρ` to influence instance synthesis.
 -/
MonadWithReader : outParam (Type u) → (Type u → Type v) → Type (max (u + 1) v)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.leftAdjointOfEquiv_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G : CategoryTheory.Functor D C} {F_obj : C → D} (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
  (he :
    ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
      (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g))
  (a : C), (CategoryTheory.Adjunction.leftAdjointOfEquiv e he).obj a = F_obj a
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_eq_of_same : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {a b : M} {d : ↥S}, f.mk' a d = f.mk' b d ↔ ∃ c, ↑c * a = ↑c * b
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.changeLevel_trans : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m d : ℕ} (hm : n ∣ m) (hd : m ∣ d),
  (DirichletCharacter.changeLevel ⋯) χ = (DirichletCharacter.changeLevel hd) ((DirichletCharacter.changeLevel hm) χ)
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_mulVec_repr : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂)
  (x : M₁), ((LinearMap.toMatrix v₁ v₂) f).mulVec ⇑(v₁.repr x) = ⇑(v₂.repr (f x))
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- The cocone on `F₂` with apex `B`.  -/
CategoryTheory.IndParallelPairPresentation.ι₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} →
        (self : CategoryTheory.IndParallelPairPresentation f g) →
          self.F₂.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const self.I).obj B
-- Mathlib.Order.Heyting.Basic
/-- A Heyting algebra is a bounded lattice with an additional binary operation `⇨` called Heyting
implication such that `(a ⇨ ·)` is right adjoint to `(a ⊓ ·)`.  -/
HeytingAlgebra : Type u_4 → Type u_4
-- Mathlib.GroupTheory.SpecificGroups.Alternating
Equiv.Perm.isThreeCycle_subset_alternatingGroup : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], {g | g.IsThreeCycle} ⊆ ↑(alternatingGroup α)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- The circleMap is continuously differentiable.  -/
contDiff_circleMap : ∀ (c : ℂ) (R : ℝ) {n : WithTop ℕ∞}, ContDiff ℝ n (circleMap c R)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.alphaEqv : Lean.IR.IndexRenaming → Lean.IR.Expr → Lean.IR.Expr → Bool
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.TaggedPrepartition.iUnion_unionComplToSubordinate_boxes : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I)
  (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → ↑(Set.Ioi 0)),
  (π₁.unionComplToSubordinate π₂ hU r).iUnion = ↑I
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- The functor `opens X ⥤ opens Y` associated with an open immersion `f : X ⟶ Y`.  -/
AlgebraicGeometry.Scheme.Hom.opensFunctor : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) → [H : AlgebraicGeometry.IsOpenImmersion f] → CategoryTheory.Functor X.Opens Y.Opens
-- Mathlib.Order.Preorder.Finite
Set.Finite.exists_le_minimal : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α} {a : α}, s.Finite → a ∈ s → ∃ b ≤ a, Minimal (fun x => x ∈ s) b
-- Batteries.Data.AssocList
Batteries.AssocList.any.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool), Batteries.AssocList.any p Batteries.AssocList.nil = false
-- Init.Data.SInt.Bitwise
Bool.toISize.eq_1 : ∀ (b : Bool), b.toISize = if b = true then 1 else 0
-- Mathlib.Order.Comparable
incompRel_of_antisymmRel_of_incompRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → IncompRel (fun x1 x2 => x1 ≤ x2) b c → IncompRel (fun x1 x2 => x1 ≤ x2) a c
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.comp_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  {X Y Z : J.ZeroHypercover S} (f : X.Hom Y.toPreZeroHypercover) (g : Y.Hom Z.toPreZeroHypercover) (i : X.I₀),
  (CategoryTheory.CategoryStruct.comp f g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.link.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (szl : ℕ) (k' : α) (v' : β k') (l' r' l'' : Std.DTreeMap.Internal.Impl α β)
  (motive :
    Std.DTreeMap.Internal.Impl.Tree α β ((Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size) →
      Sort u_3)
  (x : Std.DTreeMap.Internal.Impl.Tree α β ((Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size))
  (h_1 :
    (ℓ : Std.DTreeMap.Internal.Impl α β) →
      (hℓ₁ : ℓ.Balanced) →
        (hℓ₂ : ℓ.size = (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size) →
          motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ })
  (ℓ : Std.DTreeMap.Internal.Impl α β) (hℓ₁ : ℓ.Balanced)
  (hℓ₂ : ℓ.size = (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size),
  x = { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } →
    (match x with
      | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } => h_1 ℓ hℓ₁ hℓ₂) ≍
      h_1 ℓ hℓ₁ hℓ₂
-- Mathlib.Data.Setoid.Basic
/-- The inductively defined equivalence closure of a binary relation r is the infimum
of the set of all equivalence relations containing r.  -/
Setoid.eqvGen_eq : ∀ {α : Type u_1} (r : α → α → Prop), Relation.EqvGen.setoid r = sInf {s | ∀ ⦃x y : α⦄, r x y → s x y}
-- Init.Data.List.Lemmas
List.getElem?_replicate_of_lt : ∀ {α : Type u_1} {a : α} {n i : ℕ}, i < n → (List.replicate n a)[i]? = some a
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instCommRingOfAddOpposite : {M : Type u_1} → [CommRing Mᵃᵒᵖ] → CommRing Mᵈᵃᵃ
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_mem : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {ι : Type u_4} {S : Type u_5} {s : S}
  [inst_2 : SetLike S α] [AddSubmonoidClass S α],
  IsClosed ↑s → ∀ {f : ι → α}, (∀ (i : ι), f i ∈ s) → ∑' (i : ι), f i ∈ s
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.mul.eq_1 : ∀ (p : Lean.Grind.Linarith.Poly) (k : ℤ), p.mul k = if (k == 0) = true then Lean.Grind.Linarith.Poly.nil else p.mul' k
-- Batteries.Control.AlternativeMonad
StateT.instLawfulAlternativeLiftOfLawfulAlternativeOfLawfulMonad : ∀ {σ : Type u_1} (m : Type u_1 → Type u_2) [inst : AlternativeMonad m] [LawfulAlternative m] [LawfulMonad m],
  LawfulAlternativeLift m (StateT σ m)
-- Mathlib.Logic.Equiv.Basic
/-- Transport dependent functions through an equivalence of the base space.
 -/
Equiv.piCongrLeft' : {α : Sort u_1} → {β : Sort u_4} → (P : α → Sort u_9) → (e : α ≃ β) → ((a : α) → P a) ≃ ((b : β) → P (e.symm b))
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.zsmul_le_zsmul_of_le_of_le_of_nonneg_of_nonneg : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.IntModule M] [Lean.Grind.OrderedAdd M]
  {k₁ k₂ : ℤ} {x y : M}, k₁ ≤ k₂ → x ≤ y → 0 ≤ k₁ → 0 ≤ x → k₁ • x ≤ k₂ • y
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.insidePart.eq_1 : ∀ (p : DyckWord), p.insidePart = if h : p = 0 then 0 else (p.take (p.firstReturn + 1) ⋯).denest ⋯
-- Std.Data.TreeSet.Raw.Basic
/-- Transforms a list into a tree set.  -/
Std.TreeSet.Raw.ofList : {α : Type u} → List α → (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.ofList._auto_1) → Std.TreeSet.Raw α cmp
-- Mathlib.Data.Rel
SetRel.image_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) (S : SetRel β γ) (s : Set α),
  (R.comp S).image s = S.image (R.image s)
-- Mathlib.FieldTheory.Extension
IntermediateField.exists_algHom_adjoin_of_splits : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {S : Set E},
  (∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) →
    ∀ {L : IntermediateField F E} (f : ↥L →ₐ[F] K) (hL : L ≤ IntermediateField.adjoin F S),
      ∃ φ, φ.comp (IntermediateField.inclusion hL) = f
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverBlockAtErrPos : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.nnnorm_toLp_inl : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (x : α), ‖WithLp.toLp p (x, 0)‖₊ = ‖x‖₊
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.lmarginalPartialTraj.eq_1 : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) (a b : ℕ)
  (f : ((n : ℕ) → X n) → ENNReal) (x₀ : (n : ℕ) → X n),
  ProbabilityTheory.Kernel.lmarginalPartialTraj κ a b f x₀ =
    ∫⁻ (z : (i : ↥(Finset.Iic b)) → X ↑i),
      f
        (Function.updateFinset x₀ (Finset.Iic b)
          z) ∂(ProbabilityTheory.Kernel.partialTraj κ a b) (Preorder.frestrictLe a x₀)
-- Init.System.IOError
/-- Converts an `IO.Error` to a descriptive string.

`IO.Error.userError` is converted to its embedded message. The other constructors are converted in a
way that preserves structured information, such as error codes and filenames, that can help
diagnose the issue.
 -/
IO.Error.toString : IO.Error → String
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
/-- The Riesz content can be approximated arbitrarily well by evaluating the positive linear
functional on test functions: for any `ε > 0`, there exists a compactly supported continuous
nonnegative function `f` on `X` such that `f ≥ 1` on `K` and such that `λ(K) ≤ Λ f < λ(K) + ε`.  -/
exists_lt_rieszContentAux_add_pos : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  [T2Space X] [LocallyCompactSpace X] (K : TopologicalSpace.Compacts X) {ε : NNReal},
  0 < ε → ∃ f, (∀ x ∈ K, 1 ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.sepByFnAux.parse : Lean.Parser.ParserFn →
  Lean.Parser.ParserFn → Bool → ℕ → Bool → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzWith.mul : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E}, LipschitzWith Kf f → LipschitzWith Kg g → LipschitzWith (Kf + Kg) fun x => f x * g x
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomologyMapData.neg_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂), γ.neg.right = γ.right.neg
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- Any relatively compact set in a pseudometric space can be covered by finitely many balls of a
given positive radius.  -/
exists_finite_cover_balls_of_isCompact_closure : ∀ {X : Type u_2} [inst : PseudoMetricSpace X] {s : Set X} {ε : ℝ},
  IsCompact (closure s) → 0 < ε → ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, Metric.ball x ε
-- Mathlib.Topology.Order.LeftRightLim
rightLim_eq_of_isTop : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] {f : α → β} {a : α},
  IsTop a → Function.rightLim f a = f a
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.toFunBilinear_apply_apply : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A)
  (p : Polynomial R), ((PolyEquivTensor.toFunBilinear R A) a) p = a • (Polynomial.aeval Polynomial.X) p
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Tensoring on the right with `X ⊗ Y` is naturally isomorphic to
tensoring on the right with `X`, and then again with `Y`.
 -/
CategoryTheory.MonoidalCategory.tensorRightTensor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y : C) →
        CategoryTheory.MonoidalCategory.tensorRight (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ≅
          (CategoryTheory.MonoidalCategory.tensorRight X).comp (CategoryTheory.MonoidalCategory.tensorRight Y)
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasProducts A]
  (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C))
  [inst_3 : CategoryTheory.Preadditive A] (X : CategoryTheory.Functor Cᵒᵖ A) (n : ℕ),
  ((CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor E).obj X).X n =
    ∏ᶜ fun i => X.obj (Opposite.op ((E.obj (Opposite.op { len := n })).obj i))
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instCofibrationCompOfIsStableUnderCompositionCofibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition] [hf : HomotopicalAlgebra.Cofibration f]
  [hg : HomotopicalAlgebra.Cofibration g], HomotopicalAlgebra.Cofibration (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.set_mul_normalizer_comm : ∀ {G : Type u_2} [inst : Group G] (S : Set G) (N : Subgroup G), S ⊆ ↑(Subgroup.normalizer ↑N) → S * ↑N = ↑N * S
-- Mathlib.Algebra.Module.PUnit
PUnit.instVAdd_mathlib : {R : Type u_1} → VAdd PUnit.{u_3 + 1} R
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
/-- The triangle indices for the Ruzsa-Szemerédi construction.  -/
_private.Mathlib.Combinatorics.Extremal.RuzsaSzemeredi.0.triangleIndices : {α : Type u_1} → [Fintype α] → [CommRing α] → Finset α → Finset (α × α × α)
-- Mathlib.Data.Set.Lattice
Set.iInter_eq_compl_iUnion_compl : ∀ {β : Type u_2} {ι : Sort u_5} (s : ι → Set β), ⋂ i, s i = (⋃ i, (s i)ᶜ)ᶜ
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_ofNatLT : ∀ {n : ℕ} (h : n < UInt8.size), (UInt8.ofNatLT n h).toUInt64 = UInt64.ofNatLT n ⋯