mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.Restriction
/-- Given `K : HomologicalComplex C c'` and `e : c.Embedding c'` (satisfying `[e.IsRelIff]`),
this is the homological complex in `HomologicalComplex C c` obtained by restriction.  -/
HomologicalComplex.restriction : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              HomologicalComplex C c' → (e : c.Embedding c') → [e.IsRelIff] → HomologicalComplex C c
-- Mathlib.Analysis.Seminorm
/-- If there is a scalar `c` with `‖c‖>1`, then any element can be moved by scalar multiplication to
any shell of width `‖c‖`. Also recap information on the norm of the rescaling element that shows
up in applications.  -/
rescale_to_shell : ∀ {𝕜 : Type u_3} {F : Type u_10} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F]
  {c : 𝕜},
  1 < ‖c‖ → ∀ {ε : ℝ}, 0 < ε → ∀ {x : F}, x ≠ 0 → ∃ d, d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖
-- Mathlib.MeasureTheory.PiSystem
piiUnionInter_singleton : ∀ {α : Type u_3} {ι : Type u_4} (π : ι → Set (Set α)) (i : ι), piiUnionInter π {i} = π i ∪ {Set.univ}
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_eq_union : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackId_hom_counit_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id X)]
  {Z : CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over X)}
  (h : CategoryTheory.Functor.id (CategoryTheory.Over X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.ChosenPullbacksAlong.pullbackId X).hom
        (CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id X)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X)).counit h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X)).counit h
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_of_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (f : β → α) {b : β},
  b ∈ s → ∃ a, s.inf (WithTop.some ∘ f) = ↑a
-- Mathlib.Data.Sym.Basic
Sym.instUnique : {α : Type u_1} → (n : ℕ) → [Unique α] → Unique (Sym α n)
-- Mathlib.Geometry.Manifold.BumpFunction
/-- The function defined by `f : SmoothBumpFunction c`. Use automatic coercion to function
instead.  -/
SmoothBumpFunction.toFun : {E : Type uE} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type uH} →
        [inst_2 : TopologicalSpace H] →
          {I : ModelWithCorners ℝ E H} →
            {M : Type uM} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] → [FiniteDimensional ℝ E] → {c : M} → SmoothBumpFunction I c → M → ℝ
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- A set `A` is the compact coherentification is closed iff for all compact sets `K`,
the intersection `K ∩ A` is closed in `K`.  -/
CompactCoherentification.isClosed_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {A : Set (CompactCoherentification X)},
  IsClosed A ↔ ∀ (K : Set X), IsCompact K → IsClosed (Subtype.val ⁻¹' ⇑(CompactCoherentification.mk X) ⁻¹' A)
-- Init.Data.BitVec.Bitblast
/-- The remainder is morally a `Bitvec wr`, and so has value less than `2^wr`.  -/
BitVec.DivModState.Lawful.hrWidth : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w},
  BitVec.DivModState.Lawful args qr → qr.r.toNat < 2 ^ qr.wr
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.supSpanSingleton_apply_mk_of_mem : ∀ {E : Type u_4} [inst : AddCommGroup E] {F : Type u_5} [inst_1 : AddCommGroup F] {K : Type u_7} {L : Type u_8}
  [inst_2 : DivisionRing K] [inst_3 : DivisionRing L] {σ : K →+* L} [inst_4 : Module K E] [inst_5 : Module L F]
  (f : E →ₛₗ.[σ] F) {x : E} (y : F) (hx : x ∉ f.domain) {x' : E} (hx' : x' ∈ f.domain),
  ↑(f.supSpanSingleton x y hx) ⟨x', ⋯⟩ = ↑f ⟨x', hx'⟩
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.ofGroup_head : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G),
  (HNNExtension.NormalWord.ofGroup g).head = g
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.ιCompMap_hom_app_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat}
  (α : F ⟶ F') (c : C) (X : ↑(F.obj c)),
  ((CategoryTheory.Grothendieck.ιCompMap α c).hom.app X).base = CategoryTheory.CategoryStruct.id c
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.comap_comap : ∀ {R : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsOrderedRing R] [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E]
  [inst_6 : AddCommMonoid F] [inst_7 : TopologicalSpace F] [inst_8 : Module R F] [inst_9 : AddCommMonoid G]
  [inst_10 : TopologicalSpace G] [inst_11 : Module R G] (g : F →L[R] G) (f : E →L[R] F) (C : ProperCone R G),
  ProperCone.comap f (ProperCone.comap g C) = ProperCone.comap (g ∘SL f) C
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.one_div_add_one_div : ∀ {p q r : ℝ}, p.HolderTriple q r → 1 / p + 1 / q = 1 / r
-- Mathlib.Algebra.Opposites
AddOpposite.op_zero : ∀ {α : Type u_1} [inst : Zero α], AddOpposite.op 0 = 0
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.op_map_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D) {X Y : Dᵒᵖ} (g : X ⟶ Y) (X_1 : Cᵒᵖᵒᵖ),
  (P.op.map g).app X_1 = (P.obj (Opposite.unop (Opposite.unop X_1))).map g
