mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The canonical projection into the colimit, as a quotient type.  -/
AddGrpCat.FilteredColimits.G.mk : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J AddGrpCat) → (j : J) × ↑(F.obj j) → ↑(AddGrpCat.FilteredColimits.G F)
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcReleaseParams.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (sessionId : UInt64) (refs : Array Lean.Json),
  sizeOf { uri := uri, sessionId := sessionId, refs := refs } = 1 + sizeOf uri + sizeOf sessionId + sizeOf refs
-- Std.Sat.AIG.CachedLemmas
/-- The central equality theorem between `mkAtomCached` and `mkAtom`.
 -/
Std.Sat.AIG.mkAtomCached_eval_eq_mkAtom_eval : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {var : α} {aig : Std.Sat.AIG α},
  ⟦assign, aig.mkAtomCached var⟧ = ⟦assign, aig.mkAtom var⟧
-- Lean.Elab.BuiltinTerm
_private.Lean.Elab.BuiltinTerm.0.Lean.Elab.Term.mkFreshTypeMVarFor : Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.DischargeResult.maxDepth : Lean.Meta.Simp.DischargeResult
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.edges_eq_zipWith_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v},
  p.edges = List.zipWith (fun x1 x2 => s(x1, x2)) p.support p.support.tail
-- Mathlib.Probability.Moments.Basic
/-- **Chernoff bound** on the lower tail of a real random variable.  -/
ProbabilityTheory.measure_le_le_exp_cgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ}
  [MeasureTheory.IsFiniteMeasure μ] (ε : ℝ),
  t ≤ 0 →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      μ.real {ω | X ω ≤ ε} ≤ Real.exp (-t * ε + ProbabilityTheory.cgf X μ t)
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.instSmallLMultispanShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C] [CategoryTheory.MorphismProperty.IsSmall.{w, v, u} W]
  [CategoryTheory.LocallySmall.{w, v, u} C],
  Small.{w, max u v} (CategoryTheory.OrthogonalReflection.D₂.multispanShape W Z).L
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.instLattice : Lattice ℚ
-- Lean.Elab.Deriving.Basic
Lean.Elab.DerivingClassView.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (hasExpose : Bool) (cls : Lean.Term),
  sizeOf { ref := ref, hasExpose := hasExpose, cls := cls } = 1 + sizeOf ref + sizeOf hasExpose + sizeOf cls
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A coequalizer morphism is an epimorphism  -/
CategoryTheory.Limits.coequalizer.π_epi : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g], CategoryTheory.Epi (CategoryTheory.Limits.coequalizer.π f g)
-- Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
MeasureTheory.measurableEquiv_range_coe_nat_of_infinite_of_countable : ∀ (α : Type u_1) [inst : MeasurableSpace α] [StandardBorelSpace α] [Infinite α] [Countable α],
  Nonempty (α ≃ᵐ ↑(Set.range Nat.cast))
-- Std.Data.ExtDTreeMap.Basic
/-- Computes the union of the given tree maps. If a key appears in both maps, the entry contained in
the second argument will appear in the result.

This function always merges the smaller map into the larger map.
 -/
Std.ExtDTreeMap.inter : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α β cmp → Std.ExtDTreeMap α β cmp
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Slice.Model.positionsFrom.eq_1 : ∀ {s : String.Slice} (p : s.Pos),
  String.Slice.Model.positionsFrom p =
    if h : p.IsAtEnd then [] else ⟨p, h⟩ :: String.Slice.Model.positionsFrom (p.next h)
-- Mathlib.Analysis.Convex.Between
Sbtw.right_mem_image_Ioi : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Sbtw R x y z → z ∈ ⇑(AffineMap.lineMap x y) '' Set.Ioi 1
-- Init.Data.List.Sublist
List.prefix_concat_iff : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α}, l₁ <+: l₂ ++ [a] ↔ l₁ = l₂ ++ [a] ∨ l₁ <+: l₂
-- Mathlib.CategoryTheory.Pi.Basic
/-- The evaluation functor at `i : I`, sending an `I`-indexed family of objects to the object over `i`.
 -/
CategoryTheory.Pi.eval : {I : Type w₀} →
  (C : I → Type u₁) →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] → (i : I) → CategoryTheory.Functor ((i : I) → C i) (C i)
