mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Closed
/-- The closure of a sieve is closed.  -/
CategoryTheory.GrothendieckTopology.close_isClosed : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
  (S : CategoryTheory.Sieve X), J₁.IsClosed (J₁.close S)
-- Mathlib.Algebra.Algebra.Operations
Submodule.instSMulCommClass_1 : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {α : Type u_1}
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α A] [inst_5 : SMulCommClass α R A] [SMulCommClass A α A],
  SMulCommClass (Submodule R A) α (Submodule R A)
-- Mathlib.GroupTheory.Torsion
AddCommMonoid.Torsion.ofTorsion.eq_1 : ∀ (G : Type u_1) [inst : AddCommMonoid G], AddCommMonoid.Torsion.ofTorsion G = ⋯.torsionAddEquiv
-- Mathlib.Algebra.Star.StarAlgHom
/-- Interpret a ⋆-algebra equivalence as an algebra equivalence.  -/
StarAlgEquiv.toAlgEquiv : {R : Type u_6} →
  {A : Type u_7} →
    {B : Type u_8} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] → [inst_5 : Star A] → [inst_6 : Star B] → (A ≃⋆ₐ[R] B) → A ≃ₐ[R] B
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- A local hypothesis.
When `contextual := true` is enabled, this fvar may exist in an extension
of the current local context; it will not be used for rewriting by simp once
it is out of scope but it may end up in the `usedSimps` trace.
 -/
Lean.Meta.Origin.fvar : Lean.FVarId → Lean.Meta.Origin
-- Mathlib.Order.Basic
/-- If a linear order has no elements `x < y < z`, then it has at most two elements.  -/
eq_or_eq_or_eq_of_forall_not_lt_lt : ∀ {α : Type u_2} [inst : LinearOrder α], (∀ ⦃x y z : α⦄, x < y → y < z → False) → ∀ (x y z : α), x = y ∨ y = z ∨ x = z
-- Mathlib.Computability.Partrec
Nat.Partrec.right : Nat.Partrec ↑fun n => (Nat.unpair n).2
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.valueGroupOrderIso₀_restrict : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : Ring R] (v : Valuation R Γ₀)
  (b : WithVal v), (WithVal.valueGroupOrderIso₀ v) ((WithVal.valuation v).restrict b) = v.restrict b.ofVal
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod.denote_go_eq_divRec_r : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (assign : α → Bool) (curr : ℕ)
  (lhs rhs rbv qbv : BitVec w) (n d q r : aig.RefVec w) (wn wr : ℕ),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
      (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
        (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
          ∀ (idx : ℕ) (hidx : idx < w),
            ⟦assign,
                { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr n d wn wr q r).aig,
                  ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr n d wn wr q r).r.get idx hidx }⟧ =
              (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).r.getLsbD idx
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.HasCardinalFilteredGenerator.mk : ∀ {C : Type u} [hC : CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
  [toLocallySmall : CategoryTheory.LocallySmall.{w, v, u} C],
  (∃ P, ∃ (_ : CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P), P.IsCardinalFilteredGenerator κ) →
    CategoryTheory.HasCardinalFilteredGenerator C κ
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Construct an isomorphism in the over category given isomorphisms of the objects whose forward
direction gives a commutative triangle.
 -/
CategoryTheory.Under.isoMk : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} →
      {f g : CategoryTheory.Under X} →
        (hr : f.right ≅ g.right) →
          autoParam (CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom) CategoryTheory.Under.isoMk._auto_1 →
            (f ≅ g)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_eraseₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {a : α},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑(m.eraseₘ a)).buckets).Perm
      (Std.Internal.List.eraseKey a (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Analysis.RCLike.Basic
/-- only an instance in the `ComplexOrder` scope  -/
RCLike.toPartialOrder : {K : semiOutParam (Type u_1)} → [self : RCLike K] → PartialOrder K
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.LocallyOfFiniteType f]
  [AlgebraicGeometry.IsSeparated f] {x : ↥X} {s : ↥S},
  f x = s →
    AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x →
      ∃ U g,
        AlgebraicGeometry.Etale g ∧
          s ∈ Set.range ⇑g ∧
            ∃ V W v,
              IsCompl V W ∧
                AlgebraicGeometry.IsFinite
                    (CategoryTheory.CategoryStruct.comp V.ι (CategoryTheory.Limits.pullback.snd f g)) ∧
                  (CategoryTheory.Limits.pullback.fst f g) ↑v = x
-- Mathlib.Order.Hom.Lattice
LatticeHom.toInfHom : {α : Type u_6} → {β : Type u_7} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom α β → InfHom α β
-- Mathlib.Topology.MetricSpace.Isometry
/-- An isometry (also known as isometric embedding) is a map preserving the edistance
between pseudoemetric spaces, or equivalently the distance between pseudometric space.  -/
Isometry : {α : Type u} → {β : Type v} → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → (α → β) → Prop
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.State.mk.sizeOf_spec : ∀ (cache : Lean.PersistentExprMap Mathlib.Tactic.BicategoryLike.Mor₁), sizeOf { cache := cache } = 1 + sizeOf cache
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_diff_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ((m₁ \ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∈ m₂)
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.hasBinaryBiproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.Limits.HasBinaryBiproducts C
-- Mathlib.Data.NNReal.Defs
NNReal.coe_lt_one : ∀ {r : NNReal}, ↑r < 1 ↔ r < 1
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coreflection_same : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι) (x : N),
  (P.coreflection i) ((P.coreflection i) x) = x
-- Lean.Server.InfoUtils
_private.Lean.Server.InfoUtils.0.Lean.Elab.Info.fmtHover?.fmtTermAndModule? : Lean.Elab.Info → Lean.MetaM (Option Lean.FormatWithInfos × Option Std.Format)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.instIsOverCompHomOfIsOver : ∀ {X Y Z S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] [inst_2 : Z.Over S] (f : X.RationalMap Y)
  (g : Y ⟶ Z) [AlgebraicGeometry.Scheme.RationalMap.IsOver S f] [AlgebraicGeometry.Scheme.Hom.IsOver g S],
  AlgebraicGeometry.Scheme.RationalMap.IsOver S (f.compHom g)
-- Qq.Macro
Qq.Impl.determineLocalInstances : Lean.LocalContext → Lean.MetaM Lean.LocalInstances
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.eq_unit_comp_map_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : C} {B : D} (f : F.obj A ⟶ B)
  (g : A ⟶ G.obj B),
  g = CategoryTheory.CategoryStruct.comp (adj.unit.app A) (G.map f) ↔
    CategoryTheory.CategoryStruct.comp (F.map g) (adj.counit.app B) = f
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.neg.injEq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (a a_1 : RingCat.Colimits.Prequotient F), (a.neg = a_1.neg) = (a = a_1)
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.normThreshold_add_one : ∀ {a : ℝ} (n : ℕ),
  ProbabilityTheory.Fernique.normThreshold a (n + 1) = √2 * ProbabilityTheory.Fernique.normThreshold a n + a
