mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Level
Lean.instForInLMVarIdSetLMVarIdOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForIn m Lean.LMVarIdSet Lean.LMVarId
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.eq_1 : @Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates =
  (@fun Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates._functor.call {basis} ms =>
      basis = [] ∨
        (∃ basis_hd basis_tl f,
            f =ᶠ[Filter.atTop] 0 ∧
              basis = basis_hd :: basis_tl ∧
                ms ≍
                  Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
                    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil f) ∨
          ∃ basis_hd f basis_tl exp coef tl,
            Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates._functor.call coef ∧
              Tactic.ComputeAsymptotics.Majorized f basis_hd exp ∧
                Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates._functor.call
                    (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk tl (f - basis_hd ^ exp * coef.toFun)) ∧
                  basis = basis_hd :: basis_tl ∧
                    ms ≍
                      Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
                        (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) f)
    @Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates
-- Mathlib.Data.ENNReal.Inv
ENNReal.one_lt_inv : ∀ {a : ENNReal}, 1 < a⁻¹ ↔ a < 1
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M],
  AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid =
    { toAddMonoid := inferInstance, neg := fun x => ⟨↑(-IsAddUnit.addUnit ⋯), ⋯⟩, sub := SubNegMonoid.sub',
      zsmul := zsmulRec, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.CategoryTheory.Skeletal
/-- This provides natural transformations `map₂Functor F x₁ ⟶ map₂Functor F x₂` given
`x₁ ⟶ x₂`  -/
CategoryTheory.ThinSkeleton.map₂NatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) →
              {x₁ x₂ : CategoryTheory.ThinSkeleton C} →
                (x₁ ⟶ x₂) →
                  (CategoryTheory.ThinSkeleton.map₂Functor F x₁ ⟶ CategoryTheory.ThinSkeleton.map₂Functor F x₂)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mem_comap : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (K₂ : LieSubalgebra R L₂) {x : L},
  x ∈ LieSubalgebra.comap f K₂ ↔ f x ∈ K₂
-- Mathlib.Data.Fintype.Defs
Finset.eq_univ_iff_forall : ∀ {α : Type u_1} [inst : Fintype α] {s : Finset α}, s = Finset.univ ↔ ∀ (x : α), x ∈ s
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.minKeyD : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → α → α
-- Aesop.RuleSet
Aesop.GlobalRuleSet.toBaseRuleSet : Aesop.GlobalRuleSet → Aesop.BaseRuleSet
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordConnectedProj_mem_ordConnectedComponent : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α) (x : ↑s), s.ordConnectedProj x ∈ s.ordConnectedComponent ↑x
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instSup : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : NormedAddCommGroup β] →
        [inst_2 : Lattice β] → [HasSolidNorm β] → [IsOrderedAddMonoid β] → Max (BoundedContinuousFunction α β)
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.rep_gHSpace_compactSpace : ∀ {p : GromovHausdorff.GHSpace}, CompactSpace p.Rep
-- Mathlib.Data.List.Dedup
List.tail_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Inhabited α] (l : List α),
  l.dedup.tail = if l.headI ∈ l.tail then l.tail.dedup.tail else l.tail.dedup
-- Lean.Elab.Term.TermElabM
/-- Execute `x`, save resulting expression and new state.
We remove any `Info` created by `x`.
The info nodes are committed when we execute `applyResult`.
We use `observing` to implement overloaded notation and decls.
We want to save `Info` nodes for the chosen alternative.
 -/
Lean.Elab.Term.observing : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM (Lean.Elab.Term.TermElabResult α)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∉ m₁ → k ∉ m₁ \ m₂
-- Mathlib.Analysis.Calculus.FDeriv.Norm
not_differentiableAt_norm_zero : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [Nontrivial E],
  ¬DifferentiableAt ℝ (fun x => ‖x‖) 0
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_append.aux.eq_2 : ∀ {α : Type u} (t : Stream'.WSeq α) (fst : α) (s : Stream'.WSeq α),
  Stream'.WSeq.destruct_append.aux t (some (fst, s)) = Computation.pure (some (fst, s.append t))
