mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.MonoidalPreadditive.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C],
  autoParam (∀ {X Y Z : C}, CategoryTheory.MonoidalCategoryStruct.whiskerLeft X 0 = 0)
      CategoryTheory.MonoidalPreadditive.whiskerLeft_zero._autoParam →
    autoParam (∀ {X Y Z : C}, CategoryTheory.MonoidalCategoryStruct.whiskerRight 0 X = 0)
        CategoryTheory.MonoidalPreadditive.zero_whiskerRight._autoParam →
      autoParam
          (∀ {X Y Z : C} (f g : Y ⟶ Z),
            CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (f + g) =
              CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f +
                CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g)
          CategoryTheory.MonoidalPreadditive.whiskerLeft_add._autoParam →
        autoParam
            (∀ {X Y Z : C} (f g : Y ⟶ Z),
              CategoryTheory.MonoidalCategoryStruct.whiskerRight (f + g) X =
                CategoryTheory.MonoidalCategoryStruct.whiskerRight f X +
                  CategoryTheory.MonoidalCategoryStruct.whiskerRight g X)
            CategoryTheory.MonoidalPreadditive.add_whiskerRight._autoParam →
          CategoryTheory.MonoidalPreadditive C
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Icc_union_Ici' : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, c ≤ b → Set.Icc a b ∪ Set.Ici c = Set.Ici (min a c)
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_add_eq : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  {ab ∈ A ×ˢ B | ab.1 + ab.2 = x}.card = A.addConvolution B x
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.instBoundedOrder : {A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] →
            [inst_3 : Module A W] → {ρ : Representation A G W} → BoundedOrder (Subrepresentation ρ)
-- Mathlib.Algebra.Order.Interval.Basic
Interval.addZeroClass.eq_1 : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  Interval.addZeroClass = { toZero := instZeroInterval, toAdd := instAddInterval, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- The characterization of weak convergence of probability measures by the condition that the
integrals of every continuous bounded nonnegative function are continuous.  -/
MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuousMap_continuous_lintegral : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {X : Type u_2} [inst_3 : TopologicalSpace X] {μs : X → MeasureTheory.ProbabilityMeasure Ω} [CompactSpace Ω],
  Continuous μs ↔ ∀ (f : C(Ω, NNReal)), Continuous fun x => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs x)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.mem_range_self : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (x : α), f x ∈ f.range
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.instResLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens)
  (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [AlgebraicGeometry.WeaklyEtale f],
  AlgebraicGeometry.WeaklyEtale (AlgebraicGeometry.Scheme.Hom.resLE f V U e)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.polynomialZ_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R},
  W'.polynomialZ =
    MvPolynomial.C W'.a₁ * MvPolynomial.X 0 * MvPolynomial.X 1 +
        MvPolynomial.C (3 * W'.a₃) * MvPolynomial.X 1 * MvPolynomial.X 2 ^ 2 -
      (MvPolynomial.C (2 * W'.a₂) * MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2 +
          MvPolynomial.C (4 * W'.a₄) * MvPolynomial.X 0 * MvPolynomial.X 2 ^ 3 +
        MvPolynomial.C (6 * W'.a₆) * MvPolynomial.X 2 ^ 5)
-- Lean.Meta.Basic
Lean.Meta.instInhabitedCache : Inhabited Lean.Meta.Cache
-- Std.Sync.SharedMutex
/-- Attempts to lock a `BaseSharedMutex` for exclusive write access. If the mutex is not available
return `false`, otherwise lock it and return `true`.

The current thread must not have already locked the mutex.
Reentrant locking is undefined behavior (inherited from the C++ implementation).
 -/
Std.BaseSharedMutex.tryWrite : Std.BaseSharedMutex → BaseIO Bool
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.lanUnit_app_app_lanAdjunction_counit_app_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F]
  (G : CategoryTheory.Functor D H) (X : C),
  CategoryTheory.CategoryStruct.comp ((L.lanUnit.app (L.comp G)).app X)
      (((L.lanAdjunction H).counit.app G).app (L.obj X)) =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (CategoryTheory.Functor C H)).obj (L.comp G)).obj X)
-- Lean.Parser.Syntax
Lean.Parser.Command.catBehaviorSymbol : Lean.Parser.Parser
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
closedBall_add_ball : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 ≤ ε → 0 < δ → ∀ (a b : E), Metric.closedBall a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.isNontrivial_iff_exists_lt_one : ∀ {K : Type u_7} [inst : DivisionRing K] {Γ₀ : Type u_8} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation K Γ₀), v.IsNontrivial ↔ ∃ x, x ≠ 0 ∧ v x < 1
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.mem_ofUnits : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ) {x : M} {y : Mˣ}, y ∈ S → ↑y = x → x ∈ S.ofUnits
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.id_symm_apply : ∀ {M : Type v} {ι : Type u_1} [inst : AddCommMonoid M] [inst_1 : Unique ι] (x : M),
  (DirectSum.id M ι).symm x = (DirectSum.of (fun i => M) default) x
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
/-- If `μ ≪ ν`, then `c • μ ≪ c • ν`.

