mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.instFullCompPreRight : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T)
  (L : CategoryTheory.Functor A T) [F.Full], (CategoryTheory.Comma.preRight L F R).Full
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- Strengthening of `IsLocalization.exist_integer_multiples`:
Let `J ≠ ⊤` be an ideal in a Dedekind domain `A`, and `f ≠ 0` a finite collection
of elements of `K = Frac(A)`, then we can multiply the elements of `f` by some `a : K`
to find a collection of elements of `A` that is not completely contained in `J`.  -/
Ideal.exist_integer_multiples_notMem : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [IsDedekindDomain A] [inst_3 : Algebra A K]
  [IsFractionRing A K] {J : Ideal A},
  J ≠ ⊤ →
    ∀ {ι : Type u_4} (s : Finset ι) (f : ι → K) {j : ι},
      j ∈ s → f j ≠ 0 → ∃ a, (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ ↑J
-- Mathlib.Data.Finset.Sum
Finset.toLeft_cons_inr : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {b : β} (hb : Sum.inr b ∉ u),
  (Finset.cons (Sum.inr b) u hb).toLeft = u.toLeft
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.add : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Add β]
  [ContinuousAdd β],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (f + g)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.pushout_inr_iso_of_right_factors_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Z : C} (f : X ⟶ Z) (h : W ⟶ X)
  [inst_1 : CategoryTheory.Epi h],
  CategoryTheory.IsIso (CategoryTheory.Limits.pushout.inr h (CategoryTheory.CategoryStruct.comp h f))
-- Mathlib.Analysis.Complex.IntegerCompl
UpperHalfPlane.coe_mem_integerComplement : ∀ (z : UpperHalfPlane), ↑z ∈ Complex.integerComplement
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_sup_left : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) (p₁ p₂ : Submodule R M) (q : Submodule R N),
  Submodule.map₂ f (p₁ ⊔ p₂) q = Submodule.map₂ f p₁ q ⊔ Submodule.map₂ f p₂ q
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_piecewise_const : ∀ {Ω : Type u_1} {s : Set Ω} [inst : DecidablePred fun x => x ∈ s] {ι' : Type u_4} {α : Type u_5} [inst_1 : Nonempty ι']
  {i j : ι'} {f : ι' → Ω → α},
  MeasureTheory.stoppedValue f (s.piecewise (fun x => ↑i) fun x => ↑j) = s.piecewise (f i) (f j)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α}, k ∉ t₁ → (t₁ \ t₂).get? k = none
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.antilipschitz : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂]
  [inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕),
  AntilipschitzWith 1 ⇑f
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction.le_go_iff : ∀ {pat : ByteArray} {stackPos : ℕ} {hst : stackPos < pat.size} {k k' : ℕ},
  k ≤ String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction.go✝ pat stackPos hst k' ↔
    ∃ k'', k ≤ k'' ∧ k'' ≤ k' ∧ String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat pat k'' (stackPos + 1)
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.AddSemigrp.Hom.mk : {A B : AddSemigrp} → (↑A →ₙ+ ↑B) → A.Hom B
-- Mathlib.Topology.AlexandrovDiscrete
principal_nhdsKer_singleton : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] (a : α), Filter.principal (nhdsKer {a}) = nhds a
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.ofInvolutive_symm : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → α) (hf : Function.Involutive f) (hf' : Measurable f),
  (MeasurableEquiv.ofInvolutive f hf hf').symm = MeasurableEquiv.ofInvolutive f hf hf'
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset : HSub Std.Time.Nanosecond.Offset Std.Time.Millisecond.Offset Std.Time.Nanosecond.Offset
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.vertexSet_bot : ∀ {α : Type u_1} {β : Type u_2}, ⊥.vertexSet = ∅
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.mulForbidden.eq_1 : ∀ {A : Type u_1} {G : Type u_2} [inst : Inhabited A] [inst_1 : Monoid G]
  (F : Set (SymbolicDynamics.FullShift.Pattern A G)),
  SymbolicDynamics.FullShift.mulForbidden F = {x | ∀ p ∈ F, ∀ (g : G), ¬p.mulOccursInAt x g}
-- Mathlib.LinearAlgebra.Matrix.Block
/-- `BlockTriangular` matrices form a subalgebra.  -/
Matrix.blockTriangularSubalgebra : {α : Type u_1} →
  {m : Type u_3} →
    (R : Type v) →
      (A : Type u_8) →
        (m → α) →
          [LinearOrder α] →
            [inst : CommSemiring R] →
              [inst_1 : Semiring A] →
                [inst_2 : Algebra R A] → [inst_3 : DecidableEq m] → [inst_4 : Fintype m] → Subalgebra R (Matrix m m A)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformGroup.uniformity_countably_generated : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] [(nhds 1).IsCountablyGenerated],
  (uniformity α).IsCountablyGenerated
-- Mathlib.NumberTheory.LSeries.Injectivity
/-- The abscissa of absolute convergence of `f + g` is at most the maximum of those
of `f` and `g`.  -/
LSeries.abscissaOfAbsConv_add_le : ∀ (f g : ℕ → ℂ), LSeries.abscissaOfAbsConv (f + g) ≤ max (LSeries.abscissaOfAbsConv f) (LSeries.abscissaOfAbsConv g)
-- Mathlib.Algebra.Module.Congruence.Defs
VAddCon.ker.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : VAdd R M] [inst_1 : VAdd S N] {φ : R → S}
  (f : M →ₑ[φ] N), VAddCon.ker f = { toSetoid := Setoid.ker ⇑f, vadd := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_of_le_of_nonpos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b c : α}, b ≤ c → a ≤ 0 → b + a ≤ c
