mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelp.activeSignature? : Lean.Lsp.SignatureHelp → Option ℕ
-- Mathlib.RingTheory.Derivation.Basic
Derivation.mk.sizeOf_spec : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] [inst_6 : SizeOf R]
  [inst_7 : SizeOf A] [inst_8 : SizeOf M] (toLinearMap : A →ₗ[R] M) (map_one_eq_zero' : toLinearMap 1 = 0)
  (leibniz' : ∀ (a b : A), toLinearMap (a * b) = a • toLinearMap b + b • toLinearMap a),
  sizeOf { toLinearMap := toLinearMap, map_one_eq_zero' := map_one_eq_zero', leibniz' := leibniz' } =
    1 + sizeOf toLinearMap + sizeOf map_one_eq_zero'
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.center.addCommMonoid.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M],
  AddSubmonoid.center.addCommMonoid = { toAddMonoid := (AddSubmonoid.center M).toAddMonoid, add_comm := ⋯ }
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_inter_toMeasurable : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  μ s ≠ ⊤ → MeasurableSet t → s ⊆ t → μ.restrict (t ∩ MeasureTheory.toMeasurable μ s) = μ.restrict s
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.Walk.IsPath.isContained_pathGraph : ∀ {V : Type u_3} {G : SimpleGraph V} {u v : V} {w : G.Walk u v},
  w.IsPath → (SimpleGraph.pathGraph (w.length + 1)).IsContained G
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.PEquivOn.mk : {ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      [inst : LinearOrder ι] →
        {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} →
          [inst_1 : SuccOrder ι] →
            {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} →
              {s : Set ι} →
                (equiv : (i : ↑s) → F ↑i ≃ InverseSystem.piLT X ↑i) →
                  InverseSystem.IsNatEquiv f equiv →
                    (∀ {i : ι} (hsi : Order.succ i ∈ s) (hi : ¬IsMax i) (x : F ↑⟨Order.succ i, hsi⟩),
                        (equiv ⟨Order.succ i, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2) →
                      InverseSystem.PEquivOn f equivSucc s
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.spanCarrier.below.mem_add : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S : Set (Projectivization K V)}
  {motive : (a : Projectivization K V) → Projectivization.Subspace.spanCarrier S a → Prop} (v w : V) (hv : v ≠ 0)
  (hw : w ≠ 0) (hvw : v + w ≠ 0) (a : Projectivization.Subspace.spanCarrier S (Projectivization.mk K v hv))
  (a_1 : Projectivization.Subspace.spanCarrier S (Projectivization.mk K w hw)),
  Projectivization.Subspace.spanCarrier.below a →
    motive (Projectivization.mk K v hv) a →
      Projectivization.Subspace.spanCarrier.below a_1 →
        motive (Projectivization.mk K w hw) a_1 → Projectivization.Subspace.spanCarrier.below ⋯
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
nonZeroDivisorsEquivUnits_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (u : ↥(nonZeroDivisors G₀)), nonZeroDivisorsEquivUnits u = Units.mk0 ↑u ⋯
-- Mathlib.Topology.Algebra.Group.Basic
continuousOn_neg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [ContinuousNeg G] {s : Set G}, ContinuousOn Neg.neg s
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_updateRow : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : DecidableEq m] (i : m) {A : X → Matrix m n R} {B : X → n → R},
  Continuous A → Continuous B → Continuous fun x => (A x).updateRow i (B x)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Spec.homEquiv_symm_apply : ∀ {R S : CommRingCat} (f : R ⟶ S), AlgebraicGeometry.Spec.homEquiv.symm f = AlgebraicGeometry.Spec.map f
-- Mathlib.Util.Export
Lean.Export.Alloc.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] (map : Std.HashMap α ℕ) (next : ℕ),
  sizeOf { map := map, next := next } = 1 + sizeOf map + sizeOf next
-- Mathlib.CategoryTheory.Triangulated.Subcategory
/-- An object `X` satisfies `extensionProduct P Q` if there exists a distinguished triangle
`Y ⟶ X ⟶ Z ⟶ Y⟦1⟧` such that `Y` satisfies `P` and `Z` satisfies `Q`.  -/
CategoryTheory.ObjectProperty.extensionProduct : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} 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] →
            [CategoryTheory.Pretriangulated C] →
              CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C
