mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Depth.Rees
_private.Mathlib.RingTheory.Depth.Rees.0.smul_top_quotSMulTop_ne_top_of_smul_top_ne_top : ∀ {R : Type u} [inst : CommRing R] {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R} {r : R},
  r ∈ I → I • ⊤ ≠ ⊤ → I • ⊤ ≠ ⊤
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.inducedFunctor_additive : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} D] [inst_1 : CategoryTheory.Preadditive D]
  (F : C → D), (CategoryTheory.inducedFunctor F).Additive
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.HasCardinalFilteredColimits.congr_simp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (κ κ_1 : Cardinal.{w}) (e_κ : κ = κ_1)
  [inst_1 : Fact κ.IsRegular],
  CategoryTheory.HasCardinalFilteredColimits C κ = CategoryTheory.HasCardinalFilteredColimits C κ_1
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.smul_inj : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f]
  (s : ↥S) (m₁ m₂ : M'), s • m₁ = s • m₂ ↔ m₁ = m₂
-- Mathlib.Data.Nat.Fib.Basic
/-- Computes `(Nat.fib n, Nat.fib (n + 1))` using the binary representation of `n`.
Supports `Nat.fastFib`.  -/
Nat.fastFibAux : ℕ → ℕ × ℕ
-- Aesop.Builder.Basic
Aesop.CoreRuleBuilderOutput.pattern? : Aesop.CoreRuleBuilderOutput → Option Aesop.RulePattern
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mk_self : ∀ {R : Type u} [inst : CommSemiring R], CommRing.Pic.mk R R = 1
-- Init.Data.String.Basic
String.Pos.Raw.extract.go₂ : List Char → String.Pos.Raw → String.Pos.Raw → List Char
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.isBigO_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v → v =O[l] u
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.regOfFamily_eq_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ},
  ¬NumberField.Units.IsMaxRank u → NumberField.Units.regOfFamily u = 0
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- A variant of `IsConjRoot.iff_eq_zero`, only assuming `IsDomain R`,
`IsTorsionFree R A` and `Function.Injective (algebraMap R A)` instead of `Field R`. `x` is a
conjugate root of `0` if and only if `x = 0`.
 -/
isConjRoot_zero_iff_eq_zero_of_injective : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain S]
  [IsDomain R] {x : S} [Module.IsTorsionFree R S], Function.Injective ⇑(algebraMap R S) → (IsConjRoot R 0 x ↔ x = 0)
-- Lean.Elab.PreDefinition.WF.GuessLex
_private.Lean.Elab.PreDefinition.WF.GuessLex.0.Lean.Elab.WF.GuessLex.withRecApps.containsRecFn : {α : Type} → (recFnName : Lean.Name) → Lean.Expr → Lean.Elab.WF.GuessLex.M recFnName α Bool
-- Mathlib.Algebra.MvPolynomial.Nilpotent
MvPolynomial.instIsLocalHomRingHomAlgebraMap : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R], IsLocalHom (algebraMap R (MvPolynomial σ R))
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.comp_inj_right : ∀ {V : Type u} [inst : Quiver V] {a b c : V} {p : Quiver.Path a b} {q₁ q₂ : Quiver.Path b c},
  p.comp q₁ = p.comp q₂ ↔ q₁ = q₂
