mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.comul_counit_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.ComonObj X] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.ComonObj.counit) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv h
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.inv.instSigmaFinite : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SigmaFinite μ], MeasureTheory.SigmaFinite μ.inv
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecTheorem.mk.sizeOf_spec : ∀ (name : Lean.Name) (levelParams : List Lean.Name) (type : Lean.Expr),
  sizeOf { name := name, levelParams := levelParams, type := type } = 1 + sizeOf name + sizeOf levelParams + sizeOf type
-- Mathlib.CategoryTheory.Sites.Coherent.Basic
/-- Given an effective epi family `π₁` over `B₁` and a morphism `f : B₂ ⟶ B₁`, there exists
an effective epi family `π₂` over `B₂`, such that `π₂` factors through `π₁`.
 -/
CategoryTheory.Precoherent.pullback : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Precoherent C] {B₁ B₂ : C}
  (f : B₂ ⟶ B₁) (α : Type) [Finite α] (X₁ : α → C) (π₁ : (a : α) → X₁ a ⟶ B₁),
  CategoryTheory.EffectiveEpiFamily X₁ π₁ →
    ∃ β,
      ∃ (_ : Finite β),
        ∃ X₂ π₂,
          CategoryTheory.EffectiveEpiFamily X₂ π₂ ∧
            ∃ i ι,
              ∀ (b : β),
                CategoryTheory.CategoryStruct.comp (ι b) (π₁ (i b)) = CategoryTheory.CategoryStruct.comp (π₂ b) f
-- Mathlib.Topology.Algebra.Order.UpperLower
Set.OrdConnected.interior : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [HasUpperLowerClosure α] {s : Set α},
  s.OrdConnected → (interior s).OrdConnected
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.toList : {α : Type u_1} → {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → List (α × β)
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.any : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → (α → Bool) → Bool
-- Mathlib.Topology.Algebra.LinearTopology
/-- A variant of `IsLinearTopology.mk_of_hasBasis` asking for an explicit proof that `S`
is a class of submodules instead of relying on (fragile) typeclass inference of `SMulCommClass`.  -/
IsLinearTopology.mk_of_hasBasis' : ∀ (R : Type u_1) {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] {ι : Sort u_4} {S : Type u_5} [inst_4 : SetLike S M] [AddSubmonoidClass S M]
  {p : ι → Prop} {s : ι → S},
  ((nhds 0).HasBasis p fun i => ↑(s i)) → (∀ (s : S) (r : R), ∀ m ∈ s, r • m ∈ s) → IsLinearTopology R M
-- Init.Data.SInt.Lemmas
Int8.toISize_div_of_ne_right : ∀ (a b : Int8), b ≠ -1 → (a / b).toISize = a.toISize / b.toISize
-- Init.System.IOError
IO.Error.userError.sizeOf_spec : ∀ (msg : String), sizeOf (IO.Error.userError msg) = 1 + sizeOf msg
-- Init.Core
/-- An alternative induction principle for quotients that can be used when the target type is a
subsingleton, in which all elements are equal.

In these cases, the proof that the function respects the quotient's relation is trivial, so any
function can be lifted.

`Quot.rec` does not assume that the type is a subsingleton.
 -/
Quot.recOnSubsingleton : {α : Sort u} →
  {r : α → α → Prop} →
    {motive : Quot r → Sort v} →
      [h : ∀ (a : α), Subsingleton (motive (Quot.mk r a))] → (q : Quot r) → ((a : α) → motive (Quot.mk r a)) → motive q
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂'_obj_obj_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (G k j : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂' C).obj G).obj k).obj j =
    CategoryTheory.MonoidalCategoryStruct.tensorObj j (CategoryTheory.MonoidalCategoryStruct.tensorObj G k)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp_assoc_right : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h))
      (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h)) =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv)
      (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h))
          (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom))
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- The trivial square-zero extension is nontrivial if it is over a nontrivial module.  -/
TrivSqZeroExt.instNontrivial_of_right : ∀ {R : Type u_3} {M : Type u_4} [Nonempty R] [Nontrivial M], Nontrivial (TrivSqZeroExt R M)
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.proj_isQuotientMap : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X), Topology.IsQuotientMap S.proj
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.property.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.property = 1
-- Init.Ext
PSigma.ext_iff : ∀ {α : Sort u} {β : α → Sort v} {x y : PSigma β}, x = y ↔ x.fst = y.fst ∧ x.snd ≍ y.snd
-- Mathlib.Analysis.Normed.Order.Hom.Basic
GroupNormClass.toNormedGroup_norm_eq : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : Group α] [inst_2 : GroupNormClass F α ℝ] (f : F)
  (x : α), ‖x‖ = f x
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.inner_sq_add_areaForm_sq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (a b : E), inner ℝ a b ^ 2 + (o.areaForm a) b ^ 2 = ‖a‖ ^ 2 * ‖b‖ ^ 2
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.continuous_smul : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] [LocallyCompactSpace X] [T2Space X] {𝕜 : Type u_9}
  [inst_6 : NormedRing 𝕜] [inst_7 : Module 𝕜 E] [NormSMulClass 𝕜 E] [SecondCountableTopologyEither X 𝕜] {f : X → E}
  {g : X → 𝕜},
  Continuous g → MeasureTheory.LocallyIntegrable f μ → MeasureTheory.LocallyIntegrable (fun x => g x • f x) μ
