mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.LocallyDiscrete.mkPseudofunctor_obj : ∀ {B₀ : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} B₀] [inst_1 : CategoryTheory.Bicategory C]
  (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b'))
  (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b))
  (mapComp :
    {b₀ b₁ b₂ : B₀} →
      (f : b₀ ⟶ b₁) →
        (g : b₁ ⟶ b₂) →
          map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g))
  (map₂_associator :
    autoParam
      (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv)
                  (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_1)
  (map₂_left_unitor :
    autoParam
      (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f))
              (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_3)
  (map₂_right_unitor :
    autoParam
      (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom)
              (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.LocallyDiscrete.mkPseudofunctor._auto_5)
  (b : CategoryTheory.LocallyDiscrete B₀),
  (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor
          map₂_right_unitor).obj
      b =
    obj b.as
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- If a function is injective on a finset, products over the original finset or its image coincide.
See also `prod_image_of_pairwise_eq_one` for a version with weaker assumptions.  -/
Finset.prod_image : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι] {s : Finset κ}
  {g : κ → ι}, Set.InjOn g ↑s → ∏ x ∈ Finset.image g s, f x = ∏ x ∈ s, f (g x)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_hom_app_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} {mor₁ : obj₁ ⟶ obj₂}
  {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)}
  {obj₁' obj₂' obj₃' : CategoryTheory.Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'}
  {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (iso₁ : obj₁ ≅ obj₁') (iso₂ : obj₂ ≅ obj₂')
  (iso₃ : obj₃ ≅ obj₃')
  (comm₁ : CategoryTheory.CategoryStruct.comp mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom mor₁')
  (comm₂ : CategoryTheory.CategoryStruct.comp mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom mor₂')
  (comm₃ :
    CategoryTheory.CategoryStruct.comp mor₃
        (CategoryTheory.Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) =
      CategoryTheory.CategoryStruct.comp iso₃.hom mor₃')
  (j : J),
  ((CategoryTheory.Pretriangulated.Triangle.functorIsoMk' iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom.app j).hom₁ =
    iso₁.hom.app j
-- Lean.DocString.Extension
Lean.VersoModuleDocs.Snippet.mk.inj : ∀ {text : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)}
  {sections : Array (ℕ × Lean.DeclarationRange × Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)}
  {declarationRange : Lean.DeclarationRange} {text_1 : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)}
  {sections_1 : Array (ℕ × Lean.DeclarationRange × Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)}
  {declarationRange_1 : Lean.DeclarationRange},
  { text := text, sections := sections, declarationRange := declarationRange } =
      { text := text_1, sections := sections_1, declarationRange := declarationRange_1 } →
    text = text_1 ∧ sections = sections_1 ∧ declarationRange = declarationRange_1
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.eq_zero : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {r : R}, v₁ r = 0 ↔ v₂ r = 0
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Swapping the second and third points in an oriented angle negates the sign of that angle.  -/
EuclideanGeometry.oangle_swap₂₃_sign : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₂ p₃ : P), -(EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₁ p₃ p₂).sign
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalateTR.match_1.splitter : {α : Type u_1} →
  (motive : List (List α) → Sort u_2) →
    (x : List (List α)) →
      (Unit → motive []) →
        ((x : List α) → motive [x]) →
          ((x : List α) → (xs : List (List α)) → (xs = [] → False) → motive (x :: xs)) → motive x
-- Mathlib.Analysis.Complex.CanonicalDecomposition
_private.Mathlib.Analysis.Complex.CanonicalDecomposition.0.Complex.canonicalDecomposition_aux₂ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ} {f : ℂ → E},
  MeromorphicOn f (Metric.closedBall 0 R) →
    MeromorphicOn.divisor (∏ᶠ (u : ℂ), Complex.canonicalFactor R u ^ (MeromorphicOn.divisor f (Metric.ball 0 R)) u)
        (Metric.ball 0 R) =
      -MeromorphicOn.divisor f (Metric.ball 0 R)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.measure_ne_zero : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [Countable G] [MeasureTheory.SMulInvariantMeasure G α μ],
  μ ≠ 0 → MeasureTheory.IsFundamentalDomain G s μ → μ s ≠ 0
-- Mathlib.Combinatorics.Graph.Delete
Graph.restrict_le : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} {E₀ : Set β}, G.restrict E₀ ≤ G
-- Mathlib.Order.LiminfLimsup
/-- In other words, `liminf cofinite s` is the set of elements lying outside the family `s`
finitely often.  -/
Filter.cofinite.liminf_set_eq : ∀ {α : Type u_1} {ι : Type u_4} {s : ι → Set α}, Filter.liminf s Filter.cofinite = {x | {n | x ∉ s n}.Finite}
-- Mathlib.Combinatorics.Quiver.Basic
/-- The type of edges/arrows/morphisms between a given source and target.  -/
Quiver.Hom : {V : Type u} → [self : Quiver V] → V → V → Type v
-- Mathlib.Topology.Algebra.ProperConstSMul
instProperConstSMulOfContinuousConstSMulOfT2SpaceOfCompactSpace : ∀ {M : Type u_1} {X : Type u_2} [inst : SMul M X] [inst_1 : TopologicalSpace X] [ContinuousConstSMul M X] [T2Space X]
  [CompactSpace X], ProperConstSMul M X
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the second of three points is strictly between the other two, the angle at the first point
(reversed) is zero.  -/
Sbtw.angle₃₁₂_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.angle p₃ p₁ p₂ = 0
-- Mathlib.LinearAlgebra.Pi
Submodule.le_comap_single_pi : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (p : (i : ι) → Submodule R (φ i)) {I : Set ι} {i : ι},
  p i ≤ Submodule.comap (LinearMap.single R φ i) (Submodule.pi I p)
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_leftUnitor : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitor f).op2 = CategoryTheory.Bicategory.rightUnitor f.op
-- Mathlib.NumberTheory.PrimeCounting
Nat.two_le_of_mem_primesBelow : ∀ {p n : ℕ}, p ∈ n.primesBelow → 2 ≤ p
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.forM_eq_forM_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → m PUnit.{w + 1}}, (forM t fun a => f a.fst) = t.keys.forM f
-- Init.Data.UInt.Lemmas
UInt32.not_lt_zero : ∀ {a : UInt32}, ¬a < 0
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.coe_im : ∀ (z : UpperHalfPlane), (↑z).im = z.im
-- Mathlib.RingTheory.Ideal.Height
IsLocalization.height_under : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [IsLocalization S A] (J : Ideal A), (Ideal.under R J).height = J.height
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- The underlying matrix of the Coxeter matrix.  -/
CoxeterMatrix.M : {B : Type u_1} → CoxeterMatrix B → Matrix B B ℕ
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.of_isoOfHomeo : ∀ {X Y : TopCat} (f : ↑X ≃ₜ ↑Y), TopCat.homeoOfIso (TopCat.isoOfHomeo f) = f
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcCallParams.toTextDocumentPositionParams : Lean.Lsp.RpcCallParams → Lean.Lsp.TextDocumentPositionParams
-- Mathlib.Topology.Constructions
isClosedMap_sigmaMk : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {i : ι}, IsClosedMap (Sigma.mk i)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rco.toArray_iter : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rco α}, r.iter.toArray = r.toArray
-- Mathlib.Order.SuccPred.Basic
Order.Icc_subset_Ico_succ_right : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Icc a b ⊆ Set.Ico a (Order.succ b)
-- Mathlib.Data.ZMod.Basic
_private.Mathlib.Data.ZMod.Basic.0.Nat.xgcdAux.match_1.splitter : (motive : (n : ℕ) → ((m : ℕ) → m < n → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → Sort u_1) →
  (n : ℕ) →
    (ih : (m : ℕ) → m < n → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) →
      ((ih : (m : ℕ) → m < 0 → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → motive 0 ih) →
        ((k : ℕ) → (ih : (m : ℕ) → m < k.succ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ) → motive k.succ ih) → motive n ih
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.ext : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) {σ τ : p.Gal},
  (∀ x ∈ p.rootSet p.SplittingField, σ x = τ x) → σ = τ
-- Lean.Declaration
/-- List of all inductive datatypes in the mutual declaration that generated this recursor  -/
Lean.RecursorVal.all : Lean.RecursorVal → List Lean.Name
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
/-- The equivalence between height-one prime ideals of `R` and primes in `ℕ`.  -/
Rat.HeightOneSpectrum.primesEquiv : {R : Type u_2} →
  [inst : CommRing R] →
    [inst_1 : Algebra R ℚ] →
      [IsIntegralClosure R ℤ ℚ] → [IsDedekindDomain R] → IsDedekindDomain.HeightOneSpectrum R ≃ Nat.Primes
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- Multiplication `y ↦ y * x` as an `IsometryEquiv`.  -/
IsometryEquiv.mulRight : {G : Type v} → [inst : Group G] → [inst_1 : PseudoEMetricSpace G] → [IsIsometricSMul Gᵐᵒᵖ G] → G → G ≃ᵢ G
-- Mathlib.Topology.GDelta.Basic
/-- A set is meagre iff it is contained in a countable union of nowhere dense sets.  -/
isMeagre_iff_countable_union_isNowhereDense : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  IsMeagre s ↔ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
-- Mathlib.Topology.Order.SuccPred
SuccOrder.isOpen_singleton_of_not_isSuccPrelimit : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] {a : α} [SuccOrder α],
  ¬Order.IsSuccPrelimit a → IsOpen {a}
