mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.instDistribMulActionOfUniformContinuousConstSMul : {α : Type u_3} →
  [inst : UniformSpace α] →
    [inst_1 : AddGroup α] →
      [inst_2 : IsUniformAddGroup α] →
        {M : Type u_5} →
          [inst_3 : Monoid M] →
            [inst_4 : DistribMulAction M α] →
              [UniformContinuousConstSMul M α] → DistribMulAction M (UniformSpace.Completion α)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_neg : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N'), ↑(-g) = -↑g
-- Mathlib.RingTheory.Jacobson.Ring
IsJacobsonRing.mk : ∀ {R : Type u_3} [inst : CommRing R], (∀ (I : Ideal R), I.IsRadical → I.jacobson = I) → IsJacobsonRing R
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
/-- The diagonal of a formally unramified morphism of finite type is an open immersion.  -/
AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.FormallyUnramified f]
  [AlgebraicGeometry.LocallyOfFiniteType f],
  AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.pullback.diagonal f)
-- Std.Internal.Do.WP.Basic
/-- `StateT`'s `WP` interpretation: lift the base interpretation by adding a state argument.  -/
Std.Internal.Do.StateT.wpInst : {m : Type u → Type z} →
  {α : Type u} →
    {EPred : Type v} →
      {σ : Type u} →
        {Pred : Type w} →
          [inst : Std.Internal.Do.Assertion Pred] →
            [inst_1 : Std.Internal.Do.Assertion EPred] →
              [Std.Internal.Do.WP (m (α × σ)) (α × σ) Pred EPred] → Std.Internal.Do.WP (StateT σ m α) α (σ → Pred) EPred
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The Weierstrass `℘` function with the `l₀`-term missing.
This is mainly a tool for calculations where one would want to omit a diverging term.
This has the notation `℘[L - l₀]` in the namespace `PeriodPairs`.  -/
PeriodPair.weierstrassPExcept : PeriodPair → ℂ → ℂ → ℂ
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- For any point, the product of distances to two intersection
points on a line through the point equals the absolute value of the power of the point.  -/
EuclideanGeometry.Sphere.mul_dist_eq_abs_power : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {P : Type u_2} [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p a b : P},
  p ∈ line[ℝ, a, b] → a ∈ s → b ∈ s → dist p a * dist p b = |s.power p|
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_inv' : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b : α} [MulRightStrictMono α],
  a < b⁻¹ ↔ b < a⁻¹
-- Mathlib.NumberTheory.LSeries.Dirichlet
DirichletCharacter.mul_delta : ∀ {n : ℕ} (χ : DirichletCharacter ℂ n), (fun n_1 => χ ↑n_1) * LSeries.delta = LSeries.delta
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.id_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C], CategoryTheory.CategoryStruct.id 0 = 0
-- Init.Data.SInt.Lemmas
Int8.add_right_neg : ∀ (a : Int8), a + -a = 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
PresheafOfModules.forget₂_map_pushforward_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R) {U : Cᵒᵖ} {M N : PresheafOfModules R} (g : M ⟶ N),
  (CategoryTheory.forget₂ (ModuleCat ↑(S.obj U)) Ab).map (((PresheafOfModules.pushforward φ).map g).app U) =
    (CategoryTheory.forget₂ (ModuleCat ↑(R.obj (F.op.obj U))) Ab).map (g.app (F.op.obj U))
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.sub_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Sub α] (A B : Matrix m n α) (i : m) (j : n),
  (A - B) i j = A i j - B i j
-- Lean.ReducibilityAttrs
/-- Set the given declaration as `[irreducible]`  -/
Lean.setIrreducibleAttribute : {m : Type → Type} → [Lean.MonadEnv m] → Lean.Name → m Unit
-- Mathlib.Data.ENNReal.BigOperators
/-- **Alias** of `ENNReal.ofNNReal_finsetSum`. -/
ENNReal.coe_finsetSum : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → NNReal), ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Batteries.Data.String.Lemmas
String.utf8Len_reverse : ∀ (cs : List Char), String.utf8Len cs.reverse = String.utf8Len cs
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- A morphism between source objects `S ⟶ S'`
contravariantly induces a functor between structured arrows,
`StructuredArrow S' T ⥤ StructuredArrow S T`.

