mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- The set of finite `ℝ≥0∞` numbers is homeomorphic to `ℝ≥0`.  -/
ENNReal.neTopHomeomorphNNReal : ↑{a | a ≠ ⊤} ≃ₜ NNReal
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is a `MulOneClass` under pointwise operations if `α` is.  -/
Filter.mulOneClass : {α : Type u_2} → [MulOneClass α] → MulOneClass (Filter α)
-- Mathlib.Analysis.Seminorm
Seminorm.uniformContinuous_of_continuousAt_zero : ∀ {𝕝 : Type u_6} {E : Type u_7} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕝 E]
  [inst_3 : UniformSpace E] [IsUniformAddGroup E] {p : Seminorm 𝕝 E}, ContinuousAt (⇑p) 0 → UniformContinuous ⇑p
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_sub_add : ∀ (R : Type u_1) {V : Type u_2} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  (x y : V), midpoint R (x - y) (x + y) = x
-- Mathlib.Topology.NhdsWithin
nhdsWithin_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s u : Set α} {t v : Set β}
  {a : α} {b : β}, u ∈ nhdsWithin a s → v ∈ nhdsWithin b t → u ×ˢ v ∈ nhdsWithin (a, b) (s ×ˢ t)
-- Init.Data.String.Iterator
_private.Init.Data.String.Iterator.0.String.Legacy.Iterator.next.eq_1 : ∀ (s : String) (i : String.Pos.Raw), { s := s, i := i }.next = { s := s, i := String.Pos.Raw.next s i }
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.zero_negPart : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasureTheory.JordanDecomposition.negPart 0 = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false → (t.insertMany l).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.Data.ZMod.Basic
ZMod.neg_eq_self_mod_two : ∀ (a : ZMod 2), -a = a
-- Mathlib.Data.List.Basic
List.Perm.disjoint_right : ∀ {α : Type u} {l₁ l₂ l : List α}, l₁.Perm l₂ → (l.Disjoint l₁ ↔ l.Disjoint l₂)
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.SplitIf.mkDischarge? : optParam Bool false → Lean.MetaM Lean.Meta.Simp.Discharge
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
_private.Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree.0.WeierstrassCurve.expDegree_cast : ∀ {n : ℕ}, n ≠ 0 → 2 * ↑(WeierstrassCurve.expDegree✝ n) = ↑n ^ 2 - if Even n then 4 else 1
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_inv_app : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : A),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso eB hF).inv.app X =
    CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.inverse.map (eB.counitIso.hom.app (F.obj X))))
      (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.inverse.map (hF.inv.app X)))
        (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.unitIso.inv.app (eA.functor.obj X)))
          (eA.unitIso.inv.app X)))
-- Mathlib.NumberTheory.LSeries.Convergence
/-- If `f` is real-valued and `x` is strictly greater than the abscissa of absolute convergence
of `f`, then the real series `∑' n, f n / n ^ x` converges.  -/
LSeries.summable_real_of_abscissaOfAbsConv_lt : ∀ {f : ℕ → ℝ} {x : ℝ}, (LSeries.abscissaOfAbsConv fun x => ↑(f x)) < ↑x → Summable fun n => f n / ↑n ^ x
-- Mathlib.Tactic.Abel
/-- Apply the function `n : ∀ {α} [inst : AddWhatever α], _` to the
implicit parameters in the context, and the given list of arguments.  -/
Mathlib.Tactic.Abel.Context.app : Mathlib.Tactic.Abel.Context → Lean.Name → Lean.Expr → Array Lean.Expr → Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.getVert_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) (n : ℕ),
  (SimpleGraph.Walk.map f p).getVert n = f (p.getVert n)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- If the equalizer of two morphisms is an epimorphism, then the two morphisms are equal.  -/