-- Mathlib.Order.Bounds.Basic
subset_upperBounds_lowerBounds : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α), s ⊆ upperBounds (lowerBounds s)
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.differentiable_LFunction_of_sum_zero : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ}, ∑ j, Φ j = 0 → Differentiable ℂ (ZMod.LFunction Φ)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- The 2-morphisms underlying the oplax naturality constraint.  -/
CategoryTheory.Oplax.OplaxTrans.naturality : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          (self : CategoryTheory.Oplax.OplaxTrans F G) →
            {a b : B} →
              (f : a ⟶ b) →
                CategoryTheory.CategoryStruct.comp (F.map f) (self.app b) ⟶
                  CategoryTheory.CategoryStruct.comp (self.app a) (G.map f)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- **Alias** of `cbiSup_eq_ciSup_subtype`. -/
ciSup_subtype' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α},
  BddAbove (Set.range fun i => f ↑i ⋯) → sSup ∅ ≤ ⨆ i, f ↑i ⋯ → ⨆ i, ⨆ (h : p i), f i h = ⨆ x, f ↑x ⋯
-- Std.Time.Format.Modifier
Std.Time.ExtendedDayPeriod.morning.sizeOf_spec : sizeOf Std.Time.ExtendedDayPeriod.morning = 1
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.le_iterate_of_add_int_le_map : ∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ}, x + ↑m ≤ f x → ∀ (n : ℕ), x + ↑n * ↑m ≤ (⇑f)^[n] x
-- Mathlib.Analysis.Normed.Order.Hom.Basic
/-- Constructs a `SeminormedAddCommGroup` structure from an `AddGroupSeminormClass`
on an `AddCommGroup`.  -/
AddGroupSeminormClass.toSeminormedAddCommGroup : {F : Type u_1} →
  {α : Type u_2} →
    [inst : FunLike F α ℝ] → [inst_1 : AddCommGroup α] → [AddGroupSeminormClass F α ℝ] → F → SeminormedAddCommGroup α
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.top_isIndContained_iff_top_isContained : ∀ {V : Type u_1} {W : Type u_2} {H : SimpleGraph W}, ⊤.IsIndContained H ↔ ⊤.IsContained H
-- Mathlib.Data.List.Duplicate
List.exists_duplicate_iff_not_nodup : ∀ {α : Type u_1} {l : List α}, (∃ x, List.Duplicate x l) ↔ ¬l.Nodup
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The map from the target of `f` to `cokernel f`.  -/
CategoryTheory.Limits.cokernel.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → (f : X ⟶ Y) → [inst_2 : CategoryTheory.Limits.HasCokernel f] → Y ⟶ CategoryTheory.Limits.cokernel f
-- Lean.Meta.Tactic.Grind.Anchor
_private.Lean.Meta.Tactic.Grind.Anchor.0.Lean.Meta.Grind.getNumDigitsForAnchors.go : {α : Type u_1} → [Lean.Meta.Grind.HasAnchor α] → Array α → ℕ → ℕ
-- Mathlib.Geometry.Manifold.IsManifold.Basic
instModuleTangentSpace : {𝕜 : 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) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] → [inst_5 : ChartedSpace H M] → (_x : M) → Module 𝕜 (TangentSpace I _x)
-- Mathlib.Analysis.InnerProductSpace.Projection.Minimal
/-- **Existence of minimizers**, aka the **Hilbert projection theorem**.