-- Lean.Meta.Closure
Lean.Meta.Closure.pickNextToProcessAux : Lean.LocalContext →
  ℕ →
    Array Lean.Meta.Closure.ToProcessElement →
      Lean.Meta.Closure.ToProcessElement → Lean.Meta.Closure.ToProcessElement × Array Lean.Meta.Closure.ToProcessElement
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.modifyStateImpl : {σ : Type} → Lean.EnvExtension σ → Array Lean.EnvExtensionState → (σ → σ) → Array Lean.EnvExtensionState
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.finite_subcomplex_of_finite`.

---

A subcomplex of a finite CW complex is again finite.  -/
Topology.CWComplex.Subcomplex.finite_subcomplex_of_finite : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  [Topology.RelCWComplex.Finite C] (E : Topology.RelCWComplex.Subcomplex C), Topology.RelCWComplex.Finite ↑E
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.AbsolutelyContinuous.restrict : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → ∀ (s : Set α), (μ.restrict s).AbsolutelyContinuous (ν.restrict s)
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.getUnassignedLevelMVars : Lean.Expr → Lean.MetaM (Array Lean.LMVarId)
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.ext : ∀ {X Y : AlgebraicGeometry.Scheme} (f g : X.PartialIso Y) (e : f.source = g.source) (e' : g.target = f.target),
  f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e' → f = g
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.maxKeyD fallback ∈ t
-- Mathlib.NumberTheory.Pell
/-- The set of solutions with `x > 0` is closed under multiplication.  -/
Pell.Solution₁.x_mul_pos : ∀ {d : ℤ} {a b : Pell.Solution₁ d}, 0 < a.x → 0 < b.x → 0 < (a * b).x
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovaryOn_inv_left`. -/
AntivaryOn.inv_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn f g s → MonovaryOn f⁻¹ g s
-- Mathlib.GroupTheory.Rank
Group.rank_le : ∀ {G : Type u_1} [inst : Group G] [h : Group.FG G] {S : Finset G}, Subgroup.closure ↑S = ⊤ → Group.rank G ≤ S.card
-- Init.Data.SInt.Lemmas
Int64.toISize_ofIntClamp : ∀ {n : ℤ}, -2 ^ 63 ≤ n → n < 2 ^ 63 → (Int64.ofIntClamp n).toISize = ISize.ofInt n
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGE_iff_pairwise`. -/
List.Pairwise.sortedGE : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], List.Pairwise (fun x1 x2 => x1 ≥ x2) l → l.SortedGE
-- Mathlib.Data.ENNReal.Inv
/-- The inverse map `fun x ↦ x⁻¹` is an order isomorphism between `ℝ≥0∞` and its `OrderDual`  -/
OrderIso.invENNReal : ENNReal ≃o ENNRealᵒᵈ
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.braidingHomCorepresenting.eq_1 : ∀ {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.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  (F G : CategoryTheory.Functor C V) [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution G F],
  CategoryTheory.MonoidalCategory.DayConvolution.braidingHomCorepresenting F G =
    {
      app := fun x =>
        CategoryTheory.CategoryStruct.comp (β_ ((F, G).1.obj x.1) ((F, G).2.obj x.2)).hom
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit G F).app (x.2, x.1))
            ((CategoryTheory.MonoidalCategory.DayConvolution.convolution G F).map (β_ (x.2, x.1).1 (x.2, x.1).2).hom)),
      naturality := ⋯ }
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.norm_unit : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (u : (NumberField.RingOfIntegers K)ˣ),
  NumberField.mixedEmbedding.norm ((NumberField.mixedEmbedding K) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) =
    1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasCokernel S.f] (hg : S.g = 0),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg).H = CategoryTheory.Limits.cokernel S.f
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.isAlgebraic_iff_bot : ∀ (R : Type u_1) (S : Type u_2) {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S]
  [Algebra.IsAlgebraic S A] [FaithfulSMul S A], Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic R S
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
/-- Any ordered group is isomorphic to the units of itself adjoined with `0`.  -/
OrderMonoidIso.unitsWithZero : {α : Type u_6} → [inst : Group α] → [inst_1 : Preorder α] → (WithZero α)ˣ ≃*o α
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
/-- The addition of two maps `L.obj X ⟶ L.obj Y` when `L : C ⥤ D` is a localization
functor, `C` is preadditive and there is a left calculus of fractions.  -/
CategoryTheory.Localization.Preadditive.add' : {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.Preadditive C] →
          {L : CategoryTheory.Functor C D} →
            (W : CategoryTheory.MorphismProperty C) →
              [L.IsLocalization W] →
                [W.HasLeftCalculusOfFractions] →
                  {X Y : C} → (L.obj X ⟶ L.obj Y) → (L.obj X ⟶ L.obj Y) → (L.obj X ⟶ L.obj Y)
-- Mathlib.Data.Multiset.Lattice
Multiset.inf_ndinsert : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] [inst_2 : DecidableEq α] (a : α) (s : Multiset α),
  (Multiset.ndinsert a s).inf = a ⊓ s.inf
-- Mathlib.Algebra.Category.Ring.Basic
/-- The forgetful functor from commutative rings to (multiplicative) commutative monoids.  -/
CommSemiRingCat.hasForgetToCommMonCat : CategoryTheory.HasForget₂ CommSemiRingCat CommMonCat
-- Init.Core
imp_iff_right : ∀ {b a : Prop}, a → (a → b ↔ b)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {f : Option (β k) → Option (β k)},
  m.WF → (m.alter k f).get? k' = if h : (k == k') = true then cast ⋯ (f (m.get? k)) else m.get? k'
-- Mathlib.Topology.Algebra.Constructions
AddUnits.isEmbedding_embedProduct : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M], Topology.IsEmbedding ⇑(AddUnits.embedProduct M)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.πE_map : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (β : CategoryTheory.ComposableArrows.mk₂ f₁ f₂ ⟶ CategoryTheory.ComposableArrows.mk₂ f₁' f₂') (n₀ n₁ n₂ : ℤ),
  autoParam (β = CategoryTheory.ComposableArrows.homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯)
      CategoryTheory.Abelian.SpectralObject.πE_map._auto_1 →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.πE_map._auto_3)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.πE_map._auto_5),
      CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
          (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂) =
        CategoryTheory.CategoryStruct.comp (X.cyclesMap f₁ f₂ f₁' f₂' β n₁) (X.πE f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.mono_lift_of_mono_right : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Mono g],
  CategoryTheory.Mono (CategoryTheory.Limits.biprod.lift f g)
-- Mathlib.Data.Set.Subset
Set.image_val_injective : ∀ {α : Type u_2} {A : Set α}, Function.Injective (Set.image Subtype.val)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.d_fst_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i j k : ℤ)
  (hij : i + 1 = j) (hjk : j + 1 = k),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d i j)
      ((↑(CochainComplex.mappingCone.fst φ)).v j k hjk) =
    -CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) (F.d j k)
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Prequotient.of.injEq : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat} (j : J) (x : ↑(F.obj j))
  (j_1 : J) (x_1 : ↑(F.obj j_1)),
  (MonCat.Colimits.Prequotient.of j x = MonCat.Colimits.Prequotient.of j_1 x_1) = (j = j_1 ∧ x ≍ x_1)
-- Mathlib.Data.List.GetD
List.getI_eq_getElem : ∀ {α : Type u} (l : List α) [inst : Inhabited α] {n : ℕ} (hn : n < l.length), l.getI n = l[n]
-- Mathlib.Data.Set.Prod
Set.prod_subset_prod_iff_left : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t : Set β}, t.Nonempty → (s ×ˢ t ⊆ s₁ ×ˢ t ↔ s ⊆ s₁)
-- Mathlib.Logic.Equiv.Option
Equiv.removeNoneAux.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) (x : α),
  e.removeNoneAux x = if h : (e (some x)).isSome = true then (e (some x)).get h else (e none).get ⋯
-- Mathlib.Algebra.Field.Defs
DivisionRing.toNontrivial : ∀ {K : Type u_2} [self : DivisionRing K], Nontrivial K
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The subgroup of the vertex group at `c` given by the subgroupoid  -/
CategoryTheory.Subgroupoid.vertexSubgroup : {C : Type u} →
  [inst : CategoryTheory.Groupoid C] → (S : CategoryTheory.Subgroupoid C) → {c : C} → c ∈ S.objs → Subgroup (c ⟶ c)
-- Mathlib.Geometry.Euclidean.Angle.Bisector
/-- Auxiliary lemma for the degenerate case of `dist_orthogonalProjection_eq_iff_angle_eq` where
`p` lies in `s₁` or `s₂`.  -/
_private.Mathlib.Geometry.Euclidean.Angle.Bisector.0.EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq_aux : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p p' : P} {s₁ s₂ : AffineSubspace ℝ P} [inst_4 : s₁.direction.HasOrthogonalProjection]
  [inst_5 : s₂.direction.HasOrthogonalProjection] (hp'₁ : p' ∈ s₁) (hp'₂ : p' ∈ s₂),
  p ∈ s₁ ∨ p ∈ s₂ →
    (dist p ↑((EuclideanGeometry.orthogonalProjection s₁) p) = dist p ↑((EuclideanGeometry.orthogonalProjection s₂) p) ↔
      EuclideanGeometry.angle p p' ↑((EuclideanGeometry.orthogonalProjection s₁) p) =
        EuclideanGeometry.angle p p' ↑((EuclideanGeometry.orthogonalProjection s₂) p))
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGE.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (size : ℕ) (ky : α) (y : β ky)
  (l r : Std.DTreeMap.Internal.Impl α β) (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.getKeyGE k (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he =
    match h : compare k ky with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.getKeyGED k l ky
    | Ordering.eq => ky
    | Ordering.gt => Std.DTreeMap.Internal.Impl.getKeyGE k r ⋯ ⋯
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.evalAt_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (g h : G) (X : LeftInvariantDerivation I G),
  (LeftInvariantDerivation.evalAt (g * h)) X = (hfdifferential ⋯) ((LeftInvariantDerivation.evalAt h) X)
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.pointwise_isCentralScalar : ∀ {M : Type u_3} {A : Type u_4} [inst : Monoid M] [inst_1 : AddGroup A] [inst_2 : DistribMulAction M A]
  [inst_3 : DistribMulAction Mᵐᵒᵖ A] [IsCentralScalar M A], IsCentralScalar M (AddSubgroup A)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_map_val : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (f : ι → M),
  (Multiset.map f s.val).sum = ∑ a ∈ s, f a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_star : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  cfc (fun x => star (f x)) a = star (cfc f a)
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C),
  AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.hom.app X =
    AlgebraicTopology.DoldKan.Γ₂.map (AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁.hom.app X)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instNonAssocSemiring : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring k] → [inst_1 : Monoid G] → [MulSemiringAction G k] → NonAssocSemiring (SkewMonoidAlgebra k G)
-- Mathlib.Order.Directed
Monotone.directed_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [IsDirectedOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Directed (fun x1 x2 => x1 ≤ x2) f
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.ofPreGNS_toPreGNS : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] (f : A →ₚ[ℂ] ℂ) (a : A),
  f.ofPreGNS (f.toPreGNS a) = a
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.hasCountableCoproducts_of_hasCountableColimits : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCountableColimits C],
  CategoryTheory.Limits.HasCountableCoproducts C
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.isUnit_det_zpow_iff : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R} {z : ℤ}, IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
/-- **Alias** of `MeasureTheory.Measure.AbsolutelyContinuous.ae_le`.

---

**Alias** of the reverse direction of `MeasureTheory.Measure.ae_le_iff_absolutelyContinuous`. -/
MeasureTheory.Measure.ae_mono' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → MeasureTheory.ae μ ≤ MeasureTheory.ae ν
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ofInjective_apply : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f)
  {x : G}, ↑((AddMonoidHom.ofInjective hf) x) = f x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go.eq_def : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (best : Option (α × β))
  (a : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go k best a =
    match a with
    | Std.DTreeMap.Internal.Impl.leaf => best
    | Std.DTreeMap.Internal.Impl.inner size ky y l r =>
      match compare k ky with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go k (some (ky, y)) l
      | x => Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go k best r
-- Mathlib.Data.Set.Basic
Set.union_univ : ∀ {α : Type u} (s : Set α), s ∪ Set.univ = Set.univ
-- Mathlib.Data.Erased
Erased.out_mk : ∀ {α : Sort u_1} (a : α), (Erased.mk a).out = a
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- A functor to types `F : C ⥤ Type w'` is `w`-small if for any `X : C`,
the type `F.obj X` is `w`-small.  -/
CategoryTheory.FunctorToTypes.Small : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (Type w') → Prop
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- The approximation sequence converges at the successor of the domain's cardinality
to the greatest fixed point if starting from `⊥`  -/
OrdinalApprox.gfpApprox_ord_eq_gfp : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α),
  OrdinalApprox.gfpApprox f ⊤ (Order.succ (Cardinal.mk α)).ord = OrderHom.gfp f
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.trans_le : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : Norm E] [inst_1 : Norm F] [inst_2 : Norm G]
  {f : α → E} {g : α → F} {k : α → G} {l : Filter α}, f =o[l] g → (∀ (x : α), ‖g x‖ ≤ ‖k x‖) → f =o[l] k
