mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_image : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {M' : Type u_4} [inst_7 : AddCommMonoid M'] [inst_8 : Module R M'] (s : Set M')
  (q : M' →ₗ[R] M), PointedCone.dual p (⇑q '' s) = PointedCone.dual (p ∘ₗ q) s
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iio_subset_Iio : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α], a ≤ b → Finset.Iio a ⊆ Finset.Iio b
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.nullMeasurableSet_eq : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasurableSingletonClass (MeasureTheory.NullMeasurableSpace α μ)] {a : α},
  MeasureTheory.NullMeasurableSet {x | x = a} μ
-- Mathlib.Topology.Category.TopCat.Yoneda
/-- A universe polymorphic Yoneda presheaf on `TopCat` given by continuous maps into a topological
space `Y`.
 -/
ContinuousMap.yonedaPresheaf' : (Y : Type w') → [TopologicalSpace Y] → CategoryTheory.Functor TopCatᵒᵖ (Type (max w w'))
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.mul_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : Preorder α] [inst_2 : CommMonoid β]
  [inst_3 : Preorder β] [inst_4 : IsOrderedMonoid β] (f g : α →*o β) (a : α), (f * g) a = f a * g a
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.instPreservesZeroMorphismsRepModuleCatFunctor : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] (n : ℕ), (groupHomology.functor k G n).PreservesZeroMorphisms
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.isCover_minimalCover : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal},
  Metric.coveringNumber ε A ≠ ⊤ → Metric.IsCover ε A (Metric.minimalCover ε A)
-- Init.Data.List.Basic
List.headD_cons : ∀ {α : Type u} {a : α} {l : List α} {d : α}, (a :: l).headD d = a
-- Mathlib.FieldTheory.PerfectClosure
/-- Prior to https://github.com/leanprover-community/mathlib4/pull/15862, this lemma was called `mk_zero_zero`.
See `mk_zero_right` for the lemma used to be called `mk_zero`.  -/
PerfectClosure.mk_zero : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p],
  PerfectClosure.mk K p 0 = 0
-- Init.Prelude
EStateM.instMonad : {ε σ : Type u} → Monad (EStateM ε σ)
-- Mathlib.Topology.Bornology.Basic
Bornology.nonempty_of_not_isBounded : ∀ {α : Type u_2} {x : Bornology α} {s : Set α}, ¬Bornology.IsBounded s → s.Nonempty
-- Mathlib.Algebra.Ring.Invertible
AddUnits.val_neg_mulRight : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R), ↑(-x.mulRight y) = x.neg * y
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasurableEmbedding.integral_map : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {β : Type u_6} {x : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f → ∀ (g : β → G), ∫ (y : β), g y ∂MeasureTheory.Measure.map f μ = ∫ (x : α), g (f x) ∂μ
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.lineDerivOpCLM_eq_lineDerivCLM : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F] {v : E},
  LineDeriv.lineDerivOpCLM 𝕜 (TestFunction Ω F ⊤) v = TestFunction.lineDerivCLM 𝕜 v
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.div_rpow : ∀ {x y : ℝ}, 0 ≤ x → 0 ≤ y → ∀ (z : ℝ), (x / y) ^ z = x ^ z / y ^ z
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- The equivalence between natural transformations from the yoneda embedding (to the sheaf category)
and elements of `F.val.obj X`.
 -/
CategoryTheory.GrothendieckTopology.yonedaEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : J.Subcanonical] →
        {X : C} → {F : CategoryTheory.Sheaf J (Type v)} → (J.yoneda.obj X ⟶ F) ≃ F.obj.obj (Opposite.op X)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.algHom_ext : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {A : Type u_2} [inst_5 : Semiring A] [inst_6 : Algebra R' A]
  ⦃f g : TrivSqZeroExt R' M →ₐ[R'] A⦄, (∀ (m : M), f (TrivSqZeroExt.inr m) = g (TrivSqZeroExt.inr m)) → f = g