-- Mathlib.Data.Set.Function
Set.RightInvOn.congr_right : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : α → β} {f' : β → α},
  Set.RightInvOn f' f₁ t → Set.MapsTo f' t s → Set.EqOn f₁ f₂ s → Set.RightInvOn f' f₂ t
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.foldr.match_1.eq_1 : ∀ {α : Type u_1} {σ : Sort u_3} (motive : RBTree.RBNode α → σ → Sort u_2) (b : σ)
  (h_1 : (b : σ) → motive RBTree.RBNode.nil b)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → (b : σ) → motive (RBTree.RBNode.node c l v r) b),
  (match RBTree.RBNode.nil, b with
    | RBTree.RBNode.nil, b => h_1 b
    | RBTree.RBNode.node c l v r, b => h_2 c l v r b) =
    h_1 b
-- Mathlib.Data.List.Perm.Basic
/-- **Alias** of the reverse direction of `List.perm_eraseIdx_of_getElem?_eq`. -/
List.Perm.eraseIdx_of_getElem?_eq : ∀ {α : Type u_1} {l₁ l₂ : List α} {m n : ℕ}, l₁[m]? = l₂[n]? → l₁.Perm l₂ → (l₁.eraseIdx m).Perm (l₂.eraseIdx n)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.ofIso_truth : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒞 : CategoryTheory.Subobject.Classifier C) {Ω₀ Ω : C}
  (eΩ : 𝒞.Ω ≅ Ω) (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) (from' : (C_1 : C) → C_1 ⟶ Ω₀) (t : Ω₀ ⟶ Ω)
  (ht :
    autoParam (t = CategoryTheory.CategoryStruct.comp eΩ₀.inv (CategoryTheory.CategoryStruct.comp 𝒞.truth eΩ.hom))
      CategoryTheory.Subobject.Classifier.ofIso._auto_1),
  (𝒞.ofIso eΩ eΩ₀ from' t ht).truth = t
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.mk : ∀ {α : Type u_1} {V : Type u_2} [inst : Zero α] [inst_1 : One α] {A : Matrix V V α},
  autoParam (∀ (i j : V), A i j = 0 ∨ A i j = 1) Matrix.IsAdjMatrix.zero_or_one._autoParam →
    autoParam A.IsSymm Matrix.IsAdjMatrix.symm._autoParam →
      autoParam (∀ (i : V), A i i = 0) Matrix.IsAdjMatrix.apply_diag._autoParam → A.IsAdjMatrix
-- Mathlib.Algebra.Order.Archimedean.Basic
instMulArchimedeanNNRat : MulArchimedean ℚ≥0
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonWindowClientCapabilities : Lean.ToJson Lean.Lsp.WindowClientCapabilities
-- Mathlib.Data.FunLike.Group
FunLike.commMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : One F]
  [inst_3 : Pow F ℕ] [inst_4 : CommMonoid β] [inst_5 : IsOneApply F α β] [inst_6 : IsMulApply F α β]
  [inst_7 : IsPowApply ℕ F α β], FunLike.commMonoid = Function.Injective.commMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯
-- Mathlib.MeasureTheory.Constructions.Pi
/-- The measurable equiv `(α₁ → β₁) ≃ᵐ (α₂ → β₂)` induced by `α₁ ≃ α₂` and `β₁ ≃ᵐ β₂` is
volume preserving.  -/
MeasureTheory.volume_preserving_arrowCongr' : ∀ {α₁ : Type u_4} {β₁ : Type u_5} {α₂ : Type u_6} {β₂ : Type u_7} [inst : Fintype α₁] [inst_1 : Fintype α₂]
  [inst_2 : MeasureTheory.MeasureSpace β₁] [inst_3 : MeasureTheory.MeasureSpace β₂]
  [MeasureTheory.SigmaFinite MeasureTheory.volume] (hα : α₁ ≃ α₂) (hβ : β₁ ≃ᵐ β₂),
  MeasureTheory.MeasurePreserving (⇑hβ) MeasureTheory.volume MeasureTheory.volume →
    MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.arrowCongr' hα hβ)) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.Hom.eq_2 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.WithInitial C) (a : C),
  (∀ (Y : C), x = CategoryTheory.WithInitial.of Y → False) → (CategoryTheory.WithInitial.of a).Hom x = PEmpty.{v + 1}
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Three points are collinear if and only if they are not affinely
independent.  -/
collinear_iff_not_affineIndependent : ∀ {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] {p : Fin 3 → P}, Collinear k (Set.range p) ↔ ¬AffineIndependent k p
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.setInterior_subset_affineSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {I : Set k} {n : ℕ} {s : Affine.Simplex k P n},
  Affine.Simplex.setInterior I s ⊆ ↑(affineSpan k (Set.range s.points))
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.uniqueHomFromTrivial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (A : CategoryTheory.CommGrp C) → Unique (CategoryTheory.CommGrp.trivial C ⟶ A)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Moebius
Irreducible.moebius_eq : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α},
  Irreducible a → UniqueFactorizationMonoid.moebius a = -1
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
log_deriv_riemannZeta_add_inv_sub_bounded : (fun s => deriv riemannZeta s / riemannZeta s + (s - 1)⁻¹) =O[nhdsWithin 1 {1}ᶜ] fun x => 1
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The **first isomorphism** theorem for algebras, computable version.  -/
Ideal.quotientKerAlgEquivOfRightInverse : {R₁ : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R₁] →
        [inst_1 : Ring A] →
          [inst_2 : Algebra R₁ A] →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra R₁ B] →
                {f : A →ₐ[R₁] B} → {g : B → A} → Function.RightInverse g ⇑f → (A ⧸ RingHom.ker f) ≃ₐ[R₁] B