-- Mathlib.Data.Prod.Basic
Prod.total_right : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [Std.Trichotomous r] [Std.Total s],
  Std.Total (Prod.Lex r s)
-- Mathlib.Order.Hom.CompleteLattice
/-- `CompleteLatticeHomClass F α β` states that `F` is a type of complete lattice morphisms.

You should extend this class when you extend `CompleteLatticeHom`.  -/
CompleteLatticeHomClass : (F : Type u_8) → (α : Type u_9) → (β : Type u_10) → [CompleteLattice α] → [CompleteLattice β] → [FunLike F α β] → Prop
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  [inst_3 : Inhabited α] {k k' : α} {f : β k → β k},
  m.WF → (m.modify k f).getKey! k' = if (k == k') = true then if k ∈ m then k else default else m.getKey! k'
-- Init.Data.String.Modify
/-- Replaces the character at a specified position in a string with a new character.

If both the replacement character and the replaced character are 7-bit ASCII characters and the
string is not shared, then it is updated in-place and not copied.

Examples:
* `("abc".pos ⟨1⟩ (by decide)).set 'B' (by decide) = "aBc"`
* `("L∃∀N".pos ⟨4⟩ (by decide)).set 'X' (by decide) = "L∃XN"`
 -/
String.Pos.set : {s : String} → (p : s.Pos) → Char → p ≠ s.endPos → String
-- Mathlib.Computability.TuringMachine.Config
/-- In order to extract a compositional semantics from the sequential execution behavior of
configurations, we observe that continuations have a monoid structure, with `Cont.halt` as the unit
and `Cont.then` as the multiplication. `Cont.then k₁ k₂` runs `k₁` until it halts, and then takes
the result of `k₁` and passes it to `k₂`.

We will not prove it is associative (although it is), but we are instead interested in the
associativity law `k₂ (eval c k₁) = eval c (k₁.then k₂)`. This holds at both the sequential and
compositional levels, and allows us to express running a machine without the ambient continuation
and relate it to the original machine's evaluation steps. In the literature this is usually
where one uses Turing machines embedded inside other Turing machines, but this approach allows us
to avoid changing the ambient type `Cfg` in the middle of the recursion.
 -/
Turing.ToPartrec.Cont.then : Turing.ToPartrec.Cont → Turing.ToPartrec.Cont → Turing.ToPartrec.Cont
-- Init.Data.SInt.Bitwise
Int32.toBitVec_not : ∀ {a : Int32}, (~~~a).toBitVec = ~~~a.toBitVec
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.labellingCostarEquiv_symm_apply_fst : ∀ {V : Type u_1} {M : Type u_2} [inst : Group M] [inst_1 : MulAction M V] {S : Type u_3} (ι : S → M)
  (x : Quiver.SchreierGraph V ι) (x_1 : Quiver.Costar (Quiver.SingleObj.star S)),
  ((Quiver.SchreierGraph.labellingCostarEquiv ι x).symm x_1).fst = (ι x_1.snd)⁻¹ • x
-- Mathlib.Tactic.MoveAdd
/-- `move_oper op [a]` repeatedly moves `a` to the far right hand side in applications of `op`.
Here the constant `op` refers to a binary associative commutative operation, and `a` is any term
(potentially with underscores).

If `a` contains underscores, they are filled in by unification with the first matching occurrence.
Subterms with different values for the underscores are not matched, unless you repeat `a`.

Currently, `move_oper` supports the operators `HAdd.hAdd` (`· + ·`), `HMul.hMul` (`· * ·`),
`And` (`· ∧ ·`), `Or` (`· ∨ ·`), `Max.max` and `Min.min`. To support more operations, add them to
`Mathlib.MoveAdd.moveOperSimpCtx`.

* `move_add [...]` uses addition as the operation: it abbreviates `move_oper HAdd.add [...]`.
* `move_mul [...]` uses multiplication as the operation: it abbreviates `move_oper HMul.mul [...]`.
* `move_oper op [← a]` moves the atoms matching `a` to the far left hand side instead of the right.
* `move_oper op [a, b, ← c, ← d, ...]` moves multiple atoms simultaneously, in the order indicated
  by the arguments: `c` will appear to the left of `d` and `a` will appear to the left of `b`.
 -/
