mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.ArgsPacker
/-- Given types `(x : A) → R₁[x]` and `(z : B) → R₂[z]`, returns the type
```
(x : A ⊕' B) → (match x with | .inl x => R₁[x] | .inr R₂[z]
```
if the codomains are dependent, or
```
(x : A ⊕' B) → R
```
if they are all the same.

 -/
Lean.Meta.ArgsPacker.Mutual.uncurryType : Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Ring.Equiv
/-- The inverse of a ring isomorphism is a ring isomorphism.  -/
RingEquiv.symm : {R : Type u_4} →
  {S : Type u_5} → [inst : Mul R] → [inst_1 : Mul S] → [inst_2 : Add R] → [inst_3 : Add S] → R ≃+* S → S ≃+* R
-- Mathlib.RingTheory.Ideal.Maps
Ideal.mem_map_of_equiv : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {E : Type u_4} [inst_2 : EquivLike E R S]
  [RingEquivClass E R S] (e : E) {I : Ideal R} (y : S), y ∈ Ideal.map e I ↔ ∃ x ∈ I, e x = y
-- Init.Data.AC
Lean.Data.AC.Expr.toList : Lean.Data.AC.Expr → List ℕ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.mk : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol → Lean.Lsp.DocumentSymbol
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.BoundedFormula.freeVarFinset.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (_n : ℕ)
  (t₁ t₂ : L.Term (α ⊕ Fin _n)) (h_1 : (_n : ℕ) → motive _n FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (_n : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin _n)) → motive _n (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (_n l : ℕ) →
      (_R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin _n)) → motive _n (FirstOrder.Language.BoundedFormula.rel _R ts))
  (h_4 : (_n : ℕ) → (f₁ f₂ : L.BoundedFormula α _n) → motive _n (f₁.imp f₂))
  (h_5 : (_n : ℕ) → (f : L.BoundedFormula α (_n + 1)) → motive _n f.all),
  (match _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂ with
    | _n, FirstOrder.Language.BoundedFormula.falsum => h_1 _n
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 _n t₁ t₂
    | _n, FirstOrder.Language.BoundedFormula.rel _R ts => h_3 _n l _R ts
    | _n, f₁.imp f₂ => h_4 _n f₁ f₂
    | _n, f.all => h_5 _n f) =
    h_2 _n t₁ t₂
-- Mathlib.LinearAlgebra.Multilinear.Curry
/-- Given a family of modules `N : (ι ⊕ ι') → Type*`, a multilinear map
on `(fun _ : ι ⊕ ι' => M')` induces a multilinear map on
`(fun (i : ι) ↦ N (.inl i))` taking values in the space of
linear maps on `(fun (i : ι') ↦ N (.inr i))`.  -/
MultilinearMap.currySum : {R : Type uR} →
  {ι : Type uι} →
    {ι' : Type uι'} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₂] →
            [inst_2 : Module R M₂] →
              {N : ι ⊕ ι' → Type u_1} →
                [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)] →
                  [inst_4 : (i : ι ⊕ ι') → Module R (N i)] →
                    MultilinearMap R N M₂ →
                      MultilinearMap R (fun i => N (Sum.inl i)) (MultilinearMap R (fun i => N (Sum.inr i)) M₂)
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CompletelyPositiveMap.toLinearMap : {A₁ : Type u_1} →
  {A₂ : Type u_2} →
    [inst : NonUnitalCStarAlgebra A₁] →
      [inst_1 : NonUnitalCStarAlgebra A₂] →
        [inst_2 : PartialOrder A₁] →
          [inst_3 : PartialOrder A₂] →
            [inst_4 : StarOrderedRing A₁] → [inst_5 : StarOrderedRing A₂] → CompletelyPositiveMap A₁ A₂ → A₁ →ₗ[ℂ] A₂
-- Mathlib.Order.Completion
DedekindCut.factorEmbedding.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : PartialOrder β] (f : β ↪o α),
  DedekindCut.factorEmbedding f = OrderEmbedding.ofMapLEIff (fun A => sSup (⇑f '' A.left)) ⋯
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cokernelIsoCycles_hom_fac : ∀ {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) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.π ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)))
      (CategoryTheory.CategoryStruct.comp (X.cokernelIsoCycles f g fg h n).hom (X.iCycles f g n)) =
    (X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- The diagram presenting `A`.  -/
CategoryTheory.IndParallelPairPresentation.F₁ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} → (self : CategoryTheory.IndParallelPairPresentation f g) → CategoryTheory.Functor self.I C
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- For a presheaf `P`, consider the forgetful functor from the category of representable
presheaves over `P` to the category of presheaves. There is a tautological cocone over this
functor whose leg for a natural transformation `V ⟶ P` with `V` representable is just that
natural transformation. (In this version, we allow the presheaf `P` to have values in
a larger universe.)  -/
CategoryTheory.Presheaf.tautologicalCocone' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))) →
      CategoryTheory.Limits.Cocone
        ((CategoryTheory.CostructuredArrow.proj CategoryTheory.uliftYoneda.{w, v₁, u₁} P).comp
          CategoryTheory.uliftYoneda.{w, v₁, u₁})
