mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.HeadIndex
Lean.HeadIndex.proj.inj : ∀ {structName : Lean.Name} {idx : ℕ} {structName_1 : Lean.Name} {idx_1 : ℕ},
  Lean.HeadIndex.proj structName idx = Lean.HeadIndex.proj structName_1 idx_1 → structName = structName_1 ∧ idx = idx_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_max : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LinearOrder α] [MulLeftMono α] (a b c : α), a * max b c = max (a * b) (a * c)
-- ProofWidgets.Util
/-- Delaborate the elements of a list literal separately, calling `elem` on each.  -/
Lean.PrettyPrinter.Delaborator.delabListLiteral : {α : Type} → Lean.PrettyPrinter.Delaborator.DelabM α → Lean.PrettyPrinter.Delaborator.DelabM (Array α)
-- Mathlib.Algebra.Group.Action.Units
Units.smulCommClass_left : ∀ {M : Type u_3} {N : Type u_4} {α : Type u_5} [inst : Monoid M] [inst_1 : SMul M α] [inst_2 : SMul N α]
  [SMulCommClass M N α], SMulCommClass Mˣ N α
-- Mathlib.Order.Minimal
maximal_mem_image_antitone_iff : ∀ {α : Type u_2} {β : Type u_3} {a : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  a ∈ s →
    (∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ x ≤ y)) →
      (Maximal (fun x => x ∈ f '' s) (f a) ↔ Minimal (fun x => x ∈ s) a)
-- Lean.Elab.Binders
Lean.Elab.Term.BinderView.mk.injEq : ∀ (ref id type : Lean.Syntax) (bi : Lean.BinderInfo) (ref_1 id_1 type_1 : Lean.Syntax) (bi_1 : Lean.BinderInfo),
  ({ ref := ref, id := id, type := type, bi := bi } = { ref := ref_1, id := id_1, type := type_1, bi := bi_1 }) =
    (ref = ref_1 ∧ id = id_1 ∧ type = type_1 ∧ bi = bi_1)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.isPrefixOf.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (as : List α) (b : α) (bs : List α)
  (h_1 : (x : List α) → motive [] x) (h_2 : (x : List α) → motive x [])
  (h_3 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)),
  (match a :: as, b :: bs with
    | [], x => h_1 x
    | x, [] => h_2 x
    | a :: as, b :: bs => h_3 a as b bs) =
    h_3 a as b bs
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
WfDvdMonoid.induction_on_irreducible : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [WfDvdMonoid α] {motive : α → Prop} (a : α),
  motive 0 →
    (∀ (u : α), IsUnit u → motive u) → (∀ (a i : α), a ≠ 0 → Irreducible i → motive a → motive (i * a)) → motive a
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.uniformBell_zero_left : ∀ (n : ℕ), Nat.uniformBell 0 n = 1
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.karoubiUniversal₁_counitIso : ∀ (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],
  (CategoryTheory.Idempotents.karoubiUniversal₁ C D).counitIso =
    CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso C D
-- Mathlib.Order.CompleteLattice.Finset
/-- Infimum of `s i`, `i : ι`, is equal to the infimum over `t : Finset ι` of infima
`⨅ i ∈ t, s i`. This version assumes `ι` is a `Type*`. See `iInf_eq_iInf_finset'` for a version
that works for `ι : Sort*`.  -/
iInf_eq_iInf_finset : ∀ {α : Type u_2} {ι : Type u_5} [inst : CompleteLattice α] (s : ι → α), ⨅ i, s i = ⨅ t, ⨅ i ∈ t, s i
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The difference of two `C^n` functions on a domain is `C^n`.  -/
ContDiffOn.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {s : Set E} {f g : E → F}, ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n g s → ContDiffOn 𝕜 n (fun x => f x - g x) s
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.mk'_ker : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  [inst_6 : LieModule R L M], (LieSubmodule.Quotient.mk' N).ker = N
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk.sizeOf_spec : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  [inst_2 : SizeOf M] [inst_3 : SizeOf N] (toAddHom : M →ₙ+ N) (isLocalizationMap : S.IsLocalizationMap toAddHom.toFun),
  sizeOf { toAddHom := toAddHom, isLocalizationMap := isLocalizationMap } =
    1 + sizeOf toAddHom + sizeOf isLocalizationMap
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
/-- The initial functor `ℕᵒᵖ ⥤ J`, which allows us to turn cofiltered limits over countable preorders
into sequential limits.
 -/
