mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterWeightsUnnorm_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S), (s.restrict S hS).excenterWeightsUnnorm = s.excenterWeightsUnnorm
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.append_assoc : ∀ {V : Type u} {G : SimpleGraph V} {u v w x : V} (p : G.Walk u v) (q : G.Walk v w) (r : G.Walk w x),
  p.append (q.append r) = (p.append q).append r
-- Mathlib.Analysis.Complex.Circle
Circle.star_addChar : ∀ {e : AddChar ℝ Circle} (x : ℝ), star ↑(e x) = ↑(e (-x))
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι_ι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))
      (AlgebraicGeometry.IsAffineOpen.fromSpec ⋯)
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.comap_id : ∀ {X : Type u_1} {Z : Type u_3} [inst : TopologicalSpace X], LocallyConstant.comap (ContinuousMap.id X) = id
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coord_apply_combination_of_notMem : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) {s : Finset ι} {i : ι},
  i ∉ s → ∀ {w : ι → k}, s.sum w = 1 → (b.coord i) ((Finset.affineCombination k s ⇑b) w) = 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_smul : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] [StarModule ℝ A] {r : NNReal} {a : A},
  (r • a)⁻ = r • a⁻
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne_eq_image : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.normAtAllPlaces '' NumberField.mixedEmbedding.fundamentalCone.normLeOne K =
    ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis '' NumberField.mixedEmbedding.fundamentalCone.paramSet K
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- The module structure is inherited as the pullback under the additive group monomorphism
`DoubleCentralizer.toProd : 𝓜(𝕜, A) →+ (A →L[𝕜] A) × (A →L[𝕜] A)`  -/
DoubleCentralizer.instModule : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] →
            [inst_4 : IsScalarTower 𝕜 A A] →
              {S : Type u_3} →
                [inst_5 : Semiring S] →
                  [inst_6 : Module S A] →
                    [SMulCommClass 𝕜 S A] →
                      [ContinuousConstSMul S A] →
                        [IsScalarTower S A A] → [SMulCommClass S A A] → Module S (DoubleCentralizer 𝕜 A)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_of_isEmpty : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] [IsEmpty α] (f : α → ε) (p : ENNReal), MeasureTheory.eLpNorm f p μ = 0
