mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- **Alias** of `Set.image_finsetProd`. -/
Set.image_finset_prod : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : FunLike F α β] [inst_1 : CommMonoid α]
  [inst_2 : CommMonoid β] [MonoidHomClass F α β] (f : F) (m : Finset ι) (s : ι → Set α),
  ⇑f '' ∏ i ∈ m, s i = ∏ i ∈ m, ⇑f '' s i
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.l2_opNorm_mul : ∀ {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} {l : Type u_4} [inst : RCLike 𝕜] [inst_1 : Fintype m]
  [inst_2 : Fintype n] [inst_3 : DecidableEq n] [inst_4 : Fintype l] [inst_5 : DecidableEq l] (A : Matrix m n 𝕜)
  (B : Matrix n l 𝕜), ‖A * B‖ ≤ ‖A‖ * ‖B‖
-- Batteries.Tactic.PrintPrefix
/-- The command `#print prefix foo` will print all definitions that start with
the namespace `foo`.

For example, the command below will print out definitions in the `List` namespace:

```lean
#print prefix List
```

`#print prefix` can be controlled by flags in `PrintPrefixConfig`.  These provide
options for filtering names and formatting.   For example,
`#print prefix` by default excludes internal names, but this can be controlled
via config:
```lean
#print prefix (config := {internals := true}) List
```

By default, `#print prefix` prints the type after each name.  This can be controlled
by setting `showTypes` to `false`:
```lean
#print prefix (config := {showTypes := false}) List
```

The complete set of flags can be seen in the documentation
for `Lean.Elab.Command.PrintPrefixConfig`.
 -/
