mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ModuleCat k}
  (h : ModuleCat.of k ↥(groupHomology.cycles₂ B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.cyclesMap f φ 2)
      (CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₂ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₂ A).hom
      (CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₂ f φ) h)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.mk.injEq : ∀ {R : Type u} [inst : CommRing R] (toModuleCat : ModuleCat R) (form : QuadraticForm R ↑toModuleCat)
  (toModuleCat_1 : ModuleCat R) (form_1 : QuadraticForm R ↑toModuleCat_1),
  ({ toModuleCat := toModuleCat, form := form } = { toModuleCat := toModuleCat_1, form := form_1 }) =
    (toModuleCat = toModuleCat_1 ∧ form ≍ form_1)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.le_lt_combine_cert.eq_1 : ∀ (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.le_lt_combine_cert p₁ p₂ p₃ =
    (decide (↑p₁.leadCoeff.natAbs > 0) && p₃ == (p₁.mul ↑p₂.leadCoeff.natAbs).combine (p₂.mul ↑p₁.leadCoeff.natAbs))
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.PlausibleStep.skipLeft : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  {it : Std.IterM m (β₁ × β₂)},
  it.internalState.memoizedLeft = none →
    ∀ {it' : Std.IterM m β₁},
      it.internalState.left.IsPlausibleStep (Std.IterStep.skip it') →
        Std.Iterators.Types.Zip.PlausibleStep it
          (Std.IterStep.skip
            { internalState := { left := it', memoizedLeft := none, right := it.internalState.right } })
-- Mathlib.Algebra.Category.Grp.Colimits
/-- The categorical cokernel of a morphism in `AddCommGrpCat`
agrees with the usual group-theoretical quotient.
 -/
AddCommGrpCat.cokernelIsoQuotient : {G H : AddCommGrpCat} →
  (f : G ⟶ H) → CategoryTheory.Limits.cokernel f ≅ AddCommGrpCat.of (↑H ⧸ (AddCommGrpCat.Hom.hom f).range)
-- Lean.Meta.Sym.DSimp.DSimpM
/-- Configuration options for the definitional simplifier.  -/
Lean.Meta.Sym.DSimp.Config : Type
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.coeFn_ofSeqClosedGraph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_5} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {g : E →ₗ[𝕜] F}
  (hg :
    ∀ (u : ℕ → E) (x : E) (y : F),
      Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (⇑g ∘ u) Filter.atTop (nhds y) → y = g x),
  ⇑(ContinuousLinearMap.ofSeqClosedGraph hg) = ⇑g
-- Mathlib.Topology.Inseparable
Topology.IsInducing.inseparable_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y},
  Topology.IsInducing f → (Inseparable (f x) (f y) ↔ Inseparable x y)
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.mk₀.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y),
  CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f =
    CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorZero' C m₀ hm₀).inv.app Y)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.unop_h₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.unop.h₃ = h.h₀.unop
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.inv_Iio₀ : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α},
  a < 0 → (Set.Iio a)⁻¹ = Set.Ioo a⁻¹ 0
-- Lean.Util.CollectMVars
Lean.CollectMVars.State.mk.inj : ∀ {visitedExpr : Lean.ExprSet} {result : Array Lean.MVarId} {visitedExpr_1 : Lean.ExprSet}
  {result_1 : Array Lean.MVarId},
  { visitedExpr := visitedExpr, result := result } = { visitedExpr := visitedExpr_1, result := result_1 } →
    visitedExpr = visitedExpr_1 ∧ result = result_1
-- Mathlib.CategoryTheory.Monoidal.Braided.PushoutObjObj
CategoryTheory.Functor.PushoutObjObj.flipTensor_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ Y₁ X₂ Y₂ : C} {f₁ : X₁ ⟶ Y₁} {f₂ : X₂ ⟶ Y₂}
  (sq : (CategoryTheory.MonoidalCategory.curriedTensor C).PushoutObjObj f₁ f₂),
  sq.flipTensor.ι = CategoryTheory.CategoryStruct.comp sq.ι (β_ Y₂ Y₁).inv
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.compatible_of_mem_maximalAtlas : ∀ {𝕜 : 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} {n : WithTop ℕ∞}
  {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {e e' : OpenPartialHomeomorph M H},
  e ∈ IsManifold.maximalAtlas I n M → e' ∈ IsManifold.maximalAtlas I n M → e.symm.trans e' ∈ contDiffGroupoid n I
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- Smoothness exponent for analytic functions.  -/
ContDiff.termω : Lean.ParserDescr
-- Init.Data.Int.Order
Int.le_of_add_le_add_right : ∀ {a b c : ℤ}, a + b ≤ c + b → a ≤ c
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_sumInl : ∀ {𝕜 : 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] {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {p : M ⊕ M'} {q : M}, mfderiv% Sum.inl q = ContinuousLinearMap.id 𝕜 (TangentSpace I p)
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : 𝕜 → 𝕜` is convex on `s`, then for any point `x ∈ s` the slope of the secant line of `f`
through `x` is monotone on `s \ {x}`.  -/
ConvexOn.slope_mono : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜},
  ConvexOn 𝕜 s f → x ∈ s → MonotoneOn (slope f x) (s \ {x})
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_one`. -/
ENat.coe_one : ↑1 = 1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_eq_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} {fallback : β}, Std.DTreeMap.Const.getD t a fallback = t.getD a fallback
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfOplax_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) (F' : F.PseudoCore) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.Pseudofunctor.mkOfOplax F F').mapComp f g = F'.mapCompIso f g
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- The existence of binary biproducts implies that there is at most one preadditive structure.  -/
CategoryTheory.subsingleton_preadditive_of_hasBinaryBiproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasBinaryBiproducts C], Subsingleton (CategoryTheory.Preadditive C)
-- Mathlib.Data.Rel
SetRel.isSymm_inter : ∀ {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsSymm] [R₂.IsSymm], (R₁ ∩ R₂).IsSymm
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.IsLE.le : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {inst_2 : CategoryTheory.Limits.HasZeroObject C} {inst_3 : CategoryTheory.HasShift C ℤ}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  {t : CategoryTheory.Triangulated.TStructure C} {X : C} {n : ℤ} [self : t.IsLE X n], t.le n X
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.star_def : ∀ {ι : Type u_1} {R : ι → Type u_6} [inst : (i : ι) → Star (R i)] (x : (i : ι) → R i), star x = fun i => star (x i)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_whiskerLeft_inv_hom_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h k : c ⟶ d} (η : h ≅ k)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g k) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η.inv))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η.hom)) h_1) =
    h_1
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_univ : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Submodule.span R Set.univ = ⊤
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.ext : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x y : ℤ_[p]}, ↑x = ↑y → x = y
-- Init.Data.Array.Lemmas
Array.back?_isSome : ∀ {α : Type u_1} {xs : Array α}, xs.back?.isSome = true ↔ xs ≠ #[]
-- Batteries.Data.List.Lemmas
List.exists_of_replaceF : ∀ {α : Type u_1} {p : α → Option α} {l : List α} {a a' : α},
  a ∈ l →
    p a = some a' →
      ∃ a a' l₁ l₂, (∀ b ∈ l₁, p b = none) ∧ p a = some a' ∧ l = l₁ ++ a :: l₂ ∧ List.replaceF p l = l₁ ++ a' :: l₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.toList_insert_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : BEq α]
  [Std.TransCmp cmp] [Std.LawfulBEqCmp cmp] {k : α} {v : β},
  (Std.DTreeMap.Const.toList (t.insert k v)).Perm
    ((k, v) :: List.filter (fun x => decide ¬(k == x.1) = true) (Std.DTreeMap.Const.toList t))
-- Batteries.Recycling.RBTree.Lemmas
/-- Wraps a list of elements with the left and right elements of the path.  -/
RBTree.RBNode.Path.withList : {α : Type u_1} → RBTree.RBNode.Path α → List α → List α
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.IsRingHom.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {R₁ R₂ : C} [inst_2 : CategoryTheory.AddMonObj R₁] [inst_3 : CategoryTheory.AddMonObj R₂]
  [inst_4 : CategoryTheory.MonObj R₁] [inst_5 : CategoryTheory.MonObj R₂] {f : R₁ ⟶ R₂}
  [toIsAddMonHom : CategoryTheory.IsAddMonHom f] [toIsMonHom : CategoryTheory.IsMonHom f], CategoryTheory.IsRingHom f
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instSMul : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] →
          {𝕜 : Type u_5} → [inst_2 : SMul 𝕜 γ] → [ContinuousConstSMul 𝕜 γ] → SMul 𝕜 (α →ₘ[μ] γ)
