mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- If `f, g : X ⟶ Y` and `f', g : X' ⟶ Y'` pairwise form a commutative square with isomorphisms
`X ≅ X'` and `Y ≅ Y'`, the categories of forks are equivalent.
 -/
CategoryTheory.Limits.Fork.equivOfIsos : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        {X' Y' : C} →
          {f' g' : X' ⟶ Y'} →
            (e₀ : X ≅ X') →
              (e₁ : Y ≅ Y') →
                autoParam (CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom)
                    CategoryTheory.Limits.Fork.equivOfIsos._auto_1 →
                  autoParam (CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom)
                      CategoryTheory.Limits.Fork.equivOfIsos._auto_3 →
                    (CategoryTheory.Limits.Fork f g ≌ CategoryTheory.Limits.Fork f' g')
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
VectorFourier.norm_fourierSMulRight : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V), ‖VectorFourier.fourierSMulRight L f v‖ = 2 * Real.pi * ‖L v‖ * ‖f v‖
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_lt : ∀ {a b : UInt16}, a.toUInt64 < b.toUInt64 ↔ a < b
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
/-- Given `hA : IsUnit A.det` and `b : Basis R b`, `A.toLinearEquiv b hA` is
the `LinearEquiv` arising from `toLin b b A`.

See `Matrix.toLinearEquiv'` for this result on `n → R`.
 -/
Matrix.toLinearEquiv : {n : Type u_1} →
  [inst : Fintype n] →
    {R : Type u_2} →
      {M : Type u_3} →
        [inst_1 : CommRing R] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              Module.Basis n R M → [inst_4 : DecidableEq n] → (A : Matrix n n R) → IsUnit A.det → M ≃ₗ[R] M
-- Lean.Meta.Tactic.Repeat
_private.Lean.Meta.Tactic.Repeat.0.Lean.Meta.repeat'Core.go.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_self_ofReal_re : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), ↑(RCLike.re (inner 𝕜 x x)) = inner 𝕜 x x
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- **Alias** of `Metric.exists_forall_closedEBall_subset_aux₂`.

---

Auxiliary lemma for `exists_continuous_real_forall_closedEBall_subset`
and its smooth counterpart.  -/
EMetric.exists_forall_closedBall_subset_aux₂ : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X} (y : X),
  Convex ℝ (Set.Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ i, ⋂ (_ : y ∈ K i), {r | Metric.closedEBall y r ⊆ U i})
-- Mathlib.RingTheory.Extension.Generators
/-- Version of `Hom.algebraMap_toAlgHom` where `S = S'`, sometimes useful for rewriting.  -/
Algebra.Generators.Hom.algebraMap_toAlgHom' : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {ι' : Type u_3} [inst_3 : CommRing R'] [inst_4 : Algebra R R']
  [inst_5 : Algebra R' S] [IsScalarTower R R' S] {P' : Algebra.Generators R' S ι'} (f : P.Hom P') (x : P.Ring),
  (MvPolynomial.aeval P'.val) (f.toAlgHom x) = (MvPolynomial.aeval P.val) x
-- Std.Time.Format.DateFormat
Std.Time.instInhabitedDayPeriodSymbols : Inhabited Std.Time.DayPeriodSymbols
-- Mathlib.Order.PartialSups
partialSups_mono : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι],
  Monotone partialSups
