mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Free
/-- Given an exact sequence `X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` of `R`-modules and spanning
families `v : ι → X₁` and `w : ι' → X₃`, we get a spanning family `ι ⊕ ι' → X₂`  -/
ModuleCat.span_rightExact : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.Exact →
    ∀ {v : ι → ↑S.X₁} {w : ι' → ↑S.X₃},
      ⊤ ≤ Submodule.span R (Set.range v) →
        ⊤ ≤ Submodule.span R (Set.range w) →
          CategoryTheory.Epi S.g →
            ⊤ ≤
              Submodule.span R
                (Set.range
                  (Sum.elim (⇑(CategoryTheory.ConcreteCategory.hom S.f) ∘ v)
                    (Function.invFun (ModuleCat.Hom.hom S.g).toFun ∘ w)))
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The value of a cochain on a triplet `⟨p, q, hpq⟩`.  -/
CochainComplex.HomComplex.Cochain.v : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        {n : ℤ} → CochainComplex.HomComplex.Cochain F G n → (p q : ℤ) → p + n = q → (F.X p ⟶ G.X q)
-- Mathlib.Data.List.Permutation
List.permutations_append : ∀ {α : Type u_1} (is ts : List α),
  (is ++ ts).permutations = List.map (fun x => x ++ ts) is.permutations ++ ts.permutationsAux is.reverse
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  DifferentiableWithinAt 𝕜 f s x →
    DifferentiableWithinAt 𝕜 g s x → derivWithin (f - g) s x = derivWithin f s x - derivWithin g s x
-- Mathlib.Algebra.Order.Star.Basic
IsSelfAdjoint.of_nonneg : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x : R}, 0 ≤ x → IsSelfAdjoint x
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.support_nodup : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCycle → p.support.tail.Nodup
-- Mathlib.Analysis.Complex.RealDeriv
HasDerivAt.complexToReal_fderiv : ∀ {f : ℂ → ℂ} {f' x : ℂ}, HasDerivAt f f' x → HasFDerivAt f (f' • 1) x
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoX₂_inv_hom_id : ∀ {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] (hg : S.g = 0),
  CategoryTheory.CategoryStruct.comp (S.cyclesIsoX₂ hg).inv S.iCycles = CategoryTheory.CategoryStruct.id S.X₂
-- Batteries.Data.Array.Merge
/-- Auxiliary definition for `mergeAdjacentDups`.  -/
Array.mergeAdjacentDups.go : {α : Type u_1} → [eq : BEq α] → (α → α → α) → Array α → Array α → ℕ → α → Array α
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (n : ℤ),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor = CategoryTheory.shiftFunctor Cᵒᵖ n
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.instIsIsoEImageMonoFactorisationOfHasZeroObjectOfMonoOfCoimageImageComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f]
  [CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)],
  CategoryTheory.IsIso (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).e
-- Mathlib.RingTheory.MatrixAlgebra
MatrixEquivTensor.right_inv : ∀ (n : Type u_3) (R : Type u_5) (A : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] (M : Matrix n n A),
  (MatrixEquivTensor.toFunAlgHom n R A) (MatrixEquivTensor.invFun n R A M) = M
-- Mathlib.Order.Hom.WithTopBot
/-- The coercion `α → WithTop α` bundled as monotone map.  -/
WithTop.coeOrderHom : {α : Type u_4} → [inst : Preorder α] → α ↪o WithTop α
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.CoPolarization_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι],
  P.CoPolarization = P.flip.Polarization
-- Mathlib.Analysis.Convex.Mul
/-- `x^n`, `n : ℕ` is convex on `[0, +∞)` for all `n`.  -/
convexOn_pow : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (n : ℕ),
  ConvexOn 𝕜 (Set.Ici 0) fun x => x ^ n
-- Mathlib.SetTheory.Ordinal.Notation
ONote.zero_def : ONote.zero = 0
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalRingHom.range_eq_map : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S),
  f.range = NonUnitalSubring.map f ⊤
