mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Std
Preorder.OfStdArgs.mk.injEq : ∀ {α : Type u_1} (le : autoParam (LE α) Preorder.OfStdArgs.le._autoParam)
  (lt :
    autoParam
      (let this := le;
      LT α)
      Preorder.OfStdArgs.lt._autoParam)
  (lawfulOrderLT :
    autoParam
      (let this := le;
      let this_1 := lt;
      Std.LawfulOrderLT α)
      Preorder.OfStdArgs.lawfulOrderLT._autoParam)
  (isPreorder :
    autoParam
      (let this := le;
      Std.IsPreorder α)
      Preorder.OfStdArgs.isPreorder._autoParam)
  (le_1 : autoParam (LE α) Preorder.OfStdArgs.le._autoParam)
  (lt_1 :
    autoParam
      (let this := le_1;
      LT α)
      Preorder.OfStdArgs.lt._autoParam)
  (lawfulOrderLT_1 :
    autoParam
      (let this := le_1;
      let this_1 := lt_1;
      Std.LawfulOrderLT α)
      Preorder.OfStdArgs.lawfulOrderLT._autoParam)
  (isPreorder_1 :
    autoParam
      (let this := le_1;
      Std.IsPreorder α)
      Preorder.OfStdArgs.isPreorder._autoParam),
  ({ le := le, lt := lt, lawfulOrderLT := lawfulOrderLT, isPreorder := isPreorder } =
      { le := le_1, lt := lt_1, lawfulOrderLT := lawfulOrderLT_1, isPreorder := isPreorder_1 }) =
    (le = le_1 ∧ lt = lt_1)
-- Mathlib.LinearAlgebra.Quotient.Bilinear
/-- Special case of `LinearMap.liftQ₂` with left and right spaces the same. Reducible so
that simp lemmas about `LinearMap.liftQ₂` apply to it.  -/
LinearMap.IsRefl.liftQ₂ : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      {P : Type u_4} →
        [inst : AddCommGroup M] →
          [inst_1 : CommRing R] →
            [inst_2 : CommRing S] →
              [inst_3 : Module R M] →
                [inst_4 : AddCommGroup P] →
                  [inst_5 : Module S P] →
                    {I₁ I₂ : R →+* S} →
                      (f : M →ₛₗ[I₁] M →ₛₗ[I₂] P) →
                        (N : Submodule R M) → f.IsRefl → N ≤ f.ker → M ⧸ N →ₛₗ[I₁] M ⧸ N →ₛₗ[I₂] P
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.darts_dropLast : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.dropLast.darts = p.darts.dropLast
-- Mathlib.Data.Setoid.Basic
/-- Given a surjective function f whose kernel is contained in an equivalence relation r, the
equivalence relation on f's codomain defined by x ≈ y ↔ the elements of f⁻¹(x) are related to
the elements of f⁻¹(y) by r.  -/
Setoid.mapOfSurjective : {α : Type u_1} → {β : Type u_2} → (r : Setoid α) → (f : α → β) → Setoid.ker f ≤ r → Function.Surjective f → Setoid β
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- In explicit mode, decides whether or not the applied function needs `@`,
where `numArgs` is the number of arguments actually supplied to `f`.
 -/
Lean.PrettyPrinter.Delaborator.needsExplicit : Lean.Expr → ℕ → Array Lean.PrettyPrinter.Delaborator.ParamKind → Bool
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.ReducedWord.empty_head : ∀ (G : Type u_1) [inst : Group G] (A B : Subgroup G), (HNNExtension.NormalWord.ReducedWord.empty G A B).head = 1
-- Mathlib.Order.Minimal
OrderEmbedding.inter_preimage_setOfPred_maximal_eq_of_subset : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α ↪o β} {t : Set β},
  t ⊆ ⇑f '' s → (x ∈ s ∩ ⇑f ⁻¹' {y | Maximal (fun x => x ∈ t) y} ↔ Maximal (fun x => x ∈ s ∩ ⇑f ⁻¹' t) x)
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- See also `yonedaEquiv_naturality'` for a more general version.  -/
CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : C} {F : CategoryTheory.Sheaf J (Type v)} (f : J.yoneda.obj X ⟶ F) (g : Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (F.obj.map g.op)) (J.yonedaEquiv f) =
    J.yonedaEquiv (CategoryTheory.CategoryStruct.comp (J.yoneda.map g) f)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.mem_mk : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ι → ι → ℝ)
  (h : ∀ (J : BoxIntegral.Box ι), f J ∈ BoxIntegral.Box.Icc I),
  J ∈ { toPrepartition := π, tag := f, tag_mem_Icc := h } ↔ J ∈ π
