mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber_map_fiberMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] {U : N} {X : C} (f : p.obj U ⟶ X) {Y : C} (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber p).map g))
      (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk f) =
    CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
instCompleteLatticeWithBot : {α : Type u_1} → [CompleteLattice α] → CompleteLattice (WithBot α)
-- Mathlib.Data.Finset.Piecewise
Finset.update_piecewise_of_mem : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)]
  [inst_1 : DecidableEq ι] {i : ι},
  i ∈ s → ∀ (v : π i), Function.update (s.piecewise f g) i v = s.piecewise (Function.update f i v) g
-- Mathlib.Data.List.Sigma
List.kinsert.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) (l : List (Sigma β)),
  List.kinsert a b l = ⟨a, b⟩ :: List.kerase a l
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.giSaturation.eq_1 : ∀ (M : Type u_1) [inst : AddZeroClass M],
  AddSubmonoid.giSaturation M =
    { choice := fun s hs => { toAddSubmonoid := s, addSaturated := ⋯ }, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
-- Mathlib.Topology.Category.Compactum
_private.Mathlib.Topology.Category.Compactum.0.Compactum.subset_cl : ∀ {X : Compactum} (A : Set X.A), A ⊆ Compactum.cl✝ A
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.star_dotProduct : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalSemiring α] [inst_2 : StarRing α] (v w : m → α),
  star v ⬝ᵥ w = star (star w ⬝ᵥ v)
-- Mathlib.Topology.Algebra.Ring.Ideal
/-- The connected component of zero in a topological ring as an ideal.  -/
Ideal.connectedComponentOfZero : (R : Type u_1) → [inst : TopologicalSpace R] → [inst_1 : Ring R] → [IsTopologicalRing R] → Ideal R
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_assoc_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.MonObj X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.mul)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h))
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFreeOn_empty : ∀ {α : Type u_1} (G : SimpleGraph α) {n : ℕ}, G.CliqueFreeOn ∅ n ↔ n ≠ 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₆_of_isShortNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF], W.c₆ = -864 * W.a₆
-- Std.Http.Data.Status
/-- 504 Gateway Timeout
 -/
Std.Http.Status.gatewayTimeout : Std.Http.Status
-- Mathlib.Data.Set.Image
Subtype.preimage_coe_eq_preimage_coe_iff : ∀ {α : Type u_1} {s t u : Set α}, Subtype.val ⁻¹' t = Subtype.val ⁻¹' u ↔ s ∩ t = s ∩ u
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.unop_refl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ),
  (CategoryTheory.Iso.refl X).unop = CategoryTheory.Iso.refl (Opposite.unop X)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.ι_image_top : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ⊤ = U
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLE?.go.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option ((a : α) × β a)) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryLE?.go k best (Std.DTreeMap.Internal.Impl.inner size k' v l r) =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.getEntryLE?.go k best l
    | Ordering.eq => some ⟨k', v⟩
    | Ordering.gt => Std.DTreeMap.Internal.Impl.getEntryLE?.go k (some ⟨k', v⟩) r
-- Init.Data.Int.Gcd
Int.gcd_eq_natAbs_right : ∀ {b a : ℤ}, b ∣ a → a.gcd b = b.natAbs
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.instInhabitedEvenHomSubtypeMemSubalgebraEven : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q : QuadraticForm R M) → Inhabited (CliffordAlgebra.EvenHom Q ↥(CliffordAlgebra.even Q))
-- Mathlib.Probability.Kernel.Condexp
/-- The conditional expectation of `f` with respect to a σ-algebra `m` is
(`μ.trim hm`)-almost everywhere equal to the integral `∫ y, f y ∂(condExpKernel μ m ω)`.  -/
ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel : ∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : NormedAddCommGroup F] {f : Ω → F}
  [inst_3 : NormedSpace ℝ F] [CompleteSpace F] (hm : m ≤ mΩ),
  MeasureTheory.Integrable f μ → μ[f | m] =ᵐ[μ.trim hm] fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω
