mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
/-- This is a functor `embedding F : Cᵒᵖ ⥤ ModuleCat (EmbeddingRing F)`. We have that `embedding F`
is faithful and preserves finite limits and colimits. Furthermore, `F ⋙ embedding F` is full.  -/
CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.embedding : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type v} →
      [inst_1 : CategoryTheory.SmallCategory D] →
        (F : CategoryTheory.Functor D Cᵒᵖ) →
          [inst_2 : CategoryTheory.Abelian C] →
            [inst_3 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] →
              CategoryTheory.Functor Cᵒᵖ
                (ModuleCat (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing F))
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.σ_denom : ∀ (g h : GL (Fin 2) ℝ) (z : ℂ),
  (UpperHalfPlane.σ g) (UpperHalfPlane.denom h z) = UpperHalfPlane.denom h ((UpperHalfPlane.σ g) z)
-- Mathlib.CategoryTheory.Grothendieck
/-- Composition of morphisms in the Grothendieck category.
 -/
CategoryTheory.Grothendieck.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {X Y Z : CategoryTheory.Grothendieck F} → X.Hom Y → Y.Hom Z → X.Hom Z
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_insert' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α},
  autoParam (BddAbove s) csSup_insert'._auto_1 → sSup (insert a s) = max a (sSup s)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ι_m : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j),
  CategoryTheory.CategoryStruct.comp c.ιSigmaHorn (f.m j) =
    CategoryTheory.CategoryStruct.comp c.horn.ι c.ιSigmaStdSimplex
-- Init.WF
Acc.below : {α : Sort u} → {r : α → α → Prop} → {motive : (a : α) → Acc r a → Prop} → {a : α} → Acc r a → Prop
-- Std.Internal.UV.System
/-- Gets the value of an environment variable.
 -/