-- Mathlib.NumberTheory.LucasLehmer
_private.Mathlib.NumberTheory.LucasLehmer.0.LucasLehmer.norm_num_ext.sModNatTR.go.eq_2 : ∀ (q a n : ℕ),
  LucasLehmer.norm_num_ext.sModNatTR.go✝ q n.succ a = LucasLehmer.norm_num_ext.sModNatTR.go✝ q n ((a ^ 2 + (q - 2)) % q)
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Equivalence.inverse_additive : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (e : C ≌ D) [e.functor.Additive], e.inverse.Additive
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldrM_eq_foldrM_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ},
  Std.DTreeMap.foldrM (fun a x d => f a d) init t = List.foldrM f init t.keys
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsIsometricSMul.isometry_smul : ∀ {M : Type u} (X : Type w) {inst : PseudoEMetricSpace X} {inst_1 : SMul M X} [self : IsIsometricSMul M X] (c : M),
  Isometry fun x => c • x
-- Init.Data.Fin.Fold
Fin.foldl_add : ∀ {α : Sort u_1} {n m : ℕ} (f : α → Fin (n + m) → α) (x : α),
  Fin.foldl (n + m) f x =
    Fin.foldl m (fun x i => f x (Fin.natAdd n i)) (Fin.foldl n (fun x i => f x (Fin.castLE ⋯ i)) x)
-- Mathlib.Data.Nat.Prime.Basic
/-- A prime `p` satisfies `p % 2 = 1` if and only if `p ≠ 2`.  -/
Nat.Prime.mod_two_eq_one_iff_ne_two : ∀ {p : ℕ}, Nat.Prime p → (p % 2 = 1 ↔ p ≠ 2)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- `LinearMap.BilinMap.toQuadraticMap` as a linear map  -/
LinearMap.BilinMap.toQuadraticMapLinearMap : (S : Type u_1) →
  (R : Type u_3) →
    (M : Type u_4) →
      {N : Type u_5} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R N] →
                  [inst_5 : Semiring S] →
                    [inst_6 : Module S N] →
                      [inst_7 : SMulCommClass S R N] →
                        [inst_8 : SMulCommClass R S N] → LinearMap.BilinMap R M N →ₗ[S] QuadraticMap R M N
-- Mathlib.Tactic.FunProp.Types
/-- Indicated origin of a function or a statement.  -/
Mathlib.Meta.FunProp.Origin : Type
-- Mathlib.GroupTheory.Coset.Card
Subgroup.card_quotient_dvd_card : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Nat.card (α ⧸ s) ∣ Nat.card α
-- Init.Grind.Lint
/-- `#grind_lint skip thm₁ …` marks the given theorem(s) to be skipped entirely by `#grind_lint check`.
Skipped theorems are neither analyzed nor reported, but may still be used for
instantiation when analyzing other theorems.

`#grind_lint skip suffix name₁ …` marks all theorems with the given suffix(es) to be skipped.
For example, `#grind_lint skip suffix foo` will skip `bar.foo`, `qux.foo`, etc.

Examples:
```
#grind_lint skip Array.range_succ
#grind_lint skip suffix append
```
 -/
