mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_of_succ_le : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), i.succ ≤ p → p.succAbove i = i.castSucc
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_Ψ₂Sq : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.Ψ₂Sq.coeff 3 = 4
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitMVar : Lean.Expr → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Mathlib.Topology.MetricSpace.IsometricSMul
Prod.instIsIsometricVAdd : ∀ {M : Type u} {X : Type w} {Y : Type u_1} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y]
  [inst_2 : VAdd M X] [IsIsometricVAdd M X] [inst_4 : VAdd M Y] [IsIsometricVAdd M Y], IsIsometricVAdd M (X × Y)
-- Lean.MetavarContext
Lean.instantiateLevelMVars : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.Level → m Lean.Level
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.hii'.eq_1 : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] [inst_2 : CategoryTheory.IsCofiltered I]
  [inst_3 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)]
  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f), A.hii' = ⋯.choose
-- Mathlib.Topology.Defs.Basic
isOpen_univ : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpen Set.univ
-- Mathlib.Order.Filter.AtTopBot.Finset
/-- `Tendsto` along `atTop` for a function precomposed with `Finset.card` reduces to `Tendsto` along
`pure (Fintype.card α)`, when `α` is finite.  -/
Filter.tendsto_comp_card_atTop_iff_of_fintype : ∀ {α : Type u_3} {β : Type u_4} [inst : Fintype α] {f : ℕ → β} {l : Filter β},
  Filter.Tendsto (fun s => f s.card) Filter.atTop l ↔ Filter.Tendsto f (pure (Fintype.card α)) l
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.prod.inr_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.inr X Y) CategoryTheory.Limits.prod.fst = 0
-- Mathlib.Data.Fintype.BigOperators
/-- The number of dependent maps `f : Π j, s j` for which the `i` component is `a` is the product
over all `j ≠ i` of `#(s j)`.

Note that this is just a composition of easier lemmas, but there's some glue missing to make that
smooth enough not to need this lemma.  -/
Fintype.card_filter_piFinset_eq_of_mem : ∀ {ι : Type u_4} {α : ι → Type u_6} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  (s : (i : ι) → Finset (α i)) (i : ι) {a : α i},
  a ∈ s i → {f ∈ Fintype.piFinset s | f i = a}.card = ∏ j ∈ Finset.univ.erase i, (s j).card
