mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Basic
Filter.GenerateSets.below.inter : ∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → Filter.GenerateSets g a → Prop} {s t : Set α}
  (a : Filter.GenerateSets g s) (a_1 : Filter.GenerateSets g t),
  Filter.GenerateSets.below a → motive s a → Filter.GenerateSets.below a_1 → motive t a_1 → Filter.GenerateSets.below ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.isCharTwoNF_of_isCharTwoJEqZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF], W.IsCharTwoNF
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- This is [grinberg_clifford_2016] Theorem 12  -/
CliffordAlgebra.contractRight_mul_ι : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (d : Module.Dual R M) (a : M) (b : CliffordAlgebra Q),
  (CliffordAlgebra.contractRight (b * (CliffordAlgebra.ι Q) a)) d =
    d a • b - (CliffordAlgebra.contractRight b) d * (CliffordAlgebra.ι Q) a
-- Mathlib.Algebra.Group.Commute.Units
isAddUnit_nsmul_succ_iff : ∀ {M : Type u_1} [inst : AddMonoid M] {n : ℕ} {a : M}, IsAddUnit ((n + 1) • a) ↔ IsAddUnit a
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ico : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => a * x) ⁻¹' Set.Ico b c = Set.Ico (b / a) (c / a)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSup : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [Max β] → Max (l.Germ β)
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.locallyCompactSpace_of_hasBasis : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : AddGroup X] [IsTopologicalAddGroup X]
  [inst_3 : UniformSpace Y] [inst_4 : AddCommGroup Y] [IsUniformAddGroup Y] [T0Space Y] [CompactSpace Y]
  [LocallyCompactSpace X] (V : ℕ → Set Y),
  (∀ {n : ℕ} {x : Y}, x ∈ V n → x + x ∈ V n → x ∈ V (n + 1)) →
    (nhds 0).HasBasis (fun x => True) V → LocallyCompactSpace (X →ₜ+ Y)
-- Mathlib.Data.Matrix.Basic
LinearEquiv.mapMatrix_refl : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type u_11} [inst : Semiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : Module R α], (LinearEquiv.refl R α).mapMatrix = LinearEquiv.refl R (Matrix m n α)
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
NonUnitalNonAssocCommSemiring.mul_comm : ∀ {α : Type u} [self : NonUnitalNonAssocCommSemiring α] (a b : α), a * b = b * a
-- Mathlib.Algebra.GroupWithZero.Commute
Commute.zero_right : ∀ {G₀ : Type u_2} [inst : MulZeroClass G₀] (a : G₀), Commute a 0
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.iConvexComb_congr : ∀ {R : Type u_1} {M : Type u_3} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] {w : Convexity.StdSimplex R I} {f g : I → M},
  (∀ (i : I), w.weights i ≠ 0 → f i = g i) → Convexity.iConvexComb w f = Convexity.iConvexComb w g
-- Mathlib.Tactic.Simps.Basic
/-- Make `MkSimpContextResult` giving data instead of Syntax. Doesn't support arguments.
Intended to be very similar to `Lean.Elab.Tactic.mkSimpContext`
Todo: support arguments.  -/
Lean.Meta.mkSimpContextResult : optParam Lean.Meta.Simp.Config { } →
  optParam Bool false →
    optParam Lean.Elab.Tactic.SimpKind Lean.Elab.Tactic.SimpKind.simp →
      optParam Lean.Elab.Tactic.Simp.DischargeWrapper Lean.Elab.Tactic.Simp.DischargeWrapper.default →
        optParam Bool false → Lean.MetaM Lean.Elab.Tactic.MkSimpContextResult
