mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.AddGroupWithTop
/-- A linearly ordered commutative group with an additively absorbing `⊤` element.
Instances should include number systems with an infinite element adjoined.  -/
LinearOrderedAddCommGroupWithTop : Type u_3 → Type u_3
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus_map : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (i : U ≤ V) (s : Set ↑(X.presheaf.obj (Opposite.op V))),
  X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE i).op)) '' s) = X.zeroLocus s ∪ (↑U)ᶜ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarCoord_symm_eq : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  ↑(NumberField.mixedEmbedding.polarCoord K).symm =
    ⇑(NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace K).symm ∘
      ↑(NumberField.mixedEmbedding.polarCoordReal K).symm
-- Lean.Elab.DeclModifiers
Lean.Elab.ComputeKind.noConfusionType : Sort v✝ → Lean.Elab.ComputeKind → Lean.Elab.ComputeKind → Sort v✝
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mul_lt_aleph0_iff : ∀ {a b : Cardinal.{u_1}}, a * b < Cardinal.aleph0 ↔ a = 0 ∨ b = 0 ∨ a < Cardinal.aleph0 ∧ b < Cardinal.aleph0
-- Mathlib.RingTheory.LocalRing.NonLocalRing
/-- The product of two nontrivial (semi)rings is not local.  -/
IsLocalRing.not_isLocalRing_of_prod_of_nontrivial : ∀ (R₁ : Type u_1) (R₂ : Type u_2) [inst : Semiring R₁] [inst_1 : Semiring R₂] [Nontrivial R₁] [Nontrivial R₂],
  ¬IsLocalRing (R₁ × R₂)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.descCocycle_coe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K M m) (β : CochainComplex.HomComplex.Cocycle L M n) (h : m + 1 = n)
  (hαβ : CochainComplex.HomComplex.δ m n α + m.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0),
  ↑(CochainComplex.mappingCocone.descCocycle φ α β h hαβ) = CochainComplex.mappingCocone.descCochain φ α (↑β) h
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateFVarImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu → Lean.FVarId → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.LetValue pu
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceLT : Lean.Meta.Simp.Simproc
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.substFunc.eq_1 : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} (x : {n : ℕ} → L.Functions n → L'.Term (Fin n))
  (a : α), (FirstOrder.Language.var a).substFunc x = FirstOrder.Language.var a
-- Std.Time.Format.Modifier
/-- Post meridiem (after noon)
 -/
Std.Time.DayPeriod.pm : Std.Time.DayPeriod
-- Mathlib.Analysis.Real.Pi.Chudnovsky
/-- The term at index `n` in Chudnovsky's series for `π⁻¹`  -/
chudnovskyTerm : ℕ → ℚ
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.mk : {α : Type u_4} →
  [inst : TopologicalSpace α] →
    (toCompacts : TopologicalSpace.Compacts α) → IsOpen toCompacts.carrier → TopologicalSpace.CompactOpens α
-- Mathlib.Analysis.Normed.Ring.Basic
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
NonUnitalNormedCommRing.mul_comm : ∀ {α : Type u_5} [self : NonUnitalNormedCommRing α] (a b : α), a * b = b * a
-- Mathlib.CategoryTheory.SingleObj
MulEquiv.toSingleObjEquiv_unitIso_hom : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (e : M ≃* N),
  e.toSingleObjEquiv.unitIso.hom = CategoryTheory.eqToHom ⋯
-- Init.Grind.ToInt
Lean.Grind.IntInterval.mem_co : ∀ (lo hi x : ℤ), x ∈ Lean.Grind.IntInterval.co lo hi ↔ lo ≤ x ∧ x < hi
-- Mathlib.Order.Lattice
SemilatticeSup.toMax.eq_1 : ∀ {α : Type u} [inst : SemilatticeSup α], SemilatticeSup.toMax = { max := fun a b => SemilatticeSup.sup a b }
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.Cotangent.equivOfEq_toCotangent : ∀ {R : Type u} [inst : CommRing R] (I J : Ideal R) (hIJ : I = J) (x : ↥I),
  (Ideal.Cotangent.equivOfEq I J hIJ) (I.toCotangent x) = J.toCotangent ((LinearEquiv.ofEq I J hIJ) x)
-- Mathlib.MeasureTheory.Measure.Sub
MeasureTheory.Measure.sub_add_cancel_of_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν],
  ν ≤ μ → μ - ν + ν = μ
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesImage.iso_hom_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasCokernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesImage.iso F f).hom
      (CategoryTheory.Abelian.image.ι (F.map f)) =
    F.map (CategoryTheory.Abelian.image.ι f)
