mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_single_index : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ] {i : ι} {b : β i} {h : (i : ι) → β i → γ},
  h i 0 = 1 → (fun₀ | i => b).prod h = h i b
-- Mathlib.Analysis.InnerProductSpace.PiL2
Matrix.ofLp_toEuclideanLin_apply : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {m : Type u_7} {n : Type u_8} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (M : Matrix m n 𝕜) (v : EuclideanSpace 𝕜 n), ((Matrix.toEuclideanLin M) v).ofLp = M.mulVec v.ofLp
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_subset_uIcc_iff_mem : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α},
  Finset.uIcc a₁ b₁ ⊆ Finset.uIcc a₂ b₂ ↔ a₁ ∈ Finset.uIcc a₂ b₂ ∧ b₁ ∈ Finset.uIcc a₂ b₂
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toUnder_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F),
  c.toUnder.pt = CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id c.pt)
-- Mathlib.Data.Fin.SuccPred
Fin.castAdd_injective : ∀ (m n : ℕ), Function.Injective (Fin.castAdd n)
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swapEquiv_inverse_map_toFun : ∀ {X Y : Bipointed} (f : X ⟶ Y) (a : X.X), (Bipointed.swapEquiv.inverse.map f).toFun a = f.toFun a
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.instAdditiveArrowRightFunc : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [inst_1 : CategoryTheory.Preadditive T],
  CategoryTheory.Arrow.rightFunc.Additive
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.unzero_mul : ∀ {α : Type u_1} [inst : Mul α] {x y : WithZero α} (hxy : x * y ≠ 0),
  WithZero.unzero hxy = WithZero.unzero ⋯ * WithZero.unzero ⋯
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.processUnassigned.unassignOrFail : (mvars : Array Lean.Expr) →
  (i : ℕ) →
    Lean.Expr →
      i < mvars.size →
        Lean.Meta.Grind.EMatchTheorem →
          ℕ → Lean.Expr → Lean.Expr → OptionT (StateT Lean.Meta.Grind.EMatch.Choice Lean.Meta.Grind.EMatch.M) Unit
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_toAddSubmonoid : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), ↑s.toAddSubmonoid = ↑s
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
MvPowerSeries.gaussNorm_zero : ∀ {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) [inst : Semiring R], v 0 = 0 → MvPowerSeries.gaussNorm v c 0 = 0
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.instSliceableRoiSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.instSliceableRoiSlice._auto_1) →
    Std.Roi.Sliceable (Std.TreeSet.Raw α cmp) α (Std.DTreeMap.Internal.Unit.RoiSlice α)
-- Lean.Server.InfoUtils
Lean.Elab.InfoWithCtx.mk.inj : ∀ {ctx : Lean.Elab.ContextInfo} {info : Lean.Elab.Info} {children : Lean.PersistentArray Lean.Elab.InfoTree}
  {ctx_1 : Lean.Elab.ContextInfo} {info_1 : Lean.Elab.Info} {children_1 : Lean.PersistentArray Lean.Elab.InfoTree},
  { ctx := ctx, info := info, children := children } = { ctx := ctx_1, info := info_1, children := children_1 } →
    ctx = ctx_1 ∧ info = info_1 ∧ children = children_1
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.isNonZero.eq_2 : ∀ (k : ℕ) (v : Nat.Internal.Linear.Var) (p_2 : List (ℕ × Nat.Internal.Linear.Var)),
  Nat.Internal.Linear.Poly.isNonZero ((k, v) :: p_2) =
    bif v == Nat.Internal.Linear.fixedVar then decide (k > 0) else Nat.Internal.Linear.Poly.isNonZero p_2
-- Mathlib.LinearAlgebra.Ray
/-- If a vector is in the same ray as its negation, that vector is zero.  -/
eq_zero_of_sameRay_self_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x : M} [IsDomain R] [Module.IsTorsionFree R M],
  SameRay R x (-x) → x = 0
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.ensureHasTypeWithErrorMsgs : Option Lean.Expr →
  Lean.Expr →
    (Option Lean.MessageData → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData) →
      (Lean.MVarId → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData) → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.v.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (γ γ_1 : CochainComplex.HomComplex.Cochain F G n),
  γ = γ_1 → ∀ (p q : ℤ) (hpq : p + n = q), γ.v p q hpq = γ_1.v p q hpq
