mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
/-- We have that `λ ^ 2 = -3 * η`.  -/
_private.Mathlib.NumberTheory.NumberField.Cyclotomic.Three.0.IsCyclotomicExtension.Rat.Three.lambda_sq : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3), (hζ.toInteger - 1) ^ 2 = -3 * ↑⋯.unit
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.linearEquivOp_apply_coe : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) (a : ↥S.toSubsemiring), ↑(S.linearEquivOp a) = MulOpposite.op ↑a
-- Mathlib.Order.SuccPred.Limit
PredOrder.colimitRecOn_isMax : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : PredOrder α]
  [inst_2 : WellFoundedGT α] (isMax : (a : α) → IsMax a → motive a)
  (pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
  (isPredLimit : (a : α) → Order.IsPredLimit a → ((b : α) → a < b → motive b) → motive a) (hb : IsMax b),
  PredOrder.colimitRecOn b isMax pred isPredLimit = isMax b hb
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.measurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν → Measurable f
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearMap.transvection.eq_1 : ∀ {R : Type u_1} {V : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V]
  (f : Module.Dual R V) (v : V),
  LinearMap.transvection f v = { toFun := fun x => x + f x • v, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instAddCommMonoid : {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] → AddCommMonoid (LieSubmodule R L M)
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- `corecF` is used as a basis for defining the corecursor of `Cofix F α`. `corecF`
uses corecursion to construct the M-type generated by `q.P` and uses function on `F`
as a corecursive step  -/
MvQPF.corecF : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} →
    [q : MvQPF F] → {α : TypeVec.{u} n} → {β : Type u} → (β → F (α ::: β)) → β → (MvQPF.P F).M α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k : α} {h' : k ∈ Std.TreeMap.map f t}, (Std.TreeMap.map f t).getKey k h' = t.getKey k ⋯
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.Fun.mk.inj : ∀ {X : Type u_1} {Y : Type u_2} {toFun toFun_1 : X → Y}, { toFun := toFun } = { toFun := toFun_1 } → toFun = toFun_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).getKey? a = if compare k a = Ordering.eq then none else t.getKey? a
-- Mathlib.Data.Rat.Cast.Order
Rat.intCast_le_cast : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {m : ℤ} {n : ℚ}, ↑m ≤ ↑n ↔ ↑m ≤ n
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_iSup : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Sort u_3}
  (f : L.Hom M N) (s : ι → L.Substructure M),
  FirstOrder.Language.Substructure.map f (⨆ i, s i) = ⨆ i, FirstOrder.Language.Substructure.map f (s i)
-- Std.Data.DHashMap.Basic
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.DHashMap.getThenInsertIfNew? : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → [LawfulBEq α] → Std.DHashMap α β → (a : α) → β a → Option (β a) × Std.DHashMap α β
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
orthonormal_iUnion_of_directed : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {η : Type u_5} {s : η → Set E},
  Directed (fun x1 x2 => x1 ⊆ x2) s → (∀ (i : η), Orthonormal 𝕜 fun x => ↑x) → Orthonormal 𝕜 fun x => ↑x
-- Init.Data.Dyadic.Basic
Int.trailingZeros_shiftLeft : ∀ {x : ℤ}, x ≠ 0 → ∀ (n : ℕ), (x <<< n).trailingZeros = x.trailingZeros + n
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Submodule.mkQ.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
  p.mkQ = { toFun := Submodule.Quotient.mk, map_add' := ⋯, map_smul' := ⋯ }
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_eq_some_getKey!_of_contains : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, m.contains a = true → m.getKey? a = some (m.getKey! a)
-- Mathlib.Topology.Connected.PathConnected
isPathConnected_univ : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PathConnectedSpace X], IsPathConnected Set.univ
-- Mathlib.Topology.Separation.Hausdorff
IsPreirreducible.subsingleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {S : Set X}, IsPreirreducible S → S.Subsingleton
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (h : F.CoreMonoidal), CategoryTheory.Functor.LaxMonoidal.ε F = h.εIso.hom
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.ιFree_mapFree_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u)
  (η : SheafOfModules.unit S ⟶ F.obj (SheafOfModules.unit R)) (i : I) {Z : SheafOfModules S}
  (h : F.obj (SheafOfModules.free I) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i)
      (CategoryTheory.CategoryStruct.comp (SheafOfModules.mapFree F I η) h) =
    CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (F.map (SheafOfModules.ιFree i)) h)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.toSnowflaking_ofSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} (x : Metric.Snowflaking X α hα₀ hα₁),
  Metric.Snowflaking.toSnowflaking (Metric.Snowflaking.ofSnowflaking x) = x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.containsThenInsert_fst : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.containsThenInsert k v).1 = m.contains k
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
/-- If `f : X ⟶ Z` is iso, then `X ×[Z] Y ≅ Y`. This is the explicit limit cone.  -/
CategoryTheory.Limits.pullbackConeOfLeftIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → [CategoryTheory.IsIso f] → CategoryTheory.Limits.PullbackCone f g
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_mul_iff_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α] [MulRightMono α] [MulRightReflectLE α] (a : α) {b c : α},
  b * a ≤ c * a ↔ b ≤ c