-- Init.Grind.Lemmas
Lean.Grind.ne_of_ne_of_eq_right : ∀ {α : Sort u} {a b c : α}, a = c → b ≠ c → b ≠ a
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.max_val : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : LinearOrder α] (a b : AddUnits α), ↑(max a b) = max ↑a ↑b
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.ShortComplex.exact_iff_exact_image_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  S.Exact ↔
    { X₁ := CategoryTheory.Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := CategoryTheory.Abelian.image.ι S.f, g := S.g,
        zero := ⋯ }.Exact
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Prod.isAffineMap_snd : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {X : Type u_3}
  {Y : Type u_4} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y],
  Convexity.IsAffineMap R Prod.snd
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.cgf_le : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X c μ → ∀ (t : ℝ), ProbabilityTheory.cgf X μ t ≤ ↑c * t ^ 2 / 2
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instZeroAddGroupSeminorm : {E : Type u_3} → [inst : AddGroup E] → Zero (AddGroupSeminorm E)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along column `j`.  -/
Matrix.det_succ_column : ∀ {R : Type v} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (j : Fin n.succ),
  A.det = ∑ i, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingNorm.ext_iff : ∀ {R : Type u_1} [inst : NonUnitalRing R] {p q : RingNorm R}, p = q ↔ ∀ (x : R), p x = q x
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.ι_colimitIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E) [inst_4 : CategoryTheory.Limits.HasColimit G] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) X)
      (CategoryTheory.Functor.Final.colimitIso F G).hom =
    CategoryTheory.Limits.colimit.ι G (F.obj X)
