mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.WellFoundedSet
Set.wellFoundedOn_iff_no_descending_seq : ∀ {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α},
  s.WellFoundedOn r ↔ ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
-- Mathlib.Algebra.Group.AddChar
/-- The function maps `0` to `1`.

Do not use this directly. Instead use `AddChar.map_zero_eq_one`.  -/
AddChar.map_zero_eq_one' : ∀ {A : Type u_1} [inst : AddMonoid A] {M : Type u_2} [inst_1 : Monoid M] (self : AddChar A M), self.toFun 0 = 1
-- Std.Data.ByteSlice
instSliceableByteArrayNatByteSlice_2 : Std.Rci.Sliceable ByteArray ℕ ByteSlice
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_dvd : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} {a : α}, (∀ b ∈ s, f b ∣ a) → s.lcm f ∣ a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_keys : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.keys.isEmpty = m.isEmpty
-- Mathlib.Algebra.Group.Invertible.Basic
/-- `invertibleOfInvertibleMul` and `invertibleMul` as an equivalence.  -/
Invertible.mulLeft : {α : Type u} → [inst : Monoid α] → {a : α} → Invertible a → (b : α) → Invertible b ≃ Invertible (a * b)
-- Mathlib.Order.Basic
Decidable.eq_or_lt_of_le : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α} [DecidableLE α], a ≤ b → a = b ∨ a < b
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimitRecOn_pred : ∀ {α : Type u_1} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : PredOrder α]
  (pred : (a : α) → ¬IsMin a → motive (Order.pred a)) (isPredPrelimit : (a : α) → Order.IsPredPrelimit a → motive a)
  [inst_2 : NoMinOrder α] (b : α), Order.isPredPrelimitRecOn (Order.pred b) pred isPredPrelimit = pred b ⋯
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopicalAlgebra.fibrantObjects.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] (X : C),
  HomotopicalAlgebra.fibrantObjects C X = HomotopicalAlgebra.IsFibrant X
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.forM_eq_forM : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : (a : α) → β a → m' PUnit.{w + 1}},
  Std.DHashMap.forM f m = forM m fun a => f a.fst a.snd
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} [inst_1 : Inhabited (γ k)],
  (Std.DHashMap.map f m).get! k = (Option.map (f k) (m.get? k)).get!
-- Mathlib.Analysis.CStarAlgebra.Classes
instCStarAlgebraForall : {ι : Type u_1} → {A : ι → Type u_2} → [Fintype ι] → [(i : ι) → CStarAlgebra (A i)] → CStarAlgebra ((i : ι) → A i)
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.pairingIn_reflectionPerm_self_right : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [FaithfulSMul S R] [inst_8 : P.IsValuedIn S] (i j : ι),
  P.pairingIn S i ((P.reflectionPerm j) j) = -P.pairingIn S i j
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.and_const_right' : ∀ {w b c : ℕ} {a : BitVec w}, a &&& BitVec.ofNat w b &&& BitVec.ofNat w c = BitVec.ofNat w b &&& BitVec.ofNat w c &&& a
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.trim_congr : ∀ {α : Type u_1} [inst : MeasurableSpace α] {m₁ m₂ : MeasureTheory.OuterMeasure α},
  (∀ {s : Set α}, MeasurableSet s → m₁ s = m₂ s) → m₁.trim = m₂.trim
-- Batteries.Util.ProofWanted
/-- Reducible accessor so a binder of type `DefWanted.Val foo` reduces to `foo`'s
type. Used by the desugaring of `❰foo❱` when `foo` is a `def_wanted`.  -/
DefWanted.Val : {α : Sort u} → DefWanted α → Sort u
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
CategoryTheory.ShortComplex.ShortExact.comp_extClass : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact),
  (CategoryTheory.Abelian.Ext.mk₀ S.g).comp hS.extClass ⋯ = 0
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet.indep_generateFrom_of_disjoint : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set Ω},
  (∀ (n : ι), MeasurableSet (s n)) →
    ProbabilityTheory.iIndepSet s μ →
      ∀ (S T : Set ι),
        Disjoint S T →
          ProbabilityTheory.Indep (MeasurableSpace.generateFrom {t | ∃ n ∈ S, s n = t})
            (MeasurableSpace.generateFrom {t | ∃ k ∈ T, s k = t}) μ
