mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- An isomorphism of short complexes `S₁ ≅ S₂` induces an isomorphism on the `Q` fields
of right homology data of `S₁` and `S₂`.  -/
CategoryTheory.ShortComplex.opcyclesMapIso' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (S₁ ≅ S₂) → (h₁ : S₁.RightHomologyData) → (h₂ : S₂.RightHomologyData) → h₁.Q ≅ h₂.Q
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- Assume that, applied to all the elements of a π-system, a sequence of probability measures
converges to a limiting probability measure. Assume also that the π-system contains arbitrarily
small neighborhoods of any point. Then the sequence of probability measures converges for the
weak topology.  -/
IsPiSystem.tendsto_probabilityMeasure_of_tendsto_of_mem : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [SecondCountableTopology Ω]
  [inst_3 : OpensMeasurableSpace Ω] {S : Set (Set Ω)},
  IsPiSystem S →
    ∀ {μ : ι → MeasureTheory.ProbabilityMeasure Ω} {ν : MeasureTheory.ProbabilityMeasure Ω} {l : Filter ι}
      [l.IsCountablyGenerated],
      (∀ s ∈ S, MeasurableSet s) →
        (∀ (u : Set Ω), IsOpen u → ∀ x ∈ u, ∃ s ∈ S, s ∈ nhds x ∧ s ⊆ u) →
          (∀ s ∈ S, Filter.Tendsto (fun i => (μ i) s) l (nhds (ν s))) → Filter.Tendsto μ l (nhds ν)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_map_mono : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  Function.Surjective ⇑f →
    ∀ [CategoryTheory.Mono φ] (i : ℕ), CategoryTheory.Mono ((groupCohomology.cochainsMap f φ).f i)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.single_sum : ∀ {α : Type u_1} {ι : Type u_2} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] (s : ι →₀ M)
  (f : ι → M → N) (a : α), (fun₀ | a => s.sum f) = s.sum fun d c => fun₀ | a => f d c
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.smul_snd : ∀ {R : Type u_1} {A : Type u_2} {E : Type u_3} {F : Type u_4} [inst : SMul R E] [inst_1 : SMul R F]
  (x : WithCStarModule A (E × F)) (c : R), (c • x).2 = c • x.2
-- Mathlib.Order.RelIso.Basic
/-- It suffices to prove `f` is monotone between strict relations
to show it is a relation embedding.  -/
RelEmbedding.ofMonotone : {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} →
      {s : β → β → Prop} →
        [Std.Trichotomous r] → [Std.Asymm s] → (f : α → β) → (∀ (a b : α), r a b → s (f a) (f b)) → r ↪r s
-- Mathlib.Data.Matrix.Mul
Matrix.transpose_mul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddCommMonoid α] [inst_1 : CommMagma α]
  [inst_2 : Fintype n] (M : Matrix m n α) (N : Matrix n l α), (M * N).transpose = N.transpose * M.transpose
-- Mathlib.Data.ZMod.Basic
ZMod.nontrivial' : Nontrivial (ZMod 0)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If three points are not collinear, the angle between them is not π.  -/
EuclideanGeometry.angle_ne_pi_of_not_collinear : ∀ {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₃ : P}, ¬Collinear ℝ {p₁, p₂, p₃} → EuclideanGeometry.angle p₁ p₂ p₃ ≠ Real.pi
-- Mathlib.Topology.ExtremallyDisconnected
/-- Lemma 2.3 in [Gleason, *Projective topological spaces*][gleason1958]:
a continuous surjection from a compact Hausdorff space to an extremally disconnected Hausdorff space
satisfying the "Zorn subset condition" is a homeomorphism.  -/
ExtremallyDisconnected.homeoCompactToT2 : {A E : Type u} →
  [inst : TopologicalSpace A] →
    [inst_1 : TopologicalSpace E] →
      [ExtremallyDisconnected A] →
        [T2Space A] →
          [T2Space E] →
            [CompactSpace E] →
              {ρ : E → A} →
                Continuous ρ →
                  Function.Surjective ρ → (∀ (E₀ : Set E), E₀ ≠ Set.univ → IsClosed E₀ → ρ '' E₀ ≠ Set.univ) → E ≃ₜ A