Mathlib.MoveAdd.tacticMove_mul_ : Lean.ParserDescr
-- Aesop.Search.Queue
Aesop.LIFOQueue.mk.injEq : ∀ (goals goals_1 : Array Aesop.GoalRef), ({ goals := goals } = { goals := goals_1 }) = (goals = goals_1)
-- Mathlib.Topology.Connected.Basic
Set.Subsingleton.isPreconnected : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, s.Subsingleton → IsPreconnected s
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SupSet α] [inst_1 : SupSet β] [inst_2 : SupSet γ]
  (g : sSupHom β γ) (f : sSupHom α β), sSupHom.dual (g.comp f) = (sSupHom.dual g).comp (sSupHom.dual f)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.instInfSet : (M : Type u_1) → [inst : MulOneClass M] → InfSet (SaturatedSubmonoid M)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- The strong transformation of oplax functors induced by a strong transformation of
pseudofunctors.  -/
CategoryTheory.Pseudofunctor.StrongTrans.toOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          F.StrongTrans G → CategoryTheory.Oplax.StrongTrans F.toOplax G.toOplax
-- Mathlib.NumberTheory.NumberField.DirichletDensity
/-- The Dirichlet density of `S` is at most `1`.  -/
NumberField.Set.dirichletDensity_le_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))), NumberField.Set.dirichletDensity S ≤ 1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
/-- denotes `e + o` where `o` is expression definitionally equal to `n`  -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.NatOffset.offset : Lean.Expr → Lean.Expr → ℕ → Nat.NatOffset✝
-- Mathlib.Order.Interval.Finset.Defs
Prod.instLocallyFiniteOrder : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [LocallyFiniteOrder α] → [LocallyFiniteOrder β] → [DecidableLE (α × β)] → LocallyFiniteOrder (α × β)
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.strictWidthInfty_mem_strictPeriods : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)), 𝒢.strictWidthInfty ∈ 𝒢.strictPeriods
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.instCategory : CategoryTheory.Category.{u, u + 1} AddSemigrp
-- Mathlib.Data.Finset.Basic
Finset.erase_cons : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α} (h : a ∉ s), (Finset.cons a s h).erase a = s
-- Init.Data.Rat.Lemmas
Rat.sub_right_le_iff_le_add : ∀ {a b c : ℚ}, a - c ≤ b ↔ a ≤ b + c
-- Mathlib.Topology.Algebra.Module.Basic
/-- Let `R` be a topological ring such that zero is not an isolated point (e.g., a nontrivially
normed field, see `NormedField.punctured_nhds_neBot`). Let `M` be a nontrivial module over `R`
such that `c • x = 0` implies `c = 0 ∨ x = 0`. Then `M` has no isolated points. We formulate this
using `NeBot (𝓝[≠] x)`.

This lemma is not an instance because Lean would need to find `[ContinuousSMul ?m_1 M]` with
unknown `?m_1`. We register this as an instance for `R = ℝ` in `Real.punctured_nhds_module_neBot`.
One can also use `haveI := Module.punctured_nhds_neBot R M` in a proof.
 -/
Module.punctured_nhds_neBot : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] [ContinuousAdd M] [inst_5 : Module R M] [ContinuousSMul R M] [IsDomain R] [Nontrivial M]
  [(nhdsWithin 0 {0}ᶜ).NeBot] [Module.IsTorsionFree R M] (x : M), (nhdsWithin x {x}ᶜ).NeBot
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.StronglyAdapted.upcrossingStrat : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0},
  MeasureTheory.StronglyAdapted ℱ f → MeasureTheory.StronglyAdapted ℱ (MeasureTheory.upcrossingStrat a b f N)
-- Mathlib.Data.Finsupp.Basic
/-- A version of `Finsupp.comapDomain_add` that's easier to use.  -/
Finsupp.comapDomain_add_of_injective : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddZeroClass M] {f : α → β} (hf : Function.Injective f)
  (v₁ v₂ : β →₀ M), Finsupp.comapDomain f (v₁ + v₂) ⋯ = Finsupp.comapDomain f v₁ ⋯ + Finsupp.comapDomain f v₂ ⋯
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.associativity_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z))
        (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (F.obj Z)))
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_union_Ico_eq_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ≤ b → b ≤ c → Set.Ico a b ∪ Set.Ico b c = Set.Ico a c
-- Std.Time.Date.Basic
/-- Convert `Minute.Offset` into `Day.Offset`.
 -/
