mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_preimage_mem_nhds' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {t : Set M} [inst_5 : ChartedSpace H M] {x x' : M},
  x' ∈ (extChartAt I x).source → t ∈ nhds x' → ↑(extChartAt I x).symm ⁻¹' t ∈ nhds (↑(extChartAt I x) x')
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Functor.IsLocallyFull.ext : ∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {D : Type uD} [inst_1 : CategoryTheory.Category.{vD, uD} D]
  {K : CategoryTheory.GrothendieckTopology D} (G : CategoryTheory.Functor C D) [G.IsLocallyFull K]
  (ℱ : CategoryTheory.Sheaf K (Type u_2)) {X Y : C} (i : G.obj X ⟶ G.obj Y) {s t : ℱ.obj.obj (Opposite.op (G.obj X))},
  (∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y),
      G.map f = CategoryTheory.CategoryStruct.comp (G.map j) i →
        (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) s =
          (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) t) →
    s = t
-- Mathlib.Algebra.Star.MonoidHom
/-- A *star monoid homomorphism* is a monoid homomorphism which is `star`-preserving.  -/
StarMonoidHom : (A : Type u_6) → (B : Type u_7) → [Monoid A] → [Star A] → [Monoid B] → [Star B] → Type (max u_6 u_7)
-- Mathlib.Algebra.DirectSum.Basic
/-- create a homomorphism from `⨁ i, α i` to `⨁ i, β i` by giving the component-wise map `f`.  -/
DirectSum.map : {ι : Type u_3} →
  {α : ι → Type u_4} →
    {β : ι → Type u_5} →
      [inst : (i : ι) → AddCommMonoid (α i)] →
        [inst_1 : (i : ι) → AddCommMonoid (β i)] →
          ((i : ι) → α i →+ β i) → (DirectSum ι fun i => α i) →+ DirectSum ι fun i => β i
-- Mathlib.RingTheory.Localization.Integral
IsLocalization.scaleRoots_commonDenom_mem_lifts : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {Rₘ : Type u_3} [inst_1 : CommRing Rₘ] [inst_2 : Algebra R Rₘ]
  [inst_3 : IsLocalization M Rₘ] (p : Polynomial Rₘ),
  p.leadingCoeff ∈ (algebraMap R Rₘ).range →
    p.scaleRoots ((algebraMap R Rₘ) ↑(IsLocalization.commonDenom M p.support p.coeff)) ∈
      Polynomial.lifts (algebraMap R Rₘ)
-- Batteries.Lean.Meta.DiscrTree
/-- Auxiliary definition for `mergePreservingDuplicates`.  -/
Lean.Meta.DiscrTree.Trie.mergePreservingDuplicates.mergeChildren : {α : Type} →
  Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) →
    Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) →
      Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)
-- Mathlib.Topology.MetricSpace.Bounded
totallyBounded_Ioc : ∀ {α : Type u} [inst : UniformSpace α] [inst_1 : Preorder α] [CompactIccSpace α] (a b : α), TotallyBounded (Set.Ioc a b)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.div : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β]
  [inst_1 : GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β] [TopologicalSpace.MetrizableSpace β],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (f / g)
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The object underlying `⊥ : Subobject B` is (up to isomorphism) the initial object.  -/
CategoryTheory.Subobject.botCoeIsoInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasInitial C] →
      [inst_2 : CategoryTheory.Limits.InitialMonoClass C] → {B : C} → CategoryTheory.Subobject.underlying.obj ⊥ ≅ ⊥_ C
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (p q : ℤ)
  (hpq : p + -1 = q) {Z : C}
  (h : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle φ).obj₁).X q ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q hpq)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.triangle φ).mor₃.f q) h) =
    CategoryTheory.CategoryStruct.comp (-(K.shiftFunctorObjXIso 1 q p ⋯).inv) h
