mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- **Alias** of `EMetricSpace.ofRiemannianMetric`.

---

The emetric space structure associated to a Riemannian metric on a manifold. Designed
so that the topology is defeq to the original one.

This should only be used when constructing data in specific situations. To develop the theory,
one should rather assume that there is an already existing emetric space structure, which satisfies
additionally the predicate `IsRiemannianManifold I M`.  -/
EmetricSpace.ofRiemannianMetric : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_2} →
        [inst_2 : TopologicalSpace H] →
          (I : ModelWithCorners ℝ E H) →
            (M : Type u_3) →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] →
                  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] →
                    [inst_6 : IsManifold I 1 M] →
                      [IsContinuousRiemannianBundle E fun x => TangentSpace I x] → [T3Space M] → EMetricSpace M
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.coe_id : ∀ {X : AddSemigrp}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulOneClass α] [inst_4 : MulOneClass β] [inst_5 : MulOneClass γ] {g₁ g₂ : β →*o γ} {f : α →*o β},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Order.WithBot
WithTop.ofDual_le_ofDual_iff : ∀ {α : Type u_1} [inst : LE α] {x y : WithTop αᵒᵈ}, WithTop.ofDual y ≤ WithTop.ofDual x ↔ x ≤ y
-- Init.Omega.Constraint
Lean.Omega.Constraint.exact.eq_1 : ∀ (r : ℤ), Lean.Omega.Constraint.exact r = { lowerBound := some r, upperBound := some r }
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false → (Std.ExtTreeMap.ofList l cmp).getD k fallback = fallback
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.isIso_of_isLeftKanExtension : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ} [CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  (α : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) [L.IsLeftKanExtension α], CategoryTheory.IsIso α
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instCommSemigroup : {α : Type u_1} → [CommSemigroup α] → CommSemigroup αᵃᵒᵖ
-- Mathlib.Order.Bounds.Basic
lowerBounds_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ≤ a → lowerBounds (Set.Icc b a) = Set.Iic b
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.stmts₁.match_1.eq_5 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4) (Q : Turing.TM1.Stmt Γ Λ σ)
  (h_1 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.move a q → motive (Turing.TM1.Stmt.move a q))
  (h_2 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → Γ) →
        (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.write a q → motive (Turing.TM1.Stmt.write a q))
  (h_3 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.load a q → motive (Turing.TM1.Stmt.load a q))
  (h_4 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → Bool) →
        (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.branch a q₁ q₂ → motive (Turing.TM1.Stmt.branch a q₁ q₂))
  (h_5 : (Q : Turing.TM1.Stmt Γ Λ σ) → motive Q),
  (∀ (a : Turing.Dir) (q : Turing.TM1.Stmt Γ Λ σ), Q = Turing.TM1.Stmt.move a q → False) →
    (∀ (a : Γ → σ → Γ) (q : Turing.TM1.Stmt Γ Λ σ), Q = Turing.TM1.Stmt.write a q → False) →
      (∀ (a : Γ → σ → σ) (q : Turing.TM1.Stmt Γ Λ σ), Q = Turing.TM1.Stmt.load a q → False) →
        (∀ (a : Γ → σ → Bool) (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ), Q = Turing.TM1.Stmt.branch a q₁ q₂ → False) →
          (match Q with
            | Q@h:(Turing.TM1.Stmt.move a q) => h_1 Q a q h
            | Q@h:(Turing.TM1.Stmt.write a q) => h_2 Q a q h
            | Q@h:(Turing.TM1.Stmt.load a q) => h_3 Q a q h
            | Q@h:(Turing.TM1.Stmt.branch a q₁ q₂) => h_4 Q a q₁ q₂ h
            | Q => h_5 Q) =
            h_5 Q
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.map_star : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] [inst_3 : InvolutiveStar R]
  [inst_4 : StarRing A] [StarModule R A] (a : A), spectrum R (star a) = star (spectrum R a)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- If `C` holds for the `algebraMap` of `r : R` into `ExteriorAlgebra R M`, the `ι` of `x : M`,
and is preserved under addition and multiplication, then it holds for all of `ExteriorAlgebra R M`.
 -/
