mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.ext_iff : ∀ {B : Type u_1} {M : CoxeterMatrix B} {W : Type u_2} {inst : Group W} {x y : CoxeterSystem M W},
  x = y ↔ x.mulEquiv = y.mulEquiv
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.comap_const : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y))
  (y : Y), (∀ (x : X), f x = y) → LocallyConstant.comap f = fun g => LocallyConstant.const X (g y)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.find?_some_memP : ∀ {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBTree.RBNode α},
  x ∈ RBTree.RBNode.find? cut t → RBTree.RBNode.MemP cut t
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentPositionParams.mk.inj : ∀ {textDocument : Lean.Lsp.TextDocumentIdentifier} {position : Lean.Lsp.Position}
  {textDocument_1 : Lean.Lsp.TextDocumentIdentifier} {position_1 : Lean.Lsp.Position},
  { textDocument := textDocument, position := position } = { textDocument := textDocument_1, position := position_1 } →
    textDocument = textDocument_1 ∧ position = position_1
-- Lean.Elab.Tactic.Omega.Frontend
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.formatErrorMessage.prettyAtoms : Array String → Array Lean.Expr → Array Bool → Lean.MessageData
-- Mathlib.Data.Set.Image
Set.range_quot_mk : ∀ {α : Type u_1} (r : α → α → Prop), Set.range (Quot.mk r) = Set.univ
-- Mathlib.Order.Lattice
/-- The supremum is the *least* upper bound  -/
SemilatticeSup.sup_le : ∀ {α : Type u} [self : SemilatticeSup α] (a b c : α), a ≤ c → b ≤ c → SemilatticeSup.sup a b ≤ c
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α}, a ∈ m → m.getKey? a = some (m.getKeyD a fallback)
-- Mathlib.Algebra.Ring.Commute
/-- Representation of a difference of two squares in a commutative ring as a product.  -/
mul_self_sub_mul_self : ∀ {R : Type u} [inst : NonUnitalNonAssocCommRing R] (a b : R), a * a - b * b = (a + b) * (a - b)
-- Mathlib.CategoryTheory.Sites.CoproductSheafCondition
/-- Let `{ fᵢ : Xᵢ ⟶ S }` be a family of morphisms. If `∐ᵢ Xᵢ` is a universal coproduct
and the presheaf `F` preserves products, then `F` is a sheaf for the single object covering
`{ ∐ᵢ Xᵢ ⟶ S }` if and only if it is a sheaf for `{ fᵢ : Xᵢ ⟶ S }ᵢ`.
 -/
CategoryTheory.Presieve.isSheafFor_sigmaDesc_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} {ι : Type u_3} {X : ι → C}
  (f : (i : ι) → X i ⟶ S) [inst_1 : (CategoryTheory.Presieve.ofArrows X f).HasPairwisePullbacks]
  {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.IsUniversalColimit c →
    ∀
      [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)
          (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)]
      [∀ (i : ι), CategoryTheory.Limits.HasPullback (f i) (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)]
      (F : CategoryTheory.Functor Cᵒᵖ (Type u_4))
      [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun i => Opposite.op (X i)) F]
      [CategoryTheory.Limits.PreservesLimit
          (CategoryTheory.Discrete.functor fun ij => Opposite.op (CategoryTheory.Limits.pullback (f ij.1) (f ij.2))) F],
      CategoryTheory.Presieve.IsSheafFor F
          (CategoryTheory.Presieve.singleton (CategoryTheory.Limits.Cofan.IsColimit.desc hc f)) ↔
        CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X f)