-- Mathlib.Control.Monad.Cont
ContT.run_mk : ∀ {r : Type u} {m : Type u → Type v} {α : Type w} (f : (α → m r) → m r) (k : α → m r), (ContT.mk f).run k = f k
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.sqrt : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  AEMeasurable f μ → AEMeasurable (fun x => √(f x)) μ
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.self_lt_rpow_of_one_lt : ∀ {x y : ℝ}, 1 < x → 1 < y → x < x ^ y
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Two different points are equidistant from a third point if and only if that third point
equals some multiple of a `π / 2` rotation of the vector between those points, plus the midpoint
of those points.  -/
EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p : P},
  p₁ ≠ p₂ →
    (dist p₁ p = dist p₂ p ↔ ∃ r, r • (EuclideanGeometry.o.rotation ↑(Real.pi / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p)
-- Mathlib.Data.Finset.Sups
Finset.singleton_diffs_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {a b : α}, {a}.diffs {b} = {a \ b}
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instIsAtomicOfIsArtinian : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] [IsArtinian R M], IsAtomic (LieSubmodule R L M)
-- Lean.Elab.Do.Control
_private.Lean.Elab.Do.Control.0.Lean.Elab.Do.ControlStack.stateT.mutVarNames : Array Lean.Elab.Do.MutVar → Array Lean.Name
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.getThenInsertIfNew?.match_1.splitter : {α : Type u_3} →
  {β : α → Type u_1} →
    (k : α) →
      (motive : Option (β k) → Sort u_2) →
        (x : Option (β k)) → (Unit → motive none) → ((b : β k) → motive (some b)) → motive x
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- We say that `π ≤ π'` if each box of `π` is a subbox of some box of `π'`.  -/
BoxIntegral.Prepartition.instLE : {ι : Type u_1} → {I : BoxIntegral.Box ι} → LE (BoxIntegral.Prepartition I)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ici_subset_Icc_union_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ici a ⊆ Set.Icc a b ∪ Set.Ioi b
-- Init.Data.String.Decode
ByteArray.isUTF8FirstByte_getElem_zero_utf8EncodeChar_append : ∀ {c : Char} {b : ByteArray}, ((String.utf8EncodeChar c).toByteArray ++ b)[0].IsUTF8FirstByte
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
RingSubgroupsBasis.mem_addGroupFilterBasis : ∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] [inst_1 : Nonempty ι] {B : ι → AddSubgroup A}
  (hB : RingSubgroupsBasis B) (i : ι), ↑(B i) ∈ hB.toRingFilterBasis.toAddGroupFilterBasis
-- Lean.Declaration
Lean.ConstantVal.mk.sizeOf_spec : ∀ (name : Lean.Name) (levelParams : List Lean.Name) (type : Lean.Expr),
  sizeOf { name := name, levelParams := levelParams, type := type } = 1 + sizeOf name + sizeOf levelParams + sizeOf type
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.normedCommGroup.eq_1 : ∀ {E : Type u_2} [inst : NormedCommGroup E],
  ULift.normedCommGroup =
    NormedCommGroup.induced (ULift.{u_5, u_2} E) E { toFun := ULift.down, map_one' := ⋯, map_mul' := ⋯ } ⋯
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.isCoprime_map : ∀ {R : Type u} {k : Type y} [inst : Field R] {p q : Polynomial R} [inst_1 : Field k] (f : R →+* k),
  IsCoprime (Polynomial.map f p) (Polynomial.map f q) ↔ IsCoprime p q
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.instMonoFaceι : ∀ {n : ℕ} (i : Fin (n + 1)), CategoryTheory.Mono (SSet.boundary.faceι i)
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.exists_embedding_to_hilbert_cube : ∀ {X : Type u_3} [inst : MetricSpace X] [TopologicalSpace.SeparableSpace X], ∃ F, Topology.IsEmbedding F
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.apply_eq_iff_eq_symm_apply : ∀ {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 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂) {p₁ : P₁} {p₂ : P₂}, e p₁ = p₂ ↔ p₁ = e.symm p₂
-- Mathlib.Order.Filter.Map
Filter.map_pure : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), Filter.map f (pure a) = pure (f a)
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.opEquiv.match_17.eq_3 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : CategoryTheory.WithInitial Cᵒᵖ) → (x ⟶ y) → Sort u_3)
  (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star)
  (h_1 :
    (x y : C) →
      (f : CategoryTheory.WithInitial.of (Opposite.op x) ⟶ CategoryTheory.WithInitial.of (Opposite.op y)) →
        motive (CategoryTheory.WithInitial.of (Opposite.op x)) (CategoryTheory.WithInitial.of (Opposite.op y)) f)
  (h_2 :
    (unop : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of (Opposite.op unop)) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of (Opposite.op unop)) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x with
    | CategoryTheory.WithInitial.of (Opposite.op x), CategoryTheory.WithInitial.of (Opposite.op y), f => h_1 x y f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of (Opposite.op unop), x => h_2 unop x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_3 x
