mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.category_id_right : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'),
  (CategoryTheory.CategoryStruct.id ψ).right = CategoryTheory.CategoryStruct.id ψ.right
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_iInf : ∀ {ι : Sort u_1} {R : Type u_2} [inst : NonAssocSemiring R] (S : ι → Subsemiring R), (iInf S).op = ⨅ i, (S i).op
-- Init.Data.Nat.ToString
Nat.six_eq_digitChar : ∀ {n : ℕ}, '6' = n.digitChar ↔ n = 6
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.eq_of_xn_modEq_le : ∀ {a : ℕ} (a1 : 1 < a) {i j n : ℕ},
  i ≤ j → j ≤ 2 * n → Pell.xn a1 i ≡ Pell.xn a1 j [MOD Pell.xn a1 n] → ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2) → i = j
-- Mathlib.RingTheory.WittVector.Defs
/-- An auxiliary definition used in `WittVector.eval`.
Evaluates a polynomial whose variables come from the disjoint union of `k` copies of `ℕ`,
with a curried evaluation `x`.
This can be defined more generally but we use only a specific instance here.  -/
WittVector.peval : {R : Type u_1} → [CommRing R] → {k : ℕ} → MvPolynomial (Fin k × ℕ) ℤ → (Fin k → ℕ → R) → R
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_add : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R) (n : ℕ), (p + q).coeff n = p.coeff n + q.coeff n
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- A parallelepiped can be expressed on the standard basis.  -/
Module.Basis.parallelepiped_eq_map : ∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  (b : Module.Basis ι ℝ E),
  b.parallelepiped =
    TopologicalSpace.PositiveCompacts.map ⇑b.equivFun.symm ⋯ ⋯ (TopologicalSpace.PositiveCompacts.piIcc01 ι)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {km : α}, t.minKey? = some km → t.getKey! km = km
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub_zsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + m
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Pullback of a pre-`0`-hypercover along a morphism. The components are `pullback f (E.f i)`.  -/
CategoryTheory.PreZeroHypercover.pullback₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S T : C} →
      (f : S ⟶ T) →
        (E : CategoryTheory.PreZeroHypercover T) →
          [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] → CategoryTheory.PreZeroHypercover S
-- Lean.Meta.Hint
/-- Automatically select diff granularity based on edit distance.  -/
Lean.Meta.Hint.DiffGranularity.auto : Lean.Meta.Hint.DiffGranularity
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsTree.dist_eq_dist_add_one_of_adj : ∀ {V : Type u_1} {G : SimpleGraph V},
  G.IsTree → ∀ (u : V) {v w : V}, G.Adj v w → G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- If `f = g`, then base change along `f` is naturally isomorphic to base change along `g`.  -/
CategoryTheory.MorphismProperty.Over.pullbackCongr : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      [inst_1 : Q.IsMultiplicative] →
        {X Y : T} →
          {f : X ⟶ Y} →
            [inst_2 : P.HasPullbacksAlong f] →
              [inst_3 : P.IsStableUnderBaseChangeAlong f] →
                [inst_4 : Q.IsStableUnderBaseChange] →
                  {g : X ⟶ Y} →
                    (h : f = g) →
                      CategoryTheory.MorphismProperty.Over.pullback P Q f ≅
                        CategoryTheory.MorphismProperty.Over.pullback P Q g
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.AbsolutelyContinuous.zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
  (v : MeasureTheory.VectorMeasure α N), MeasureTheory.VectorMeasure.AbsolutelyContinuous 0 v
