mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (H : X ≅ Y),
  (AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso H).inv =
    TopCat.Presheaf.pushforwardToOfIso ((AlgebraicGeometry.PresheafedSpace.forget C).mapIso H).symm H.inv.c
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.coe_ideal_span_singleton_mul_inv : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {x : R₁}, x ≠ 0 → ↑(Ideal.span {x}) * (↑(Ideal.span {x}))⁻¹ = 1
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.hom_id : ∀ (R : Type u) [inst : CommRing R] {A : AlgCat R}, AlgCat.Hom.hom (CategoryTheory.CategoryStruct.id A) = AlgHom.id R ↑A
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.mk.inj : ∀ {M : Type u_1} {inst : AddZeroClass M} {toAddSubmonoid : AddSubmonoid M} {addSaturated : toAddSubmonoid.AddSaturated}
  {toAddSubmonoid_1 : AddSubmonoid M} {addSaturated_1 : toAddSubmonoid_1.AddSaturated},
  { toAddSubmonoid := toAddSubmonoid, addSaturated := addSaturated } =
      { toAddSubmonoid := toAddSubmonoid_1, addSaturated := addSaturated_1 } →
    toAddSubmonoid = toAddSubmonoid_1
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.hasShift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {β : Type u_1} →
      [inst_1 : AddCommGroup β] → (s : β) → CategoryTheory.HasShift (CategoryTheory.GradedObjectWithShift s C) ℤ
-- Mathlib.CategoryTheory.IsConnected
/-- If there is a zigzag from `j₁` to `j₂`, then there is a zigzag from `F j₁` to
`F j₂` as long as `F` is a functor.
 -/
CategoryTheory.zigzag_obj_of_zigzag : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J K) {j₁ j₂ : J},
  CategoryTheory.Zigzag j₁ j₂ → CategoryTheory.Zigzag (F.obj j₁) (F.obj j₂)
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.mulConst_mul_card : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G), A.mulConst B * ↑A.card = ↑(A * B).card
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
/-- Given an object `Y : Karoubi (SimplicialObject C)`, this lemma
computes `PInfty` for the associated object in `SimplicialObject (Karoubi C)`
in terms of `PInfty` for `Y.X : SimplicialObject C` and `Y.p`.  -/
AlgebraicTopology.DoldKan.karoubi_PInfty_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {Y : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)} (n : ℕ),
  (AlgebraicTopology.DoldKan.PInfty.f n).f =
    CategoryTheory.CategoryStruct.comp (Y.p.app (Opposite.op { len := n })) (AlgebraicTopology.DoldKan.PInfty.f n)
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.mk : Option Lean.Elab.ConfigEval.EvalConfigItemHandler →
  Array (String × Lean.Elab.ConfigEval.HandlerTrie✝) →
    Option Lean.Elab.ConfigEval.EvalConfigItemHandler →
      Option Lean.Name → Option Lean.Name → Lean.Elab.ConfigEval.HandlerTrie✝
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
mem_affineSpan_pair_iff_exists_lineMap_rev_eq : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p p₁ p₂ : P}, p ∈ line[k, p₁, p₂] ↔ ∃ r, (AffineMap.lineMap p₂ p₁) r = p
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
RingCat.moduleCatRestrictScalarsPseudofunctor_mapId : ∀ (x : CategoryTheory.LocallyDiscrete RingCatᵒᵖ),
  RingCat.moduleCatRestrictScalarsPseudofunctor.mapId x =
    CategoryTheory.Cat.Hom.isoMk (ModuleCat.restrictScalarsId ↑(Opposite.unop x.as))
-- Mathlib.Data.Nat.ChineseRemainder
Nat.chineseRemainderOfList_modEq_unique : ∀ {ι : Type u_1} (a s : ι → ℕ) (l : List ι) (co : List.Pairwise (Function.onFun Nat.Coprime s) l) {z : ℕ},
  (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(Nat.chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
-- Mathlib.RingTheory.WittVector.Compare
WittVector.fromPadicInt_comp_toPadicInt : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)],
  (WittVector.fromPadicInt p).comp (WittVector.toPadicInt p) = RingHom.id (WittVector p (ZMod p))