-- Mathlib.Order.RelSeries
not_infiniteDimensionalOrder_iff : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α], ¬InfiniteDimensionalOrder α ↔ FiniteDimensionalOrder α
-- Mathlib.Topology.Maps.Proper.UniversallyClosed
/-- A map `f : X → Y` is proper if and only if it is continuous and the map
`(Prod.map f id : X × Ultrafilter X → Y × Ultrafilter X)` is closed. This is stronger than
`isProperMap_iff_universally_closed` since it shows that there's only one space to check to get
properness, but in most cases it doesn't matter.  -/
isProperMap_iff_isClosedMap_ultrafilter : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instMonadBacktrackSavedStateGrindTacticM : Lean.MonadBacktrack Lean.Elab.Tactic.Grind.SavedState Lean.Elab.Tactic.Grind.GrindTacticM
-- Mathlib.Data.PFunctor.Univariate.M
/-- select a subtree using an `i : F.Idx` or return an arbitrary tree if
`i` designates no subtree of `x`  -/
PFunctor.M.ichildren : {F : PFunctor.{uA, uB}} → [Inhabited F.M] → [DecidableEq F.A] → F.Idx → F.M → F.M
-- Mathlib.RingTheory.Localization.Away.Lemmas
/-- Given a set `s` in a ring `R` and for every `t : s` a set `p t` of fractions in
a localization of `R` at `t`, this is the function sending a pair `(t, y)`, with
`t : s` and `y : t a`, to `t` multiplied with a numerator of `y`. The range
of this function spans the unit ideal, if `s` and every `p t` do.  -/
IsLocalization.Away.mulNumerator : {R : Type u_1} →
  [inst : CommRing R] →
    (s : Set R) →
      {Rₜ : ↑s → Type u_2} →
        [inst_1 : (t : ↑s) → CommRing (Rₜ t)] →
          [inst_2 : (t : ↑s) → Algebra R (Rₜ t)] →
            [∀ (t : ↑s), IsLocalization.Away (↑t) (Rₜ t)] → (p : (t : ↑s) → Set (Rₜ t)) → (t : ↑s) × ↑(p t) → R
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.rightUnitor_δ : ∀ {G : Type v} [inst : Monoid G] {k : Type u} [inst_1 : CommSemiring k] (X : Action (Type u) G),
  ↑(Representation.TensorProduct.rid k (Representation.linearize k G X)).symm =
    ((Representation.IntertwiningMap.lTensor (Representation.linearize k G X)
              (Representation.LinearizeMonoidal.η k G)).comp
          (Representation.LinearizeMonoidal.δ X
            (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G)))).comp
      (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)
