mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Basic
_private.Init.Data.Iterators.Basic.0.Std.IterStep.successor.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Std.IterStep α β → Sort u_3) (it : α)
  (h_1 : (it : α) → (out : β) → motive (Std.IterStep.yield it out)) (h_2 : (it : α) → motive (Std.IterStep.skip it))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it with
    | Std.IterStep.yield it out => h_1 it out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_2 it
-- Mathlib.MeasureTheory.Function.Jacobian
/-- A differentiable function maps sets of measure zero to sets of measure zero.  -/
MeasureTheory.addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure],
  DifferentiableOn ℝ f s → μ s = 0 → μ (f '' s) = 0
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.diagram_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C), D.diagram.left = D.V
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.Xzero_subst_Xzero : ∀ {R : Type u_1} [inst : CommRing R] (F : FormalGroup R), PowerSeries.subst F.Xzero F.Xzero = F.Xzero
-- Mathlib.Data.FunLike.IsApply
IsOneApply.one_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : One β}
  {inst_2 : One F} [self : IsOneApply F α β] (x : α), 1 x = 1
-- Lean.DocString.Add
/-- Adds an elaborated Verso docstring to the environment, recording its `deferred` checks under this
declaration as their `site`.
 -/
Lean.addVersoDocStringCore : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [MonadLiftT BaseIO m] →
        [Lean.MonadError m] → Lean.Name → Lean.VersoDocString → Array Lean.Doc.DeferredCheck → m Unit
-- Mathlib.Algebra.Module.Basic
/-- If `E` is a vector space over a division semiring `R` and has a monoid action by `α`, then that
action commutes by scalar multiplication of inverses of natural numbers in `R`.  -/
inv_natCast_smul_comm : ∀ {α : Type u_5} {E : Type u_6} (R : Type u_7) [inst : AddCommMonoid E] [inst_1 : DivisionSemiring R]
  [inst_2 : Module R E] [inst_3 : DistribSMul α E] (n : ℕ) (s : α) (x : E), (↑n)⁻¹ • s • x = s • (↑n)⁻¹ • x
-- Init.Data.Int.Lemmas
Int.neg_sub : ∀ (a b : ℤ), -(a - b) = b - a
-- Mathlib.FieldTheory.IntermediateField.Basic
Subfield.mem_extendScalars : ∀ {L : Type u_2} [inst : Field L] {F E : Subfield L} (h : F ≤ E) {x : L}, x ∈ Subfield.extendScalars h ↔ x ∈ E
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    Std.DHashMap.Const.get? (Std.DHashMap.Const.insertMany m l) k = Std.DHashMap.Const.get? m k
-- Init.Data.String.Subslice
String.Slice.startInclusive_subslice : ∀ {s : String.Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd},
  (s.subslice newStart newEnd h).startInclusive = newStart
-- Mathlib.Data.List.TakeDrop
_private.Mathlib.Data.List.TakeDrop.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.coe_comp : ∀ {X Y Z : AddMagmaCat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.Order.Module.Defs
smul_one_mono : ∀ {α : Type u_1} (β : Type u_2) [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β]
  [inst_4 : One β] [ZeroLEOneClass β] [SMulPosMono α β], Monotone fun x => x • 1
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_iUnion : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_9}
  (s : ι → Set M), Submodule.span R (⋃ i, s i) = ⨆ i, Submodule.span R (s i)
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.conjExponent : ∀ {p : ENNReal}, 1 ≤ p → p.HolderConjugate p.conjExponent
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv : ∀ {p q n : ℕ}
  (z :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n })),
  z ∈
      (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
            (SSet.stdSimplex.obj { len := q })).nonDegenerate
        n ↔
    StrictMono ⇑(SSet.prodStdSimplex.objEquiv z)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.ext_col_iff : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {A B : Matrix m n α}, A = B ↔ ∀ (j : n), A.col j = B.col j
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Schwartz functions are in `L^∞`; does not require `hμ.HasTemperateGrowth`.  -/
SchwartzMap.memLp_top : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F]
  (f : SchwartzMap E F) (μ : autoParam (MeasureTheory.Measure E) SchwartzMap.memLp_top._auto_1),
  MeasureTheory.MemLp ⇑f ⊤ μ
-- Mathlib.Algebra.MvPolynomial.Rename
/-- Rename all the variables in a multivariable polynomial.  -/
MvPolynomial.rename : {σ : Type u_1} →
  {τ : Type u_2} → {R : Type u_4} → [inst : CommSemiring R] → (σ → τ) → MvPolynomial σ R →ₐ[R] MvPolynomial τ R
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_image2_le : ∀ {α β γ : Type u} {f : α → β → γ} {s : Set α} {t : Set β},
  Cardinal.mk ↑(Set.image2 f s t) ≤ Cardinal.mk ↑s * Cardinal.mk ↑t
