mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapAddEquiv_trans : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] [inst_3 : Mul M] (e₁ : R ≃+ S) (e₂ : S ≃+ T),
  MonoidAlgebra.mapAddEquiv M (e₁.trans e₂) = (MonoidAlgebra.mapAddEquiv M e₁).trans (MonoidAlgebra.mapAddEquiv M e₂)
-- Mathlib.Data.Fin.Tuple.Sort
Tuple.self_comp_sort : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] (f : Fin n → α),
  f ∘ ⇑(Tuple.sort f) = Tuple.graph.proj ∘ ⇑(Tuple.graphEquiv₂ f)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_sub_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a - x) ⁻¹' Set.uIcc b c = Set.uIcc (a - b) (a - c)
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.failure : {α : Type} → Lean.PrettyPrinter.Delaborator.DelabM α
-- Init.Data.Int.Cooper
Int.add_of_le.congr_simp : ∀ {a b : ℤ} (h : a ≤ b), Int.add_of_le h = Int.add_of_le h
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_one_eq_integral_norm : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  {f : α → E}, MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.lpNorm f 1 μ = ∫ (x : α), ‖f x‖ ∂μ
-- Mathlib.GroupTheory.GroupAction.SubMulAction
fixedPointsSubAddOfNormal.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {H : AddSubgroup G} [hH : H.Normal],
  fixedPointsSubAddOfNormal = { carrier := AddAction.fixedPoints (↥H) α, vadd_mem' := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsMultiplicativeTrWOfIsTriangulatedOfIsTriangulated : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] [P.IsTriangulated], P.trW.IsMultiplicative
-- Mathlib.Analysis.Normed.Lp.lpHolder
lp.norm_mapCLM_le : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : α → Type u_3} {F : α → Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : α) → NormedAddCommGroup (E i)] [inst_2 : (i : α) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : α) → NormedAddCommGroup (F i)] [inst_4 : (i : α) → NormedSpace 𝕜 (F i)] (p : ENNReal)
  [inst_5 : Fact (1 ≤ p)] (T : (i : α) → E i →L[𝕜] F i) {K : ℝ} (hK : 0 ≤ K) (hTK : ∀ (i : α), ‖T i‖ ≤ K),
  ‖lp.mapCLM p T hK hTK‖ ≤ K
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_zero_right : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x : F), inner 𝕜 x 0 = 0
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 0).unitIso.inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C 0).map ((CategoryTheory.shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop).op
      ((CategoryTheory.shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op
-- Mathlib.Order.WithBot
WithBot.decidableLT : {α : Type u_1} → [inst : LT α] → [DecidableLT α] → DecidableLT (WithBot α)
-- Mathlib.AlgebraicGeometry.Gluing
/-- The immersion from `D.U i` into the glued space.  -/
AlgebraicGeometry.Scheme.GlueData.ι : (D : AlgebraicGeometry.Scheme.GlueData) → (i : D.J) → D.U i ⟶ D.glued
-- Mathlib.Data.Finset.NoncommProd
/-- Product of a `s : Multiset α` with `[Monoid α]`, given a proof that `*` commutes
on all elements `x ∈ s`.  -/
Multiset.noncommProd : {α : Type u_3} → [inst : Monoid α] → (s : Multiset α) → {x | x ∈ s}.Pairwise Commute → α
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α], 1⁺ᵐ = 1
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {toGlueData : CategoryTheory.GlueData (AlgebraicGeometry.PresheafedSpace C)}
  {f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (toGlueData.f i j)}
  {toGlueData_1 : CategoryTheory.GlueData (AlgebraicGeometry.PresheafedSpace C)}
  {f_open_1 : ∀ (i j : toGlueData_1.J), AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (toGlueData_1.f i j)},
  { toGlueData := toGlueData, f_open := f_open } = { toGlueData := toGlueData_1, f_open := f_open_1 } →
    toGlueData = toGlueData_1
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.lTensor_comp_rTensor : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} {Q : Type u_7} [inst_8 : AddCommMonoid Q] [inst_9 : Module A Q] {υ : Representation A G Q}
  (f : ρ.IntertwiningMap τ) (g : σ.IntertwiningMap υ),
  (Representation.IntertwiningMap.lTensor τ g).comp (Representation.IntertwiningMap.rTensor σ f) = f.tensor g
-- Mathlib.NumberTheory.FermatPsp
Nat.decidableProbablePrime : (n b : ℕ) → Decidable (n.ProbablePrime b)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.map : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {β : Type u_10} [inst_2 : MeasurableSpace β]
  {φ : X → β} {f : β → E},
  MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map φ μ.variation) →
    μ.Integrable (f ∘ φ) → (μ.map φ).Integrable f
