mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A seminormed commutative ring is a commutative ring endowed with a seminorm which satisfies
the inequality `‖x y‖ ≤ ‖x‖ ‖y‖`.  -/
SeminormedCommRing : Type u_5 → Type u_5
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_pi : Complex.cos ↑Real.pi = -1
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.instMonoidalMopFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → (CategoryTheory.mopFunctor C).Monoidal
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α} {k k' fallback : α},
  (k == k') = true →
    k ∉ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertMany l).getD k' fallback = k
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.sum_cycleType_le : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (σ : Equiv.Perm α), σ.cycleType.sum ≤ Fintype.card α
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.monoCLM_apply : ∀ (𝕜 : 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] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n₁ n₂ : ℕ∞} {K₁ K₂ : TopologicalSpace.Compacts E}
  (f : ContDiffMapSupportedIn E F n₁ K₁),
  ⇑((ContDiffMapSupportedIn.monoCLM 𝕜) f) = ⇑(if n₂ ≤ n₁ ∧ K₁ ≤ K₂ then f else 0)
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.instAddCommGroupOfTwoCocycle : {R : Type u_1} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    (c : ↥(LieModule.Cohomology.twoCocycle R L M)) → AddCommGroup (LieAlgebra.ofTwoCocycle c)
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
AlgebraicTopology.DoldKan.σ_comp_PInfty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) {n : ℕ} (i : Fin (n + 1)),
  CategoryTheory.CategoryStruct.comp (X.σ i) (AlgebraicTopology.DoldKan.PInfty.f (n + 1)) = 0
-- Lean.Elab.Term.TermElabM
/-- Standard tactic metavariable, arising from `by ...` syntax.  -/
Lean.Elab.Term.TacticMVarKind.term : Lean.Elab.Term.TacticMVarKind
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Cofix.dest.eq_1 : ∀ {F : Type u → Type u} [q : QPF F], QPF.Cofix.dest = Quot.lift (fun x => Quot.mk QPF.Mcongr <$> QPF.abs x.dest) ⋯
-- Init.Data.String.FindPos
/-- Iterates `p.prev` `n` times.

If this would move `p` past the start of `s`, the result is `s.startPos`.
 -/
