mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Structure which contains the data and properties for a morphism `h` satisfying
`Sieve.bind S R h`.  -/
CategoryTheory.Sieve.BindStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      (S : CategoryTheory.Presieve X) →
        (⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Sieve Y) → {Z : C} → (Z ⟶ X) → Type (max u₁ v₁)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_ric_eq_toArray_rcc : ∀ {n : ℕ}, (*...=n).toArray = (0...=n).toArray
-- Init.Data.Int.Lemmas
Int.add_assoc : ∀ (a b c : ℤ), a + b + c = a + (b + c)
-- Mathlib.RingTheory.IdealFilter.Basic
/-- The Gabriel composition of ideal filters `F` and `G`.
See [nLab: Gabriel composition](https://ncatlab.org/nlab/show/Gabriel+composition+of+filters).  -/
IdealFilter.gabrielComposition : {A : Type u_1} → [inst : Ring A] → IdealFilter A → IdealFilter A → IdealFilter A
-- Init.Data.Vector.Lex
Vector.lt_of_le_of_lt' : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  [Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2] {xs ys zs : Vector α n},
  xs ≤ ys → ys < zs → xs < zs
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.PseudoCore.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F : CategoryTheory.OplaxFunctor B C} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (mapIdIso : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a))
  (mapCompIso :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          F.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g))
  (mapIdIso_hom :
    autoParam (∀ {a : B}, (mapIdIso a).hom = F.mapId a) CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso_hom._autoParam)
  (mapCompIso_hom :
    autoParam (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso f g).hom = F.mapComp f g)
      CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom._autoParam),
  sizeOf
      { mapIdIso := mapIdIso, mapCompIso := mapCompIso, mapIdIso_hom := mapIdIso_hom,
        mapCompIso_hom := mapCompIso_hom } =
    1
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.exists_conts_a_of_num : ∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K] {A : K},
  g.nums n = A → ∃ conts, g.conts n = conts ∧ conts.a = A
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.transpose_transpose : ∀ (μ : YoungDiagram), μ.transpose.transpose = μ
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
continuousAt_extChartAt_symm : ∀ {𝕜 : 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} [inst_5 : ChartedSpace H M] (x : M),
  ContinuousAt (↑(extChartAt I x).symm) (↑(extChartAt I x) x)
-- Mathlib.Analysis.Normed.Affine.Simplex
Affine.Triangle.equilateral_iff_dist_01_eq_02_and_dist_01_eq_12 : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : Module R V] [inst_4 : NormedAddTorsor V P] {t : Affine.Triangle R P},
  Affine.Simplex.Equilateral t ↔
    dist (t.points 0) (t.points 1) = dist (t.points 0) (t.points 2) ∧
      dist (t.points 0) (t.points 1) = dist (t.points 1) (t.points 2)
-- Mathlib.Algebra.Ring.Prod
NonUnitalRingHom.fst_comp_prod : ∀ {R : Type u_1} {S : Type u_3} {T : Type u_5} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] [inst_2 : NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T),
  (NonUnitalRingHom.fst S T).comp (f.prod g) = f