-- Init.Data.Vector.Perm
Vector.Perm.of_eq : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n}, xs = ys → xs.Perm ys
-- Mathlib.Topology.UniformSpace.Equiv
/-- Uniform continuity of the function  -/
UniformEquiv.uniformContinuous_toFun : ∀ {α : Type u_4} {β : Type u_5} [inst : UniformSpace α] [inst_1 : UniformSpace β] (self : α ≃ᵤ β),
  UniformContinuous self.toFun
-- Mathlib.Order.SymmDiff
symmDiff_symmDiff_self' : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b : α), symmDiff (symmDiff a b) a = b
-- Mathlib.Logic.Embedding.Basic
Equiv.embeddingCongr_symm : ∀ {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂),
  (e₁.embeddingCongr e₂).symm = e₁.symm.embeddingCongr e₂.symm
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- If a point has the same distance from all vertices of a simplex,
the orthogonal projection of that point onto the subspace spanned by
that simplex is its circumcenter.  -/
Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p : P} {r : ℝ},
  (∀ (i : Fin (n + 1)), dist (s.points i) p = r) → ↑(s.orthogonalProjectionSpan p) = s.circumcenter
-- Init.Grind.Offset
Lean.Grind.Nat.of_le_eq_false : ∀ (u v : ℕ), (u ≤ v) = False → v + 1 ≤ u
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.integrable_iff_integrableAtFilter_atTop : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε]
  [inst_5 : LinearOrder X] [OrderBot X] [CompactIccSpace X],
  MeasureTheory.Integrable f μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atTop μ ∧ MeasureTheory.LocallyIntegrable f μ
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_mul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v), (x * y).toCompletion = x.toCompletion * y.toCompletion
-- Mathlib.Order.Heyting.Hom
CoheytingHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β]
  [inst_2 : CoheytingAlgebra γ] {f : CoheytingHom α β} {g₁ g₂ : CoheytingHom β γ},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} {x y : D₁.Hom D₂},
  x.hom = y.hom → x = y
-- Mathlib.Algebra.Ring.ULift
ULift.instNatCast : {R : Type u} → [NatCast R] → NatCast (ULift.{u_1, u} R)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.instIsBalanced : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [P.IsAnisotropic], P.IsBalanced
-- Mathlib.Order.Defs.Unbundled
LowerSet.mk.injEq : ∀ {α : Type u_1} [inst : LE α] (carrier : Set α) (lower' : IsLowerSet carrier) (carrier_1 : Set α)
  (lower'_1 : IsLowerSet carrier_1),
  ({ carrier := carrier, lower' := lower' } = { carrier := carrier_1, lower' := lower'_1 }) = (carrier = carrier_1)
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_eq_iff_eq_mul_right : ∀ {a b c : ℤ}, b ≠ 0 → b ∣ a → (a.tdiv b = c ↔ a = b * c)
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquivClass.toRingEquivClass : ∀ {F : Type u_1} {A : outParam (Type u_2)} {B : outParam (Type u_3)} {inst : Add A} {inst_1 : Mul A} {inst_2 : Star A}
  {inst_3 : Add B} {inst_4 : Mul B} {inst_5 : Star B} {inst_6 : EquivLike F A B} [self : StarRingEquivClass F A B],
  RingEquivClass F A B
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Presheaf.χ_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor Cᵒᵖ (Type (max u v))} (m : F ⟶ G)
  (X : Cᵒᵖ),
  (CategoryTheory.Presheaf.χ m).app X =
    TypeCat.ofHom fun x =>
      {
        arrows := fun Y f =>
          ∃ a,
            (CategoryTheory.ConcreteCategory.hom (G.map f.op)) x =
              (CategoryTheory.ConcreteCategory.hom (m.app (Opposite.op Y))) a,
        downward_closed := ⋯ }
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.map_smul_of_tower : ∀ {S : Type u_1} {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] (Q : QuadraticMap R M N)
  [inst_5 : CommSemiring S] [inst_6 : Algebra S R] [inst_7 : SMul S M] [IsScalarTower S R M] [inst_9 : Module S N]
  [IsScalarTower S R N] (a : S) (x : M), Q (a • x) = (a * a) • Q x
-- Mathlib.Probability.Distributions.Exponential
/-- The Lebesgue integral of the exponential pdf over nonpositive reals equals 0  -/
ProbabilityTheory.lintegral_exponentialPDF_of_nonpos : ∀ {x r : ℝ}, x ≤ 0 → ∫⁻ (y : ℝ) in Set.Iio x, ProbabilityTheory.exponentialPDF r y = 0
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.glueData_U : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) (a : ι),
  (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).U a = X a