-- Mathlib.Data.Set.Basic
Set.sep_or : ∀ {α : Type u} {s : Set α} {p q : α → Prop}, {x | x ∈ s ∧ (p x ∨ q x)} = {x | x ∈ s ∧ p x} ∪ {x | x ∈ s ∧ q x}
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RiiSlice : Type u_1 → Type u_2 → Type (max u_2 u_1)
-- Mathlib.CategoryTheory.Shift.Localization
/-- Auxiliary definition for `Functor.commShiftOfLocalization`.  -/
CategoryTheory.Functor.commShiftOfLocalization.iso : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (L : CategoryTheory.Functor C D) →
              (W : CategoryTheory.MorphismProperty C) →
                [L.IsLocalization W] →
                  {A : Type w} →
                    [inst_4 : AddMonoid A] →
                      [inst_5 : CategoryTheory.HasShift C A] →
                        (F : CategoryTheory.Functor C E) →
                          (F' : CategoryTheory.Functor D E) →
                            [CategoryTheory.Localization.Lifting L W F F'] →
                              [inst_7 : CategoryTheory.HasShift D A] →
                                [inst_8 : CategoryTheory.HasShift E A] →
                                  [L.CommShift A] →
                                    [F.CommShift A] →
                                      (a : A) →
                                        (CategoryTheory.shiftFunctor D a).comp F' ≅
                                          F'.comp (CategoryTheory.shiftFunctor E a)
-- Mathlib.Order.Filter.Map
Filter.mem_comap' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {s : Set α},
  s ∈ Filter.comap f l ↔ {y | ∀ ⦃x : α⦄, f x = y → x ∈ s} ∈ l
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.addSubgroupOf_map_subtype : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G), AddSubgroup.map K.subtype (H.addSubgroupOf K) = H ⊓ K
-- Init.Data.UInt.Lemmas
USize.toUInt32_ofNatClamp_of_lt : ∀ {n : ℕ}, n < USize.size → (USize.ofNatClamp n).toUInt32 = UInt32.ofNat n
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.Precheck.Context.quotLCtx : Lean.Elab.Term.Quotation.Precheck.Context → Lean.NameSet
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∈ t₂ → (t₁ \ t₂)[k]! = default
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.IterM.Equiv.refl : ∀ {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : LawfulMonad m] {α : Type w}
  [inst_2 : Std.Iterator α m β] (it : Std.IterM m β), it.Equiv it
-- Mathlib.Data.Set.Function
Function.invFunOn_image_image_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : α → β) (s : Set α), Function.invFunOn f s '' f '' s ⊆ s
-- Mathlib.Tactic.Linarith.Frontend
_private.Mathlib.Tactic.Linarith.Frontend.0.Mathlib.Tactic.instEvalExprCertificateOracle.unsafe_1 : Lean.Expr → Lean.MetaM Mathlib.Tactic.Linarith.CertificateOracle
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.instCompleteLattice.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M],
  AddSubmonoid.instCompleteLattice =
    { le := fun x1 x2 => x1 ≤ x2, lt := fun x1 x2 => x1 < x2, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
      le_antisymm := ⋯, sup := SemilatticeSup.sup, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯,
      inf := fun x1 x2 => x1 ⊓ x2, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯,
      toSupSet := (completeLatticeOfInf (AddSubmonoid M) ⋯).toSupSet, isLUB_sSup := ⋯,
      toInfSet := AddSubmonoid.instInfSet, isGLB_sInf := ⋯, toTop := AddSubmonoid.instTop, le_top := ⋯,
      toBot := AddSubmonoid.instBot, bot_le := ⋯ }
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
OpenPartialHomeomorph.MDifferentiable.mfderiv_injective : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M M'},
  OpenPartialHomeomorph.MDifferentiable I I' e → ∀ {x : M}, x ∈ e.source → Function.Injective ⇑(mfderiv% ↑e x)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- In a metric space, the minimal edistance to a nonempty set is finite.  -/
Metric.infEDist_ne_top : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, s.Nonempty → Metric.infEDist x s ≠ ⊤
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.values.eq_1 : ∀ {α : Type u} {β : Type v} (m : Std.DHashMap.Raw α fun x => β),
  m.values = Std.DHashMap.Raw.Internal.foldRev (fun acc x v => v :: acc) [] m
-- Mathlib.CategoryTheory.Limits.Fubini
/-- A variant of the Fubini theorem for a functor `G : J × K ⥤ C`,
showing that $\lim_k \lim_j G(j,k) ≅ \lim_j \lim_k G(j,k)$.
 -/
CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (G : CategoryTheory.Functor (J × K) C) →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C] →
                [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J C] →
                  [inst_5 :
                      CategoryTheory.Limits.HasLimit
                        ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] →
                    CategoryTheory.Limits.limit
                        ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).comp
                          CategoryTheory.Limits.lim) ≅
                      CategoryTheory.Limits.limit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)
