mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Graded
LieDerivation.ofGrading.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} {L : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid ι] [inst_2 : CommRing R]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ℒ : ι → Submodule R L) [inst_5 : GradedLieAlgebra ℒ] (φ : ι →+ R),
  LieDerivation.ofGrading ℒ φ =
    {
      toFun := fun x =>
        (DirectSum.decomposeLinearEquiv ℒ).symm
          ((LieDerivation.ofGradingSum ℒ φ) ((DirectSum.decomposeLinearEquiv ℒ) x)),
      map_add' := ⋯, map_smul' := ⋯, leibniz' := ⋯ }
-- Mathlib.Algebra.Opposites
AddOpposite.instZero.eq_1 : ∀ {α : Type u_1} [inst : Zero α], AddOpposite.instZero = { zero := AddOpposite.op 0 }
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.mem_adjoin_range_iff : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Type u_3} (i : ι → E)
  (x : E), x ∈ IntermediateField.adjoin F (Set.range i) ↔ ∃ r s, x = (MvPolynomial.aeval i) r / (MvPolynomial.aeval i) s
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.nilpotencyLength_eq_one_iff : ∀ (L : Type v) (M : Type w) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] [Nontrivial M],
  LieModule.nilpotencyLength L M = 1 ↔ LieModule.IsTrivial L M
-- Init.SimpLemmas
instLawfulIdentityAndTrue : Std.LawfulIdentity And True
-- Init.Data.Array.Lemmas
Array.contains_empty : ∀ {α : Type u_1} {a : α} [inst : BEq α], #[].contains a = false
-- Lean.Meta.Basic
/-- Sort free variables using an order `x < y` iff `x` was defined before `y`.
If a free variable is not in the local context, we use their id.  -/
Lean.Meta.sortFVarIds : Array Lean.FVarId → Lean.MetaM (Array Lean.FVarId)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
IsLocalRing.isLocalHom_iff_comap_closedPoint : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : IsLocalRing R] {S : Type v} [inst_2 : CommSemiring S]
  [inst_3 : IsLocalRing S] (f : R →+* S),
  IsLocalHom f ↔ PrimeSpectrum.comap f (IsLocalRing.closedPoint S) = IsLocalRing.closedPoint R
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_s₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] (i : E.saturate.I₀), E.fromSaturateOfHasPullbacks.s₀ i = i
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Construct a morphism to the multiequalizer from its universal property.  -/
CategoryTheory.Limits.Multiequalizer.lift : {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] →
          (W : C) →
            (k : (a : J.L) → W ⟶ I.left a) →
              (∀ (b : J.R),
                  CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) =
                    CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)) →
                (W ⟶ CategoryTheory.Limits.multiequalizer I)