-- Mathlib.Tactic.GCongr.Core
/-- Get the binder names from a lambda function.  -/
_private.Mathlib.Tactic.GCongr.Core.0.Mathlib.Tactic.GCongr.applyGCongrLemma.lambdaBinderNames : Lean.Expr → optParam (Array Lean.Name) #[] → Array Lean.Name
-- Std.Async.Timer
_private.Std.Async.Timer.0.Std.Async.Interval.ofNative.injEq : ∀ (native native_1 : Std.Internal.UV.Timer), ({ native := native } = { native := native_1 }) = (native = native_1)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.transHomeomorph_target : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z),
  (e.transHomeomorph f').target = ⇑f'.symm ⁻¹' e.target
-- Std.Data.DTreeMap.Internal.Operations
/-- Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
same key `k` with respect to `cmp`, the provided function is used to determine the new value from
the respective values in `t₁` and `t₂`.
 -/
Std.DTreeMap.Internal.Impl.Const.mergeWith! : {α : Type u} →
  {β : Type v} →
    [Ord α] →
      (α → β → β → β) →
        (Std.DTreeMap.Internal.Impl α fun x => β) →
          (Std.DTreeMap.Internal.Impl α fun x => β) → Std.DTreeMap.Internal.Impl α fun x => β
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castLE_Iic : ∀ {n m : ℕ} (a : Fin n) (h : n ≤ m), Finset.image (Fin.castLE h) (Finset.Iic a) = Finset.Iic (Fin.castLE h a)
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.Realize.match_1.eq_5 : ∀ {L : FirstOrder.Language} {M : Type u_5} {α : Type u_3}
  (motive : (x : ℕ) → L.BoundedFormula α x → (α → M) → (Fin x → M) → Sort u_4) (x : ℕ) (f : L.BoundedFormula α (x + 1))
  (v : α → M) (xs : Fin x → M)
  (h_1 : (x : ℕ) → (_v : α → M) → (_xs : Fin x → M) → motive x FirstOrder.Language.BoundedFormula.falsum _v _xs)
  (h_2 :
    (x : ℕ) →
      (t₁ t₂ : L.Term (α ⊕ Fin x)) →
        (v : α → M) → (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂) v xs)
  (h_3 :
    (x l : ℕ) →
      (R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin x)) →
          (v : α → M) → (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.rel R ts) v xs)
  (h_4 : (x : ℕ) → (f₁ f₂ : L.BoundedFormula α x) → (v : α → M) → (xs : Fin x → M) → motive x (f₁.imp f₂) v xs)
  (h_5 : (x : ℕ) → (f : L.BoundedFormula α (x + 1)) → (v : α → M) → (xs : Fin x → M) → motive x f.all v xs),
  (match x, f.all, v, xs with
    | x, FirstOrder.Language.BoundedFormula.falsum, _v, _xs => h_1 x _v _xs
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂, v, xs => h_2 x t₁ t₂ v xs
    | x, FirstOrder.Language.BoundedFormula.rel R ts, v, xs => h_3 x l R ts v xs
    | x, f₁.imp f₂, v, xs => h_4 x f₁ f₂ v xs
    | x, f.all, v, xs => h_5 x f v xs) =
    h_5 x f v xs
-- Mathlib.Algebra.Group.Basic
left_ne_add : ∀ {M : Type u_4} [inst : AddMonoid M] [IsLeftCancelAdd M] {a b : M}, a ≠ a + b ↔ b ≠ 0
-- Mathlib.Algebra.Field.Defs
Semifield.toNNRatCast : {K : Type u_2} → [self : Semifield K] → NNRatCast K
-- Mathlib.Analysis.RCLike.Basic
RCLike.conjLIE_apply : ∀ {K : Type u_1} [inst : RCLike K], ⇑RCLike.conjLIE = ⇑(starRingEnd K)
-- Mathlib.Util.AtLocation
Mathlib.Tactic.BehaviorIfUnchanged.warning.sizeOf_spec : sizeOf Mathlib.Tactic.BehaviorIfUnchanged.warning = 1
-- Init.Data.List.Scan.Lemmas
List.scanrM_concat : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} {xs : List α} {x : α} [inst : Monad m]
  [LawfulMonad m] {f : α → β → m β},
  List.scanrM f init (xs ++ [x]) = do
    let __do_lift ← f x init
    let __do_lift ← List.scanrM f __do_lift xs
    pure (__do_lift ++ [init])