-- Mathlib.NumberTheory.LSeries.Convolution
LSeries.convolution.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (f g : ℕ → R),
  LSeries.convolution f g = ⇑(toArithmeticFunction f * toArithmeticFunction g)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffAt.fun_comp : ∀ {𝕜 : 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 : F → G} {n : WithTop ℕ∞} (x : E),
  ContDiffAt 𝕜 n g (f x) → ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n (fun x => g (f x)) x
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sigma_isBase_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {M : (i : ι) → Matroid (α i)} {B : Set ((i : ι) × α i)},
  (Matroid.sigma M).IsBase B ↔ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_insert_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.insert k v).size ≤ m.size + 1
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- In "English notation", a Young diagram is drawn so that (i1, j1) ≤ (i2, j2)
means (i1, j1) is weakly up-and-left of (i2, j2).  -/
YoungDiagram.up_left_mem : ∀ (μ : YoungDiagram) {i1 i2 j1 j2 : ℕ}, i1 ≤ i2 → j1 ≤ j2 → (i2, j2) ∈ μ → (i1, j1) ∈ μ
-- Mathlib.Analysis.Real.Cardinality
/-- The cardinality of the interval $[a, b]$.  -/
Cardinal.mk_Icc_real : ∀ {a b : ℝ}, a < b → Cardinal.mk ↑(Set.Icc a b) = Cardinal.continuum
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.step_intermediateDropWhile.match_3.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    {it : Std.Iter β} →
      (motive : it.Step → Sort u_2) →
        (x : it.Step) →
          ((it' : Std.Iter β) →
              (out : β) →
                (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
            ((it' : Std.Iter β) →
                (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
              ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.toPerfPair_flip_comp_coroot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  ⇑P.flip.toPerfPair ∘ ⇑P.coroot = P.coroot'
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.le_equalizer_of_isDPMorphism : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {B : Type u_2} [inst_1 : CommSemiring B]
  (f : A →+* B) {K : Ideal B},
  Ideal.map f I ≤ K →
    ∀ (hK hK' : DividedPowers K), hI.IsDPMorphism hK f → hI.IsDPMorphism hK' f → Ideal.map f I ≤ hK.dpEqualizer hK'
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.instSemilatticeInf.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : SemilatticeInf β] [inst_3 : OrderTop β],
  InfTopHom.instSemilatticeInf = Function.Injective.semilatticeInf DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {X Y : CategoryTheory.Grothendieck F} →
        (base : X.base ⟶ Y.base) → ((F.map base).toFunctor.obj X.fiber ⟶ Y.fiber) → X.Hom Y
-- Init.Grind.Offset
Lean.Grind.Nat.ro_eq_true_of_le : ∀ (u v k : ℕ), u ≤ v → (u ≤ v + k) = True
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
/-- A continuous function with compact support belongs to `L^∞`.
See `Continuous.memLp_of_hasCompactSupport` for a version for `L^p`.  -/
Continuous.memLp_top_of_hasCompactSupport : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] {X : Type u_7} [inst_1 : TopologicalSpace X] [inst_2 : MeasurableSpace X]
  [OpensMeasurableSpace X] {f : X → E},
  Continuous f → HasCompactSupport f → ∀ (μ : MeasureTheory.Measure X), MeasureTheory.MemLp f ⊤ μ
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t_inv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j : D.J)
  {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_1 : CategoryTheory.ConcreteCategory C F] (x : carrier (D.V (i, j))),
  (CategoryTheory.ConcreteCategory.hom (D.t j i)) ((CategoryTheory.ConcreteCategory.hom (D.t i j)) x) = x
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.findInterpDecl : Lean.Environment → Lean.Name → Option Lean.IR.Decl
-- Mathlib.ModelTheory.Bundled
/-- A type bundled with the structure induced by an equivalence.  -/
Equiv.bundledInduced : (L : FirstOrder.Language) → {M : Type w} → [L.Structure M] → {N : Type w'} → M ≃ N → CategoryTheory.Bundled L.Structure
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.combine.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Sort u_1) (p₁ p₂ : Lean.Grind.Linarith.Poly)
  (h_1 : (p₂ : Lean.Grind.Linarith.Poly) → motive Lean.Grind.Linarith.Poly.nil p₂)
  (h_2 : (p₁ : Lean.Grind.Linarith.Poly) → motive p₁ Lean.Grind.Linarith.Poly.nil)
  (h_3 :
    (a₁ : ℤ) →
      (x₁ : Lean.Grind.Linarith.Var) →
        (p₁ : Lean.Grind.Linarith.Poly) →
          (a₂ : ℤ) →
            (x₂ : Lean.Grind.Linarith.Var) →
              (p₂ : Lean.Grind.Linarith.Poly) →
                motive (Lean.Grind.Linarith.Poly.add a₁ x₁ p₁) (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂))
  (p₁_1 : Lean.Grind.Linarith.Poly),
  p₁ = p₁_1 →
    p₂ = Lean.Grind.Linarith.Poly.nil →
      (p₁_1 = Lean.Grind.Linarith.Poly.nil → False) →
        (match p₁, p₂ with
          | Lean.Grind.Linarith.Poly.nil, p₂ => h_1 p₂
          | p₁, Lean.Grind.Linarith.Poly.nil => h_2 p₁
          | Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂ => h_3 a₁ x₁ p₁ a₂ x₂ p₂) ≍
          h_2 p₁_1
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.findEntryAux : {α : Type u_1} → {β : Type u_2} → [BEq α] → Lean.PersistentHashMap.Node α β → USize → α → Option (α × β)
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
min_le_mul_of_one_le_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : MulOneClass α] [MulRightMono α] {a b : α}, 1 ≤ a → min a b ≤ a * b
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- The inf of two non-unital subsemirings is their intersection.  -/
NonUnitalSubsemiring.instMin : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → Min (NonUnitalSubsemiring R)
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `none` if the
map is empty.
 -/
Std.TreeMap.Raw.minEntry? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Option (α × β)
-- Init.Data.BitVec.Lemmas
BitVec.toNat_twoPow_eq_ite : ∀ {i w : ℕ}, (BitVec.twoPow w i).toNat = if i < w then 2 ^ i else 0
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_succEmb_Ioi : ∀ {n : ℕ} (i : Fin n), Finset.map (Fin.succEmb n) (Finset.Ioi i) = Finset.Ioi i.succ
-- Mathlib.Algebra.Module.Congruence.Defs
/-- A congruence relation that preserves addition and scalar multiplication.
The quotient by a `ModuleCon` inherits `DistribSMul`, `DistribMulAction`, and `Module` instances.  -/
ModuleCon : (S : Type u_2) → (M : Type u_3) → [Add M] → [SMul S M] → Type u_3
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofReal_natCast : ∀ (n : ℕ), ENNReal.ofReal ↑n = ↑n
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Diagnostics : Type
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.sub_zsmul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : AddGroup α],
  Function.Periodic f c → ∀ (n : ℤ), f (x - n • c) = f x
-- Lean.Server.GoTo
Lean.Server.locationLinksOfInfo : Lean.Server.DocumentMeta →
  Lean.Server.GoToKind →
    Lean.Elab.InfoWithCtx → optParam (Option Lean.Elab.InfoTree) none → IO (Array Lean.Lsp.LeanLocationLink)
-- Mathlib.Data.Finsupp.AList
AList.insert_lookupFinsupp : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : DecidableEq α] (l : AList fun _x => M) (a : α) (m : M),
  (AList.insert a m l).lookupFinsupp = l.lookupFinsupp.update a m
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.unop.eq_1 : ∀ {α : Type u_7} {β : Type u_8} [inst : Add α] [inst_1 : Mul α] [inst_2 : Add β] [inst_3 : Mul β],
  RingEquiv.unop = RingEquiv.op.symm
-- Mathlib.Control.Bifunctor
LawfulBifunctor.id_bimap : ∀ {F : Type u₀ → Type u₁ → Type u₂} {inst : Bifunctor F} [self : LawfulBifunctor F] {α : Type u₀} {β : Type u₁}
  (x : F α β), bimap id id x = x
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instDecidableLtOrdinal : {x y : Std.Time.Nanosecond.Ordinal} → Decidable (x < y)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instIntCast : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} → [GradedRing 𝒜] → {x : Submonoid A} → IntCast (HomogeneousLocalization 𝒜 x)
-- Init.System.IO
/-- Converts an `Except ε` action into an `EIO ε` action.