-- Init.Data.UInt.Lemmas
UInt64.toUSize_div : ∀ (a b : UInt64), a < 4294967296 → b < 4294967296 → (a / b).toUSize = a.toUSize / b.toUSize
-- Mathlib.Data.Nat.BitIndices
Nat.two_pow_le_of_mem_bitIndices : ∀ {a n : ℕ}, a ∈ n.bitIndices → 2 ^ a ≤ n
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteS.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℕ),
  Lean.Grind.CommRing.Expr.denoteS ctx (Lean.Grind.CommRing.Expr.natCast k) = OfNat.ofNat k
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.mk : {α : Type u} → [inst : Group α] → (toTopologicalSpace : TopologicalSpace α) → IsTopologicalGroup α → GroupTopology α
-- Mathlib.Data.Fintype.Basic
/-- By iterating over the elements of a fintype, we can lift an existential statement `∃ a, P a`
to `Trunc (Σ' a, P a)`, containing data.
 -/
truncSigmaOfExists : {α : Type u_4} → [Fintype α] → {P : α → Prop} → [DecidablePred P] → (∃ a, P a) → Trunc ((a : α) ×' P a)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_union_le : ∀ {α : Type u_1} (f : α → ENNReal) (s t : Set α), ∑' (x : ↑(s ∪ t)), f ↑x ≤ ∑' (x : ↑s), f ↑x + ∑' (x : ↑t), f ↑x
-- Mathlib.Algebra.Order.Module.Field
Mathlib.Meta.Positivity.smul_ne_zero_of_ne_zero_of_pos : ∀ {α : Type u_3} {β : Type u_4} [inst : Semiring α] [IsDomain α] [inst_2 : AddCommMonoid β] [inst_3 : Module α β]
  [Module.IsTorsionFree α β] {a : α} {b : β} [inst_5 : Preorder β], a ≠ 0 → 0 < b → a • b ≠ 0
-- Mathlib.Order.Interval.Set.Basic
Set.left_mem_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ∈ Set.Icc a b ↔ a ≤ b
-- Mathlib.Data.FunLike.Module
/-- A `FunLike` type with scalar multiplication that satisfies `(m • f) x = m • f x`
is an `AddAction` if `β` is an `AddAction`.  -/
FunLike.addAction : {M : Type u_1} →
  {F : Type u_3} →
    {α : Type u_4} →
      {β : Type u_5} →
        [i : FunLike F α β] →
          [inst : VAdd M F] → [inst_1 : AddMonoid M] → [inst_2 : AddAction M β] → [IsVAddApply M F α β] → AddAction M F
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tan_zero : Complex.tan 0 = 0
-- Mathlib.LinearAlgebra.Finsupp.LSum
Submodule.mulLeftMap_apply : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_4} [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : SMulCommClass R R S] [inst_4 : SMulCommClass R S S] {M N : Submodule R S} {ι : Type u_5} (m : ι → ↥M)
  (n : ι →₀ ↥N), (Submodule.mulLeftMap N m) n = n.sum fun i n => ↑(m i) * ↑n
