mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Cases
Lean.Meta.Cases.Context.mk.inj : ∀ {inductiveVal : Lean.InductiveVal} {nminors : ℕ} {majorDecl : Lean.LocalDecl} {majorTypeFn : Lean.Expr}
  {majorTypeArgs majorTypeIndices : Array Lean.Expr} {inductiveVal_1 : Lean.InductiveVal} {nminors_1 : ℕ}
  {majorDecl_1 : Lean.LocalDecl} {majorTypeFn_1 : Lean.Expr} {majorTypeArgs_1 majorTypeIndices_1 : Array Lean.Expr},
  { inductiveVal := inductiveVal, nminors := nminors, majorDecl := majorDecl, majorTypeFn := majorTypeFn,
        majorTypeArgs := majorTypeArgs, majorTypeIndices := majorTypeIndices } =
      { inductiveVal := inductiveVal_1, nminors := nminors_1, majorDecl := majorDecl_1, majorTypeFn := majorTypeFn_1,
        majorTypeArgs := majorTypeArgs_1, majorTypeIndices := majorTypeIndices_1 } →
    inductiveVal = inductiveVal_1 ∧
      nminors = nminors_1 ∧
        majorDecl = majorDecl_1 ∧
          majorTypeFn = majorTypeFn_1 ∧ majorTypeArgs = majorTypeArgs_1 ∧ majorTypeIndices = majorTypeIndices_1
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Reinterpret an element of a type of semilinear maps as a semilinear map.  -/
SemilinearMapClass.instCoeToSemilinearMap : {R : Type u_1} →
  {S : Type u_5} →
    {M : Type u_8} →
      {M₃ : Type u_11} →
        {F : Type u_14} →
          [inst : Semiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module S M₃] →
                      {σ : R →+* S} →
                        [inst_6 : FunLike F M M₃] → [SemilinearMapClass F σ M M₃] → CoeHead F (M →ₛₗ[σ] M₃)
-- Mathlib.RingTheory.Int.Basic
Int.isCoprime_two_right : ∀ {m : ℤ}, IsCoprime m 2 ↔ Odd m
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.mem_zeroLocus_iff : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  {I : Ideal (MvPolynomial σ k)} {x : σ → K}, x ∈ MvPolynomial.zeroLocus K I ↔ ∀ p ∈ I, (MvPolynomial.aeval x) p = 0
-- Mathlib.Topology.Algebra.Monoid.Defs
Continuous.add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M}, Continuous f → Continuous g → Continuous (f + g)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications `M` and `M₂` will be topological modules over the topological
ring `R`.  -/
«term_→SL[_]_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.span_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.span f g).obj CategoryTheory.Limits.WalkingSpan.zero = X
-- Aesop.Script.GoalWithMVars
Aesop.GoalWithMVars.mk.inj : ∀ {goal : Lean.MVarId} {mvars : Std.HashSet Lean.MVarId} {goal_1 : Lean.MVarId} {mvars_1 : Std.HashSet Lean.MVarId},
  { goal := goal, mvars := mvars } = { goal := goal_1, mvars := mvars_1 } → goal = goal_1 ∧ mvars = mvars_1
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.ite_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (P : Prop) [inst : Decidable P] (A B : Matrix m n α) (i : m) (j : n),
  (if P then A else B) i j = if P then A i j else B i j
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toBialgHom_injective : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B],
  Function.Injective BialgEquiv.toBialgHom
-- Mathlib.Data.Vector3
Vector3.recOn_nil : ∀ {α : Type u_1} {C : {n : ℕ} → Vector3 α n → Sort u_2} {H0 : C []}
  {Hs : {n : ℕ} → (a : α) → (w : Vector3 α n) → C w → C (Vector3.cons a w)}, [].recOn H0 Hs = H0
-- Mathlib.Data.Countable.Defs
Countable.exists_injective_nat : ∀ (α : Sort u) [Countable α], ∃ f, Function.Injective f
-- Mathlib.Order.Grade
grade_injective : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : LinearOrder α] [inst_2 : GradeOrder 𝕆 α],
  Function.Injective (grade 𝕆)