-- Std.Time.Format
/-- Parses a `String` in the rfc822 format and returns a `DateTime`.
 -/
Std.Time.DateTime.fromRFC822String : String → Except String Std.Time.DateTime
-- Mathlib.GroupTheory.Subsemigroup.Center
AddSubsemigroup.center.addCommSemigroup.eq_1 : ∀ {M : Type u_1} [inst : Add M],
  AddSubsemigroup.center.addCommSemigroup =
    { toAdd := AddMemClass.add (AddSubsemigroup.center M), add_assoc := ⋯, add_comm := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_inf_eq : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂),
  Function.Injective ⇑f →
    ∀ (s₁ s₂ : AffineSubspace k P₁), AffineSubspace.map f (s₁ ⊓ s₂) = AffineSubspace.map f s₁ ⊓ AffineSubspace.map f s₂
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.SMulMemClass.subtype.eq_1 : ∀ {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] {A : Type u_1} [inst_2 : SetLike A M]
  [hA : VAddMemClass A R M] (S' : A), SubAddAction.SMulMemClass.subtype S' = { toFun := Subtype.val, map_vadd' := ⋯ }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l → ∀ {h : k' ∈ Std.DHashMap.Raw.ofList l}, (Std.DHashMap.Raw.ofList l).get k' h = cast ⋯ v
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (m : β) (f : β → α),
  HasProd ({m}.domRestrict f) (f m)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- The underlying object of the chosen pullback along `g` of `f`.  -/
CategoryTheory.ChosenPullbacksAlong.pullbackObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y Z X : C} → (Y ⟶ X) → (g : Z ⟶ X) → [CategoryTheory.ChosenPullbacksAlong g] → C
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.nondegenerate_iff_det_ne_zero : ∀ {M₂ : Type u_4} [inst : AddCommGroup M₂] {A : Type u_5} [inst_1 : CommRing A] [IsDomain A] [inst_3 : Module A M₂]
  {ι : Type u_6} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι] {B : LinearMap.BilinForm A M₂} (b : Module.Basis ι A M₂),
  B.Nondegenerate ↔ ((LinearMap.BilinForm.toMatrix b) B).det ≠ 0
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.Normal.mk : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, (∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H) → H.Normal
-- Mathlib.Data.List.Basic
List.length_eq_two : ∀ {α : Type u} {l : List α}, l.length = 2 ↔ ∃ a b, l = [a, b]
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.denote_mkAtom : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {var : α} {aig : Std.Sat.AIG α},
  ⟦assign, aig.mkAtom var⟧ = assign var
-- Mathlib.Order.Defs.Unbundled
/-- An upper set relative to a predicate `P` is a set such that all elements satisfy `P` and
any element greater than one of its members and satisfying `P` is also a member.  -/
RelUpperSet : {α : Type u_1} → [LE α] → (α → Prop) → Type u_1
-- Mathlib.InformationTheory.Coding.KraftMcMillan
_private.Mathlib.InformationTheory.Coding.KraftMcMillan.0.InformationTheory.concatFn_length : ∀ {α : Type u_1} {S : Finset (List α)} {r : ℕ} {w : Fin r → ↥S},
  (InformationTheory.concatFn✝ w).length = ∑ i, (↑(w i)).length
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- the class of cofibrations  -/
HomotopicalAlgebra.CategoryWithCofibrations.cofibrations : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : HomotopicalAlgebra.CategoryWithCofibrations C] → CategoryTheory.MorphismProperty C
-- Std.Sat.CNF.Basic
Std.Sat.CNF.VarMem_add : ∀ {α : Type u_1} {v : α} {c : Std.Sat.CNF.Clause α} {f : Std.Sat.CNF α},
  Std.Sat.CNF.VarMem v (Std.Sat.CNF.add c f) ↔ Std.Sat.CNF.Clause.Mem v c ∨ Std.Sat.CNF.VarMem v f
