mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α}
  {fallback : β}, t.contains a = false → t.getD a fallback = fallback
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.Total.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type u_1} {I : J → Type u_2}
  {inst_1 : CategoryTheory.Category.{v_1, u_1} J} {inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)}
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {k l : CategoryTheory.Limits.ColimitPresentation.Total P} {x y : k.Hom l}, x.base = y.base → x.hom = y.hom → x = y
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instModule : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    {S : Type u_4} →
                      [inst_7 : Semiring S] →
                        [inst_8 : Module S M] →
                          [SMulCommClass R S M] →
                            [LieDerivation.SMulBracketCommClass S L M] → Module S (LieDerivation R L M)
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instSmallOppositeOp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.ObjectProperty.Small.{w, v, u} P], CategoryTheory.ObjectProperty.Small.{w, v, u} P.op
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsMatch.exists_isLongestMatch : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsMatch pat pos → ∃ pos', String.Slice.Pattern.Model.IsLongestMatch pat pos'
-- Mathlib.SetTheory.ZFC.PSet
/-- The pre-set powerset operator  -/
PSet.powerset : PSet.{u_1} → PSet.{u_1}
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.quasiIsoAt_πTruncGE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] {j : ι} {j' : ι'}, e.f j = j' → QuasiIsoAt (K.πTruncGE e) j'
-- Mathlib.Analysis.Calculus.DiffContOnCl
/-- A predicate saying that a function is differentiable on a set and is continuous on its
closure. This is a common assumption in complex analysis.  -/
DiffContOnCl : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedAddCommGroup F] → [NormedSpace 𝕜 E] → [NormedSpace 𝕜 F] → (E → F) → Set E → Prop
-- Mathlib.RingTheory.Regular.ProjectiveDimension
ModuleCat.projectiveDimension_quotient_eq_length : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsLocalRing R] [IsNoetherianRing R] (rs : List R),
  RingTheory.Sequence.IsRegular R rs →
    CategoryTheory.projectiveDimension (ModuleCat.of R (Shrink.{v, u} (R ⧸ Ideal.ofList rs))) = ↑rs.length
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.disjoint_boxes_of_disjoint_iUnion : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I},
  Disjoint π₁.iUnion π₂.iUnion → Disjoint π₁.boxes π₂.boxes
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_commute_left : ∀ (R : Type u_1) [inst : Semiring R] (p : Polynomial R) {S : Type u_2} [inst_1 : Semiring S] [inst_2 : Module R S]
  [IsScalarTower R S S] [SMulCommClass R S S] {x y : S}, Commute x y → Commute (p.smeval x) y
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- The underlying list  -/
DyckWord.toList : DyckWord → List DyckStep
-- Mathlib.Data.ENNReal.Inv
ENNReal.toReal_div : ∀ (a b : ENNReal), (a / b).toReal = a.toReal / b.toReal
-- Mathlib.Data.Vector.Basic
List.Vector.toList_injective : ∀ {α : Type u_1} {n : ℕ}, Function.Injective List.Vector.toList
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.comap_iInf : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β]
  (f : BoundedLatticeHom α β) (L : ι → BooleanSubalgebra β),
  BooleanSubalgebra.comap f (⨅ i, L i) = ⨅ i, BooleanSubalgebra.comap f (L i)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_le_card_sub_left : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] {s t : Finset α}, s.Nonempty → t.card ≤ (s - t).card