Earlier, this name was used for what's now called `AbsolutelyContinuous.smul_left`.  -/
MeasureTheory.Measure.AbsolutelyContinuous.smul : ∀ {α : Type u_1} {R : Type u_5} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal], μ.AbsolutelyContinuous ν → ∀ (c : R), (c • μ).AbsolutelyContinuous (c • ν)
-- Batteries.Tactic.GeneralizeProofs
/-- Create a mapping of all propositions in the local context to their fvars.
 -/
Batteries.Tactic.GeneralizeProofs.initialPropToFVar : Lean.MetaM (Lean.ExprMap Lean.Expr)
-- Init.Data.ByteArray.Basic
/-- The current position.

This position is not necessarily valid for the array, for instance if one keeps calling
`Iterator.next` when `Iterator.atEnd` is true. If the position is not valid, then the
current byte is `(default : UInt8)`.  -/
ByteArray.Iterator.idx : ByteArray.Iterator → ℕ
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.ColimitType.instZero : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) → Zero (CommRingCat.Colimits.ColimitType F)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {x y : CategoryTheory.StrictlyUnitaryLaxFunctor B C},
  x.obj = y.obj →
    @Prefunctor.map B inst.toQuiver C inst_1.toQuiver x.toPrefunctor ≍
        @Prefunctor.map B inst.toQuiver C inst_1.toQuiver y.toPrefunctor →
      @CategoryTheory.PrelaxFunctorStruct.map₂ B inst.toQuiver
            (fun a b => (CategoryTheory.Bicategory.homCategory a b).toQuiver) C inst_1.toQuiver
            (fun a b => (CategoryTheory.Bicategory.homCategory a b).toQuiver) x.toPrelaxFunctorStruct ≍
          @CategoryTheory.PrelaxFunctorStruct.map₂ B inst.toQuiver
            (fun a b => (CategoryTheory.Bicategory.homCategory a b).toQuiver) C inst_1.toQuiver
            (fun a b => (CategoryTheory.Bicategory.homCategory a b).toQuiver) y.toPrelaxFunctorStruct →
        x.mapId ≍ y.mapId →
          @CategoryTheory.LaxFunctor.mapComp B inst C inst_1 x.toLaxFunctor ≍
              @CategoryTheory.LaxFunctor.mapComp B inst C inst_1 y.toLaxFunctor →
            x = y