If the `Except ε` action throws an exception, then the resulting `EIO ε` action throws the same
exception. Otherwise, the value is returned.
 -/
EIO.ofExcept : {ε α : Type} → Except ε α → EIO ε α
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.face_le_horn : ∀ {n : ℕ} (i j : Fin (n + 1)), i ≠ j → SSet.stdSimplex.face {i}ᶜ ≤ SSet.horn n j
-- Mathlib.Data.Finsupp.Interval
/-- Pointwise `Finset.Icc` bundled as a `Finsupp`.  -/
Finsupp.rangeIcc : {ι : Type u_1} →
  {α : Type u_2} →
    [inst : Zero α] →
      [inst_1 : PartialOrder α] → [LocallyFiniteOrder α] → [DecidableEq ι] → (ι →₀ α) → (ι →₀ α) → ι →₀ Finset α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget.hlen : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {outWidth : ℕ}
  (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget aig outWidth), 0 < self.len
-- Mathlib.Algebra.Group.Units.Equiv
Units.mulRight_bijective : ∀ {M : Type u_3} [inst : Monoid M] (a : Mˣ), Function.Bijective fun x => x * ↑a
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit L) R),
  ((CategoryTheory.StructuredArrow.map₂ α β).obj X).hom =
    CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (G.map X.hom) (β.app X.right))
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
_private.Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification.0.NumberField.InfinitePlace.embeddingConjugateIte_pos : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K} {w : NumberField.InfinitePlace L},
  NumberField.ComplexEmbedding.LiesOver w.embedding v.embedding →
    NumberField.InfinitePlace.embeddingConjugateIte✝ v w = w.embedding
