mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Iterate
String.Slice.Model.map_get_positionsFrom_startPos : ∀ {s : String.Slice}, List.map (fun p => (↑p).get ⋯) (String.Slice.Model.positionsFrom s.startPos) = s.copy.toList
-- Batteries.Data.List.Lemmas
List.getElem_getElem_idxsOf_of_lawful : ∀ {α : Type u_1} {i : ℕ} {xs : List α} {x : α} [inst : BEq α] [LawfulBEq α] (h : i < (List.idxsOf x xs).length),
  xs[(List.idxsOf x xs)[i]] = x
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue.mapCodeM : {m : Type → Type u_1} →
  {pu : Lean.Compiler.LCNF.Purity} →
    [Monad m] →
      (Lean.Compiler.LCNF.Code pu → m (Lean.Compiler.LCNF.Code pu)) →
        Lean.Compiler.LCNF.DeclValue pu → m (Lean.Compiler.LCNF.DeclValue pu)
-- Mathlib.Algebra.Group.Prod
/-- `Prod.map` as an `AddMonoidHom`  -/
AddHom.prodMap : {M : Type u_3} →
  {N : Type u_4} →
    {M' : Type u_6} →
      {N' : Type u_7} →
        [inst : Add M] →
          [inst_1 : Add N] → [inst_2 : Add M'] → [inst_3 : Add N'] → (M →ₙ+ M') → (N →ₙ+ N') → M × N →ₙ+ M' × N'
-- Mathlib.Algebra.Lie.Subalgebra
/-- Given nested Lie subalgebras `K ⊆ K'`, there is a natural equivalence from `K` to its image in
`K'`.  -/
LieSubalgebra.equivOfLe : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] → {K K' : LieSubalgebra R L} → (h : K ≤ K') → ↥K ≃ₗ⁅R⁆ ↥(LieSubalgebra.ofLe h)
-- Mathlib.Data.PNat.Basic
Nat.succPNat_inj : ∀ {n m : ℕ}, n.succPNat = m.succPNat ↔ n = m
-- Mathlib.Data.Set.Basic
Set.inter_inter_distrib_left : ∀ {α : Type u} (s t u : Set α), s ∩ (t ∩ u) = s ∩ t ∩ (s ∩ u)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.hom_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  (Φ₁ Φ₂ : S₁ ⟶ S₂), (∀ (n : ℕ), Φ₁.f n = Φ₂.f n) → Φ₁ = Φ₂
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
/-- A `SymmetricAlgebra` over a nontrivial semiring is nontrivial.  -/
SymmetricAlgebra.instNontrivial : ∀ {R : Type u_1} (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R],
  Nontrivial (SymmetricAlgebra R M)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- `K` and `Kᗮ` have trivial intersection.  -/
ClosedSubmodule.orthogonal_disjoint : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : ClosedSubmodule 𝕜 E), Disjoint K Kᗮ
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.length_digits_le_length_digits_succ : ∀ (b n : ℕ), (b.digits n).length ≤ (b.digits (n + 1)).length
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- The quoted dimension expression from the reified determinant call.  -/
Mathlib.Tactic.Determinant.Ctx.dimensionLit : {u : Lean.Level} → {α : Q(Type u)} → {rα : Q(CommRing «$α»)} → Mathlib.Tactic.Determinant.Ctx rα → Q(ℕ)
-- Mathlib.Algebra.Module.Submodule.EqLocus
LinearMap.eqOn_sup : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {F : Type u_5} [inst_6 : FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f g : F} {S T : Submodule R M},
  Set.EqOn ⇑f ⇑g ↑S → Set.EqOn ⇑f ⇑g ↑T → Set.EqOn ⇑f ⇑g ↑(S ⊔ T)
