mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Sublist
List.sublist_cons_self : ∀ {α : Type u_1} (a : α) (l : List α), l.Sublist (a :: l)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.eta_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F),
  c.eta.inv.hom = CategoryTheory.CategoryStruct.id c.pt
-- Lean.Server.FileWorker.SemanticHighlighting
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState.mk.inj : ∀ {nonOverlapping : Array Lean.Server.FileWorker.AbsoluteLspSemanticToken}
  {current? : Option Lean.Server.FileWorker.AbsoluteLspSemanticToken}
  {surrounding : List Lean.Server.FileWorker.AbsoluteLspSemanticToken}
  {nonOverlapping_1 : Array Lean.Server.FileWorker.AbsoluteLspSemanticToken}
  {current?_1 : Option Lean.Server.FileWorker.AbsoluteLspSemanticToken}
  {surrounding_1 : List Lean.Server.FileWorker.AbsoluteLspSemanticToken},
  { nonOverlapping := nonOverlapping, current? := current?, surrounding := surrounding } =
      { nonOverlapping := nonOverlapping_1, current? := current?_1, surrounding := surrounding_1 } →
    nonOverlapping = nonOverlapping_1 ∧ current? = current?_1 ∧ surrounding = surrounding_1
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.coe_comp : ∀ {X Y Z : GrpWithZero} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.zero_rpow_eq_iff : ∀ {x a : ℝ}, 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
-- Init.Data.String.Basic
String.Slice.Pos.get_eq_get_ofSliceFrom : ∀ {s : String.Slice} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos} {h : pos ≠ (s.sliceFrom p₀).endPos},
  pos.get h = (String.Slice.Pos.ofSliceFrom pos).get ⋯
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.bientails.mp : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, (P ⊣⊢ₛ Q) → P ⊢ₛ Q
-- Lean.Elab.Match
/-- Checks the number of patterns and appropriately adds holes if needed.  -/
Lean.Elab.Term.checkNumPatterns : ℕ → Array Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Syntax)
-- Mathlib.Analysis.Normed.Group.Constructions
Multiplicative.seminormedGroup : {E : Type u_2} → [SeminormedAddGroup E] → SeminormedGroup (Multiplicative E)
-- Mathlib.Order.Lattice
sup_eq_left : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = a ↔ b ≤ a
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.Ordnode.ofAscListAux₁.match_5.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((x : α) → (xs : List α) → motive (x :: xs)) → motive x
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.empty_not_isCircuit : ∀ {α : Type u_1} (M : Matroid α), ¬M.IsCircuit ∅
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δAux_toAlgHom : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {ι' : Type w₃} {Q : Algebra.Generators S T ι} {Q' : Algebra.Generators S T ι'} (f : Q.Hom Q') (x : Q.Ring),
  (Algebra.Generators.H1Cotangent.δAux R Q') (f.toAlgHom x) =
    (Algebra.Generators.H1Cotangent.δAux R Q) x +
      (Finsupp.linearCombination T (⇑(Algebra.Generators.H1Cotangent.δAux R Q') ∘ f.val))
        (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (KaehlerDifferential.D S Q.Ring) x))
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.isTriangulated_of_iso : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] [inst_4 : CategoryTheory.Limits.HasZeroObject C]
  [inst_5 : CategoryTheory.Limits.HasZeroObject D] [inst_6 : CategoryTheory.Preadditive C]
  [inst_7 : CategoryTheory.Preadditive D] [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂)
  [inst_12 : F₁.CommShift ℤ] [inst_13 : F₂.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ] [F₁.IsTriangulated],
  F₂.IsTriangulated
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.FormatType.match_1.eq_3 : ∀ (motive : Std.Time.FormatString → Sort u_1)
  (h_1 :
    (entry : Std.Time.Modifier) → (xs : List Std.Time.FormatPart) → motive (Std.Time.FormatPart.modifier entry :: xs))
  (h_2 : (val : String) → (xs : List Std.Time.FormatPart) → motive (Std.Time.FormatPart.string val :: xs))
  (h_3 : Unit → motive []),
  (match [] with
    | Std.Time.FormatPart.modifier entry :: xs => h_1 entry xs
    | Std.Time.FormatPart.string val :: xs => h_2 val xs
    | [] => h_3 ()) =
    h_3 ()
-- Mathlib.Topology.CompactOpen
ContinuousMap.image_coev : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {y : Y} (s : Set X),
  ⇑(ContinuousMap.coev X Y y) '' s = {y} ×ˢ s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_insert_le_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {km kmi : α}, t.minKey? = some km → (t.insert k v).minKey?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The associator isomorphism for binary coproducts.  -/
CategoryTheory.Limits.coprod.associator : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] → (P Q R : C) → (P ⨿ Q) ⨿ R ≅ P ⨿ Q ⨿ R
-- Mathlib.Topology.AlexandrovDiscrete
interior_iInter : ∀ {ι : Sort u_1} {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] (f : ι → Set α),
  interior (⋂ i, f i) = ⋂ i, interior (f i)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.trans_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Semiring C]
  [inst_6 : TopologicalSpace C] [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : Algebra R C] (e₁ : A ≃A[R] B)
  (e₂ : B ≃A[R] C) (a : A), (e₁.trans e₂) a = e₂ (e₁ a)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α},
  t.getKey? k = some k' → k' ∈ t
