mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Limits
/-- If `E` is a colimit cocone of presheaves, over a diagram factoring through sheaves,
then `sheafifyCocone E` is a colimit cocone.  -/
CategoryTheory.Sheaf.isColimitSheafifyCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {K : Type z} →
            [inst_2 : CategoryTheory.Category.{z', z} K] →
              [inst_3 : CategoryTheory.HasWeakSheafify J D] →
                {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} →
                  (E : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf J D))) →
                    CategoryTheory.Limits.IsColimit E →
                      CategoryTheory.Limits.IsColimit (CategoryTheory.Sheaf.sheafifyCocone E)
-- Mathlib.Algebra.Ring.Invertible
AddUnits.neg_mul_eq_mul_neg : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] {x y : AddUnits R}, ↑(-x) * ↑y = ↑x * ↑(-y)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I] (b : J.R)
  {Z : C} (h : I.right b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (J.fst b))
      (CategoryTheory.CategoryStruct.comp (I.fst b) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (J.snd b))
      (CategoryTheory.CategoryStruct.comp (I.snd b) h)
-- Batteries.Data.ByteArray
ByteArray.emptyWithCapacity.eq_1 : ∀ (c : ℕ), ByteArray.emptyWithCapacity c = { data := #[] }
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- The functor to the base.  -/
CategoryTheory.BasedCategory.p : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    (self : CategoryTheory.BasedCategory 𝒮) → CategoryTheory.Functor self.obj 𝒮
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α}
  {v : β k}, (m.insertIfNew k v).get? a = if h : (k == a) = true ∧ k ∉ m then some (cast ⋯ v) else m.get? a
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.one_vlt_inv : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : ValuativeRel K] {x : K}, x ≠ 0 → (1 <ᵥ x⁻¹ ↔ x <ᵥ 1)
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.SpecialLinear.sl_non_abelian : ∀ (n : Type u_1) (R : Type u₂) [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] [Nontrivial R],
  1 < Fintype.card n → ¬IsLieAbelian ↥(LieAlgebra.SpecialLinear.sl n R)
-- Mathlib.RingTheory.AdicCompletion.Basic
IsHausdorff.eq_iff_smodEq : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsHausdorff I M] {x y : M}, x = y ↔ ∀ (n : ℕ), x ≡ y [SMOD I ^ n • ⊤]
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring of a `NonAssocCommRing` is a `NonAssocCommRing`.  -/
SubringClass.toNonAssocCommRing : {S : Type v} →
  (s : S) →
    {R : Type u_1} → [inst : NonAssocCommRing R] → [inst_1 : SetLike S R] → [SubringClass S R] → NonAssocCommRing ↥s
-- Mathlib.Probability.Martingale.Upcrossing
/-- The number of upcrossings of a realization of a stochastic process (`upcrossings` takes value
in `ℝ≥0∞` and so is allowed to be `∞`).  -/
MeasureTheory.upcrossings : {Ω : Type u_1} → {ι : Type u_2} → [inst : Preorder ι] → [OrderBot ι] → [InfSet ι] → ℝ → ℝ → (ι → Ω → ℝ) → Ω → ENNReal
-- Mathlib.Algebra.GroupWithZero.Divisibility
isRelPrime_of_no_nonunits_factors : ∀ {α : Type u_1} [inst : MonoidWithZero α] {x y : α},
  ¬(x = 0 ∧ y = 0) → (∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y) → IsRelPrime x y
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.instAddMonObjOfIsCommAddMonObjX.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M : CategoryTheory.AddMon C}
  [inst_3 : CategoryTheory.IsCommAddMonObj M.X],
  CategoryTheory.AddMon.instAddMonObjOfIsCommAddMonObjX =
    { zero := { hom := CategoryTheory.AddMonObj.zero, isAddMonHom_hom := ⋯ },
      add := { hom := CategoryTheory.AddMonObj.add, isAddMonHom_hom := ⋯ }, zero_add := ⋯, add_zero := ⋯,
      add_assoc := ⋯ }
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Zero X] {A : Type u_2} [inst_2 : NonUnitalRing A]
  [inst_3 : StarRing A] [inst_4 : Module ℝ A], Function.Injective NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_erase_eq_of_not_compare_maxKeyD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k fallback : α},
      (t.erase k).isEmpty = false →
        ¬cmp k (t.maxKeyD fallback) = Ordering.eq → (t.erase k).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_ofSubtype : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {p : α → Prop} [inst_2 : DecidablePred p]
  (u : Equiv.Perm (Subtype p)), (Equiv.Perm.ofSubtype u).support = Finset.map (Function.Embedding.subtype p) u.support
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFiltered.coeq₃Hom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ : C}
  (f g h : j₁ ⟶ j₂),
  CategoryTheory.IsFiltered.coeq₃Hom f g h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.IsFiltered.coeqHom f g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.IsFiltered.leftToMax (CategoryTheory.IsFiltered.coeq f g) (CategoryTheory.IsFiltered.coeq g h))
        (CategoryTheory.IsFiltered.coeqHom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsFiltered.coeqHom f g)
            (CategoryTheory.IsFiltered.leftToMax (CategoryTheory.IsFiltered.coeq f g)
              (CategoryTheory.IsFiltered.coeq g h)))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsFiltered.coeqHom g h)
            (CategoryTheory.IsFiltered.rightToMax (CategoryTheory.IsFiltered.coeq f g)
              (CategoryTheory.IsFiltered.coeq g h)))))
