mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.comp_homologySequenceδ : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological] [inst_9 : F.ShiftSequence ℤ],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
      CategoryTheory.CategoryStruct.comp ((F.shift n₀).map T.mor₂) (F.homologySequenceδ T n₀ n₁ h) = 0
-- Mathlib.Order.Category.Preord
Preord.Hom.ext : ∀ {X Y : Preord} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Makes an ordered group homomorphism from a proof that the map preserves multiplication.  -/
OrderMonoidHom.mk' : {α : Type u_2} →
  {β : Type u_3} →
    {x : CommGroup α} →
      {x_1 : Preorder α} →
        {x_2 : CommGroup β} →
          {x_3 : PartialOrder β} → (f : α → β) → Monotone f → (∀ (a b : α), f (a * b) = f a * f b) → α →*o β
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.toDerivation_injective : ∀ {𝕜 : 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],
  Function.Injective LeftInvariantDerivation.toDerivation
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.impFrom : Lean.Parser.Parser
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- The measure equivalence between `EuclideanSpace ℝ ι` and `ι → ℝ` is volume preserving.  -/
EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp : ∀ (ι : Type u_4) [inst : Fintype ι],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)).symm) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.IsAddModHom.map_vadd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] {X : C} [inst_3 : CategoryTheory.AddModObj M X] {Y : C}
  [inst_4 : CategoryTheory.AddModObj M Y] (f : X ⟶ Y) [CategoryTheory.IsAddModHom M f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X)
  {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (m +ᵥ x) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (m +ᵥ CategoryTheory.CategoryStruct.comp x f) h
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.instLocallyConnectedSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [LocallyConnectedSpace α],
  LocallyConnectedSpace (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.instFaithfulIncl : FintypeCat.incl.Faithful
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.instRingEnd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Preadditive C] → {X : C} → Ring (CategoryTheory.End X)
-- Mathlib.Computability.Reduce
manyOneReducible_toNat : ∀ {α : Type u} [inst : Primcodable α] [inst_1 : Inhabited α] {p : Set α}, p ≤₀ toNat p
-- Mathlib.Tactic.NormNum.NatFactorial
_private.Mathlib.Tactic.NormNum.NatFactorial.0.Mathlib.Meta.NormNum.evalNatDescFactorialZero : {x' y' : Q(ℕ)} →
  (x y z : Q(ℕ)) →
    «$y» =Q «$z» + «$x» + 1 →
      Q(Mathlib.Meta.NormNum.IsNat «$x'» «$x») →
        Q(Mathlib.Meta.NormNum.IsNat «$y'» «$y») →
          (n : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNat («$x'».descFactorial «$y'») «$n»)
-- Mathlib.Data.Complex.Basic
Complex.reProdIm.eq_1 : ∀ (s t : Set ℝ), s ×ℂ t = Complex.re ⁻¹' s ∩ Complex.im ⁻¹' t
-- Init.Data.Int.Lemmas
Int.sub_sub_self : ∀ (a b : ℤ), a - (a - b) = b
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The unit object is always closed.
This isn't an instance because most of the time we'll prove closedness for all objects at once,
rather than just for this one.
 -/
CategoryTheory.unitClosed : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.Lie.Loop
/-- A 2-cochain on a loop algebra given by an invariant bilinear form. When `A = ℤ`, the alternating
condition amounts to the fact that Res f df = 0.  -/
LieAlgebra.LoopAlgebra.twoCochainOfBilinear : (R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : CommRing A] →
              [IsAddTorsionFree R] →
                [Algebra A R] →
                  (Φ : LinearMap.BilinForm R L) →
                    Φ.IsSymm →
                      ↥(LieModule.Cohomology.twoCochain R (LieAlgebra.loopAlgebra R A L)
                          (TrivialLieModule R (LieAlgebra.loopAlgebra R A L) R))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.zero_neg_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.AddGrpObj G] {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The natural bijection between `α → Π i, δ i` and `Π i, α → δ i`, upgraded to a uniform
isomorphism between `α →ᵤ[𝔖] (Π i, δ i)` and `Π i, α →ᵤ[𝔖] δ i`.  -/
UniformOnFun.uniformEquivPiComm : {α : Type u_1} →
  {ι : Type u_4} →
    (𝔖 : Set (Set α)) →
      (δ : ι → Type u_5) →
        [inst : (i : ι) → UniformSpace (δ i)] → UniformOnFun α ((i : ι) → δ i) 𝔖 ≃ᵤ ((i : ι) → UniformOnFun α (δ i) 𝔖)
-- Mathlib.Data.Fintype.Pi
Fintype.piFinset_subset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} (t₁ t₂ : (a : α) → Finset (δ a)),
  (∀ (a : α), t₁ a ⊆ t₂ a) → Fintype.piFinset t₁ ⊆ Fintype.piFinset t₂
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_add_atTop_iff_nat : ∀ {α : Type u_3} {f : ℕ → α} {l : Filter α} (k : ℕ),
  Filter.Tendsto (fun n => f (n + k)) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.mem_iInf_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Sort u_4} (s : ι → AffineSubspace k P) (p : P), p ∈ iInf s ↔ ∀ (i : ι), p ∈ s i
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableAt_comp_add_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} (a : E), DifferentiableAt 𝕜 (fun x => f (a + x)) x ↔ DifferentiableAt 𝕜 f (a + x)
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with
`[ContinuousAdd]`. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to `EReal`.  -/
LowerSemicontinuousAt.add : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_5} [inst_1 : AddCommMonoid γ] [inst_2 : LinearOrder γ]
  [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ] {f g : α → γ},
  LowerSemicontinuousAt f x → LowerSemicontinuousAt g x → LowerSemicontinuousAt (fun z => f z + g z) x
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.parseFirstByte : UInt8 → ByteArray.utf8DecodeChar?.FirstByte
-- Mathlib.Data.Sym.Basic
/-- Change the length of a `Sym` using an equality.
The simp-normal form is for the `cast` to be pushed outward.  -/
Sym.cast : {α : Type u_1} → {n m : ℕ} → n = m → Sym α n ≃ Sym α m
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- For an open immersion `f : X ⟶ Y` and an open set `U ⊆ X`, we have the map `X(U) ⟶ Y(U)`.  -/
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : AlgebraicGeometry.SheafedSpace C} →
      (f : X ⟶ Y) →
        [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] →
          (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) →
            X.presheaf.obj (Opposite.op U) ⟶
              Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).obj U))
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereo_right_inv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) (w : ↥(ℝ ∙ v)ᗮ),
  stereoToFun v ↑(stereoInvFun hv w) = w
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.continuousAt_equivIoc : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜]
  {x : AddCircle p}, x ≠ ↑a → ContinuousAt (⇑(AddCircle.equivIoc p a)) x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.braiding_inv_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).inv s.snd = t.fst
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- Two partial maps are equivalent if they are equal on a dense open subscheme.  -/
AlgebraicGeometry.Scheme.PartialMap.equiv : {X Y : AlgebraicGeometry.Scheme} → X.PartialMap Y → X.PartialMap Y → Prop
-- Mathlib.Algebra.Group.Pi.Basic
Pi.divisionMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → DivisionMonoid (f i)] → DivisionMonoid ((i : I) → f i)
-- Lean.Declaration
Lean.QuotVal.kindEx : Lean.QuotVal → Lean.QuotKind
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Functor.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (obj : C → D) (map map_1 : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (e_map : map = map_1)
  (map_id : ∀ (X : C), map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj X))
  (map_comp :
    ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
      map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map f) (map g)),
  { obj := obj, map := map, map_id := map_id, map_comp := map_comp } =
    { obj := obj, map := map_1, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.HigherFacesVanish.on_Γ₀_summand_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) (n : ℕ),
  AlgebraicTopology.DoldKan.HigherFacesVanish (n + 1)
    (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op { len := n + 1 })).inj
      (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n + 1 })))
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.orbit_eq_univ : ∀ (M : Type u) [inst : Monoid M] {α : Type v} [inst_1 : MulAction M α] [MulAction.IsPretransitive M α] (a : α),
  MulAction.orbit M a = Set.univ
