mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.LinearIsometry
LinearIsometry.strictConvexSpace_range : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F]
  [StrictConvexSpace 𝕜 E] (e : E →ₗᵢ[𝕜] F), StrictConvexSpace 𝕜 ↥(↑e).range
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.rcons_eq_smul : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {i : ι} (p : Monoid.CoprodI.Word.Pair M i),
  Monoid.CoprodI.Word.rcons p = Monoid.CoprodI.of p.head • p.tail
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
/-- Also see `IsTranscendenceBasis.algebraMap_comp`
for the composition with an algebraic extension.  -/
AlgEquiv.isTranscendenceBasis : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing A'] [inst_3 : Algebra R A] [inst_4 : Algebra R A'] (e : A ≃ₐ[R] A'),
  IsTranscendenceBasis R x → IsTranscendenceBasis R (⇑e ∘ x)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.instIsIsoInvApp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X),
  CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f U)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_eq_fallback : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a fallback : α},
  a ∉ t → t.getKeyD a fallback = fallback
-- Mathlib.Algebra.Order.SuccPred
monotoneOn_of_le_add_one : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : One α]
  [inst_4 : SuccAddOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f a ≤ f (a + 1)) → MonotoneOn f s
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.ofSubsingleton_toAlternatingMap : ∀ (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : Subsingleton ι] (i : ι) (f : M →L[R] N),
  ((ContinuousAlternatingMap.ofSubsingleton R M N i) f).toAlternatingMap = (AlternatingMap.ofSubsingleton R M N i) ↑f
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.instReprDaylightSavingRule : Repr Std.Time.TimeZone.DaylightSavingRule
-- Init.Notation
/-- Position reporting for `#guard_msgs`:
- `positions := true` will report the positions of messages with the line numbers computed
  relative to the line of the `#guard_msgs` token, e.g.
  ```
  @ +3:7...+4:2
  info: <message>
  ```
  Note that the reported column is absolute.
- `positions := false` (the default) will not render positions.
 -/
Lean.guardMsgsPositions : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.TangentCone.Prod
/-- The tangent cone of a product contains the tangent cone of its left factor.  -/
subset_tangentConeAt_prod_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [inst_6 : AddCommGroup F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {x : E} {s : Set E}
  {y : F} {t : Set F}, y ∈ closure t → ⇑(LinearMap.inl 𝕜 E F) '' tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)
-- Mathlib.Topology.Order.T5
OrderTopology.t5Space : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X], T5Space X
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.kerAdjunction_counit_app : ∀ (Y : AlgebraicGeometry.Scheme) (f : (CategoryTheory.Over Y)ᵒᵖ),
  Y.kerAdjunction.counit.app f =
    (CategoryTheory.Over.homMk (AlgebraicGeometry.Scheme.Hom.toImage (Opposite.unop f).hom) ⋯).op
-- Mathlib.SetTheory.ZFC.Cardinal
ZFSet.card_empty : ∅.card = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_insertMany_list : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (↑(m.insertMany l)).contains k = (m.contains k || (List.map Sigma.fst l).contains k)
-- Init.Core
Lean.Syntax.ident.inj : ∀ {info : Lean.SourceInfo} {rawVal : Substring.Raw} {val : Lean.Name} {preresolved : List Lean.Syntax.Preresolved}
  {info_1 : Lean.SourceInfo} {rawVal_1 : Substring.Raw} {val_1 : Lean.Name}
  {preresolved_1 : List Lean.Syntax.Preresolved},
  Lean.Syntax.ident info rawVal val preresolved = Lean.Syntax.ident info_1 rawVal_1 val_1 preresolved_1 →
    info = info_1 ∧ rawVal = rawVal_1 ∧ val = val_1 ∧ preresolved = preresolved_1
-- Mathlib.Analysis.Convex.Combination
/-- `convexHull` is an additive monoid morphism under pointwise addition.  -/
convexHullAddMonoidHom : (R : Type u_1) →
  (E : Type u_3) →
    [inst : Field R] →
      [inst_1 : AddCommGroup E] → [Module R E] → [inst_3 : LinearOrder R] → [IsStrictOrderedRing R] → Set E →+ Set E
