mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.StarAlgHom
/-- See Note [custom simps projection]  -/
StarAlgEquiv.Simps.symm_apply : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : Add A] →
        [inst_1 : Add B] →
          [inst_2 : Mul A] →
            [inst_3 : Mul B] →
              [inst_4 : SMul R A] → [inst_5 : SMul R B] → [inst_6 : Star A] → [inst_7 : Star B] → (A ≃⋆ₐ[R] B) → B → A
-- Mathlib.Algebra.Lie.UniversalEnveloping
/-- The natural Lie algebra morphism from a Lie algebra to its universal enveloping algebra.  -/
UniversalEnvelopingAlgebra.ι : (R : Type u₁) →
  {L : Type u₂} →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → L →ₗ⁅R⁆ UniversalEnvelopingAlgebra R L
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo : ∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCat} [inst : IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X),
  IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.stalkClosedPointTo f))
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instSupSet : {R : Type u_2} →
  {N : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid N] →
        [inst_2 : TopologicalSpace N] →
          [inst_3 : Module R N] → [ContinuousAdd N] → [ContinuousConstSMul R N] → SupSet (ClosedSubmodule R N)
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.rootDiscr_def : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.rootDiscr K = ↑|NumberField.discr K| ^ (↑(Module.finrank ℚ K))⁻¹
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_nilpotencyClass : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G], ⊤.lowerCentralSeries (Group.nilpotencyClass G) = ⊥
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.innerHornInclusions.intro : ∀ {n : ℕ} (i : Fin (n + 3)), 0 < i → i < Fin.last (n + 2) → SSet.innerHornInclusions (SSet.horn (n + 2) i).ι
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.preimage_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), (TopologicalSpace.Opens.map f.base).obj ⊤ = ⊤
-- Mathlib.Topology.Compactness.Compact
IsCompact.compl_mem_cocompact : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsCompact s → sᶜ ∈ Filter.cocompact X
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.inter : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {s' : Set α} {t' : Set β},
  e.IsImage s t → e.IsImage s' t' → e.IsImage (s ∩ s') (t ∩ t')
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Functor.CommShift.isoZero'.congr_simp : ∀ {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] (F : CategoryTheory.Functor C D) (A : Type u_4) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] (a : A) (ha : a = 0),
  CategoryTheory.Functor.CommShift.isoZero' F A a ha = CategoryTheory.Functor.CommShift.isoZero' F A a ha
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_funUnique : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Unique ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace M], ⇑(ContinuousLinearEquiv.funUnique ι R M) = Function.eval default
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.add_both_eq_both : ∀ (b : Bool),
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment b Std.Tactic.BVDecide.LRAT.Internal.Assignment.both =
    Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S : Solution`, we have that `2 ≤ S.multiplicity`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.two_le_multiplicity : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K], 2 ≤ FermatLastTheoremForThreeGen.Solution.multiplicity✝ S
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformAddGroup.mk : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : AddGroup α],
  (UniformContinuous fun p => p.1 - p.2) → IsUniformAddGroup α
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.mulMap_map_comp_eq : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] (A B : Subalgebra R S) (f : S →ₐ[R] T),
  ((Subalgebra.map f A).mulMap (Subalgebra.map f B)).comp
      (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)) =
    f.comp (A.mulMap B)
-- Mathlib.Analysis.LocallyConvex.AbsConvex
subset_closedAbsConvexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] [inst_4 : TopologicalSpace E] {s : Set E}, s ⊆ (closedAbsConvexHull 𝕜) s
-- Mathlib.Topology.Filter
ContinuousOn.nhds : ∀ {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  ContinuousOn f s → ContinuousOn (nhds ∘ f) s
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.inclusion_obj : ∀ (a : SimplexCategory), AugmentedSimplexCategory.inclusion.obj a = CategoryTheory.WithInitial.of a
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_reindexRange : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂)
  [inst_8 : DecidableEq M₁] (f : M₁ →ₗ[R] M₂) (k : m) (i : n),
  (LinearMap.toMatrix v₁.reindexRange v₂.reindexRange) f ⟨v₂ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (LinearMap.toMatrix v₁ v₂) f k i
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap_comm_of_commute : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S),
  (∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n) → N.mulMap M = M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M)
-- Init.Data.UInt.Lemmas
USize.ofBitVec_div : ∀ (a b : BitVec System.Platform.numBits), { toBitVec := a / b } = { toBitVec := a } / { toBitVec := b }
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.AtomNode.mk : ℕ → ℕ → ℕ → Mathlib.Tactic.BicategoryLike.Atom → Mathlib.Tactic.Widget.StringDiagram.AtomNode
-- Std.Time.Zoned.Database.PosixTz
/-- Parse a POSIX TZ footer string into a `RecurringRule`, returning an error on failure.

When `extended` is `true`, transition times accept signed hours in the range
-`167` to `167` instead of the POSIX-required 0 to `24` (TZif version 3+).
 -/
Std.Time.TimeZone.parsePosixTz : String → optParam Bool false → Except String Std.Time.TimeZone.RecurringRule
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
_private.Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin.0.ContinuousAlternatingMap.alternatizeUncurryFinCLM.aux.eq_1 : ∀ {𝕜 : 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] {n : ℕ},
  ContinuousAlternatingMap.alternatizeUncurryFinCLM.aux✝ =
    AlternatingMap.alternatizeUncurryFinLM ∘ₗ
      LinearMap.compRight 𝕜 ContinuousAlternatingMap.toAlternatingMapLinear ∘ₗ ContinuousLinearMap.coeLM 𝕜
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.enum_typein : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] (a : α),
  (Ordinal.enum r) ⟨(Ordinal.typein r).toRelEmbedding a, ⋯⟩ = a
-- Lean.Meta.Tactic.Util
/-- Produces an error message indicating that tactic `tacticName` has failed with the message `msg`,
and displays the state of `mvarId` below the message.
 -/
Lean.Meta.mkTacticExMsg : Lean.Name → Lean.MVarId → Lean.MessageData → Lean.MessageData
-- Mathlib.Topology.Algebra.Group.Basic
continuous_sub_left : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Sub G] [ContinuousSub G] (a : G), Continuous fun x => a - x
-- Init.Data.UInt.Lemmas
USize.one_def : 1 = { toBitVec := 1 }
-- Mathlib.Algebra.Free
_private.Mathlib.Algebra.Free.0.FreeMagma.liftAux.match_1.eq_2 : ∀ {α : Type u_1} (motive : FreeMagma α → Sort u_2) (x y : FreeMagma α) (h_1 : (x : α) → motive (FreeMagma.of x))
  (h_2 : (x y : FreeMagma α) → motive (x.mul y)),
  (match x.mul y with
    | FreeMagma.of x => h_1 x
    | x.mul y => h_2 x y) =
    h_2 x y
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
/-- The **spectral mapping theorem** for the non-unital continuous functional calculus.  -/
cfcₙHom_map_quasispectrum : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  (f : ContinuousMapZero (↑(quasispectrum R a)) R), quasispectrum R ((cfcₙHom ha) f) = Set.range ⇑f
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_g : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₃.g =
    CategoryTheory.Limits.cokernel.map (CategoryTheory.CategoryStruct.comp f g) g f (CategoryTheory.CategoryStruct.id Z)
      ⋯
-- Mathlib.Analysis.Complex.Exponential
Real.abs_exp : ∀ (x : ℝ), |Real.exp x| = Real.exp x
-- Mathlib.Computability.RegularExpressions
RegularExpression.instDecidablePredListMemLanguageMatches' : {α : Type u_1} → [DecidableEq α] → (P : RegularExpression α) → DecidablePred fun x => x ∈ P.matches'
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.Icc_mem_nhds : ∀ {x ε : ENNReal}, x ≠ ⊤ → ε ≠ 0 → Set.Icc (x - ε) (x + ε) ∈ nhds x
-- Mathlib.CategoryTheory.Abelian.Opposite
/-- The opposite of the image of `g.unop` is the image of `g`.  -/
CategoryTheory.imageUnopOp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {A B : Cᵒᵖ} → (g : A ⟶ B) → Opposite.op (CategoryTheory.Limits.image g.unop) ≅ CategoryTheory.Limits.image g
-- Mathlib.Order.CompleteBooleanAlgebra
biSup_inf_biSup : ∀ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} {s : Set ι} {t : Set ι'},
  (⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j = ⨆ p ∈ s ×ˢ t, f p.1 ⊓ g p.2
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotCoeff.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P P_1 : RootPairing ι R M N} (e_P : P = P_1) [inst_8 : P.IsCrystallographic] (i i_1 : ι),
  i = i_1 → ∀ (j j_1 : ι), j = j_1 → RootPairing.chainBotCoeff i j = RootPairing.chainBotCoeff i_1 j_1
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.instPreorder : {X : SSet} → Preorder X.N
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- Given `F : CofFibFactorizationQuasiIsoLE f n₀`, this is the morphism which relates
the intermediate objects in the factorisations `F.next n₁ _` and `F`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.fromNext : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        {f : K ⟶ L} →
          [inst_2 : CategoryTheory.EnoughInjectives C] →
            {n₀ : ℤ} →
              (F : CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE✝ f n₀) →
                (n₁ : ℤ) →
                  (hn₁ : n₀ + 1 = n₁) →
                    (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.CofFibFactorizationQuasiIsoLE.next✝ F n₁
                          hn₁).obj ⟶
                      F.obj
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- When `N` and `P` are equivalent, quadratic maps on `M` into `N` are equivalent to quadratic
maps on `M` into `P`.

See `LinearMap.BilinMap.congr₂` for the bilinear map version.  -/
LinearEquiv.congrQuadraticMap : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      {P : Type u_6} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R N] →
                  [inst_5 : AddCommMonoid P] →
                    [inst_6 : Module R P] → (N ≃ₗ[R] P) → QuadraticMap R M N ≃ₗ[R] QuadraticMap R M P
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfPair.congr : ∀ {R : Type u_1} {M : Type u_3} {M' : Type u_4} {N : Type u_5} {N' : Type u_6} [inst : AddCommGroup M]
  [inst_1 : AddCommGroup N] [inst_2 : AddCommGroup M'] [inst_3 : AddCommGroup N'] [inst_4 : CommRing R]
  [inst_5 : Module R M] [inst_6 : Module R M'] [inst_7 : Module R N] [inst_8 : Module R N'] (p : M →ₗ[R] N →ₗ[R] R)
  [p.IsPerfPair] (eM : M' ≃ₗ[R] M) (eN : N' ≃ₗ[R] N) (q : M' →ₗ[R] N' →ₗ[R] R),
  q.compl₁₂ ↑eM.symm ↑eN.symm = p → q.IsPerfPair
-- Lean.CoreM
Lean.instMonadRuntimeExceptionReaderT : {m : Type → Type} → {ρ : Type} → [Lean.MonadRuntimeException m] → Lean.MonadRuntimeException (ReaderT ρ m)
-- Mathlib.Order.MinMax
max_min_distrib_right : ∀ {α : Type u} [inst : LinearOrder α] (a b c : α), max (min a b) c = min (max a c) (max b c)
-- Mathlib.Logic.Function.OfArity
Function.OfArity.inhabited : {α β : Type u_1} → {n : ℕ} → [Inhabited β] → Inhabited (Function.OfArity α β n)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItemData.pos : Lean.Lsp.ResolvableCompletionItemData → Lean.Lsp.Position
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.isLemma : Lean.Meta.SimpTheorems → Lean.Meta.Origin → Bool
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f * g) x = f x * g x` has left cancellative multiplication if
`β` has left cancellative multiplication.  -/
FunLike.isLeftCancelMul : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : Mul β]
  [IsLeftCancelMul β] [IsMulApply F α β], IsLeftCancelMul F