-- Init.Data.List.Int.Sum
List.sum_le_max_mul_length_int : ∀ {xs : List ℤ} (h : xs ≠ []), xs.sum ≤ xs.max h * ↑xs.length
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- Notation for `BasedFunctor`.  -/
CategoryTheory.«term_⥤ᵇ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- If a monoid `R` acts on another monoid `S`, then a non-unital algebra homomorphism
over `S` can be viewed as a non-unital algebra homomorphism over `R`.  -/
NonUnitalAlgHom.restrictScalars : (R : Type u_1) →
  {S : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : Monoid R] →
          [inst_1 : Monoid S] →
            [inst_2 : NonUnitalNonAssocSemiring A] →
              [inst_3 : NonUnitalNonAssocSemiring B] →
                [inst_4 : MulAction R S] →
                  [inst_5 : DistribMulAction S A] →
                    [inst_6 : DistribMulAction S B] →
                      [inst_7 : DistribMulAction R A] →
                        [inst_8 : DistribMulAction R B] →
                          [IsScalarTower R S A] → [IsScalarTower R S B] → (A →ₙₐ[S] B) → A →ₙₐ[R] B
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.map_chainComplex_d : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) (X : A) [inst_2 : ι.Full] [inst_3 : ι.Faithful]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A] (n : ℕ),
  ι.map ((Λ.chainComplex X).d (n + 2) (n + 1)) =
    CategoryTheory.CategoryStruct.comp (ι.map (Λ.chainComplexXIso X n).hom)
      (CategoryTheory.CategoryStruct.comp
        (Λ.π.app (CategoryTheory.Limits.kernel (ι.map ((Λ.chainComplex X).d (n + 1) n))))
        (CategoryTheory.Limits.kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))))
-- Mathlib.Topology.Order.LawsonTopology
/-- `toLawson` is the identity function to the `WithLawson` of a type.  -/
Topology.WithLawson.toLawson : {α : Type u_1} → α ≃ Topology.WithLawson α
-- Mathlib.NumberTheory.Height.NumberField
NumberField.instAdmissibleAbsValues : {K : Type u_1} → [inst : Field K] → [NumberField K] → Height.AdmissibleAbsValues K
-- Mathlib.Order.SuccPred.Basic
Order.Ico_subset_Ioo_pred_left_of_not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, ¬IsMin b → Set.Ico b a ⊆ Set.Ioo (Order.pred b) a
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_const_smul_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {V : (x : M') → TangentSpace I' x} {c : 𝕜},
  VectorField.mpullbackWithin I I' f (c • V) s x = c • VectorField.mpullbackWithin I I' f V s x
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ShiftTarget.vec : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {w : ℕ} → aig.ShiftTarget w → aig.RefVec w
-- Mathlib.Order.Filter.Map
Filter.comap_comap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : γ → β} {n : β → α},
  Filter.comap m (Filter.comap n f) = Filter.comap (n ∘ m) f
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coeFnAddMonoidHom.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddMonoid β]
  [inst_3 : ContinuousAdd β], ContinuousMap.coeFnAddMonoidHom = { toFun := fun f => ⇑f, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.hom_ext : ∀ {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]
  {F G : CategoryTheory.MonoidalCategory.DayFunctor C V} {α β : F ⟶ G}, α.natTrans = β.natTrans → α = β
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableWithinAt.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (f : E → F) (s : Set E)
  (x v : E),
  LineDifferentiableWithinAt 𝕜 f s x v =
    DifferentiableWithinAt 𝕜 (fun t => f (x + t • v)) ((fun t => x + t • v) ⁻¹' s) 0
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
/-- Auxiliary definition for `HasCokernels SemiNormedGrp`.  -/
SemiNormedGrp.isColimitCokernelCocone : {X Y : SemiNormedGrp} → (f : X ⟶ Y) → CategoryTheory.Limits.IsColimit (SemiNormedGrp.cokernelCocone f)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.id_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  (E : J.OneHypercover S) (x : E.I₀),
  (CategoryTheory.CategoryStruct.id E).h₀ x = CategoryTheory.CategoryStruct.id (E.X x)
-- Mathlib.Data.ENat.Lattice
ENat.natCast_sInf : ∀ {s : Set ℕ}, s.Nonempty → ↑(sInf s) = ⨅ a ∈ s, ↑a
-- Init.Data.BitVec.Bitblast
/-- `DivModState` is a structure that maintains the state of recursive `divrem` calls.  -/
BitVec.DivModState : ℕ → Type
-- Mathlib.Order.CompleteLattice.Defs
CompleteLinearOrder.toCompl : {α : Type u_8} → [self : CompleteLinearOrder α] → Compl α
-- Lean.Elab.DefView
Lean.Elab.instNonemptyHeaderProcessedSnapshot : Nonempty Lean.Elab.HeaderProcessedSnapshot
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.map_injective_of_surjOn_or_injective : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q},
  Set.SurjOn ⇑g ↑S ↑T ∨ Function.Injective ⇑k → Function.Injective ⇑g → Function.Injective ⇑(f.map hy k)
-- Mathlib.CategoryTheory.CofilteredSystem
/-- The inverse limit of nonempty finite types is nonempty.

See `nonempty_sections_of_finite_cofiltered_system` for a generalization to cofiltered limits.
That version applies in almost all cases, and the only difference is that this version
allows `J` to be empty.

This may be regarded as a generalization of Kőnig's lemma.
To specialize: given a locally finite connected graph, take `Jᵒᵖ` to be `ℕ` and
`F j` to be length-`j` paths that start from an arbitrary fixed vertex.
Elements of `F.sections` can be read off as infinite rays in the graph.  -/
nonempty_sections_of_finite_inverse_system : ∀ {J : Type u} [inst : Preorder J] [IsDirectedOrder J] (F : CategoryTheory.Functor Jᵒᵖ (Type v))
  [∀ (j : Jᵒᵖ), Finite (F.obj j)] [∀ (j : Jᵒᵖ), Nonempty (F.obj j)], F.sections.Nonempty
-- Mathlib.Algebra.Divisibility.Basic
RightDvd.refl : ∀ {α : Type u_1} [inst : Monoid α] (a : α), a ∣ᵣ a
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.isPrime_map_of_liesOver : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Sₚ : Type u_5) [inst_4 : CommSemiring Sₚ] [inst_5 : Algebra S Sₚ]
  [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] (P : Ideal S) [P.IsPrime] [P.LiesOver p],
  (Ideal.map (algebraMap S Sₚ) P).IsPrime