String.Pos.prevn : {s : String} → s.Pos → ℕ → s.Pos
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.singleton_mem : ∀ {A : Type u_1} (T : ↥(Descriptive.tree A)) {a : A} {x : List A}, a :: x ∈ T → [a] ∈ T
-- Mathlib.Order.Lattice
sup_sup_distrib_left : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)
-- Mathlib.Topology.Inseparable
SeparationQuotient.instInhabited : {X : Type u_1} → [inst : TopologicalSpace X] → [Inhabited X] → Inhabited (SeparationQuotient X)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
TotalComplexShape.rel₁ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  {c₁₂ : ComplexShape I₁₂} [self : TotalComplexShape c₁ c₂ c₁₂] {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' →
    ∀ (i₂ : I₂), c₁₂.Rel (TotalComplexShape.π c₁ c₂ c₁₂ (i₁, i₂)) (TotalComplexShape.π c₁ c₂ c₁₂ (i₁', i₂))
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.BinaryInput.lhs_cast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α} (input : aig1.BinaryInput)
  (h : aig1.decls.size ≤ aig2.decls.size), (input.cast h).lhs = input.lhs.cast h
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.comap_normalClosure_image_ge : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (s : Set G) (f : G →+ N),
  AddSubgroup.normalClosure s ≤ AddSubgroup.comap f (AddSubgroup.normalClosure (⇑f '' s))
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Iso.boxProdSumDistrib_apply : ∀ {V : Type u_4} {W₁ : Type u_8} {W₂ : Type u_9} (G : SimpleGraph V) (H₁ : SimpleGraph W₁) (H₂ : SimpleGraph W₂)
  (a : V × (W₁ ⊕ W₂)),
  (SimpleGraph.Iso.boxProdSumDistrib G H₁ H₂) a = Sum.map Prod.swap Prod.swap ((Equiv.sumProdDistrib W₁ W₂ V) a.swap)
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- The ring of integers adjoined with a square root of `d`.
These have the form `a + b √d` where `a b : ℤ`. The components
are called `re` and `im` by analogy to the negative `d` case.  -/
«termℤ√_» : Lean.ParserDescr
-- Mathlib.Order.SuccPred.Basic
instSuccOrderOrderDualOfPredOrder.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α],
  instSuccOrderOrderDualOfPredOrder =
    { succ := ⇑OrderDual.toDual ∘ PredOrder.pred ∘ ⇑OrderDual.ofDual, le_succ := ⋯, max_of_succ_le := ⋯,
      succ_le_of_lt := ⋯ }
-- Mathlib.Data.Set.Restrict
Set.domRestrict_apply : ∀ {α : Type u_1} {π : α → Type u_6} (f : (a : α) → π a) (s : Set α) (x : ↑s), s.domRestrict f x = f ↑x
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.CWComplex.Subcomplex.map_def : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : T2Space X] [inst_1 : Topology.CWComplex C]
  (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ) (i : ↑(E.I n)),
  Topology.RelCWComplex.map n i = Topology.RelCWComplex.map n ↑i
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_get?_eq_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α}, (t.get? a).isSome = t.contains a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α}, a ∈ (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl ↔ compare k a ≠ Ordering.eq ∧ a ∈ t
-- Init.Data.Format.Basic
/-- Concatenation of two `Format`s.  -/
Std.Format.append : Std.Format → Std.Format → Std.Format
-- Mathlib.Data.TypeVec
TypeVec.prod.diag.eq_def : ∀ (x : ℕ) (x_1 : TypeVec.{u} x) (x_2 : Fin2 x) (x_3 : x_1 x_2),
  TypeVec.prod.diag x_2 x_3 =
    match x, x_1, x_2, x_3 with
    | n.succ, α, a.fs, x => TypeVec.prod.diag a x
    | n.succ, x, Fin2.fz, x_4 => (x_4, x_4)
-- Init.Prelude
/-- `True` is true, and `True.intro` (or more commonly, `trivial`)
is the proof.  -/
True.intro : True
-- Mathlib.Algebra.Star.LinearMap
Module.End.spectrum_intrinsicStar : ∀ {R : Type u_4} {V : Type u_5} [inst : CommRing R] [inst_1 : InvolutiveStar R] [inst_2 : AddCommGroup V]
  [inst_3 : StarAddMonoid V] [inst_4 : Module R V] [inst_5 : StarModule R V] (f : WithConv (Module.End R V)),
  spectrum R (star f).ofConv = star (spectrum R f.ofConv)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarKind.coe.sizeOf_spec : ∀ (header? : Option String) (expectedType e : Lean.Expr) (f? : Option Lean.Expr)
  (mkErrorMsg? : Option (Lean.MVarId → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData)),
  sizeOf (Lean.Elab.Term.SyntheticMVarKind.coe header? expectedType e f? mkErrorMsg?) =
    1 + sizeOf header? + sizeOf expectedType + sizeOf e + sizeOf f? + sizeOf mkErrorMsg?
-- Mathlib.Algebra.Order.SuccPred
monotone_of_le_add_one : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : One α]
  [inst_4 : SuccAddOrder α] [IsSuccArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMax a → f a ≤ f (a + 1)) → Monotone f
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.IsReduced.of_reduce_eq : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α], FreeGroup.reduce L = L → FreeGroup.IsReduced L
-- Std.Data.Iterators.Lemmas.Producers.Repeat
Std.Iter.atIdxSlow?_succ_repeat_eq_map : ∀ {α : Type w} {f : α → α} {init : α} {k : ℕ},
  Std.Iter.atIdxSlow? (k + 1) (Std.Iter.repeat f init) = f <$> Std.Iter.atIdxSlow? k (Std.Iter.repeat f init)
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.decorateErrorMessageWithLambdaImplicitVars : Lean.Exception → Array Lean.Expr → Lean.Elab.TermElabM Lean.Exception
-- Mathlib.Algebra.Divisibility.Units
isRelPrime_comm : ∀ {α : Type u_1} [inst : CommMonoid α] {x y : α}, IsRelPrime x y ↔ IsRelPrime y x
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.bounded' : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] (f : CauSeq β abv) (x : α), ∃ r > x, ∀ (i : ℕ), abv (↑f i) < r
-- Mathlib.CategoryTheory.Action
CategoryTheory.ActionCategory.stabilizerIsoEnd_apply : ∀ (M : Type u_1) [inst : Monoid M] {X : Type u} [inst_1 : MulAction M X] (x : X)
  (f : ↥(MulAction.stabilizerSubmonoid M x)), (CategoryTheory.ActionCategory.stabilizerIsoEnd M x) f = f
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.AddMonCat.Hom.mk.inj : ∀ {A B : AddMonCat} {hom' hom'_1 : ↑A →+ ↑B}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_list_prod_noncomm : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S) (ps : List (Polynomial R)),
  (∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x) →
    Polynomial.eval₂ f x ps.prod = (List.map (Polynomial.eval₂ f x) ps).prod
