mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.card_incidenceSet_eq_degree : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)] [inst_1 : DecidableEq V],
  Fintype.card ↑(G.incidenceSet v) = G.degree v
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.of_isLocalization : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Ideal R) (hp : p ∈ minimalPrimes R) (S : Type u_2)
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [IsLocalization.AtPrime S p], Ring.KrullDimLE 0 S
-- Init.Data.SInt.Lemmas
ISize.ofNat_mul : ∀ (a b : ℕ), ISize.ofNat (a * b) = ISize.ofNat a * ISize.ofNat b
-- Mathlib.CategoryTheory.Sites.Descent.IsStack
CategoryTheory.Pseudofunctor.IsStack.of_isStackFor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  {J : CategoryTheory.GrothendieckTopology C}, (∀ (S : C), ∀ R ∈ J S, F.IsStackFor R.arrows) → F.IsStack J
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {Z : CategoryTheory.Functor C (Type w)} (h : F₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.equalizer.ι f g)
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.equalizer.ι f g)
      (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Order.ModularLattice
/-- A codisjoint element can be shrunk to a complementary element.  -/
Codisjoint.exists_isCompl : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] [inst_2 : BoundedOrder α] [ComplementedLattice α] {a b : α},
  Codisjoint a b → ∃ a' ≤ a, IsCompl a' b
-- Init.Data.Array.Lemmas
Array.getElem_swap_left : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ} {hi : i < xs.size} {hj : j < xs.size}, (xs.swap i j hi hj)[i] = xs[j]
-- Mathlib.Analysis.Seminorm
Seminorm.ball_finset_sup' : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : ι → Seminorm 𝕜 E) (s : Finset ι) (H : s.Nonempty) (e : E) (r : ℝ),
  (s.sup' H p).ball e r = s.inf' H fun i => (p i).ball e r
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.comp_liftCycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A' A : C}
  (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (α : A' ⟶ A)
  {Z : C} (h : K.cycles i ⟶ Z),
  CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj hk) h) =
    CategoryTheory.CategoryStruct.comp (K.liftCycles (CategoryTheory.CategoryStruct.comp α k) j hj ⋯) h
-- Init.Data.Vector.Lemmas
Vector.foldl_eq_foldlM : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {f : β → α → β} {b : β} {xs : Vector α n},
  Vector.foldl f b xs = (Vector.foldlM (fun x1 x2 => pure (f x1 x2)) b xs).run
-- Mathlib.Probability.Distributions.Pareto
ProbabilityTheory.paretoPDF_of_lt : ∀ {t r x : ℝ}, x < t → ProbabilityTheory.paretoPDF t r x = 0
-- Mathlib.Data.EReal.Basic
EReal.bot_lt_coe_ennreal : ∀ (x : ENNReal), ⊥ < ↑x
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.argEquiv_symm_apply : ⇑Circle.argEquiv.symm = ⇑Circle.exp ∘ Subtype.val
-- Init.Data.UInt.Basic
instPowUInt8Nat : Pow UInt8 ℕ
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.Sign.forall_iff : ∀ {p : Float.Model.UnpackedFloat.Sign → Prop},
  (∀ (s : Float.Model.UnpackedFloat.Sign), p s) ↔
    p Float.Model.UnpackedFloat.Sign.positive ∧ p Float.Model.UnpackedFloat.Sign.negative
-- Mathlib.SetTheory.ZFC.PSet
/-- The image of a function from pre-sets to pre-sets.  -/
PSet.image : (PSet.{u} → PSet.{u}) → PSet.{u} → PSet.{u}
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_le_size_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.size ≤ (t.insert k).size
-- Init.Data.Slice.Array.Iterator
instIteratorSubarrayIteratorId : {α : Type u} → Std.Iterator (SubarrayIterator α) Id α
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.tensorModelOfHasCoeffsInv_comp : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀],
  (P.tensorModelOfHasCoeffsInv R₀).comp (P.tensorModelOfHasCoeffsHom R₀) =
    AlgHom.id R (TensorProduct R₀ R (Algebra.Presentation.ModelOfHasCoeffs R₀))