-- Lean.MetavarContext
Lean.MetavarContext.MkBindingM.Context : Type
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenter_singleton_injective : ∀ {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],
  Function.Injective fun i => s.excenter {i}
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_ofReal_eq_iff : ∀ {a : ℝ}, (ENNReal.ofReal a).toReal = a ↔ 0 ≤ a
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.congr : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X Y : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.HasLaw X μ P → Y =ᵐ[P] X → ProbabilityTheory.HasLaw Y μ P
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.isNilpotent_monomial_iff : ∀ {R : Type u_1} {r : R} [inst : Semiring R] {n : ℕ}, IsNilpotent ((Polynomial.monomial n) r) ↔ IsNilpotent r
-- Mathlib.Order.Booleanisation
Booleanisation.comp_sup_lift : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (a b : α),
  Booleanisation.comp a ⊔ Booleanisation.lift b = Booleanisation.comp (a \ b)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a fallback : α}, m.contains a = false → m.getKeyD a fallback = fallback
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
summable_prod_eisSummand : ∀ {k : ℕ}, 3 ≤ k → ∀ (z : UpperHalfPlane), Summable fun x => EisensteinSeries.eisSummand ↑k ![x.1, x.2] z
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.toSubgroup_injective : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G], Function.Injective OpenSubgroup.toSubgroup
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is an `AddCommMonoid` under pointwise operations if `α` is.  -/
Finset.addCommMonoid : {α : Type u_2} → [DecidableEq α] → [AddCommMonoid α] → AddCommMonoid (Finset α)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.subsemigroupMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (M' : Subsemigroup M),
  f.subsemigroupMap M' = { toFun := fun x => ⟨f ↑x, ⋯⟩, map_mul' := ⋯ }
-- Mathlib.Order.BooleanAlgebra.Set
Set.union_sdiff_right : ∀ {α : Type u_1} {s t : Set α}, (s ∪ t) \ t = s \ t
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.totalFlipIsoX_hom_D₂_assoc : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] (j j' : J) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c) j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.totalFlipIsoX c j).hom (CategoryTheory.CategoryStruct.comp (K.D₂ c j j') h) =
    CategoryTheory.CategoryStruct.comp (K.flip.D₁ c j j')
      (CategoryTheory.CategoryStruct.comp (K.totalFlipIsoX c j').hom h)
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_of_neg : ∀ {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] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w₁ w₂ : Fin (n + 1) → R},
  ∑ j, w₁ j = 1 →
    ∑ j, w₂ j = 1 →
      ∀ {i : Fin (n + 1)},
        0 < w₁ i →
          w₂ i < 0 →
            (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide
              ((Finset.affineCombination R Finset.univ s.points) w₁)
              ((Finset.affineCombination R Finset.univ s.points) w₂)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.isEquivalent_const_iff_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u : α → β} {l : Filter α} {c : β},
  c ≠ 0 → (Asymptotics.IsEquivalent l u (Function.const α c) ↔ Filter.Tendsto u l (nhds c))
-- Mathlib.Topology.Category.TopPair
TopPair.Hom.w_assoc : ∀ {X Y : TopPair} (f : X ⟶ Y) {Z : TopCat} (h : TopPair.fst ⟶ Z),
  CategoryTheory.CategoryStruct.comp (TopPair.Hom.snd f) (CategoryTheory.CategoryStruct.comp TopPair.map h) =
    CategoryTheory.CategoryStruct.comp TopPair.map (CategoryTheory.CategoryStruct.comp (TopPair.Hom.fst f) h)
-- Mathlib.Order.Filter.Extr
IsMaxOn.sup : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup β] {f g : α → β} {a : α} {s : Set α},
  IsMaxOn f s a → IsMaxOn g s a → IsMaxOn (fun x => f x ⊔ g x) s a
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- For finite values `a₀`, the logarithmic counting function `logCounting f a₀` is the logarithmic
counting function for the zeros of `f - a₀`.
 -/
ValueDistribution.logCounting_coe : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a₀ : E},
  ValueDistribution.logCounting f ↑a₀ =
    Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor (fun x => f x - a₀) Set.univ)⁺
-- Mathlib.MeasureTheory.Function.EssSup
ae_le_essSup : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLinearOrder β] {f : α → β} [inst_1 : TopologicalSpace β] [FirstCountableTopology β]
  [OrderTopology β],
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f) ae_le_essSup._auto_1 →
    ∀ᵐ (y : α) ∂μ, f y ≤ essSup f μ