-- Mathlib.Algebra.Category.Grp.Yoneda
/-- The Hom bifunctor sending a type `X` and a commutative group `G` to the commutative group
`X → G` with pointwise operations.

This is also the coyoneda embedding of `Type` into `AddCommGrpCat`-valued presheaves of commutative
groups.  -/
AddCommGrpCat.coyonedaType : CategoryTheory.Functor Type uᵒᵖ (CategoryTheory.Functor AddCommGrpCat AddCommGrpCat)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.hasDerivAt_arccos : ∀ {x : ℝ}, x ≠ -1 → x ≠ 1 → HasDerivAt Real.arccos (-(1 / √(1 - x ^ 2))) x
-- Mathlib.Algebra.Category.MonCat.Limits
/-- `limit.π (F ⋙ forget MonCat) j` as a `MonoidHom`.  -/
MonCat.limitπMonoidHom : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J MonCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] →
        (j : J) → (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget MonCat))).pt →* ↑(F.obj j)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] (g : β → γ)
  (f : MeasureTheory.SimpleFunc α β), ⇑(MeasureTheory.SimpleFunc.map g f) = g ∘ ⇑f
-- Init.Data.List.Lemmas
List.dropLast_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α}, (List.replicate n a).dropLast = List.replicate (n - 1) a
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.pOpcycles_opcyclesIsoSc'_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology] {Z : C} (h : (K.sc' i j k).opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.pOpcycles j)
      (CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).hom h) =
    CategoryTheory.CategoryStruct.comp (K.sc' i j k).pOpcycles h
-- Lean.Server.References
/-- Parent declaration of an identifier.  -/
Lean.Server.References.ParentDecl : Type
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.Even.toUnitHom_eval_neg_one : ∀ {S : Type u_2} [inst : CommRing S] {m : ℕ} (ψ : DirichletCharacter S m), ψ.Even → (MulChar.toUnitHom ψ) (-1) = 1
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mem_inf : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I},
  J ∈ π₁ ⊓ π₂ ↔ ∃ J₁ ∈ π₁, ∃ J₂ ∈ π₂, ↑J = ↑J₁ ⊓ ↑J₂
