mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_mon : ∀ {R : Type u} [inst : CommRing R] (A : AlgCat R),
  (ModuleCat.MonModuleEquivalenceAlgebra.inverse.obj A).mon = ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A
-- Mathlib.Tactic.Push
/-- `pull c` rewrites the goal by pulling the constant `c` closer to the head of the expression.
For instance, `pull _ ∈ _` rewrites `x ∈ y ∨ ¬ x ∈ z` into `x ∈ y ∪ zᶜ`.
More precisely, the `pull` tactic repeatedly rewrites an expression by applying lemmas
of the form `... (c ...) = c ...` (where `c` can appear 1 or more times on the left hand side).
`pull` is the inverse tactic to `push`. To extend the `pull` tactic, you can tag a lemma
with the `@[push]` attribute. `pull` works as both a tactic and a conv tactic.

A lemma is considered a `pull` lemma if its reverse direction is a `push` lemma
that actually moves the given constant away from the head. For example
- `not_or : ¬ (p ∨ q) ↔ ¬ p ∧ ¬ q` is a `pull` lemma, but `not_not : ¬ ¬ p ↔ p` is not.
- `log_mul : log (x * y) = log x + log y` is a `pull` lemma, but `log_abs : log |x| = log x` is not.
- `Pi.mul_def : f * g = fun (i : ι) => f i * g i` and `Pi.one_def : 1 = fun (x : ι) => 1` are both
  `pull` lemmas for `fun`, because every `push fun _ ↦ _` lemma is also considered a `pull` lemma.

TODO: define a `@[pull]` attribute for tagging `pull` lemmas that are not `push` lemmas.

* `pull _ ~ _` pulls the operator or relation `~`.
* `pull c at l1 l2 ...` rewrites at the given locations.
* `pull c at *` rewrites at all hypotheses and the goal.
* `pull (disch := tac) c` uses the tactic `tac` to discharge any hypotheses for `@[push]` lemmas.

Examples:
* `pull _ ∈ _` rewrites `x ∈ y ∨ ¬ x ∈ z` into `x ∈ y ∪ zᶜ`.
* `pull (disch := positivity) Real.log` rewrites `log a + 2 * log b` into `log (a * b ^ 2)`.
* `pull fun _ ↦ _` rewrites `f ^ 2 + 5` into `fun x => f x ^ 2 + 5` where `f` is a function.
 -/
Mathlib.Tactic.Push.convPull____ : Lean.ParserDescr
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Two spheres intersect in at most two points in a two-dimensional subspace containing their
centers; this is a version of `eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two` for bundled
spheres.  -/
EuclideanGeometry.eq_of_mem_sphere_of_mem_sphere_of_mem_of_finrank_eq_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [FiniteDimensional ℝ ↥s.direction],
  Module.finrank ℝ ↥s.direction = 2 →
    ∀ {s₁ s₂ : EuclideanGeometry.Sphere P} {p₁ p₂ p : P},
      s₁.center ∈ s →
        s₂.center ∈ s →
          p₁ ∈ s →
            p₂ ∈ s →
              p ∈ s → s₁ ≠ s₂ → p₁ ≠ p₂ → p₁ ∈ s₁ → p₂ ∈ s₁ → p ∈ s₁ → p₁ ∈ s₂ → p₂ ∈ s₂ → p ∈ s₂ → p = p₁ ∨ p = p₂
-- Init.Tactics
/-- The `injection` tactic is based on the fact that constructors of inductive data
types are injections.
That means that if `c` is a constructor of an inductive datatype, and if `(c t₁)`
and `(c t₂)` are two terms that are equal then  `t₁` and `t₂` are equal too.
If `q` is a proof of a statement of conclusion `t₁ = t₂`, then injection applies
injectivity to derive the equality of all arguments of `t₁` and `t₂` placed in
the same positions. For example, from `(a::b) = (c::d)` we derive `a=c` and `b=d`.
To use this tactic `t₁` and `t₂` should be constructor applications of the same constructor.
Given `h : a::b = c::d`, the tactic `injection h` adds two new hypothesis with types
`a = c` and `b = d` to the main goal.
The tactic `injection h with h₁ h₂` uses the names `h₁` and `h₂` to name the new hypotheses.
 -/