-- Init.System.IO
/-- The number of whole seconds.  -/
IO.FS.SystemTime.sec : IO.FS.SystemTime → ℤ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceAbs : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.List.Chain
WellFounded.asymmetricₙ : ∀ {α : Type u_1} {r : α → α → Prop} {l : List α},
  WellFounded r → ∀ (hne : l ≠ []), List.IsChain r l → ¬r (l.getLast hne) (l.head hne)
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_submatrix : ∀ {X : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace R] {A : X → Matrix l n R},
  Continuous A → ∀ (e₁ : m → l) (e₂ : p → n), Continuous fun x => (A x).submatrix e₁ e₂
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_insert_le_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α} {v : β k}, (cmp (t.insert k v).minKey! t.minKey!).isLE = true
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α},
  m.WF → (k ∈ Std.DHashMap.Raw.filterMap f m ↔ ∃ (h : k ∈ m), (f k (m.get k h)).isSome = true)
-- Init.Try
/-- If `missing` is `true`, allows the construction of partial solutions where some of the subgoals are `sorry`.  -/
Lean.Try.Config.missing : Lean.Try.Config → Bool
-- Mathlib.NumberTheory.Real.Irrational
Irrational.mul_ratCast : ∀ {x : ℝ}, Irrational x → ∀ {q : ℚ}, q ≠ 0 → Irrational (x * ↑q)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.lift.congr_simp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f f_1 : X ⟶ Z) (e_f : f = f_1) (g g_1 : Y ⟶ Z) (e_g : g = g_1)
  [H : AlgebraicGeometry.IsOpenImmersion f] (H' : Set.range ⇑g ⊆ Set.range ⇑f),
  AlgebraicGeometry.IsOpenImmersion.lift f g H' = AlgebraicGeometry.IsOpenImmersion.lift f_1 g_1 ⋯
-- Std.Time.DateTime
/-- Creates a new `DateTime` by adjusting the `second` component.
 -/
Std.Time.DateTime.withSeconds : Std.Time.DateTime → Std.Time.Second.Ordinal true → Std.Time.DateTime
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.tendsto_stieltjesOfMeasurableRat_atBot : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : Measurable f) (a : α),
  Filter.Tendsto (↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a)) Filter.atBot (nhds 0)
