mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Reflective.comparison_full : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {R : CategoryTheory.Functor D C} [R.Full] {L : CategoryTheory.Functor C D} (adj : L ⊣ R),
  (CategoryTheory.Monad.comparison adj).Full
-- Mathlib.Order.Partition.Finpartition
Finpartition.mem_part_ofSetSetoid_iff_rel : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Setoid α} (x : Finset α) [inst_1 : DecidableRel ⇑s] {b : α},
  b ∈ (Finpartition.ofSetSetoid s x).part a ↔ a ∈ x ∧ b ∈ x ∧ s a b
-- Mathlib.Probability.Process.LocalProperty
_private.Mathlib.Probability.Process.LocalProperty.0.ProbabilityTheory.isPreLocalizingSequence_of_isLocalizingSequence_aux : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : ConditionallyCompleteLinearOrderBot ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  {𝓕 : MeasureTheory.Filtration ι mΩ} [SecondCountableTopology ι] [MeasureTheory.IsFiniteMeasure P]
  {τ : ℕ → Ω → WithTop ι} {σ : ℕ → ℕ → Ω → WithTop ι},
  ProbabilityTheory.IsLocalizingSequence 𝓕 τ P →
    (∀ (n : ℕ), ProbabilityTheory.IsLocalizingSequence 𝓕 (σ n) P) →
      ∃ nk T,
        StrictMono nk ∧
          Filter.Tendsto T Filter.atTop Filter.atTop ∧
            ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.count_coe_nonneg : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (J : Ideal R),
  0 ≤ FractionalIdeal.count K v ↑J
-- Init.Data.UInt.Basic
/-- Converts word-sized unsigned integers to 32-bit unsigned integers. This cannot overflow because
`USize.size` is either `2^32` or `2^64`.

This function is overridden at runtime with an efficient implementation.
 -/
USize.toUInt64 : USize → UInt64
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedDecomposition.decompose'_eq : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : DecidableEq M],
  DirectSum.Decomposition.decompose' = fun φ =>
    (DirectSum.mk (fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i))
        (Finset.image (⇑(Finsupp.weight w)) φ.support))
      fun m => ⟨(MvPolynomial.weightedHomogeneousComponent w ↑m) φ, ⋯⟩
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.eq_append_of_dropPrefix?_string_eq_some : ∀ {pat : String} {s res : String.Slice}, s.dropPrefix? pat = some res → s.copy = pat ++ res.copy
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C),
  X.rightOpLeftOpIso.inv.right = CategoryTheory.CategoryStruct.id X.right
-- Init.Data.Vector.Lemmas
Vector.toArray_zipIdx : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} (k : optParam ℕ 0), (xs.zipIdx k).toArray = xs.toArray.zipIdx k
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.colimitCoconeComp_isColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (t : CategoryTheory.Limits.ColimitCocone G),
  (CategoryTheory.Functor.Final.colimitCoconeComp F t).isColimit =
    (CategoryTheory.Functor.Final.isColimitWhiskerEquiv F t.cocone).symm t.isColimit
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- The closure of a singleton `{a}` in the lower set topology is the right-closed left-infinite
interval $(-∞,a]$.
 -/
Topology.IsLowerSet.closure_singleton : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLowerSet α] {a : α},
  closure {a} = Set.Ici a
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_hom₂_nonempty : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P]
  {l : List ι} (f : M → N → P),
  (∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d) →
    ∀ (f₁ : ι → M) (f₂ : ι → N),
      l ≠ [] → (List.map (fun i => f (f₁ i) (f₂ i)) l).prod = f (List.map f₁ l).prod (List.map f₂ l).prod
