mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNeg : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [Neg G] → Neg (l.Germ G)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.addRight.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A : C} [inst_2 : CategoryTheory.AddGrpObj A] (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A),
  CategoryTheory.AddGrpObj.addRight f =
    {
      hom :=
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) f))
          CategoryTheory.AddMonObj.add,
      inv :=
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
              (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg)))
          CategoryTheory.AddMonObj.add,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Init.Data.Array.Lemmas
Array.contains_iff_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, xs.contains a = true ↔ a ∈ xs
-- Std.Async.System
/-- Gets the group by its ID.
 -/
Std.Async.System.getGroup : Std.Async.System.GroupId → IO (Option Std.Async.System.GroupInfo)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_lt_of_lt_div : ∀ {a b c : Ordinal.{u_4}}, a < b / c → c * a < b
-- Mathlib.Analysis.Normed.Order.Lattice
/-- Let `α` be a normed lattice ordered group, then the order dual is also a
normed lattice ordered group.
 -/
OrderDual.instHasSolidNorm : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α],
  HasSolidNorm αᵒᵈ
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.count_withDensity : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [MeasurableSingletonClass α] (f : α → ENNReal),
  MeasureTheory.Measure.count.withDensity f = MeasureTheory.Measure.sum fun a => f a • MeasureTheory.Measure.dirac a
-- Lean.AuxRecursor
/-- Is this a constructor elimination or a sparse casesOn?  -/
Lean.isSparseCasesOn : Lean.Environment → Lean.Name → Bool
-- Mathlib.Topology.MetricSpace.Algebra
Prod.instIsBoundedSMul : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : PseudoMetricSpace γ] [inst_3 : Zero α] [inst_4 : Zero β] [inst_5 : Zero γ] [inst_6 : SMul α β]
  [inst_7 : SMul α γ] [IsBoundedSMul α β] [IsBoundedSMul α γ], IsBoundedSMul α (β × γ)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_ne_nil_iff : ∀ {m n : ℕ}, (m<...=n).toArray ≠ #[] ↔ m < n
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_iInf_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {ι : Type u_5} {f : M →ₙ* N},
  Function.Injective ⇑f → ∀ (S : ι → Subsemigroup M), Subsemigroup.comap f (⨅ i, Subsemigroup.map f (S i)) = iInf S
-- Mathlib.Tactic.ProdAssoc
Lean.Expr.ProdTree.type.inj : ∀ {tp : Lean.Expr} {l : Lean.Level} {tp_1 : Lean.Expr} {l_1 : Lean.Level},
  Lean.Expr.ProdTree.type tp l = Lean.Expr.ProdTree.type tp_1 l_1 → tp = tp_1 ∧ l = l_1
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor.mk : Mathlib.Tactic.Linarith.PreprocessorBase →
  (Lean.MVarId → List Lean.Expr → Lean.MetaM (List Mathlib.Tactic.Linarith.Branch)) →
    Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor
-- Mathlib.CategoryTheory.Abelian.SerreClass.Basic
CategoryTheory.ObjectProperty.IsSerreClass.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {P : CategoryTheory.ObjectProperty C} [toContainsZero : P.ContainsZero]
  [toIsClosedUnderSubobjects : P.IsClosedUnderSubobjects] [toIsClosedUnderQuotients : P.IsClosedUnderQuotients]
  [toIsClosedUnderExtensions : P.IsClosedUnderExtensions], P.IsSerreClass
