mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- A polynomial functor `P` is given by a type `A` and a family `B` of types over `A`. `P` maps
any type `α` to a new type `P α`, which is defined as the sigma type `Σ x, P.B x → α`.

An element of `P α` is a pair `⟨a, f⟩`, where `a` is an element of a type `A` and
`f : B a → α`. Think of `a` as the shape of the object and `f` as an index to the relevant
elements of `α`.
 -/
PFunctor : Type (max (uA + 1) (uB + 1))
-- Lean.Meta.Tactic.Grind.Attr
/-- Extension backing the `@[lia]` attribute. It uses the same recording mechanism as `@[grind]`
(see `registerAttr`), but provides a separate, smaller E-matching lemma set that the `lia`
tactic instantiates (e.g. `Nat.max_def`), without enabling the full `@[grind]` set.
 -/
Lean.Meta.Grind.liaExt : Lean.Meta.Grind.Extension
-- Mathlib.MeasureTheory.Measure.Sub
MeasureTheory.Measure.sub_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ - ⊤ = 0
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrictₗ_apply : ∀ {α : Type u_2} {_m0 : MeasurableSpace α} (s : Set α) (μ : MeasureTheory.Measure α),
  (MeasureTheory.Measure.restrictₗ s) μ = μ.restrict s
-- Init.Data.List.Find
List.finIdxOf?_nil : ∀ {α : Type u_1} {a : α} [inst : BEq α], List.finIdxOf? a [] = none
-- Init.Tactics
Lean.Parser.Tactic.DecideConfig.mk : Bool → Bool → Bool → Bool → Lean.Parser.Tactic.DecideConfig
-- Mathlib.Order.Antisymmetrization
instPartialOrderAntisymmetrization : {α : Type u_1} → [inst : Preorder α] → PartialOrder (Antisymmetrization α fun x1 x2 => x1 ≤ x2)
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
FiniteDimensional.basisSingleton_apply : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (ι : Type u_1)
  [inst_3 : Unique ι] (h : Module.finrank K V = 1) (v : V) (hv : v ≠ 0) (i : ι),
  (FiniteDimensional.basisSingleton ι h v hv) i = v
-- Std.Http.Data.URI.Encoding
Std.Http.URI.EncodedString.instToString : {r : UInt8 → Bool} → ToString (Std.Http.URI.EncodedString r)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.mk.sizeOf_spec : ∀ {𝕜 : Type u} {A : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SizeOf 𝕜]
  [inst_6 : SizeOf A] (toProd : (A →L[𝕜] A) × (A →L[𝕜] A)) (central : ∀ (x y : A), toProd.2 x * y = x * toProd.1 y),
  sizeOf { toProd := toProd, central := central } = 1 + sizeOf toProd
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- A local frame locally spans the space of sections for `V`: for each local trivialisation `e`
of `V` around `x`, we have
`s = ∑ i, (LinearMap.piApply (b.localFrameCoeff e i) s) • b.localFrame e i` near `x`.  -/
Bundle.Trivialization.eventually_eq_localFrame_sum_coeff_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V] {ι : Type u_7}
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_14 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F)
  [inst_15 : ContMDiffVectorBundle 1 F V I] {x : M} {s : (x : M) → V x} [inst_16 : Fintype ι],
  x ∈ e.baseSet →
    ∀ᶠ (x' : M) in nhds x, s x' = ∑ i, (Bundle.Trivialization.localFrameCoeff I e b i x') (s x') • e.localFrame b i x'
-- Mathlib.Data.ENNReal.Inv
ENNReal.orderIsoIicCoe_symm_apply_coe : ∀ (a : NNReal) (b : ↑(Set.Iic a)), ↑((ENNReal.orderIsoIicCoe a).symm b) = ↑↑b
-- Lean.Util.Path
_private.Lean.Util.Path.0.Lean.modToFilePath.go : System.FilePath → Lean.Name → System.FilePath
-- Mathlib.Data.FinEnum
FinEnum.card_bitVec : ∀ (n : ℕ), FinEnum.card (BitVec n) = 2 ^ n
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtension.newDiseq : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Order.FixedPoints
OrderHom.map_le_gfp : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α}, a ≤ OrderHom.gfp f → f a ≤ OrderHom.gfp f
-- Lean.ToExpr
Lean.instToExprArrayOfToLevel : {α : Type u} → [Lean.ToLevel] → [Lean.ToExpr α] → Lean.ToExpr (Array α)
-- Init.Data.String.Lemmas.Order
String.Pos.ofSliceTo_le_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos},
  String.Pos.ofSliceTo p ≤ q ↔ ∀ (h : q ≤ p₀), p ≤ p₀.sliceTo q h