-- Std.Time.Date.Unit.Day
/-- Convert `Day.Offset` into `Hour.Offset`.
 -/
Std.Time.Day.Offset.toHours : Std.Time.Day.Offset → Std.Time.Hour.Offset
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.objEquiv_yonedaEquiv_id : ∀ (n : ℕ),
  SSet.stdSimplex.objEquiv (SSet.yonedaEquiv (CategoryTheory.CategoryStruct.id (SSet.stdSimplex.obj { len := n }))) =
    CategoryTheory.CategoryStruct.id { len := n }
-- Mathlib.RingTheory.LaurentSeries
/-- Having established that the `K⸨X⸩` is complete and contains `K⟮X⟯` as a dense
subspace, it gives rise to an abstract completion of `K⟮X⟯`.  -/
LaurentSeries.LaurentSeriesPkg : (K : Type u_2) → [inst : Field K] → AbstractCompletion.{u_2, u_2} (WithVal (RatFunc.polynomialValuationX K))
-- Lean.Elab.ConfigEval.Types
Lean.Elab.ConfigEval.unsupportedExprExceptionId : Lean.InternalExceptionId
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.locallyLinear_bot : ∀ {α : Type u_1}, ⊥.LocallyLinear
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k fallback : α},
  k ∉ t → l.contains k = false → (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).getKeyD k fallback = fallback
-- Mathlib.Computability.RegularExpressions
RegularExpression.matchEpsilon.eq_def : ∀ {α : Type u_1} (x : RegularExpression α),
  x.matchEpsilon =
    match x with
    | RegularExpression.zero => false
    | RegularExpression.epsilon => true
    | RegularExpression.char a => false
    | P.plus Q => P.matchEpsilon || Q.matchEpsilon
    | P.comp Q => P.matchEpsilon && Q.matchEpsilon
    | _P.star => true
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.toSuccArrow_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (X : C),
  (Φ.toSuccArrow X).hom = Φ.toSucc X
-- Mathlib.Topology.Constructions
isOpen_pi_iff : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {s : Set ((a : ι) → A a)},
  IsOpen s ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- Constructor for simplices of the standard simplex which takes a `OrderHom` as an input.  -/
SSet.stdSimplex.objMk : {n : SimplexCategory} →
  {m : SimplexCategoryᵒᵖ} → (Fin ((Opposite.unop m).len + 1) →o Fin (n.len + 1)) → (SSet.stdSimplex.obj n).obj m
-- Mathlib.Algebra.Lie.Basis.Basic
/-- The basis for the Cartan subalgebra.  -/
LieAlgebra.Basis.h : {ι : Type u_1} →
  {R : Type u_2} →
    {L : Type u_3} →
      [inst : Finite ι] →
        [inst_1 : CommRing R] →
          [inst_2 : LieRing L] → [inst_3 : LieAlgebra R L] → {H : LieSubalgebra R L} → LieAlgebra.Basis ι H → ι → L
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.IsConj.symm : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)},
  NumberField.ComplexEmbedding.IsConj φ σ → NumberField.ComplexEmbedding.IsConj φ σ.symm
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instNormedSpace : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : SeminormedAddCommGroup β] →
        {𝕜 : Type u_2} → [inst_2 : NormedField 𝕜] → [NormedSpace 𝕜 β] → NormedSpace 𝕜 (ZeroAtInftyContinuousMap α β)
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.length.eq_1 : ∀ {V : Type u} [inst : Quiver V] {a : V}, Quiver.Path.nil.length = 0
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchAux : Option Bool →
  Array Lean.Syntax → Array Lean.Elab.Term.TermMatchAltView → Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Lean.Meta.HaveTelescope
