mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid of a `CommMonoid` is a `CommMonoid`.  -/
Submonoid.toCommMonoid : {M : Type u_5} → [inst : CommMonoid M] → (S : Submonoid M) → CommMonoid ↥S
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- In the presence of the strict Segal condition, a path of length `n` can be
"composed" by taking the diagonal edge of the resulting `n`-simplex.  -/
SSet.StrictSegal.spineToDiagonal : {X : SSet} → X.StrictSegal → {n : ℕ} → X.Path n → X.obj (Opposite.op { len := 1 })
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.ιM_jointly_surjective₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {cR : CategoryTheory.Limits.Cocone R} {hcR : CategoryTheory.Limits.IsColimit cR} {M : PresheafOfModules R}
  {cM : CategoryTheory.Limits.Cocone M.presheaf} {hcM : CategoryTheory.Limits.IsColimit cM} {M' : PresheafOfModules R}
  {cM' : CategoryTheory.Limits.Cocone M'.presheaf} {hcM' : CategoryTheory.Limits.IsColimit cM'}
  (m : PresheafOfModules.ModuleColimit hcR hcM) (m' : PresheafOfModules.ModuleColimit hcR hcM'),
  ∃ U x x', PresheafOfModules.ModuleColimit.ιM x = m ∧ PresheafOfModules.ModuleColimit.ιM x' = m'
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
/-- The property of objects in `HomotopyCategory.Plus C` that is satisfied
by acyclic complexes.  -/
HomotopyCategory.Plus.subcategoryAcyclic : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.ObjectProperty (HomotopyCategory.Plus C)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α}, m.isEmpty = true → m.getKeyD a fallback = fallback
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.fg_closure_singleton : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (x : M),
  ((FirstOrder.Language.Substructure.closure L).toFun {x}).FG
-- Mathlib.Topology.Algebra.UniformRing
/-- Given a topological ring `α` equipped with a uniform structure that makes subtraction uniformly
continuous, get an equivalence between the separated quotient of `α` and the quotient ring
corresponding to the closure of zero.  -/
UniformSpace.sepQuotRingEquivRingQuot : (α : Type u_2) →
  [inst : CommRing α] →
    [inst_1 : TopologicalSpace α] → [inst_2 : IsTopologicalRing α] → SeparationQuotient α ≃+* α ⧸ ⊥.closure
-- Lean.Util.Trace
_private.Lean.Util.Trace.0.Lean.withStartStop : {α : Type} → {m : Type → Type} → [Monad m] → [MonadLiftT BaseIO m] → Lean.Options → m α → m (α × Float × Float)
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Action of `iterateFrobeniusAux` on the top field.  -/
_private.Mathlib.FieldTheory.PurelyInseparable.Exponent.0.IsPurelyInseparable.algebraMap_iterateFrobeniusAux : ∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable.HasExponent K L] (p : ℕ) [ExpChar K p] {n : ℕ},
  IsPurelyInseparable.exponent K L ≤ n →
    ∀ (a : L), (algebraMap K L) (IsPurelyInseparable.iterateFrobeniusAux✝ K L p n a) = a ^ p ^ n
-- Init.Data.List.Attach
List.length_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ a ∈ l, p a},
  (List.pmap f l H).length = l.length
-- Mathlib.SetTheory.Ordinal.Notation
ONote.scale.eq_def : ∀ (x x_1 : ONote),
  x.scale x_1 =
    match x_1 with
    | ONote.zero => 0
    | e.oadd n a => (x + e).oadd n (x.scale a)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.lift_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {V W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) {Z_1 : C} (h_1 : Y ⨯ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map h k) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp f h)
        (CategoryTheory.CategoryStruct.comp g k))
      h_1
-- Std.Sync.Broadcast
/-- A channel that can receive messages from `Bounded`.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver : Type → Type
-- Mathlib.Data.Finset.Card
Finset.card_eq_four : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α],
  s.card = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