-- Mathlib.Data.Stream.Defs
/-- The constant stream: `Stream'.get n (Stream'.const a) = a`.  -/
Stream'.const : {α : Type u} → α → Stream' α
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
IsStarNormal.nnnorm_sub_eq_max : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {a b : A},
  IsStarNormal a → IsStarNormal b → Commute a b → a * b = 0 → ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊
-- Mathlib.Order.Atoms
IsAtom.Iic_eq : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, IsAtom a → Set.Iic a = {⊥, a}
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.IsSheaf.amalgamate.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A}
  (hP : CategoryTheory.Presheaf.IsSheaf J P) (S : J.Cover X) (x x_1 : (I : S.Arrow) → E ⟶ P.obj (Opposite.op I.Y))
  (e_x : x = x_1)
  (hx :
    ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂),
      CategoryTheory.CategoryStruct.comp (x I₁) (P.map r.g₁.op) =
        CategoryTheory.CategoryStruct.comp (x I₂) (P.map r.g₂.op)),
  hP.amalgamate S x hx = hP.amalgamate S x_1 ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (c : CategoryTheory.TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'), (c.ofArrowIso e).F = c.F
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The trivial monoid algebra is the base ring.  -/
MonoidAlgebra.uniqueRingEquiv : {R : Type u_1} → (M : Type u_4) → [inst : Semiring R] → [inst_1 : Monoid M] → [Subsingleton M] → MonoidAlgebra R M ≃+* R
-- Mathlib.Topology.Algebra.Group.Extension
TopologicalGroup.IsSES.isClosedEmbedding : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C},
  TopologicalGroup.IsSES φ ψ → Topology.IsClosedEmbedding ⇑φ
-- Mathlib.Algebra.Order.Hom.Basic
MulRingSeminormClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : NonAssocRing α] [inst_1 : Semiring β]
  [inst_2 : PartialOrder β] [inst_3 : FunLike F α β] [toAddGroupSeminormClass : AddGroupSeminormClass F α β]
  [toMonoidHomClass : MonoidHomClass F α β], MulRingSeminormClass F α β
-- Lean.Setup
Lean.ImportArtifacts.irParts : Lean.ImportArtifacts → Array System.FilePath
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.id : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (CategoryTheory.Functor.id C).LaxMonoidal
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_update_sum : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) {α : Type u_12}
  [inst_5 : DecidableEq ι] (t : Finset α) (i : ι) (g : α → M) (m : ι → M),
  f (Function.update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (Function.update m i (g a))
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.uliftFunctor_map : ∀ {x x_1 : CommGrpCat} (f : x ⟶ x_1),
  CommGrpCat.uliftFunctor.map f =
    CommGrpCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((CommGrpCat.Hom.hom f).comp MulEquiv.ulift.toMonoidHom))
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey?_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] {β : Type v} {γ : Type w} {f : α → β → Option γ}
  {l : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      (Std.Internal.List.getKey? k l).pfilter fun x h => (f x (Std.Internal.List.getValue x l ⋯)).isSome
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.not_mem_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α} {c : ℕ},
  a ∉ Std.DHashMap.Raw.emptyWithCapacity c
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Extend the total space of a pretrivialization from the preimage of a set to the whole space.  -/
Bundle.Pretrivialization.domExtend : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            {s : Set B} →
              (Bundle.Pretrivialization F fun z => proj ↑z) → [Nonempty (Z → F)] → Bundle.Pretrivialization F proj
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGT.congr_simp : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k k_1 : α) (e_k : k = k_1)
  (t t_1 : Std.DTreeMap.Internal.Impl α fun x => β) (e_t : t = t_1) (ho : t.Ordered)
  (he : ∃ a ∈ t, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.Const.getEntryGT k t ho he = Std.DTreeMap.Internal.Impl.Const.getEntryGT k_1 t_1 ⋯ ⋯
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.functorEquivalence_functor : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C],
  (CategoryTheory.ShortComplex.functorEquivalence J C).functor =
    CategoryTheory.ShortComplex.FunctorEquivalence.functor J C
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Icc_mul_Ico_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] (a b c d : α),
  Set.Icc a b * Set.Ico c d ⊆ Set.Ico (a * c) (b * d)
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mem_cellsOfRowLens : ∀ {w : List ℕ} {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens w ↔ ∃ (h : c.1 < w.length), c.2 < w[c.1]
-- Mathlib.Order.InitialSeg
/-- The range of the order embedding is the set of elements `b` such that `s b top`  -/
PrincipalSeg.mem_range_iff_rel' : ∀ {α : Type u_4} {β : Type u_5} {r : α → α → Prop} {s : β → β → Prop} (self : PrincipalSeg r s) (b : β),
  b ∈ Set.range ⇑self.toRelEmbedding ↔ s b self.top
-- Mathlib.Topology.Algebra.Module.FiniteDimension
Submodule.ClosedComplemented.of_finiteDimensional_quotient : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E] [ContinuousSMul 𝕜 E]
  {p : Submodule 𝕜 E}, IsClosed ↑p → ∀ [hq : FiniteDimensional 𝕜 (E ⧸ p)], p.ClosedComplemented