-- Mathlib.Algebra.Homology.ExactSequence
/-- The short complex consisting of maps `S.map' i (i + 1)` and `S.map' (i + 1) (i + 2)`
when we know that `S : ComposableArrows C n` is exact.  -/
CategoryTheory.ComposableArrows.Exact.sc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {n : ℕ} →
        {S : CategoryTheory.ComposableArrows C n} →
          S.Exact →
            (i : ℕ) →
              autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.Exact.sc._auto_1 → CategoryTheory.ShortComplex C
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.orthogonal_ker : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (T : E →L[𝕜] F),
  (↑T).kerᗮ = (↑(ContinuousLinearMap.adjoint T)).range.topologicalClosure
-- Mathlib.Data.Seq.Computation
Computation.destruct_think : ∀ {α : Type u} (s : Computation α), s.think.destruct = Sum.inr s
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.IsInitial.to_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsInitial X),
  t.to X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.finsupport_subset_fintsupport : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X),
  ρ.finsupport x₀ ⊆ ρ.fintsupport x₀
-- Mathlib.GroupTheory.Sylow
/-- The cardinality of a Sylow subgroup is `p ^ n`
where `n` is the multiplicity of `p` in the group order.  -/
Sylow.card_eq_multiplicity : ∀ {G : Type u} [inst : Group G] [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)] (P : Sylow p G),
  Nat.card ↥↑P = p ^ (Nat.card G).factorization p
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
Std.Iterators.Types.TakeWhile.instIterator : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [Monad m] →
        [Std.Iterator α m β] →
          {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
            Std.Iterator (Std.Iterators.Types.TakeWhile α m β P) m β
-- Mathlib.Tactic.Translate.ToAdditive
/-- The global `do_translate`/`dont_translate` attributes specify whether operations on
a given type should be translated. `dont_translate` can be used for types that are translated,
such as `MonoidAlgebra` -> `AddMonoidAlgebra`, or for fixed types, such as `Fin n`/`ZMod n`.
`do_translate` is for types without arguments, like `Unit` and `Empty`, where the structure on it
can be translated.

Note: The name generation is not aware of `dont_translate`, so if some part of a lemma is not
  translated thanks to this, you generally have to specify the translated name manually.
 -/
Mathlib.Tactic.ToAdditive.to_additive_do_translate : Lean.ParserDescr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_apply_of_not_map_zero : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {f : R → R} (a : A),
  ¬f 0 = 0 → cfcₙ f a = 0
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSMul' : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → {M : Type u_5} → [SMul M β] → SMul (l.Germ M) (l.Germ β)
-- Mathlib.RingTheory.Etale.Field
IsArtinianRing.equivPi.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsArtinianRing R] [inst_2 : IsReduced R],
  IsArtinianRing.equivPi R = IsArtinianRing.equivPi R
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.range_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' F'' : CategoryTheory.Functor C (Type w)} (f : F ⟶ F')
  (g : F' ⟶ F''),
  CategoryTheory.Subfunctor.range (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.Subfunctor.range f).image g
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.trace_one : ∀ {R : Type u_2} {a b : R} [inst : CommRing R], QuadraticAlgebra.trace 1 = 2
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
/-- The pushforward functor by the identity morphism identifies to
the identify functor of the category of presheaves of modules.  -/
PresheafOfModules.pushforwardId : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    (R : CategoryTheory.Functor Dᵒᵖ RingCat) →
      PresheafOfModules.pushforward (CategoryTheory.CategoryStruct.id R) ≅
        CategoryTheory.Functor.id (PresheafOfModules R)
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- The set of periodic points of a given (possibly non-minimal) period.  -/
Function.ptsOfPeriod : {α : Type u_1} → (α → α) → ℕ → Set α
-- Mathlib.Data.Vector.Basic
/-- Define `C v w` by induction on a pair of vectors `v : Vector α n` and `w : Vector β n`.  -/
List.Vector.inductionOn₂ : {α : Type u_1} →
  {n : ℕ} →
    {β : Type u_6} →
      {C : {n : ℕ} → List.Vector α n → List.Vector β n → Sort u_8} →
        (v : List.Vector α n) →
          (w : List.Vector β n) →
            C List.Vector.nil List.Vector.nil →
              ({n : ℕ} →
                  {a : α} → {b : β} → {x : List.Vector α n} → {y : List.Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)) →
                C v w
-- Mathlib.Dynamics.Transitive
MulAction.isTopologicallyTransitive_of_isMinimal : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Monoid M] [inst_2 : MulAction M α]
  [MulAction.IsMinimal M α], MulAction.IsTopologicallyTransitive M α
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasStrictDerivAt.congr_deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' g' : F} {x : 𝕜},
  HasStrictDerivAt f f' x → f' = g' → HasStrictDerivAt f g' x