-- Mathlib.Algebra.Homology.Homotopy
/-- A homotopy between morphisms of homological complexes `K ⟶ L` induces a homotopy
between morphisms of short complexes `K.sc i ⟶ L.sc i`.  -/
Homotopy.toShortComplex : {C : Type u_2} →
  [inst : CategoryTheory.Category.{v_1, u_2} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_3} →
        {c : ComplexShape ι} →
          [DecidableRel c.Rel] →
            {K L : HomologicalComplex C c} →
              {f g : K ⟶ L} →
                Homotopy f g →
                  (i : ι) →
                    CategoryTheory.ShortComplex.Homotopy ((HomologicalComplex.shortComplexFunctor C c i).map f)
                      ((HomologicalComplex.shortComplexFunctor C c i).map g)
-- Mathlib.Data.FunLike.IsApply
IsVAddApply.mk : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} [inst : FunLike F α β]
  [inst_1 : VAdd M β] [inst_2 : VAdd M F], (∀ (f : F) (n : M) (x : α), (n +ᵥ f) x = n +ᵥ f x) → IsVAddApply M F α β
-- Aesop.Util.UnorderedArraySet
Aesop.instInhabitedUnorderedArraySet.default : {α : Type u_1} → {inst : BEq α} → Aesop.UnorderedArraySet α
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- To prove that a property holds for any strongly measurable function, it is enough to show
that it holds for constant indicator functions of measurable sets and that it is closed under
addition and pointwise limit.

To use in an induction proof, the syntax is
`induction f, hf using StronglyMeasurable.induction with`.  -/
MeasureTheory.StronglyMeasurable.induction : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : AddZeroClass β] [inst_2 : TopologicalSpace β]
  {P : (f : α → β) → MeasureTheory.StronglyMeasurable f → Prop},
  (∀ (c : β) ⦃s : Set α⦄ (hs : MeasurableSet s), P (s.indicator fun x => c) ⋯) →
    (∀ ⦃f g : α → β⦄ (hf : MeasureTheory.StronglyMeasurable f) (hg : MeasureTheory.StronglyMeasurable g)
        (hfg : MeasureTheory.StronglyMeasurable (f + g)),
        Disjoint (Function.support f) (Function.support g) → P f hf → P g hg → P (f + g) hfg) →
      (∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (f n))
          (hg : MeasureTheory.StronglyMeasurable g),
          (∀ (n : ℕ), P (f n) ⋯) →
            (∀ (x : α), Filter.Tendsto (fun x_1 => f x_1 x) Filter.atTop (nhds (g x))) → P g hg) →
        ∀ (f : α → β) (hf : MeasureTheory.StronglyMeasurable f), P f hf
-- Mathlib.Topology.Algebra.ConstMulAction
tendsto_const_vadd_iff : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G]
  [inst_2 : AddAction G α] [ContinuousConstVAdd G α] {f : β → α} {l : Filter β} {a : α} (c : G),
  Filter.Tendsto (fun x => c +ᵥ f x) l (nhds (c +ᵥ a)) ↔ Filter.Tendsto f l (nhds a)
