mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.comp`.

---

Composition of module object morphisms.  -/
CategoryTheory.Mod_.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.MonObj A] → {M N O : CategoryTheory.Mod D A} → M.Hom N → N.Hom O → M.Hom O
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.ι_app_homEquiv_symm_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) {W : C}
  (f : F ⟶ (CategoryTheory.Functor.const J).obj W) (j : J) {Z : C} (h_1 : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.ι.app j) (CategoryTheory.CategoryStruct.comp (h.homEquiv.symm f) h_1) =
    CategoryTheory.CategoryStruct.comp (f.app j) h_1
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.throwInvalidUsrModifier : {α : Type} → Lean.CoreM α
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer reflection of colimits along a natural isomorphism in the diagram.  -/
CategoryTheory.Limits.reflectsColimit_of_iso_diagram : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K₁ K₂ : CategoryTheory.Functor J C}
  (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂) [CategoryTheory.Limits.ReflectsColimit K₁ F],
  CategoryTheory.Limits.ReflectsColimit K₂ F
-- Mathlib.Analysis.Normed.Group.Basic
SeminormedAddGroup.disjoint_nhds_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (f : Filter E), Disjoint (nhds 0) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y‖
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.map_top : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, MeasurableSpace.map f ⊤ = ⊤
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.indexEquiv_apply_isReal : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (w : { w // w.IsReal }),
  (NumberField.mixedEmbedding.indexEquiv K) (Sum.inl w) = (↑w).embedding
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to `X₃`.  -/
CategoryTheory.Limits.ChosenPullback₃.p₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {f₃ : X₃ ⟶ S} →
            {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} →
              {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃} →
                {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} →
                  (self : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) → self.chosenPullback.pullback ⟶ X₃
-- Mathlib.ModelTheory.Definability
/-- A function symbol is a definable function.  -/
Set.DefinableFun.fun_symbol : ∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {n : ℕ} (f : L.Functions n),
  Set.DefinableFun L ∅ (FirstOrder.Language.Structure.funMap f)
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Consumer.normal : IO.Promise (Option Std.Http.Chunk) → Std.Http.Body.Channel.Consumer✝
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instMaxAbs : {α : Type u_1} → [inst : Field α] → [inst_1 : LinearOrder α] → [inst_2 : IsStrictOrderedRing α] → Max (CauSeq α abs)
-- Std.Data.HashMap.Lemmas
Std.HashMap.foldM_eq_foldlM_keysArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ},
  Std.HashMap.foldM (fun d a x => f d a) init m = Array.foldlM f init m.keysArray
-- Plausible.Testable
/-- `PrintableProp p` allows one to print a proposition so that
`Plausible` can indicate how values relate to each other.
It's basically a poor man's delaborator.
 -/
Plausible.PrintableProp : Prop → Type
-- Mathlib.Topology.Algebra.Group.Pointwise
closure_subset_of_mem_nhds_zero_of_neg_add_left_subset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {s s' t : Set G},
  s ∈ nhds 0 → (∀ x ∈ s, -x ∈ s) → s + s' ⊆ t → closure s' ⊆ t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.equation_iff : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R),
  W'.Equation P ↔
    P 1 ^ 2 + W'.a₁ * P 0 * P 1 * P 2 + W'.a₃ * P 1 * P 2 ^ 3 -
        (P 0 ^ 3 + W'.a₂ * P 0 ^ 2 * P 2 ^ 2 + W'.a₄ * P 0 * P 2 ^ 4 + W'.a₆ * P 2 ^ 6) =
      0
-- Mathlib.CategoryTheory.Sites.Coherent.Comparison
CategoryTheory.Coverage.mk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (toPrecoverage toPrecoverage_1 : CategoryTheory.Precoverage C) (e_toPrecoverage : toPrecoverage = toPrecoverage_1)
  (pullback :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X), ∀ S ∈ toPrecoverage.coverings X, ∃ T ∈ toPrecoverage.coverings Y, T.FactorsThruAlong S f),
  { toPrecoverage := toPrecoverage, pullback := pullback } = { toPrecoverage := toPrecoverage_1, pullback := ⋯ }
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The preimage of an open normal subgroup under a morphism to a profinite group.  -/
ProfiniteAddGrp.ProfiniteCompletion.preimage : {G : AddGrpCat} →
  {P : ProfiniteAddGrp.{u}} →
    (G ⟶ AddGrpCat.of ↑P.toProfinite.toTop) →
      OpenNormalAddSubgroup ↑P.toProfinite.toTop → FiniteIndexNormalAddSubgroup ↑G
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.main : List Lean.Meta.Grind.TGrind → Lean.Meta.Grind.Collector.Collect✝ Unit
-- Mathlib.Data.Fintype.Fin
Finset.sup_fin_univ : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {n : ℕ} (f : ℕ → α),
  (Finset.univ.sup fun n_1 => f ↑n_1) = (Finset.range n).sup f
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.map : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M : Matrix m m R} {b : m → α} [inst : LT α] {S : Type u_9} {F : Type u_10}
  [inst_1 : FunLike F R S] [inst_2 : Zero R] [inst_3 : Zero S] [ZeroHomClass F R S] (f : F),
  M.BlockTriangular b → (M.map ⇑f).BlockTriangular b
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_aeval : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  {B : Type u_2} [inst_3 : CommSemiring B] (g : σ → S₁) (φ : S₁ →+* B) (p : MvPolynomial σ R),
  φ ((MvPolynomial.aeval g) p) = (MvPolynomial.eval₂Hom (φ.comp (algebraMap R S₁)) fun i => φ (g i)) p
-- Init.Core
Quotient.inductionOn₃ : ∀ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid φ}
  {motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃),
  (∀ (a : α) (b : β) (c : φ), motive ⟦a⟧ ⟦b⟧ ⟦c⟧) → motive q₁ q₂ q₃
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The canonical ring homomorphism interpreting an element of `R` as an element of
the stalk of `structureSheaf R` at `x`.  -/
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.toStalkₗ' : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
          ModuleCat.of R M ⟶ (AlgebraicGeometry.structurePresheafInModuleCat R M).stalk x
-- Std.Data.HashSet.Raw
/-- Retrieves the key from the set that matches `a`. Ensures that such a key exists by requiring a proof
of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the set.
 -/
Std.HashSet.Raw.get : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → (m : Std.HashSet.Raw α) → (a : α) → a ∈ m → α
-- Init.Data.Array.Lemmas
Array.pop_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α}, (Array.replicate n a).pop = Array.replicate (n - 1) a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.insertMany!_list_equiv_foldl : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ : Std.DTreeMap.Internal.Impl α β} {l : List ((a : α) × β a)},
  (↑(t₁.insertMany! l)).Equiv (List.foldl (fun acc p => Std.DTreeMap.Internal.Impl.insert! p.fst p.snd acc) t₁ l)
-- Mathlib.Data.Sym.Sym2
/-- Symmetric relations define a set on `Sym2 α` by taking all those pairs
of elements that are related.
 -/
Sym2.fromRel : {α : Type u_1} → {r : α → α → Prop} → Std.Symm r → Set (Sym2 α)
-- Mathlib.Analysis.Complex.Exponential
Real.exp_lt_one_iff : ∀ {x : ℝ}, Real.exp x < 1 ↔ x < 0
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgSemiHomClass.mk : ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} [inst : Monoid R] [inst_1 : Monoid S]
  {φ : outParam (R →* S)} {A : outParam (Type u_4)} {B : outParam (Type u_5)} [inst_2 : NonUnitalNonAssocSemiring A]
  [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : DistribMulAction R A] [inst_5 : DistribMulAction S B]
  [inst_6 : FunLike F A B] [toDistribMulActionSemiHomClass : DistribMulActionSemiHomClass F (⇑φ) A B]
  [toMulHomClass : MulHomClass F A B], NonUnitalAlgSemiHomClass F φ A B
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.anyM_filter : ∀ {α β : Type w} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α Id m] [LawfulMonad m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {f : β → Bool}
  {p : β → m Bool},
  Std.Iter.anyM p (Std.Iter.filter f it) = Std.Iter.anyM (fun x => if f x = true then p x else pure false) it
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- One gets a pseudometric space from an emetric space if the edistance
is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the
uniformity are defeq in the pseudometric space and the pseudoemetric space. In this definition, the
distance is given separately, to be able to prescribe some expression which is not defeq to the
push-forward of the edistance to reals. See note [reducible non-instances].  -/
PseudoEMetricSpace.toPseudoMetricSpaceOfDist : {X : Type u_3} →
  [e : PseudoEMetricSpace X] →
    (dist : X → X → ℝ) →
      (∀ (x y : X), 0 ≤ dist x y) → (∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)) → PseudoMetricSpace X
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the reverse direction of `Equiv.Perm.sameCycle_subtypePerm`. -/
Equiv.Perm.SameCycle.subtypePerm : ∀ {α : Type u_2} {f : Equiv.Perm α} {p : α → Prop} {h : ∀ (x : α), p (f x) ↔ p x} {x y : { x // p x }},
  f.SameCycle ↑x ↑y → (f.subtypePerm h).SameCycle x y
-- Mathlib.Analysis.Complex.RealDeriv
/-- If a complex function is differentiable at a real point, then the induced real function is also
differentiable at this point, with a derivative equal to the real part of the complex derivative.  -/
HasStrictDerivAt.real_of_complex : ∀ {e : ℂ → ℂ} {e' : ℂ} {z : ℝ}, HasStrictDerivAt e e' ↑z → HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.tensorObj₃'_ext : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ : CategoryTheory.GradedObject I C} [inst_3 : X₁.HasTensor X₂]
  [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] {j : I} {A : C}
  (f g : CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ j ⟶ A)
  [H : X₁.HasGoodTensor₁₂Tensor X₂ X₃],
  (∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)
          g) →
    f = g
-- Mathlib.Geometry.Manifold.MFDeriv.Tangent
tangentBundleCore.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u_6)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M],
  tangentBundleCore I M =
    { baseSet := fun i => (↑i).source, isOpen_baseSet := ⋯, indexAt := achart H, mem_baseSet_at := ⋯,
      coordChange := fun i j x =>
        fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (Set.range ↑I) (↑((↑i).extend I) x),
      coordChange_self := ⋯, continuousOn_coordChange := ⋯, coordChange_comp := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct Z] {X : C} (π : (a : α) → Z a ⟶ X),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc π).op
      (CategoryTheory.Limits.opCoproductIsoProduct Z).hom =
    CategoryTheory.Limits.Pi.lift fun a => (π a).op
-- Aesop.Stats.File
Aesop.StatsFileRecord.mk : Aesop.Stats → String → String → Option Lean.Position → Option Lean.Name → Bool → Aesop.StatsFileRecord
-- Init.Data.List.OfFn
/-- Creates a list wrapped in a monad by applying the monadic function `f : Fin n → m α`
to each potential index in order, starting at `0`.
 -/
List.ofFnM : {m : Type u_1 → Type u_2} → {α : Type u_1} → {n : ℕ} → [Monad m] → (Fin n → m α) → m (List α)
-- Init.Prelude
Or.neg_resolve_right : ∀ {a b : Prop}, a ∨ ¬b → b → a
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.mk.inj : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} {inst : CommRing A} {inst_1 : SetLike σ A} {𝒜 : ι → σ} {x : Submonoid A}
  {deg : ι} {num den : ↥(𝒜 deg)} {den_mem : ↑den ∈ x} {deg_1 : ι} {num_1 den_1 : ↥(𝒜 deg_1)} {den_mem_1 : ↑den_1 ∈ x},
  { deg := deg, num := num, den := den, den_mem := den_mem } =
      { deg := deg_1, num := num_1, den := den_1, den_mem := den_mem_1 } →
    deg = deg_1 ∧ num ≍ num_1 ∧ den ≍ den_1
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isAddCyclic_of_card_le_addOrderOf : ∀ {α : Type u_1} [inst : AddGroup α] [Finite α] (x : α), Nat.card α ≤ addOrderOf x → IsAddCyclic α
-- Mathlib.Algebra.Group.Action.Basic
vadd_eq_iff_eq_neg_vadd : ∀ {α : Type u_5} {β : Type u_6} [inst : AddGroup α] [inst_1 : AddAction α β] (g : α) {x y : β}, g +ᵥ x = y ↔ x = -g +ᵥ y
-- Mathlib.Analysis.Convolution
MeasureTheory.convolutionExistsAt_iff_integrable_swap : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'} {x : G}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  {L : E →L[𝕜] E' →L[𝕜] F} [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddCommGroup G]
  [MeasurableNeg G] [μ.IsAddLeftInvariant] [MeasurableAdd G] [μ.IsNegInvariant],
  MeasureTheory.ConvolutionExistsAt f g x L μ ↔ MeasureTheory.Integrable (fun t => (L (f (x - t))) (g t)) μ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodyLT_mem : ∀ (K : Type u_1) [inst : Field K] (f : NumberField.InfinitePlace K → NNReal) {x : K},
  (NumberField.mixedEmbedding K) x ∈ NumberField.mixedEmbedding.convexBodyLT K f ↔
    ∀ (w : NumberField.InfinitePlace K), w x < ↑(f w)
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.IsZariskiLocalAtSource.isClosedUnderColimitsOfShape_discrete : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {ι : Type u_2} [Small.{u, u_2} ι] {C : Type u_3} [inst : CategoryTheory.Category.{v_2, u_3} C]
  [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ι) C]
  (L : CategoryTheory.Functor C AlgebraicGeometry.Scheme)
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) L] (X : AlgebraicGeometry.Scheme),
  (CategoryTheory.MorphismProperty.costructuredArrowObj L P).IsClosedUnderColimitsOfShape (CategoryTheory.Discrete ι)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.subst : Int.Internal.Linear.Var →
  Lean.Meta.Grind.Arith.Cutsat.EqCnstr →
    Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Init.Data.Int.Linear
Int.Internal.Linear.le_neg_cert.eq_1 : ∀ (p₁ p₂ : Int.Internal.Linear.Poly), Int.Internal.Linear.le_neg_cert p₁ p₂ = p₂.beq' ((p₁.mul_k (-1)).addConst_k 1)
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_neg : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → AddGroup (N a)] (f g : Π₀ (a : α), N a), (-f).neLocus g = f.neLocus (-g)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R] [inst_2 : NormalizationMonoid R]
  {a b : R} {n : ℕ},
  Irreducible a →
    b ≠ 0 →
      (↑n ≤ emultiplicity a b ↔ Multiset.replicate n (normalize a) ≤ UniqueFactorizationMonoid.normalizedFactors b)
-- Mathlib.RingTheory.Spectrum.Prime.TensorProduct
PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T],
  (algebraMap R T).SurjectiveOnStalks →
    ∀ (p₁ p₂ : PrimeSpectrum (TensorProduct R S T)),
      PrimeSpectrum.tensorProductTo R S T p₁ = PrimeSpectrum.tensorProductTo R S T p₂ → p₁ ≤ p₂
-- Init.Data.Iterators.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.match_1.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {P : β → Prop}
  (it : Std.IterM m { out // P out }) (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM m β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h
-- Mathlib.Algebra.Homology.TotalComplex
/-- Given a bicomplex `K`, this is a constructor for morphisms from `(K.total c₁₂).X i₁₂`.  -/
HomologicalComplex₂.totalDesc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {I₁₂ : Type u_4} →
            {c₁ : ComplexShape I₁} →
              {c₂ : ComplexShape I₂} →
                (K : HomologicalComplex₂ C c₁ c₂) →
                  {c₁₂ : ComplexShape I₁₂} →
                    [inst_2 : TotalComplexShape c₁ c₂ c₁₂] →
                      [inst_3 : DecidableEq I₁₂] →
                        [inst_4 : K.HasTotal c₁₂] →
                          {A : C} →
                            {i₁₂ : I₁₂} →
                              ((i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)) →
                                ((K.total c₁₂).X i₁₂ ⟶ A)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_eq_isSome_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.contains a = (t.getKey? a).isSome
-- Init.Data.Vector.Range
Vector.range'_succ_left : ∀ {s n step : ℕ}, Vector.range' (s + 1) n step = Vector.map (fun x => x + 1) (Vector.range' s n step)
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_X : ∀ (X : AlgebraicGeometry.Scheme) (U : X.AffineZariskiSite),
  (AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover X).X U = ↑↑U
-- Mathlib.Analysis.Convex.Extreme
extremePoints_pi : ∀ {𝕜 : Type u_1} {ι : Type u_4} {M : ι → Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module 𝕜 (M i)] (s : (i : ι) → Set (M i)),
  Set.extremePoints 𝕜 (Set.univ.pi s) = Set.univ.pi fun i => Set.extremePoints 𝕜 (s i)
-- Mathlib.Algebra.Order.Monovary
Antivary.nsmul_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Antivary f g → ∀ (n : ℕ), Antivary (n • f) g
-- Std.Sync.Channel
/-- `ch.forAsync f` calls `f` for every message received on `ch`.

Note that if this function is called twice, each message will only arrive at exactly one invocation.
 -/
Std.Channel.forAsync : {α : Type} →
  [Inhabited α] → (α → BaseIO Unit) → Std.Channel α → optParam Task.Priority Task.Priority.default → BaseIO (Task Unit)
-- Mathlib.MeasureTheory.Measure.Content
/-- The inner content of a supremum of opens is at most the sum of the individual inner contents.  -/
MeasureTheory.Content.innerContent_iSup_nat : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (U : ℕ → TopologicalSpace.Opens G),
  μ.innerContent (⨆ i, U i) ≤ ∑' (i : ℕ), μ.innerContent (U i)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.lift_openEmbedding_symm_source : ∀ {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace X']
  [inst_2 : TopologicalSpace Z] [inst_3 : Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z)
  (hf : Topology.IsOpenEmbedding f), (e.lift_openEmbedding hf).symm.source = e.target
-- Init.Data.BitVec.Basic
/-- Rotates the bits in a bitvector to the left.

All the bits of `x` are shifted to higher positions, with the top `n` bits wrapping around to fill
the vacated low bits.

SMT-LIB name: `rotate_left`, except this operator uses a `Nat` shift amount.

Example:
 * `(0b0011#4).rotateLeft 3 = 0b1001`
 -/
BitVec.rotateLeft : {w : ℕ} → BitVec w → ℕ → BitVec w
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Cases.discr : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Cases pu → Lean.FVarId
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- An explicit description of `χ₄` on integers / naturals  -/
ZMod.χ₄_int_eq_if_mod_four : ∀ (n : ℤ), ZMod.χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.integral_condExp : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (hm : m ≤ m₀)
  [hμm : MeasureTheory.SigmaFinite (μ.trim hm)], ∫ (x : α), μ[f | m] x ∂μ = ∫ (x : α), f x ∂μ
-- Mathlib.Order.Antisymmetrization
AntisymmRel.lt_congr_right : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α], AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → (a < b ↔ a < c)
-- Mathlib.Algebra.GroupWithZero.Basic
not_isNilpotent_one : ∀ {R : Type u_3} [inst : MonoidWithZero R] [Nontrivial R], ¬IsNilpotent 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.beq.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] [inst_2 : (k : α) → BEq (β k)]
  (t₁ t₁_1 : Std.DTreeMap.Internal.Impl α β),
  t₁ = t₁_1 → ∀ (t₂ t₂_1 : Std.DTreeMap.Internal.Impl α β), t₂ = t₂_1 → t₁.beq t₂ = t₁_1.beq t₂_1
-- Mathlib.Data.Nat.Factorial.Basic
Nat.add_factorial_le_factorial_add : ∀ (i : ℕ) {n : ℕ}, 1 ≤ n → i + n.factorial ≤ (i + n).factorial
-- Lean.Parser.Command
Lean.Parser.Command.abbrev.formatter : Lean.PrettyPrinter.Formatter