-- Init.Data.Nat.Lemmas
Nat.le_of_mod_lt : ∀ {a b : ℕ}, a % b < a → b ≤ a
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.IsZeroOrProbabilityMeasure.measure_univ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [self : MeasureTheory.IsZeroOrProbabilityMeasure μ], μ Set.univ = 0 ∨ μ Set.univ = 1
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.instInhabitedEqCnstrProof : Inhabited Lean.Meta.Grind.AC.EqCnstrProof
-- Mathlib.Algebra.Group.Basic
eq_zero_sub_of_add_eq_zero_left : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a b : α}, b + a = 0 → b = 0 - a
-- Mathlib.Algebra.Group.Action.TypeTags
toMul_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] (a : Additive α) (b : β), Additive.toMul a • b = a +ᵥ b
-- Mathlib.CategoryTheory.EqToHom
/-- Proving equality between functors. This isn't an extensionality lemma,
because usually you don't really want to do this.  -/
CategoryTheory.Functor.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h_obj : ∀ (X : C), F.obj X = G.obj X),
  autoParam
      (∀ (X Y : C) (f : X ⟶ Y),
        F.map f =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.eqToHom ⋯)))
      CategoryTheory.Functor.ext._auto_1 →
    F = G
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizer.condition : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) g
-- Init.Data.Array.Attach
_private.Init.Data.Array.Attach.0.Array.unattach.eq_1 : ∀ {α : Type u_1} {p : α → Prop} (xs : Array { x // p x }), xs.unattach = Array.map (fun x => ↑x) xs
-- Std.Http.Protocol.H1
/-- Consumes fixed-length body bytes, yielding complete or partial segments.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.parseFixedBody : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir →
    ℕ → Std.Http.Protocol.H1.Machine dir × Option Std.Http.Protocol.H1.PulledChunk × Bool
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_coe_unitary : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Algebra ℝ A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (U : ↥(unitary A)), CFC.abs ↑U = 1
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.em.injEq : ∀ (classical : Bool) (p : Lean.Name) (classical_1 : Bool) (p_1 : Lean.Name),
  (Mathlib.Tactic.ITauto.Proof.em classical p = Mathlib.Tactic.ITauto.Proof.em classical_1 p_1) =
    (classical = classical_1 ∧ p = p_1)
-- Mathlib.CategoryTheory.DifferentialObject
/-- The identity morphism of a differential object.  -/
CategoryTheory.DifferentialObject.Hom.id : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] → (X : CategoryTheory.DifferentialObject S C) → X.Hom X
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.cocone_pt : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantFrom i₀) [inst_2 : CategoryTheory.IsFiltered J], h.cocone.pt = F.obj i₀
-- Mathlib.Topology.Maps.Strict.Module
/-- The product (in the sense of `LinearMap.prodMap`) of strict linear maps is strict.  -/
LinearMap.isStrictMap_prodMap : ∀ {R : Type u_1} {M : Type u_3} {Nₗ : Type u_5} {M' : Type u_6} {Nₗ' : Type u_7} [inst : Ring R]
  [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup Nₗ] [inst_3 : AddCommGroup M'] [inst_4 : AddCommGroup Nₗ']
  [inst_5 : Module R M] [inst_6 : Module R Nₗ] [inst_7 : Module R M'] [inst_8 : Module R Nₗ'] {fₗ : M →ₗ[R] Nₗ}
  {gₗ : M' →ₗ[R] Nₗ'} [inst_9 : TopologicalSpace M] [inst_10 : TopologicalSpace Nₗ] [IsTopologicalAddGroup M]
  [inst_12 : TopologicalSpace M'] [IsTopologicalAddGroup M'] [inst_14 : TopologicalSpace Nₗ'],
  Topology.IsStrictMap ⇑fₗ → Topology.IsStrictMap ⇑gₗ → Topology.IsStrictMap ⇑(fₗ.prodMap gₗ)
-- Mathlib.GroupTheory.Congruence.Basic
/-- Given types with multiplications `M, N`, the product of two congruence relations `c` on `M` and
`d` on `N`: `(x₁, x₂), (y₁, y₂) ∈ M × N` are related by `c.prod d` iff `x₁` is related to `y₁`
by `c` and `x₂` is related to `y₂` by `d`.  -/
Con.prod : {M : Type u_1} → {N : Type u_2} → [inst : Mul M] → [inst_1 : Mul N] → Con M → Con N → Con (M × N)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.map_refl : ∀ {α : Type u_1} [inst : Preorder α], UpperSet.map (OrderIso.refl α) = OrderIso.refl (UpperSet α)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_indicator_index_eq_prod_attach : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {s : Finset α}
  (f : (a : α) → a ∈ s → M) {h : α → M → N},
  (∀ a ∈ s, h a 0 = 1) → (Finsupp.indicator s f).prod h = ∏ x ∈ s.attach, h (↑x) (f ↑x ⋯)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_iff_isSome_getElem? : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, a ∈ m ↔ m[a]?.isSome = true
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.comm₄_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) {Z : C}
  (h : (CategoryTheory.shiftFunctor C 1).obj X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp w₁₃
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map u₁₂) h) =
    CategoryTheory.CategoryStruct.comp self.m₃ (CategoryTheory.CategoryStruct.comp w₂₃ h)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.eq_of_le_of_le : ∀ {ι : Type u_1} {I J J₁ J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I),
  J₁ ∈ π → J₂ ∈ π → J ≤ J₁ → J ≤ J₂ → J₁ = J₂
