mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.mul_entry_mul_eq_inner_toCLM : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A]
  [inst_2 : PartialOrder A] [inst_3 : StarOrderedRing A] [inst_4 : Fintype n] [inst_5 : DecidableEq m]
  [inst_6 : DecidableEq n] {M : CStarMatrix m n A} {i : m} {j : n} (a b : A),
  a * M i j * star b =
    inner A ((WithCStarModule.equiv A (n → A)).symm (Pi.single j b))
      ((CStarMatrix.toCLM M) ((WithCStarModule.equiv A (m → A)).symm (Pi.single i a)))
-- Init.Data.Array.MapIdx
Array.getElem_zipIdx : ∀ {α : Type u_1} {xs : Array α} {k i : ℕ} (h : i < (xs.zipIdx k).size), (xs.zipIdx k)[i] = (xs[i], k + i)
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.integral_integral_add' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E] ⦃f g : β × γ → E⦄,
  MeasureTheory.Integrable f ((κ.compProd η) a) →
    MeasureTheory.Integrable g ((κ.compProd η) a) →
      ∫ (x : β), ∫ (y : γ), (f + g) (x, y) ∂η (a, x) ∂κ a =
        ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a + ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.unionProd.image_β_inv : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex), (S.unionProd T).image (β_ Y X).inv = T.unionProd S
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.mem_gammaSet_one : ∀ (v : Fin 2 → ℤ), v ∈ EisensteinSeries.gammaSet 1 1 0 ↔ IsCoprime (v 0) (v 1)
-- Lean.Elab.Open
/-- Uniquely resolves the identifier `idStx` in the provided namespaces `nss`.

If the identifier does not indicate a name in exactly one of the namespaces, an exception is thrown.
 -/