-- Mathlib.LinearAlgebra.FreeModule.PID
Ideal.smithCoeffs.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  {S : Type u_4} [inst_3 : CommRing S] [inst_4 : IsDomain S] [inst_5 : Algebra R S] [inst_6 : Finite ι]
  (b b_1 : Module.Basis ι R S),
  b = b_1 →
    ∀ (I I_1 : Ideal S) (e_I : I = I_1) (hI : I ≠ ⊥) (a a_1 : ι),
      a = a_1 → Ideal.smithCoeffs b I hI a = Ideal.smithCoeffs b_1 I_1 ⋯ a_1
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- The evaluation of an element `f` of a reproducing kernel Hilbert space at a point `x` is
bounded by `‖f‖` times the square root of the kernel diagonal `‖kernel H x x‖` at `x`.  -/
RKHS.norm_apply_le : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (f : H) (x : X),
  ‖f x‖ ≤ ‖f‖ * √‖RKHS.kernel H x x‖
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.zipWithM.eq_1 : ∀ {α : Type u} {β : Type u_1} {γ : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → β → m γ) (as : Array α)
  (bs : Array β), Array.zipWithM f as bs = as.zipWithMAux bs f 0 #[]
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.monFunctorCategoryEquivalence_functor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D],
  (CategoryTheory.Monoidal.monFunctorCategoryEquivalence C D).functor =
    CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_smul : ∀ {R : Type u} {α : Type u_1} [inst : SMul α R] (x : R) (n : α), Tropical.trop (n • x) = Tropical.trop x ^ n
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.map_fst_darts_append : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), List.map (fun x => x.toProd.1) p.darts ++ [v] = p.support
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Mon.mul_denote.go : ∀ (ctx : Nat.Internal.Linear.Context) (fuel : ℕ) (m₁ m₂ : Nat.Internal.SOM.Mon),
  Nat.Internal.SOM.Mon.denote ctx (Nat.Internal.SOM.Mon.mul.go✝ fuel m₁ m₂) =
    Nat.Internal.SOM.Mon.denote ctx m₁ * Nat.Internal.SOM.Mon.denote ctx m₂
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
/-- The natural transformation `t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ⟶ t.eTruncLT.obj b`
for all `a` and `b` in `EInt`.  -/
CategoryTheory.Triangulated.TStructure.eTruncLTLTToLT : {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) →
                (a b : EInt) → (t.eTruncLT.obj a).comp (t.eTruncLT.obj b) ⟶ t.eTruncLT.obj b
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_cons : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (x : M) (f : Fin n → M), ∑ i, Fin.cons x f i = x + ∑ i, f i
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.piEquivFin.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (n : ℕ),
  AdicCompletion.piEquivFin I n = AdicCompletion.piEquivOfFintype I fun x => R
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getPatternVarsEx : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec : ∀ {R S : CommRingCat} [inst : IsLocalRing ↑S] (φ : R ⟶ S),
  CategoryTheory.CategoryStruct.comp
      ((AlgebraicGeometry.Spec R).presheaf.germ ⊤ ((AlgebraicGeometry.Spec.map φ) (IsLocalRing.closedPoint ↑S)) trivial)
      (AlgebraicGeometry.Scheme.stalkClosedPointTo (AlgebraicGeometry.Spec.map φ)) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).hom φ
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.and : Std.Tactic.BVDecide.Gate
-- Std.Data.DHashMap.IteratorLemmas
_private.Std.Data.DHashMap.IteratorLemmas.0.Std.DHashMap.valuesIter.eq_1 : ∀ {α β : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap α fun x => β),
  m.valuesIter = Std.Iter.map (fun e => e.snd) m.iter
-- Init.Grind.ToInt
Lean.Grind.IntInterval.nonEmpty.eq_3 : ∀ (hi : ℤ), (Lean.Grind.IntInterval.io hi).nonEmpty = true
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.sec.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [inst_3 : IsLocalization.Away x S] (s : S),
  IsLocalization.Away.sec x s = ((IsLocalization.sec (Submonoid.powers x) s).1, Exists.choose ⋯)
