mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_assoc : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e)
  {Z : a ⟶ e}
  (h_1 :
    CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h i)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom) h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom h_1)
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- A nonsquare is a natural number that is not equal to the square of an
integer. This is implemented as a typeclass because it's a necessary condition
for much of the Pell equation theory.  -/
Zsqrtd.Nonsquare : ℕ → Prop
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.finitePresentation : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] (f : Polynomial R) [inst_1 : CommRing S] [inst_2 : Algebra S R]
  [Algebra.FinitePresentation S R], Algebra.FinitePresentation S (AdjoinRoot f)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  {k k' fallback : α} {f : β → β},
  (Std.DTreeMap.Const.modify t k f).getKeyD k' fallback =
    if cmp k k' = Ordering.eq then if k ∈ t then k else fallback else t.getKeyD k' fallback
-- Lean.Expr
Lean.Int.mkInstHAdd : Lean.Expr
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.UnusedSimpArgsInfo.mk.inj : ∀ {mask mask_1 : Array Bool}, { mask := mask } = { mask := mask_1 } → mask = mask_1
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- **Alias** of `sub_apply`. -/
SlashInvariantForm.sub_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Sub β}
  {inst_2 : Sub F} [self : IsSubApply F α β] (f g : F) (x : α), (f - g) x = f x - g x
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd : ∀ {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] [NeZero m]
  [hK : IsCyclotomicExtension {m} ℚ K], ¬p ∣ m → P.inertiaDeg ℤ = orderOf ↑p
-- Mathlib.Data.EReal.Inv
EReal.coe_pow : ∀ (x : ℝ) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.graphFunctor_obj : ∀ (X : Type u), CategoryTheory.RelCat.graphFunctor.obj X = X
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Path.interval.eq_1 : ∀ {X : SSet} {n : ℕ} (f : X.Path n) (j l : ℕ) (h : j + l ≤ n), f.interval j l h = SSet.Truncated.Path.interval f j l h
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.infty_smulCommClass : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NonUnitalNormedRing (B i)] {𝕜 : Type u_7} [inst_1 : NormedRing 𝕜]
  [inst_2 : (i : I) → Module 𝕜 (B i)] [inst_3 : ∀ (i : I), IsBoundedSMul 𝕜 (B i)]
  [∀ (i : I), SMulCommClass 𝕜 (B i) (B i)], SMulCommClass 𝕜 ↥(lp B ⊤) ↥(lp B ⊤)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonNatTrans_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [inst_5 : F'.LaxMonoidal] (f : F ⟶ F')
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal f] (X : CategoryTheory.AddMon C),
  ((CategoryTheory.Functor.mapAddMonNatTrans f).app X).hom = f.app X.X
-- Lean.Elab.InfoTree.Main
/-- This does the same job as `realizeGlobalConstNoOverload`; resolving an identifier
syntax to a unique fully resolved name or throwing if there are ambiguities.
But also adds this resolved name to the infotree. This means that when you hover
over a name in the source file you will see the fully resolved name in the hover info. -/
Lean.Elab.realizeGlobalConstNoOverloadWithInfo : Lean.Syntax → optParam (Option Lean.Expr) none → Lean.CoreM Lean.Name
-- Std.Data.TreeSet.Basic
/-- Folds the given function over the elements of the tree set in ascending order.  -/
Std.TreeSet.foldl : {α : Type u} → {cmp : α → α → Ordering} → {δ : Type w} → (δ → α → δ) → δ → Std.TreeSet α cmp → δ
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffAt.vadd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {H'' : Type u_6} [inst_7 : TopologicalSpace H''] {E'' : Type u_7}
  [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {I'' : ModelWithCorners 𝕜 E'' H''} {G : Type u_8}
  [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H G] {M : Type u_9} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace H'' N]
  [inst_16 : VAdd G M] {n : WithTop ℕ∞} [ContMDiffVAdd I I' n G M] {f : N → G} {g : N → M} {x : N},
  ContMDiffAt I'' I n f x → ContMDiffAt I'' I' n g x → ContMDiffAt I'' I' n (f +ᵥ g) x
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.mk : {α : Type u_5} →
  {β : Type u_6} →
    [inst : TopologicalSpace α] →
      [inst_1 : Zero β] →
        [inst_2 : TopologicalSpace β] →
          (toContinuousMap : C(α, β)) → HasCompactSupport toContinuousMap.toFun → CompactlySupportedContinuousMap α β
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.cancel_right : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] {g₁ g₂ : N →ₙ* P}
  {f : M →ₙ* N}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Algebra.Group.Basic