-- Init.Data.Order.LemmasExtra
Std.instTotalLeOfLawfulOrderOrd : ∀ {α : Type u_1} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.Analysis.Quaternion
Quaternion.summable_coe : ∀ {α : Type u_1} {L : SummationFilter α} {f : α → ℝ}, Summable (fun a => ↑(f a)) L ↔ Summable f L
-- Mathlib.Data.Set.Sups
Set.singleton_sups : ∀ {α : Type u_2} [inst : SemilatticeSup α] {t : Set α} {a : α}, {a} ⊻ t = (fun b => a ⊔ b) '' t
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.Method.static.sizeOf_spec : sizeOf Aesop.ScriptGenerated.Method.static = 1
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
CompleteLattice.MulticoequalizerDiagram.multispanIndex_fst : ∀ {T : Type u} [inst : CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T}
  (d : CompleteLattice.MulticoequalizerDiagram x u v) (x_1 : (CategoryTheory.Limits.MultispanShape.prod ι).L),
  d.multispanIndex.fst x_1 = CategoryTheory.homOfLE ⋯
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.LevyProkhorov.toMeasureEquiv_symm_apply_toMeasure : ∀ {α : Type u_2} (toMeasure : α), (MeasureTheory.LevyProkhorov.toMeasureEquiv.symm toMeasure).toMeasure = toMeasure
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.isClosed_range : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H),
  IsClosed (Set.range ↑I)
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.mem_map : ∀ {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'} {I : LieIdeal R L} {x : L},
  x ∈ I → f x ∈ LieIdeal.map f I
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- We can think of a morphism `f : mop X ⟶ mop Y` as a morphism `X ⟶ Y`.  -/
Quiver.Hom.unmop : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : Cᴹᵒᵖ} → (X ⟶ Y) → (X.unmop ⟶ Y.unmop)
-- Mathlib.Algebra.Module.Submodule.Map
LinearEquiv.submoduleMap_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂)
  (p : Submodule R M) (x : ↥(Submodule.map (↑e) p)), ↑((e.submoduleMap p).symm x) = e.symm ↑x
-- Init.Data.List.MinMax
List.max?_singleton : ∀ {α : Type u_1} [inst : Max α] {x : α}, [x].max? = some x
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.rank_eq_four : ∀ {R : Type u_3} (c₁ c₂ c₃ : R) [inst : CommRing R] [StrongRankCondition R],
  Module.rank R (QuaternionAlgebra R c₁ c₂ c₃) = 4
-- Init.Data.SInt.Basic
/-- The power operation, raising an 8-bit signed integer to a natural number power,
wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently *not* overridden at runtime with an efficient implementation,
and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
 -/
Int8.pow : Int8 → ℕ → Int8
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_of_mem_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  k ∈ Std.DTreeMap.Const.insertMany t l → (List.map Prod.fst l).contains k = false → k ∈ t
-- Mathlib.Order.Hom.Basic
OrderIso.arrowCongr_apply : ∀ {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] (f : α ≃o γ) (g : β ≃o δ) (p : α →o β),
  (f.arrowCongr g) p = (↑g).comp (p.comp ↑f.symm)
-- Mathlib.Data.Fintype.EquivFin
Fintype.card_eq_one_of_forall_eq : ∀ {α : Type u_1} [inst : Fintype α] {i : α}, (∀ (j : α), j = i) → Fintype.card α = 1
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.decompLinearEquiv_symm_contLinear : ∀ (R : Type u_1) (S : Type u_2) (V : Type u_3) (W : Type u_4) [inst : Ring S] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : IsTopologicalAddGroup V]
  [inst_6 : AddCommGroup W] [inst_7 : Module R W] [inst_8 : TopologicalSpace W] [inst_9 : Module S W]
  [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : IsTopologicalAddGroup W]
  (p : W × (V →L[R] W)), ((ContinuousAffineMap.decompLinearEquiv R S V W).symm p).contLinear = p.2
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesMap f φ 0))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesIso₀ A).inv) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesIso₀ B).inv) ((Rep.Hom.hom φ) x)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.IsCycles.existsUnique_ne_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {v w : V}, G.IsCycles → G.Adj v w → ∃! w', w ≠ w' ∧ G.Adj v w'
-- Lean.Meta.Sym.Simp.SimpM
/-- The result of simplifying an expression `e`.

The `done` flag controls whether simplification should continue after this result:
- `done = false` (default): Continue with subsequent simplification steps
- `done = true`: Stop processing, return this result as final

## Use cases for `done = true`

### In `pre` simprocs
Skip simplification of certain subterms entirely:
```
def skipLambdas : Simproc := fun e =>
  if e.isLambda then return .rfl (done := true)
  else return .rfl
```

### In `post` simprocs
Perform single-pass normalization without recursive simplification:
```
def singlePassNormalize : Simproc := fun e =>
  if let some (e', h) ← tryNormalize e then
    return .step e' h (done := true)
  else return .rfl
```
With `done = true`, the result `e'` won't be recursively simplified.

## Behavior

The `done` flag affects:
1. **`andThen` composition**: If the first simproc returns `done = true`,
   the second simproc is skipped.
2. **Recursive simplification**: After `pre` or `post` returns `.step e' h`,
   `simp` normally recurses on `e'`. With `done = true`, recursion is skipped.