Lean.Parser.Tactic.injection : Lean.ParserDescr
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
height_le_ringKrullDim_quotient_add_spanFinrank : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {p I : Ideal R} [p.IsPrime],
  I ≤ p → ↑p.height ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_neg_left : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ)
  (f g : (i : ι) → E i), ⟪-f, g⟫_[𝕜, w] = -⟪f, g⟫_[𝕜, w]
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂]
  [CategoryTheory.Mono φ.τ₃], S₁.Exact ↔ S₂.Exact
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eccent_le_iff : ∀ {α : Type u_1} {G : SimpleGraph α} (u : α) (k : ℕ∞), G.eccent u ≤ k ↔ ∀ (v : α), G.edist u v ≤ k
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.CoconeMorphism.mk.sizeOf_spec : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cocone F} [inst_2 : SizeOf J] [inst_3 : SizeOf C]
  (hom : A.pt ⟶ B.pt)
  (w :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι.app j) hom = B.ι.app j)
      CategoryTheory.Limits.CoconeMorphism.w._autoParam),
  sizeOf { hom := hom, w := w } = 1 + sizeOf hom
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.AffineOpenCover.ofIsOpenCover_X : ∀ {X : AlgebraicGeometry.Scheme} {ι : Type u_1} (U : ι → X.Opens) (hU : TopologicalSpace.IsOpenCover U)
  (hU' : ∀ (i : ι), AlgebraicGeometry.IsAffineOpen (U i)) (i : ι),
  (AlgebraicGeometry.Scheme.AffineOpenCover.ofIsOpenCover U hU hU').X i = X.presheaf.obj (Opposite.op (U i))
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansion_coeff_unique : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {h : ℝ} (f : F) {c : ℕ → ℂ},
  0 < h →
    AnalyticAt ℂ (UpperHalfPlane.cuspFunction h ⇑f) 0 →
      (∀ (τ : UpperHalfPlane), HasSum (fun m => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) →
        ∀ (m : ℕ), c m = (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h ⇑f)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.nsmul_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (f : X ⟶ M) (n : ℕ)
  (g : M ⟶ N) [CategoryTheory.IsAddMonHom g] {Z : C} (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp (n • f) (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp (n • CategoryTheory.CategoryStruct.comp f g) h
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `ω ↦ exp (u * X ω)` is integrable at `u ≤ 0`, then it is integrable on `[u, 0]`.  -/
ProbabilityTheory.integrable_exp_mul_of_nonpos_of_ge : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t u : ℝ}
  [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Integrable (fun ω => Real.exp (u * X ω)) μ →
    t ≤ 0 → u ≤ t → MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ
-- Mathlib.Order.Closure
ClosureOperator.mk₂_isClosed : ∀ {α : Type u_1} [inst : PartialOrder α] (f : α → α) (hf : ∀ (x : α), x ≤ f x) (hmin : ∀ ⦃x y : α⦄, x ≤ f y → f x ≤ f y)
  (x : α), (ClosureOperator.mk₂ f hf hmin).IsClosed x = (f x = x)
-- Mathlib.Order.WithBot
WithBot.le_def_aux : ∀ {α : Type u_1} [inst : LE α] (a a_1 : WithBot α), a.LE a_1 ↔ a = ⊥ ∨ ∃ a_2 b, a_2 ≤ b ∧ a = ↑a_2 ∧ a_1 = ↑b
-- Mathlib.Order.Hom.Basic
/-- Lift an order homomorphism `f : α →o β` to an order homomorphism `ULift α →o ULift β` in a
higher universe.  -/
OrderHom.uliftMap : {α : Type u_2} →
  {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → ULift.{u_8, u_2} α →o ULift.{u_9, u_3} β
-- Mathlib.Algebra.GroupWithZero.Semiconj
SemiconjBy.zero_right : ∀ {G₀ : Type u_1} [inst : MulZeroClass G₀] (a : G₀), SemiconjBy a 0 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_iSup : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {ι : Sort u_8} (f : P₁ →ᵃ[k] P₂) (s : ι → AffineSubspace k P₁),
  AffineSubspace.map f (iSup s) = ⨆ i, AffineSubspace.map f (s i)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.evaluation_obj_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C) {X_1 Y : CategoryTheory.Functor C D} (α : X_1 ⟶ Y), ((CategoryTheory.evaluation C D).obj X).map α = α.app X
-- Mathlib.Util.PrintSorries
/-- Type of intermediate computation of sorry-tracking.  -/
Mathlib.PrintSorries.State : Type
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAtFilter.comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {L : Filter (𝕜 × 𝕜)} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' : 𝕜'}
  {L' : Filter (𝕜' × 𝕜')},
  HasDerivAtFilter h₂ h₂' L' →
    HasDerivAtFilter h h' L → Filter.Tendsto (Prod.map h h) L L' → HasDerivAtFilter (h₂ ∘ h) (h₂' * h') L
-- Init.Data.Vector.Lemmas
Vector.contains_reverse : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs : Vector α n} {x : α}, xs.reverse.contains x = xs.contains x
-- Mathlib.Data.LawfulXor.Basic
LawfulXor.xor_assoc : ∀ {α : Type u_1} {inst : XorOp α} {inst_1 : Zero α} [self : LawfulXor α] (a b c : α), a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
-- Mathlib.CategoryTheory.ObjectProperty.Small
/-- A property of objects is essentially small relative to a universe `w`
if it is contained in the closure by isomorphisms of a small property.  -/
CategoryTheory.ObjectProperty.EssentiallySmall : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Topology.UniformSpace.Basic
MulOpposite.uniformContinuous_unop : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous MulOpposite.unop
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.Option.map_cast_apply : ∀ {γ γ' : Type u} (h : γ = γ') (x : Option γ), Option.map (cast h) x = cast ⋯ x
-- Mathlib.ModelTheory.Syntax
/-- The sentence indicating that a basic relation symbol is antisymmetric.  -/
FirstOrder.Language.Relations.antisymmetric : {L : FirstOrder.Language} → L.Relations 2 → L.Sentence
-- Mathlib.Algebra.Group.Action.Pi
Pi.mulAction' : {ι : Type u_1} →
  {α : ι → Type u_4} →
    {β : ι → Type u_5} →
      {m : (i : ι) → Monoid (α i)} → [(i : ι) → MulAction (α i) (β i)] → MulAction ((i : ι) → α i) ((i : ι) → β i)
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hV4 : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Monoid G] (self : TopRep k G),
  IsTopologicalAddGroup ↑self
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
/-- `Spec (R / I)` is order-isomorphic to `Z(I)`.  -/
Ideal.primeSpectrumQuotientOrderIsoZeroLocus : {R : Type u} → [inst : CommRing R] → (I : Ideal R) → PrimeSpectrum (R ⧸ I) ≃o ↑(PrimeSpectrum.zeroLocus ↑I)
-- Mathlib.Analysis.Normed.Group.Bounded
/-- **Alias** of the forward direction of `isBounded_iff_forall_norm_le'`. -/
Bornology.IsBounded.exists_norm_le' : ∀ {E : Type u_2} [inst : SeminormedGroup E] {s : Set E}, Bornology.IsBounded s → ∃ C, ∀ x ∈ s, ‖x‖ ≤ C
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (H : CategoryTheory.Functor C D)
  (F : CategoryTheory.Functor (SimplexCategory.Truncated n) C) (X : SimplexCategory.Truncated n),
  (((CategoryTheory.CosimplicialObject.Truncated.whiskering C D).obj H).obj F).obj X = H.obj (F.obj X)
-- Mathlib.CategoryTheory.Localization.FiniteProducts
CategoryTheory.Localization.instHasFiniteProductsLocalization' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C)
  [W.ContainsIdentities] [CategoryTheory.Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts]
  [inst_4 : W.HasLocalization], CategoryTheory.Limits.HasFiniteProducts W.Localization'
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
Lean.Meta.Grind.hashEMatchTheoremPtr.unsafe_impl_2 : Lean.Meta.Grind.EMatchTheorem → UInt64
-- Mathlib.Tactic.CongrExclamation
CongrState.mk : Array Lean.MVarId → List (Lean.TSyntax `rintroPat) → CongrState
-- Mathlib.Algebra.Group.Submonoid.Basic
MonoidHom.coe_ofClosureMEqTopLeft : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] {s : Set M} (f : M → N)
  (hs : Submonoid.closure s = ⊤) (h1 : f 1 = 1) (hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y),
  ⇑(MonoidHom.ofClosureMEqTopLeft f hs h1 hmul) = f
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- For any rings `R, S` and a ring homomorphism `f : R →+* S`, there is a functor from `R`-module to
`S`-module defined by `M ↦ (S →ₗ[R] M)` where `S` is considered as an `R`-module via restriction of
scalars and `g : M ⟶ M'` is sent to `h ↦ g ∘ h`.

The definition of `(coextendScalars f).obj` is given by `CoextendScalars.equiv`.
 -/
ModuleCat.coextendScalars : {R : Type u₁} →
  {S : Type u₂} → [inst : Ring R] → [inst_1 : Ring S] → (R →+* S) → CategoryTheory.Functor (ModuleCat R) (ModuleCat S)
-- Mathlib.Tactic.CongrExclamation
/-- Allow both sides to be partial applications, and allow overapplications.
When false, given an equality `f a b = g x y z` this means we never consider
proving `f a = g x y`.

In this case, we might still consider `f = g x` if a pass generates a congruence lemma using the
left-hand side. Use `sameFun := true` to ensure both sides are applications
of the same function (making it be similar to the `congr` tactic).  -/
Congr!.Config.partialApp : Congr!.Config → Bool
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
/-- The type of Presburger arithmetic functions, defined as (0, 1, +).  -/
FirstOrder.presburgerFunc : ℕ → Type
-- Init.Data.ByteArray.Lemmas
ByteArray.append_eq_empty_iff : ∀ {a b : ByteArray}, a ++ b = ByteArray.empty ↔ a = ByteArray.empty ∧ b = ByteArray.empty
-- Init.Data.List.Lemmas
List.intercalate_cons_cons : ∀ {α : Type u_1} {ys l l' : List α} {zs : List (List α)},
  ys.intercalate (l :: l' :: zs) = l ++ ys ++ ys.intercalate (l' :: zs)
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.traceForm_cartan_nondegenerate : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsKilling R L] [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra],
  (LieModule.traceForm R (↥H) L).Nondegenerate
-- Mathlib.Topology.CantorBendixson
CantorBendixson.iteratedDerivedSet_zero : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, CantorBendixson.iteratedDerivedSet s 0 = s
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Operations.0.SimpleGraph.Walk.drop.match_1.eq_3 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → ℕ → Sort u_2) (v v_1 : V)
  (h : G.Adj u v_1) (q : G.Walk v_1 v) (n : ℕ) (h_1 : (x : ℕ) → motive u SimpleGraph.Walk.nil x)
  (h_2 : (v : V) → (p : G.Walk u v) → motive v p 0)
  (h_3 : (v v_2 : V) → (h : G.Adj u v_2) → (q : G.Walk v_2 v) → (n : ℕ) → motive v (SimpleGraph.Walk.cons h q) n.succ),
  (match v, SimpleGraph.Walk.cons h q, n.succ with
    | .(u), SimpleGraph.Walk.nil, x => h_1 x
    | v, p, 0 => h_2 v p
    | v, SimpleGraph.Walk.cons h q, n.succ => h_3 v v_2 h q n) =
    h_3 v v_1 h q n
-- Lean.Meta.Basic
/-- Evaluates `k` from within a `lambdaLetTelescope`, then uses `mkLetFVars` to rebuild the telescope.
 -/
Lean.Meta.mapLambdaLetTelescope : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      [MonadLiftT Lean.MetaM n] →
        Lean.Expr →
          (Array Lean.Expr → Lean.Expr → n Lean.Expr) →
            optParam Bool false → optParam Bool true → optParam Bool true → n Lean.Expr
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoRightHomology_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] (hg : S.g = 0),
  (S.opcyclesIsoRightHomology hg).inv = S.rightHomologyι
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesLimits.γ_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (j : J),
  (CategoryTheory.Monad.ForgetCreatesLimits.γ D).app j = (D.obj j).a
-- Init.Data.String.Basic
String.Pos.sliceTo.congr_simp : ∀ {s : String} (p₀ pos pos_1 : s.Pos) (e_pos : pos = pos_1) (h : pos ≤ p₀), p₀.sliceTo pos h = p₀.sliceTo pos_1 ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.compare_minKeyD_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {fallback : α}, cmp ((t.modify k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
-- Mathlib.RingTheory.Nilpotent.Defs
nilpotencyClass_eq_succ_iff : ∀ {R : Type u_1} {x : R} [inst : MonoidWithZero R] {k : ℕ}, nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.rightOp_inverse_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : Cᵒᵖ ≌ D) {X Y : Dᵒᵖ} (f : X ⟶ Y), e.rightOp.inverse.map f = (e.inverse.map f.unop).unop
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- The context for a certificate evaluation.  -/
Mathlib.Tactic.Determinant.Ctx : {u : Lean.Level} → {α : Q(Type u)} → Q(CommRing «$α») → Type
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.vcomp_naturality_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans F G)
  (θ : CategoryTheory.Oplax.StrongTrans G H) {a b : B} (f : a ⟶ b),
  ((η.vcomp θ).naturality f).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (θ.app b)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom (θ.app b))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (θ.app b)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f).hom)
            (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (H.map f)).inv)))
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.RelCWComplex.mkFinite_cell : ∀ {X : Type u} [inst : TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : ℕ → Type u)
  (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X)
  (eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)) (finite_cell : ∀ (n : ℕ), Finite (cell n))
  (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1)
  (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1))
  (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target)
  (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1)
  (disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' Metric.ball 0 1) D)
  (mapsTo :
    ∀ (n : ℕ) (i : cell n),
      Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1))
  (isClosedBase : IsClosed D) (union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C) (n : ℕ),
  Topology.RelCWComplex.cell C n = cell n
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l → (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).get? k' = some (cast ⋯ v)
-- Mathlib.Data.FinEnum
FinEnum.decEq : {α : Sort u_1} → [self : FinEnum α] → DecidableEq α
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.lineDerivCLM_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n k : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F]
  {f : TestFunction Ω F n} {v x : E},
  ((TestFunction.lineDerivCLM 𝕜 v) f) x = if k + 1 ≤ n then lineDeriv ℝ (⇑f) x v else 0
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mkHom.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M},
  AddLocalization.mkHom = { toFun := fun x => AddLocalization.mk x.1 x.2, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.instInhabited : (α : Type u_2) → [inst : Lattice α] → [inst_1 : BoundedOrder α] → Inhabited (BoundedLatticeHom α α)
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.succ?_toFun : ∀ {α : Type u} {β : Type v} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  (self : Std.PRange.UpwardEnumerable.Map α β) (a : α),
  Std.PRange.succ? (self.toFun a) = Option.map self.toFun (Std.PRange.succ? a)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.fixed_point_card_lt_of_ne_one : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {σ : Equiv.Perm α},
  σ ≠ 1 → {x | σ x = x}.card < Fintype.card α - 1
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instUniqueSubtypeMemBot.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.instUniqueSubtypeMemBot = { default := 0, uniq := ⋯ }
-- Mathlib.Algebra.Group.Basic
inv_div' : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), (a / b)⁻¹ = a⁻¹ / b⁻¹
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_val_Icc_val : ∀ {n : ℕ} (i j : Fin n), Fin.val ⁻¹' Set.Icc ↑i ↑j = Set.Icc i j
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_loops_eq : ∀ {α : Type u_1} (M : Matroid α) (D : Set α), (M.delete D).loops = M.loops \ D
-- Mathlib.Order.Closure
ClosureOperator.isClosed_iff_closure_le : ∀ {α : Type u_1} [inst : PartialOrder α] {c : ClosureOperator α} {x : α}, c.IsClosed x ↔ c x ≤ x
-- Std.Data.HashSet.Raw
/-- Computes the difference of the given hash sets.

This function always iterates through the smaller, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.HashSet.Raw.diff : {α : Type u} → [BEq α] → [Hashable α] → Std.HashSet.Raw α → Std.HashSet.Raw α → Std.HashSet.Raw α
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ_stalkSpecializes_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {y : ↑X} (hy : y ∈ U) {x : ↑X} (h : x ⤳ y)
  {F_1 : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)}
  [inst_2 : CategoryTheory.ConcreteCategory C F_1] (x_1 : carrier (F.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h))
      ((CategoryTheory.ConcreteCategory.hom (F.germ U y hy)) x_1) =
    (CategoryTheory.ConcreteCategory.hom (F.germ U x ⋯)) x_1