/-- The set of `have`s that the type of the body depends on, as indices into `haveInfo`.
This is the set of fixed `have`s.  -/
Lean.Meta.HaveTelescopeInfo.bodyTypeDeps : Lean.Meta.HaveTelescopeInfo → Std.HashSet ℕ
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM : Type → Type
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.nhds_basis_closedBall_inv_nat_succ : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α},
  (nhds x).HasBasis (fun x => True) fun n => Metric.closedBall x (1 / (↑n + 1))
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.ext : ∀ {R : Type u_1} {x y : PrimeSpectrum.BasicConstructibleSetData R}, x.f = y.f → x.n = y.n → x.g ≍ y.g → x = y
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLTD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β) (fallback : α),
  Std.DTreeMap.Internal.Impl.getKeyLTD k t fallback = (Std.DTreeMap.Internal.Impl.getKeyLT? k t).getD fallback
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} {fallback : β}, t.contains a = false → t.getD a fallback = fallback
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.prod_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) {ι : Type w} {t : Finset ι} {f : ι → A}, (∀ x ∈ t, f x ∈ S) → ∏ x ∈ t, f x ∈ S
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.mk.sizeOf_spec : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [inst_1 : SizeOf R]
  {point : WeierstrassCurve.Jacobian.PointClass R} (nonsingular : W'.NonsingularLift point),
  sizeOf { point := point, nonsingular := nonsingular } = 1 + sizeOf point + sizeOf nonsingular
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiffWithinAt_finsetSum'`. -/
contMDiffWithinAt_finset_sum' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι}
  {f : ι → M → G}, (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) → ContMDiffWithinAt I' I n (∑ i ∈ t, f i) s x
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.compMono_e : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.MonoFactorisation f) {Y' : C} (g : Y ⟶ Y') [inst_1 : CategoryTheory.Mono g],
  (F.compMono g).e = F.e
-- Lean.Server.CodeActions.Attr
/-- The state of the command code actions extension.  -/
Lean.CodeAction.CommandCodeActions : Type
-- Mathlib.NumberTheory.Divisors
Nat.sum_properDivisors_eq_one_iff_prime : ∀ {n : ℕ}, ∑ x ∈ n.properDivisors, x = 1 ↔ Nat.Prime n
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.mul_pair : ∀ {α : Type u_2} [inst : Mul α] (s : Set α) (a b : α), s * {a, b} = MulOpposite.op a • s ∪ MulOpposite.op b • s
-- Mathlib.Algebra.Order.Invertible
invOf_lt_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} [inst_3 : Invertible a],
  1 < a → ⅟a < 1
-- Mathlib.Analysis.Complex.AbsMax
/-- **Maximum modulus principle**: if `f : E → F` is complex differentiable on a bounded set `U` and
`‖f z‖ ≤ C` for any `z ∈ frontier U`, then the same is true for any `z ∈ closure U`.  -/
Complex.norm_le_of_forall_mem_frontier_norm_le : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [Nontrivial E] {f : E → F} {U : Set E},
  Bornology.IsBounded U →
    DiffContOnCl ℂ f U → ∀ {C : ℝ}, (∀ z ∈ frontier U, ‖f z‖ ≤ C) → ∀ {z : E}, z ∈ closure U → ‖f z‖ ≤ C
-- Mathlib.CategoryTheory.Abelian.Opposite
/-- The kernel of `f.op` is the opposite of `cokernel f`.  -/
CategoryTheory.kernelOpOp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.kernel f.op ≅ Opposite.op (CategoryTheory.Limits.cokernel f)
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.sum : ∀ {α : Type u_4} {β : Type u_5} {M : Type u_6} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M]
  (f : α ⊕ β → M), Summable (f ∘ Sum.inl) → Summable (f ∘ Sum.inr) → Summable f
-- Batteries.Lean.LawfulMonadLift
EIO.adapt_bind : ∀ {ε₁ ε₂ α β : Type} (f : ε₁ → ε₂) (ma : EIO ε₁ α) (g : α → EIO ε₁ β),
  EIO.adapt f (ma >>= g) = do
    let a ← EIO.adapt f ma
    EIO.adapt f (g a)
-- Mathlib.Logic.Equiv.Functor
Functor.mapEquiv_symm_apply : ∀ {α β : Type u} (f : Type u → Type v) [inst : Functor f] [inst_1 : LawfulFunctor f] (h : α ≃ β) (y : f β),
  (Functor.mapEquiv f h).symm y = ⇑h.symm <$> y