Batteries.Tactic.printPrefix : Lean.ParserDescr
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsuppLid_single_tmul_single : ∀ (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid N]
  [inst_2 : Module R N] (a : ι) (b : κ) (r : R) (n : N),
  (finsuppTensorFinsuppLid R N ι κ) ((fun₀ | a => r) ⊗ₜ[R] fun₀ | b => n) = fun₀ | (a, b) => r • n
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IteratorLoop.WithWF.mk : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        {γ : Type x} →
          {PlausibleForInStep : β → γ → ForInStep γ → Prop} →
            {hwf : Std.IteratorLoop.WellFounded α m PlausibleForInStep} →
              Std.IterM m β → γ → Std.IteratorLoop.WithWF α m PlausibleForInStep hwf
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insert_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl k ⋯ = v
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists.Equiv.decidable.match_1.eq_3 : ∀ {α : Type u_1} (motive : Lists α → Lists α → Sort u_2) (l₁ : Lists' α true) (l₂ : Lists' α false)
  (h_1 : (l₁ l₂ : Lists' α false) → motive ⟨false, l₁⟩ ⟨false, l₂⟩)
  (h_2 : (l₁ : Lists' α false) → (l₂ : Lists' α true) → motive ⟨false, l₁⟩ ⟨true, l₂⟩)
  (h_3 : (l₁ : Lists' α true) → (l₂ : Lists' α false) → motive ⟨true, l₁⟩ ⟨false, l₂⟩)
  (h_4 : (l₁ l₂ : Lists' α true) → motive ⟨true, l₁⟩ ⟨true, l₂⟩),
  (match ⟨true, l₁⟩, ⟨false, l₂⟩ with
    | ⟨false, l₁⟩, ⟨false, l₂⟩ => h_1 l₁ l₂
    | ⟨false, l₁⟩, ⟨true, l₂⟩ => h_2 l₁ l₂
    | ⟨true, l₁⟩, ⟨false, l₂⟩ => h_3 l₁ l₂
    | ⟨true, l₁⟩, ⟨true, l₂⟩ => h_4 l₁ l₂) =
    h_3 l₁ l₂
-- Init.Data.UInt.Lemmas
UInt16.ofNat_sub : ∀ {a b : ℕ}, b ≤ a → UInt16.ofNat (a - b) = UInt16.ofNat a - UInt16.ofNat b
-- Mathlib.Order.Filter.Map
Filter.comap_neBot_iff_compl_range : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β}, (Filter.comap m f).NeBot ↔ (Set.range m)ᶜ ∉ f
-- Mathlib.Condensed.Equivalence
Condensed.StoneanProfinite.instReflectsEffectiveEpisStoneanProfiniteToProfinite : Stonean.toProfinite.ReflectsEffectiveEpis
-- Mathlib.LinearAlgebra.Matrix.DualNumber
Matrix.dualNumberEquiv_apply : ∀ {R n : Type} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n (DualNumber R)),
  Matrix.dualNumberEquiv A =
    (Matrix.of fun i j => TrivSqZeroExt.fst (A i j), Matrix.of fun i j => TrivSqZeroExt.snd (A i j))
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.isoMk_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x y : F.Elements)
  (e : x.fst ≅ y.fst) (he : (CategoryTheory.ConcreteCategory.hom (F.map e.hom)) x.snd = y.snd),
  (CategoryTheory.CategoryOfElements.isoMk x y e he).hom = CategoryTheory.CategoryOfElements.homMk x y e.hom he
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.mk : {R : Type u} →
  {M : Type v} →
    {N : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                (toFun : M → N) →
                  (∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x) →
                    (∃ B, ∀ (x y : M), toFun (x + y) = toFun x + toFun y + (B x) y) → QuadraticMap R M N
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.evalTryTraceWith : Lean.Elab.Tactic.Tactic
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- For a point outside or on the sphere, the product of distances to two intersection
points on a line through the point equals the power of the point.  -/
EuclideanGeometry.Sphere.mul_dist_eq_power_of_radius_le_dist_center : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p a b : P},
  0 ≤ s.radius → p ∈ line[ℝ, a, b] → a ∈ s → b ∈ s → s.radius ≤ dist p s.center → dist p a * dist p b = s.power p
-- Mathlib.Analysis.Distribution.TestFunction
/-- `fderivCLM 𝕜 n k` is the continuous `𝕜`-linear-map sending `f : 𝓓^{n}_{K}(E, F)` to
its derivative as an element of `𝓓^{k}_{K}(E, E →L[ℝ] F)`.
This only makes mathematical sense if `k + 1 ≤ n`, otherwise we define it as the zero map.  -/
TestFunction.fderivCLM : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace ℝ E] →
          {Ω : TopologicalSpace.Opens E} →
            {F : Type u_4} →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace ℝ F] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    (n k : ℕ∞) →
                      [inst_6 : Algebra ℝ 𝕜] →
                        [inst_7 : IsScalarTower ℝ 𝕜 F] → TestFunction Ω F n →L[𝕜] TestFunction Ω (E →L[ℝ] F) k
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.Rels.add.injEq : ∀ {R : Type u} {ι : Type u_4} {M : Type u_5} (m : ι → M) (i : ι) (x y : M) (m_1 : ι → M) (i_1 : ι) (x_1 y_1 : M),
  (exteriorPower.presentation.Rels.add m i x y = exteriorPower.presentation.Rels.add m_1 i_1 x_1 y_1) =
    (m = m_1 ∧ i = i_1 ∧ x = x_1 ∧ y = y_1)
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- Being a closed immersion is stable under base change.  -/
AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsClosedImmersion
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.image_trans_source : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z),
  ↑e '' (e.trans e').source = e.target ∩ e'.source
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- If there is any isomorphism `⊥ ⟶ G.obj ⊥`, then `G` preserves initial objects.  -/
CategoryTheory.Limits.preservesInitial_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasInitial C]
  [inst_3 : CategoryTheory.Limits.HasInitial D] (f : ⊥_ D ⟶ G.obj (⊥_ C)) [i : CategoryTheory.IsIso f],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_eq_toFinset_prod : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) (s : Set α) [inst_1 : Fintype ↑s],
  ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ s.toFinset, f i
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1)
  [W.RespectsIso],
  (∀ (X₁ X₂ : J → C) [inst_2 : CategoryTheory.Limits.HasProduct X₁] [inst_3 : CategoryTheory.Limits.HasProduct X₂]
      (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (CategoryTheory.Limits.Pi.map f)) →
    W.IsStableUnderProductsOfShape J
-- Mathlib.Topology.ContinuousOn
ContinuousOn.comp_continuous : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set β},
  ContinuousOn g s → Continuous f → (∀ (x : α), f x ∈ s) → Continuous (g ∘ f)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.neg_nonempty_iff`. -/
Finset.Nonempty.neg : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] {s : Finset α}, s.Nonempty → (-s).Nonempty
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Restriction of an `AddMonoidHom` to its range interpreted as an `AddSubmonoid`.  -/
AddMonoidHom.mrangeRestrict : {M : Type u_1} →
  [inst : AddZeroClass M] → {N : Type u_5} → [inst_1 : AddZeroClass N] → (f : M →+ N) → M →+ ↥(AddMonoidHom.mrange f)
-- Init.Data.Nat.MinMax
Nat.add_min_add_left : ∀ (a b c : ℕ), min (a + b) (a + c) = a + min b c
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.le_of_le_cert.match_1.eq_4 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (a₁ : ℤ) (x₁ : Int.Internal.Linear.Var)
  (p₁ : Int.Internal.Linear.Poly) (a₂ : ℤ) (x₂ : Int.Internal.Linear.Var) (p₂ : Int.Internal.Linear.Poly)
  (h_1 :
    (k : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k_1 : ℤ) → motive (Int.Internal.Linear.Poly.add k v p) (Int.Internal.Linear.Poly.num k_1))
  (h_2 :
    (k k_1 : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k) (Int.Internal.Linear.Poly.add k_1 v p))
  (h_3 : (c₁ c₂ : ℤ) → motive (Int.Internal.Linear.Poly.num c₁) (Int.Internal.Linear.Poly.num c₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂)),
  (match Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ with
    | Int.Internal.Linear.Poly.add k v p, Int.Internal.Linear.Poly.num k_1 => h_1 k v p k_1
    | Int.Internal.Linear.Poly.num k, Int.Internal.Linear.Poly.add k_1 v p => h_2 k k_1 v p
    | Int.Internal.Linear.Poly.num c₁, Int.Internal.Linear.Poly.num c₂ => h_3 c₁ c₂
    | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) =
    h_4 a₁ x₁ p₁ a₂ x₂ p₂
-- Init.Data.List.MinMaxOn
List.minOn_eq_of_minOn?_eq_some : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} {x : α}
  (h : List.minOn? f xs = some x), List.minOn f xs ⋯ = x
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- Notation for `Measurable` with respect to a non-standard σ-algebra in the domain and codomain.
 -/
MeasureTheory.«termMeasurable[_,_]» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_filter!_eq_false_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filter! f t).isEmpty = false ↔
      ∃ k,
        ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true),
          f (t.getKey k h) (Std.DTreeMap.Internal.Impl.Const.get t k h) = true)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.isAcyclic_of_path_unique : ∀ {V : Type u_1} {G : SimpleGraph V}, (∀ (v w : V) (p q : G.Path v w), p = q) → G.IsAcyclic
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.MkTableKey.State.emap : Lean.Meta.SynthInstance.MkTableKey.State → Std.HashMap Lean.MVarId Lean.Expr
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_map_mul : ∀ {ι : Type u_2} {M : Type u_5} [inst : CommMonoid M] {m : Multiset ι} {f g : ι → M},
  (Multiset.map (fun i => f i * g i) m).prod = (Multiset.map f m).prod * (Multiset.map g m).prod
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `Ne.pos`.

---

**Alias** of `pos_of_ne_zero`.

---

**Alias** of the reverse direction of `pos_iff_ne_zero`. -/
NE.ne.pos : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α], a ≠ 0 → 0 < a
-- Mathlib.Order.RelIso.Set
Subrel.instIsWellFoundedSubtype : ∀ {α : Type u_1} (r : α → α → Prop) [IsWellFounded α r] (p : α → Prop), IsWellFounded (Subtype p) (Subrel r p)
-- Mathlib.GroupTheory.FreeGroup.GeneratorEquiv
/-- `A` is a basis of the ℤ-module `FreeAbelianGroup A`.  -/
FreeAbelianGroup.basis : (α : Type u_5) → Module.Basis α ℤ (FreeAbelianGroup α)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_biInter_eq_biInter_closure_of_biUnion_indep : ∀ {α : Type u_2} {M : Matroid α} {ι : Type u_4} {A : Set ι},
  A.Nonempty → ∀ {I : ι → Set α}, M.Indep (⋃ i ∈ A, I i) → M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.DTreeMap.Const.getEntryLE? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α → Option (α × β)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_eq_Ico_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c d : α}, a < b ∨ c < d → (Set.Ico a b = Set.Ico c d ↔ a = c ∧ b = d)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.one_prod_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : One β], 1 ×ˢ 1 = 1
-- Mathlib.Order.RelIso.Basic
/-- `Quotient.mk` as a relation homomorphism between the relation and the lift of a relation.  -/
Quotient.mkRelHom : {α : Type u_1} →
  {x : Setoid α} →
    {r : α → α → Prop} → (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) → r →r Quotient.lift₂ r H
-- Mathlib.Tactic.Have
/-- Retrieves the name of the optional identifier, if provided. Returns `this` otherwise  -/
Mathlib.Tactic.optBinderIdent.name : Lean.TSyntax `Mathlib.Tactic.optBinderIdent → Lean.Name
-- Mathlib.RingTheory.Valuation.Integers
Valuation.ltIdeal_v_le_of_mem : ∀ {Γ₀ : Type v} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_1} [inst_1 : Field K] {v : Valuation K Γ₀}
  {I : Ideal ↥v.integer} {x : ↥v.integer}, x ∈ I → ∀ (hxv : v ↑x ≠ 0), v.ltIdeal (Units.mk0 (v ↑x) hxv) ≤ I
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instInhabited : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Inhabited (Std.DTreeMap α β cmp)
-- Mathlib.Topology.Path
Path.mk.sizeOf_spec : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} [inst_1 : SizeOf X] (toContinuousMap : C(↑unitInterval, X))
  (source' : toContinuousMap.toFun 0 = x) (target' : toContinuousMap.toFun 1 = y),
  sizeOf { toContinuousMap := toContinuousMap, source' := source', target' := target' } =
    1 + sizeOf toContinuousMap + sizeOf source' + sizeOf target'