-- Mathlib.Analysis.SpecialFunctions.Arsinh
HasStrictDerivAt.arsinh : ∀ {f : ℝ → ℝ} {a f' : ℝ},
  HasStrictDerivAt f f' a → HasStrictDerivAt (fun x => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') a
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData'.t_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i j : self.J)
  (hij : i ≠ j) {Z : C} (h : self.V i j ⋯ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.t i j hij) (CategoryTheory.CategoryStruct.comp (self.t j i ⋯) h) = h
-- Batteries.Control.LawfulMonadState
/-- Calling `get` twice is the same as just using the first retreived state value.  -/
LawfulMonadStateOf.get_bind_get_bind : ∀ {σ : semiOutParam (Type u_1)} {m : Type u_1 → Type u_2} {inst : Monad m} {inst_1 : MonadStateOf σ m}
  [self : LawfulMonadStateOf σ m] {α : Type u_1} (mx : σ → σ → m α),
  (do
      let s ← get
      let s' ← get
      mx s s') =
    do
    let s ← get
    mx s s
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C} (a : C) (str : F.obj a ⟶ a)
  (a_1 : C) (str_1 : F.obj a_1 ⟶ a_1), ({ a := a, str := str } = { a := a_1, str := str_1 }) = (a = a_1 ∧ str ≍ str_1)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.QuasiMeasurePreserving.prod_of_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {f : α × β → γ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  {τ : MeasureTheory.Measure γ},
  Measurable f →
    ∀ [MeasureTheory.SFinite ν],
      (∀ᵐ (x : α) ∂μ, MeasureTheory.Measure.QuasiMeasurePreserving (fun y => f (x, y)) ν τ) →
        MeasureTheory.Measure.QuasiMeasurePreserving f (μ.prod ν) τ
-- Lean.DocString.Types
Lean.Doc.instBEqPart.beq : {i : Type u_1} →
  {b : Type u_2} → {p : Type u_3} → [BEq i] → [BEq b] → [BEq p] → Lean.Doc.Part i b p → Lean.Doc.Part i b p → Bool
-- Mathlib.Data.Pi.Interval
Pi.card_uIcc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → Lattice (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) → α i),
  (Finset.uIcc a b).card = ∏ i, (Finset.uIcc (a i) (b i)).card