neg_bijective : ∀ {G : Type u_3} [inst : InvolutiveNeg G], Function.Bijective Neg.neg
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.d₁_eq' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' →
    ∀ (i₂ : I₂) (j : J),
      HomologicalComplex.mapBifunctor.d₁ K₁ K₂ F c i₁ i₂ j =
        c₁.ε₁ c₂ c (i₁, i₂) •
          CategoryTheory.CategoryStruct.comp ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
            (K₁.ιMapBifunctorOrZero K₂ F c i₁' i₂ j)
-- Mathlib.Order.Filter.IsBounded
Filter.IsCobounded.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop) (f : Filter α),
  Filter.IsCobounded r f = ∃ b, ∀ (a : α), (∀ᶠ (x : α) in f, r x a) → r b a
-- Mathlib.Order.Hom.Basic
/-- The "forgetful functor" from `α →o β` to `α → β` that takes the underlying function,
is monotone.  -/
OrderHom.coeFnHom : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) →o α → β
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- Integrals are invariant when functions change along discrete sets.  -/
intervalIntegral.integral_congr_codiscreteWithin : ∀ {a b : ℝ} {f₁ f₂ : ℝ → ℝ},
  f₁ =ᶠ[Filter.codiscreteWithin (Set.uIoc a b)] f₂ → ∫ (x : ℝ) in a..b, f₁ x = ∫ (x : ℝ) in a..b, f₂ x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_insert_le_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {k : α} {v : β k} {fallback : α}, (cmp ((t.insert k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup_of_singleton_bijective : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {a : α},
  Function.Bijective ⇑(SubMulAction.ofFixingSubgroup_of_singleton M a)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- A morphism between sheaves of modules is a morphism between the underlying
presheaves of modules.  -/
SheafOfModules.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} → SheafOfModules R → SheafOfModules R → Type (max u₁ v)
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.uniformContinuous_mk : ∀ {α : Type u} [inst : UniformSpace α], UniformContinuous SeparationQuotient.mk
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.powerFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (α : Type t)
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] (U : CategoryTheory.Limits.FormalCoproduct C),
  (CategoryTheory.Limits.FormalCoproduct.powerFunctor α).obj U = U.power α
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.coeffs_lc : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M} (h : Module.DualBases e ε) (l : ι →₀ R), h.coeffs (Module.DualBases.lc e l) = l
-- Init.Data.List.BasicAux
List.sizeOf_lt_of_mem : ∀ {α : Type u_1} {a : α} [inst : SizeOf α] {as : List α}, a ∈ as → sizeOf a < sizeOf as
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.mulL.injEq : ∀ (k : ℕ) (a : Nat.Internal.Linear.Expr) (k_1 : ℕ) (a_1 : Nat.Internal.Linear.Expr),
  (Nat.Internal.Linear.Expr.mulL k a = Nat.Internal.Linear.Expr.mulL k_1 a_1) = (k = k_1 ∧ a = a_1)
-- Mathlib.Tactic.DefEqTransformations
/-- `eta_struct at loc` transforms structure constructor applications such as `S.mk x.1 ... x.n`
(pretty printed as, for example, `{a := x.a, b := x.b, ...}`) into `x`.
This also exists as a `conv`-mode tactic.

The transformation is known as eta reduction for structures, and it yields definitionally
equal expressions.

For example, given `x : α × β`, then `(x.1, x.2)` becomes `x` after this transformation.
 -/
Mathlib.Tactic.convEta_struct : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBumpBase.eq_one : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (self : ContDiffBumpBase E) (R : ℝ),
  1 < R → ∀ (x : E), ‖x‖ ≤ 1 → self.toFun R x = 1
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNIndepSet.isIndepSet : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α}, G.IsNIndepSet n s → G.IsIndepSet ↑s
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.snd_natCast : ∀ {q : ℕ} (n : ℕ), (↑n).2 = 0
-- Mathlib.Data.Fin.Tuple.Basic
Fin.removeNth_fun_const : ∀ {α : Type u_3} {n : ℕ} (i : Fin (n + 1)) (a : α), (i.removeNth fun x => a) = fun x => a
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.IsDecompOn.of_leftInvOn : ∀ {X : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] {f g : X → X} {A : Set X} {S : Finset G},
  Equidecomp.IsDecompOn f A S → Set.LeftInvOn g f A → Equidecomp.IsDecompOn g (f '' A) S⁻¹
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsMarkovKernel.isProbabilityMeasure : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [self : ProbabilityTheory.IsMarkovKernel κ] (a : α), MeasureTheory.IsProbabilityMeasure (κ a)
-- Mathlib.Algebra.Order.Floor.Defs
/-- A natural number `n` is smaller than `FloorSemiring.floor a` iff its coercion to `α` is
smaller than `a`.  -/
FloorSemiring.gc_floor : ∀ {α : Type u_4} {inst : Semiring α} {inst_1 : PartialOrder α} [self : FloorSemiring α] {a : α} {n : ℕ},
  0 ≤ a → (n ≤ FloorSemiring.floor a ↔ ↑n ≤ a)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverTerms.next.inj : ∀ {solverId : ℕ} {e : Lean.Expr} {rest : Lean.Meta.Grind.SolverTerms} {solverId_1 : ℕ} {e_1 : Lean.Expr}
  {rest_1 : Lean.Meta.Grind.SolverTerms},
  Lean.Meta.Grind.SolverTerms.next solverId e rest = Lean.Meta.Grind.SolverTerms.next solverId_1 e_1 rest_1 →
    solverId = solverId_1 ∧ e = e_1 ∧ rest = rest_1