Lean.Elab.OpenDecl.resolveNameUsingNamespacesCore : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [MonadExceptOf Lean.Exception m] →
        [Lean.MonadRef m] →
          [Lean.AddErrorMessageContext m] →
            [Lean.AddMessageContext m] →
              [Lean.MonadLog m] →
                [Lean.MonadOptions m] → [Lean.MonadResolveName m] → List Lean.Name → Lean.Syntax → m Lean.Name
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.add_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂), (φ + φ').τ₂ = φ.τ₂ + φ'.τ₂
-- Init.Data.UInt.Bitwise
UInt8.or_zero : ∀ {a : UInt8}, a ||| 0 = a
-- Mathlib.Topology.Sheaves.Presheaf
/-- If `f : X ⟶ Y`, this is the isomorphism between the pullback functor by `f` and the
"naive" pullback given by composing presheaves with the functor `(Open X)ᵒᵖ ⥤ (Open Y)ᵒᵖ`
induced by `f`.
 -/
IsOpenMap.pullbackIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} →
        {f : X ⟶ Y} →
          (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) →
            TopCat.Presheaf.pullback C f ≅
              (CategoryTheory.Functor.whiskeringLeft (TopologicalSpace.Opens ↑X)ᵒᵖ (TopologicalSpace.Opens ↑Y)ᵒᵖ C).obj
                hf.functor.op
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.instGroup : {ι : Type u_1} → (G : ι → Type u_4) → [inst : (i : ι) → Group (G i)] → Group (Monoid.CoprodI G)
-- Mathlib.Algebra.Category.Grp.AB
instAB5AddCommGrpCat : CategoryTheory.AB5 AddCommGrpCat
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.instAddActionElemFinset.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {n : ℕ} [inst_2 : DecidableEq α],
  Set.powersetCard.instAddActionElemFinset G =
    { vadd := Set.powersetCard.instAddActionElemFinset._aux_1 G, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaGrp_map_app_shrinkYonedaObjObjEquiv_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] {M M' : CategoryTheory.Grp C} {Y : Cᵒᵖ}
  (f : Opposite.unop Y ⟶ M.X) (g : M ⟶ M'),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaGrp.{w, v, u}.map g).app Y))
      (CategoryTheory.shrinkYonedaGrpObjObjEquiv.symm f) =
    CategoryTheory.shrinkYonedaGrpObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp f g.hom.hom)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDeriv_const_smul_apply : ∀ {𝕜 : 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] {f : E → F}
  {x : E} {R : Type u_3} [inst_5 : DistribSMul R F] [inst_6 : SMulCommClass 𝕜 R F] [inst_7 : ContinuousConstSMul R F]
  {i : ℕ} {a : R}, ContDiffAt 𝕜 (↑i) f x → iteratedFDeriv 𝕜 i (a • f) x = a • iteratedFDeriv 𝕜 i f x
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.one_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (a : R), Nat.rawCast 1 * a = a
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_ssubset_Ioi_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi b ⊂ Set.Ioi a ↔ a < b
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_mono_set' : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Preorder M] [CanonicallyOrderedMul M] (f : ι → M),
  Monotone fun s => ∏ x ∈ s, f x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_eq : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  ↑NumberField.mixedEmbedding.fundamentalCone.expMap
      ((NumberField.mixedEmbedding.fundamentalCone.completeBasis K) NumberField.Units.dirichletUnitTheorem.w₀) =
    fun x => Real.exp 1
-- Mathlib.Data.Rat.Cast.Defs
NNRat.cast_divNat_of_ne_zero : ∀ {α : Type u_3} [inst : DivisionSemiring α] (a : ℕ) {b : ℕ}, ↑b ≠ 0 → ↑(NNRat.divNat a b) = ↑a / ↑b
-- Init.Data.Nat.Lemmas
Nat.add_left_cancel_iff : ∀ {m k n : ℕ}, n + m = n + k ↔ m = k
-- Mathlib.Order.Closure
ClosureOperator.ext : ∀ {α : Type u_1} [inst : Preorder α] (c₁ c₂ : ClosureOperator α), (∀ (x : α), c₁ x = c₂ x) → c₁ = c₂
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.toRatCDF.eq_1 : ∀ {α : Type u_1} (f : α → ℚ → ℝ) (a : α),
  ProbabilityTheory.toRatCDF f a =
    if ProbabilityTheory.IsRatStieltjesPoint f a then f a else ProbabilityTheory.defaultRatCDF
-- Mathlib.Geometry.Manifold.Immersion
/-- Given an immersion `f` at `x`, this is a choice of complement which lives in the same universe
as the model space for the co-domain of `f`: this is useful to avoid universe restrictions.  -/
Manifold.IsImmersionAtOfComplement.smallComplement : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        {F : Type u_5} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup E''] →
                [inst_4 : NormedSpace 𝕜 E''] →
                  [inst_5 : NormedAddCommGroup F] →
                    [inst_6 : NormedSpace 𝕜 F] →
                      {H : Type u_7} →
                        [inst_7 : TopologicalSpace H] →
                          {G : Type u_9} →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    [inst_9 : TopologicalSpace M] →
                                      [inst_10 : ChartedSpace H M] →
                                        {N : Type u_13} →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} → Manifold.IsImmersionAtOfComplement F I J n f x → Type u
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.glueMorphisms.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.Scheme} (f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y)
  (hf :
    ∀ (x y : 𝒰.I₀),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (f x) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) (f y)),
  AlgebraicGeometry.Scheme.Cover.glueMorphisms 𝒰 f hf =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (AlgebraicGeometry.Scheme.Cover.ulift 𝒰).fromGlued)
      (CategoryTheory.Limits.Multicoequalizer.desc (AlgebraicGeometry.Scheme.Cover.ulift 𝒰).gluedCover.diagram Y
        (fun i => f (AlgebraicGeometry.Scheme.Cover.idx 𝒰 i)) ⋯)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.smul_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {S : Type u_6} [inst_10 : Monoid S]
  [inst_11 : DistribMulAction S W] [inst_12 : SMulCommClass R S W] [inst_13 : ContinuousConstSMul S W]
  [inst_14 : LinearMap.CompatibleSMul W W S R] (s : S) (f : ContIntertwiningMap π₁ π₂) (v : V), (s • f) v = s • f v
-- Mathlib.Topology.Order
induced_compose : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {tγ : TopologicalSpace γ} {f : α → β} {g : β → γ},
  TopologicalSpace.induced f (TopologicalSpace.induced g tγ) = TopologicalSpace.induced (g ∘ f) tγ