-- Lean.Data.Position
/-- The line numbers associated with the `positions` of the `FileMap`.
`fmap.getLine i` is the iᵗʰ entry of `#[1, 2, …, n-1, n-1]`
where `n` is the `size` of `positions`.  -/
Lean.FileMap.getLine : Lean.FileMap → ℕ → ℕ
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_le_iff_le_toReal : ∀ {a : ℝ} {b : ENNReal}, b ≠ ⊤ → (ENNReal.ofReal a ≤ b ↔ a ≤ b.toReal)
-- Lean.Server.FileWorker.SignatureHelp
_private.Lean.Server.FileWorker.SignatureHelp.0.Lean.Server.FileWorker.SignatureHelp.isPositionInLineComment : Lean.FileMap → String.Pos.Raw → Bool
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.comapMk'OrderIso.eq_1 : ∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [hn : N.Normal],
  QuotientAddGroup.comapMk'OrderIso N =
    { toFun := fun H' => ⟨AddSubgroup.comap (QuotientAddGroup.mk' N) H', ⋯⟩,
      invFun := fun H => AddSubgroup.map (QuotientAddGroup.mk' N) ↑H, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Lean.Environment
Lean.ImportM.Context.mk : Lean.Environment → Lean.Options → Lean.ImportM.Context
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.map_inl : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  (equiv : S.Equiv S') (n : N), equiv (S.inl n) = S'.inl n
-- Mathlib.Topology.Convenient.Category
/-- The property of objects of `TopCat` which is satisfied by `X`-generated spaces.  -/
TopCat.generatedBy : {ι : Type t} → (X : ι → Type u) → [(i : ι) → TopologicalSpace (X i)] → CategoryTheory.ObjectProperty TopCat
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.toCompletion_add : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (x y : v.Completion),
  (x + y).toCompletion = x.toCompletion + y.toCompletion
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.instIsOverHomSchemeIsoSpecSpec : ∀ {R : CommRingCat} {X : AlgebraicGeometry.Scheme} [inst : X.Over (AlgebraicGeometry.Spec R)]
  [inst_1 : AlgebraicGeometry.IsAffine X], AlgebraicGeometry.Scheme.Hom.IsOver X.isoSpec.hom (AlgebraicGeometry.Spec R)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.fst.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.mappingCone.fst φ =
    CochainComplex.HomComplex.Cocycle.mk
      (CochainComplex.HomComplex.Cochain.mk fun p q hpq => HomologicalComplex.homotopyCofiber.fstX φ p q hpq) 2
      CochainComplex.mappingCone.fst._proof_2 ⋯
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {D₁ : Type u_1} {D₂ : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D₁] [inst_3 : CategoryTheory.Category.{v_2, u_2} D₂]
  (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [inst_4 : L₁.IsLocalization W₁]
  [inst_5 : L₂.IsLocalization W₂] [Φ.IsRightDerivabilityStructure],
  CategoryTheory.TwoSquare.GuitartExact (CategoryTheory.CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom
-- Lean.MonadEnv
Lean.getAsyncConstInfo : {m : Type → Type} →
  [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → optParam Bool false → m Lean.AsyncConstantInfo
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_homothetyUnitsMulHom_apply_symm : ∀ {R : Type u_10} {V : Type u_11} {P : Type u_12} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : AddTorsor V P] (p : P) (t : Rˣ),
  ⇑((AffineEquiv.homothetyUnitsMulHom p) t).symm = ⇑(AffineMap.homothety p ↑t⁻¹)
-- Mathlib.Algebra.Field.Equiv
MulEquiv.isField : ∀ {A : Type u_1} {B : Type u_2} [inst : Semiring A] [inst_1 : Semiring B], IsField B → ∀ (e : A ≃* B), IsField A
-- Mathlib.Algebra.Algebra.Hom
AlgHom.mk.sizeOf_spec : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : SizeOf R] [inst_6 : SizeOf A] [inst_7 : SizeOf B]
  (toRingHom : A →+* B) (commutes' : ∀ (r : R), (↑↑toRingHom).toFun ((algebraMap R A) r) = (algebraMap R B) r),
  sizeOf { toRingHom := toRingHom, commutes' := commutes' } = 1 + sizeOf toRingHom
-- Mathlib.Algebra.Group.Units.Equiv
AddUnits.addLeft_bijective : ∀ {M : Type u_3} [inst : AddMonoid M] (a : AddUnits M), Function.Bijective fun x => ↑a + x
-- Mathlib.RingTheory.Artinian.Module
/-- In an Artinian ring, an element is a unit iff it is a non-zero-divisor.
See also `isUnit_iff_mem_nonZeroDivisors_of_finite`.  -/
IsArtinianRing.isUnit_iff_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : Ring R] [IsArtinianRing R] {a : R}, IsUnit a ↔ a ∈ nonZeroDivisors R
-- Mathlib.Analysis.Convex.Cone.Dual
ProperCone.dual_empty : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : ClosedIciTopology R] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : TopologicalSpace M] [inst_8 : AddCommGroup N] [inst_9 : Module R N] [inst_10 : TopologicalSpace N]
  {p : M →ₗ[R] N →ₗ[R] R} [inst_11 : p.IsContPerfPair], ProperCone.dual p ∅ = ⊤
-- Mathlib.Data.Matrix.Mul
Matrix.ext_iff_mulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype n] {A B : Matrix m n α},
  A = B ↔ ∀ (v : n → α), A.mulVec v = B.mulVec v