-- Mathlib.Data.Num.Lemmas
PosNum.natSize.eq_1 : PosNum.one.natSize = 1
-- Mathlib.Analysis.Complex.Hadamard
/-- `sSup` of `norm` translated by `ε > 0` is positive applied to the image of `f` on the
vertical line `re z = x`  -/
Complex.HadamardThreeLines.sSupNormIm_eps_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) {ε : ℝ},
  ε > 0 → ∀ (x : ℝ), 0 < ε + Complex.HadamardThreeLines.sSupNormIm f x
-- Mathlib.Analysis.Seminorm
Seminorm.instFunLike : {𝕜 : Type u_3} →
  {E : Type u_7} → [inst : SeminormedRing 𝕜] → [inst_1 : AddGroup E] → [inst_2 : SMul 𝕜 E] → FunLike (Seminorm 𝕜 E) E ℝ
-- Mathlib.Topology.Category.UniformSpace
/-- The underlying uniform space.  -/
UniformSpaceCat.carrier : UniformSpaceCat → Type u
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.MonadShareCommon.isDebugEnabled : {m : Type → Type} → [self : Lean.Meta.Sym.Internal.MonadShareCommon m] → m Bool
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.tan_arg : ∀ (x : ℂ), Real.tan x.arg = x.im / x.re
-- Mathlib.Topology.Order.Lattice
ContinuousAt.finset_sup : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [inst_3 : OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} {x : X},
  (∀ i ∈ s, ContinuousAt (f i) x) → ContinuousAt (s.sup f) x
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k k' fallback : α},
  (k == k') = true → m.getD k fallback = m.getD k' fallback
-- Lean.Environment
Lean.PersistentEnvExtensionDescrCore.mk.injEq : ∀ {α β σ : Type} (name : autoParam Lean.Name Lean.PersistentEnvExtensionDescrCore.name._autoParam) (mkInitial : IO σ)
  (addImportedFn : Array (Array α) → Lean.ImportM σ) (addEntryFn : σ → β → σ)
  (exportEntriesFnEx : Lean.Environment → σ → Lean.OLeanEntries (Array α)) (statsFn : σ → Std.Format)
  (asyncMode : Lean.EnvExtension.AsyncMode) (replay? : Option (Lean.ReplayFn σ))
  (name_1 : autoParam Lean.Name Lean.PersistentEnvExtensionDescrCore.name._autoParam) (mkInitial_1 : IO σ)
  (addImportedFn_1 : Array (Array α) → Lean.ImportM σ) (addEntryFn_1 : σ → β → σ)
  (exportEntriesFnEx_1 : Lean.Environment → σ → Lean.OLeanEntries (Array α)) (statsFn_1 : σ → Std.Format)
  (asyncMode_1 : Lean.EnvExtension.AsyncMode) (replay?_1 : Option (Lean.ReplayFn σ)),
  ({ name := name, mkInitial := mkInitial, addImportedFn := addImportedFn, addEntryFn := addEntryFn,
        exportEntriesFnEx := exportEntriesFnEx, statsFn := statsFn, asyncMode := asyncMode, replay? := replay? } =
      { name := name_1, mkInitial := mkInitial_1, addImportedFn := addImportedFn_1, addEntryFn := addEntryFn_1,
        exportEntriesFnEx := exportEntriesFnEx_1, statsFn := statsFn_1, asyncMode := asyncMode_1,
        replay? := replay?_1 }) =
    (name = name_1 ∧
      mkInitial = mkInitial_1 ∧
        addImportedFn = addImportedFn_1 ∧
          addEntryFn = addEntryFn_1 ∧
            exportEntriesFnEx = exportEntriesFnEx_1 ∧
              statsFn = statsFn_1 ∧ asyncMode = asyncMode_1 ∧ replay? = replay?_1)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.isPath_cons' : ∀ {F : PFunctor.{uA, uB}} {xs : PFunctor.Approx.Path F} {a : F.A} {f : F.B a → F.M} {i : F.B a},
  PFunctor.M.IsPath (⟨a, i⟩ :: xs) (PFunctor.M.mk ⟨a, f⟩) → PFunctor.M.IsPath xs (f i)
-- Init.Control.Lawful.Basic
seq_eq_bind : ∀ {m : Type u → Type u_1} {α β : Type u} [inst : Monad m] [LawfulMonad m] (mf : m (α → β)) (x : m α),
  mf <*> x = do
    let f ← mf
    f <$> x
-- Mathlib.Data.Nat.ModEq
/-- Modular equality. `n.ModEq a b`, or `a ≡ b [MOD n]`, means that `a % n = b % n`.  -/
«term_≡_[MOD_]» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
self_le_mul_left : ∀ {α : Type u} [inst : Mul α] [inst_1 : LE α] [CanonicallyOrderedMul α] (a b : α), a ≤ b * a
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instIntCast : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → IntCast (CauSeq β abv)
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.nonDegenerate_iff_of_isIso : ∀ {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.IsIso f] {n : ℕ} (x : X.obj (Opposite.op { len := n })),
  (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) x ∈ Y.nonDegenerate n ↔ x ∈ X.nonDegenerate n
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visitChild.match_1.eq_6 : ∀ (motive : Lean.Expr → Sort u_1) (u : Lean.Level) (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a))
  (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (e : Lean.Expr) → motive e),
  (match Lean.Expr.sort u with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | e => h_7 e) =
    h_6 u