-- Mathlib.Algebra.GroupWithZero.Units.Fintype
Fintype.card_units_int : Fintype.card ℤˣ = 2
-- Lean.Language.Basic
_private.Lean.Language.Basic.0.Lean.Language.Snapshot.Diagnostics.mk.inj : ∀ {msgLog : Lean.MessageLog} {interactiveDiagsRef? : Option (IO.Ref (Option Dynamic))} {msgLog_1 : Lean.MessageLog}
  {interactiveDiagsRef?_1 : Option (IO.Ref (Option Dynamic))},
  { msgLog := msgLog, interactiveDiagsRef? := interactiveDiagsRef? } =
      { msgLog := msgLog_1, interactiveDiagsRef? := interactiveDiagsRef?_1 } →
    msgLog = msgLog_1 ∧ interactiveDiagsRef? = interactiveDiagsRef?_1
-- Lean.Parser.Syntax
Lean.Parser.Command.infix.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Submodule.IsPrincipal.contentIdeal_generator_dvd_coeff : ∀ {R : Type u_3} [inst : CommSemiring R] {p : Polynomial R} (h_prin : Submodule.IsPrincipal p.contentIdeal) (n : ℕ),
  Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- The ball of radius one consists of just the center.  -/
SimpleGraph.ball_one : ∀ {V : Type u_1} {G : SimpleGraph V} {c : V}, G.ball c 1 = {c}
-- Mathlib.CategoryTheory.Limits.Types.PreservesLimit
CategoryTheory.Presheaf.preservesLimit_eq_isLocal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] (F : CategoryTheory.Functor J Cᵒᵖ) [inst_3 : Small.{w, u'} J],
  CategoryTheory.ObjectProperty.preservesLimit F =
    (CategoryTheory.MorphismProperty.ofHoms (CategoryTheory.Presheaf.preservesLimitHomFamily F)).isLocal
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableAux.mk : {Γ₀ Γ₁ : Type} → (tm : Turing.FinTM2) → tm.Γ tm.k₀ ≃ Γ₀ → tm.Γ tm.k₁ ≃ Γ₁ → Turing.TM2ComputableAux Γ₀ Γ₁
-- Mathlib.Logic.Small.Defs
/-- If a type is `Small.{w}`, then there exists an equivalence with some `S : Type w`  -/
Small.equiv_small : ∀ {α : Type v} [self : Small.{w, v} α], ∃ S, Nonempty (α ≃ S)
-- Mathlib.Computability.Encoding
Computability.Γ'.blank : Computability.Γ'
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.single_eq_C_mul_T : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (n : ℤ),
  AddMonoidAlgebra.single n r = LaurentPolynomial.C r * LaurentPolynomial.T n
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomial_mul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {s s' : σ →₀ ℕ} {a b : R},
  (MvPolynomial.monomial s) a * (MvPolynomial.monomial s') b = (MvPolynomial.monomial (s + s')) (a * b)
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.liftExpand.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_3}
  [inst_2 : MulAction R X] {C : Sort u_2} (P : X → ↥S → C)
  (hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩),
  OreLocalization.liftExpand P hP = Quotient.lift (fun p => P p.1 p.2) ⋯
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumElim_comp_inl : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L'),
  (ϕ.sumElim ψ).comp FirstOrder.Language.LHom.sumInl = ϕ
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.nilRank_le_natTrailingDegree_charpoly : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup L] [inst_2 : Module R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M) [inst_5 : Module.Free R M]
  [inst_6 : Module.Finite R M] [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] [Nontrivial R] (x : L),
  φ.nilRank ≤ (LinearMap.charpoly (φ x)).natTrailingDegree
-- Aesop.Tree.Data
Aesop.GoalState.noConfusionType : Sort v✝ → Aesop.GoalState → Aesop.GoalState → Sort v✝
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.integrable_compProd_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  ⦃f : β × γ → E⦄,
  MeasureTheory.AEStronglyMeasurable f ((κ.compProd η) a) →
    (MeasureTheory.Integrable f ((κ.compProd η) a) ↔
      (∀ᵐ (x : β) ∂κ a, MeasureTheory.Integrable (fun y => f (x, y)) (η (a, x))) ∧
        MeasureTheory.Integrable (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a))
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.lift_apply_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P) (x : N), (Monoid.Coprod.lift f g) (Monoid.Coprod.inr x) = g x
-- Mathlib.FieldTheory.Finite.GaloisField
instFiniteDimensionalZModGaloisField : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (n : ℕ), FiniteDimensional (ZMod p) (GaloisField p n)