-- Batteries.Data.List.Lemmas
List.getElem_getElem_findIdxs_sub : ∀ {i : ℕ} {α : Type u_1} {xs : List α} {p : α → Bool} (s : ℕ) (h : i < (List.findIdxs p xs s).length),
  p xs[(List.findIdxs p xs s)[i] - s] = true
-- Init.Notation
/-- Normalize casts in an expression using the same method as the `norm_cast` tactic.  -/
Lean.modCast : Lean.ParserDescr
-- Mathlib.NumberTheory.SiegelsLemma
/-- The sup norm of a non-zero integer matrix is at least one  -/
Int.Matrix.one_le_norm_A_of_ne_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] (A : Matrix α β ℤ), A ≠ 0 → 1 ≤ ‖A‖
-- Mathlib.Computability.TuringMachine.Config
/-- This is a temporary definition, because we will prove in `code_is_ok` that it always holds.
It asserts that `c` is semantically correct; that is, for any `k` and `v`,
`eval (stepNormal c k v) = eval (Cfg.ret k (Code.eval c v))`, as an equality of partial values
(so one diverges iff the other does).

In particular, we can let `k = Cont.halt`, and then this asserts that `stepNormal c Cont.halt v`
evaluates to `Cfg.halt (Code.eval c v)`.  -/
Turing.ToPartrec.Code.Ok : Turing.ToPartrec.Code → Prop
-- Mathlib.Analysis.Normed.Order.UpperLower
IsUpperSet.mem_interior_of_forall_lt : ∀ {ι : Type u_2} [Finite ι] {s : Set (ι → ℝ)} {x y : ι → ℝ},
  IsUpperSet s → x ∈ closure s → (∀ (i : ι), x i < y i) → y ∈ interior s
-- Init.Data.Order.LemmasExtra
/-- This lemma derives a `LawfulOrderBEq α` instance from a property involving an `Ord α` instance.
 -/
Std.LawfulOrderBEq.of_ord : ∀ (α : Type u) [inst : Ord α] [inst_1 : BEq α] [inst_2 : LE α] [Std.LawfulOrderOrd α],
  (∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq) → Std.LawfulOrderBEq α
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.findSomeM?_eq_match_step.match_1.eq_1 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (h_1 : Unit → motive none) (h_2 : (fx : γ) → motive (some fx)),
  (match none with
    | none => h_1 ()
    | some fx => h_2 fx) =
    h_1 ()
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivativeFinsupp_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.derivativeFinsupp 1 = fun₀ | 0 => 1
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- `f.app (Y.basicOpen r)` is isomorphic to map induced on localizations
`Γ(Y, Y.basicOpen r) ⟶ Γ(X, X.basicOpen (f.app U r))`  -/
AlgebraicGeometry.IsAffineOpen.appBasicOpenIsoAwayMap : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    {U : Y.Opens} →
      (hU : AlgebraicGeometry.IsAffineOpen U) →
        (h : AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)) →
          (r : ↑(Y.presheaf.obj (Opposite.op U))) →
            CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.app f (Y.basicOpen r)) ≅
              CategoryTheory.Arrow.mk
                (CommRingCat.ofHom
                  (IsLocalization.Away.map (↑(Y.presheaf.obj (Opposite.op (Y.basicOpen r))))
                    (↑(X.presheaf.obj
                        (Opposite.op
                          (X.basicOpen
                            ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) r)))))
                    (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)) r))
-- Mathlib.Data.Nat.Squarefree
Nat.primeFactors_div_gcd : ∀ {m n : ℕ}, Squarefree m → n ≠ 0 → (m / m.gcd n).primeFactors = m.primeFactors \ n.primeFactors
-- Mathlib.LinearAlgebra.Basis.Fin
Module.Basis.coe_mkFinSnocOfLE : ∀ {R : Type u_3} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  {N O : Submodule R M} (b : Module.Basis (Fin n) R ↥N) (hNO : N ≤ O) (y : M) (yO : y ∈ O)
  (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z ∈ O, ∃ c, z + c • y ∈ N),
  ⇑(b.mkFinSnocOfLE hNO y yO hli hsp) = Fin.snoc (⇑(Submodule.inclusion hNO) ∘ ⇑b) ⟨y, yO⟩