ExteriorAlgebra.induction : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {C : ExteriorAlgebra R M → Prop},
  (∀ (r : R), C ((algebraMap R (ExteriorAlgebra R M)) r)) →
    (∀ (x : M), C ((ExteriorAlgebra.ι R) x)) →
      (∀ (a b : ExteriorAlgebra R M), C a → C b → C (a * b)) →
        (∀ (a b : ExteriorAlgebra R M), C a → C b → C (a + b)) → ∀ (a : ExteriorAlgebra R M), C a
-- Mathlib.Condensed.Discrete.Colimit
/-- A presheaf, which takes a light profinite set written as a sequential limit to the corresponding
colimit, agrees with the left Kan extension of its restriction.
 -/
LightCondensed.lanPresheafIso : {S : LightProfinite} →
  {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} →
    CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)) →
      ((LightCondensed.lanPresheaf F).obj (Opposite.op S) ≅ F.obj (Opposite.op S))
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instSubsingletonOverTerminalScheme : ∀ {X : AlgebraicGeometry.Scheme}, Subsingleton (X.Over (⊤_ AlgebraicGeometry.Scheme))
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opCoproductIsoProduct_hom_comp_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct Z] (i : α) {Z_1 : Cᵒᵖ} (h : Opposite.op (Z i) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct Z).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => Opposite.op (Z x)) i) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι Z i).op h
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.isHomLift_iff : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴) {R S : 𝒮} {a b : 𝒳.obj} (f : R ⟶ S)
  (φ : a ⟶ b), 𝒴.p.IsHomLift f (F.map φ) ↔ 𝒳.p.IsHomLift f φ
-- Mathlib.Algebra.Regular.Pi
Pi.isLeftRegular_iff : ∀ {ι : Type u_1} {R : ι → Type u_3} [inst : (i : ι) → Mul (R i)] {a : (i : ι) → R i},
  IsLeftRegular a ↔ ∀ (i : ι), IsLeftRegular (a i)
-- Init.Data.List.MinMaxIdx
List.le_minIdxOn_of_apply_getElem_lt_apply_getElem : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : ℕ} (hi : i < xs.length),
  (∀ (j : ℕ) (x : j < i), f xs[i] < f xs[j]) → i ≤ List.minIdxOn f xs h
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.mul_toMatrix : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (M : Matrix n n R₁),
  M * (LinearMap.BilinForm.toMatrix b) B =
    (LinearMap.BilinForm.toMatrix b) (B.compLeft ((Matrix.toLin b b) M.transpose))
-- Mathlib.Topology.Algebra.Module.Cardinality
/-- A nontrivial module over a complete nontrivially normed field has cardinality at least
continuum.  -/
continuum_le_cardinal_of_module : ∀ (𝕜 : Type u) (E : Type v) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E] [Module 𝕜 E]
  [Nontrivial E], Cardinal.continuum ≤ Cardinal.mk E
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- `Polynomial.eval₂` as an `AlgHom` for noncommutative algebras.

This is `Polynomial.eval₂RingHom'` for `AlgHom`s.  -/
Polynomial.eval₂AlgHom : {R : Type u} →
  {A : Type z} →
    {B : Type u_2} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] → (f : A →ₐ[R] B) → (b : B) → (∀ (a : A), Commute (f a) b) → Polynomial A →ₐ[R] B
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_iInf₂ : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {κ : Sort u_4}
  {κ' : κ → Sort u_5} (s : (i : κ) → κ' i → HomogeneousIdeal 𝒜), (⨅ i, ⨅ j, s i j).toIdeal = ⨅ i, ⨅ j, (s i j).toIdeal
-- Init.Data.Range.Polymorphic.Lemmas
Std.PRange.UpwardEnumerable.exists_of_succ_lt : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LT (Std.PRange.succ a) b →
    ∃ b', b = Std.PRange.succ b' ∧ Std.PRange.UpwardEnumerable.LT a b'
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.sum_of_iIndepFun : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ},
  ProbabilityTheory.iIndepFun X μ →
    ∀ {c : ι → NNReal} {s : Finset ι},
      (∀ i ∈ s, ProbabilityTheory.HasSubgaussianMGF (X i) (c i) μ) →
        ProbabilityTheory.HasSubgaussianMGF (fun ω => ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.mk₀_addEquiv₀_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (f : CategoryTheory.Abelian.Ext X Y 0),
  CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.Abelian.Ext.addEquiv₀ f) = f
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_prod_of_regular : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {ι : Type u_3} {P : ι → MvPolynomial σ R}
  {s : Finset ι},
  (∀ i ∈ s, IsRegular (m.leadingCoeff (P i))) → m.leadingCoeff (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)