-- Lean.Parser.Types
Lean.Parser.ParserState.stackSize : Lean.Parser.ParserState → ℕ
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSpanningSubgraph.banana_mono : ∀ {α : Type u_1} {β : Type u_2} {u v : α} {F₁ F₂ : Set β}, F₁ ⊆ F₂ → Graph.banana u v F₁ ≤s Graph.banana u v F₂
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- Predicate for a comonoid object to be commutative.  -/
CategoryTheory.IsCommComonObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → (X : C) → [CategoryTheory.ComonObj X] → Prop
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- A choice of octahedron' given by the octahedron axiom.  -/
CategoryTheory.Triangulated.someOctahedron' : {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] →
              [CategoryTheory.IsTriangulated C] →
                {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                  {u₁₂ : X₁ ⟶ X₂} →
                    {u₂₃ : X₂ ⟶ X₃} →
                      {u₁₃ : X₁ ⟶ X₃} →
                        (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) →
                          {v₁₂ : Z₁₂ ⟶ X₁} →
                            {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂} →
                              (h₁₂ :
                                  CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈
                                    CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                {v₂₃ : Z₂₃ ⟶ X₂} →
                                  {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃} →
                                    (h₂₃ :
                                        CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈
                                          CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                      {v₁₃ : Z₁₃ ⟶ X₁} →
                                        {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃} →
                                          (h₁₃ :
                                              CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈
                                                CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                            CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃
-- Mathlib.Algebra.Group.Action.Defs
AddSemigroupAction.ext : ∀ {G : Type u_9} {P : Type u_10} {inst : AddSemigroup G} {x y : AddSemigroupAction G P}, VAdd.vadd = VAdd.vadd → x = y
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNorm_mulLeftRight_le : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R],
  ‖ContinuousLinearMap.mulLeftRight 𝕜 R‖ ≤ 1
-- Mathlib.Data.Multiset.Lattice
Multiset.sup_dedup : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] (s : Multiset α),
  s.dedup.sup = s.sup
-- Mathlib.CategoryTheory.EssentialImage
/-- The essential image of a functor, interpreted as a full subcategory of the target category.  -/
CategoryTheory.Functor.EssImageSubcategory : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Type u₂
-- Mathlib.RingTheory.Coalgebra.Basic
Finsupp.comul_comp_lapply : ∀ (R : Type u) (ι : Type v) (A : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] (i : ι),
  CoalgebraStruct.comul ∘ₗ Finsupp.lapply i =
    TensorProduct.map (Finsupp.lapply i) (Finsupp.lapply i) ∘ₗ CoalgebraStruct.comul
-- Mathlib.Order.Atoms
/-- **Alias** of `IsSimpleOrder.eq_bot_of_lt`. -/
LT.lt.eq_bot : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α] {a b : α}, a < b → a = ⊥
-- Std.Http.Data.Status
/-- 402 Payment Required
 -/
Std.Http.Status.paymentRequired : Std.Http.Status
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.instSubsingleton : ∀ {α : Type u₁} [Subsingleton α], Subsingleton (CategoryTheory.Discrete α)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
/-- `N ≤r M` means that `N` is a `Restriction` of `M`.  -/
Matroid.«term_≤r_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_right_pointReflection : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (𝕜 : Type u_5) [inst_3 : NormedField 𝕜] [NormedSpace 𝕜 V] (p q : P),
  dist q ((Equiv.pointReflection p) q) = ‖2‖ * dist p q
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.contains.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.contains k Std.DTreeMap.Internal.Impl.leaf = false
-- Init.Data.String.Lemmas.TakeDrop
String.toList_copy_dropEnd : ∀ {s : String} {n : ℕ}, (s.dropEnd n).copy.toList = List.take (s.toList.length - n) s.toList
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.rightUnitor_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_2 : CategoryTheory.Limits.HasInitial C] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id (⊥_ C)))
      (CategoryTheory.Limits.coprod.rightUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.rightUnitor X).hom f