-- Init.Data.String.Slice
String.Slice.SplitInclusiveIterator.operating : {σ : String.Slice → Type} →
  {ρ : Type} →
    {pat : ρ} →
      {s : String.Slice} →
        [inst : String.Slice.Pattern.ToForwardSearcher pat σ] →
          s.Pos → Std.Iter (String.Slice.Pattern.SearchStep s) → String.Slice.SplitInclusiveIterator pat s
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.ContinuousRiemannianMetric.symm : ∀ {B : Type u_4} [inst : TopologicalSpace B] {F : Type u_5} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {E : B → Type u_6} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (b : B) → TopologicalSpace (E b)]
  [inst_5 : (b : B) → AddCommGroup (E b)] [inst_6 : (b : B) → Module ℝ (E b)] [inst_7 : FiberBundle F E]
  [inst_8 : VectorBundle ℝ F E] (self : Bundle.ContinuousRiemannianMetric F E) (b : B) (v w : E b),
  ((self.inner b) v) w = ((self.inner b) w) v
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of adding a point to a finite-dimensional subspace is finite-dimensional.  -/
finiteDimensional_vectorSpan_insert : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : AffineSubspace k P) [FiniteDimensional k ↥s.direction] (p : P),
  FiniteDimensional k ↥(vectorSpan k (insert p ↑s))
-- Mathlib.Data.Int.Cast.Lemmas
MonoidHom.ext_mint_iff : ∀ {M : Type u_5} [inst : Monoid M] {f g : Multiplicative ℤ →* M},
  f = g ↔ f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)
-- Mathlib.Order.Disjoint
Codisjoint.of_codisjoint_sup_of_le : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b c : α},
  Codisjoint (a ⊔ b) c → c ≤ a → Codisjoint a b
-- Mathlib.RingTheory.LocalProperties.Injective
Module.injective_of_isLocalizedModule : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submonoid R)
  [Small.{v, u} R] [IsNoetherianRing R] {Rₛ : Type u'} [Small.{v', u'} Rₛ] [inst_6 : CommRing Rₛ]
  [inst_7 : Algebra R Rₛ] {Mₛ : Type v'} [inst_8 : AddCommGroup Mₛ] [inst_9 : Module R Mₛ] [inst_10 : Module Rₛ Mₛ]
  [IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalization S Rₛ] [IsLocalizedModule S f] [Module.Injective R M],
  Module.Injective Rₛ Mₛ
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Clean.State.used : Lean.Meta.Grind.Clean.State → Lean.PHashSet Lean.Name
-- Mathlib.Topology.Constructions
nhds_ofDual : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X), nhds (OrderDual.ofDual x) = Filter.map (⇑OrderDual.ofDual) (nhds x)
-- Mathlib.Geometry.Manifold.Bordism
/-- A map of topological spaces induces a corresponding map of singular manifolds.  -/
SingularManifold.map : {X : Type u_7} →
  {Y : Type u_8} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {k : WithTop ℕ∞} →
          {E : Type u_9} →
            {H : Type u_10} →
              [inst_2 : NormedAddCommGroup E] →
                [inst_3 : NormedSpace ℝ E] →
                  [inst_4 : FiniteDimensional ℝ E] →
                    [inst_5 : TopologicalSpace H] →
                      {I : ModelWithCorners ℝ E H} →
                        SingularManifold X k I → {φ : X → Y} → Continuous φ → SingularManifold Y k I
-- Init.Data.Nat.Basic
Nat.and_forall_add_one : ∀ {p : ℕ → Prop}, (p 0 ∧ ∀ (n : ℕ), p (n + 1)) ↔ ∀ (n : ℕ), p n
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Ring
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.Ring.0.Pentagonal.powMulProdOneSubPow.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (k n : ℕ) (x : R),
  Pentagonal.powMulProdOneSubPow✝ k n x = x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The functoriality of `X.opcycles` with respect to morphisms in
`ComposableArrows ι 2`.  -/
CategoryTheory.Abelian.SpectralObject.opcyclesMap : {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 j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  {i' j' k' : ι} →
                    (f' : i' ⟶ j') →
                      (g' : j' ⟶ k') →
                        (CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') →
                          (n : ℤ) → X.opcycles f g n ⟶ X.opcycles f' g' n
-- Mathlib.Algebra.Star.Conjneg
conjnegRingHom_apply : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] (f : G → R) (a : G),
  conjnegRingHom f a = conjneg f a
-- Init.Core
not_iff_false_intro : ∀ {a : Prop}, a → (¬a ↔ False)
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.updateAllBuckets : {α : Type u} →
  {β : α → Type v} →
    {δ : α → Type w} →
      Array (Std.DHashMap.Internal.AssocList α β) →
        (Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α δ) →
          Array (Std.DHashMap.Internal.AssocList α δ)
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.mk.injEq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (toLinearMap : A →ₗ[R] B) (counit_comp : CoalgebraStruct.counit ∘ₗ toLinearMap = CoalgebraStruct.counit)
  (map_comp_comul :
    TensorProduct.map toLinearMap toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ toLinearMap)
  (toLinearMap_1 : A →ₗ[R] B) (counit_comp_1 : CoalgebraStruct.counit ∘ₗ toLinearMap_1 = CoalgebraStruct.counit)
  (map_comp_comul_1 :
    TensorProduct.map toLinearMap_1 toLinearMap_1 ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ toLinearMap_1),
  ({ toLinearMap := toLinearMap, counit_comp := counit_comp, map_comp_comul := map_comp_comul } =
      { toLinearMap := toLinearMap_1, counit_comp := counit_comp_1, map_comp_comul := map_comp_comul_1 }) =
    (toLinearMap = toLinearMap_1)
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.subseq.go : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.SubseqResult
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.initiallySmall_of_essentiallySmall : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.EssentiallySmall.{w, v, u} J],
  CategoryTheory.InitiallySmall J
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.diagramCompIso_hom_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (W : (J.Cover X)ᵒᵖ) (i : (Opposite.unop W).Arrow) {Z : E}
  (h : ((Opposite.unop W).index (P.comp F)).left i ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P X).hom.app W)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (P.comp F)) i) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index P) i)) h