-- Mathlib.Analysis.Normed.Group.Pointwise
closedBall_div_singleton : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x y : E),
  Metric.closedBall x δ / {y} = Metric.closedBall (x / y) δ
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Pretrivialization.continuousLinearMap.eq_1 : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj)
  (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) [inst_13 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : (x : B) → TopologicalSpace (E₂ x)] [inst_16 : FiberBundle F₂ E₂]
  [inst_17 : Bundle.Trivialization.IsLinear 𝕜₁ e₁] [inst_18 : Bundle.Trivialization.IsLinear 𝕜₂ e₂],
  Bundle.Pretrivialization.continuousLinearMap σ e₁ e₂ =
    {
      toFun := fun p =>
        (p.proj,
          Bundle.Trivialization.continuousLinearMapAt 𝕜₂ e₂ p.proj ∘SL
            p.snd ∘SL Bundle.Trivialization.symmL 𝕜₁ e₁ p.proj),
      invFun := fun p =>
        ⟨p.1, Bundle.Trivialization.symmL 𝕜₂ e₂ p.1 ∘SL p.2 ∘SL Bundle.Trivialization.continuousLinearMapAt 𝕜₁ e₁ p.1⟩,
      source := Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet), target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ,
      map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_target := ⋯,
      baseSet := e₁.baseSet ∩ e₂.baseSet, open_baseSet := ⋯, source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- Any morphism `k : Y ⟶ W` satisfying `∀ j₁ j₂, f j₁ ≫ k = f j₂ ≫ k` factors through the
wide coequalizer of `f` via `wideCoequalizer.desc : wideCoequalizer f ⟶ W`.  -/
CategoryTheory.Limits.wideCoequalizer.desc : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f] →
            [Nonempty J] →
              {W : C} →
                (k : Y ⟶ W) →
                  (∀ (j₁ j₂ : J),
                      CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k) →
                    (CategoryTheory.Limits.wideCoequalizer f ⟶ W)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv_subset_sdiv : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s₁ s₂ t₁ t₂ : Set β}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ /ₛ t₁ ⊆ s₂ /ₛ t₂
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_mono : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  f ≤ᵐ[μ] g → μ.withDensity f ≤ μ.withDensity g
-- Init.Prelude
/-- `And.intro : a → b → a ∧ b` is the constructor for the And operation.  -/
And.intro : ∀ {a b : Prop}, a → b → a ∧ b
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.toExtendScalars_val : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u_7}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T]
  (P : Algebra.Generators R T ι) (n : ι), P.toExtendScalars.val n = MvPolynomial.X n
-- Mathlib.Data.Int.Init
Int.mul_dvd_of_dvd_div : ∀ {a b c : ℤ}, c ∣ b → a ∣ b / c → c * a ∣ b
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The composition `t.truncGE a ⋙ t.truncGE b`.  -/
CategoryTheory.Triangulated.TStructure.truncLEGE : {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] →
              CategoryTheory.Triangulated.TStructure C → ℤ → ℤ → CategoryTheory.Functor C C