-- Lean.Elab.Tactic.Doc
Lean.Elab.Tactic.Doc.TacticDoc.mk.injEq : ∀ (internalName : Lean.Name) (userName : String) (tags : Lean.NameSet) (docString : Option String)
  (extensionDocs : Array String) (internalName_1 : Lean.Name) (userName_1 : String) (tags_1 : Lean.NameSet)
  (docString_1 : Option String) (extensionDocs_1 : Array String),
  ({ internalName := internalName, userName := userName, tags := tags, docString := docString,
        extensionDocs := extensionDocs } =
      { internalName := internalName_1, userName := userName_1, tags := tags_1, docString := docString_1,
        extensionDocs := extensionDocs_1 }) =
    (internalName = internalName_1 ∧
      userName = userName_1 ∧ tags = tags_1 ∧ docString = docString_1 ∧ extensionDocs = extensionDocs_1)
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.homologyMap_map_of_eq_neg_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K K' : ChainComplex C ℕ} {L L' : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L)
  (h' : CochainComplex.ConnectData K' L') (fK : K ⟶ K') (fL : L ⟶ L')
  (f_comm : CategoryTheory.CategoryStruct.comp (fK.f 0) h'.d₀ = CategoryTheory.CategoryStruct.comp h.d₀ (fL.f 0))
  (n : ℕ) [inst_2 : NeZero n] (m : ℤ) (hmn : m = -↑(n + 1)) [inst_3 : HomologicalComplex.HasHomology h.cochainComplex m]
  [inst_4 : HomologicalComplex.HasHomology K n] [inst_5 : HomologicalComplex.HasHomology h'.cochainComplex m]
  [inst_6 : HomologicalComplex.HasHomology K' n],
  HomologicalComplex.homologyMap (h.map h' fK fL f_comm) m =
    CategoryTheory.CategoryStruct.comp (h.homologyIsoNeg n m hmn).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap fK n) (h'.homologyIsoNeg n m hmn).inv)
-- Mathlib.GroupTheory.OrderOfElement
pow_inj_iff_of_orderOf_eq_zero : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] {x : G}, orderOf x = 0 → ∀ {n m : ℕ}, x ^ n = x ^ m ↔ n = m
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.ofFunctor.injEq : ∀ {C D : CategoryTheory.Cat} (toFunctor toFunctor_1 : CategoryTheory.Functor ↑C ↑D),
  ({ toFunctor := toFunctor } = { toFunctor := toFunctor_1 }) = (toFunctor = toFunctor_1)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- Clopen subsets in the prime spectrum of a commutative semiring are in order-preserving
bijection with pairs of elements with product 0 and sum 1. (By definition, `(e₁, f₁) ≤ (e₂, f₂)`
iff `e₁ * e₂ = e₁`.) Both elements in such pairs must be idempotents, but there may exists
idempotents that do not form such pairs (does not have a "complement"). For example, in the
semiring `{0, 0.5, 1}` with `⊔` as `+` and `⊓` as `*`, `0.5` has no complement.  -/
PrimeSpectrum.mulZeroAddOneEquivClopens : {R : Type u} →
  [inst : CommSemiring R] → { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 } ≃o TopologicalSpace.Clopens (PrimeSpectrum R)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- A nondegenerate bilinear form is a bilinear form that is both left-separating and
right-separating, i.e. if `B x y = 0` for all `y` then `x = 0`, and if `B x y = 0` for all `x` then
`y = 0`.

Note that these conditions are independent of each other in general, but in the common case of
finite-dimensional vector spaces (or, more generally, finite free modules over an integral
domain), either of these conditions implies the other; see
`LinearMap.BilinForm.Nondegenerate.ofSeparatingLeft` and
`LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot`, proved in a later file.
 -/
LinearMap.BilinForm.Nondegenerate : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.BilinForm R M → Prop
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddRightStrictMono.toIsRightCancelAdd : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LinearOrder α] [AddRightStrictMono α], IsRightCancelAdd α
-- Mathlib.Topology.MetricSpace.HausdorffDimension
le_dimH_of_hausdorffMeasure_ne_zero : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {s : Set X} {d : NNReal},
  (MeasureTheory.Measure.hausdorffMeasure ↑d) s ≠ 0 → ↑d ≤ dimH s
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₂ → (m₁ ∪ m₂).get? k = m₁.get? k
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
UniformFun.toFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2}, UniformFun.toFun = UniformFun.ofFun.symm
-- Mathlib.Topology.Constructions.SumProd
/-- The sum of `X` with any empty topological space is homeomorphic to `X`.  -/
Homeomorph.emptySum : (X : Type u) → (Y : Type v) → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → [IsEmpty Y] → Y ⊕ X ≃ₜ X
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.i.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct A A], P.i = CategoryTheory.Limits.coprod.desc P.i₀ P.i₁
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {fallback : β},
  Std.ExtDTreeMap.Const.getD (t₁ \ t₂) k fallback =
    if k ∈ t₂ then fallback else Std.ExtDTreeMap.Const.getD t₁ k fallback
-- Mathlib.Topology.Order
closure_indiscrete : ∀ {α : Type u_1} {t₂ : TopologicalSpace α} [IndiscreteTopology α] {s : Set α}, s.Nonempty → closure s = Set.univ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false →
    (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getKey! k = default
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.instMonoidHomClass : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N], MonoidHomClass (M →* N) M N
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instIsPretransitiveSMul : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : SMul M X] [inst_2 : ContinuousConstSMul M X]
  [MulAction.IsPretransitive M X], MulAction.IsPretransitive M (SeparationQuotient X)
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_equiv_eq_comap_symm' : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G ≃* N) (K : Subgroup G),
  Subgroup.map f.toMonoidHom K = Subgroup.comap f.symm.toMonoidHom K
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.martingale_densityProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β},
      MeasurableSet s →
        MeasureTheory.Martingale (fun n x => κ.densityProcess ν n a x s) (ProbabilityTheory.countableFiltration γ) (ν a)