-- Mathlib.Order.Filter.Basic
Filter.not_frequently : ∀ {α : Type u} {p : α → Prop} {f : Filter α}, (¬∃ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, ¬p x
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.toFunctor_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) {Y : C} (f : Y ⟶ X)
  (hf : S.arrows f) (Z : Cᵒᵖ),
  (S.toFunctor f hf).app Z = TypeCat.ofHom fun g => ⟨CategoryTheory.CategoryStruct.comp g f, ⋯⟩
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovary_inv_left₀`. -/
Monovary.of_inv_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {f : ι → α} {g : ι → β}, StrongLT 0 f → Monovary f⁻¹ g → Antivary f g
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {ι : Type t}
  {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S},
  CategoryTheory.Sieve.ofArrows X' f' ∈ J S →
    ∀ (i : ι),
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve✝ f f' i ∈
        (J.over (X i)) (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (X i)))
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset : ∀ {A B : GrpCat} (f : A ⟶ B),
  (GrpCat.SurjectiveOfEpiAuxs.tau f)
      (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(GrpCat.Hom.hom f).range, ⋯⟩) =
    GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₁₂.τ₂ = CategoryTheory.kernelCokernelCompSequence.φ f g
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.coeff_reverse : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R) (n : ℕ),
  f.reverse.coeff n = f.coeff ((Polynomial.revAt f.natDegree) n)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Rotating left by a constant value.
 -/
Std.Tactic.BVDecide.BVUnOp.rotateLeft : ℕ → Std.Tactic.BVDecide.BVUnOp
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.Forall.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) →
      (Unit → motive []) →
        ((x : α) → motive [x]) → ((x : α) → (l : List α) → (l = [] → False) → motive (x :: l)) → motive x
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Two morphisms are equal if there is a fork whose inclusion is epi.  -/
CategoryTheory.Limits.eq_of_epi_fork_ι : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g)
  [CategoryTheory.Epi t.ι], f = g
-- Mathlib.Order.Basic
eq_of_le_of_not_lt' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, b ≤ a → ¬b < a → a = b
-- Mathlib.Analysis.Calculus.ContDiff.Comp
Continuous.fderiv_one : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F → G} {g : E → F},
  ContDiff 𝕜 1 (Function.uncurry f) → Continuous g → Continuous fun x => fderiv 𝕜 (f x) (g x)
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.dvd_total : ∀ {R : Type u_1} [inst : Semigroup R] [h : PreValuationRing R] (x y : R), x ∣ y ∨ y ∣ x
-- Mathlib.Probability.Distributions.Beta
ProbabilityTheory.beta_pos : ∀ {α β : ℝ}, 0 < α → 0 < β → 0 < ProbabilityTheory.beta α β
-- Mathlib.Data.FunLike.Group
FunLike.addCancelCommMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Zero F]
  [inst_3 : SMul ℕ F] [inst_4 : AddCancelCommMonoid β] [inst_5 : IsZeroApply F α β] [inst_6 : IsAddApply F α β]
  [inst_7 : IsSMulApply ℕ F α β],
  FunLike.addCancelCommMonoid = Function.Injective.addCancelCommMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_eq_one_of : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω},
  s.Finite → s.Nonempty → s ⊆ t → (ProbabilityTheory.uniformOn s) t = 1
-- Init.Data.String.PosRaw
String.Pos.Raw.add_eq : ∀ {p₁ p₂ : String.Pos.Raw}, p₂.offsetBy p₁ = { byteIdx := p₁.byteIdx + p₂.byteIdx }
-- Init.Data.SInt.Lemmas
Int32.toInt_le_iSizeMaxValue : ∀ (x : Int32), x.toInt ≤ ISize.maxValue.toInt
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.ball_iInter : ∀ {β : Type ub} {ι : Sort u_1} {x : β} {V : ι → Set (β × β)},
  UniformSpace.ball x (⋂ i, V i) = ⋂ i, UniformSpace.ball x (V i)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.preimage_closure : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂),
  ⇑e ⁻¹' closure s = closure (⇑e ⁻¹' s)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.union.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m₁ m₁_1 : Std.ExtHashMap α β),
  m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.ExtHashMap α β), m₂ = m₂_1 → m₁.union m₂ = m₁_1.union m₂_1
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.isBasis_setOfPred_insert_isBasis : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → M.IsBasis I {x | M.IsBasis I (insert x I)}
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- The expression for the underlying category.  -/
Mathlib.Tactic.Bicategory.Context.B : (self : Mathlib.Tactic.Bicategory.Context) → Q(Type udummy._pp_uniq.3)
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_3.eq_4 : ∀ {σ : String.Slice → Type} [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  {s : String.Slice} (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) (motive : searcher.Step → Sort u_1)
  (property : searcher.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos endPos : s.Pos) →
        (hps :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos))) →
          ⟨Std.IterStep.done, property⟩ =
              ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ →
            motive ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩)
  (h_2 :
    (searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos endPos : s.Pos) →
        (hps :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos))) →
          ⟨Std.IterStep.done, property⟩ =
              ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ →
            motive ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩)
  (h_3 :
    (searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (hps : searcher.IsPlausibleStep (Std.IterStep.skip searcher')) →
        ⟨Std.IterStep.done, property⟩ = ⟨Std.IterStep.skip searcher', hps⟩ → motive ⟨Std.IterStep.skip searcher', hps⟩)
  (h_4 :
    (property_1 : searcher.IsPlausibleStep Std.IterStep.done) →
      ⟨Std.IterStep.done, property⟩ = ⟨Std.IterStep.done, property_1⟩ → motive ⟨Std.IterStep.done, property_1⟩),
  (match h : ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ =>
      h_1 searcher' startPos endPos hps h
    | ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ =>
      h_2 searcher' startPos endPos hps h
    | ⟨Std.IterStep.skip searcher', hps⟩ => h_3 searcher' hps h
    | ⟨Std.IterStep.done, property_1⟩ => h_4 property_1 h) =
    h_4 property ⋯
-- Mathlib.RingTheory.Int.Basic
Int.instDecidablePredIrreducible : DecidablePred Irreducible
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.order.eq_1 : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (f : MvPowerSeries σ R),
  f.order = MvPowerSeries.weightedOrder (fun x => 1) f
-- Mathlib.LinearAlgebra.Orientation
/-- If the index type has cardinality equal to the finite dimension, a basis with the given
orientation.  -/
Orientation.someBasis : {R : Type u_1} →
  [inst : Field R] →
    [inst_1 : LinearOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} →
          [inst_3 : AddCommGroup M] →
            [inst_4 : Module R M] →
              {ι : Type u_3} →
                [inst_5 : Fintype ι] →
                  [Nonempty ι] →
                    [DecidableEq ι] →
                      [FiniteDimensional R M] →
                        Orientation R M ι → Fintype.card ι = Module.finrank R M → Module.Basis ι R M
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.destruct.match_1.eq_3 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Option α)) → Sort u_2) (a : α) (s' : Stream'.Seq (Option α))
  (h_1 : Unit → motive none) (h_2 : (s' : Stream'.Seq (Option α)) → motive (some (none, s')))
  (h_3 : (a : α) → (s' : Stream'.Seq (Option α)) → motive (some (some a, s'))),
  (match some (some a, s') with
    | none => h_1 ()
    | some (none, s') => h_2 s'
    | some (some a, s') => h_3 a s') =
    h_3 a s'
-- Mathlib.NumberTheory.RamificationInertia.Galois
/-- If `L / K` is a Galois extension, it can be seen from the theorem
`Ideal.ramificationIdx_eq_of_isGaloisGroup` that all `Ideal.ramificationIdx` over a fixed
maximal ideal `p` of `A` are the same, which we define as `Ideal.ramificationIdxIn`.  -/
Ideal.ramificationIdxIn : {A : Type u_1} → [inst : CommRing A] → Ideal A → (B : Type u_2) → [inst_1 : CommRing B] → [Algebra A B] → ℕ
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.refineOneHypercover_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (E : CategoryTheory.PreZeroHypercover X)
  [inst_1 : E.HasPullbacks]
  (F : (i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))),
  (E.refineOneHypercover F).toPreZeroHypercover = E
-- Mathlib.Topology.Separation.Hausdorff
instT2SpaceOfR1SpaceOfT0Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] [T0Space X], T2Space X
-- Mathlib.Topology.Connected.PathConnected
Joined.listProd : ∀ {M : Type u_4} [inst : MulOneClass M] [inst_1 : TopologicalSpace M] [ContinuousMul M] {l l' : List M},
  List.Forall₂ Joined l l' → Joined l.prod l'.prod
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairRight_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (Fₗ : CategoryTheory.Functor C E) (Fᵣ : CategoryTheory.Functor D E')
  (X : D),
  (CategoryTheory.Join.mapPairRight Fₗ Fᵣ).hom.app X =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right (Fᵣ.obj X))
-- Mathlib.Algebra.Ring.Defs
NonAssocCommSemiring.toNonAssocSemiring : {α : Type u} → [self : NonAssocCommSemiring α] → NonAssocSemiring α
-- Std.Data.DHashMap.Lemmas
_private.Std.Data.DHashMap.Lemmas.0.Std.DHashMap.insertIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} (m : Std.DHashMap α β) (a : α) (b : β a),
  m.insertIfNew a b = { inner := ↑(Std.DHashMap.Internal.Raw₀.insertIfNew ⟨m.inner, ⋯⟩ a b), wf := ⋯ }
-- Init.Data.Float.Model.Unpacked.Operations.Compare
/-- Determines whether `a` is less than or equal to `b` according to IEEE rules.

This is not a total ordering, and `≤` is not reflexive.
 -/
Float.Model.UnpackedFloat.le : Float.Model.UnpackedFloat → Float.Model.UnpackedFloat → Bool
-- Init.Data.String.Subslice
String.Slice.Subslice.copy_eq : ∀ {s : String.Slice}, String.Slice.Subslice.copy = String.Slice.copy ∘ String.Slice.Subslice.toSlice
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a fallback : α},
  (t.erase k).getKeyD a fallback = if cmp k a = Ordering.eq then fallback else t.getKeyD a fallback
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- State for each algebraic structure by this module.
Each type must at least implement the instance `IntModule`.
For being able to process inequalities, it must at least implement `Preorder`, and `OrderedAdd`
 -/
Lean.Meta.Grind.Arith.Linear.Struct : Type
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.norm_coeff_le_choose_mul_mahlerMeasure : ∀ (n : ℕ) (p : Polynomial ℂ), ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mahlerMeasure
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
lt_of_mul_lt_mul_of_nonpos_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b c : R} [ExistsAddOfLE R] [MulPosMono R]
  [AddRightMono R] [AddRightReflectLE R], a * c < b * c → c ≤ 0 → b < a
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ιMulti_mul_ιMulti : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m n : ℕ}
  (a : Fin m → M) (b : Fin n → M),
  (ExteriorAlgebra.ιMulti R m) a * (ExteriorAlgebra.ιMulti R n) b = (ExteriorAlgebra.ιMulti R (m + n)) (Fin.append a b)
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.bind_diag_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w}
  [inst_1 : CategoryTheory.SmallCategory J] [inst_2 : (j : J) → CategoryTheory.SmallCategory (I j)] {X : C}
  (P : CategoryTheory.Limits.ColimitPresentation J X)
  (Q : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (P.diag.obj j))
  [inst_3 : ∀ (j : J), CategoryTheory.IsFiltered (I j)]
  [inst_4 : ∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((Q j).diag.obj i)]
  {k l : CategoryTheory.Limits.ColimitPresentation.Total Q} (f : k ⟶ l), (P.bind Q).diag.map f = f.hom
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
/-- The property that there exists a universal derivation for
a morphism of presheaves of commutative rings `S ⟶ F.op ⋙ R`.  -/
PresheafOfModules.HasDifferentials : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
          {F : CategoryTheory.Functor C D} → {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} → (S ⟶ F.op.comp R) → Prop
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
AddSubgroup.tendsto_coe_cofinite_of_discrete : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G]
  (H : AddSubgroup G), IsDiscrete ↑H → Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact G)
-- Mathlib.CategoryTheory.Localization.Predicate
/-- When `W` consists of isomorphisms, the identity satisfies the universal property
of the localization.  -/
CategoryTheory.Localization.strictUniversalPropertyFixedTargetId : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (E : Type u_3) →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} E] →
          W ≤ CategoryTheory.MorphismProperty.isomorphisms C →
            CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (CategoryTheory.Functor.id C) W E
-- Mathlib.Algebra.Group.Submonoid.Support
/-- The support of a submonoid `M` of a group `G` is `M ∩ -M`,
the largest subgroup of `G` contained in `M`.  -/
AddSubmonoid.support : {G : Type u_1} → [inst : AddGroup G] → AddSubmonoid G → AddSubgroup G
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
/-- **Alias** of `Ideal.Fiber.algEquivQuotient`.

---

`p.Fiber S` is isomorphic to the quotient `Sₚ ⧸ pSₚ`.  -/
Fiber.algEquivQuotient : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (p : Ideal R) →
            [inst_3 : p.IsPrime] →
              p.Fiber S ≃ₐ[S]
                Localization (Algebra.algebraMapSubmonoid S p.primeCompl) ⧸
                  Ideal.map
                    (algebraMap (Localization p.primeCompl) (Localization (Algebra.algebraMapSubmonoid S p.primeCompl)))
                    (IsLocalRing.maximalIdeal (Localization p.primeCompl))
-- Mathlib.Tactic.DefEqAbuse
/-- Check whether a rendered isDefEq check string has syntactically identical LHS and RHS
(e.g. `"⊤ =?= ⊤"` or `"Quiver C =?= Quiver C"`).
Comparison is whitespace-insensitive to handle cases where LHS and RHS are semantically identical
but rendered with different line breaks or spacing.
TODO: once https://github.com/leanprover/lean4/pull/12698 is available, refactor to use
`TraceData.result?` and compare the LHS/RHS `Expr`s structurally instead of string-matching.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Mathlib.Tactic.DefEqAbuse.isIdenticalSidesStr : String → Bool
-- Std.Http.Data.URI.Basic
/-- Replaces all query parameters. Keys and values will be automatically percent-encoded when building.
 -/
Std.Http.URI.Builder.setQuery : Std.Http.URI.Builder → Array (String × Option String) → Std.Http.URI.Builder
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.π_homologyIsoSc'_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology] {Z : C} (h : K.homology j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyπ
      (CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).inv h) =
    CategoryTheory.CategoryStruct.comp (K.cyclesIsoSc' i j k hi hk).inv
      (CategoryTheory.CategoryStruct.comp (K.homologyπ j) h)
-- Batteries.Tactic.Congr
Batteries.Tactic.Congr.Config.mk.injEq : ∀ (closePre closePost closePre_1 closePost_1 : Bool),
  ({ closePre := closePre, closePost := closePost } = { closePre := closePre_1, closePost := closePost_1 }) =
    (closePre = closePre_1 ∧ closePost = closePost_1)