mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.hom_ext : ∀ {X : AlgebraicGeometry.Scheme} {M N : X.Modules} (f g : M ⟶ N),
  (∀ (U : X.Opens), AlgebraicGeometry.Scheme.Modules.Hom.app f U = AlgebraicGeometry.Scheme.Modules.Hom.app g U) → f = g
-- Plausible.Testable
/-- A configuration with all the trace options enabled, useful for debugging.  -/
Plausible.Configuration.verbose : Plausible.Configuration
-- Mathlib.RingTheory.WittVector.Identities
WittVector.iterate_frobenius_coeff : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] (x : WittVector p R) (i k : ℕ),
  ((⇑WittVector.frobenius)^[i] x).coeff k = x.coeff k ^ p ^ i
-- Mathlib.Topology.Semicontinuity.Defs
LowerSemicontinuous.lowerSemicontinuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β},
  LowerSemicontinuous f → ∀ (s : Set α), LowerSemicontinuousOn f s
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedHomogeneousSubmodule_fg : ∀ (R : Type u_1) [inst : CommSemiring R] {σ : Type u_3} [Finite σ] (w : σ → ℕ),
  (∀ (x : σ), w x ≠ 0) → ∀ (n : ℕ), (MvPolynomial.weightedHomogeneousSubmodule R w n).FG
-- Mathlib.Data.Multiset.UnionInter
/-- **Alias** of the forward direction of `Multiset.disjoint_right`. -/
Disjoint.notMem_of_mem_right_multiset : ∀ {α : Type u_1} {s t : Multiset α}, Disjoint s t → ∀ {a : α}, a ∈ t → a ∉ s
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources.mk.injEq : ∀ {α β : Type} (socket : Option α) (expect : Option ℕ)
  (response : Option (Std.Channel (Except IO.Error (Std.Http.Response β)))) (responseBody : Option β)
  (requestBody : Option Std.Http.Body.Stream) (timeout : Std.Time.Millisecond.Offset)
  (keepAliveTimeout : Option Std.Time.Millisecond.Offset) (headerTimeout : Option Std.Time.Timestamp)
  (connectionContext : Std.CancellationContext) (socket_1 : Option α) (expect_1 : Option ℕ)
  (response_1 : Option (Std.Channel (Except IO.Error (Std.Http.Response β)))) (responseBody_1 : Option β)
  (requestBody_1 : Option Std.Http.Body.Stream) (timeout_1 : Std.Time.Millisecond.Offset)
  (keepAliveTimeout_1 : Option Std.Time.Millisecond.Offset) (headerTimeout_1 : Option Std.Time.Timestamp)
  (connectionContext_1 : Std.CancellationContext),
  ({ socket := socket, expect := expect, response := response, responseBody := responseBody, requestBody := requestBody,
        timeout := timeout, keepAliveTimeout := keepAliveTimeout, headerTimeout := headerTimeout,
        connectionContext := connectionContext } =
      { socket := socket_1, expect := expect_1, response := response_1, responseBody := responseBody_1,
        requestBody := requestBody_1, timeout := timeout_1, keepAliveTimeout := keepAliveTimeout_1,
        headerTimeout := headerTimeout_1, connectionContext := connectionContext_1 }) =
    (socket = socket_1 ∧
      expect = expect_1 ∧
        response = response_1 ∧
          responseBody = responseBody_1 ∧
            requestBody = requestBody_1 ∧
              timeout = timeout_1 ∧
                keepAliveTimeout = keepAliveTimeout_1 ∧
                  headerTimeout = headerTimeout_1 ∧ connectionContext = connectionContext_1)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_homologyFunctor_map_of_epi_of_isIso_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : CategoryTheory.CategoryWithHomology C]
  [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃],
  CategoryTheory.IsIso ((CategoryTheory.ShortComplex.homologyFunctor C).map φ)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.norm_bv_add_mul : ∀ {w : ℕ} {x y : BitVec w}, ~~~(x * ~~~y) + 1#w = x + x * y
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShift_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ₁ γ₂ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n'),
  (γ₁ + γ₂).leftShift a n' hn' = γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn'
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- the functor preserves all the right homology data of the short complex  -/
CategoryTheory.Functor.PreservesRightHomologyOf.isPreservedBy : ∀ {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.Limits.HasZeroMorphisms C}
  {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} {F : CategoryTheory.Functor C D}
  {inst_4 : F.PreservesZeroMorphisms} {S : CategoryTheory.ShortComplex C} [self : F.PreservesRightHomologyOf S]
  (h : S.RightHomologyData), h.IsPreservedBy F