-- Mathlib.GroupTheory.Transfer
MonoidHom.transfer.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
  [inst_2 : H.FiniteIndex],
  ϕ.transfer =
    { toFun := fun g => Subgroup.leftTransversals.diff ϕ default (g • default), map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.RingTheory.Valuation.RankOne
ValuativeRel.isRankLeOne_of_rankOne : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [h : (ValuativeRel.valuation R).RankOne],
  ValuativeRel.IsRankLeOne R
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.rotateR.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (lk : α) (lv : β lk) (ll lr r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.rotateR k v lk lv ll lr r =
    if lr.size < Std.DTreeMap.Internal.ratio * ll.size then Std.DTreeMap.Internal.Impl.singleR k v lk lv ll lr r
    else
      match lr with
      | Std.DTreeMap.Internal.Impl.leaf => Std.DTreeMap.Internal.Impl.singleR k v lk lv ll lr r
      | Std.DTreeMap.Internal.Impl.inner size lrk lrv lrl lrr =>
        Std.DTreeMap.Internal.Impl.doubleR k v lk lv ll lrk lrv lrl lrr r
-- Mathlib.NumberTheory.Padics.RingHoms
_private.Mathlib.NumberTheory.Padics.RingHoms.0.Int.neg.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.negSucc n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_2 n
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_zero_one : ∀ {R : Type u} [inst : Semiring R], (Polynomial.monomial 0) 1 = 1
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
WithTop.iInf_coe_lt_top : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α}, ⨅ i, ↑(f i) < ⊤ ↔ Nonempty ι
-- Lean.Compiler.LCNF.Types
Lean.Compiler.LCNF.isPropFormerTypeQuick : Lean.Expr → Bool
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- The difference of two covariant derivatives, as a function `Γ(V) → Γ(Hom(TM, V))`.
Future lemmas will upgrade this to a one-form taking values in the endomorphisms of `V`.  -/
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic.0.IsCovariantDerivativeOn.differenceAux : {𝕜 : 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} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {V : M → Type u_6} →
                        [inst_6 : (x : M) → AddCommGroup (V x)] →
                          [inst_7 : (x : M) → Module 𝕜 (V x)] →
                            [inst_8 : (x : M) → TopologicalSpace (V x)] →
                              [∀ (x : M), IsTopologicalAddGroup (V x)] →
                                (((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x) →
                                  (((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x) →
                                    ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
-- Mathlib.Order.Basic
compl_lt : ∀ {α : Type u_2} [inst : LinearOrder α], (fun x1 x2 => x1 < x2)ᶜ = fun x1 x2 => x1 ≥ x2
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_add_one' : ∀ {y : ℝ}, y + 1 ≠ 0 → ∀ (x : NNReal), x ^ (y + 1) = x ^ y * x
-- Mathlib.Analysis.Normed.Lp.Matrix
Matrix.toLpLin_toLp : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  (p q : ENNReal) (A : Matrix m n R) (x : n → R),
  ((Matrix.toLpLin p q) A) (WithLp.toLp p x) = WithLp.toLp q ((Matrix.toLin' A) x)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instBEqSimpTheorem : BEq Lean.Meta.SimpTheorem
-- Init.Data.List.Perm
List.Perm.rec_heq : ∀ {α : Type u_1} {β : List α → Sort u_2} {f : (a : α) → (l : List α) → β l → β (a :: l)} {b : β []} {l l' : List α},
  l.Perm l' →
    (∀ {a : α} {l l' : List α} {b : β l} {b' : β l'}, l.Perm l' → b ≍ b' → f a l b ≍ f a l' b') →
      (∀ {a a' : α} {l : List α} {b : β l}, f a (a' :: l) (f a' l b) ≍ f a' (a :: l) (f a l b)) →
        List.rec b f l ≍ List.rec b f l'
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- The space of `E`-valued measures on `X`, i.e. continuous linear maps `C(X, R) → E`. (The case
`R = E` is the most important case.)

This is the same space `C(X, R) →L[R] E`, but we do not want it to inherit the default
(norm) topology, so we make a type synonym.
 -/
AbstractMeasure : (X : Type u_1) →
  (R : Type u_3) →
    (E : Type u_4) →
      [TopologicalSpace X] →
        [inst : AddCommGroup E] →
          [TopologicalSpace E] →
            [inst_2 : CommRing R] →
              [inst_3 : TopologicalSpace R] → [IsTopologicalRing R] → [Module R E] → Type (max (max u_3 u_1) u_4)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Path.zoom_del.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α)
  (r : RBTree.RBNode α)
  (h_1 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r))
  (h_2 : (x : RBTree.RBNode α) → motive x),
  (match RBTree.RBNode.node c l v r with
    | RBTree.RBNode.node c l v r => h_1 c l v r
    | x => h_2 x) =
    h_1 c l v r
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.getFunName : Lean.FVarId → List Lean.Elab.Term.LetRecToLift → Lean.Elab.TermElabM Lean.Name
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeftObjIdIso_inv_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E]
  (X : CategoryTheory.Functor C E) (X_1 : C),
  (CategoryTheory.Functor.whiskeringLeftObjIdIso.inv.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Mathlib.Tactic.DuplicateDecls
/-- Return the list of duplicate declarations, grouped by the name of the module
with the biggest `ModuleKey`.  -/
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.sortedDuplicateDeclarations : Mathlib.Tactic.DuplicateDecls.Target → Lean.CoreM (Array (String × Array (Array Lean.Name)))
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.cons.congr_simp : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g g_1 : G),
  g = g_1 →
    ∀ (u u_1 : ℤˣ) (e_u : u = u_1) (w w_1 : HNNExtension.NormalWord d) (e_w : w = w_1) (h1 : w.head ∈ d.set u)
      (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'),
      HNNExtension.NormalWord.cons g u w h1 h2 = HNNExtension.NormalWord.cons g_1 u_1 w_1 ⋯ ⋯
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
/-- Construction of the homotopy from `PInfty` to the identity using eventually
(termwise) constant homotopies from `P q` to the identity for all `q`  -/
AlgebraicTopology.DoldKan.homotopyPInftyToId : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (X : CategoryTheory.SimplicialObject C) →
        Homotopy AlgebraicTopology.DoldKan.PInfty
          (CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X))
-- Init.Data.Int.DivMod.Basic
/-- Integer modulus that uses the E-rounding convention. Usually accessed via the `%` operator.

In the E-rounding convention (Euclidean division), `Int.emod x y` satisfies `0 ≤ Int.emod x y < Int.natAbs y`
for `y ≠ 0` and `Int.ediv` is the unique function satisfying `Int.emod x y + (Int.ediv x y) * y = x`
for `y ≠ 0`.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
* `(7 : Int) % (0 : Int) = 7`
* `(0 : Int) % (7 : Int) = 0`
* `(12 : Int) % (6 : Int) = 0`
* `(12 : Int) % (-6 : Int) = 0`
* `(-12 : Int) % (6 : Int) = 0`
* `(-12 : Int) % (-6 : Int) = 0`
* `(12 : Int) % (7 : Int) = 5`
* `(12 : Int) % (-7 : Int) = 5`
* `(-12 : Int) % (7 : Int) = 2`
* `(-12 : Int) % (-7 : Int) = 2`
 -/
Int.emod : ℤ → ℤ → ℤ
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. A measurable function is greater than its mean on a set of positive
measure.  -/
MeasureTheory.measure_setLAverage_le_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
  μ s ≠ 0 →
    MeasureTheory.NullMeasurableSet s μ →
      ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤ → 0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.periodicOrbit_chain' : ∀ {α : Type u_1} (r : α → α → Prop) {f : α → α} {x : α},
  x ∈ Function.periodicPts f → (Cycle.Chain r (Function.periodicOrbit f x) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x))
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instAdd : {E : Type u_3} → [inst : Group E] → Add (GroupSeminorm E)
-- Mathlib.NumberTheory.Dioph
Poly.instCommRing : {α : Type u_1} → CommRing (Poly α)
-- Lean.Elab.Tactic.BuiltinTactic
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalRunTac.unsafe_impl_2 : Lean.TSyntax `term → Lean.Elab.TermElabM (Lean.Elab.Tactic.TacticM Unit)
-- Init.Data.Array.Lemmas
Array.findRev?_eq_find?_reverse : ∀ {α : Type} {f : α → Bool} {xs : Array α}, Array.findRev? f xs = Array.find? f xs.reverse
-- Lean.DocString.Parser
/-- Parses a character that's allowed as part of inline text. This resolves escaped characters and
performs limited lookahead for characters that only begin a different inline as part of a sequence.
 -/
Lean.Doc.Parser.inlineTextChar : Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₂.X₁ = Y
-- Mathlib.Data.List.Forall2
List.forall₂_iff : ∀ {α : Type u_1} {β : Type u_2} (R : α → β → Prop) (a : List α) (a_1 : List β),
  List.Forall₂ R a a_1 ↔
    a = [] ∧ a_1 = [] ∨ ∃ a_2 b l₁ l₂, R a_2 b ∧ List.Forall₂ R l₁ l₂ ∧ a = a_2 :: l₁ ∧ a_1 = b :: l₂
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.WEquiv.below.abs : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n}
  {motive : (a a_1 : (MvQPF.P F).W α) → MvQPF.WEquiv a a_1 → Prop} (a₀ : (MvQPF.P F).A)
  (f'₀ : ((MvQPF.P F).drop.B a₀).Arrow α) (f₀ : (MvQPF.P F).last.B a₀ → (MvQPF.P F).W α) (a₁ : (MvQPF.P F).A)
  (f'₁ : ((MvQPF.P F).drop.B a₁).Arrow α) (f₁ : (MvQPF.P F).last.B a₁ → (MvQPF.P F).W α)
  (a : MvQPF.abs ⟨a₀, (MvQPF.P F).appendContents f'₀ f₀⟩ = MvQPF.abs ⟨a₁, (MvQPF.P F).appendContents f'₁ f₁⟩),
  MvQPF.WEquiv.below ⋯
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Complex.GammaSeq_eq_betaIntegral_of_re_pos : ∀ {s : ℂ}, 0 < s.re → ∀ (n : ℕ), s.GammaSeq n = ↑n ^ s * s.betaIntegral (↑n + 1)
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.good.eq_2 : ∀ {α : Type u_1} (p : α → Prop), Encodable.good✝ p none = False
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.comp_toFunctor : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {𝒵 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴)
  (G : CategoryTheory.BasedFunctor 𝒴 𝒵), (F.comp G).toFunctor = F.comp G.toFunctor
-- Init.Core
instInhabitedTask : {a : Type u_1} → [Inhabited a] → Inhabited (Task a)
-- Mathlib.Topology.Homotopy.TopCat.Path
TopCat.Path.hom₁ : ∀ {X : TopCat} {x y : ↑X} (self : X.Path x y), (CategoryTheory.ConcreteCategory.hom self.hom) 1 = y
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
/-- The property of objects that are kernels of morphisms satisfying `W`.  -/
CategoryTheory.MorphismProperty.kernels : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.MorphismProperty C → CategoryTheory.ObjectProperty C
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- You can compute a sum over an encodable type by summing over the natural numbers
and taking a supremum. This is useful for outer measures.  -/
tsum_iSup_decode₂ : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {β : Type u_4}
  [inst_2 : Encodable β] [inst_3 : CompleteLattice α] (m : α → M),
  m ⊥ = 0 → ∀ (s : β → α), ∑' (i : ℕ), m (⨆ b ∈ Encodable.decode₂ β i, s b) = ∑' (b : β), m (s b)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- If `s i` and `t i` are linearly equivalent for every `i` in `ι`, then `⨂[R] i, s i` and
`⨂[R] i, t i` are linearly equivalent.

This is the n-ary version of `TensorProduct.congr`
 -/
PiTensorProduct.congr : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            {t : ι → Type u_11} →
              [inst_3 : (i : ι) → AddCommMonoid (t i)] →
                [inst_4 : (i : ι) → Module R (t i)] →
                  ((i : ι) → s i ≃ₗ[R] t i) → (PiTensorProduct R fun i => s i) ≃ₗ[R] PiTensorProduct R fun i => t i
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.finite_sub : ∀ {α : Type u_2} [inst : AddGroup α] {s t : Set α}, (s - t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.algEquivOfTranscendental_X : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : L)
  (h : Transcendental K f), ↑((RatFunc.algEquivOfTranscendental f h) RatFunc.X) = f
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.setLIntegral_dirac' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {a : α} {f : α → ENNReal},
  Measurable f →
    ∀ {s : Set α},
      MeasurableSet s →
        ∀ [inst_1 : Decidable (a ∈ s)], ∫⁻ (x : α) in s, f x ∂MeasureTheory.Measure.dirac a = if a ∈ s then f a else 0
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.hasSum_strict_mono : ∀ {α : Type u_1} {f g : α → NNReal} {sf sg : NNReal}, HasSum f sf → HasSum g sg → f < g → sf < sg
-- Mathlib.Analysis.BoundedVariation
/-- A real function into a finite-dimensional real vector space with bounded variation on a set
is differentiable almost everywhere in this set.  -/
LocallyBoundedVariationOn.ae_differentiableWithinAt_of_mem : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [FiniteDimensional ℝ V] {f : ℝ → V}
  {s : Set ℝ}, LocallyBoundedVariationOn f s → ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.EquivalenceJ.functor_obj : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) {X₂ : C₂}
  {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃) (f : w.StructuredArrowRightwards g),
  (CategoryTheory.TwoSquare.EquivalenceJ.functor w g).obj f =
    CategoryTheory.CostructuredArrow.mk
      (CategoryTheory.StructuredArrow.homMk (CategoryTheory.StructuredArrow.right f).hom ⋯)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flip_injective : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D]
  {F₁ F₂ : CategoryTheory.Functor B (CategoryTheory.Functor C D)}, F₁.flip = F₂.flip → F₁ = F₂
-- Mathlib.Data.Finset.Sups
Finset.sups_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s₁ s₂ t₁ t₂ : Finset α},
  s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊻ t₁ ⊆ s₂ ⊻ t₂
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.comp_right : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.SimplicialObject.Augmented C}
  (a : X ⟶ Y) (a_1 : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp a a_1).right = CategoryTheory.CategoryStruct.comp a.right a_1.right
-- Mathlib.Algebra.Homology.Monoidal
/-- Given three homological complexes `K₁`, `K₂`, and `K₃`, this asserts that for
all `j`, the functor `- ⊗ K₃.X i₃` commutes with the coproduct of
the `K₁.X i₁ ⊗ K₂.X i₂` such that `i₁ + i₂ = j`.  -/
HomologicalComplex.HasGoodTensor₁₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        {I : Type u_2} →
          [inst_3 : AddMonoid I] →
            {c : ComplexShape I} →
              [c.TensorSigns] → HomologicalComplex C c → HomologicalComplex C c → HomologicalComplex C c → Prop
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.equiv_iff_keysArray_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.keysArray = t₂.keysArray)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_one : ∀ {α : Type u_2} [inst : One α], ↑1 = 1
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- Continuity from below: the measure of the union of a sequence of (not necessarily measurable)
sets is the limit of the measures of the partial unions.  -/
MeasureTheory.FiniteMeasure.tendsto_measure_iUnion_accumulate : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_2} [inst_1 : Preorder ι] [Filter.atTop.IsCountablyGenerated]
  {μ : MeasureTheory.FiniteMeasure Ω} {f : ι → Set Ω},
  Filter.Tendsto (fun i => μ (Set.accumulate f i)) Filter.atTop (nhds (μ (⋃ i, f i)))
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- Category structure on the lax natural transformations between oplax functors.

Note that this is a scoped instance in the `Oplax.LaxTrans` namespace.  -/
CategoryTheory.Oplax.LaxTrans.homCategory : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          CategoryTheory.Category.{max u₁ w₂, max (max (max u₁ v₁) v₂) w₂} (F ⟶ G)
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.const.injEq : ∀ (moduleName identName moduleName_1 identName_1 : String),
  (Lean.Lsp.RefIdent.const moduleName identName = Lean.Lsp.RefIdent.const moduleName_1 identName_1) =
    (moduleName = moduleName_1 ∧ identName = identName_1)
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.of_comp_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {g : Y → Z} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (f : X → Y),
  Topology.IsOpenEmbedding g → (Topology.IsOpenEmbedding (g ∘ f) ↔ Topology.IsOpenEmbedding f)
-- Mathlib.CategoryTheory.Action.Basic
Action.FunctorCategoryEquivalence.counitIso_hom_app_app : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  (X : CategoryTheory.Functor (CategoryTheory.SingleObj G) V) (X_1 : CategoryTheory.SingleObj G),
  (Action.FunctorCategoryEquivalence.counitIso.hom.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.obj PUnit.unit)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_inter_distrib_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), s ∩ t ∩ u = s ∩ u ∩ (t ∩ u)
-- Mathlib.Algebra.Ring.Associator
AddMonoidHom.mulLeft₃_eq_mulRight₃ : ∀ {R : Type u_1} [inst : NonUnitalSemiring R], AddMonoidHom.mulLeft₃ = AddMonoidHom.mulRight₃
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_comp_equiv : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ι : Type u_8} {ι' : Type u_9} (e : ι' ≃ ι) (m : ι → MeasureTheory.Measure α),
  MeasureTheory.Measure.sum (m ∘ ⇑e) = MeasureTheory.Measure.sum m
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.instPreservesOneHypercoversOverForgetOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (X : C),
  (CategoryTheory.Over.forget X).PreservesOneHypercovers (J.over X) J
-- Std.Data.DTreeMap.Raw.Iterator
_private.Std.Data.DTreeMap.Raw.Iterator.0.Std.DTreeMap.Raw.valuesIter.eq_1 : ∀ {α β : Type u} {cmp : α → α → Ordering} (m : Std.DTreeMap.Raw α (fun x => β) cmp),
  m.valuesIter = Std.Iter.map (fun e => e.snd) m.iter
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addLeftMono : ∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [AddLeftMono α], AddLeftMono (WithBot α)
-- Std.Data.String.ToNat
String.isNat_append_underscore_append : ∀ {s t : String}, s.isNat = true → t.isNat = true → (s ++ "_" ++ t).isNat = true