-- Mathlib.Algebra.Group.Units.Equiv
/-- In a `DivisionCommMonoid`, `Equiv.inv` is a `MulEquiv`. There is a variant of this
`MulEquiv.inv' G : G ≃* Gᵐᵒᵖ` for the non-commutative case.  -/
MulEquiv.inv : (G : Type u_6) → [inst : DivisionCommMonoid G] → G ≃* G
-- Mathlib.Data.Finite.Prod
Set.finite_prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅)
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'_assoc : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ i₅ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (hi₄₅ : i₄ ≤ i₅) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'._auto_3) {Z : C}
  (h :
    X'.E (CategoryTheory.homOfLE hi₁₂) (CategoryTheory.homOfLE hi₂₃) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) h) =
    CategoryTheory.CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯ n₀ n₁ n₂ hn₁ hn₂) h)
-- Mathlib.Order.Basic
/-- **Alias** of `eq_of_le_of_not_lt`. -/
LE.le.eq_of_not_lt : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≤ b → ¬a < b → a = b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.fst_app : ∀ {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.CartesianMonoidalCategory C]
  (F₁ F₂ : CategoryTheory.Functor J C) (j : J),
  (CategoryTheory.SemiCartesianMonoidalCategory.fst F₁ F₂).app j =
    CategoryTheory.SemiCartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
/-- `QuadraticAlgebra.equivTuple` as a `LinearEquiv`  -/
QuadraticAlgebra.linearEquivTuple : {R : Type u_1} → (a b : R) → [inst : Semiring R] → QuadraticAlgebra R a b ≃ₗ[R] Fin 2 → R
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- An element is in `pinGroup Q` if and only if it is in `lipschitzGroup Q` and `unitary`.  -/
pinGroup.mem_iff : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q},
  x ∈ pinGroup Q ↔
    x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ∧
      x ∈ unitary (CliffordAlgebra Q)
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_nonneg : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  0 ≤ Int.fract a
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_lt_iff : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderTop α] {s : Finset ι} {f : ι → α} {a : α},
  s.inf f < a ↔ ∃ b ∈ s, f b < a
-- Mathlib.Combinatorics.Derangements.Finite
numDerangements_sum : ∀ (n : ℕ), ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.coproductCocone_ι : ∀ (A B : CommRingCat),
  (A.coproductCocone B).ι =
    {
      app := fun x =>
        match x.as with
        | CategoryTheory.Limits.WalkingPair.left => CommRingCat.ofHom ↑Algebra.TensorProduct.includeLeft
        | CategoryTheory.Limits.WalkingPair.right => CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight,
      naturality := ⋯ }
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- An ordered finpartition gives an equivalence between `Fin n` and the disjoint union of the
parts, each of them parameterized by `Fin (c.partSize i)`.  -/
OrderedFinpartition.equivSigma : {n : ℕ} → (c : OrderedFinpartition n) → (i : Fin c.length) × Fin (c.partSize i) ≃ Fin n
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.isIso_iff_isOpenImmersion_and_epi_base : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  CategoryTheory.IsIso f ↔ AlgebraicGeometry.IsOpenImmersion f ∧ CategoryTheory.Epi f.base
-- Lean.Meta.Tactic.Grind.Inv
_private.Lean.Meta.Tactic.Grind.Inv.0.Lean.Meta.Grind.checkMatchCondParent : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.instInhabitedFunIndInfo : Inhabited Lean.Meta.FunIndInfo
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
Real.summable_log_one_add_of_summable : ∀ {ι : Type u_1} {f : ι → ℝ}, Summable f → Summable fun i => Real.log (1 + f i)
-- Mathlib.RingTheory.DedekindDomain.PID
/-- A Dedekind domain is a PID if its set of maximal ideals is finite.  -/
IsPrincipalIdealRing.of_finite_maximals : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R], {I | I.IsMaximal}.Finite → IsPrincipalIdealRing R
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.eqToHom.hcongr_5 : ∀ (C C' : Type u₁),
  C = C' →
    ∀ (inst : CategoryTheory.CategoryStruct.{v₁, u₁} C) (inst' : CategoryTheory.CategoryStruct.{v₁, u₁} C'),
      inst ≍ inst' →
        ∀ (X : C) (X' : C'),
          X ≍ X' →
            ∀ (Y : C) (Y' : C'),
              Y ≍ Y' → ∀ (p : X = Y) (p' : X' = Y'), p ≍ p' → CategoryTheory.eqToHom p ≍ CategoryTheory.eqToHom p'
