mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_pow_pow : ∀ {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {m n : ℕ}, m < n → (fun x => x ^ n) =o[nhds 0] fun x => x ^ m
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  (Std.Internal.List.insertEntry k v l).isEmpty = false
-- Mathlib.Data.Finset.Disjoint
Finset.decidableDisjoint : {α : Type u_2} → [DecidableEq α] → (U V : Finset α) → Decidable (Disjoint U V)
-- Mathlib.Algebra.Order.Group.Abs
mabs_mul' : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] (a b : G), |a|ₘ ≤ |b|ₘ * |b * a|ₘ
-- Mathlib.Order.BourbakiWitt
NonemptyChain.mk.sizeOf_spec : ∀ {α : Type u_4} [inst : LE α] [inst_1 : SizeOf α] (carrier : Set α) (Nonempty' : carrier.Nonempty)
  (isChain' : IsChain (fun x1 x2 => x1 ≤ x2) carrier),
  sizeOf { carrier := carrier, Nonempty' := Nonempty', isChain' := isChain' } = 1 + sizeOf Nonempty'
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsRightInversion.eq_1 : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w t : W),
  cs.IsRightInversion w t = (cs.IsReflection t ∧ cs.length (w * t) < cs.length w)
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.irreducible_of_irreducible_absNorm : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] {I : Ideal S},
  Irreducible (Ideal.absNorm I) → Irreducible I
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.E : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Weekday
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.comapDomain_add : ∀ {ι : Type u} {β : ι → Type v} {κ : Type u_1} [inst : (i : ι) → AddZeroClass (β i)] (h : κ → ι)
  (hh : Function.Injective h) (f g : Π₀ (i : ι), β i),
  DFinsupp.comapDomain h hh (f + g) = DFinsupp.comapDomain h hh f + DFinsupp.comapDomain h hh g
-- Init.Data.List.ToArray
List.set_toArray : ∀ {α : Type u_1} (l : List α) (i : ℕ) (a : α) (h : i < l.length), l.toArray.set i a h = (l.set i a).toArray
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_modify : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} [inst_4 : Inhabited β] {f : β → β},
  m.WF → (m.modify k f)[k']! = if (k == k') = true then (Option.map f m[k]?).get! else m[k']!
-- Mathlib.Logic.Equiv.Finset
Denumerable.isChain_cons_raise' : ∀ (l : List ℕ) (m : ℕ), List.IsChain (fun x1 x2 => x1 < x2) (m :: Denumerable.raise' l (m + 1))
-- Mathlib.Analysis.Convex.Basic
Convex.smul_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (c : 𝕜), Convex 𝕜 ((fun z => c • z) ⁻¹' s)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add_comp : ∀ {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.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y Z : C} {X' Y' Z' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y')
  (eZ : L.obj Z ≅ Z') (f₁ f₂ : X' ⟶ Y') (g : Y' ⟶ Z'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Preadditive.add W eX eY f₁ f₂) g =
    CategoryTheory.Localization.Preadditive.add W eX eZ (CategoryTheory.CategoryStruct.comp f₁ g)
      (CategoryTheory.CategoryStruct.comp f₂ g)
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
intervalIntegral.inv_mul_integral_comp_div_add : ∀ {a b : ℝ} {f : ℝ → ℝ} (c d : ℝ), c⁻¹ * ∫ (x : ℝ) in a..b, f (x / c + d) = ∫ (x : ℝ) in a / c + d..b / c + d, f x
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.exists_iso_Q_obj_of_isLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory C) (n : ℤ) [hX : X.IsLE n],
  ∃ K, ∃ (_ : K.IsStrictlyLE n), Nonempty (X ≅ DerivedCategory.Q.obj K)
-- Mathlib.Order.Category.Preord
preordToCat_map : ∀ {X Y : Preord} (f : X ⟶ Y), preordToCat.map f = ⋯.functor.toCatHom
-- Mathlib.RingTheory.HopfAlgebra.Basic
HopfAlgebra.sum_mul_antipode_eq_smul : ∀ {R : Type u} {A : Type v} {ι : Type u_1} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A]
  {a : A} (repr : Coalgebra.Repr R a ι),
  ∑ i ∈ repr.index, repr.left i * (HopfAlgebraStruct.antipode R) (repr.right i) = CoalgebraStruct.counit a • 1