-- Mathlib.Analysis.Distribution.FourierMultiplier
/-- Fourier multiplier on Schwartz functions.  -/
SchwartzMap.fourierMultiplierCLM : {𝕜 : Type u_2} →
  {E : Type u_3} →
    (F : Type u_4) →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : InnerProductSpace ℝ E] →
              [inst_4 : NormedSpace ℂ F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℂ 𝕜 F] →
                    [FiniteDimensional ℝ E] →
                      [inst_8 : MeasurableSpace E] → [BorelSpace E] → (E → 𝕜) → SchwartzMap E F →L[𝕜] SchwartzMap E F
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_ofNat_zero : ∀ {R : Type u_1} [inst : Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (a : ℕ) [inst_2 : a.AtLeastTwo],
  (OfNat.ofNat a).coeff 0 = OfNat.ofNat a
-- Mathlib.Order.CompleteLattice.Basic
biSup_gt_eq_iSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} [inst_1 : LT ι] [NoMinOrder ι] {f : ι → α},
  ⨆ i, ⨆ j, ⨆ (_ : j > i), f j = ⨆ i, f i
-- Init.Data.SInt.Lemmas
Int8.toInt_bmod_18446744073709551616 : ∀ (x : Int8), x.toInt.bmod 18446744073709551616 = x.toInt
-- Mathlib.Algebra.Group.Defs
/-- Typeclass for expressing that `1⁻¹ = 1`.  -/
InvOneClass : Type u_2 → Type u_2
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  Submodule.span R ↑(Submodule.span R s) = Submodule.span R s
-- Init.Control.Lawful.Instances
OptionT.ext_iff : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {x y : OptionT m α}, x = y ↔ x.run = y.run
-- Mathlib.LinearAlgebra.Projectivization.Independence
/-- A family of points in a projective space is dependent if and only if their
representatives are linearly dependent.  -/
Projectivization.dependent_iff : ∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {f : ι → Projectivization K V}, Projectivization.Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_le_one : ∀ {α : Type u} [inst : One α] [inst_1 : LE α] {a : α}, ↑a ≤ 1 ↔ a ≤ 1
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- Auxiliary lemma for `exists_continuous_real_forall_closedEBall_subset`
and its smooth counterpart.  -/
Metric.exists_forall_closedEBall_subset_aux₂ : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X} (y : X),
  Convex ℝ (Set.Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ i, ⋂ (_ : y ∈ K i), {r | Metric.closedEBall y r ⊆ U i})
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.toCocycles_comp_isoCocycles₁_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.toCocycles A 0 1) (groupCohomology.isoCocycles₁ A).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₀ A).hom
      (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.f'
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.parseTransitionTimes : Std.Internal.Parsec.ByteArray.Parser ℤ → UInt32 → Std.Internal.Parsec.ByteArray.Parser (Array ℤ)
-- Mathlib.Order.Interval.Finset.Defs
LocallyFiniteOrder.toLocallyFiniteOrderBot : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → [OrderBot α] → LocallyFiniteOrderBot α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.id_whiskerRight : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''},
  CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (CategoryTheory.CategoryStruct.id ψ) φ =
    CategoryTheory.CategoryStruct.id (ψ.comp φ)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insert k v},
  (m.insert k v).getKey a h₁ = if h₂ : (k == a) = true then k else m.getKey a ⋯
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOf.ext : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  {i : M →ₗ[R] N} {f : M →ₗ[R] Q} {a b : Module.Baer.ExtensionOf i f},
  a.domain = b.domain →
    (∀ ⦃x : N⦄ ⦃ha : x ∈ a.domain⦄ ⦃hb : x ∈ b.domain⦄, ↑a.toLinearPMap ⟨x, ha⟩ = ↑b.toLinearPMap ⟨x, hb⟩) → a = b
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_nat' : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddMonoidWithOne G]
  [inst_2 : AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ), f ↑n = f 0 + n • b