CategoryTheory.Limits.eq_of_epi_equalizer : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] [CategoryTheory.Epi (CategoryTheory.Limits.equalizer.ι f g)], f = g
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.levelParams : Lean.Elab.PreDefinition → List Lean.Name
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
_private.Mathlib.Combinatorics.SimpleGraph.Triangle.Removal.0.SimpleGraph.card_bound : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {s : Finset α} {P : Finpartition Finset.univ} {ε : ℝ},
  P.IsEquipartition →
    P.parts.card ≤ SzemerediRegularity.bound (ε / 8) ⌈4 / ε⌉₊ →
      s ∈ P.parts → ↑(Fintype.card α) / (2 * ↑(SzemerediRegularity.bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑s.card
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.span_singleton_eq_range : ∀ (R : Type u_1) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  R ∙ x = (LinearMap.toSpanSingleton R M x).range
-- Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
/-- See also `Finset.prod_apply`, with the same conclusion but with the weaker hypothesis
`f : α → M → N`  -/
MonoidHom.finsetProd_apply : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : CommMonoid N] (f : ι → M →* N)
  (s : Finset ι) (b : M), (∏ x ∈ s, f x) b = ∏ x ∈ s, (f x) b
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.mk_surjective : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p],
  Function.Surjective (PerfectClosure.mk K p)
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_Ioi_rpow_iff : ∀ {s t : ℝ}, 0 < t → (MeasureTheory.IntegrableOn (fun x => x ^ s) (Set.Ioi t) MeasureTheory.volume ↔ s < -1)
-- Mathlib.GroupTheory.Coset.Card
Subgroup.card_dvd_of_injective : ∀ {α : Type u_1} [inst : Group α] {H : Type u_2} [inst_1 : Group H] (f : α →* H),
  Function.Injective ⇑f → Nat.card α ∣ Nat.card H
-- Init.Data.SInt.Lemmas
ISize.toInt16_toInt64 : ∀ (n : ISize), n.toInt64.toInt16 = n.toInt16
-- Init.Data.SInt.Lemmas
Int16.neg_add_mul_eq_mul_not : ∀ {a b : Int16}, -(a + a * b) = a * ~~~b
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_mul_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : StrongNormalizedGCDMonoid α] (a b c : α),
  lcm (a * b) (a * c) = normalize a * lcm b c
-- Mathlib.Algebra.Algebra.Equiv
MulSemiringAction.toAlgEquiv_toEquiv : ∀ {G : Type u_2} (R : Type u_3) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G A] [inst_5 : SMulCommClass G R A] (g : G),
  ↑(MulSemiringAction.toAlgEquiv R A g) = ↑((MulSemiringAction.toRingEquiv G A) g)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.trAux.eq_def : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ) (s : Γ) (x : Turing.TM1.Stmt Γ Λ σ)
  (x_1 : σ),
  Turing.TM1to0.trAux M s x x_1 =
    match x, x_1 with
    | Turing.TM1.Stmt.move d q, v => ((some q, v), Turing.TM0.Stmt.move d)
    | Turing.TM1.Stmt.write a q, v => ((some q, v), Turing.TM0.Stmt.write (a s v))
    | Turing.TM1.Stmt.load a q, v => Turing.TM1to0.trAux M s q (a s v)
    | Turing.TM1.Stmt.branch p q₁ q₂, v => bif p s v then Turing.TM1to0.trAux M s q₁ v else Turing.TM1to0.trAux M s q₂ v
    | Turing.TM1.Stmt.goto l, v => ((some (M (l s v)), v), Turing.TM0.Stmt.write s)
    | Turing.TM1.Stmt.halt, v => ((none, v), Turing.TM0.Stmt.write s)
-- Mathlib.Data.Seq.Defs
/-- Combine two sequences with a function  -/
Stream'.Seq.zipWith : {α : Type u} → {β : Type v} → {γ : Type w} → (α → β → γ) → Stream'.Seq α → Stream'.Seq β → Stream'.Seq γ
-- Mathlib.Data.NNRat.Defs
NNRat.ext_iff : ∀ {p q : ℚ≥0}, p = q ↔ ↑p = ↑q
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- For a positive linear functional `Λ : C_c(α, ℝ≥0) → ℝ≥0`, define a positive `ℝ`-linear map.  -/
CompactlySupportedContinuousMap.toRealPositiveLinear : {α : Type u_2} →
  [inst : TopologicalSpace α] →
    (CompactlySupportedContinuousMap α NNReal →ₗ[NNReal] NNReal) → CompactlySupportedContinuousMap α ℝ →ₚ[ℝ] ℝ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.beq_iff_equiv : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : (k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)],
  m₁.WF → m₂.WF → (m₁.beq m₂ = true ↔ m₁.Equiv m₂)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.toList_nil : ∀ {α : Type u_1}, RBTree.RBNode.nil.toList = []
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.instIsUpperWithUpper : ∀ {α : Type u_1} [inst : Preorder α], Topology.IsUpper (Topology.WithUpper α)
-- Mathlib.Order.WellFoundedSet
Finset.wellFoundedOn_sup : ∀ {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] (s : Finset ι) {f : ι → Set α},
  (s.sup f).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r
