mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.coeff_mapDomainBialgHom_apply : ∀ (R : Type u_1) {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  (f : M →+ N) (a : AddMonoidAlgebra R M),
  ((AddMonoidAlgebra.mapDomainBialgHom R f) a).coeff = Finsupp.mapDomain (⇑f) a.coeff
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.eraOfIndex : ℕ → Std.Time.Year.Era
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
IsQuasiregular.eq_1 : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] (x : R), IsQuasiregular x = ∃ u, PreQuasiregular.equiv.symm ↑u = x
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_eq_bot_of_inverse : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {τ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₁] M},
  g ∘ₛₗ f = LinearMap.id → f.ker = ⊥
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_le_comap : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {p : Submodule R₂ M₂} (f : M →ₛₗ[τ₁₂] M₂), f.ker ≤ Submodule.comap f p
-- Mathlib.Data.Finset.SDiff
Finset.notMem_sdiff_of_notMem_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∉ s → a ∉ s \ t
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The obvious ring hom `R/I → R/(I ⊔ J)`  -/
DoubleQuot.quotLeftToQuotSup : {R : Type u} → [inst : CommRing R] → (I J : Ideal R) → R ⧸ I →+* R ⧸ I ⊔ J
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGEMap_comp_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [inst_2 : e.IsTruncGE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : ∀ (i' : ι'), M.HasHomology i'] [inst_6 : CategoryTheory.Limits.HasZeroObject C]
  {Z : HomologicalComplex C c'} (h : M.truncGE e ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGEMap (CategoryTheory.CategoryStruct.comp φ φ') e) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGEMap φ e)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGEMap φ' e) h)
-- Mathlib.Topology.Homotopy.HSpaces
Path.continuous_delayReflRight : ∀ {X : Type u} [inst : TopologicalSpace X] {x y : X}, Continuous fun p => Path.delayReflRight p.1 p.2
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.ctor.injEq : ∀ (info : Lean.IR.CtorInfo) (b : Lean.IR.FnBody) (info_1 : Lean.IR.CtorInfo) (b_1 : Lean.IR.FnBody),
  (Lean.IR.Alt.ctor info b = Lean.IR.Alt.ctor info_1 b_1) = (info = info_1 ∧ b = b_1)
-- Mathlib.Data.Finset.Sups
Finset.disjSups_subset_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s t₁ t₂ : Finset α}, t₁ ⊆ t₂ → s.disjSups t₁ ⊆ s.disjSups t₂
-- Mathlib.RingTheory.Bialgebra.Convolution
BialgHom.toLinearMap_convOne : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R C], WithConv.toConv ↑(WithConv.ofConv 1) = 1
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- The identity strong natural transformation.  -/
CategoryTheory.Oplax.StrongTrans.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.OplaxFunctor B C) → CategoryTheory.Oplax.StrongTrans F F
-- Mathlib.Algebra.Ring.Int.Parity
Int.even_or_odd' : ∀ (n : ℤ), ∃ k, n = 2 * k ∨ n = 2 * k + 1
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.le_eq_isMinor : ∀ {α : Type u_1}, (fun M M' => M ≤ M') = Matroid.IsMinor
-- Mathlib.CategoryTheory.Sites.MorphismProperty
/-- If `P` is also multiplicative, the topology induced by `P` is the topology induced by the
pretopology induced by `P`.  -/
CategoryTheory.MorphismProperty.grothendieckTopology_eq_toGrothendieck_pretopology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C}
  [inst_1 : P.IsStableUnderBaseChange] [inst_2 : CategoryTheory.Limits.HasPullbacks C] [inst_3 : P.IsMultiplicative],
  P.grothendieckTopology = P.pretopology.toGrothendieck
-- Mathlib.LinearAlgebra.Basis.Submodule
/-- Let `b` be an `S`-basis of `M`. Let `R` be a CommRing such that `Algebra R S` has no zero smul
divisors, then the submodule of `M` spanned by `b` over `R` admits `b` as an `R`-basis.  -/
Module.Basis.restrictScalars : {ι : Type u_1} →
  (R : Type u_3) →
    {M : Type u_5} →
      {S : Type u_7} →
        [inst : CommRing R] →
          [IsDomain R] →
            [inst_2 : Ring S] →
              [Nontrivial S] →
                [inst_4 : AddCommGroup M] →
                  [inst_5 : Algebra R S] →
                    [inst_6 : Module S M] →
                      [inst_7 : Module R M] →
                        [IsScalarTower R S M] →
                          [Module.IsTorsionFree R S] →
                            (b : Module.Basis ι S M) → Module.Basis ι R ↥(Submodule.span R (Set.range ⇑b))