-- Init.Data.UInt.Bitwise
UInt64.and_le_left : ∀ {a b : UInt64}, a &&& b ≤ a
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.equivOp_symm_apply_coe : ∀ {M : Type u_2} [inst : Add M] (H : AddSubsemigroup M) (b : ↥H.op), ↑(H.equivOp.symm b) = AddOpposite.unop ↑b
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- Two semilinear maps `(M ⊗ N) ⊗ (P ⊗ Q) → P₂` which agree on all elements of the
form `(m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)` are equal.  -/
TensorProduct.ext_fourfold' : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P : Type u_9} {Q : Type u_10} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid P] [inst_5 : AddCommMonoid Q] [inst_6 : AddCommMonoid P₂] [inst_7 : Module R M]
  [inst_8 : Module R N] [inst_9 : Module R₂ P₂] [inst_10 : Module R P] [inst_11 : Module R Q]
  {φ ψ : TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) →ₛₗ[σ₁₂] P₂},
  (∀ (w : M) (x : N) (y : P) (z : Q), φ (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) = ψ (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z))) → φ = ψ
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.mem_weightedHomogeneousSubmodule : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M) (m : M)
  (p : MvPolynomial σ R), p ∈ MvPolynomial.weightedHomogeneousSubmodule R w m ↔ MvPolynomial.IsWeightedHomogeneous w p m
-- Init.Data.Iterators.Producers.Monadic.List
/-- The underlying state of a list iterator. Its contents are internal and should
not be used by downstream users of the library.
 -/
Std.Iterators.Types.ListIterator : Type w → Type w
-- Mathlib.SetTheory.Ordinal.Notation
ONote.omega0_le_oadd : ∀ (e : ONote) (n : ℕ+) (a : ONote), Ordinal.omega0 ^ e.repr ≤ (e.oadd n a).repr
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAtChain_startPos_endPos_iff : ∀ {pat : String} {s : String.Slice},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat s.startPos s.endPos ↔
    ∃ n, s.copy = String.join (List.replicate n pat)
-- Lean.Attributes
Lean.TagAttribute.attr : Lean.TagAttribute → Lean.AttributeImpl
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- Let `s` be a subset of `𝕜`-inner product space, and `K` a subspace. Then the `d`-dimensional
Hausdorff measure of the orthogonal projection of `s` onto `K` is less than or equal to the
`d`-dimensional Hausdorff measure of `s`.
 -/