-- Mathlib.Topology.UniformSpace.Compact
Filter.HasBasis.lebesgue_number_lemma_nhdsWithin : ∀ {α : Type ua} [inst : UniformSpace α] {K : Set α} {ι' : Sort u_2} {p : ι' → Prop} {V : ι' → Set (α × α)}
  {U : α → Set α},
  (uniformity α).HasBasis p V →
    IsCompact K → (∀ x ∈ K, U x ∈ nhdsWithin x K) → ∃ i, p i ∧ ∀ x ∈ K, ∃ y, UniformSpace.ball x (V i) ∩ K ⊆ U y
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.cases.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (cases cases_1 : Lean.Compiler.LCNF.Cases pu),
  (Lean.Compiler.LCNF.Code.cases cases = Lean.Compiler.LCNF.Code.cases cases_1) = (cases = cases_1)
-- Mathlib.RingTheory.WittVector.WittPolynomial
map_wittPolynomial : ∀ (p : ℕ) {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (f : R →+* S) (n : ℕ),
  (MvPolynomial.map f) (wittPolynomial p R n) = wittPolynomial p S n
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- The pullback commutes with the Lie bracket of vector fields on manifolds.  -/
VectorField.mpullbackWithin_mlieBracketWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] [IsManifold I (minSmoothness 𝕜 2) M]
  [inst_12 : IsManifold I' (minSmoothness 𝕜 2) M'] [CompleteSpace E] {n : WithTop ℕ∞} {f : M → M'}
  {V W : (x : M') → TangentSpace I' x} {x₀ : M} {s : Set M} {t : Set M'},
  MDiffAt[t] (T% V) (f x₀) →
    MDiffAt[t] (T% W) (f x₀) →
      UniqueMDiff[s] →
        ContMDiffWithinAt I I' n f s x₀ →
          x₀ ∈ s →
            minSmoothness 𝕜 2 ≤ n →
              f ⁻¹' t ∈ nhdsWithin x₀ s →
                x₀ ∈ closure (interior s) →
                  VectorField.mpullbackWithin I I' f (VectorField.mlieBracketWithin I' V W t) s x₀ =
                    VectorField.mlieBracketWithin I (VectorField.mpullbackWithin I I' f V s)
                      (VectorField.mpullbackWithin I I' f W s) s x₀
-- Lean.Parser.Command
Lean.Parser.Command.in : Lean.Parser.TrailingParser
-- Mathlib.Topology.LocalAtTarget
/-- **Alias** of `Set.restrictPreimage_isEmbedding`. -/
Topology.IsEmbedding.restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} (s : Set β),
  Topology.IsEmbedding f → Topology.IsEmbedding (s.restrictPreimage f)
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.instSubcanonicalProetaleTopology : AlgebraicGeometry.Scheme.proetaleTopology.Subcanonical
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.isLocallyInjective_toPlus : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  (P : CategoryTheory.Functor Cᵒᵖ (Type (max u v))), CategoryTheory.Presheaf.IsLocallyInjective J (J.toPlus P)
-- Init.Data.List.Sublist
List.drop_sublist_drop_left : ∀ {α : Type u_1} (l : List α) {i j : ℕ}, i ≤ j → (List.drop j l).Sublist (List.drop i l)
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.getCurrMacroScope : Lean.Elab.Tactic.TacticM Lean.MacroScope
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_of_contains_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  {f : (a : α) → β a → Option (γ a)} {k : α}, (Std.DTreeMap.filterMap f t).contains k = true → t.contains k = true
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.ctorAlt : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.CtorInfo →
    Lean.Compiler.LCNF.Code pu →
      autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_3 → Lean.Compiler.LCNF.Alt pu
-- Mathlib.Topology.ContinuousMap.Polynomial
Polynomial.toContinuousMapAlgHom_apply : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R]
  (p : Polynomial R), Polynomial.toContinuousMapAlgHom p = p.toContinuousMap
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- In order to define a natural isomorphism `F ≅ G` with `F G : FreeGroupoid ⥤ D`,
it suffices to do so after precomposing with `FreeGroupoid.of C`.  -/
CategoryTheory.FreeGroupoid.liftNatIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : Type u₁} →
      [inst_1 : CategoryTheory.Groupoid G] →
        (F₁ F₂ : CategoryTheory.Functor (CategoryTheory.FreeGroupoid C) G) →
          ((CategoryTheory.FreeGroupoid.of C).comp F₁ ≅ (CategoryTheory.FreeGroupoid.of C).comp F₂) → (F₁ ≅ F₂)
-- Mathlib.Topology.Path
Path.exists_congr : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₁ x₂ y₁ y₂ : X} {p : Path x₁ y₁ → Prop} (hx : x₁ = x₂) (hy : y₁ = y₂),
  (∃ γ, p γ) ↔ ∃ γ, p (γ.cast hx hy)
-- Aesop.Search.Expansion.Norm
Aesop.withNormTraceNode : Aesop.DisplayRuleName → Aesop.NormM (Option Aesop.NormRuleResult) → Aesop.NormM (Option Aesop.NormRuleResult)
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedUserInfo.default : Std.Http.URI.UserInfo
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.nonZeroDivisorsLeft_eq_isUnitSubmonoid : ∀ (R : Type u_1) [inst : Ring R] [IsArtinianRing Rᵐᵒᵖ], IsUnit.submonoid R = nonZeroDivisorsLeft R
-- Mathlib.LinearAlgebra.Transvection.Generation
_private.Mathlib.LinearAlgebra.Transvection.Generation.0.LinearEquiv.auxTransvection_mul_fixed : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] {e : V ≃ₗ[K] V} {f : Module.Dual K V} {u : V}
  {hf : (↑e).fixedSubmodule ⊔ K ∙ (e u - u) ≤ LinearMap.ker f},
  f u = 1 → (↑(LinearEquiv.auxTransvection✝ hf * e)).fixedSubmodule = (↑e).fixedSubmodule ⊔ K ∙ u
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.associator_map_inr : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {X Y : E} (f : X ⟶ Y),
  (CategoryTheory.sum.associator C D E).map ((CategoryTheory.Sum.inr_ (C ⊕ D) E).map f) =
    (CategoryTheory.Sum.inr_ C (D ⊕ E)).map ((CategoryTheory.Sum.inr_ D E).map f)
