mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.Compact
/-- If a continuous function lies strictly above `a` on a compact set,
it has a lower bound strictly above `a`.  -/
IsCompact.exists_forall_le' : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIicTopology α] [NoMaxOrder α] {f : β → α} {s : Set β},
  IsCompact s → ContinuousOn f s → ∀ {a : α}, (∀ b ∈ s, a < f b) → ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.Gamma_integrand_intervalIntegrable : ∀ (s : ℂ) {X : ℝ},
  0 < s.re → 0 ≤ X → IntervalIntegrable (fun x => ↑(Real.exp (-x)) * ↑x ^ (s - 1)) MeasureTheory.volume 0 X
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : β → β}, (m.modify k f)[k]? = Option.map f m[k]?
-- Init.Data.Option.Monadic
Option.bindM_none : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Pure m] (f : α → m (Option β)),
  Option.bindM f none = pure none
-- Lean.ToLevel
/-- `ToLevel` for `imax u v`. This is not an instance since it causes divergence.  -/
Lean.ToLevel.imax : [Lean.ToLevel] → [Lean.ToLevel] → Lean.ToLevel
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- Constant to use for field completion terminfo.  -/
Lean.Elab.ConfigEval.EvalConfigItemHandler.struct? : Lean.Elab.ConfigEval.EvalConfigItemHandler → Option Lean.Name
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → (Std.ExtDTreeMap.Const.unitOfList l cmp).size = l.length
-- Mathlib.Algebra.Homology.Localization
/-- The functor `F.mapHomologicalComplexUpToQuasiIso c` is induced by
`F.mapHomotopyCategory c`.  -/
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh : {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] →
        (F : CategoryTheory.Functor C D) →
          {ι : Type u_3} →
            (c : ComplexShape ι) →
              [inst_2 : CategoryTheory.Preadditive C] →
                [inst_3 : CategoryTheory.Preadditive D] →
                  [inst_4 : CategoryTheory.CategoryWithHomology C] →
                    [inst_5 : CategoryTheory.CategoryWithHomology D] →
                      [inst_6 : (HomologicalComplex.quasiIso D c).HasLocalization] →
                        [inst_7 : F.Additive] →
                          [inst_8 : F.PreservesHomology] →
                            [inst_9 : (HomologicalComplex.quasiIso C c).HasLocalization] →
                              [inst_10 : c.QFactorsThroughHomotopy C] →
                                [inst_11 : c.QFactorsThroughHomotopy D] →
                                  [(HomotopyCategory.quotient C c).IsLocalization
                                        (HomologicalComplex.homotopyEquivalences C c)] →
                                    HomologicalComplexUpToQuasiIso.Qh.comp (F.mapHomologicalComplexUpToQuasiIso c) ≅
                                      (F.mapHomotopyCategory c).comp HomologicalComplexUpToQuasiIso.Qh
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.IsSimple.instIsIrreducible : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSimple R L], LieModule.IsIrreducible R L L
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.associated_rightInverse : ∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : CommSemiring S] [inst_6 : Algebra S R]
  [inst_7 : Module S N] [inst_8 : IsScalarTower S R N] [inst_9 : Invertible 2],
  Function.RightInverse (⇑(QuadraticMap.associatedHom S)) LinearMap.BilinMap.toQuadraticMap
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.row_submatrix : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {m₀ : Type u_10} {n₀ : Type u_11} (A : Matrix m n α) (r : m₀ → m)
  (c : n₀ → n) (i : m₀), (A.submatrix r c).row i = (A.submatrix id c).row (r i)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ)
  {x : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I)) ↔
    x ∈ ⇑(NumberField.mixedEmbedding K) '' ↑↑I
-- Init.Data.Dyadic.Round
_private.Init.Data.Dyadic.Round.0.Rat.toDyadic.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_1 n
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mapEquiv_sup_eq : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] [inst_7 : ContinuousAdd N] [inst_8 : ContinuousConstSMul R N] [inst_9 : ContinuousAdd M]
  [inst_10 : ContinuousConstSMul R M] (f : M ≃L[R] N) {s t : ClosedSubmodule R M},
  (ClosedSubmodule.mapEquiv f) (s ⊔ t) = (ClosedSubmodule.mapEquiv f) s ⊔ (ClosedSubmodule.mapEquiv f) t
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.add.inj : ∀ {a b a_1 b_1 : Lean.Grind.CommRing.Expr}, a.add b = a_1.add b_1 → a = a_1 ∧ b = b_1
-- Mathlib.Computability.Primrec.List
List.lookup.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (x : α), List.lookup x [] = none
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.delete : {α : outParam (Type u)} →
  {β : outParam (Type v)} →
    {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} →
      {σ : Type w} →
        {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} →
          [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] → σ → Array ℕ → σ
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_26 : HSub Std.Time.Hour.Offset Std.Time.Second.Offset Std.Time.Second.Offset
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.ScopedEntries.mk.inj : ∀ {β : Type} {map map_1 : Lean.SMap Lean.Name (Lean.PArray β)}, { map := map } = { map := map_1 } → map = map_1
-- Mathlib.Data.Set.Operations
Set.prod_image_left : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → γ) (s : Set α) (t : Set β),
  (f '' s) ×ˢ t = (fun x => (f x.1, x.2)) '' s ×ˢ t