-- Mathlib.Topology.Metrizable.Basic
/-- Given an inducing map of a topological space into a pseudometrizable space, the source space
is also pseudometrizable.  -/
Topology.IsInducing.pseudoMetrizableSpace : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [TopologicalSpace.PseudoMetrizableSpace Y] {f : X → Y},
  Topology.IsInducing f → TopologicalSpace.PseudoMetrizableSpace X
-- Mathlib.RingTheory.Smooth.Kaehler
toAlgHom_comp_sectionOfRetractionKerToTensor : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S)))
  (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S]
  (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hf : Function.Surjective ⇑(algebraMap P S)),
  (IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensor l hl hf' hf) = AlgHom.id R S
-- Mathlib.Tactic.Sat.FromLRAT
/-- `v.satisfies_fmla f` asserts that formula `f` is satisfied by the valuation.
A formula is satisfied if all clauses in it are satisfied.  -/
Sat.Valuation.satisfies_fmla : Sat.Valuation → Sat.Fmla → Prop
-- Lean.Server.Requests
Lean.Server.RequestT : (Type → Type u_1) → Type → Type u_1
-- Mathlib.Order.SuccPred.Relation
/-- `(n, m)` is in the transitive closure of a reflexive relation `~` if `i ~ succ i` and
`succ i ~ i` for all `i` between `n` and `m`.  -/
transGen_of_succ_of_refl : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] (r : α → α → Prop) {n m : α}
  [Std.Refl r],
  (∀ i ∈ Set.Ico n m, r i (Order.succ i)) → (∀ i ∈ Set.Ico m n, r (Order.succ i) i) → Relation.TransGen r n m
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_wf : WellFounded fun x1 x2 => x1 ∈ x2
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.CancelParams.mk.sizeOf_spec : ∀ (id : Lean.JsonRpc.RequestID), sizeOf { id := id } = 1 + sizeOf id
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_range_inclusion_eq_top : ∀ {R : Type u_1} {M : Type u_4} {S : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] (p : Submodule R M)
  (q : Submodule S M) (h₁ : p ≤ Submodule.restrictScalars R q),
  q ≤ Submodule.span S ↑p → Submodule.span S (Set.range ⇑(Submodule.inclusion h₁)) = ⊤
-- Init.Data.List.Find
List.getLast?_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α},
  (List.filterMap f l).getLast? = List.findSome? f l.reverse