-- Mathlib.Order.Max
IsTop.mono : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsTop a → a ≤ b → IsTop b
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk_X_0 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) →
      (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0),
  (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 0 = X₀
-- Init.Data.Nat.Log2
Nat.log2_terminates : ∀ n ≥ 2, n / 2 < n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β} {h₁ : a ∈ t.insert k v}, (t.insert k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq then k else t.getKey a ⋯
-- Mathlib.RingTheory.Congruence.Basic
RingCon.toCon_bot : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R], ⊥.toCon = ⊥
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonWindowClientCapabilities : Lean.FromJson Lean.Lsp.WindowClientCapabilities
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The identity map of fixing subgroup of stabilizer
into the fixing subgroup of the extended set, as an equivariant map.  -/
SubMulAction.ofFixingSubgroup_insert_map : {M : Type u_1} →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] →
        (a : α) →
          (s : Set ↥(SubMulAction.ofStabilizer M a)) →
            ↥(SubMulAction.ofFixingSubgroup M
                  (insert a (Subtype.val '' s))) →ₑ[⇑(SubMulAction.fixingSubgroupInsertEquiv a s)]
              ↥(SubMulAction.ofFixingSubgroup (↥(MulAction.stabilizer M a)) s)
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_sub : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (s : Set E) (x : E),
  Metric.ball x δ - s = x +ᵥ Metric.thickening δ (-s)
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.ιTruncLE_naturality_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncLE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : CategoryTheory.Limits.HasZeroObject C] {Z : HomologicalComplex C c'} (h : L ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncLEMap φ e)
      (CategoryTheory.CategoryStruct.comp (L.ιTruncLE e) h) =
    CategoryTheory.CategoryStruct.comp (K.ιTruncLE e) (CategoryTheory.CategoryStruct.comp φ h)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.exists_eq_cons_of_ne : ∀ {V : Type u} {G : SimpleGraph V} {u v : V},
  u ≠ v → ∀ (p : G.Walk u v), ∃ w, ∃ (h : G.Adj u w), ∃ p', p = SimpleGraph.Walk.cons h p'
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_eq_preimage_infEDist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α),
  Metric.cthickening δ E = (fun x => Metric.infEDist x E) ⁻¹' Set.Iic (ENNReal.ofReal δ)
-- Init.Data.UInt.Bitwise
UInt16.zero_or : ∀ {a : UInt16}, 0 ||| a = a
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- If the domain of a surjective linear map is finite dimensional, the codomain must be as well.  -/
FiniteDimensional.of_surjective : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂),
  Function.Surjective ⇑f → ∀ [FiniteDimensional K V], FiniteDimensional K V₂
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
Cardinal.SharplyLT.le : ∀ {κ₁ κ₂ : Cardinal.{w}} [inst : Fact κ₁.IsRegular] [inst_1 : Fact κ₂.IsRegular], κ₁.SharplyLT κ₂ → κ₁ ≤ κ₂
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.isSplitMono_iff_isIso_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C)
  [CategoryTheory.IsIso T.μ], CategoryTheory.IsSplitMono (T.η.app X) ↔ CategoryTheory.IsIso (T.η.app X)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_lt_add_iff_left : ∀ {α : Type u} [inst : Add α] {x y z : WithTop α} [inst_1 : LT α] [AddLeftStrictMono α] [AddLeftReflectLT α],
  x ≠ ⊤ → (x + y < x + z ↔ y < z)
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_hom_app : ∀ (X : CommRingCat),
  AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity.hom.app X = CategoryTheory.inv (AlgebraicGeometry.toSpecΓ X)
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Result.proof : Mathlib.Meta.FunProp.Result → Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.contDiffAt_rpow_const_of_ne : ∀ {x p : ℝ} {n : WithTop ℕ∞}, x ≠ 0 → ContDiffAt ℝ n (fun x => x ^ p) x
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.sheafIso_inv_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ ℱ' : CategoryTheory.Sheaf K A} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj),
  (CategoryTheory.Functor.IsCoverDense.sheafIso i).inv.hom =
    CategoryTheory.inv (CategoryTheory.Functor.IsCoverDense.sheafHom i.hom)