-- Mathlib.Order.Filter.CountablyGenerated
/-- `IsCountableBasis p s` means the image of `s` bounded by `p` is a countable filter basis.  -/
Filter.IsCountableBasis : {α : Type u_1} → {ι : Type u_4} → (ι → Prop) → (ι → Set α) → Prop
-- Mathlib.Algebra.Group.Pi.Lemmas
MulHom.piMap.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [inst : (i : ι) → Mul (M i)] [inst_1 : (i : ι) → Mul (N i)]
  (g : (i : ι) → M i →ₙ* N i), MulHom.piMap g = MulHom.pi fun i => (g i).comp (Pi.evalMulHom M i)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.eqToHom_proj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {I : Type u_1} {x x' : CategoryTheory.GradedObject I C}
  (h : x = x') (i : I), CategoryTheory.eqToHom h i = CategoryTheory.eqToHom ⋯
-- Mathlib.Data.PEquiv
/-- `invFun` is the partial inverse of `toFun`  -/
PEquiv.inv : ∀ {α : Type u} {β : Type v} (self : α ≃. β) (a : α) (b : β), self.invFun b = some a ↔ self.toFun a = some b
-- Mathlib.Order.Nucleus
Nucleus.coe_bot : ∀ {X : Type u_1} [inst : SemilatticeInf X], ⇑⊥ = id
-- Mathlib.Analysis.Seminorm
Seminorm.comp_zero : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedRing 𝕜₂]
  {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup E₂]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ E₂] (p : Seminorm 𝕜₂ E₂), p.comp 0 = 0
-- Lean.Meta.Tactic.Grind.Arith.Linear.Model
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Model.0.Lean.Meta.Grind.Arith.Linear.evalTermAt?.go : Lean.Meta.Grind.Arith.Linear.Struct → Std.HashMap Lean.Expr ℚ → Lean.Expr → OptionT Lean.MetaM ℚ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, k ∈ Std.ExtTreeMap.map f t ↔ k ∈ t
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
IsIntegral.add : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {x y : A},
  IsIntegral R x → IsIntegral R y → IsIntegral R (x + y)
-- Init.Data.String.Legacy
_private.Init.Data.String.Legacy.0.String.splitAux.eq_def : ∀ (s : String) (p : Char → Bool) (b i : String.Pos.Raw) (r : List String),
  s.splitAux p b i r =
    if h : String.Pos.Raw.atEnd s i = true then
      have r := String.Pos.Raw.extract s b i :: r;
      r.reverse
    else
      have this := ⋯;
      if p (String.Pos.Raw.get s i) = true then
        have i' := String.Pos.Raw.next s i;
        s.splitAux p i' i' (String.Pos.Raw.extract s b i :: r)
      else s.splitAux p b (String.Pos.Raw.next s i) r
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
/-- An object `X` in an abelian category has Injective dimension `< n` if
all `Ext X Y i` vanish when `n ≤ i`. See also `HasInjectiveDimensionLE`.
(Do not use the `subsingleton'` field directly. Use the constructor
`HasInjectiveDimensionLT.mk`, and the lemmas `hasInjectiveDimensionLT_iff` and
`Ext.eq_zero_of_hasInjectiveDimensionLT`.)  -/
CategoryTheory.HasInjectiveDimensionLT : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → C → ℕ → Prop
-- Mathlib.CategoryTheory.Subobject.Basic
/-- Two morphisms into a subobject are equal exactly if
the morphisms into the ambient object are equal  -/
CategoryTheory.Subobject.eq_of_comp_arrow_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {P : CategoryTheory.Subobject Y}
  {f g : X ⟶ CategoryTheory.Subobject.underlying.obj P},
  CategoryTheory.CategoryStruct.comp f P.arrow = CategoryTheory.CategoryStruct.comp g P.arrow → f = g
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- `cfcHom` bundled as a continuous linear map.  -/
cfcL : {R : Type u_1} →
  {A : Type u_2} →
    {p : A → Prop} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : MetricSpace R] →
            [inst_3 : IsTopologicalSemiring R] →
              [inst_4 : ContinuousStar R] →
                [inst_5 : TopologicalSpace A] →
                  [inst_6 : Ring A] →
                    [inst_7 : StarRing A] →
                      [inst_8 : Algebra R A] →
                        [instCFC : ContinuousFunctionalCalculus R A p] → {a : A} → p a → C(↑(spectrum R a), R) →L[R] A
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.unop_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : Cᵒᵖ ≌ Dᵒᵖ), e.unop.unitIso = (CategoryTheory.NatIso.unop e.unitIso).symm
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.le_one_iff : ∀ {a : Ordinal.{u_1}}, a ≤ 1 ↔ a = 0 ∨ a = 1
-- Std.Http.Protocol.H1
/-- Converts a validated `BodyMode` into the concrete reader state to enter next.