-- Mathlib.Order.SupClosed
SupClosed.iSup_mem : ∀ {ι : Sort u_1} {α : Type u_3} [inst : CompleteLattice α] {f : ι → α} {s : Set α} [Finite ι],
  SupClosed s → ⊥ ∈ s → (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.map_add : ∀ {F : Type u} {K : Type v} [inst : Field F] [inst_1 : Field K] {W : WeierstrassCurve.Jacobian F} (f : F →+* K)
  {P Q : Fin 3 → F}, W.Nonsingular P → W.Nonsingular Q → (W.map f).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q
-- Lean.Parser.Term
Lean.Parser.Termination.partialFixpoint.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_extend_by_one : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (f : ι → M),
  (∏ i ∈ s, if i ∈ s then f i else 1) = ∏ i ∈ s, f i
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.find?.eq_2 : ∀ {α : Type u_1} (cut : α → Ordering) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  RBTree.RBNode.find? cut (RBTree.RBNode.node c l v r) =
    match cut v with
    | Ordering.lt => RBTree.RBNode.find? cut l
    | Ordering.gt => RBTree.RBNode.find? cut r
    | Ordering.eq => some v
-- Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
/-- If `T : X →L[𝕜] X` is a compact operator on a Banach space `X`, and `μ ≠ 0` is not an
eigenvalue of `T`, then `T - μ • 1` is antilipschitz with positive constant.
That is, `T - μ • 1` is bounded below as an operator.

This is a useful step in the proof of the Fredholm alternative for compact operators.  -/
IsCompactOperator.antilipschitz_of_not_hasEigenvalue : ∀ {𝕜 : Type u_1} {X : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {T : X →L[𝕜] X} {μ : 𝕜},
  IsCompactOperator ⇑T → μ ≠ 0 → ¬Module.End.HasEigenvalue (↑T) μ → ∃ K, AntilipschitzWith K ⇑(T - μ • 1)
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
StrongDual.extendRCLikeₗᵢ_symm_apply : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : IsScalarTower ℝ 𝕜 F] (f : StrongDual 𝕜 F),
  StrongDual.extendRCLikeₗᵢ.symm f = RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f
-- Mathlib.Analysis.Convex.Segment
openSegment_symm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (x y : E), openSegment 𝕜 x y = openSegment 𝕜 y x
-- Init.Data.Int.Order
Int.le_refl : ∀ (a : ℤ), a ≤ a
-- Mathlib.Topology.MetricSpace.Isometry
/-- A map that preserves distances is an isometry  -/
Isometry.of_dist_eq : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  (∀ (x y : α), dist (f x) (f y) = dist x y) → Isometry f
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1` and `*` is a commutative monoid, if it admits an injective map that
preserves `1` and `*` to a commutative monoid.  See note [reducible non-instances].  -/
Function.Injective.commMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : CommMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 1 = 1 →
                  (∀ (x y : M₁), f (x * y) = f x * f y) → (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → CommMonoid M₁
-- Mathlib.Algebra.Group.Submonoid.BigOperators
AddSubmonoid.coe_finsetSum : ∀ {ι : Type u_4} {M : Type u_5} [inst : AddCommMonoid M] (S : AddSubmonoid M) (f : ι → ↥S) (s : Finset ι),
  ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The conversion from a Weierstrass curve in Jacobian coordinates to affine coordinates.  -/
WeierstrassCurve.Jacobian.toAffine : {R : Type r} → WeierstrassCurve.Jacobian R → WeierstrassCurve.Affine R
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_ball_self : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, 0 < ε → x ∈ Metric.ball x ε
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Grothendieck.final_pre : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D CategoryTheory.Cat) (G : CategoryTheory.Functor C D) [hG : G.Final],
  (CategoryTheory.Grothendieck.pre F G).Final
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_snd_obj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X_1 : X),
  ((CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X).obj J).snd.obj X_1 = (J.obj X_1).snd
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.fullShift.eq_1 : ∀ (A : Type u_1) (G : Type u_2) [inst : TopologicalSpace A] [inst_1 : AddMonoid G],
  SymbolicDynamics.FullShift.fullShift A G = { carrier := Set.univ, isClosed := ⋯, mapsTo := ⋯ }
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry?.eq_1 : ∀ {α : Type u} {β : Type v}, Std.DTreeMap.Internal.Impl.Const.minEntry? Std.DTreeMap.Internal.Impl.leaf = none
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_inv : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {x : β} (hx : x ≠ 0),
  CauSeq.const abv x⁻¹ = (CauSeq.const abv x).inv ⋯
-- Mathlib.Order.Filter.Pi
Filter.map_eval_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → Filter (α i)) [∀ (i : ι), (f i).NeBot] (i : ι),
  Filter.map (Function.eval i) (Filter.pi f) = f i
-- Lean.Server.Completion.CompletionUtils
_private.Lean.Server.Completion.CompletionUtils.0.Lean.Server.Completion.minimizeGlobalIdentifierInContext.shortenInOpenNamespace : Lean.Name → Lean.Name → Lean.Name
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
ContDiffAt.log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {n : WithTop ℕ∞},
  ContDiffAt ℝ n f x → f x ≠ 0 → ContDiffAt ℝ n (fun x => Real.log (f x)) x
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.constantCoeff_zeroX : ∀ {R : Type u_1} [inst : CommRing R] (F : FormalGroup R), PowerSeries.constantCoeff F.zeroX = 0
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.Lp.constₗ_apply : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : MeasureTheory.IsFiniteMeasure μ] (𝕜 : Type u_3) [inst_2 : NormedRing 𝕜]
  [inst_3 : Module 𝕜 E] [inst_4 : IsBoundedSMul 𝕜 E] (a : E),
  (MeasureTheory.Lp.constₗ p μ 𝕜) a = (MeasureTheory.Lp.const p μ) a
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.aeval_eq_smeval : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : Algebra R S] (x : S)
  (p : Polynomial R), (Polynomial.aeval x) p = p.smeval x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∉ m → (f m[k]?).isNone = true → (m.alter k f).size = m.size
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instPartialOrder : {α : Type u_1} → [inst : PartialOrder α] → PartialOrder (NonemptyInterval α)
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.laxMonoidalPi'_μ : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : (i : I) → CategoryTheory.Functor D (C i)) [inst_4 : (i : I) → (F i).LaxMonoidal] (X Y : D) (i : I),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Functor.pi' F) X Y i =
    CategoryTheory.Functor.LaxMonoidal.μ (F i) X Y
-- Mathlib.Data.Set.Sigma
Set.Nonempty.sigma_fst : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)}, (s.sigma t).Nonempty → s.Nonempty
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
/-- Converse to the mean value inequality: if `f` is line differentiable at `x₀` and `C`-lipschitz
on a neighborhood of `x₀` then its line derivative at `x₀` in the direction `v` has norm
bounded by `C * ‖v‖`. This version only assumes that `‖f x - f x₀‖ ≤ C * ‖x - x₀‖` in a
neighborhood of `x`.  -/
HasLineDerivAt.le_of_lip' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {v : E}
  {f : E → F} {f' : F} {x₀ : E},
  HasLineDerivAt 𝕜 f f' x₀ v → ∀ {C : ℝ}, 0 ≤ C → (∀ᶠ (x : E) in nhds x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) → ‖f'‖ ≤ C * ‖v‖
-- Mathlib.Data.Set.Lattice
Set.biInter_insert : ∀ {α : Type u_1} {β : Type u_2} (a : α) (s : Set α) (t : α → Set β), ⋂ x ∈ insert a s, t x = t a ∩ ⋂ x ∈ s, t x
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.is_add_left_invariant_innerContent : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : AddGroup G]
  [inst_2 : SeparatelyContinuousAdd G],
  (∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g + x) ⋯ K) = μ K) →
    ∀ (g : G) (U : TopologicalSpace.Opens G),
      μ.innerContent ((TopologicalSpace.Opens.comap ↑(Homeomorph.addLeft g)) U) = μ.innerContent U
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonWorkDoneProgressParams.fromJson : Lean.Json → Except String Lean.Lsp.WorkDoneProgressParams
-- Lean.MetavarContext
/-- The local context containing the free variables that the mvar is permitted to depend upon.  -/
Lean.MetavarDecl.lctx : Lean.MetavarDecl → Lean.LocalContext
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.other.inj : ∀ {message message_1 : String},
  Std.Http.Protocol.H1.Error.other message = Std.Http.Protocol.H1.Error.other message_1 → message = message_1
-- Mathlib.Order.CountableSupClosed
countableSupClosure_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (s : Set α) (t : Set β),
  countableSupClosure (s ×ˢ t) = countableSupClosure s ×ˢ countableSupClosure t
-- Mathlib.Analysis.Matrix.Normed
Matrix.nnnorm_conjTranspose : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] [inst_3 : StarAddMonoid α] [NormedStarGroup α] (A : Matrix m n α),
  ‖A.conjTranspose‖₊ = ‖A‖₊
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The continuous linear equivalence between the Euclidean mixed space and the mixed space.  -/
NumberField.mixedEmbedding.euclidean.toMixed : (K : Type u_1) →
  [inst : Field K] →
    [NumberField K] → NumberField.mixedEmbedding.euclidean.mixedSpace K ≃L[ℝ] NumberField.mixedEmbedding.mixedSpace K
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.Odd.eval_neg : ∀ {S : Type u_2} [inst : CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) (x : ZMod m), ψ.Odd → ψ (-x) = -ψ x
-- Aesop.Builder.Basic
Aesop.PhaseSpec.phase : Aesop.PhaseSpec → Aesop.PhaseName
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.foldM.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (α × Batteries.BinomialHeap.Imp.Heap α) → Sort u_2) (h_1 : none = none → motive none)
  (h_2 : (hd : α) → (tl : Batteries.BinomialHeap.Imp.Heap α) → none = some (hd, tl) → motive (some (hd, tl))),
  (match eq : none with
    | none => h_1 eq
    | some (hd, tl) => h_2 hd tl eq) =
    h_1 ⋯
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the cosine of the adjacent angle equals the
hypotenuse.  -/
Orientation.norm_div_cos_oangle_add_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → ‖x‖ / (o.oangle x (x + y)).cos = ‖x + y‖
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.delta_apply : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : E) (f : SchwartzMap E ℂ),
  (TemperedDistribution.delta x) f = f x
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mk_eq_bot : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (carrier : AddSubmonoid M) (smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier.carrier → c • x ∈ carrier.carrier),
  { toAddSubmonoid := carrier, smul_mem' := smul_mem' } = ⊥ ↔ carrier = ⊥
-- Mathlib.Data.List.Basic
List.mem_dropLast_of_mem_of_ne_getLast? : ∀ {α : Type u} {l : List α} {a : α}, a ∈ l → some a ≠ l.getLast? → a ∈ l.dropLast
-- Mathlib.Data.FunLike.Equiv
EquivLike.mk : {E : Sort u_1} →
  {α : outParam (Sort u_2)} →
    {β : outParam (Sort u_3)} →
      (coe : E → α → β) →
        (inv : E → β → α) →
          (∀ (e : E), Function.LeftInverse (inv e) (coe e)) →
            (∀ (e : E), Function.RightInverse (inv e) (coe e)) →
              (∀ (e g : E), coe e = coe g → inv e = inv g → e = g) → EquivLike E α β
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.tr_respects : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K]
  (M : Λ → Turing.TM2.Stmt Γ Λ σ),
  StateTransition.Respects (Turing.TM2.step M) (Turing.TM1.step (Turing.TM2to1.tr M)) Turing.TM2to1.TrCfg
-- Mathlib.Data.List.OffDiag
List.offDiag_singleton : ∀ {α : Type u_1} (a : α), [a].offDiag = []
-- Mathlib.Order.UpperLower.Closure
UpperSet.sdiff_singleton : ∀ {α : Type u_1} [inst : Preorder α] (s : UpperSet α) (a : α), s.sdiff {a} = s.erase a
-- Mathlib.LinearAlgebra.Matrix.WithConv
instStarMulWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [inst : Mul α] → [StarMul α] → StarMul (WithConv (Matrix m n α))
-- Mathlib.Data.Nat.Factorization.Basic
Nat.coprime_ordCompl : ∀ {n p : ℕ}, Nat.Prime p → n ≠ 0 → p.Coprime (n / p ^ n.factorization p)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.instHasKernelπ : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J)
  [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)],
  CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.biproduct.π f i)
-- Lean.DocString.Add
/-- Adds a docstring to the environment, if it is provided. If no docstring is provided, nothing
happens.

Whether the docstring is processed as Verso or as Markdown is determined by its syntax tree, which
reflects the `doc.verso` option at the docstring's parse site.  To explicitly control whether the
docstring is in Verso format, use `addDocStringOf` instead.

Markdown docstrings have their documentation links validated.

For Verso docstrings, `binders` should be the syntax of the parameters to the constant that is being
documented, as a null node that contains a sequence of bracketed binders. It is used to allow
interactive features such as document highlights and “find references” to work for documented
parameters. If no parameter binders are available, pass `Syntax.missing` or an empty null node.
`binders` is not used for Markdown docstrings.

 -/
Lean.addDocString' : Lean.Name → Lean.Syntax → Option (Lean.TSyntax `Lean.Parser.Command.docComment) → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Group.Action.Pi
Pi.vaddCommClass' : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → VAdd M (β i)]
  [inst_1 : (i : ι) → VAdd (α i) (β i)] [∀ (i : ι), VAddCommClass M (α i) (β i)],
  VAddCommClass M ((i : ι) → α i) ((i : ι) → β i)