-- Mathlib.Analysis.Fourier.ZMod
/-- The discrete Fourier transform of `Φ` is odd if and only if `Φ` itself is.  -/
ZMod.dft_odd_iff : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ}, Function.Odd (ZMod.dft Φ) ↔ Function.Odd Φ
-- Mathlib.Data.NNRat.Defs
NNRat.num_natCast : ∀ (n : ℕ), (↑n).num = n
-- Mathlib.Order.Basic
min_def_lt' : ∀ {α : Type u_2} [inst : LinearOrder α] (a b : α), min a b = if b < a then b else a
-- Std.Internal.Do.Order.Basic
/-- Indexed supremum  -/
Lean.Order.«term⨆_,_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.homEquiv_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) {W : C}
  (f : t.pt ⟶ W), h.homEquiv f = (t.extend f).ι
-- Mathlib.Data.Setoid.Partition
/-- Makes an equivalence relation from a set of sets partitioning α.  -/
Setoid.mkClasses : {α : Type u_1} → (c : Set (Set α)) → (∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b) → Setoid α
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittZero.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.wittZero p = wittStructureInt p 0
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.apply_of_lt_skipWhile_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos pos' : s.Pos},
  pos ≤ pos' → ∀ (h₂ : pos' < pos.skipWhile P), P (pos'.get ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.HasCountableCoproducts.out : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Limits.HasCountableCoproducts C]
  (J : Type) [Countable J], CategoryTheory.Limits.HasCoproductsOfShape J C
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CategoryTheory.Functor.mapCochainComplexShiftIso_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] (n : ℤ) (X : HomologicalComplex C (ComplexShape.up ℤ)) (i : ℤ),
  ((F.mapCochainComplexShiftIso n).inv.app X).f i = CategoryTheory.CategoryStruct.id (F.obj (X.X (i + n)))
-- Lean.SubExpr
Lean.SubExpr.Pos.instOrd : Ord Lean.SubExpr.Pos
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.naive_toGenerators : ∀ {R : Type u} {ι : Type w} {σ : Type t} [inst : CommRing R] {v : ι → MvPolynomial σ R}
  (s : optParam (MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R) (Function.surjInv ⋯))
  (hs :
    autoParam
      (∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x)
      Algebra.Presentation.naive._auto_1),
  (Algebra.Presentation.naive s hs).toGenerators = Algebra.Generators.naive s hs
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.minEntry! : {α : Type u} → {β : Type v} → [Inhabited (α × β)] → (Std.DTreeMap.Internal.Impl α fun x => β) → α × β
-- Init.Data.UInt.Bitwise
USize.zero_shiftRight : ∀ {a : USize}, 0 >>> a = 0
-- Mathlib.MeasureTheory.Function.UnifTight
/-- Forward direction of Vitali's convergence theorem:
if `f` is a sequence of uniformly integrable, uniformly tight functions that converge in
measure to some function `g` in a finite measure space, then `f` converge in Lp to `g`.  -/
MeasureTheory.tendsto_Lp_of_tendstoInMeasure : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup β] {μ : MeasureTheory.Measure α}
  {p : ENNReal} {f : ℕ → α → β} {g : α → β},
  1 ≤ p →
    p ≠ ⊤ →
      (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
        MeasureTheory.MemLp g p μ →
          MeasureTheory.UnifIntegrable f p μ →
            MeasureTheory.UnifTight f p μ →
              MeasureTheory.TendstoInMeasure μ f Filter.atTop g →
                Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.pointReflection_center_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ → (Equiv.pointReflection s.center) p₁ = p₂
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousOn.inv : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Inv G]
  [ContinuousInv G] {f : X → G} {s : Set X}, ContinuousOn f s → ContinuousOn f⁻¹ s
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.mem_range : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {f : MeasureTheory.SimpleFunc α β} {b : β},
  b ∈ f.range ↔ b ∈ Set.range ⇑f