-- Mathlib.Tactic.Widget.StringDiagram
/-- The underlying expression of the variable.  -/
Mathlib.Tactic.Widget.StringDiagram.PenroseVar.e : Mathlib.Tactic.Widget.StringDiagram.PenroseVar → Lean.Expr
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instIsStableUnderBaseChangeFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)],
  (HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverse_mem_evenOdd_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) {x : CliffordAlgebra Q} {n : ZMod 2},
  CliffordAlgebra.reverse x ∈ CliffordAlgebra.evenOdd Q n ↔ x ∈ CliffordAlgebra.evenOdd Q n
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.algebraMap_norm_eq_mul_star : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (z : QuadraticAlgebra R a b),
  (algebraMap R (QuadraticAlgebra R a b)) (QuadraticAlgebra.norm z) = z * star z
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.get!_eq_getValueCast! : ∀ {α : Type u} {β : α → Type v} [instBEq : BEq α] [inst : Ord α] [inst_1 : Std.LawfulBEqOrd α] [Std.TransOrd α]
  [inst_3 : Std.LawfulEqOrd α] {k : α} [inst_4 : Inhabited (β k)] {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered → t.get! k = Std.Internal.List.getValueCast! k t.toListModel
-- Mathlib.Topology.CantorBendixson
/-- If the iterated derived set stops changing at a successor stage, then `sᵈ[a]` is a fixed
point of `relDerivSet`.  -/
CantorBendixson.mem_fixedPoints_of_iteratedDerivedSet_succ_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {a : Ordinal.{u}},
  CantorBendixson.iteratedDerivedSet s (a + 1) = CantorBendixson.iteratedDerivedSet s a →
    CantorBendixson.iteratedDerivedSet s a ∈ Function.fixedPoints ⇑relDerivedSet
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop_embDomain : ∀ {Γ' : Type u_2} {R : Type u_3} [inst : Zero R] [inst_1 : PartialOrder Γ'] {Γ : Type u_5} [inst_2 : LinearOrder Γ]
  {f : Γ ↪o Γ'} {x : HahnSeries Γ R}, (HahnSeries.embDomain f x).orderTop = WithTop.map (⇑f) x.orderTop
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_fst_of_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion (CategoryTheory.Limits.pullback.fst g f)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.comp_def : ∀ {B : Type u} [inst : Quiver B] {a b c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.FreeBicategory.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
orthogonalFamily_iff_pairwise : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {V : ι → Submodule 𝕜 E},
  (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) ↔ Pairwise (Function.onFun (fun x1 x2 => x1 ⟂ x2) V)
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.smulZeroClass : {I : Type u} →
  {f : I → Type v} →
    (α : Type u_1) → {n : (i : I) → Zero (f i)} → [(i : I) → SMulZeroClass α (f i)] → SMulZeroClass α ((i : I) → f i)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_cons : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {hd : α} {tl : List α},
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity (hd :: tl)) =
    ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit
        (Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertIfNew hd ()) tl)
-- Mathlib.Algebra.Group.Int.Defs
Int.zsmul_eq_mul : ∀ (n a : ℤ), n • a = n * a
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialProd_contractNth : ∀ {G : Type u_3} [inst : Monoid G] {n : ℕ} (g : Fin (n + 1) → G) (a : Fin (n + 1)),
  Fin.partialProd (a.contractNth (fun x1 x2 => x1 * x2) g) = Fin.partialProd g ∘ a.succ.succAbove
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
uniqueMDiffWithinAt_iff_uniqueDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E}, UniqueMDiffAt[s] x ↔ UniqueDiffWithinAt 𝕜 s x
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜}, MeromorphicOn f U → MeromorphicOn (-f) U
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.isOpen_preimage_ofLawson : ∀ {α : Type u_1} [inst : Preorder α] {S : Set α},
  IsOpen (⇑Topology.WithLawson.ofLawson ⁻¹' S) ↔ TopologicalSpace.IsOpen S
-- Init.Core
/-- `∅` or `{}` is the empty set or empty collection.
It is supported by the `EmptyCollection` typeclass. 

Conventions for notations in identifiers:

 * The recommended spelling of `{}` in identifiers is `empty`. -/
«term{}» : Lean.ParserDescr
-- Init.Data.List.Lex
List.nil_lt_cons : ∀ {α : Type u_1} [inst : LT α] (a : α) (l : List α), [] < a :: l
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.instBEqMon.beq.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit)
  (h_2 :
    (a : Lean.Grind.CommRing.Power) →
      (a_1 : Lean.Grind.CommRing.Mon) →
        (b : Lean.Grind.CommRing.Power) →
          (b_1 : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult a a_1) (Lean.Grind.CommRing.Mon.mult b b_1))
  (h_3 : (x x_1 : Lean.Grind.CommRing.Mon) → motive x x_1),
  (match Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit with
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => h_1 ()
    | Lean.Grind.CommRing.Mon.mult a a_1, Lean.Grind.CommRing.Mon.mult b b_1 => h_2 a a_1 b b_1
    | x, x_1 => h_3 x x_1) =
    h_1 ()
-- Mathlib.Analysis.Normed.Group.Basic
enorm_mul_le' : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ESeminormedMonoid E] (a b : E), ‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioi_nonempty : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α], (Finset.Ioi a).Nonempty ↔ ¬IsMax a
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.refl_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V] {ρ : ContRepresentation R G V}
  (v : V), (ContRepresentation.Equiv.refl ρ) v = v