-- Mathlib.Order.Hom.Order
OrderHom.iSup_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {ι : Sort u_3} [inst_1 : CompleteLattice β] (f : ι → α →o β)
  (x : α), (⨆ i, f i) x = ⨆ i, (f i) x
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.neg_iff : ∀ {f : ℝ → ℝ}, AkraBazziRecurrence.GrowsPolynomially f ↔ AkraBazziRecurrence.GrowsPolynomially (-f)
-- Init.Data.String.Basic
/-- Given a position in `s.sliceTo p₀`, obtain the corresponding position in `s`.  -/
String.Pos.ofSliceTo : {s : String} → {p₀ : s.Pos} → (s.sliceTo p₀).Pos → s.Pos
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.addEquivAddHaarChar_symm : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalAddGroup G] [inst_5 : LocallyCompactSpace G] {φ : G ≃ₜ+ G},
  MeasureTheory.addEquivAddHaarChar φ.symm = (MeasureTheory.addEquivAddHaarChar φ)⁻¹
-- Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
Lean.Meta.Grind.Arith.CommRing.MonadRing.modifyRing : {m : Type → Type} →
  [self : Lean.Meta.Grind.Arith.CommRing.MonadRing m] →
    (Lean.Meta.Grind.Arith.CommRing.Ring → Lean.Meta.Grind.Arith.CommRing.Ring) → m Unit