Std.Internal.UV.System.osGetenv : String → IO (Option String)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k k' : α} {f : β → β} {hc : k' ∈ t.modify k f},
  (t.modify k f)[k'] = if heq : cmp k k' = Ordering.eq then f t[k] else t[k']
-- Mathlib.Topology.Algebra.ConstMulAction
instContinuousConstVAddOrderDual : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α],
  ContinuousConstVAdd M αᵒᵈ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : ℝ≥0 → ℝ≥0` is continuous on a compact set `s` and `a : X → A` is continuous at `x₀`, and
eventually `0 ≤ a x` and has spectrum contained in `s`, then `fun x ↦ cfc f (a x)` is continuous
at `x₀`.  -/
ContinuousAt.cfc_nnreal : ∀ {X : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [inst_10 : TopologicalSpace X] {s : Set NNReal},
  IsCompact s →
    ∀ (f : NNReal → NNReal) {a : X → A} {x₀ : X},
      ContinuousAt a x₀ →
        (∀ᶠ (x : X) in nhds x₀, spectrum NNReal (a x) ⊆ s) →
          (∀ᶠ (x : X) in nhds x₀, 0 ≤ a x) →
            autoParam (ContinuousOn f s) ContinuousAt.cfc_nnreal._auto_1 → ContinuousAt (fun x => cfc f (a x)) x₀
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Returns `true` if `e` is a constant for a `match`-expression congruence equation.  -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.isMatchCongrEqConst : Lean.Expr → Lean.CoreM Bool
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.zero : {α : Type u} → [Zero α] → Zero (WithTop α)
-- Mathlib.Data.DFinsupp.Order
DFinsupp.coe_inf : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → SemilatticeInf (α i)]
  (f g : Π₀ (i : ι), α i), ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_mul_left_image : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, ⋃ a ∈ s, (fun x => a * x) '' t = s * t
-- Lean.Parser.Module
_private.Lean.Parser.Module.0.Lean.Parser.mkErrorMessage.lastTrailing : Lean.Parser.SyntaxStack → Option Substring.Raw
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nsmul_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : AddMonoid α] [inst_1 : AddMonoid β] (s : Set α) (t : Set β) (n : ℕ),
  n • s ×ˢ t = (n • s) ×ˢ (n • t)
-- Mathlib.GroupTheory.Sylow
/-- If `H` is a subgroup of `G` of cardinality `p ^ n`,
then `H` is contained in a subgroup of cardinality `p ^ m`
if `n ≤ m` and `p ^ m` divides the cardinality of `G`  -/
Sylow.exists_subgroup_card_pow_prime_le : ∀ {G : Type u} [inst : Group G] [Finite G] (p : ℕ) {n m : ℕ} [_hp : Fact (Nat.Prime p)],
  p ^ m ∣ Nat.card G → ∀ (H : Subgroup G), Nat.card ↥H = p ^ n → n ≤ m → ∃ K, Nat.card ↥K = p ^ m ∧ H ≤ K
-- Init.Data.Nat.Lemmas
Nat.le_div_two_of_div_two_lt_sub : ∀ {a b : ℕ}, a / 2 < a - b → b ≤ a / 2
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Valuation.hasBasis_nhds : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_3 : TopologicalSpace R] (v : Valuation R Γ₀) [v.Compatible] [IsValuativeTopology R] (x : R),
  (nhds x).HasBasis (fun x => True) fun γ => {z | v.restrict (z - x) < ↑γ}
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.contains_ofList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α}, (Std.DHashMap.Raw.Const.ofList l).contains k = (List.map Prod.fst l).contains k
-- Batteries.Logic
/-- **Alias** of `congrFun`. -/
congr_fun : ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
-- Mathlib.Order.Defs.Unbundled
Std.Trichotomous.decide : ∀ {α : Sort u_1} {r : α → α → Prop} [inst : DecidableRel r] [Std.Trichotomous r],
  Std.Trichotomous fun a b => decide (r a b) = true
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.mem_normalizedFactors_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  [Subsingleton αˣ] {p x : α}, x ≠ 0 → (p ∈ UniqueFactorizationMonoid.normalizedFactors x ↔ Prime p ∧ p ∣ x)
-- Mathlib.Algebra.Module.Submodule.EqLocus
/-- A linear map version of `AddMonoidHom.eqLocusM`  -/
LinearMap.eqLocus : {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_3} →
      {M₂ : Type u_4} →
        [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₂} → (M →ₛₗ[τ₁₂] M₂) → (M →ₛₗ[τ₁₂] M₂) → Submodule R M
-- Mathlib.GroupTheory.Coset.Basic
QuotientAddGroup.orbit_eq_out_vadd : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (x : α ⧸ s),
  AddAction.orbitRel.Quotient.orbit x = Quotient.out x +ᵥ ↑s
-- Mathlib.Data.Finset.Sym
/-- If `a` does not belong to the finset `s`, then the `n`th symmetric power of `{a} ∪ s` is
in 1-1 correspondence with the disjoint union of the `n - i`th symmetric powers of `s`,
for `0 ≤ i ≤ n`.  -/
Finset.symInsertEquiv : {α : Type u_1} →
  {s : Finset α} →
    {a : α} → [inst : DecidableEq α] → {n : ℕ} → a ∉ s → ↥((insert a s).sym n) ≃ (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
-- Mathlib.Analysis.Real.Cardinality
Cardinal.cantorFunction_le : ∀ {c : ℝ} {f g : ℕ → Bool},
  0 ≤ c → c < 1 → (∀ (n : ℕ), f n = true → g n = true) → Cardinal.cantorFunction c f ≤ Cardinal.cantorFunction c g
-- Aesop.Tree.State
Aesop.Rapp.isUnprovableNoCache : Aesop.Rapp → BaseIO Bool
-- Mathlib.Data.Set.Basic
Set.union_subset_union_left : ∀ {α : Type u} {s₁ s₂ : Set α} (t : Set α), s₁ ⊆ s₂ → s₁ ∪ t ⊆ s₂ ∪ t
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.inj_right : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {φ : MvPolynomial σ R} {m n : ℕ},
  φ.IsHomogeneous m → φ.IsHomogeneous n → φ ≠ 0 → m = n
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.map_mem_bot : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α} {y : α},
  (∀ (x : α), x ≤ f x) → y ∈ ChainCompletePartialOrder.bot x f → f y ∈ ChainCompletePartialOrder.bot x f
-- Mathlib.Tactic.NormNum.NatSqrt
Mathlib.Meta.NormNum.nat_sqrt_helper : ∀ {x y r : ℕ}, y * y + r = x → r.ble (2 * y) = true → x.sqrt = y
-- Mathlib.Algebra.Order.Interval.Basic
/-- The length of an interval is its first component minus its second component. This measures the
accuracy of the approximation by an interval.  -/
NonemptyInterval.length : {α : Type u_2} → [AddCommGroup α] → [inst : PartialOrder α] → NonemptyInterval α → α
-- Mathlib.Probability.HasLaw
ProbabilityTheory.IndepFun.hasLaw_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {M : Type u_3} [inst : Monoid M]
  {mM : MeasurableSpace M} [MeasurableMul₂ M] {μ ν : MeasureTheory.Measure M} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] {X Y : Ω → M},
  ProbabilityTheory.HasLaw X μ P →
    ProbabilityTheory.HasLaw Y ν P → ProbabilityTheory.IndepFun X Y P → ProbabilityTheory.HasLaw (X * Y) (μ.mconv ν) P
-- Mathlib.Data.PFunctor.Univariate.Basic
/-- Applying `P` to an object of `Type`  -/
PFunctor.Obj : PFunctor.{uA, uB} → Type v → Type (max v uA uB)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_assoc : ∀ {R : Type u} [inst : Semiring R] {I J K : Ideal R}, I * J * K = I * (J * K)
-- Mathlib.Data.List.Induction
_private.Mathlib.Data.List.Induction.0.List.reverseRec.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match [] with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_1 ()
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.nonempty_antidiagonal : ∀ {M : Type u_2} [inst : Monoid M] [inst_1 : Finset.HasMulAntidiagonal M] (a : M),
  (Finset.HasMulAntidiagonal.mulAntidiagonal a).Nonempty
-- Mathlib.MeasureTheory.Measure.MeasuredSets
MeasureTheory.instSetLikeMeasuredSets : {α : Type u_1} → [mα : MeasurableSpace α] → {μ : MeasureTheory.Measure α} → SetLike (MeasureTheory.MeasuredSets μ) α
-- Mathlib.Topology.Sets.Compacts
/-- See Note [custom simps projection].  -/
TopologicalSpace.NonemptyCompacts.Simps.coe : {α : Type u_1} → [inst : TopologicalSpace α] → TopologicalSpace.NonemptyCompacts α → Set α
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.essSurj_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E]
  (e : C ≌ E), e.inverse.EssSurj
-- Mathlib.RingTheory.FinitePresentation
AlgHom.FinitePresentation.of_comp_finiteType : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : CommRing C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  (f : A →ₐ[R] B) {g : B →ₐ[R] C}, (g.comp f).FinitePresentation → f.FiniteType → g.FinitePresentation
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorAccess.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (next : α) (h_1 : Unit → motive none)
  (h_2 : (next : α) → motive (some next)),
  (match some next with
    | none => h_1 ()
    | some next => h_2 next) =
    h_2 next
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.setLIntegral_condDistrib_of_measurableSet : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {s : Set Ω},
  Measurable X →
    AEMeasurable Y μ →
      MeasurableSet s →
        ∀ {t : Set α},
          MeasurableSet t → ∫⁻ (a : α) in t, ((ProbabilityTheory.condDistrib Y X μ) (X a)) s ∂μ = μ (t ∩ Y ⁻¹' s)
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
/-- If `g` is an orientation reversing matrix with trace zero and `c ≠ 0`,
then its action on the upper half plane has a half-circle of fixed points.
In the hyperbolic geometry, this half-circle is a line.  -/
UpperHalfPlane.gl_smul_eq_self_iff_dist_eq : ∀ {g : GL (Fin 2) ℝ} {z : UpperHalfPlane},
  (↑g).det < 0 →
    (↑g).trace = 0 → ↑g 1 0 ≠ 0 → (g • z = z ↔ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) = √(-(↑g).det) / |↑g 1 0|)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.eq_of_eqOn_dense : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddMonoid M] {s : Set G},
  AddSubgroup.closure s = ⊤ → ∀ {f g : G →+ M}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.Functor.mapShortComplex_map_τ₃ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y),
  (F.mapShortComplex.map φ).τ₃ = F.map φ.τ₃
-- Mathlib.LinearAlgebra.Ray
SameRay.exists_pos_left : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x y : M}, SameRay R x y → x ≠ 0 → y ≠ 0 → ∃ r, 0 < r ∧ r • x = y
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
minpolyDiv_eq_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  ¬IsIntegral R x → minpolyDiv R x = 0
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.liftHom₂LeftUnitorInv : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (f : a ⟶ b) →
        [inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
          Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.leftUnitor f).inv
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.mapₐ_id : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I : Ideal A)
  [inst_3 : I.IsPrime], Ideal.ResidueField.mapₐ I I (AlgHom.id R A) ⋯ = AlgHom.id R I.ResidueField
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- Taking projective resolutions is functorial,
if considered with target the homotopy category
(`ℕ`-indexed chain complexes and chain maps up to homotopy).
 -/
CategoryTheory.projectiveResolutions : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [CategoryTheory.HasProjectiveResolutions C] → CategoryTheory.Functor C (HomotopyCategory C (ComplexShape.down ℕ))
-- Init.Data.Vector.Basic
Vector.cast.congr_simp : ∀ {n m : ℕ} {α : Type u_1} (h : n = m) (xs xs_1 : Vector α n), xs = xs_1 → Vector.cast h xs = Vector.cast h xs_1
-- Std.Internal.Do.Triple.Basic
Std.Internal.Do.Triple.entails_wp_of_post : ∀ {Pred EPred : Type u} {Prog : Type v} {Value : Type u} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] {x : Prog} {pre : Pred}
  {post post' : Value → Pred} {epost : EPred},
  ⦃ pre ⦄ x ⦃ post'; epost ⦄ →
    Lean.Order.PartialOrder.rel post' post → Lean.Order.PartialOrder.rel pre (Std.Internal.Do.wp x post epost)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt16.reduceOfNat : Lean.Meta.Simp.DSimproc
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.le_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {k : α}, (cmp k t.minKey!).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_const_add_id' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (c : 𝕜), (deriv fun x => c + x) = fun x => 1
-- Mathlib.Data.Semiquot
/-- Convert a `Trunc α` to a `Semiquot α`.  -/
Semiquot.ofTrunc : {α : Type u_1} → Trunc α → Semiquot α
-- Init.Data.UInt.Basic
/-- Negation of 64-bit unsigned integers, computed modulo `UInt64.size`.

`UInt64.neg a` is equivalent to `18_446_744_073_709_551_615 - a + 1`.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.neg : UInt64 → UInt64
-- Mathlib.Topology.Connected.LocallyPathConnected
isOpen_isPathConnected_basis : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] (x : X),
  (nhds x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsPathConnected s) id
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.least_ascending_central_series_length_eq_nilpotencyClass`.

---

The nilpotency class of a nilpotent `G` is equal to the smallest `n` for which an ascending
central series reaches `G` in its `n`-th term.  -/
least_ascending_central_series_length_eq_nilpotencyClass : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G], Nat.find ⋯ = Group.nilpotencyClass G
-- Mathlib.Topology.Order.IsLocallyClosed
isLocallyClosed_Icc : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} [inst_1 : Preorder X] [OrderClosedTopology X],
  IsLocallyClosed (Set.Icc a b)