-- Mathlib.Data.Vector3
/-- The empty vector  -/
Vector3.nil : {α : Type u_1} → Vector3 α 0
-- Mathlib.Algebra.Order.Field.Basic
/-- The `positivity` extension which identifies expressions of the form `a⁻¹`,
such that `positivity` successfully recognises `a`.  -/
Mathlib.Meta.Positivity.evalInv : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- Reinterpret an `AddSubgroup` as an `AddSubmonoid`.  -/
AddSubgroup.toAddSubmonoid : {G : Type u_3} → [inst : AddGroup G] → AddSubgroup G → AddSubmonoid G
-- Init.System.IO
allocprof : {α : Type} → String → IO α → IO α
-- Init.Data.SInt.Lemmas
Int32.not_maxValue_lt : ∀ {a : Int32}, ¬Int32.maxValue < a
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AccLevelState.mk.sizeOf_spec : ∀ (levels : Lean.LevelMap ℤ), sizeOf { levels := levels } = 1 + sizeOf levels
-- Mathlib.Testing.Plausible.Sampleable
Plausible.PNat.sampleableExt : Plausible.SampleableExt ℕ+
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (Y : CategoryTheory.Over X),
  CategoryTheory.Sieve.overEquiv Y =
    { toFun := CategoryTheory.Sieve.functorPushforward (CategoryTheory.Over.forget X),
      invFun := CategoryTheory.Sieve.functorPullback (CategoryTheory.Over.forget X), left_inv := ⋯, right_inv := ⋯,
      map_rel_iff' := ⋯ }
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_insert_le_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, (cmp (t.insert k).min! k).isLE = true
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.strictMono_rpow_of_pos : ∀ {z : ℝ}, 0 < z → StrictMono fun x => x ^ z
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.BinaryTree.toOrdNode.match_1.eq_2 : ∀ {α : Type u_1} (motive : BinaryTree α → Sort u_2) (x : α) (l r : BinaryTree α) (h_1 : Unit → motive BinaryTree.nil)
  (h_2 : (x : α) → (l r : BinaryTree α) → motive (BinaryTree.node x l r)),
  (match BinaryTree.node x l r with
    | BinaryTree.nil => h_1 ()
    | BinaryTree.node x l r => h_2 x l r) =
    h_2 x l r
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
/-- The multiplicative `v`-adic valuations on `K⟮S, n⟯` for all `v ∈ S`.  -/
IsDedekindDomain.selmerGroup.valuation : {R : Type u} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      {K : Type v} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              {S : Set (IsDedekindDomain.HeightOneSpectrum R)} →
                {n : ℕ} → ↥IsDedekindDomain.selmerGroup →* ↑S → Multiplicative (ZMod n)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEq.inj : ∀ {a b : Lean.Expr} {la lb : Lean.Meta.Grind.Arith.Linear.LinExpr} {a_1 b_1 : Lean.Expr}
  {la_1 lb_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEq a b la lb =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEq a_1 b_1 la_1 lb_1 →
    a = a_1 ∧ b = b_1 ∧ la = la_1 ∧ lb = lb_1
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsNonneg.mk : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {I₁ I₂ : R →+* R} [inst_3 : LE R] {B : M →ₛₗ[I₁] M →ₛₗ[I₂] R}, (∀ (x : M), 0 ≤ (B x) x) → B.IsNonneg
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.getJsxText : Lean.TSyntax `ProofWidgets.Jsx.jsxText → String
-- Mathlib.Analysis.BoxIntegral.Box.Basic
/-- A nontrivial rectangular box in `ι → ℝ` with corners `lower` and `upper`. Represents the product
of half-open intervals `(lower i, upper i]`.  -/
BoxIntegral.Box : Type u_2 → Type u_2
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
Returns `none` if `f` returns `none` for all outputs.

`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
iteration.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.findSome?` always terminates after finitely many steps.

Examples:
 * `[7, 6, 5, 8, 1, 2, 6].iter.findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
 * `[7, 6, 5, 8, 1, 2, 6].iter.findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
Std.Iter.findSome? : {α β : Type w} →
  {γ : Type x} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Iter β → (β → Option γ) → Option γ
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- `mem_tac` tries to prove goals of the form `x ∈ 𝒜 i` when `x` has the form of:
* `y ^ n` where `i = n • j` and `y ∈ 𝒜 j`.
* a natural number `n`.
 -/
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.tacticMem_tac : Lean.ParserDescr
-- Mathlib.Algebra.Group.EvenFunction
/-- If `f` is arbitrary and `g` is even, then `f ∘ g` is even.  -/
Function.Even.left_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] {γ : Type u_3} {g : α → β},
  Function.Even g → ∀ (f : β → γ), Function.Even (f ∘ g)
-- Mathlib.LinearAlgebra.LinearPMap
/-- Given two partial linear maps that agree on the intersection of their domains,
`f.sup g h` is the unique partial linear map on `f.domain ⊔ g.domain` that agrees
with `f` and `g`.  -/
LinearPMap.sup : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module S F] →
                      (f g : E →ₛₗ.[σ] F) → (∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y) → E →ₛₗ.[σ] F
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.ms_eq_mk_iff : ∀ {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)}
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl))
  (s : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) (f : ℝ → ℝ),
  ms = Tactic.ComputeAsymptotics.MultiseriesExpansion.mk s f ↔ ms.seq = s ∧ ms.toFun = f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.mkIso_hom_left : ∀ {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'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right)
  (base : ψ.base ≅ ψ'.base)
  (left_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
          (CategoryTheory.Functor.whiskerRight left.hom F') =
        CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom)
          (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
      CategoryTheory.Limits.CatCospanTransform.mkIso._auto_1)
  (right_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
          (CategoryTheory.Functor.whiskerRight right.hom G') =
        CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom)
          (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom)
      CategoryTheory.Limits.CatCospanTransform.mkIso._auto_3),
  (CategoryTheory.Limits.CatCospanTransform.mkIso left right base left_coherence right_coherence).hom.left = left.hom
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.lift'_mk : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : T0Space β] {f : α → β},
  UniformContinuous f → ∀ (a : α), SeparationQuotient.lift' f (SeparationQuotient.mk a) = f a
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.setRed.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (a : RBTree.RBNode α) (v : α)
  (b : RBTree.RBNode α)
  (h_1 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) → (v : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node c a v b))
  (h_2 : Unit → motive RBTree.RBNode.nil),
  (match RBTree.RBNode.node c a v b with
    | RBTree.RBNode.node c a v b => h_1 c a v b
    | RBTree.RBNode.nil => h_2 ()) =
    h_1 c a v b
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.eq_lift_neg_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj B] (f g h : A ⟶ B),
  f =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CartesianMonoidalCategory.lift
          (CategoryTheory.CategoryStruct.comp g CategoryTheory.AddGrpObj.neg) h)
        CategoryTheory.AddMonObj.add ↔
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g f)
        CategoryTheory.AddMonObj.add =
      h
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedAddSubgroup.instCoeAddSubgroup : (G : Type u) → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → Coe (ClosedAddSubgroup G) (AddSubgroup G)
-- Mathlib.Analysis.Seminorm
Seminorm.sSup_empty : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E], sSup ∅ = ⊥
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
CategoryTheory.FunctorToTypes.monoFactorisation_e : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.Functor C (Type u)} (f : F ⟶ G),
  (CategoryTheory.FunctorToTypes.monoFactorisation f).e = CategoryTheory.Subfunctor.toRange f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.all_eq_false_iff_exists_mem_getElem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α]
  {p : α → β → Bool}, m.WF → (m.all p = false ↔ ∃ a, ∃ (h : a ∈ m), p a m[a] = false)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.not_indep_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, autoParam (X ⊆ M.E) Matroid.not_indep_iff._auto_1 → (¬M.Indep X ↔ M.Dep X)
-- Init.Data.Array.Basic
/-- Returns a pair of arrays that together contain all the elements of `as`. The first array contains
those elements for which `p` returns `true`, and the second contains those for which `p` returns
`false`.

`as.partition p` is equivalent to `(as.filter p, as.filter (not ∘ p))`, but it is
more efficient since it only has to do one pass over the array.

Examples:
 * `#[1, 2, 5, 2, 7, 7].partition (· > 2) = (#[5, 7, 7], #[1, 2, 2])`
 * `#[1, 2, 5, 2, 7, 7].partition (fun _ => false) = (#[], #[1, 2, 5, 2, 7, 7])`
 * `#[1, 2, 5, 2, 7, 7].partition (fun _ => true) = (#[1, 2, 5, 2, 7, 7], #[])`
 -/
Array.partition : {α : Type u} → (α → Bool) → Array α → Array α × Array α
-- Mathlib.Algebra.Order.Group.Synonym
isAddRightRegular_ofColex : ∀ {α : Type u_1} [inst : AddMonoid α] {a : Colex α}, IsAddRightRegular (ofColex a) ↔ IsAddRightRegular a
-- Mathlib.AlgebraicGeometry.Scheme
/-- The induced map of a ring homomorphism on the ring spectra, as a morphism of schemes.  -/
AlgebraicGeometry.Spec.map : {R S : CommRingCat} → (R ⟶ S) → (AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec R)
-- Mathlib.Analysis.SpecialFunctions.CompareExp
/-- If `l : Filter ℂ` is an "exponential comparison filter", then for any complex `a₁`, `a₂` and any
integer `b₁ < b₂`, we have
`(fun z ↦ z ^ a₁ * exp (b₁ * z)) =o[l] (fun z ↦ z ^ a₂ * exp (b₂ * z))`.  -/
Complex.IsExpCmpFilter.isLittleO_zpow_mul_exp : ∀ {l : Filter ℂ} {b₁ b₂ : ℝ},
  Complex.IsExpCmpFilter l →
    b₁ < b₂ → ∀ (m n : ℤ), (fun z => z ^ m * Complex.exp (↑b₁ * z)) =o[l] fun z => z ^ n * Complex.exp (↑b₂ * z)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqExpr : BEq Lean.Grind.CommRing.Expr
-- Std.Http.Data.Body.Basic
Std.Http.Body.instToByteArrayString : Std.Http.Body.ToByteArray String
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- From a natural transformation `α : G → F` we get a functor from
algebras of `F` to algebras of `G`.
 -/
CategoryTheory.Endofunctor.Algebra.functorOfNatTrans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C C} →
      (G ⟶ F) → CategoryTheory.Functor (CategoryTheory.Endofunctor.Algebra F) (CategoryTheory.Endofunctor.Algebra G)
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
exists_continuous_add_one_of_isCompact_nnreal : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] {s₀ s₁ t : Set X},
  IsCompact s₀ →
    IsCompact s₁ →
      IsCompact t →
        Disjoint s₀ s₁ → s₀ ∪ s₁ ⊆ t → ∃ f₀ f₁, Set.EqOn (⇑f₀) 1 s₀ ∧ Set.EqOn (⇑f₁) 1 s₁ ∧ Set.EqOn (⇑(f₀ + f₁)) 1 t
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.decodeNum : (s : String) → s.Pos → Lean.Name → ℕ → Lean.Name
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_pos : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] {a : M},
  0 < a → ∀ {k : ℕ}, k ≠ 0 → 0 < k • a