-- Mathlib.Analysis.Normed.Group.AddTorsor
dist_vadd_cancel_left : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (v : V) (x y : P), dist (v +ᵥ x) (v +ᵥ y) = dist x y
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abs_isAbsoluteValue : ∀ {S : Type u_5} [inst : Ring S] [inst_1 : LinearOrder S] [IsStrictOrderedRing S], IsAbsoluteValue abs
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` reflects limits, then `F.leftOp : Cᵒᵖ ⥤ D` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimits_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsLimits F],
  CategoryTheory.Limits.ReflectsColimits F.leftOp
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocFrame.titleString : Lean.VersoModuleDocs.DocFrame✝ → String
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital subalgebra of a non-unital normed ring is also a non-unital normed ring,
with the restriction of the norm.  -/
NonUnitalSubalgebraClass.nonUnitalNormedRing : {S : Type u_5} →
  {𝕜 : Type u_6} →
    {E : Type u_7} →
      [inst : CommRing 𝕜] →
        [inst_1 : NonUnitalNormedRing E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : SetLike S E] →
              [NonUnitalSubringClass S E] → [SMulMemClass S 𝕜 E] → (s : S) → NonUnitalNormedRing ↥s
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.CollectState.mk : Std.HashSet Lean.Meta.Sym.ExprPtr →
  Std.HashSet (Lean.Meta.Grind.Origin × Lean.Meta.Grind.EMatchTheoremKind) →
    Array Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.Action.CollectState✝
-- Mathlib.Topology.NhdsWithin
nhdsWithin_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α), nhdsWithin a {a} = pure a
-- Aesop.Check
Aesop.Check.script : Aesop.Check
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.eq_symm_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) {x : N} {y : M}, y = e.symm x ↔ e y = x
-- Mathlib.Algebra.Notation.Support
Function.support_subset_iff' : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M} {s : Set ι}, Function.support f ⊆ s ↔ ∀ x ∉ s, f x = 0
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The composition functor is also the composition on additive monoid objects.  -/
CategoryTheory.Functor.mapAddMonCompIso : {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 D E} →
                      [inst_6 : F.LaxMonoidal] →
                        [inst_7 : G.LaxMonoidal] → (F.comp G).mapAddMon ≅ F.mapAddMon.comp G.mapAddMon
-- Mathlib.Algebra.Group.Submonoid.Units
/-- The equivalence between the additive subgroup of additive units of
`S` and the type of additive units of `S`.  -/
AddSubmonoid.addUnitsEquivAddUnitsType : {M : Type u_1} → [inst : AddMonoid M] → (S : AddSubmonoid M) → ↥S.addUnits ≃+ AddUnits ↥S
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.norm_term_le : ∀ {f g : ℕ → ℂ} (s : ℂ) {n : ℕ}, ‖f n‖ ≤ ‖g n‖ → ‖LSeries.term f s n‖ ≤ ‖LSeries.term g s n‖
-- Init.Data.Array.Basic
/-- Returns `true` if `p` returns `true` for any element of `as`.

Short-circuits upon encountering the first `true`.

The optional parameters `start` and `stop` control the region of the array to be checked. Only the
elements with indices from `start` (inclusive) to `stop` (exclusive) are checked. By default, the
entire array is checked.

Examples:
* `#[2, 4, 6].any (· % 2 = 0) = true`
* `#[2, 4, 6].any (· % 2 = 1) = false`
* `#[2, 4, 5, 6].any (· % 2 = 0) = true`
* `#[2, 4, 5, 6].any (· % 2 = 1) = true`
 -/
Array.any : {α : Type u} → (as : Array α) → (α → Bool) → optParam ℕ 0 → optParam ℕ as.size → Bool
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.top_typein : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r], (Ordinal.typein r).top = Ordinal.type r
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fun_div_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (c : ℝ),
  ProbabilityTheory.covariance X (fun ω => Y ω / c) μ = ProbabilityTheory.covariance X Y μ / c
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.instHomIsOverComp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] [inst_3 : CategoryTheory.OverClass Z S] (f : X ⟶ Y) (g : Y ⟶ Z)
  [CategoryTheory.HomIsOver f S] [CategoryTheory.HomIsOver g S],
  CategoryTheory.HomIsOver (CategoryTheory.CategoryStruct.comp f g) S
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- If `f` is a ring seminorm on `R` with `f 1 ≤ 1` and `s : ℕ → ℕ` is bounded by `n`, then
`f (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ))` is eventually bounded.  -/
RingSeminorm.isBoundedUnder : ∀ {R : Type u_1} [inst : Ring R] (p : RingSeminorm R),
  p 1 ≤ 1 →
    ∀ {s : ℕ → ℕ},
      (∀ (n : ℕ), s n ≤ n) →
        ∀ {x : R} (ψ : ℕ → ℕ), Filter.IsBoundedUnder LE.le Filter.atTop fun n => p (x ^ s (ψ n)) ^ (1 / ↑(ψ n))
-- Mathlib.Data.Finsupp.Single
Finsupp.support_update : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α) (b : M) [inst_1 : DecidableEq α]
  [inst_2 : DecidableEq M], (f.update a b).support = if b = 0 then f.support.erase a else insert a f.support
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.evalCompInclIsoId_hom_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (A : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] (X : CategoryTheory.Functor C A) (X_1 : C),
  ((CategoryTheory.Limits.FormalCoproduct.evalCompInclIsoId C A).hom.app X).app X_1 =
    CategoryTheory.Limits.Sigma.desc fun x => CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.insertListₘ.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : List ((a : α) × β a) → Sort u_3) →
      (l : List ((a : α) × β a)) →
        (Unit → motive []) → ((hd : (a : α) × β a) → (tl : List ((a : α) × β a)) → motive (hd :: tl)) → motive l
