mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.mem_list_cycles_iff : ∀ {α : Type u_4} [Finite α] {l : List (Equiv.Perm α)},
  (∀ σ ∈ l, σ.IsCycle) →
    List.Pairwise Equiv.Perm.Disjoint l → ∀ {σ : Equiv.Perm α}, σ ∈ l ↔ σ.IsCycle ∧ ∀ (a : α), σ a ≠ a → σ a = l.prod a
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_unitIso_hom_app_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) (X : CategoryTheory.Core C), (E.core.unitIso.hom.app X).iso.inv = E.unitIso.inv.app X.of
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuous.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {z : Set β},
  UpperHemicontinuous fun _x => z
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_div_summable_of_mem_ball : ∀ (𝕂 : Type u_1) {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedDivisionRing 𝔸]
  [inst_2 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸],
  ∀ x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius, Summable fun n => x ^ n / ↑n.factorial
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, `H₀(G, A)` is isomorphic
to the cokernel of `ρ(g) - Id(A)`.  -/
Rep.FiniteCyclicGroup.groupHomologyIso₀ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : CommGroup G] →
      [Fintype G] →
        (A : Rep.{u, u, u} k G) →
          (g : G) →
            (∀ (x : G), x ∈ Subgroup.zpowers g) →
              (groupHomology A 0 ≅
                ModuleCat.of k (↑A ⧸ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range))
-- Init.Data.BitVec.Basic
/-- Notation for bitvector literals without truncation. `i#'lt` is a shorthand for `BitVec.ofNatLT i lt`.  -/
BitVec.«term__#'__» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Set.subtype_vadd_set : ∀ {S : Type u_7} {α : Type u_8} {β : Type u_9} [inst : VAdd α β] [inst_1 : SetLike S α] {s : S} (x : ↥s) (t : Set β),
  x +ᵥ t = ↑x +ᵥ t
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.instBot : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] → {𝒜 : ι → σ} → [inst_5 : GradedRing 𝒜] → Bot (HomogeneousIdeal 𝒜)
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.handleCompletion : Lean.Lsp.CompletionParams → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.ResolvableCompletionList)
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.isEagerCasesCandidate : Lean.Expr → Lean.Meta.Grind.GrindM Bool
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.ShortExact.isIso_f_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C},
  S.ShortExact → ∀ [CategoryTheory.Balanced C], CategoryTheory.IsIso S.f ↔ CategoryTheory.Limits.IsZero S.X₃
-- Mathlib.Tactic.CategoryTheory.CategoryStar
/-- Insert `newLevel` immediately after the elements of `levelNames` which are in `us`, or at the
front of the list (as the most recent level) if there are no such elements.
 -/
_private.Mathlib.Tactic.CategoryTheory.CategoryStar.0.Mathlib.Tactic.CategoryStar.insertAfterLevels : Array Lean.Name → List Lean.Name → Lean.Name → List Lean.Name
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment.eq_1 : ∀ (b : Bool) (a : Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b a =
    if b = true then a.hasPosAssignment else a.hasNegAssignment
-- Mathlib.Order.Filter.NAry
Filter.map₂.eq_1 : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (m : α → β → γ) (f : Filter α) (g : Filter β),
  Filter.map₂ m f g = (Filter.map (Function.uncurry m) (f ×ˢ g)).copy {s | ∃ u ∈ f, ∃ v ∈ g, Set.image2 m u v ⊆ s} ⋯
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- The map part of the functor `LightCondSet ⥤ TopCat`  -/
LightCondSet.toTopCatMap : {X Y : LightCondSet} → (X ⟶ Y) → (X.toTopCat ⟶ Y.toTopCat)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.instCoeSortType : CoeSort AlgebraicGeometry.Scheme (Type u_1)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_def_of_nonpos : ∀ {x : ℝ},
  x ≤ 0 →
    ∀ (y : ℝ), x ^ y = if x = 0 then if y = 0 then 1 else 0 else Real.exp (Real.log x * y) * Real.cos (y * Real.pi)
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_nnnorm_one : ∀ {n : Type u_4} {α : Type u_5} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : SeminormedAddCommGroup α]
  [inst_3 : One α], ‖1‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- Implementation; see `nonempty_indParallelPairPresentation`.  -/