-- Mathlib.CategoryTheory.Action.Limits
/-- `Action.forget V G : Action V G ⥤ V` preserves the colimit of some `K : J ⥤ Action V G` if
`K ⋙ Action.forget V G` has a colimit.  -/
Action.instPreservesColimitForgetOfHasColimitComp : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} J] (K : CategoryTheory.Functor J (Action V G))
  [CategoryTheory.Limits.HasColimit (K.comp (Action.forget V G))],
  CategoryTheory.Limits.PreservesColimit K (Action.forget V G)
-- Init.Data.UInt.Lemmas
UInt64.toUSize_toUInt8 : ∀ (n : UInt64), n.toUInt8.toUSize = n.toUSize % 256
-- Mathlib.Order.Category.CompleteLat
/-- The equivalence between `CompleteLat` and itself induced by `OrderDual` both ways.  -/
CompleteLat.dualEquiv : CompleteLat ≌ CompleteLat
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.subst.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (x : α → L.Term β) (l : ℕ) (f : L.Functions l)
  (ts : Fin l → L.Term α), (FirstOrder.Language.func f ts).subst x = FirstOrder.Language.func f fun i => (ts i).subst x
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.dist_apply_le : ∀ {p : ENNReal} {ι : Type u_2} {β : ι → Type u_4} [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → PseudoMetricSpace (β i)] (x y : PiLp p β) (i : ι), dist (x.ofLp i) (y.ofLp i) ≤ dist x y
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.powers_of_orderTop_pos : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] {x : HahnSeries Γ R}, 0 < x.orderTop → ∀ (n : ℕ), (HahnSeries.SummableFamily.powers x) n = x ^ n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (k : α) (f : Option (β k) → Option (β k)), (t₁.alter k f).Equiv (t₂.alter k f)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.inr.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoid.Coprod.inr =
    { toFun := fun x => AddMonoid.Coprod.mk (FreeAddMonoid.of (Sum.inr x)), map_zero' := ⋯, map_add' := ⋯ }
-- Init.Data.BitVec.Basic
/-- Reverses the bits in a bitvector.  -/
BitVec.reverse : {w : ℕ} → BitVec w → BitVec w
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.Scheme.IsSeparated.isSeparated_terminal_from : ∀ {X : AlgebraicGeometry.Scheme} [self : X.IsSeparated],
  AlgebraicGeometry.IsSeparated (CategoryTheory.Limits.terminal.from X)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.counitForward_naturality₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G)
  (s : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ) (x : F.obj s),
  CategoryTheory.OverPresheafAux.counitForward G (Opposite.unop s) ((CategoryTheory.ConcreteCategory.hom (η.app s)) x) =
    (CategoryTheory.OverPresheafAux.counitForward F (Opposite.unop s) x).map₁
      (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ η) ⋯
-- Mathlib.Order.KrullDimension
Order.coheight_bot_eq_krullDim : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α], ↑(Order.coheight ⊥) = Order.krullDim α
-- Mathlib.Data.Multiset.Bind
Multiset.count_bind : ∀ {α : Type u_1} {β : Type v} [inst : DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α},
  Multiset.count a (m.bind f) = (Multiset.map (fun b => Multiset.count a (f b)) m).sum