-- Mathlib.FieldTheory.KummerExtension
autAdjoinRootXPowSubCEquiv_root : ∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K}
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) [inst_1 : NeZero n] (η : ↥(rootsOfUnity n K)),
  ((autAdjoinRootXPowSubCEquiv hζ H) η) (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)) =
    ↑↑η • AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_1 : ∀ {R : Type u} [inst : Semiring R], Polynomial.C 1 = 1
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.sum_add_tsum_nat_add' : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [T2Space M] [ContinuousAdd M] {f : ℕ → M}
  {k : ℕ}, (Summable fun n => f (n + k)) → ∑ i ∈ Finset.range k, f i + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.is_mul_left_invariant_innerContent : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : Group G]
  [inst_2 : SeparatelyContinuousMul G],
  (∀ (g : G) {K : TopologicalSpace.Compacts G}, μ (TopologicalSpace.Compacts.map (fun x => g * x) ⋯ K) = μ K) →
    ∀ (g : G) (U : TopologicalSpace.Opens G),
      μ.innerContent ((TopologicalSpace.Opens.comap ↑(Homeomorph.mulLeft g)) U) = μ.innerContent U
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counitInv_functor_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X : C) {Z : D} (h : e.functor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.obj X))
      (CategoryTheory.CategoryStruct.comp (e.functor.map (e.unitInv.app X)) h) =
    h
-- Mathlib.Algebra.Category.Grp.EpiMono
AddGrpCat.forget_grp_preserves_epi : (CategoryTheory.forget AddGrpCat).PreservesEpimorphisms
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Extract the forward direction of an additive equivalence
as an addition-preserving function.  -/
AddEquiv.toAddMonoidHom : {M : Type u_4} → {N : Type u_5} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M ≃+ N → M →+ N
-- Mathlib.Data.Multiset.UnionInter
Multiset.sub_add_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s - t + s ∩ t = s
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
/-- `dp R n m` is the equivalence class of `X (⟨n, m⟩)` in `DividedPowerAlgebra R M`.  -/
DividedPowerAlgebra.dp : (R : Type u_2) →
  {M : Type u_3} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → ℕ → M → DividedPowerAlgebra R M
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- See Note [custom simps projection]  -/
AffineEquiv.Simps.apply : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] → [inst_6 : AddTorsor V₂ P₂] → (P₁ ≃ᵃ[k] P₂) → P₁ → P₂
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.forIn_congr : ∀ {γ α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad n] [Monad m]
  [inst_2 : Std.Iterator α m β] [inst_3 : Std.IteratorLoop α m n] [inst_4 : MonadLiftT m n] {ita itb : Std.IterM m β},
  ita = itb →
    ∀ {b b' : γ},
      b = b' → ∀ {f g : β → γ → n (ForInStep γ)}, (∀ (a : β) (b : γ), f a b = g a b) → forIn ita b f = forIn itb b' g
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- A typeclass mixin saying that scalar multiplication and Lie bracket are left commutative.  -/
LieDerivation.SMulBracketCommClass : (S : Type u_4) →
  (L : Type u_5) →
    (α : Type u_6) → [SMul S α] → [inst : LieRing L] → [inst_1 : AddCommGroup α] → [LieRingModule L α] → Prop
-- Mathlib.NumberTheory.EulerProduct.Basic
EulerProduct.one_sub_inv_eq_geometric_of_summable_norm : ∀ {F : Type u_1} [inst : NormedField F] [CompleteSpace F] {f : ℕ →*₀ F} {p : ℕ},
  Nat.Prime p → (Summable fun x => ‖f x‖) → (1 - f p)⁻¹ = ∑' (e : ℕ), f (p ^ e)
-- Init.Data.Slice.List.Lemmas
List.size_mkSlice_roi : ∀ {α : Type u_1} {xs : List α} {lo : ℕ}, Std.Slice.size (Std.Roi.Sliceable.mkSlice xs lo<...*) = xs.length - (lo + 1)
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.sub : ∀ {α : Type u} {β : Type v} [inst : Sub β] {f f' g g' : α → β} {l : Filter α},
  f =ᶠ[l] g → f' =ᶠ[l] g' → f - f' =ᶠ[l] g - g'
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R], ↑1 = 1
-- Std.Sync.Channel
/-- Try to send a value to the channel. If this can be completed right away without blocking return
`true`; otherwise, don't send the value and return `false`.
 -/