-- Mathlib.Algebra.Order.Group.Synonym
isRegular_toDual : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, IsRegular (OrderDual.toDual a) ↔ IsRegular a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_filter_le_size : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool} (h : t.WF), (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.size ≤ t.size
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.Integrable.ae_of_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  ⦃f : β × γ → E⦄,
  MeasureTheory.Integrable f ((κ.compProd η) a) →
    ∀ᵐ (x : β) ∂κ a, MeasureTheory.Integrable (fun y => f (x, y)) (η (a, x))
-- Mathlib.Data.List.Sort
List.orderedInsert.congr_simp : ∀ {α : Type u_1} (r r_1 : α → α → Prop),
  r = r_1 →
    ∀ {inst : DecidableRel r} [inst_1 : DecidableRel r_1] (a a_1 : α),
      a = a_1 → ∀ (a_2 a_3 : List α), a_2 = a_3 → List.orderedInsert r a a_2 = List.orderedInsert r_1 a_1 a_3
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RiiSliceData.mk.inj : ∀ {α : Type u} {β : α → Type v} {treeMap : Std.DTreeMap.Internal.Impl α β} {range : Std.Rii α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α β} {range_1 : Std.Rii α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.GroupTheory.ArchimedeanDensely
OrderMonoidIso.mulArchimedean : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : CommMonoid β]
  [inst_3 : PartialOrder β] (e : α ≃*o β) [MulArchimedean α], MulArchimedean β
-- Lean.Meta.Tactic.Grind.Types
/-- Stores information for a node in the E-graph.
Each internalized expression `e` has an `ENode` associated with it.
 -/
Lean.Meta.Grind.ENode : Type
-- Mathlib.MeasureTheory.Constructions.AddChar
AddChar.instDiscreteMeasurableSpace : ∀ {A : Type u_1} {M : Type u_2} [inst : AddMonoid A] [inst_1 : Monoid M] [inst_2 : MeasurableSpace A]
  [inst_3 : DiscreteMeasurableSpace A] [inst_4 : Finite A], DiscreteMeasurableSpace (AddChar A M)
-- Lean.Meta.Sym.Apply
/-- Similar to `BackwardRule.apply', but throws an error if unification fails.
 -/
Lean.Meta.Sym.BackwardRule.apply' : Lean.MVarId → Lean.Meta.Sym.BackwardRule → Lean.Meta.Sym.SymM (List Lean.MVarId)
-- Mathlib.Algebra.Order.SuccPred
Order.not_isMax_zero : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : Zero α] [inst_2 : One α] [ZeroLEOneClass α] [NeZero 1], ¬IsMax 0
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
PrimeSpectrum.isMaximal_of_toPiLocalization_surjective : ∀ {R : Type u_1} [inst : CommSemiring R],
  Function.Surjective ⇑(PrimeSpectrum.toPiLocalization R) → ∀ (I : PrimeSpectrum R), I.asIdeal.IsMaximal
-- Mathlib.Order.RelIso.Basic
RelIso.refl_trans : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s), (RelIso.refl r).trans e = e
-- Std.Internal.Parsec.ByteArray
/-- Scans while `pred` is satisfied, bounded by `limit`.
Returns `(count, iterator, hitEof)`.
 -/
_private.Std.Internal.Parsec.ByteArray.0.Std.Internal.Parsec.ByteArray.scanWhileUpTo : (UInt8 → Bool) → ℕ → ℕ → ByteArray.Iterator → ℕ × ByteArray.Iterator × Bool
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.containsThenInsert_fst : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.containsThenInsert k v).1 = t.contains k
-- Lean.Elab.Arg
Lean.Elab.Term.NamedArg.mk.injEq : ∀ (ref : Lean.Syntax) (name : Lean.Name) (val : Lean.Elab.Term.Arg) (numImplicitParams : ℕ) (ref_1 : Lean.Syntax)
  (name_1 : Lean.Name) (val_1 : Lean.Elab.Term.Arg) (numImplicitParams_1 : ℕ),
  ({ ref := ref, name := name, val := val, numImplicitParams := numImplicitParams } =
      { ref := ref_1, name := name_1, val := val_1, numImplicitParams := numImplicitParams_1 }) =
    (ref = ref_1 ∧ name = name_1 ∧ val = val_1 ∧ numImplicitParams = numImplicitParams_1)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.compare_maxKey_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {he : t.modify k f ≠ ∅}, cmp ((t.modify k f).maxKey he) (t.maxKey ⋯) = Ordering.eq
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- The covering map from `ℝ` to the "unit additive circle" `ℝ ⧸ ℤ` is measure-preserving,
considered with respect to the standard measure (defined to be the Haar measure of total mass 1)
on the additive circle, and with respect to the restriction of Lebesgue measure on `ℝ` to an
interval $(t, t + 1]$.  -/
UnitAddCircle.measurePreserving_mk : ∀ (t : ℝ),
  MeasureTheory.MeasurePreserving QuotientAddGroup.mk (MeasureTheory.volume.restrict (Set.Ioc t (t + 1)))
    MeasureTheory.volume
-- Mathlib.Order.Basic
/-- See if the term is `a < b` and the goal is `a ≤ b`.  -/
Mathlib.Tactic.GCongr.exactLeOfLt : Mathlib.Tactic.GCongr.ForwardExt
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  List.find? (fun x => cmp x.1 k == Ordering.eq) t.toList = none ↔ k ∉ t
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getNoNatDivInst : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Expr
-- Mathlib.Order.Antichain
IsWeakAntichain.insert : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)} {a : (i : ι) → α i},
  IsWeakAntichain s →
    (∀ ⦃b : (i : ι) → α i⦄, b ∈ s → a ≠ b → ¬StrongLT b a) →
      (∀ ⦃b : (i : ι) → α i⦄, b ∈ s → a ≠ b → ¬StrongLT a b) → IsWeakAntichain (insert a s)
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m β] →
      {it : Std.IterM m β} →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.Algebra.Notation.Support
Function.support_zero : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M], Function.support 0 = ∅
-- Mathlib.Order.Filter.AtTopBot.Ring
Filter.Tendsto.atTop_mul_atTop₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {l : Filter β}
  {f g : β → α},
  Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Lean.DocString.Markdown
_private.Lean.DocString.Markdown.0.Lean.Doc.MarkdownM.State.mk : Array (String × String) → Lean.Doc.MarkdownM.State
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOfMaxAdjoin.eqn : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (i : M →ₗ[R] N) {f : M →ₗ[R] Q} [inst_7 : Fact (Function.Injective ⇑i)] {y : N}
  (x : ↥(Module.Baer.supExtensionOfMaxSingleton i f y)),
  ↑x = ↑(Module.Baer.ExtensionOfMaxAdjoin.fst i x) + Module.Baer.ExtensionOfMaxAdjoin.snd i x • y
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.SMulInvariantMeasure.add : ∀ {M : Type v} {α : Type w} [inst : SMul M α] {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
  [MeasureTheory.SMulInvariantMeasure M α μ] [MeasureTheory.SMulInvariantMeasure M α ν],
  MeasureTheory.SMulInvariantMeasure M α (μ + ν)
-- Mathlib.Order.ULift
ULift.instLT_mathlib : {α : Type u} → [LT α] → LT (ULift.{v, u} α)
-- Init.MetaTypes
Lean.Meta.EtaStructMode.notClasses.sizeOf_spec : sizeOf Lean.Meta.EtaStructMode.notClasses = 1
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.funLike : (Γ : Subgroup (GL (Fin 2) ℝ)) → (k : ℤ) → FunLike (CuspForm Γ k) UpperHalfPlane ℂ
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- An indexed family of points that is injective on the given
`Finset` has the same centroid as the image of that `Finset`.  This is
stated in terms of a set equal to the image to provide control of
definitional equality for the index type used for the centroid of the
image.  -/
Finset.centroid_eq_centroid_image_of_inj_on : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {p : ι → P},
  (∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j) →
    ∀ {ps : Set P} [inst_4 : Fintype ↑ps],
      ps = p '' ↑s → Finset.centroid k s p = Finset.centroid k Finset.univ fun x => ↑x
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.kerLift_mk : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H) (g : G),
  (QuotientAddGroup.kerLift φ) ↑g = φ g
-- Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
/-- Fundamental theorem of calculus for set integrals:
if `μ` is a measure that is finite at a filter `l` and
`f` is a measurable function that has a finite limit `b` at `l ⊓ ae μ`, then
`∫ x in s i, f x ∂μ = μ (s i) • b + o(μ (s i))` at a filter `li` provided that
`s i` tends to `l.smallSets` along `li`.
Since `μ (s i)` is an `ℝ≥0∞` number, we use `μ.real (s i)` in the actual statement.

Often there is a good formula for `μ.real (s i)`, so the formalization can take an optional
argument `m` with this formula and a proof of `(fun i => μ.real (s i)) =ᶠ[li] m`. Without these
arguments, `m i = μ.real (s i)` is used in the output.  -/
Filter.Tendsto.integral_sub_linear_isLittleO_ae : ∀ {X : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure X} {l : Filter X} [l.IsMeasurablyGenerated]
  {f : X → E} {b : E},
  Filter.Tendsto f (l ⊓ MeasureTheory.ae μ) (nhds b) →
    StronglyMeasurableAtFilter f l μ →
      μ.FiniteAtFilter l →
        ∀ {s : ι → Set X} {li : Filter ι},
          Filter.Tendsto s li l.smallSets →
            ∀ (m : optParam (ι → ℝ) fun i => μ.real (s i)),
              autoParam ((fun i => μ.real (s i)) =ᶠ[li] m) Filter.Tendsto.integral_sub_linear_isLittleO_ae._auto_1 →
                (fun i => ∫ (x : X) in s i, f x ∂μ - m i • b) =o[li] m
-- Init.Data.BitVec.Lemmas
BitVec.toInt_setWidth : ∀ {w v : ℕ} (x : BitVec w), (BitVec.setWidth v x).toInt = (↑x.toNat).bmod (2 ^ v)
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_pos_iff_nonempty_of_smulInvariant : ∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [inst_3 : TopologicalSpace α]
  [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} [μ.Regular], μ ≠ 0 → IsOpen U → (0 < μ U ↔ U.Nonempty)
-- Init.GrindInstances.ToInt
Lean.Grind.instModNatCiOfNatInt : Lean.Grind.ToInt.Mod ℕ (Lean.Grind.IntInterval.ci 0)
-- Mathlib.LinearAlgebra.Matrix.WithConv
instNonAssocSemiringWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [NonAssocSemiring α] → NonAssocSemiring (WithConv (Matrix m n α))
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.aeval.eq_1 : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {a : σ → S} [inst_4 : IsTopologicalSemiring R] [inst_5 : IsUniformAddGroup R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : CompleteSpace S] [inst_8 : T2Space S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S]
  (ha : MvPowerSeries.HasEval a), MvPowerSeries.aeval ha = { toRingHom := MvPowerSeries.eval₂Hom ⋯ ha, commutes' := ⋯ }
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max!_erase_eq_of_not_compare_max!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → ¬cmp k t.max! = Ordering.eq → (t.erase k).max! = t.max!
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionRule.erase.sizeOf_spec : ∀ (a : Lean.Name) (a_1 : Lean.Syntax), sizeOf (Simps.ProjectionRule.erase a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Data.Finset.Image
Finset.subtype.eq_1 : ∀ {α : Type u_4} (p : α → Prop) [inst : DecidablePred p] (s : Finset α),
  Finset.subtype p s = Finset.map { toFun := fun x => ⟨↑x, ⋯⟩, inj' := ⋯ } (Finset.filter p s).attach
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.map_nhds_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (x : X),
  Filter.map (⇑h) (nhds x) = nhds (h x)
-- Lean.Meta.Tactic.Grind.ForallProp
_private.Lean.Meta.Tactic.Grind.ForallProp.0.Lean.Meta.Grind.getOrigin : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Grind.Origin
-- Mathlib.RingTheory.Localization.Integer
IsLocalization.card_finsetIntegerMultiple : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] [inst_4 : DecidableEq R] (s : Finset S),
  (IsLocalization.finsetIntegerMultiple M s).card = s.card
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.State.mk.inj : ∀ {σ : Type} {state : σ} {activeScopes : Lean.NameSet} {delimitsLocal : Bool} {state_1 : σ}
  {activeScopes_1 : Lean.NameSet} {delimitsLocal_1 : Bool},
  { state := state, activeScopes := activeScopes, delimitsLocal := delimitsLocal } =
      { state := state_1, activeScopes := activeScopes_1, delimitsLocal := delimitsLocal_1 } →
    state = state_1 ∧ activeScopes = activeScopes_1 ∧ delimitsLocal = delimitsLocal_1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.contains a = false → m[a]? = none
-- Mathlib.Order.Filter.Defs
/-- `Filter.Tendsto` is the generic "limit of a function" predicate.
`Tendsto f l₁ l₂` asserts that for every `l₂` neighborhood `a`,
the `f`-preimage of `a` is an `l₁` neighborhood.  -/
Filter.Tendsto : {α : Type u_1} → {β : Type u_2} → (α → β) → Filter α → Filter β → Prop
-- Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
AlternatingMap.alternatizeUncurryFin_add : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f g : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N),
  AlternatingMap.alternatizeUncurryFin (f + g) =
    AlternatingMap.alternatizeUncurryFin f + AlternatingMap.alternatizeUncurryFin g
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply : ∀ (G : Type u_1) (A : Type u_2) (B : Type u_4) [inst : Group G] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B] [hA : IsGaloisGroup G A B] [inst_5 : FaithfulSMul A B]
  (x : ↥(FixedPoints.subsemiring B G)), (algebraMap A B) ((IsGaloisGroup.ringEquivFixedPoints G A B).symm x) = ↑x
-- Mathlib.Order.Interval.Multiset
Multiset.Ioo_eq_zero_iff : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [DenselyOrdered α],
  Multiset.Ioo a b = 0 ↔ ¬a < b
-- Mathlib.Algebra.RingQuot
RingQuot.idealQuotientToRingQuot_apply : ∀ {B : Type uR} [inst : CommRing B] (r : B → B → Prop) (x : B),
  (RingQuot.idealQuotientToRingQuot r) ((Ideal.Quotient.mk (Ideal.ofRel r)) x) = (RingQuot.mkRingHom r) x
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- The cofan consisting of the inclusions given by `ιMapBifunctor₁₂BifunctorMapObj`.  -/
CategoryTheory.GradedObject.cofan₃MapBifunctor₁₂BifunctorMapObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₁₂ : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] →
                    (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) →
                      (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) →
                        {I₁ : Type u_7} →
                          {I₂ : Type u_8} →
                            {I₃ : Type u_9} →
                              {J : Type u_10} →
                                {r : I₁ × I₂ × I₃ → J} →
                                  (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r) →
                                    (X₁ : CategoryTheory.GradedObject I₁ C₁) →
                                      (X₂ : CategoryTheory.GradedObject I₂ C₂) →
                                        (X₃ : CategoryTheory.GradedObject I₃ C₃) →
                                          [inst_5 :
                                              (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj
                                                    X₂).HasMap
                                                ρ₁₂.p] →
                                            [(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
                                                          (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁
                                                            X₂)).obj
                                                      X₃).HasMap
                                                  ρ₁₂.q] →
                                              (j : J) →
                                                ((((CategoryTheory.GradedObject.mapTrifunctor
                                                                  (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj
                                                              X₁).obj
                                                          X₂).obj
                                                      X₃).CofanMapObjFun
                                                  r j
-- Mathlib.Algebra.Group.Invertible.Defs
Invertible.mk : {α : Type u} → [inst : Mul α] → [inst_1 : One α] → {a : α} → (invOf : α) → invOf * a = 1 → a * invOf = 1 → Invertible a
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  CategoryTheory.Limits.IsZero T.obj₁ →
    (T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ CategoryTheory.IsIso T.mor₂)
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.initGrindNorm.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
TateCohomology.δ_map : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G]
  {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hS : S.ShortExact) (n : ℤ),
  CategoryTheory.CategoryStruct.comp (TateCohomology.δ hS n) ((tateCohomologyFunctor (n + 1)).map S.f) = 0