-- Mathlib.Analysis.Convex.Between
sbtw_iff_mem_image_Ioo_and_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] {x y z : P},
  Sbtw R x y z ↔ y ∈ ⇑(AffineMap.lineMap x z) '' Set.Ioo 0 1 ∧ x ≠ z
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
/-- An alternate constructor for strict pseudofunctors between strict bicategories, that
only requires the data bundled in `StrictPseudofunctorPreCore`.  -/
CategoryTheory.StrictPseudofunctor.mk'' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        [CategoryTheory.Bicategory.Strict B] →
          [CategoryTheory.Bicategory.Strict C] →
            CategoryTheory.StrictPseudofunctorPreCore B C → CategoryTheory.StrictPseudofunctor B C
-- Init.Data.Vector.FinRange
Vector.getElem_finRange : ∀ {n i : ℕ} (h : i < n), (Vector.finRange n)[i] = ⟨i, h⟩
-- Mathlib.Analysis.Complex.Basic
Complex.mul_conj' : ∀ (z : ℂ), z * (starRingEnd ℂ) z = ↑‖z‖ ^ 2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldr_eq_foldr_toArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {f : (a : α) → β a → δ → δ}
  {init : δ}, Std.DTreeMap.Internal.Impl.foldr f init t = Array.foldr (fun a b => f a.fst a.snd b) init t.toArray
-- Mathlib.Algebra.Group.Basic
div_eq_div_iff_mul_eq_mul : ∀ {G : Type u_3} [inst : CommGroup G] {a b c d : G}, a / b = c / d ↔ a * d = c * b
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicator_mono_infEDist : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) {E : Set α} {x y : α},
  Metric.infEDist x E ≤ Metric.infEDist y E → (thickenedIndicator δ_pos E) y ≤ (thickenedIndicator δ_pos E) x
-- Init.Data.List.Basic
/-- Replace the head of the list with the result of applying `f` to it. Returns the empty list if the
list is empty.

Examples:
 * `[1, 2, 3].modifyHead (· * 10) = [10, 2, 3]`
 * `[].modifyHead (· * 10) = []`
 -/