The flag is orthogonal to caching: both `.rfl` and `.step` results are cached
regardless of the `done` flag, and cached results are always treated as final.

## Context-dependent results

The `contextDependent` flag tracks whether the result depends on the local context
(e.g., hypotheses introduced when entering binders). Context-dependent results are
stored in a transient cache that is cleared when entering binders, while
context-independent results persist across binder entry and across `simp` invocations.

**Propagation rule**: when combining sub-results (congruence, transitivity, etc.),
`contextDependent` is the disjunction of all sub-results' flags. This includes
`.rfl` results: if `simp` returned `.rfl (contextDependent := true)`, it means
`simp` might produce a *different* result in another local context (e.g., a conditional
rewrite could succeed), so all downstream results must be marked context-dependent.
 -/
Lean.Meta.Sym.Simp.Result : Type
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_iff_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {a : α}, m.contains a = true ↔ a ∈ m
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.isoEquivHomeo_symm_apply : ∀ {P : TopCat → Prop} {X Y : CompHausLike P} (f : ↑X.toTop ≃ₜ ↑Y.toTop),
  CompHausLike.isoEquivHomeo.symm f = CompHausLike.isoOfHomeo f
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.instDecidableRelAdjBetweenOfDecidablePredMemSet : {V : Type u_1} →
  {G : SimpleGraph V} →
    {s t : Set V} →
      [DecidableRel G.Adj] →
        [DecidablePred fun x => x ∈ s] → [DecidablePred fun x => x ∈ t] → DecidableRel (SimpleGraph.between s t G).Adj
-- Mathlib.Data.Nat.Totient
Nat.sum_totient : ∀ (n : ℕ), n.divisors.sum Nat.totient = n
-- Mathlib.Analysis.Convex.Segment
openSegment_eq_image : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (x y : E), openSegment 𝕜 x y = (fun θ => (1 - θ) • x + θ • y) '' Set.Ioo 0 1
-- Mathlib.Analysis.MellinTransform
hasMellin_const_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E} {s : ℂ},
  MellinConvergent f s →
    ∀ {R : Type u_2} [inst_2 : NormedRing R] [inst_3 : Module R E] [IsBoundedSMul R E] [SMulCommClass ℂ R E] (c : R),
      HasMellin (fun t => c • f t) s (c • mellin f s)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.ne_of_lt : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LT a b → a ≠ b
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.instContinuousMapClass : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  ContinuousMapClass C(X, Y) X Y
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_eq_tsum_div : ∀ {𝔸 : Type u_2} [inst : DivisionRing 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] [CharZero 𝔸],
  NormedSpace.exp = fun x => ∑' (n : ℕ), x ^ n / ↑n.factorial
-- Batteries.Data.Nat.Bisect
_private.Batteries.Data.Nat.Bisect.0.Nat.bisect.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : true = false → motive false) (h_2 : true = true → motive true),
  (match hmid : true with
    | false => h_1 hmid
    | true => h_2 hmid) =
    h_2 ⋯
-- Mathlib.Combinatorics.Matroid.Map
Matroid.restrictSubtype_ground_isBasis_iff : ∀ {α : Type u_1} {M : Matroid α} {I X : Set ↑M.E},
  (M.restrictSubtype M.E).IsBasis I X ↔ M.IsBasis (Subtype.val '' I) (Subtype.val '' X)
-- Std.Sat.AIG.LawfulOperator
_private.Std.Sat.AIG.LawfulOperator.0.Std.Sat.AIG.toGraphviz.go.match_1.eq_2 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (idx : α)
  (h_1 : Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx_1 : α) → Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.atom idx_1 → motive (Std.Sat.AIG.Decl.atom idx_1))
  (h_3 :
    (lhs rhs : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match elem : Std.Sat.AIG.Decl.atom idx with
    | Std.Sat.AIG.Decl.false => h_1 elem
    | Std.Sat.AIG.Decl.atom idx_1 => h_2 idx_1 elem
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs elem) =
    h_2 idx ⋯
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Uniform equicontinuity implies equicontinuity.  -/
UniformEquicontinuous.equicontinuous : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α},
  UniformEquicontinuous F → Equicontinuous F