-- Mathlib.Data.Set.Finite.Basic
/-- **Alias** of `Set.Infinite.sdiff`. -/
Set.Infinite.diff : ∀ {α : Type u} {s t : Set α}, s.Infinite → t.Finite → (s \ t).Infinite
-- Mathlib.CategoryTheory.GradedObject.Single
CategoryTheory.GradedObject.singleObjApplyIso_inv_single_map : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasInitial C] [inst_2 : DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j X).inv
      ((CategoryTheory.GradedObject.single j).map f j) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.GradedObject.singleObjApplyIso j Y).inv
-- Mathlib.Probability.Moments.Tilted
/-- The integral of `X` against the tilted measure `μ.tilted (t * X ·)` is the first derivative of
the cumulant-generating function of `X` at `t`.  -/
ProbabilityTheory.integral_tilted_mul_self : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    (∫ (x : Ω), X x ∂μ.tilted fun x => t * X x) = deriv (ProbabilityTheory.cgf X μ) t
-- Mathlib.CategoryTheory.GradedObject
/-- Pull back an `I`-graded object in `C` to a `J`-graded object along a function `J → I`.  -/
CategoryTheory.GradedObject.comap : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type u_1} →
      {J : Type u_2} →
        (J → I) → CategoryTheory.Functor (CategoryTheory.GradedObject I C) (CategoryTheory.GradedObject J C)
-- Init.Data.List.SplitOn.Lemmas
_private.Init.Data.List.SplitOn.Lemmas.0.List.splitOnPPrepend.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      ((acc : List α) → motive [] acc) → ((a : α) → (t acc : List α) → motive (a :: t) acc) → motive x x_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_insertManyIfNewUnit_emptyWithCapacity_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α} {k : α} {fallback : Unit},
  Std.DHashMap.Internal.Raw₀.Const.getD
      (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k
      fallback =
    ()
-- Init.Data.BitVec.Lemmas
BitVec.umod_eq_and : ∀ {x y : BitVec 1}, x % y = x &&& ~~~y
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- The continuous multilinear map on `A^ι`, where `A` is a normed commutative algebra
over `𝕜`, associating to `m` the product of all the `m i`.

See also `ContinuousMultilinearMap.mkPiAlgebraFin`.  -/
ContinuousMultilinearMap.mkPiAlgebra : (R : Type u) →
  (ι : Type v) →
    (A : Type u_1) →
      [Fintype ι] →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : TopologicalSpace A] → [ContinuousMul A] → ContinuousMultilinearMap R (fun x => A) A
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.add : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : Add β] [ContinuousAdd β],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (f + g) μ
-- Std.Http.Data.Status
Std.Http.Status.notAcceptable.sizeOf_spec : sizeOf Std.Http.Status.notAcceptable = 1
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.IsoCat.refl_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C],
  (CategoryTheory.IsoCat.refl C).functor = CategoryTheory.Functor.id C
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_eq_zero : ∀ {E : Type u_5} [inst : NormedAddGroup E] {a : E}, ‖a‖₊ = 0 ↔ a = 0
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.ExtraTheorem.const.injEq : ∀ (declName declName_1 : Lean.Name),
  (Lean.Elab.Tactic.Grind.ExtraTheorem.const declName = Lean.Elab.Tactic.Grind.ExtraTheorem.const declName_1) =
    (declName = declName_1)
-- Init.Data.String.Lemmas.Slice
String.Slice.front_eq : ∀ {s : String.Slice}, s.front = s.front?.getD default
-- Aesop.Rule
Aesop.Safety.safe : Aesop.Safety
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsLinearSet.closure_finset : ∀ {M : Type u_1} [inst : AddCommMonoid M] (s : Finset M), IsLinearSet ↑(AddSubmonoid.closure ↑s)
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_eq_ite : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Group α] {a : α} [MulLeftMono α], a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1
-- Mathlib.RingTheory.RingHom.Locally
/-- If `f` satisfies `P`, then in particular it satisfies `Locally P`.  -/
RingHom.locally_of : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {R S : Type u}
  [inst : CommRing R] [inst_1 : CommRing S],
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    ∀ (f : R →+* S), P f → RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => P) f
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.presheafEquivOfIso_counitIso_inv_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y)
  (X_1 : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) (X_2 : (TopologicalSpace.Opens ↑Y)ᵒᵖ),
  ((TopCat.Presheaf.presheafEquivOfIso C H).counitIso.inv.app X_1).app X_2 = X_1.map (CategoryTheory.eqToHom ⋯)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.mem_op : ∀ {G : Type u_2} [inst : AddGroup G] {x : Gᵃᵒᵖ} {S : AddSubgroup G}, x ∈ S.op ↔ AddOpposite.unop x ∈ S
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.finrank_submodule : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (v : Projectivization K V), Module.finrank K ↥v.submodule = 1
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepNormal.eq_5 : ∀ (f g : Turing.ToPartrec.Code),
  Turing.ToPartrec.stepNormal (f.comp g) = fun k v => Turing.ToPartrec.stepNormal g (Turing.ToPartrec.Cont.comp f k) v
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.mem_inf : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R} {x : R}, x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J
-- Mathlib.Topology.CompactOpen
ContinuousMap.isOpen_setOfPred_mapsTo : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {K : Set X} {U : Set Y},
  IsCompact K → IsOpen U → IsOpen {f | Set.MapsTo (⇑f) K U}