-- Mathlib.Order.Concept
Concept.mem_intent_of_intent_rel : ∀ {α : Type u_2} {r' : α → α → Prop} {c' : Concept α α r'} [IsTrans α r'] {x y : α},
  r' x y → x ∈ c'.intent → y ∈ c'.intent
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_add_sub : ∀ (R : Type u_1) {V : Type u_2} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  (x y : V), midpoint R (x + y) (x - y) = x
-- Aesop.Search.SearchM
Aesop.enqueueGoals : {Q : Type} → [inst : Aesop.Queue Q] → Array Aesop.GoalRef → Aesop.SearchM Q Unit
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.prod_eq_bot_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {s : Submonoid M} {t : Submonoid N},
  s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- If a subgroup of an additive topological group has `0` in its interior, then it is
open.  -/
AddSubgroup.isOpen_of_zero_mem_interior : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousAdd G] (H : AddSubgroup G),
  0 ∈ interior ↑H → IsOpen ↑H
-- Batteries.Lean.Except
Except.pmap_error : ∀ {ε : Type u} {α β : Type v} (e : ε) (f : (a : α) → Except.error e = Except.ok a → β),
  (Except.error e).pmap f = Except.error e
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- **Alias** of `MonoidHom.domRestrict_range`. -/
MonoidHom.restrict_range : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (K : Subgroup G) (f : G →* N),
  (f.domRestrict K).range = Subgroup.map f K
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
OrderDual.instIsCountablyGeneratedAtBot : ∀ {α : Type u_1} [inst : Preorder α] [Filter.atTop.IsCountablyGenerated], Filter.atBot.IsCountablyGenerated
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.toGHSpace_continuous : ∀ {X : Type u} [inst : MetricSpace X], Continuous TopologicalSpace.NonemptyCompacts.toGHSpace
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral_restrict : ∀ {α : Type u_1} {m : MeasurableSpace α} (f : MeasureTheory.SimpleFunc α ENNReal) (s : Set α)
  (μ : MeasureTheory.Measure α), f.lintegral (μ.restrict s) = ∑ y ∈ f.range, y * μ (⇑f ⁻¹' {y} ∩ s)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.mkIso'_inv_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} (e : M ≅ N) [inst_3 : CategoryTheory.MonObj M]
  [inst_4 : CategoryTheory.IsCommMonObj M] [inst_5 : CategoryTheory.MonObj N] [inst_6 : CategoryTheory.IsCommMonObj N]
  [inst_7 : CategoryTheory.IsMonHom e.hom], (CategoryTheory.CommMon.mkIso' e).inv.hom.hom = e.inv
-- Mathlib.Analysis.LocallyConvex.AbsConvex
convex_absConvexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s : Set E}, Convex 𝕜 ((absConvexHull 𝕜) s)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.ofSimplex_map_le : ∀ {X : SSet} {n m : ℕ} (f : { len := n } ⟶ { len := m }) (x : X.obj (Opposite.op { len := m })),
  SSet.Subcomplex.ofSimplex ((CategoryTheory.ConcreteCategory.hom (X.map f.op)) x) ≤ SSet.Subcomplex.ofSimplex x
-- Std.Http.Protocol.H1
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.BodyMode.eof.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Machine.BodyMode.eof✝ = 1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `FunLike.coe_neg`. -/
ContinuousLinearMap.coe_neg' : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Neg F] [inst_2 : Neg β]
  [IsNegApply F α β] (f : F), ⇑(-f) = -⇑f
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.add_eq_zero_iff_neg_eq : ∀ {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α}, ↑u + a = 0 ↔ ↑(-u) = a
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.Context.mk : (level₂ level₁ level₀ : Lean.Level) →
  (B : Q(Type level₀)) → Q(CategoryTheory.Bicategory «$B») → Mathlib.Tactic.Bicategory.Context