-- Batteries.Data.Fin.Lemmas
Fin.exists_eq_true_of_isSome_findRev? : ∀ {n : ℕ} {p : Fin n → Bool}, (Fin.findRev? p).isSome = true → ∃ i, p i = true
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer : Type
-- Mathlib.Order.Concept
/-- A set is an intent when either of the following equivalent definitions holds:

- The `upperPolar` of its `lowerPolar` is itself.
- The set is the `upperPolar` of some other set.

The latter is used as a definition, but one can rewrite using the former via `IsIntent.eq`.
 -/
Order.IsIntent : {α : Type u_2} → {β : Type u_3} → (α → β → Prop) → Set β → Prop
-- Mathlib.InformationTheory.Hamming
hammingNorm_le_card_fintype : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → Zero (β i)] {x : (i : ι) → β i}, hammingNorm x ≤ Fintype.card ι
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodComm_apply : ∀ (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  ⇑(AddEquiv.coprodComm M N) = ⇑(AddMonoid.Coprod.swap M N)
-- Std.Do.PostCond
Std.Do.PostCond.and_imp : ∀ {α : Type u_1} {ps : Std.Do.PostShape} {P' Q' : Std.Do.PostCond α ps}, (P'.and (P'.imp Q')).entails (P'.and Q')
-- Init.Data.Nat.ToString
Nat.digitChar_eq_two : ∀ {n : ℕ}, n.digitChar = '2' ↔ n = 2
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- The definition of the centroid.  -/
Finset.centroid_def : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P),
  Finset.centroid k s p = (Finset.affineCombination k s p) (Finset.centroidWeights k s)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
/-- The set-theoretic extensionality of `HomogeneousSubmodule`.
 -/
HomogeneousSubmodule.ext' : ∀ {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A]
  [inst_1 : AddCommMonoid M] [inst_2 : Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [inst_3 : DecidableEq ιA]
  [inst_4 : AddMonoid ιA] [inst_5 : SetLike σA A] [inst_6 : AddSubmonoidClass σA A] [inst_7 : GradedRing 𝒜]
  [inst_8 : DecidableEq ιM] [inst_9 : SetLike σM M] [inst_10 : AddSubmonoidClass σM M]
  [inst_11 : DirectSum.Decomposition ℳ] [inst_12 : VAdd ιA ιM] [inst_13 : SetLike.GradedSMul 𝒜 ℳ]
  {I J : HomogeneousSubmodule 𝒜 ℳ}, (∀ (i : ιM), ∀ x ∈ ℳ i, x ∈ I ↔ x ∈ J) → I = J
-- Mathlib.Tactic.Simps.Basic
/-- The namespace that the final name will reside in.  -/
_private.Mathlib.Tactic.Simps.Basic.0.NameStruct.parent : NameStruct✝ → Lean.Name
-- Mathlib.Data.Set.Subsingleton
Set.Subsingleton.antitoneOn : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  s.Subsingleton → AntitoneOn f s
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.instIsRegularEpiπ_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R A : C} (p₁ p₂ : R ⟶ A)
  (e : CategoryTheory.EffectiveEquivalenceRelation p₁ p₂), CategoryTheory.IsRegularEpi e.π
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- The open immersion `Spec (A_f)₀ ⟶ Proj A`.  -/
AlgebraicGeometry.Proj.awayι : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (f : A) →
                {m : ℕ} →
                  f ∈ 𝒜 m →
                    0 < m →
                      (AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶
                        AlgebraicGeometry.Proj 𝒜)
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.evenEquivEvenNeg_symm_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (a : ↥(CliffordAlgebra.even (-Q))),
  (CliffordAlgebra.evenEquivEvenNeg Q).symm a = (CliffordAlgebra.evenToNeg (-Q) Q ⋯) a
-- Mathlib.Tactic.Linarith.Datatypes
/-- Some preprocessors perform branching case splits.
A `GlobalBranchingPreprocessor` produces a list of branches to run.
Each branch is independent, so hypotheses that appear in multiple branches should be duplicated.
The preprocessor is responsible for making sure that each branch contains the correct goal
metavariable.
 -/
Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor : Type
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Complex.cos` is complex analytic.  -/
Complex.analyticOn_cos : ∀ {s : Set ℂ}, AnalyticOn ℂ Complex.cos s
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- For any element `m : M` and any set `B` in the basis, `a • m` lies in `B` for all
`a` sufficiently close to `0`.  -/
SubmodulesBasis.smul : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace R] {B : ι → Submodule R M},
  SubmodulesBasis B → ∀ (m : M) (i : ι), ∀ᶠ (a : R) in nhds 0, a • m ∈ B i
-- Mathlib.Tactic.Linarith.Datatypes
/-- A `GlobalPreprocessor` lifts to a `GlobalBranchingPreprocessor` by producing only one branch.
 -/
Mathlib.Tactic.Linarith.GlobalPreprocessor.branching : Mathlib.Tactic.Linarith.GlobalPreprocessor → Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor
-- Std.Sat.AIG.Basic
/-- The `Ref.cast` equivalent for `TernaryInput`.
 -/
Std.Sat.AIG.TernaryInput.cast : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig1 aig2 : Std.Sat.AIG α} → aig1.TernaryInput → aig1.decls.size ≤ aig2.decls.size → aig2.TernaryInput
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k a : α} {h' : a ∈ t.erase k}, (t.erase k).getKey a h' = t.getKey a ⋯
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- A morphism of schemes `f : X ⟶ Y` is smooth if for each affine `U ⊆ Y` and
`V ⊆ f ⁻¹' U`, The induced map `Γ(Y, U) ⟶ Γ(X, V)` is smooth.  -/
AlgebraicGeometry.Smooth : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.RingTheory.AdjoinRoot
/-- `AdjoinRoot.modByMonicHom` sends the equivalence class of `f` mod `g` to `f %ₘ g`.

This is a well-defined right inverse to `AdjoinRoot.mk`, see `AdjoinRoot.mk_leftInverse`.  -/
AdjoinRoot.modByMonicHom : {R : Type u_1} → [inst : CommRing R] → {g : Polynomial R} → g.Monic → AdjoinRoot g →ₗ[R] Polynomial R
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_self : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E} [CompleteSpace E] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp id 2 μ →
    ∀ (x : E), ((ProbabilityTheory.covarianceBilin μ) x) x = ProbabilityTheory.variance (fun u => inner ℝ x u) μ