-- Init.Data.Range.Polymorphic.SInt
Int8.instUpwardEnumerable : Std.PRange.UpwardEnumerable Int8
-- Batteries.Data.AssocList
Batteries.AssocList.toList_replace : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (b : β) (l : Batteries.AssocList α β),
  (Batteries.AssocList.replace a b l).toList = List.replaceF (fun x => bif x.1 == a then some (a, b) else none) l.toList
-- Mathlib.Algebra.Group.Torsion
nsmul_eq_zero_iff_right : ∀ {M : Type u_1} [inst : AddMonoid M] [IsAddTorsionFree M] {n : ℕ} {a : M}, n ≠ 0 → (n • a = 0 ↔ a = 0)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.orthogonalProjectionFn_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (v : E),
  Submodule.orthogonalProjectionFn v = ↑(K.orthogonalProjectionOnto v)
-- Mathlib.RepresentationTheory.Invariants
Rep.instLinearModuleCatInvariantsFunctor : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Group G],
  CategoryTheory.Functor.Linear k (Rep.invariantsFunctor k G)
-- Mathlib.GroupTheory.Congruence.Basic
/-- The congruence relation on a monoid `M` from a submonoid of `M × M` for which membership
is an equivalence relation.  -/
Con.ofSubmonoid : {M : Type u_1} → [inst : MulOneClass M] → (N : Submonoid (M × M)) → (Equivalence fun x y => (x, y) ∈ N) → Con M
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prodComparisonNatIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasBinaryProducts C]
  [inst_3 : CategoryTheory.Limits.HasBinaryProducts D] (A : C)
  [inst_4 : ∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)],
  (CategoryTheory.Limits.prodComparisonNatIso F A).hom = CategoryTheory.Limits.prodComparisonNatTrans F A
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.Hom.mk.injEq : ∀ {X Y : Bipointed} (toFun : X.X → Y.X) (map_fst : toFun X.toProd.1 = Y.toProd.1)
  (map_snd : toFun X.toProd.2 = Y.toProd.2) (toFun_1 : X.X → Y.X) (map_fst_1 : toFun_1 X.toProd.1 = Y.toProd.1)
  (map_snd_1 : toFun_1 X.toProd.2 = Y.toProd.2),
  ({ toFun := toFun, map_fst := map_fst, map_snd := map_snd } =
      { toFun := toFun_1, map_fst := map_fst_1, map_snd := map_snd_1 }) =
    (toFun = toFun_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_union_le_size_add_size : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF), (m₁.union m₂ ⋯ ⋯).size ≤ m₁.size + m₂.size
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.inner_right_rankOne_apply : ∀ {𝕜 : Type u_4} {F : Type u_6} {G : Type u_7} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F]
  [inst_2 : InnerProductSpace 𝕜 F] [inst_3 : SeminormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G] (x y : F)
  (z w : G), inner 𝕜 x ((((InnerProductSpace.rankOne 𝕜) y) z) w) = inner 𝕜 x y * inner 𝕜 z w
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.updateLast : {α : Type u_1} → (a : Array α) → (α → Option α) → Fin (a.size + 1) → Option (Array α)
-- Mathlib.Algebra.Vertex.VertexOperator
/-- In the literature, the `n`th normalized coefficient of a vertex operator `A` is written as
either `Aₙ` or `A(n)`.  -/
VertexOperator.«term_[[_]]» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.toAddSubmonoid_mono : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R], Monotone NonUnitalSubsemiring.toAddSubmonoid
-- Mathlib.Data.Finset.Fold
Finset.fold_max_lt : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [inst : LinearOrder β] (c : β),
  Finset.fold max b f s < c ↔ b < c ∧ ∀ x ∈ s, f x < c