-- Init.Data.Order.Classes
/-- This typeclass states that the synthesized `LT α` instance is compatible with the `LE α`
instance. This means that `LT.lt a b` holds if and only if `a` is less or equal to `b` according
to the `LE α` instance, but `b` is not less or equal to `a`.

`LawfulOrderLT α` automatically entails that `LT α` is asymmetric: `a < b` and `b < a` can never
be true simultaneously.

`LT α` does not uniquely determine the `LE α`: There can be only one compatible order data
instance that is total, but there can be others that are not total.
 -/
Std.LawfulOrderLT : (α : Type u) → [LT α] → [LE α] → Prop
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.tendsto_atTop_of_linearGrowthInf_natCast_pos : ∀ {v : ℕ → ℕ}, (LinearGrowth.linearGrowthInf fun n => ↑(v n)) ≠ 0 → Filter.Tendsto v Filter.atTop Filter.atTop
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- **Alias** of `isTotallyDisconnected_of_isTotallySeparated`. -/
IsTotallySeparated.isTotallyDisconnected : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsTotallySeparated s → IsTotallyDisconnected s
-- Mathlib.Algebra.Polynomial.Derivation
Polynomial.derivation_ext : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (Polynomial R) A] {D₁ D₂ : Derivation R (Polynomial R) A},
  D₁ Polynomial.X = D₂ Polynomial.X → D₁ = D₂
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- **Alias** of `Convexity.ConvexSpace.sConvexComb_single`.

---

A convex combination of a single point is that point.  -/
Convexity.ConvexSpace.convexCombination_single : ∀ {R : Type u} {M : Type v} {inst₁ : PartialOrder R} {inst₂ : Semiring R} {inst₃ : IsStrictOrderedRing R}
  [self : Convexity.ConvexSpace R M] (x : M), Convexity.sConvexComb (Convexity.StdSimplex.single x) = x
-- Mathlib.GroupTheory.Torsion
/-- For prime `p`, `g` lies in the `p`-primary component iff its order is a power of `p`.  -/
CommGroup.mem_primaryComponent_iff_orderOf : ∀ {G : Type u_1} [inst : CommGroup G] {p : ℕ} [Fact (Nat.Prime p)] {g : G},
  g ∈ CommGroup.primaryComponent G p ↔ ∃ n, orderOf g = p ^ n
