mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.rankOne_one_right_eq_toSpanSingleton : ∀ {𝕜 : Type u_4} {F : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  (x : F), ((InnerProductSpace.rankOne 𝕜) x) 1 = ContinuousLinearMap.toSpanSingleton 𝕜 x
-- Mathlib.Order.Filter.Basic
/-- **Alias** of `Filter.sdiff_mem_inf_principal_compl`. -/
Filter.diff_mem_inf_principal_compl : ∀ {α : Type u} {f : Filter α} {s : Set α}, s ∈ f → ∀ (t : Set α), s \ t ∈ f ⊓ Filter.principal tᶜ
-- Mathlib.Topology.Connected.Basic
PreconnectedSpace.mk : ∀ {α : Type u} [inst : TopologicalSpace α], IsPreconnected Set.univ → PreconnectedSpace α
-- Mathlib.CategoryTheory.Limits.Final.Connected
CategoryTheory.instFinalDiscreteOfIsConnected : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : Type w} [Unique T]
  (F : CategoryTheory.Functor C (CategoryTheory.Discrete T)) [CategoryTheory.IsConnected C], F.Final
-- Mathlib.CategoryTheory.Triangulated.Subcategory
/-- Given `P : ObjectProperty C` with `C` a pretriangulated category, this
is the property that whenever `X₁ ⟶ X₂ ⟶ X₃ ⟶ X₁⟦1⟧` is a distinguished triangle
such that `P X₁` and `P X₂` hold, then `P.isoClosure X₃` holds.  -/
CategoryTheory.ObjectProperty.IsTriangulatedClosed₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [CategoryTheory.Pretriangulated C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Order.Comparable
/-- Exactly one of the following is true.  -/
lt_or_antisymmRel_or_gt_or_incompRel : ∀ {α : Type u_1} [inst : Preorder α] (a b : α),
  a < b ∨ AntisymmRel (fun x1 x2 => x1 ≤ x2) a b ∨ b < a ∨ IncompRel (fun x1 x2 => x1 ≤ x2) a b
-- Batteries.Data.Float.Basic
/-- Returns `v, exp` integers such that `f = v * 2^exp`.
Like `toRatParts`, but `e` is guaranteed to be minimal (`v` is always odd), unless `v = 0`.
`v.abs` will be at most `2^53 - 1` because `Float` has 53 bits of precision.
Returns `none` when `f` is not finite (i.e. `inf`, `-inf` or a `nan`).  -/
Float.toRatParts' : Float → Option (ℤ × ℤ)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (toAddEquiv : α ≃+ β) (map_le_map_iff' : ∀ {a b : α}, toAddEquiv.toFun a ≤ toAddEquiv.toFun b ↔ a ≤ b)
  (toAddEquiv_1 : α ≃+ β) (map_le_map_iff'_1 : ∀ {a b : α}, toAddEquiv_1.toFun a ≤ toAddEquiv_1.toFun b ↔ a ≤ b),
  ({ toAddEquiv := toAddEquiv, map_le_map_iff' := map_le_map_iff' } =
      { toAddEquiv := toAddEquiv_1, map_le_map_iff' := map_le_map_iff'_1 }) =
    (toAddEquiv = toAddEquiv_1)
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivial.trivialization.isLinear : ∀ (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace B],
  Bundle.Trivialization.IsLinear 𝕜 (Bundle.Trivial.trivialization B F)
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.mem_centralizer_iff : ∀ {M : Type u_1} {S : Set M} [inst : AddMonoid M] {z : M}, z ∈ AddSubmonoid.centralizer S ↔ ∀ g ∈ S, g + z = z + g
-- Mathlib.AlgebraicGeometry.Cover.Directed
/-- The directed affine open cover of `X` given by all affine opens.  -/
AlgebraicGeometry.Scheme.directedAffineCover : (X : AlgebraicGeometry.Scheme) → X.OpenCover
-- Mathlib.CategoryTheory.Functor.OfSequence
_private.Mathlib.CategoryTheory.Functor.OfSequence.0.CategoryTheory.Functor.OfSequence.map.match_3.eq_2 : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  (motive : (x : ℕ → C) → ((n : ℕ) → x n ⟶ x (n + 1)) → ℕ → ℕ → Sort u_3) (x : ℕ → C) (f : (n : ℕ) → x n ⟶ x (n + 1))
  (h_1 : (x : ℕ → C) → (x_1 : (n : ℕ) → x n ⟶ x (n + 1)) → motive x x_1 0 0)
  (h_2 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → motive x f 0 1)
  (h_3 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → (l : ℕ) → motive x f 0 l.succ)
  (h_4 : (x : ℕ → C) → (x_1 : (n : ℕ) → x n ⟶ x (n + 1)) → (n : ℕ) → motive x x_1 n.succ 0)
  (h_5 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → (k l : ℕ) → motive x f k.succ l.succ),
  (match x, f, 0, 1 with
    | x, x_1, 0, 0 => h_1 x x_1
    | x, f, 0, 1 => h_2 x f
    | x, f, 0, l.succ => h_3 x f l
    | x, x_1, n.succ, 0 => h_4 x x_1 n
    | x, f, k.succ, l.succ => h_5 x f k l) =
    h_2 x f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {a : α}, m.contains a = false → Std.DHashMap.Const.get! m a = default
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.Rels.add.sizeOf_spec : ∀ {R : Type u} {ι : Type u_4} {M : Type u_5} [inst : SizeOf R] [inst_1 : SizeOf ι] [inst_2 : SizeOf M] (m : ι → M)
  (i : ι) (x y : M), sizeOf (exteriorPower.presentation.Rels.add m i x y) = 1 + sizeOf i + sizeOf x + sizeOf y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  {f : (a : α) → β a → γ a} {k fallback : α},
  t.WF → (Std.DTreeMap.Internal.Impl.map f t).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.mem_rcons_iff : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : (i : ι) → DecidableEq (M i)] {i j : ι}
  (p : Monoid.CoprodI.Word.Pair M i) (m : M j),
  ⟨j, m⟩ ∈ (Monoid.CoprodI.Word.rcons p).toList ↔ ⟨j, m⟩ ∈ p.tail.toList ∨ m ≠ 1 ∧ ∃ (h : i = j), m = h ▸ p.head