-- Init.Data.Array.Basic
Array.mem_def : ∀ {α : Type u} {a : α} {as : Array α}, a ∈ as ↔ a ∈ as.toList
-- Mathlib.Data.WSeq.Relation
_private.Mathlib.Data.WSeq.Relation.0.Stream'.WSeq.LiftRelO.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option (α × Stream'.WSeq α) → Option (β × Stream'.WSeq β) → Sort u_3) (a : α)
  (s : Stream'.WSeq α) (b : β) (t : Stream'.WSeq β) (h_1 : Unit → motive none none)
  (h_2 : (a : α) → (s : Stream'.WSeq α) → (b : β) → (t : Stream'.WSeq β) → motive (some (a, s)) (some (b, t)))
  (h_3 : (x : Option (α × Stream'.WSeq α)) → (x_1 : Option (β × Stream'.WSeq β)) → motive x x_1),
  (match some (a, s), some (b, t) with
    | none, none => h_1 ()
    | some (a, s), some (b, t) => h_2 a s b t
    | x, x_1 => h_3 x x_1) =
    h_2 a s b t
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_app_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X : C} {F : CategoryTheory.Sheaf J (Type (max v v'))} (x : F.obj.obj (Opposite.op X))
  (Y : Cᵒᵖ) (f : Opposite.unop Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaEquiv.symm x).hom.app Y)) { down := f } =
    (CategoryTheory.ConcreteCategory.hom (F.obj.map f.op)) x
-- Init.Data.List.Lemmas
List.flatten.eq_2 : ∀ {α : Type u_1} (l : List α) (L : List (List α)), (l :: L).flatten = l.append L.flatten
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_add_intCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (z : ℤ),
  ⌊a + ↑z⌋ = ⌊a⌋ + z
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.Iterators.Types.Zip.instIterator.match_5.splitter : {m : Type u_1 → Type u_2} →
  {α₁ β₁ : Type u_1} →
    [inst : Std.Iterator α₁ m β₁] →
      (motive : Option { out // ∃ it, it.IsPlausibleOutput out } → Sort u_3) →
        (x : Option { out // ∃ it, it.IsPlausibleOutput out }) →
          (x = none → motive none) →
            ((out₁ : { out // ∃ it, it.IsPlausibleOutput out }) → x = some out₁ → motive (some out₁)) → motive x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isEmpty_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α}, (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Topology.Order.Basic
nhds_order_unbounded : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {a : α},
  (∃ u, a < u) → (∃ l, l < a) → nhds a = ⨅ l, ⨅ (_ : l < a), ⨅ u, ⨅ (_ : a < u), Filter.principal (Set.Ioo l u)
-- Init.Data.SInt.Lemmas
Int64.not_le : ∀ {n m : Int64}, ¬n ≤ m ↔ m < n
-- Mathlib.Logic.Function.Basic
Function.update_of_ne : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] {a a' : α},
  a ≠ a' → ∀ (v : β a') (f : (a : α) → β a), Function.update f a' v a = f a
-- Mathlib.CategoryTheory.HomCongr
CategoryTheory.Iso.isoCongr_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ≅ X₂) (g : Y₁ ≅ Y₂) (h : X₂ ≅ Y₂),
  (f.isoCongr g).symm h = f ≪≫ h ≪≫ g.symm
-- Mathlib.Order.Hom.Basic
/-- Order isomorphism between `α → β` and `β`, where `α` has a unique element.  -/
OrderIso.funUnique : (α : Type u_6) → (β : Type u_7) → [Unique α] → [inst : Preorder β] → (α → β) ≃o β
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.FunctorToTypes.shrinkMap_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w')} (τ : F ⟶ G)
  [inst_1 : CategoryTheory.FunctorToTypes.Small.{w, w', v, u} F]
  [inst_2 : CategoryTheory.FunctorToTypes.Small.{w, w', v, u} G] (X : C),
  (CategoryTheory.FunctorToTypes.shrinkMap τ).app X =
    TypeCat.ofHom
      (⇑(equivShrink (G.obj X)) ∘ ⇑(CategoryTheory.ConcreteCategory.hom (τ.app X)) ∘ ⇑(equivShrink (F.obj X)).symm)
-- Mathlib.GroupTheory.ResiduallyFinite
Group.ResiduallyFinite.iInf_eq_bot : ∀ {G : Type u_1} {inst : Group G} [self : Group.ResiduallyFinite G], ⨅ H, H.toSubgroup = ⊥
-- Init.Data.Rat.Lemmas
Rat.nonneg_total : ∀ (a : ℚ), 0 ≤ a ∨ 0 ≤ -a
-- Mathlib.SetTheory.Ordinal.Enum
/-- Enumerator function for an unbounded set of ordinals.

The definition is an implementation detail; this function is entirely characterized by being an
order isomorphism. See `enumOrdOrderIso`.  -/
Ordinal.enumOrd : Set Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
-- Mathlib.Topology.UniformSpace.UniformEmbedding
uniformly_extend_unique : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] {e : β → α} (h_e : IsUniformInducing e) (h_dense : DenseRange e) {f : β → γ} [T0Space γ]
  {g : α → γ}, (∀ (b : β), g (e b) = f b) → Continuous g → ⋯.extend f = g
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev_lt_iff_le : ∀ {s : String} {p q : s.Pos} {h : p ≠ s.startPos}, p.prev h < q ↔ p ≤ q
-- Mathlib.CategoryTheory.Core
Equiv.toIso.eq_1 : ∀ {X Y : Type u} (e : X ≃ Y),
  e.toIso =
    { hom := TypeCat.ofHom fun x => e x, inv := TypeCat.ofHom fun x => e.symm x, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanFinset.congr_simp : ∀ (R₁ : Type u_3) [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] {ι : Type u_5} (s s_1 : Finset ι),
  s = s_1 → ∀ (f f_1 : ι → K), f = f_1 → FractionalIdeal.spanFinset R₁ s f = FractionalIdeal.spanFinset R₁ s_1 f_1
-- Mathlib.Algebra.Category.ModuleCat.Abelian
/-- In the category of modules, every epimorphism is normal.  -/
ModuleCat.normalEpi : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → (f : M ⟶ N) → CategoryTheory.Epi f → CategoryTheory.NormalEpi f
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : SMul K β] (c : K)
  (f : MeasureTheory.SimpleFunc α β), ⇑(c • f) = c • ⇑f
-- Init.Data.SInt.Lemmas
Int8.toInt_ofInt : ∀ {n : ℤ}, (Int8.ofInt n).toInt = n.bmod Int8.size
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono φ h).φH = CategoryTheory.CategoryStruct.id h.H
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncKind.full : Lean.Lsp.TextDocumentSyncKind
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.inv_one_sub_inv : ∀ {a : NNReal}, 0 < a → a < 1 → a⁻¹.HolderConjugate (1 - a)⁻¹
-- Lean.LocalContext
Lean.instInhabitedLocalDeclKind.default : Lean.LocalDeclKind
-- Mathlib.Algebra.Order.GroupWithZero.Finset
Finset.sup_div₀ : ∀ {ι : Type u_1} {G₀ : Type u_3} [inst : LinearOrderedCommGroupWithZero G₀] {a : G₀},
  0 ≤ a → ∀ (s : Finset ι) (f : ι → G₀), s.sup f / a = s.sup fun i => f i / a
-- Std.Internal.Parsec.ByteArray
/-- Parses while a predicate is satisfied, up to a given limit.
Fails with `.eof` if input ends before stopping or reaching the limit.
 -/
Std.Internal.Parsec.ByteArray.takeWhileUpTo : (UInt8 → Bool) → ℕ → Std.Internal.Parsec.ByteArray.Parser ByteSlice
-- Init.Data.Zero
/-- The fundamental scalar multiplication in an additive monoid.
`nsmulRec n a = a+a+...+a` n times.
This function should not be used directly;
it is often used to implement an instance for scalar multiplication.
 -/
nsmulRec : {M : Type u_1} → [Zero M] → [Add M] → ℕ → M → M
-- Std.Time.Date.PlainDate
/-- Creates a new `PlainDate` by adjusting the year to the given `year` value. The month and day are rolled
over to the next valid month and day if necessary.
 -/
Std.Time.PlainDate.withYearRollOver : Std.Time.PlainDate → Std.Time.Year.Offset → Std.Time.PlainDate
-- Lean.Level
Lean.Level.PP.M : Type → Type
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.toList_nil : ∀ {α : Type u}, Stream'.WSeq.nil.toList = Computation.pure []
-- Mathlib.Algebra.Lie.Nilpotent
/-- Note that this result is not quite a special case of
`LieModule.isNilpotent_range_toEnd_iff` which concerns nilpotency of the
`(ad R L).range`-module `L`, whereas this result concerns nilpotency of the `(ad R L).range`-module
`(ad R L).range`.  -/
LieAlgebra.isNilpotent_range_ad_iff : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieRing.IsNilpotent ↥(LieAlgebra.ad R L).range ↔ LieRing.IsNilpotent L
-- Mathlib.Data.Seq.Defs
Stream'.Seq.ext : ∀ {α : Type u} {s t : Stream'.Seq α}, (∀ (n : ℕ), s.get? n = t.get? n) → s = t
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
/-- When `s : X.S` is such that `s.dim = d`, this is a term
that is equal to `s`, but whose dimension if definitionally equal to `d`.  -/
SSet.S.cast : {X : SSet} → (s : X.S) → {d : ℕ} → s.dim = d → X.S
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(f₁ * f₂, g) = Res(f₁, g) * Res(f₂, g)`.  -/
Polynomial.resultant_mul_left : ∀ {R : Type u_1} [inst : CommRing R] (f₁ f₂ g : Polynomial R) (n : ℕ),
  g.natDegree ≤ n →
    (f₁ * f₂).resultant g (f₁.natDegree + f₂.natDegree) n =
      f₁.resultant g f₁.natDegree n * f₂.resultant g f₂.natDegree n
-- Init.Data.String.Basic
String.Pos.toSlice_comp_ofToSlice : ∀ {s : String}, String.Pos.toSlice ∘ String.Pos.ofToSlice = id
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.instIsStableUnderBaseChangeInnerFibrations : SSet.innerFibrations.IsStableUnderBaseChange
-- Mathlib.Analysis.Convex.Gauge
tendsto_gauge_nhds_zero_nhdsGE : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
  [ContinuousSMul ℝ E], s ∈ nhds 0 → Filter.Tendsto (gauge s) (nhds 0) (nhdsWithin 0 (Set.Ici 0))
-- Mathlib.Order.Filter.Pointwise
Filter.mem_one : ∀ {α : Type u_2} [inst : One α] {s : Set α}, s ∈ 1 ↔ 1 ∈ s
-- Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
/-- If a sequence of continuous functions `f i x` on an open subset `K` have norms eventually
bounded by a summable function, then `∏' i, (1 + f i x)` is locally uniformly convergent on `K`.  -/
Summable.hasProdLocallyUniformlyOn_one_add : ∀ {α : Type u_1} {ι : Type u_2} {K : Set α} {u : ι → ℝ} {R : Type u_3} [inst : NormedCommRing R] [NormOneClass R]
  [CompleteSpace R] [inst_3 : TopologicalSpace α] {f : ι → α → R} [LocallyCompactSpace α],
  IsOpen K →
    Summable u →
      (∀ᶠ (i : ι) in Filter.cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) →
        (∀ (i : ι), ContinuousOn (f i) K) →
          HasProdLocallyUniformlyOn (fun i x => 1 + f i x) (fun x => ∏' (i : ι), (1 + f i x)) K
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
instFiniteRingKrullDimOfIsLocalRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [IsLocalRing R], FiniteRingKrullDim R
-- Mathlib.Analysis.Convex.Function
ConcaveOn.subset : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {t : Set E}, ConcaveOn 𝕜 t f → s ⊆ t → Convex 𝕜 s → ConcaveOn 𝕜 s f
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.pure_exists : ∀ {σs : List (Type u)} {α : Sort u_1} {φ : α → Prop}, (∃ x, ⌜φ x⌝) ⊣⊢ₛ ⌜∃ x, φ x⌝
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- A morphism `P ⟶ Q` in the category `Karoubi C` is a morphism in the underlying category
`C` which satisfies a relation, which in the preadditive case, expresses that it induces a
map between the corresponding "formal direct factors" and that it vanishes on the complement
formal direct factor.  -/
CategoryTheory.Idempotents.Karoubi.Hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.Idempotents.Karoubi C → CategoryTheory.Idempotents.Karoubi C → Type v_1
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.sigmaFunctor_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C] (X : C)
  (α : Type w), (CategoryTheory.Limits.sigmaFunctor.obj X).obj α = ∐ fun t => X
-- Mathlib.Tactic.Order.Preprocessing
/-- Find the "best" instance of an order on a given type. A linear order is preferred over a partial
order, and a partial order is preferred over a preorder.  -/
Mathlib.Tactic.Order.findBestOrderInstance : Lean.Expr → Lean.MetaM (Option Mathlib.Tactic.Order.OrderType)
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.presheafFiber.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A],
  Φ.presheafFiber =
    ((CategoryTheory.Functor.whiskeringLeft Φ.fiber.Elementsᵒᵖ Cᵒᵖ A).obj
          (CategoryTheory.CategoryOfElements.π Φ.fiber).op).comp
      CategoryTheory.Limits.colim
-- Mathlib.Analysis.Calculus.AbsolutelyMonotone
/-- The sum of two absolutely monotone functions is absolutely monotone.  -/
AbsolutelyMonotoneOn.add : ∀ {f g : ℝ → ℝ} {s : Set ℝ}, AbsolutelyMonotoneOn f s → AbsolutelyMonotoneOn g s → AbsolutelyMonotoneOn (f + g) s
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.isoOfEq_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} (X Y : CategoryTheory.Subobject B) (h : X = Y),
  (X.isoOfEq Y h).inv = Y.ofLE X ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.Truncated.hom_ext : ∀ {n : ℕ} {X Y : SSet.Truncated n} {f g : X ⟶ Y},
  (∀ (n_1 : (SimplexCategory.Truncated n)ᵒᵖ), f.app n_1 = g.app n_1) → f = g
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instAdd.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S],
  AddOreLocalization.instAdd = { add := AddOreLocalization.vadd }
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
/-- If two regular measures give the same integral for every function in `C_c(X, ℝ≥0)`, then they
are equal.  -/
MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported_nnreal : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] [inst_3 : MeasurableSpace X]
  [BorelSpace X] {μ ν : MeasureTheory.Measure X} [μ.Regular] [ν.Regular],
  (∀ (f : CompactlySupportedContinuousMap X NNReal), ∫ (x : X), ↑(f x) ∂μ = ∫ (x : X), ↑(f x) ∂ν) → μ = ν
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.hasExprMVar : Lean.Meta.Match.Pattern → Bool
-- Init.Data.List.Erase
List.le_length_eraseP : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, l.length - 1 ≤ (List.eraseP p l).length
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.IsMonoidalClosed.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : CategoryTheory.MonoidalClosed C],
  autoParam (∀ (X Y : C), P X → P Y → P (X ⟹ Y)) CategoryTheory.ObjectProperty.IsMonoidalClosed.prop_ihom._autoParam →
    P.IsMonoidalClosed
-- Mathlib.NumberTheory.NumberField.AdeleRing
NumberField.instCommRingAdeleRing : (R : Type u_1) →
  (K : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : IsDedekindDomain R] →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → CommRing (NumberField.AdeleRing R K)
-- Std.Data.ExtTreeSet.Basic
/-- Computes the intersection of the given tree sets.

This function always iterates through the smaller set.
 -/
Std.ExtTreeSet.inter : {α : Type u} →
  {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → Std.ExtTreeSet α cmp → Std.ExtTreeSet α cmp
-- Mathlib.Logic.Equiv.Set
/-- If `f : α → β` has a left-inverse when `α` is nonempty, then `α` is computably equivalent to the
range of `f`.

While awkward, the `Nonempty α` hypothesis on `f_inv` and `hf` allows this to be used when `α` is
empty too. This hypothesis is absent on analogous definitions on stronger `Equiv`s like
`LinearEquiv.ofLeftInverse` and `RingEquiv.ofLeftInverse` as their typeclass assumptions
are already sufficient to ensure non-emptiness.  -/
Equiv.ofLeftInverse : {α : Sort u_3} →
  {β : Type u_4} →
    (f : α → β) →
      (f_inv : Nonempty α → β → α) → (∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f) → α ≃ ↑(Set.range f)
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- Given an orthogonal basis with respect to a bilinear form, the bilinear form is nondegenerate
iff the basis has no elements which are self-orthogonal.  -/
LinearMap.BilinForm.iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : Type w}
  [IsDomain R] (B : LinearMap.BilinForm R M) (v : Module.Basis n R M),
  B.iIsOrtho ⇑v → (B.Nondegenerate ↔ ∀ (i : n), (B (v i)) (v i) ≠ 0)