-- Mathlib.Order.Category.FinBddDistLat
/-- Construct a bundled `FinBddDistLat` from a `Nonempty` `Fintype` `DistribLattice`.  -/
FinBddDistLat.of' : (α : Type u_1) → [DistribLattice α] → [Fintype α] → [Nonempty α] → FinBddDistLat
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_nonneg : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : PartialOrder E]
  [ClosedIciTopology E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E], 0 ≤ᵐ[μ] f → 0 ≤ᵐ[μ] μ[f | m]
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
/-- The forget functor `AddCommGrpCat.{u} ⥤ Type u` is corepresentable.  -/
AddCommGrpCat.coyonedaObjIsoForget : CategoryTheory.coyoneda.obj (Opposite.op (AddCommGrpCat.of (ULift.{u, 0} ℤ))) ≅ CategoryTheory.forget AddCommGrpCat
-- Mathlib.Logic.Equiv.Fin.Basic
finProdFinEquiv_apply_val : ∀ {m n : ℕ} (x : Fin m × Fin n), ↑(finProdFinEquiv x) = ↑x.2 + n * ↑x.1
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.brecOn : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y : CategoryTheory.FreeMonoidalCategory C} {a a_1 : X.Hom Y}
  (t : CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1),
  (∀ {X Y : CategoryTheory.FreeMonoidalCategory C} (a a_2 : X.Hom Y)
      (t : CategoryTheory.FreeMonoidalCategory.HomEquiv a a_2),
      CategoryTheory.FreeMonoidalCategory.HomEquiv.below t → motive a a_2 t) →
    motive a a_1 t
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.head_some_of_head_tail_some : ∀ {α : Type u} {s : Stream'.WSeq α} {a : α}, some a ∈ s.tail.head → ∃ a', some a' ∈ s.head
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.compl_range_coe : ∀ {X : Type u_1}, (Set.range OnePoint.some)ᶜ = {OnePoint.infty}
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.const_add : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddSemigroup α] [inst_1 : Neg β],
  Function.Antiperiodic f c → ∀ (a : α), Function.Antiperiodic (fun x => f (a + x)) c
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.hom_ext : ∀ {X Y : NonemptyFinLinOrd} {f g : X ⟶ Y}, LinOrd.Hom.hom f.hom = LinOrd.Hom.hom g.hom → f = g
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prod_id : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] (X : C) (Y : D),
  CategoryTheory.CategoryStruct.id (X, Y) =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y)
-- Lean.Elab.Tactic.Conv.Basic
/-- Replace `lhs` with the definitionally equal `lhs'`.  -/
Lean.Elab.Tactic.Conv.changeLhs : Lean.Expr → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Data.Int.Fib.Basic
Int.fib_neg : ∀ (n : ℤ), Int.fib (-n) = if Even n then -Int.fib n else Int.fib n
-- Mathlib.Data.Set.Function
Set.BijOn.insert : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {a : α},
  Set.BijOn f s t → f a ∉ t → Set.BijOn f (insert a s) (insert (f a) t)
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.varFinsetLeft.match_1.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u_4} {β : Type u_3} (motive : L.Term (α ⊕ β) → Sort u_5) (l : ℕ)
  (_f : L.Functions l) (ts : Fin l → L.Term (α ⊕ β)) (h_1 : (i : α) → motive (FirstOrder.Language.var (Sum.inl i)))
  (h_2 : (_i : β) → motive (FirstOrder.Language.var (Sum.inr _i)))
  (h_3 : (l : ℕ) → (_f : L.Functions l) → (ts : Fin l → L.Term (α ⊕ β)) → motive (FirstOrder.Language.func _f ts)),
  (match FirstOrder.Language.func _f ts with
    | FirstOrder.Language.var (Sum.inl i) => h_1 i
    | FirstOrder.Language.var (Sum.inr _i) => h_2 _i
    | FirstOrder.Language.func _f ts => h_3 l _f ts) =
    h_3 l _f ts
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.sInf_toSubalgebra : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S : Set (StarSubalgebra R A)),
  (sInf S).toSubalgebra = sInf (StarSubalgebra.toSubalgebra '' S)