-- Mathlib.Order.BoundedOrder.Basic
bot_lt_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [Nontrivial α], ⊥ < ⊤
-- Init.Data.UInt.Lemmas
UInt64.le_iff_toNat_le : ∀ {a b : UInt64}, a ≤ b ↔ a.toNat ≤ b.toNat
-- Mathlib.FieldTheory.SeparableDegree
/-- A polynomial has non-zero separable degree if and only if it is non-constant.  -/
Polynomial.natSepDegree_ne_zero_iff : ∀ {F : Type u} [inst : Field F] (f : Polynomial F), f.natSepDegree ≠ 0 ↔ f.natDegree ≠ 0
-- Mathlib.Order.LiminfLimsup
Filter.cofinite.blimsup_set_eq : ∀ {α : Type u_1} {ι : Type u_4} {p : ι → Prop} {s : ι → Set α},
  Filter.blimsup s Filter.cofinite p = {x | {n | p n ∧ x ∈ s n}.Infinite}
-- Mathlib.SetTheory.Ordinal.Notation
ONote.split.eq_def : ∀ (x : ONote),
  x.split =
    match x with
    | ONote.zero => (0, 0)
    | e.oadd n a =>
      if e = 0 then (0, ↑n)
      else
        match a.split with
        | (a', m) => (e.oadd n a', m)
-- Aesop.RuleSet
Aesop.GlobalRuleSet.onBaseM : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    [Monad m] → (Aesop.BaseRuleSet → m (Aesop.BaseRuleSet × α)) → Aesop.GlobalRuleSet → m (Aesop.GlobalRuleSet × α)
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker_eq_top_of_subsingleton : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rcf : RingHomClass F R S] [Subsingleton S] (f : F), RingHom.ker f = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.pullbackAssoc_inv_fst_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄]
  [inst_4 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
        (CategoryTheory.Limits.pullback.fst f₁ f₂)) =
    CategoryTheory.Limits.pullback.fst f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)
-- Mathlib.Topology.Semicontinuity.Defs
semicontinuous_iff_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop},
  Semicontinuous r ↔ ∀ (b : β), IsOpen {x | r x b}
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.centralizer_centralizer_centralizer : ∀ (M : Type u_1) [inst : Monoid M] {s : Set M},
  Submonoid.centralizer s.centralizer.centralizer = Submonoid.centralizer s
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.fundamentalGroupToMulOpposite_injective : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {x : X} (e : ↑(p ⁻¹' {x}))
  [SimplyConnectedSpace E], Function.Injective ⇑(hp.fundamentalGroupToMulOpposite e)
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the smallest element that is greater than or equal to the
given element, panicking if no such element exists.
 -/
Std.TreeSet.Raw.getGE! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet.Raw α cmp → α → α
-- Mathlib.Topology.Basic
isOpen_fold : ∀ {X : Type u} {s : Set X} {t : TopologicalSpace X}, TopologicalSpace.IsOpen s = IsOpen s
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.lTensor_exact_iff_exact : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N1 : Type u_1}
  [inst_3 : AddCommGroup N1] [inst_4 : Module R N1] {N2 : Type u_2} [inst_5 : AddCommGroup N2] [inst_6 : Module R N2]
  {N3 : Type u_3} [inst_7 : AddCommGroup N3] [inst_8 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3)
  [Module.FaithfullyFlat R M],
  Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23) ↔ Function.Exact ⇑l12 ⇑l23
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.topologicalSpaceConePtOfConeForget : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    {F : CategoryTheory.Functor J TopCat} →
      (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget TopCat))) →
        TopologicalSpace (TopCat.conePtOfConeForget c)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Complex.continuousAt_Gamma_one : ContinuousAt Complex.Gamma 1
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Convenience reformulation of the second iterated derivative, as a map from `E` to bilinear maps
`E →ₗ[ℝ] E →ₗ[ℝ] ℝ`.
 -/
bilinearIteratedFDerivWithinTwo : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → (E → F) → Set E → E → E →ₗ[𝕜] E →ₗ[𝕜] F
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.instIsIsoContinuousGeneratedByCatMapTopCatToContinuousGeneratedByCatAppAdjCounit : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] (Z : TopCat),
  CategoryTheory.IsIso ((TopCat.toContinuousGeneratedByCat X).map (GeneratedByTopCat.adjCounit.app Z))
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.leftUnitor_comp_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c}
  (h : CategoryTheory.CategoryStruct.comp f g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).hom
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).hom g) h)
-- Mathlib.Analysis.Convex.Strict
strictConvex_Iic : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace β]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [OrderTopology β]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r : β), StrictConvex 𝕜 (Set.Iic r)
-- Aesop.Builder.Constructors
Aesop.RuleBuilder.getConstructorsIndexingMode : Lean.Meta.TransparencyMode → Lean.InductiveVal → Lean.MetaM Aesop.IndexingMode
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.hasStrictDerivAt_arcosh : ∀ {x : ℝ}, x ∈ Set.Ioi 1 → HasStrictDerivAt Real.arcosh (√(x ^ 2 - 1))⁻¹ x
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
GenContFract.IntFractPair.fr : {K : Type u_1} → GenContFract.IntFractPair K → K
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.HasProducts.instHasProduct : ∀ (J : Type v) (f : J → ωCPO), CategoryTheory.Limits.HasProduct f
-- Init.Data.SInt.Lemmas
Int8.toBitVec_mul : ∀ {a b : Int8}, (a * b).toBitVec = a.toBitVec * b.toBitVec
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.homologyShortComplex_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ),
  (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.homologyShortComplex✝ f n).f =
    HomologicalComplex.homologyMap f n