For EOF-delimited bodies this also disables keep-alive since the message
boundary depends on socket close.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.readerStateForMode : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir →
    Std.Http.Protocol.H1.Machine.BodyMode✝ → Std.Http.Protocol.H1.Machine dir × Std.Http.Protocol.H1.Reader.State dir
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.Std.Iter.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.inv_whiskerLeft : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ') [inst_9 : CategoryTheory.IsIso θ],
  CategoryTheory.inv (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ) =
    CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (CategoryTheory.inv θ)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.det_kronecker : ∀ {R : Type u_1} {m : Type u_10} {n : Type u_11} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing R] (A : Matrix m m R) (B : Matrix n n R),
  (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B).det = A.det ^ Fintype.card n * B.det ^ Fintype.card m
-- Lean.Parser.Extra
Lean.Parser.rawIdent : Lean.Parser.Parser
-- Mathlib.Computability.NFA
NFA.evalFrom_eq_biUnion_singleton : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) (x : List α), M.evalFrom S x = ⋃ s ∈ S, M.evalFrom {s} x
-- Init.Data.Int.Order
Int.lt_min : ∀ {a b c : ℤ}, a < min b c ↔ a < b ∧ a < c
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_filter_key : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {f : α → Bool}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey! k (List.filter (fun p => f p.fst) l) =
      (Option.filter f (Std.Internal.List.getKey? k l)).get!
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConst_k : ℤ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.inl_π : ∀ {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.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (CategoryTheory.kernelCokernelCompSequence.π f g) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp f g))
-- Mathlib.Topology.Order.WithTop
WithTop.tendsto_untop : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] (a : ↑{a | a ≠ ⊤}),
  Filter.Tendsto (fun x => (↑x).untop ⋯) (nhds a) (nhds ((↑a).untop ⋯))
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.inv_def : ∀ {K : Type u_1} [inst : Field K] {a b : K} (z : QuadraticAlgebra K a b), z⁻¹ = (QuadraticAlgebra.norm z)⁻¹ • star z
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instMulPosStrictMono : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [inst_2 : Preorder α] [MulPosStrictMono α],
  MulPosStrictMono (WithBot α)
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.preorder : {α : Type u_1} → [Preorder α] → Preorder (Additive α)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The direction of the sup of two nonempty affine subspaces is the sup of the two directions and
of any one difference between points in the two subspaces.  -/
AffineSubspace.direction_sup : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : AffineSubspace k P} {p₁ p₂ : P},
  p₁ ∈ s₁ → p₂ ∈ s₂ → (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
-- Mathlib.Topology.Order.OrderClosed
/-- The limit of a collection of functions that is frequently antitone is antitone.  -/
antitone_of_frequently_antitone_of_tendsto : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α] {ι : Type u_1}
  {l : Filter ι} [inst_2 : Preorder β] {F : ι → β → α} {f : β → α},
  (∃ᶠ (i : ι) in l, Antitone (F i)) → (∀ (x : β), Filter.Tendsto (fun i => F i x) l (nhds (f x))) → Antitone f
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.addNamedQuotInfo : Lean.Syntax → Lean.SyntaxNodeKind → Lean.Elab.TermElabM Lean.SyntaxNodeKind
-- Mathlib.Topology.Category.FinTopCat
FinTopCat.fintype : (self : FinTopCat) → Fintype ↑self.toTop
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- Variant of `meromorphicTrailingCoeffAt_of_order_eq_finite`: Definition of the trailing coefficient
in case where `f` is meromorphic of finite order and a presentation is given.
 -/
AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {x : 𝕜} {n : ℤ},
  AnalyticAt 𝕜 g x →
    g x ≠ 0 → (f =ᶠ[nhdsWithin x {x}ᶜ] fun z => (z - x) ^ n • g z) → meromorphicTrailingCoeffAt f x = g x
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- The delaborated discriminants, without `h :` annotations.  -/
Lean.PrettyPrinter.Delaborator.AppMatchState.discrs : Lean.PrettyPrinter.Delaborator.AppMatchState → Array Lean.Term
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- The gluing of two pre-path objects.  -/
HomotopicalAlgebra.PrepathObject.trans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} →
      (P P' : HomotopicalAlgebra.PrepathObject A) →
        [CategoryTheory.Limits.HasPullback P.p₁ P'.p₀] → HomotopicalAlgebra.PrepathObject A
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.out' : ∀ {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it →
    it = { s := String.ofList (l.reverse ++ r), i := { byteIdx := String.utf8Len l.reverse } }
-- Mathlib.Topology.MetricSpace.CauSeqFilter
CauSeq.cauchySeq : ∀ {β : Type v} [inst : NormedField β] (f : CauSeq β norm), CauchySeq ↑f
-- Mathlib.MeasureTheory.Integral.Pi
/-- On a finite product space, a product of integrable functions depending on each coordinate is
integrable.  -/
MeasureTheory.Integrable.fintype_prod : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : Fintype ι] [inst_1 : NormedCommRing 𝕜] {E : Type u_3} {f : ι → E → 𝕜}
  {mE : MeasurableSpace E} {μ : ι → MeasureTheory.Measure E} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)],
  (∀ (i : ι), MeasureTheory.Integrable (f i) (μ i)) →
    MeasureTheory.Integrable (fun x => ∏ i, f i (x i)) (MeasureTheory.Measure.pi μ)
-- Mathlib.Order.Basic
/-- **Alias** of `lt_asymm`. -/
LT.lt.not_gt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬b < a
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.foldlM.loop.match_1.splitter : (motive : ℕ → Sort u_1) → (i : ℕ) → (Unit → motive 0) → ((i' : ℕ) → motive i'.succ) → motive i
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.cooper.injEq : ∀ (c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) (c₃ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr)
  (c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) (c₃_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.cooper c₁ c₂ c₃ =
      Lean.Meta.Grind.Arith.Cutsat.UnsatProof.cooper c₁_1 c₂_1 c₃_1) =
    (c₁ = c₁_1 ∧ c₂ = c₂_1 ∧ c₃ = c₃_1)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instReprCustomEliminator : Repr Lean.Meta.CustomEliminator
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instNatPowAssoc : NatPowAssoc Complex.UnitClosedDisc
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt8.reduceGT : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.BigOperators.Group.List.Defs
List.prod_replicate : ∀ {M : Type u_2} [inst : Monoid M] (n : ℕ) (a : M), (List.replicate n a).prod = a ^ n
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.instInjectiveOfHasInjectiveDimensionLTOfNatNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C)
  [CategoryTheory.HasInjectiveDimensionLT X 1], CategoryTheory.Injective X
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.foldl_eq_foldl_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  {f : δ → α → β → δ} {init : δ},
  Std.DTreeMap.foldl f init t = Array.foldl (fun a b => f a b.1 b.2) init (Std.DTreeMap.Const.toArray t)
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- The `n`th coefficient of a multivariate formal power series.  -/
MvPowerSeries.coeff : {σ : Type u_1} → {R : Type u_2} → [inst : Semiring R] → (σ →₀ ℕ) → MvPowerSeries σ R →ₗ[R] R
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ico_of_Ioo : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α} [MeasureTheory.NullSingletonClass μ],
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ico A B)) l fun i => Set.Ioo (a i) (b i)
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ioc_pred_left_eq_Icc_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a : α},
  ¬IsMin a → ∀ (b : α), Set.Ioc (Order.pred a) b = Set.Icc a b
-- Lean.Elab.Do.Basic
Lean.Elab.Do.MutVar.mk.inj : ∀ {ident : Lean.Ident} {baseId : Lean.FVarId} {ident_1 : Lean.Ident} {baseId_1 : Lean.FVarId},
  { ident := ident, baseId := baseId } = { ident := ident_1, baseId := baseId_1 } → ident = ident_1 ∧ baseId = baseId_1
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The natural isomorphism arising from `mapForget_eq`.  -/
CategoryTheory.Over.mapId : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    (Y : T) →
      CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id Y) ≅ CategoryTheory.Functor.id (CategoryTheory.Over Y)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- The inner product of two linear combinations of a set of orthonormal vectors, expressed as
a sum over the second `Finsupp`.  -/
Orthonormal.inner_finsupp_eq_sum_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E},
  Orthonormal 𝕜 v →
    ∀ (l₁ l₂ : ι →₀ 𝕜),
      inner 𝕜 ((Finsupp.linearCombination 𝕜 v) l₁) ((Finsupp.linearCombination 𝕜 v) l₂) =
        l₂.sum fun i y => (starRingEnd 𝕜) (l₁ i) * y
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity follows from pairwise scaled extended distance. Backward direction of
`similar_iff_exists_pairwise_edist_eq`.  -/
Similar.of_exists_pairwise_edist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂],
  (∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ => edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)) → Similar v₁ v₂
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The induced map from the quotient by the kernel to the range.  -/
QuotientGroup.rangeKerLift : {G : Type u} → [inst : Group G] → {H : Type v} → [inst_1 : Group H] → (φ : G →* H) → G ⧸ φ.ker →* ↥φ.range