-- Init.Grind.Ring.Basic
/-- Zero is left absorbing for multiplication.  -/
Lean.Grind.Semiring.mul_zero : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (a : α), a * 0 = 0
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.X.eq_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (n : σ),
  MvPolynomial.X n = (MvPolynomial.monomial fun₀ | n => 1) 1
-- Mathlib.Algebra.Quandle
/-- A rack acts on itself by equivalences.  -/
Rack.act' : {R : Type u_1} → [Rack R] → R → R ≃ R
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.WF.mk : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α}, m.inner.WF → m.WF
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.op_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor C D} (α : F ≅ G) (β : G ≅ H),
  CategoryTheory.NatIso.op (α ≪≫ β) = CategoryTheory.NatIso.op β ≪≫ CategoryTheory.NatIso.op α
-- Lean.Elab.Tactic.Basic
Lean.Elab.Term.reportUnsolvedGoals : List Lean.MVarId → Lean.MetaM Unit
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Text.parseDelete : Std.Internal.Parsec.ByteArray.Parser Std.Tactic.BVDecide.LRAT.IntAction
-- Mathlib.RingTheory.RingHomProperties
RingHom.isStableUnderCobaseChange_toMorphismProperty_iff : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).IsStableUnderCobaseChange ↔
    RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.NatTrans.prod'_app_fst : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor A B}
  {H K : CategoryTheory.Functor A C} (α : F ⟶ G) (β : H ⟶ K) (X : A),
  ((CategoryTheory.NatTrans.prod' α β).app X).1 = α.app X
-- Lean.Meta.Sym.Arith.Types
/-- Id of the envelope ring `OfSemiring.Q type`  -/
Lean.Meta.Sym.Arith.CommSemiring.ringId : Lean.Meta.Sym.Arith.CommSemiring → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.darts_toPath_subset_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), (↑p.toPath).darts ⊆ p.darts
-- Mathlib.Control.Traversable.Instances
_private.Mathlib.Control.Traversable.Instances.0.List.next?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (l : List α) → motive (a :: l)) → motive x
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.app.injEq : ∀ (arr arr_1 : Array Mathlib.Tactic.ClickSuggestions.ApplyLemma),
  (Mathlib.Tactic.ClickSuggestions.Candidates.app✝ arr = Mathlib.Tactic.ClickSuggestions.Candidates.app✝ arr_1) =
    (arr = arr_1)
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.eulerChar.eq_1 : ∀ (𝕜 : Type u_2) (α : Type u_5) [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] [inst_5 : BoundedOrder α],
  IncidenceAlgebra.eulerChar 𝕜 α = (IncidenceAlgebra.mu 𝕜) ⊥ ⊤
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is a `Monoid` under pointwise operations if `α` is.  -/
Set.monoid : {α : Type u_2} → [Monoid α] → Monoid (Set α)
-- Mathlib.CategoryTheory.GlueData
/-- The projection `∐ D.U ⟶ D.glued` given by the colimit.  -/
CategoryTheory.GlueData.π : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (D : CategoryTheory.GlueData C) →
      [inst_1 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] →
        [inst_2 : CategoryTheory.Limits.HasColimits C] → D.sigmaOpens ⟶ D.glued