-- Mathlib.Data.Setoid.Partition
IndexedPartition.piecewise_preimage : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {β : Type u_3} (f : ι → α → β) (t : Set β),
  hs.piecewise f ⁻¹' t = ⋃ i, s i ∩ f i ⁻¹' t
-- Mathlib.Computability.Primrec.Basic
/-- Calls the given function on a pair of entries `n`, encoded via the pairing function.  -/
Nat.unpaired : {α : Sort u_1} → (ℕ → ℕ → α) → ℕ → α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The `a₂` coefficient of a Weierstrass curve.  -/
WeierstrassCurve.a₂ : {R : Type u} → WeierstrassCurve R → R
-- Mathlib.FieldTheory.PurelyInseparable.Basic
finInsepDegree_eq_pow : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [ExpChar F q]
  [FiniteDimensional F E], ∃ n, Field.finInsepDegree F E = q ^ n
-- Mathlib.Algebra.Lie.Derivation.BaseChange
/-- A Lie derivation of an `R-`Lie algebra `L`, induces a Lie derivation of `A ⊗[R] L` for any
Algebra `A` over `R`.  -/
Lie.Derivation.ofLieDerivation : {R : Type u_1} →
  [inst : CommRing R] →
    (A : Type u_2) →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          {L : Type u_3} →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra R L] →
                LieDerivation R L L →ₗ⁅R⁆ LieDerivation R (TensorProduct R A L) (TensorProduct R A L)