-- Mathlib.Algebra.Order.Hom.Monoid
/-- An `OrderAddMonoidHom` is a monotone function.  -/
OrderAddMonoidHom.monotone' : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (self : α →+o β), Monotone (↑self.toAddMonoidHom).toFun
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_sup_right : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N N' : LieSubmodule R L M} {x : M}, x ∈ N' → x ∈ N ⊔ N'
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Iter.forIn'_eq_match_step.match_3.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out h
-- Lean.Meta.Match.CaseArraySizes
_private.Lean.Meta.Match.CaseArraySizes.0.Lean.Meta.introArrayLit : Lean.MVarId → Lean.Expr → ℕ → Lean.Name → Lean.Expr → Lean.MetaM Lean.MVarId
-- Mathlib.Order.Interval.Finset.Defs
WithBot.instLocallyFiniteOrder : (α : Type u_1) → [inst : PartialOrder α] → [OrderBot α] → [LocallyFiniteOrder α] → LocallyFiniteOrder (WithBot α)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  (Std.Internal.List.insertEntryIfNew k v l).isEmpty = false
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.toContinuousAffineEquiv_inj : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] {f g : P ≃ᵃⁱ[𝕜] P₂},
  f.toContinuousAffineEquiv = g.toContinuousAffineEquiv ↔ f = g