-- Mathlib.Algebra.Order.Module.Defs
nonneg_of_smul_nonneg_of_pos_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulReflectLE α β], 0 ≤ a • b → 0 < a → 0 ≤ b
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.brecOn_2.eq : ∀ {motive_1 : Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u}
  {motive_2 : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u}
  {motive_3 : List (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u}
  {motive_4 : String × Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u}
  (t : List (String × Lean.Elab.ConfigEval.HandlerTrie✝))
  (F_1 : (t : Lean.Elab.ConfigEval.HandlerTrie✝) → Lean.Elab.ConfigEval.HandlerTrie.below✝ t → motive_1 t)
  (F_2 :
    (t : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝)) → Lean.Elab.ConfigEval.HandlerTrie.below_1✝ t → motive_2 t)
  (F_3 :
    (t : List (String × Lean.Elab.ConfigEval.HandlerTrie✝)) → Lean.Elab.ConfigEval.HandlerTrie.below_2✝ t → motive_3 t)
  (F_4 : (t : String × Lean.Elab.ConfigEval.HandlerTrie✝) → Lean.Elab.ConfigEval.HandlerTrie.below_3✝ t → motive_4 t),
  Lean.Elab.ConfigEval.HandlerTrie.brecOn_2✝ t F_1 F_2 F_3 F_4 =
    F_3 t (Lean.Elab.ConfigEval.HandlerTrie.brecOn_2.go✝ t F_1 F_2 F_3 F_4).2