-- Mathlib.Data.Fin.Fin2
Fin2.rev.eq_2 : ∀ (n_1 : ℕ) (i : Fin2 n_1), i.fs.rev = i.rev.castSucc
-- Mathlib.Analysis.Analytic.Constructions
/-- Finite products of analytic functions are analytic  -/
Finset.analyticOn_prod : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_9} [inst_3 : NormedCommRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : α → E → A}
  {s : Set E} (N : Finset α), (∀ n ∈ N, AnalyticOn 𝕜 (f n) s) → AnalyticOn 𝕜 (∏ n ∈ N, f n) s
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- A semigroup homomorphism `M →ₙ* N` can equivalently be viewed as a semigroup homomorphism
`Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms.  -/
MulHom.op : {M : Type u_3} → {N : Type u_4} → [inst : Mul M] → [inst_1 : Mul N] → (M →ₙ* N) ≃ (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ)
-- Mathlib.Algebra.Group.Action.Units
AddUnits.vadd_neg : ∀ {G : Type u_1} {M : Type u_3} [inst : AddGroup G] [inst_1 : AddMonoid M] [inst_2 : AddAction G M]
  [inst_3 : VAddCommClass G M M] [inst_4 : VAddAssocClass G M M] (g : G) (m : AddUnits M), -(g +ᵥ m) = -g +ᵥ -m
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_inf : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S₁ S₂ : Subsemiring Rᵐᵒᵖ), (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
-- Mathlib.Data.Nat.Cast.NeZero
NeZero.natCast_ne : ∀ (n : ℕ) (R : Type u_1) [inst : AddMonoidWithOne R] [h : NeZero ↑n], ↑n ≠ 0
-- Mathlib.RingTheory.Kaehler.Basic
/-- The sequence `B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0` is exact.
Also see `KaehlerDifferential.map_surjective`.  -/
KaehlerDifferential.exact_mapBaseChange_map : ∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B],
  Function.Exact ⇑(KaehlerDifferential.mapBaseChange R A B) ⇑(KaehlerDifferential.map R A B B)
-- Mathlib.AlgebraicGeometry.Artinian
/-- A scheme `X` is locally Artinian if `𝒪ₓ(U)` is Artinian for all affine `U`.  -/
AlgebraicGeometry.IsLocallyArtinian : AlgebraicGeometry.Scheme → Prop
-- Mathlib.Data.Matrix.Mul
/-- Left multiplication by a matrix, as an `AddMonoidHom` from vectors to vectors.  -/
Matrix.mulVec.addMonoidHomLeft : {m : Type u_2} →
  {n : Type u_3} → {α : Type v} → [inst : NonUnitalNonAssocSemiring α] → [Fintype n] → (n → α) → Matrix m n α →+ m → α
-- Mathlib.Tactic.Linter.Whitespace
/-- Scan the two input strings `L` and `M`, assuming `M` is the pretty-printed version of `L`.
This almost means that `L` and `M` only differ in whitespace.

While scanning the two strings, accumulate any discrepancies --- with some heuristics to avoid
flagging some line-breaking changes.
(The pretty-printer does not always produce desirably formatted code.)
 -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.parallelScan : String → String → Array Mathlib.Linter.FormatError✝
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.freeGroupCongr_refl : ∀ {α : Type u}, FreeGroup.freeGroupCongr (Equiv.refl α) = MulEquiv.refl (FreeGroup α)
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.assumption.inj : ∀ {s : Lean.Omega.Constraint} {x : Lean.Omega.Coeffs} {i i_1 : ℕ},
  Lean.Elab.Tactic.Omega.Justification.assumption s x i = Lean.Elab.Tactic.Omega.Justification.assumption s x i_1 →
    i = i_1
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_eq_preAleph : ∀ (o : Ordinal.{u_1}), Cardinal.aleph o = Cardinal.preAleph (Ordinal.omega0 + o)
-- Mathlib.Topology.Semicontinuity.Defs
/-- A function `f : α → Set β` is upper hemicontinuous if, for all `x`, whenever `t` is a
neighborhood of `f x`, then `t` is a neighborhood of `f x'` for all `x'` sufficiently close
to `x`.  -/
UpperHemicontinuous : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [TopologicalSpace β] → (α → Set β) → Prop
-- Mathlib.Topology.Separation.CompletelyRegular
t35Space_iff : ∀ (X : Type u) [inst : TopologicalSpace X], T35Space X ↔ T0Space X ∧ CompletelyRegularSpace X
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Needed to make `affineSpan (s.points '' {i}ᶜ)` nonempty.  -/
Affine.Simplex.instNonemptyElemComplSetSingletonOfNontrivial : ∀ {α : Type u_8} [Nontrivial α] (i : α), Nonempty ↑{i}ᶜ
-- Init.Data.String.Extra
String.Pos.Raw.next'.congr_simp : ∀ (s s_1 : String) (e_s : s = s_1) (p p_1 : String.Pos.Raw) (e_p : p = p_1) (h : ¬String.Pos.Raw.atEnd s p = true),
  String.Pos.Raw.next' s p h = String.Pos.Raw.next' s_1 p_1 ⋯
-- Lean.Elab.DeprecatedSyntax
/-- The syntax node kind that is deprecated.  -/
Lean.Elab.SyntaxDeprecationEntry.kind : Lean.Elab.SyntaxDeprecationEntry → Lean.SyntaxNodeKind
-- Mathlib.Data.Quot
Trunc.instSubsingletonTrunc : ∀ {α : Sort u_1}, Subsingleton (Trunc α)
-- Mathlib.Data.Nat.BinaryRec
Nat.binaryRec_zero : ∀ {motive : ℕ → Sort u} (zero : motive 0) (bit : (b : Bool) → (n : ℕ) → motive n → motive (Nat.bit b n)),
  Nat.binaryRec zero bit 0 = zero
-- Mathlib.SetTheory.Ordinal.Univ
Cardinal.aleph0_lt_univ : Cardinal.aleph0 < Cardinal.univ.{u, v}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
/-- The natural isomorphism `eq(f ×[S] T, g ×[S] T) ≅ eq(f, g) ×[S] T`.  -/
CategoryTheory.Limits.equalizerPullbackMapIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasEqualizers C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        {X Y S T : C} →
          {f g : X ⟶ Y} →
            {s : X ⟶ S} →
              {t : Y ⟶ S} →
                (hf : CategoryTheory.CategoryStruct.comp f t = s) →
                  (hg : CategoryTheory.CategoryStruct.comp g t = s) →
                    (v : T ⟶ S) →
                      CategoryTheory.Limits.equalizer
                          (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
                            (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
                          (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
                            (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) ≅
                        CategoryTheory.Limits.pullback (CategoryTheory.Limits.equalizer.ι f g)
                          (CategoryTheory.Limits.pullback.fst s v)
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
RingEquiv.restrict.congr_simp : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σR : Type u_1} {σS : Type u_2}
  [inst_2 : SetLike σR R] [inst_3 : SetLike σS S] [inst_4 : SubsemiringClass σR R] [inst_5 : SubsemiringClass σS S]
  (e e_1 : R ≃+* S) (e_e : e = e_1) (s' : σR) (s : σS) (h : ∀ (x : R), x ∈ s' ↔ e x ∈ s),
  e.restrict s' s h = e_1.restrict s' s ⋯
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op ⊤)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp hU.fromSpec (CategoryTheory.CategoryStruct.comp X.toSpecΓ h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) h
-- Mathlib.Topology.MetricSpace.DilationEquiv
/-- Composition of `DilationEquiv`s.  -/
DilationEquiv.trans : {X : Type u_1} →
  {Y : Type u_2} →
    {Z : Type u_3} →
      [inst : PseudoEMetricSpace X] →
        [inst_1 : PseudoEMetricSpace Y] → [inst_2 : PseudoEMetricSpace Z] → X ≃ᵈ Y → Y ≃ᵈ Z → X ≃ᵈ Z
-- Mathlib.Tactic.Linter.Whitespace
/-- `mkWindow orig start ctx` extracts from `orig` a string that starts at the first
non-whitespace character before `start`, then expands to cover `ctx` more characters
and continues still until the first non-whitespace character.

In essence, it extracts the substring of `orig` that begins at `start`, continues for `ctx`
characters plus expands left and right until it encounters the first whitespace character,
to avoid cutting into "words".

*Note*. `start` is the number of characters *from the right* where our focus is!
 -/
Mathlib.Linter.Style.Whitespace.mkWindow : String → ℕ → ℕ → String
-- Mathlib.Algebra.Quandle
ShelfHom.ext : ∀ {S₁ : Type u_1} {S₂ : Type u_2} {inst : Shelf S₁} {inst_1 : Shelf S₂} {x y : ShelfHom S₁ S₂},
  x.toFun = y.toFun → x = y
-- Mathlib.Order.GameAdd
Sym2.GameAdd.snd : ∀ {α : Type u_1} {rα : α → α → Prop} {a b₁ b₂ : α}, rα b₁ b₂ → Sym2.GameAdd rα s(a, b₁) s(a, b₂)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_fun_zero : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] (f : α →₀ M),
  (f.sum fun x x_1 => 0) = 0
-- Init.Data.Option.Attach
Option.unattach_eq_none_iff : ∀ {α : Type u_1} {p : α → Prop} {o : Option { x // p x }}, o.unattach = none ↔ o = none
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNatCommRing.sizeOf_spec : ∀ (h : Lean.Expr) (x : Int.Internal.Linear.Var) (e' : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly)
  (re : Lean.Meta.Grind.Arith.CommRing.RingExpr) (rp : Lean.Grind.CommRing.Poly) (p' : Int.Internal.Linear.Poly),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNatCommRing h x e' p re rp p') =
    1 + sizeOf h + sizeOf x + sizeOf e' + sizeOf p + sizeOf re + sizeOf rp + sizeOf p'