Ideally this would be described as a 2-functor from `D`
(promoted to a 2-category with equations as 2-morphisms)
to `Cat`.
 -/
CategoryTheory.StructuredArrow.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S S' : D} →
          {T : CategoryTheory.Functor C D} →
            (S ⟶ S') → CategoryTheory.Functor (CategoryTheory.StructuredArrow S' T) (CategoryTheory.StructuredArrow S T)
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- In the trivial `ChartedSpace` structure of a space modelled over itself through the identity,
the atlas members are just the identity.  -/
chartedSpaceSelf_atlas : ∀ {H : Type u_5} [inst : TopologicalSpace H] {e : OpenPartialHomeomorph H H},
  e ∈ atlas H H ↔ e = OpenPartialHomeomorph.refl H
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.mkAnchorSyntaxFromPrefix : ℕ → UInt64 → Lean.CoreM (Lean.TSyntax `Lean.Parser.Tactic.anchor)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanDeclIdent : Lean.FromJson Lean.Lsp.LeanDeclIdent
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getₘ_eq_getValue : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m) {a : α} {h : m.containsₘ a = true},
  m.getₘ a h = Std.Internal.List.getValueCast a (Std.DHashMap.Internal.toListModel (↑m).buckets) ⋯
-- Lean.Exception
/-- Throw an error exception with the specified name at the position `ref`.

Note: Use the macro `throwNamedErrorAt`, which validates error names, instead of calling this
function directly.
 -/
Lean.throwNamedErrorAt : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadError m] → Lean.Syntax → Lean.Name → Lean.MessageData → m α
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- A vector lies in the `vectorSpan` of two points if and only if it is a multiple of their
difference (reversed).  -/
mem_vectorSpan_pair_rev : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ : P} {v : V}, v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₂ -ᵥ p₁) = v
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.StructuredArrowRightwards.mk_surjective : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {w : CategoryTheory.TwoSquare T L R B} {X₂ : C₂}
  {X₃ : C₃} {g : R.obj X₂ ⟶ B.obj X₃} (f : w.StructuredArrowRightwards g),
  ∃ X₁ a b,
    ∃ (comm :
      CategoryTheory.CategoryStruct.comp (R.map a) (CategoryTheory.CategoryStruct.comp (w.app X₁) (B.map b)) = g),
      f = CategoryTheory.TwoSquare.StructuredArrowRightwards.mk w g X₁ a b comm
-- Init.Data.Nat.Basic
Nat.eq_of_le_of_lt_succ : ∀ {n m : ℕ}, n ≤ m → m < n + 1 → m = n
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.instCompScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.WeaklyEtale f]
  [AlgebraicGeometry.WeaklyEtale g], AlgebraicGeometry.WeaklyEtale (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Ring.Equiv
/-- Produce a ring isomorphism from a bijective ring homomorphism.  -/
RingEquiv.ofBijective : {F : Type u_1} →
  {R : Type u_4} →
    {S : Type u_5} →
      [inst : NonUnitalNonAssocSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring S] →
          [inst_2 : FunLike F R S] → [NonUnitalRingHomClass F R S] → (f : F) → Function.Bijective ⇑f → R ≃+* S
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- A non-quantitative version of Markov inequality for integrable functions: the measure of points
where `‖f x‖ ≥ ε` is finite for all positive `ε`.  -/
MeasureTheory.Integrable.measure_norm_ge_lt_top : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β}, MeasureTheory.Integrable f μ → ∀ {ε : ℝ}, 0 < ε → μ {x | ε ≤ ‖f x‖} < ⊤
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_toList_roc : ∀ {m n : ℤ}, (m<...=n).toList.toArray = (m<...=n).toArray
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The canonical transition map `(Uᵢ ×[Z] Y) ×[X] Uⱼ ⟶ (Uⱼ ×[Z] Y) ×[X] Uᵢ` given by the fact
that pullbacks are associative and symmetric.  -/
AlgebraicGeometry.Scheme.Pullback.t : {X Y Z : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (f : X ⟶ Z) →
      (g : Y ⟶ Z) →
        [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] →
          (i j : 𝒰.I₀) → AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i j ⟶ AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g j i
-- Mathlib.Algebra.Lie.Subalgebra
LieHom.surjective_rangeRestrict : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂), Function.Surjective ⇑f.rangeRestrict
-- Mathlib.RepresentationTheory.Coinduced
/-- `coind φ A` and `coind' φ A` are isomorphic representations, with the underlying
`k`-linear equivalence given by `coindVEquiv`.  -/
Rep.coindIso : {k : Type u} →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] →
            (φ : G →* H) → (A : Rep.{max u w, u, v} k G) → Rep.coind.{u, v, w, max u w} φ A ≅ Rep.coind' φ A