-- Std.Data.DTreeMap.Internal.Operations
/-- Internal implementation detail of the hash map  -/
Std.DTreeMap.Internal.Impl.Const.beq : {α : Type u} →
  {β : Type v} →
    [Ord α] → [BEq β] → (Std.DTreeMap.Internal.Impl α fun x => β) → (Std.DTreeMap.Internal.Impl α fun x => β) → Bool
-- Mathlib.Algebra.CharP.Algebra
/-- If the algebra map `R →+* A` is injective and `R` has characteristic zero then so does `A`.  -/
charZero_of_injective_algebraMap : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Function.Injective ⇑(algebraMap R A) → ∀ [CharZero R], CharZero A
-- Std.Time.Format.Modifier
/-- `k`: Clock hour of day (1-24) (e.g., 24).
 -/
Std.Time.Modifier.k : Std.Time.Number → Std.Time.Modifier
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.ennreal_mass : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω}, ↑μ.mass = ↑μ Set.univ
-- Lean.Elab.PreDefinition.FixedParams
_private.Lean.Elab.PreDefinition.FixedParams.0.Lean.Elab.FixedParamPerm.pickFixed.go : {α : Type u_1} → List (Option ℕ × α) → Array α → Id (Array α)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- If a coequalizer of `f` and `g` exists, we can access an arbitrary choice of such by
saying `coequalizer f g`.  -/
CategoryTheory.Limits.coequalizer : {C : Type u} →
  {X Y : C} → [inst : CategoryTheory.Category.{v, u} C] → (f g : X ⟶ Y) → [CategoryTheory.Limits.HasCoequalizer f g] → C
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.instInvolutiveStar : {n : Type u_3} → {α : Type v} → [InvolutiveStar α] → InvolutiveStar (Matrix n n α)
-- Init.Data.Nat.Lemmas
Nat.add_lt_add_iff_left : ∀ {k n m : ℕ}, k + n < k + m ↔ n < m
-- Mathlib.Algebra.Order.Group.Abs
abs_sub : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (a b : G), |a - b| ≤ |a| + |b|
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.smul : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} {𝕜 : Type u_9} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  {f : X → E}, MeasureTheory.LocallyIntegrableOn f s μ → ∀ (c : 𝕜), MeasureTheory.LocallyIntegrableOn (c • f) s μ
-- Mathlib.Tactic.FunProp.Core
/-- Try to prove `e` using the *identity lambda theorem*.

For example, `e = q(Continuous fun x ↦ x)` and `funPropDecl` is `FunPropDecl` for `Continuous`.
 -/
Mathlib.Meta.FunProp.applyIdRule : Mathlib.Meta.FunProp.FunPropDecl →
  Lean.Expr →
    (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
      Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Mathlib.Data.Finsupp.Basic
/-- `Finsupp.mapDomain` is an `AddMonoidHom`.  -/
Finsupp.mapDomain.addMonoidHom : {α : Type u_1} → {β : Type u_2} → {M : Type u_5} → [inst : AddCommMonoid M] → (α → β) → (α →₀ M) →+ β →₀ M