CategoryTheory.Limits.IsFiltered.sequentialFunctor : (J : Type u_2) → [Countable J] → [inst : Preorder J] → [CategoryTheory.IsFiltered J] → CategoryTheory.Functor ℕ J
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Real.cosh` is real analytic.  -/
Real.analyticOnNhd_cosh : ∀ {s : Set ℝ}, AnalyticOnNhd ℝ Real.cosh s
-- Init.Data.UInt.Lemmas
UInt32.toUSize_toUInt64 : ∀ (n : UInt32), n.toUInt64.toUSize = n.toUSize
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff : ∀ {K : Type u_1} [inst : Field K] {x : NumberField.mixedEmbedding.mixedSpace K},
  (∀ (w : NumberField.InfinitePlace K), (NumberField.mixedEmbedding.normAtPlace w) x = 0) ↔ x = 0
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.quotEquivOfEq_mk : ∀ {R : Type u} [inst : Ring R] {I J : Ideal R} [inst_1 : I.IsTwoSided] [inst_2 : J.IsTwoSided] (h : I = J) (x : R),
  (Ideal.quotEquivOfEq h) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk J) x
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeWalkingCospanCospanForget : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) AlgebraicGeometry.Scheme.forget
-- Mathlib.FieldTheory.Perfect
powMulEquiv_one : ∀ (M : Type u_1) [inst : CommMonoid M], powMulEquiv M 1 = MulEquiv.refl M
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyData.unop_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.LeftHomologyData), h.unop.p = h.i.unop
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.IsUniquelyCodimOneFace.iff_of_iso : ∀ {X Y : SSet} (e : X ≅ Y) (x y : X.S),
  { dim := x.dim,
          simplex :=
            (CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op { len := x.dim })))
              x.simplex }.IsUniquelyCodimOneFace
      { dim := y.dim,
        simplex := (CategoryTheory.ConcreteCategory.hom (e.hom.app (Opposite.op { len := y.dim }))) y.simplex } ↔
    x.IsUniquelyCodimOneFace y
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Aut.Aut_mul_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) (f g : CategoryTheory.Aut X), f * g = g ≪≫ f
-- Std.Internal.UV.System
Std.Internal.UV.System.PasswdInfo.username : Std.Internal.UV.System.PasswdInfo → String
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ_eq_of_isBasis : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {B : Set (TopologicalSpace.Opens ↑X)},
  TopologicalSpace.Opens.IsBasis B →
    ∀ (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (x : ↑X) (mU : x ∈ U) (mV : x ∈ V)
      {s : CategoryTheory.ToType (F.obj (Opposite.op U))} {t : CategoryTheory.ToType (F.obj (Opposite.op V))},
      (CategoryTheory.ConcreteCategory.hom (F.germ U x mU)) s =
          (CategoryTheory.ConcreteCategory.hom (F.germ V x mV)) t →
        ∃ W,
          ∃ (_ : x ∈ W) (_ : W ∈ B) (hWU : W ≤ U) (hWV : W ≤ V),
            (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hWU).op)) s =
              (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hWV).op)) t
-- Mathlib.CategoryTheory.Limits.Final
/-- The hypotheses also imply that `G` is initial, see `initial_of_comp_full_faithful'`.  -/
CategoryTheory.Functor.initial_of_comp_full_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [G.Full] [G.Faithful] [(F.comp G).Initial], F.Initial
-- Init.Data.String.Termination
String.Slice.Pos.remainingBytes_eq : ∀ {s : String.Slice} {p : s.Pos}, p.remainingBytes = s.utf8ByteSize - p.offset.byteIdx
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_zero' : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), (Polynomial.hasseDeriv 0) f = f
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_append_of_eq : ∀ {k w i : ℕ} {x : BitVec (k * w)} {y : BitVec w}, i = k → BitVec.extractLsb' (i * w) w (y ++ x) = y
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.one_smul_sub_smul_one_mem_ideal : ∀ (R : Type u) {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (a : S),
  1 ⊗ₜ[R] a - a ⊗ₜ[R] 1 ∈ KaehlerDifferential.ideal R S
-- Init.Data.String.Lemmas.Splits
/-- You might want to invoke `Pos.Splits.exists_eq_append_singleton_of_ne_startPos` to be able to apply this.  -/
String.Pos.Splits.of_prev : ∀ {t₁ : String} {c : Char} {t₂ s : String} {p : s.Pos} {hp : p ≠ s.startPos},
  (p.prev hp).Splits t₁ (String.singleton c ++ t₂) → p.Splits (t₁ ++ String.singleton c) t₂
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.skipUntilDedent : ℕ → Lean.Parser.ParserFn
-- Mathlib.Analysis.Normed.Group.AddTorsor
NormedAddTorsor.mk : {V : outParam (Type u_1)} →
  {P : Type u_2} →
    [inst : SeminormedAddCommGroup V] →
      [inst_1 : PseudoMetricSpace P] →
        [toAddTorsor : AddTorsor V P] → (∀ (x y : P), dist x y = ‖x -ᵥ y‖) → NormedAddTorsor V P
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.const_apply : ∀ {X Y : TopCat} (y : ↑Y) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (TopCat.const y)) x = y
-- Mathlib.Algebra.GroupWithZero.Defs
/-- `a / b := a * b⁻¹`  -/
CommGroupWithZero.div_eq_mul_inv : ∀ {G₀ : Type u_2} [self : CommGroupWithZero G₀] (a b : G₀), a / b = a * b⁻¹
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- The forgetful functor from the category of based functors `𝒳 ⥤ᵇ 𝒴` to the category of
functors of underlying categories, `𝒳.obj ⥤ 𝒴.obj`.  -/
CategoryTheory.BasedNatTrans.forgetful : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    (𝒳 : CategoryTheory.BasedCategory 𝒮) →
      (𝒴 : CategoryTheory.BasedCategory 𝒮) →
        CategoryTheory.Functor (CategoryTheory.BasedFunctor 𝒳 𝒴) (CategoryTheory.Functor 𝒳.obj 𝒴.obj)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- The ring homomorphism that takes a section of the structure sheaf of `Proj` on the open set `U`,