-- Init.Data.SInt.Lemmas
Int32.toInt8_ofIntClamp : ∀ {n : ℤ}, -2 ^ 31 ≤ n → n < 2 ^ 31 → (Int32.ofIntClamp n).toInt8 = Int8.ofInt n
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.rename_inj : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (e : σ ↪ τ) (p q : MvPowerSeries σ R),
  (MvPowerSeries.rename ⇑e) p = (MvPowerSeries.rename ⇑e) q ↔ p = q
-- Mathlib.RingTheory.Localization.LocalizationLocalization
IsLocalization.mk'_eq_algebraMap_mk'_of_submonoid_le : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] {M N : Submonoid R} (h : M ≤ N) [inst_5 : IsLocalization M S]
  [inst_6 : IsLocalization N T] [inst_7 : Algebra S T] [IsScalarTower R S T] (x : R) (y : ↥M),
  IsLocalization.mk' T x ⟨↑y, ⋯⟩ = (algebraMap S T) (IsLocalization.mk' S x y)
-- Init.Data.SInt.Lemmas
Int8.toInt64_neg_of_ne : ∀ {x : Int8}, x ≠ -128 → (-x).toInt64 = -x.toInt64
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualAnnihilator_iInf_eq : ∀ {K : Type u_1} {V₁ : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁] {ι : Type u_4}
  [Finite ι] (W : ι → Subspace K V₁), Submodule.dualAnnihilator (⨅ i, W i) = ⨆ i, Submodule.dualAnnihilator (W i)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α),
  Std.Internal.List.getValueCast? a [] = none
-- Std.Time.DateTime
/-- Add `Second.Offset` to a `DateTime`.
 -/
Std.Time.DateTime.addSeconds : Std.Time.DateTime → Std.Time.Second.Offset → Std.Time.DateTime
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.inverse_domain : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f : E →ₗ.[R] F}, f.inverse.domain = f.toFun.range
-- Init.Data.SInt.Basic
/-- Converts an 64-bit signed integer into the 64-bit unsigned integer that is its two's complement
encoding.
 -/
Int64.toUInt64 : Int64 → UInt64
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop : {α : Type u_1} → [LinearOrderedAddCommGroupWithTop α] → LinearOrderedCommGroupWithZero (Multiplicative αᵒᵈ)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α}, (Std.TreeMap.filter f t).getKey? k = (t.getKey? k).pfilter fun x h' => f x t[x]
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftId.congr_simp : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso],
  CategoryTheory.MorphismProperty.Comma.mapLeftId L R = CategoryTheory.MorphismProperty.Comma.mapLeftId L R
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.erase.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (x : MonoidAlgebra R M),
  MonoidAlgebra.erase m x = MonoidAlgebra.ofCoeff (Finsupp.erase m x.coeff)