-- Mathlib.Order.Sublocale
Sublocale.toNucleus_le_toNucleus : ∀ {X : Type u_1} [inst : Order.Frame X] {S T : Sublocale X}, S.toNucleus ≤ T.toNucleus ↔ T ≤ S
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.d_stepk_certC.eq_1 : ∀ (k₁ : ℤ) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂ p : Lean.Grind.CommRing.Poly)
  (c : ℕ),
  Lean.Grind.CommRing.Stepwise.d_stepk_certC k₁ p₁ k₂ m₂ p₂ p c =
    p.beq' ((Lean.Grind.CommRing.Poly.mulConstC k₁ p₁ c).combineC (Lean.Grind.CommRing.Poly.mulMonC k₂ m₂ p₂ c) c)
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.missingDocs : Lean.Linter
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.extend_of_empty : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {δ : Type u_2}
  [inst_2 : TopologicalSpace δ] [inst_3 : DiscreteTopology δ] [IsEmpty α] (f : α ↪ δ)
  (g : BoundedContinuousFunction α β) (h : BoundedContinuousFunction δ β), BoundedContinuousFunction.extend f g h = h
-- Init.Internal.Order.Lemmas
Lean.Order.List.monotone_foldlM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → β → α → m β) (init : β) (xs : List α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => List.foldlM (f x) init xs
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_eq_get_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.minKey he = t.minKey?.get ⋯
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k : α} {f : β → β},
      Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.Const.modify m k f) k =
        Option.map f (Std.DHashMap.Internal.Raw₀.Const.get? m k)
-- Mathlib.CategoryTheory.Sites.JointlySurjective
CategoryTheory.Types.instHasIsosJointlySurjectivePrecoverage : CategoryTheory.Types.jointlySurjectivePrecoverage.HasIsos
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_alter_eq_sub_one : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∈ m → (f (Std.DHashMap.Const.get? m k)).isNone = true → (Std.DHashMap.Const.alter m k f).size = m.size - 1
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The canonical bijection `(stdSimplex.obj n ⟶ X) ≃ X.obj (op n)`.  -/
SSet.yonedaEquiv : {X : SSet} → {n : SimplexCategory} → (SSet.stdSimplex.obj n ⟶ X) ≃ X.obj (Opposite.op n)
-- Init.WF
WellFounded.fixF_eq : ∀ {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α)
  (acx : Acc r x), WellFounded.fixF F x acx = F x fun y p => WellFounded.fixF F y ⋯
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
/-- Application of a natural transformation at a fixed object,
as group homomorphism  -/
CategoryTheory.NatTrans.appHom : {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] →
        [inst_2 : CategoryTheory.Preadditive D] →
          {F G : CategoryTheory.Functor C D} → (X : C) → (F ⟶ G) →+ (F.obj X ⟶ G.obj X)
-- Init.Data.Int.LemmasAux
Int.toNat_lt' : ∀ {m : ℤ} {n : ℕ}, 0 < n → (m.toNat < n ↔ m < ↑n)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.enum_le_enum : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {o₁ o₂ : ↑(Set.Iio (Ordinal.type r))},
  ¬r ((Ordinal.enum r) o₁) ((Ordinal.enum r) o₂) ↔ o₂ ≤ o₁
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_ric_eq_none_iff : ∀ {n i : ℕ}, (*...=n).toArray[i]? = none ↔ n < i
-- Mathlib.Algebra.Order.Group.Indicator
Function.mulSupport_sup : ∀ {α : Type u_2} {M : Type u_3} [inst : One M] [inst_1 : SemilatticeSup M] (f g : α → M),
  (Function.mulSupport fun x => f x ⊔ g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
-- Mathlib.Tactic.Ring.Basic
/-- Applies `Int.cast` to an int polynomial to produce a polynomial in `α`.

* `↑0 = 0`
* `↑(a + b) = ↑a + ↑b`
 -/
Mathlib.Tactic.Ring.ExSum.evalIntCast : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {v : Lean.Level} →
        {β : Q(Type v)} →
          (sβ : Q(CommSemiring «$β»)) →
            {a : Q(ℤ)} →
              (rα : Q(CommRing «$α»)) →
                Mathlib.Tactic.Ring.ExSum sβ a →
                  Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.ExSum sα) q(↑«$a»))