-- Mathlib.Tactic.Linter.Style
/-- `findDollarSyntax stx` extracts from `stx` the syntax nodes of `kind` `$`.  -/
Mathlib.Linter.Style.dollarSyntax.findDollarSyntax : Lean.Syntax → Array Lean.Syntax
-- Mathlib.Data.NNRat.Defs
instInhabitedNNRat : Inhabited ℚ≥0
-- Mathlib.Analysis.Normed.Group.Defs
/-- A normed group is an additive group endowed with a norm for which `dist x y = ‖-x + y‖` defines
a metric space structure.  -/
NormedAddCommGroup : Type u_8 → Type u_8
-- Mathlib.NumberTheory.LSeries.Convolution
/-- The L-series of the convolution product `f ⍟ g` of two sequences `f` and `g`
equals the product of their L-series, assuming both L-series converge.  -/
LSeriesHasSum.convolution : ∀ {f g : ℕ → ℂ} {s a b : ℂ},
  LSeriesHasSum f s a → LSeriesHasSum g s b → LSeriesHasSum (LSeries.convolution f g) s (a * b)
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Sheaf.classifier_χ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  {U X : CategoryTheory.Sheaf J (Type (max u v))} (m : U ⟶ X) (x : CategoryTheory.Mono m),
  (CategoryTheory.Sheaf.classifier J).χ m = CategoryTheory.Sheaf.χ m
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)),
  ((CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X).obj Y).left =
    CategoryTheory.StructuredArrow.mk Y.hom.left
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- The integral defining the `Γ` function converges for complex `s` with `0 < re s`.

This is proved by reduction to the real case.  -/
Complex.GammaIntegral_convergent : ∀ {s : ℂ},
  0 < s.re → MeasureTheory.IntegrableOn (fun x => ↑(Real.exp (-x)) * ↑x ^ (s - 1)) (Set.Ioi 0) MeasureTheory.volume
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_associator_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)),
  (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.mapComp f g).hom.toNatTrans.app X))
        (CategoryTheory.CategoryStruct.comp ((self.mapComp g h).inv.toNatTrans.app ((self.map f).toFunctor.obj X))
          ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv.toNatTrans.app X)))
-- Mathlib.Data.Vector.Basic
List.Vector.inductionOn_nil : ∀ {α : Type u_1} {C : {n : ℕ} → List.Vector α n → Sort u_6} (nil : C List.Vector.nil)
  (cons : {n : ℕ} → {x : α} → {w : List.Vector α n} → C w → C (x ::ᵥ w)),
  (List.Vector.nil.inductionOn nil fun {n} {x} {w} => cons) = nil
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.opHomeomorph.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M],
  AddOpposite.opHomeomorph = { toEquiv := AddOpposite.opEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
RingHom.IsIntegral.to_finite : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.IsIntegral → f.FiniteType → f.Finite
-- Mathlib.Topology.Homotopy.Path
/-- Evaluating a path homotopy at an intermediate point, giving us a `Path`.
 -/
Path.Homotopy.eval : {X : Type u} →
  [inst : TopologicalSpace X] → {x₀ x₁ : X} → {p₀ p₁ : Path x₀ x₁} → p₀.Homotopy p₁ → ↑unitInterval → Path x₀ x₁
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
OnePoint.IsZeroAt.add : ∀ {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} {f' : UpperHalfPlane → ℂ},
  c.IsZeroAt f k → c.IsZeroAt f' k → c.IsZeroAt (f + f') k
-- Mathlib.Tactic.CrossRefAttribute
/-- Extract the underlying tag as a string from a `stacksTag` node.  -/
Lean.TSyntax.getStacksTag : Lean.TSyntax Mathlib.CrossRef.stacksTagKind → Lean.CoreM String
-- Mathlib.Data.Fin.Tuple.Basic
/-- Append a tuple of length `m` to a tuple of length `n` to get a tuple of length `m + n`.
This is a non-dependent version of `Fin.add_cases`.  -/
Fin.append : {m n : ℕ} → {α : Sort u_1} → (Fin m → α) → (Fin n → α) → Fin (m + n) → α
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulLeftMono.toPosMulMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulLeftMono α], PosMulMono α
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_eq_mapIdx : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : (i : ℕ) → α → i < n → β} {g : ℕ → α → β},
  (∀ (i : ℕ) (h : i < n), f i xs[i] h = g i xs[i]) → xs.mapFinIdx f = Vector.mapIdx g xs
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_diagonal : ∀ {R : Type u_6} [inst : AddCommMonoid R] {o : Type u_8} [inst_1 : Fintype o] [inst_2 : DecidableEq o] (d : o → R),
  (Matrix.diagonal d).trace = ∑ i, d i