mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Term
/-- A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

At parse time, `docComment` checks the value of the `doc.verso` option. If it is true, the contents
are parsed as Verso markup. If not, the contents are treated as plain text or Markdown. Use
`plainDocComment` to always treat the contents as plain text.

A plain text doc comment node contains a `/--` atom and then the remainder of the comment, `foo -/`
in this example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node.
A Verso comment node contains the `/--` atom, the document's syntax tree, and a closing `-/` atom.
 -/
Lean.Parser.Command.plainDocComment : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.id_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Adjunction.id.counit =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).comp (CategoryTheory.Functor.id C))
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {k : α}, k ∈ m₂ → (m₁ \ m₂).get! k = default
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.instIsIsoMapObjEIntFunctorETruncLTAppETruncLTι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a : EInt) (X : C),
  CategoryTheory.IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
_private.Std.Tactic.BVDecide.LRAT.Internal.Clause.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.match_6.splitter : {n : ℕ} →
  (motive : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → Sort u_1) →
    (acc : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool)) →
      (Unit → motive none) →
        ((map : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → motive (some map)) → motive acc
-- Mathlib.Algebra.Homology.ShortComplex.Ab
/-- In an exact sequence of abelian groups, if the first and last groups are finite, then so is the
middle one.  -/
CategoryTheory.ShortComplex.Exact.ab_finite : ∀ {S : CategoryTheory.ShortComplex Ab}, S.Exact → ∀ [Finite ↑S.X₁] [Finite ↑S.X₃], Finite ↑S.X₂
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.denseRange_coe : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K), DenseRange fun x => { toCompletion := ↑x }
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `NonUnitalRing` instance along an injective function.  -/
Function.Injective.nonUnitalRing : {R : Type u_1} →
  {S : Type u_2} →
    (f : S → R) →
      Function.Injective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : Neg S] →
                [inst_4 : Sub S] →
                  [inst_5 : SMul ℕ S] →
                    [inst_6 : SMul ℤ S] →
                      [inst_7 : NonUnitalRing R] →
                        f 0 = 0 →
                          (∀ (x y : S), f (x + y) = f x + f y) →
                            (∀ (x y : S), f (x * y) = f x * f y) →
                              (∀ (x : S), f (-x) = -f x) →
                                (∀ (x y : S), f (x - y) = f x - f y) →
                                  (∀ (n : ℕ) (x : S), f (n • x) = n • f x) →
                                    (∀ (n : ℤ) (x : S), f (n • x) = n • f x) → NonUnitalRing S
-- Mathlib.Analysis.Complex.Basic
Complex.norm_of_nonneg' : ∀ {x : ℂ}, 0 ≤ x → ↑‖x‖ = x
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.not_tautology : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)), l ∉ c.toList ∨ l.negate ∉ c.toList
-- Mathlib.Data.Nat.Factorial.SuperFactorial
Nat.superFactorial_four_mul : ∀ (n : ℕ),
  (4 * n).superFactorial = ((∏ i ∈ Finset.range (2 * n), (2 * i + 1).factorial) * 2 ^ n) ^ 2 * (2 * n).factorial