-- Mathlib.Algebra.Group.End
Equiv.Perm.zpow_apply_comm : ∀ {α : Type u_7} (σ : Equiv.Perm α) (m n : ℤ) {x : α}, (σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x)
-- Mathlib.Order.Interval.Set.Image
directedOn_le_Iic : ∀ {α : Type u_1} [inst : Preorder α] (b : α), DirectedOn (fun x1 x2 => x1 ≤ x2) (Set.Iic b)
-- Mathlib.Topology.Separation.NotNormal
/-- Let `s` be a closed set in a separable normal space. If the induced topology on `s` is discrete,
then `s` has cardinality less than continuum.  -/
IsClosed.mk_lt_continuum : ∀ {X : Type u} [inst : TopologicalSpace X] [TopologicalSpace.SeparableSpace X] [NormalSpace X] {s : Set X},
  IsClosed s → ∀ [DiscreteTopology ↑s], Cardinal.mk ↑s < Cardinal.continuum
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.leadingCoeff_normalize : ∀ {R : Type u} [inst : CommRing R] [inst_1 : NoZeroDivisors R] [inst_2 : NormalizationMonoid R] (p : Polynomial R),
  (normalize p).leadingCoeff = normalize p.leadingCoeff
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sign_touchpointWeights_singleton_pos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  {i j : Fin (n + 1)}, i ≠ j → SignType.sign (s.touchpointWeights {i} i j) = 1
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_singleton_left : ∀ {α : Type u_2} {s : Finset α} {a : α}, Disjoint {a} s ↔ a ∉ s
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- The unique `AlgHom` from `QuadraticAlgebra R a b` to an `R`-algebra `A`,
constructed by replacing `ω` with the provided root.
Conversely, this associates to every algebra morphism `QuadraticAlgebra R a b →ₐ[R] A`
a value of `ω` in `A`.  -/
QuadraticAlgebra.lift : {R : Type u_2} →
  {a b : R} →
    [inst : CommSemiring R] →
      {A : Type u_3} →
        [inst_1 : Ring A] → [inst_2 : Algebra R A] → { u // u * u = a • 1 + b • u } ≃ (QuadraticAlgebra R a b →ₐ[R] A)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_zero : Complex.arg 0 = 0
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.splits_iff_comp_splits_of_natDegree_eq_one : ∀ {R : Type u_1} [inst : Field R] {f g : Polynomial R}, g.natDegree = 1 → (f.Splits ↔ (f.comp g).Splits)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coprodEquiv_symm_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R]
  [inst_1 : TopologicalSpace M] [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : ContinuousAdd M] [inst_7 : AddCommMonoid M₁] [inst_8 : Module R M₁]
  [inst_9 : AddCommMonoid M₂] [inst_10 : Module R M₂] [inst_11 : ContinuousAdd M₁] [inst_12 : ContinuousAdd M₂]
  [inst_13 : Semiring S] [inst_14 : Module S M] [inst_15 : ContinuousConstSMul S M] [inst_16 : SMulCommClass R S M]
  (f : M₁ × M₂ →L[R] M),
  ContinuousLinearMap.coprodEquiv.symm f =
    (f ∘SL ContinuousLinearMap.inl R M₁ M₂, f ∘SL ContinuousLinearMap.inr R M₁ M₂)
-- Std.Data.ExtDTreeMap.Basic
/-- Folds the given function over the mappings in the map in descending order.  -/
Std.ExtDTreeMap.foldr : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} → [Std.TransCmp cmp] → ((a : α) → β a → δ → δ) → δ → Std.ExtDTreeMap α β cmp → δ
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.forIn_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} {δ : Type w} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {b : δ} {f : α → δ → m (ForInStep δ)},
  t₁.Equiv t₂ → forIn t₁ b f = forIn t₂ b f
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.opEquiv.match_3.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : (CategoryTheory.WithInitial C)ᵒᵖ) → (Opposite.unop y ⟶ Opposite.unop x) → (x ⟶ y) → Sort u_3)
  (x y : C)
  (f :
    Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of y)) ⟶
      Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of x)))
  (x_1 : Opposite.op (CategoryTheory.WithInitial.of x) ⟶ Opposite.op (CategoryTheory.WithInitial.of y))
  (h_1 :
    (x y : C) →
      (f :
          Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of y)) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of x))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of x) ⟶ Opposite.op (CategoryTheory.WithInitial.of y)) →
          motive (Opposite.op (CategoryTheory.WithInitial.of x)) (Opposite.op (CategoryTheory.WithInitial.of y)) f x_2)
  (h_2 :
    (a : C) →
      (x :
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of a))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of a) ⟶ Opposite.op CategoryTheory.WithInitial.star) →
          motive (Opposite.op (CategoryTheory.WithInitial.of a)) (Opposite.op CategoryTheory.WithInitial.star) x x_2)
  (h_3 :
    (x :
        Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star)) →
      (x_2 : Opposite.op CategoryTheory.WithInitial.star ⟶ Opposite.op CategoryTheory.WithInitial.star) →
        motive (Opposite.op CategoryTheory.WithInitial.star) (Opposite.op CategoryTheory.WithInitial.star) x x_2),
  (match Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_1 with
    | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_2 =>
      h_1 x y f x_2
    | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_2 a x x_2
    | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_3 x x_2) =
    h_1 x y f x_1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Chord