-- Mathlib.RingTheory.Invariant.Defs
/-- An action of a group `G` on an extension of rings `B/A` is invariant if every fixed point of
`B` lies in the image of `A`. The converse statement that every point in the image of `A` is fixed
by `G` is `smul_algebraMap` (assuming `SMulCommClass A B G`).  -/
Algebra.IsInvariant : (A : Type u_1) →
  (B : Type u_2) →
    (G : Type u_3) →
      [inst : CommSemiring A] →
        [inst_1 : Semiring B] → [Algebra A B] → [inst : Group G] → [MulSemiringAction G B] → Prop
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- `ComposableArrows C n` is the type of functors `Fin (n + 1) ⥤ C`.  -/
CategoryTheory.ComposableArrows : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → ℕ → Type (max v_1 u_1)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.sum_pow_eq_max_aleph0 : ∀ {x : Cardinal.{u_1}}, x ≠ 0 → (Cardinal.sum fun n => x ^ n) = max Cardinal.aleph0 x
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.isPullback_fiberToSpecResidueField_of_isPullback : ∀ {P X Y Z : AlgebraicGeometry.Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z}
  (h : CategoryTheory.IsPullback fst snd f g) (y : ↥Y),
  CategoryTheory.IsPullback
    (CategoryTheory.Limits.pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯)
    (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField snd y)
    (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f (g y))
    (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap g y))
-- Lean.Syntax
Lean.Syntax.MonadTraverser.goRight : {m : Type → Type} → [t : Lean.Syntax.MonadTraverser m] → m Unit
-- Mathlib.Algebra.Group.Nat.Hom
MonoidHom.apply_mnat : ∀ {M : Type u_1} [inst : Monoid M] (f : Multiplicative ℕ →* M) (n : Multiplicative ℕ),
  f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n
-- Mathlib.Analysis.Normed.Group.Constructions
/-- The seminorm of an element in a product space is `≤ r` if and only if the norm of each
component is.  -/
pi_norm_le_iff_of_nonneg' : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (G i)] {x : (i : ι) → G i}
  {r : ℝ}, 0 ≤ r → (‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `ContinuousLinearMap.comp_finsetSum`. -/
ContinuousLinearMap.comp_finset_sum : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {ι : Type u_9} {s : Finset ι}
  [inst_13 : ContinuousAdd M₂] [inst_14 : ContinuousAdd M₃] (g : M₂ →SL[σ₂₃] M₃) (f : ι → M₁ →SL[σ₁₂] M₂),
  g ∘SL ∑ i ∈ s, f i = ∑ i ∈ s, g ∘SL f i
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.map_eq : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasLaw._auto_1},
  ProbabilityTheory.HasLaw X μ P → MeasureTheory.Measure.map X P = μ