implemented as a subtype of dependent functions to localizations at homogeneous prime ideals, and
evaluates the section on the point corresponding to a given homogeneous prime ideal.  -/
AlgebraicGeometry.openToLocalization : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)) →
                (x : ↑(ProjectiveSpectrum.top 𝒜)) →
                  x ∈ U →
                    ((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op U) ⟶
                      CommRingCat.of (HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal))
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements),
  ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).obj X).base = X.fst
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Lattice.BicartSq.multicoequalizerDiagram : ∀ {T : Type u} [inst : CompleteLattice T] {x₁ x₂ x₃ x₄ : T},
  Lattice.BicartSq x₁ x₂ x₃ x₄ →
    CompleteLattice.MulticoequalizerDiagram x₄ (fun i => bif i then x₃ else x₂) fun i j =>
      bif i then bif j then x₃ else x₁ else bif j then x₁ else x₂
-- Lean.Data.DeclarationRange
Lean.DeclarationLocation.mk.sizeOf_spec : ∀ (module : Lean.Name) (range : Lean.DeclarationRange),
  sizeOf { module := module, range := range } = 1 + sizeOf module + sizeOf range
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_toUInt64 : ∀ (n : UInt16), n.toUInt64.toBitVec = BitVec.setWidth 64 n.toBitVec
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.mem_adjoin_simple_self : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E), α ∈ F⟮α⟯
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Given a right adjoint functor between categories of cones,
the image of a limit cone is a limit cone.
 -/
CategoryTheory.Limits.IsLimit.ofRightAdjoint : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {D : Type u₄} →
                [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                  {G : CategoryTheory.Functor K D} →
                    {left : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone G)} →
                      {right : CategoryTheory.Functor (CategoryTheory.Limits.Cone G) (CategoryTheory.Limits.Cone F)} →
                        (left ⊣ right) →
                          {c : CategoryTheory.Limits.Cone G} →
                            CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsLimit (right.obj c)
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.mulLeft_apply : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G] (c x : G),
  (IsometryEquiv.mulLeft c) x = c * x