Let `u` be a point in a real inner product space, and let `K` be a nonempty complete convex subset.
Then there exists a (unique) `v` in `K` that minimizes the distance `‖u - v‖` to `u`.  -/
exists_norm_eq_iInf_of_complete_convex : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {K : Set F},
  K.Nonempty → IsComplete K → Convex ℝ K → ∀ (u : F), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
-- Mathlib.Analysis.Convex.Gauge
gauge_le_of_mem : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} {a : ℝ},
  0 ≤ a → x ∈ a • s → gauge s x ≤ a
-- Mathlib.Order.Filter.CardinalInter
Filter.instCardinalInterFilterComap : ∀ {α β : Type u} {c : Cardinal.{u}} (l : Filter β) [CardinalInterFilter l c] (f : α → β),
  CardinalInterFilter (Filter.comap f l) c
-- Lean.Elab.Command
Lean.Elab.Command.Linter.mk.injEq : ∀ (run : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit)
  (name : autoParam Lean.Name Lean.Elab.Command.Linter.name._autoParam)
  (run_1 : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit)
  (name_1 : autoParam Lean.Name Lean.Elab.Command.Linter.name._autoParam),
  ({ run := run, name := name } = { run := run_1, name := name_1 }) = (run = run_1 ∧ name = name_1)
