mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The short complex `E^n(f₁, f₂, f₃) ⟶ opZ^n(f₂, f₃) ⟶ H^{n+1}(f₁)` identifies
to the kernel sequence of the definition of the homology of the short
complex `shortComplex` as a kernel of `ShortComplex.fromOpcycles`.  -/
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (n₀ n₁ n₂ : ℤ) →
                      (hn₁ :
                          autoParam (n₀ + 1 = n₁)
                            CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso._auto_1) →
                        (hn₂ :
                            autoParam (n₁ + 1 = n₂)
                              CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso._auto_3) →
                          X.kernelSequenceOpcyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ≅
                            { X₁ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology,
                              X₂ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).opcycles,
                              X₃ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₃,
                              f := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homologyι,
                              g := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles, zero := ⋯ }
-- Mathlib.Order.Filter.Ultrafilter.Defs
Filter.le_iff_ultrafilter : ∀ {α : Type u} {f₁ f₂ : Filter α}, f₁ ≤ f₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ f₁ → ↑g ≤ f₂
-- Mathlib.Data.Nat.Factorization.Basic
/-- If `n` is a nonzero natural number and `p ≠ 1`, then there are natural numbers `e`
and `n'` such that `n'` is not divisible by `p` and `n = p^e * n'`.  -/
Nat.exists_eq_pow_mul_and_not_dvd : ∀ {n : ℕ}, n ≠ 0 → ∀ (p : ℕ), p ≠ 1 → ∃ e n', ¬p ∣ n' ∧ n = p ^ e * n'
-- Mathlib.Data.ENNReal.Inv
ENNReal.toNNReal_div : ∀ (a b : ENNReal), (a / b).toNNReal = a.toNNReal / b.toNNReal
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.eLpNorm_add_le : ∀ {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε]
  {p : ENNReal} {μ : MeasureTheory.Measure α} {f g : α → ε},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      1 ≤ p → MeasureTheory.eLpNorm (f + g) p μ ≤ MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.snd_exp : ∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [Algebra ℚ R] [Module ℚ M]
  [inst_4 : Module R M] [inst_5 : Module Rᵐᵒᵖ M] [inst_6 : IsCentralScalar R M] [inst_7 : TopologicalSpace R]
  [inst_8 : TopologicalSpace M] [inst_9 : IsTopologicalRing R] [inst_10 : IsTopologicalAddGroup M]
  [inst_11 : ContinuousSMul R M] [inst_12 : ContinuousSMul Rᵐᵒᵖ M] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M),
  (NormedSpace.exp x).snd = NormedSpace.exp x.fst • x.snd
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instOrderBot : {α : Type u_1} → [inst : TopologicalSpace α] → OrderBot (TopologicalSpace.CompactOpens α)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Left.pos_add_of_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [IsBotZeroClass α] [AddLeftMono α] {a : α},
  0 < a → ∀ (b : α), 0 < a + b
-- Std.Data.ExtTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the largest key.
 -/
Std.ExtTreeMap.maxKey : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → t ≠ ∅ → α
-- Mathlib.Order.Lattice
/-- Pointwise supremum of two monotone functions is a monotone function.  -/
Monotone.sup : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : SemilatticeSup β] {f g : α → β},
  Monotone f → Monotone g → Monotone (f ⊔ g)
-- Mathlib.NumberTheory.Chebyshev
_private.Mathlib.NumberTheory.Chebyshev.0.Chebyshev.psi_sub_theta_bounds : ∀ {x : ℝ},
  0 ≤ x →
    Chebyshev.psi x - Chebyshev.theta x ≤ Chebyshev.psi (x ^ 2⁻¹) + Chebyshev.psi (x ^ 3⁻¹) + Chebyshev.psi (x ^ 5⁻¹) ∧
      Chebyshev.psi (x ^ 2⁻¹) + Chebyshev.psi (x ^ 3⁻¹) + Chebyshev.psi (x ^ 7⁻¹) ≤ Chebyshev.psi x - Chebyshev.theta x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_eq_some_get! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)], a ∈ m → m.get? a = some (m.get! a)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_iff_forall_pos_lt_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a b : α},
  a ≤ b ↔ ∀ (ε : α), 0 < ε → a < b + ε
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.CostructuredArrow.hasColimit : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} {X : T}
  (F : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow G X))
  [i₁ : CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.CostructuredArrow.proj G X))]
  [i₂ : CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.CostructuredArrow.proj G X)) G],
  CategoryTheory.Limits.HasColimit F