-- Std.Time.Zoned.ZoneRules
/-- Find the current `TimeZone` out of a `Transition` in a `ZoneRules`
 -/
Std.Time.TimeZone.ZoneRules.timezoneAt : Std.Time.TimeZone.ZoneRules → Std.Time.Timestamp → Std.Time.TimeZone
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
/-- the homology map is an isomorphism  -/
CategoryTheory.ShortComplex.QuasiIso.isIso' : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {S₁ S₂ : CategoryTheory.ShortComplex C} {inst_2 : S₁.HasHomology} {inst_3 : S₂.HasHomology} {φ : S₁ ⟶ S₂}
  [self : CategoryTheory.ShortComplex.QuasiIso φ], CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
-- Mathlib.Data.Rel
SetRel.image_inv : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t : Set β), R.inv.image t = R.preimage t
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.sheafEquivOver_unitIso_inv_app_hom_app : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) {A : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} A] (X_1 : CategoryTheory.Sheaf ((Opens.grothendieckTopology X).over U) A)
  (X_2 : (CategoryTheory.Over U)ᵒᵖ),
  (U.sheafEquivOver.unitIso.inv.app X_1).hom.app X_2 =
    X_1.obj.map (U.overEquivalence.unitIso.hom.app (Opposite.unop X_2)).op
-- Lean.Parser.Basic
Lean.Parser.PrattParsingTables.mk.sizeOf_spec : ∀ (leadingTable : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)) (leadingParsers : List (Lean.Parser.Parser × ℕ))
  (trailingTable : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)) (trailingParsers : List (Lean.Parser.Parser × ℕ)),
  sizeOf
      { leadingTable := leadingTable, leadingParsers := leadingParsers, trailingTable := trailingTable,
        trailingParsers := trailingParsers } =
    1 + sizeOf leadingTable + sizeOf leadingParsers + sizeOf trailingTable + sizeOf trailingParsers
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rio.Internal.toList_eq_toList_iter : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rio α}, r.toList = (Std.Rio.Internal.iter r).toList
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.ofArrowIso_e : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  (F : CategoryTheory.Limits.MonoFactorisation f.hom) (sq : f ⟶ g) [inst_1 : CategoryTheory.IsIso sq],
  (F.ofArrowIso sq).e = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Arrow.Hom.left sq)) F.e
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.smul_faceOppositeCentroid_vsub_point_eq_sum_vsub : ∀ {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] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  ↑n • (s.faceOppositeCentroid i -ᵥ s.points i) = ∑ x, (s.points x -ᵥ s.points i)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- A finite orthonormal family of vectors whose span has trivial orthogonal complement is an
orthonormal basis.  -/
OrthonormalBasis.mkOfOrthogonalEqBot : {ι : Type u_1} →
  {𝕜 : Type u_3} →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : Fintype ι] →
              {v : ι → E} → Orthonormal 𝕜 v → (Submodule.span 𝕜 (Set.range v))ᗮ = ⊥ → OrthonormalBasis ι 𝕜 E
