mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPowerSeries.Inverse
/-- The map between multivariate formal power series over the same indexing set
induced by a local ring hom `A → B` is local  -/
MvPowerSeries.map.isLocalHom : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) [IsLocalHom f],
  IsLocalHom (MvPowerSeries.map f)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instOverTerminalScheme : (X : AlgebraicGeometry.Scheme) → X.Over (⊤_ AlgebraicGeometry.Scheme)
-- Mathlib.Data.Num.Lemmas
Num.cast_succ' : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (n : Num), ↑n.succ' = ↑n + 1
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.map_lowerCentralSeries : ∀ {G : Type u_1} [inst : AddGroup G] (S : AddSubgroup G) {K : Type u_2} [inst_1 : AddGroup K] (f : G →+ K) (n : ℕ),
  AddSubgroup.map f (S.lowerCentralSeries n) = (AddSubgroup.map f S).lowerCentralSeries n
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
CategoryTheory.Adjunction.derivedε_fac_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [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} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂}
  (W₂ : CategoryTheory.MorphismProperty C₂) [inst_4 : L₂.IsLocalization W₂] {G' : CategoryTheory.Functor D₁ D₂}
  {F' : CategoryTheory.Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F')
  [inst_5 :
    (F'.comp G').IsRightDerivedFunctor
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G') (L₂.associator F' G').hom) W₂]
  (X₂ : C₂),
  CategoryTheory.CategoryStruct.comp (G'.map (β.app X₂)) ((adj.derivedε W₂ α β).app (L₂.obj X₂)) =
    CategoryTheory.CategoryStruct.comp (α.app (F.obj X₂)) (L₂.map (adj.counit.app X₂))
-- Mathlib.Data.Seq.Computation
Computation.length_think : ∀ {α : Type u} (s : Computation α) [h : s.Terminates], s.think.length = s.length + 1
-- Mathlib.Combinatorics.Additive.Convolution
Finset.addConvolution_univ : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] [inst_2 : Fintype G] (A : Finset G) (a : G),
  A.addConvolution Finset.univ a = A.card
-- Mathlib.Algebra.Order.Field.GeomSum
geom₂_sum_of_gt : ∀ {K : Type u_1} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K]
  [inst_4 : Sub K] [OrderedSub K] {x y : K},
  y < x → ∀ (n : ℕ), ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- `(Z ⨯ Y) ×[Y] X ≅ Z ⨯ X`  -/
CategoryTheory.Limits.pullbackProdSndIsoProd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        (Z : C) →
          [inst_1 : CategoryTheory.Limits.HasBinaryProduct Z Y] →
            [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z X] →
              [inst_3 : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.prod.snd f] →
                CategoryTheory.Limits.pullback CategoryTheory.Limits.prod.snd f ≅ Z ⨯ X
-- Mathlib.RingTheory.PolynomialAlgebra
Polynomial.algebraMap_def : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  algebraMap (Polynomial R) (Polynomial A) = Polynomial.mapRingHom (algebraMap R A)
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.image_mem_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsOpenEmbedding f → ∀ {s : Set X} {x : X}, f '' s ∈ nhds (f x) ↔ s ∈ nhds x
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.readMessage : Lean.Lsp.Ipc.IpcM Lean.JsonRpc.Message
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.neg_pi_div_two_ne_zero : ↑(-Real.pi / 2) ≠ 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryGE!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α},
  t₁.Equiv t₂ → Std.DTreeMap.Const.getEntryGE! t₁ k = Std.DTreeMap.Const.getEntryGE! t₂ k
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k k' : α} {f : Option β → Option β},
  (Std.ExtDHashMap.Const.alter m k f).getKey! k' =
    if (k == k') = true then if (f (Std.ExtDHashMap.Const.get? m k)).isSome = true then k else default else m.getKey! k'
-- Aesop.Util.Basic
_private.Aesop.Util.Basic.0.Aesop.filterTrieM : {m : Type u_1 → Type u_2} →
  {σ : Type u_1} →
    {α : Type} →
      [Monad m] →
        [Inhabited σ] →
          (σ → α → m σ) →
            (α → m (ULift.{u_1, 0} Bool)) → σ → Lean.Meta.DiscrTree.Trie α → m (Lean.Meta.DiscrTree.Trie α × σ)
-- Mathlib.GroupTheory.GroupAction.ConjAct
/-- The set of fixed points of the conjugation action of `G` on itself is the center of `G`.  -/
ConjAct.fixedPoints_eq_center : ∀ {G : Type u_3} [inst : Group G], MulAction.fixedPoints (ConjAct G) G = ↑(Subgroup.center G)
-- Mathlib.LinearAlgebra.Complex.Module
Complex.I_mem_skewAdjoint : Complex.I ∈ skewAdjoint ℂ
-- Mathlib.Topology.Category.Profinite.Basic
/-- The category of profinite sets is reflective in the category of compact Hausdorff spaces  -/
Profinite.toCompHaus.reflective : CategoryTheory.Reflective profiniteToCompHaus
-- Qq.MatchImpl
Qq.Impl.mkIsDefEqResultVal : (decls : List Qq.Impl.PatVarDecl) →
  (have a := Qq.Impl.mkIsDefEqType decls;
    Q(«$a»)) →
    Q(Bool)
-- Lean.Meta.CtorIdxHInj
_private.Lean.Meta.CtorIdxHInj.0.Lean.Meta.hinjSuffix : String
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- The Euler integral for the `Γ` function converges for positive real `s`.  -/
Real.GammaIntegral_convergent : ∀ {s : ℝ}, 0 < s → MeasureTheory.IntegrableOn (fun x => Real.exp (-x) * x ^ (s - 1)) (Set.Ioi 0) MeasureTheory.volume
-- Mathlib.Topology.ClopenBox
TopologicalSpace.Clopens.countable_prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace Y]
  [CompactSpace X] [Countable (TopologicalSpace.Clopens X)] [Countable (TopologicalSpace.Clopens Y)],
  Countable (TopologicalSpace.Clopens (X × Y))