-- Mathlib.Algebra.Divisibility.Units
isRelPrime_one_right : ∀ {α : Type u_1} [inst : CommMonoid α] {x : α}, IsRelPrime x 1
-- Mathlib.Topology.Order.OrderClosed
le_of_tendsto' : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] {f : β → α}
  {a b : α} {x : Filter β} [hx : x.NeBot], Filter.Tendsto f x (nhds a) → (∀ (c : β), f c ≤ b) → a ≤ b
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_diff_le_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  (t₁ \ t₂).size ≤ t₁.size
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.downMulHom : (G : Type u) → [inst : Mul G] → ULift.{u_1, u} G →ₙ* G
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.EditableDocumentCore.mk.inj : ∀ {«meta» : Lean.Server.DocumentMeta} {initSnap : Lean.Language.Lean.InitialSnapshot}
  {cmdSnaps : Lean.AsyncList IO.Error Lean.Server.Snapshots.Snapshot}
  {diagnosticsMutex : Std.Mutex Lean.Server.FileWorker.DiagnosticsState} {meta_1 : Lean.Server.DocumentMeta}
  {initSnap_1 : Lean.Language.Lean.InitialSnapshot}
  {cmdSnaps_1 : Lean.AsyncList IO.Error Lean.Server.Snapshots.Snapshot}
  {diagnosticsMutex_1 : Std.Mutex Lean.Server.FileWorker.DiagnosticsState},
  { «meta» := «meta», initSnap := initSnap, cmdSnaps := cmdSnaps, diagnosticsMutex := diagnosticsMutex } =
      { «meta» := meta_1, initSnap := initSnap_1, cmdSnaps := cmdSnaps_1, diagnosticsMutex := diagnosticsMutex_1 } →
    «meta» = meta_1 ∧ initSnap = initSnap_1 ∧ cmdSnaps = cmdSnaps_1 ∧ diagnosticsMutex = diagnosticsMutex_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
nonpos_of_add_le_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddLeftReflectLE α] {a b : α}, a + b ≤ a → b ≤ 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, (m₁ \ m₂).getKey! k = if k ∈ m₂ then default else m₁.getKey! k
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β} {f : β → β},
  (m.modify k f).getD k fallback = (Option.map f m[k]?).getD fallback
-- Mathlib.Order.Category.Frm
Frm.hasForgetToLat : CategoryTheory.HasForget₂ Frm Lat
-- Mathlib.Order.Partition.Basic
Partition.IsRepFun.idem : ∀ {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α} {a : α}, P.IsRepFun f → f (f a) = f a
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.basis_repr : ∀ {R : Type u_1} [inst : Semiring R] {n : ℕ} (i : Fin n) (P : ↥(Polynomial.degreeLT R n)),
  ((Polynomial.degreeLT.basis R n).repr P) i = (↑P).coeff ↑i
-- Mathlib.Analysis.Normed.Group.Indicator
norm_indicator_eq_indicator_norm : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedAddGroup E] {s : Set α} (f : α → E) (a : α),
  ‖s.indicator f a‖ = s.indicator (fun a => ‖f a‖) a
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.minimalCover.eq_1 : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (A : Set X),
  Metric.minimalCover ε A = if h : Metric.coveringNumber ε A ≠ ⊤ then ⋯.choose else ∅
-- Init.Data.Vector.Lemmas
Vector.toList_ofFn : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → α}, (Vector.ofFn f).toList = List.ofFn f
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
/-- Continuity at a point can be read under right composition with an open partial homeomorphism, if
the point is in its target  -/
OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_right : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Y → Z} {x : Y},
  x ∈ e.target → (ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x))