-- Init.Data.Int.LemmasAux
_private.Init.Data.Int.LemmasAux.0.Int.toNat.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (a : ℕ) → motive (Int.negSucc a)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc a => h_2 a) =
    h_1 n
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_eq_sum_iff_of_le : ∀ {ι : Type u_9} {M : Type u_10} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M]
  {s : Finset ι} {f g : ι → M}, (∀ i ∈ s, f i ≤ g i) → (∑ i ∈ s, f i = ∑ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i)
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- `ModuleCat.Hom.hom` bundled as an `Equiv`.  -/
ModuleCat.homEquiv : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → (M ⟶ N) ≃ (↑M →ₗ[R] ↑N)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.explicitBinder.parenthesizer : optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Trace.Basic
Algebra.traceMatrix_of_basis : ∀ {κ : Type w} {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Fintype κ] [inst_4 : DecidableEq κ] (b : Module.Basis κ A B),
  Algebra.traceMatrix A ⇑b = (LinearMap.BilinForm.toMatrix b) (Algebra.traceForm A B)
-- Lean.Data.Lsp.Basic
/-- A snippet is a string that gets inserted into a document,
and can afterwards be edited by the user in a structured way.

Snippets contain instructions that
specify how this structured editing should proceed.
They are expressed in a domain-specific language
based on one from TextMate,
including the following constructs:
- Designated positions for subsequent user input,
  called "tab stops" after their most frequently-used keybinding.
  They are denoted with `$1`, `$2`, and so forth.
  `$0` denotes where the cursor should be positioned after all edits are completed,
  defaulting to the end of the string.
  Snippet tab stops are unrelated to tab stops used for indentation.
- Tab stops with default values, called _placeholders_, written `${1:default}`.
  The default may itself contain a tab stop or a further placeholder
  and multiple options to select from may be provided
  by surrounding them with `|`s and separating them with `,`,
  as in `${1|if $2 then $3 else $4,if let $2 := $3 then $4 else $5|}`.
- One of a set of predefined variables that are replaced with their values.
  This includes the current line number (`$TM_LINE_NUMBER`)
  or the text that was selected when the snippet was invoked (`$TM_SELECTED_TEXT`).
- Formatting instructions to modify variables using regular expressions
  or a set of predefined filters.