-- Mathlib.GroupTheory.Commensurable
Subgroup.Commensurable.trans : ∀ {G : Type u_1} [inst : Group G] {H K L : Subgroup G}, H.Commensurable K → K.Commensurable L → H.Commensurable L
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.leftDistrib : FirstOrder.Field.FieldAxiom
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The family of objects `B x.i` parametrized by `x : FunctorObjIndex f πX`.  -/
CategoryTheory.SmallObject.functorObjTgtFamily : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) → {S X : C} → (πX : X ⟶ S) → CategoryTheory.SmallObject.FunctorObjIndex f πX → C
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map f =
    CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk
      (CategoryTheory.MorphismProperty.LeftFraction.ofHom W f)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.toCycles_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp S.toCycles S.iCycles = S.f
-- Mathlib.Computability.TuringDegree
/-- `f` is Turing reducible to `g` if `f` is partial recursive given access to the oracle `g`
 -/
TuringReducible : (ℕ →. ℕ) → (ℕ →. ℕ) → Prop
-- Std.Data.DHashMap.Internal.AssocList.Basic
_private.Std.Data.DHashMap.Internal.AssocList.Basic.0.Std.DHashMap.Internal.AssocList.forInStep.go : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      {m : Type w → Type w'} →
        [Monad m] → ((a : α) → β a → δ → m (ForInStep δ)) → Std.DHashMap.Internal.AssocList α β → δ → m (ForInStep δ)
-- Mathlib.Topology.Constructions.SumProd
/-- The product of two dense sets is a dense set.  -/
Dense.prod : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
  Dense s → Dense t → Dense (s ×ˢ t)
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandElaboratingSnapshot.mk.sizeOf_spec : ∀ (toSnapshot : Lean.Language.Snapshot) (elabSnap : Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot)
  (resultSnap : Lean.Language.SnapshotTask Lean.Language.Lean.CommandResultSnapshot)
  (infoTreeSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf)
  (reportSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotTree),
  sizeOf
      { toSnapshot := toSnapshot, elabSnap := elabSnap, resultSnap := resultSnap, infoTreeSnap := infoTreeSnap,
        reportSnap := reportSnap } =
    1 + sizeOf toSnapshot + sizeOf elabSnap + sizeOf resultSnap + sizeOf infoTreeSnap + sizeOf reportSnap
-- Mathlib.Geometry.Euclidean.Volume.Measure
/-- Euclidean Hausdorff measure `μHE[d]`, defined as `μH[d]` scaled to agree with Lebesgue measure
on a `d`-dimensional Euclidean space. While this is defined on any (e)metric space, it is intended
to be used for affine space associated with an inner product space, where it agrees with the volume
measure on the inner product space.
 -/
MeasureTheory.«termμHE[_]» : Lean.ParserDescr
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.drain_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  it.drain = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, property⟩ => it'.drain
      | ⟨Std.IterStep.skip it', property⟩ => it'.drain
      | ⟨Std.IterStep.done, property⟩ => pure PUnit.unit
-- Mathlib.CategoryTheory.Limits.Creates
/-- Satisfy the inhabited linter  -/
CategoryTheory.inhabitedLiftableCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {K : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cone (K.comp (CategoryTheory.Functor.id C))) →
            Inhabited (CategoryTheory.LiftableCone K (CategoryTheory.Functor.id C) c)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.symm_toHomeomorph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n),
  h.symm.toHomeomorph = h.toHomeomorph.symm
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.coe_zero : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {σ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] [inst_8 : Subsingleton M]
  [inst_9 : Subsingleton M₂], ⇑0 = 0