-- Mathlib.Topology.Covering.Quotient
/-- A quotient covering map `f` induces a permutation action on each fiber.  -/
IsQuotientCoveringMap.toPermFiber : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {f : E → X} →
          {G : Type u_3} →
            [inst_2 : Group G] →
              [inst_3 : MulAction G E] → IsQuotientCoveringMap f G → (x : X) → G →* Equiv.Perm ↑(f ⁻¹' {x})
-- Mathlib.LinearAlgebra.Transvection.Generation
LinearEquiv.finrank_fixedSubmodule_mul_dilatransvection_le : ∀ {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 f : V ≃ₗ[K] V),
  f ∈ LinearEquiv.dilatransvections K V →
    Module.finrank K ↥(↑(e * f)).fixedSubmodule ≤ 1 + Module.finrank K ↥(↑e).fixedSubmodule
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.coe_injective : ∀ {α : Type u_2} {ι : Type u_3} [Nontrivial α], Function.Injective Combinatorics.Line.toFun
-- Lean.Elab.InfoTree.Main
_private.Lean.Elab.InfoTree.Main.0.Lean.Elab.formatElabInfo : Lean.Elab.ContextInfo → Lean.Elab.ElabInfo → Std.Format
-- Lean.DocString.Formatter
Lean.Doc.Parser.document.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Logic.Equiv.Fintype
/-- If two sets have the same finite cardinality, their set differences are equivalent.  -/
Equiv.setDiffEquiv : {α : Type u_1} →
  {s t : Set α} → [inst : Fintype ↑s] → [inst_1 : Fintype ↑t] → Fintype.card ↑s = Fintype.card ↑t → ↑(s \ t) ≃ ↑(t \ s)
-- Mathlib.Analysis.SpecialFunctions.Exp
ContinuousAt.cexp : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℂ} {x : α},
  ContinuousAt f x → ContinuousAt (fun y => Complex.exp (f y)) x
-- Lean.Elab.Exception
Lean.Elab.abortTermExceptionId : Lean.InternalExceptionId
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.congr_symm_apply_of : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] {G' : ι → Type u_5} [inst_5 : (i : ι) → AddCommMonoid (G' i)]
  [inst_6 : (i : ι) → Module R (G' i)] {f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j} (e : (i : ι) → G i ≃ₗ[R] G' i)
  (he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)) {i : ι} (g : G' i),
  (Module.DirectLimit.congr e he).symm ((Module.DirectLimit.of R ι G' f' i) g) =
    (Module.DirectLimit.of R ι G f i) ((e i).symm g)
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.leftDeriv_mul_log : ∀ {x : ℝ}, x ≠ 0 → derivWithin (fun x => x * Real.log x) (Set.Iio x) x = Real.log x + 1
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.mk.inj : ∀ {H : Type u} {inst : NormedAddCommGroup H} {inst_1 : InnerProductSpace ℂ H} {inst_2 : CompleteSpace H}
  {toStarSubalgebra : StarSubalgebra ℂ (H →L[ℂ] H)}
  {centralizer_centralizer' : toStarSubalgebra.carrier.centralizer.centralizer = toStarSubalgebra.carrier}
  {toStarSubalgebra_1 : StarSubalgebra ℂ (H →L[ℂ] H)}
  {centralizer_centralizer'_1 : toStarSubalgebra_1.carrier.centralizer.centralizer = toStarSubalgebra_1.carrier},
  { toStarSubalgebra := toStarSubalgebra, centralizer_centralizer' := centralizer_centralizer' } =
      { toStarSubalgebra := toStarSubalgebra_1, centralizer_centralizer' := centralizer_centralizer'_1 } →
    toStarSubalgebra = toStarSubalgebra_1
-- Init.Data.SInt.Lemmas
Int64.zero_sub : ∀ (a : Int64), 0 - a = -a
-- Mathlib.RingTheory.Polynomial.SeparableDegree
Polynomial.HasSeparableContraction.dvd_degree' : ∀ {F : Type u_1} [inst : CommSemiring F] {q : ℕ} {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f),
  ∃ m, hf.degree * q ^ m = f.natDegree
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `ContDiff.smul`

---

The scalar multiplication of two `C^n` functions is `C^n`.  -/
ContDiff.fun_smul : ∀ {𝕜 : 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] {n : WithTop ℕ∞}
  {𝕜' : Type u_3} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F] [IsBoundedSMul 𝕜' F]
  [IsScalarTower 𝕜 𝕜' F] {f : E → 𝕜'} {g : E → F}, ContDiff 𝕜 n f → ContDiff 𝕜 n g → ContDiff 𝕜 n fun i => f i • g i
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
CategoryTheory.Functor.isDenseAt_iff : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : D},
  F.isDenseAt X ↔
    Nonempty
      (CategoryTheory.Limits.IsColimit
        ((CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.Functor.id D) F.rightUnitor.inv).coconeAt X))
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.min_const : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : α → ℝ} {Kf : NNReal},
  LipschitzWith Kf f → ∀ (a : ℝ), LipschitzWith Kf fun x => min (f x) a
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- A closed subset of a completely pseudometrizable space is also completely pseudometrizable.  -/
IsClosed.isCompletelyPseudoMetrizableSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace X] {s : Set X},
  IsClosed s → TopologicalSpace.IsCompletelyPseudoMetrizableSpace ↑s
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.exists_bucket' : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α]
  (self : Array (Std.DHashMap.Internal.AssocList α β)) (i : USize) (hi : i.toNat < self.size),
  ∃ l,
    (List.flatMap Std.DHashMap.Internal.AssocList.toList self.toList).Perm (self[i.toNat].toList ++ l) ∧
      ∀ [LawfulHashable α],
        Std.DHashMap.Internal.IsHashSelf self →
          ∀ (k : α),
            (↑(Std.DHashMap.Internal.mkIdx self.size ⋯ (hash k))).toNat = i.toNat →
              Std.Internal.List.containsKey k l = false