Std.Channel.trySend : {α : Type} → Std.Channel α → α → BaseIO Bool
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- A linear map from a `Module` to an `InnerProductSpace` induces an `InnerProductSpace`
structure on the domain using the `SeminormedAddCommGroup.induced` norm.

See note [reducible non-instances].  -/
InnerProductSpace.induced : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      {G : Type u_4} →
        [inst_1 : SeminormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : AddCommGroup G] →
              [inst_4 : Module 𝕜 G] →
                {F : Type u_5} →
                  [inst_5 : FunLike F G E] → [inst_6 : LinearMapClass F 𝕜 G E] → (f : F) → InnerProductSpace 𝕜 G
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.preservesMonomorphisms_π₂ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C],
  CategoryTheory.ShortComplex.π₂.PreservesMonomorphisms
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
/-- The extension of `Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C`
on the idempotent completions. It shall be an equivalence of categories
for any additive category `C`.  -/
AlgebraicTopology.DoldKan.Γ₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteCoproducts C] →
        CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ))
          (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C))
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.toLinOrd : NonemptyFinLinOrd → LinOrd
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.instAddMonoidHomClass : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], AddMonoidHomClass (A →ₜ+ B) A B
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.Away.map_comp : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {B : Type u_4} {τ : Type u_5} [inst_6 : CommRing B] [inst_7 : SetLike τ B]
  [inst_8 : AddSubgroupClass τ B] {ℬ : ι → τ} [inst_9 : GradedRing ℬ] {C : Type u_6} {ψ : Type u_7}
  [inst_10 : CommRing C] [inst_11 : SetLike ψ C] [inst_12 : AddSubgroupClass ψ C] {𝒞 : ι → ψ} [inst_13 : GradedRing 𝒞]
  (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒞) (s : A),
  HomogeneousLocalization.Away.map (g.comp f) s =
    (HomogeneousLocalization.Away.map g (f s)).comp (HomogeneousLocalization.Away.map f s)
-- Mathlib.Order.RelClasses
isWellOrder_gt : ∀ {α : Type u} [inst : LinearOrder α] [WellFoundedGT α], IsWellOrder α fun x1 x2 => x2 < x1
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable, then
for any element `x` of `K` separable over `F`, it has the same minimal polynomials over `F` and
over `E`.  -/
minpoly.map_eq_of_isSeparable_of_isPurelyInseparable : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] (x : K),
  IsSeparable F x → ∀ [IsPurelyInseparable F E], Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.zero_comp : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : AddZeroClass P]
  (f : M →+ N), AddMonoidHom.comp 0 f = 0
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.isOpenMap_iff_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Type u_3}
  {U : ι → TopologicalSpace.Opens α},
  TopologicalSpace.IsOpenCover U → (IsOpenMap f ↔ ∀ (i : ι), IsOpenMap (f ∘ Subtype.val))
-- Lean.Parser.Term
/-- The *extended field notation* `e.f` is roughly short for `T.f e` where `T` is the type of `e`.
More precisely,
* if `e` is of a function type, `e.f` is translated to `Function.f (p := e)`
  where `p` is the first explicit parameter of function type