CategoryTheory.NonemptyParallelPairPresentationAux.F₁ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      (f g : A ⟶ B) →
        (P₁ : CategoryTheory.Limits.IndObjectPresentation A) →
          (P₂ : CategoryTheory.Limits.IndObjectPresentation B) →
            CategoryTheory.Functor (CategoryTheory.NonemptyParallelPairPresentationAux.K f g P₁ P₂) C
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.mulL : ℤ → Int.Internal.Linear.Expr → Int.Internal.Linear.Expr
-- Mathlib.RepresentationTheory.Character
/-- If `V` and `W` are finite-dimensional representations of a finite group, then the
scalar product of their characters is equal to the dimension of the space of
equivariant maps from `V` to `W`.
 -/
FDRep.scalar_product_char_eq_finrank_equivariant : ∀ {k : Type u} [inst : Field k] {G : Type v} [inst_1 : Group G] [inst_2 : Fintype G] [Invertible ↑(Nat.card G)]
  (V W : FDRep k G), (↑(Nat.card G))⁻¹ * ∑ g, W.character g * V.character g⁻¹ = ↑(Module.finrank k (V ⟶ W))
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_mul_eq_right : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] {f g : α → M},
  Disjoint (Function.mulSupport f) (Function.mulSupport g) → (Function.mulSupport g).mulIndicator (f * g) = g
-- Mathlib.Order.KrullDimension
Order.krullDim_of_noMinOrder : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] [NoMinOrder α], Order.krullDim α = ⊤
-- Mathlib.LinearAlgebra.Matrix.Kronecker
/-- `Matrix.kroneckerMapBilinear` commutes with `*` if `f` does.

This is primarily used with `R = ℕ` to prove `Matrix.mul_kronecker_mul`.  -/
Matrix.kroneckerMapBilinear_mul_mul : ∀ {R : Type u_1} {S : Type u_2} {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10}
  {n : Type u_11} {l' : Type u_15} {m' : Type u_16} {n' : Type u_17} [inst : Semiring S] [inst_1 : Semiring R]
  [inst_2 : Fintype m] [inst_3 : Fintype m'] [inst_4 : NonUnitalNonAssocSemiring α]
  [inst_5 : NonUnitalNonAssocSemiring β] [inst_6 : NonUnitalNonAssocSemiring γ] [inst_7 : Module R α]
  [inst_8 : Module R γ] [inst_9 : Module S β] [inst_10 : Module S γ] [inst_11 : SMulCommClass S R γ]
  (f : α →ₗ[R] β →ₗ[S] γ),
  (∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b') →
    ∀ (A : Matrix l m α) (B : Matrix m n α) (A' : Matrix l' m' β) (B' : Matrix m' n' β),
      ((Matrix.kroneckerMapBilinear f) (A * B)) (A' * B') =
        ((Matrix.kroneckerMapBilinear f) A) A' * ((Matrix.kroneckerMapBilinear f) B) B'
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_filter_containsKey_eq_length_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ →
    (∀ (a : α), Std.Internal.List.containsKey a l₁ = true → Std.Internal.List.containsKey a l₂ = true) →
      (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁).length = l₁.length
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] [inst_2 : Inhabited α] (h : t.WF) {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)).getKey! k = t.getKey! k
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- The map from the source to the image of a morphism.  -/
CategoryTheory.Limits.factorThruImage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (f : X ⟶ Y) → [inst_1 : CategoryTheory.Limits.HasImage f] → X ⟶ CategoryTheory.Limits.image f
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Valuation.apply_posSubmonoid_pos : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_2} [inst_2 : LinearOrderedCommMonoidWithZero Γ₀]
  (v : Valuation R Γ₀) [v.Compatible] (x : ↥(ValuativeRel.posSubmonoid R)), 0 < v ↑x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.Hom.isMonHom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Mon C} (self : M.Hom N), CategoryTheory.IsMonHom self.hom