-- Lean.Meta.LazyDiscrTree
/-- Evaluate all partial matches and add resulting matches to `MatchResult`.

The partial matches are stored in an array that is used as a stack. When adding
multiple partial matches to explore next, to ensure the order of results matches
user expectations, this code must add paths we want to prioritize and return
results earlier are added last.
 -/
Lean.Meta.LazyDiscrTree.getMatchLoop : {α : Type} →
  Array Lean.Meta.LazyDiscrTree.PartialMatch →
    Lean.Meta.LazyDiscrTree.MatchResult α → Lean.Meta.LazyDiscrTree.MatchM α (Lean.Meta.LazyDiscrTree.MatchResult α)
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.glue.eq_3 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hl_2 : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced) (sz' : ℕ) (k'_1 : α) (v'_1 : β k'_1)
  (l'' r'' : Std.DTreeMap.Internal.Impl α β) (hr_2 : (Std.DTreeMap.Internal.Impl.inner sz' k'_1 v'_1 l'' r'').Balanced)
  (hlr_3 :
    Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size
      (Std.DTreeMap.Internal.Impl.inner sz' k'_1 v'_1 l'' r'').size),
  (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').glue (Std.DTreeMap.Internal.Impl.inner sz' k'_1 v'_1 l'' r'') hl_2
      hr_2 hlr_3 =
    if size < sz' then
      match Std.DTreeMap.Internal.Impl.minView k'_1 v'_1 l'' r'' ⋯ ⋯ ⋯ with
      | { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } } =>
        Std.DTreeMap.Internal.Impl.balanceLErase dk dv (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') dt hl_2 ⋯ ⋯
    else
      match Std.DTreeMap.Internal.Impl.maxView k' v' l' r' ⋯ ⋯ ⋯ with
      | { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } } =>
        Std.DTreeMap.Internal.Impl.balanceRErase dk dv dt (Std.DTreeMap.Internal.Impl.inner sz' k'_1 v'_1 l'' r'') ⋯
          hr_2 ⋯
-- Mathlib.Data.Vector3
Fin2.insertPerm.eq_def : ∀ (x : ℕ) (x_1 x_2 : Fin2 x),
  x_1.insertPerm x_2 =
    match x, x_1, x_2 with
    | .(n + 1), Fin2.fz, Fin2.fz => Fin2.fz
    | .(n + 1), Fin2.fz, j.fs => j.fs
    | .(a.succ + 1), a_1.fs, Fin2.fz => Fin2.fz.fs
    | .(a.succ + 1), i.fs, j.fs =>
      match i.insertPerm j with
      | Fin2.fz => Fin2.fz
      | k.fs => k.fs.fs
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_ne_zero_iff : ∀ {x : EReal}, x.toENNReal ≠ 0 ↔ 0 < x
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instSemigroupOfMulHomClass.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → Semigroup (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)],
  DirectLimit.instSemigroupOfMulHomClass = { toMul := DirectLimit.instMul, mul_assoc := ⋯ }
-- Mathlib.NumberTheory.LSeries.SumCoeff
_private.Mathlib.NumberTheory.LSeries.SumCoeff.0.LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₂ : ∀ {l : ℂ} {s T ε : ℝ} {S : ℝ → ℂ},
  MeasureTheory.LocallyIntegrableOn (fun t => S t - l * ↑t) (Set.Ici 1) MeasureTheory.volume →
    0 < ε →
      1 < s →
        1 ≤ T → (∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t) → (s - 1) * ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε
-- Mathlib.AlgebraicTopology.SingularHomology.Basic
AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (n : ℕ) (R : C) (X : TopCat) [TotallyDisconnectedSpace ↑X]
  [inst_4 : CategoryTheory.CategoryWithHomology C],
  n ≠ 0 → CategoryTheory.Limits.IsZero (((AlgebraicTopology.singularHomologyFunctor C n).obj R).obj X)
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitYonedaHomIsoLimit'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (D : CategoryTheory.Functor I Cᵒᵖ) (F : CategoryTheory.Functor Cᵒᵖ (Type u₂))
  [inst_2 : CategoryTheory.Limits.HasColimit (D.leftOp.comp CategoryTheory.yoneda)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))],
  CategoryTheory.Limits.colimitYonedaHomIsoLimit' D F =
    CategoryTheory.Limits.colimitHomIsoLimitYoneda' (D.leftOp.comp CategoryTheory.yoneda) F ≪≫
      CategoryTheory.Limits.HasLimit.isoOfNatIso
        ((D.comp (CategoryTheory.Prod.sectL Cᵒᵖ F)).isoWhiskerLeft (CategoryTheory.yonedaLemma C))