Lean.Grind.grindLintSkip : Lean.ParserDescr
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.checkDeprecated : Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM Unit
-- Mathlib.Data.Seq.Basic
Stream'.Seq.get?_set_of_ne : ∀ {α : Type u} (x : α) (s : Stream'.Seq α) {m n : ℕ}, n ≠ m → (s.set m x).get? n = s.get? n
-- Mathlib.Order.SymmDiff
sup_himp_bihimp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⊔ b ⇨ bihimp a b = bihimp a b
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.tmulEquiv_symm_apply : ∀ {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [inst : CommSemiring R] (M : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (a : ι ⊕ ι₂ → M),
  (PiTensorProduct.tmulEquiv R M).symm ((PiTensorProduct.tprod R) fun i => a i) =
    ((PiTensorProduct.tprod R) fun i => a (Sum.inl i)) ⊗ₜ[R] (PiTensorProduct.tprod R) fun i => a (Sum.inr i)
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- See `resultant_add_mul_right`.  -/
_private.Mathlib.RingTheory.Polynomial.Resultant.Basic.0.Polynomial.resultant_add_mul_monomial_right : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (r : R) (m n k : ℕ),
  k + m ≤ n → f.natDegree ≤ m → f.resultant (g + f * (Polynomial.monomial k) r) m n = f.resultant g m n
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- **Alias** of `CategoryTheory.Functor.ReflectsMonomorphisms.of_iso`. -/
CategoryTheory.Functor.reflectsMonomorphisms.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [F.ReflectsMonomorphisms] (α : F ≅ G), G.ReflectsMonomorphisms
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- Let `r` be an element of the base ring. If `y` is a conjugate root of `x`, then `y + r` is a
conjugate root of `x + r`.
 -/
IsConjRoot.add_algebraMap : ∀ {K : Type u_2} {S : Type u_4} [inst : CommRing S] [inst_1 : Field K] [inst_2 : Algebra K S] {x y : S} (r : K),
  IsConjRoot K x y → IsConjRoot K (x + (algebraMap K S) r) (y + (algebraMap K S) r)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- this is slightly different from `StronglyMeasurable.piecewise`. It can be used to show
`StronglyMeasurable (ite (x=0) 0 1)` by
`exact StronglyMeasurable.ite (measurableSet_singleton 0) stronglyMeasurable_const
stronglyMeasurable_const`, but replacing `StronglyMeasurable.ite` by
`StronglyMeasurable.piecewise` in that example proof does not work.  -/
MeasureTheory.StronglyMeasurable.ite : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {x : MeasurableSpace α} [inst : TopologicalSpace β] {p : α → Prop}
  {x_1 : DecidablePred p},
  MeasurableSet {a | p a} →
    MeasureTheory.StronglyMeasurable f →
      MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun x => if p x then f x else g x
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.getElemAsFin_val : ∀ {m : ℕ} {L : List ℕ} (hl : SimplexCategoryGenRel.IsAdmissible m L) (k : ℕ) (hK : k < L.length),
  ↑(hl.getElemAsFin k hK) = L[k]
-- Lean.Meta.Basic
/-- `withNewMCtxDepth k` executes `k` with a higher metavariable context depth,
where metavariables created outside the `withNewMCtxDepth` (with a lower depth) cannot be assigned.
If `allowLevelAssignments` is set to true, then the level metavariable depth
is not increased, and level metavariables from the outer scope can be
assigned.  (This is used by TC synthesis.)
 -/
Lean.Meta.withNewMCtxDepth : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → optParam Bool false → n α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_eq_isSome_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α}, t.contains a = (t.get? a).isSome
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.IsSheaf.of_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {K : CategoryTheory.GrothendieckTopology C}
  {F : CategoryTheory.Functor Cᵒᵖ A}, J ≤ K → CategoryTheory.Presheaf.IsSheaf K F → CategoryTheory.Presheaf.IsSheaf J F
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.commSemigroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : CommSemigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (mul : ∀ (x y : M₁), f (x * y) = f x * f y),
  Function.Injective.commSemigroup f hf mul = { toSemigroup := Function.Injective.semigroup f hf mul, mul_comm := ⋯ }
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonWorkspaceEditClientCapabilities.toJson : Lean.Lsp.WorkspaceEditClientCapabilities → Lean.Json
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findM?.eq_2 : ∀ {m : Type → Type u} [inst : Monad m] {α : Type} (p : α → m Bool) (a : α) (as : List α),
  List.findM? p (a :: as) = do
    let __do_lift ← p a
    match __do_lift with
      | true => pure (some a)
      | false => List.findM? p as
-- Mathlib.Algebra.Algebra.Defs
Algebra.compHom_smul_def : ∀ {R : Type u} {S : Type v} (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (f : S →+* R) (s : S) (x : A), s • x = f s • x
-- Std.Data.Iterators.Lemmas.Producers.Empty
Std.Iter.toIterM_empty : ∀ {β : Type u_1}, (Std.Iter.empty β).toIterM = Std.IterM.empty Id β
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- This is a technical lemma saying that `partialTraj κ a b` consists of two independent parts, the
first one being the identity. It allows to compute integrals.  -/
ProbabilityTheory.Kernel.partialTraj_eq_prod : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsSFiniteKernel (κ n)] (a b : ℕ),
  ProbabilityTheory.Kernel.partialTraj κ a b =
    (ProbabilityTheory.Kernel.id.prod ((ProbabilityTheory.Kernel.partialTraj κ a b).map (Finset.restrict₂ ⋯))).map
      (IicProdIoc a b)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_of_mem_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → Option (γ a)} {k : α}, k ∈ Std.DHashMap.filterMap f m → k ∈ m
-- Init.Data.Float.Model.Float32
/-- Compute the quotient of two `Float32.Model`.
 -/
Float32.Model.div : Float32.Model → Float32.Model → Float32.Model
-- Lean.DocString.Extension
/-- Checks whether `stx` is a docstring that was parsed as Verso rather than Markdown.
 -/