The full syntax and semantics of snippets,
including the available variables and the rules for escaping control characters,
are described in the [LSP specification](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#snippet_syntax).  -/
Lean.Lsp.SnippetString : Type
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_eq_sum_theta : ∀ {x : ℝ}, 0 ≤ x → Chebyshev.psi x = ∑ n ∈ Finset.Icc 1 ⌊Real.log x / Real.log 2⌋₊, Chebyshev.theta (x ^ (1 / ↑n))
-- Init.Data.List.Nat.Modify
List.modifyTailIdx_eq_take_drop : ∀ {α : Type u_1} (f : List α → List α),
  f [] = [] → ∀ (l : List α) (i : ℕ), l.modifyTailIdx i f = List.take i l ++ f (List.drop i l)
-- Mathlib.Order.SuccPred.Basic
Order.pred_top_lt_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a : α} [inst_2 : OrderTop α] [NoMinOrder α],
  Order.pred ⊤ < a ↔ a = ⊤
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ext_iff : ∀ {numVarsSucc : ℕ} {x y : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc}, x = y ↔ x.clause = y.clause
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.zero_lt_card : ∀ {o : Ordinal.{u_1}}, 0 < o.card ↔ 0 < o
-- Std.Async.Basic
/-- Typeclass for monads that can "await" a computation of type `t α` in a monad `m` until the result is
available.
 -/
Std.Async.MonadAwait : (Type → Type) → (Type → Type) → Type 1
-- Mathlib.CategoryTheory.Balanced
CategoryTheory.isIso_iff_epi_and_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Balanced C] {X Y : C} (f : Y ⟶ X),
  CategoryTheory.IsIso f ↔ CategoryTheory.Epi f ∧ CategoryTheory.Mono f
-- Lean.Elab.Tactic.SolveByElim
Lean.Elab.Tactic.SolveByElim.evalSolveByElim : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instCategory : CategoryTheory.Category.{u, u + 1} CommGrpCat
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List α} {k fallback : α},
      k ∉ t → l.contains k = false → (t.insertManyIfNewUnit l).getKeyD k fallback = fallback
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.brecOn_1.go : {motive_1 : Lean.IR.Alt → Sort u} →
  {motive_2 : Lean.IR.FnBody → Sort u} →
    {motive_3 : Array Lean.IR.Alt → Sort u} →
      {motive_4 : List Lean.IR.Alt → Sort u} →
        (t : Array Lean.IR.Alt) →
          ((t : Lean.IR.Alt) → t.below → motive_1 t) →
            ((t : Lean.IR.FnBody) → t.below → motive_2 t) →
              ((t : Array Lean.IR.Alt) → Lean.IR.Alt.below_1 t → motive_3 t) →
                ((t : List Lean.IR.Alt) → Lean.IR.Alt.below_2 t → motive_4 t) → motive_3 t ×' Lean.IR.Alt.below_1 t
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace_div : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (f : Module.End K V)
  (a b : K), b ≠ 0 → (f.genEigenspace (a / b)) 1 = (b • f - a • 1).ker
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₁_fst : ∀ (X : SSet),
  CategoryTheory.CategoryStruct.comp SSet.ι₁
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X (SSet.stdSimplex.obj { len := 1 })) =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.RingTheory.AdicCompletion.Basic
isHausdorff_iff : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsHausdorff I M ↔ ∀ (x : M), (∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]) → x = 0
-- Mathlib.Order.Heyting.Hom
CoheytingHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] (f : CoheytingHom α β),
  f.comp (CoheytingHom.id α) = f
-- Init.Data.Bool
Bool.apply_cond : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) {b : Bool} {a a' : α}, f (bif b then a else a') = bif b then f a else f a'
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Given a map `f : R →+ S`, return the corresponding map `R[M] → S[M]` obtained by mapping
each coefficient along `f`.  -/
MonoidAlgebra.map : {R : Type u_3} →
  {S : Type u_4} →
    {M : Type u_6} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+ S) → MonoidAlgebra R M → MonoidAlgebra S M
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toSubring_injective : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  Function.Injective Subalgebra.toSubring
-- Mathlib.Topology.Order.DenselyOrdered
nhdsLT_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] (a : α), (nhdsWithin a (Set.Iio a)).NeBot
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.trans : ∀ {α : Type u_1} {M₁ M₂ M₃ : Matroid α}, M₁.IsRestriction M₂ → M₂.IsRestriction M₃ → M₁.IsRestriction M₃
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.brecOn.eq : ∀ {C : Type u} {motive : CategoryTheory.FreeMonoidalCategory C → Sort u_1} (t : CategoryTheory.FreeMonoidalCategory C)
  (F_1 : (t : CategoryTheory.FreeMonoidalCategory C) → CategoryTheory.FreeMonoidalCategory.below t → motive t),
  CategoryTheory.FreeMonoidalCategory.brecOn t F_1 = F_1 t (CategoryTheory.FreeMonoidalCategory.brecOn.go t F_1).2