-- Mathlib.Topology.Compactness.CountablyCompact
/-- In a Hereditarily Lindelöf space, a countably compact set is compact.  -/
IsCountablyCompact.isCompact : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E} [HereditarilyLindelofSpace E],
  IsCountablyCompact A → IsCompact A
-- Mathlib.Algebra.Module.Submodule.Map
/-- A linear isomorphism induces an order isomorphism of submodules.  -/
Submodule.orderIsoMapComapOfBijective : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} →
                      [RingHomSurjective σ₁₂] →
                        (f : M →ₛₗ[σ₁₂] M₂) → Function.Bijective ⇑f → Submodule R M ≃o Submodule R₂ M₂
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_reindex : ∀ {X : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace R] {A : X → Matrix l n R},
  Continuous A → ∀ (e₁ : l ≃ m) (e₂ : n ≃ p), Continuous fun x => (Matrix.reindex e₁ e₂) (A x)
-- Mathlib.NumberTheory.LSeries.Nonvanishing
DirichletCharacter.LSeriesSummable_zetaMul : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ}, 1 < s.re → LSeriesSummable (⇑χ.zetaMul) s
-- Mathlib.AlgebraicGeometry.Sites.Small
/-- If `P` and `Q` are morphism properties with `P ≤ Q`, this is the Grothendieck topology
induced via the forgetful functor `Q.Over ⊤ S ⥤ Over S` by the topology defined by `P`.  -/
AlgebraicGeometry.Scheme.smallGrothendieckTopology : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme →
  {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
    (S : AlgebraicGeometry.Scheme) → CategoryTheory.GrothendieckTopology (Q.Over ⊤ S)
-- Init.Data.List.Basic
List.Perm.below.cons : ∀ {α : Type u} {motive : (a a_1 : List α) → a.Perm a_1 → Prop} (x : α) {l₁ l₂ : List α} (a : l₁.Perm l₂),
  List.Perm.below a → motive l₁ l₂ a → List.Perm.below ⋯
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instPow.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Monoid β]
  [inst_3 : ContinuousMul β], ContinuousMap.instPow = { pow := fun f n => { toFun := ⇑f ^ n, continuous_toFun := ⋯ } }
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
BialgEquiv.toHopfAlgIso_inv : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : Ring X] [inst_2 : Ring Y] [inst_3 : HopfAlgebra R X]
  [inst_4 : HopfAlgebra R Y] (e : X ≃ₐc[R] Y), e.toHopfAlgIso.inv = HopfAlgCat.ofHom ↑e.symm
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.two_two : NNReal.HolderConjugate 2 2
-- Mathlib.Data.Setoid.Basic
/-- The second isomorphism theorem for sets.  -/
Setoid.comapQuotientEquiv : {α : Type u_1} →
  {β : Type u_2} → (f : α → β) → (r : Setoid β) → Quotient (Setoid.comap f r) ≃ ↑(Set.range (Quotient.mk'' ∘ f))
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
Rep.comp_eq_zero : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (M : Rep.{u, u, u} R G),
  CategoryTheory.CategoryStruct.comp (groupHomology.d₁₀ M) (Rep.Hom.toModuleCatHom M.norm) = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.instInhabitedSubtypeIsElliptic : {F : Type u_2} → [inst : Field F] → [DecidableEq F] → Inhabited { W // W.IsElliptic }
-- Mathlib.Data.Seq.Defs
_private.Mathlib.Data.Seq.Defs.0.Stream'.Seq.BisimO.match_1.eq_3 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 α) → Option (Stream'.Seq1 α) → Sort u_2)
  (x x_1 : Option (Stream'.Seq1 α)) (h_1 : Unit → motive none none)
  (h_2 : (a : α) → (s : Stream'.Seq α) → (a' : α) → (s' : Stream'.Seq α) → motive (some (a, s)) (some (a', s')))
  (h_3 : (x x_2 : Option (Stream'.Seq1 α)) → motive x x_2),
  (x = none → x_1 = none → False) →
    (∀ (a : α) (s : Stream'.Seq α) (a' : α) (s' : Stream'.Seq α), x = some (a, s) → x_1 = some (a', s') → False) →
      (match x, x_1 with
        | none, none => h_1 ()
        | some (a, s), some (a', s') => h_2 a s a' s'
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverseOpEquiv_opComm : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, AlgEquiv.opComm CliffordAlgebra.reverseOpEquiv = CliffordAlgebra.reverseOpEquiv.symm
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- A natural transformation `L₁ ⟶ L₂` induces a functor `P.Comma L₂ R Q W ⥤ P.Comma L₁ R Q W`.  -/
CategoryTheory.MorphismProperty.Comma.mapLeft : {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] →
            (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] →
                        {L₁ L₂ : CategoryTheory.Functor A T} →
                          (l : L₁ ⟶ L₂) →
                            (∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
                                P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom)) →
                              CategoryTheory.Functor (CategoryTheory.MorphismProperty.Comma L₂ R P Q W)
                                (CategoryTheory.MorphismProperty.Comma L₁ R P Q W)
-- Mathlib.Algebra.Group.Units.Defs
Subsingleton.addUnits_of_isAddUnit : ∀ {M : Type u_1} [inst : AddMonoid M], (∀ (a : M), IsAddUnit a → a = 0) → Subsingleton (AddUnits M)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.get?_eq_get?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α), m.get? a = m.get?ₘ a
-- Aesop.RuleTac.Basic
Aesop.RuleApplication.goals : Aesop.RuleApplication → Array Aesop.Subgoal
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, local version.

If `f` has a finite limit `c` almost surely at `l'`, where `(l, l')` is an
`intervalIntegral.FTCFilter` pair around `a`, then `∫ x in u..v, f x ∂μ = (v - u) • c + o (v - u)`
as both `u` and `v` tend to `l`.  -/
intervalIntegral.integral_sub_linear_isLittleO_of_tendsto_ae : ∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E}
  {c : E} {l l' : Filter ℝ} {lt : Filter ι} {a : ℝ} [intervalIntegral.FTCFilter a l l'],
  StronglyMeasurableAtFilter f l' MeasureTheory.volume →
    Filter.Tendsto f (l' ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
      ∀ {u v : ι → ℝ},
        Filter.Tendsto u lt l →
          Filter.Tendsto v lt l → (fun t => (∫ (x : ℝ) in u t..v t, f x) - (v t - u t) • c) =o[lt] (v - u)
-- Mathlib.Data.Set.Function
Function.insert_injOn : ∀ {α : Type u_1} (s : Set α), Set.InjOn (fun a => insert a s) sᶜ
-- Lean.Meta.Constructions.SparseCasesOn
Lean.Meta.SparseCasesOnInfo.indName : Lean.Meta.SparseCasesOnInfo → Lean.Name
-- Mathlib.Data.Finset.Max
Finset.toDual_max' : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} (hs : s.Nonempty),
  OrderDual.toDual (s.max' hs) = (Finset.image (⇑OrderDual.toDual) s).min' ⋯
-- Mathlib.Topology.Order.IntermediateValue
/-- If a function `f : α → β` is continuous on a nonempty interval `s`, its restriction to `s`
tends to `Filter.atBot : Filter β` along `Filter.atBot : Filter ↥s` and tends to
`Filter.atTop : Filter β` along `Filter.atTop : Filter ↥s`, then the restriction of `f` to `s` is
surjective. We formulate the conclusion as `Function.surjOn f s Set.univ`.  -/
ContinuousOn.surjOn_of_tendsto : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {f : α → δ} {s : Set α} [s.OrdConnected],
  s.Nonempty →
    ContinuousOn f s →
      Filter.Tendsto (fun x => f ↑x) Filter.atBot Filter.atBot →
        Filter.Tendsto (fun x => f ↑x) Filter.atTop Filter.atTop → Set.SurjOn f s Set.univ