-- Mathlib.Algebra.Group.Irreducible.Lemmas
irreducible_mul_units : ∀ {M : Type u_2} [inst : Monoid M] {y : M} (u : Mˣ), Irreducible (y * ↑u) ↔ Irreducible y
-- Mathlib.Topology.Algebra.MulAction
/-- Eta-expanded form of `Continuous.smul` -/
Continuous.fun_smul : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [ContinuousSMul M X] {f : Y → M} {g : Y → X},
  Continuous f → Continuous g → Continuous fun i => f i • g i
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.fold.eq_2 : ∀ {α : Type u} (x : α) (n : ℕ) (f : (i : ℕ) → i < n.succ → α → α), n.succ.fold f x = f n ⋯ (n.fold (fun i h => f i ⋯) x)
-- Mathlib.LinearAlgebra.Dimension.Basic
Module.exists_set_linearIndependent_of_lt_rank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {c : Cardinal.{v}},
  c < Module.rank R M → ∃ s, Cardinal.mk ↑s = c ∧ LinearIndepOn R id s
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.instAddCommMonoid : {R : Type u_1} →
  [inst : LinearOrder R] → [inst_1 : CommRing R] → [inst_2 : IsStrictOrderedRing R] → AddCommMonoid (ArchimedeanClass R)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpInd.congr_simp : ∀ {α : Type u_1} (G : Type u_4) [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m m0 : MeasurableSpace α}
  (hm : m ≤ m0) (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (s s_1 : Set α),
  s = s_1 → MeasureTheory.condExpInd G hm μ s = MeasureTheory.condExpInd G hm μ s_1
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.subset_pointwise_smul_iff : ∀ {M : Type u_1} {R : Type u_3} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S T : Ideal R}, S ≤ a • T ↔ a⁻¹ • S ≤ T
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.mk.injEq : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (toLinearEquiv : M₁ ≃ₗ[R] M₂)
  (map_app' : ∀ (m : M₁), Q₂ ((↑toLinearEquiv).toFun m) = Q₁ m) (toLinearEquiv_1 : M₁ ≃ₗ[R] M₂)
  (map_app'_1 : ∀ (m : M₁), Q₂ ((↑toLinearEquiv_1).toFun m) = Q₁ m),
  ({ toLinearEquiv := toLinearEquiv, map_app' := map_app' } =
      { toLinearEquiv := toLinearEquiv_1, map_app' := map_app'_1 }) =
    (toLinearEquiv = toLinearEquiv_1)
-- Mathlib.Algebra.Order.Group.PosPart
inv_le_leOnePart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] (a : α), a⁻¹ ≤ a⁻ᵐ
-- Lean.Parser.Term
/-- Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
inherited. If `e` is itself a variable called `x`, it can be elided:
`fun y => { x := 1, y }`.
A *structure update* of an existing value can be given via `with`:
`{ point with x := 1 }`.
The structure type can be specified if not inferable:
`{ x := 1, y := 2 : Point }`.
 -/
Lean.Parser.Term.structInst : Lean.Parser.Parser
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.associator_def : ∀ {R : Type u} [inst : CommRing R] (M N K : ModuleCat R),
  CategoryTheory.MonoidalCategoryStruct.associator M N K = (TensorProduct.assoc R ↑M ↑N ↑K).toModuleIso
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
/-- **Alias** of `ModelWithCorners.contMDiff`. -/
contMDiff_model : ∀ {𝕜 : 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 ℕ∞},
  ContMDiff I (modelWithCornersSelf 𝕜 E) n ↑I
-- Mathlib.Analysis.Convex.PathConnected
Path.eqOn_extend_segment : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [inst_3 : ContinuousAdd E]
  [inst_4 : ContinuousSMul ℝ E] (a b : E), Set.EqOn (⇑(Path.segment a b).extend) (⇑(AffineMap.lineMap a b)) unitInterval
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- Let `f : G →+ G` be a continuous surjective additive group endomorphism
of a compact topological additive group with second countable topology.
If the preimages of `0` under the iterations of `f` are dense,
then `f` is ergodic with respect to any finite inner regular left invariant measure.  -/
AddMonoidHom.ergodic_of_dense_iUnion_preimage_zero : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [SecondCountableTopology G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] [CompactSpace G] {μ : MeasureTheory.Measure G} [μ.IsAddHaarMeasure]
  (f : G →+ G), Dense (⋃ n, (⇑f)^[n] ⁻¹' 0) → Continuous ⇑f → Function.Surjective ⇑f → Ergodic (⇑f) μ
-- Mathlib.Logic.Relation
Relation.TransGen.instIsPreorderOfRefl : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r], IsPreorder α (Relation.TransGen r)
-- Mathlib.ModelTheory.Basic
/-- A homomorphism between first-order structures is a function that commutes with the
interpretations of functions and maps tuples in one structure where a given relation is true to
tuples in the second structure where that relation is still true.  -/
FirstOrder.Language.Hom : (L : FirstOrder.Language) → (M : Type w) → (N : Type w') → [L.Structure M] → [L.Structure N] → Type (max w w')
-- Std.Http.Data.Method
Std.Http.Method.ofNat_ctorIdx : ∀ (x : Std.Http.Method), Std.Http.Method.ofNat x.ctorIdx = x
-- Mathlib.Data.Finset.Erase
/-- An element of `s` that is not an element of `erase s a` must be `a`.  -/
Finset.eq_of_mem_of_notMem_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, b ∈ s → b ∉ s.erase a → b = a
-- Mathlib.Data.Set.Subsingleton
Set.Nontrivial.not_subset_singleton : ∀ {α : Type u} {s : Set α} {x : α}, s.Nontrivial → ¬s ⊆ {x}
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trLList.eq_1 : Turing.PartrecToTM2.trLList [] = []
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonChangeAnnotation : Lean.ToJson Lean.Lsp.ChangeAnnotation
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.Iterators.Types.TakeWhile.instIterator.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (P out).Property → Sort u_3) (h' : (P out).Property { down := false })
  (h_1 : (h' : (P out).Property { down := true }) → motive ⟨{ down := true }, h'⟩)
  (h_2 : (h' : (P out).Property { down := false }) → motive ⟨{ down := false }, h'⟩),
  (match ⟨{ down := false }, h'⟩ with
    | ⟨{ down := true }, h'⟩ => h_1 h'
    | ⟨{ down := false }, h'⟩ => h_2 h') =
    h_2 h'
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.BinaryBiconeMorphism.winr : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B),
  CategoryTheory.CategoryStruct.comp A.inr self.hom = B.inr
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.mk : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  r ≤ p.radius →
    0 < r →
      (∀ {y : E}, y ∈ Metric.eball 0 r → HasSum (fun n => (p n) fun x => y) (f (x + y))) → HasFPowerSeriesOnBall f p x r
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.coe_orthogonalProjectionOnto_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection] (v : E), ↑(U.orthogonalProjectionOnto v) = U.starProjection v
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.map_cos : ∀ {A : Type u_1} {A' : Type u_2} [inst : Ring A] [inst_1 : Ring A'] [inst_2 : Algebra ℚ A] [inst_3 : Algebra ℚ A']
  (f : A →+* A'), (PowerSeries.map f) (PowerSeries.cos A) = PowerSeries.cos A'
-- Init.Data.Vector.Attach
Vector.getElem?_attach : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, xs.attach[i]? = Option.pmap Subtype.mk xs[i]? ⋯
-- Mathlib.RingTheory.Invariant.Basic
instMulSemiringActionQuotientSubgroupSubtypeMemSubringSubring : {B : Type u_2} →
  [inst : CommRing B] →
    {G : Type u_3} →
      [inst_1 : Group G] →
        [inst_2 : MulSemiringAction G B] →
          (H : Subgroup G) → [inst_3 : H.Normal] → MulSemiringAction (G ⧸ H) ↥(FixedPoints.subring B ↥H)
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.whiskerLeft_inr_comp_pushoutSymmetry_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Q (CategoryTheory.Limits.pushout g f) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inr f g))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushoutSymmetry f g).hom) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inl g f)) h
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabLetE : Lean.PrettyPrinter.Delaborator.Delab
-- Init.System.IO
/-- Truncates the handle to its read/write cursor.