-- Lean.Meta.MethodSpecs
Lean.instInhabitedMethodSpecsAttrData.default : Lean.MethodSpecsAttrData
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_ne_zero_iff_nontrivial : ∀ {α : Type u_1} {G : SimpleGraph α}, G.ediam ≠ 0 ↔ Nontrivial α
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousAt.comp_upperSemicontinuousWithinAt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
  [OrderTopology δ] {g : γ → δ} {f : α → γ},
  ContinuousAt g (f x) → UpperSemicontinuousWithinAt f s x → Monotone g → UpperSemicontinuousWithinAt (g ∘ f) s x
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
/-- `IsKernelPair f a b` expresses that `(a, b)` is a kernel pair for `f`, i.e. `a ≫ f = b ≫ f`
and the square
  R → X
  ↓   ↓
  X → Y
is a pullback square.
This is just an abbreviation for `IsPullback a b f f`.
 -/
CategoryTheory.IsKernelPair : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {R X Y : C} → (X ⟶ Y) → (R ⟶ X) → (R ⟶ X) → Prop
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.bijective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), Function.Bijective ⇑e
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.lTensorOne_one_tmul : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {N : Submodule R S}
  (n : ↥N), N.lTensorOne (1 ⊗ₜ[R] n) = n
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `lowerSemicontinuouAt_neg_iff`. -/
UpperSemicontinuousAt.neg : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β], UpperSemicontinuousAt f a → LowerSemicontinuousAt (-f) a
-- Init.Data.Nat.Basic
Nat.succ_pred_eq_of_pos : ∀ {n : ℕ}, 0 < n → n.pred.succ = n
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulZeroOneClass α] [inst_4 : MulZeroOneClass β] [inst_5 : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β)
  (a : α), (f.comp g) a = f (g a)