-- Lean.Hygiene
_private.Lean.Hygiene.0.Lean.mkInaccessibleUserName : Bool → Lean.Name → Lean.Name
-- Std.Time.Time.Unit.Basic
/-- Converts a `Millisecond.Offset` to an `Hour.Offset`.
 -/
Std.Time.Millisecond.Offset.toHours : Std.Time.Millisecond.Offset → Std.Time.Hour.Offset
-- Init.Prelude
Lean.Syntax.brecOn.eq : ∀ {motive_1 : Lean.Syntax → Sort u} {motive_2 : Array Lean.Syntax → Sort u} {motive_3 : List Lean.Syntax → Sort u}
  (t : Lean.Syntax) (F_1 : (t : Lean.Syntax) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.Syntax) → Lean.Syntax.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.Syntax) → Lean.Syntax.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (Lean.Syntax.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesOnBall.mk : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → (∀ (m : ℕ), n ≤ m → p m = 0) → HasFiniteFPowerSeriesOnBall f p x n r
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.max_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {h' : t₁.isEmpty = false}
  (h : t₁.Equiv t₂), t₁.max h' = t₂.max ⋯
-- Lean.Elab.InfoTree.Main
Lean.Elab.addCompletionInfo : {m : Type → Type} → [Monad m] → [Lean.Elab.MonadInfoTree m] → Lean.Elab.CompletionInfo → m Unit
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.inverse_compare : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α),
  pkg.compare pkg' ∘ pkg'.compare pkg = id
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- The inverse of `MulEquiv.withZero`.  -/
MulEquiv.unzero : {α : Type u_1} → {β : Type u_2} → [inst : Group α] → [inst_1 : Group β] → WithZero α ≃* WithZero β → α ≃* β
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symm_trans_self : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N), e.symm.trans e = MulEquiv.refl N
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.spine_map_subinterval : ∀ (X : SSet) (n j l : ℕ) (h : j + l ≤ n) (Δ : X.obj (Opposite.op { len := n })),
  X.spine l ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.subinterval j l h).op)) Δ) =
    (X.spine n Δ).interval j l h
-- Lean.Elab.Tactic.BuiltinTactic
/-- Evaluates a tactic script in form of a syntax node with alternating tactics and separators as
children.
  -/
Lean.Elab.Tactic.evalSepTactics : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Lie.Basic
/-- An equivalence of Lie algebra modules (denoted as `M ≃ₗ⁅R,L⁆ N`) is a linear equivalence
which is also a morphism of Lie algebra modules.  -/
«term_≃ₗ⁅_,_⁆_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.liftAlgHom_toRingHom : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_4} [inst_1 : CommRing A] {K : Type u_5} [inst_2 : Field K]
  {L : Type u_7} [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] [inst_6 : Algebra R A]
  [inst_7 : Algebra R K] [inst_8 : IsScalarTower R A K] [inst_9 : Algebra R L] {g : A →ₐ[R] L}
  (hg : Function.Injective ⇑g), (IsFractionRing.liftAlgHom hg).toRingHom = IsFractionRing.lift hg