* if `e` is of a named type `T ...` and there is a declaration `T.f` (possibly from `export`),
  `e.f` is translated to `T.f (p := e)` where `p` is the first explicit parameter of type `T ...`
* otherwise, if `e` is of a structure type,
  the above is repeated for every base type of the structure.

The field index notation `e.i`, where `i` is a positive number,
is short for accessing the `i`-th field (1-indexed) of `e` if it is of a structure type.  -/
Lean.Parser.Term.proj : Lean.Parser.TrailingParser
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsWeakLimit t) {W : C} (h : W ⟶ X)
  (k : W ⟶ Y) (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift ht h k w) t.snd = k
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_toNat : ∀ (n : UInt64), UInt64.ofNatLT n.toNat ⋯ = n
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- The canonical continuous bilinear map `E → F → E ⊗ F`. This is the continuous version of
`mk`.  -/
TensorProduct.mkL : (𝕜 : Type u_1) →
  (E : Type u_2) →
    (F : Type u_3) →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : InnerProductSpace 𝕜 F] → E →L[𝕜] F →L[𝕜] TensorProduct 𝕜 E F
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.completedLFunction₀.congr_simp : ∀ {N : ℕ} [inst : NeZero N] (Φ Φ_1 : ZMod N → ℂ),
  Φ = Φ_1 → ∀ (s s_1 : ℂ), s = s_1 → ZMod.completedLFunction₀ Φ s = ZMod.completedLFunction₀ Φ_1 s_1
-- Mathlib.Algebra.GroupWithZero.Action.Defs
DistribMulAction.toAddMonoidEnd_apply : ∀ (M : Type u_1) (A : Type u_7) [inst : Monoid M] [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A] (x : M),
  (DistribMulAction.toAddMonoidEnd M A) x = DistribSMul.toAddMonoidHom A x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The homology map data associated to the identity morphism of a short complex.  -/
CategoryTheory.ShortComplex.HomologyMapData.id : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.HomologyData) → CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.CategoryStruct.id S) h h
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
associatesNonZeroDivisorsEquiv_symm_mk_mk : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] (a : M₀) (ha : a ∈ nonZeroDivisors M₀),
  associatesNonZeroDivisorsEquiv.symm ⟦⟨a, ha⟩⟧ = ⟨⟦a⟧, ⋯⟩
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getCast?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α),
  Std.DHashMap.Internal.AssocList.getCast? a Std.DHashMap.Internal.AssocList.nil = none
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.preserves_desc_mapCocone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesColimit F G]
  (c₁ c₂ : CategoryTheory.Limits.Cocone F) (t : CategoryTheory.Limits.IsColimit c₁),
  (CategoryTheory.Limits.isColimitOfPreserves G t).desc (G.mapCocone c₂) = G.map (t.desc c₂)
-- Mathlib.Analysis.Complex.Circle
Circle.exp_zsmul : ∀ (x : ℝ) (z : ℤ), Circle.exp (z • x) = Circle.exp x ^ z
-- Mathlib.RingTheory.PowerSeries.Inverse
/-- The ring isomorphism between the residue field of the ring of power series valued in a field `K`
and `K` itself.  -/
PowerSeries.residueFieldOfPowerSeries : {k : Type u_2} → [inst : Field k] → IsLocalRing.ResidueField (PowerSeries k) ≃+* k
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Triangulated.Localization.instPretriangulatedLocalization : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (W : CategoryTheory.MorphismProperty C) →
                [inst_6 : W.HasLeftCalculusOfFractions] →
                  [inst_7 : W.IsCompatibleWithTriangulation] → CategoryTheory.Pretriangulated W.Localization
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.preprocessPattern : Lean.Expr → optParam Bool true → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.MvPolynomial.Comap
MvPolynomial.comap_eq_id_of_eq_id : ∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R] (f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R),
  (∀ (φ : MvPolynomial σ R), f φ = φ) → ∀ (x : σ → R), MvPolynomial.comap f x = x
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.M.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat),
  AddMonCat.FilteredColimits.M F = (F.comp (CategoryTheory.forget AddMonCat)).ColimitType