-- Mathlib.Order.WithBot
WithTop.le_untopD_iff : ∀ {α : Type u_1} {a b : α} [inst : LE α] {x : WithTop α}, (x = ⊤ → b ≤ a) → (b ≤ WithTop.untopD a x ↔ ↑b ≤ x)
-- Mathlib.Algebra.Group.End
Equiv.Perm.subtypePerm_apply : ∀ {α : Type u_4} {p : α → Prop} (f : Equiv.Perm α) (h : ∀ (x : α), p (f x) ↔ p x) (x : { x // p x }),
  (f.subtypePerm h) x = ⟨f ↑x, ⋯⟩
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Cosimplicial objects.  -/
CategoryTheory.CosimplicialObject : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max v u)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.hom_ext_iff : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} {f g : A ⟶ B},
  f = g ↔ CommAlgCat.Hom.hom f = CommAlgCat.Hom.hom g
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- An action is preprimitive iff it is `1`-preprimitive.  -/
AddAction.is_zero_preprimitive_iff : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α],
  AddAction.IsMultiplyPreprimitive M α 1 ↔ AddAction.IsPreprimitive M α
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorRightTensor_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C),
  (CategoryTheory.MonoidalCategory.tensorRightTensor X Y).inv.app Z =
    (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).hom
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α}, (k == k') = true → m.getKey? k = m.getKey? k'
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.FilterMap.PlausibleStep.done : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α}
  {f : β → Std.Iterators.PostconditionT n (Option γ)} [inst : Std.Iterator α m β] {it : Std.IterM n γ},
  it.internalState.inner.IsPlausibleStep Std.IterStep.done →
    Std.Iterators.Types.FilterMap.PlausibleStep it Std.IterStep.done
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.id : ∀ (α : Type u) [inst : Preorder α], RightOrdContinuous id
-- Mathlib.RingTheory.WittVector.IsPoly
/-- A macro for a common simplification when rewriting with ghost component equations.  -/
WittVector.Tactic.ghostSimp : Lean.ParserDescr
-- Mathlib.Tactic.Order.Graph.Basic
/-- Destination of the edge.  -/
Mathlib.Tactic.Order.Edge.dst : Mathlib.Tactic.Order.Edge → ℕ
-- Lean.Meta.InferType
/-- The expression is definitely of the form `A_1 -> ... -> A_n -> B`
where `B` is a proposition.
 -/
_private.Lean.Meta.InferType.0.Lean.Meta.ArrowPropResult.true : Lean.Meta.ArrowPropResult✝
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.length_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v'),
  (p.copy hu hv).length = p.length