-- Mathlib.Analysis.Complex.OperatorNorm
/-- The determinant of `conjLIE`, as a linear map.  -/
Complex.det_conjLIE : LinearMap.det ↑Complex.conjLIE.toLinearEquiv = -1
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.widget.injEq : ∀ (wi : Lean.Widget.WidgetInstance) (alt : Lean.Widget.TaggedText Lean.Widget.MsgEmbed)
  (wi_1 : Lean.Widget.WidgetInstance) (alt_1 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed),
  (Lean.Widget.MsgEmbed.widget wi alt = Lean.Widget.MsgEmbed.widget wi_1 alt_1) = (wi = wi_1 ∧ alt = alt_1)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_eq_iff_eq_add_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → (a - b = c ↔ a = c + b)
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_lt_iff_lt : ∀ {a b : BitVec 64}, { toBitVec := a } < { toBitVec := b } ↔ a < b
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.projectMapAux.eq_6 : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (x : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f (CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom x) =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.projectObj f x)).hom
-- Init.System.ST
ST.bind : {σ α β : Type} → ST σ α → (α → ST σ β) → ST σ β
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instNonUnitalSemiringOfMulOpposite : {M : Type u_1} → [NonUnitalSemiring Mᵐᵒᵖ] → NonUnitalSemiring Mᵈᵐᵃ
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.bifunctorComp₂₃Iso_hom_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {C₂₃ : Type u_5} {E : Type u_9}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] [inst_3 : CategoryTheory.Category.{v_5, u_5} C₂₃]
  [inst_4 : CategoryTheory.Category.{v_9, u_9} E] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ E))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) (X : C₁) (X_1 : C₂) (X_2 : C₃),
  (((F.bifunctorComp₂₃Iso G₂₃).hom.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id ((F.obj X).obj ((G₂₃.obj X_1).obj X_2))
-- Init.Data.Vector.Lemmas
Vector.any_flatMap : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {xs : Vector α n} {f : α → Vector β m} {p : β → Bool},
  (xs.flatMap f).any p = xs.any fun a => (f a).any p
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.symm_trans_self : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N), e.symm.trans e = ContinuousMulEquiv.refl N
-- Mathlib.Algebra.Order.Module.Defs
/-- Typeclass for reverse monotonicity of scalar multiplication by positive elements on the left,
namely `a • b₁ ≤ a • b₂ → b₁ ≤ b₂` if `0 < a`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedModule`.  -/
PosSMulReflectLE : (α : Type u_1) → (β : Type u_2) → [SMul α β] → [Preorder α] → [Preorder β] → [Zero α] → Prop
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.foldr_eq_foldr : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type u_1} {f : (a : α) → β a → δ → δ}
  {init : δ}, Std.DTreeMap.Internal.Impl.foldr f init t = List.foldr (fun p acc => f p.fst p.snd acc) init t.toListModel
-- Init.Data.Range.Polymorphic.SInt
Int32.instRxcHasSize : Std.Rxc.HasSize Int32
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.leadingCoeff_ne_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R},
  x.leadingCoeff ≠ 0 ↔ x ≠ 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryGE!_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} [inst : Inhabited (α × β)],
          Std.DTreeMap.Internal.Impl.Const.getEntryGE! k t₁ = Std.DTreeMap.Internal.Impl.Const.getEntryGE! k t₂
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_toFinsupp : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.toFinsupp.coeff.support = p.support
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Over.w_assoc : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Over Q X} (f : A ⟶ B) {Z : T}
  (h : (CategoryTheory.Functor.fromPUnit X).obj B.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp f.left (CategoryTheory.CategoryStruct.comp B.hom h) =
    CategoryTheory.CategoryStruct.comp A.hom h
-- Mathlib.Data.Part
Part.add_def : ∀ {α : Type u_1} [inst : Add α] (a b : Part α),
  a + b = do
    let y ← a
    Part.map (fun x => y + x) b
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.instIsIsoSymmetryOfFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [inst_2 : F.Full] [F.Faithful],
  CategoryTheory.IsIso (hf'.symmetry hg)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_prodMap : ∀ {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {P₄ : Type u_14} {V₁ : Type u_15} {V₂ : Type u_16}
  {V₃ : Type u_17} {V₄ : Type u_18} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂]
  [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : TopologicalSpace P₃] [inst_13 : AddCommGroup V₄] [inst_14 : Module k V₄]
  [inst_15 : AddTorsor V₄ P₄] [inst_16 : TopologicalSpace P₄] (f : P₁ →ᴬ[k] P₂) (g : P₃ →ᴬ[k] P₄),
  ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
-- Mathlib.Algebra.BigOperators.Finprod
/-- For finite sets, multiplication commutes with `finsum_mem`. See `finsum_mem_mul'` for a statement
assuming finiteness of support.
 -/
finsum_mem_mul' : ∀ {α : Type u_1} {R : Type u_7} [inst : NonUnitalNonAssocSemiring R] {s : Set α} (f : α → R) (r : R),
  s.Finite → (∑ᶠ (a : α) (_ : a ∈ s), f a) * r = ∑ᶠ (a : α) (_ : a ∈ s), f a * r
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapIsometry_apply_carrier : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : X ≃ᵢ Y) (D : Delone.DeloneSet X),
  ((Delone.DeloneSet.mapIsometry f) D).carrier = ⇑f '' D.carrier