-- Mathlib.Data.Set.Lattice.Image
Set.image2_iUnion₂_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_8} (f : α → β → γ) (s : Set α)
  (t : (i : ι) → κ i → Set β), Set.image2 f s (⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, Set.image2 f s (t i j)
-- Init.Dynamic
/-- Stores the provided value in a `Dynamic`.

Use `Dynamic.get? α` to retrieve it.
 -/
Dynamic.mk : {α : Type u_1} → [TypeName α] → α → Dynamic
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.instSMul_1 : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    {R : Type u_3} →
      {V : Type u_4} →
        {β : Type u_6} →
          [inst : PartialOrder Γ] →
            [inst_1 : PartialOrder Γ'] →
              [inst_2 : AddCommMonoid V] →
                [inst_3 : AddCommMonoid R] →
                  [SMulWithZero R V] →
                    [inst_5 : VAdd Γ Γ'] →
                      [IsOrderedCancelVAdd Γ Γ'] → SMul (HahnSeries Γ R) (HahnSeries.SummableFamily Γ' V β)
-- Lean.Meta.Constructions.CtorElim
_private.Lean.Meta.Constructions.CtorElim.0.Lean.mkIndCtorElim : Lean.Name → Lean.MetaM Unit
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.mul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [NoZeroDivisors R]
  {a b : S}, IsAlgebraic R a → IsAlgebraic R b → IsAlgebraic R (a * b)
-- Init.Data.BitVec.Lemmas
BitVec.fill_true : ∀ {w : ℕ}, BitVec.fill w true = BitVec.allOnes w
-- Mathlib.Algebra.Order.Positive.Ring
/-- If `R` is a nontrivial linear ordered commutative semiring, then `{x : R // 0 < x}` is a linear
ordered cancellative commutative monoid.  -/
Positive.isOrderedCancelMonoid : ∀ {R : Type u_2} [inst : CommSemiring R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R],
  IsOrderedCancelMonoid { x // 0 < x }
-- Std.Data.Internal.List.Associative
Std.Internal.List.keys_nil : ∀ {α : Type u} {β : α → Type v}, Std.Internal.List.keys [] = []
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.monic_finprod_X_sub_C : ∀ {R : Type u} [inst : CommRing R] {α : Type u_1} (b : α → R), (∏ᶠ (k : α), (Polynomial.X - Polynomial.C (b k))).Monic
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.of_isConstant : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {assign : α → Bool} {ref : aig.Ref}
  {b : Bool}, aig.isConstant ref b = true → ⟦assign, { aig := aig, ref := ref }⟧ = b
-- Init.Data.UInt.Bitwise
USize.zero_and : ∀ {a : USize}, 0 &&& a = 0
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- The natural coercion of `A` into `𝓜(𝕜, A)` given by sending `a : A` to the pair of linear
maps `Lₐ Rₐ : A →L[𝕜] A` given by left- and right-multiplication by `a`, respectively.

Warning: if `A = 𝕜`, then this is a coercion which is not definitionally equal to the
`algebraMap 𝕜 𝓜(𝕜, 𝕜)` coercion, but these are propositionally equal. See
`DoubleCentralizer.coe_eq_algebraMap` below.  -/
DoubleCentralizer.instCoeTC : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → CoeTC A (DoubleCentralizer 𝕜 A)
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl)
Define the map `λ : L ⟶ TL`, which will serve as the structure of the algebra on `L`, and
we will show is the limiting object. We use the cone constructed by `c` and the fact that
`T` preserves limits to produce this morphism.
 -/
CategoryTheory.Comonad.ForgetCreatesLimits'.lambda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {T : CategoryTheory.Comonad C} →
          {D : CategoryTheory.Functor J T.Coalgebra} →
            (c : CategoryTheory.Limits.Cone (D.comp T.forget)) →
              CategoryTheory.Limits.IsLimit c →
                [CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor] → c.pt ⟶ (T.mapCone c).pt
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.manyCore : {α ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] →
      [Std.Internal.Parsec.Input ι elem idx] → Std.Internal.Parsec ι α → Array α → Std.Internal.Parsec ι (Array α)