mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_g' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).g' = S.g
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The canonical ring homomorphism interpreting an element of `R` as an element of
the stalk of `structureSheaf R` at `x`.  -/
AlgebraicGeometry.StructureSheaf.toStalkₗ : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
          M →ₗ[R] ↑(TopCat.Presheaf.stalk (AlgebraicGeometry.moduleStructurePresheaf R M).presheaf x)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.G₂_off_diag_nonpos : ∀ (i j : Fin 2), i ≠ j → CartanMatrix.G₂ i j ≤ 0
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function has a power series `p` within a set of unique differentiability, inside a ball,
and is differentiable at a point, then the derivative series of `p` is summable at a point, with
sum the given differential. Note that this theorem does not require completeness of the space.  -/
HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E},
  HasFPowerSeriesWithinOnBall f p s x r →
    ∀ {f' : E →L[𝕜] F} {y : E},
      ↑‖y‖₊ < r →
        x + y ∈ insert x s →
          HasFDerivWithinAt f f' (insert x s) (x + y) →
            UniqueDiffOn 𝕜 (insert x s) → HasSum (fun n => (p.derivSeries n) fun x => y) f'
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Two equivalent partial equivs have the same source.  -/
PartialEquiv.EqOnSource.source_eq : ∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β}, e ≈ e' → e.source = e'.source
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.map_def : ∀ {ι : Type u_1} [inst : Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6}
  (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)]
  [inst_2 : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7}
  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)]
  [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] [inst_5 : IsDirectedOrder ι] (ih : (i : ι) → F₁ i → F₂ i)
  (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i), (f₂ i j h) (ih i x) = ih j ((f₁ i j h) x)) (x : (i : ι) × F₁ i),
  DirectLimit.map f₁ f₂ ih compat ⟦x⟧ = ⟦⟨x.fst, ih x.fst x.snd⟩⟧
-- Mathlib.GroupTheory.SpecificGroups.Alternating
Equiv.altCongrHom_apply_coe : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {β : Type u_2} [inst_2 : Fintype β]
  [inst_3 : DecidableEq β] (e : α ≃ β) (a : ↥(alternatingGroup α)), ↑(e.altCongrHom a) = e.permCongr ↑a
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
ContinuousMap.aeStronglyMeasurable_mkD_of_uncurry : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [CompactSpace Y] [inst_4 : TopologicalSpace X] [OpensMeasurableSpace X]
  [SecondCountableTopologyEither X C(Y, E)] (f : X → Y → E) (g : C(Y, E)),
  Continuous (Function.uncurry f) → MeasureTheory.AEStronglyMeasurable (fun x => ContinuousMap.mkD (f x) g) μ
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.pointwise_smul_le_pointwise_smul_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Group α] [inst_2 : MulDistribMulAction α G] {a : α}
  {S T : Subgroup G}, a • S ≤ a • T ↔ S ≤ T
-- Mathlib.Data.Set.Basic
SetCoe.ext : ∀ {α : Type u} {s : Set α} {a b : ↑s}, ↑a = ↑b → a = b
-- Mathlib.Algebra.Group.PNatPowAssoc
ppow_mul_comm : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Pow M ℕ+] [PNatPowAssoc M] (m n : ℕ+) (x : M), x ^ m * x ^ n = x ^ n * x ^ m
-- Init.Data.Queue
/-- `O(|vs|)`. Push a list of elements `vs` on the front of the queue.  -/
Std.Queue.enqueueAll : {α : Type u} → List α → Std.Queue α → Std.Queue α
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Filter.IsIncreasingApproximateUnit.eventually_norm : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {l : Filter A},
  l.IsIncreasingApproximateUnit → ∀ᶠ (x : A) in l, ‖x‖ ≤ 1
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_conj : ∀ (x : ℂ), ((starRingEnd ℂ) x).arg = if x.arg = Real.pi then Real.pi else -x.arg
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.counit_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (self : F.DescentDataAsCoalgebra f) (i : ι)
  {Z : ↑(F.obj { as := Opposite.op (X i) }).obj}
  (h : (CategoryTheory.CategoryStruct.id (F.obj { as := Opposite.op (X i) }).obj).toFunctor.obj (self.obj i) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.hom i i)
      (CategoryTheory.CategoryStruct.comp ((F.map (f i).op.toLoc).adj.counit.toNatTrans.app (self.obj i)) h) =
    h
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.forget_createsLimitsOfShape.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J],
  GrpCat.forget_createsLimitsOfShape = { CreatesLimit := fun {K} => inferInstance }