-- Mathlib.Algebra.DirectSum.Decomposition
/-- Noncomputably conjure a decomposition instance from a `DirectSum.IsInternal` proof.  -/
DirectSum.IsInternal.chooseDecomposition : {ι : Type u_1} →
  {M : Type u_3} →
    {σ : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : SetLike σ M] →
            [inst_3 : AddSubmonoidClass σ M] → (ℳ : ι → σ) → DirectSum.IsInternal ℳ → DirectSum.Decomposition ℳ
-- Mathlib.MeasureTheory.Function.Egorov
/-- Egorov's theorem for finite measure spaces.  -/
MeasureTheory.tendstoUniformlyOn_of_ae_tendsto' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} [inst_1 : SemilatticeSup ι] [Nonempty ι] [Countable ι] {f : ι → α → β} {g : α → β}
  [MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) →
    MeasureTheory.StronglyMeasurable g →
      (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
        ∀ {ε : ℝ}, 0 < ε → ∃ t, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g Filter.atTop tᶜ
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.isCyclicallyReduced_cons_append_iff : ∀ {α : Type u} {L : List (α × Bool)} {a b : α × Bool},
  FreeAddGroup.IsCyclicallyReduced (b :: L ++ [a]) ↔ FreeAddGroup.IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)
-- Mathlib.Analysis.Calculus.Deriv.Add
differentiableAt_iff_comp_const_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜},
  DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x => f (b + x)) (-b + a)
-- Mathlib.SetTheory.Ordinal.Notation
/-- Print an ordinal notation  -/
ONote.toString : ONote → String
-- Mathlib.Order.SuccPred.Archimedean
antitone_of_le_pred : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : PredOrder α]
  [IsPredArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMin a → f a ≤ f (Order.pred a)) → Antitone f
-- Mathlib.Tactic.DepRewrite
/-- Check that casting `e : t` is allowed in the current mode.
(We don't need to know what type `e` is cast to:
we only check the sort of `t`, and it cannot change.)  -/
Mathlib.Tactic.DepRewrite.checkCastAllowed : Lean.Expr → Lean.Expr → Mathlib.Tactic.DepRewrite.CastMode → Lean.MetaM Unit
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.frobeniusRotation.congr_simp : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  {a₁ a₁_1 : WittVector p k} (e_a₁ : a₁ = a₁_1) {a₂ a₂_1 : WittVector p k} (e_a₂ : a₂ = a₂_1) (ha₁ : a₁.coeff 0 ≠ 0)
  (ha₂ : a₂.coeff 0 ≠ 0), WittVector.frobeniusRotation p ha₁ ha₂ = WittVector.frobeniusRotation p ⋯ ⋯
-- Mathlib.Topology.NhdsWithin
mem_of_mem_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s t : Set α}, a ∈ s → t ∈ nhdsWithin a s → a ∈ t
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- When `g` is an isomorphism, the cokernel of `f ≫ g` is isomorphic to the cokernel of `f`.
 -/