-- Lean.Elab.PreDefinition.EqnsUtils
Lean.Elab.Eqns.tryContradiction : Lean.MVarId → Lean.MetaM Bool
-- Batteries.Data.BinomialHeap.Basic
/-- Tail-recursive version of `HeapNode.rank`.  -/
Batteries.BinomialHeap.Imp.HeapNode.rankTR : {α : Type u_1} → Batteries.BinomialHeap.Imp.HeapNode α → ℕ
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_fiberwise_eq_prod_filter : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq κ] (s : Finset ι)
  (t : Finset κ) (g : ι → κ) (f : ι → M), ∏ j ∈ t, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s with g i ∈ t, f i
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.map_adj_iff : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') {v w : V},
  G'.Adj (f v) (f w) ↔ G.Adj v w
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
sub_mul_sub_nonpos_iff : ∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] {a b : R} [MulPosStrictMono R] [PosMulStrictMono R]
  [AddLeftMono R] (x : R), a ≤ b → ((x - a) * (x - b) ≤ 0 ↔ a ≤ x ∧ x ≤ b)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.replaceTopology_eq : ∀ {γ : Type u_3} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ)
  (H : U = PseudoMetricSpace.toUniformSpace.toTopologicalSpace), m.replaceTopology H = m
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.instInhabitedNormCastExtension : Inhabited Lean.Meta.NormCast.NormCastExtension
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNorm_indicator_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {s : Set α} (f : α → ε),
  MeasureTheory.eLpNorm (s.indicator f) p μ ≤ MeasureTheory.eLpNorm f p μ
-- Lean.Data.PrefixTree
_private.Lean.Data.PrefixTree.0.Lean.PrefixTreeNode.find?.loop : {α : Type u_1} → {β : Type u_2} → (cmp : α → α → Ordering) → Lean.PrefixTreeNode α β cmp → List α → Option β
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital ring homomorphism from a `NonUnitalRing` to a `NonUnitalSeminormedRing`
induces a `NonUnitalSeminormedRing` structure on the domain.

See note [reducible non-instances]  -/
NonUnitalSeminormedRing.induced : {F : Type u_5} →
  (R : Type u_6) →
    (S : Type u_7) →
      [inst : FunLike F R S] →
        [inst_1 : NonUnitalRing R] →
          [inst_2 : NonUnitalSeminormedRing S] → [NonUnitalRingHomClass F R S] → F → NonUnitalSeminormedRing R
-- Mathlib.Order.Atoms
IsAtom.Iic : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderBot α] {a x : α}, IsAtom a → ∀ (hax : a ≤ x), IsAtom ⟨a, hax⟩
-- Mathlib.RepresentationTheory.Coinvariants
Rep.finsuppToCoinvariantsTensorFree.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (α : Type u) [inst_2 : DecidableEq α],
  A.finsuppToCoinvariantsTensorFree α =
    Representation.Coinvariants.map ((A.ρ.tprod (Representation.leftRegular k G)).finsupp α)
        (A.ρ.tprod (Rep.free k G α).ρ) ↑(A.ρ.finsuppTensorRight (Representation.leftRegular k G) α).symm ∘ₗ
      ↑(((A.ρ.tprod (Representation.leftRegular k G)).coinvariantsFinsuppLEquiv α).trans
            (Finsupp.lcongr (Equiv.refl α) A.ρ.coinvariantsTprodLeftRegularLEquiv)).symm
-- Std.Time.Zoned.ZoneRules
/-- The specific time of the transition event.
 -/