-- Mathlib.Algebra.Category.AlgCat.Limits
/-- The category of R-algebras has all limits.  -/
AlgCat.hasLimitsOfSize : ∀ {R : Type u} [inst : CommRing R] [UnivLE.{v, w}],
  CategoryTheory.Limits.HasLimitsOfSize.{t, v, w, max (w + 1) u} (AlgCat R)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_lt_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → (a⁻¹ < 1 ↔ 1 < a)
-- Lean.Elab.DocString
/-- Adds a builtin documentation code block.

Should be run during initialization.
 -/
Lean.Doc.addBuiltinDocCodeBlock : Lean.Name → Lean.Name → Lean.Doc.DocCodeBlockExpander → IO Unit
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
/-- The **spectral mapping theorem** for the non-unital continuous functional calculus.  -/
cfcₙ_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] (f : R → R) (a : A),
  autoParam (ContinuousOn f (quasispectrum R a)) _auto_251✝ →
    autoParam (f 0 = 0) _auto_253✝ → autoParam (p a) _auto_259✝ → quasispectrum R (cfcₙ f a) = f '' quasispectrum R a
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoalCore.pretty : Lean.Widget.InteractiveGoalCore → Option String → String → Std.Format
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.hom_ext_iff : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : X ⟶ Y}, f = g ↔ f.hom = g.hom
-- Mathlib.FieldTheory.PrimeField
instSubsingletonSubfieldZMod : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], Subsingleton (Subfield (ZMod p))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.homAddMonoidHom_apply : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.AddMonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal] (a : X ⟶ M), F.homAddMonoidHom a = F.map a
-- Mathlib.Data.Set.Lattice
Set.biUnion_univ : ∀ {α : Type u_1} {β : Type u_2} (s : α → Set β), ⋃ x ∈ Set.univ, s x = ⋃ x, s x
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.vadd_cancel : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] {r : X} {s t : ↥S}, (↑s -ₒ t) +ᵥ r -ₒ s = r -ₒ t
-- Batteries.Data.String.Lemmas
String.firstDiffPos_loop_eq : ∀ (l₁ l₂ r₁ r₂ : List Char) (stop p : ℕ),
  p = String.utf8Len l₁ →
    p = String.utf8Len l₂ →
      stop = min (String.utf8Len l₁ + String.utf8Len r₁) (String.utf8Len l₂ + String.utf8Len r₂) →
        String.firstDiffPos.loop (String.ofList (l₁ ++ r₁)) (String.ofList (l₂ ++ r₂)) { byteIdx := stop }
            { byteIdx := p } =
          { byteIdx := p + String.utf8Len (List.takeWhile₂ (fun x1 x2 => decide (x1 = x2)) r₁ r₂).1 }
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertListIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)), Std.Internal.List.insertListIfNew l [] = l
-- Init.Data.UInt.IntToBitVec
USize.ne_iff_toBitVec64_ne : ∀ {a b : USize} (h : System.Platform.numBits = 64), a ≠ b ↔ a.toBitVec64 h ≠ b.toBitVec64 h
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.colimitCocone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat),
  AddGrpCat.FilteredColimits.colimitCocone F =
    { pt := AddGrpCat.FilteredColimits.colimit F,
      ι :=
        {
          app := fun J_1 =>
            AddGrpCat.ofHom
              (AddMonCat.Hom.hom
                ((AddMonCat.FilteredColimits.colimitCocone (F.comp (CategoryTheory.forget₂ AddGrpCat AddMonCat))).ι.app
                  J_1)),
          naturality := ⋯ } }
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Min α] [inst_1 : Min β] [inst_2 : Top α] [inst_3 : Top β]
  (toInfHom : InfHom α β) (map_top' : toInfHom.toFun ⊤ = ⊤) (toInfHom_1 : InfHom α β)
  (map_top'_1 : toInfHom_1.toFun ⊤ = ⊤),
  ({ toInfHom := toInfHom, map_top' := map_top' } = { toInfHom := toInfHom_1, map_top' := map_top'_1 }) =
    (toInfHom = toInfHom_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.map_reflexion_comp_map_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C),
  CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
      (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) =
    CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingReflexivePair.zero)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst toInsert).contains k = false →
    Std.Internal.List.getKeyD k (Std.Internal.List.insertList l toInsert) fallback =
      Std.Internal.List.getKeyD k l fallback