-- Mathlib.Algebra.Ring.Defs
NonAssocSemiring.toOne : {α : Type u} → [self : NonAssocSemiring α] → One α
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- The monad used for evaluating a `LazyEntry`.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.LazyM : Type → Type
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
/-- `Abelian.coimage S.g` is the cokernel of `kernel.ι S.g ≫ cokernel.π S.f`  -/
CategoryTheory.ShortComplex.cokernelToAbelianCoimageIsCokernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex C) →
        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.cokernelToAbelianCoimage ⋯)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
/-- Map a walk to its own subgraph.  -/
SimpleGraph.Walk.mapToSubgraph : {V : Type u} → {G : SimpleGraph V} → {u v : V} → (w : G.Walk u v) → w.toSubgraph.coe.Walk ⟨u, ⋯⟩ ⟨v, ⋯⟩
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.map_lid_comp_map_rid : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) {X X' : C} {Y Y' : D} (f : X ⟶ X') (g : Y ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (P.map (CategoryTheory.CategoryStruct.id X) g)
      (P.map f (CategoryTheory.CategoryStruct.id Y)) =
    P.map f g
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.add_neg_toRightFun_mem : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {T : Set G} (hT : AddSubgroup.IsComplement (↑H) T) (g : G),
  g + -↑(hT.toRightFun g) ∈ H
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.ω_mul_f : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : Fintype ι] (i : ↥b.support),
  RootPairing.GeckConstruction.ω b * RootPairing.GeckConstruction.f i =
    RootPairing.GeckConstruction.e i * RootPairing.GeckConstruction.ω b
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.instReflQuiverα : (C : CategoryTheory.ReflQuiv) → CategoryTheory.ReflQuiver ↑C
-- Mathlib.Tactic.ApplyWith
/-- Elaborator for the configuration in `apply (config := cfg)` syntax.  -/
Mathlib.Tactic.elabApplyConfig : Lean.Syntax → optParam Lean.Meta.ApplyConfig { } → optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Meta.ApplyConfig
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIoc.eq_1 : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜] (f : 𝕜 → B),
  AddCircle.liftIoc p a f = (Set.Ioc a (a + p)).domRestrict f ∘ ⇑(AddCircle.equivIoc p a)
-- Mathlib.Topology.Closure
closure_inter_subset_inter_closure : ∀ {X : Type u} [inst : TopologicalSpace X] (s t : Set X), closure (s ∩ t) ⊆ closure s ∩ closure t
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} →
        (aig : Std.Sat.AIG α) →
          aig.Ref → aig.Ref → old.decls.size ≤ aig.decls.size → Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput old