MeasureTheory.hausdorffMeasure_orthogonalProjectionOnto_le : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (K : Submodule 𝕜 E) [inst_5 : K.HasOrthogonalProjection] (d : ℝ)
  (s : Set E),
  0 ≤ d →
    (MeasureTheory.Measure.hausdorffMeasure d) (⇑K.orthogonalProjectionOnto '' s) ≤
      (MeasureTheory.Measure.hausdorffMeasure d) s
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.instIsStandardSmoothOfRelativeDimensionOfNatNatOfSubsingleton : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Subsingleton S],
  Algebra.IsStandardSmoothOfRelativeDimension 0 R S
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.opEquiv_apply : ∀ {X : SSet} (x : X.op.N), SSet.N.opEquiv x = SSet.N.mk (SSet.opObjEquiv x.simplex) ⋯
-- Mathlib.Analysis.Analytic.Basic
AnalyticAt.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F) (x : E),
  AnalyticAt 𝕜 f x = ∃ p, HasFPowerSeriesAt f p x
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.ofMonComon_map_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.Mon (CategoryTheory.Comon C)} (f : X ⟶ Y),
  ((CategoryTheory.Bimon.ofMonComon C).map f).hom = (CategoryTheory.Comon.forget C).mapMon.map f
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pattern.BackwardSliceSearcher.endsWith.eq_1 : ∀ (pat s : String.Slice),
  String.Slice.Pattern.BackwardSliceSearcher.endsWith pat s =
    if h : pat.utf8ByteSize ≤ s.utf8ByteSize then
      let sStart := s.endPos.offset.unoffsetBy pat.rawEndPos;
      let patStart := pat.startPos.offset;
      have hs := ⋯;
      have hp := ⋯;
      String.Slice.Pattern.Internal.memcmpSlice s pat sStart patStart pat.rawEndPos hs hp
    else false
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function `g` is at each point `x` a limit of `f` to the left or to the right (or more
generally a cluster point of the values of `f` around `x`) then the variation of `g` is bounded
by that of `f`.  -/
_private.Mathlib.Topology.EMetricSpace.BoundedVariation.0.eVariationOn.eVariationOn_le_of_mapClusterPt : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f g : α → E} {s : Set α},
  (∀ x ∈ s, MapClusterPt (g x) (nhdsWithin x s) f) → eVariationOn g s ≤ eVariationOn f s
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instSup : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Max β] → Max (MeasureTheory.SimpleFunc α β)
-- Batteries.Data.List.Perm
List.mem_swap : ∀ {α : Type u_1} {xs : List α} (i j : ℕ) {a : α}, a ∈ xs.swap i j ↔ a ∈ xs
-- Init.Data.UInt.Lemmas
UInt32.toFin_val : ∀ (x : UInt32), ↑x.toFin = x.toNat
-- Mathlib.Algebra.Star.Unitary
val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe : ∀ {M : Type u_5} [inst : Monoid M] [inst_1 : StarMul M] (x : ↥(unitary M)),
  ↑(↑(unitarySubgroupUnitsEquiv.symm x))⁻¹ = star ↑x
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.memLp_two_iff_integrable_sq : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ → (MeasureTheory.MemLp f 2 μ ↔ MeasureTheory.Integrable (fun x => f x ^ 2) μ)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_of_get_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.LawfulEqCmp cmp] {k : α}
  {v : β k} {w : k ∈ t}, t.get k w = v → k ∈ t
-- Mathlib.Topology.Order.Basic
/-- A function that is order-theoretically both left- and right-continuous is continuous, assuming
the function is between conditionally complete linear orders with order topologies.  -/
Continuous.of_ordContinuous : ∀ {X : Type u_1} [inst : ConditionallyCompleteLinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X]
  {Y : Type u_2} [inst_3 : ConditionallyCompleteLinearOrder Y] [inst_4 : TopologicalSpace Y] [OrderTopology Y]
  {f : X → Y}, LeftOrdContinuous f → RightOrdContinuous f → Continuous f
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsColoop.eq_1 : ∀ {α : Type u_1} (M : Matroid α) (e : α), M.IsColoop e = M✶.IsLoop e
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ClientInfo.version? : Lean.Lsp.ClientInfo → Option String
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instSMulNatHom : {k : Type u} → {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → {A B : Rep.{w, u, v} k G} → SMul ℕ (A ⟶ B)
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainLength.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  LieAlgebra.IsKilling.chainLength α β = if hα : α.IsZero then 0 else ⋯.choose
-- Mathlib.Order.Minimal
image_antitone_setOfPred_maximal : ∀ {α : Type u_2} {β : Type u_3} {P : α → Prop} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  (∀ ⦃y x : α⦄, P y → P x → (f y ≤ f x ↔ x ≤ y)) →
    f '' {x | Maximal P x} = {x | Minimal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addY_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.addY P Q = P 1 ^ 2 * Q 2 * Q 1