-- Init.Data.Option.Lemmas
Option.any_eq_false_iff_get : ∀ {α : Type u_1} (p : α → Bool) (x : Option α), Option.any p x = false ↔ ∀ (h : x.isSome = true), p (x.get h) = false
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
FDerivMeasurableAux.mem_A_of_differentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {ε : ℝ},
  0 < ε → ∀ {x : E}, DifferentiableAt 𝕜 f x → ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, x ∈ FDerivMeasurableAux.A f (fderiv 𝕜 f x) r ε
-- Lean.Exception
Lean.Exception.hasSyntheticSorry : Lean.Exception → Bool
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- A rewrite lemma for `padicValNat p (a * b)` with conditions `a ≠ 0`, `b ≠ 0`.  -/
padicValNat.mul : ∀ {p a b : ℕ} [hp : Fact (Nat.Prime p)], a ≠ 0 → b ≠ 0 → padicValNat p (a * b) = padicValNat p a + padicValNat p b
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map_nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {basis_hd' : ℝ → ℝ}
  {basis_tl' : Tactic.ComputeAsymptotics.Basis} (f : ℝ → ℝ)
  (g :
    Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl → Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl'),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map f g
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.card_eq : ∀ {α : Type u_1} {n : ℕ} (s : ↑(Set.powersetCard α n)), (↑s).card = n
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Fin.instMeasurableSingletonClass : ∀ (n : ℕ), MeasurableSingletonClass (Fin n)
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_add : ∀ (a b : BitVec 8), { toBitVec := a + b } = { toBitVec := a } + { toBitVec := b }
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
_private.Mathlib.Algebra.BigOperators.Group.List.Lemmas.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.associator_inv.sizeOf_spec : ∀ {B : Type u} [inst : Quiver B] [inst_1 : SizeOf B] {a b c d : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c)
  (h : c ⟶ d),
  sizeOf (CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h) =
    1 + sizeOf a + sizeOf b + sizeOf c + sizeOf d + sizeOf f + sizeOf g + sizeOf h
-- Mathlib.Algebra.Quaternion
Quaternion.coe_zpow : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] (x : R) (z : ℤ),
  ↑(x ^ z) = ↑x ^ z
-- Init.Data.BitVec.Lemmas
BitVec.toNat_ne : ∀ {n : ℕ} {x y : BitVec n}, x ≠ y ↔ x.toNat ≠ y.toNat
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_mul : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Mul α] (s : ι → Set α) (t : Set α), (⋃ i, s i) * t = ⋃ i, s i * t
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.small_Iic : ∀ (o : Ordinal.{u}), Small.{u, u + 1} ↑(Set.Iic o)
-- Mathlib.Util.Export
Lean.Export.Entry.expr.inj : ∀ {n n_1 : Lean.Expr}, Lean.Export.Entry.expr n = Lean.Export.Entry.expr n_1 → n = n_1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.SimpleFunc.aestronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (f : MeasureTheory.SimpleFunc α β), MeasureTheory.AEStronglyMeasurable (⇑f) μ
-- Mathlib.Algebra.Module.Submodule.Invariant
/-- `p` is `f` invariant if and only if `Set.MapsTo f p p`.  -/
Module.End.mem_invtSubmodule_iff_mapsTo : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p : Submodule R M}, p ∈ f.invtSubmodule ↔ Set.MapsTo ⇑f ↑p ↑p
-- Qq.Macro
Qq.Impl.MVarSynth.isAssigned : Qq.Impl.MVarSynth → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.shrink_eq_shrink_of_presieve₀_eq_presieve₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S},
  E.presieve₀ = F.presieve₀ → E.shrink = F.shrink
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.IsocrystalEquiv.mk.inj : ∀ {p : ℕ} {inst : Fact (Nat.Prime p)} {k : Type u_1} {inst_1 : CommRing k} {inst_2 : CharP k p}
  {inst_3 : PerfectRing k p} {V : Type u_2} {inst_4 : AddCommGroup V} {inst_5 : WittVector.Isocrystal p k V}
  {V₂ : Type u_3} {inst_6 : AddCommGroup V₂} {inst_7 : WittVector.Isocrystal p k V₂}
  {toLinearEquiv : V ≃ₗ[FractionRing (WittVector p k)] V₂}
  {frob_equivariant :
    ∀ (x : V),
      (WittVector.Isocrystal.frobenius p k) (toLinearEquiv x) = toLinearEquiv ((WittVector.Isocrystal.frobenius p k) x)}
  {toLinearEquiv_1 : V ≃ₗ[FractionRing (WittVector p k)] V₂}
  {frob_equivariant_1 :
    ∀ (x : V),
      (WittVector.Isocrystal.frobenius p k) (toLinearEquiv_1 x) =
        toLinearEquiv_1 ((WittVector.Isocrystal.frobenius p k) x)},
  { toLinearEquiv := toLinearEquiv, frob_equivariant := frob_equivariant } =
      { toLinearEquiv := toLinearEquiv_1, frob_equivariant := frob_equivariant_1 } →
    toLinearEquiv = toLinearEquiv_1
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ideal.mulQuot.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (a : R) (I : Ideal R),
  Ideal.mulQuot a I = Submodule.mapQ I (a • I) ((LinearMap.mul R R) a) ⋯