-- Mathlib.RingTheory.Flat.Stability
/-- If `M` is a flat `R`-module and `S` is any `R`-algebra, `S ⊗[R] M` is `S`-flat.  -/
Module.Flat.baseChange : ∀ (R : Type u) (S : Type v) (M : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [Module.Flat R M], Module.Flat S (TensorProduct R S M)
-- Mathlib.Data.PNat.Factors
PrimeMultiset.prod_sup : ∀ (u v : PrimeMultiset), (u ⊔ v).prod = u.prod.lcm v.prod
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_zero : ∀ {α : Type u_2} {_m0 : MeasurableSpace α} (s : Set α), MeasureTheory.Measure.restrict 0 s = 0
-- Mathlib.Order.RelIso.Set
Acc.of_subrel : ∀ {α : Type u_1} {r : α → α → Prop} [IsTrans α r] {b : α} (a : { a // r a b }),
  Acc (Subrel r fun x => r x b) a → Acc r ↑a
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Every manifold is a Fréchet space (T1 space) -- regardless of whether it is
Hausdorff.  -/
ModelWithCorners.t1Space : ∀ {𝕜 : 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 : TopologicalSpace M] [ChartedSpace H M], T1Space M
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.toMatrix_eigenvectorBasis : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n),
  (LinearMap.toMatrix (hT.eigenvectorBasis hn).toBasis (hT.eigenvectorBasis hn).toBasis) T =
    Matrix.diagonal (RCLike.ofReal ∘ hT.eigenvalues hn)
-- Init.Tactics
/-- `any_goals tac` applies the tactic `tac` to every goal,
concatenating the resulting goals for successful tactic applications.
If the tactic fails on all of the goals, the entire `any_goals` tactic fails.

This tactic is like `all_goals try tac` except that it fails if none of the applications of `tac` succeeds.
 -/
Lean.Parser.Tactic.anyGoals : Lean.ParserDescr
-- Mathlib.RingTheory.WittVector.MulCoeff
/-- This is the polynomial whose degree we want to get a handle on.  -/
WittVector.polyOfInterest : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Addneg-addneg-addneg version.  -/
Finset.ruzsa_triangle_inequality_addNeg_addNeg_addNeg : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] (A B C : Finset G),
  (A + -C).card * B.card ≤ (A + -B).card * (C + -B).card
-- Mathlib.Order.Defs.Unbundled
/-- The carrier of an `UpperSet` is an upper set.  -/
UpperSet.upper' : ∀ {α : Type u_1} [inst : LE α] (self : UpperSet α), IsUpperSet self.carrier
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.mem_mk : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {x : R} {c : RingCon R}, x ∈ TwoSidedIdeal.mk c ↔ c x 0
-- Lean.MetavarContext
/-- Information about a metavariable.  -/
Lean.MetavarDecl : Type