-- Mathlib.Data.ENNReal.Basic
ENNReal.iSup_coe_eq_top : ∀ {ι : Sort u_2} {f : ι → NNReal}, ⨆ i, ↑(f i) = ⊤ ↔ ¬BddAbove (Set.range f)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.eq_of_bisim_friend : ∀ {γ : Type u_1} {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {op :
    γ →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  [Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass op]
  {x y : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  (motive :
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl → Prop),
  motive x y →
    (∀ (x y : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
        motive x y →
          x = y ∨
            ∃ exp coef c x' y',
              x = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef (op c x') ∧
                y = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef (op c y') ∧ motive x' y') →
      x = y
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
cmp_add_right : ∀ {α : Type u_3} [inst : Add α] [inst_1 : LinearOrder α] [AddRightStrictMono α] (a b c : α),
  cmp (a + c) (b + c) = cmp a b
-- Init.Data.AC
Lean.Data.AC.sort.loop.eq_def : ∀ (a a_1 : List ℕ),
  Lean.Data.AC.sort.loop a a_1 =
    match a, a_1 with
    | acc, [] => acc
    | acc, x :: xs => Lean.Data.AC.sort.loop (Lean.Data.AC.insert x acc) xs
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.ofCoeff_sum : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (s : Finset ι) (f : ι → ℕ →₀ M), { coeff := ∑ i ∈ s, f i } = ∑ i ∈ s, { coeff := f i }
-- Mathlib.RingTheory.Ideal.Operations
IsCoprime.exists : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, IsCoprime I J → ∃ i ∈ I, ∃ j ∈ J, i + j = 1
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.get_push_ref_lt : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} (s : aig.RefVec len)
  (ref : aig.Ref) (idx : ℕ) (hidx : idx < len), (s.push ref).get idx ⋯ = s.get idx hidx
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.antitoneOn_slope_lt : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜},
  ConcaveOn 𝕜 s f → x ∈ s → AntitoneOn (slope f x) {y | y ∈ s ∧ y < x}
-- Mathlib.Order.Category.Lat
/-- Typecheck a `LatticeHom` as a morphism in `Lat`.  -/
Lat.ofHom : {X Y : Type u} → [inst : Lattice X] → [inst_1 : Lattice Y] → LatticeHom X Y → (Lat.of X ⟶ Lat.of Y)
-- Mathlib.NumberTheory.Padics.PadicNumbers
instOnePadic : (p : ℕ) → [inst : Fact (Nat.Prime p)] → One ℚ_[p]
-- Mathlib.Tactic.NormNum.Result
/-- The result is `proof : IsNNRat x n d`,
where `n` a raw nat literal, `d` is a raw nat literal (not 0 or 1),
`n` and `d` are coprime, and `q` is the value of `n / d`.  -/
Mathlib.Meta.NormNum.Result.isNNRat : {u : Lean.Level} →
  {α : Q(Type u)} →
    {x : Q(«$α»)} →
      (inst : autoParam Q(DivisionSemiring «$α») Mathlib.Meta.NormNum.Result.isNNRat._auto_1) →
        ℚ → (n d : Q(ℕ)) → Q(Mathlib.Meta.NormNum.IsNNRat «$x» «$n» «$d») → Mathlib.Meta.NormNum.Result x
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instIntCast : {R : Type u_1} → [IntCast R] → IntCast Rᵐᵒᵖ
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ModuleDiscrTreeRef.mk : {α : Type} → IO.Ref (Lean.Meta.LazyDiscrTree α) → Lean.Meta.LazyDiscrTree.ModuleDiscrTreeRef α
-- Batteries.Data.UnionFind.Basic
/-- Check whether two union-find nodes are equivalent, updating structure using path compression.
Panics if either index is out of bounds.  -/
Batteries.UnionFind.checkEquiv! : Batteries.UnionFind → ℕ → ℕ → Batteries.UnionFind × Bool
-- Mathlib.RingTheory.LocalRing.ResidueField.Defs
/-- The residue field of a local ring is the quotient of the ring by its maximal ideal.  -/
IsLocalRing.ResidueField : (R : Type u_1) → [inst : CommRing R] → [IsLocalRing R] → Type u_1
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.toCompacts : {α : Type u_4} → [inst : TopologicalSpace α] → TopologicalSpace.CompactOpens α → TopologicalSpace.Compacts α
-- Mathlib.Topology.Continuous
map_mem_closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X}
  {x : X} {t : Set Y}, Continuous f → x ∈ closure s → Set.MapsTo f s t → f x ∈ closure t
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.expand_mul_eq_comp : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (q : ℕ) (hq : q ≠ 0),
  PowerSeries.expand (p * q) ⋯ = (PowerSeries.expand p hp).comp (PowerSeries.expand q hq)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cot_conj : ∀ (x : ℂ), ((starRingEnd ℂ) x).cot = (starRingEnd ℂ) x.cot
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.hasFPowerSeriesOnBall_exp_of_radius_pos : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸] [CharZero 𝕂],
  0 < (NormedSpace.expSeries 𝕂 𝔸).radius →
    HasFPowerSeriesOnBall NormedSpace.exp (NormedSpace.expSeries 𝕂 𝔸) 0 (NormedSpace.expSeries 𝕂 𝔸).radius
-- Aesop.RuleSet
/-- An index for the rule patterns associated with rules contained in this rule
set. When rules are removed from the rule set, their patterns are not removed
from this index.
 -/
Aesop.BaseRuleSet.rulePatterns : Aesop.BaseRuleSet → Aesop.RulePatternIndex
-- Mathlib.Tactic.FunProp.Types
/-- Get the expression specified by `origin`.  -/
Mathlib.Meta.FunProp.Origin.getValue : Mathlib.Meta.FunProp.Origin → Lean.MetaM Lean.Expr
-- Std.Http.Protocol.H1
/-- Checks that request-target form and method are compatible
(`CONNECT` requires authority-form and `*` is reserved for `OPTIONS`).

Reference: https://www.rfc-editor.org/rfc/rfc9110#name-methods
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.isValidRequestTargetForMethod : Std.Http.Protocol.H1.Message.Head Std.Http.Protocol.H1.Direction.receiving → Bool
-- Init.Control.Basic
/-- Same as `Bind.bind` but with arguments swapped. 

Conventions for notations in identifiers:

 * The recommended spelling of `=<<` in identifiers is `bindLeft`. -/
«term_=<<_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.coe_detMonoidHom : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R],
  ⇑Matrix.detMonoidHom = Matrix.det
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.dot.injEq : ∀ (termInfo : Lean.Elab.TermInfo) (expectedType? : Option Lean.Expr) (termInfo_1 : Lean.Elab.TermInfo)
  (expectedType?_1 : Option Lean.Expr),
  (Lean.Elab.CompletionInfo.dot termInfo expectedType? = Lean.Elab.CompletionInfo.dot termInfo_1 expectedType?_1) =
    (termInfo = termInfo_1 ∧ expectedType? = expectedType?_1)
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_id : ∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M],
  LinearMap.det LinearMap.id = 1
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- If `A` is a topological `R`-module and the identity map from (`A` with its given
topology) to (`A` with the module topology) is continuous, then the topology on `A` is
the module topology.  -/
IsModuleTopology.of_continuous_id : ∀ {R : Type u_1} [inst : TopologicalSpace R] {A : Type u_2} [inst_1 : Add A] [inst_2 : SMul R A]
  [τA : TopologicalSpace A] [ContinuousAdd A] [ContinuousSMul R A], Continuous id → IsModuleTopology R A
-- Mathlib.Data.Fintype.Quotient
/-- Lift a function on `∀ i, α i` to a function on `∀ i, Trunc (α i)`.  -/
Trunc.finLiftOn : {ι : Type u_1} →
  [DecidableEq ι] →
    [Fintype ι] →
      {α : ι → Sort u_2} →
        {β : Sort u_3} → ((i : ι) → Trunc (α i)) → (f : ((i : ι) → α i) → β) → (∀ (a b : (i : ι) → α i), f a = f b) → β
-- Mathlib.Data.Finset.NAry
/-- The other direction does not hold because of the `u`-`u` cross terms on the RHS.  -/
Finset.image₂_distrib_subset_right : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {δ : Type u_7} {ε : Type u_9} [inst : DecidableEq α']
  [inst_1 : DecidableEq β'] [inst_2 : DecidableEq ε] {s : Finset α} {t : Finset β} [inst_3 : DecidableEq δ]
  {γ : Type u_14} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ} {f₁ : α → γ → α'} {f₂ : β → γ → β'} {g' : α' → β' → ε},
  (∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)) →
    Finset.image₂ f (Finset.image₂ g s t) u ⊆ Finset.image₂ g' (Finset.image₂ f₁ s u) (Finset.image₂ f₂ t u)
-- Std.Data.ExtDHashMap.Basic
/-- Creates a hash map from an array of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofArray`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.  -/
Std.ExtDHashMap.Const.unitOfArray : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Array α → Std.ExtDHashMap α fun x => Unit
-- Mathlib.Geometry.Manifold.MFDeriv.Tangent
/-- The derivative of the inverse of the chart at a base point is the inverse of the chart of the
tangent bundle, composed with the identification between the tangent bundle of the model space and
the product space.  -/
tangentMap_chart_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] {p : TangentBundle I M}
  {q : TangentBundle I H},
  q.proj ∈ (chartAt H p.proj).target →
    tangentMap I I (↑(chartAt H p.proj).symm) q = ↑(chartAt (ModelProd H E) p).symm ((Bundle.TotalSpace.toProd H E) q)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.hom_add : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {M₁ M₂ : TopModuleCat R} (φ₁ φ₂ : M₁ ⟶ M₂),
  TopModuleCat.Hom.hom (φ₁ + φ₂) = TopModuleCat.Hom.hom φ₁ + TopModuleCat.Hom.hom φ₂
-- Mathlib.Probability.Density
MeasureTheory.HasPDF.haveLebesgueDecomposition : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} {X : Ω → E}
  {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} [MeasureTheory.HasPDF X ℙ μ],
  (MeasureTheory.Measure.map X ℙ).HaveLebesgueDecomposition μ
-- Mathlib.RingTheory.Polynomial.Vieta
/-- A sum version of Vieta's formula for `MvPolynomial`: viewing `X i` as variables,
the product of linear terms `λ + X i` is equal to a linear combination of
the symmetric polynomials `esymm σ R j`.  -/
MvPolynomial.prod_C_add_X_eq_sum_esymm : ∀ (R : Type u_1) (σ : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype σ],
  ∏ i, (Polynomial.X + Polynomial.C (MvPolynomial.X i)) =
    ∑ j ∈ Finset.range (Fintype.card σ + 1),
      Polynomial.C (MvPolynomial.esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Grp.hom_mul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (H : CategoryTheory.Grp C) [inst_3 : CategoryTheory.IsCommMonObj H.X],
  CategoryTheory.MonObj.mul.hom.hom = CategoryTheory.MonObj.mul
-- Mathlib.Tactic.Widget.CommDiag
/-- Expressions to display as labels in a diagram.  -/
Mathlib.Tactic.Widget.ExprEmbeds : Type
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_of_isEmpty_insertMany : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type v} [inst_2 : ForIn Id ρ α]
  [EquivBEq α] [LawfulHashable α], m.WF → ∀ {l : ρ}, (m.insertMany l).isEmpty = true → m.isEmpty = true
-- Init.Meta.Defs
Lean.version.isRelease : Bool
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.iInf_adj_of_nonempty : ∀ {ι : Sort u_1} {V : Type u} {a b : V} [Nonempty ι] {f : ι → SimpleGraph V},
  (⨅ i, f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
/-- A modular form with `valueAtInfty f = 0` is zero at infinity.  -/
ModularForm.isZeroAtImInfty_of_valueAtInfty_eq_zero : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] [DiscreteTopology ↥Γ]
  [Γ.HasDetPlusMinusOne] [Fact (IsCusp OnePoint.infty Γ)] [ModularFormClass F Γ k] (f : F),
  UpperHalfPlane.valueAtInfty ⇑f = 0 → UpperHalfPlane.IsZeroAtImInfty ⇑f
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.LimitOfShape.limitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C} (h : P.LimitOfShape J X), P.limitsOfShape J X
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBMap.alter.adapt.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (v : β) → motive (some v)),
  (match none with
    | none => h_1 ()
    | some v => h_2 v) =
    h_1 ()
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoidClass.toAddMonoid.eq_1 : ∀ {M : Type u_4} [inst : AddMonoid M] {A : Type u_5} [inst_1 : SetLike A M] [inst_2 : AddSubmonoidClass A M] (S : A),
  AddSubmonoidClass.toAddMonoid S =
    { toAddSemigroup := AddMemClass.toAddSemigroup S, toZero := ZeroMemClass.zero S, zero_add := ⋯, add_zero := ⋯,
      toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instIsCompactlyGenerated : ∀ (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], IsCompactlyGenerated (LieSubmodule R L M)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_eq_multiset_prod : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (f : ι → M),
  ∏ x ∈ s, f x = (Multiset.map f s.val).prod
-- Mathlib.Order.Sublattice
Sublattice.mem_inf : ∀ {α : Type u_2} [inst : Lattice α] {L M : Sublattice α} {a : α}, a ∈ L ⊓ M ↔ a ∈ L ∧ a ∈ M
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Localization
Module.associatedPrimes.minimalPrimes_annihilator_subset_associatedPrimes : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_3) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherianRing R]
  [Module.Finite R M], (Module.annihilator R M).minimalPrimes ⊆ associatedPrimes R M
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyOutgoingCall.fromRanges : Lean.Lsp.CallHierarchyOutgoingCall → Array Lean.Lsp.Range
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_zero : UInt8.toBitVec 0 = 0#8
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.sup_mul_inf : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a b : Associates α),
  (a ⊔ b) * (a ⊓ b) = a * b
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedMonoid.mk : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α],
  (∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c) → (∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b) → IsOrderedMonoid α
-- Mathlib.Data.Int.ConditionallyCompleteOrder
Int.csInf_eq_leastOfBdd : ∀ {s : Set ℤ} [inst : DecidablePred fun x => x ∈ s] (b : ℤ) (Hb : ∀ z ∈ s, b ≤ z) (Hinh : ∃ z, z ∈ s),
  sInf s = ↑(b.leastOfBdd Hb Hinh)
-- Mathlib.RingTheory.Smooth.Basic
/-- Any formally smooth extension can be used to calculate `H¹(L_{A/R})`.  -/
Algebra.Extension.equivH1CotangentOfFormallySmooth : {R : Type u} →
  {A : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          (P : Algebra.Extension R A) → [Algebra.FormallySmooth R P.Ring] → P.H1Cotangent ≃ₗ[A] Algebra.H1Cotangent R A
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_15 : HSub Std.Time.Second.Offset Std.Time.Hour.Offset Std.Time.Second.Offset
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Makes a continuous multiplicative isomorphism from
a homeomorphism which preserves multiplication.  -/
ContinuousMulEquiv.mk' : {M : Type u_1} →
  {N : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace N] →
        [inst_2 : Mul M] → [inst_3 : Mul N] → (f : M ≃ₜ N) → (∀ (x y : M), f (x * y) = f x * f y) → M ≃ₜ* N
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.restrict_toRationalMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain),
  (f.restrict U hU hU').toRationalMap = f.toRationalMap
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- The variables which have been *implicitly eliminated*.
These are variables that appear in the historical set,
do not appear in `c` itself, and are not in `effective`.  -/
Mathlib.Tactic.Linarith.PComp.implicit : Mathlib.Tactic.Linarith.PComp → Std.TreeSet ℕ compare
-- Mathlib.Topology.Order.Bornology
IsOrderBornology.mk : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : Preorder α],
  (∀ (s : Set α), Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s) → IsOrderBornology α
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RciSliceData.range : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RciSliceData α → Std.Rci α
-- Mathlib.Data.NNRat.Defs
NNRat.coe_pos : ∀ {q : ℚ≥0}, 0 < ↑q ↔ 0 < q
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
/-- The canonical map from a disjoint union of prime spectra of commutative semirings to
the prime spectrum of the product semiring.
This is always an open embedding, see `PrimeSpectrum.isOpenEmbedding_sigmaToPi` and
a homeomorphism if `ι` is finite, see `PrimeSpectrum.sigmaHomeoPi`.
 -/
PrimeSpectrum.sigmaToPi : {ι : Type u_3} →
  (R : ι → Type u_2) →
    [inst : (i : ι) → CommSemiring (R i)] → (i : ι) × PrimeSpectrum (R i) → PrimeSpectrum ((i : ι) → R i)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.disjoint_commonNeighbors : ∀ {V : Type u} {G H : SimpleGraph V},
  (∀ (u v : V), Disjoint (G.commonNeighbors u v) (H.commonNeighbors u v)) ↔ Disjoint G H
-- Lean.Elab.InfoTree.Types
Lean.Elab.MonadInfoTree : (Type → Type) → Type
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- A linear surjection to a module with the module topology is open.  -/
IsModuleTopology.isOpenMap_of_surjective : ∀ {R : Type u_1} [τR : TopologicalSpace R] [inst : Ring R] {A : Type u_3} [inst_1 : AddCommGroup A]
  [inst_2 : Module R A] [inst_3 : TopologicalSpace A] {B : Type u_4} [inst_4 : AddCommGroup B] [inst_5 : Module R B]
  [inst_6 : TopologicalSpace B] [IsModuleTopology R B] [ContinuousAdd A] [ContinuousSMul R A] {φ : A →ₗ[R] B},
  Function.Surjective ⇑φ → IsOpenMap ⇑φ
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.X_mem_supported : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R] {s : Set σ} [Nontrivial R] {i : σ},
  MvPolynomial.X i ∈ MvPolynomial.supported R s ↔ i ∈ s
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The natural transformation between two functors out of the
walking pair, specified by its components.  -/
CategoryTheory.Limits.mapPair : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} →
      (F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶
          G.obj { as := CategoryTheory.Limits.WalkingPair.left }) →
        (F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶
            G.obj { as := CategoryTheory.Limits.WalkingPair.right }) →
          (F ⟶ G)
-- Mathlib.Topology.Continuous
/-- If a continuous map `f` maps `s` to a closed set `t`, then it maps `closure s` to `t`.  -/
Set.MapsTo.closure_left : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X}
  {t : Set Y}, Set.MapsTo f s t → Continuous f → IsClosed t → Set.MapsTo f (closure s) t