-- Mathlib.Data.Nat.DvdSequence
Nat.IsStrongDvdSequence.eq_1 : ∀ (f : ℕ → ℕ), Nat.IsStrongDvdSequence f = ∀ (a b : ℕ), (f a).gcd (f b) = f (a.gcd b)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 1st group cohomology of `A`, defined as the 1st cohomology of the complex of inhomogeneous
cochains, is isomorphic to `cocycles₁ A ⧸ coboundaries₁ A`, which is a simpler type.  -/
groupCohomology.H1Iso : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → groupCohomology.H1 A ≅ (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.H
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter.congr_simp : ∀ (i i_1 : ℕ) (e_i : i = i_1) {n m : ℕ} (hi : n + i = m), SimplexCategory.δ₀Iter i hi = SimplexCategory.δ₀Iter i_1 ⋯
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.union_right : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t u : Set α},
  MeasureTheory.AEDisjoint μ s t → MeasureTheory.AEDisjoint μ s u → MeasureTheory.AEDisjoint μ s (t ∪ u)
-- Mathlib.LinearAlgebra.LinearPMap
/-- The graph of a `LinearPMap` viewed as a submodule on `E × F`.  -/
LinearPMap.graph : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_4} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] →
          {F : Type u_5} → [inst_3 : AddCommGroup F] → [inst_4 : Module R F] → (E →ₗ.[R] F) → Submodule R (E × F)
-- Lean.Parser.Basic
Lean.Parser.tokenAntiquotFn : Lean.Parser.ParserFn
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_Iio_lt : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (x : α),
  Ordinal.type LT.lt = (Ordinal.typein LT.lt).toRelEmbedding x
-- Mathlib.Logic.Equiv.Defs
Equiv.trans_cancel_left : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β ≃ γ) (g : α ≃ γ), e.trans f = g ↔ f = e.symm.trans g
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the second of three points is weakly between the other two, and not equal to the third,
the angle at the third point is zero.  -/
Wbtw.angle₂₃₁_eq_zero_of_ne : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, Wbtw ℝ p₁ p₂ p₃ → p₂ ≠ p₃ → EuclideanGeometry.angle p₂ p₃ p₁ = 0
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.shift_v' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a p q : ℤ) (hpq : p + n = q),
  (γ.shift a).v p q hpq = γ.v (p + a) (q + a) ⋯