-- Mathlib.Analysis.Complex.Asymptotics
Complex.isTheta_ofReal : ∀ {α : Type u_1} (f : α → ℝ) (l : Filter α), (fun x => ↑(f x)) =Θ[l] f
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instLEOffset : LE Std.Time.Nanosecond.Offset
-- Mathlib.LinearAlgebra.Matrix.Kronecker
/-- Produce a matrix with `f` applied to every pair of elements from `A` and `B`.  -/
Kronecker.«term_⊗ₖ_» : Lean.TrailingParserDescr
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_iff_meet_eq_right : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l},
  Lean.Order.PartialOrder.rel P Q ↔ Lean.Order.meet Q P = P
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddZero : {α : Type u_1} → [AddZero α] → AddZero αᵃᵒᵖ
-- Mathlib.Order.LiminfLimsup
Filter.le_limsInf_of_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f : Filter α} {a : α},
  autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) f) Filter.le_limsInf_of_le._auto_1 →
    (∀ᶠ (n : α) in f, a ≤ n) → a ≤ f.limsInf
-- Lean.Meta.Tactic.Grind.Action
/-- Choice: tries `x`, if not applicable, tries `y`.
 -/
Lean.Meta.Grind.Action.orElse : Lean.Meta.Grind.Action → Lean.Meta.Grind.Action → Lean.Meta.Grind.Action
-- Mathlib.Algebra.Ring.Parity
Nat.Odd.sub_even : ∀ {m n : ℕ}, n ≤ m → Odd m → Even n → Odd (m - n)
-- Mathlib.Analysis.Normed.Group.AddTorsor
nndist_vadd_vadd_le : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (v v' : V) (p p' : P), nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p'
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.isIso_post : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.Limits.HasFiniteColimits C]
  (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [inst_2 : CategoryTheory.SmallCategory J]
  [inst_3 : CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ)
  [CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)],
  CategoryTheory.IsIso (CategoryTheory.Limits.limit.post K A)
-- Mathlib.Analysis.Convex.Between
wbtw_smul_vadd_smul_vadd_of_nonneg_of_nonpos : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (x : P) (v : V) {r₁ r₂ : R},
  0 ≤ r₁ → r₂ ≤ 0 → Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)