-- Lean.Elab.Do.Basic
Lean.Elab.Do.CodeLiveness.alive.sizeOf_spec : sizeOf Lean.Elab.Do.CodeLiveness.alive = 1
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
instIsRegularCardinalOrderOfSubsingleton : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [Subsingleton α], IsRegularCardinalOrder α
-- Mathlib.Order.Interval.Finset.Defs
LocallyFiniteOrderTop.ofIci.eq_1 : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : DecidableEq α] (finsetIci : α → Finset α)
  (mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x),
  LocallyFiniteOrderTop.ofIci α finsetIci mem_Ici =
    { finsetIoi := fun a => {x ∈ finsetIci a | a ≠ x}, finsetIci := finsetIci, finset_mem_Ici := mem_Ici,
      finset_mem_Ioi := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.coreMonoidalTransport_μIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (i : F ≅ G) (X Y : C),
  ((CategoryTheory.Functor.Monoidal.coreMonoidalTransport i).μIso X Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (i.inv.app X) (i.inv.app Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
        (i.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)))
-- Mathlib.Geometry.Convex.Cone.DualFinite
/-- **Alias** of `PointedCone.DualFG.dual_of_fg`.

---

The dual of a finitely generated cone is dually finitely generated.  -/
PointedCone.FG.dual_dualfg : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  (p : M →ₗ[R] N →ₗ[R] R) {C : PointedCone R M}, Submodule.FG C → PointedCone.DualFG p (PointedCone.dual p ↑C)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.r_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s : S.Splitting) {Z : C} (h : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp s.r (CategoryTheory.CategoryStruct.comp S.f h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id S.X₂ - CategoryTheory.CategoryStruct.comp S.g s.s) h
-- Init.Data.Array.Perm
Array.Perm.mem_iff : ∀ {α : Type u_1} {a : α} {xs ys : Array α}, xs.Perm ys → (a ∈ xs ↔ a ∈ ys)
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_pred_self : ∀ {n : ℕ} (p : Fin (n + 1)) (h : p ≠ 0), p.succAbove (p.pred h) = (p.pred h).castSucc
-- Mathlib.Order.RelClasses
instTrichotomousGe : ∀ {α : Type u} [inst : LinearOrder α], Std.Trichotomous fun x1 x2 => x2 ≤ x1
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.instTopologicalSpace.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  ContinuousAddMonoidHom.instTopologicalSpace A B =
    TopologicalSpace.induced ContinuousAddMonoidHom.toContinuousMap ContinuousMap.compactOpen
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.singleOneRingHom_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] (a : R),
  MonoidAlgebra.singleOneRingHom a = (↑(MonoidAlgebra.singleAddHom 1)).toFun a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.isAddUnit_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SubtractionMonoid α] {s : Finset α},
  IsAddUnit s ↔ ∃ a, s = {a} ∧ IsAddUnit a
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
CliffordAlgebra.GradedAlgebra.lift_ι_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (i' : ZMod 2) (x' : ↥(CliffordAlgebra.evenOdd Q i')),
  ((CliffordAlgebra.lift Q) ⟨CliffordAlgebra.GradedAlgebra.ι Q, ⋯⟩) ↑x' =
    (DirectSum.of (fun i => ↥(CliffordAlgebra.evenOdd Q i)) i') x'
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_id : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α}, ContinuousWithinAt id s x
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalAlgHom.equalizer.congr_simp : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (ϕ ϕ_1 : F),
  ϕ = ϕ_1 → ∀ (ψ ψ_1 : F), ψ = ψ_1 → NonUnitalAlgHom.equalizer ϕ ψ = NonUnitalAlgHom.equalizer ϕ_1 ψ_1
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_eq_ite : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} {f : ι → M} (a : ι),
  (∀ b ∈ s, b ≠ a → f b = 0) → ∑ x ∈ s, f x = if a ∈ s then f a else 0
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstr.mk.injEq : ∀ (p : Int.Internal.Linear.Poly) (h : Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof) (p_1 : Int.Internal.Linear.Poly)
  (h_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof), ({ p := p, h := h } = { p := p_1, h := h_1 }) = (p = p_1 ∧ h = h_1)
-- Mathlib.Data.Finite.Prod
Pi.finite : ∀ {α : Sort u_3} {β : α → Sort u_4} [Finite α] [∀ (a : α), Finite (β a)], Finite ((a : α) → β a)
-- Mathlib.Order.Disjoint
disjoint_subtype_iff : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {pr : α → Prop},
  (∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)) → ∀ (hbot : pr ⊥) {a b : Subtype pr}, Disjoint a b ↔ Disjoint ↑a ↑b