-- Mathlib.Algebra.Exact.Basic
Function.Exact.linearEquivOfSurjective_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) (x : N ⧸ f.range),
  (h.linearEquivOfSurjective hg) x = (f.range.liftQ g ⋯) x
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.PosNum.divMod.match_3.eq_2 : ∀ (motive : PosNum → Sort u_1) (n : PosNum) (h_1 : (n : PosNum) → motive n.bit0) (h_2 : (n : PosNum) → motive n.bit1)
  (h_3 : Unit → motive PosNum.one),
  (match n.bit1 with
    | n.bit0 => h_1 n
    | n.bit1 => h_2 n
    | PosNum.one => h_3 ()) =
    h_2 n
-- Mathlib.Data.Finset.Max
Finset.mem_of_max : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} {a : α}, s.max = ↑a → a ∈ s
-- Init.Data.UInt.Lemmas
UInt64.add_sub_cancel : ∀ (a b : UInt64), a + b - b = a
-- Mathlib.Order.Filter.Lift
Filter.lift'_mono : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {h₁ h₂ : Set α → Set β},
  f₁ ≤ f₂ → h₁ ≤ h₂ → f₁.lift' h₁ ≤ f₂.lift' h₂
-- Std.Data.TreeSet.Basic
/-- Check if any element satisfies the predicate, short-circuiting if a predicate succeeds.  -/
Std.TreeSet.all : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → (α → Bool) → Bool
-- Mathlib.CategoryTheory.Quotient
/-- For `F : C ⥤ D`, `F.homRel` is a congruence.  -/
CategoryTheory.Functor.congruence_homRel : ∀ {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_2, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] (F : CategoryTheory.Functor C D), CategoryTheory.Congruence F.homRel
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.submodule_closure_single : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (F : I.Filtration M), AddSubmonoid.closure (⋃ i, PolynomialModule.single R i '' ↑(F.N i)) = F.submodule.toAddSubmonoid
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] (P : Algebra.PreSubmersivePresentation R S ι σ) (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀]
  (x : MvPolynomial ι R₀),
  (algebraMap (MvPolynomial ι R₀)
        (MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Algebra.Presentation.relationOfHasCoeffs R₀))))
      x =
    (Ideal.Quotient.mk (Ideal.span (Set.range (Algebra.Presentation.relationOfHasCoeffs R₀)))) x