-- Batteries.Data.Fin.Fold
Fin.dfoldlM_loop_eq : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : Monad m]
  (f : (i : Fin n) → α i.castSucc → m (α i.succ)) (x : α ⟨n, ⋯⟩), Fin.dfoldlM.loop n α f n ⋯ x = pure x
-- Lean.Meta.CoeAttr
/-- The coercion to a function type, see `CoeFun.coe`  -/
Lean.Meta.CoeFnType.coeFun : Lean.Meta.CoeFnType
-- Mathlib.Order.MinMax
/-- **Alias** of `max_right_comm`. -/
Max.right_comm : ∀ {α : Type u} [inst : LinearOrder α] (a b c : α), max (max a b) c = max (max a c) b
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_range_zero : ∀ {M : Type u_3} [inst : AddCommMonoid M] (f : ℕ → M), ∑ k ∈ Finset.range 0, f k = 0
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.of_cancel_le : ∀ (ctx : Nat.Internal.Linear.Context) (a b c d : Nat.Internal.Linear.Expr),
  a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly) →
    (Nat.Internal.Linear.Expr.denote ctx a ≤ Nat.Internal.Linear.Expr.denote ctx b) =
      (Nat.Internal.Linear.Expr.denote ctx c ≤ Nat.Internal.Linear.Expr.denote ctx d)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.findEntry?_some : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {x : α} {y : α × β} [Std.TransCmp cmp]
  {t : RBTree.RBMap α β cmp}, t.findEntry? x = some y ↔ y ∈ t.toList ∧ cmp x y.1 = Ordering.eq
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.vec2_dotProduct : ∀ {α : Type u} [inst : AddCommMonoid α] [inst_1 : Mul α] (v w : Fin 2 → α), v ⬝ᵥ w = v 0 * w 0 + v 1 * w 1
-- Init.Data.Int.Order
Int.neg_min_neg : ∀ (a b : ℤ), min (-a) (-b) = -max a b
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.const_mul : ∀ {A : Type u_7} [inst : NormedRing A] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → A},
  IntervalIntegrable f μ a b → ∀ (c : A), IntervalIntegrable (fun x => c * f x) μ a b
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.modifyNth.eq_def : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (f : Γ → Γ) (x : ℕ) (x_1 : Turing.ListBlank Γ),
  Turing.ListBlank.modifyNth f x x_1 =
    match x, x_1 with
    | 0, L => Turing.ListBlank.cons (f L.head) L.tail
    | n.succ, L => Turing.ListBlank.cons L.head (Turing.ListBlank.modifyNth f n L.tail)
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `⊤ \ a` is `￢a`  -/
CompleteDistribLattice.top_sdiff : ∀ {α : Type u_1} [self : CompleteDistribLattice α] (a : α), ⊤ \ a = ￢a
-- Mathlib.Topology.Closure
frontier_univ : ∀ {X : Type u} [inst : TopologicalSpace X], frontier Set.univ = ∅
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_33 : HSub Std.Time.Day.Offset Std.Time.Minute.Offset Std.Time.Minute.Offset
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsUpper.mk : ∀ {α : Type u_3} [t : TopologicalSpace α] [inst : Preorder α], t = Topology.upper α → Topology.IsUpper α
-- Mathlib.Order.Circular
btw_rfl_left_right : ∀ {α : Type u_1} [inst : CircularOrder α] {a b : α}, btw a b a
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- Eta-expanded form of `MeasureTheory.integrable_zero` -/
MeasureTheory.integrable_fun_zero : ∀ (α : Type u_1) {m : MeasurableSpace α} (ε' : Type u_8) [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε']
  (μ : MeasureTheory.Measure α), MeasureTheory.Integrable (fun x => 0) μ