-- Mathlib.Logic.Basic
forall₂_and : ∀ {α : Sort u_1} {p : α → Prop} {P Q : (x : α) → p x → Prop},
  (∀ (x : α) (h : p x), P x h ∧ Q x h) ↔ (∀ (x : α) (h : p x), P x h) ∧ ∀ (x : α) (h : p x), Q x h
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xn_one : ∀ {a : ℕ} (a1 : 1 < a), Pell.xn a1 1 = a
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.checkAltNames : Array Lean.Elab.Tactic.ElimApp.Alt → Array Lean.Syntax → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Topology.PartitionOfUnity
/-- If `f` is a partition of unity on a set `s : Set X` and `g : ι → X → E` is a family of functions
such that each `g i` is continuous at every point of the topological support of `f i`, then the sum
`fun x ↦ ∑ᶠ i, f i x • g i x` is continuous on the whole space.  -/
PartitionOfUnity.continuous_finsum_smul : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {E : Type u_1} [inst_1 : AddCommMonoid E]
  [inst_2 : SMulWithZero ℝ E] [inst_3 : TopologicalSpace E] [ContinuousSMul ℝ E] {s : Set X}
  (f : PartitionOfUnity ι X s) [ContinuousAdd E] {g : ι → X → E},
  (∀ (i : ι), ∀ x ∈ tsupport ⇑(f i), ContinuousAt (g i) x) → Continuous fun x => ∑ᶠ (i : ι), (f i) x • g i x
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_nontrivial : ∀ {α : Type u} {s : Set α} (h : s.Finite), h.toFinset.Nontrivial ↔ s.Nontrivial
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.nonneg : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) (i : ι) (x : X),
  0 ≤ (f i) x
-- Mathlib.CategoryTheory.Limits.Types.Images
CategoryTheory.Limits.Types.instInhabitedImage : {α β : Type u} → (f : α ⟶ β) → [Inhabited α] → Inhabited (CategoryTheory.Limits.Types.Image f)
-- Mathlib.Data.Nat.Log
Nat.add_pred_div_lt : ∀ {b n : ℕ}, 1 < b → 2 ≤ n → (n + b - 1) / b < n
-- Mathlib.Topology.Bornology.Hom
/-- Composition of `LocallyBoundedMap`s as a `LocallyBoundedMap`.  -/
LocallyBoundedMap.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Bornology α] →
        [inst_1 : Bornology β] →
          [inst_2 : Bornology γ] → LocallyBoundedMap β γ → LocallyBoundedMap α β → LocallyBoundedMap α γ
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- The image of a semilinear set under a homomorphism is semilinear.  -/
IsSemilinearSet.image : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_5} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : FunLike F M N] [AddMonoidHomClass F M N] {s : Set M},
  IsSemilinearSet s → ∀ (f : F), IsSemilinearSet (⇑f '' s)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.haarContent.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G),
  MeasureTheory.Measure.haar.haarContent K₀ =
    { toFun := fun K => ⟨MeasureTheory.Measure.haar.chaar K₀ K, ⋯⟩, mono' := ⋯, sup_disjoint' := ⋯, sup_le' := ⋯ }
-- Mathlib.Algebra.Field.Basic
Commute.inv_sub_inv : ∀ {K : Type u_1} [inst : DivisionRing K] {a b : K}, Commute a b → a ≠ 0 → b ≠ 0 → a⁻¹ - b⁻¹ = (b - a) / (a * b)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
IsSemilinearSet.iInter : ∀ {M : Type u_1} {ι : Type u_3} [inst : AddCommMonoid M] [AddMonoid.FG M] [Finite ι] {s : ι → Set M},
  (∀ (i : ι), IsSemilinearSet (s i)) → IsSemilinearSet (⋂ i, s i)
-- Mathlib.Analysis.InnerProductSpace.Calculus
DifferentiableOn.norm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E}
  {s : Set G}, DifferentiableOn ℝ f s → (∀ x ∈ s, f x ≠ 0) → DifferentiableOn ℝ (fun y => ‖f y‖) s
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (M : X.Modules) (U : Y.Opens),
  ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj M).presheaf.obj (Opposite.op U) =
    M.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U))