-- Init.System.IOError
/-- The operation was interrupted.

This corresponds to the POSIX error `EINTR`.
 -/
IO.Error.interrupted : String → UInt32 → String → IO.Error
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushoutCoconeOfRightIso_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g],
  (CategoryTheory.Limits.pushoutCoconeOfRightIso f g).inl = CategoryTheory.CategoryStruct.id Y
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_sup_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Injective ⇑f →
    ∀ (S T : Subsemigroup M), Subsemigroup.comap f (Subsemigroup.map f S ⊔ Subsemigroup.map f T) = S ⊔ T
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.toTopCat_obj : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)] (Y : ContinuousGeneratedByCat X),
  (ContinuousGeneratedByCat.toTopCat X).obj Y = TopCat.of (Topology.WithGeneratedByTopology X ↑Y)
-- Init.System.IOError
IO.Error.mkEofError : Unit → IO.Error
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk_d_1_0 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) →
      (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0),
  (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 0 = d₀
-- Lean.Parser.Basic
Lean.Parser.OrElseOnAntiquotBehavior.noConfusionType : Sort v✝ → Lean.Parser.OrElseOnAntiquotBehavior → Lean.Parser.OrElseOnAntiquotBehavior → Sort v✝
-- Mathlib.Data.Rel
SetRel.isSymm_inv_comp : ∀ {α : Type u_1} {R : SetRel α α}, (R.inv.comp R).IsSymm
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- compatibility condition  -/
CategoryTheory.Endofunctor.Algebra.Hom.h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (self : A₀.Hom A₁),
  CategoryTheory.CategoryStruct.comp (F.map self.f) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str self.f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
/-- The `Z`-coordinate of a representative of `2 • P` for a Jacobian point representative `P` on a
Weierstrass curve.  -/
WeierstrassCurve.Jacobian.dblZ : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → R
-- Mathlib.Data.Matrix.Basis
Matrix.single_mul_apply_of_ne : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq l] [inst_1 : DecidableEq m]
  [inst_2 : Fintype m] [inst_3 : NonUnitalNonAssocSemiring α] (c : α) (i : l) (j : m) (a : l) (b : n),
  a ≠ i → ∀ (M : Matrix m n α), (Matrix.single i j c * M) a b = 0
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.toSubgraph_surjOn : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β},
  Set.SurjOn SimpleGraph.Copy.toSubgraph Set.univ {B' | Nonempty (A ≃g B'.coe)}
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.faithful_sheafPushforwardContinuous : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G],
  (G.sheafPushforwardContinuous A J K).Faithful
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, k ∉ m₁ → (m₁ \ m₂).get! k = default
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum over `s.subtype pred` equals one over `{x ∈ s | pred x}`.  -/
Finset.weightedVSubOfPoint_subtype_eq_filter : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (b : P) (pred : ι → Prop)
  [inst_3 : DecidablePred pred],
  (((Finset.subtype pred s).weightedVSubOfPoint (fun i => p ↑i) b) fun i => w ↑i) =
    ({x ∈ s | pred x}.weightedVSubOfPoint p b) w
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItem.label : Lean.Lsp.CompletionItem → String
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.nilpotent_iff_lowerCentralSeries`.

---

A group is nilpotent if and only if its lower central series eventually reaches
the trivial subgroup.  -/
nilpotent_iff_lowerCentralSeries : ∀ {G : Type u_1} [inst : Group G], Group.IsNilpotent G ↔ ∃ n, ⊤.lowerCentralSeries n = ⊥
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_fract : ∀ {F : Type u_1} {H : Type u_3} {b : H} {R : Type u_4} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R]
  [inst_3 : AddGroup H] [inst_4 : FunLike F R H] [AddConstMapClass F R H 1 b] (f : F) (x : R),
  f (Int.fract x) = f x - ⌊x⌋ • b
-- Mathlib.Algebra.Order.Star.Basic
/-- While `IsSelfAdjoint.map` assumes the map is star-preserving, this lemma instead assumes the
map is an order-preserving additive map from a space where self-adjoint elements can be expressed as
differences of nonnegative elements, and whose codomain is a star-ordered ring. When such maps are
linear over `ℂ`, they are also star-preserving, and this lemma is used to establish that one by
splitting into real and imaginary parts.  -/
IsSelfAdjoint.map' : ∀ {F : Type u_6} {E : Type u_7} {R : Type u_8} [inst : AddCommGroup E] [inst_1 : PartialOrder E]
  [inst_2 : StarAddMonoid E] [inst_3 : NonUnitalRing R] [inst_4 : PartialOrder R] [inst_5 : StarRing R]
  [StarOrderedRing R] [SelfAdjointDecompose E] [inst_8 : FunLike F E R] [OrderHomClass F E R] [AddMonoidHomClass F E R]
  {a : E}, IsSelfAdjoint a → ∀ (f : F), IsSelfAdjoint (f a)
-- Mathlib.Analysis.Complex.AbsMax
/-- **Maximum modulus principle** on a connected set. Let `U` be a (pre)connected open set in a
complex normed space. Let `f : E → F` be a function that is complex differentiable on `U`. Suppose
that `‖f x‖` takes its maximum value on `U` at `c ∈ U`. Then `‖f x‖ = ‖f c‖` for all `x ∈ U`.  -/
Complex.norm_eqOn_of_isPreconnected_of_isMaxOn : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {f : E → F} {U : Set E} {c : E},
  IsPreconnected U →
    IsOpen U → DifferentiableOn ℂ f U → c ∈ U → IsMaxOn (norm ∘ f) U c → Set.EqOn (norm ∘ f) (Function.const E ‖f c‖) U
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag'_zero : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : Zero α], Matrix.blockDiag' 0 = 0
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.symm_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C],
  P.symm.i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding A A).hom P.i
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.allDiffAux : {α : Type u} → [BEq α] → Array α → ℕ → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.of_forall_isPushout_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F₁ F₂ F₃ F₄ : CategoryTheory.Functor C D} {f₁ : F₁ ⟶ F₂} {f₂ : F₁ ⟶ F₃} {f₃ : F₂ ⟶ F₄} {f₄ : F₃ ⟶ F₄},
  (∀ (X : C), CategoryTheory.IsPushout (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)) →
    CategoryTheory.IsPushout f₁ f₂ f₃ f₄
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.id_adj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a : CategoryTheory.Bicategory.Adj B),
  (CategoryTheory.CategoryStruct.id a).adj = CategoryTheory.Bicategory.Adjunction.id a.obj
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
/-- Exterior derivative of a differential form within a set.

There are a few competing definitions of the exterior derivative of a differential form
that differ from each other by a normalization factor.
We use the following one:

$$
dω(x; v_0, \dots, v_n) = \sum_{i=0}^n (-1)^i D_x ω(x; v_0, \dots, \widehat{v_i}, \dots, v_n) · v_i
$$

where $\widehat{v_i}$ means that we omit this element of the tuple, see `extDerivWithin_apply`.
 -/
extDerivWithin : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → {n : ℕ} → (E → E [⋀^Fin n]→L[𝕜] F) → Set E → E → E [⋀^Fin (n + 1)]→L[𝕜] F
-- Mathlib.Algebra.Order.Star.Basic
star_left_conjugate_pos : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {a : R}, 0 < a → ∀ {c : R}, IsRegular c → 0 < star c * a * c
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β],
  Finset.vadd = { vadd := Finset.image₂ fun x1 x2 => x1 +ᵥ x2 }
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.ofRingHom_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (g : S →+* R)
  (h₁ : f.comp g = RingHom.id S) (h₂ : g.comp f = RingHom.id R) (a : R), (RingEquiv.ofRingHom f g h₁ h₂) a = f a
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_succEmb_Ico : ∀ {n : ℕ} (i j : Fin n), Finset.map (Fin.succEmb n) (Finset.Ico i j) = Finset.Ico i.succ j.succ
-- Mathlib.Algebra.FreeAlgebra
/-- `FreeAlgebra R X` is nontrivial when `R` is.  -/
FreeAlgebra.instNontrivial : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] [Nontrivial R], Nontrivial (FreeAlgebra R X)
-- Mathlib.Order.Category.BoolAlg
BoolAlg.ofHom_comp : ∀ {X Y Z : Type u} [inst : BooleanAlgebra X] [inst_1 : BooleanAlgebra Y] [inst_2 : BooleanAlgebra Z]
  (f : BoundedLatticeHom X Y) (g : BoundedLatticeHom Y Z),
  BoolAlg.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (BoolAlg.ofHom f) (BoolAlg.ofHom g)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrp_obj_grp_one : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (A : CategoryTheory.Grp C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.MonObj.one)
-- Init.Meta.Defs
/-- Syntax that represents a string literal.
 -/
Lean.Syntax.StrLit : Type
-- Mathlib.Data.WSeq.Defs
/-- Get the indexes of occurrences of `a` in `s`  -/
Stream'.WSeq.indexesOf : {α : Type u} → [DecidableEq α] → α → Stream'.WSeq α → Stream'.WSeq ℕ
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_one : ∀ {x z : ℝ}, 0 ≤ x → x ≤ 1 → 0 ≤ z → x ^ z ≤ 1
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.restrictScalars_toLinearMap : ∀ (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module S M] [inst_7 : Module S M₂] [inst_8 : LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂),
  ↑(LinearEquiv.restrictScalars R f) = ↑R ↑f
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.uniformSpace_eq : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : UniformSpace F] [inst_8 : IsUniformAddGroup F]
  (𝔖 : Set (Set E)),
  UniformConvergenceCLM.instUniformSpace σ F 𝔖 =
    UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
StandardBorelSpace.instMeasurableEq : ∀ {α : Type u_1} [inst : MeasurableSpace α] [StandardBorelSpace α], MeasurableEq α
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.le_iff : ∀ {X : Type u_1} {d₁ d₂ : DiffeologicalSpace X},
  d₁ ≤ d₂ ↔ ∀ (n : ℕ), DiffeologicalSpace.plots n ⊆ DiffeologicalSpace.plots n
-- Batteries.Lean.LawfulMonadLift
_private.Batteries.Lean.LawfulMonadLift.0.EIO.toBaseIO.match_1.splitter : {ε α : Type} →
  (motive : EST.Out ε IO.RealWorld α → Sort u_1) →
    (x : EST.Out ε IO.RealWorld α) →
      ((a : α) → (s : Void IO.RealWorld) → motive (EST.Out.ok a s)) →
        ((ex : ε) → (s : Void IO.RealWorld) → motive (EST.Out.error ex s)) → motive x
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pushforward_map_app : ∀ {X Y : AlgebraicGeometry.Scheme} {M N : X.Modules} (f : X ⟶ Y) (φ : M ⟶ N) (U : Y.Opens),
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.pushforward f).map φ) U =
    AlgebraicGeometry.Scheme.Modules.Hom.app φ ((TopologicalSpace.Opens.map f.base).obj U)
-- Init.Data.Array.OfFn
Array.toList_ofFnM : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [inst : Monad m] [LawfulMonad m] {f : Fin n → m α},
  Array.toList <$> Array.ofFnM f = List.ofFnM f
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
/-- A category has countable coproducts if it has all coproducts indexed by countable types.  -/
CategoryTheory.Limits.HasCountableCoproducts : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.measureReal_eq_measureReal_larger_of_between_null_sdiff`. -/
MeasureTheory.measureReal_eq_measureReal_larger_of_between_null_diff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α},
  s₁ ⊆ s₂ →
    s₂ ⊆ s₃ →
      μ.real (s₃ \ s₁) = 0 →
        autoParam (μ (s₃ \ s₁) ≠ ⊤) MeasureTheory.measureReal_eq_measureReal_larger_of_between_null_sdiff._auto_1 →
          μ.real s₂ = μ.real s₃
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- On a set with unique derivatives, a `C^n` function has derivatives up to `n` which are
continuous.  -/
ContDiffOn.continuousOn_iteratedDerivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : WithTop ℕ∞} {m : ℕ},
  ContDiffOn 𝕜 n f s → ↑m ≤ n → UniqueDiffOn 𝕜 s → ContinuousOn (iteratedDerivWithin m f s) s
-- Mathlib.Algebra.BigOperators.Ring.Nat
Finset.odd_sum_iff_odd_card_odd : ∀ {ι : Type u_1} {s : Finset ι} (f : ι → ℕ), Odd (∑ i ∈ s, f i) ↔ Odd {x ∈ s | Odd (f x)}.card
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.rclike_simps_proc : Lean.ParserDescr