-- Mathlib.Algebra.GroupWithZero.Associated
dvd_dvd_iff_associated : ∀ {M : Type u_1} [inst : MonoidWithZero M] [IsLeftCancelMulZero M] {a b : M}, a ∣ b ∧ b ∣ a ↔ Associated a b
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Two vectors with zero angle between them are equal if and only if they have equal norms.  -/
Orientation.eq_iff_norm_eq_of_oangle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = 0 → (x = y ↔ ‖x‖ = ‖y‖)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Replace the function attached to a multiseries.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.replaceFun : {basis_hd : ℝ → ℝ} →
  {basis_tl : List (ℝ → ℝ)} →
    Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl) →
      (ℝ → ℝ) → Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.instEquivLike : {X : Type u_1} →
  {Y : Type u_2} → [inst : PseudoEMetricSpace X] → [inst_1 : PseudoEMetricSpace Y] → EquivLike (X ≃ᵈ Y) X Y
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.instMembership : {α : Type u_1} → Membership α (RBTree.RBNode α)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a ⟶ Y}
  {c : C} (i : F.obj c ⟶ X) (h : c ⟶ a)
  (hi : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp (F.map h) g) [inst_2 : F.Full],
  CategoryTheory.CategoryStruct.comp (F.map (hf.lift i h hi)) (hf.fst g) = i
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.instMonoid : {A : Type u_2} → [inst : Monoid A] → [inst_1 : Star A] → Monoid (A →⋆* A)
-- Mathlib.Tactic.Attr.Register
/-- Simp set for `functor_norm`  -/
Parser.Attr.functor_norm : Lean.ParserDescr
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.skeleton_mono`. -/
Topology.CWComplex.skeleton_mono : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  {n m : ℕ∞}, m ≤ n → ↑(Topology.RelCWComplex.skeleton C m) ⊆ ↑(Topology.RelCWComplex.skeleton C n)
-- Std.Time.Format.Modifier
/-- `u`: Proleptic/astronomical year (e.g., 2004, 04, -0001, -1). Can be negative: year 0 exists and -0001 = 2 BC.
Use `y` + `G` instead when you want the era-based (always-positive) representation.
 -/
Std.Time.Modifier.u : Std.Time.Year → Std.Time.Modifier
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.WalkingParallelPairHom.id_comp : ∀ {X Y : CategoryTheory.Limits.WalkingParallelPair} (g : CategoryTheory.Limits.WalkingParallelPairHom X Y),
  (CategoryTheory.Limits.WalkingParallelPairHom.id X).comp g = g
-- Lean.Elab.Term.TermElabM
/-- Similar to `addAutoBoundImplicits`, but converts all metavariables into free variables.

It uses `mkForallFVars` + `forallBoundedTelescope` to convert metavariables into free variables.
The type `type` is modified during the process if type depends on `xs`.
We use this method to simplify the conversion of code using `autoBoundImplicitsOld` to `autoBoundImplicits`.
 -/
Lean.Elab.Term.addAutoBoundImplicits' : {α : Type} →
  Array Lean.Expr →
    Lean.Expr →
      (Array Lean.Expr → Lean.Expr → Lean.Elab.TermElabM α) →
        optParam (Option String.Pos.Raw) none → Lean.Elab.TermElabM α
-- Init.Data.String.Basic
String.Slice.slice.congr_simp : ∀ (s : String.Slice) (newStart newStart_1 : s.Pos) (e_newStart : newStart = newStart_1) (newEnd newEnd_1 : s.Pos)
  (e_newEnd : newEnd = newEnd_1) (h : newStart ≤ newEnd), s.slice newStart newEnd h = s.slice newStart_1 newEnd_1 ⋯
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_ne_univ_iff_nonempty : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), sᶜ ≠ Finset.univ ↔ s.Nonempty
-- Init.Data.Nat.Div.Lemmas
Nat.div_pos : ∀ {b a : ℕ}, b ≤ a → 0 < b → 0 < a / b
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow_apply : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {n : ℕ}
  (hn_fac : IsUnit ↑(n - 1).factorial) (hnI : I ^ n = 0) {m : ℕ} {x : A},
  (DividedPowers.OfInvertibleFactorial.dividedPowers hn_fac hnI).dpow m x =
    if x ∈ I then Ring.inverse ↑m.factorial * x ^ m else 0
-- Init.Data.SInt.Lemmas
Int16.toISize_ne_neg_one : ∀ (a : Int16), a ≠ -1 → a.toISize ≠ -1
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.removeNeutrals.loop.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_coeff_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → Bool
-- Mathlib.Algebra.Order.Group.Finset
Finset.add_sup : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] [CanonicallyOrderedAdd M]
  [inst_3 : Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} [inst_6 : OrderBot M],
  s.Nonempty → ∀ (f : ι → M) (a : M), a + s.sup f = s.sup fun i => a + f i
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whisker_assoc_symm_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g' h) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h)) h_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g' h).hom h_1))
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.set_add_normalizer_comm : ∀ {G : Type u_2} [inst : AddGroup G] (S : Set G) (N : AddSubgroup G), S ⊆ ↑(AddSubgroup.normalizer ↑N) → S + ↑N = ↑N + S
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_minValue : ∀ (h : System.Platform.numBits = 32), ISize.minValue.toBitVec32 h = BitVec.intMin 32
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false)
  {h : k ∈ Std.DHashMap.Const.insertMany m l}, (Std.DHashMap.Const.insertMany m l).getKey k h = m.getKey k ⋯
-- Mathlib.Analysis.Polynomial.Norm
Polynomial.supNorm.eq_1 : ∀ {A : Type u_1} [inst : SeminormedRing A] (p : Polynomial A),
  p.supNorm = Polynomial.gaussNorm (SeminormedRing.toRingSeminorm A) 1 p
-- Mathlib.Topology.ContinuousOn
continuousOn_iff' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
/-- The absolute value satisfies the triangle inequality.  -/
abs_add_le : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b : α), |a + b| ≤ |a| + |b|
-- Mathlib.Algebra.Group.Prod
divMonoidHom.eq_1 : ∀ {α : Type u_6} [inst : DivisionCommMonoid α],
  divMonoidHom = { toFun := fun a => a.1 / a.2, map_one' := ⋯, map_mul' := ⋯ }
-- Std.Data.DTreeMap.Raw.Basic
/-- Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise `fallback`.
The key in the returned pair will compare equal to the input `a`.
 -/
Std.DTreeMap.Raw.getEntryD : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → (a : α) × β a → (a : α) × β a