-- Lean.Parser.Term
Lean.Parser.Term.funImplicitBinder.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Probability.Distributions.Gaussian.Basic
/-- A real Gaussian measure is Gaussian.  -/
ProbabilityTheory.isGaussian_gaussianReal : ∀ (m : ℝ) (v : NNReal), ProbabilityTheory.IsGaussian (ProbabilityTheory.gaussianReal m v)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instKrullDimLEOfNatNatSubtypeMemValuationSubringValuationSubringAtPrime : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  Ring.KrullDimLE 1 ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v)
-- Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
DerivedCategory.instFullSingleFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (n : ℤ), (DerivedCategory.singleFunctor C n).Full
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of functions `∑' n, f n x`. If the series converges at a
point, and all functions in the series are differentiable with a summable bound on the derivatives,
then the series converges everywhere.  -/
summable_of_summable_hasDerivAt : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [inst_4 : NormedSpace 𝕜 F] {g g' : α → 𝕜 → F} {y₀ : 𝕜},
  Summable u →
    (∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y) →
      (∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n) → (Summable fun n => g n y₀) → ∀ (y : 𝕜), Summable fun n => g n y
-- Mathlib.Data.Multiset.Defs
Multiset.pairwise_coe_iff_pairwise : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r] {l : List α}, Multiset.Pairwise r ↑l ↔ List.Pairwise r l
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- Split equalizers are absolute: they are preserved by any functor.  -/
CategoryTheory.IsSplitEqualizer.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X Y : C} →
          {f g : X ⟶ Y} →
            {W : C} →
              {ι : W ⟶ X} →
                CategoryTheory.IsSplitEqualizer f g ι →
                  (F : CategoryTheory.Functor C D) → CategoryTheory.IsSplitEqualizer (F.map f) (F.map g) (F.map ι)
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.instCoeSortType : CoeSort PartOrdEmb (Type u_1)
-- Lean.Elab.Parallel
/-- Runs a list of CoreM computations in parallel and collects results in the original order,
discarding state information.

Unlike `par`, this doesn't return state information from tasks.

The final CoreM state is restored to the initial state (before tasks ran).
 -/
Lean.Core.CoreM.par' : {α : Type} → List (Lean.CoreM α) → Lean.CoreM (List (Except Lean.Exception α))
-- Mathlib.Algebra.CharP.Lemmas
Commute.exists_add_pow_prime_pow_eq : ∀ {R : Type u_1} [inst : Semiring R] {p : ℕ},
  Nat.Prime p → ∀ {x y : R}, Commute x y → ∀ (n : ℕ), ∃ r, (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * x * y * r
-- Init.Data.List.Attach
List.getElem_attachWith : ∀ {α : Type u_1} {xs : List α} {P : α → Prop} {H : ∀ a ∈ xs, P a} {i : ℕ} (h : i < (xs.attachWith P H).length),
  (xs.attachWith P H)[i] = ⟨xs[i], ⋯⟩
-- Mathlib.RingTheory.Ideal.HasGoingUp
/-- This generalizes `exists_ideal_over_prime_of_isIntegral_of_isPrime`
to arbitrary length chains.  -/
Ideal.exists_ltSeries_of_hasGoingUp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.HasGoingUp R S] (l : LTSeries (PrimeSpectrum R)) (P : Ideal S) [inst_4 : P.IsPrime]
  [lo : P.LiesOver (RelSeries.head l).asIdeal],
  ∃ L,
    L.length = l.length ∧
      RelSeries.head L = { asIdeal := P, isPrime := ⋯ } ∧
        List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = RelSeries.toList l
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂_symm' : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] {σ₁ : R →+* R} [inst_7 : Fintype n]
  [inst_8 : Fintype m] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁)
  (b₂ : Module.Basis m R M₂), (LinearMap.toMatrix₂ b₁ b₂).symm = Matrix.toLinearMapₛₗ₂ σ₁ b₁ b₂
-- Mathlib.Tactic.GRewrite.Core
/-- The congruence loop keeps track of its progress using 3 states.
- Each rewrite starts off as `noMatch`.
- As soon as a rewrite has successfully been applied with `GRewriteLemma.apply`,
  this switches to `matched`. In this state we continue trying to rewrite.
- When the rewrite lemma is not valid anymore in the local context, i.e. if the lemma depends on a
  free variable that is not in scope anymore, then we switch to `matchedOutOfScope`.
  In this state we stop trying to rewrite.
 -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.Progress : Type
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd_symm_apply_snd_coe : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : Finset.HasMulAntidiagonal A] (x : A × A),
  ↑(Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd.symm x).snd = x
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- The main technical lemma for `GammaSeq_tendsto_Gamma`, expressing the integral defining the
Gamma function for `0 < re s` as the limit of a sequence of integrals over finite intervals.  -/
Complex.approx_Gamma_integral_tendsto_Gamma_integral : ∀ {s : ℂ},
  0 < s.re →
    Filter.Tendsto (fun n => ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) Filter.atTop
      (nhds (Complex.Gamma s))