-- Std.Data.ByteSlice
/-- The stopping index is no later than the end of the byte array.

The ending index is exclusive. If it is equal to the size of the byte array, then the last byte of
the byte array is in the byte slice.
 -/
Std.Slice.Internal.ByteSliceData.stop_le_size_byteArray : ∀ (self : Std.Slice.Internal.ByteSliceData), self.stop ≤ self.byteArray.size
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₁.get k ⋯
-- Lean.Parser.Basic
Lean.Parser.checkTailNoWs : Lean.Syntax → Bool
-- Mathlib.Combinatorics.SimpleGraph.Partition
/-- Whether a partition `P` has at most `n` parts. A graph with a partition
satisfying this predicate called `n`-partite. (See `SimpleGraph.Partitionable`.)  -/
SimpleGraph.Partition.PartsCardLe : {V : Type u} → {G : SimpleGraph V} → G.Partition → ℕ → Prop
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.three_le_egirth : ∀ {α : Type u_1} {G : SimpleGraph α}, 3 ≤ G.egirth
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instMonoidalCategory : {k : Type u} →
  {G : Type v} → [inst : CommRing k] → [inst_1 : Monoid G] → CategoryTheory.MonoidalCategory (Rep.{u, u, v} k G)
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.EditableDocument.mk : Lean.Server.FileWorker.EditableDocumentCore → Lean.Server.ServerTask Unit → Lean.Server.FileWorker.EditableDocument
-- Init.Data.SInt.Basic
Int8.ofUInt8 : UInt8 → Int8
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.toLinearMap_comp : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : AddCommMonoid E₃]
  [inst_6 : PartialOrder E₃] [inst_7 : Module R E₁] [inst_8 : Module R E₂] [inst_9 : Module R E₃] (g : E₂ →ₚ[R] E₃)
  (f : E₁ →ₚ[R] E₂), (g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- A function `f` is **Lipschitz continuous** with constant `K ≥ 0` if for all `x, y`
we have `dist (f x) (f y) ≤ K * dist x y`.  -/
LipschitzWith : {α : Type u} → {β : Type v} → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → NNReal → (α → β) → Prop
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.FibrantObject.toHoCatLocalizerMorphism C).IsLocalizedEquivalence
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_hom : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] [inst_4 : CategoryTheory.Limits.HasColimit F]
  [inst_5 : CategoryTheory.Limits.HasColimit F'] (i : C),
  CategoryTheory.CategoryStruct.comp (α.app i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F' (L.obj i))
        (F'.colimitIsoOfIsLeftKanExtension α).hom) =
    CategoryTheory.Limits.colimit.ι F i
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_reindex : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (e₁ e₂ : n ≃ m) (A : Matrix n n α),
  ((Matrix.reindex e₁ e₂) A)⁻¹ = (Matrix.reindex e₂ e₁) A⁻¹
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.linearCombinationEquiv.congr_simp : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (hv : LinearIndependent R v), hv.linearCombinationEquiv = hv.linearCombinationEquiv
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.tuple.injEq : ∀ (args args_1 : List Lean.Parser.Tactic.MCasesPat),
  (Lean.Parser.Tactic.MCasesPat.tuple args = Lean.Parser.Tactic.MCasesPat.tuple args_1) = (args = args_1)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Composition of linear isometries.  -/
LinearIsometry.comp : {R : Type u_1} →
  {R₂ : Type u_2} →
    {R₃ : Type u_3} →
      {E : Type u_5} →
        {E₂ : Type u_6} →
          {E₃ : Type u_7} →
            [inst : Semiring R] →
              [inst_1 : Semiring R₂] →
                [inst_2 : Semiring R₃] →
                  {σ₁₂ : R →+* R₂} →
                    {σ₁₃ : R →+* R₃} →
                      {σ₂₃ : R₂ →+* R₃} →
                        [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                          [inst_4 : SeminormedAddCommGroup E] →
                            [inst_5 : SeminormedAddCommGroup E₂] →
                              [inst_6 : SeminormedAddCommGroup E₃] →
                                [inst_7 : Module R E] →
                                  [inst_8 : Module R₂ E₂] →
                                    [inst_9 : Module R₃ E₃] → (E₂ →ₛₗᵢ[σ₂₃] E₃) → (E →ₛₗᵢ[σ₁₂] E₂) → E →ₛₗᵢ[σ₁₃] E₃
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- **Alias** of `GradedAlgHom.coe_toAlgHom_injective`. -/
GradedAlgHom.coe_algHom_injective : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  Function.Injective GradedAlgHom.toAlgHom
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.add : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₁ =o[l] g → f₂ =o[l] g → (fun x => f₁ x + f₂ x) =o[l] g
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.RealizeConstResult.newConsts : Lean.Environment.RealizeConstResult✝ → Lean.VisibilityMap✝ (List Lean.AsyncConst✝)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.lift_adjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E)
  (S : Set ↥K), IntermediateField.lift (IntermediateField.adjoin F S) = IntermediateField.adjoin F (Subtype.val '' S)
-- Mathlib.NumberTheory.LucasLehmer
/-- **Lucas–Lehmer primality test**: sufficiency direction.  -/
lucas_lehmer_sufficiency : ∀ (p : ℕ), 1 < p → LucasLehmerTest p → Nat.Prime (mersenne p)
-- Lean.Data.Json.Basic
Lean.JsonNumber.instCoeNat : Coe ℕ Lean.JsonNumber
-- Init.Data.Ord.Basic
Ordering.isNe_eq_false : ∀ {o : Ordering}, o.isNe = false ↔ o = Ordering.eq
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_shiftConcat_eq_decide : ∀ {w : ℕ} (x : BitVec w) (b : Bool) (i : ℕ),
  (x.shiftConcat b).getLsbD i = (decide (i < w) && (decide (i = 0) && b || decide (0 < i) && x.getLsbD (i - 1)))
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassP_coe : ∀ (L : PeriodPair) (l : ↥L.lattice), L.derivWeierstrassP ↑l = 0
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Int.cast_det : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n ℤ),
  ↑M.det = (M.map fun x => ↑x).det
-- Aesop.Forward.Substitution
/-- Returns `true` if any expression in the codomain of `s` contains `hyp`.  -/
Aesop.Substitution.containsHyp : Lean.FVarId → Aesop.Substitution → Bool
-- Mathlib.Tactic.Ring.Common
/-- An atomic expression `e` with id `id`.

Atomic expressions are those which a `ring`-like tactic cannot parse any further.
For instance, `a + (a % b)` has `a` and `(a % b)` as atoms.
The `ring1` tactic does not normalize the subexpressions in atoms, but `ring_nf` does.

Atoms in fact represent equivalence classes of expressions, modulo definitional equality.
The field `index : ℕ` should be a unique number for each class,
while `e : Q($α)` contains a representative of this class.
 -/
Mathlib.Tactic.Ring.Common.ExBase.atom : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → ℕ → Mathlib.Tactic.Ring.Common.ExBase BaseType sα e
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.isGE_of_ge : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (p q : ℤ),
  autoParam (p ≤ q) CategoryTheory.Triangulated.TStructure.isGE_of_ge._auto_1 → ∀ [t.IsGE X q], t.IsGE X p
-- Mathlib.CategoryTheory.Sums.Products
/-- A consequence of `functorEquiv`: we can construct a natural isomorphism of functors
`A ⊕ A' ⥤ B` from the data of natural isomorphisms of their whiskering with `inl_` and `inr_`.  -/
CategoryTheory.Sum.natIsoOfWhiskerLeftInlInr : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {A' : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
        {B : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} B] →
            {F G : CategoryTheory.Functor (A ⊕ A') B} →
              ((CategoryTheory.Sum.inl_ A A').comp F ≅ (CategoryTheory.Sum.inl_ A A').comp G) →
                ((CategoryTheory.Sum.inr_ A A').comp F ≅ (CategoryTheory.Sum.inr_ A A').comp G) → (F ≅ G)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Set.OrdConnected.measurableSet : ∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α]
  [inst_2 : LinearOrder α] [OrderClosedTopology α], s.OrdConnected → MeasurableSet s
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- This function computes the integral of a function `f` against `partialTraj`,
and allows to view it as a function depending on all the variables.

This is inspired by `MeasureTheory.lmarginal`, to be able to write
`lmarginalPartialTraj κ b c (lmarginalPartialTraj κ a b f) = lmarginalPartialTraj κ a c`.  -/
ProbabilityTheory.Kernel.lmarginalPartialTraj : {X : ℕ → Type u_1} →
  {mX : (n : ℕ) → MeasurableSpace (X n)} →
    ((n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) →
      ℕ → ℕ → (((n : ℕ) → X n) → ENNReal) → ((n : ℕ) → X n) → ENNReal
-- Mathlib.Algebra.Ring.Semiconj
SemiconjBy.neg_left : ∀ {R : Type u} [inst : Mul R] [inst_1 : HasDistribNeg R] {a x y : R}, SemiconjBy a x y → SemiconjBy (-a) x y
-- Mathlib.GroupTheory.Congruence.Basic
Con.mulDistribMulAction : {α : Type u_4} →
  {M : Type u_5} →
    [inst : Monoid α] →
      [inst_1 : Monoid M] →
        [inst_2 : MulDistribMulAction α M] → [IsScalarTower α M M] → (c : Con M) → MulDistribMulAction α c.Quotient
-- Mathlib.NumberTheory.NumberField.CMField
/-- The complex conjugation of the CM-field `K`.
 -/
NumberField.IsCMField.complexConj : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : CharZero K] →
      [NumberField.IsCMField K] → [Algebra.IsIntegral ℚ K] → Gal(K/↥(NumberField.maximalRealSubfield K))
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SupSet α] [inst_1 : SupSet β] [inst_2 : SupSet γ]
  {g₁ g₂ : sSupHom β γ} {f : sSupHom α β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.MeasureTheory.Group.Measure
/-- Continuity of the measure of translates of a compact set:
Given a closed compact set `k` in an additive topological group,
the measure of `g +ᵥ k \ k` tends to zero as `g` tends to `0`.  -/
MeasureTheory.tendsto_measure_vadd_sdiff_isCompact_isClosed : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  [μ.InnerRegularCompactLTTop] {k : Set G},
  IsCompact k → IsClosed k → Filter.Tendsto (fun g => μ ((g +ᵥ k) \ k)) (nhds 0) (nhds 0)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_insert_le : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, (m.insert k).size ≤ m.size + 1
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [Std.LawfulEqCmp cmp] [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t.toList ↔ k ∈ t
-- Init.Data.String.Lemmas.IsEmpty
String.isEmpty_sliceTo : ∀ {s : String} {p : s.Pos}, (s.sliceTo p).isEmpty = true ↔ p = s.startPos
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.XIso.congr_simp : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c) {i : Option ι} {j : ι} (hj : i = some j),
  HomologicalComplex.extend.XIso K hj = HomologicalComplex.extend.XIso K hj
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.domDomCongr_apply : ∀ {R : Type u} {ι : Type v} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] [inst_5 : TopologicalSpace M₂]
  [inst_6 : TopologicalSpace M₃] {ι' : Type u_1} (e : ι ≃ ι') (f : ContinuousMultilinearMap R (fun x => M₂) M₃)
  (v : ι' → M₂), (ContinuousMultilinearMap.domDomCongr e f) v = f fun i => v (e i)
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- Right whiskering for morphisms  -/
CategoryTheory.Bicategory.«term_▷_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.le_generate : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X),
  R ≤ (CategoryTheory.Sieve.generate R).arrows
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- This function is the kernel given by the Ionescu-Tulcea theorem. It is shown below that it
is measurable and turned into a true kernel in `Kernel.traj`.  -/
ProbabilityTheory.Kernel.trajFun : {X : ℕ → Type u_1} →
  [inst : (n : ℕ) → MeasurableSpace (X n)] →
    (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) →
      [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] →
        (a : ℕ) → ((i : ↥(Finset.Iic a)) → X ↑i) → MeasureTheory.Measure ((n : ℕ) → X n)
-- Mathlib.Analysis.Real.Hyperreal
/-- Hyperreal numbers on the ultrafilter extending the cofinite filter.  -/
Hyperreal : Type
-- Mathlib.Order.Filter.Basic
Filter.generate_eq_biInf : ∀ {α : Type u} (S : Set (Set α)), Filter.generate S = ⨅ s ∈ S, Filter.principal s
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.ofNat : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] [NoZeroDivisors R] (d : ℕ) [inst_6 : d.AtLeastTwo], (OfNat.ofNat d).PosDef
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.instLinearOrder.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  ArchimedeanClass.instLinearOrder =
    { le := fun a a_1 => Quot.lift (fun a₁ => Quotient.lift ((fun x1 x2 => x1 ≤ x2) a₁) ⋯ a_1) ⋯ a,
      lt := fun a a_1 => Quot.lift (fun a₁ => Quotient.lift ((fun x1 x2 => x1 < x2) a₁) ⋯ a_1) ⋯ a, le_refl := ⋯,
      le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯, min := fun a a_1 => if a ≤ a_1 then a else a_1,
      max := fun a a_1 => if a ≤ a_1 then a_1 else a, compare := fun a a_1 => compareOfLessAndEq a a_1, le_total := ⋯,
      toDecidableLE := fun a b =>
        ⋯ ▸
          (Quot.lift
              (Quot.indep fun a =>
                (fun a => Quot.recOnSubsingleton b fun a_1 => (fun a b => Classical.propDecidable (a ≤ b)) a a_1) a)
              ⋯ a).snd,
      toDecidableEq := fun a b => decidableEqOfDecidableLE a b,
      toDecidableLT := fun a b =>
        ⋯ ▸
          (Quot.lift
              (Quot.indep fun a =>
                (fun a => Quot.recOnSubsingleton b fun a_1 => (fun a b => Classical.propDecidable (a < b)) a a_1) a)
              ⋯ a).snd,
      min_def := ⋯, max_def := ⋯, compare_eq_compareOfLessAndEq := ⋯ }
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smul_pow.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
  [inst_3 : MulActionWithZero R S] (x : S) (n : ℕ) (r : R), Polynomial.smul_pow x n r = r • x ^ n
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageRequestParams.mk.injEq : ∀ (type : Lean.Lsp.MessageType) (message : String) (actions? : Option (Array Lean.Lsp.MessageActionItem))
  (type_1 : Lean.Lsp.MessageType) (message_1 : String) (actions?_1 : Option (Array Lean.Lsp.MessageActionItem)),
  ({ type := type, message := message, actions? := actions? } =
      { type := type_1, message := message_1, actions? := actions?_1 }) =
    (type = type_1 ∧ message = message_1 ∧ actions? = actions?_1)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instReprDecl : {α : Type} → [Repr α] → Repr (Std.Sat.AIG.Decl α)
-- Mathlib.SetTheory.ZFC.Basic
/-- Turns a pre-set into a ZFC set.  -/
ZFSet.mk : PSet.{u_1} → ZFSet.{u_1}
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.nearestPt.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α] [inst_2 : OpensMeasurableSpace α]
  (e : ℕ → α) (N : ℕ),
  MeasureTheory.SimpleFunc.nearestPt e N = MeasureTheory.SimpleFunc.map e (MeasureTheory.SimpleFunc.nearestPtInd e N)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_le_primeCounting_mul_log : ∀ (n : ℕ), Chebyshev.psi ↑n ≤ ↑n.primeCounting * Real.log ↑n