-- Mathlib.Algebra.Order.Floor.Ring
Int.map_fract : ∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : Ring S]
  [inst_3 : LinearOrder S] [inst_4 : FloorRing R] [inst_5 : FloorRing S] [inst_6 : FunLike F R S] [RingHomClass F R S]
  (f : F), StrictMono ⇑f → ∀ (a : R), Int.fract (f a) = f (Int.fract a)
-- Mathlib.Topology.Category.TopCat.ULift
TopCat.instPreservesColimitsOfSizeUliftFunctor : CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} TopCat.uliftFunctor
-- Mathlib.RingTheory.DedekindDomain.SInteger
Set.integer.congr_simp : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (S S_1 : Set (IsDedekindDomain.HeightOneSpectrum R)),
  S = S_1 →
    ∀ (K : Type v) [inst_2 : Field K] [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K], S.integer K = S_1.integer K
-- Init.Data.SInt.Lemmas
Int16.toISize_le : ∀ {a b : Int16}, a.toISize ≤ b.toISize ↔ a ≤ b
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.instMonoidalCategoryStruct : (R : Type u) → [inst : CommRing R] → CategoryTheory.MonoidalCategoryStruct (CoalgCat R)
-- Mathlib.Data.List.Sigma
_private.Mathlib.Data.List.Sigma.0.List.kunion.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : List (Sigma β) → List (Sigma β) → Sort u_3) →
      (x x_1 : List (Sigma β)) →
        ((l₂ : List (Sigma β)) → motive [] l₂) →
          ((s : Sigma β) → (l₁ : List (Sigma β)) → (l₂ : List (Sigma β)) → motive (s :: l₁) l₂) → motive x x_1
-- Init.Data.String.Lemmas.Splits
String.sliceTo_append_sliceFrom : ∀ {s : String} {pos : s.Pos}, (s.sliceTo pos).copy ++ (s.sliceFrom pos).copy = s
-- Mathlib.GroupTheory.PushoutI
/-- The map from the base monoid into the pushout  -/
Monoid.PushoutI.base : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Monoid (G i)] → [inst_1 : Monoid H] → (φ : (i : ι) → H →* G i) → H →* Monoid.PushoutI φ
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.equiv_unitIso_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (X : CategoryTheory.MonoidalCategory.DayFunctor C V),
  (CategoryTheory.MonoidalCategory.DayFunctor.equiv C V).unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