-- Mathlib.Topology.Inseparable
Inseparable.symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable x y → Inseparable y x
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsIdempotentElem.ker_eq_range : ∀ {S : Type u_5} [inst : Semiring S] {E : Type u_7} [inst_1 : AddCommGroup E] [inst_2 : Module S E] {p : E →ₗ[S] E},
  IsIdempotentElem p → p.ker = (LinearMap.id - p).range
-- Mathlib.GroupTheory.OrderOfElement
sum_card_orderOf_eq_card_pow_eq_one : ∀ {G : Type u_1} [inst : Monoid G] {n : ℕ} [inst_1 : Fintype G] [inst_2 : DecidableEq G],
  n ≠ 0 → ∑ m ∈ n.divisors, {x | orderOf x = m}.card = {x | x ^ n = 1}.card
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- Let `x` be a nondegenerate `d`-simplex of `Δ[m + 1] ⊗ Δ[n]` which
does not belong to `Λ[m + 1, k.castSucc].unionProd ∂Δ[n]`. This is
the smallest `l : Fin (d + 1)` such that `x l` is of the form `(k.succ, _)`.  -/
SSet.prodStdSimplex.pairingCore.min : {m : ℕ} →
  {k : Fin (m + 1)} →
    {n : ℕ} → (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) → {d : ℕ} → x.dim = d → Fin (d + 1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ \ m₂).getKey? k = m₁.getKey? k
-- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
InformationTheory.integrable_llr_map : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {g : 𝓧 → 𝓨},
  μ.AbsolutelyContinuous ν →
    Measurable g →
      MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
        MeasureTheory.Integrable (MeasureTheory.llr (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν))
          (MeasureTheory.Measure.map g μ)
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- Common factors on the right can be turned into common factors on the left, a weak form of
cancellability.  -/
OreLocalization.ore_right_cancel : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r₁ r₂ : R) (s : ↥S),
  r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.toSubalgebra_inj : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {F E : IntermediateField K L}, F.toSubalgebra = E.toSubalgebra ↔ F = E
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_modify_eq_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β}, (t.modify k f).maxKey? = t.maxKey?
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- Every finite subset of a linearly independent set is linearly independent.  -/
linearIndependent_finset_map_embedding_subtype : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
  LinearIndependent R Subtype.val → ∀ (t : Finset ↑s), LinearIndependent R Subtype.val
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrp_obj_grp_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (A : CategoryTheory.Grp C),
  CategoryTheory.GrpObj.inv = F.map CategoryTheory.GrpObj.inv
-- Init.Data.UInt.Lemmas
instAssociativeUInt16HMul : Std.Associative fun x1 x2 => x1 * x2
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.instCompactSpace : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] [ProperSpace 𝕜] (a : A), CompactSpace ↑(spectrum 𝕜 a)
-- Mathlib.Topology.EMetricSpace.Paracompact
/-- A `PseudoEMetricSpace` is always a paracompact space.
Formalization is based on [MR0236876].  -/
Metric.instParacompactSpace : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α], ParacompactSpace α
-- Mathlib.RingTheory.Length
Module.length_eq_one : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSimpleModule R M],
  Module.length R M = 1
-- Lean.Data.JsonRpc
/-- Internal JSON-RPC error.  -/
Lean.JsonRpc.ErrorCode.internalError : Lean.JsonRpc.ErrorCode
-- Mathlib.Topology.Algebra.OpenSubgroup
AddSubgroup.isClosed_of_isOpen : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousAdd G] (U : AddSubgroup G),
  IsOpen ↑U → IsClosed ↑U