-- Mathlib.Algebra.Homology.Functor
HomologicalComplex.asFunctor_map_f : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_3}
  {c : ComplexShape ι} (C : HomologicalComplex (CategoryTheory.Functor T V) c) {X Y : T} (h : X ⟶ Y) (i : ι),
  (C.asFunctor.map h).f i = (C.X i).map h
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR.run.match_3.eq_2 : ∀ {α : Type u_1} (motive : (x : ℕ) → { l // l.length = x } → Sort u_2) (a : α) (property : [a].length = 1)
  (h_1 : (property : [].length = 0) → motive 0 ⟨[], property⟩)
  (h_2 : (a : α) → (property : [a].length = 1) → motive 1 ⟨[a], property⟩)
  (h_3 : (n : ℕ) → (xs : { l // l.length = n + 2 }) → motive n.succ.succ xs),
  (match 1, ⟨[a], property⟩ with
    | 0, ⟨[], property⟩ => h_1 property
    | 1, ⟨[a], property⟩ => h_2 a property
    | n.succ.succ, xs => h_3 n xs) =
    h_2 a property
-- Mathlib.Order.SuccPred.Limit
Order.isGLB_Ioi_iff_isPredPrelimit : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α], IsGLB (Set.Ioi a) a ↔ Order.IsPredPrelimit a
-- Init.Data.UInt.Lemmas
USize.le_iff_toBitVec_le : ∀ {a b : USize}, a ≤ b ↔ a.toBitVec ≤ b.toBitVec
-- Mathlib.Data.List.Sigma
List.kinsert_def : ∀ {α : 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.Ext
Monoid.ext : ∀ {M : Type u} ⦃m₁ m₂ : Monoid M⦄, HMul.hMul = HMul.hMul → m₁ = m₂
-- Lean.Data.Lsp.Internal
Lean.Lsp.DeclInfo.mk.sizeOf_spec : ∀
  (rangeStartPosLine rangeStartPosCharacter rangeEndPosLine rangeEndPosCharacter selectionRangeStartPosLine
    selectionRangeStartPosCharacter selectionRangeEndPosLine selectionRangeEndPosCharacter : ℕ),
  sizeOf
      { rangeStartPosLine := rangeStartPosLine, rangeStartPosCharacter := rangeStartPosCharacter,
        rangeEndPosLine := rangeEndPosLine, rangeEndPosCharacter := rangeEndPosCharacter,
        selectionRangeStartPosLine := selectionRangeStartPosLine,
        selectionRangeStartPosCharacter := selectionRangeStartPosCharacter,
        selectionRangeEndPosLine := selectionRangeEndPosLine,
        selectionRangeEndPosCharacter := selectionRangeEndPosCharacter } =
    1 + sizeOf rangeStartPosLine + sizeOf rangeStartPosCharacter + sizeOf rangeEndPosLine +
              sizeOf rangeEndPosCharacter +
            sizeOf selectionRangeStartPosLine +
          sizeOf selectionRangeStartPosCharacter +
        sizeOf selectionRangeEndPosLine +
      sizeOf selectionRangeEndPosCharacter
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
_private.Mathlib.MeasureTheory.Function.SpecialFunctions.Inner.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Data.Nat.SuccPred
Nat.le_succ_iff_eq_or_le : ∀ {m n : ℕ}, m ≤ n.succ ↔ m = n.succ ∨ m ≤ n