-- Mathlib.Algebra.Group.UniqueProds.Basic
instUniqueSumsDFinsupp : ∀ {ι : Type u_2} (G : ι → Type u_1) [inst : (i : ι) → AddZeroClass (G i)] [∀ (i : ι), UniqueSums (G i)],
  UniqueSums (Π₀ (i : ι), G i)
-- Mathlib.Computability.Primrec.Basic
/-- Builds a `Primcodable` instance from an equivalence to a `Primcodable` type.  -/
Primcodable.ofEquiv : (α : Type u_1) → {β : Type u_2} → [Primcodable α] → β ≃ α → Primcodable β
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.perm_of_beqModel : ∀ {α : Type u} {β : Type v} [inst : BEq α] [LawfulBEq α] [inst_2 : BEq β] [LawfulBEq β] {l₁ l₂ : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.DistinctKeys l₂ → Std.Internal.List.Const.beqModel l₁ l₂ = true → l₁.Perm l₂
-- Mathlib.Algebra.Opposites
AddOpposite.instSubsingleton : ∀ {α : Type u_1} [Subsingleton α], Subsingleton αᵃᵒᵖ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right}
  (hd : CategoryTheory.Limits.IsColimit d) (K : CategoryTheory.Limits.Multicofork I),
  (I.toSigmaCoforkFunctor hc hd).obj K = CategoryTheory.Limits.Multicofork.toSigmaCofork hc hd K