-- Mathlib.Topology.Instances.NNReal.Lemmas
/-- A monotone, bounded above sequence `f : ℕ → ℝ` has a finite limit.  -/
Real.tendsto_of_bddAbove_monotone : ∀ {f : ℕ → ℝ}, BddAbove (Set.range f) → Monotone f → ∃ r, Filter.Tendsto f Filter.atTop (nhds r)
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.restrict_Iio_eq_restrict_Iic : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a : α}, μ.restrict (Set.Iio a) = μ.restrict (Set.Iic a)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_eq_zero : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K},
  ArchimedeanClass.stdPart x = 0 ↔ ArchimedeanClass.mk x ≠ 0
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.hasFiniteIntegral_prod_iff' : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  ⦃f : α × β → E⦄,
  MeasureTheory.AEStronglyMeasurable f (μ.prod ν) →
    (MeasureTheory.HasFiniteIntegral f (μ.prod ν) ↔
      (∀ᵐ (x : α) ∂μ, MeasureTheory.HasFiniteIntegral (fun y => f (x, y)) ν) ∧
        MeasureTheory.HasFiniteIntegral (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.naive_σ : ∀ {R : Type u} [inst : CommRing R] {σ : Type u_2} {I : Ideal (MvPolynomial σ R)}
  (s : MvPolynomial σ R ⧸ I → MvPolynomial σ R) (hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x),
  (Algebra.Generators.naive s hs).σ = s
-- Lean.Declaration
Lean.DefinitionVal.value : Lean.DefinitionVal → Lean.Expr
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsStronglyCocartesian.map_self : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCocartesian f φ],
  CategoryTheory.Functor.IsStronglyCocartesian.map p f φ ⋯ φ = CategoryTheory.CategoryStruct.id b
-- Mathlib.GroupTheory.Order.Min
Monoid.minOrder_le_natCard : ∀ {G : Type u_1} [inst : Group G] {s : Subgroup G}, s ≠ ⊥ → (↑s).Finite → Monoid.minOrder G ≤ ↑(Nat.card ↥s)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonUnitalRing.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : AddSemigroup M],
  AddMonoidAlgebra.nonUnitalRing = { toNonUnitalNonAssocRing := AddMonoidAlgebra.nonUnitalNonAssocRing, mul_assoc := ⋯ }
-- Init.Data.Int.Lemmas
Int.mul_sub : ∀ (a b c : ℤ), a * (b - c) = a * b - a * c
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_inter_mulSupport : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] (s : Set α) (f : α → M),
  (s ∩ Function.mulSupport f).mulIndicator f = s.mulIndicator f
-- Init.Data.Vector.Lemmas
Vector.getElem?_singleton : ∀ {α : Type u_1} {a : α} {i : ℕ}, #v[a][i]? = if i = 0 then some a else none
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.toSub : {α : Type u_3} → [self : LinearOrderedAddCommGroupWithTop α] → Sub α
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.ExactPairing.coevaluation_evaluation'' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  [inst_2 : CategoryTheory.ExactPairing X Y],
  CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (η_ X Y))
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ X Y) Y) =
    CategoryTheory.MonoidalCoherence.iso.hom
-- Mathlib.Algebra.Group.Action.Defs
add_vadd_comm : ∀ {α : Type u_5} {β : Type u_6} [inst : Add β] [inst_1 : VAdd α β] [VAddCommClass α β β] (s : α) (x y : β),
  x + (s +ᵥ y) = s +ᵥ x + y
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Presheaf.IsSheaf.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf J P =
    ∀ (E : A), CategoryTheory.Presieve.IsSheaf J (P.comp (CategoryTheory.coyoneda.obj (Opposite.op E)))
-- Lean.Meta.Tactic.Grind.Types
/-- Next element in the equivalence class.  -/
Lean.Meta.Grind.ENode.next : Lean.Meta.Grind.ENode → Lean.Expr
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_eq_some_get! : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF → ∀ {a : α}, a ∈ m → Std.DHashMap.Raw.Const.get? m a = some (Std.DHashMap.Raw.Const.get! m a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.neg.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P : Fin 3 → R),
  W'.neg P = ![P 0, W'.negY P, P 2]