CategoryTheory.Limits.cokernelCompIsIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y Z : C} →
        (f : X ⟶ Y) →
          (g : Y ⟶ Z) →
            [inst_2 : CategoryTheory.Limits.HasCokernel f] →
              [inst_3 : CategoryTheory.IsIso g] →
                CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp f g) ≅
                  CategoryTheory.Limits.cokernel f
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.coeff_subst_X_pow : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S] {k : ℕ},
  k ≠ 0 →
    ∀ (f : PowerSeries R) (n : ℕ),
      (PowerSeries.coeff n) (PowerSeries.subst (PowerSeries.X ^ k) f) =
        if k ∣ n then (algebraMap R S) ((PowerSeries.coeff (n / k)) f) else 0
-- Lean.Syntax
Lean.unreachIsNodeMissing : {β : Sort u_1} → Lean.IsNode Lean.Syntax.missing → β
-- Mathlib.Computability.Partrec
Nat.Partrec.zero : Nat.Partrec (pure 0)
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionDisabled.mk.injEq : ∀ (reason reason_1 : String), ({ reason := reason } = { reason := reason_1 }) = (reason = reason_1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
instNonUnitalClosedEmbeddingContinuousFunctionalCalculusOfCompleteSpace : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : CommSemiring R] [inst_1 : Nontrivial R]
  [inst_2 : StarRing R] [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : NonUnitalRing A] [inst_7 : StarRing A] [inst_8 : MetricSpace A] [inst_9 : Module R A]
  [inst_10 : IsScalarTower R A A] [inst_11 : SMulCommClass R A A] [NonUnitalIsometricContinuousFunctionalCalculus R A p]
  [CompleteSpace R], NonUnitalClosedEmbeddingContinuousFunctionalCalculus R A p
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.toList_rcc : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.toList_rcc._auto_1)
  [Std.TransCmp cmp] {t : Std.DTreeMap.Raw α β cmp},
  t.WF →
    ∀ {lowerBound upperBound : α},
      Std.Slice.toList (Std.Rcc.Sliceable.mkSlice t lowerBound...=upperBound) =
        List.filter (fun e => decide ((cmp e.fst lowerBound).isGE = true ∧ (cmp e.fst upperBound).isLE = true)) t.toList
-- Mathlib.Algebra.Group.EvenFunction
/-- The sum of the values of an odd function is 0.  -/
Function.Odd.sum_eq_zero : ∀ {α : Type u_3} {β : Type u_4} [inst : AddCommGroup β] [IsAddTorsionFree β] [inst_2 : Fintype α]
  [inst_3 : InvolutiveNeg α] {f : α → β}, Function.Odd f → ∑ a, f a = 0
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.mem_sphere : ∀ {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 : EuclideanGeometry.Sphere P} {p : P} {as : AffineSubspace ℝ P},
  s.IsTangentAt p as → p ∈ s
-- Std.Time.Format.Modifier
/-- `m`: Minute of hour (e.g., 30).
 -/
Std.Time.Modifier.m : Std.Time.Number → Std.Time.Modifier
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.ensureNoUnassignedLevelMVarsAtInductives : Array Lean.Elab.Command.InductiveView → List Lean.InductiveType → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Group.Basic
add_zsmul_self : ∀ {G : Type u_3} [inst : AddGroup G] (a : G) (n : ℤ), a + n • a = (n + 1) • a
-- Plausible.Random
/-- Computes a `RandT m α` using the global `stdGenRef` as RNG.

Note that:
- `stdGenRef` is not necessarily properly seeded on program startup
  as of now and will therefore be deterministic.
- `stdGenRef` is not thread local, hence two threads accessing it
  at the same time will get the exact same generator.
 -/
Plausible.runRand : {m : Type → Type} → [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → {α : Type} → Plausible.RandT m α → m α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_filterMap_eq_size_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ},
  t.WF → ((Std.TreeMap.Raw.filterMap f t).size = t.size ↔ ∀ (a : α) (h : a ∈ t), (f (t.getKey a h) t[a]).isSome = true)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.eval_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type w} (b : β) (X : CategoryTheory.GradedObject β C),
  (CategoryTheory.GradedObject.eval b).obj X = X b
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
quasispectrum_imaginaryPart' : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [inst_6 : StarModule ℂ A]
  [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A),
  autoParam (IsStarNormal a) quasispectrum_imaginaryPart'._auto_1 →
    quasispectrum ℝ ↑(imaginaryPart a) = Complex.im '' quasispectrum ℂ a