-- Init.Data.UInt.Bitwise
UInt32.toUSize_not : ∀ (a : UInt32), (~~~a).toUSize = ~~~a.toUSize % 4294967296
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalStarSubalgebra.nonUnitalCStarAlgebra : {S : Type u_1} →
  {A : Type u_2} →
    [inst : NonUnitalCStarAlgebra A] →
      [inst_1 : SetLike S A] →
        [NonUnitalSubringClass S A] →
          [SMulMemClass S ℂ A] → [StarMemClass S A] → (s : S) → [h_closed : IsClosed ↑s] → NonUnitalCStarAlgebra ↥s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false} {fallback : α}, t.getKeyD (t.minKey he) fallback = t.minKey he
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.pointwise_isCentralScalar : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α G]
  [inst_3 : MulDistribMulAction αᵐᵒᵖ G] [IsCentralScalar α G], IsCentralScalar α (Subgroup G)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.rid_symm_apply : ∀ (R : Type uR) (S : Type uS) {A : Type uA} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] (a : A),
  (Algebra.TensorProduct.rid R S A).symm a = a ⊗ₜ[R] 1
-- Mathlib.RingTheory.RootsOfUnity.Complex
Complex.isPrimitiveRoot_I : IsPrimitiveRoot Complex.I 4
-- Init.Data.Int.Order
Int.add_lt_of_lt_sub_right : ∀ {a b c : ℤ}, a < c - b → a + b < c
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.dynEntourage_monotone : ∀ {X : Type u_1} (T : X → X) (n : ℕ), Monotone fun U => Dynamics.dynEntourage T U n
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.pullbackSpecIso'.eq_1 : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  AlgebraicGeometry.pullbackSpecIso' R S T =
    AlgebraicGeometry.pullbackSpecIso ↑(CommRingCat.of R) ↑(CommRingCat.of S) ↑(CommRingCat.of T)
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingField.instField : {K : Type v} → [inst : Field K] → (f : Polynomial K) → Field f.SplittingField
-- Mathlib.CategoryTheory.Action.Monoidal
Action.rightUnitor_hom_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] (X : Action V G),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.V).hom
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- Every `SlashInvariantForm` `f` satisfies ` f (γ • z) = (denom γ z) ^ k * f z`.  -/
SlashInvariantForm.slash_action_eqn_SL'' : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
  [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F)
  {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ},
  γ ∈ Γ →
    ∀ (z : UpperHalfPlane),
      f (γ • z) =
        UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))
              ↑z ^
            k *
          f z
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projection`.

---

The linear projection onto a subspace along its complement
as a map from the full space to itself, as opposed to `Submodule.projectionOnto`,
which maps into the subtype.
This version is important as it satisfies `IsIdempotentElem`.

See also:
* `Submodule.projectionOntoL` and `Submodule.projectionL` for the continuous versions.
* `Submodule.orthogonalProjection` and `Submodule.orthogonalProjectionOnto` for the projections
  along the orthogonal subspace.  -/
Submodule.IsCompl.projection : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} → [inst_1 : AddCommGroup E] → [inst_2 : Module R E] → (p q : Submodule R E) → IsCompl p q → E →ₗ[R] E
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJNe0Or1728_j : ∀ {R : Type u_1} [inst : CommRing R] (j : R) [inst_1 : Fact (IsUnit j)] [inst_2 : Fact (IsUnit (j - 1728))],
  (WeierstrassCurve.ofJNe0Or1728 j).j = j
-- Mathlib.RepresentationTheory.Character
/-- The character of a representation is constant on conjugacy classes.  -/
FDRep.char_conj : ∀ {k : Type u} [inst : Field k] {G : Type v} [inst_1 : Group G] (V : FDRep k G) (g h : G),
  V.character (h * g * h⁻¹) = V.character g
-- Mathlib.Data.Setoid.Partition
/-- A family of bijective functions with pairwise disjoint
domains and pairwise disjoint ranges can be glued together
to form a bijective function.  -/
IndexedPartition.piecewise_bij : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {β : Type u_3} {f : ι → α → β} {t : ι → Set β}
  (ht : IndexedPartition t), (∀ (i : ι), Set.BijOn (f i) (s i) (t i)) → Function.Bijective (hs.piecewise f)
-- Lean.Util.Path
Lean.addSearchPathFromEnv : Lean.SearchPath → IO Lean.SearchPath
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Walk.isPath_of_length_eq_dist : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.length = G.dist u v → p.IsPath
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.pullbackObjIso_inv_comp_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D)
  {Z : C} (h : G.obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackObjIso f g d).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pullback.snd f g).app d) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (f.app d) (g.app d)) h
-- Mathlib.Topology.Bornology.Constructions
instBoundedSpaceProd : ∀ {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst_1 : Bornology β] [BoundedSpace α] [BoundedSpace β],
  BoundedSpace (α × β)
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodAssoc_symm_apply_inr_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddMonoid P]
  (x : N),
  (AddEquiv.coprodAssoc M N P).symm (AddMonoid.Coprod.inr (AddMonoid.Coprod.inl x)) =
    AddMonoid.Coprod.inl (AddMonoid.Coprod.inr x)
-- Mathlib.Tactic.Linter.Header
/-- Check the `Syntax` `imports` for broad imports:
`Mathlib.Tactic`, any import starting with `Lake`, or `Mathlib.Tactic.{Have,Replace}`.  -/
_private.Mathlib.Tactic.Linter.Header.0.Mathlib.Linter.Style.header.broadImportsCheck : Array Lean.Syntax → Lean.Name → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsExtrFilter.hasLineDerivAt_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {a b : E} {f' : ℝ} {l : Filter E},
  IsExtrFilter f l a → HasLineDerivAt ℝ f f' a b → Filter.Tendsto (fun t => a + t • b) (nhds 0) l → f' = 0
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.continuous_coordChange : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e₁ e₂ : Bundle.Trivialization F proj) {b : B},
  b ∈ e₁.baseSet → b ∈ e₂.baseSet → Continuous (e₁.coordChange e₂ b)
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.union_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s ∪ ∅ = s
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.Supports.eq_8 : ∀ (S : Finset Turing.PartrecToTM2.Λ') (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.Λ'.ret k) = (Turing.PartrecToTM2.contSupp k ⊆ S)
-- Mathlib.SetTheory.Cardinal.Free
instCountableFreeAbelianGroup : ∀ (α : Type u) [Countable α], Countable (FreeAbelianGroup α)
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- The limit in measure is ae unique.  -/
MeasureTheory.tendstoInMeasure_ae_unique : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : EMetricSpace E] {g h : α → E} {f : ι → α → E} {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated],
  MeasureTheory.TendstoInMeasure μ f u g → MeasureTheory.TendstoInMeasure μ f u h → g =ᵐ[μ] h
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.length_filterMap_eq_length_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] {f : α → β → Option γ} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ((List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l).length = l.length ↔
      ∀ (a : α) (h : Std.Internal.List.containsKey a l = true),
        (f (Std.Internal.List.getKey a l h) (Std.Internal.List.getValue a l h)).isSome = true)
-- Mathlib.Tactic.Ring.RingNF
/-- `ring1` solves the goal when it is an equality in *commutative* (semi)rings,
allowing variables in the exponent.

This version of `ring` fails if the target is not an equality.

* `ring1!` uses a more aggressive reducibility setting to determine equality of atoms.


Extensions:

 * * `ring1_nf` additionally uses `ring_nf` to simplify in atoms.
   * `ring1_nf!` will use a more aggressive reducibility setting
     to determine equality of atoms. -/
Mathlib.Tactic.RingNF.ring1NF : Lean.ParserDescr
-- Mathlib.FieldTheory.AlgebraicClosure
/-- The algebraic closure of `F` in `E` is the integral closure of `F` in `E`.  -/
algebraicClosure.isIntegralClosure : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  IsIntegralClosure (↥(algebraicClosure F E)) F E
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- Change-of-variables formula for `Ioi` integrals of vector-valued functions, proved by taking
limits from the result for finite intervals.  -/
MeasureTheory.integral_deriv_smul_comp_Ioi : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E} {a : ℝ},
  ContinuousOn f (Set.Ici a) →
    Filter.Tendsto f Filter.atTop Filter.atTop →
      (∀ x ∈ Set.Ioi a, HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
        ContinuousOn g (f '' Set.Ioi a) →
          MeasureTheory.IntegrableOn g (f '' Set.Ici a) MeasureTheory.volume →
            MeasureTheory.IntegrableOn (fun x => f' x • (g ∘ f) x) (Set.Ici a) MeasureTheory.volume →
              ∫ (x : ℝ) in Set.Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Set.Ioi (f a), g u
-- Mathlib.CategoryTheory.IsoCat
/-- The inverse isomorphism of categories, obtained by swapping `functor` and `inverse`.  -/
CategoryTheory.IsoCat.symm : {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.IsoCat C D → CategoryTheory.IsoCat D C
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.image_inter_image_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (U V : Set α),
  Quotient.mk' '' U ∩ Quotient.mk' '' V = ∅ ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V
-- Mathlib.Analysis.CStarAlgebra.Classes
instCStarAlgebraProd : {A : Type u_1} → {B : Type u_2} → [CStarAlgebra A] → [CStarAlgebra B] → CStarAlgebra (A × B)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.mem_top : ∀ {M : Type u_1} [inst : MulOneClass M] {x : M}, x ∈ ⊤
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.comp_apply : ∀ {A B C : ProfiniteGrp.{u}} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A.toProfinite.toTop),
  (ProfiniteGrp.Hom.hom (CategoryTheory.CategoryStruct.comp f g)) a =
    (ProfiniteGrp.Hom.hom g) ((ProfiniteGrp.Hom.hom f) a)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_filter_key_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → Bool},
  (Std.DHashMap.filter (fun k x => f k) m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) = true
-- Mathlib.Data.ZMod.Basic
ZMod.eq_one_of_isUnit_natCast : ∀ {n : ℕ}, IsUnit ↑n → n = 1
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
/-- The map from the C⋆-algebra to the GNS space, as a linear equivalence.  -/
PositiveLinearMap.toPreGNS : {A : Type u_1} → [inst : NonUnitalCStarAlgebra A] → [inst_1 : PartialOrder A] → (f : A →ₚ[ℂ] ℂ) → A ≃ₗ[ℂ] f.PreGNS
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.essImage_Spec : ∀ {X : AlgebraicGeometry.Scheme}, AlgebraicGeometry.Scheme.Spec.essImage X ↔ AlgebraicGeometry.IsAffine X
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.ClosureState.mk : Array Lean.LocalDecl →
  Array Lean.LocalDecl → Array Lean.LocalDecl → Array Lean.Expr → Lean.Elab.Term.MutualClosure.ClosureState
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.TriangleMorphism.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} (hom₁ : T₁.obj₁ ⟶ T₂.obj₁) (hom₂ : T₁.obj₂ ⟶ T₂.obj₂)
  (hom₃ : T₁.obj₃ ⟶ T₂.obj₃)
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp T₁.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ T₂.mor₁)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₁._autoParam)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp T₁.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ T₂.mor₂)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₂._autoParam)
  (comm₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) =
        CategoryTheory.CategoryStruct.comp hom₃ T₂.mor₃)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₃._autoParam)
  (hom₁_1 : T₁.obj₁ ⟶ T₂.obj₁) (hom₂_1 : T₁.obj₂ ⟶ T₂.obj₂) (hom₃_1 : T₁.obj₃ ⟶ T₂.obj₃)
  (comm₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp T₁.mor₁ hom₂_1 = CategoryTheory.CategoryStruct.comp hom₁_1 T₂.mor₁)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₁._autoParam)
  (comm₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp T₁.mor₂ hom₃_1 = CategoryTheory.CategoryStruct.comp hom₂_1 T₂.mor₂)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₂._autoParam)
  (comm₃_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁_1) =
        CategoryTheory.CategoryStruct.comp hom₃_1 T₂.mor₃)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₃._autoParam),
  ({ hom₁ := hom₁, hom₂ := hom₂, hom₃ := hom₃, comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃ } =
      { hom₁ := hom₁_1, hom₂ := hom₂_1, hom₃ := hom₃_1, comm₁ := comm₁_1, comm₂ := comm₂_1, comm₃ := comm₃_1 }) =
    (hom₁ = hom₁_1 ∧ hom₂ = hom₂_1 ∧ hom₃ = hom₃_1)
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- A version of `Set.mem_finsetSum` with a simpler RHS for sums over a Fintype.  -/
Set.mem_fintype_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Fintype ι] (f : ι → Set α) (a : α),
  a ∈ ∑ i, f i ↔ ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), ∑ i, g i = a