-- Mathlib.CategoryTheory.Action.Continuous
/-- Restriction of scalars along a topological monoid isomorphism induces an equivalence of
categories.  -/
ContAction.resEquiv : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
              {G : Type u_4} →
                [inst_4 : Monoid G] →
                  [inst_5 : TopologicalSpace G] →
                    {H : Type u_5} →
                      [inst_6 : Monoid H] → [inst_7 : TopologicalSpace H] → G ≃ₜ* H → (ContAction V H ≌ ContAction V G)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt32.reduceMod : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.Set.Disjoint
Disjoint.subset_left_of_subset_union : ∀ {α : Type u_1} {s t u : Set α}, s ⊆ t ∪ u → Disjoint s u → s ⊆ t
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.realize_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ ψ : L.Formula α} {M : Type u_2} [Nonempty M]
  [inst : L.Structure M] [M ⊨ T], T.Iff φ ψ → ∀ {v : α → M}, φ.Realize v ↔ ψ.Realize v
-- Mathlib.Order.Interval.Set.Basic
Set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α} {s : Set α},
  Set.Ioo a b ⊆ s → s ⊆ Set.Icc a b → s ∈ {Set.Icc a b, Set.Ico a b, Set.Ioc a b, Set.Ioo a b}
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.max_rpow : ∀ {x y : ENNReal} {p : ℝ}, 0 ≤ p → max x y ^ p = max (x ^ p) (y ^ p)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.isoMk_hom_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e₁ : S₁.X₁ ≅ S₂.X₁) (e₂ : S₁.X₂ ≅ S₂.X₂) (e₃ : S₁.X₃ ≅ S₂.X₃)
  (comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom)
      CategoryTheory.ShortComplex.isoMk._auto_1)
  (comm₂₃ :
    autoParam (CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom)
      CategoryTheory.ShortComplex.isoMk._auto_3),
  (CategoryTheory.ShortComplex.isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).hom.τ₁ = e₁.hom