Std.Time.Minute.Offset.toDays : Std.Time.Minute.Offset → Std.Time.Day.Offset
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.fixedPoints.eq_1 : ∀ (M : Type u_1) (α : Type u_3) [inst : Monoid M] [inst_1 : MulAction M α],
  MulAction.fixedPoints M α = {a | ∀ (m : M), m • a = a}
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallySmall_isPresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {κ : Cardinal.{w}}
  [inst_1 : Fact κ.IsRegular],
  P.IsCardinalFilteredGenerator κ →
    ∀ [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [CategoryTheory.LocallySmall.{w, v, u} C],
      CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (CategoryTheory.isCardinalPresentable C κ)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddCancelMonoid : {α : Type u_1} → [AddCancelMonoid α] → AddCancelMonoid (Lex α)
-- Mathlib.Topology.Sober
/-- A generic point of a sober irreducible space.  -/
genericPoint : (α : Type u_1) → [inst : TopologicalSpace α] → [QuasiSober α] → [IrreducibleSpace α] → α
-- Lean.PrettyPrinter.Formatter
/-- Textual content of `stack` up to the first whitespace (not enclosed in an escaped ident). We assume that the textual
content of `stack` is modified only by `push` and `pushWhitespace`, so `leadWord` is adjusted there accordingly.  -/
Lean.PrettyPrinter.Formatter.State.leadWord : Lean.PrettyPrinter.Formatter.State → String
-- Mathlib.Topology.EMetricSpace.Defs
Metric.ordConnected_setOfPred_closedEBall_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) (s : Set α), {r | Metric.closedEBall x r ⊆ s}.OrdConnected
-- Mathlib.Data.Num.Lemmas
/-- This tactic tries to prove (in)equalities about `PosNum`s by transferring them to the `Nat` world
and then trying to call `simp`.
```lean
example (n : PosNum) (m : PosNum) : n ≤ n + m := by transfer
```
 -/
PosNum.transfer : Lean.ParserDescr
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_zero_index : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {h : α → M → N},
  Finsupp.prod 0 h = 1
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The canonical map `Φ.op.RightResolution X₂ → Φ.LeftResolution X₂`.  -/
CategoryTheory.LocalizerMorphism.RightResolution.unop : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂ᵒᵖ} → Φ.op.RightResolution X₂ → Φ.LeftResolution (Opposite.unop X₂)
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- Given `x : X`, `y : Y` and `s : S` such that `f x = s = g y`,
this is `Spec (κ(x) ⊗[κ(s)] κ(y)) ⟶ X ×ₛ Y`.  -/
AlgebraicGeometry.Scheme.Pullback.Triplet.SpecTensorTo : {X Y S : AlgebraicGeometry.Scheme} →
  {f : X ⟶ S} →
    {g : Y ⟶ S} →
      (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) →
        AlgebraicGeometry.Spec T.tensor ⟶ CategoryTheory.Limits.pullback f g
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF → ∀ {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (m.insertMany l)[k]! = m[k]!
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
/-- The polar coordinates open partial homeomorphism in `ℂ`, mapping `r (cos θ + I * sin θ)` to
`(r, θ)`. It is a homeomorphism between `ℂ - ℝ≤0` and `(0, +∞) × (-π, π)`.  -/
Complex.polarCoord : OpenPartialHomeomorph ℂ (ℝ × ℝ)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew_fst_eq_containsₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced)
  (a : α) (b : β a), (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew a b t htb).1 = t.containsₘ a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_modify : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Internal.Impl.Const.modify k f t).size = t.size
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.map_id_map : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {x y : F.CoGrothendieck}
  (f : x ⟶ y), (CategoryTheory.Pseudofunctor.CoGrothendieck.map (CategoryTheory.CategoryStruct.id F)).map f = f
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
commGroupAddCommGroupEquivalence_counitIso : commGroupAddCommGroupEquivalence.counitIso =
  CategoryTheory.Iso.refl (AddCommGrpCat.toCommGrp.comp CommGrpCat.toAddCommGrp)