-- Init.Data.Float.Float32
Float32.repr : Float32 → ℕ → Std.Format
-- Mathlib.Tactic.FieldSimp
Mathlib.Tactic.FieldSimp.DenomCondition.positive.sizeOf_spec : ∀ {v : Lean.Level} {M : Q(Type v)} {iM : Q(GroupWithZero «$M»)} (iM' : Q(PartialOrder «$M»))
  (iM'' : Q(PosMulStrictMono «$M»)) (iM''' : Q(PosMulReflectLT «$M»)) (iM'''' : Q(ZeroLEOneClass «$M»)),
  sizeOf (Mathlib.Tactic.FieldSimp.DenomCondition.positive iM' iM'' iM''' iM'''') =
    1 + sizeOf iM' + sizeOf iM'' + sizeOf iM''' + sizeOf iM''''
-- Init.Data.BitVec.Bitblast
BitVec.neg_sle_zero : ∀ {w : ℕ}, 0 < w → ∀ {x : BitVec w}, (-x).sle 0#w = (x == BitVec.intMin w || (0#w).sle x)
-- Mathlib.LinearAlgebra.Matrix.Circulant
/-- Multiplication of circulant matrices commutes when the elements do.  -/
Matrix.circulant_mul_comm : ∀ {α : Type u_1} {n : Type u_3} [inst : CommMagma α] [inst_1 : AddCommMonoid α] [inst_2 : Fintype n]
  [inst_3 : AddCommGroup n] (v w : n → α),
  Matrix.circulant v * Matrix.circulant w = Matrix.circulant w * Matrix.circulant v
-- Init.Data.List.Lemmas
List.getLast!_of_getLast? : ∀ {α : Type u_1} {a : α} [inst : Inhabited α] {l : List α}, l.getLast? = some a → l.getLast! = a
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.Result.mk.injEq : ∀ (proof proof_1 : Lean.Expr), ({ proof := proof } = { proof := proof_1 }) = (proof = proof_1)
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.Options.mk.injEq : ∀ (recursive ignoreIfNotExists recursive_1 ignoreIfNotExists_1 : Bool),
  ({ recursive := recursive, ignoreIfNotExists := ignoreIfNotExists } =
      { recursive := recursive_1, ignoreIfNotExists := ignoreIfNotExists_1 }) =
    (recursive = recursive_1 ∧ ignoreIfNotExists = ignoreIfNotExists_1)
-- Batteries.Data.String.Matcher
String.Matcher.mk : Array.Matcher Char → Substring.Raw → String.Matcher
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.map.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (f : X ⟶ Y),
  I.map f = AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp I.subschemeι f)
-- Mathlib.RingTheory.Polynomial.Radical
divRadical_dvd_derivative : ∀ {k : Type u_1} [inst : Field k] [inst_1 : DecidableEq k] (a : Polynomial k),
  EuclideanDomain.divRadical a ∣ Polynomial.derivative a
-- Lean.Util.Diff
/-- Invariant: the count is non-zero iff there is a saved index  -/
Lean.Diff.Histogram.Entry.rightWF : ∀ {α : Type u} {lsize rsize : ℕ} (self : Lean.Diff.Histogram.Entry α lsize rsize),
  self.rightCount = 0 ↔ self.rightIndex = none
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.naturalityProperty.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F₁ F₂ : CategoryTheory.Functor C D} (app : (X : C) → F₁.obj X ⟶ F₂.obj X) (X Y : C) (f : X ⟶ Y),
  CategoryTheory.MorphismProperty.naturalityProperty app f =
    (CategoryTheory.CategoryStruct.comp (F₁.map f) (app Y) = CategoryTheory.CategoryStruct.comp (app X) (F₂.map f))
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.instIsKInjectiveCochainComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y : C}
  (R : CategoryTheory.InjectiveResolution Y), R.cochainComplex.IsKInjective
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.symm_neg : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E],
  (LinearIsometryEquiv.neg R).symm = LinearIsometryEquiv.neg R
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.pi_mem_of_mulSingle_mem : ∀ {η : Type u_3} {f : η → Type u_4} [inst : (i : η) → Group (f i)] [Finite η] [inst_2 : DecidableEq η]
  {H : Subgroup ((i : η) → f i)} (x : (i : η) → f i), (∀ (i : η), Pi.mulSingle i (x i) ∈ H) → x ∈ H
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Subfunctor.sheafify_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G G' : CategoryTheory.Subfunctor F),
  G ≤ G' →
    CategoryTheory.Presieve.IsSheaf J F →
      CategoryTheory.Presieve.IsSheaf J G'.toFunctor → CategoryTheory.Subfunctor.sheafify J G ≤ G'