-- Lean.Expr
Lean.ExprStructEq.instToString : ToString Lean.ExprStructEq
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHSubOffset : HSub Std.Time.PlainDateTime Std.Time.Day.Offset Std.Time.PlainDateTime
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.ParamKind.mk.injEq : ∀ (name : Lean.Name) (bInfo : Lean.BinderInfo) (defVal : Option Lean.Expr) (isAutoParam : Bool) (name_1 : Lean.Name)
  (bInfo_1 : Lean.BinderInfo) (defVal_1 : Option Lean.Expr) (isAutoParam_1 : Bool),
  ({ name := name, bInfo := bInfo, defVal := defVal, isAutoParam := isAutoParam } =
      { name := name_1, bInfo := bInfo_1, defVal := defVal_1, isAutoParam := isAutoParam_1 }) =
    (name = name_1 ∧ bInfo = bInfo_1 ∧ defVal = defVal_1 ∧ isAutoParam = isAutoParam_1)
-- Init.Data.Float.Model.Float
/-- Compute the quotient of two `Float.Model`.
 -/
Float.Model.div : Float.Model → Float.Model → Float.Model
-- Mathlib.FieldTheory.Normal.Basic
AlgHom.liftNormal_commutes : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} {K₂ : Type u_4} [inst_1 : Field K₁] [inst_2 : Field K₂]
  [inst_3 : Algebra F K₁] [inst_4 : Algebra F K₂] (ϕ : K₁ →ₐ[F] K₂) (E : Type u_6) [inst_5 : Field E]
  [inst_6 : Algebra F E] [inst_7 : Algebra K₁ E] [inst_8 : Algebra K₂ E] [inst_9 : IsScalarTower F K₁ E]
  [inst_10 : IsScalarTower F K₂ E] [inst_11 : Normal F E] (x : K₁),
  (ϕ.liftNormal E) ((algebraMap K₁ E) x) = (algebraMap K₂ E) (ϕ x)
-- Mathlib.Tactic.Variable
Mathlib.Command.Variable.completeBinders : ℕ →
  Bool →
    Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder →
      Lean.Elab.TermElabM (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder × Array Bool)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
groupCohomology.epi_δ_of_isZero : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) (n : ℕ),
  CategoryTheory.Limits.IsZero (groupCohomology X.X₂ (n + 1)) → CategoryTheory.Epi (groupCohomology.δ hX n (n + 1) ⋯)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffOn.pow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3} [inst_1 : TopologicalSpace H]
  {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5}
  [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6}
  [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M]
  {s : Set M} {g : M → G}, ContMDiffOn I' I n g s → ∀ (m : ℕ), ContMDiffOn I' I n (fun x => g x ^ m) s
-- Mathlib.Algebra.Module.LinearMap.Defs
Module.compHom.toLinearMap_apply : ∀ {R : Type u_14} {S : Type u_15} [inst : Semiring R] [inst_1 : Semiring S] (g : R →+* S) (a : R),
  (Module.compHom.toLinearMap g) a = g a
-- Mathlib.Topology.Instances.Rat
Int.dist_cast_rat : ∀ (x y : ℤ), dist ↑x ↑y = dist x y
-- Std.Data.DTreeMap.Internal.Operations
/-- The tree.  -/
Std.DTreeMap.Internal.Impl.View.tree : {α : Type u} →
  {β : α → Type v} → {size : ℕ} → Std.DTreeMap.Internal.Impl.View α β size → Std.DTreeMap.Internal.Impl.Tree α β size
-- Init.Data.String.Basic
/-- Non-strict inequality on strings, typically used via the `≤` operator.

`a ≤ b` is defined to mean `¬ b < a`.
 -/