List.modifyHead : {α : Type u} → (α → α) → List α → List α
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyGE! : {α : Type u} → {β : α → Type v} → [Ord α] → [Inhabited α] → α → Std.DTreeMap.Internal.Impl α β → α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.unitOfList_equiv_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {l : List α},
  (Std.DHashMap.Const.unitOfList l).Equiv (List.foldl (fun acc p => acc.insertIfNew p ()) ∅ l)
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
/-- If `C` is a monoidal closed category and `D` is a groupoid, then the functor category `D ⥤ C`,
with the pointwise monoidal structure, is monoidal closed.  -/
CategoryTheory.Functor.monoidalClosed : {D : Type u} →
  {C : Type u_1} →
    [inst : CategoryTheory.Groupoid D] →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalClosed C] → CategoryTheory.MonoidalClosed (CategoryTheory.Functor D C)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : Inhabited α]
  [EquivBEq α] [LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∪ m₂).getKey! k = m₂.getKey! k
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.mem_invtRootSubmodule_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) {q : Submodule R M},
  q ∈ P.invtRootSubmodule ↔ ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)
-- Mathlib.Topology.Category.TopCat.Basic
_private.Mathlib.Topology.Category.TopCat.Basic.0.TopCat.Hom.mk.injEq : ∀ {X Y : TopCat} (hom' hom'_1 : C(↑X, ↑Y)), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- Smooth is stable under base change.  -/
AlgebraicGeometry.smooth_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.Smooth
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
WittVector.mk_pow_fontaineTheta : ∀ {R : Type u} [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p]
  [inst_3 : IsAdicComplete (Ideal.span {↑p}) R] (n : ℕ) (x : WittVector p (PreTilt R p)),
  (Ideal.Quotient.mk (Ideal.span {↑p} ^ (n + 1))) ((WittVector.fontaineTheta R p) x) =
    (WittVector.fontaineThetaModPPow R p n) x
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.instSetLikeFinset : {ι : Type u_1} → SetLike (AbstractSimplicialComplex ι) (Finset ι)
-- Mathlib.CategoryTheory.Triangulated.Yoneda
/-- [Stacks Tag 0149](https://stacks.math.columbia.edu/tag/0149) -/
CategoryTheory.Pretriangulated.instIsHomologicalAddCommGrpCatObjOppositeFunctorPreadditiveCoyoneda : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (A : Cᵒᵖ), (CategoryTheory.preadditiveCoyoneda.obj A).IsHomological
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.toSubsemigroup_injective : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R], Function.Injective NonUnitalSubsemiring.toSubsemigroup
-- Mathlib.Order.Category.Frm
Frm.Hom.ext_iff : ∀ {X Y : Frm} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Lean.Meta.Tactic.Grind.Intro
Lean.Meta.Grind.Solvers.mkAction : IO Lean.Meta.Grind.Action
-- Mathlib.Combinatorics.Graph.Maps
Graph.IsLoopAt.map : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {v : α} {e : β} (f : α → α'),
  G.IsLoopAt e v → (Graph.map f G).IsLoopAt e (f v)
-- Lean.Meta.Tactic.Simp.Rewrite
_private.Lean.Meta.Tactic.Simp.Rewrite.0.Lean.Meta.Simp.synthesizeArgs.synthesizeInstance : Lean.Meta.Origin → Lean.Expr → Lean.Expr → Lean.Meta.SimpM Bool
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.toSubsemiring_mono : ∀ {R : Type u} [inst : NonAssocRing R], Monotone Subring.toSubsemiring
-- Mathlib.Topology.Compactness.Compact
/-- For every open cover of a compact set, there exists a finite subcover.  -/
IsCompact.elim_finite_subcover : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
  IsCompact s → ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.one_prod_one : ∀ {𝕜 : Type u_2} {α : Type u_5} {β : Type u_6} [inst : Ring 𝕜] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : DecidableEq α] [inst_4 : DecidableEq β], IncidenceAlgebra.prod 1 1 = 1
-- Mathlib.RingTheory.Derivation.DifferentialRing
/-- A delaborator for the x′ notation. This is required because it's not direct function application,
so the default delaborator doesn't work.
 -/