Std.Time.TimeZone.Transition.time : Std.Time.TimeZone.Transition → Std.Time.Second.Offset
-- Mathlib.Data.Setoid.Partition
IndexedPartition.disjoint : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s), Pairwise (Function.onFun Disjoint s)
-- Mathlib.Algebra.GroupWithZero.Defs
/-- A type `G₀` is a “group with zero” if it is a monoid with zero element (distinct from `1`)
such that every nonzero element is invertible.
The type is required to come with an “inverse” function, and the inverse of `0` must be `0`.

Examples include division rings and the ordered monoids that are the
target of valuations in general valuation theory.  -/
GroupWithZero : Type u → Type u
-- Lean.Environment
/-- Allows `realizeConst` calls for the given declaration in all derived environment branches.
Realizations will run using the given environment and options to ensure deterministic results. Note
that while we check that the function isn't called before the declaration is actually added to the
environment, we cannot automatically check that it isn't otherwise called too early in the sense
that helper declarations and environment extension state that may be relevant to realizations may
not have been added yet. We do check that we are not calling it from a different branch than `c` was
added on, which would be definitely too late. Thus, this function should generally be called in
elaborators calling `addDecl` (when that declaration is a plausible target for realization) at the
latest possible point, i.e. at the very end of the elaborator or just before a first realization may
be triggered if any.
 -/
Lean.Environment.enableRealizationsForConst : Lean.Environment → Lean.Options → Lean.Name → BaseIO Lean.Environment
-- Mathlib.Algebra.Group.ForwardDiff
Polynomial.fwdDiff_iter_degree_eq_factorial : ∀ {R : Type u_3} [inst : CommRing R] (P : Polynomial R),
  ((fwdDiff 1)^[P.natDegree] fun x => Polynomial.eval x P) = P.leadingCoeff • ↑P.natDegree.factorial
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.of_eq : ∀ {α : Type u} {β : Type v} {l : Filter α} {f g : α → β}, f = g → f =ᶠ[l] g
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertManyIfNewUnit_list_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, m.insertManyIfNewUnit [k] = m.insertIfNew k ()
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_mk : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : Submodule R P) (hI : IsFractional S I), ↑⟨I, hI⟩ = I
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.add_comp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β}, μ.bind ⇑(κ + η) = μ.bind ⇑κ + μ.bind ⇑η
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.nest.eq_1 : ∀ (p : DyckWord),
  p.nest = { toList := [DyckStep.U] ++ ↑p ++ [DyckStep.D], count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.sub.injEq : ∀ (a b a_1 b_1 : Lean.Grind.Linarith.Expr), (a.sub b = a_1.sub b_1) = (a = a_1 ∧ b = b_1)
-- Lean.Server.Completion.CompletionCollectors
Lean.Server.Completion.errorNameCompletion : Lean.Lsp.DocumentUri →
  Lean.Lsp.Position →
    ℕ → Lean.Elab.ContextInfo → Lean.Syntax → Lean.Lsp.ClientCapabilities → IO (Array Lean.Lsp.ResolvableCompletionItem)
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.PseudoMetrizableSpace.subtype : ∀ {X : Type u_2} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] (s : Set X),
  TopologicalSpace.PseudoMetrizableSpace ↑s
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasInitial C],
  CategoryTheory.Limits.HasZeroObject.zeroIsoInitial.inv = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- The cosine of `π / 3` is `1 / 2`.  -/
Real.cos_pi_div_three : Real.cos (Real.pi / 3) = 1 / 2
-- Std.Sat.AIG.LawfulOperator
/-- The prefix may never be longer than the other array.
 -/
Std.Sat.AIG.IsPrefix.size_le : ∀ {α : Type} {decls1 decls2 : Array (Std.Sat.AIG.Decl α)},
  Std.Sat.AIG.IsPrefix decls1 decls2 → decls1.size ≤ decls2.size
-- Aesop.RuleTac.Tactic
Aesop.RuleTac.singleRuleTacImpl : Lean.Name → Aesop.RuleTac
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.isTrans_map`.

---

**Alias** of `IsTrans.map`. -/
Relation.map_transitive : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [IsTrans α r] {f : α → β},
  (∀ (x y : α), f x = f y → r x y) → IsTrans β (Relation.Map r f f)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.im_one : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R] [inst_1 : One R], QuaternionAlgebra.im 1 = 0