-- Mathlib.Data.Set.Basic
Set.inter_empty : ∀ {α : Type u} (a : Set α), a ∩ ∅ = ∅
-- Mathlib.RingTheory.LaurentSeries
/-- `polynomialValuationX` is an abbreviation for the `X`-adic valuation given by
`(Polynomial.idealX K).valuation K⟮X⟯`.  -/
RatFunc.polynomialValuationX : (K : Type u_2) → [inst : Field K] → Valuation (RatFunc K) (WithZero (Multiplicative ℤ))
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.unit_uniqueUpToIso_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {F G : CategoryTheory.Functor C V} (h h' : CategoryTheory.MonoidalCategory.DayConvolution F G)
  {Z : CategoryTheory.Functor (C × C) V}
  (h_1 :
    (CategoryTheory.MonoidalCategory.tensor C).comp (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.unit F G)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.tensor C).whiskerLeft (h.uniqueUpToIso h').inv) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.unit F G) h_1
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.mem_mk' : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (carrier : Set R) (zero_mem : 0 ∈ carrier)
  (add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier) (neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier)
  (mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier)
  (mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier) (x : R),
  x ∈ TwoSidedIdeal.mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right ↔ x ∈ carrier
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.bol : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.monadLift_ReaderT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α ρ : Type u} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m α)
  (Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ ps)),
  ⦃fun s => (Std.Do.wp x).apply (fun a => Q.1 a s, Q.2)⦄ MonadLift.monadLift x ⦃Q⦄
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_rename : ∀ {R : Type u} {σ : Type u_1} {τ : Type u_2} [inst : CommSemiring R] (f : σ → τ) (φ : MvPolynomial σ R),
  ((MvPolynomial.rename f) φ).degrees ⊆ Multiset.map f φ.degrees
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of an n-ary product is the sup of the nilpotency classes of the factors.  -/
Group.nilpotencyClass_pi : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] [inst_1 : Fintype η]
  [∀ (i : η), Group.IsNilpotent (Gs i)],
  Group.nilpotencyClass ((i : η) → Gs i) = Finset.univ.sup fun i => Group.nilpotencyClass (Gs i)
-- Mathlib.Data.Nat.ModEq
Nat.chineseRemainder'_lt_lcm : ∀ {m n a b : ℕ} (h : a ≡ b [MOD n.gcd m]), n ≠ 0 → m ≠ 0 → ↑(Nat.chineseRemainder' h) < n.lcm m
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {l : List α} {k : α}, k ∉ m → l.contains k = false → (m.insertMany l).get! k = default
-- Mathlib.Order.Filter.Map
Filter.map_le_map_iff_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : Filter α} {f : α → β} {s : Set α},
  s ∈ l₁ → s ∈ l₂ → Set.InjOn f s → (Filter.map f l₁ ≤ Filter.map f l₂ ↔ l₁ ≤ l₂)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Metavariable assignments for `.labelledStar` patterns in the discrimination tree.