-- Mathlib.Computability.Primrec.Basic
Primrec.option_bind₁ : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → Option σ},
  Primrec f → Primrec fun o => o.bind f
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.distribSMul' : {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {n : (i : I) → AddZeroClass (g i)} →
        [(i : I) → DistribSMul (f i) (g i)] → DistribSMul ((i : I) → f i) ((i : I) → g i)
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- Let `L / K` be a normal field extension. For any two elements `x` and `y` in `L`, if `y` is a
conjugate root of `x`, then there exists a `K`-automorphism `σ : Gal(L/K)` such
that `σ y = x`.
 -/
IsConjRoot.exists_algEquiv : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Normal K L] {x y : L},
  IsConjRoot K x y → ∃ σ, σ y = x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_insertManyIfNewUnit_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} {ρ : Type w} [inst : ForIn Id ρ α]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ} {k : α}, k ∈ m → k ∈ m.insertManyIfNewUnit l
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.parseLocalTimeTypes : UInt32 → Std.Internal.Parsec.ByteArray.Parser (Array Std.Time.TimeZone.TZif.LocalTimeType)
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.trunc'_map : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : DecidableEq σ] [inst_1 : CommSemiring R]
  [inst_2 : CommSemiring S] (n : σ →₀ ℕ) (f : R →+* S) (p : MvPowerSeries σ R),
  (MvPowerSeries.trunc' S n) ((MvPowerSeries.map f) p) = (MvPolynomial.map f) ((MvPowerSeries.trunc' R n) p)
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.lid_toCoalgEquiv : ∀ {R : Type u_1} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring B] [inst_2 : Bialgebra R B],
  ↑(Bialgebra.TensorProduct.lid R B) = Coalgebra.TensorProduct.lid R B
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The functor `C ⥤ D × E` obtained from two oplax monoidal functors is oplax monoidal.  -/
CategoryTheory.Functor.OplaxMonoidal.prod' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (F : CategoryTheory.Functor C D) →
                    (G : CategoryTheory.Functor C E) → [F.OplaxMonoidal] → [G.OplaxMonoidal] → (F.prod' G).OplaxMonoidal
-- Lean.Elab.Term.TermElabM
/-- Execute `x` but discard changes performed to the state.
However, the info trees and messages are not discarded.  -/
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.withoutModifyingStateWithInfoAndMessagesImpl : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Mathlib.Dynamics.Ergodic.Extreme
Ergodic.eq_of_absolutelyContinuous : ∀ {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} {f : X → X}
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν],
  Ergodic f μ → MeasureTheory.MeasurePreserving f ν ν → ν.AbsolutelyContinuous μ → ν = μ
-- Mathlib.Data.List.Intervals
List.Ico.filter_lt_of_ge : ∀ {n m l : ℕ}, l ≤ m → List.filter (fun x => decide (x < l)) (List.Ico n m) = List.Ico n l
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.instIsFractionRingInteger : ∀ {K : Type v} {Γ : Type w} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ),
  IsFractionRing (↥v.integer) K