-- Mathlib.Algebra.Group.Defs
DivInvOneMonoid.toInvOneClass : {G : Type u_2} → [self : DivInvOneMonoid G] → InvOneClass G
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.instRatCast : {K : Type u} →
  [inst : DivisionRing K] → {S : Type u_1} → [inst_1 : SetLike S K] → [h : SubfieldClass S K] → (s : S) → RatCast ↥s
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_eq_some_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.max? = some (t.maxD fallback)
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
/-- If `f (g x) = x` for `x` in some neighborhood of `a`, `g` is continuous at `a`,
and `f` has an invertible derivative `f'` at `g a`, then `g` has the derivative `f'⁻¹` at `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function.  -/
HasFDerivAt.of_local_left_inverse : ∀ {𝕜 : 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] {g : E → F} {f : F → E}
  {f' : F ≃L[𝕜] E} {a : E},
  ContinuousAt g a → HasFDerivAt f (↑f') (g a) → (∀ᶠ (y : E) in nhds a, f (g y) = y) → HasFDerivAt g (↑f'.symm) a
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by weight, strict inequality version:
if the total weight of a finite set of pigeons is less than `n • b`, and they are sorted into `n`
pigeonholes, then for some pigeonhole, the total weight of the pigeons in this pigeonhole is less
than `b`.  -/
Finset.exists_sum_fiber_lt_of_maps_to_of_sum_lt_nsmul : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M}
  {b : M} [inst_1 : AddCommMonoid M] [inst_2 : LinearOrder M] [IsOrderedCancelAddMonoid M],
  (∀ a ∈ s, f a ∈ t) → ∑ x ∈ s, w x < t.card • b → ∃ y ∈ t, ∑ x ∈ s with f x = y, w x < b
-- Mathlib.RingTheory.Valuation.FiniteField
/-- **Alias** of `FiniteField.valuation_algebraMap_eq_one`. -/
Valuation.FiniteField.algebraMap_eq_one : ∀ {Fq : Type u_1} {A : Type u_2} {Γ : Type u_3} [inst : Field Fq] [Finite Fq] [inst_2 : Ring A] [inst_3 : Algebra Fq A]
  [inst_4 : LinearOrderedCommMonoidWithZero Γ] (v : Valuation A Γ) (a : Fq), a ≠ 0 → v ((algebraMap Fq A) a) = 1
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.tendsto_nhds_iff : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {α : Type u_5} {l : Filter α} {f : α → Z} {z : Z},
  z ∈ e.source →
    (Filter.Tendsto f l (nhds z) ↔
      Filter.Tendsto (proj ∘ f) l (nhds (proj z)) ∧ Filter.Tendsto (fun x => (↑e (f x)).2) l (nhds (↑e z).2))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tan_periodic : Function.Periodic Complex.tan ↑Real.pi
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerLeft_whiskerRight_assoc : ∀ (A : Type u_1) {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] {F G : CategoryTheory.Functor B C} (η : F ⟶ G)
  (H : CategoryTheory.Functor C D) {Z : CategoryTheory.Functor (CategoryTheory.Join A B) (CategoryTheory.Join A D)}
  (h : CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) (G.comp H) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Join.mapWhiskerLeft (CategoryTheory.Functor.id A) (CategoryTheory.Functor.whiskerRight η H)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompRight A F H).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.mapWhiskerLeft (CategoryTheory.Functor.id A) η)
          (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) H))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompRight A G H).inv h))
-- Init.System.IOError
/-- Constructs an `IO.Error` from a string.

`IO.Error` is the type of exceptions thrown by the `IO` monad.
 -/
IO.userError : String → IO.Error
-- Mathlib.Order.Heyting.Basic
HeytingAlgebra.toOrderBot : {α : Type u_4} → [self : HeytingAlgebra α] → OrderBot α
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.map.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f f_1 : X ⟶ Y) (e_f : f = f_1)
  [inst_1 : CategoryTheory.Mono f], CategoryTheory.MonoOver.map f = CategoryTheory.MonoOver.map f_1
-- Mathlib.NumberTheory.Pell
/-- A positive solution is a generator (up to sign) of the group of all solutions to the
Pell equation `x^2 - d*y^2 = 1` if and only if it is a fundamental solution.  -/
Pell.pos_generator_iff_fundamental : ∀ {d : ℤ} (a : Pell.Solution₁ d),
  (1 < a.x ∧ 0 < a.y ∧ ∀ (b : Pell.Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n) ↔ Pell.IsFundamental a
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CochainComplex.Plus.localizerMorphism_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (CochainComplex.Plus.localizerMorphism C).functor = (CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k a : α} {v : β k},
  (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ k ∉ m then k else m.getKey! a
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.uliftFunctor_map : ∀ {x x_1 : AddGrpCat} (f : x ⟶ x_1),
  AddGrpCat.uliftFunctor.map f =
    AddGrpCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp ((AddGrpCat.Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom))
-- Mathlib.Algebra.Group.Nat.Hom
powersHom_apply : ∀ {M : Type u_1} [inst : Monoid M] (x : M) (n : Multiplicative ℕ), ((powersHom M) x) n = x ^ Multiplicative.toAdd n
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.instSubsingletonLocallyConstantElemForallBoolEmptyCollectionSetInt : ∀ {I : Type u}, Subsingleton (LocallyConstant ↑∅ ℤ)
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.Lean.Parser.ParserContext.mk.injEq : ∀ (toParserContextCore toParserContextCore_1 : Lean.Parser.ParserContextCore),
  ({ toParserContextCore := toParserContextCore } = { toParserContextCore := toParserContextCore_1 }) =
    (toParserContextCore = toParserContextCore_1)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
MulEquiv.symm_toContinuousMulEquiv : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Mul G] [inst_3 : Mul H]
  {e : G ≃* H} (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s),
  (e.toContinuousMulEquiv he).symm = e.symm.toContinuousMulEquiv ⋯
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
/-- `IsClosedUnderFiniteProducts` may be checked at any universe.  -/
CategoryTheory.ObjectProperty.IsClosedUnderFiniteCoproducts.of_isClosedUnderColimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C},
  (∀ (J : Type w) [Finite J], P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete J)) →
    P.IsClosedUnderFiniteCoproducts
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- For `s` to be a fundamental domain, it's enough to check
`MeasureTheory.AEDisjoint (g • s) s` for `g ≠ 1`.  -/
MeasureTheory.IsFundamentalDomain.mk'' : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α},
  MeasureTheory.NullMeasurableSet s μ →
    (∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s) →
      (∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s) →
        (∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g • x) μ μ) →
          MeasureTheory.IsFundamentalDomain G s μ
-- Mathlib.RingTheory.AdicCompletion.Basic
IsPrecomplete.prec : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsPrecomplete I M →
    ∀ {f : ℕ → M}, (∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]) → ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.prod_eq_two_power : ∀ {ι : Type u} [Infinite ι] {c : ι → Cardinal.{v}},
  (∀ (i : ι), 2 ≤ c i) →
    (∀ (i : ι), Cardinal.lift.{u, v} (c i) ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)) →
      Cardinal.prod c = 2 ^ Cardinal.lift.{v, u} (Cardinal.mk ι)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.depthLt.sizeOf_spec : ∀ (lhs n : ℕ), sizeOf (Lean.Meta.Grind.EMatchTheoremConstraint.depthLt lhs n) = 1 + sizeOf lhs + sizeOf n
-- Mathlib.Algebra.Ring.Subring.IntPolynomial
/-- Given a polynomial in `K[X]` such that all coefficients belong to the subring `R`,
`Polynomial.int` is the corresponding polynomial in `R[X]`.  -/
Polynomial.int : {K : Type u_1} → [inst : Field K] → (R : Subring K) → (P : Polynomial K) → (∀ (n : ℕ), P.coeff n ∈ R) → Polynomial ↥R
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.isArtinianObject_iff_antitone_chain_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.IsArtinianObject X ↔ ∀ (f : ℕ →o (CategoryTheory.Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- The (Loewner) partial order on continuous linear maps on a Hilbert space determined by
`f ≤ g` if and only if `g - f` is a positive linear map (in the sense of
`ContinuousLinearMap.IsPositive`). With this partial order, the continuous linear maps form a
`StarOrderedRing`.  -/
ContinuousLinearMap.instLoewnerPartialOrder : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → PartialOrder (E →L[𝕜] E)
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
/-- The canonical isomorphism of triangles
`(triangleOfDegreewiseSplit S σ).rotate.rotate ≅ mappingCone.triangle (homOfDegreewiseSplit S σ)`
when `S` is a degreewise split short exact sequence of cochain complexes.  -/
CochainComplex.triangleOfDegreewiseSplitRotateRotateIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) →
        (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) →
          [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
            (CochainComplex.triangleOfDegreewiseSplit S σ).rotate.rotate ≅
              CochainComplex.mappingCone.triangle (CochainComplex.homOfDegreewiseSplit S σ)
-- Init.Data.Int.DivMod.Basic
Int.negSucc_emod_ofNat : ∀ {a b : ℕ}, Int.negSucc a % ↑b = Int.subNatNat b (a % b).succ
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformRight.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (e : α) (x : Finset α × Finset α),
  Finset.mulETransformRight e x = (x.1 ∪ MulOpposite.op e • x.1, x.2 ∩ e⁻¹ • x.2)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.coe_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ), ↑(e.trans e') = ↑e' ∘ ↑e