-- Mathlib.RingTheory.WittVector.Teichmuller
/-- `teichmuller` is a natural transformation.  -/
WittVector.map_teichmuller : ∀ (p : ℕ) {R : Type u_1} {S : Type u_2} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [inst_1 : CommRing S]
  (f : R →+* S) (r : R), (WittVector.map f) ((WittVector.teichmuller p) r) = (WittVector.teichmuller p) (f r)
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.homEquiv_comp_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] {F₁ F₂ F₃ : CategoryTheory.Functor J C}
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₂ F₃]
  [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₃] (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) {Z : V}
  (h : CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Enriched.FunctorCategory.homEquiv V) (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.Enriched.FunctorCategory.homEquiv V) f)
          ((CategoryTheory.Enriched.FunctorCategory.homEquiv V) g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedComp V F₁ F₂ F₃) h))
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mk.sizeOf_spec : ∀ {α : Type u_2} [inst : BooleanAlgebra α] [inst_1 : SizeOf α] (toSublattice : Sublattice α)
  (compl_mem' : ∀ {a : α}, a ∈ toSublattice.carrier → aᶜ ∈ toSublattice.carrier) (bot_mem' : ⊥ ∈ toSublattice.carrier),
  sizeOf { toSublattice := toSublattice, compl_mem' := compl_mem', bot_mem' := bot_mem' } =
    1 + sizeOf toSublattice + sizeOf bot_mem'
-- Mathlib.Data.Prod.TProd
List.TProd.elim_mk : ∀ {ι : Type u} {α : ι → Type v} [inst : DecidableEq ι] (l : List ι) (f : (i : ι) → α i) {i : ι} (hi : i ∈ l),
  (List.TProd.mk l f).elim hi = f i
-- Mathlib.Algebra.RingQuot
RingQuot.eq_lift_comp_mkRingHom : ∀ {R : Type uR} [inst : Semiring R] {T : Type uT} [inst_1 : Semiring T] {r : R → R → Prop} (f : RingQuot r →+* T),
  f = RingQuot.lift ⟨f.comp (RingQuot.mkRingHom r), ⋯⟩