This operation does not automatically flush output buffers, so the contents of the output device may
not reflect the change immediately. This does not usually lead to problems because the read/write
cursor includes buffered writes. However, buffered writes followed by `IO.FS.Handle.rewind`, then
`IO.FS.Handle.truncate`, and then closing the file may lead to a non-empty file. If unsure, call
`IO.FS.Handle.flush` before truncating.
 -/
IO.FS.Handle.truncate : IO.FS.Handle → IO Unit
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.instHasCoeffs : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) (R₀ : Type u_5)
  [inst_4 : CommRing R₀] [inst_5 : Algebra R₀ R] [inst_6 : Algebra R₀ S] [inst_7 : IsScalarTower R₀ R S]
  [P.HasCoeffs R₀], P.HasCoeffs R₀
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_obj₁ : ∀ {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) (n : ℤ) (j : C), ((t.triangleLEGT n).obj j).obj₁ = (t.truncLE n).obj j
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.endPos_rejected : ∀ {s : String.Slice} {p q : s.Pos}, (String.Slice.Pattern.SearchStep.rejected p q).endPos = q
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorμ_natural_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (Z₁ Z₂ : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Z₂))
      (CategoryTheory.MonoidalCategory.tensorμ Y₁ Y₂ Z₁ Z₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Z₁ Z₂)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₁ Z₁)
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₂ Z₂))
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instLEOffset : LE Std.Time.Millisecond.Offset
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.expansion_empty : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (K : ℝ) (S : Finset G), Finset.expansion✝ K S ∅ = 0
-- Mathlib.RingTheory.FreeCommRing
FreeRing.coe_surjective : ∀ (α : Type u), Function.Surjective FreeRing.castFreeCommRing
-- Std.Data.ByteSlice
instSliceableByteArrayNatByteSlice_6 : Std.Ric.Sliceable ByteArray ℕ ByteSlice
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.single_zero : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ),
  PolynomialModule.single R n 0 = 0