-- Lean.Data.Trie
_private.Lean.Data.Trie.0.Lean.Data.Trie.find?.loop : {α : Type} → String → ℕ → Lean.Data.Trie α → Option α
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.instSmooth : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Etale f], AlgebraicGeometry.Smooth f
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.some_getEntryLE_eq_getEntryLE? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (t : Std.DTreeMap.Internal.Impl α β)
  {ho : t.Ordered} {he : ∃ a ∈ t, (compare a k).isLE = true},
  some (Std.DTreeMap.Internal.Impl.getEntryLE k t ho he) = Std.DTreeMap.Internal.Impl.getEntryLE? k t
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.listSum_map : ∀ {α : Type u_1} {n : ℤ} {l : List α} {f g : α → ℤ},
  (∀ x ∈ l, f x ≡ g x [ZMOD n]) → (List.map f l).sum ≡ (List.map g l).sum [ZMOD n]
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.IsAscendingCentralSeries`.

---

A sequence of subgroups of `G` is an ascending central series if `H 0` is trivial and
`⁅H (n + 1), G⁆ ⊆ H n` for all `n`. Note that we do not require that `H n = G` for some `n`.  -/
IsAscendingCentralSeries : {G : Type u_1} → [inst : Group G] → (ℕ → Subgroup G) → Prop
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.mulAntidiagonal_subtype_ext_iff : ∀ {A : Type u_1} [inst : CancelMonoid A] [inst_1 : Finset.HasMulAntidiagonal A] {n : A}
  {p q : ↥(Finset.HasMulAntidiagonal.mulAntidiagonal n)}, p = q ↔ (↑p).1 = (↑q).1
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.hasSum_nat_cosKernel₀ : ∀ (a : ℝ) {t : ℝ},
  0 < t →
    HasSum (fun n => 2 * Real.cos (2 * Real.pi * a * (↑n + 1)) * Real.exp (-Real.pi * (↑n + 1) ^ 2 * t))
      (HurwitzZeta.cosKernel (↑a) t - 1)
-- Mathlib.Topology.Algebra.SeparationQuotient.Section
SeparationQuotient.outCLM_uniformContinuous : ∀ (K : Type u_1) (E : Type u_2) [inst : DivisionRing K] [inst_1 : AddCommGroup E] [inst_2 : Module K E]
  [inst_3 : UniformSpace E] [inst_4 : IsUniformAddGroup E] [inst_5 : ContinuousConstSMul K E],
  UniformContinuous ⇑(SeparationQuotient.outCLM K E)
-- Mathlib.CategoryTheory.Localization.Bousfield
/-- Given `P : ObjectProperty C`, this is the class of morphisms `g : Y ⟶ Z`
such that for all `X : C` such that `P X`, the postcomposition with `g` induces
a bijection `(X ⟶ Y) ≃ (X ⟶ Z)`. (One of the applications of this notion
is the right Bousfield localization of model categories.)  -/
CategoryTheory.ObjectProperty.isColocal : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.ObjectProperty C → CategoryTheory.MorphismProperty C
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.ListSlice.internalIter_eq.match_1.eq_2 : ∀ (motive : Option ℕ → Sort u_1) (h_1 : (stop : ℕ) → motive (some stop)) (h_2 : Unit → motive none),
  (match none with
    | some stop => h_1 stop
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.epic_of_localizationMap : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {P : Type u_4} [inst_2 : AddMonoid P] {j k : N →+ P},
  j.comp f.toAddMonoidHom = k.comp f.toAddMonoidHom → j = k
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- The norm of a maximal ideal is a prime power.
The prime is `(P.under ℤ).absNorm` and the exponent is `(P.under ℤ).inertialDeg P`.
See `Ideal.absNorm_pow_inertiaDeg`.  -/
Ideal.exists_prime_and_absNorm_eq_pow : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  (P : Ideal S) [P.IsMaximal], ∃ p n, 0 < n ∧ ↑p ∈ P ∧ Nat.Prime p ∧ Ideal.absNorm P = p ^ n
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.lift_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M M' : CategoryTheory.Functor C MonCat} (p : M ⟶ M')
  (S' : CategoryTheory.SubmonoidFunctor M') (hp : CategoryTheory.SubmonoidFunctor.image p ⊤ ≤ S')
  {Z : CategoryTheory.Functor C MonCat} (h : M' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SubmonoidFunctor.lift p S' hp)
      (CategoryTheory.CategoryStruct.comp S'.ι h) =
    CategoryTheory.CategoryStruct.comp p h
-- Mathlib.Analysis.Analytic.Basic
AnalyticWithinAt.mono_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s t : Set E}
  {x : E}, AnalyticWithinAt 𝕜 f s x → s ∈ nhdsWithin x t → AnalyticWithinAt 𝕜 f t x
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zero_mem_zero : ∀ {α : Type u_2} [inst : Zero α], 0 ∈ 0
-- Mathlib.LinearAlgebra.Contraction
dualTensorHom_bijective_of_finite_left_projective_right : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] [Module.Finite R M] [Module.Projective R N],
  Function.Bijective ⇑(dualTensorHom R M N)
-- Mathlib.Combinatorics.Hindman
/-- Constructor for `FS`. This is the preferred spelling over `FS.tail'`.  -/
Hindman.FS.tail : ∀ {M : Type u_1} [inst : AddSemigroup M] (a : Stream' M) (m : M), Hindman.FS a.tail m → m ∈ Hindman.FS a
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.zsmul_apply : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (r : ℤ)
  (f : NormedAddGroupHom V₁ V₂) (v : V₁), (r • f) v = r • f v
-- Init.Data.Fin.Basic
/-- Bitwise xor (“exclusive or”).
 -/
Fin.xor : {n : ℕ} → Fin n → Fin n → Fin n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constEntryAtIdx!_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {i : ℕ} [inst : Inhabited (α × β)],
          Std.DTreeMap.Internal.Impl.Const.entryAtIdx! t₁ i = Std.DTreeMap.Internal.Impl.Const.entryAtIdx! t₂ i
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageMap.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g}
  (map : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom)
  (map_ι :
    autoParam
      (CategoryTheory.CategoryStruct.comp map (CategoryTheory.Limits.image.ι g.hom) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq))
      CategoryTheory.Limits.ImageMap.map_ι._autoParam)
  (map_1 : CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom)
  (map_ι_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp map_1 (CategoryTheory.Limits.image.ι g.hom) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) (CategoryTheory.Arrow.Hom.right sq))
      CategoryTheory.Limits.ImageMap.map_ι._autoParam),
  ({ map := map, map_ι := map_ι } = { map := map_1, map_ι := map_ι_1 }) = (map = map_1)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α} (h : k ∈ m),
  (m.get k h == k) = true
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- This is not covered by `Pi.opensMeasurableSpace` as it does not require second countability.  -/
Pi.opensMeasurableSpace_of_subsingleton : ∀ {ι : Type u_6} {X : ι → Type u_7} [Subsingleton ι] [inst : (i : ι) → TopologicalSpace (X i)]
  [inst_1 : (i : ι) → MeasurableSpace (X i)] [∀ (i : ι), OpensMeasurableSpace (X i)],
  OpensMeasurableSpace ((i : ι) → X i)
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Let `e` be a trivialization of a `C^n` vector bundle `E₁` over `B`. Then `m ↦ e.symmL 𝕜 m`
defines a section of the bundle of continuous linear maps `F₁ →L[𝕜] E₁` over `B`, and this section
is `C^n` on `e.baseSet`.  -/
Bundle.Trivialization.contMDiffOn_symmL : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {EB : Type u_4}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_5} [inst_3 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B] {E₁ : B → Type u_6}
  [inst_6 : (x : B) → AddCommGroup (E₁ x)] [inst_7 : (x : B) → Module 𝕜 (E₁ x)] [inst_8 : NormedAddCommGroup F₁]
  [inst_9 : NormedSpace 𝕜 F₁] [inst_10 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_11 : (x : B) → TopologicalSpace (E₁ x)] [inst_12 : ∀ (x : B), IsTopologicalAddGroup (E₁ x)]
  [inst_13 : ∀ (x : B), ContinuousSMul 𝕜 (E₁ x)] [inst_14 : FiberBundle F₁ E₁] [inst_15 : VectorBundle 𝕜 F₁ E₁]
  [ContMDiffVectorBundle n F₁ E₁ IB] (e : Bundle.Trivialization F₁ Bundle.TotalSpace.proj)
  [inst_17 : MemTrivializationAtlas e],
  ContMDiffOn IB (IB.prod (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₁))) n (fun m => ⟨m, Bundle.Trivialization.symmL 𝕜 e m⟩)
    e.baseSet
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCardAux_eq_map_coe : ∀ {α : Type u_1} {n : ℕ} {l : List α}, Multiset.powersetCardAux n l = List.map Multiset.ofList (List.sublistsLen n l)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd_zero_add_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A) (X : C),
  (CategoryTheory.shiftFunctorAdd C 0 a).hom.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      ((CategoryTheory.shiftFunctor C a).map ((CategoryTheory.shiftFunctorZero C A).inv.app X))
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α], Finset.neg = { neg := Finset.image Neg.neg }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- The pushout cocone obtained by pasting two pushout cocones horizontally.  -/
CategoryTheory.Limits.PushoutCocone.pasteHoriz : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ : C} →
      {f₁ : X₁ ⟶ X₂} →
        {f₂ : X₂ ⟶ X₃} →
          {i₁ : X₁ ⟶ Y₁} →
            (t₁ : CategoryTheory.Limits.PushoutCocone i₁ f₁) →
              {i₂ : X₂ ⟶ t₁.pt} →
                CategoryTheory.Limits.PushoutCocone i₂ f₂ →
                  i₂ = t₁.inr → CategoryTheory.Limits.PushoutCocone i₁ (CategoryTheory.CategoryStruct.comp f₁ f₂)