-- Mathlib.Algebra.PresentedMonoid.Basic
_private.Mathlib.Algebra.PresentedMonoid.Basic.0.PresentedMonoid.termP₂ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The projection onto the first summand of a binary biproduct.  -/
CategoryTheory.Limits.biprod.fst : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] → X ⊞ Y ⟶ X
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.hom_inv_associator : ∀ {R : Type u} [inst : CommSemiring R] {M N K : SemimoduleCat R},
  SemimoduleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).inv =
    ↑(TensorProduct.assoc R ↑M ↑N ↑K).symm
-- Mathlib.Probability.Process.PartitionFiltration
ProbabilityTheory.iSup_partitionFiltration : ∀ {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)),
  MeasurableSpace.generateFrom (Set.range t) = m → ⨆ n, ↑(ProbabilityTheory.partitionFiltration ht) n = m
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.inclusion_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.Core C} (f : X ⟶ Y),
  (CategoryTheory.Core.inclusion C).map f = f.iso.hom
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_orbit_of_mem_orbit_addSubgroup : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : AddSubgroup G} {a b : α},
  a ∈ AddAction.orbit (↥H) b → a ∈ AddAction.orbit G b
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.id_apply : ∀ (R : Type u) [inst : Semiring R] (M : CategoryTheory.Mat R) (i j : M.obj),
  CategoryTheory.CategoryStruct.id M i j = if i = j then 1 else 0
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_tensor_comp_tensor_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  (f : W ⟶ X) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Y) f)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id X)) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom g f
-- Init.Notation
/-- The attribute `@[deprecated]` on a declaration indicates that the declaration
is discouraged for use in new code, and/or should be migrated away from in
existing code. It may be removed in a future version of the library.

* `@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
* `@[deprecated myBetterDef "use myBetterDef instead"]` allows customizing the deprecation message.
* `@[deprecated (since := "2024-04-21")]` records when the deprecation was first applied.
 -/
Lean.deprecated : Lean.ParserDescr
-- Mathlib.Topology.MetricSpace.HausdorffDimension
Real.dimH_ne_top : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (s : Set E),
  dimH s ≠ ⊤
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_lt_iff_lt : ∀ {a b : ℕ} (ha : a < UInt8.size) (hb : b < UInt8.size), UInt8.ofNatLT a ha < UInt8.ofNatLT b hb ↔ a < b
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaAssocProd_symm_apply_fst : ∀ {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a : (a : α) × (b : β) × γ a b),
  (Equiv.sigmaAssocProd.symm a).fst = (((Equiv.sigmaAssoc γ).symm a).fst.fst, ((Equiv.sigmaAssoc γ).symm a).fst.snd)
-- Mathlib.Order.Filter.Pointwise
Filter.pow_mem_pow : ∀ {α : Type u_2} [inst : Monoid α] {f : Filter α} {s : Set α}, s ∈ f → ∀ (n : ℕ), s ^ n ∈ f ^ n
-- Mathlib.Data.Fintype.Order
/-- A nonempty finite lattice is complete. If the lattice is already a `BoundedOrder`, then use
`Fintype.toCompleteLattice` instead, as this gives definitional equality for `⊥` and `⊤`.  -/
Fintype.toCompleteLatticeOfNonempty : (α : Type u_2) → [Fintype α] → [Nonempty α] → [Lattice α] → CompleteLattice α
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isLongestMatchAtChain_startPos_endPos_iff_toList : ∀ {p : Char → Bool} {s : String.Slice},
  String.Slice.Pattern.Model.IsLongestMatchAtChain p s.startPos s.endPos ↔ ∀ c ∈ s.copy.toList, p c = true
-- Mathlib.RingTheory.ClassGroup.Basic
toPrincipalIdeal.congr_simp : ∀ (R : Type u_3) (K : Type u_4) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K], toPrincipalIdeal R K = toPrincipalIdeal R K
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.toTransfiniteCompositionOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          [inst_3 : SuccOrder J] →
            [inst_4 : WellFoundedLT J] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} →
                    {X Y : C} →
                      {f : X ⟶ Y} →
                        HomotopicalAlgebra.RelativeCellComplex basicCell f →
                          CategoryTheory.TransfiniteCompositionOfShape J f
-- Mathlib.Topology.Separation.GDelta
IsGδ.compl_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X) [T1Space X], IsGδ {x}ᶜ