-- Mathlib.Data.Quot
/-- Map a function `f : α → β` that sends equivalent elements to equivalent elements
to a function `Quotient sa → Quotient sb`. Useful to define unary operations on quotients.
This is a version of `Quotient.map` using `Setoid.r` instead of `≈`.  -/
Quotient.map' : {α : Sort u_1} →
  {β : Sort u_2} →
    {s₁ : Setoid α} → {s₂ : Setoid β} → (f : α → β) → (∀ (a b : α), s₁ a b → s₂ (f a) (f b)) → Quotient s₁ → Quotient s₂
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.num_intCast : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : DecidableEq m] (a : ℤ), (↑a).num = ↑a
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The image under a ring homomorphism of the subring generated by a set equals
the subring generated by the image of the set.  -/
RingHom.map_closure : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S) (s : Set R),
  Subring.map f (Subring.closure s) = Subring.closure (⇑f '' s)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instSemiring : {d : ℤ} → Semiring (ℤ√d)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Cardinal.add_one_of_aleph0_le : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c + 1 = c
-- Mathlib.Topology.UniformSpace.Cauchy
/-- The discrete uniformity makes a space complete.  -/
DiscreteUniformity.instCompleteSpace : ∀ {α : Type u} [uniformSpace : UniformSpace α] [DiscreteUniformity α], CompleteSpace α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k : α} [inst_3 : Inhabited (β k)],
      (List.map Sigma.fst l).contains k = false → (↑(m.insertMany l)).get! k = m.get! k
-- Lean.Elab.Parallel
/-- Runs a list of CoreM computations in parallel and collects results in the original order,
including the saved state after each task completes.

Unlike `parIter`, this waits for all tasks to complete and returns results
in the same order as the input list, not in completion order.

Results are wrapped in `Except Exception (α × Core.SavedState)` so that errors in individual
tasks don't stop the collection - you can observe all results including which tasks failed.

The final CoreM state is restored to the initial state (before tasks ran).
 -/
Lean.Core.CoreM.par : {α : Type} → List (Lean.CoreM α) → Lean.CoreM (List (Except Lean.Exception (α × Lean.Core.SavedState)))
-- Mathlib.Algebra.DirectSum.Module
DirectSum.linearEquivFunOnFintype_lof : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (i : ι) (m : M i),
  (DirectSum.linearEquivFunOnFintype R ι M) ((DirectSum.lof R ι M i) m) = Pi.single i m
-- Mathlib.Data.List.PeriodicityLemma
List.hasPeriod_of_length_le : ∀ {α : Type u_1} (w : List α) (p : ℕ), w.length ≤ p → w.HasPeriod p
-- Mathlib.CategoryTheory.Grothendieck
/-- A natural isomorphism between functors `G ≅ H` induces a natural isomorphism between the canonical
morphism `pre F G` and `pre F H`, up to composition with
`Grothendieck (G ⋙ F) ⥤ Grothendieck (H ⋙ F)`.
 -/
CategoryTheory.Grothendieck.preNatIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
        (F : CategoryTheory.Functor C CategoryTheory.Cat) →
          {G H : CategoryTheory.Functor D C} →
            (α : G ≅ H) →
              CategoryTheory.Grothendieck.pre F G ≅
                (CategoryTheory.Grothendieck.map (CategoryTheory.Functor.whiskerRight α.hom F)).comp
                  (CategoryTheory.Grothendieck.pre F H)
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
/-- The characteristic function of a measure with all moments is `C^∞`. See `contDiff_charFun`
for the version proving only `C^n` by only assuming that the moment of order `n` exists.  -/
MeasureTheory.contDiff_charFun' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] {n : ℕ∞},
  (∀ (k : ℕ), MeasureTheory.MemLp id (↑k) μ) → ContDiff ℝ (↑n) (MeasureTheory.charFun μ)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace : ∀ (K : Type u_1) [inst : Field K], Function.Injective ⇑NumberField.mixedEmbedding.mixedSpaceOfRealSpace
-- Lean.Server.InfoUtils
/-- Try to retrieve `TacticInfo` for `hoverPos`.
We retrieve all `TacticInfo` nodes s.t. `hoverPos` is inside the node's range plus trailing whitespace.
We usually prefer the innermost such nodes so that for composite tactics such as `induction`, we show the nested proofs' states.
However, if `hoverPos` is after the tactic, we prefer nodes that are not indented relative to it, meaning that e.g. at `|` in
```lean
have := by
  exact foo
|
```
we show the (final, see below) state of `have`, not `exact`.

Moreover, we instruct the LSP server to use the state after tactic execution if
- the hover position is after the info's start position *and*
- there is no nested tactic info after the hover position (tactic combinators should decide for themselves
  where to show intermediate states by calling `withTacticInfoContext`)  -/