-- Lean.Meta.Tactic.Grind.Attr
_private.Lean.Meta.Tactic.Grind.Attr.0.Lean.Meta.Grind.Extension.eraseFunCCAttr : Lean.Meta.Grind.Extension → Lean.Name → Lean.CoreM Unit
-- Std.Time.DateTime.WallTime
/-- Adds a `Millisecond.Offset` to the given `WallTime`.
 -/
Std.Time.WallTime.addMilliseconds : Std.Time.WallTime → Std.Time.Millisecond.Offset → Std.Time.WallTime
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H] {D₁ : Type u₄}
  {D₂ : Type u₅} [inst_3 : CategoryTheory.Category.{v₄, u₄} D₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} D₂]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₁.IsLocalization W₁] [inst_6 : L₂.IsLocalization W₂] (F : CategoryTheory.Functor C₂ H)
  (F₁ : CategoryTheory.Functor D₁ H) (α₁ : Φ.functor.comp F ⟶ L₁.comp F₁) (F₂ : CategoryTheory.Functor D₂ H)
  (α₂ : F ⟶ L₂.comp F₂) [inst_7 : F₁.IsRightDerivedFunctor α₁ W₁],
  CategoryTheory.CategoryStruct.comp α₁ (L₁.whiskerLeft (Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂)) =
    CategoryTheory.CategoryStruct.comp (Φ.functor.whiskerLeft α₂)
      (CategoryTheory.CategoryStruct.comp (Φ.functor.associator L₂ F₂).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight
            (CategoryTheory.CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom F₂)
          (L₁.associator (Φ.localizedFunctor L₁ L₂) F₂).hom))
-- Mathlib.Tactic.ClickSuggestions.Apply
/-- Whether the two suggestions are duplicates of each other.  -/
Mathlib.Tactic.ClickSuggestions.ApplyKey.isDuplicate : Mathlib.Tactic.ClickSuggestions.ApplyKey → Mathlib.Tactic.ClickSuggestions.ApplyKey → Lean.MetaM Bool
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `NormedAddCommGroup E` instance from a `NormedSpace.Core`. Note that if this is
used to define an instance on a type, it also provides a new distance measure from the norm.
it must therefore not be used on a type with a preexisting distance measure.
See note [reducible non-instances].  -/
NormedAddCommGroup.ofCore : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] → [inst_3 : Norm E] → NormedSpace.Core 𝕜 E → NormedAddCommGroup E
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IccExtend_range : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) (f : ↑(Set.Icc a b) → β),
  Set.range (Set.IccExtend h f) = Set.range f
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_prod_of_isCoseparator_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (G H : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct G H],
  CategoryTheory.IsCoseparator G → CategoryTheory.IsCoseparator (G ⨯ H)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.isPlausibleOutput_iff : ∀ {α : Type u} {a : α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  {it : Std.Iter α}, it.IsPlausibleOutput a ↔ it.internalState.next = some a ∧ a < it.internalState.upperBound
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_univ : ∀ {R : Type u} [inst : NonAssocSemiring R], Subsemiring.closure Set.univ = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The retract of a bicone `B` given by `B.ι j` and `B.π j`.  -/
CategoryTheory.Limits.Bicone.retract : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → (B : CategoryTheory.Limits.Bicone F) → (j : J) → CategoryTheory.Retract (F j) B.pt
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.algebraMap_mk : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (a : R) (s : ↥S),
  (algebraMap (Localization S) (LocalizedModule S A)) (Localization.mk a s) = LocalizedModule.mk ((algebraMap R A) a) s
-- Aesop.Forward.State
/-- The premises that appear in the rule's conclusion. These are the same for
all cluster states of a rule, but are stored here for convenience.  -/
Aesop.ClusterState.conclusionDeps : Aesop.ClusterState → Array Aesop.PremiseIndex
-- Mathlib.Data.Finset.PImage
Finset.pimage_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f g : α →. β} [inst_1 : (x : α) → Decidable (f x).Dom]
  [inst_2 : (x : α) → Decidable (g x).Dom] {s t : Finset α},
  s = t → (∀ x ∈ t, f x = g x) → Finset.pimage f s = Finset.pimage g t