-- Lean.Elab.Tactic.Grind.Basic
/-- An extra theorem passed to `simp` in `sym =>` mode.  -/
Lean.Elab.Tactic.Grind.ExtraTheorem : Type
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_of_mem_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → Option (γ a)} {k : α},
  k ∈ Std.ExtDHashMap.filterMap f m → k ∈ m
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGet?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, t₁.Equiv t₂ → Std.DTreeMap.Const.get? t₁ k = Std.DTreeMap.Const.get? t₂ k
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.mk : {R : Type u_1} → [inst : CommSemiring R] → (asIdeal : Ideal R) → asIdeal.IsPrime → PrimeSpectrum R
-- Mathlib.Topology.Compactness.Compact
/-- The preimage of a compact set under a closed embedding is a compact set.  -/
Topology.IsClosedEmbedding.isCompact_preimage : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → ∀ {K : Set Y}, IsCompact K → IsCompact (f ⁻¹' K)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.beq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.DTreeMap.Raw α β cmp} [inst : (k : α) → BEq (β k)]
  [inst_1 : Std.LawfulEqCmp cmp] [Std.TransCmp cmp] [∀ (k : α), ReflBEq (β k)],
  m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.beq m₂ = true
-- Mathlib.Data.EReal.Basic
EReal.top_ne_coe : ∀ (x : ℝ), ⊤ ≠ ↑x
-- Mathlib.SetTheory.Lists
/-- Converts a proper ZFA prelist to a ZFA list.  -/
Lists.of' : {α : Type u_1} → Lists' α true → Lists α
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
MeasurableSet.image_of_monotoneOn_of_continuousOn : ∀ {α : Type u_6} {β : Type u_7} {t : Set α} {g : α → β} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
  [BorelSpace α] [inst_3 : LinearOrder α] [OrderTopology α] [PolishSpace α] [inst_6 : TopologicalSpace β]
  [inst_7 : MeasurableSpace β] [BorelSpace β] [inst_9 : LinearOrder β] [OrderTopology β],
  MeasurableSet t → MonotoneOn g t → ContinuousOn g t → MeasurableSet (g '' t)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.all_eq_true_iff_forall_contains_get : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {p : (a : α) → β a → Bool}, m.WF → (m.all p = true ↔ ∀ (a : α) (h : m.contains a = true), p a (m.get a h) = true)
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.CofibrantObject.homMk_homMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] {X Y Z : C} [inst_3 : HomotopicalAlgebra.IsCofibrant X]
  [inst_4 : HomotopicalAlgebra.IsCofibrant Y] [inst_5 : HomotopicalAlgebra.IsCofibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.homMk f)
      (HomotopicalAlgebra.CofibrantObject.homMk g) =
    HomotopicalAlgebra.CofibrantObject.homMk (CategoryTheory.CategoryStruct.comp f g)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.fold_filter : ∀ {α β δ : Type w} {m : Type w → Type w'} {Pred EPred : Type w} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_2 : Monad m] [inst_3 : Std.Internal.Do.Assertion Pred] [inst_4 : Std.Internal.Do.Assertion EPred]
  [inst_5 : Std.Internal.Do.WPMonad m Pred EPred] [inst_6 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m]
  {f : β → Bool} {g : δ → β → δ} {init : δ} {it : Std.IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄ Std.IterM.fold (fun d b => if f b = true then g d b else d) init it ⦃ Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.IterM.filter f it) ⦃ Q; eQ ⦄
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHomClass.toZeroHomClass : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {inst : AddZero M} {inst_1 : AddZero N}
  {inst_2 : FunLike F M N} [self : AddMonoidHomClass F M N], ZeroHomClass F M N
-- Init.Data.Rat.Lemmas
Rat.natCast_pos : ∀ {a : ℕ}, 0 < ↑a ↔ 0 < a
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Additivity of a continuous alternating map along all coordinates at the same time,
writing `f (m + m')` as the sum of `f (s.piecewise m m')` over all sets `s`.  -/
ContinuousAlternatingMap.map_add_univ : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [inst_7 : DecidableEq ι] [inst_8 : Fintype ι] (m m' : ι → M),
  f (m + m') = ∑ s, f (s.piecewise m m')
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- If `G` acts freely on `X`, `X` is equivalent to the product of the quotient of `X` by
`G` and `G`.  -/
AddAction.selfEquivOrbitsQuotientProd : {G : Type u} →
  {X : Type v} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G X] → (∀ (b : X), AddAction.stabilizer G b = ⊥) → X ≃ Quotient (AddAction.orbitRel G X) × G
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_add : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (a b : MvPolynomial σ R),
  (a + b).totalDegree ≤ max a.totalDegree b.totalDegree
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.instIsLocallySurjectiveFunWhiskerRightOppositeForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) [CategoryTheory.Presheaf.IsLocallySurjective J f],
  CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.Functor.whiskerRight f (CategoryTheory.forget A))
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.toReal_klDiv_smul_left : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
      ∀ (c : NNReal),
        (InformationTheory.klDiv (c • μ) ν).toReal =
          ↑c * (InformationTheory.klDiv μ ν).toReal + (1 - ↑c) * ν.real Set.univ + ↑c * Real.log ↑c * μ.real Set.univ
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- Finite measures are defined as the subtype of measures that have the property of being finite
measures (i.e., their total mass is finite).  -/
MeasureTheory.FiniteMeasure : (Ω : Type u_2) → [MeasurableSpace Ω] → Type u_2
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rco_eq_some_iff : ∀ {k m n i : ℕ}, (m...n).toArray[i]? = some k ↔ i < n - m ∧ m + i = k
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.UnorderedListType.all : List Lean.Doc.Parser.UnorderedListType
-- Mathlib.Data.List.Nodup
List.Nodup.diff : ∀ {α : Type u} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α], l₁.Nodup → (l₁.diff l₂).Nodup
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_ofNat : ∀ (n : ℕ), { toBitVec := BitVec.ofNat 16 n } = OfNat.ofNat n
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns a `List` of the values in order.  -/
Std.DTreeMap.Internal.Impl.values : {α : Type u} → {β : Type v} → (Std.DTreeMap.Internal.Impl α fun x => β) → List β
-- Mathlib.LinearAlgebra.Dimension.Basic
LinearEquiv.lift_rank_map_eq : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M ≃ₗ[R] M') (p : Submodule R M),
  Cardinal.lift.{v, v'} (Module.rank R ↥(Submodule.map (↑f) p)) = Cardinal.lift.{v', v} (Module.rank R ↥p)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- `sum f g` is the sum of `g a (f a)` over the support of `f`.  -/