-- Mathlib.Util.Superscript
/-- The super/subscript parser.

* `m`: the character mapping
* `antiquotName`: the name to use for antiquotation bindings `$a:antiquotName`.
  Note that the actual syntax kind bound will be the body kind (parsed by `p`), not `kind`.
* `errorMsg`: shown when the parser does not match
* `p`: the inner parser (usually `term`), to be called on the body of the superscript
* `many`: if false, whitespace is not allowed inside the superscript
* `kind`: the term will be wrapped in a node with this kind;
  generally this is a name of the parser declaration itself.
 -/
Mathlib.Tactic.Superscript.scriptParser : Mathlib.Tactic.Superscript.Mapping →
  String →
    String →
      Lean.Parser.Parser →
        optParam Bool true →
          autoParam Lean.SyntaxNodeKind Mathlib.Tactic.Superscript.scriptParser._auto_1 → Lean.Parser.Parser
-- Mathlib.GroupTheory.OrderOfElement
subgroupOfIdempotent.eq_1 : ∀ {G : Type u_6} [inst : Group G] [inst_1 : Finite G] (S : Set G) (hS1 : S.Nonempty) (hS2 : S * S = S),
  subgroupOfIdempotent S hS1 hS2 = { carrier := S, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.Algebra.Module.Torsion.Basic
Ideal.coe_torsionOf : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  ↑(Ideal.torsionOf R M x) = ⇑(LinearMap.toSpanSingleton R M x) ⁻¹' {0}
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonLeanServerCapabilities.toJson : Lean.Lsp.LeanServerCapabilities → Lean.Json
-- Init.Data.Int.DivMod.Lemmas
Int.sub_fmod_left : ∀ (a b : ℤ), (a - b).fmod a = (-b).fmod a
-- Batteries.Data.List.Scan
List.getElem_partialSums : ∀ {α : Type u_1} {i : ℕ} [inst : Add α] [inst_1 : Zero α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0] {l : List α} (h : i < l.partialSums.length),
  l.partialSums[i] = (List.take i l).sum
-- Mathlib.Probability.HasLaw
/-- If there is a random variable `X` with law `μ` such that `f(X)` has law `ν`, then
for any random variable `Y` with law `μ`, `f(Y)` has law `ν`.  -/
ProbabilityTheory.HasLaw.comp_of_hasLaw_comp : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω} {Ω' : Type u_3} {𝓨 : Type u_4} {m' : MeasurableSpace Ω'}
  {m𝓨 : MeasurableSpace 𝓨} {P' : MeasureTheory.Measure Ω'} {ν : MeasureTheory.Measure 𝓨} {f : 𝓧 → 𝓨} {Y : Ω' → 𝓧},
  AEMeasurable f μ →
    ProbabilityTheory.HasLaw X μ P →
      ProbabilityTheory.HasLaw Y μ P' →
        ProbabilityTheory.HasLaw (fun ω => f (X ω)) ν P → ProbabilityTheory.HasLaw (fun ω => f (Y ω)) ν P'
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_neg_iff : ∀ {x : ℝ}, Real.arsinh x < 0 ↔ x < 0
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.toTopologicalSpace_injective : ∀ {α : Type u} [inst : AddGroup α], Function.Injective AddGroupTopology.toTopologicalSpace
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The canonical map from `G` to its profinite completion, as a function.  -/
ProfiniteGrp.ProfiniteCompletion.etaFn : (G : GrpCat) → ↑G → ↑(ProfiniteGrp.ProfiniteCompletion.completion G).toProfinite.toTop
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- `MonoidAlgebra.coeff` as a linear equiv.  -/
MonoidAlgebra.coeffLinearEquiv : (R : Type u_1) →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] → [inst_1 : Semiring S] → [inst_2 : Module R S] → MonoidAlgebra S M ≃ₗ[R] M →₀ S
-- Std.Time.Time.Unit.Second
Std.Time.Second.instLawfulEqOrdOffset : Std.LawfulEqOrd Std.Time.Second.Offset
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddSemigroup α], OrderDual.instAddSemigroup = { toAdd := OrderDual.instAdd, add_assoc := ⋯ }
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Measure.ext_of_integral_mul_prod_boundedContinuousFunction' : ∀ {κ : Type u_2} {Z : Type u_3} {Y : κ → Type u_6} {mY : (j : κ) → MeasurableSpace (Y j)}
  [inst : (j : κ) → TopologicalSpace (Y j)] [∀ (j : κ), BorelSpace (Y j)] [∀ (j : κ), HasOuterApproxClosed (Y j)]
  {mZ : MeasurableSpace Z} [inst_3 : TopologicalSpace Z] [BorelSpace Z] [HasOuterApproxClosed Z] [Finite κ]
  {μ ν : MeasureTheory.Measure (Z × ((i : κ) → Y i))} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (f : BoundedContinuousFunction Z ℝ) (g : BoundedContinuousFunction ((j : κ) → Y j) ℝ),
      ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂μ = ∫ (p : Z × ((i : κ) → Y i)), f p.1 * g p.2 ∂ν) →
    μ = ν
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.pushEqHEq : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of a product is the product of the trailing coefficients.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {f₁ f₂ : 𝕜 → 𝕜},
  MeromorphicAt f₁ x →
    MeromorphicAt f₂ x →
      meromorphicTrailingCoeffAt (f₁ * f₂) x = meromorphicTrailingCoeffAt f₁ x * meromorphicTrailingCoeffAt f₂ x
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.instIsTriangularizableOfIsAlgClosed : ∀ (K : Type u_1) (L : Type u_3) (M : Type u_4) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [inst_3 : Field K] [inst_4 : LieAlgebra K L] [inst_5 : Module K M] [inst_6 : LieModule K L M] [FiniteDimensional K M]
  [IsAlgClosed K], LieModule.IsTriangularizable K L M