-- Mathlib.Data.Multiset.Range
Multiset.range_add_eq_union : ∀ (a b : ℕ), Multiset.range (a + b) = Multiset.range a ∪ Multiset.map (fun x => a + x) (Multiset.range b)
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val : ∀ (n : ℕ) [inst : NeZero n] (j : ZMod n),
  ↑↑((rootsOfUnityCircleEquiv n) ((ZMod.rootsOfUnityAddChar n) j)) =
    Complex.exp (2 * ↑Real.pi * Complex.I * ↑j.val / ↑n)
-- Mathlib.Order.PFilter
/-- A predicate for when a subset of `P` is a filter.  -/
Order.IsPFilter : {P : Type u_1} → [Preorder P] → Set P → Prop
-- Init.Data.Vector.Lemmas
Vector.toArray_beq_toArray : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs ys : Vector α n}, (xs.toArray == ys.toArray) = (xs == ys)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.wellFoundedRelation : WellFoundedRelation Ordinal.{u_1}
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `g` is a linear map `M → M''` such that all scalar multiplication by `s : S` is invertible and
`l` is another linear map `LocalizedModule S M ⟶ M''` such that `l ∘ mkLinearMap = g` then
`l = lift g`
 -/
LocalizedModule.lift_unique : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M''] [inst_3 : Module R M] [inst_4 : Module R M''] (g : M →ₗ[R] M'')
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (l : LocalizedModule S M →ₗ[R] M''),
  l ∘ₗ LocalizedModule.mkLinearMap S M = g → LocalizedModule.lift S g h = l
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.LawfulUpwardEnumerableLE.mk : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α],
  (∀ (a b : α), a ≤ b ↔ Std.PRange.UpwardEnumerable.LE a b) → Std.PRange.LawfulUpwardEnumerableLE α