We use a `List Key`, in the reverse order.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.PartialMatch.treeStars : Lean.Meta.RefinedDiscrTree.PartialMatch✝ → Std.HashMap ℕ (List Lean.Meta.RefinedDiscrTree.Key)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.meas_gen : ∀ {a : outParam ℝ} (outer : Filter ℝ) {inner : outParam (Filter ℝ)} [self : intervalIntegral.FTCFilter a outer inner],
  inner.IsMeasurablyGenerated
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instEmptyCollection : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → EmptyCollection (Std.ExtTreeMap α β cmp)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.appendCore.loop.match_1.splitter : (motive : ℕ → Sort u_1) → (i : ℕ) → (Unit → motive 0) → ((i' : ℕ) → motive i'.succ) → motive i
-- Mathlib.GroupTheory.Congruence.Defs
Con.instInfSet.eq_1 : ∀ {M : Type u_1} [inst : Mul M],
  Con.instInfSet = { sInf := fun S => { r := fun x y => ∀ c ∈ S, c x y, iseqv := ⋯, mul' := ⋯ } }
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- For an s-finite measure `μ`, there exists a finite measure `ν`
such that each of `μ` and `ν` is absolutely continuous with respect to the other.
 -/
MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ],
  ∃ ν, MeasureTheory.IsFiniteMeasure ν ∧ μ.AbsolutelyContinuous ν ∧ ν.AbsolutelyContinuous μ
-- Init.Data.Fin.Lemmas
Fin.cases_zero : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {zero : motive 0} {succ : (i : Fin n) → motive i.succ},
  Fin.cases zero succ 0 = zero
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.add_eq_zero_iff : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α]
  {s t : NonemptyInterval α}, s + t = 0 ↔ ∃ a b, s = NonemptyInterval.pure a ∧ t = NonemptyInterval.pure b ∧ a + b = 0
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.mk : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero R] →
      [inst_1 : Add R] →
        [inst_2 : LE R] →
          (toFun : X → X → R) →
            (∀ (x : X), toFun x x = 0) →
              (∀ (x y : X), toFun x y = toFun y x) →
                (∀ (x y z : X), toFun x z ≤ toFun x y + toFun y z) → PseudoMetric X R
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_erase_of_comm : ∀ {M : Type u_4} [inst : AddMonoid M] {l : List M} {a : M} [inst_1 : DecidableEq M],
  a ∈ l → (∀ x ∈ l, ∀ y ∈ l, x + y = y + x) → a + (l.erase a).sum = l.sum
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom : ∀ {α : Type u_1} [inst : TopologicalSpace α] [SecondCountableTopology α] {s : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis s → borel α = MeasurableSpace.generateFrom s
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.expansion_submodularity : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A B S : Finset G},
  Finset.expansion✝ K S (A ∩ B) + Finset.expansion✝ K S (A ∪ B) ≤ Finset.expansion✝ K S A + Finset.expansion✝ K S B
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algHom_eval₂_algebraMap : ∀ {R : Type u_3} {A : Type u_4} {B : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (p : Polynomial R) (f : A →ₐ[R] B) (a : A),
  f (Polynomial.eval₂ (algebraMap R A) a p) = Polynomial.eval₂ (algebraMap R B) (f a) p
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonFloat : Lean.ToJson Float
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated derivative commutes with shifting the function by a constant on the left.  -/
iteratedFDerivWithin_comp_add_left' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} (n : ℕ) (a : E),
  iteratedFDerivWithin 𝕜 n (fun z => f (a + z)) s = fun x => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Equiv.Perm.OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α},
  (∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1) →
    (Equiv.Perm.OnCycleFactors.kerParam g).range = Subgroup.centralizer {g}
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ₀Iter_coe_eq_of_ge : ∀ (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : autoParam (n + i = m) SimplexCategory.σ₀Iter_coe_eq_of_ge._auto_1),
  autoParam (i ≤ ↑j) SimplexCategory.σ₀Iter_coe_eq_of_ge._auto_3 →
    ↑((CategoryTheory.ConcreteCategory.hom (SimplexCategory.σ₀Iter i hi)) j) = ↑j - i
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.mem_carrier : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R] {s : StarSubsemiring R} {x : R}, x ∈ s.carrier ↔ x ∈ s
-- Mathlib.GroupTheory.Congruence.Defs
Con.instInhabited : {M : Type u_1} → [inst : Mul M] → Inhabited (Con M)
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.tendsto_norm_atTop : ∀ {α : Type u_1} {R : Type u_2} [inst : NormedRing R] [IsAbsoluteValue norm] (p : Polynomial R),
  0 < p.degree →
    ∀ {l : Filter α} {z : α → R},
      Filter.Tendsto (fun x => ‖z x‖) l Filter.atTop →
        Filter.Tendsto (fun x => ‖Polynomial.eval (z x) p‖) l Filter.atTop
-- Std.Data.ExtHashMap.Lemmas
_private.Std.Data.ExtHashMap.Lemmas.0.Std.ExtHashMap.ext : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m m' : Std.ExtHashMap α β}, m.inner = m'.inner → m = m'
-- Lean.Environment
Lean.EffectiveImport.mk : Lean.Import → Lean.IRPhases → Bool → Lean.EffectiveImport
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_erase_self : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, (m.erase k).get! k = default
-- Mathlib.Algebra.Field.Defs
/-- A `Semifield` is a `CommSemiring` with multiplicative inverses for nonzero elements.

An instance of `Semifield K` includes maps `nnratCast : ℚ≥0 → K` and `nnqsmul : ℚ≥0 → K → K`.
Those two fields are needed to implement the `DivisionSemiring K → Algebra ℚ≥0 K` instance since we
need to control the specific definitions for some special cases of `K` (in particular `K = ℚ≥0`
itself). See also note [forgetful inheritance].