-- Std.Time.Zoned.Database.TZdb
/-- Parses binary timezone data into zone rules based on a given timezone ID.
 -/
Std.Time.Database.TZdb.parseTZif : ByteArray → String → Except String Std.Time.TimeZone.ZoneRules
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- An induction principle for additive closure membership. If `p`
holds for `0` and all elements of `k`, and is preserved under addition and inverses, then `p`
holds for all elements of the additive closure of `k`.

See also `AddSubgroup.closure_induction_left` and `AddSubgroup.closure_induction_left` for
versions that only require showing `p` is preserved by addition by elements in `k`.  -/
AddSubgroup.closure_induction : ∀ {G : Type u_1} [inst : AddGroup G] {k : Set G} {p : (g : G) → g ∈ AddSubgroup.closure k → Prop},
  (∀ (x : G) (hx : x ∈ k), p x ⋯) →
    p 0 ⋯ →
      (∀ (x y : G) (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k), p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x : G) (hx : x ∈ AddSubgroup.closure k), p x hx → p (-x) ⋯) →
          ∀ {x : G} (hx : x ∈ AddSubgroup.closure k), p x hx
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
CategoryTheory.regularEpiCategoryOfNormalEpiCategory : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.IsNormalEpiCategory C], CategoryTheory.IsRegularEpiCategory C
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- If `t : LeftLift f (𝟙 c ≫ g)` is a Kan lift, then `t.ofIdComp : LeftLift f g` is also
a Kan lift.  -/
CategoryTheory.Bicategory.LeftLift.IsKan.ofIdComp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          (t :
              CategoryTheory.Bicategory.LeftLift f
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)) →
            t.IsKan → t.ofIdComp.IsKan
-- Lean.Meta.Tactic.LibrarySearch
Lean.Meta.LibrarySearch.instInhabitedDeclMod.default : Lean.Meta.LibrarySearch.DeclMod
-- Std.Time.Date.Unit.Week
/-- Convert `Week.Offset` into `Nanosecond.Offset`.
 -/
Std.Time.Week.Offset.toNanoseconds : Std.Time.Week.Offset → Std.Time.Nanosecond.Offset
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visitChild.match_1.eq_2 : ∀ (motive : Lean.Expr → Sort u_1) (mvarId : Lean.MVarId) (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a))
  (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (e : Lean.Expr) → motive e),
  (match Lean.Expr.mvar mvarId with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | e => h_7 e) =
    h_2 mvarId
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
/-- Base-changing the vector space of a clifford algebra is isomorphic as an A-algebra to
base-changing the clifford algebra itself; $<|Cℓ(A ⊗_R V, Q_A) ≅ A ⊗_R Cℓ(V, Q)<|$.

This is `CliffordAlgebra.toBaseChange` and `CliffordAlgebra.ofBaseChange` as an equivalence.  -/
CliffordAlgebra.equivBaseChange : {R : Type u_1} →
  (A : Type u_2) →
    {V : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R V] →
                [inst_5 : Invertible 2] →
                  (Q : QuadraticForm R V) →
                    CliffordAlgebra (QuadraticForm.baseChange A Q) ≃ₐ[A] TensorProduct R A (CliffordAlgebra Q)
-- Mathlib.Data.Sym.Basic
Sym.instIsEmptySucc : ∀ {α : Type u_1} (n : ℕ) [IsEmpty α], IsEmpty (Sym α n.succ)
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.mk.injEq : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {X : Type u_2}
  {Y : Type u_3} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y] (toFun : X → Y)
  (isAffineMap_toFun :
    autoParam (Convexity.IsAffineMap R toFun) Convexity.ConvexSpace.AffineMap.isAffineMap_toFun._autoParam)
  (toFun_1 : X → Y)
  (isAffineMap_toFun_1 :
    autoParam (Convexity.IsAffineMap R toFun_1) Convexity.ConvexSpace.AffineMap.isAffineMap_toFun._autoParam),
  ({ toFun := toFun, isAffineMap_toFun := isAffineMap_toFun } =
      { toFun := toFun_1, isAffineMap_toFun := isAffineMap_toFun_1 }) =
    (toFun = toFun_1)