-- Mathlib.Order.Bounds.Image
isLUB_pi : ∀ {α : Type u} {π : α → Type u_1} [inst : (a : α) → Preorder (π a)] {s : Set ((a : α) → π a)} {f : (a : α) → π a},
  IsLUB s f ↔ ∀ (a : α), IsLUB (Function.eval a '' s) (f a)
-- Mathlib.Order.Category.Semilat
/-- The underlying type of an inf-semilattice with a top element.  -/
SemilatInfCat.X : SemilatInfCat → Type u
-- Mathlib.Algebra.BigOperators.Finprod
/-- The product of the constant function `1` over any set equals `1`.  -/
finprod_mem_one : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (s : Set α), ∏ᶠ (i : α) (_ : i ∈ s), 1 = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.continuous_tan : Continuous fun x => Real.tan ↑x
-- Mathlib.CategoryTheory.Subobject.Comma
/-- Technical lemma for `quotientEquiv`.  -/
CategoryTheory.CostructuredArrow.unop_left_comp_ofMkLEMk_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} {A : CategoryTheory.CostructuredArrow S T}
  {P Q : (CategoryTheory.CostructuredArrow S T)ᵒᵖ} {f : P ⟶ Opposite.op A} {g : Q ⟶ Opposite.op A}
  [inst_2 : CategoryTheory.Mono f.unop.left.op] [inst_3 : CategoryTheory.Mono g.unop.left.op]
  (h : CategoryTheory.Subobject.mk f.unop.left.op ≤ CategoryTheory.Subobject.mk g.unop.left.op),
  CategoryTheory.CategoryStruct.comp g.unop.left
      (CategoryTheory.Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop =
    f.unop.left
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- A form of `map_ideal` that is easier to rewrite with.  -/
AlgebraicGeometry.Scheme.IdealSheafData.map_ideal' : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : Opposite.op ↑V ⟶ Opposite.op ↑U),
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.map h)) (I.ideal V) = I.ideal U
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.cochainComplex_d_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.ProjectiveResolution X) (n₁ n₂ : ℤ) (k₁ k₂ : ℕ)
  (h₁ : autoParam (-↑k₁ = n₁) CategoryTheory.ProjectiveResolution.cochainComplex_d._auto_1)
  (h₂ : autoParam (-↑k₂ = n₂) CategoryTheory.ProjectiveResolution.cochainComplex_d._auto_3) {Z : C}
  (h : R.cochainComplex.X n₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (R.cochainComplex.d n₁ n₂) h =
    CategoryTheory.CategoryStruct.comp (R.cochainComplexXIso n₁ k₁ ⋯).hom
      (CategoryTheory.CategoryStruct.comp (R.complex.d k₁ k₂)
        (CategoryTheory.CategoryStruct.comp (R.cochainComplexXIso n₂ k₂ ⋯).inv h))
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (f : ℕ → α → ENNReal),
  (∀ (n : ℕ), f n ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν) →
    ∀ (n : ℕ), ⨆ k, ⨆ (_ : k ≤ n), f k ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν
-- Init.Meta.Defs
/-- Extracts the components of a scientific numeric literal.

Returns a triple `(n, sign, e) : Nat × Bool × Nat`; the number's value is given by:

```
if sign then n * 10 ^ (-e) else n * 10 ^ e
```

Returns `(0, false, 0)` if the syntax is malformed.
 -/
Lean.TSyntax.getScientific : Lean.ScientificLit → ℕ × Bool × ℕ
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.exists_lt_mul : ∀ {b c : Ordinal.{u_4}} {P : Ordinal.{u_4} → Prop}, (∃ a < b * c, P a) ↔ ∃ q < c, ∃ r < b, P (b * q + r)
-- Init.Data.Array.Lemmas
Array.toList_mapM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m β} {xs : Array α},
  Array.toList <$> Array.mapM f xs = List.mapM f xs.toList
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.FVarSubst.map : Lean.Meta.FVarSubst → Lean.AssocList Lean.FVarId Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
/-- If a zero morphism is a kernel of `f`, then `f` is a monomorphism.  -/
CategoryTheory.NormalEpiCategory.mono_of_zero_kernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C]
  [CategoryTheory.IsNormalEpiCategory C] {X Y : C} (f : X ⟶ Y) (Z : C)
  (l : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι 0 ⋯)), CategoryTheory.Mono f