-- Mathlib.Algebra.Category.BialgCat.Monoidal
BialgCat.instMonoidalCategory : (R : Type u) → [inst : CommRing R] → CategoryTheory.MonoidalCategory (BialgCat R)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- A subgraph is called a *spanning subgraph* if it contains all the vertices of `G`.  -/
SimpleGraph.Subgraph.IsSpanning : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → Prop
-- Mathlib.Analysis.Calculus.MeanValue
/-- A function on `[a, b]` with the norm of the derivative within `[a, b]`
bounded by `C` satisfies `‖f x - f a‖ ≤ C * (x - a)`, `HasDerivWithinAt`
version.  -/
norm_image_sub_le_of_norm_deriv_le_segment' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E} {C : ℝ},
  (∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) →
    (∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ C) → ∀ x ∈ Set.Icc a b, ‖f x - f a‖ ≤ C * (x - a)
-- Mathlib.Order.Hom.Lattice
LatticeHom.coe_id : ∀ (α : Type u_2) [inst : Lattice α], ⇑(LatticeHom.id α) = id
-- Mathlib.Order.Defs.PartialOrder
le_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → a ≤ b
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
_private.Mathlib.Topology.UniformSpace.UniformConvergenceTopology.0.UniformOnFun.«term𝒱(_,_,_,_)» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Defs
IsAddCommutative.instAddCommMonoid.eq_1 : ∀ {M : Type u_2} [inst : AddMonoid M] [inst_1 : IsAddCommutative M],
  IsAddCommutative.instAddCommMonoid = { toAddMonoid := inst, add_comm := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.instHasPushoutOppositeOpOfHasPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [CategoryTheory.Limits.HasPullback f g], CategoryTheory.Limits.HasPushout f.op g.op
-- Mathlib.RingTheory.FinitePresentation
/-- An algebra over a commutative semiring is `Algebra.FinitePresentation` if it is the quotient of
a polynomial ring in `n` variables by a finitely generated ideal.  -/
Algebra.FinitePresentation : (R : Type w₁) → (A : Type w₂) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Prop
-- Mathlib.Data.Seq.Computation
/-- `corec f b` is the corecursor for `Computation α` as a coinductive type.
If `f b = inl a` then `corec f b = pure a`, and if `f b = inl b'` then
`corec f b = think (corec f b')`.  -/
Computation.corec : {α : Type u} → {β : Type v} → (β → α ⊕ β) → β → Computation α
-- Init.Data.Nat.Lemmas
Nat.lt_one_add_iff : ∀ {m n : ℕ}, m < 1 + n ↔ m ≤ n
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ZeroExtend
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorExtendTargetBlastZeroExtend : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.ExtendTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend
-- Mathlib.Analysis.Normed.Group.Basic
SeminormedAddGroup.induced.eq_1 : ∀ {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [inst : FunLike 𝓕 E F] [inst_1 : AddGroup E]
  [inst_2 : SeminormedAddGroup F] [inst_3 : AddMonoidHomClass 𝓕 E F] (f : 𝓕),
  SeminormedAddGroup.induced E F f =
    { norm := fun a => ‖f a‖, toAddGroup := inst_1, dist := fun a a_1 => dist (f a) (f a_1), dist_self := ⋯,
      dist_comm := ⋯, dist_triangle := ⋯, edist := fun a a_1 => PseudoMetricSpace.edist (f a) (f a_1), edist_dist := ⋯,
      toUniformSpace :=
        { toTopologicalSpace := TopologicalSpace.induced (⇑f) PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
          uniformity := Filter.comap (fun p => (f p.1, f p.2)) (uniformity F), symm := ⋯, comp := ⋯,
          nhds_eq_comap_uniformity := ⋯ },
      uniformity_dist := ⋯, toBornology := { cobounded := Filter.comap (⇑f) (Bornology.cobounded F), le_cofinite := ⋯ },
      cobounded_sets := ⋯, dist_eq := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.IsConnected.nonempty : ∀ {X : SSet} [self : X.IsConnected], X.Nonempty
-- Mathlib.Topology.Compactification.OnePoint.Basic
_private.Mathlib.Topology.Compactification.OnePoint.Basic.0.instReprOnePoint.match_1.eq_1 : ∀ {X : Type u_1} (motive : OnePoint X → Sort u_2) (h_1 : Unit → motive none) (h_2 : (a : X) → motive (some a)),
  (match none with
    | none => h_1 ()
    | some a => h_2 a) =
    h_1 ()
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.Legacy.findAux.eq_def : ∀ (s : String) (p : Char → Bool) (stopPos pos : String.Pos.Raw),
  String.Legacy.findAux s p stopPos pos =
    if h : pos < stopPos then
      if p (String.Pos.Raw.get s pos) = true then pos
      else
        have this := ⋯;
        String.Legacy.findAux s p stopPos (String.Pos.Raw.next s pos)
    else pos
-- Mathlib.Geometry.Diffeology.Basic
/-- Every locally smooth map `EuclideanSpace ℝ (Fin n) → X` is a plot.  -/
DiffeologicalSpace.locality : ∀ {X : Type u_1} [self : DiffeologicalSpace X] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
  (∀ (x : EuclideanSpace ℝ (Fin n)),
      ∃ u,
        IsOpen u ∧
          x ∈ u ∧
            ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
              (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ (↑⊤) f → p ∘ f ∈ DiffeologicalSpace.plots m) →
    p ∈ DiffeologicalSpace.plots n
-- Init.Data.Option.Lemmas
Option.merge_some_some : ∀ {α : Type u_1} {f : α → α → α} {a b : α}, Option.merge f (some a) (some b) = some (f a b)
-- Lean.Elab.Command
Lean.Elab.Command.ModuleLinter.mk.sizeOf_spec : ∀ (run : Array Lean.Syntax → Lean.Elab.Command.CommandElabM Unit)
  (name : autoParam Lean.Name Lean.Elab.Command.ModuleLinter.name._autoParam),
  sizeOf { run := run, name := name } = 1 + sizeOf name
-- Mathlib.GroupTheory.Perm.ViaEmbedding
Equiv.Perm.viaEmbeddingHom_injective : ∀ {α : Type u_1} {β : Type u_2} (ι : α ↪ β), Function.Injective ⇑(Equiv.Perm.viaEmbeddingHom ι)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.splitToList.eq_1 : ∀ (s : String) (p : Char → Bool), s.splitToList p = s.splitAux p 0 0 []
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.zero'.sizeOf_spec : sizeOf Turing.ToPartrec.Code.zero' = 1
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le_coe_unzeroD : ∀ {α : Type u_1} [inst : Preorder α] (x : WithZero α) (b : α), x ≤ ↑(WithZero.unzeroD b x)
-- Mathlib.Topology.Constructible
/-- [Stacks Tag 005J](https://stacks.math.columbia.edu/tag/005J) (Extracted from the proof) -/
IsRetrocompact.preimage_of_isOpenEmbedding : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  Topology.IsOpenEmbedding f → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_inf_distrib_left : ∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] [inst_1 : OrderBot α] (s : Finset ι) (f : ι → α) (a : α),
  a ⊓ s.sup f = s.sup fun i => a ⊓ f i
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.colimitsOfShape_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [W.IsStableUnderColimitsOfShape J], W.colimitsOfShape J ≤ W
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.mk : {A : Type u_1} →
  {E : Type u_2} →
    [inst : NonUnitalSemiring A] →
      [inst_1 : StarRing A] →
        [inst_2 : Module ℂ A] →
          [inst_3 : AddCommGroup E] →
            [inst_4 : Module ℂ E] →
              [inst_5 : PartialOrder A] →
                [inst_6 : SMul A E] →
                  [inst_7 : Norm A] →
                    [inst_8 : Norm E] →
                      [toInner : Inner A E] →
                        (∀ {x y z : E}, inner A x (y + z) = inner A x y + inner A x z) →
                          (∀ {x : E}, 0 ≤ inner A x x) →
                            (∀ {x : E}, inner A x x = 0 ↔ x = 0) →
                              (∀ {a : A} {x y : E}, inner A x (a • y) = a * inner A x y) →
                                (∀ {z : ℂ} {x y : E}, inner A x (z • y) = z • inner A x y) →
                                  (∀ (x y : E), star (inner A x y) = inner A y x) →
                                    (∀ (x : E), ‖x‖ = √‖inner A x x‖) → CStarModule A E
-- Init.Data.UInt.Bitwise
UInt8.xor_not : ∀ {a b : UInt8}, a ^^^ ~~~b = ~~~(a ^^^ b)
-- Std.Internal.UV.TCP
/-- Tries to accept an incoming connection on a listening TCP socket.
 -/
Std.Internal.UV.TCP.Socket.tryAccept : Std.Internal.UV.TCP.Socket → IO (Except IO.Error (Option Std.Internal.UV.TCP.Socket))
-- Init.Data.List.Lemmas
List.contains_replicate : ∀ {α : Type u_1} [inst : BEq α] {n : ℕ} {a b : α}, (List.replicate n b).contains a = (a == b && !n == 0)
-- Mathlib.Data.ZMod.Basic
ZMod.isUnit_iff_coprime : ∀ (m n : ℕ), IsUnit ↑m ↔ m.Coprime n
-- Mathlib.Probability.Decision.Risk.Basic
/-- See `bayesRisk_le_iInf` for a simpler result when `P` is a Markov kernel.  -/
ProbabilityTheory.bayesRisk_le_iInf' : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal},
  Measurable (Function.uncurry ℓ) →
    ∀ (P : ProbabilityTheory.Kernel Θ 𝓧) (π : MeasureTheory.Measure Θ),
      ProbabilityTheory.bayesRisk ℓ P π ≤ ⨅ y, ∫⁻ (θ : Θ), ℓ θ y * (P θ) Set.univ ∂π
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.sheaf_eq_amalgamation : ∀ {D : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {A : Type u_4} [inst_1 : CategoryTheory.Category.{v_4, u_4} A] (ℱ : CategoryTheory.Sheaf K A) {X : A} {U : D}
  {T : CategoryTheory.Sieve U} (hT : T ∈ K U)
  (x : CategoryTheory.Presieve.FamilyOfElements (ℱ.obj.comp (CategoryTheory.coyoneda.obj (Opposite.op X))) T.arrows)
  (hx : x.Compatible) (t : (ℱ.obj.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).obj (Opposite.op U)),
  x.IsAmalgamation t → t = ⋯.amalgamate x hx
-- Init.Data.UInt.Lemmas
USize.ofNatClamp_uInt32ToNat : ∀ (n : UInt32), USize.ofNatClamp n.toNat = n.toUSize
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.getPendingMVarErrorMessage : Array Lean.Elab.DefView → Lean.MessageData
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddSemigroupOfAddHomClass.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → AddSemigroup (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)],
  DirectLimit.instAddSemigroupOfAddHomClass = { toAdd := DirectLimit.instAdd, add_assoc := ⋯ }
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Two linear isometric equivalences are equal if they are equal on basis vectors.  -/
Module.Basis.ext_linearIsometryEquiv : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  {ι : Type u_11} (b : Module.Basis ι R E) {f₁ f₂ : E ≃ₛₗᵢ[σ₁₂] E₂}, (∀ (i : ι), f₁ (b i) = f₂ (b i)) → f₁ = f₂
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.sub_int_iff : ∀ {p x : ℝ} {m : ℤ}, LiouvilleWith p (x - ↑m) ↔ LiouvilleWith p x
-- Mathlib.Data.ENat.BigOperators
ENat.iInf_sum : ∀ {ι : Type u_2} {α : Type u_3} {f : ι → α → ℕ∞} {s : Finset α} [Nonempty ι],
  (∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a) → ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.RelCWComplex.finite_of_finiteDimensional_finiteType : ∀ {X : Type u_1} [inst : TopologicalSpace X] (C : Set X) {D : Set X} [inst_1 : Topology.RelCWComplex C D]
  [Topology.RelCWComplex.FiniteDimensional C] [Topology.RelCWComplex.FiniteType C], Topology.RelCWComplex.Finite C
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.mem_closure_singleton_self : ∀ {M : Type u_1} [inst : Monoid M] {y : M}, y ∈ Submonoid.closure {y}
-- Mathlib.Algebra.Group.Submonoid.Membership
VAddCommClass.of_mclosure_eq_top : ∀ {M : Type u_1} {N : Type u_4} {α : Type u_5} [inst : AddMonoid M] [inst_1 : VAdd N α] [inst_2 : AddAction M α]
  {s : Set M},
  AddSubmonoid.closure s = ⊤ → (∀ x ∈ s, ∀ (y : N) (z : α), x +ᵥ y +ᵥ z = y +ᵥ x +ᵥ z) → VAddCommClass M N α
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.primeHeight_le_ringKrullDim : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} [inst_1 : I.IsPrime], ↑(Ideal.primeHeight✝ I) ≤ ringKrullDim R
-- Mathlib.Control.Traversable.Basic
/-- `traverse` plays well with composition of applicative functors.  -/
LawfulTraversable.comp_traverse : ∀ {t : Type u → Type u} {inst : Traversable t} [self : LawfulTraversable t] {F G : Type u → Type u}
  [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α β γ : Type u}
  (f : β → F γ) (g : α → G β) (x : t α),
  traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field K] [inst_1 : CharZero K]
  [inst_2 : DecidableEq ι] [inst_3 : Fintype ι] [inst_4 : AddCommGroup M] [inst_5 : Module K M]
  [inst_6 : AddCommGroup N] [inst_7 : Module K N] {P : RootPairing ι K M N} [inst_8 : P.IsCrystallographic]
  {b : P.Base},
  ↑(LieModule.genWeightSpace (↥b.support ⊕ ι → K) 0) = Submodule.span K (Set.range RootPairing.GeckConstruction.u)
-- Mathlib.Data.Rel.Separated
SetRel.isSeparated_insert : ∀ {X : Type u_1} {R : SetRel X X} {s : Set X} {x : X} [R.IsSymm],
  R.IsSeparated (insert x s) ↔ R.IsSeparated s ∧ ∀ y ∈ s, (x, y) ∈ R → x = y
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.toArray_keys_eq_keysArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β), (↑m).keys.toArray = (↑m).keysArray
-- Init.Data.Bool
Bool.default_bool : default = false
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.left_C : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P), c.left.C = c.C
-- Batteries.Data.List.Lemmas
List.getElem_idxsOf_lt : ∀ {α : Type u_1} {i : ℕ} {xs : List α} {x : α} {s : ℕ} [inst : BEq α] (h : i < (List.idxsOf x xs s).length),
  (List.idxsOf x xs s)[i] < xs.length + s