-- Mathlib.Analysis.Complex.ReImTopology
Complex.interior_setOfPred_le_re : ∀ (a : ℝ), interior {z | a ≤ z.re} = {z | a < z.re}
-- Mathlib.Lean.ContextInfo
/-- Embeds a `CoreM` action in `CommandElabM`, returning both the result and the InfoTrees produced.

Similar to `runCoreMWithMessages` but also captures InfoTrees for extracting "Try this:" suggestions.  -/
Lean.Elab.ContextInfo.runCoreMCapturingInfoTree : {α : Type} →
  Lean.Elab.ContextInfo → Lean.CoreM α → Lean.Elab.Command.CommandElabM (α × Lean.PersistentArray Lean.Elab.InfoTree)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.addActionSet.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : AddMonoid α] [inst_1 : AddAction α β],
  Set.addActionSet = { toVAdd := Set.vaddSet, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CStarAlgebra.nonneg_iff_exists_isSelfAdjoint_and_eq_mul_self : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [StarOrderedRing A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A]
  [T2Space A] {a : A}, 0 ≤ a ↔ ∃ b, IsSelfAdjoint b ∧ a = b * b
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.modify : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [LawfulBEq α] → (a : α) → (β a → β a) → Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectedSystem.natLERec.eq_1 : ∀ {L : FirstOrder.Language} {G' : ℕ → Type w} [inst : (i : ℕ) → L.Structure (G' i)]
  (f' : (n : ℕ) → L.Embedding (G' n) (G' (n + 1))) (m n : ℕ) (h : m ≤ n),
  FirstOrder.Language.DirectedSystem.natLERec f' m n h =
    Nat.leRecOn h (fun k g => (f' k).comp g) (FirstOrder.Language.Embedding.refl L (G' m))
-- Init.Control.Except
ExceptT.instMonadLift : {ε : Type u} → {m : Type u → Type v} → [Monad m] → MonadLift m (ExceptT ε m)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.smul : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] (c : ℝ),
  ProbabilityTheory.HasGaussianLaw X P → ProbabilityTheory.HasGaussianLaw (c • X) P
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
NonUnitalStarSubsemiring.instSetLike : {R : Type v} → [inst : NonUnitalNonAssocSemiring R] → [inst_1 : Star R] → SetLike (NonUnitalStarSubsemiring R) R
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.preimage_coe_top : ∀ {α : Type u_1}, WithTop.some ⁻¹' {⊤} = ∅
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.L2.integrable_inner : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (f g : ↥(MeasureTheory.Lp E 2 μ)),
  MeasureTheory.Integrable (fun x => inner 𝕜 (↑↑f x) (↑↑g x)) μ
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_div : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u v : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] [inst_2 : Div β],
  MeasureTheory.stoppedProcess (u / v) τ = MeasureTheory.stoppedProcess u τ / MeasureTheory.stoppedProcess v τ
-- Mathlib.Control.Traversable.Instances
Sum.traverse.eq_2 : ∀ {σ : Type u} {F : Type u → Type u} [inst : Applicative F] {α : Type u_1} {β : Type u} (f : α → F β) (x_1 : α),
  Sum.traverse f (Sum.inr x_1) = Sum.inr <$> f x_1