String.le : String → String → Prop
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.strictMonoOn_logb_of_base_lt_one : ∀ {b : ℝ}, 0 < b → b < 1 → StrictMonoOn (Real.logb b) (Set.Iio 0)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.le : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.Arith.Cutsat.UnsatProof
-- Lean.Parser.StrInterpolation
Lean.Parser.interpolatedStrFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Algebra.Azumaya.Defs
TensorProduct.Algebra.moduleAux.eq_1 : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Module A M] [inst_6 : Module B M]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M],
  TensorProduct.Algebra.moduleAux =
    TensorProduct.lift { toFun := fun a => a • (Algebra.lsmul R R M).toLinearMap, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Combinatorics.Enumerative.Bell
/-- `Nat.bell n` is equal to the sum of `Multiset.bell m` over all multisets `m : Multiset ℕ` such
that `m.sum = n`.  -/
Nat.bell_eq_sum_partition : ∀ (n : ℕ), n.bell = ∑ p, p.parts.bell
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.isClosedEmbedding_coe_ennreal : Topology.IsClosedEmbedding ENNReal.toEReal
-- Mathlib.Probability.Independence.BoundedContinuousFunction
/-- If the indicator of a set `A` is independent from a variable `X`, then the set `A` is
independent from the sigma algebra generated by `X`.  -/
IndepFun.singleton_indepSets_of_indicator : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : Type u_4} [mX : MeasurableSpace 𝓧]
  {A : Set Ω} {X : Ω → 𝓧},
  ProbabilityTheory.IndepFun (A.indicator 1) X P → ProbabilityTheory.IndepSets {A} {s | MeasurableSet s} P
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ord_mul : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] {x : ↥X} {f g : ↑X.functionField},
  f ≠ 0 →
    g ≠ 0 → AlgebraicGeometry.Scheme.ord (f * g) x = AlgebraicGeometry.Scheme.ord f x + AlgebraicGeometry.Scheme.ord g x
-- Mathlib.Topology.List
List.continuous_sum : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : AddZeroClass α] [ContinuousAdd α], Continuous List.sum
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.Reason.yes : Std.Time.Reason✝
-- Mathlib.Algebra.Group.Action.Basic
smul_eq_iff_eq_inv_smul : ∀ {α : Type u_5} {β : Type u_6} [inst : Group α] [inst_1 : MulAction α β] (g : α) {x y : β}, g • x = y ↔ x = g⁻¹ • y
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.addSimpCongrTheorem : Lean.Name → Lean.AttributeKind → ℕ → Lean.MetaM Unit
-- Plausible.Gen
_private.Plausible.Gen.0.Plausible.Gen.backtrackFuel : {α : Type u} → ℕ → ℕ → List (ℕ × Plausible.Gen α) → Plausible.Gen α
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.re_star : ∀ {d : ℤ} (z : ℤ√d), (star z).re = z.re
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.iSup_induction' : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {ι : Sort u_1} (N : ι → LieSubmodule R L M)
  {motive : (x : M) → x ∈ ⨆ i, N i → Prop},
  (∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯) →
    motive 0 ⋯ →
      (∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), motive x hx → motive y hy → motive (x + y) ⋯) →
        ∀ {x : M} (hx : x ∈ ⨆ i, N i), motive x hx
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.instAddTermRing : (α : Type u_2) → Add (FirstOrder.Language.ring.Term α)
-- Mathlib.Topology.Algebra.Group.Basic
neg_closure : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G] (s : Set G),
  -closure s = closure (-s)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.hom.faithful : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) (c d : ↑S.objs),
  Function.Injective fun f => S.hom.map f
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.extension_coe : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  [inst_2 : T0Space H] [inst_3 : CompleteSpace H] (f : NormedAddGroupHom G H) (v : G), f.extension ↑v = f v
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_comp_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, (p.comp q).natDegree ≤ p.natDegree * q.natDegree
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.overEquivOfIsInitial_inverse : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X),
  (CategoryTheory.overEquivOfIsInitial.{w, v_1, u_1} X h).inverse =
    CategoryTheory.Functor.fromPUnit (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id X))
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue.kinds : Lean.Json.CompressWorkItemQueue✝ → Array Lean.Json.CompressWorkItemKind✝
-- Mathlib.Data.Vector3
vectorAllP_singleton : ∀ {α : Type u_1} (p : α → Prop) (x : α), VectorAllP p [x] = p x
-- Mathlib.Order.Defs.PartialOrder
le_iff_lt_or_eq' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ≤ a ↔ b < a ∨ a = b
-- Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
SSet.Subcomplex.unionProd.ιIso_hom_right_app_hom_apply : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex) (X_1 : SimplexCategoryᵒᵖ)
  (a : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj X_1),
  (CategoryTheory.ConcreteCategory.hom ((SSet.Subcomplex.unionProd.ιIso S T).hom.right.app X_1)) a = a
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.map_op_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : M), Filter.map MulOpposite.op (nhds x) = nhds (MulOpposite.op x)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.hom_f_injective : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c},
  Function.Injective fun f => f.f
-- Init.Data.Fin.Lemmas
Fin.castAdd_zero : ∀ {n : ℕ}, Fin.castAdd 0 = Fin.cast ⋯
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.uset.sizeOf_spec : ∀ (x : Lean.IR.VarId) (i : ℕ) (y : Lean.IR.VarId) (b : Lean.IR.FnBody),
  sizeOf (Lean.IR.FnBody.uset x i y b) = 1 + sizeOf x + sizeOf i + sizeOf y + sizeOf b