If the semifield has positive characteristic `p`, our division by zero convention forces
`nnratCast (1 / p) = 1 / 0 = 0`.  -/
Semifield : Type u_2 → Type u_2
-- Mathlib.Logic.Godel.GodelBetaFunction
/-- **Gödel's Beta Function Lemma**  -/
Nat.beta_unbeta_coe : ∀ (l : List ℕ) (i : Fin l.length), (Nat.unbeta l).beta ↑i = l[i]
-- Std.Data.TreeMap.Raw.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.TreeMap.Raw.alter : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → (Option β → Option β) → Std.TreeMap.Raw α β cmp
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Functor.isLeftAdjoint_comp_iff_left : ∀ {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 D)
  (G : CategoryTheory.Functor D E) [G.IsEquivalence], (F.comp G).IsLeftAdjoint ↔ F.IsLeftAdjoint
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insert k v},
  (m.insert k v).getKey a h₁ = if h₂ : (k == a) = true then k else m.getKey a ⋯
-- Lean.Meta.LazyDiscrTree
/-- `findMatches` searches for entries in a lazily initialized discriminator tree.

* `ref` is a process-global `IO.Ref` for caching the import lazy discriminator tree.
* `addEntry` is the function for creating discriminator tree entries from constants.
* `droppedKeys` contains keys we do not want to consider when searching for matches.
  It is used for dropping very general keys.
* `droppedEntriesRef` optionally stores entries dropped from the tree for later use.
 -/
Lean.Meta.LazyDiscrTree.findMatches : {α : Type} →
  IO.Ref (Option (Lean.Meta.LazyDiscrTree α)) →
    (Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) →
      optParam (List (List Lean.Meta.LazyDiscrTree.Key)) [] →
        optParam ℕ 1000 → optParam (Option (IO.Ref (Option (Array α)))) none → Lean.Expr → Lean.MetaM (Array α)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonInitializationOptions : Lean.FromJson Lean.Lsp.InitializationOptions
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.commGroup_isMulCommutative : ∀ {G : Type u_3} [inst : CommGroup G] (H : Subgroup G), IsMulCommutative ↥H
-- Init.Grind.ToIntLemmas
_private.Init.Grind.ToIntLemmas.0.Lean.Grind.IntInterval.lo?.match_1.splitter : (motive : Lean.Grind.IntInterval → Sort u_1) →
  (i : Lean.Grind.IntInterval) →
    ((lo hi : ℤ) → motive (Lean.Grind.IntInterval.co lo hi)) →
      ((lo : ℤ) → motive (Lean.Grind.IntInterval.ci lo)) →
        ((hi : ℤ) → motive (Lean.Grind.IntInterval.io hi)) → (Unit → motive Lean.Grind.IntInterval.ii) → motive i
-- Mathlib.NumberTheory.AbelSummation
/-- Specialized version of `sum_mul_eq_sub_sub_integral_mul` for the case `a = 0`  -/
sum_mul_eq_sub_integral_mul : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} {b : ℝ},
  0 ≤ b →
    (∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t) →
      MeasureTheory.IntegrableOn (deriv f) (Set.Icc 0 b) MeasureTheory.volume →
        ∑ k ∈ Finset.Icc 0 ⌊b⌋₊, f ↑k * c k =
          f b * ∑ k ∈ Finset.Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k
-- Init.Data.String.Basic
String.Slice.endExclusive_slice : ∀ {s : String.Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd},
  (s.slice newStart newEnd h).endExclusive = newEnd.str
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A B : CategoryTheory.Endofunctor.Coalgebra F} {f g : A ⟶ B},
  f = g ↔ autoParam (f.f = g.f) CategoryTheory.Endofunctor.Coalgebra.ext._auto_1
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- Given a multivariate formal power series `p` and a subring `T` that contains the
coefficients of `p`, return the corresponding multivariate formal power series
whose coefficients are in `T`.  -/
MvPowerSeries.toSubring : {σ : Type u_1} →
  {R : Type u_2} →
    [inst : Ring R] →
      (p : MvPowerSeries σ R) → (T : Subring R) → (∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff n) p ∈ T) → MvPowerSeries σ ↥T
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.range_lift : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {K : Type u_3} [inst_2 : AddGroup K]
  (f : G →+ K) (g : H →+ K), (AddMonoid.Coprod.lift f g).range = f.range ⊔ g.range
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instAlgebra_1 : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] →
      {S : Type u_3} →
        [inst_1 : CommSemiring R] → [inst_2 : Ring S] → [Algebra R S] → (v : Valuation S Γ₀) → Algebra R (WithVal v)