-- Mathlib.Combinatorics.Derangements.Basic
mem_derangements_iff_fixedPoints_eq_empty : ∀ {α : Type u_1} {f : Equiv.Perm α}, f ∈ derangements α ↔ Function.fixedPoints ⇑f = ∅
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.reindex_trans : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {l₂ : Type u_10} {o₂ : Type u_11}
  (eₘ : m ≃ l) (eₙ : n ≃ o) (eₘ₂ : l ≃ l₂) (eₙ₂ : o ≃ o₂),
  (Matrix.reindex eₘ eₙ).trans (Matrix.reindex eₘ₂ eₙ₂) = Matrix.reindex (eₘ.trans eₘ₂) (eₙ.trans eₙ₂)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_le_maxKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {k : α} {v : β}, (cmp t.maxKey! (t.insert k v).maxKey!).isLE = true
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_C : ∀ {R : Type u_1} [inst : Semiring R] (r : R), (Polynomial.C r).eraseLead = 0
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Martingale.congr : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f g : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E],
  MeasureTheory.Martingale f ℱ μ →
    MeasureTheory.StronglyAdapted ℱ g → (∀ (t : ι), f t =ᵐ[μ] g t) → MeasureTheory.Martingale g ℱ μ
-- Mathlib.Order.Interval.Finset.Basic
/-- In a locally finite preorder, `<` is the transitive closure of `⋖`.  -/
lt_iff_transGen_covBy : ∀ {α : Type u_2} [inst : Preorder α] [LocallyFiniteOrder α] {x y : α},
  x < y ↔ Relation.TransGen (fun x1 x2 => x1 ⋖ x2) x y
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMap_eq_prependMapGT_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (r : Std.DTreeMap.Internal.Impl α β)
  (z : Std.DTreeMap.Internal.Zipper α β) (lowerBound : α),
  r.Ordered →
    (∀ e ∈ r.toList, compare lowerBound e.fst = Ordering.lt) →
      Std.DTreeMap.Internal.Zipper.prependMap r z = Std.DTreeMap.Internal.Zipper.prependMapGT r lowerBound z