-- Mathlib.Data.Set.Lattice.Image
Set.image2_iInter₂_subset_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_8} (f : α → β → γ)
  (s : (i : ι) → κ i → Set α) (t : Set β), Set.image2 f (⋂ i, ⋂ j, s i j) t ⊆ ⋂ i, ⋂ j, Set.image2 f (s i j) t
-- Mathlib.Data.PNat.Xgcd
/-- `succ₂ [t.1, t.2] = [t.1.succ, t.2.succ]`  -/
PNat.XgcdType.succ₂ : ℕ × ℕ → ℕ × ℕ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The proposition that a projective point representative `(x, y, z)` lies in a Weierstrass curve
`W`.

In other words, it satisfies the homogeneous Weierstrass equation `W(X, Y, Z) = 0`.  -/
WeierstrassCurve.Projective.Equation : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → Prop
-- Mathlib.CategoryTheory.Monoidal.Limits.Basic
CategoryTheory.Limits.lim_ε_π_assoc : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_3 : CategoryTheory.MonoidalCategory C] (j : J) {Z : C}
  (h : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor J C)).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Limits.lim)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor J C))
          j)
        h) =
    h
-- Init.Data.List.Basic
List.instBEq : {α : Type u} → [BEq α] → BEq (List α)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp}, t.keysArray.isEmpty = t.isEmpty
-- Init.Data.Order.Ord
Std.LawfulBEqOrd.compare_beq_eq_beq : ∀ {α : Type u} {x : Ord α} {x_1 : BEq α} [Std.LawfulBEqOrd α] {a b : α}, (compare a b == Ordering.eq) = (a == b)
-- Std.Http.Data.URI.Basic
/-- Checks if a query parameter exists.
 -/
Std.Http.URI.Query.containsEncoded : Std.Http.URI.Query → Std.Http.URI.EncodedQueryParam → Bool
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.opEquiv_inverse_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {x y : CategoryTheory.WithTerminal Cᵒᵖ} (f : x ⟶ y),
  (CategoryTheory.WithInitial.opEquiv C).inverse.map f =
    match x, y, f with
    | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f =>
      CategoryTheory.WithInitial.down f
    | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x =>
      Opposite.op (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of unop))
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x =>
      CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.WithInitial.star)
-- Mathlib.Algebra.Homology.EulerCharacteristic
ComplexShape.eulerCharSignsDownInt : (ComplexShape.down ℤ).EulerCharSigns
-- Init.Data.Rat.Lemmas
Rat.ceil_add_intCast : ∀ {x : ℚ} {y : ℤ}, (x + ↑y).ceil = x.ceil + y
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.go_denote_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {n w : ℕ} (aig : Std.Sat.AIG α) (distance : aig.RefVec n),
  ∀ curr ≤ n - 1,
    ∀ (acc : aig.RefVec w) (lhs : BitVec w) (rhs : BitVec n) (assign : α → Bool),
      (∀ (idx : ℕ) (hidx : idx < w),
          ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (lhs.shiftLeftRec rhs curr).getLsbD idx) →
        (∀ (idx : ℕ) (hidx : idx < n), ⟦assign, { aig := aig, ref := distance.get idx hidx }⟧ = rhs.getLsbD idx) →
          ∀ (idx : ℕ) (hidx : idx < w),
            ⟦assign,
                { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.go aig distance curr acc).aig,
                  ref :=
                    (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.go aig distance curr acc).vec.get idx hidx }⟧ =
              (lhs.shiftLeftRec rhs (n - 1)).getLsbD idx
-- Mathlib.RingTheory.Extension.Generators
/-- The canonical `R`-generators of the polynomial algebra `MvPolynomial ι R`,
indexed by `ι` via the variables `X`.  -/
Algebra.Generators.mvPolynomial : (R : Type u) → (ι : Type w) → [inst : CommRing R] → Algebra.Generators R (MvPolynomial ι R) ι
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.TransitionRule.mk : Std.Time.TimeZone.TransitionSpec → Std.Time.Second.Offset → Std.Time.TimeZone.TransitionRule
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The Kleisli category on a monad `T`.
cf Definition 5.2.9 in [Riehl][riehl2017].  -/
CategoryTheory.Kleisli.category : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (T : CategoryTheory.Monad C) → CategoryTheory.Category.{v, u} (CategoryTheory.Kleisli T)