-- Mathlib.Algebra.Group.End
Equiv.swap_mul_self : ∀ {α : Type u_4} [inst : DecidableEq α] (i j : α), Equiv.swap i j * Equiv.swap i j = 1
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE_app_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
  AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Scheme.Hom.resLE f U V e) ⊤ =
    CategoryTheory.CategoryStruct.comp U.topIso.hom
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V e) V.topIso.inv)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasProdLocallyUniformly_iff_tendstoLocallyUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasProdLocallyUniformly f g ↔ TendstoLocallyUniformly (fun x1 x2 => ∏ i ∈ x1, f i x2) g Filter.atTop
-- Mathlib.Algebra.Order.Group.CompleteLattice
ciSup_div : ∀ {ι : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
  [MulRightMono G], BddAbove (Set.range f) → ∀ (a : G), (⨆ i, f i) / a = ⨆ i, f i / a
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.addLinearEquiv_castAdd : ∀ {R : Type u_1} [inst : Semiring R] {m n : ℕ} (i : Fin m),
  (Polynomial.degreeLT.addLinearEquiv R m n) ((Polynomial.degreeLT.basis R (m + n)) (Fin.castAdd n i)) =
    ((Polynomial.degreeLT.basis R m) i, 0)
-- Mathlib.Data.Matrix.Mul
Matrix.sum_mul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : Fintype m] (s : Finset β) (f : β → Matrix l m α) (M : Matrix m n α), (∑ a ∈ s, f a) * M = ∑ a ∈ s, f a * M
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insertIfNew : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {fallback v : β},
  Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl a fallback =
    if compare k a = Ordering.eq ∧ k ∉ t then v else Std.DTreeMap.Internal.Impl.Const.getD t a fallback
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerivedNatTrans_app_assoc : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (RF RF' : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : RF.IsRightDerivedFunctor α W] (τ : F ⟶ F') (X : C) {Z : H} (h : RF'.obj (L.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.app X)
      (CategoryTheory.CategoryStruct.comp ((RF.rightDerivedNatTrans RF' α α' W τ).app (L.obj X)) h) =
    CategoryTheory.CategoryStruct.comp (τ.app X) (CategoryTheory.CategoryStruct.comp (α'.app X) h)
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.coe_extendedHom_eq_span : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] [inst_12 : Algebra K L] [inst_13 : Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] (I : FractionalIdeal (nonZeroDivisors A) K),
  ↑((FractionalIdeal.extendedHom L B) I) = Submodule.span B (⇑(algebraMap K L) '' ↑I)
-- Mathlib.Probability.Distributions.Cauchy
/-- A Cauchy distribution on `ℝ` with location parameter `x₀` and scale parameter `γ`.  -/
ProbabilityTheory.cauchyMeasure : ℝ → NNReal → MeasureTheory.Measure ℝ
-- Mathlib.Order.WithBot
WithTop.monotone_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : WithTop α → β},
  Monotone f ↔ (Monotone fun a => f ↑a) ∧ ∀ (x : α), f ↑x ≤ f ⊤
-- Mathlib.Algebra.Algebra.Defs
algebraMap.coe_neg : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (x : R), ↑(-x) = -↑x
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.coprodSpec_inl : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (AlgebraicGeometry.coprodSpec R S) =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.fst R S))
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_smul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E]
  [SMulCommClass ℝ 𝕜 E] (f : α → E) (r : 𝕜), μ.withDensityᵥ (r • f) = r • μ.withDensityᵥ f
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.image_preimage_is_empty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasLimits C] {ι : Type v}
  (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) (AlgebraicGeometry.SheafedSpace C))
  [inst_2 : CategoryTheory.Limits.HasColimit F] (i j : CategoryTheory.Discrete ι),
  i ≠ j →
    ∀ (U : TopologicalSpace.Opens ↑↑(F.obj i).toPresheafedSpace),
      (TopologicalSpace.Opens.map
              (CategoryTheory.Limits.colimit.ι (F.comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace)
                  j).base).obj
          ((TopologicalSpace.Opens.map
                (CategoryTheory.preservesColimitIso AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace
                      F).inv.base).obj
            (⋯.functor.obj U)) =
        ⊥
-- Mathlib.Algebra.Module.Torsion.Basic
Module.IsTorsionBySet.isSemisimpleModule_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  [inst_3 : I.IsTwoSided] (hM : Module.IsTorsionBySet R M ↑I), IsSemisimpleModule (R ⧸ I) M ↔ IsSemisimpleModule R M
-- Mathlib.Order.BoundedOrder.Basic
le_top : ∀ {α : Type u} [inst : LE α] [inst_1 : OrderTop α] {a : α}, a ≤ ⊤
-- Init.Data.SInt.Lemmas
Int8.instIsLinearOrder : Std.IsLinearOrder Int8
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.frontier : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.IsImage (frontier s) (frontier t)
-- Mathlib.FieldTheory.SeparableClosure
Field.sepDegree.eq_1 : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Field.sepDegree F E = Module.rank F ↥(separableClosure F E)