-- Lean.Elab.Term.TermElabM
/-- Execute `x` but discard changes performed at `Term.State` and `Meta.State`.
Recall that the `Environment`, `InfoState` and messages are at `Core.State`.  Thus, any updates to
it will be preserved.
This method is useful for performing computations where all metavariable must be resolved or
discarded.
The `InfoTree`s are not discarded, however, and wrapped in `InfoTree.Context`
to store their metavariable context.
 -/
Lean.Elab.Term.withoutModifyingElabMetaStateWithInfo : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- Sum of series is analytic on its ball of convergence.  -/
FormalMultilinearSeries.analyticOnNhd : ∀ {𝕜 : 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] [CompleteSpace F]
  {p : FormalMultilinearSeries 𝕜 E F}, AnalyticOnNhd 𝕜 p.sum (Metric.eball 0 p.radius)
-- Mathlib.NumberTheory.NumberField.ClassNumber
NumberField.classNumber.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.classNumber K = Fintype.card (ClassGroup (NumberField.RingOfIntegers K))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (t.insertMany l).getKey? k = t.getKey? k
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley_le_iff : ∀ {M : Type u_1} (s : Set M) [inst : Mul M] (G : SimpleGraph M),
  SimpleGraph.mulCayley s ≤ G ↔ ∀ g ∈ s, ∀ (a : M), a * g ≠ a → G.Adj (a * g) a
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.le_of_eq : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α]
  (ctx : Lean.Grind.Linarith.Context α) (lhs rhs : Lean.Grind.Linarith.Expr) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.norm_cert lhs rhs p = true →
    Lean.Grind.Linarith.Expr.denote ctx lhs = Lean.Grind.Linarith.Expr.denote ctx rhs →
      Lean.Grind.Linarith.Poly.denote' ctx p ≤ 0