SimpleGraph.Adj.isChordless_toWalk : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), h.toWalk.IsChordless
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.mk.inj : ∀ {α : Type u_2} {inst : TopologicalSpace α} {x : α} {toOpens : TopologicalSpace.Opens α} {mem' : x ∈ toOpens.carrier}
  {toOpens_1 : TopologicalSpace.Opens α} {mem'_1 : x ∈ toOpens_1.carrier},
  { toOpens := toOpens, mem' := mem' } = { toOpens := toOpens_1, mem' := mem'_1 } → toOpens = toOpens_1
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
_private.Mathlib.Algebra.SkewMonoidAlgebra.Basic.0.SkewMonoidAlgebra.smul.match_1.splitter : {k : Type u_1} →
  {G : Type u_2} →
    [inst : AddMonoid k] →
      {S : Type u_4} →
        (motive : S → SkewMonoidAlgebra k G → Sort u_3) →
          (x : S) → (x_1 : SkewMonoidAlgebra k G) → ((s : S) → (b : G →₀ k) → motive s { coeff := b }) → motive x x_1
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.continuousWithinAt_of_dominated : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {Y : Type u_8}
  [inst_6 : TopologicalSpace Y] [FirstCountableTopology Y] {F_1 : Y → X → E} {x₀ : Y} {bound : X → ℝ} {s : Set Y},
  (∀ᶠ (x : Y) in nhdsWithin x₀ s, MeasureTheory.AEStronglyMeasurable (F_1 x) μ.variation) →
    (∀ᶠ (x : Y) in nhdsWithin x₀ s, ∀ᵐ (a : X) ∂μ.variation, ‖F_1 x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ.variation →
        (∀ᵐ (a : X) ∂μ.variation, ContinuousWithinAt (fun x => F_1 x a) s x₀) →
          ContinuousWithinAt (fun x => ∫ᵛ (a : X), F_1 x a ∂[B; μ]) s x₀
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A CW complex has weak topology, i.e. a set `A` in `X` is closed iff its intersection with
every closed cell and `D` is closed. Use `RelCWComplex.closed` instead.  -/
Topology.RelCWComplex.closed' : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D],
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : Topology.RelCWComplex.cell C n),
          IsClosed (A ∩ ↑(Topology.RelCWComplex.map n j) '' Metric.closedBall 0 1)) ∧
        IsClosed (A ∩ D) →
      IsClosed A
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instInfOpenAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenAddSubgroup.instInfOpenAddSubgroup = { min := fun U V => { toAddSubgroup := ↑U ⊓ ↑V, isOpen' := ⋯ } }
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n log n)`. Convert the heap to a list in increasing order.  -/
Batteries.BinomialHeap.Imp.Heap.toList : {α : Type u_1} → (α → α → Bool) → Batteries.BinomialHeap.Imp.Heap α → List α
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- Composition of `StrictlyUnitaryLaxFunctor` is strictly associative  -/
CategoryTheory.StrictlyUnitaryLaxFunctor.comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] {E : Type u₄} [inst_3 : CategoryTheory.Bicategory E]
  (F : CategoryTheory.StrictlyUnitaryLaxFunctor B C) (G : CategoryTheory.StrictlyUnitaryLaxFunctor C D)
  (H : CategoryTheory.StrictlyUnitaryLaxFunctor D E), (F.comp G).comp H = F.comp (G.comp H)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The retract of a binary bicone `c` given by `c.inr` and `c.snd`.  -/
CategoryTheory.Limits.BinaryBicone.retract_right : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → (c : CategoryTheory.Limits.BinaryBicone P Q) → CategoryTheory.Retract Q c.pt
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.dirac_eq_one_iff_mem : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} {a : α},
  MeasurableSet s → ((MeasureTheory.Measure.dirac a) s = 1 ↔ a ∈ s)
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
/-- The triangle `(t.triangleω₁δ a b c hab hbc).obj X` is isomorphic to
the (distinguished) triangle obtained by applying the functor `t.eTriangleLTGE.obj b`
to the object `(t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X)`.  -/
CategoryTheory.Triangulated.TStructure.triangleω₁δObjIso : {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) →
                [inst_6 : CategoryTheory.IsTriangulated C] →
                  (a b c : EInt) →
                    (hab : a ≤ b) →
                      (hbc : b ≤ c) →
                        (X : C) →
                          (t.triangleω₁δ a b c hab hbc).obj X ≅
                            (t.eTriangleLTGE.obj b).obj
                              ((t.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯))).obj X)
-- Mathlib.Topology.Spectral.ConstructibleTopology
/-- If `X` is quasi-separated, quasi-sober, prespectral and quasi-compact, then `X`
is still quasi-compact in the constructible topology. This holds in particular for spectral
spaces.  -/
compactSpace_withConstructibleTopology : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactSpace X] [QuasiSober X] [PrespectralSpace X]
  [QuasiSeparatedSpace X], CompactSpace (WithConstructibleTopology X)
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.inr.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  OrderMonoidHom.inr α β = { toMonoidHom := MonoidHom.inr α β, monotone' := ⋯ }
-- Batteries.Data.List.Lemmas
List.beq_iff_exists_findIdxNth : ∀ {α : Type u_1} {i : ℕ} {x : α} [inst : BEq α] {xs : List α} {h : i < xs.length},
  (xs[i] == x) = true ↔ ∃ n, List.idxOfNth x xs n = i
-- Init.Data.BitVec.Lemmas
/-- Non-overflowing signed division bounds when numerator is nonneg, denominator is nonpos.  -/
BitVec.toInt_ediv_toInt_nonpos_of_nonneg_of_nonpos : ∀ {w : ℕ} {x y : BitVec w}, 0 ≤ x.toInt → y.toInt ≤ 0 → x.toInt / y.toInt ≤ 0
-- Init.Core
Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- More flexible corecursor for `Cofix F`. Allows the return of a fully formed
value instead of making a recursive call  -/
MvQPF.Cofix.corec' : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} →
    [q : MvQPF F] → {α : TypeVec.{u} n} → {β : Type u} → (β → F (α ::: (MvQPF.Cofix F α ⊕ β))) → β → MvQPF.Cofix F α
-- Mathlib.GroupTheory.Exponent
/-- **Alias** of the reverse direction of `AddMonoid.exponent_ne_zero`. -/
AddMonoid.ExponentExists.exponent_ne_zero : ∀ {G : Type u} [inst : AddMonoid G], AddMonoid.ExponentExists G → AddMonoid.exponent G ≠ 0
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheorem.mk.inj : ∀ {levelParams : Array Lean.Name} {proof : Lean.Expr} {numParams : ℕ} {patterns : List Lean.Expr}
  {symbols : List Lean.HeadIndex} {origin : Lean.Meta.Grind.Origin} {kind : Lean.Meta.Grind.EMatchTheoremKind}
  {minIndexable : Bool} {cnstrs : List Lean.Meta.Grind.EMatchTheoremConstraint} {levelParams_1 : Array Lean.Name}
  {proof_1 : Lean.Expr} {numParams_1 : ℕ} {patterns_1 : List Lean.Expr} {symbols_1 : List Lean.HeadIndex}
  {origin_1 : Lean.Meta.Grind.Origin} {kind_1 : Lean.Meta.Grind.EMatchTheoremKind} {minIndexable_1 : Bool}
  {cnstrs_1 : List Lean.Meta.Grind.EMatchTheoremConstraint},
  { levelParams := levelParams, proof := proof, numParams := numParams, patterns := patterns, symbols := symbols,
        origin := origin, kind := kind, minIndexable := minIndexable, cnstrs := cnstrs } =
      { levelParams := levelParams_1, proof := proof_1, numParams := numParams_1, patterns := patterns_1,
        symbols := symbols_1, origin := origin_1, kind := kind_1, minIndexable := minIndexable_1, cnstrs := cnstrs_1 } →
    levelParams = levelParams_1 ∧
      proof = proof_1 ∧
        numParams = numParams_1 ∧
          patterns = patterns_1 ∧
            symbols = symbols_1 ∧ origin = origin_1 ∧ kind = kind_1 ∧ minIndexable = minIndexable_1 ∧ cnstrs = cnstrs_1
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.instMulEquivClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β],
  MulEquivClass (α ≃*o β) α β
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.sum_subset : ∀ {M : Type u_4} {ι : Type u_7} [inst : Fintype ι] [inst_1 : AddCommMonoid M] {s : Finset ι} {f : ι → M},
  (∀ (i : ι), f i ≠ 0 → i ∈ s) → ∑ i ∈ s, f i = ∑ i, f i
-- Mathlib.Order.RelSeries
LTSeries.longestOf_len_unique : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : FiniteDimensionalOrder α] (p : LTSeries α),
  (∀ (q : LTSeries α), q.length ≤ p.length) → p.length = (LTSeries.longestOf α).length
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
_private.Mathlib.CategoryTheory.Limits.Shapes.Kernels.0.CategoryTheory.Limits.compNatIso.match_1.eq_1 : ∀ (motive : CategoryTheory.Limits.WalkingParallelPair → Sort u_1)
  (h_1 : Unit → motive CategoryTheory.Limits.WalkingParallelPair.zero)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingParallelPair.one),
  (match CategoryTheory.Limits.WalkingParallelPair.zero with
    | CategoryTheory.Limits.WalkingParallelPair.zero => h_1 ()
    | CategoryTheory.Limits.WalkingParallelPair.one => h_2 ()) =
    h_1 ()
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- A proof that `f` is meromorphic on `closedBall 0 R`.  -/
Complex.ECanonicalDecomp.meromorphicOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {R : ℝ},
  Complex.ECanonicalDecomp f g R → MeromorphicOn f (Metric.closedBall 0 R)
-- Mathlib.Analysis.Meromorphic.IsolatedZeros
/-- If meromorphic `f` and `g` agree on `codiscreteWithin U`, so do their derivatives.  -/
MeromorphicOn.deriv_eventuallyEq_codiscreteWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f g : 𝕜 → E},
  MeromorphicOn f U →
    MeromorphicOn g U → f =ᶠ[Filter.codiscreteWithin U] g → deriv f =ᶠ[Filter.codiscreteWithin U] deriv g
-- Init.Prelude
/-- The implementation of `a >>> b : α`. See `HShiftRight`.  -/
ShiftRight.shiftRight : {α : Type u} → [self : ShiftRight α] → α → α → α
-- Mathlib.Topology.ContinuousOn
continuousOn_id : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, ContinuousOn id s
-- Mathlib.Computability.DFA
DFA.inter_start : ∀ {α : Type u} {σ1 σ2 : Type v} (M1 : DFA α σ1) (M2 : DFA α σ2), (M1.inter M2).start = (M1.start, M2.start)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∉ t₁ → (t₁ \ t₂).getKey? k = none
-- Init.Data.Option.Array
Option.foldr_toArray : ∀ {β : Type u_1} {α : Type u_2} (o : Option β) (a : α) (f : β → α → α),
  Array.foldr f a o.toArray = o.elim a fun b => f b a
-- Mathlib.LinearAlgebra.Prod
/-- Product of modules is commutative up to linear isomorphism.  -/
LinearEquiv.prodComm : (R : Type u_3) →
  (M : Type u_4) →
    (N : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] → [inst_3 : Module R M] → [inst_4 : Module R N] → (M × N) ≃ₗ[R] N × M
-- Lean.Declaration
Lean.QuotKind.lift : Lean.QuotKind
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.trivial_p₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  (x x_1 : (CategoryTheory.PreZeroHypercover.singleton (CategoryTheory.CategoryStruct.id S)).I₀) (x_2 : PUnit.{w + 1}),
  (CategoryTheory.PreOneHypercover.trivial S).p₂ x_2 = CategoryTheory.CategoryStruct.id S
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instReprEMatchTheoremConstraint.repr : Lean.Meta.Grind.EMatchTheoremConstraint → ℕ → Std.Format
-- Mathlib.RingTheory.RamificationInertia.Basic
Ideal.sum_ramification_inertia_eq_finrank_fiber : ∀ {R : Type u_1} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsPrime] (S : Type u_2) [inst_2 : CommRing S]
  [inst_3 : Algebra R S] [Algebra.QuasiFinite R S] [inst_5 : Fintype ↑(p.primesOver S)],
  ∑ q, (↑q).ramificationIdx R * (↑q).inertiaDeg R = Module.finrank p.ResidueField (p.Fiber S)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.map_mono : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) [∀ (j : J), CategoryTheory.Mono (p j)],
  CategoryTheory.Mono (CategoryTheory.Limits.biproduct.map p)
-- Mathlib.Algebra.Exact.Basic
Function.Exact.inl_snd : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N], Function.Exact ⇑(LinearMap.inl R M N) ⇑(LinearMap.snd R M N)