-- Mathlib.Order.Filter.Basic
Filter.frequently_sSup : ∀ {α : Type u} {p : α → Prop} {fs : Set (Filter α)}, (∃ᶠ (x : α) in sSup fs, p x) ↔ ∃ f ∈ fs, ∃ᶠ (x : α) in f, p x
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.hasSum_nat_add_iff : ∀ {f : ℕ → NNReal} (k : ℕ) {a : NNReal}, HasSum (fun n => f (n + k)) a ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.Sheaf.isConstant_iff_forget : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {B : Type u_3} [inst_3 : CategoryTheory.Category.{v_3, u_3} B] (U : CategoryTheory.Functor D B)
  [inst_4 : CategoryTheory.HasWeakSheafify J B] [J.PreservesSheafification U] [inst_6 : J.HasSheafCompose U]
  (F : CategoryTheory.Sheaf J D) [(CategoryTheory.constantSheaf J D).Faithful] [(CategoryTheory.constantSheaf J D).Full]
  [(CategoryTheory.constantSheaf J B).Faithful] [(CategoryTheory.constantSheaf J B).Full]
  [(CategoryTheory.sheafCompose J U).ReflectsIsomorphisms] {T : C} (hT : CategoryTheory.Limits.IsTerminal T),
  CategoryTheory.Sheaf.IsConstant J F ↔ CategoryTheory.Sheaf.IsConstant J ((CategoryTheory.sheafCompose J U).obj F)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.toPresheaf_map_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) (X : Cᵒᵖ) (x : ↑(M₁.obj X)),
  (AddCommGrpCat.Hom.hom (((PresheafOfModules.toPresheaf R).map f).app X)) x =
    (CategoryTheory.ConcreteCategory.hom (f.app X)) x
-- Mathlib.Condensed.Light.Explicit
/-- The light condensed object associated to a presheaf on `LightProfinite` which preserves finite
products and satisfies the equalizer condition.
 -/
LightCondensed.ofSheafLightProfinite : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    (F : CategoryTheory.Functor LightProfiniteᵒᵖ A) →
      [CategoryTheory.Limits.PreservesFiniteProducts F] →
        CategoryTheory.regularTopology.EqualizerCondition F → LightCondensed A
-- Init.Data.Array.MapIdx
_private.Init.Data.Array.MapIdx.0.List.mapIdxM_toArray.go : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {l : List α} {f : ℕ → α → m β} (bs : List α)
  (acc : Array β) (inv : bs.length + acc.size = l.length),
  List.mapFinIdxM.go l (fun i a h => f i a) bs acc inv = List.mapIdxM.go f bs acc
-- Mathlib.Tactic.Order.Preprocessing
/-- Preprocesses facts for partial orders. Replaces `x < y`, `¬ (x ≤ y)`, and `x = y` with
equivalent facts involving only `≤`, `≠`, and `≮`. For each fact `x = y ⊔ z` adds `y ≤ x`
and `z ≤ x` facts, and similarly for `⊓`.  -/
Mathlib.Tactic.Order.preprocessFactsPartial : Array Mathlib.Tactic.Order.AtomicFact → Mathlib.Tactic.AtomM (Array Mathlib.Tactic.Order.AtomicFact)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearEquiv.arrowCongr_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : AddCommGroup E]
  [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H] [inst_4 : NormedField 𝕜]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] [inst_7 : Module 𝕜 G] [inst_8 : Module 𝕜 H] [inst_9 : TopologicalSpace E]
  [inst_10 : TopologicalSpace F] [inst_11 : TopologicalSpace G] [inst_12 : TopologicalSpace H]
  [inst_13 : IsTopologicalAddGroup G] [inst_14 : IsTopologicalAddGroup H] [inst_15 : ContinuousConstSMul 𝕜 G]
  [inst_16 : ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) (f : E →L[𝕜] H) (x : F),
  ((e₁.arrowCongr e₂) f) x = e₂ (f (e₁.symm x))