-- Mathlib.Analysis.Normed.Group.Bounded
Bornology.IsBounded.exists_pos_norm_le' : ∀ {E : Type u_2} [inst : SeminormedGroup E] {s : Set E}, Bornology.IsBounded s → ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.HasCoreflexiveEqualizers.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ ⦃A B : C⦄ (f g : A ⟶ B) [CategoryTheory.IsCoreflexivePair f g], CategoryTheory.Limits.HasEqualizer f g) →
    CategoryTheory.Limits.HasCoreflexiveEqualizers C
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.smul_def : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {i : ι} (m : M i) (w : Monoid.CoprodI.Word M),
  m • w =
    Monoid.CoprodI.Word.rcons
      (have __src := (Monoid.CoprodI.Word.equivPair i) w;
      { head := m * ((Monoid.CoprodI.Word.equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯ })
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuousAt.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : TopologicalSpace β] {f : α → Set β} {g : γ → α} {c : γ},
  UpperHemicontinuousAt f (g c) → ContinuousAt g c → UpperHemicontinuousAt (f ∘ g) c
-- Mathlib.CategoryTheory.Sites.Hypercover.One
_private.Mathlib.CategoryTheory.Sites.Hypercover.One.0.CategoryTheory.PreOneHypercover.Hom.mapMulticospan.match_3.splitter : {C : Type u_3} →
  [inst : CategoryTheory.Category.{u_2, u_3} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        (motive : (X Y : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape) → (X ⟶ Y) → Sort u_4) →
          (X Y : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape) →
            (x : X ⟶ Y) →
              ((x : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape) →
                  motive x x (CategoryTheory.Limits.WalkingMulticospan.Hom.id x)) →
                ((i : E.multicospanShape.R) →
                    motive (CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.fst i))
                      (CategoryTheory.Limits.WalkingMulticospan.right i)
                      (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i)) →
                  ((i : E.multicospanShape.R) →
                      motive (CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.snd i))
                        (CategoryTheory.Limits.WalkingMulticospan.right i)
                        (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i)) →
                    motive X Y x
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.piCongrLeft'_apply : ∀ (R : Type u) {ι : Type x} {ι' : Type x'} [inst : Semiring R] (φ : ι → Type u_1)
  [inst_1 : (i : ι) → AddCommMonoid (φ i)] [inst_2 : (i : ι) → Module R (φ i)] (e : ι ≃ ι') (a : (a : ι) → φ a)
  (b : ι'), (LinearEquiv.piCongrLeft' R φ e) a b = a (e.symm b)
-- Mathlib.MeasureTheory.Measure.TightNormed
/-- In a proper normed group, a set of measures `S` is tight if and only if
the function `r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}` tends to `0` at infinity.  -/
MeasureTheory.isTightMeasureSet_iff_tendsto_measure_norm_gt : ∀ {E : Type u_1} {mE : MeasurableSpace E} {S : Set (MeasureTheory.Measure E)} [inst : NormedAddCommGroup E]
  [ProperSpace E],
  MeasureTheory.IsTightMeasureSet S ↔ Filter.Tendsto (fun r => ⨆ μ ∈ S, μ {x | r < ‖x‖}) Filter.atTop (nhds 0)
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The completed L-function of the (unique) Dirichlet character mod 1 is the completed Riemann zeta
function.
 -/
DirichletCharacter.completedLFunction_modOne_eq : ∀ {χ : DirichletCharacter ℂ 1}, DirichletCharacter.completedLFunction χ = completedRiemannZeta
-- Aesop.Frontend.Extension.Init
/-- The collection of declared rule sets. Each rule set has an extension, the
name of the associated `SimpExtension` and the name of the associated
`SimprocExtension`. The two simp extensions are expected to be declared.
 -/
Aesop.DeclaredRuleSets.ruleSets : Aesop.DeclaredRuleSets → Std.HashMap Aesop.RuleSetName (Aesop.RuleSetExtension × Lean.Name × Lean.Name)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.aleph0_mul_aleph : ∀ (o : Ordinal.{u_1}), Cardinal.aleph0 * Cardinal.aleph o = Cardinal.aleph o
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.ihom_obj : ∀ (K : Type u) [inst : Field K] (V W : FGModuleCat K), (V ⟹ W) = FGModuleCat.of K (V.obj ⟶ W.obj)
-- Init.Grind.ToIntLemmas
_private.Init.Grind.ToIntLemmas.0.Lean.Grind.IntInterval.lo?.match_1.eq_3 : ∀ (motive : Lean.Grind.IntInterval → Sort u_1) (hi : ℤ) (h_1 : (lo hi : ℤ) → motive (Lean.Grind.IntInterval.co lo hi))
  (h_2 : (lo : ℤ) → motive (Lean.Grind.IntInterval.ci lo)) (h_3 : (hi : ℤ) → motive (Lean.Grind.IntInterval.io hi))
  (h_4 : Unit → motive Lean.Grind.IntInterval.ii),
  (match Lean.Grind.IntInterval.io hi with
    | Lean.Grind.IntInterval.co lo hi => h_1 lo hi
    | Lean.Grind.IntInterval.ci lo => h_2 lo
    | Lean.Grind.IntInterval.io hi => h_3 hi
    | Lean.Grind.IntInterval.ii => h_4 ()) =
    h_3 hi
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get!_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ \ m₂).get! k = default
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec` is fully faithful on `R`-Hopf algebras, with inverse `Gamma`.  -/
AlgebraicGeometry.hopfSpec.fullyFaithful : {R : CommRingCat} → (AlgebraicGeometry.hopfSpec R).FullyFaithful
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.SpecialLinear.sl_bracket : ∀ (n : Type u_1) (R : Type u₂) [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (A B : ↥(LieAlgebra.SpecialLinear.sl n R)), ↑⁅A, B⁆ = ↑A * ↑B - ↑B * ↑A
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The adjoint of the composition of two operators is the composition of the two adjoints
in reverse order.  -/
LinearMap.adjoint_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 E]
  [inst_5 : InnerProductSpace 𝕜 F] [inst_6 : InnerProductSpace 𝕜 G] [inst_7 : FiniteDimensional 𝕜 E]
  [inst_8 : FiniteDimensional 𝕜 F] [inst_9 : FiniteDimensional 𝕜 G] (A : F →ₗ[𝕜] G) (B : E →ₗ[𝕜] F),
  LinearMap.adjoint (A ∘ₗ B) = LinearMap.adjoint B ∘ₗ LinearMap.adjoint A
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.homRel.map_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.FreeGroupoid.homRel C ((Quiver.FreeGroupoid.of C).map (CategoryTheory.CategoryStruct.id X))
    (CategoryTheory.CategoryStruct.id ((Quiver.FreeGroupoid.of C).obj X))
-- Std.Http.Data.URI.Encoding
/-- The underlying byte array containing the percent-encoded data.
 -/
Std.Http.URI.EncodedString.toByteArray : {r : UInt8 → Bool} → Std.Http.URI.EncodedString r → ByteArray
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOn.curry_left : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G} {s : Set (E × F)} {y : F},
  AnalyticOn 𝕜 f s → AnalyticOn 𝕜 (fun x => f (x, y)) {x | (x, y) ∈ s}