-- Mathlib.Data.Seq.Computation
Computation.of_thinkN_terminates : ∀ {α : Type u} (s : Computation α) (n : ℕ), (s.thinkN n).Terminates → s.Terminates
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_append_size_left : ∀ {a b : ByteArray} {i : ℕ}, (a ++ b).extract i a.size = a.extract i a.size
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Problem.mvarId : Lean.Meta.Match.Problem → Lean.MVarId
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.instPreservesLimitWalkingCospanCospanOfIsIso_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [CategoryTheory.IsIso g], CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) F
-- Mathlib.Topology.Algebra.ProperConstSMul
/-- `(c +ᵥ ·)` is a proper map.  -/
isProperMap_vadd : ∀ {M : Type u_1} (c : M) (X : Type u_2) [inst : VAdd M X] [inst_1 : TopologicalSpace X] [h : ProperConstVAdd M X],
  IsProperMap fun x => c +ᵥ x
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Functor.q_isLocalization : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C),
  W.Q.IsLocalization W
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.homogeneous : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m)
  (q :
    ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
            (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace),
  Ideal.IsHomogeneous 𝒜 (AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal f_deg hm q)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.zeroEquiv_symm_apply : ∀ (R : Type u) [inst : CommRing R] (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (a : R),
  (exteriorPower.zeroEquiv R M).symm a = a • (exteriorPower.ιMulti R 0) fun a => ⋯.elim
-- Aesop.Rule
Aesop.instInhabitedUnsafeRuleInfo.default : Aesop.UnsafeRuleInfo
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.weights_single : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R] (x : M),
  (Convexity.StdSimplex.single x).weights = fun₀ | x => 1
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- A family of additive monoid homomorphisms `f a : γ →+ β a` defines a monoid homomorphism
`Pi.addMonoidHom f : γ →+ Π a, β a` given by `Pi.addMonoidHom f x b = f b x`.  -/
AddMonoidHom.pi : {I : Type u} →
  {f : I → Type v} →
    [inst : (i : I) → AddZeroClass (f i)] →
      {γ : Type w} → [inst_1 : AddZeroClass γ] → ((i : I) → γ →+ f i) → γ →+ (i : I) → f i
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instIsCentralVAdd : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : VAdd M X] [inst_2 : ContinuousConstVAdd M X]
  [inst_3 : VAdd Mᵃᵒᵖ X] [inst_4 : IsCentralVAdd M X], IsCentralVAdd M (SeparationQuotient X)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_add : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜]
  (I J : HomogeneousIdeal 𝒜), (I + J).toIdeal = I.toIdeal + J.toIdeal
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- The localization of an `AddCommMonoid` at one of its submonoids (as a quotient type).  -/
AddLocalization : {M : Type u_1} → [inst : AddCommMonoid M] → AddSubmonoid M → Type u_1
-- Init.Data.UInt.Lemmas
USize.toNat_ofBitVec : ∀ {a : BitVec System.Platform.numBits}, { toBitVec := a }.toNat = a.toNat
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
AddCommMonCat.forget_isCorepresentable : (CategoryTheory.forget AddCommMonCat).IsCorepresentable
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.union.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Raw α β),
  m₁.union m₂ =
    if h₁ : 0 < m₁.buckets.size then
      if h₂ : 0 < m₂.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.union ⟨m₁, h₁⟩ ⟨m₂, h₂⟩) else m₁
    else m₂
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding : ∀ {K : Type u_1} [inst : Field K] (x : K) (w : NumberField.InfinitePlace K),
  NumberField.mixedEmbedding.normAtAllPlaces ((NumberField.mixedEmbedding K) x) w = w x
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Coerce a gcf by elementwise coercion.  -/
GenContFract.instCoe : {α : Type u_1} → {β : Type u_2} → [Coe α β] → Coe (GenContFract α) (GenContFract β)
-- Init.Data.UInt.Bitwise
instCommutativeUInt64HXor : Std.Commutative fun x1 x2 => x1 ^^^ x2
-- Mathlib.RingTheory.FiniteLength
IsFiniteLength.below.of_simple_quotient : ∀ {R : Type u_1} [inst : Ring R]
  {motive : (M : Type u_2) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → IsFiniteLength R M → Prop}
  {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M} [inst_3 : IsSimpleModule R (M ⧸ N)]
  (a : IsFiniteLength R ↥N), IsFiniteLength.below a → motive (↥N) a → IsFiniteLength.below ⋯
-- Mathlib.Algebra.Module.Injective
Module.Baer.instPartialOrderExtensionOf : {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) → PartialOrder (Module.Baer.ExtensionOf i f)
-- Lean.Elab.Tactic.Try
/-- Executes code with unlimited heartbeats (maxHeartbeats set to 0).
Used by try? infrastructure itself so it doesn't timeout while testing tactics.
 -/