-- Init.Data.UInt.Lemmas
UInt8.toNat_mul : ∀ (a b : UInt8), (a * b).toNat = a.toNat * b.toNat % 2 ^ 8
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.append.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) (x : RBTree.RBNode α)
  (h_1 : (x : RBTree.RBNode α) → motive RBTree.RBNode.nil x) (h_2 : (x : RBTree.RBNode α) → motive x RBTree.RBNode.nil)
  (h_3 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.red c y d))
  (h_4 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.black a x b) (RBTree.RBNode.node RBTree.RBColor.black c y d))
  (h_5 :
    (a l : RBTree.RBNode α) →
      (v : α) →
        (r : RBTree.RBNode α) →
          a = RBTree.RBNode.node RBTree.RBColor.black l v r →
            (b : RBTree.RBNode α) →
              (x : α) →
                (c : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.black l v r) (RBTree.RBNode.node RBTree.RBColor.red b x c))
  (h_6 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c l : RBTree.RBNode α) →
          (v : α) →
            (r : RBTree.RBNode α) →
              c = RBTree.RBNode.node RBTree.RBColor.black l v r →
                motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.black l v r)),
  (x = RBTree.RBNode.nil → False) →
    (match x, RBTree.RBNode.nil with
      | RBTree.RBNode.nil, x => h_1 x
      | x, RBTree.RBNode.nil => h_2 x
      | RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.red c y d => h_3 a x b c y d
      | RBTree.RBNode.node RBTree.RBColor.black a x b, RBTree.RBNode.node RBTree.RBColor.black c y d => h_4 a x b c y d
      | a@h:(RBTree.RBNode.node RBTree.RBColor.black l v r), RBTree.RBNode.node RBTree.RBColor.red b x c =>
        h_5 a l v r h b x c
      | RBTree.RBNode.node RBTree.RBColor.red a x b, c@h:(RBTree.RBNode.node RBTree.RBColor.black l v r) =>
        h_6 a x b c l v r h) =
      h_2 x
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.isEmptyRingEquiv.congr_simp : ∀ (R : Type u) (σ : Type u_1) [inst : CommSemiring R] [inst_1 : IsEmpty σ],
  MvPolynomial.isEmptyRingEquiv R σ = MvPolynomial.isEmptyRingEquiv R σ
-- Mathlib.Topology.Order.LeftRightNhds
/-- The set of points which are isolated on the left is countable when the space is
second-countable.  -/
countable_setOfPred_isolated_left : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α],
  {x | nhdsWithin x (Set.Iio x) = ⊥}.Countable
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.minEntryD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {fallback : α × β}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minEntryD fallback = t₂.minEntryD fallback
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.comap_id : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X), DiscreteQuotient.comap (ContinuousMap.id X) S = S
-- Mathlib.Topology.Algebra.ConstMulAction
continuous_const_vadd_iff : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G]
  [inst_2 : AddAction G α] [ContinuousConstVAdd G α] [inst_4 : TopologicalSpace β] {f : β → α} (c : G),
  (Continuous fun x => c +ᵥ f x) ↔ Continuous f
-- Mathlib.GroupTheory.ArchimedeanDensely
mulEquivOfOrderOfEq.congr_simp : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] {g g_1 : G} (e_g : g = g_1)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' g'_1 : G'} (e_g' : g' = g'_1) (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g')
  (h : orderOf g = orderOf g'), mulEquivOfOrderOfEq hg hg' h = mulEquivOfOrderOfEq ⋯ ⋯ ⋯
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- Construct an element of the monoid algebra `R[M]`
from its coefficients `M →₀ R`.  -/
MonoidAlgebra.ofCoeff : {R : Type u_8} → {M : Type u_9} → [inst : Semiring R] → (M →₀ R) → MonoidAlgebra R M
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h₂.homologyIso.hom
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ioi_sub_one_eq_Ici_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {a : α},
  ¬IsMin a → Set.Ioi (a - 1) = Set.Ici a
-- Mathlib.Algebra.Category.Ring.Topology
CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_fst : ∀ (σ : Type v) (R A : CommRingCat) [inst : TopologicalSpace ↑R] [inst_1 : IsTopologicalRing ↑R]
  (f : CommRingCat.of (MvPolynomial σ ↑A) ⟶ R),
  ((CommRingCat.HomTopology.mvPolynomialHomeomorph σ R A) f).1 =
    CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom MvPolynomial.C) f
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.uniqueOfRight : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {M : Type u_8} →
      {M₂ : Type u_10} →
        [inst : Semiring R₁] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R₁ M] →
                  [inst_5 : Module R₂ M₂] → {σ₁₂ : R₁ →+* R₂} → [Subsingleton M₂] → Unique (M →ₛₗ[σ₁₂] M₂)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.aestronglyMeasurable_restrict_uIoc : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b → MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b))
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.commaFromOver_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (K : CategoryTheory.Functor J (CategoryTheory.Over X)),
  (CategoryTheory.WithTerminal.commaFromOver.obj K).left = K.comp (CategoryTheory.Over.forget X)