-- Lean.Server.Requests
Lean.Server.registerPartialStatefulLspRequestHandler : String →
  String →
    ℕ →
      (paramType : Type) →
        [Lean.FromJson paramType] →
          [Lean.Lsp.FileSource paramType] →
            (respType : Type) →
              [Lean.ToJson respType] →
                (stateType : Type) →
                  [TypeName stateType] →
                    stateType →
                      (paramType → stateType → Lean.Server.RequestM (Lean.Server.LspResponse respType × stateType)) →
                        (Lean.Lsp.DidChangeTextDocumentParams → StateT stateType Lean.Server.RequestM Unit) → IO Unit
-- Mathlib.Tactic.Linter.Style
/-- Whether a syntax element is a `set_option` command, tactic or term:
Return the name of the option being set, if any.  -/
_private.Mathlib.Tactic.Linter.Style.0.Mathlib.Linter.Style.setOption.parseSetOption : Lean.Syntax → Option Lean.Name
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.Characteristic.mk : ∀ {A : Type u_4} [inst : AddGroup A] {H : AddSubgroup A},
  (∀ (ϕ : A ≃+ A), AddSubgroup.comap ϕ.toAddMonoidHom H = H) → H.Characteristic
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.instIsScalarTowerZModExtension : ∀ (k : Type u_1) [inst : Field k] [inst_1 : Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [inst_4 : NeZero n] [inst_5 : Algebra (ZMod p) k], IsScalarTower (ZMod p) k (FiniteField.Extension k p n)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- The `Key`s that have already been computed.

Sometimes, more than one `Key` ends up being computed in one go. This happens when
there are lambda binders (because it depends on the body whether the lambda key
should be indexed or not). In that case the remaining `Key`s are stored in `results`.
 -/
Lean.Meta.RefinedDiscrTree.LazyEntry.computedKeys : Lean.Meta.RefinedDiscrTree.LazyEntry → List Lean.Meta.RefinedDiscrTree.Key