-- Mathlib.Algebra.Group.Basic
div_mul_eq_mul_div : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a / b * c = a * c / b
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
CategoryTheory.Functor.IsWellOrderContinuous.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : PartialOrder J]
  {F : CategoryTheory.Functor J C},
  (∀ (m : J), Order.IsSuccLimit m → Nonempty (CategoryTheory.Limits.IsColimit ((Set.principalSegIio m).cocone F))) →
    F.IsWellOrderContinuous
-- Init.Data.UInt.Lemmas
instAssociativeUInt64HMul : Std.Associative fun x1 x2 => x1 * x2
-- Mathlib.Data.Sym.Sym2
Sym2.instSubsingleton : ∀ {α : Type u_1} [Subsingleton α], Subsingleton (Sym2 α)
-- Init.Data.SInt.Lemmas
Int8.toInt_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt = (↑n).bmod Int8.size
-- Mathlib.Analysis.ODE.PicardLindelof
/-- Given a continuous time-dependent vector field `f` and a continuous curve `α`, the composition
`f t (α t)` is continuous in `t`.  -/
ODE.continuousOn_comp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {α : ℝ → E} {s : Set ℝ} {u : Set E},
  ContinuousOn (Function.uncurry f) (s ×ˢ u) → ContinuousOn α s → Set.MapsTo α s u → ContinuousOn (fun t => f t (α t)) s
-- Mathlib.Topology.Algebra.Module.Basic
QuotientModule.Quotient.topologicalSpace : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → [TopologicalSpace M] → (S : Submodule R M) → TopologicalSpace (M ⧸ S)
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.Embedding.toPartialEquiv_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  Function.Injective fun f => f.toPartialEquiv
-- Mathlib.Algebra.Order.ToIntervalMod
AddCommGroup.modEq_iff_toIcoMod_ne_toIocMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α}, a ≡ b [PMOD p] ↔ toIcoMod hp a b ≠ toIocMod hp a b
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalGroup.ext_iff : ∀ {G : Type u_1} [inst : Group G] {t t' : TopologicalSpace G},
  IsTopologicalGroup G → IsTopologicalGroup G → (t = t' ↔ nhds 1 = nhds 1)
-- Init.Data.List.Count
List.countP_flatMap : ∀ {α : Type u_2} {β : Type u_1} {p : β → Bool} {l : List α} {f : α → List β},
  List.countP p (List.flatMap f l) = (List.map (List.countP p ∘ f) l).sum
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv_transpose_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (j : n),
  ((LinearMap.toMatrixAlgEquiv v₁) f).transpose j = ⇑(v₁.repr (f (v₁ j)))
-- Batteries.Data.List.Lemmas
List.Sublist.diff_right : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ l₃ : List α}, l₁.Sublist l₂ → (l₁.diff l₃).Sublist (l₂.diff l₃)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₁ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.Algebra.GCDMonoid.Basic
dvd_normalize_iff : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] {a b : α}, a ∣ normalize b ↔ a ∣ b
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.tuesday.sizeOf_spec : sizeOf Std.Time.Weekday.tuesday = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.any_eq_false_iff_forall_mem_get : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {p : (a : α) → β a → Bool}, m.WF → (m.any p = false ↔ ∀ (a : α) (h : a ∈ m), p a (m.get a h) = false)
-- Std.Async.TCP
/-- Represents a TCP client socket, used to connect to a server.
 -/
Std.Async.TCP.Socket.Client : Type
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.coe_refl : ∀ {R : Type u_2} {A : Type u_3} [inst : Add A] [inst_1 : Mul A] [inst_2 : SMul R A] [inst_3 : Star A],
  ⇑(StarAlgEquiv.refl R A) = id