-- Mathlib.CategoryTheory.Action.Monoidal
Action.diagonalSuccIsoTensorTrivial_hom_hom_apply : ∀ {G : Type u} [inst : Group G] {n : ℕ} (f : Fin (n + 1) → G),
  (CategoryTheory.ConcreteCategory.hom (Action.diagonalSuccIsoTensorTrivial G n).hom.hom) f =
    (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iic_bot : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : OrderBot α], Finset.Iic ⊥ = {⊥}
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.id_map : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] (C : Type u₁)
  [inst_2 : CategoryTheory.EnrichedCategory V C] (x x_1 : C),
  (CategoryTheory.EnrichedFunctor.id V C).map x x_1 = CategoryTheory.CategoryStruct.id (x ⟶[V] x_1)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.getVert_endpoint_iff : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {i : ℕ} {p : G.Walk u u},
  p.IsCycle → i ≤ p.length → (p.getVert i = u ↔ i = 0 ∨ i = p.length)
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.getStarResult : {α : Type} → Lean.Meta.DiscrTree α → Array α
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- Given an edge incident to a particular vertex, get the other vertex on the edge.  -/
SimpleGraph.otherVertexOfIncident : {V : Type u} → (G : SimpleGraph V) → [DecidableEq V] → {v : V} → {e : Sym2 V} → e ∈ G.incidenceSet v → V
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State.funBinders : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.State → Array Bool
-- Mathlib.Order.Filter.Basic
Filter.sdiff_mem_inf_principal_compl : ∀ {α : Type u} {f : Filter α} {s : Set α}, s ∈ f → ∀ (t : Set α), s \ t ∈ f ⊓ Filter.principal tᶜ
-- Mathlib.Data.Set.Lattice
Set.iUnion₂_congr : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s t : (i : ι) → κ i → Set α},
  (∀ (i : ι) (j : κ i), s i j = t i j) → ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, t i j
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.add_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X : C} [inst_2 : CategoryTheory.AddMonObj M] (f₁ f₂ : X ⟶ M),
  f₁ + f₂ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂)
      CategoryTheory.AddMonObj.add
-- Std.Time.Date.Unit.Week
/-- Creates an `Offset` from an integer.
 -/
Std.Time.Week.Offset.ofInt : ℤ → Std.Time.Week.Offset
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.mk.sizeOf_spec : ∀ {α : Type u_5} [inst : SizeOf α] (toField : Field α)
  (toConditionallyCompleteLinearOrder : ConditionallyCompleteLinearOrder α)
  [toIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid α] [toZeroLEOneClass : ZeroLEOneClass α]
  [toPosMulStrictMono : PosMulStrictMono α] [toMulPosStrictMono : MulPosStrictMono α],
  sizeOf
      { toField := toField, toConditionallyCompleteLinearOrder := toConditionallyCompleteLinearOrder,
        toIsOrderedCancelAddMonoid := toIsOrderedCancelAddMonoid, toZeroLEOneClass := toZeroLEOneClass,
        toPosMulStrictMono := toPosMulStrictMono, toMulPosStrictMono := toMulPosStrictMono } =
    1 + sizeOf toField + sizeOf toConditionallyCompleteLinearOrder + sizeOf toIsOrderedCancelAddMonoid +
          sizeOf toZeroLEOneClass +
        sizeOf toPosMulStrictMono +
      sizeOf toMulPosStrictMono
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If there exists a primitive root of unity of order `n` in `B`, then
`IsCyclotomicExtension S A B` implies `IsCyclotomicExtension (S ∪ {n}) A B`.  -/
IsCyclotomicExtension.union_of_isPrimitiveRoot : ∀ {n : ℕ} [NeZero n] (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [hB : IsCyclotomicExtension S A B] {r : B},
  IsPrimitiveRoot r n → IsCyclotomicExtension (S ∪ {n}) A B
-- Mathlib.Computability.Language
Language.kstar_def : ∀ {α : Type u_1} (l : Language α), KStar.kstar l = {x | ∃ L, x = L.flatten ∧ ∀ y ∈ L, y ∈ l}
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.collectUnassignedMVars.go : (Lean.MVarId → Bool) → List Lean.MVarId → Array Lean.Expr → Array Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)
-- Std.Data.DTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.DTreeMap.Const.entryAtIdx! : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap α (fun x => β) cmp → ℕ → α × β