mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
  {f : X → Y}, HolderWith C r f → 0 < r → Continuous f
-- Mathlib.InformationTheory.KullbackLeibler.ChainRule
/-- **Chain rule** for the Kullback-Leibler divergence, with conditional KL expressed using
composition-products.
This version holds without any assumption on the measurable spaces.  -/
InformationTheory.klDiv_compProd_eq_add : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} (μ ν : MeasureTheory.Measure 𝓧)
  (κ η : ProbabilityTheory.Kernel 𝓧 𝓨) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η],
  InformationTheory.klDiv (μ.compProd κ) (ν.compProd η) =
    InformationTheory.klDiv μ ν + InformationTheory.klDiv (μ.compProd κ) (μ.compProd η)
-- Mathlib.Data.List.Sublists
List.nodup_sublists : ∀ {α : Type u} {l : List α}, l.sublists.Nodup ↔ l.Nodup
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.function.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.function = 1
-- Mathlib.RingTheory.LocalProperties.Submodule
Submodule.eq_bot_of_localization_maximal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Algebra R (Rₚ P)]
  [inst_5 : ∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_6 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_7 : (P : Ideal R) → [inst_7 : P.IsMaximal] → Module R (Mₚ P)]
  [inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)]
  [inst_9 : ∀ (P : Ideal R) [inst_9 : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)]
  (f : (P : Ideal R) → [inst_10 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_10 : ∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (N : Submodule R M),
  (∀ (P : Ideal R) [inst_11 : P.IsMaximal], Submodule.localized' (Rₚ P) P.primeCompl (f P) N = ⊥) → N = ⊥
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalClosure_eq_iInf : ∀ {G : Type u_1} [inst : Group G] {s : Set G}, Subgroup.normalClosure s = ⨅ N, ⨅ (_ : N.Normal), ⨅ (_ : s ⊆ ↑N), N
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.closedCell_subset_complex`. -/
Topology.CWComplex.closedCell_subset_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.closedCell n j ⊆ C
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtrOn.comp_continuousOn : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β}
  [inst_2 : TopologicalSpace δ] {t : Set α} {s : Set δ} (g : δ → α) {b : δ},
  IsLocalExtrOn f t (g b) → s ⊆ g ⁻¹' t → ContinuousOn g s → b ∈ s → IsLocalExtrOn (f ∘ g) s b
-- Init.Data.SInt.Lemmas
Int32.toISize_mod : ∀ (a b : Int32), (a % b).toISize = a.toISize % b.toISize
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.SupportsStmt.match_1.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4) (a : Turing.Dir)
  (q : Turing.TM1.Stmt Γ Λ σ) (h_1 : (a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.move a q))
  (h_2 : (a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.write a q))
  (h_3 : (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.load a q))
  (h_4 : (a : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.branch a q₁ q₂))
  (h_5 : (l : Γ → σ → Λ) → motive (Turing.TM1.Stmt.goto l)) (h_6 : Unit → motive Turing.TM1.Stmt.halt),
  (match Turing.TM1.Stmt.move a q with
    | Turing.TM1.Stmt.move a q => h_1 a q
    | Turing.TM1.Stmt.write a q => h_2 a q
    | Turing.TM1.Stmt.load a q => h_3 a q
    | Turing.TM1.Stmt.branch a q₁ q₂ => h_4 a q₁ q₂
    | Turing.TM1.Stmt.goto l => h_5 l
    | Turing.TM1.Stmt.halt => h_6 ()) =
    h_1 a q
-- Mathlib.Data.ZMod.Basic
ZMod.cast_pow : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] {m : ℕ} [CharP R m], m ∣ n → ∀ (a : ZMod n) (k : ℕ), (a ^ k).cast = a.cast ^ k
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- If `I` is boundaryless, `M` has full interior.  -/
ModelWithCorners.interior_eq_univ : ∀ {𝕜 : 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] [BoundarylessManifold I M],
  ModelWithCorners.interior M = Set.univ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α}, Std.DTreeMap.Const.get! (t.erase k) k = default
-- Init.Data.List.Sort.Impl
List.MergeSort.Internal.splitRevInTwo'_fst : ∀ {α : Type u_1} {n : ℕ} (l : { l // l.length = n }),
  (List.MergeSort.Internal.splitRevInTwo' l).1 = ⟨↑(List.MergeSort.Internal.splitInTwo ⟨(↑l).reverse, ⋯⟩).2, ⋯⟩
-- Init.Data.String.Lemmas.Splits
String.Slice.splits_endPos : ∀ (s : String.Slice), s.endPos.Splits s.copy ""
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.pow_smul_eq_iff_minimalPeriod_dvd : ∀ {α : Type v} {G : Type u} [inst : Group G] [inst_1 : MulAction G α] {a : G} {b : α} {n : ℕ},
  a ^ n • b = b ↔ Function.minimalPeriod (fun x => a • x) b ∣ n
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- Vertical composition of modifications.  -/
CategoryTheory.Lax.OplaxTrans.Modification.vcomp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η θ ι : F ⟶ G} →
            CategoryTheory.Lax.OplaxTrans.Modification η θ →
              CategoryTheory.Lax.OplaxTrans.Modification θ ι → CategoryTheory.Lax.OplaxTrans.Modification η ι
-- Mathlib.Algebra.Homology.Monoidal
/-- The right unitor for the tensor product of homological complexes.  -/
HomologicalComplex.rightUnitor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive] →
            [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] →
              {I : Type u_2} →
                [inst_6 : AddMonoid I] →
                  {c : ComplexShape I} →
                    [inst_7 : c.TensorSigns] →
                      (K : HomologicalComplex C c) →
                        [inst_8 : DecidableEq I] →
                          [inst_9 :
                              ∀ (X₁ : C),
                                CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                                  ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] →
                            K.tensorObj (HomologicalComplex.tensorUnit C c) ≅ K
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.pullback.isLimit_lift : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g]
  (s : CategoryTheory.Limits.PullbackCone f g),
  (CompHausLike.pullback.isLimit f g).lift s = CompHausLike.pullback.lift f g s.fst s.snd ⋯
-- Init.Data.SInt.Lemmas
Int16.ofInt_eq_ofIntLE_mod : ∀ {a b : ℤ} (ha₁ : Int16.minValue.toInt ≤ a) (ha₂ : a ≤ Int16.maxValue.toInt) (hb₁ : Int16.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int16.maxValue.toInt), Int16.ofInt (a.tmod b) = Int16.ofIntLE a ha₁ ha₂ % Int16.ofIntLE b hb₁ hb₂
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Algebra.IsQuadraticExtension.toFree : ∀ {R : Type u_2} {S : Type u_3} {inst : CommSemiring R} {inst_1 : StrongRankCondition R} {inst_2 : Semiring S}
  {inst_3 : Algebra R S} [self : Algebra.IsQuadraticExtension R S], Module.Free R S
-- Init.Data.String.Basic
String.Pos.ofSliceTo_lt_ofSliceTo_iff : ∀ {s : String} {p : s.Pos} {q r : (s.sliceTo p).Pos}, String.Pos.ofSliceTo q < String.Pos.ofSliceTo r ↔ q < r
-- Mathlib.Algebra.Group.ULift
ULift.addRightCancelSemigroup.eq_1 : ∀ {α : Type u} [inst : AddRightCancelSemigroup α],
  ULift.addRightCancelSemigroup = Function.Injective.addRightCancelSemigroup ⇑Equiv.ulift ⋯ ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [EquivBEq α] {f : (a : α) → β a → γ a}
  {l : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKeyD k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) fallback =
      Std.Internal.List.getKeyD k l fallback
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
/-- The equivalence of categories between `GrpCat` and `AddGrpCat`
 -/
groupAddGroupEquivalence : GrpCat ≌ AddGrpCat
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_injOn_of_forall_sub_mem_Ioo : ∀ {s : Set ℝ}, (∀ x ∈ s, ∀ y ∈ s, x - y ∈ Set.Ioo (-2 * Real.pi) (2 * Real.pi)) → Set.InjOn (⇑Circle.exp) s
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.cutsatExt : Lean.Meta.Grind.SolverExtension Lean.Meta.Grind.Arith.Cutsat.State
-- Mathlib.Order.Lattice
instCommutativeMin_mathlib : ∀ {α : Type u} [inst : SemilatticeInf α], Std.Commutative fun x1 x2 => x1 ⊓ x2
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.d_comm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (i₁ i₁' : I₁) (i₂ i₂' : I₂),
  CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) ((K.X i₁').d i₂ i₂') =
    CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') ((K.d i₁ i₁').f i₂')
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Two different points are affinely independent.  -/
affineIndependent_of_ne : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ : P}, p₁ ≠ p₂ → AffineIndependent k ![p₁, p₂]
-- Mathlib.Algebra.Group.End
AddAut.coe_neg : ∀ (M : Type u_2) [inst : Add M] (e : AddAut M), ⇑(-e) = ⇑(AddEquiv.symm e)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Finite
CategoryTheory.Limits.instPreservesFiniteColimitsFunctorObjEvaluationOfHasFiniteColimits : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] [CategoryTheory.Limits.HasFiniteColimits C] (k : K),
  CategoryTheory.Limits.PreservesFiniteColimits ((CategoryTheory.evaluation K C).obj k)
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.eq_zero_iff_dvd : ∀ {R : Type u_5} [inst : CommRing R] (x y : R), (Ideal.Quotient.mk (Ideal.span {x})) y = 0 ↔ x ∣ y
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
/-- A local algebra isomorphism induces an algebra isomorphism on the residue fields.

See `mapAlgEquiv` for a variant where the base ring `R` is not quotiented.  -/
IsLocalRing.ResidueField.mapAlgEquiv' : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : IsLocalRing R] →
          [inst_2 : CommRing S] →
            [inst_3 : IsLocalRing S] →
              [inst_4 : CommRing T] →
                [inst_5 : IsLocalRing T] →
                  [inst_6 : Algebra R S] →
                    [inst_7 : Algebra R T] →
                      [inst_8 : IsLocalHom (algebraMap R S)] →
                        [inst_9 : IsLocalHom (algebraMap R T)] →
                          (S ≃ₐ[R] T) →
                            IsLocalRing.ResidueField S ≃ₐ[IsLocalRing.ResidueField R] IsLocalRing.ResidueField T
-- Lean.Data.NameMap.Basic
/-- `filter f s` returns the `NameHashSet` consisting of all `x` in `s` where `f x` returns `true`.  -/
Lean.NameHashSet.filter : (Lean.Name → Bool) → Lean.NameHashSet → Lean.NameHashSet
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.map_apply_eq_iff_map_symm_apply_eq : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) {f : β ≃ᵐ γ} (η : ProbabilityTheory.Kernel α γ),
  κ.map ⇑f = η ↔ κ = η.map ⇑f.symm
-- Mathlib.RingTheory.Localization.Basic
isScalarTower_localizationAlgebra : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {Rₘ : Type u_4} {Sₘ : Type u_5} [inst_3 : CommSemiring Rₘ] [inst_4 : CommSemiring Sₘ]
  [inst_5 : Algebra R Rₘ] [inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ]
  [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [inst_8 : Algebra R Sₘ] [IsScalarTower R S Sₘ],
  IsScalarTower R Rₘ Sₘ
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
/-- `stalkwise P` holds for a morphism if all stalks satisfy `P`.  -/
AlgebraicGeometry.stalkwise : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) →
  CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme
-- Mathlib.Algebra.Algebra.Subalgebra.Prod
Subalgebra.prod_inf_prod : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {S T : Subalgebra R A} {S₁ T₁ : Subalgebra R B},
  S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)
-- Init.Data.Iterators.Consumers.Monadic.Collect
/-- Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, `toListRev` is usually more efficient that `toList`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.toList`.
 -/
Std.IterM.Total.toList : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [Monad m] → [inst : Std.Iterator α m β] → [Std.Iterators.Finite α m] → Std.IterM.Total m β → m (List β)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Homeomorph.measurable : ∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace γ] [BorelSpace γ] (h : α ≃ₜ γ), Measurable ⇑h
-- Lean.Parser.Term
Lean.Parser.Term.generalizingParam : Lean.Parser.Parser
-- Mathlib.RingTheory.Localization.Defs
/-- If `M` contains `0` then the localization at `M` is trivial.  -/
IsLocalization.subsingleton : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S], 0 ∈ M → Subsingleton S
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.toL1.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f f_1 : α → β) (e_f : f = f_1) (hf : MeasureTheory.Integrable f μ),
  MeasureTheory.Integrable.toL1 f hf = MeasureTheory.Integrable.toL1 f_1 ⋯