-- Init.Data.Array.Lemmas
Array.mem_push : ∀ {α : Type u_1} {xs : Array α} {x y : α}, x ∈ xs.push y ↔ x ∈ xs ∨ x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Fan.ext_hom_hom : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Fan f}
  (e : c₁.pt ≅ c₂.pt)
  (w :
    autoParam (∀ (b : β), c₁.proj b = CategoryTheory.CategoryStruct.comp e.hom (c₂.proj b))
      CategoryTheory.Limits.Fan.ext._auto_1),
  (CategoryTheory.Limits.Fan.ext e w).hom.hom = e.hom
-- Lean.Parser.Basic
Lean.Parser.identFnAux : String.Pos.Raw → Option Lean.Parser.Token → Lean.Name → optParam Bool true → Lean.Parser.ParserFn
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.toWord_pow : ∀ {α : Type u_1} [inst : DecidableEq α] (x : FreeGroup α) (n : ℕ),
  (x ^ n).toWord = FreeGroup.reduce (List.replicate n x.toWord).flatten
-- Mathlib.Topology.Algebra.Field
Nonneg.unitsEquivPos.congr_simp : ∀ (R : Type u_2) [inst : DivisionSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : PosMulReflectLT R], Nonneg.unitsEquivPos R = Nonneg.unitsEquivPos R