-- Std.Do.PredTrans
Std.Do.PredTrans.apply_throw : ∀ {ps : Std.Do.PostShape} {α ε : Type u} (e : ε) (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)),
  (Std.Do.PredTrans.throw e).apply Q = Q.2.1 e
-- Mathlib.Probability.Independence.Basic
/-- **Alias** of `ProbabilityTheory.iIndepFun.indepFun_finsetSum_of_notMem`. -/
ProbabilityTheory.iIndepFun.indepFun_finset_sum_of_notMem : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : AddCommMonoid β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) → ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.IndepFun (∑ j ∈ s, f j) (f i) μ
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- a morphism between the zeroth lines  -/
CategoryTheory.ShortComplex.SnakeInput.Hom.f₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} → S₁.Hom S₂ → (S₁.L₀ ⟶ S₂.L₀)
-- Mathlib.GroupTheory.Finiteness
QuotientGroup.fg : ∀ {G : Type u_3} [inst : Group G] [Group.FG G] (N : Subgroup G) [inst_2 : N.Normal], Group.FG (G ⧸ N)
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.dSmooth_id : ∀ {X : Type u_1} [inst : DiffeologicalSpace X], Diffeology.DSmooth id
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.normalizerMonoidHom_apply_apply_coe : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (x : ↥(Subgroup.normalizer ↑H)) (a : ↥H),
  ↑((H.normalizerMonoidHom x) a) = ↑x * ↑a * (↑x)⁻¹
-- Init.Data.Int.Order
Int.neg_le_zero_iff : ∀ {a : ℤ}, -a ≤ 0 ↔ 0 ≤ a
-- Mathlib.Data.Set.Sups
Set.sup_mem_sups : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t : Set α} {a b : α}, a ∈ s → b ∈ t → a ⊔ b ∈ s ⊻ t
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.length_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Topology.SmallInductiveDimension
smallInductiveDimension_le_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {n : ℕ}, smallInductiveDimension X ≤ ↑n ↔ HasSmallInductiveDimensionLE X n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.le_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {he : t.isEmpty = false}, (cmp k (t.minKey he)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ},
  ContDiffOn ℝ 1 f (Set.Icc a b) → a ≤ b → ‖f b - f a‖ₑ ≤ ∫⁻ (x : ℝ) in Set.Icc a b, ‖derivWithin f (Set.Icc a b) x‖ₑ
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category `C` is said to have exact limits of shape `J` provided that limits of shape `J`
exist and are exact (in the sense that they preserve finite colimits).
 -/