-- Mathlib.Algebra.GroupWithZero.Defs
CommMonoidWithZero.toZero : {M₀ : Type u_2} → [self : CommMonoidWithZero M₀] → Zero M₀
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.top_lt : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : OrderTop α], Order.IsPredLimit a → a < ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.right_comp_retraction_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B)
  [inst_1 : CategoryTheory.IsCoreflexivePair f g] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (CategoryTheory.commonRetraction f g) h) = h
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y : C}
  [inst_2 : CategoryTheory.Closed A] (g : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ X),
  CategoryTheory.MonoidalClosed.curry g =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app Y) ((CategoryTheory.ihom A).map g)
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.toLieSubalgebra.eq_1 : ∀ (R : Type u_1) {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {h e f : L}
  (t : IsSl2Triple h e f),
  IsSl2Triple.toLieSubalgebra R t = { toSubmodule := Submodule.span R {e, f, h}, lie_mem' := ⋯ }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.toArray_toList_eq_toArray : ∀ {α : Type u} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (Std.DHashMap.Raw.Const.toList ↑m).toArray = Std.DHashMap.Raw.Const.toArray ↑m
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_le_coeff_tight : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.norm_le_coeff_tight_cert lhs rhs p k = true →
    (Int.Internal.Linear.Expr.denote ctx lhs ≤ Int.Internal.Linear.Expr.denote ctx rhs) =
      (Int.Internal.Linear.Poly.denote' ctx p ≤ 0)
-- Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
DomMulAct.smul_mulDistribActionHom_apply : ∀ {M : Type u_1} {N : Type u_2} {A : Type u_3} {B : Type u_4} [inst : AddMonoid A] [inst_1 : DistribSMul M A]
  [inst_2 : Monoid N] [inst_3 : AddMonoid B] [inst_4 : DistribMulAction N A] [inst_5 : SMulCommClass M N A]
  [inst_6 : DistribMulAction N B] (c : Mᵈᵐᵃ) (f : A →+[N] B) (a : A), (c • f) a = f (DomMulAct.mk.symm c • a)
-- Init.Data.SInt.Lemmas
Int16.ofInt_add : ∀ (a b : ℤ), Int16.ofInt (a + b) = Int16.ofInt a + Int16.ofInt b
-- Mathlib.Topology.Bornology.Absorbs
Absorbent.vadd_absorbs : ∀ {M : Type u_1} {E : Type u_2} [inst : Bornology M] [inst_1 : AddZeroClass E] [inst_2 : DistribSMul M E]
  {s₁ s₂ t : Set E} {x : E}, Absorbent M s₁ → Absorbs M s₂ t → Absorbs M (s₁ + s₂) (x +ᵥ t)
-- Mathlib.Algebra.Group.Irreducible.Defs
addIrreducible_iff : ∀ {M : Type u_1} [inst : AddMonoid M] {p : M},
  AddIrreducible p ↔ ¬IsAddUnit p ∧ ∀ ⦃a b : M⦄, p = a + b → IsAddUnit a ∨ IsAddUnit b
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- A generalisation of `FriendlyOperation.coind` which allows using `opf ∘ op'` in the tail
of `op s` where `opf` is friendly and `op'` is a function satisfying `motive`.  -/
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.coind_comp_friend_left : ∀ {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α} (motive : (Stream'.Seq α → Stream'.Seq α) → Prop),
  motive op →
    (∀ (op : Stream'.Seq α → Stream'.Seq α),
        motive op →
          ∃ T,
            ∀ (s : Stream'.Seq α),
              (op s).destruct =
                Option.map
                  (fun x =>
                    match x with
                    | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
                  (T s.head)) →
      Tactic.ComputeAsymptotics.Seq.FriendlyOperation op
-- Mathlib.Topology.Bornology.Hom
/-- The type of bounded maps from `α` to `β`, the maps which send a bounded set to a bounded set.  -/
LocallyBoundedMap : (α : Type u_6) → (β : Type u_7) → [Bornology α] → [Bornology β] → Type (max u_6 u_7)
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.mk : {X Y : SSet} →
  {i : X ⟶ Y} →
    {d : ℕ} →
      (simplex : Y.obj (Opposite.op { len := d })) →
        simplex ∈ Y.nonDegenerate d →
          simplex ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := d }))) →
            SSet.relativeCellComplexOfMono.Cell i d
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPMotivesAll : Lean.Options → Bool
-- Mathlib.Data.Fin.SuccPred
Fin.pred_last : ∀ {n : ℕ} (h : optParam (¬Fin.last (n + 1) = 0) ⋯), (Fin.last (n + 1)).pred h = Fin.last n
-- Mathlib.Order.Ideal
IsCoatom.isProper : ∀ {P : Type u_1} [inst : LE P] [inst_1 : IsDirectedOrder P] [inst_2 : Nonempty P] {I : Order.Ideal P},
  IsCoatom I → I.IsProper
-- Mathlib.Algebra.DirectSum.Ring
/-- A direct sum of copies of a `Semiring` inherits the multiplication structure.  -/
Semiring.directSumGSemiring : (ι : Type u_1) → {R : Type u_2} → [inst : AddMonoid ι] → [inst_1 : Semiring R] → DirectSum.GSemiring fun x => R
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {f : α → Bool} {k : α}, (Std.ExtHashSet.filter f m).get! k = (Option.filter f (m.get? k)).get!
-- Std.Data.DHashMap.Raw
/-- Carries out a monadic action on each mapping in the hash map in some order.  -/
Std.DHashMap.Raw.Const.forMUncurried : {α : Type u} →
  {m : Type w → Type w'} →
    [Monad m] → {β : Type v} → (α × β → m PUnit.{w + 1}) → (Std.DHashMap.Raw α fun x => β) → m PUnit.{w + 1}
-- Lean.Meta.Tactic.Grind.PP
Lean.Meta.Grind.ppGoals : List Lean.Meta.Grind.Goal → Lean.MetaM Lean.MessageData
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.isometry_map_mkMetric : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] (m : ENNReal → ENNReal) {f : X → Y},
  Isometry f →
    Monotone m ∨ Function.Surjective f →
      (MeasureTheory.OuterMeasure.map f) (MeasureTheory.OuterMeasure.mkMetric m) =
        (MeasureTheory.OuterMeasure.restrict (Set.range f)) (MeasureTheory.OuterMeasure.mkMetric m)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.isAdmissible_of_isChain_of_forall_getElem_le : ∀ {m : ℕ} {L : List ℕ},
  List.IsChain (fun x1 x2 => x1 < x2) L →
    (∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k) → SimplexCategoryGenRel.IsAdmissible m L
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.instIsClosedUnderLimitsOfShapeOverIsMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} J]
  (X : C), (CategoryTheory.Over.isMono X).IsClosedUnderLimitsOfShape J
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.codisjoint_map : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N},
  Function.Surjective ⇑f → ∀ {H K : Subgroup G}, Codisjoint H K → Codisjoint (Subgroup.map f H) (Subgroup.map f K)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
Std.IterM.toList_take_zero : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite (Std.Iterators.Types.Take α m) m] {it : Std.IterM m β}, (Std.IterM.take 0 it).toList = pure []
-- Mathlib.CategoryTheory.Center.Localization
CategoryTheory.CatCenter.localization.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (r r_1 : CategoryTheory.CatCenter C),
  r = r_1 →
    ∀ (L L_1 : CategoryTheory.Functor C D) (e_L : L = L_1) (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1)
      [inst_2 : L.IsLocalization W], r.localization L W = r_1.localization L_1 W_1
-- Lean.Server.CodeActions.Provider
Lean.CodeAction.FindTacticResult.tactic.inj : ∀ {a a_1 : Lean.Syntax.Stack},
  Lean.CodeAction.FindTacticResult.tactic a = Lean.CodeAction.FindTacticResult.tactic a_1 → a = a_1
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.Hom.partialIso_source : ∀ {X U : AlgebraicGeometry.Scheme} (f : U ⟶ X) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsDominant f], (AlgebraicGeometry.Scheme.Hom.partialIso f).source = ⊤