-- Mathlib.Topology.Algebra.Algebra.Equiv
/-- The natural coercion from a continuous algebra isomorphism
to a continuous linear isomorphism.  -/
ContinuousAlgEquiv.toContinuousLinearEquiv : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] → [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → (A ≃A[R] B) → A ≃L[R] B
-- Mathlib.Data.Set.Monotone
StrictAntiOn.mono : ∀ {α : Type u_1} {β : Type u_2} {s s₂ : Set α} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  StrictAntiOn f s → s₂ ⊆ s → StrictAntiOn f s₂
-- Init.Prelude
/-- Creates a `USize` from a `BitVec System.Platform.numBits`. This function is overridden with a
native implementation.
 -/
USize.ofBitVec : BitVec System.Platform.numBits → USize
-- Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Finset.prod_boole : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : CommMonoidWithZero M₀] {p : ι → Prop} [inst_1 : DecidablePred p]
  {s : Finset ι}, (∏ i ∈ s, if p i then 1 else 0) = if ∀ i ∈ s, p i then 1 else 0
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_eq_X_mul_T_sub_pol_U : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.T R (n + 2) =
    Polynomial.X * Polynomial.Chebyshev.T R (n + 1) - (1 - Polynomial.X ^ 2) * Polynomial.Chebyshev.U R n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    k ∉ t →
      List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
        k ∈ l → (Std.DTreeMap.Const.insertManyIfNewUnit t l).getKey! k' = k
-- Mathlib.Algebra.Order.Floor.Ring
Int.preimage_Ico : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a b : R},
  Int.cast ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉ ⌈b⌉
-- Mathlib.Order.Defs.Unbundled
IsPreorder.mk : ∀ {α : Sort u_1} {r : α → α → Prop} [toRefl : Std.Refl r] [toIsTrans : IsTrans α r], IsPreorder α r
-- Mathlib.Order.Partition.Finpartition
Finpartition.eq_of_mem_parts : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α} (P : Finpartition s) {a : α},
  t ∈ P.parts → u ∈ P.parts → a ∈ t → a ∈ u → t = u
-- Mathlib.GroupTheory.Commutator.Basic
commutatorElement_inv_right : ∀ {G : Type u_1} [inst : Group G] (a b : G), ⁅a, b⁻¹⁆ = b⁻¹ * ⁅b, a⁆ * b
-- Mathlib.Data.FunLike.IsApply
IsSMulApply.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.instAddRightCancelSemigroup : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddRightCancelSemigroup α] → AddRightCancelSemigroup (Matrix m n α)
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_prod_Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (a₁ a₂ : α) (b₁ b₂ : β),
  Set.Icc a₁ a₂ ×ˢ Set.Icc b₁ b₂ = Set.Icc (a₁, b₁) (a₂, b₂)
-- Batteries.Util.ProofWanted
/-- Command keyword used in error messages, e.g. `theorem_wanted`.  -/
_private.Batteries.Util.ProofWanted.0.WantedCmdKind.cmdName : WantedCmdKind✝ → String
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.mk.congr_simp : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B}
  (toReducedWord toReducedWord_1 : HNNExtension.NormalWord.ReducedWord G A B)
  (e_toReducedWord : toReducedWord = toReducedWord_1)
  (mem_set : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toReducedWord.toList → g ∈ d.set u),
  { toReducedWord := toReducedWord, mem_set := mem_set } = { toReducedWord := toReducedWord_1, mem_set := ⋯ }
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_eq_setToFun : ∀ {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} {f : X → E},
  ∫ᵛ (x : X), f x ∂[B; μ] = MeasureTheory.setToFun μ.variation ⇑(μ.transpose B) ⋯ f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas
Std.Tactic.BVDecide.BVLogicalExpr.denote_bitblast : ∀ (expr : Std.Tactic.BVDecide.BVLogicalExpr) (assign : Std.Tactic.BVDecide.BVExpr.Assignment),
  ⟦assign.toAIGAssignment, expr.bitblast⟧ = Std.Tactic.BVDecide.BVLogicalExpr.eval assign expr
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.evaluation₃_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  CategoryTheory.Square.evaluation₃.obj sq = sq.X₃
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonEmpty : Lean.ToJson Empty
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_update_left : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] {a : δ} [inst_1 : DecidableEq δ] {x : X a},
  Measurable fun x_1 => Function.update x_1 a x
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.mono_iff_isZero_kernel' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  (c : CategoryTheory.Limits.KernelFork f) (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.Mono f ↔ CategoryTheory.Limits.IsZero c.pt
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
/-- **Alias** of `AlgebraicGeometry.UniversallyOpen.universally_isOpenMap`. -/
AlgebraicGeometry.UniversallyOpen.out : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.UniversallyOpen f],
  (AlgebraicGeometry.topologically @IsOpenMap).universally f
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.lift_self : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (z : ℤ_[p]), (PadicInt.lift ⋯) z = z
-- Lean.Elab.MutualInductive
Lean.Elab.Command.updateViewWithFunctorName : Lean.Elab.Command.InductiveView → Lean.Elab.Command.InductiveView
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
/-- The pre-`0`-hypercover family on the category of schemes underlying the fpqc precoverage.  -/
AlgebraicGeometry.Scheme.qcCoverFamily : CategoryTheory.PreZeroHypercoverFamily AlgebraicGeometry.Scheme
-- Batteries.Data.ByteSlice
/-- Returns the subslice obtained by removing the first element.  -/
ByteSlice.popFront : ByteSlice → ByteSlice
-- Mathlib.GroupTheory.OrderOfElement
isOfFinOrder_iff_pow_eq_one : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, IsOfFinOrder x ↔ ∃ n, 0 < n ∧ x ^ n = 1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldl_reverse : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N)
  (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N) (x : CliffordAlgebra Q),
  ((CliffordAlgebra.foldl Q f hf) n) (CliffordAlgebra.reverse x) = ((CliffordAlgebra.foldr Q f hf) n) x
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.isNoetherian_iff : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  {I : FractionalIdeal (nonZeroDivisors R₁) K}, IsNoetherian R₁ ↥↑I ↔ ∀ J ≤ I, (↑J).FG
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_lt_add_iff_right : ∀ {α : Type u} [inst : Add α] {x y z : WithBot α} [inst_1 : LT α] [AddRightStrictMono α] [AddRightReflectLT α],
  z ≠ ⊥ → (x + z < y + z ↔ x < y)
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.maxIdeal.isMaximal : ∀ (k : Type u) [inst : Field k], (AlgebraicClosure.maxIdeal k).IsMaximal
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.coe_toAddMonoidHom : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (f : A →ₜ+ B), f.toAddMonoidHom = ↑f
-- Init.Data.List.Sublist
List.dropWhile_suffix : ∀ {α : Type u_1} {l : List α} (p : α → Bool), List.dropWhile p l <:+ l
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.finite_basisSet : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι], (IsProperLinearSet.basisSet✝ hs).Finite
-- Init.Data.Array.Lemmas
Array.getElem?_push : ∀ {α : Type u_1} {i : ℕ} {xs : Array α} {x : α}, (xs.push x)[i]? = if i = xs.size then some x else xs[i]?
-- Init.Data.Option.Lemmas
Option.isSome_pbind_iff : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β},
  (o.pbind f).isSome = true ↔ ∃ a, ∃ (h : o = some a), (f a h).isSome = true
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_typein : ∀ (o : Ordinal.{u}), Ordinal.lsub ⇑(Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding = o
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point.0.WeierstrassCurve.Affine.Point.toClass.match_1.eq_2 : ∀ {F : Type u_1} [inst : Field F] {W : WeierstrassCurve.Affine F} (motive : W.Point → Sort u_2) (x y : F)
  (h : W.Nonsingular x y) (h_1 : Unit → motive WeierstrassCurve.Affine.Point.zero)
  (h_2 : (x y : F) → (h : W.Nonsingular x y) → motive (WeierstrassCurve.Affine.Point.some x y h)),
  (match WeierstrassCurve.Affine.Point.some x y h with
    | WeierstrassCurve.Affine.Point.zero => h_1 ()
    | WeierstrassCurve.Affine.Point.some x y h => h_2 x y h) =
    h_2 x y h