Lean.isVersoDocComment : Lean.TSyntax `Lean.Parser.Command.docComment → Bool
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.cuspFunction_smul : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ},
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (a : ℂ) (f : F) [ModularFormClass F Γ k],
        UpperHalfPlane.cuspFunction h (a • ⇑f) = a • UpperHalfPlane.cuspFunction h ⇑f
-- Mathlib.RingTheory.HahnSeries.PowerSeries
/-- If R has no zero divisors and `σ` is finite,
then `R⟦σ →₀ ℕ⟧` has no zero divisors  -/
HahnSeries.instNoZeroDivisorsFinsuppNat : ∀ {R : Type u_2} [inst : Semiring R] {σ : Type u_3} [Finite σ] [NoZeroDivisors R],
  NoZeroDivisors (HahnSeries (σ →₀ ℕ) R)
-- Mathlib.Analysis.Calculus.VectorField
ContDiff.lieBracket_vectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {m n : WithTop ℕ∞},
  ContDiff 𝕜 n V → ContDiff 𝕜 n W → m + 1 ≤ n → ContDiff 𝕜 m (VectorField.lieBracket 𝕜 V W)
-- Std.Sync.Notify
/-- A notify is a synchronization primitive that allows multiple consumers to wait
until notify is called.
 -/
Std.Notify : Type
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasure.mk.injEq : ∀ {α : Type u_2} (measureOf : Set α → ENNReal) (empty : measureOf ∅ = 0)
  (mono : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf s₁ ≤ measureOf s₂)
  (iUnion_nat :
    ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → measureOf (⋃ i, s i) ≤ ∑' (i : ℕ), measureOf (s i))
  (measureOf_1 : Set α → ENNReal) (empty_1 : measureOf_1 ∅ = 0)
  (mono_1 : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf_1 s₁ ≤ measureOf_1 s₂)
  (iUnion_nat_1 :
    ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → measureOf_1 (⋃ i, s i) ≤ ∑' (i : ℕ), measureOf_1 (s i)),
  ({ measureOf := measureOf, empty := empty, mono := mono, iUnion_nat := iUnion_nat } =
      { measureOf := measureOf_1, empty := empty_1, mono := mono_1, iUnion_nat := iUnion_nat_1 }) =
    (measureOf = measureOf_1)
-- Mathlib.RepresentationTheory.Intertwining
/-- The projection of a product representation onto its first component is an intertwining map.  -/
Representation.IntertwiningMap.fst : (A : Type u_1) →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → (ρ.prod σ).IntertwiningMap ρ
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ico_succ_top : ∀ {M : Type u_3} [inst : CommMonoid M] {a b : ℕ},
  a ≤ b → ∀ (f : ℕ → M), ∏ k ∈ Finset.Ico a (b + 1), f k = (∏ k ∈ Finset.Ico a b, f k) * f b
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₂ : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleInvRotateIso.hom.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₁)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.continuous_coe : ∀ {K : Type u_2} [inst : Field K], Continuous ⇑(algebraMap (RatFunc K) (LaurentSeries K))
-- Mathlib.Topology.Bornology.Hom
Bornology.IsBounded.image : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Bornology α] [inst_2 : Bornology β]
  [LocallyBoundedMapClass F α β] (f : F) {s : Set α}, Bornology.IsBounded s → Bornology.IsBounded (⇑f '' s)
-- Mathlib.RingTheory.IntegralDomain
/-- Every finite nontrivial cancellative monoid with zero is a group with zero.  -/
Fintype.groupWithZeroOfCancel : (M : Type u_2) →
  [inst : MonoidWithZero M] → [IsLeftCancelMulZero M] → [DecidableEq M] → [Fintype M] → [Nontrivial M] → GroupWithZero M
-- Mathlib.MeasureTheory.Function.Piecewise
/-- This is the analogue of `SimpleFunc.piecewise` for `IndexedPartition`.  -/
IndexedPartition.simpleFunc_piecewise : {ι : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MeasurableSpace α] →
        {s : ι → Set α} →
          [Finite ι] →
            IndexedPartition s →
              (∀ (i : ι), MeasurableSet (s i)) → (ι → MeasureTheory.SimpleFunc α β) → MeasureTheory.SimpleFunc α β
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.induction_on : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i → G j} [Nonempty ι] [IsDirectedOrder ι] {C : Ring.DirectLimit G f → Prop}
  (z : Ring.DirectLimit G f), (∀ (i : ι) (x : G i), C ((Ring.DirectLimit.of G f i) x)) → C z
-- Init.Data.UInt.Lemmas
UInt8.one_mul : ∀ (a : UInt8), 1 * a = a
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.rightRel_apply : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {x y : α}, (QuotientGroup.rightRel s) x y ↔ y * x⁻¹ ∈ s
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.initiallySmall_of_initial_of_essentiallySmall : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {K : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} K]
  [CategoryTheory.EssentiallySmall.{w, v₁, u₁} K] (F : CategoryTheory.Functor K J) [F.Initial],
  CategoryTheory.InitiallySmall J
-- Mathlib.Data.Set.List
/-- If each element of a list can be lifted to some type, then the whole list can be
lifted to this type.  -/
List.canLift : ∀ {α : Type u_1} {β : Type u_2} (c : β → α) (p : α → Prop) [CanLift α β c p],
  CanLift (List α) (List β) (List.map c) fun l => ∀ x ∈ l, p x
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `sbtw_const_vadd_iff`. -/
Sbtw.const_vadd : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (v : V), Sbtw R x y z → Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.isCompact : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] [ProperSpace 𝕜] (a : A), IsCompact (spectrum 𝕜 a)
-- Mathlib.Order.Filter.IsBounded
Filter.IsBounded.isCobounded_ge : ∀ {α : Type u_1} {f : Filter α} [inst : Preorder α] [f.NeBot],
  Filter.IsBounded (fun x1 x2 => x1 ≤ x2) f → Filter.IsCobounded (fun x1 x2 => x2 ≤ x1) f
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- Auxiliary lemma for `MeasureTheory.MemLp.eLpNorm_indicator_le`.  -/
MeasureTheory.MemLp.eLpNorm_indicator_le' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} {f : α → β},
  1 ≤ p →
    p ≠ ⊤ →
      MeasureTheory.MemLp f p μ →
        MeasureTheory.StronglyMeasurable f →
          ∀ {ε : ℝ},
            0 < ε →
              ∃ δ,
                ∃ (_ : 0 < δ),
                  ∀ (s : Set α),
                    MeasurableSet s →
                      μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
-- Mathlib.Analysis.SpecialFunctions.Artanh
/-- `artanh` is the right inverse of `tanh` over (-1, 1).  -/
Real.tanh_artanh : ∀ {x : ℝ}, x ∈ Set.Ioo (-1) 1 → Real.tanh (Real.artanh x) = x
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.substFunc.eq_def : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (x : L.Term α)
  (x_1 : {n : ℕ} → L.Functions n → L'.Term (Fin n)),
  x.substFunc x_1 =
    match x, x_1 with
    | FirstOrder.Language.var a, x => FirstOrder.Language.var a
    | FirstOrder.Language.func f ts, tf => (tf f).subst fun i => (ts i).substFunc fun {n} => tf
-- Lean.Elab.ConfigEval.DeriveEvalExpr
_private.Lean.Elab.ConfigEval.DeriveEvalExpr.0.Lean.Elab.ConfigEval.ensureEvalExpr.useCtor : Lean.InductiveVal → Lean.Name → Bool
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.mk : {α : Type u_3} →
  [toAddCommMonoid : AddCommMonoid α] →
    [toLinearOrder : LinearOrder α] →
      [toIsOrderedAddMonoid : IsOrderedAddMonoid α] →
        [toOrderTop : OrderTop α] →
          [toNeg : Neg α] →
            [toSub : Sub α] →
              [toZSMul : ZSMul α] →
                autoParam (∀ (a b : α), a - b = a + -b) SubNegMonoid.sub_eq_add_neg._autoParam →
                  autoParam (∀ (a : α), 0 • a = 0) SubNegMonoid.zsmul_zero'._autoParam →
                    autoParam (∀ (n : ℕ) (a : α), ↑n.succ • a = ↑n • a + a) SubNegMonoid.zsmul_succ'._autoParam →
                      autoParam (∀ (n : ℕ) (a : α), Int.negSucc n • a = -(↑n.succ • a))
                          SubNegMonoid.zsmul_neg'._autoParam →
                        [toNontrivial : Nontrivial α] →
                          (∀ (x : α), ⊤ + x = ⊤) →
                            -⊤ = ⊤ → (∀ ⦃x : α⦄, x ≠ ⊤ → x + -x = 0) → LinearOrderedAddCommGroupWithTop α