Finsupp.sum : {α : Type u_1} → {M : Type u_8} → {N : Type u_10} → [inst : Zero M] → [AddCommMonoid N] → (α →₀ M) → (α → M → N) → N
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.inf_pow_eq_prod_of_prime`.

---

The intersection of distinct prime powers in a Dedekind domain is the product of these
prime powers.  -/
IsDedekindDomain.inf_prime_pow_eq_prod : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_4} [IsDedekindDomain R] (s : Finset ι) (f : ι → Ideal R) (e : ι → ℕ),
  (∀ i ∈ s, Prime (f i)) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j) → (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EffectiveEquivalenceRelation.toEquivalenceRelation : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R A : C} →
      {p₁ p₂ : R ⟶ A} → CategoryTheory.EffectiveEquivalenceRelation p₁ p₂ → CategoryTheory.EquivalenceRelation p₁ p₂
-- Mathlib.Logic.Equiv.Set
Equiv.Set.rangeSplittingImageEquiv_apply_coe_coe : ∀ {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set ↑(Set.range f)) (x : ↑(Set.rangeSplitting f '' s)),
  ↑↑((Equiv.Set.rangeSplittingImageEquiv f s) x) = f ↑x
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Polynomial.sub_one_pow_totient_lt_natAbs_cyclotomic_eval : ∀ {n q : ℕ}, 1 < n → q ≠ 1 → (q - 1) ^ n.totient < (Polynomial.eval (↑q) (Polynomial.cyclotomic n ℤ)).natAbs
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.exists_le_prime_disjoint : ∀ {α : Type u} [inst : CommSemiring α] (I : Ideal α) (S : Submonoid α),
  Disjoint ↑I ↑S → ∃ p, p.IsPrime ∧ I ≤ p ∧ Disjoint ↑p ↑S
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.toAffineEquiv_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), ↑e.symm = (↑e).symm
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedActionResult.default : Lean.Meta.Grind.ActionResult
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
_private.Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv.0.GenContFract.contsAux.match_1.eq_1 : ∀ {K : Type u_1} (motive : Option (GenContFract.Pair K) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (gp : GenContFract.Pair K) → motive (some gp)),
  (match none with
    | none => h_1 ()
    | some gp => h_2 gp) =
    h_1 ()
-- Init.Data.SInt.Lemmas
Int32.toISize_ofIntLE : ∀ {n : ℤ} (h₁ : Int32.minValue.toInt ≤ n) (h₂ : n ≤ Int32.maxValue.toInt),
  (Int32.ofIntLE n h₁ h₂).toISize = ISize.ofIntLE n ⋯ ⋯
-- Mathlib.Algebra.Module.FinitePresentation
Module.finitePresentation_of_projective : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Projective R M]
  [Module.Finite R M], Module.FinitePresentation R M
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.getD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α] (a : α) (fallback : β a)
  (size : ℕ) (buckets : Array (Std.DHashMap.Internal.AssocList α β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.getD ⟨{ size := size, buckets := buckets }, hm⟩ a fallback =
    Std.DHashMap.Internal.AssocList.getCastD a fallback buckets[↑(Std.DHashMap.Internal.mkIdx buckets.size hm (hash a))]