-- Qq.AssertInstancesCommute
Qq.doElemAssumeInstancesCommute : Lean.ParserDescr
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.instMonoOfMkLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (f : A ⟶ B) [inst_1 : CategoryTheory.Mono f]
  (X : CategoryTheory.Subobject B) (h : CategoryTheory.Subobject.mk f ≤ X),
  CategoryTheory.Mono (CategoryTheory.Subobject.ofMkLE f X h)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instCancelMonoid : {α : Type u_1} → [CancelMonoid α] → CancelMonoid (Lex α)
-- Mathlib.Algebra.Quaternion
/-- The cardinality of the quaternions, as a set.  -/
Cardinal.mk_univ_quaternion : ∀ (R : Type u_1) [inst : Zero R] [inst_1 : One R] [inst_2 : Neg R], Cardinal.mk ↑Set.univ = Cardinal.mk R ^ 4
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(f, f) = 0` unless `deg f = 0`. Also see `resultant_self_eq_zero`.  -/
Polynomial.resultant_self : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R), f.resultant f = 0 ^ f.natDegree
-- Init.Data.List.Lemmas
List.tail?_append_of_ne_nil : ∀ {α : Type u_1} {l l' : List α}, l ≠ [] → (l ++ l').tail? = some (l.tail ++ l')
-- Std.Data.HashMap.Basic
/-- Hash maps.

This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
and an array of buckets, where each bucket is a linked list of key-value pairs. The number of buckets
is always a power of two. The hash map doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.

The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
avoid expensive copies.

The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if `a == b` implies `a = b`.

These hash maps contain a bundled well-formedness invariant, which means that they cannot
be used in nested inductive types. For these use cases, `Std.Data.HashMap.Raw` and
`Std.Data.HashMap.Raw.WF` unbundle the invariant from the hash map. When in doubt, prefer
`HashMap` over `HashMap.Raw`.

Dependent hash maps, in which keys may occur in their values' types, are available as
`Std.Data.DHashMap`.
 -/
Std.HashMap : (α : Type u) → Type v → [BEq α] → [Hashable α] → Type (max u v)
-- Lean.Parser.Module
Lean.Parser.ModuleParserState.mk : String.Pos.Raw → Bool → Bool → Lean.Parser.ModuleParserState
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
StrongDual.toWeakDual_apply : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  (x' : StrongDual 𝕜 E) (y : E), (StrongDual.toWeakDual x') y = x' y
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
/-- If `f` is majorized with a negative exponent, then it tends to zero.  -/
Tactic.ComputeAsymptotics.Majorized.tendsto_zero_of_neg : ∀ {f b : ℝ → ℝ} {exp : ℝ},
  exp < 0 → Tactic.ComputeAsymptotics.Majorized f b exp → Filter.Tendsto f Filter.atTop (nhds 0)
-- Mathlib.Data.Prod.Lex
Prod.Lex.toLex_ge_toLex : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LE β] {x y : α × β},
  toLex y ≤ toLex x ↔ y.1 < x.1 ∨ x.1 = y.1 ∧ y.2 ≤ x.2
-- Mathlib.Order.CompleteLattice.Basic
sSup_insert : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α}, sSup (insert a s) = a ⊔ sSup s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, t.isEmpty = true → (t.insertIfNew k v).minKey? = some k
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.finite_of_finite : ∀ {α : Type u_1} [Finite α] {M : Matroid α}, M.Finite
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.forIn_eq_forIn_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {α_1 : Type u_1} {init : α_1} {f : α → α_1 → m (ForInStep α_1)}
  [inst : Monad m] [LawfulMonad m] {t : RBTree.RBNode α}, forIn t init f = forIn t.toList init f
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.EditableDocumentCore.mk.sizeOf_spec : ∀ («meta» : Lean.Server.DocumentMeta) (initSnap : Lean.Language.Lean.InitialSnapshot)
  (cmdSnaps : Lean.AsyncList IO.Error Lean.Server.Snapshots.Snapshot)
  (diagnosticsMutex : Std.Mutex Lean.Server.FileWorker.DiagnosticsState),
  sizeOf { «meta» := «meta», initSnap := initSnap, cmdSnaps := cmdSnaps, diagnosticsMutex := diagnosticsMutex } =
    1 + sizeOf «meta» + sizeOf initSnap + sizeOf cmdSnaps + sizeOf diagnosticsMutex
-- Mathlib.RingTheory.Ideal.Maps
/-- For a maximal ideal `p` of `R`, `p` extended to `S` and restricted back to `R` is `p` if
its image in `S` is not equal to `⊤`.
 -/
Ideal.comap_map_eq_self_of_isMaximal : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) {p : Ideal R}
  [hP' : p.IsMaximal], Ideal.map f p ≠ ⊤ → Ideal.comap f (Ideal.map f p) = p
-- Lean.Elab.App
Lean.Elab.Term.elabExplicitUniv : Lean.Elab.Term.TermElab
-- Init.Data.UInt.Lemmas
UInt16.toNat_mod_uInt64Size : ∀ (n : UInt16), n.toNat % UInt64.size = n.toNat
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The action by a subalgebra is the action by the underlying algebra.  -/
Subalgebra.moduleLeft : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {α : Type u_1} → [inst_3 : AddCommMonoid α] → [Module A α] → (S : Subalgebra R A) → Module (↥S) α
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Array index of a `Trie α` in the `tries` of a `RefinedDiscrTree`.  -/
Lean.Meta.RefinedDiscrTree.TrieIndex : Type
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_sdiff_Ico_right : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] (a b c : α),
  Finset.Ico a b \ Finset.Ico c b = Finset.Ico a (min b c)
-- Mathlib.Order.Filter.Bases.Basic
Filter.asBasis_filter : ∀ {α : Type u_1} (f : Filter α), f.asBasis.filter = f
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.map_sym_eq_piAntidiag : ∀ {ι : Type u_1} [inst : DecidableEq ι] (s : Finset ι) (n : ℕ),
  Finset.map { toFun := fun m a => Multiset.count a ↑m, inj' := ⋯ } (s.sym n) = s.piAntidiag n
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
/-- If `f : X ⟶ Y` is universally closed and `Y` is affine,
then the map on global sections is integral.  -/
AlgebraicGeometry.isIntegral_appTop_of_universallyClosed : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.UniversallyClosed f] [AlgebraicGeometry.IsAffine Y],
  (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)).IsIntegral
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.forIn.visit.match_1.eq_2 : ∀ {α : Type u_1} {σ : Type u_3} (motive : RBTree.RBNode α → σ → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α)
  (v : α) (r : RBTree.RBNode α) (b : σ) (h_1 : (b : σ) → motive RBTree.RBNode.nil b)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → (b : σ) → motive (RBTree.RBNode.node c l v r) b),
  (match RBTree.RBNode.node c l v r, b with
    | RBTree.RBNode.nil, b => h_1 b
    | RBTree.RBNode.node c l v r, b => h_2 c l v r b) =
    h_2 c l v r b
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
instHasEnoughRootsOfUnityCircle : ∀ (n : ℕ) [NeZero n], HasEnoughRootsOfUnity Circle n
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.not_disjoint_of_mem_mem : ∀ {α : Type u_1} {β : Type u_2} {x : α} {G H : Graph α β}, x ∈ G.vertexSet → x ∈ H.vertexSet → ¬Disjoint G H
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorAdd_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (a b n : ℤ),
  ((CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n = (HomologicalComplex.XIsoOfEq K ⋯).hom
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.evalIdentKey : Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `AddCommGroup.torsion_eq_torsion_addSubmonoid`.

---

The torsion additive submonoid of an abelian group equals the torsion
additive subgroup as an additive submonoid.  -/
AddCommGroup.add_torsion_eq_add_torsion_submonoid : ∀ (G : Type u_1) [inst : AddCommGroup G], AddCommMonoid.addTorsion G = (AddCommGroup.torsion G).toAddSubmonoid
-- Aesop.Search.Expansion.Simp
Aesop.SimpResult.unchanged : Aesop.SimpResult
-- Mathlib.Data.Int.Log
/-- `Int.clog b` and `zpow b` (almost) form a Galois connection.  -/
Int.zpow_lt_iff_lt_clog : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ}, 1 < b → ∀ {x : ℤ} {r : R}, 0 < r → (↑b ^ x < r ↔ x < Int.clog b r)
-- Lean.Declaration
Lean.instBEqDefinitionVal : BEq Lean.DefinitionVal
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
/-- The equalizer cone for a parallel pair of morphisms of seminormed groups.  -/
SemiNormedGrp.fork : {V W : SemiNormedGrp} → (f g : V ⟶ W) → CategoryTheory.Limits.Fork f g
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
BoxIntegral.Box.coe_ae_eq_Icc : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) [inst : Fintype ι], ↑I =ᵐ[MeasureTheory.volume] BoxIntegral.Box.Icc I
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_insertManyIfNewUnit!_list_le : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t.WF → ∀ {l : List α}, (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).size ≤ t.size + l.length
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.WellFormedBasis.single : ∀ (f : ℝ → ℝ), Filter.Tendsto f Filter.atTop Filter.atTop → Tactic.ComputeAsymptotics.WellFormedBasis [f]
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepFun.eq_1 : ∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  {β : Type u_3} {γ : Type u_4} [inst_1 : MeasurableSpace β] [inst_2 : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ)
  (μ : MeasureTheory.Measure Ω) [inst_3 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.CondIndepFun m' hm' f g μ =
    ProbabilityTheory.Kernel.IndepFun f g (ProbabilityTheory.condExpKernel μ m') (μ.trim hm')
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.aevalAevalEquiv_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (xy : A × A),
  (Polynomial.aevalAevalEquiv R A) xy = Polynomial.aevalAeval xy.1 xy.2
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_eq_zero_iff : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω},
  s.Finite → ((ProbabilityTheory.uniformOn s) t = 0 ↔ s ∩ t = ∅)
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.nth_cont_eq_succ_nth_contAux : ∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K], g.conts n = g.contsAux (n + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_isoBot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (c : CategoryTheory.TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'),
  (c.ofArrowIso e).isoBot = c.isoBot ≪≫ CategoryTheory.Arrow.leftFunc.mapIso e
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.y_pos_of_mem_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {D : ℝ} {x : E},
  0 < D → D < 1 → x ∈ Metric.ball 0 (1 + D) → 0 < ExistsContDiffBumpBase.y D x
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.lift_openEmbedding_symm_target : ∀ {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace X']
  [inst_2 : TopologicalSpace Z] [inst_3 : Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z)
  (hf : Topology.IsOpenEmbedding f), (e.lift_openEmbedding hf).symm.target = f '' e.source
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.mk.sizeOf_spec : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} [inst_9 : SizeOf ι] [inst_10 : SizeOf R] [inst_11 : SizeOf M]
  [inst_12 : SizeOf N] [inst_13 : SizeOf ι₂] [inst_14 : SizeOf M₂] [inst_15 : SizeOf N₂] (weightMap : M →ₗ[R] M₂)
  (coweightMap : N₂ →ₗ[R] N) (indexEquiv : ι ≃ ι₂)
  (weight_coweight_transpose : weightMap.dualMap ∘ₗ ↑Q.flip.toPerfPair = ↑P.flip.toPerfPair ∘ₗ coweightMap)
  (root_weightMap : ⇑weightMap ∘ ⇑P.root = ⇑Q.root ∘ ⇑indexEquiv)
  (coroot_coweightMap : ⇑coweightMap ∘ ⇑Q.coroot = ⇑P.coroot ∘ ⇑indexEquiv.symm),
  sizeOf
      { weightMap := weightMap, coweightMap := coweightMap, indexEquiv := indexEquiv,
        weight_coweight_transpose := weight_coweight_transpose, root_weightMap := root_weightMap,
        coroot_coweightMap := coroot_coweightMap } =
    1 + sizeOf weightMap + sizeOf coweightMap + sizeOf indexEquiv + sizeOf weight_coweight_transpose +
        sizeOf root_weightMap +
      sizeOf coroot_coweightMap