-- Mathlib.Algebra.Group.PNatPowAssoc
/-- A `Prop`-valued mixin for power-associative multiplication in the non-unital setting.  -/
PNatPowAssoc : (M : Type u_2) → [Mul M] → [Pow M ℕ+] → Prop
-- Batteries.Lean.AttributeExtra
Lean.TagAttributeExtra.mk.sizeOf_spec : ∀ (ext : Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet) (base : Lean.NameHashSet),
  sizeOf { ext := ext, base := base } = 1 + sizeOf ext + sizeOf base
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_3.splitter : {m : Type u_1 → Type u_2} →
  {α β : Type u_1} →
    [inst : Std.Iterator α m β] →
      (it : Std.IterM m β) →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_counitIso_inv_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).counitIso.inv.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Order.Directed
exists_lt_of_directed_ge : ∀ (β : Type u_2) [inst : PartialOrder β] [Nontrivial β] [IsCodirectedOrder β], ∃ a b, a < b
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The coequalizer of `(f, g)`, where `f = g`, is an isomorphism.  -/
CategoryTheory.Limits.coequalizer.π_of_eq : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g],
  f = g → CategoryTheory.IsIso (CategoryTheory.Limits.coequalizer.π f g)
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasStrictFDerivAt_natCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : NatCast F] (n : ℕ) (x : E), HasStrictFDerivAt (↑n) 0 x
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_eq_singleton_append : ∀ {n : ℕ}, 0 < n → (*...n).toArray = #[0] ++ (1...n).toArray
-- Mathlib.Data.TypeVec
/-- append an arrow and a function as well as their respective source and target types / typevecs  -/
TypeVec.«term_:::__1» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.Quot.desc_quotQuotUliftAddEquiv : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J] (c : CategoryTheory.Limits.Cocone F),
  (AddCommGrpCat.Colimits.Quot.desc (F.comp AddCommGrpCat.uliftFunctor) (AddCommGrpCat.uliftFunctor.mapCocone c)).comp
      (AddCommGrpCat.Colimits.quotQuotUliftAddEquiv F).toAddMonoidHom =
    AddEquiv.ulift.symm.toAddMonoidHom.comp (AddCommGrpCat.Colimits.Quot.desc F c)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.isTrail : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsPath → p.IsTrail
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (n : ℕ) (X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ),
  (CategoryTheory.ComposableArrows.opEquivalence C n).unitIso.hom.app X =
    CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.funInvIdAssoc
            (Opposite.unop X)).hom.op
      ((⋯.functor.comp (CategoryTheory.orderDualEquivalence (Fin (n + 1))).functor).whiskerLeft
          (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).inverse.comp ⋯.functor).comp
                    (Opposite.unop X)).rightOpLeftOpIso.hom.op.unop).op
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous.comp_uniformContinuousOn : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f : α → β} {s : Set α} {g : β → γ}, UniformContinuous g → UniformContinuousOn f s → UniformContinuousOn (g ∘ f) s
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.stableUnderComposition : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.IsSeparated
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_empty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {a : α},
  Std.DTreeMap.Internal.Impl.contains a Std.DTreeMap.Internal.Impl.empty = false
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.hasPushout_unop_iff_hasPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.Limits.HasPushout f.unop g.unop ↔ CategoryTheory.Limits.HasPullback f g
-- Mathlib.Analysis.Normed.Module.Basic
instSeminormedAddCommGroupRestrictScalars : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} → {E : Type u_3} → [I : SeminormedAddCommGroup E] → SeminormedAddCommGroup (RestrictScalars 𝕜 𝕜' E)
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.iIndepFun.charFunDual_map_fun_sum_eq_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {E : Type u_3}
  [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E}
  [inst_4 : Fintype ι] [inst_5 : NormedSpace ℝ E],
  (∀ (i : ι), AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun X P →
      MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) P) =
        ∏ i, MeasureTheory.charFunDual (MeasureTheory.Measure.map (X i) P)
-- Batteries.Data.Fin.Lemmas
Fin.isNone_of_isNone_findSomeRev? : ∀ {n : ℕ} {α : Type u_1} {i : Fin n} {f : Fin n → Option α}, (Fin.findSomeRev? f).isNone = true → (f i).isNone = true