-- Init.Data.SInt.Lemmas
Int8.sub_right_inj : ∀ {a b : Int8} (c : Int8), c - a = c - b ↔ a = b
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isAdjointPair_id : ∀ {R : Type u_1} {M : Type u_5} {M₃ : Type u_8} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃}, B.IsAdjointPair B id id
-- Init.Data.Range.Polymorphic.Basic
Std.Rxi.HasSize.mk : {α : Type u} → (α → ℕ) → Std.Rxi.HasSize α
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.commShiftIso_inv_app_counit_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] [adj.CommShift A] (a : A)
  (Y : D) {Z : D} (h : (CategoryTheory.shiftFunctor D a).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (G.comp F) a).inv.app Y)
      (CategoryTheory.CategoryStruct.comp (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj Y)) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (adj.counit.app Y)) h
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.firstM.go.eq_def : ∀ {β : Type v} {α : Type u} {m : Type v → Type w} [inst : Alternative m] (f : α → m β) (as : Array α) (i : ℕ),
  Array.firstM.go✝ f as i = if hlt : i < as.size then f as[i] <|> Array.firstM.go✝ f as (i + 1) else failure
-- Mathlib.NumberTheory.Dioph
Poly.zero_apply : ∀ {α : Type u_1} (x : α → ℕ), 0 x = 0
-- Mathlib.Algebra.Order.Hom.Basic
RingSeminormClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : NonUnitalNonAssocRing α]
  [inst_1 : Semiring β] [inst_2 : PartialOrder β] [inst_3 : FunLike F α β]
  [toAddGroupSeminormClass : AddGroupSeminormClass F α β]
  [toSubmultiplicativeHomClass : SubmultiplicativeHomClass F α β], RingSeminormClass F α β
-- Mathlib.Logic.Equiv.Set
Equiv.Set.congr_symm_apply : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (t : Set β), (Equiv.Set.congr e).symm t = ⇑e.symm '' t
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.volume_Ioi : ∀ (x : ↑unitInterval), MeasureTheory.volume (Set.Ioi x) = ENNReal.ofReal (1 - ↑x)
-- Std.Data.DHashMap.Basic
Std.DHashMap.instForMSigmaOfMonad : {α : Type u} →
  {β : α → Type v} →
    {m : Type w → Type w'} →
      [Monad m] → [inst : BEq α] → [inst_1 : Hashable α] → ForM m (Std.DHashMap α β) ((a : α) × β a)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.post_map_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T)
  (F : CategoryTheory.Functor T C) {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y),
  ((CategoryTheory.Comma.post L R F).map f).right = f.right
-- Lean.Server.CodeActions.Attr
/-- The declaration to tag  -/
Lean.CodeAction.CommandCodeActionEntry.declName : Lean.CodeAction.CommandCodeActionEntry → Lean.Name
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.le_retracts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C), P ≤ P.retracts
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsMarkovKernel.swapRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsMarkovKernel κ],
  ProbabilityTheory.IsMarkovKernel κ.swapRight
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul : ∀ {α : Type u_1} {F : Type u_3} {G : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G} {c : NNReal},
  (∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) → ∀ (p : ENNReal), MeasureTheory.eLpNorm f p μ ≤ c • MeasureTheory.eLpNorm g p μ
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.Set.prod_symm_apply_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set X) (t : Set Y)
  (x : { a // (fun x => x ∈ s) a } × { b // (fun x => x ∈ t) b }), ↑((Homeomorph.Set.prod s t).symm x) = (↑x.1, ↑x.2)
-- Batteries.Lean.Meta.Inaccessible
/-- Rename all inaccessible fvars. An fvar is inaccessible if (a) its user name is
inaccessible or (b) it is shadowed by a later fvar with the same user name. This
function gives all inaccessible fvars a unique, accessible user name. It returns
the new goal and the fvars that were renamed.
 -/
Lean.MVarId.renameInaccessibleFVars : Lean.MVarId → Lean.MetaM (Lean.MVarId × Array Lean.FVarId)
-- Mathlib.Data.Set.Pairwise.Basic
pairwise_subtype_iff_pairwise_set : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), (Pairwise fun x y => r ↑x ↑y) ↔ s.Pairwise r
-- Mathlib.Analysis.Analytic.IteratedFDeriv
ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E [×n]→L[𝕜] F) (x : E) (v : Fin n → E),
  (iteratedFDeriv 𝕜 n (fun x => f fun x_1 => x) x) v = ∑ σ, f fun i => v (σ i)