-- Mathlib.Algebra.Group.Even
IsSquare.map : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MulOneClass α] [inst_1 : MulOneClass β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] {a : α} (f : F), IsSquare a → IsSquare (f a)
-- Lean.CompactedRegion
/-- Path the region was loaded from.  -/
Lean.CompactedRegion.filePath : Lean.CompactedRegion → System.FilePath
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k),
  algebraMap (MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R))
      (TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)) =
    (MvPolynomial.aeval (Sum.elim (fun x => MvPolynomial.X x ⊗ₜ[R] 1) fun x => 1 ⊗ₜ[R] MvPolynomial.X x)).toRingHom
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterExists_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  [inst_8 : NeZero n] (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂),
  (s.map f.toAffineMap ⋯).ExcenterExists = s.ExcenterExists
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.AC.EqCnstr → Sort u} {motive_2 : Lean.Meta.Grind.AC.EqCnstrProof → Sort u}
  (t : Lean.Meta.Grind.AC.EqCnstrProof) (F_1 : (t : Lean.Meta.Grind.AC.EqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.AC.EqCnstrProof) → t.below → motive_2 t),
  t.brecOn F_1 F_2 = F_2 t (Lean.Meta.Grind.AC.EqCnstrProof.brecOn.go t F_1 F_2).2
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
RootPairingCat.category : {R : Type u} → [inst : CommRing R] → CategoryTheory.Category.{v, max (v + 1) u} (RootPairingCat R)
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.neg_le : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {S T : Submodule R M}, -S ≤ T ↔ S ≤ -T
-- Init.Data.Rat.Lemmas
Rat.mk_eq_normalize : ∀ (num : ℤ) (den : ℕ) (nz : den ≠ 0) (c : num.natAbs.Coprime den),
  { num := num, den := den, den_nz := nz, reduced := c } = Rat.normalize num den nz
-- Mathlib.Data.Prod.Basic
Prod.Lex.trans : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans α r] [IsTrans β s] {x y z : α × β},
  Prod.Lex r s x y → Prod.Lex r s y z → Prod.Lex r s x z
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressBegin.title : Lean.Lsp.WorkDoneProgressBegin → String
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `monotoneOn_comp_ofDual_iff`. -/
AntitoneOn.dual_left : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  AntitoneOn f s → MonotoneOn (f ∘ ⇑OrderDual.ofDual) s
-- Mathlib.SetTheory.ZFC.PSet
PSet.empty_def : ∅ = PSet.mk PEmpty.{u_1 + 1} PEmpty.elim
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.dvd_lcm_right : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (x y : R), y ∣ EuclideanDomain.lcm x y
-- Mathlib.Tactic.Abel
/-- The expression representing `0 : α`.  -/
Mathlib.Tactic.Abel.Context.α0 : Mathlib.Tactic.Abel.Context → Lean.Expr
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C} (Z : C)
  [HomotopicalAlgebra.IsFibrant Z] (f : X ⟶ Y) [HomotopicalAlgebra.Cofibration f]
  [HomotopicalAlgebra.WeakEquivalence f], Function.Bijective fun g => g.precomp f
-- Mathlib.Algebra.Order.Field.Basic
sub_inv_antitoneOn_Iio : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {c : α},
  AntitoneOn (fun x => (x - c)⁻¹) (Set.Iio c)
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `Topology.IsOpenEmbedding.locallyPathConnectedSpace`. -/
Topology.IsOpenEmbedding.locPathConnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyPathConnectedSpace X]
  {e : Y → X}, Topology.IsOpenEmbedding e → LocallyPathConnectedSpace Y
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff_add : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] {x y : HahnSeries Γ R} {a : Γ},
  (x + y).coeff a = x.coeff a + y.coeff a
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.RelCWComplex.Subcomplex.I.hcongr_7 : ∀ (X X' : Type u_1),
  X = X' →
    ∀ (t : TopologicalSpace X) (t' : TopologicalSpace X'),
      t ≍ t' →
        ∀ (C : Set X) (C' : Set X'),
          C ≍ C' →
            ∀ (D : Set X) (D' : Set X'),
              D ≍ D' →
                ∀ (inst : Topology.RelCWComplex C D) (inst' : Topology.RelCWComplex C' D'),
                  inst ≍ inst' →
                    ∀ (self : Topology.RelCWComplex.Subcomplex C) (self' : Topology.RelCWComplex.Subcomplex C'),
                      self ≍ self' → ∀ (n n' : ℕ), n = n' → self.I n ≍ self'.I n'
-- Lean.Server.ServerTask
Lean.Server.ServerTask : Type u → Type u