mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The negative of a `C^n` function within a domain at a point is `C^n` within this domain at
this point.  -/
ContDiffWithinAt.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {n : WithTop ℕ∞} {s : Set E} {f : E → F}, ContDiffWithinAt 𝕜 n f s x → ContDiffWithinAt 𝕜 n (fun x => -f x) s x
-- Lean.Data.SMap
Lean.SMap.forM : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] →
        {m : Type u_1 → Type u_2} → [Monad m] → Lean.SMap α β → (α → β → m PUnit.{u_1 + 1}) → m PUnit.{u_1 + 1}
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- Eta-expanded form of `MeromorphicOn.logDeriv_zpow_eventuallyEq`

---

Away from a codiscrete subset of `U`, the logarithmic derivative of the `n`-th power of a
meromorphic function is `n` times the logarithmic derivative.
 -/
MeromorphicOn.logDeriv_fun_zpow_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {U : Set 𝕜},
  MeromorphicOn f U → ∀ (n : ℤ), (logDeriv fun i => f i ^ n) =ᶠ[Filter.codiscreteWithin U] fun i => n • logDeriv f i
-- Init.Data.SInt.Lemmas
ISize.toInt_toBitVec : ∀ (x : ISize), x.toBitVec.toInt = x.toInt
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
HasFDerivWithinAt.of_comp_of_isEmbedding : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {g' : E →L[𝕜] F}
  {f' : F →L[𝕜] G} {a : E} {s : Set E} {t : Set F},
  Filter.Tendsto g (nhdsWithin a s) (nhdsWithin (g a) t) →
    HasFDerivWithinAt f f' t (g a) →
      Topology.IsEmbedding ⇑f' →
        HasFDerivWithinAt h (f' ∘SL g') s a → f ∘ g =ᶠ[nhdsWithin a s] h → a ∈ s → HasFDerivWithinAt g g' s a
-- Mathlib.Data.Sum.Order
Sum.Lex.noMinOrder : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] [NoMinOrder α] [NoMinOrder β], NoMinOrder (α ⊕ₗ β)
-- Mathlib.Topology.Homotopy.Lifting
IsAddQuotientCoveringMap.unop_fundamentalGroupToMulOpposite_smul : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hp : IsAddQuotientCoveringMap p G) {x : X} {e : ↑(p ⁻¹' {x})}
  {γ : FundamentalGroup X x}, MulOpposite.unop ((hp.fundamentalGroupToMulOpposite e) γ) • ↑e = ↑(⋯.monodromy γ e)
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.Saturate.top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Coverage C} (X : C), K.Saturate X ⊤
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_erase_eq_of_not_compare_maxKey!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, t.erase k ≠ ∅ → ¬cmp k t.maxKey! = Ordering.eq → (t.erase k).maxKey! = t.maxKey!
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- The property of preserving terminal objects expressed in terms of `IsTerminal`.  -/
CategoryTheory.Limits.IsTerminal.isTerminalObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          (X : C) →
            [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] →
              CategoryTheory.Limits.IsTerminal X → CategoryTheory.Limits.IsTerminal (G.obj X)
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrtHom.eq_1 : NNReal.sqrtHom =
  { toFun := ⇑NNReal.sqrt, map_zero' := NNReal.sqrt_zero, map_one' := NNReal.sqrt_one, map_mul' := NNReal.sqrt_mul }
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.memLp_indicator_iff_restrict : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {s : Set α} {f : α → ε},
  MeasurableSet s → (MeasureTheory.MemLp (s.indicator f) p μ ↔ MeasureTheory.MemLp f p (μ.restrict s))
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.monotone_gen : ∀ {α : Type u} [inst : UniformSpace α], Monotone CauchyFilter.gen
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.instSMulCommClassMulOppositeAut : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  SMulCommClass P.Autᵐᵒᵖ R N
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_X : ∀ {R : Type u} {σ : Type u_1} {n : σ} [inst : CommSemiring R] [Nontrivial R],
  (MvPolynomial.X n).support = {fun₀ | n => 1}
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.numBound_casesOn_succ : ∀ (k₀ k : ℕ) (D : ℕ → ℕ) (n : ℕ),
  ChevalleyThm.MvPolynomialC.numBound k₀ (fun x => Nat.casesOn x k D) (n + 1) =
    ChevalleyThm.MvPolynomialC.numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n
-- Std.Do.PostCond
Std.Do.ExceptConds.imp.eq_3 : ∀ (ε : Type u) (ps_2 : Std.Do.PostShape) (x_2 y_2 : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps_2)),
  (x_2 →ₑ y_2) = (fun e => spred(x_2.1 e → y_2.1 e), x_2.2 →ₑ y_2.2)
-- Mathlib.Geometry.Euclidean.Incenter
/-- The unnormalized weights of the vertices in an affine combination that gives an excenter with
signs determined by the given set of indices (for the empty set, this is the incenter; for a
singleton set, this is the excenter opposite a vertex).  An excenter with those signs exists if
and only if the sum of these weights is nonzero (so the normalized weights sum to 1).  -/
Affine.Simplex.excenterWeightsUnnorm : {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 : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → Finset (Fin (n + 1)) → Fin (n + 1) → ℝ
-- Init.Grind.Lemmas
Lean.Grind.imp_eq_of_eq_false_left : ∀ {a b : Prop}, a = False → (a → b) = True
-- Init.Prelude
instLEBitVec : {w : ℕ} → LE (BitVec w)
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.ext_iff : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} {f g : B₁ →bᵢ B₂}, f = g ↔ ∀ (x : M₁), f x = g x
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
tangentMapWithin_eq_tangentMap : ∀ {𝕜 : 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'] {f : M → M'} {s : Set M}
  {p : TangentBundle I M},
  UniqueMDiffAt[s] p.proj → MDiffAt f p.proj → tangentMapWithin I I' f s p = tangentMap I I' f p
-- Mathlib.CategoryTheory.Sites.Point.Presheaf
CategoryTheory.GrothendieckTopology.pointBot_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] (X : C),
  (CategoryTheory.GrothendieckTopology.pointBot X).fiber =
    CategoryTheory.shrinkYoneda.{w, v, u}.flip.obj (Opposite.op X)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalStarRing.lift_apply : ∀ {ι : 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 : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : (i : ι) → StarRing (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [inst_8 : Nonempty ι] (P : Type u_7)
  [inst_9 : NonUnitalNonAssocSemiring P] [inst_10 : StarRing P] (g : (i : ι) → G i →⋆ₙ+* P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (z : DirectLimit G f),
  (DirectLimit.NonUnitalStarRing.lift G f P g Hg) z = DirectLimit.lift f (fun x1 x2 => (g x1) x2) ⋯ z
-- Mathlib.Data.Nat.Log
Nat.pow_log_le_self : ∀ (b : ℕ) {x : ℕ}, x ≠ 0 → b ^ Nat.log b x ≤ x
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.compact_supp : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  HasCompactSupport ⇑f
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.eball_prod_same`. -/
EMetric.ball_prod_same : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal),
  Metric.eball x r ×ˢ Metric.eball y r = Metric.eball (x, y) r
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instRepresentablyCoflatIndYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.RepresentablyCoflat CategoryTheory.Ind.yoneda
-- Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
/-- Whether a given piece of syntax represents a `decide` tactic call with the `native` option
enabled. This may have false negatives for `decide (config := {<options>})` syntax.  -/
_private.Mathlib.Tactic.Linter.DeprecatedSyntaxLinter.0.Mathlib.Linter.Style.isDecideNative : Lean.Syntax → Bool
-- Mathlib.Algebra.Order.GroupWithZero.Defs
lt_of_mul_lt_mul_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [PosMulReflectLT α],
  a * b < a * c → 0 ≤ a → b < c
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
/-- **Alias** of `_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.Nat.isSemilinearSet_sdiff`. -/
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.Nat.isSemilinearSet_diff : ∀ {ι : Type u_3} [Finite ι] {s₁ s₂ : Set (ι → ℕ)}, IsSemilinearSet s₁ → IsSemilinearSet s₂ → IsSemilinearSet (s₁ \ s₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.associator_inv_base_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂}
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A'''] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B''']
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''}
  {G''' : CategoryTheory.Functor C''' B'''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  (φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'')
  (φ'' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G''') (x : B),
  (φ.associator φ' φ'').inv.base.app x = CategoryTheory.CategoryStruct.id (φ''.base.obj (φ'.base.obj (φ.base.obj x)))
-- Batteries.Recycling.RBTree.Basic
/-- Inner loop of `forIn`.  -/
RBTree.RBNode.forIn.visit : {m : Type u_1 → Type u_2} →
  {α : Type u_3} → {σ : Type u_1} → [Monad m] → (α → σ → m (ForInStep σ)) → RBTree.RBNode α → σ → m (ForInStep σ)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_mono : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s t : Set A},
  s ⊆ t → Algebra.adjoin R s ≤ Algebra.adjoin R t
-- Init.Data.UInt.Basic
/-- Converts an `Int` to a `USize` by taking the (non-negative remainder of the division by `2 ^ numBits`.  -/
USize.ofInt : ℤ → USize
-- Mathlib.Tactic.NormNum.Core
/-- Erase a name marked as a `norm_num` attribute.

Check that it does in fact have the `norm_num` attribute by making sure it names a `NormNumExt`
found somewhere in the state's tree, and is not erased.
 -/
Mathlib.Meta.NormNum.NormNums.erase : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → Mathlib.Meta.NormNum.NormNums → Lean.Name → m Mathlib.Meta.NormNum.NormNums
-- Mathlib.RingTheory.Valuation.AlgebraInstances
ValuationSubring.instIsScalarTowerSubtypeMemValuationSubringWithZeroMultiplicativeInt : ∀ {K : Type u_1} [inst : Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_2) [inst_1 : Field L]
  [inst_2 : Algebra K L] (E : Type u_3) [inst_3 : Field E] [inst_4 : Algebra K E] [inst_5 : Algebra L E]
  [IsScalarTower K L E], IsScalarTower (↥v.valuationSubring) L E
-- Init.Data.Array.Perm
Array.swap_perm : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ} (h₁ : i < xs.size) (h₂ : j < xs.size), (xs.swap i j h₁ h₂).Perm xs
-- Mathlib.CategoryTheory.ObjectProperty.Small
_private.Mathlib.CategoryTheory.ObjectProperty.Small.0.CategoryTheory.ObjectProperty.instSmallMax.match_1.splitter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    {P Q : CategoryTheory.ObjectProperty C} →
      (motive : Subtype P ⊕ Subtype Q → Sort u_2) →
        (x : Subtype P ⊕ Subtype Q) →
          ((x : Subtype P) → motive (Sum.inl x)) → ((x : Subtype Q) → motive (Sum.inr x)) → motive x
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.map_eq_zero_iff : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R ≃+* S) {x : R}, f x = 0 ↔ x = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {f : α → β → Bool} {k : α} (h : t.WF),
  (Std.TreeMap.Raw.filter f t)[k]! = (t[k]?.pfilter fun x h' => f (t.getKey k ⋯) x).get!
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.fun_add : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : Add β] [ContinuousAdd β],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun i => f i + g i) μ
-- Mathlib.Analysis.Convex.Cone.Closure
ConvexCone.closure_eq : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] {E : Type u_2} [inst_2 : AddCommMonoid E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : SMul 𝕜 E] [inst_6 : ContinuousConstSMul 𝕜 E]
  {K L : ConvexCone 𝕜 E}, K.closure = L ↔ closure ↑K = ↑L
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The induced index map `E.I₁' → F.I₁'` from a refinement morphism `E ⟶ F`.  -/
CategoryTheory.PreOneHypercover.Hom.s₁' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} → {F : CategoryTheory.PreOneHypercover S} → E.Hom F → E.I₁' → F.I₁'
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.opFunctor_map : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y),
  (CategoryTheory.Comma.opFunctor L R).map f =
    Opposite.op { left := Opposite.op f.right, right := Opposite.op f.left, w := ⋯ }
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentChangeRegistrationOptions.documentSelector? : Lean.Lsp.TextDocumentChangeRegistrationOptions → Option Lean.Lsp.DocumentSelector
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Compositions of continuous linear maps with harmonic functions are harmonic.
 -/
InnerProductSpace.HarmonicOnNhd.comp_CLM : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {G : Type u_3}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace ℝ G] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicOnNhd f s → ∀ (l : F →L[ℝ] G), InnerProductSpace.HarmonicOnNhd (⇑l ∘ f) s
-- Lean.Parser.Term
Lean.Parser.Term.configItem.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.restrictScalars_apply : ∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : TopologicalSpace M] [inst_6 : LinearMap.CompatibleSMul M M R S]
  (f : M ≃L[S] M) (a : M), (ContinuousLinearEquiv.restrictScalars R f) a = f a
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.mk.sizeOf_spec : ∀ {β : Type u_4} [inst : SizeOf β] (filter : Filter (Finset β)), sizeOf { filter := filter } = 1 + sizeOf filter
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.mk : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E},
  ContDiffAt ℝ (↑k) f a →
    ((fun x => iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a) =O[nhds a] fun x => ‖x - a‖ ^ ↑α) →
      ContDiffPointwiseHolderAt k α f a
-- Mathlib.Topology.Maps.Strict.Basic
/-- The homeomorphism `Quotient (Setoid.ker f) ≃ₜ Set.range f` given by a strict map `f`.
This is the homeomorphism obtained from the first isomorphism theorem.  -/
Homeomorph.quotientKerEquivRange : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f : X → Y} → Topology.IsStrictMap f → Quotient (Setoid.ker f) ≃ₜ ↑(Set.range f)
-- Batteries.Data.Vector.Lemmas
Vector.get_tail : ∀ {α : Type u_1} {n : ℕ} (v : Vector α (n + 1)) (i : Fin n), v.tail.get i = v.get i.succ
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.pullback.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (f f_1 : X ⟶ Y), f = f_1 → CategoryTheory.Subobject.pullback f = CategoryTheory.Subobject.pullback f_1
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.IsSymm.transpose : ∀ {α : Type u_1} {n : Type u_3} {A : Matrix n n α}, A.IsSymm → A.transpose.IsSymm
-- Mathlib.Data.ENNReal.Inv
ENNReal.add_div : ∀ {a b c : ENNReal}, (a + b) / c = a / c + b / c
-- Mathlib.Tactic.Inhabit
/-- `evalInhabit` takes in the MVarId of the main goal, runs the core portion of the inhabit tactic,
and returns the resulting MVarId  -/
Lean.Elab.Tactic.evalInhabit : Lean.MVarId → Option Lean.Ident → Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.MVarId
-- Mathlib.GroupTheory.Congruence.Basic
/-- This version infers the surjectivity of the function from a MulEquiv function  -/
Con.comapQuotientEquivOfSurj_symm_mk' : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (c : Con M) (f : N ≃* M) (x : N),
  (c.comapQuotientEquivOfSurj ↑f ⋯).symm ⟦f x⟧ = ↑x
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
AlgebraicTopology.DoldKan.DegeneraciesVanish.comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {n : ℕ} {T : C} {f : X.obj (Opposite.op { len := n }) ⟶ T},
  AlgebraicTopology.DoldKan.DegeneraciesVanish f →
    ∀ {U : C} (g : T ⟶ U), AlgebraicTopology.DoldKan.DegeneraciesVanish (CategoryTheory.CategoryStruct.comp f g)
-- Lean.Parser.Syntax
Lean.Parser.Syntax.unicodeAtom.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- Repeated pointwise addition/subtraction (not the same as pointwise repeated
addition/subtraction!) of a `Finset`. See note [pointwise nat action].  -/
Finset.zsmul : {α : Type u_2} → [DecidableEq α] → [Zero α] → [Add α] → [Neg α] → SMul ℤ (Finset α)
-- Mathlib.Algebra.Ring.CharZero
/-- `Nat.cast` as an embedding into monoids of characteristic `0`.  -/
Nat.castEmbedding : {R : Type u_2} → [inst : AddMonoidWithOne R] → [CharZero R] → ℕ ↪ R
-- Mathlib.Algebra.Group.Defs
isLeftRegular_iff_isRegular : ∀ {G : Type u_1} [inst : CommMagma G] {a : G}, IsLeftRegular a ↔ IsRegular a
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.get.match_1.eq_1 : ∀ (motive : Substring.Raw → String.Pos.Raw → Sort u_1) (s : String) (b stopPos p : String.Pos.Raw)
  (h_1 : (s : String) → (b stopPos p : String.Pos.Raw) → motive { str := s, startPos := b, stopPos := stopPos } p),
  (match { str := s, startPos := b, stopPos := stopPos }, p with
    | { str := s, startPos := b, stopPos := stopPos }, p => h_1 s b stopPos p) =
    h_1 s b stopPos p
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.of_toArray_perm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.toArray.Perm t₂.toArray → t₁.Equiv t₂
-- Mathlib.MeasureTheory.OuterMeasure.OfAddContent
/-- Every `s ∈ C` for an `m : AddContent C` with `IsSetSemiring C` is Carathéodory measurable
with respect to the `inducedOuterMeasure` from `m`.  -/
MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure_of_mem : ∀ {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (m : MeasureTheory.AddContent ENNReal C)
  {s : Set α}, s ∈ C → (MeasureTheory.inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯).IsCaratheodory s
-- Init.Data.Ord.Basic
Ordering.isLE_eq_false : ∀ {o : Ordering}, o.isLE = false ↔ o = Ordering.gt
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.length_eq_zero : ∀ {α : Type u_1} {a : FreeAddMonoid α}, a.length = 0 ↔ a = 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
eq_one_of_mul_le_one_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : PartialOrder α] [MulLeftMono α] {a b : α},
  1 ≤ a → 1 ≤ b → a * b ≤ 1 → a = 1
-- Mathlib.LinearAlgebra.Dimension.RankNullity
LinearMap.lift_rank_comap_le : ∀ {R : Type u_1} {M : Type u} {M' : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
  [inst_3 : Module R M] [inst_4 : Module R M'] [HasRankNullity.{u, u_1} R] {f : M →ₗ[R] M'} (p : Submodule R M'),
  Cardinal.lift.{v, u} (Module.rank R ↥(Submodule.comap f p)) ≤
    Cardinal.lift.{u, v} (Module.rank R ↥p) + Cardinal.lift.{v, u} (Module.rank R ↥f.ker)
-- Mathlib.Data.ENNReal.Operations
ENNReal.top_mul_top : ⊤ * ⊤ = ⊤
-- Init.Data.List.Perm
/-- This theorem is a variant of `Perm.foldl_eq` defined in Mathlib which uses typeclasses rather
than the explicit `comm` argument.
 -/
List.Perm.foldl_eq' : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} {l₁ l₂ : List α},
  l₁.Perm l₂ →
    (∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z : β), f (f z x) y = f (f z y) x) →
      ∀ (init : β), List.foldl f init l₁ = List.foldl f init l₂
-- Init.Data.Option.Lemmas
Option.not_isNone : ∀ {α : Type u_1} (a : Option α), (!a.isNone) = a.isSome
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sign_excenterWeights_singleton_pos : ∀ {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) [n.AtLeastTwo]
  {i j : Fin (n + 1)}, i ≠ j → SignType.sign (s.excenterWeights {i} j) = 1