-- Plausible.Testable
/-- Result of trying to disprove `p`  -/
Plausible.TestResult : Prop → Type
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- Up to an equivalence, the category `DescentData` for a pseudofunctor `F` and
a family of morphisms `f : X i ⟶ S` is unchanged when we replace `S` by an isomorphic object,
or when we replace `f` by another family which generate the same sieve.  -/
CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {S' : C} →
                {ι' : Type t'} →
                  {X' : ι' → C} →
                    {f' : (j : ι') → X' j ⟶ S'} →
                      (e : S' ≅ S) →
                        {α : ι' → ι} →
                          {p' : (j : ι') → X' j ⟶ X (α j)} →
                            (∀ (j : ι'),
                                CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) =
                                  CategoryTheory.CategoryStruct.comp (f' j) e.hom) →
                              {β : ι → ι'} →
                                {q' : (i : ι) → X i ⟶ X' (β i)} →
                                  (∀ (i : ι),
                                      CategoryTheory.CategoryStruct.comp (q' i) (f' (β i)) =
                                        CategoryTheory.CategoryStruct.comp (f i) e.inv) →
                                    (F.DescentData f ≌ F.DescentData f')
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.ofFun_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul β] (f g : α → β),
  UniformFun.ofFun (f * g) = UniformFun.ofFun f * UniformFun.ofFun g
-- Mathlib.Order.Hom.WithTopBot
OrderIso.withBotCongr_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (e : α ≃o β),
  ⇑e.withBotCongr = WithBot.map ⇑e
-- Mathlib.Data.Set.Card
/-- The cardinality of `s : Set α` . Has the junk value `0` if `s` is infinite  -/
Set.ncard : {α : Type u_1} → Set α → ℕ
-- Std.Data.DTreeMap.Internal.Operations
/-- A balanced tree.  -/
Std.DTreeMap.Internal.Impl.BalancedTree : (α : Type u) → (α → Type v) → Type (max u v)
-- Std.Tactic.Do.Syntax
/-- `massumption` is like `assumption`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : Q ⊢ₛ P → Q := by
  mintro _ _
  massumption
```
 -/
Lean.Parser.Tactic.massumption : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_apply_eq_apply_iff : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o a : Ordinal.{u}},
  Order.IsNormal f → (Ordinal.veblenWith f o (f a) = f a ↔ Ordinal.veblenWith f o a = a)
-- Mathlib.CategoryTheory.Limits.Connected
/-- When `J` is a connected category, the colimit of a
constant functor `J ⥤ C` with value `X : C` identifies to `X`.  -/
CategoryTheory.Limits.isColimitConstCocone : (J : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        (X : C) →
          [CategoryTheory.IsConnected J] → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.constCocone J X)
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- Given a finite-dimensional subspace `K₂`, and a subspace `K₁`
contained in it, the dimensions of `K₁` and the intersection of its
orthogonal subspace with `K₂` add to that of `K₂`.  -/
Submodule.finrank_add_inf_finrank_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K₁ K₂ : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥K₂],
  K₁ ≤ K₂ → Module.finrank 𝕜 ↥K₁ + Module.finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = Module.finrank 𝕜 ↥K₂
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.eigenvectorBasis.congr_simp : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T T_1 : E →ₗ[𝕜] E} (e_T : T = T_1) [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric)
  (hn : Module.finrank 𝕜 E = n), hT.eigenvectorBasis hn = ⋯.eigenvectorBasis hn
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_exponent_zero : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.eLpNorm' f 0 μ = 1
-- Mathlib.Order.CompleteLattice.Basic
OrderIso.map_sInf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (s : Set α),
  f (sInf s) = ⨅ a ∈ s, f a
-- Mathlib.Data.List.MinMax
List.argAux_self : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r], Std.Irrefl r → ∀ (a : α), List.argAux r (some a) a = some a
-- Aesop.Frontend.Tactic
Aesop.Frontend.Parser.«tactic_clause(Simp_config:=_)» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Category.RelCat
/-- Build a morphism `X ⟶ Y` for `X Y : RelCat` from a relation between `X` and `Y`.  -/
CategoryTheory.RelCat.Hom.ofRel : {X Y : CategoryTheory.RelCat} → SetRel X Y → X.Hom Y
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.dvd_lcm_left : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (x y : R), x ∣ EuclideanDomain.lcm x y
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'.eq_3 : ∀ {α : Type u_1} (a : α), (RegularExpression.char a).matches' = {[a]}
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
comap_measurable : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace β} (f : α → β), Measurable f
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.div_div_cancel_left : ∀ {α : Type u} [inst : DivisionCommMonoid α] {a b : α}, IsUnit a → a / b / a = b⁻¹
-- Mathlib.Topology.Sets.Closeds
/-- The type of irreducible closed subsets of a topological space.  -/
TopologicalSpace.IrreducibleCloseds : (α : Type u_4) → [TopologicalSpace α] → Type u_4
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.of_indicator_const : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : Zero β] {s : Set α} {c : β},
  Filter.EventuallyConst (s.indicator fun x => c) l → c ≠ 0 → Filter.EventuallyConst s l
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.log_zpow : ∀ {G : Type u_5} [inst : AddGroup G] (x : WithZero (Multiplicative G)) (n : ℤ), (x ^ n).log = n • x.log
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.forIn_pure_yield_eq_fold : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {f : β → γ → γ} {init : γ}
  {it : Std.IterM m β},
  (forIn it init fun c b => pure (ForInStep.yield (f c b))) = Std.IterM.fold (fun b c => f c b) init it
-- Mathlib.Topology.Order.IntermediateValue
/-- Every continuous injective `f : (a, b) → δ` is strictly monotone
or antitone (increasing or decreasing).  -/
ContinuousOn.strictMonoOn_of_injOn_Ioo : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ},
  a < b →
    ContinuousOn f (Set.Ioo a b) →
      Set.InjOn f (Set.Ioo a b) → StrictMonoOn f (Set.Ioo a b) ∨ StrictAntiOn f (Set.Ioo a b)
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextEdit.mk.sizeOf_spec : ∀ (range : Lean.Lsp.Range) (newText : String) (leanExtSnippet? : Option Lean.Lsp.SnippetString)
  (annotationId? : Option String),
  sizeOf { range := range, newText := newText, leanExtSnippet? := leanExtSnippet?, annotationId? := annotationId? } =
    1 + sizeOf range + sizeOf newText + sizeOf leanExtSnippet? + sizeOf annotationId?
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- **Alias** of `hasFDerivWithinAt_sdiff_singleton_self`. -/
hasFDerivWithinAt_diff_singleton_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' (s \ {x}) x ↔ HasFDerivWithinAt f f' s x
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.nonZeroDivisors_le_comap : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S], nonZeroDivisors R ≤ Submonoid.comap (algebraMap R S) (nonZeroDivisors S)
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  (A : CategoryTheory.CommMon (CategoryTheory.Functor C D)) (X : C),
  CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul.app X
-- Mathlib.Topology.Algebra.UniformConvergence
instAddMonoidUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoid β],
  instAddMonoidUniformFun =
    { toAdd := instAddUniformFun, add_assoc := ⋯, toZero := instZeroUniformFun, zero_add := ⋯, add_zero := ⋯,
      toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasStrictFDerivAt_add_const_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} (c : F), HasStrictFDerivAt (fun x => f x + c) f' x ↔ HasStrictFDerivAt f f' x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.toArray_eq_empty_iff : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.Rxc.IsAlwaysFinite α],
  r.toArray = #[] ↔ ¬r.lower < r.upper
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β}, (t.alter k f)[k']? = if cmp k k' = Ordering.eq then f t[k]? else t[k']?
-- Std.Http.Protocol.H1
/-- The state of the writer.
 -/
Std.Http.Protocol.H1.Machine.writer : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Writer dir
-- Aesop.Stats.Extension
Aesop.StatsExtensionEntry.forCurrentFile : {m : Type → Type} → [Monad m] → [Lean.MonadLog m] → Lean.Syntax → Aesop.Stats → m Aesop.StatsExtensionEntry
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The natural transformation `S.cycles ⟶ S.leftHomology` for all short complexes `S`.  -/
CategoryTheory.ShortComplex.leftHomologyπNatTrans : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasKernels C] →
        [inst_3 : CategoryTheory.Limits.HasCokernels C] →
          CategoryTheory.ShortComplex.cyclesFunctor C ⟶ CategoryTheory.ShortComplex.leftHomologyFunctor C
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.eq : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {a b : α}, ↑a = ↑b ↔ -a + b ∈ s
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) [inst_2 : Inhabited (β k)],
  Std.DTreeMap.Internal.Impl.leaf.get! k =
    panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.get!" 108 13
      "Key is not present in map"
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the second of three points is strictly between the other two, the oriented angle at that
point is π.  -/
Sbtw.oangle₁₂₃_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi
-- Mathlib.Topology.ContinuousMap.CocompactMap
/-- `CocompactMapClass F α β` states that `F` is a type of cocompact continuous maps.

You should also extend this typeclass when you extend `CocompactMap`.  -/
CocompactMapClass : (F : Type u_1) →
  (α : outParam (Type u_2)) →
    (β : outParam (Type u_3)) → [TopologicalSpace α] → [TopologicalSpace β] → [FunLike F α β] → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer.0.CategoryTheory.Limits.MulticospanIndex.multicospan.match_1.splitter : {J : CategoryTheory.Limits.MulticospanShape} →
  (motive : (x y : CategoryTheory.Limits.WalkingMulticospan J) → (x ⟶ y) → Sort u_3) →
    (x y : CategoryTheory.Limits.WalkingMulticospan J) →
      (f : x ⟶ y) →
        ((x : CategoryTheory.Limits.WalkingMulticospan J) →
            motive x x (CategoryTheory.Limits.WalkingMulticospan.Hom.id x)) →
          ((b : J.R) →
              motive (CategoryTheory.Limits.WalkingMulticospan.left (J.fst b))
                (CategoryTheory.Limits.WalkingMulticospan.right b)
                (CategoryTheory.Limits.WalkingMulticospan.Hom.fst b)) →
            ((b : J.R) →
                motive (CategoryTheory.Limits.WalkingMulticospan.left (J.snd b))
                  (CategoryTheory.Limits.WalkingMulticospan.right b)
                  (CategoryTheory.Limits.WalkingMulticospan.Hom.snd b)) →
              motive x y f
-- Batteries.Data.Array.Scan
Array.getElem_scanr : ∀ {α : Type u_1} {β : Type u_2} {i : ℕ} {b : β} {l : Array α} {f : α → β → β} (h : i < (Array.scanr f b l).size),
  (Array.scanr f b l)[i] = Array.foldr f b (l.drop i)
-- Mathlib.Topology.Separation.Hausdorff
/-- If functions `f` and `g` are continuous on a closed set `s`,
then the set of points `x ∈ s` such that `f x = g x` is a closed set.  -/
IsClosed.isClosed_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {f g : X → Y}
  {s : Set X}, IsClosed s → ContinuousOn f s → ContinuousOn g s → IsClosed {x | x ∈ s ∧ f x = g x}
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
/-- Extension for `ArithmeticFunction.zeta`.  -/
Mathlib.Meta.Positivity.evalArithmeticFunctionZeta : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.isPWO_iUnion_support_prod_smul : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ]
  [inst_1 : PartialOrder Γ'] [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid R] [inst_4 : SMulWithZero R V]
  [inst_5 : VAdd Γ Γ'] [inst_6 : IsOrderedCancelVAdd Γ Γ'] {s : α → HahnSeries Γ R} {t : β → HahnSeries Γ' V},
  (⋃ a, (s a).support).IsPWO →
    (⋃ b, (t b).support).IsPWO →
      (⋃ a, ((fun a => (HahnModule.of R).symm (s a.1 • (HahnModule.of R) (t a.2))) a).support).IsPWO
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianPDF_lt_top : ∀ {μ : ℝ} {v : NNReal} {x : ℝ}, ProbabilityTheory.gaussianPDF μ v x < ⊤
-- Mathlib.Combinatorics.Quiver.Symmetric
_private.Mathlib.Combinatorics.Quiver.Symmetric.0.Quiver.Path.reverse.match_1.eq_2 : ∀ {V : Type u_2} [inst : Quiver V] {a : V} (motive : (x : V) → Quiver.Path a x → Sort u_3) (x b : V)
  (p : Quiver.Path a b) (e : b ⟶ x) (h_1 : Unit → motive a Quiver.Path.nil)
  (h_2 : (x b : V) → (p : Quiver.Path a b) → (e : b ⟶ x) → motive x (p.cons e)),
  (match x, p.cons e with
    | .(a), Quiver.Path.nil => h_1 ()
    | x, p.cons e => h_2 x b p e) =
    h_2 x b p e
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instIsScalarTower : ∀ {α : Type u} {β : Type v} {𝕜 : Type u_2} [inst : PseudoMetricSpace 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : PseudoMetricSpace β] [inst_3 : Zero 𝕜] [inst_4 : Zero β] [inst_5 : SMul 𝕜 β] [inst_6 : IsBoundedSMul 𝕜 β]
  {𝕜' : Type u_3} [inst_7 : PseudoMetricSpace 𝕜'] [inst_8 : Zero 𝕜'] [inst_9 : SMul 𝕜' β] [inst_10 : IsBoundedSMul 𝕜' β]
  [inst_11 : SMul 𝕜' 𝕜] [IsScalarTower 𝕜' 𝕜 β], IsScalarTower 𝕜' 𝕜 (BoundedContinuousFunction α β)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- A Post-Turing machine with symbol type `Γ` and label type `Λ`
is a function which, given the current state `q : Λ` and
the tape head `a : Γ`, either halts (returns `none`) or returns
a new state `q' : Λ` and a `Stmt` describing what to do,
either a move left or right, or a write command.

Both `Λ` and `Γ` are required to be inhabited; the default value
for `Γ` is the "blank" tape value, and the default value of `Λ` is
the initial state.  -/
Turing.TM0.Machine : Type u_1 → (Λ : Type u_2) → [Inhabited Λ] → Type (max (max u_1 u_2) u_1 u_2)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonReferenceContext : Lean.ToJson Lean.Lsp.ReferenceContext
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGT : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (a b : ℤ) [t.IsGE X a], t.IsGE ((t.truncGT b).obj X) a
-- Mathlib.Algebra.Group.End
Equiv.Perm.refl_inv : ∀ {α : Type u_4}, (Equiv.refl α)⁻¹ = 1
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.fst_comp_prodAssoc : ∀ {R : Type u} {M₂ : Type w} {M₃ : Type y} {M₁ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃],
  LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ ↑(LinearEquiv.prodAssoc R M₁ M₂ M₃) =
    LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃
-- Mathlib.Util.CountHeartbeats
/-- The "countHeartbeats" linter counts the heartbeats of every declaration.

The effect of the linter is similar to `#count_heartbeats in xxx`, except that it applies
to all declarations.

Note that the linter only counts heartbeats in "top-level" declarations:
it looks inside `set_option ... in`, but not, for instance, inside `mutual` blocks.

There is a convenience notation `#count_heartbeats` that simply sets the linter option to true.
 -/
Mathlib.Linter.CountHeartbeats.countHeartbeatsLinter : Lean.Linter
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuationDef_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
  v.intValuationDef 0 = 0
-- Init.Data.List.Lex
List.lex.eq_3 : ∀ {α : Type u} [inst : BEq α] (lt : α → α → Bool) (a : α) (as : List α) (b : α) (bs : List α),
  (a :: as).lex (b :: bs) lt = (lt a b || a == b && as.lex bs lt)
-- Mathlib.GroupTheory.PGroup
IsPGroup.card_eq_or_dvd : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], IsPGroup p G → ∀ [hp : Fact (Nat.Prime p)], Nat.card G = 1 ∨ p ∣ Nat.card G
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_univ : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  ∫ᵛ (x : X) in Set.univ, f x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ]
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
/-- **Law of total probability** using `condExp` as conditional probability.  -/
MeasureTheory.integral_condExp_indicator : ∀ {α : Type u_1} {β : Type u_2} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [mβ : MeasurableSpace β]
  {Y : α → β} (hY : Measurable Y) [MeasureTheory.SigmaFinite (μ.trim ⋯)] {A : Set α},
  MeasurableSet A → ∫ (x : α), μ[A.indicator fun x => 1 | MeasurableSpace.comap Y mβ] x ∂μ = μ.real A
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The functor to `TopCat` preserves finite coproducts if they exist.  -/
CompHausLike.instPreservesFiniteCoproductsTopCatCompHausLikeToTopOfHasExplicitFiniteCoproducts : ∀ (P : TopCat → Prop) [CompHausLike.HasExplicitFiniteCoproducts P],
  CategoryTheory.Limits.PreservesFiniteCoproducts (CompHausLike.compHausLikeToTop P)