-- Mathlib.Data.PFunctor.Univariate.M
_private.Mathlib.Data.PFunctor.Univariate.M.0.PFunctor.M.«term_~_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.comp_F : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ S₃ : CategoryTheory.SimplicialObject.Split C}
  (Φ₁₂ : S₁ ⟶ S₂) (Φ₂₃ : S₂ ⟶ S₃),
  (CategoryTheory.CategoryStruct.comp Φ₁₂ Φ₂₃).F = CategoryTheory.CategoryStruct.comp Φ₁₂.F Φ₂₃.F
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WSameSide.trans_wOppSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.WSameSide x y → s.WOppSide y z → y ∉ s → s.WOppSide x z
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_eq_zero_iff_of_nonneg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : PartialOrder α] [AddLeftMono α] [AddRightMono α] {a b : α},
  0 ≤ a → 0 ≤ b → (a + b = 0 ↔ a = 0 ∧ b = 0)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.ofCoeff_neg`. -/
SkewMonoidAlgebra.ofFinsupp_neg : ∀ {k : Type u_1} {G : Type u_2} [inst : AddGroup k] {a : G →₀ k}, { coeff := -a } = -{ coeff := a }
-- Mathlib.Data.Nat.Fib.Basic
Nat.gcd_fib_add_self : ∀ (m n : ℕ), (Nat.fib m).gcd (Nat.fib (n + m)) = (Nat.fib m).gcd (Nat.fib n)
-- Mathlib.Algebra.Group.Ideal
SemigroupIdeal.closure_mono : ∀ {M : Type u_1} [inst : Mul M] {s t : Set M}, s ⊆ t → SemigroupIdeal.closure s ≤ SemigroupIdeal.closure t
-- Mathlib.Algebra.Torsor.Basic
/-- Pullback of an add torsor along an injective map.  -/
Function.Injective.addTorsor : {G : Type u_1} →
  {P : Type u_2} →
    {Q : Type u_3} →
      [inst : AddGroup G] →
        [inst_1 : AddTorsor G P] →
          [inst_2 : VAdd G Q] →
            [inst_3 : VSub G Q] →
              [Nonempty Q] →
                (f : Q → P) →
                  Function.Injective f →
                    (∀ (c : G) (x : Q), f (c +ᵥ x) = c +ᵥ f x) → (∀ (x y : Q), x -ᵥ y = f x -ᵥ f y) → AddTorsor G Q
-- Std.Time.Zoned.Database.PosixTz
_private.Std.Time.Zoned.Database.PosixTz.0.Std.Time.TimeZone.posixParseRule : optParam Bool false → Std.Internal.Parsec.String.Parser Std.Time.TimeZone.TransitionRule
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instIsUniformAddGroup : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : UniformSpace F] [inst_8 : IsUniformAddGroup F]
  (𝔖 : Set (Set E)), IsUniformAddGroup (UniformConvergenceCLM σ F 𝔖)
-- Init.Data.UInt.Lemmas
UInt8.add_zero : ∀ (a : UInt8), a + 0 = a
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.Candidate.mk : Lean.Server.FileWorker.SignatureHelp.CandidateKind → Lean.Syntax → Lean.Server.FileWorker.SignatureHelp.Candidate
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearMap.norm_inr_le_one : ∀ (𝕜 : Type u_9) [inst : NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F],
  ‖ContinuousLinearMap.inr 𝕜 E F‖ ≤ 1
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.continuous_seminorm : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [t : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι}, WithSeminorms p → ∀ (i : ι), Continuous ⇑(p i)
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- Let `v` be an indexed family of `n` vectors in an oriented `n`-dimensional real inner
product space `E`. The output of the volume form of `E` when evaluated on `v` is bounded in absolute
value by the product of the norms of the vectors `v i`.  -/
Orientation.abs_volumeForm_apply_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (v : Fin n → E), |o.volumeForm v| ≤ ∏ i, ‖v i‖
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- Conjugation induces an equivariant map between the `SubAddAction` of
the fixing subgroup of a subset and that of a translate.  -/
SubAddAction.addConjMap_ofFixingAddSubgroup : {M : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        {s t : Set α} →
          {g : M} →
            (hg : g +ᵥ t = s) →
              ↥(SubAddAction.ofFixingAddSubgroup M t) →ₑ[⇑(SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup hg)]
                ↥(SubAddAction.ofFixingAddSubgroup M s)
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Concatenation of two `GenLoop`s along the `i`th coordinate.  -/
GenLoop.transAt : {N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] → {x : X} → [DecidableEq N] → N → ↑(GenLoop N X x) → ↑(GenLoop N X x) → ↑(GenLoop N X x)
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ))
  (n : ℕ),
  (AlgebraicTopology.DoldKan.N₂Γ₂.inv.app X).f.f n =
    CategoryTheory.CategoryStruct.comp (X.p.f n)
      (((AlgebraicTopology.DoldKan.Γ₀.splitting X.X).cofan (Opposite.op { len := n })).inj
        (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n })))
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) {Z : C} (h : ((HomologicalComplex.single C c j).obj A).homology j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).inv h) =
    CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).homologyπ j) h
-- Mathlib.SetTheory.ZFC.Basic
/-- **Alias** of the forward direction of `ZFSet.hereditarily_iff`. -/
ZFSet.Hereditarily.def : ∀ {p : ZFSet.{u} → Prop} {x : ZFSet.{u}}, ZFSet.Hereditarily p x → p x ∧ ∀ y ∈ x, ZFSet.Hereditarily p y
-- Mathlib.Algebra.Module.PID
Module.exists_smul_eq_zero_and_mk_eq : ∀ {R : Type u} [inst : CommRing R] [IsPrincipalIdealRing R] {M : Type v} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [IsDomain R] {p : R},
  Irreducible p →
    ∀ (hM : Module.IsTorsion' M ↥(Submonoid.powers p)) [dec : (x : M) → Decidable (x = 0)] {z : M},
      Module.IsTorsionBy R M (p ^ Submodule.pOrder hM z) →
        ∀ {k : ℕ} (f : R ⧸ R ∙ p ^ k →ₗ[R] M ⧸ R ∙ z), ∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → aig.Ref → aig.Ref → aig.Ref → Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig
-- Init.Data.Array.Count
/-- This lemma is only relevant for `grind`.  -/
Std.Internal.Array.countP_eq_zero_of_forall : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, (∀ x ∈ xs, ¬p x = true) → Array.countP p xs = 0
-- Mathlib.Data.Multiset.Defs
Multiset.card_le_card : ∀ {α : Type u_1} {s t : Multiset α}, s ≤ t → s.card ≤ t.card
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.comonEquivalence_functor : ∀ (R : Type u) [inst : CommRing R], (CoalgCat.comonEquivalence R).functor = CoalgCat.toComon R
-- Lean.Meta.Canonicalizer
_private.Lean.Meta.Canonicalizer.0.Lean.Meta.Canonicalizer.canon.unsafe_1 : UInt64 → Lean.Meta.Canonicalizer.State → Option (List Lean.Expr)
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
IsSemisimpleRing.instMulOpposite : ∀ (R : Type u) [inst : Ring R] [IsSemisimpleRing R], IsSemisimpleRing Rᵐᵒᵖ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_inter_le_size_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ ∩ t₂).size ≤ t₂.size
-- Init.Data.List.Perm
List.Perm.count : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ : List α},
  l₁.Perm l₂ → ∀ (a : α), List.count a l₁ = List.count a l₂
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.Hom.map_smul_apply' : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_4} [inst : CommRing R] [inst_1 : CommRing A₁] [inst_2 : CommRing A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {σ : A₁ →ₐ[R] A₂} {L₁ : Type u_8} {L₂ : Type u_9}
  [inst_5 : LieRing L₁] [inst_6 : Module A₁ L₁] [inst_7 : LieRingModule L₁ A₁] [inst_8 : LieAlgebra R L₁]
  [inst_9 : LieRing L₂] [inst_10 : Module A₂ L₂] [inst_11 : LieRingModule L₂ A₂] [inst_12 : LieAlgebra R L₂]
  (self : LieRinehartAlgebra.Hom σ L₁ L₂) (a : A₁) (x : L₁), self.toLieHom (a • x) = σ a • self.toLieHom x
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
/-- The underlying ring hom of `Proj ℬ ⟶ Proj 𝒜` on the level of structure sheaves.  -/
AlgebraicGeometry.Proj.comapStructureSheaf : {A : Type u_1} →
  {B : Type u_2} →
    {σ : Type u_4} →
      {τ : Type u_5} →
        [inst : CommRing A] →
          [inst_1 : SetLike σ A] →
            [inst_2 : AddSubgroupClass σ A] →
              [inst_3 : CommRing B] →
                [inst_4 : SetLike τ B] →
                  [inst_5 : AddSubgroupClass τ B] →
                    {𝒜 : ℕ → σ} →
                      {ℬ : ℕ → τ} →
                        [inst_6 : GradedRing 𝒜] →
                          [inst_7 : GradedRing ℬ] →
                            (f : 𝒜 →+*ᵍ ℬ) →
                              (hf :
                                  HomogeneousIdeal.irrelevant ℬ ≤
                                    HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) →
                                (U : TopologicalSpace.Opens (ProjectiveSpectrum 𝒜)) →
                                  (V : TopologicalSpace.Opens (ProjectiveSpectrum ℬ)) →
                                    V.carrier ⊆ ⇑(AlgebraicGeometry.ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier →
                                      ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj
                                            (Opposite.op U)) →+*
                                        ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf ℬ).obj.obj
                                            (Opposite.op V))
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.ByteArray.utf8Decode?.go.match_1.splitter : (motive : Option Char → Sort u_1) →
  (x : Option Char) → (x = none → motive none) → ((c : Char) → x = some c → motive (some c)) → motive x
-- Mathlib.Algebra.Category.Ring.Basic
/-- This prevents `CommSemiRingCat.of R` being printed as `{ carrier := R, commSemiring := ... }` by
`delabStructureInstance`.  -/
CommSemiRingCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset.injEq : ∀ {A B : GrpCat} {f : A ⟶ B} (a a_1 : ↑(Set.range fun x => x • ↑(GrpCat.Hom.hom f).range)),
  (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset a = GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset a_1) =
    (a = a_1)
-- Mathlib.Analysis.Normed.Group.Basic
norm_eq_of_mem_sphere : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {r : ℝ} (x : ↑(Metric.sphere 0 r)), ‖↑x‖ = r
-- Init.Data.Option.Lemmas
Option.guard_eq_some_iff : ∀ {α : Type u_1} {p : α → Bool} {a b : α}, Option.guard p a = some b ↔ a = b ∧ p a = true
-- Mathlib.MeasureTheory.Measure.Complex
MeasureTheory.ComplexMeasure.equivSignedMeasureₗ_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} {R : Type u_2} [inst : Semiring R] [inst_1 : Module R ℝ]
  [inst_2 : ContinuousConstSMul R ℝ] [inst_3 : ContinuousConstSMul R ℂ] (a : MeasureTheory.ComplexMeasure α),
  MeasureTheory.ComplexMeasure.equivSignedMeasureₗ a = MeasureTheory.ComplexMeasure.equivSignedMeasure.toFun a
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Interpret a `AffineIsometryEquiv` as a `ContinuousAffineEquiv`.  -/
AffineIsometryEquiv.toContinuousAffineEquiv : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] → [inst_8 : NormedAddTorsor V₂ P₂] → (P ≃ᵃⁱ[𝕜] P₂) → P ≃ᴬ[𝕜] P₂
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.UInt32.toBitVec_cond : ∀ {c : Bool} {t e : UInt32}, (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
-- Mathlib.Topology.Maps.Strict.Basic
/-- **Alias** of `Homeomorph.isStrictMap_comp_iff`.

---

Strict maps are preserved when precomposing with a homeomorphism.  -/
Topology.Homeomorph.isStrictMap_comp_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : X ≃ₜ Y) {f : Y → Z}, Topology.IsStrictMap (f ∘ ⇑e) ↔ Topology.IsStrictMap f
-- Lean.Setup
Lean.IRPhases.noConfusionType : Sort v✝ → Lean.IRPhases → Lean.IRPhases → Sort v✝
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is meromorphic on `U` and `x ∈ U`, then `f` and its conversion to normal
form on `U` agree in a punctured neighborhood of `x`.
 -/
MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdsNE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {U : Set 𝕜},
  MeromorphicOn f U → x ∈ U → toMeromorphicNFOn f U =ᶠ[nhdsWithin x {x}ᶜ] f
-- Mathlib.Algebra.Tropical.Basic
Tropical.instAddMonoidWithOneTropical : {R : Type u} → [inst : LinearOrder R] → [OrderTop R] → [Zero R] → AddMonoidWithOne (Tropical R)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndepOn.image_subset_span_image_extend : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v : ι → V} {s t : Set ι} (hs : LinearIndepOn K v s) (hst : s ⊆ t), v '' t ⊆ ↑(Submodule.span K (v '' hs.extend hst))
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_eq_map : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {Q : Type u_4} [inst_3 : AddCommMonoid Q]
  {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T),
  (f.addEquivOfAddEquiv k H).toAddMonoidHom = f.map ⋯ k