-- Mathlib.RingTheory.Localization.FractionRing
/-- Given commutative rings `A, B` where `B` is an integral domain, with fraction rings `K`, `L`
and an injective ring hom `j : A →+* B`, we get a ring hom
sending `z : K` to `g (j x) * (g (j y))⁻¹`, where `(x, y) : A × (NonZeroDivisors A)` are
such that `z = f x * (f y)⁻¹`.  -/
IsFractionRing.map : {A : Type u_8} →
  {B : Type u_9} →
    {K : Type u_10} →
      {L : Type u_11} →
        [inst : CommRing A] →
          [inst_1 : CommRing B] →
            [IsDomain B] →
              [inst_3 : CommRing K] →
                [inst_4 : Algebra A K] →
                  [IsFractionRing A K] →
                    [inst_6 : CommRing L] →
                      [inst_7 : Algebra B L] → [IsFractionRing B L] → {j : A →+* B} → Function.Injective ⇑j → K →+* L
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- This propositional typeclass ensures that `UpwardEnumerable.succ?` will never return `none`.
In other words, it ensures that there will always be a successor.
 -/
Std.PRange.InfinitelyUpwardEnumerable : (α : Type u) → [Std.PRange.UpwardEnumerable α] → Prop
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_minKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : l.isEmpty = false},
      Std.Internal.List.getKey! (Std.Internal.List.minKey l he) l = Std.Internal.List.minKey l he
-- Init.Meta
Lean.Parser.Tactic.declareSimpLikeTactic : Lean.ParserDescr
-- Mathlib.Order.Heyting.Basic
/-- `aᶜ` is defined as `a ⇨ ⊥`  -/
HeytingAlgebra.himp_bot : ∀ {α : Type u_4} [self : HeytingAlgebra α] (a : α), a ⇨ ⊥ = aᶜ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, ∅.size = 0
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {X : C}
  {R : CategoryTheory.Presieve X}, R ∈ J.coverings X ↔ ∃ 𝒰, R = CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.hasLeftDualRightDual : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X : C} → [inst_2 : CategoryTheory.HasRightDual X] → CategoryTheory.HasLeftDual Xᘁ
-- Mathlib.Topology.SeparatedMap
t2space_iff_isSeparatedMap : ∀ {X : Type u_1} {Y : Sort u_2} [inst : TopologicalSpace X] (y : Y), T2Space X ↔ IsSeparatedMap fun x => y
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsMaxOn.lineDerivWithin_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E},
  IsMaxOn f s a → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → lineDerivWithin ℝ f s a b = 0
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- One direction of `Real.log_lt_iff_lt_exp` without positivity assumption.  -/
Real.lt_exp_of_log_lt : ∀ {x y : ℝ}, Real.log x < y → x < Real.exp y
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.innerHornInclusions_le_monomorphisms : SSet.innerHornInclusions ≤ CategoryTheory.MorphismProperty.monomorphisms SSet
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsFraisseLimit.mk : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} {M : Type w} [inst : L.Structure M]
  [inst_1 : Countable ((l : ℕ) × L.Functions l)] [inst_2 : Countable M],
  L.IsUltrahomogeneous M → L.age M = K → FirstOrder.Language.IsFraisseLimit K M
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.toFinsuppAntidiag_mem_finsuppAntidiag : ∀ {n : ℕ} (p : n.Partition), p.toFinsuppAntidiag ∈ (Finset.Icc 1 n).finsuppAntidiag n
-- Mathlib.Logic.Equiv.Sum
/-- For any predicate `p` on `α`,
the sum of the two subtypes `{a // p a}` and its complement `{a // ¬ p a}`
is naturally equivalent to `α`.

See `subtypeOrEquiv` for sum types over subtypes `{x // p x}` and `{x // q x}`
that are not necessarily `IsCompl p q`. See also `Equiv.Set.sumCompl` for a version on sets.  -/
Equiv.sumCompl : {α : Type u_9} → (p : α → Prop) → [DecidablePred p] → { a // p a } ⊕ { a // ¬p a } ≃ α