delabDeriv : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instCommGroupOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : CommGroup Mᵐᵒᵖ], DomMulAct.instCommGroupOfMulOpposite = inst
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.GoalState.enodeMap : Lean.Meta.Grind.GoalState → Lean.Meta.Grind.ENodeMap
-- Mathlib.Algebra.Ring.Subsemiring.Defs
SubsemiringClass.coe_subtype : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : SetLike S R] [hSR : SubsemiringClass S R] (s : S),
  ⇑(SubsemiringClass.subtype s) = Subtype.val
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.limit.toStructuredArrow_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] {X Y : J} (f : X ⟶ Y),
  (CategoryTheory.Limits.limit.toStructuredArrow F).map f = CategoryTheory.StructuredArrow.homMk f ⋯
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
algebraicIndependent_iUnion_of_directed : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {η : Type u_3}
  [Nonempty η] {s : η → Set A},
  Directed (fun x1 x2 => x1 ⊆ x2) s →
    (∀ (i : η), AlgebraicIndependent R Subtype.val) → AlgebraicIndependent R Subtype.val
-- Mathlib.NumberTheory.ModularForms.Basic
CuspFormClass.zero_at_infty : ∀ {k : ℤ} {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : FunLike F UpperHalfPlane ℂ] (f : F) [CuspFormClass F Γ k]
  [Fact (IsCusp OnePoint.infty Γ)], UpperHalfPlane.IsZeroAtImInfty ⇑f
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.baseChange_preΨ₄ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) [inst_2 : Algebra R S]
  {A : Type u} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : Type v}
  [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B),
  (W.baseChange B).preΨ₄ = Polynomial.map (↑f) (W.baseChange A).preΨ₄
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.canonicallyOrderedAdd : CanonicallyOrderedAdd Cardinal.{u}
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂).get k h_mem = m₁.get k ⋯
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_ric_eq_none : ∀ {n i : ℕ}, n < i → (*...=n).toList[i]? = none
-- Init.Data.Vector.Lemmas
Vector.reverse_inj : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n}, xs.reverse = ys.reverse ↔ xs = ys
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.update_zero_eq_erase : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) (n : ℕ), p.update n 0 = SkewPolynomial.erase n p
-- Mathlib.Order.Category.PartOrd
PartOrd.of.sizeOf_spec : ∀ (carrier : Type u_1) [str : PartialOrder carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.zipWithLeft'.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (a : α) (as : List α) (b : β) (bs : List β)
  (h_1 : (bs : List β) → motive [] bs) (h_2 : (a : α) → (as : List α) → motive (a :: as) [])
  (h_3 : (a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs)),
  (match a :: as, b :: bs with
    | [], bs => h_1 bs
    | a :: as, [] => h_2 a as
    | a :: as, b :: bs => h_3 a as b bs) =
    h_3 a as b bs
-- Mathlib.Data.Finset.Sort
Finset.sortedGT_sort : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α), (s.sort fun x1 x2 => x1 ≥ x2).SortedGT
-- Mathlib.Data.Num.Bitwise
SNum.zero.injEq : ∀ (a a_1 : Bool), (SNum.zero a = SNum.zero a_1) = (a = a_1)
-- Init.Data.Int.Linear
Int.Internal.Linear.instBEqPoly.beq.eq_def : ∀ (x x_1 : Int.Internal.Linear.Poly),
  Int.Internal.Linear.instBEqPoly.beq x x_1 =
    match x, x_1 with
    | Int.Internal.Linear.Poly.num a, Int.Internal.Linear.Poly.num b => a == b
    | Int.Internal.Linear.Poly.add a a_1 a_2, Int.Internal.Linear.Poly.add b b_1 b_2 =>
      a == b && (a_1 == b_1 && Int.Internal.Linear.instBEqPoly.beq a_2 b_2)
    | x, x_2 => false
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.pow : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M : Matrix m m R} {b : m → α} [inst : LinearOrder α]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : Semiring R],
  M.BlockTriangular b → ∀ (n : ℕ), (M ^ n).BlockTriangular b
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extendId.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cocone F),
  s.extendId =
    CategoryTheory.Limits.Cocone.extInv (CategoryTheory.Iso.refl (s.extend (CategoryTheory.CategoryStruct.id s.pt)).pt)
      ⋯
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instAddCommMonoid : {E : Type u_3} → [inst : Group E] → AddCommMonoid (GroupSeminorm E)
-- Mathlib.AlgebraicGeometry.ColimitsOver
CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback.congr_simp : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : P.IsStableUnderComposition] {X Y Z : T} (f : X ⟶ Y) (hPf : P f) (hQf : Q f)
  (g : Y ⟶ Z) [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : P.IsStableUnderBaseChangeAlong g]
  [inst_5 : Q.IsStableUnderBaseChange] [inst_6 : CategoryTheory.Limits.HasPullbacks T] (fg : X ⟶ Z)
  (hfg : CategoryTheory.CategoryStruct.comp f g = fg),
  CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback f hPf hQf g fg hfg =
    CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback f hPf hQf g fg hfg
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerRight_ε_η_assoc : ∀ {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 : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (T : D) {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) T ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.ε F) T)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.η F) T) h) =
    h