-- Mathlib.RepresentationTheory.Irreducible
/-- **Alias** of `Representation.isSimpleModule_iff_irreducible_ofModule`. -/
Representation.is_simple_module_iff_irreducible_ofModule : ∀ {G : Type u_1} {k : Type u_2} [inst : Monoid G] [inst_1 : Field k] (M : Type u_5) [inst_2 : AddCommGroup M]
  [inst_3 : Module (MonoidAlgebra k G) M],
  IsSimpleModule (MonoidAlgebra k G) M ↔ (Representation.ofModule M).IsIrreducible
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
equivTangentBundleProd_symm_apply_proj : ∀ {𝕜 : 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) (M : Type u_4)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
  (M' : Type u_7) [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
  (p : TangentBundle I M × TangentBundle I' M'), ((equivTangentBundleProd I M I' M').symm p).proj = (p.1.proj, p.2.proj)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] (s : Set β), s -ᵥ ∅ = ∅
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.findFinIdx?.loop.eq_def : ∀ {α : Type u} (p : α → Bool) (as : Array α) (j : ℕ),
  Array.findFinIdx?.loop✝ p as j =
    if h : j < as.size then if p as[j] = true then some ⟨j, h⟩ else Array.findFinIdx?.loop✝ p as (j + 1) else none
-- Mathlib.Order.Bounds.Image
image2_lowerBounds_upperBounds_subset_lowerBounds_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → Set.image2 f (lowerBounds s) (upperBounds t) ⊆ lowerBounds (Set.image2 f s t)
-- Mathlib.CategoryTheory.Limits.Connected
/-- The obvious cocone of a constant functor.  -/
CategoryTheory.Limits.constCocone : (J : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        (X : C) → CategoryTheory.Limits.Cocone ((CategoryTheory.Functor.const J).obj X)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.to_sep : ∀ {α : Type u_1} [inst : Preorder α] {t₁ t₂ : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} {x : α},
  t₁.Bounded o₁ ↑x → t₂.Bounded (↑x) o₂ → Ordnode.All (fun y => Ordnode.All (fun z => y < z) t₂) t₁
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The forgetful functor from monoid objects to the ambient category.  -/
CategoryTheory.Mon.forget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Functor (CategoryTheory.Mon C) C
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsExtTangentAt.symm : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P} {p : P},
  s₁.IsExtTangentAt s₂ p → s₂.IsExtTangentAt s₁ p
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- The logarithm as a function `Mᵐ⁰ → M` with junk value `log 0 = 0`.  -/
WithZero.log : {M : Type u_4} → [AddMonoid M] → WithZero (Multiplicative M) → M
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueData_t' : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (i j k : ↑X.affineOpens),
  I.glueData.t' i j k =
    CategoryTheory.Limits.pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
      (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯
-- Mathlib.Data.Nat.ChineseRemainder
Nat.modEq_list_map_prod_iff : ∀ {ι : Type u_1} {a b : ℕ} {s : ι → ℕ} {l : List ι},
  List.Pairwise (Function.onFun Nat.Coprime s) l → (a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i])
-- Init.Data.Vector.Monadic
Vector.mapM_congr : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] {xs ys : Vector α n},
  xs = ys → ∀ {f : α → m β}, Vector.mapM f xs = Vector.mapM f ys
-- Mathlib.Topology.UniformSpace.Defs
/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is reflexive.  -/
tendsto_diag_uniformity : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] (f : β → α) (l : Filter β),
  Filter.Tendsto (fun x => (f x, f x)) l (uniformity α)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.map_add' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.AddMonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal] (f g : X ⟶ M), F.map (f + g) = F.map f + F.map g
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
/-- This is an implementation of `prefixFunction` that follows the efficient procedure employed by
the `buildTable` function.
 -/
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunctionRecurrence : (pat : ByteArray) → (stackPos : ℕ) → stackPos < pat.size → (guess : ℕ) → guess < stackPos → ℕ
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
/-- A lift of a morphism to the free bicategory.
This should only exist for "structural" morphisms.  -/
Mathlib.Tactic.BicategoryCoherence.LiftHom.lift : {B : Type u} →
  {inst : CategoryTheory.Bicategory B} →
    {a b : B} →
      (f : a ⟶ b) →
        [self : Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
          CategoryTheory.FreeBicategory.of.obj a ⟶ CategoryTheory.FreeBicategory.of.obj b
-- Mathlib.LinearAlgebra.Prod
Submodule.map_inr : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (q : Submodule R M₂), Submodule.map (LinearMap.inr R M M₂) q = ⊥.prod q
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.associator_hom_left_snd_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X) {Z : C} (h : S.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd R.hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.hom T.hom) S.hom))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.hom T.hom) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj R S).hom T.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd R.hom S.hom) h)