mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.posFittingComp.congr_simp : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L], LieModule.posFittingComp R L M = LieModule.posFittingComp R L M
-- Mathlib.Order.Hom.Bounded
BotHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Bot α} {inst_1 : Bot β} {toFun : α → β} {map_bot' : toFun ⊥ = ⊥}
  {toFun_1 : α → β} {map_bot'_1 : toFun_1 ⊥ = ⊥},
  { toFun := toFun, map_bot' := map_bot' } = { toFun := toFun_1, map_bot' := map_bot'_1 } → toFun = toFun_1
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.notMem_sdiff_of_mem`. -/
Set.notMem_diff_of_mem : ∀ {α : Type u_1} {s t : Set α} {x : α}, x ∈ t → x ∉ s \ t
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.instFunLike : {M : Type u_4} → {N : Type u_5} → [inst : MulOne M] → [inst_1 : MulOne N] → FunLike (M →* N) M N
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.mem_finiteRange_iff_hasNoetherianRange : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V →ₗ[K] V₂},
  f ∈ LinearMap.finiteRange K V V₂ ↔ f.HasNoetherianRange
-- Mathlib.Algebra.Category.Grp.Colimits
/-- The candidate for the colimit of `F`, defined as the quotient of the direct sum
of the commutative groups `F.obj j` by the relations given by the morphisms in
the diagram.
 -/
AddCommGrpCat.Colimits.Quot : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] → CategoryTheory.Functor J AddCommGrpCat → [DecidableEq J] → Type (max u w)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Append.0.Std.IterM.step_append.match_1.eq_2 : ∀ {α₁ β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β] {it₁ : Std.IterM m β}
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β) (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁'))
  (h_1 :
    (it₁' : Std.IterM m β) →
      (out : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it₁', 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, h⟩ => h_3 h) =
    h_2 it₁' h
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.mk.inj : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : NonUnitalNonAssocSemiring A} {inst_2 : Module R A}
  {inst_3 : Star A} {toNonUnitalSubalgebra : NonUnitalSubalgebra R A}
  {star_mem' : ∀ {a : A}, a ∈ toNonUnitalSubalgebra.carrier → star a ∈ toNonUnitalSubalgebra.carrier}
  {toNonUnitalSubalgebra_1 : NonUnitalSubalgebra R A}
  {star_mem'_1 : ∀ {a : A}, a ∈ toNonUnitalSubalgebra_1.carrier → star a ∈ toNonUnitalSubalgebra_1.carrier},
  { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := star_mem' } =
      { toNonUnitalSubalgebra := toNonUnitalSubalgebra_1, star_mem' := star_mem'_1 } →
    toNonUnitalSubalgebra = toNonUnitalSubalgebra_1
-- Mathlib.Order.BooleanAlgebra.Set
Set.notMem_of_mem_sdiff : ∀ {α : Type u_1} {s t : Set α} {x : α}, x ∈ s \ t → x ∉ t
-- Lean.Meta.Tactic.Grind.Types
/-- Case splitting related fields for the `grind` goal.  -/
Lean.Meta.Grind.Split.State : Type
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDocumentSymbolAux.fromJson : {Self : Type} → [Lean.FromJson Self] → Lean.Json → Except String (Lean.Lsp.DocumentSymbolAux Self)
-- Mathlib.Algebra.GroupWithZero.Defs
IsLeftCancelMulZero.to_isRightCancelMulZero : ∀ {M₀ : Type u_1} [inst : CommMagma M₀] [inst_1 : Zero M₀] [IsLeftCancelMulZero M₀], IsRightCancelMulZero M₀
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.ofHom_id : ∀ {M : Type u} [inst : Add M], AddMagmaCat.ofHom (AddHom.id M) = CategoryTheory.CategoryStruct.id (AddMagmaCat.of M)
-- Init.Control.Basic
forIn'_eq_forIn : ∀ {α : Type u_1} {ρ : Type u_2} {m : Type u_3 → Type u_4} [d : Membership α ρ] [inst : ForIn' m ρ α d] {β : Type u_3}
  (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) (g : α → β → m (ForInStep β)),
  (∀ (a : α) (m_1 : a ∈ x) (b : β), f a m_1 b = g a b) → forIn' x b f = forIn x b g
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.contMDiffWithinAt_zeroSection : ∀ {n : WithTop ℕ∞} (𝕜 : Type u_1) {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)] [VectorBundle 𝕜 F E] {t : Set B}
  {x : B}, ContMDiffWithinAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (Bundle.zeroSection F E) t x
-- Mathlib.Control.Bifunctor
/-- Lawless bifunctor. This typeclass only holds the data for the bimap.  -/
Bifunctor : (Type u₀ → Type u₁ → Type u₂) → Type (max (max (u₀ + 1) (u₁ + 1)) u₂)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- If a point `x` belongs to `s`, then its edist to `s` vanishes  -/
Metric.infEDist_zero_of_mem : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, x ∈ s → Metric.infEDist x s = 0
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.IsTerminal.uniqueUpToIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T T' : C} (hT : CategoryTheory.Limits.IsTerminal T)
  (hT' : CategoryTheory.Limits.IsTerminal T'), (hT.uniqueUpToIso hT').hom = hT'.from T
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- With the data of chosen isomorphic objects to given day convolutions,
and provably equal unit maps through these isomorphisms,
we can transform a given family of Day convolutions to one with
convolutions definitionally equals to the given objects, and component of units
definitionally equal to the provided map family.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutions : (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] →
            {D : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} D] →
                [inst_5 : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] →
                  (d d' : D) →
                    CategoryTheory.MonoidalCategory.DayConvolution
                      ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V
                            D).obj
                        d)
                      ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V
                            D).obj
                        d')
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.isoExt_hom_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F)
  (hF' : CategoryTheory.Limits.IsImage F'), CategoryTheory.CategoryStruct.comp (hF.isoExt hF').hom F'.m = F.m
-- Mathlib.Order.Filter.Curry
Filter.eventually_curry_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} {p : α × β → Prop},
  (∀ᶠ (x : α × β) in l.curry m, p x) ↔ ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, p (x, y)
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.unicode_turnstile.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.ENat.Basic
ENat.canLift : CanLift ℕ∞ ℕ Nat.cast fun x => x ≠ ⊤
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.image_isVonNBounded_iff_seminorm_bounded : ∀ {𝕜 : Type u_2} {E : Type u_6} {G : Type u_8} {ι : Type u_9} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [inst_3 : TopologicalSpace E] (f : G → E)
  {s : Set G}, WithSeminorms p → (Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) (f x) < r)
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.prod_one_sub : ∀ {R : Type u_1} [inst : CommRing R] {I : Type u_3} [inst_1 : Fintype I] {e : I → R},
  CompleteOrthogonalIdempotents e → ∏ i, (1 - e i) = 0
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- The identity strong transformation.  -/
CategoryTheory.Pseudofunctor.StrongTrans.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} → [inst_1 : CategoryTheory.Bicategory C] → (F : CategoryTheory.Pseudofunctor B C) → F.StrongTrans F
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.lift_unique : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) {j : N →+ P},
  (∀ (x : M), j (f x) = g x) → f.lift hg = j
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CongrKey.mk.sizeOf_spec : ∀ {enodes : Lean.Meta.Grind.ENodeMap} (e : Lean.Expr), sizeOf { e := e } = 1 + sizeOf e
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_comp_sym : ∀ {α : Type u_1}, ⇑SymAlg.unsym ∘ ⇑SymAlg.sym = id
-- Mathlib.Order.WithBot
WithTop.ofDual_le_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithBot α} {y : WithTop αᵒᵈ}, WithTop.ofDual y ≤ x ↔ WithBot.toDual x ≤ y
-- Mathlib.Analysis.Meromorphic.Basic
/-- Derivatives of meromorphic functions are meromorphic.  -/
MeromorphicOn.deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜}, MeromorphicOn f U → ∀ [CompleteSpace E], MeromorphicOn (deriv f) U
-- Lean.Parser.Term
Lean.Parser.Tactic.quotSeq.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Hom.Bounded
BotHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Bot α] [inst_1 : Bot β] [inst_2 : Bot γ]
  [inst_3 : Bot δ] (f : BotHom γ δ) (g : BotHom β γ) (h : BotHom α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Topology.Algebra.Module.Star
/-- The skew-adjoint part of an element of a star module, as a continuous linear map.  -/
skewAdjointPartL : (R : Type u_1) →
  (A : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : StarMul R] →
        [inst_2 : TrivialStar R] →
          [inst_3 : AddCommGroup A] →
            [inst_4 : Module R A] →
              [inst_5 : StarAddMonoid A] →
                [inst_6 : StarModule R A] →
                  [Invertible 2] →
                    [inst_8 : TopologicalSpace A] →
                      [ContinuousSub A] → [ContinuousStar A] → [ContinuousConstSMul R A] → A →L[R] ↥(skewAdjoint A)
-- Mathlib.Data.List.DropRight
List.rdrop_nil : ∀ {α : Type u_1} (n : ℕ), [].rdrop n = []
-- Mathlib.Logic.Relation
Relation.transGen_reflGen : ∀ {α : Type u_1} {r : α → α → Prop}, Relation.TransGen (Relation.ReflGen r) = Relation.ReflTransGen r
-- Mathlib.Order.Bounds.Basic
/-- If `t` is bounded, then so is `s ∩ t`  -/
BddAbove.inter_of_right : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, BddAbove t → BddAbove (s ∩ t)
-- Mathlib.Probability.Distributions.Exponential
/-- The exponential pdf is nonnegative  -/
ProbabilityTheory.exponentialPDFReal_nonneg : ∀ {r : ℝ}, 0 < r → ∀ (x : ℝ), 0 ≤ ProbabilityTheory.exponentialPDFReal r x
-- Aesop.RuleTac.Basic
Aesop.Subgoal.mk : Aesop.GoalDiff → Aesop.Subgoal
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.cooper_right_core : ∀ {a b p q x : ℤ},
  a < 0 →
    0 < b →
      a * x + p ≤ 0 →
        b * x + q ≤ 0 → Int.Internal.Linear.OrOver b.natAbs fun k => b * p + -a * q + -a * ↑k ≤ 0 ∧ b ∣ q + ↑k
-- Mathlib.ModelTheory.LanguageMap
/-- A map between index types induces a map between constant languages.  -/
FirstOrder.Language.LHom.constantsOnMap : {α : Type u'} → {β : Type v'} → (α → β) → (FirstOrder.Language.constantsOn α →ᴸ FirstOrder.Language.constantsOn β)
-- Mathlib.Analysis.Matrix.Normed
Matrix.nnnorm_replicateRow : ∀ {n : Type u_4} {α : Type u_5} {ι : Type u_7} [inst : Fintype n] [inst_1 : Unique ι]
  [inst_2 : SeminormedAddCommGroup α] (v : n → α), ‖Matrix.replicateRow ι v‖₊ = ‖v‖₊
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzWith_iff_norm_sub_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] {f : E → F}
  {C : NNReal}, LipschitzWith C f ↔ ∀ (x y : E), ‖f x - f y‖ ≤ ↑C * ‖x - y‖
-- Mathlib.Topology.Algebra.InfiniteSum.Order
isLUB_hasProd : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α},
  (∀ (i : ι), 1 ≤ f i) → HasProd f a → IsLUB (Set.range fun s => ∏ i ∈ s, f i) a
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- If `i ≠ j` and `Xᵢ ← Y → Xⱼ` is a pullback diagram over `∐ X`, `Y` is initial.  -/
CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {X : ι → C} →
        [CategoryTheory.Limits.CoproductDisjoint X] →
          {i j : ι} →
            i ≠ j →
              [inst_2 : CategoryTheory.Limits.HasCoproduct X] →
                {s :
                    CategoryTheory.Limits.PullbackCone (CategoryTheory.Limits.Sigma.ι X i)
                      (CategoryTheory.Limits.Sigma.ι X j)} →
                  CategoryTheory.Limits.IsLimit s → CategoryTheory.Limits.IsInitial s.pt
-- Aesop.Index.Basic
Aesop.IndexingMode.target : Array Lean.Meta.DiscrTree.Key → Aesop.IndexingMode
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.impArrow.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.tensorLift_tmul : ∀ {R : Type u} [inst : CommRing R] {M₁ M₂ M₃ : ModuleCat R} (f : ↑M₁ → ↑M₂ → ↑M₃)
  (h₁ : ∀ (m₁ m₂ : ↑M₁) (n : ↑M₂), f (m₁ + m₂) n = f m₁ n + f m₂ n)
  (h₂ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f (a • m) n = a • f m n)
  (h₃ : ∀ (m : ↑M₁) (n₁ n₂ : ↑M₂), f m (n₁ + n₂) = f m n₁ + f m n₂)
  (h₄ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f m (a • n) = a • f m n) (m : ↑M₁) (n : ↑M₂),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.MonoidalCategory.tensorLift f h₁ h₂ h₃ h₄)) (m ⊗ₜ[R] n) = f m n
-- Init.Data.Int.Linear
Int.Internal.Linear.not_le_of_le' : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.not_le_of_le_cert p₁ p₂ = true →
    ∀ (k : ℤ), Int.Internal.Linear.Poly.denote' ctx p₁ ≤ k → ¬Int.Internal.Linear.Poly.denote' ctx p₂ ≤ -k
-- Lean.DocString.Extension
Lean.versoDocStringExt : Lean.MapDeclarationExtension Lean.VersoDocString
-- Init.Data.List.Find
List.IsPrefix.findSome?_eq_some : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l₁ l₂ : List α} {f : α → Option β},
  l₁ <+: l₂ → List.findSome? f l₁ = some b → List.findSome? f l₂ = some b
-- Mathlib.Order.Filter.Pointwise
Filter.map₂_mul : ∀ {α : Type u_2} [inst : Mul α] {f g : Filter α}, Filter.map₂ (fun x1 x2 => x1 * x2) f g = f * g
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balRight.eq_def : ∀ {α : Type u_1} (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  l.balRight v r =
    match r with
    | RBTree.RBNode.node RBTree.RBColor.red b y c =>
      RBTree.RBNode.node RBTree.RBColor.red l v (RBTree.RBNode.node RBTree.RBColor.black b y c)
    | r =>
      match l with
      | RBTree.RBNode.node RBTree.RBColor.black a x b => (RBTree.RBNode.node RBTree.RBColor.red a x b).balance1 v r
      | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) =>
        RBTree.RBNode.node RBTree.RBColor.red (a.setRed.balance1 x b) y (RBTree.RBNode.node RBTree.RBColor.black c v r)
      | l => RBTree.RBNode.node RBTree.RBColor.red l v r
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_sUnion_null_iff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {S : Set (Set α)}, S.Countable → (μ (⋃₀ S) = 0 ↔ ∀ s ∈ S, μ s = 0)
-- Mathlib.Algebra.Group.Conj
/-- We say that `a` is additively conjugate to `b` if for some additive unit `c` we
have `c + a + -c = b`.  -/
IsAddConj : {α : Type u} → [AddMonoid α] → α → α → Prop
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.Equiv.trans : ∀ {α : Type u} {s t u : Stream'.WSeq α}, s ~ʷ t → t ~ʷ u → s ~ʷ u
-- Mathlib.Data.Seq.Basic
Stream'.Seq.enum_cons : ∀ {α : Type u} (s : Stream'.Seq α) (x : α),
  (Stream'.Seq.cons x s).enum = Stream'.Seq.cons (0, x) (Stream'.Seq.map (Prod.map Nat.succ id) s.enum)
-- Mathlib.Algebra.Group.Action.Pretransitive
AddAction.IsPretransitive.mk : ∀ {M : Type u_5} {α : Type u_6} [inst : VAdd M α], (∀ (x y : α), ∃ g, g +ᵥ x = y) → AddAction.IsPretransitive M α
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.instMonObjTensorObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.MonObj M]
  [inst_4 : CategoryTheory.MonObj N],
  CategoryTheory.Mon.instMonObjTensorObj =
    {
      one :=
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one),
      mul :=
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.tensorμ { X := M, mon := inst_3 }.X { X := N, mon := inst_4 }.X
            { X := M, mon := inst_3 }.X { X := N, mon := inst_4 }.X)
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul),
      one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }
-- Mathlib.GroupTheory.Coset.Card
AddSubgroup.card_quotient_dvd_card : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), Nat.card (α ⧸ s) ∣ Nat.card α
-- Batteries.Data.HashMap.Basic
/-- Looks up an element in the map with key `a`.
```
def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.find? "one" = some 1
hashMap.find? "three" = none
```
 -/
Batteries.HashMap.find? : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α β → α → Option β
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α], Set.Iic ⊥ = {⊥}
-- Std.Time.Zoned.ZoneRules
/-- Finds the transition in effect at a given timestamp in `Array Transition`.
Returns the most recent transition that started at or before the timestamp,
or `none` if the timestamp precedes all transitions.
 -/
Std.Time.TimeZone.Transition.findTransitionForTimestamp : Array Std.Time.TimeZone.Transition → Std.Time.Timestamp → Option Std.Time.TimeZone.Transition
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.bindOnSupport_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (q : PMF β)
  (f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ),
  (p.bindOnSupport fun a ha => q.bindOnSupport (f a ha)) =
    q.bindOnSupport fun b hb => p.bindOnSupport fun a ha => f a ha b hb
-- Mathlib.Topology.Separation.Hausdorff
T2Space.t1Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X], T1Space X
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- The exterior algebra of an `R`-module `M`.
 -/
ExteriorAlgebra : (R : Type u1) → [inst : CommRing R] → (M : Type u2) → [inst_1 : AddCommGroup M] → [Module R M] → Type (max u1 u2)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.op_injective : ∀ {G : Type u_2} [inst : AddGroup G], Function.Injective AddSubgroup.op
-- Mathlib.Topology.Semicontinuity.Basic
Continuous.comp_upperSemicontinuous : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderTopology δ] {g : γ → δ}
  {f : α → γ}, Continuous g → UpperSemicontinuous f → Monotone g → UpperSemicontinuous (g ∘ f)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.tensorBimod_actLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) (N : Bimod Y Z),
  (M.tensorBimod N).actLeft = Bimod.TensorBimod.actLeft M N
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.flip_comp_polarization_eq_rootForm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι],
  P.flip.toLinearMap ∘ₗ P.Polarization = P.RootForm
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Array.map_unattach.match_1.eq_1 : ∀ {α : Type u_1} {P : α → Prop} (motive : Subtype P → Sort u_2) (x : α) (h : P x)
  (h_1 : (x : α) → (h : P x) → motive ⟨x, h⟩),
  (match ⟨x, h⟩ with
    | ⟨x, h⟩ => h_1 x h) =
    h_1 x h
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.TransitionSpec.mwd.injEq : ∀ (month : Std.Time.Month.Ordinal) (week : Std.Time.Week.Aligned.Ordinal) (day : Std.Time.Weekday.Ordinal)
  (month_1 : Std.Time.Month.Ordinal) (week_1 : Std.Time.Week.Aligned.Ordinal) (day_1 : Std.Time.Weekday.Ordinal),
  (Std.Time.TimeZone.TransitionSpec.mwd month week day = Std.Time.TimeZone.TransitionSpec.mwd month_1 week_1 day_1) =
    (month = month_1 ∧ week = week_1 ∧ day = day_1)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RccSliceData.treeMap : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RccSliceData α β → Std.DTreeMap.Internal.Impl α β
-- Lean.Elab.Command
Lean.Elab.Command.instMonadExceptOfExceptionCommandElabM : MonadExceptOf Lean.Exception Lean.Elab.Command.CommandElabM
-- Mathlib.Data.PFun
PFun.core_def : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β), f.core s = {x | ∀ y ∈ f x, y ∈ s}
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coe_fst_eventuallyEq_proj : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : Z}, x ∈ e.source → Prod.fst ∘ ↑e =ᶠ[nhds x] proj
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
_private.Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality.0.InnerProductGeometry.eq_of_angle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  ‖x‖ = 1 → ‖y‖ = 1 → InnerProductGeometry.angle x y = 0 → x = y
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Presieve.CoverByImageStructure.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {V U : D} {f : V ⟶ U}
  [inst_2 : SizeOf C] [inst_3 : SizeOf D] (obj : C) (lift : V ⟶ G.obj obj) (map : G.obj obj ⟶ U)
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp lift map = f)
      CategoryTheory.Presieve.CoverByImageStructure.fac._autoParam),
  sizeOf { obj := obj, lift := lift, map := map, fac := fac } = 1 + sizeOf obj + sizeOf lift + sizeOf map + sizeOf fac