Lean.Elab.InfoTree.goalsAt? : Lean.FileMap → Lean.Elab.InfoTree → String.Pos.Raw → List Lean.Elab.GoalsAtResult
-- Std.Data.TreeMap.Basic
/-- Computes the union of the given tree maps. If a key appears in both maps, the entry contained in
the second argument will appear in the result.

This function always merges the smaller map into the larger map.
 -/
Std.TreeMap.union : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Std.TreeMap α β cmp → Std.TreeMap α β cmp
-- Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
/-- Second version, with pointwise equicontinuity and range in a compact subset.  -/
BoundedContinuousFunction.arzela_ascoli₂ : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [CompactSpace α] [inst_2 : PseudoMetricSpace β] (s : Set β),
  IsCompact s →
    ∀ (A : Set (BoundedContinuousFunction α β)),
      IsClosed A →
        (∀ (f : BoundedContinuousFunction α β) (x : α), f ∈ A → f x ∈ s) → (Equicontinuous fun x => ⇑↑x) → IsCompact A
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_refl_app : ∀ {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) (a : ℤ) (X : C),
  (t.natTransTruncLEOfLE a a ⋯).app X = CategoryTheory.CategoryStruct.id ((t.truncLE a).obj X)
-- Lean.Elab.Term.TermElabM
/-- Task for state after tactic execution.  -/
Lean.Elab.Tactic.TacticParsedSnapshotInner.finished : {α : Type} →
  Lean.Elab.Tactic.TacticParsedSnapshotInner α → Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticFinishedSnapshot
-- Mathlib.Data.NNReal.Defs
NNReal.coe_lt_coe : ∀ {r₁ r₂ : NNReal}, ↑r₁ < ↑r₂ ↔ r₁ < r₂
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- The natural group hom from an `AddSubgroup` of `AddGroup` `G` to `G`.  -/
AddSubgroup.subtype : {G : Type u_1} → [inst : AddGroup G] → (H : AddSubgroup G) → ↥H →+ G
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_one : Int8.toNatClampNeg 1 = 1
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instSMul.eq_1 : ∀ (M : Type v) (X : Type x) [inst : UniformSpace X] [inst_1 : SMul M X],
  UniformSpace.Completion.instSMul M X = { smul := fun c => UniformSpace.Completion.map fun x => c • x }
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.splitAtPred.match_3.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.reindex_hom_π : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C)
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.reindex ε f).hom (CategoryTheory.Limits.Pi.π f (ε b)) =
    CategoryTheory.Limits.Pi.π (f ∘ ⇑ε) b
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instInter : {α : Type u_1} → [inst : MeasurableSpace α] → Inter (Subtype MeasurableSet)
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.rightToLeft.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t t_1 : CategoryTheory.Adjunction.Triple F G H),
  t = t_1 → ∀ [inst_2 : G.Full] [inst_3 : G.Faithful], t.rightToLeft = t_1.rightToLeft
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.vaddConst_apply : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (b : P₁) (v : V₁), (AffineEquiv.vaddConst k b) v = v +ᵥ b
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.zero_notMem_coeffs : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R), 0 ∉ p.coeffs
-- Init.Grind.ToInt
Lean.Grind.IntInterval.mem_ii : ∀ (x : ℤ), x ∈ Lean.Grind.IntInterval.ii ↔ True
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_insert_right : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a ≤ b → insert b (Finset.Ico a b) = Finset.Icc a b
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- `LiftPropWithinAt P f s x` is equivalent to a definition where we restrict the set we are
considering to the domain of the charts at `x` and `f x`.  -/
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    ∀ {f : M → M'},
      ChartedSpace.LiftPropWithinAt P f s x ↔
        ContinuousWithinAt f s x ∧
          P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm)
            ((chartAt H x).target ∩ ↑(chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source)) (↑(chartAt H x) x)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Two left invariant measures integrate in the same way continuous compactly supported functions,
up to the scalar `addHaarScalarFactor μ' μ`. See also
`measure_isAddInvariant_eq_smul_of_isCompact_closure`, which gives the same result for compact
sets, and `measure_isAddHaarMeasure_eq_smul_of_isOpen` for open sets.  -/
MeasureTheory.Measure.integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsAddHaarMeasure]
  [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsAddLeftInvariant] {f : G → ℝ},
  Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.addHaarScalarFactor μ • μ
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.analyticOn_bilinear : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)),
  AnalyticOn 𝕜 (fun x => (f x.1) x.2) s
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R}
  (h : ModuleCat.of R (↑S.X₂ ⧸ (ModuleCat.Hom.hom S.f).range) ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.pOpcycles (CategoryTheory.CategoryStruct.comp S.moduleCatOpcyclesIso.hom h) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (ModuleCat.Hom.hom S.f).range.mkQ) h