-- Mathlib.Topology.Category.Sequential
Sequential.instConcreteCategoryContinuousMapCarrierToTop : CategoryTheory.ConcreteCategory Sequential fun x1 x2 => C(↑x1.toTop, ↑x2.toTop)
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.foldM.match_1.splitter : {α : Type u_1} →
  (motive : Option (α × Batteries.BinomialHeap.Imp.Heap α) → Sort u_2) →
    (x : Option (α × Batteries.BinomialHeap.Imp.Heap α)) →
      (x = none → motive none) →
        ((hd : α) → (tl : Batteries.BinomialHeap.Imp.Heap α) → x = some (hd, tl) → motive (some (hd, tl))) → motive x
-- Std.Data.DHashMap.Basic
Std.DHashMap.instSDiff : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → SDiff (Std.DHashMap α β)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.verts_spanningCoe_injective : ∀ {V : Type u} {G : SimpleGraph V}, Function.Injective fun G' => (G'.verts, G'.spanningCoe)
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.foldlM.loop.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (i' : ℕ) (h_1 : Unit → motive 0) (h_2 : (i' : ℕ) → motive i'.succ),
  (match i'.succ with
    | 0 => h_1 ()
    | i'.succ => h_2 i') =
    h_2 i'
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t₁ \ t₂).get? k = if k ∈ t₂ then none else t₁.get? k
-- Mathlib.RingTheory.LocalProperties.Basic
/-- An ideal is trivial if its localization at every maximal ideal is trivial.  -/
ideal_eq_bot_of_localization : ∀ {R : Type u_1} [inst : CommSemiring R] (I : Ideal R),
  (∀ (J : Ideal R) (x : J.IsMaximal), IsLocalization.coeSubmodule (Localization.AtPrime J) I = ⊥) → I = ⊥
-- Init.Data.String.Lemmas.Basic
_private.Init.Data.String.Lemmas.Basic.0.String.Slice.Pos.nextn.eq_2 : ∀ {s : String.Slice} (p : s.Pos) (n_2 : ℕ), p.nextn n_2.succ = if h : p ≠ s.endPos then (p.next h).nextn n_2 else p
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `replicate` on `BitVec`s.  -/
BitVec.reduceReplicate : Lean.Meta.Simp.DSimproc
-- Std.Data.HashMap.Lemmas
Std.HashMap.filter_equiv_self_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → β → Bool}, (Std.HashMap.filter f m).Equiv m ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) m[k] = true
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.lapply_comp_lsingle_same : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (i : ι),
  DFinsupp.lapply i ∘ₗ DFinsupp.lsingle i = LinearMap.id
-- Mathlib.Algebra.Homology.DifferentialObject
CategoryTheory.DifferentialObject.objEqToHom_d_assoc : ∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x y : β} (h : x = y) {Z : V}
  (h_1 : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).obj X.obj y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (CategoryTheory.CategoryStruct.comp (X.d y) h_1) =
    CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.objEqToHom ⋯) h_1)
-- Mathlib.RingTheory.LocalRing.Basic
/-- The nonunits of a local semiring form an additive submonoid.  -/
IsLocalRing.nonunitsAddSubmonoid : (R : Type u_1) → [inst : Semiring R] → [IsLocalRing R] → AddSubmonoid R
-- Init.Data.String.Basic
String.data_singleton : ∀ (c : Char), (String.singleton c).toList = [c]
-- Mathlib.Topology.Algebra.UniformConvergence
instInvUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Inv β],
  instInvUniformOnFun = { inv := instInvUniformOnFun._aux_1 }
-- Mathlib.GroupTheory.Subsemigroup.Center
AddSubsemigroup.decidableMemCenter.eq_1 : ∀ {M : Type u_1} [inst : AddSemigroup M] (a : M) [inst_1 : Decidable (∀ (b : M), b + a = a + b)],
  AddSubsemigroup.decidableMemCenter a = decidable_of_iff' (∀ (g : M), g + a = a + g) ⋯
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossingStrat_le_one : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω}, MeasureTheory.upcrossingStrat a b f N n ω ≤ 1
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.basicOpen_pow : ∀ {R : Type u} [inst : CommSemiring R] (f : R) (n : ℕ),
  0 < n → PrimeSpectrum.basicOpen (f ^ n) = PrimeSpectrum.basicOpen f