-- Lean.Meta.KExprMap
Lean.Meta.instInhabitedKExprMap : {a : Type} → Inhabited (Lean.Meta.KExprMap a)
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.Hom.naturality : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {P Q : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D} (self : P.Hom Q) ⦃X X' : C⦄ ⦃Y Y' : D⦄ (f : X ⟶ X')
  (g : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (P.map f g) (self.app X' Y) =
    CategoryTheory.CategoryStruct.comp (self.app X Y') (Q.map f g)
-- Mathlib.Analysis.Calculus.VectorField
Filter.EventuallyEq.lieBracket_vectorField_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W V₁ W₁ : E → E} {x : E},
  V₁ =ᶠ[nhds x] V → W₁ =ᶠ[nhds x] W → VectorField.lieBracket 𝕜 V₁ W₁ x = VectorField.lieBracket 𝕜 V W x
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure_bot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} (J : α → Type u')
  [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] [∀ (a : α), Nonempty (J a)], ⊥.colimitsClosure J = ⊥
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- If a function is differentiable on two open sets, it is also differentiable on their union.  -/
DifferentiableOn.union_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {s t : Set E},
  DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 f t → IsOpen s → IsOpen t → DifferentiableOn 𝕜 f (s ∪ t)
-- Std.Data.Iterators.Producers.Monadic.Array
Std.Iterators.Types.ArrayIterator.mk.injEq : ∀ {α : Type w} (array : Array α) (pos : ℕ) (array_1 : Array α) (pos_1 : ℕ),
  ({ array := array, pos := pos } = { array := array_1, pos := pos_1 }) = (array = array_1 ∧ pos = pos_1)
-- Mathlib.Algebra.Category.MonCat.Yoneda
AddCommMonCat.coyonedaType_obj_map : ∀ (X : Type uᵒᵖ) {X_1 Y : AddCommMonCat} (f : X_1 ⟶ Y),
  (AddCommMonCat.coyonedaType.obj X).map f =
    AddCommMonCat.ofHom
      (AddMonoidHom.pi fun i => (AddCommMonCat.Hom.hom f).comp (Pi.evalAddMonoidHom (fun a => ↑X_1) i))
-- Mathlib.Data.Set.Sups
/-- The point-wise supremum `a ⊔ b` of `a, b : α`.  -/
HasSups.sups : {α : Type u_4} → [self : HasSups α] → α → α → α
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.le_of_carrier_le_iSup : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {ι : Sort u_4} {ρ : ι → IntermediateField.Lifts F E K}
  {σ τ : IntermediateField.Lifts F E K},
  (∀ (i : ι), ρ i ≤ σ) → (∀ (i : ι), ρ i ≤ τ) → σ.carrier ≤ ⨆ i, (ρ i).carrier → σ ≤ τ
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α},
  k ∉ m₁ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.Probability.Process.LocalProperty
_private.Mathlib.Probability.Process.LocalProperty.0.ProbabilityTheory.mkStrictMonoAux.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Init.Data.String.Defs
List.utf8Encode_append : ∀ {l l' : List Char}, (l ++ l').utf8Encode = l.utf8Encode ++ l'.utf8Encode
-- Mathlib.Tactic.TFAE
/-- Re-enables "goal-style" syntax for `tfae_have` when `true`.  -/
Mathlib.Tactic.TFAE.useDeprecated : Lean.Option Bool
-- Mathlib.Topology.Maps.Proper.Basic
/-- The coercion from a closed subset is proper.  -/
IsClosed.isProperMap_subtypeVal : ∀ {X : Type u_1} [inst : TopologicalSpace X] {C : Set X}, IsClosed C → IsProperMap Subtype.val
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- Left homotopies are compatible with postcomposition.  -/
HomotopicalAlgebra.Precylinder.LeftHomotopy.postcomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {P : HomotopicalAlgebra.Precylinder X} →
        {Y : C} →
          {f g : X ⟶ Y} →
            P.LeftHomotopy f g →
              {Z : C} →
                (p : Y ⟶ Z) →
                  P.LeftHomotopy (CategoryTheory.CategoryStruct.comp f p) (CategoryTheory.CategoryStruct.comp g p)
-- Std.Http.Data.Status
/-- 102 Processing
 -/
Std.Http.Status.processing : Std.Http.Status