-- Mathlib.Order.Concept
/-- The dual of a concept lattice is isomorphic to the concept lattice of the dual context.  -/
Concept.swapEquiv : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → (Concept α β r)ᵒᵈ ≃o Concept β α (Function.swap r)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List α} {k : α}, k ∈ t.insertMany l ↔ k ∈ t ∨ l.contains k = true
-- Mathlib.CategoryTheory.Abelian.Basic
/-- Any abelian category has pushouts  -/
CategoryTheory.Abelian.hasPushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C], CategoryTheory.Limits.HasPushouts C
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_functor_map_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) {X Y : CategoryTheory.Comma L₁ R} (f : X ⟶ Y),
  ((CategoryTheory.Comma.mapLeftIso R i).functor.map f).left = f.left
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.comp_apply : ∀ {Γ : Type u_5} {Γ' : Type u_6} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ'] {R : Type u_7} [inst_2 : CommRing R]
  {U : Type u_8} {V : Type u_9} {W : Type u_10} [inst_3 : AddCommGroup U] [inst_4 : Module R U]
  [inst_5 : AddCommGroup V] [inst_6 : Module R V] [inst_7 : AddCommGroup W] [inst_8 : Module R W]
  (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V) (u : U),
  (A.comp B) u = (HahnModule.of R) (A.compHahnSeries B u).ofIterate
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.linearEquiv_apply : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : Semiring R]
  [inst_3 : Semiring T] [inst_4 : Module R T] {v : AbsoluteValue T S} (x : WithAbs v),
  (WithAbs.linearEquiv R v) x = x.ofAbs
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃_obj_map_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X₁ : C)
  {X₂ Y₂ : C} (φ : X₂ ⟶ Y₂) (X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃ C).obj X₁).map φ).app X₃ =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X₁) X₃
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.of_add_mul_right_left : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsRelPrime (x + z * y) y → IsRelPrime x y
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.hasRightResolutions_arrow_of_essSurj_of_full : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {W₁' : CategoryTheory.MorphismProperty D₁}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [R.functor.EssSurj] [R.functor.Full] [W₂'.RespectsIso]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor) [T.arrow.HasRightResolutions], B.arrow.HasRightResolutions
-- Mathlib.RingTheory.Extension.Cotangent.Free
Algebra.Generators.cotangentRestrict_bijective_of_basis_kaehlerDifferential : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_3}
  {σ : Type u_4} {κ : Type u_5} (P : Algebra.Generators R S ι) {u : σ → ι} (hu : Function.Injective u) {v : κ → ι},
  IsCompl (Set.range v) (Set.range u) →
    ∀ (b : Module.Basis κ S Ω[S⁄R]),
      (∀ (k : κ), b k = (KaehlerDifferential.D R S) (P.val (v k))) →
        ∀ [Subsingleton (Algebra.H1Cotangent R S)], Function.Bijective ⇑(P.cotangentRestrict hu)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- `comp e f g` is the expression for `f ≫ g`, where `e` is the underlying lean expression.  -/
Mathlib.Tactic.BicategoryLike.Mor₁.comp : Lean.Expr → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Probability.Density
MeasureTheory.pdf.ae_lt_top : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure ℙ] {μ : MeasureTheory.Measure E} {X : Ω → E},
  ∀ᵐ (x : E) ∂μ, MeasureTheory.pdf X ℙ μ x < ⊤
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.differentiableAt_Λ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) {s : ℂ},
  s ≠ 0 ∨ P.f₀ = 0 → s ≠ ↑P.k ∨ P.g₀ = 0 → DifferentiableAt ℂ P.Λ s
-- Lean.Expr
Lean.Expr.mdataExpr! : Lean.Expr → Lean.Expr
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
/-- Auxiliary measure used to construct the vector measure associated to a bounded variation
function. This is *not* the total variation of this measure in general, as we need to adjust things
when there is a bot element by adding a Dirac mass there.  -/
_private.Mathlib.MeasureTheory.VectorMeasure.BoundedVariation.0.BoundedVariationOn.measureAux : {α : Type u_1} →
  [inst : LinearOrder α] →
    [DenselyOrdered α] →
      [inst_2 : TopologicalSpace α] →
        [OrderTopology α] →
          [SecondCountableTopology α] →
            [CompactIccSpace α] →
              [hα : MeasurableSpace α] →
                [BorelSpace α] →
                  {E : Type u_2} →
                    [inst_7 : NormedAddCommGroup E] →
                      [CompleteSpace E] → {f : α → E} → BoundedVariationOn f Set.univ → MeasureTheory.Measure α
-- Mathlib.Analysis.Fourier.AddCircle
fourier_add' : ∀ {T : ℝ} {m n : ℤ} {x : AddCircle T}, ↑((m + n) • x).toCircle = (fourier m) x * (fourier n) x
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
IsIntegral.map_of_comp_eq : ∀ {R : Type u_5} {S : Type u_6} {T : Type u_7} {U : Type u_8} [inst : CommRing R] [inst_1 : Ring S]
  [inst_2 : CommRing T] [inst_3 : Ring U] [inst_4 : Algebra R S] [inst_5 : Algebra T U] (φ : R →+* T) (ψ : S →+* U),
  (algebraMap T U).comp φ = ψ.comp (algebraMap R S) → ∀ {a : S}, IsIntegral R a → IsIntegral T (ψ a)