-- Lean.Elab.ParseImportsFast
Lean.PrintImportResult.mk.inj : ∀ {result? : Option Lean.ModuleHeader} {errors : Array String} {result?_1 : Option Lean.ModuleHeader}
  {errors_1 : Array String},
  { result? := result?, errors := errors } = { result? := result?_1, errors := errors_1 } →
    result? = result?_1 ∧ errors = errors_1
-- Init.Data.Option.Lemmas
Option.pfilter_eq_none_iff : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool},
  o.pfilter p = none ↔ o = none ∨ ∃ a, ∃ (ha : o = some a), p a ha = false
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.updateUnbox! : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu → Lean.FVarId → Lean.Compiler.LCNF.LetValue pu
-- Init.Grind.ToIntLemmas
Lean.Grind.IntInterval.hi?.eq_4 : Lean.Grind.IntInterval.ii.hi? = none
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.ihom_obj : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] [inst_2 : (i : I) → CategoryTheory.MonoidalClosed (C i)]
  (X Y : (i : I) → C i) (i : I), (CategoryTheory.Pi.ihom X).obj Y i = (X i ⟹ Y i)
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.radical_le_vanishingIdeal_zeroLocus : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  (I : Ideal (MvPolynomial σ k)), I.radical ≤ MvPolynomial.vanishingIdeal k (MvPolynomial.zeroLocus K I)
-- Init.Data.Vector.Extract
Vector.getElem?_extract_of_succ : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {j : ℕ}, (xs.extract 0 (j + 1))[j]? = xs[j]?
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Enriched.Functor.instEnrichedCategoryFunctorType : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.EnrichedCategory (CategoryTheory.Functor C (Type (max v' v u))) (CategoryTheory.Functor C D)
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_le_comap : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] (I : Ideal S),
  (Ideal.relNorm R) I ≤ Ideal.comap (algebraMap R S) I
-- Mathlib.Data.Set.UnionLift
Set.liftCover_of_mem : ∀ {α : Type u_1} {ι : Sort u_3} {β : Sort u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β}
  {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {hS : Set.iUnion S = Set.univ}
  {i : ι} {x : α} (hx : x ∈ S i), Set.liftCover S f hf hS x = f i ⟨x, hx⟩
-- Mathlib.Dynamics.Transitive
AddAction.isTopologicallyTransitive_of_isMinimal : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddMonoid M] [inst_2 : AddAction M α]
  [AddAction.IsMinimal M α], AddAction.IsTopologicallyTransitive M α
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ D` creates limits of shape `Jᵒᵖ`, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits of
shape `J`.  -/
CategoryTheory.Limits.createsColimitsOfShapeOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor C D) →
              [CategoryTheory.CreatesLimitsOfShape Jᵒᵖ F] → CategoryTheory.CreatesColimitsOfShape J F.op
-- Mathlib.Topology.GDelta.Basic
/-- A closed set is nowhere dense iff its interior is empty.  -/
IsClosed.isNowhereDense_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → (IsNowhereDense s ↔ interior s = ∅)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.ext_iff : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} {x y : v.Completion},
  x = y ↔ x.toCompletion = y.toCompletion
-- Mathlib.Algebra.CharP.Two
CharTwo.add_cancel_left : ∀ {R : Type u_1} [inst : Semiring R] [CharP R 2] (a b : R), a + (a + b) = b
-- Mathlib.Order.Filter.IndicatorFunction
Filter.EventuallyEq.of_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β] {l : Filter α} {f : α → β},
  (∀ᶠ (x : α) in l, f x ≠ 0) → ∀ {s t : Set α}, s.indicator f =ᶠ[l] t.indicator f → s =ᶠ[l] t
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_sub : ∀ {R : Type u} [inst : Ring R] {k : ℕ} {f g : Polynomial R},
  (⇑Polynomial.derivative)^[k] (f - g) = (⇑Polynomial.derivative)^[k] f - (⇑Polynomial.derivative)^[k] g
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.Parser.Binary.manyTillNegOrZero.go : {α : Type} → Std.Internal.Parsec.ByteArray.Parser α → Array α → Std.Internal.Parsec.ByteArray.Parser (Array α)