-- Lean.Widget.InteractiveGoal
/-- Metavariable context that the goal is well-typed in.  -/
Lean.Widget.InteractiveGoalCore.ctx : Lean.Widget.InteractiveGoalCore → Lean.Server.WithRpcRef Lean.Elab.ContextInfo
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.map_obj_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y : T} [inst_2 : P.IsStableUnderComposition]
  {f : X ⟶ Y} (hPf : P f)
  (X_1 :
    CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.fromPUnit Y) (CategoryTheory.Functor.id T) P ⊤ Q),
  ((CategoryTheory.MorphismProperty.Under.map Q hPf).obj X_1).hom = CategoryTheory.CategoryStruct.comp f X_1.hom
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constToArray_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → Std.DTreeMap.Const.toArray t₁ = Std.DTreeMap.Const.toArray t₂
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.mk.inj : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {L : CategoryTheory.Functor C D}
  {W : CategoryTheory.MorphismProperty C} {E : Type u_3} {inst_2 : CategoryTheory.Category.{v_3, u_3} E}
  {inverts : W.IsInvertedBy L} {lift : (F : CategoryTheory.Functor C E) → W.IsInvertedBy F → CategoryTheory.Functor D E}
  {fac : ∀ (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F), L.comp (lift F hF) = F}
  {uniq : ∀ (F₁ F₂ : CategoryTheory.Functor D E), L.comp F₁ = L.comp F₂ → F₁ = F₂} {inverts_1 : W.IsInvertedBy L}
  {lift_1 : (F : CategoryTheory.Functor C E) → W.IsInvertedBy F → CategoryTheory.Functor D E}
  {fac_1 : ∀ (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F), L.comp (lift_1 F hF) = F}
  {uniq_1 : ∀ (F₁ F₂ : CategoryTheory.Functor D E), L.comp F₁ = L.comp F₂ → F₁ = F₂},
  { inverts := inverts, lift := lift, fac := fac, uniq := uniq } =
      { inverts := inverts_1, lift := lift_1, fac := fac_1, uniq := uniq_1 } →
    lift = lift_1
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
ContinuousLinearMap.integral_comp_L1_comm : ∀ {X : Type u_1} {E : Type u_3} {Fₗ : Type u_5} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6}
  [inst_1 : RCLike 𝕜] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup Fₗ]
  [inst_5 : NormedSpace 𝕜 Fₗ] [inst_6 : NormedSpace ℝ Fₗ] [CompleteSpace Fₗ] [inst_8 : NormedSpace ℝ E]
  [CompleteSpace E] (L : E →L[𝕜] Fₗ) (φ : ↥(MeasureTheory.Lp E 1 μ)), ∫ (x : X), L (↑↑φ x) ∂μ = L (∫ (x : X), ↑↑φ x ∂μ)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y}
  (hc : CategoryTheory.Limits.IsColimit c) {I : C} (hI : CategoryTheory.Limits.IsInitial I),
  CategoryTheory.IsPushout
    (hI.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
    (hI.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) c.inr c.inl
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Under.hasLimit_of_hasLimit_comp_forget : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {X : C} (F : CategoryTheory.Functor J (CategoryTheory.Under X))
  [i : CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Under.forget X))], CategoryTheory.Limits.HasLimit F
-- Init.Grind.Module.Basic
/-- A type with zero, addition, negation, and subtraction,
where addition is commutative and associative,
and negation is the left inverse of addition.  -/
Lean.Grind.AddCommGroup : Type u → Type u
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- If a continuous alternating map in finitely many variables on normed spaces
satisfies the inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖`
on a shell `ε / ‖c‖ < ‖m i‖ < ε` for some positive number `ε` and an elements `c : 𝕜`, `1 < ‖c‖`,
then it satisfies this inequality for all `m`.

If the domain is a Hausdorff space, then the continuity assumption is redundant,
see `bound_of_shell` below.  -/
AlternatingMap.bound_of_shell_of_continuous : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F),
  Continuous ⇑f →
    ∀ {ε C : ℝ},
      0 < ε →
        ∀ {c : 𝕜},
          1 < ‖c‖ →
            (∀ (m : ι → E), (∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε) → ‖f m‖ ≤ C * ∏ i, ‖m i‖) →
              ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- A topological space `X` is compactly generated if a set `s` is closed when `f ⁻¹' s` is