-- Mathlib.RingTheory.Coalgebra.Basic
Finsupp.comul_single : ∀ (R : Type u) (ι : Type v) (A : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] (i : ι) (a : A),
  (CoalgebraStruct.comul fun₀ | i => a) =
    (TensorProduct.map (Finsupp.lsingle i) (Finsupp.lsingle i)) (CoalgebraStruct.comul a)
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.equiv_equiv_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {D' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D']
  (L : CategoryTheory.Functor C D) [inst_3 : L.IsLocalization W] (L' : CategoryTheory.Functor C D')
  [inst_4 : L'.IsLocalization W] (G : CategoryTheory.Functor D D') (e : L.comp G ≅ L') {X Y : C}
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y] (f : L.obj X ⟶ L.obj Y),
  (CategoryTheory.Localization.SmallHom.equiv W L') ((CategoryTheory.Localization.SmallHom.equiv W L).symm f) =
    CategoryTheory.CategoryStruct.comp (e.inv.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (e.hom.app Y))
-- Init.Data.List.Nat.TakeDrop
List.take_sublist_take_left : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, i ≤ j → (List.take i l).Sublist (List.take j l)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_add_aleph0 : ∀ (m : ℕ∞), ↑m + Cardinal.aleph0 = Cardinal.aleph0
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.dual_free : ∀ {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M] [Module.Free R M], Module.Free R (Module.Dual R M)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeFun.match_1.eq_1 : ∀ {n : ℕ} (motive : (x : ℕ) → Fin (n ^ x) → Sort u_1) (x : Fin (n ^ 0)) (h_1 : (x : Fin (n ^ 0)) → motive 0 x)
  (h_2 : (m k : ℕ) → (hk : k < n ^ (m + 1)) → motive m.succ ⟨k, hk⟩),
  (match 0, x with
    | 0, x => h_1 x
    | m.succ, ⟨k, hk⟩ => h_2 m k hk) =
    h_1 x
-- Mathlib.Algebra.Module.Submodule.Equiv
Submodule.comap_equiv_self_of_inj_of_le_apply : ∀ {R : Type u_1} {M : Type u_5} {N : Type u_9} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {f : M →ₗ[R] N} {p : Submodule R N} (hf : Function.Injective ⇑f)
  (h : p ≤ f.range) (x : ↥(Submodule.comap f p)),
  (Submodule.comap_equiv_self_of_inj_of_le hf h) x = (LinearMap.codRestrict p (f ∘ₗ (Submodule.comap f p).subtype) ⋯) x
-- Mathlib.Algebra.Lie.Semisimple.Defs
/-- A Lie algebra *has central radical* if its radical coincides with its center. Such Lie algebras
are called *reductive*, if the coefficients are a field of characteristic zero.

Note that there is absolutely [no agreement](https://mathoverflow.net/questions/284713/) on what
the label 'reductive' should mean when the coefficients are not a field of characteristic zero.  -/
LieAlgebra.HasCentralRadical : (R : Type u_1) → (L : Type u_2) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Prop
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mk_univ : ∀ {α : Type u_2} [inst : TopologicalSpace α], { carrier := Set.univ, is_open' := ⋯ } = ⊤
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH1_τ₃ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{max u u_1, u, u} k H}
  {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  (groupCohomology.mapShortComplexH1 f φ).τ₃ = groupCohomology.cochainsMap₂ f φ
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.map_lie : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (x : L) (m : M), f ⁅x, m⁆ = ⁅x, f m⁆
-- Std.Async.Basic
/-- Similar to `map`, however `f` has access to the `IO` monad. If `f` throws an error, the returned
`AsyncTask` resolves to that error.
 -/
Std.Async.AsyncTask.mapIO : {α β : Type} →
  (α → IO β) →
    Std.Async.AsyncTask α →
      optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO (Std.Async.AsyncTask β)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.mk.injEq : ∀ {G : Type u_6} [inst : Group G] (toFun : G → ℝ) (map_one' : toFun 1 = 0)
  (mul_le' : ∀ (x y : G), toFun (x * y) ≤ toFun x + toFun y) (inv' : ∀ (x : G), toFun x⁻¹ = toFun x) (toFun_1 : G → ℝ)
  (map_one'_1 : toFun_1 1 = 0) (mul_le'_1 : ∀ (x y : G), toFun_1 (x * y) ≤ toFun_1 x + toFun_1 y)
  (inv'_1 : ∀ (x : G), toFun_1 x⁻¹ = toFun_1 x),
  ({ toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' } =
      { toFun := toFun_1, map_one' := map_one'_1, mul_le' := mul_le'_1, inv' := inv'_1 }) =
    (toFun = toFun_1)
-- Mathlib.Order.Shrink
instWellFoundedGTShrink : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Preorder α] [WellFoundedGT α], WellFoundedGT (Shrink.{u, u_1} α)
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- If `χ` is a Dirichlet character and its level `M` divides `N`, then we obtain the L function
of `χ` considered as a Dirichlet character of level `N` from the L function of `χ` by multiplying
with `∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s))`.
(Note that `1 - χ p * p ^ (-s) = 1` when `p` divides `M`).  -/
DirichletCharacter.LFunction_changeLevel : ∀ {M N : ℕ} [inst : NeZero M] [inst_1 : NeZero N] (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ},
  χ ≠ 1 ∨ s ≠ 1 →
    DirichletCharacter.LFunction ((DirichletCharacter.changeLevel hMN) χ) s =
      DirichletCharacter.LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.defEq : Lean.Parser.Parser
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_ofNat' : ∀ (n : ℕ), (UInt32.ofNat n).toUInt8 = UInt8.ofNat n
-- Mathlib.Order.RelClasses
/-- Set notation form of `ge_antisymm_iff` -/
superset_antisymm_iff : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a = b ↔ b ⊆ a ∧ a ⊆ b
-- Mathlib.Topology.VectorBundle.Basic
/-- The index set of a vector bundle core, as a convenience function for dot notation  -/
VectorBundleCore.Index : {ι : Type u_5} → Type u_5
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.toArray_toList : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.IsAlwaysFinite α], r.toList.toArray = r.toArray
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
TensorProduct.Algebra.exists_of_fg : ∀ {R : Type u_1} {S : Type u_2} {N : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (u : TensorProduct R S N),
  ∃ A, A.FG ∧ u ∈ (LinearMap.rTensor N A.val.toLinearMap).range
-- Mathlib.Data.Nat.Choose.Basic
/-- `choose n 2` is the `n`-th triangle number.  -/
Nat.choose_two_right : ∀ (n : ℕ), n.choose 2 = n * (n - 1) / 2
-- Mathlib.Data.Rel
/-- A relation `R` is irreflexive if `¬ a ~[R] a`.  -/
SetRel.IsIrrefl : {α : Type u_1} → SetRel α α → Prop
-- Mathlib.RingTheory.Algebraic.Integral
Subalgebra.mem_algebraicClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain R]
  {x : S}, x ∈ Subalgebra.algebraicClosure R S ↔ IsAlgebraic R x
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.valueGroup₀Fun.congr_simp : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedCommGroupWithZero Γ₀]
  [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] [inst_2 : Ring R] {v : Valuation R Γ₀} {w : Valuation R Γ'₀}
  (h : v.IsEquiv w) (x x_1 : (MonoidWithZeroHom.ofClass v).ValueGroup₀),
  x = x_1 → h.valueGroup₀Fun x = h.valueGroup₀Fun x_1
-- Init.Data.Array.MinMax
Array.min_toList : ∀ {α : Type u_1} [inst : Min α] {xs : Array α} {h : xs.toList ≠ []}, xs.toList.min h = xs.min ⋯
-- Mathlib.Control.Monad.Writer
WriterT.instMonadOfEmptyCollectionOfAppend : {M : Type u → Type v} → {ω : Type u} → [Monad M] → [EmptyCollection ω] → [Append ω] → Monad (WriterT ω M)
-- Mathlib.Data.Num.ZNum
ZNum.dvd_iff_mod_eq_zero : ∀ {m n : ZNum}, m ∣ n ↔ n % m = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.limitConeOfUnique_cone_π : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C),
  (CategoryTheory.Limits.limitConeOfUnique f).cone.π =
    CategoryTheory.Discrete.natTrans fun x =>
      match x with
      | { as := j } => CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Group.Center
Set.centralizer_centralizer_comm_of_comm : ∀ {M : Type u_1} {S : Set M} [inst : Mul M],
  (∀ x ∈ S, ∀ y ∈ S, x * y = y * x) → ∀ x ∈ S.centralizer.centralizer, ∀ y ∈ S.centralizer.centralizer, x * y = y * x
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_snd_fst : ∀ (s : (n : ℕ) × Finset (Fin n)), (FormalMultilinearSeries.changeOriginIndexEquiv.symm s).snd.fst = s.snd.card
-- Mathlib.Tactic.Basic
/-- Return value of the executed tactic.  -/
Mathlib.Tactic.withResetServerInfo.Result.result? : {α : Type} → Mathlib.Tactic.withResetServerInfo.Result α → Option α
-- Init.Data.List.Lemmas
List.getLast?_eq_getLast : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.getLast? = some (l.getLast h)
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- For an example of a non-free projective `K`-module `V` for which the forward implication
fails, see https://stacks.math.columbia.edu/tag/05WG#comment-9913.  -/
Module.finite_dual_iff : ∀ (K : Type uK) {V : Type uV} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Free K V], Module.Finite K (Module.Dual K V) ↔ Module.Finite K V