-- Mathlib.Logic.Equiv.Defs
/-- Bijective functions are equivalent to equivalences.  -/
Equiv.bijectiveEquiv : {α : Sort u} → {β : Sort v} → { f // Function.Bijective f } ≃ (α ≃ β)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.toGermMonoidHom.eq_1 : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Monoid γ] [inst_3 : ContinuousMul γ],
  MeasureTheory.AEEqFun.toGermMonoidHom = { toFun := MeasureTheory.AEEqFun.toGerm, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- A non-instance `FunLike` instance on `X ⟶ Y`.  -/
CategoryTheory.ConcreteCategory.instFunLike : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {X Y : C} → FunLike (X ⟶ Y) (CategoryTheory.ToType X) (CategoryTheory.ToType Y)
-- Mathlib.CategoryTheory.Limits.Types.Limits
/-- The equivalence between the abstract limit of `F` in `Type max v u`
and the "concrete" definition as the sections of `F`.
 -/
CategoryTheory.Limits.Types.limitEquivSections : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type u)) →
      [inst_1 : CategoryTheory.Limits.HasLimit F] → CategoryTheory.Limits.limit F ≃ ↑F.sections
-- Lean.Meta.Tactic.Grind.Injection
/-- The `grind` tactic includes an auxiliary `injection?` tactic that is not intended for direct use by users.
This tactic is automatically applied when introducing non-dependent propositions.
It differs from the user-facing Lean `injection` tactic in the following ways:

- It does not introduce new propositions. Instead, the `grind` tactic preprocessor is responsible for introducing them.
- It assumes that `fvarId` is the latest local declaration in the current goal.
- It does not handle cases where the constructors are different because the simplifier already reduces such equalities to `False`.
- It does not have support for heterogeneous equality. Recall that the simplifier already reduces them to `Eq` if
  the types are definitionally equal.
 -/
Lean.Meta.Grind.injection? : Lean.MVarId → Lean.FVarId → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.Order.Nucleus
Nucleus.comp_eq_right_iff_le : ∀ {X : Type u_1} [inst : Order.Frame X] {n m : Nucleus X}, ⇑n ∘ ⇑m = ⇑m ↔ n ≤ m
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.of_map : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {c : NNReal} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'}
  {μ : MeasureTheory.Measure Ω'} {Y : Ω' → Ω} {X : Ω → ℝ},
  AEMeasurable Y μ →
    ProbabilityTheory.HasSubgaussianMGF X c (MeasureTheory.Measure.map Y μ) →
      ProbabilityTheory.HasSubgaussianMGF (X ∘ Y) c μ
-- Mathlib.Probability.Distributions.Cauchy
/-- The pdf of the gamma distribution, as a function valued in `ℝ≥0∞`.  -/
ProbabilityTheory.cauchyPDF : ℝ → NNReal → ℝ → ENNReal
-- Mathlib.Order.Quotient
Quotient.mk_monotone : ∀ {α : Type u_1} {s : Setoid α} [inst : Preorder α], Monotone (Quotient.mk s)
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.subrepresentationSubmoduleOrderIso_apply : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W} (σ : Subrepresentation ρ),
  Subrepresentation.subrepresentationSubmoduleOrderIso σ = σ.asSubmodule
-- Mathlib.CategoryTheory.Galois.Examples
CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeFunObjFiniteV : ∀ (G : Type u) [inst : Group G],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget (Action FintypeCat G))
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_then_ite' : ∀ {α : Sort u_1} (c0 c1 : Bool) {a b : α}, (bif c0 then bif c1 then a else b else a) = bif c0 && !c1 then b else a
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.ofLinearEquiv_refl : ∀ {k : Type u_10} {V : Type u_11} {P : Type u_12} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p : P), AffineEquiv.ofLinearEquiv (LinearEquiv.refl k V) p p = AffineEquiv.refl k P
-- Mathlib.Algebra.Homology.HomologicalComplexAbelian
CategoryTheory.instPreservesColimitsOfShapeHomologicalComplexMapHomologicalComplexOfHasColimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [inst_4 : F.PreservesZeroMorphisms]
  {J : Type u_4} [inst_5 : CategoryTheory.Category.{v_3, u_4} J] [CategoryTheory.Limits.HasColimitsOfShape J C]
  [CategoryTheory.Limits.PreservesColimitsOfShape J F],
  CategoryTheory.Limits.PreservesColimitsOfShape J (F.mapHomologicalComplex c)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.dualAnnihilator_eq_bot_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {W : Submodule R M}
  [Module.Projective R (M ⧸ W)], W.dualAnnihilator = ⊥ ↔ W = ⊤