closed for every continuous map `f : K → X`, where `K` is compact Hausdorff.  -/
compactlyGeneratedSpace_of_isClosed : ∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ (s : Set X),
      (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
          Continuous f → IsClosed (f ⁻¹' s)) →
        IsClosed s) →
    CompactlyGeneratedSpace X
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjCyclesSelfIso_inv_iCycles : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).inv
      (((HomologicalComplex.single C c j).obj A).iCycles j) =
    (HomologicalComplex.singleObjXSelf c j A).inv
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.Commute.zpow_left : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A B : Matrix n' n' R}, Commute A B → ∀ (m : ℤ), Commute (A ^ m) B
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.addUnit_mem_leftNeg : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) (x : AddUnits M), ↑x ∈ S → ↑(-x) ∈ S.leftNeg
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α],
  Colex.instAddCommMonoid = { toAddMonoid := Colex.instAddMonoid, add_comm := ⋯ }
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.map_neg : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} (R' : Type u_11) [inst_2 : Ring R']
  [inst_3 : MulSemiringAction M R'] (S' : Type u_13) [inst_4 : Ring S'] [inst_5 : MulSemiringAction N S']
  (f : R' →ₑ+*[φ] S') (x : R'), f (-x) = -f x
-- Mathlib.Order.Disjoint
Codisjoint.symm : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] ⦃a b : α⦄, Codisjoint a b → Codisjoint b a
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorAlgebra.toDirectSum_tensorPower_tprod : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (x : Fin n → M),
  TensorAlgebra.toDirectSum ((TensorAlgebra.tprod R M n) x) =
    (DirectSum.of (fun i => TensorPower R i M) n) ((PiTensorProduct.tprod R) x)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G]
  [inst_5 : NormedAddCommGroup H] [inst_6 : InnerProductSpace 𝕜 H] (g : G →L[𝕜] H) (x : TensorProduct 𝕜 E G),
  (ContinuousLinearMap.lTensor E g) x = (LinearMap.lTensor E ↑g) x
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a finite additive Haar measure under a continuous surjective additive group
homomorphism is again an additive Haar measure. See also `isAddHaarMeasure_map`.  -/
MeasureTheory.Measure.isAddHaarMeasure_map_of_isFiniteMeasure : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [BorelSpace G] [ContinuousAdd G] {H : Type u_3}
  [inst_6 : AddGroup H] [inst_7 : TopologicalSpace H] [inst_8 : MeasurableSpace H] [BorelSpace H] [ContinuousAdd H]
  [MeasureTheory.IsFiniteMeasure μ] (f : G →+ H),
  Continuous ⇑f → Function.Surjective ⇑f → (MeasureTheory.Measure.map (⇑f) μ).IsAddHaarMeasure
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on a field `K`, the valuation
subring defined by `v` is closed in the valuative topology.  -/
Valuation.isClosed_valuationSubring : ∀ {Γ₀ : Type u_3} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_4} [inst_1 : Field K] [inst_2 : ValuativeRel K]
  [inst_3 : TopologicalSpace K] [IsValuativeTopology K] (v : Valuation K Γ₀) [v.Compatible],
  IsClosed ↑v.valuationSubring
-- ProofWidgets.Component.Basic
ProofWidgets.instRpcEncodableInteractiveExprProps : Lean.Server.RpcEncodable ProofWidgets.InteractiveExprProps
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.enat_to_nat_top_proc : Lean.ParserDescr
-- Mathlib.NumberTheory.PrimeCounting
/-- `primesLE n` is the set of primes less than or equal to `n` as a `Finset`.  -/
Nat.primesLE : ℕ → Finset ℕ
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContextEntry.param : Lean.IR.IRType → Lean.IR.LocalContextEntry
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.Hom.add_app : ∀ {X : AlgebraicGeometry.Scheme} {M N : X.Modules} {U : X.Opens} (φ ψ : M ⟶ N),
  AlgebraicGeometry.Scheme.Modules.Hom.app (φ + ψ) U =
    AlgebraicGeometry.Scheme.Modules.Hom.app φ U + AlgebraicGeometry.Scheme.Modules.Hom.app ψ U
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_eq_some_getD_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {a : α} {fallback : β a}, t.contains a = true → t.get? a = some (t.getD a fallback)
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Complex.kahler : ∀ (w z : ℂ), (Complex.orientation.kahler w) z = z * (starRingEnd ℂ) w
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeTR.go : {α : Type u_1} → (α → α → Bool) → List α → List α → List α → List α
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHom_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {f₁ f₂ : F ⟶ G},
  CochainComplex.HomComplex.Cochain.ofHom f₁ = CochainComplex.HomComplex.Cochain.ofHom f₂ → f₁ = f₂
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.invFun_eq_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), e.invFun = ↑e.symm