-- Mathlib.Algebra.Star.Pointwise
Set.inter_star : ∀ {α : Type u_1} {s t : Set α} [inst : Star α], star (s ∩ t) = star s ∩ star t
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.toHomeomorph_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y),
  e.symm.toHomeomorph = e.toHomeomorph.symm
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.isEmbedding_toContinuousMap : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], Topology.IsEmbedding ContinuousMonoidHom.toContinuousMap
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.min_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : SemilatticeInf Y] [inst_2 : Zero Y]
  {D₁ D₂ : Function.locallyFinsuppWithin U Y} {x : X}, (D₁ ⊓ D₂) x = D₁ x ⊓ D₂ x
-- Init.Data.List.MapIdx
List.head_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : ℕ → α → β} {w : List.mapIdx f l ≠ []},
  (List.mapIdx f l).head w = f 0 (l.head ⋯)
-- Mathlib.Order.CompleteLattice.Defs
CompleteLinearOrder.mk : {α : Type u_8} →
  [toCompleteLattice : CompleteLattice α] →
    [toHImp : HImp α] →
      (∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c) →
        [toCompl : Compl α] →
          (∀ (a : α), a ⇨ ⊥ = aᶜ) →
            [toSDiff : SDiff α] →
              (∀ (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c) →
                [toHNot : HNot α] →
                  (∀ (a : α), ⊤ \ a = ￢a) →
                    [toOrd : Ord α] →
                      (∀ (a b : α), a ≤ b ∨ b ≤ a) →
                        DecidableLE α →
                          (toDecidableEq : DecidableEq α) →
                            (toDecidableLT : DecidableLT α) →
                              autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b)
                                  CompleteLinearOrder.compare_eq_compareOfLessAndEq._autoParam →
                                CompleteLinearOrder α
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.isLocallyInjective_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) (ψ : F₂ ⟶ F₃) [CategoryTheory.Presheaf.IsLocallyInjective J φ]
  [CategoryTheory.Presheaf.IsLocallyInjective J ψ],
  CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.CategoryStruct.comp φ ψ)
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.zsmul_vadd_eq_iff_period_dvd : ∀ {α : Type v} {G : Type u} [inst : AddGroup G] [inst_1 : AddAction G α] {j : ℤ} {g : G} {a : α},
  j • g +ᵥ a = a ↔ ↑(AddAction.period g a) ∣ j
-- Lean.PrettyPrinter
Lean.PrettyPrinter.registerParserCompilers : IO Unit
-- Mathlib.Algebra.Module.Bimodule
Subbimodule.coe_toSubbimoduleNat : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : Ring R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass R S M] (p : Submodule (TensorProduct ℤ R S) M),
  ↑(Subbimodule.toSubbimoduleNat R S M p) = ↑p
-- Mathlib.Algebra.Ring.ULift
ULift.nonAssocSemiring : {R : Type u} → [NonAssocSemiring R] → NonAssocSemiring (ULift.{u_1, u} R)
-- Mathlib.Algebra.Lie.Ideal
LieHom.ker_eq_bot : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L'), f.ker = ⊥ ↔ Function.Injective ⇑f
-- Mathlib.Data.Rat.Defs
Rat.monoid : Monoid ℚ
-- Mathlib.Algebra.Vertex.VertexOperator
VertexOperator.ncoeff.eq_1 : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  VertexOperator.ncoeff = { toFun := fun A n => HVertexOperator.coeff A (-n - 1), map_add' := ⋯, map_smul' := ⋯ }
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.addFalse.congr_simp : ∀ {aig : Std.Sat.AIG ℕ} (state : Std.Sat.AIG.toCNF.State✝ aig) (idx : ℕ) (h : idx < aig.decls.size)
  (htip : aig.decls[idx] = Std.Sat.AIG.Decl.false),
  Std.Sat.AIG.toCNF.State.addFalse✝ state idx h htip = Std.Sat.AIG.toCNF.State.addFalse✝ state idx h htip