-- Mathlib.Analysis.Normed.Lp.ProdLp
IsometryEquiv.coe_withLpUniqueProd : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] [inst_2 : Unique α], ⇑(IsometryEquiv.withLpUniqueProd p α β) = WithLp.snd
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.vaddAssocClass' : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] [inst_2 : VAdd S R]
  [inst_3 : VAdd S M] [inst_4 : VAddAssocClass S R M] (p : SubAddAction R M) {S' : Type u_1} [inst_5 : VAdd S' R]
  [inst_6 : VAdd S' S] [inst_7 : VAdd S' M] [inst_8 : VAddAssocClass S' R M] [VAddAssocClass S' S M],
  VAddAssocClass S' S ↥p
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.IsAcc.mono : ∀ {o : Ordinal.{u_1}} {S T : Set Ordinal.{u_1}}, S ⊆ T → o.IsAcc S → o.IsAcc T
-- Mathlib.Order.SuccPred.Limit
Order.isPredLimitRecOn_pred : ∀ {α : Type u_1} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : PredOrder α]
  (isMax : (a : α) → IsMax a → motive a) (pred : (a : α) → ¬IsMin a → motive (Order.pred a))
  (isPredLimit : (a : α) → Order.IsPredLimit a → motive a) [inst_2 : NoMinOrder α] (b : α),
  Order.isPredLimitRecOn (Order.pred b) isMax pred isPredLimit = pred b ⋯
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.mkGrindParams : Lean.Grind.Config →
  Bool →
    Lean.TSyntaxArray `Lean.Parser.Tactic.grindParam →
      Lean.MVarId →
        optParam (Option Lean.Meta.Grind.ExtensionStateArray) none → Lean.Elab.TermElabM Lean.Meta.Grind.Params
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.cramer_transpose_row_self : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  (i : n), A.transpose.cramer (A i) = Pi.single i A.det
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback fallback' : α}, t.getD (t.maxD fallback) fallback' = t.maxD fallback
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t.toArray ↔ k ∈ t
-- Mathlib.Order.LiminfLimsup
/-- A version of `liminf_le_iff` with large inequalities in densely ordered spaces.  -/
Filter.liminf_le_iff' : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β}
  [DenselyOrdered β] {x : β},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.liminf_le_iff'._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.liminf_le_iff'._auto_3 →
      (Filter.liminf u f ≤ x ↔ ∀ y > x, ∃ᶠ (a : α) in f, u a ≤ y)
-- Mathlib.Topology.Algebra.Monoid
/-- Let `M` be a topological space with a continuous multiplication operation and a `0`.
Let `l` be a filter on `M × M` which is disjoint from the cocompact filter. Then, the multiplication
map `M × M → M` tends to zero on `(𝓝 0).coprod (𝓝 0) ⊓ l`.  -/
tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : MulZeroClass M] [ContinuousMul M] {l : Filter (M × M)},
  Disjoint l (Filter.cocompact (M × M)) → Filter.Tendsto (fun x => x.1 * x.2) ((nhds 0).coprod (nhds 0) ⊓ l) (nhds 0)
-- Lean.Environment
/-- Mapping from constant name to `ConstantInfo`. It contains all constants (definitions, theorems,
axioms, etc) that have been already type checked by the kernel.
 -/
Lean.Environment.constants : Lean.Environment → Lean.ConstMap