-- Mathlib.RingTheory.HopfAlgebra.Quotient
HopfAlgebra.Quotient.instHopfAlgebraStructQuotientIdeal : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] →
        [inst_2 : HopfAlgebraStruct R A] →
          (I : Ideal A) → [inst_3 : I.IsTwoSided] → [Ideal.IsHopfIdeal R I] → HopfAlgebraStruct R (A ⧸ I)
-- Mathlib.Data.Set.Card
Set.ncard_eq_ncard_iff_ncard_sdiff_eq_ncard_sdiff : ∀ {α : Type u_1} {s t : Set α},
  autoParam s.Finite Set.ncard_eq_ncard_iff_ncard_sdiff_eq_ncard_sdiff._auto_1 →
    autoParam t.Finite Set.ncard_eq_ncard_iff_ncard_sdiff_eq_ncard_sdiff._auto_3 →
      (s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard)
-- Mathlib.Analysis.InnerProductSpace.LinearMap
ContinuousLinearMap.reApplyInnerSelf_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) (x : E), T.reApplyInnerSelf x = RCLike.re (inner 𝕜 (T x) x)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_matrix : ∀ {J : Type} [inst : Finite J] {K : Type} [inst_1 : Finite K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C}
  {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
      (CategoryTheory.Limits.biproduct.matrix m) =
    CategoryTheory.Limits.biproduct.lift fun k => m j k
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
Finset.invMulSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A : Finset G) (h : ↑(A * A).card < 3 / 2 * ↑A.card),
  A.invMulSubgroup h = { carrier := ↑A⁻¹ * ↑A, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Lean.Elab.Tactic.SimpTrace
/-- Constructs the syntax for a simp call, for use with `simp?`.  -/
Lean.Elab.Tactic.mkSimpCallStx : Lean.Syntax → Lean.Meta.Simp.UsedSimps → Lean.MetaM (Lean.TSyntax `tactic)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.instAddCommGroup : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Projective F} → AddCommGroup W.Point
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_self : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.add P P = W'.dblXYZ P
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
List.prod_pos : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R]
  [NeZero 1] {s : List R}, (∀ a ∈ s, 0 < a) → 0 < s.prod
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α], |1|ₘ = 1
-- Mathlib.Data.Holor
Holor.zero_mul : ∀ {ds₁ ds₂ : List ℕ} {α : Type} [inst : MulZeroClass α] (x : Holor α ds₂), Holor.mul 0 x = 0
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_surjective : ∀ {n : ℕ} (p : Fin n), Function.Surjective p.predAbove
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.comp_def : ∀ (R : Type u) [inst : Semiring R] {M N K : CategoryTheory.Mat R} (f : M ⟶ N) (g : N ⟶ K),
  CategoryTheory.CategoryStruct.comp f g = fun i k => ∑ j, f i j * g j k
-- Mathlib.Algebra.Category.Ring.Basic
RingEquiv.toSemiRingCatIso_inv : ∀ {R S : Type u} [inst : Semiring R] [inst_1 : Semiring S] (e : R ≃+* S),
  e.toSemiRingCatIso.inv = SemiRingCat.ofHom ↑e.symm
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.getKey? (t.maxKey he) = some (t.maxKey he)
-- Mathlib.SetTheory.Ordinal.Notation
/-- Exponentiation of ordinal notations  -/
NONote.opow : NONote → NONote → NONote
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
/-- The clifford algebra is graded by the even and odd parts.  -/
CliffordAlgebra.gradedAlgebra : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (Q : QuadraticForm R M) → GradedAlgebra (CliffordAlgebra.evenOdd Q)