CategoryTheory.HasExactLimitsOfShape : (J : Type u') →
  [inst : CategoryTheory.Category.{v', u'} J] →
    (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasLimitsOfShape J C] → Prop
-- Aesop.Search.Expansion.Norm
Aesop.normSimpCore : Lean.MVarId → Std.HashSet Lean.MVarId → Aesop.NormM (Option Aesop.NormRuleResult)
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.unopFunctor_map_f : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {X Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ} (f : X ⟶ Y) (i : ι),
  ((HomologicalComplex.unopFunctor V c).map f).f i = (f.unop.f i).unop
-- Mathlib.RingTheory.DividedPowers.Padic
_private.Mathlib.RingTheory.DividedPowers.Padic.0.PadicInt.dpow'_mem : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {n : ℕ} {x : ℤ_[p]},
  n ≠ 0 → ∀ (hx : x ∈ Ideal.span {↑p}), ⟨PadicInt.dpow'✝ p n ↑x, ⋯⟩ ∈ Ideal.span {↑p}
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
_private.Mathlib.MeasureTheory.Function.SimpleFuncDense.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_le : ∀ {G : Type u_1} [inst : AddGroup G] {H₁ H₂ H₃ : AddSubgroup G}, ⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ H₃
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.pair_iffₛ : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x y : M},
  LinearIndependent R ![x, y] ↔ ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'
-- Init.Data.Array.Basic
/-- Returns the first non-`none` result of applying the function `f` to each element of the
array, in order. Panics if `f` returns `none` for all elements.

Example:
```lean example
#eval #[7, 6, 5, 8, 1, 2, 6].findSome? fun i =>
  if i < 5 then
    some (i * 10)
  else
    none
```
```output
some 10
```
 -/
Array.findSome! : {α : Type u} → {β : Type v} → [Inhabited β] → (α → Option β) → Array α → β
-- Mathlib.Order.Sublocale
/-- A sublocale is closed under heyting implication.

Do NOT use directly. Use `Sublocale.himp_mem` instead.  -/
Sublocale.himp_mem' : ∀ {X : Type u_2} [inst : Order.Frame X] (self : Sublocale X) (a b : X), b ∈ self.carrier → a ⇨ b ∈ self.carrier
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_add_mul_self : ∀ {a b c : ℤ}, a ∣ b + c * a ↔ a ∣ b
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.instContinuousSMul : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [inst_8 : ContinuousSMul 𝕜 F], ContinuousSMul 𝕜 (ContinuousMultilinearMap 𝕜 E F)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.instInhabitedStrictUniversalPropertyFixedTargetLocalizationQ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (E : Type u_3) →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} E] →
          Inhabited (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget W.Q W E)
-- Mathlib.Algebra.Opposites
AddOpposite.instInvolutiveNeg.eq_1 : ∀ {α : Type u_1} [inst : InvolutiveNeg α],
  AddOpposite.instInvolutiveNeg = { toNeg := AddOpposite.instNeg, neg_neg := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
/-- The (unique) element in `SMulCandidate α φ r m`.  -/
PresheafOfModules.Sheafify.smulCandidate : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [CategoryTheory.Presheaf.IsLocallySurjective J α] →
                {M₀ : PresheafOfModules R₀} →
                  {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                    (φ : M₀.presheaf ⟶ A.obj) →
                      [CategoryTheory.Presheaf.IsLocallyInjective J φ] →
                        [CategoryTheory.Presheaf.IsLocallySurjective J φ] →
                          {X : Cᵒᵖ} →
                            (r : ↑(R.obj.obj X)) →
                              (m : ↑(A.obj.obj X)) → PresheafOfModules.Sheafify.SMulCandidate α φ r m