-- Mathlib.Data.Part
Part.toOption_eq_none_iff : ∀ {α : Type u_1} {a : Part α} [inst : Decidable a.Dom], a.toOption = none ↔ ¬a.Dom
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
CategoryTheory.Preadditive.epi_iff_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [(CategoryTheory.forget₂ C Ab).PreservesHomology]
  [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔
    Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map f))
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
CategoryTheory.ExponentialIdeal.exp_closed : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₁, u₂} D}
  {i : CategoryTheory.Functor D C} {inst_2 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_3 : CategoryTheory.MonoidalClosed C} [self : CategoryTheory.ExponentialIdeal i] {B : C},
  i.essImage B → ∀ (A : C), i.essImage (A ⟹ B)
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.tfaeHaveEqnsDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Elab.ElabRules
Lean.Elab.Command.elabElab : Lean.Elab.Command.CommandElab
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_ofFin : ∀ (n : Fin UInt32.size), (UInt32.ofFin n).toBitVec = { toFin := n }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.inter_congr : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ m₄ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ ∩ m₂).Equiv (m₃ ∩ m₄)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false → (Std.DHashMap.Raw.Const.insertMany m l).getKey? k = m.getKey? k
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Submodule.span_range_natDegree_eq_adjoin : ∀ {R : Type u_6} {A : Type u_7} [inst : CommRing R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {x : A}
  {f : Polynomial R},
  f.Monic →
    (Polynomial.aeval x) f = 0 →
      Submodule.span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree)) = Subalgebra.toSubmodule R[x]
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Extract and remove the minimum element from the tree, if it exists.

```
split_min {1, 2, 3} = some (1, {2, 3})
split_min ∅ = none
```  -/
Ordnode.splitMin : {α : Type u_1} → Ordnode α → Option (α × Ordnode α)
-- Mathlib.Algebra.Field.Defs
/-- The default definition of the coercion `ℚ → K` for a division ring `K`.

`↑q : K` is defined as `(q.num : K) / (q.den : K)`.

Do not use this directly (instances of `DivisionRing` are allowed to override that default for
better definitional properties). Instead, use the coercion.  -/
Rat.castRec : {K : Type u_1} → [NatCast K] → [IntCast K] → [Div K] → ℚ → K
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_4.splitter : (motive : Lean.Grind.CommRing.Expr → Sort u_1) →
  (x : Lean.Grind.CommRing.Expr) →
    ((k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k)) →
      ((k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k)) →
        ((k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)) →
          ((x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x)) →
            ((a b : Lean.Grind.CommRing.Expr) → motive (a.add b)) →
              ((a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) →
                ((a : Lean.Grind.CommRing.Expr) → motive a.neg) →
                  ((a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) →
                    ((a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) → motive x
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.opcyclesMap.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') (n : ℤ),
  X.opcyclesMap f g f' g' α n =
    X.descOpcycles f g (n - 1) n ⋯
      (CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.homMk₁ (α.app 0) (α.app 1) ⋯))
        (X.pOpcycles f' g' n))
      ⋯
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesOpIso_hom_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology]
  {Z : Cᵒᵖ} (h : Opposite.op S₁.cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap (CategoryTheory.ShortComplex.opMap φ))
      (CategoryTheory.CategoryStruct.comp S₁.opcyclesOpIso.hom h) =
    CategoryTheory.CategoryStruct.comp S₂.opcyclesOpIso.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ).op h)
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.String.Slice.find?.match_1.eq_1 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.SearchStep s → Sort u_1) (startPos endPos : s.Pos)
  (h_1 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched startPos endPos))
  (h_2 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.rejected startPos endPos)),
  (match String.Slice.Pattern.SearchStep.matched startPos endPos with
    | String.Slice.Pattern.SearchStep.matched startPos endPos => h_1 startPos endPos
    | String.Slice.Pattern.SearchStep.rejected startPos endPos => h_2 startPos endPos) =
    h_1 startPos endPos
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.instPartialOrderContinuousHom : {α : Type u_2} →
  {β : Type u_3} → [inst : OmegaCompletePartialOrder α] → [inst_1 : OmegaCompletePartialOrder β] → PartialOrder (α →𝒄 β)
-- Mathlib.Algebra.Algebra.Basic
/-- A special case of `eq_intCast'` that happens to be true definitionally  -/
algebraMap_int_eq : ∀ (R : Type u_1) [inst : Ring R], algebraMap ℤ R = Int.castRingHom R
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Functor.mapZeroObject.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroObject D]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.PreservesZeroMorphisms], F.mapZeroObject = F.mapZeroObject
-- Init.Data.Dyadic.Inv
/-- Inverts a dyadic number at a given (maximum) precision.
Returns the greatest dyadic number with precision at most `prec` which is less than or equal to `1/x`.
For `x = 0`, returns `0`.

This agrees with `divAtPrec 1 x prec` (see `invAtPrec_eq_divAtPrec_one`), but is kept as a
separate definition to avoid the unnecessary `1 *`-by-numerator step in `Rat`'s division at
runtime.
 -/
Dyadic.invAtPrec : Dyadic → ℤ → Dyadic