-- Mathlib.Algebra.Module.LinearMap.End
LinearMap.smulRight_zero : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R M] [inst_4 : Module R M₁] [inst_5 : Semiring S] [inst_6 : Module R S]
  [inst_7 : Module S M] [inst_8 : IsScalarTower R S M] (f : M₁ →ₗ[R] S), f.smulRight 0 = 0
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.hom_comp_hom`. -/
CategoryTheory.Classifier.hom_comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒞₁ 𝒞₂ 𝒞₃ : CategoryTheory.Subobject.Classifier C),
  CategoryTheory.CategoryStruct.comp (𝒞₁.hom 𝒞₂) (𝒞₂.hom 𝒞₃) = 𝒞₁.hom 𝒞₃
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.mk.sizeOf_spec : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  [inst_2 : (a : Type u) → SizeOf (F a)] [inst_3 : (a : Type u) → SizeOf (G a)] (app : (α : Type u) → F α → G α)
  (preserves_pure' : ∀ {α : Type u} (x : α), app α (pure x) = pure x)
  (preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app β (x <*> y) = app (α → β) x <*> app α y),
  sizeOf { app := app, preserves_pure' := preserves_pure', preserves_seq' := preserves_seq' } = 1
-- Mathlib.Algebra.Order.Group.Equiv
toLexMulEquiv.eq_1 : ∀ (α : Type u_1) [inst : Mul α], toLexMulEquiv α = { toEquiv := toLex, map_mul' := ⋯ }
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Precomposing `f` with `Prod.snd` is `C^n` at `(x, y)`  -/
ContDiffAt.snd' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : F → G} {x : E} {y : F},
  ContDiffAt 𝕜 n f y → ContDiffAt 𝕜 n (fun x => f x.2) (x, y)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
IsSelfAdjoint.toReal_spectralRadius_eq_norm : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a : A}, IsSelfAdjoint a → (spectralRadius ℝ a).toReal = ‖a‖
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_iff_of_mem_source' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x x' : M}
  {y : M'} {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n M'],
  x' ∈ (chartAt H x).source →
    f x' ∈ (chartAt H' y).source →
      (ContMDiffWithinAt I I' n f s x' ↔
        ContinuousWithinAt f s x' ∧
          ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
            ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
            (↑(extChartAt I x) x'))
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.hom_comp : ∀ {X Y T : AddSemigrp} (f : X ⟶ Y) (g : Y ⟶ T),
  AddSemigrp.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (AddSemigrp.Hom.hom g).comp (AddSemigrp.Hom.hom f)
-- Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
CategoryTheory.MorphismProperty.instIsStableUnderTransfiniteCompositionOfShapeFunctorFunctorCategoryOfHasIterationOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} (K : Type u')
  [inst_1 : LinearOrder K] [inst_2 : SuccOrder K] [inst_3 : OrderBot K] [inst_4 : WellFoundedLT K]
  [W.IsStableUnderTransfiniteCompositionOfShape K] (J : Type u'') [inst_6 : CategoryTheory.Category.{v'', u''} J]
  [CategoryTheory.Limits.HasIterationOfShape K C], (W.functorCategory J).IsStableUnderTransfiniteCompositionOfShape K
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.IsDiag.submatrix : ∀ {α : Type u_1} {n : Type u_4} {m : Type u_5} [inst : Zero α] {A : Matrix n n α},
  A.IsDiag → ∀ {f : m → n}, Function.Injective f → (A.submatrix f f).IsDiag
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.subsingleton_primeSpectrum : ∀ (R : Type u_1) [inst : CommSemiring R] [Ring.KrullDimLE 0 R] [IsLocalRing R], Subsingleton (PrimeSpectrum R)
-- Mathlib.CategoryTheory.Monoidal.Bimod
id_tensor_π_preserves_coequalizer_inv_colimMap_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  {X Y Z X' Y' Z' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ⟶ X')
  (q : CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y ⟶ Y')
  (wf :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) q =
      CategoryTheory.CategoryStruct.comp p f')
  (wg :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) q =
      CategoryTheory.CategoryStruct.comp p g')
  (h : Y' ⟶ Z') (wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.coequalizer.π f g))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorLeft Z) f g).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.colimMap
            (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) f' g' p q wf wg))
          (CategoryTheory.Limits.coequalizer.desc h wh))) =
    CategoryTheory.CategoryStruct.comp q h
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_pos : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [ProbabilityTheory.IsFiniteKernel κ]
  [ProbabilityTheory.IsFiniteKernel η] {a : α}, (κ a).AbsolutelyContinuous (η a) → ∀ᵐ (x : γ) ∂κ a, 0 < κ.rnDeriv η a x
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The pdf of a Gaussian distribution on ℝ with mean `μ` and variance `v`.  -/
ProbabilityTheory.gaussianPDF : ℝ → NNReal → ℝ → ENNReal
-- Mathlib.GroupTheory.IsPerfect
Subgroup.commutator_eq_self : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [hH : Group.IsPerfect ↥H], ⁅H, H⁆ = H
-- Init.Data.SInt.Basic
instAddInt64 : Add Int64
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.zeroHomClass : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N], ZeroHomClass (QuadraticMap R M N) M N
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_one`. -/
EMetric.diam_one : ∀ {X : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : One X], Metric.ediam 1 = 0
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If 0 belongs to the interior of the interval `integrableExpSet X μ`,
then `|X| ^ n` is integrable for all nonnegative `p : ℝ`.  -/
ProbabilityTheory.integrable_rpow_abs_of_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  0 ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ {p : ℝ}, 0 ≤ p → MeasureTheory.Integrable (fun ω => |X ω| ^ p) μ
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.not_noRepetition_append_singleton_of_suffix : ∀ {α : Type u} {a : α} {l : List α}, [a] <:+ l → ¬NoRepetition✝ a (l ++ [a])
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.balanceL!_pair_congr : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {k' : α} {v' : β k'},
  ⟨k, v⟩ = ⟨k', v'⟩ →
    ∀ {l l' r r' : Std.DTreeMap.Internal.Impl α β},
      l = l' → r = r' → Std.DTreeMap.Internal.Impl.balanceL! k v l r = Std.DTreeMap.Internal.Impl.balanceL! k' v' l' r'
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  {Y Z : C} (f : Y ⟶ Z),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).mop =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.mop { unmop := X }
-- Std.Internal.UV.Signal
/-- This function has different behavior depending on the state of the `Signal`:
- If it is initial or finished this is a no-op.
- If it's running then it drops the accept promise and if it's not repeatable it sets
  the signal handler to the initial state.
 -/
Std.Internal.UV.Signal.cancel : Std.Internal.UV.Signal → IO Unit
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatClamp n).toUInt32 = UInt32.ofNatLT n ⋯
-- Mathlib.LinearAlgebra.Dual.Defs
/-- The isomorphism `Module.evalEquiv` induces an order isomorphism on subspaces.  -/
Module.mapEvalEquiv : (R : Type u_3) →
  (M : Type u_4) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [Module.IsReflexive R M] → Submodule R M ≃o Submodule R (Module.Dual R (Module.Dual R M))