-- Init.Data.SInt.Lemmas
Int16.toInt16_toInt64 : ∀ (n : Int16), n.toInt64.toInt16 = n
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Function.Surjective.summable_iff_of_hasSum_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {α' : Type u_4}
  [inst_2 : AddCommMonoid α'] [inst_3 : TopologicalSpace α'] {e : α' → α},
  Function.Surjective e →
    ∀ {f : β → α} {g : γ → α'}, (∀ {a : α'}, HasSum f (e a) ↔ HasSum g a) → (Summable f ↔ Summable g)
-- Lean.Elab.Term.TermElabM
/-- Ensure metavariables registered using `registerMVarErrorInfos` (and used in the given declaration) have been assigned.  -/
Lean.Elab.Term.ensureNoUnassignedMVars : Lean.Declaration → Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂CompMap₂Iso_hom_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') {C' : Type u₆} [inst_4 : CategoryTheory.Category.{v₆, u₆} C'] {D' : Type u₅}
  [inst_5 : CategoryTheory.Category.{v₅, u₅} D'] {L'' : D'} {R'' : CategoryTheory.Functor C' D'}
  {F' : CategoryTheory.Functor C' C} {G' : CategoryTheory.Functor D' D} (α' : L ⟶ G'.obj L'')
  (β' : R''.comp G' ⟶ F'.comp R) (X : CategoryTheory.StructuredArrow L'' R''),
  ((CategoryTheory.StructuredArrow.map₂CompMap₂Iso α β α' β').hom.app X).right =
    CategoryTheory.CategoryStruct.id (F.obj (F'.obj X.right))
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.comp_zero : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P] (f : ZeroHom N P),
  f.comp 0 = 0
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.zero.sizeOf_spec : sizeOf Lean.Grind.Linarith.Expr.zero = 1
-- Mathlib.Data.Nat.Dist
Nat.dist_eq_sub_of_le : ∀ {n m : ℕ}, n ≤ m → n.dist m = m - n
-- Init.Prelude
SeqLeft.mk : {f : Type u → Type v} → ({α β : Type u} → f α → (Unit → f β) → f α) → SeqLeft f
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq.congr_simp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f f_1 : X ⟶ Z) (e_f : f = f_1) (g g_1 : Y ⟶ Z) (e_g : g = g_1)
  [H : AlgebraicGeometry.IsOpenImmersion f] [inst : AlgebraicGeometry.IsOpenImmersion g]
  (e : Set.range ⇑f = Set.range ⇑g),
  AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f g e = AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f_1 g_1 ⋯
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
AddGroup.is_simple_iff_prime_card : ∀ {α : Type u_1} [inst : AddGroup α] [IsAddCommutative α], IsSimpleAddGroup α ↔ Nat.Prime (Nat.card α)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeries_nilpotencyClass : ∀ {G : Type u_1} [inst : AddGroup G] [hG : AddGroup.IsNilpotent G],
  AddSubgroup.upperCentralSeries G (AddGroup.nilpotencyClass G) = ⊤
-- Batteries.Data.Array.Basic
/-- Remove the first element of a subarray. Returns the element and the remaining
subarray, or `none` if the subarray is empty.
 -/
Subarray.popHead? : {α : Type u_1} → Subarray α → Option (α × Subarray α)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.localRingHom_comp_stalkIso_apply : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  (p : ProjectiveSpectrum ℬ)
  (x : ↑((AlgebraicGeometry.Proj 𝒜).presheaf.stalk ((AlgebraicGeometry.ProjectiveSpectrum.comap f hf) p))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Proj.stalkIso ℬ p).inv)
      ((HomogeneousLocalization.localRingHom f
          ((AlgebraicGeometry.ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal p.asHomogeneousIdeal.toIdeal
          ⋯)
        ((CategoryTheory.ConcreteCategory.hom
            (AlgebraicGeometry.Proj.stalkIso 𝒜 ((AlgebraicGeometry.ProjectiveSpectrum.comap f hf) p)).hom)
          x)) =
    (CategoryTheory.ConcreteCategory.hom
        (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (AlgebraicGeometry.Proj.sheafedSpaceMap f hf).hom p))
      x