-- Mathlib.LinearAlgebra.Complex.Module
realPart_nonpos_of_nonpos : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : PartialOrder A] [StarOrderedRing A]
  [inst_4 : Module ℂ A] [inst_5 : StarModule ℂ A] {a : A}, a ≤ 0 → realPart a ≤ 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfcₙ_nnreal_lt : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_8 : NonnegSpectrumClass ℝ A]
  {f : NNReal → NNReal} {a : A} {c : NNReal}, (∀ x ∈ quasispectrum NNReal a, f x < c) → ‖cfcₙ f a‖₊ < c
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- `x ^ s = o(exp(b * x))` as `x → ∞` for any real `s` and positive `b`.  -/
isLittleO_rpow_exp_pos_mul_atTop : ∀ (s : ℝ) {b : ℝ}, 0 < b → (fun x => x ^ s) =o[Filter.atTop] fun x => Real.exp (b * x)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Break.runK.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Topology.MetricSpace.HausdorffDistance
IsCompact.exists_infEDist_eq_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α},
  IsCompact s → s.Nonempty → ∀ (x : α), ∃ y ∈ s, Metric.infEDist x s = edist x y
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
/-- Pre-composition by a *fixed* continuous linear map as a continuous linear map for the pointwise
convergence topology.  -/
PointwiseConvergenceCLM.precomp : {𝕜₁ : Type u_4} →
  {𝕜₂ : Type u_5} →
    {𝕜₃ : Type u_6} →
      [inst : NormedField 𝕜₁] →
        [inst_1 : NormedField 𝕜₂] →
          [inst_2 : NormedField 𝕜₃] →
            {σ : 𝕜₁ →+* 𝕜₂} →
              {τ : 𝕜₂ →+* 𝕜₃} →
                {ρ : 𝕜₁ →+* 𝕜₃} →
                  [RingHomCompTriple σ τ ρ] →
                    {E : Type u_7} →
                      {F : Type u_8} →
                        (G : Type u_10) →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : TopologicalSpace E] →
                              [inst_6 : AddCommGroup F] →
                                [inst_7 : TopologicalSpace F] →
                                  [inst_8 : AddCommGroup G] →
                                    [inst_9 : TopologicalSpace G] →
                                      [inst_10 : IsTopologicalAddGroup G] →
                                        [inst_11 : Module 𝕜₁ E] →
                                          [inst_12 : Module 𝕜₂ F] →
                                            [inst_13 : Module 𝕜₃ G] →
                                              [inst_14 : ContinuousConstSMul 𝕜₃ G] →
                                                (E →SL[σ] F) → (F →SLₚₜ[τ] G) →L[𝕜₃] E →SLₚₜ[ρ] G
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.natDegree_C_le : ∀ {R : Type u_1} [inst : Semiring R] (a : R), (Polynomial.C a).natDegree ≤ 0
-- Mathlib.CategoryTheory.Filtered.Connected
CategoryTheory.IsCofiltered.isConnected : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C], CategoryTheory.IsConnected C
-- Mathlib.MeasureTheory.Integral.Average
/-- Average value of a function `f` w.r.t. a measure `μ` on a set `s`.

It is equal to `(μ.real s)⁻¹ * ∫ x, f x ∂μ`, so it takes value zero if `f` is not integrable on
`s` or if `s` has infinite measure. If `s` has measure `1`, then the average of any function is
equal to its integral.

For the average w.r.t. the volume, one can omit `∂volume`.  -/
MeasureTheory.«term⨍_In_,_∂_» : Lean.ParserDescr
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.card_add_self_le : ∀ {G : Type u_1} [inst : AddGroup G] {K : ℝ} [inst_1 : DecidableEq G] {A : Finset G},
  IsApproximateAddSubgroup K ↑A → ↑(A + A).card ≤ K * ↑A.card
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x) (hn : n ≠ 0), ↑(hf.mfderivToContinuousLinearEquiv hn) = mfderiv% f x
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.Context.mk.inj : ∀ {ctx : Lean.Meta.Simp.Context} {simp : Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result}
  {ctx_1 : Lean.Meta.Simp.Context} {simp_1 : Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result},
  { ctx := ctx, simp := simp } = { ctx := ctx_1, simp := simp_1 } → ctx = ctx_1 ∧ simp = simp_1
-- Mathlib.Order.Category.Semilat
/-- The category of sup-semilattices with a bottom element.  -/
SemilatSupCat : Type (u + 1)
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.getQuotKind : Lean.Syntax → Lean.Elab.TermElabM Lean.SyntaxNodeKind
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarCoordReal.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.polarCoordReal K = NumberField.mixedEmbedding.polarCoordReal K
-- Mathlib.CategoryTheory.Category.Bipointed
pointedToBipointedFst_comp_swap : pointedToBipointedFst.comp Bipointed.swap = pointedToBipointedSnd
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.add_congr.ww : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : Add α] [Lean.Grind.ToInt.Add α i],
  i.isFinite = true → ∀ {a b : α} {a' b' : ℤ}, ↑a = i.wrap a' → ↑b = i.wrap b' → ↑(a + b) = i.wrap (a' + b')
-- Mathlib.Tactic.NormNum.Irrational
_private.Mathlib.Tactic.NormNum.Irrational.0.Mathlib.Meta.NormNum.not_power_nat_of_bounds : ∀ {n k d : ℕ}, k ^ d < n → n < (k + 1) ^ d → ∀ {m : ℕ}, n ≠ m ^ d