-- Aesop.RuleSet
/-- Forward rules. There's a special procedure for applying forward rules, so we
don't store them in the regular indices.
 -/
Aesop.BaseRuleSet.forwardRules : Aesop.BaseRuleSet → Aesop.ForwardIndex
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_pow : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : Filter α}
  {f : α → M}, Filter.Tendsto f l Filter.atTop → ∀ {n : ℕ}, 0 < n → Filter.Tendsto (fun x => f x ^ n) l Filter.atTop
-- Mathlib.Order.Heyting.Basic
sup_sdiff_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b ⊔ a = a
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_apply_real : ∀ {μ : MeasureTheory.Measure ℝ} (t : ℝ), MeasureTheory.charFun μ t = ∫ (x : ℝ), Complex.exp (↑t * ↑x * Complex.I) ∂μ
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_map_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → n γ} {g : γ → δ} {it : Std.IterM m β},
  (Std.IterM.map g (Std.IterM.mapM f it)).toList =
    (Std.IterM.mapM
        (fun b => do
          let __do_lift ← f b
          pure (g __do_lift))
        it).toList
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α}, a ∈ t → t.getKey? a = some (t.getKeyD a fallback)
-- Init.Data.List.Lemmas
List.insert_append : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List α} {a : α},
  List.insert a (l₁ ++ l₂) = if a ∈ l₂ then l₁ ++ l₂ else List.insert a l₁ ++ l₂
-- Mathlib.Analysis.RCLike.Basic
/-- There are several equivalent ways to say that a number `z` is in fact a real number.  -/
RCLike.is_real_TFAE : ∀ {K : Type u_1} [inst : RCLike K] (z : K),
  [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(RCLike.re z) = z, RCLike.im z = 0, IsSelfAdjoint z].TFAE
-- Mathlib.Algebra.Order.AddGroupWithTop
/-- A linearly ordered commutative monoid with an additively absorbing `⊤` element.
Instances should include number systems with an infinite element adjoined.  -/
LinearOrderedAddCommMonoidWithTop : Type u_3 → Type u_3
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_congr_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T T' : Set α → E →L[ℝ] F),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s) →
    ∀ (f : ↥(α →₁ₛ[μ] E)), MeasureTheory.L1.SimpleFunc.setToL1S T f = MeasureTheory.L1.SimpleFunc.setToL1S T' f
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.nonUnitalNormedCommRing : {I : Type u_5} →
  {B : I → Type u_7} → [inst : (i : I) → NonUnitalNormedCommRing (B i)] → NonUnitalNormedCommRing ↥(lp B ⊤)
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.limitConeIsLimit_lift : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type (max v u)))
  (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.Types.limitConeIsLimit F).lift s =
    TypeCat.ofHom fun v => ⟨fun j => (CategoryTheory.ConcreteCategory.hom (s.π.app j)) v, ⋯⟩