Lean.Elab.Tactic.Try.withUnlimitedHeartbeats : {α : Type} →
  {m : Type → Type} → [Monad m] → [MonadWithReaderOf Lean.Core.Context m] → [MonadControlT Lean.CoreM m] → m α → m α
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_mul_le : ∀ {m : Type um} {n : Type un} {o : Type uo} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype o]
  [inst_2 : CommSemiring R] [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R),
  (A * B).rank ≤ min A.rank B.rank
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.ringHom_ext : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A]
  {f g : MvPolynomial σ R →+* A},
  (∀ (r : R), f (MvPolynomial.C r) = g (MvPolynomial.C r)) →
    (∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) → f = g
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.mem_subgroupOf : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} {h : ↥K}, h ∈ H.subgroupOf K ↔ ↑h ∈ H
-- Init.Data.UInt.Bitwise
instCommutativeUInt8HXor : Std.Commutative fun x1 x2 => x1 ^^^ x2
-- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
InformationTheory.toReal_klDiv_map_of_ac : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {g : 𝓧 → 𝓨},
  μ.AbsolutelyContinuous ν →
    Measurable g →
      (InformationTheory.klDiv (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν)).toReal =
        ∫ (x : 𝓧), InformationTheory.klFun (ν[fun x => (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨] x) ∂ν
-- Mathlib.Order.WithBot
/-- A version of `lt_top_iff_ne_top` for `WithTop` that only requires `LT α`, not
`PartialOrder α`.  -/
WithTop.lt_top_iff_ne_top : ∀ {α : Type u_1} [inst : LT α] {x : WithTop α}, x < ⊤ ↔ x ≠ ⊤
-- Mathlib.SetTheory.Cardinal.Divisibility
Cardinal.nat_coe_dvd_iff : ∀ {n m : ℕ}, ↑n ∣ ↑m ↔ n ∣ m
-- Batteries.Tactic.Lint.Basic
/-- A `NamedLinter` is a linter associated to a particular declaration.  -/
Batteries.Tactic.Lint.NamedLinter : Type
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.eraseMany : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {ρ : Type u_1} [inst : ForIn Id ρ α] {l : ρ}
  {t : Std.TreeMap.Raw α β cmp}, t.WF → (t.eraseMany l).WF
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.quasiIsoAt_πTruncGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n q : ℤ), n ≤ q → QuasiIsoAt (K.πTruncGE n) q
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
/-- `birdDet n A` computes the determinant of the `n × n` matrix whose entries are
stored in `A` in row-major order.
 -/
BirdDet.birdDet : {R : Type u_1} → [CommRing R] → ℕ → Array R → R
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.iInf : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} [inst_2 : InfSet β] [Countable ι]
  (hf : ∀ (i : ι), AEMeasurable (f i) μ), (∀ᵐ (x : α) ∂μ, p x fun n => f n x) → ⨅ n, aeSeq hf p n =ᵐ[μ] ⨅ n, f n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.entryAtIdx_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {i : ℕ}
  {h' : i < t₁.size} (h : t₁.Equiv t₂), t₁.entryAtIdx i h' = t₂.entryAtIdx i ⋯
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.toWithBotSyn_symm_apply_bot : ∀ {σ : Type u_1} (m : MonomialOrder σ), m.toWithBotSyn.symm ⊥ = ⊥
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.instHashableSeq_lean : Hashable Lean.Grind.AC.Seq
-- Mathlib.Data.Nat.ModEq
/-- Cancel left multiplication in the modulus.

For cancelling left multiplication on both sides of the `≡`, see `nat.modeq.mul_left_cancel'`.  -/
Nat.ModEq.of_mul_left : ∀ {n a b : ℕ} (m : ℕ), a ≡ b [MOD m * n] → a ≡ b [MOD n]
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
/-- When `cfc` is applied to a function that maps zero to zero, it is equivalent to using
`cfcₙ`.  -/
cfcₙ_eq_cfc : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p]
  [ContinuousMapZero.UniqueHom R A] {f : R → R} {a : A},
  autoParam (ContinuousOn f (quasispectrum R a)) cfcₙ_eq_cfc._auto_1 →
    autoParam (f 0 = 0) cfcₙ_eq_cfc._auto_3 → cfcₙ f a = cfc f a
-- Mathlib.Topology.Instances.AddCircle.DenseSubgroup
/-- A subgroup of the circle `ℝ⧸pℤ`, `p > 0`, is dense
iff it is not generated by a single element of finite additive order.  -/
AddCircle.dense_addSubgroup_iff_ne_zmultiples : ∀ {p : ℝ} [Fact (0 < p)] {s : AddSubgroup (AddCircle p)},
  Dense ↑s ↔ ∀ (a : AddCircle p), addOrderOf a ≠ 0 → s ≠ AddSubgroup.zmultiples a