-- Batteries.Data.List.Lemmas
List.length_replaceF : ∀ {α : Type u_1} {f : α → Option α} {l : List α}, (List.replaceF f l).length = l.length
-- Init.Prelude
Lean.Macro.instInhabitedMethods : Inhabited Lean.Macro.Methods
-- Lean.Namespace
/-- Map from namespace name to (max) visibility of (any) defining module. Namespaces do not have
visibility of their own. We use this information to avoid redeclaring namespaces that would always
be provided by an import anyway.
 -/
_private.Lean.Namespace.0.Lean.State : Type
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.IsRegular.wf : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} [self : P.IsRegular], WellFounded P.AncestralRel
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_eq_get_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.maxKey he = t.maxKey?.get ⋯
-- Mathlib.Algebra.Group.Defs
/-- A `SubtractionMonoid` is a `SubNegMonoid` with involutive negation and such that
`-(a + b) = -b + -a` and `a + b = 0 → -a = b`.  -/
SubtractionMonoid : Type u → Type u
-- Init.Data.Float.Float32
/-- Computes the hyperbolic arc cosine (inverse cosine) of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`acoshf`.
 -/
Float32.acosh : Float32 → Float32
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.res_length : ∀ {α : Type u_2} (x : ℕ → α) (n : ℕ), (PiNat.res x n).length = n
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_tilted : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable (fun x => Real.exp (f x)) μ → ∀ (g : α → ℝ), (μ.tilted f).tilted g = μ.tilted (f + g)
-- Mathlib.Analysis.Analytic.Constructions
/-- Finite products of analytic functions are analytic  -/
Finset.analyticAt_fun_prod : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_9} [inst_3 : NormedCommRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : α → E → A}
  {c : E} (N : Finset α), (∀ n ∈ N, AnalyticAt 𝕜 (f n) c) → AnalyticAt 𝕜 (fun z => ∏ n ∈ N, f n z) c
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.ncard_rootSet_le : ∀ {A : Type u_1} [inst : CommRing A] (p : Polynomial A) (B : Type u_3) [inst_1 : CommRing B] [inst_2 : IsDomain B]
  [inst_3 : Algebra A B], (p.rootSet B).ncard ≤ p.natDegree
-- Mathlib.Algebra.Order.Nonneg.Basic
/-- The function `a ↦ max a 0` of type `α → {x : α // 0 ≤ x}`.  -/
Nonneg.toNonneg : {α : Type u_1} → [inst : Zero α] → [inst_1 : SemilatticeSup α] → α → { x // 0 ≤ x }
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `neg_apply`. -/
ModularForm.neg_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Neg β}
  {inst_2 : Neg F} [self : IsNegApply F α β] (f : F) (x : α), (-f) x = -f x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.mem_toList_iff_mem : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerableLT α] {a : α}, a ∈ r.toList ↔ a ∈ r
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.inr : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β], Isometry ⇑(AddMonoidHom.inr α β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryLE?_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α}, Std.DTreeMap.Internal.Impl.Const.getEntryLE? k t₁ = Std.DTreeMap.Internal.Impl.Const.getEntryLE? k t₂
-- Std.Async.Basic
/-- An asynchronous computation that never fails.
 -/
Std.Async.BaseAsync : Type → Type
-- Mathlib.Order.Category.BddLat
BddLat.instInhabited : Inhabited BddLat
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_const' : ∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] [Nonempty α] (T : Set α → F →L[ℝ] F') (x : F)
  {m : MeasurableSpace α},
  MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.SimpleFunc.const α x) = (T Set.univ) x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_append_eq_support_dropLast_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (p' : G.Walk v w),
  (p.append p').support = p.support.dropLast ++ p'.support