mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesImage.factorThruImage_iso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasCokernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))] {Z : D}
  (h : CategoryTheory.Abelian.image (F.map f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.factorThruImage f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesImage.iso F f).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.factorThruImage (F.map f)) h
-- Aesop.Stats.Basic
Aesop.ForwardStateStats.mk : Array Aesop.ForwardRuleStateStats → Aesop.ForwardStateStats
-- Mathlib.Algebra.Order.Group.Finset
Multiset.toFinset_nsmul : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (n : ℕ), n ≠ 0 → (n • s).toFinset = s.toFinset
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.toIsometryEquiv_injective : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : EquivLike F α β] [inst_3 : IsometryClass F α β], Function.Injective IsometryClass.toIsometryEquiv
-- Mathlib.GroupTheory.Exponent
AddMonoid.lcm_addOrderOf_dvd_exponent : ∀ (G : Type u) [inst : AddMonoid G] [inst_1 : Fintype G], Finset.univ.lcm addOrderOf ∣ AddMonoid.exponent G
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_zero : ∀ {R : Type u} [inst : Semiring R] {x : R}, Polynomial.eval x 0 = 0
-- Mathlib.Topology.Order.LocalExtr
/-- If `f` is antitone to the left and monotone to the right, then it has a local minimum.  -/
isLocalMin_of_anti_mono' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {β : Type u_2} [inst_2 : Preorder β] {b : α}
  {f : α → β} {a : Set α},
  a ∈ nhdsWithin b (Set.Iic b) →
    ∀ {c : Set α}, c ∈ nhdsWithin b (Set.Ici b) → AntitoneOn f a → MonotoneOn f c → IsLocalMin f b
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- If there exists `j` and `k : ℕ`, such that `a j = -k`, then the hypergeometric series is finite
and has convergence radius `∞`.  -/
Complex.radius_regularizedHGFunSeries_eq_top_of_finite : ∀ {a b : Multiset ℂ} {n : ℕ} {j : ℂ}, j ∈ a → j = -↑n → (Complex.regularizedHGFunSeries a b).radius = ⊤
-- Mathlib.Topology.AlexandrovDiscrete
closure_sUnion : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] (S : Set (Set α)),
  closure (⋃₀ S) = ⋃ s ∈ S, closure s
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.instRing : {R : Type u_1} →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] → [Module ι (Additive ℤˣ)] → Ring (GradedTensorProduct R 𝒜 ℬ)
-- Init.Data.Array.Find
Array.findIdx?_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α} {p : α → Bool},
  Array.findIdx? p (Array.replicate n a) = if 0 < n ∧ p a = true then some 0 else none
-- Mathlib.Algebra.Lie.Prod
LieEquiv.prodComm_toFun : ∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (a : L₁ × L₂), (LieEquiv.prodComm R L₁ L₂) a = a.swap
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Create a `FiniteMulArchimedeanClass` from a non-one element.  -/
FiniteMulArchimedeanClass.mk : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedMonoid M] → (a : M) → a ≠ 1 → FiniteMulArchimedeanClass M
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- If `a : ZMod p` is nonzero, then `a^(p/2)` is either `1` or `-1`.  -/
ZMod.pow_div_two_eq_neg_one_or_one : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {a : ZMod p}, a ≠ 0 → a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_comp_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X W] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Z W]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct Y W],
  CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id W))
      (CategoryTheory.Limits.prod.map g (CategoryTheory.CategoryStruct.id W))
-- Std.Http.Data.Chunk
/-- Retrieves the first value for the given trailer header name.
Returns `none` if absent.
 -/
Std.Http.Trailer.get? : Std.Http.Trailer → Std.Http.Header.Name → Option Std.Http.Header.Value
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.closure_sdiff_singleton_ssubset : ∀ {α : Type u_2} {M : Matroid α} {e : α} {I : Set α}, M.Indep I → e ∈ I → M.closure (I \ {e}) ⊂ M.closure I
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.isoOfEquivalence_hom_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasLimit F] {G : CategoryTheory.Functor K C}
  [inst_4 : CategoryTheory.Limits.HasLimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfEquivalence e w).hom
      (CategoryTheory.Limits.limit.π G k) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F (e.inverse.obj k))
      (CategoryTheory.CategoryStruct.comp (w.inv.app (e.inverse.obj k)) (G.map (e.counit.app k)))
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.supp_eq : ∀ {n : ℕ} {P : MvPFunctor.{u} n} {α : TypeVec.{u} n} (a : P.A) (f : (P.B a).Arrow α) (i : Fin2 n),
  MvFunctor.supp ⟨a, f⟩ i = f i '' Set.univ
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.dvd_pow_natDegree_of_aeval_eq_zero : ∀ {R : Type u} {A : Type u_1} [inst : CommRing R] [inst_1 : CommRing A] [IsDomain R] [inst_3 : Algebra R A]
  [Nontrivial A] [Module.IsTorsionFree R A] {p : Polynomial R},
  p.Monic →
    ∀ (x y : R) (z : A), (Polynomial.aeval z) p = 0 → z * (algebraMap R A) x = (algebraMap R A) y → x ∣ y ^ p.natDegree
-- Plausible.Testable
/-- Enable basic tracing of shrinking.
 -/
Plausible.Configuration.traceShrink : Plausible.Configuration → Bool
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.map_obj_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] {X Y : T} [inst_2 : P.IsStableUnderComposition]
  {f : X ⟶ Y} (hPf : P f)
  (X_1 :
    CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.fromPUnit Y) (CategoryTheory.Functor.id T) P ⊤ Q),
  ((CategoryTheory.MorphismProperty.Under.map Q hPf).obj X_1).right = X_1.right
-- Std.Time.Date.Unit.Day
/-- Creates an `Offset` from an integer.
 -/
Std.Time.Day.Offset.ofInt : ℤ → Std.Time.Day.Offset
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.fppfTopology_le_fpqcTopology : AlgebraicGeometry.Scheme.fppfTopology ≤ AlgebraicGeometry.Scheme.fpqcTopology
-- Aesop.Frontend.Extension
Aesop.Frontend.getGlobalRuleSetData : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      [MonadLiftT IO m] →
        [MonadLiftT Lean.CoreM m] →
          Aesop.RuleSetName →
            m
              (Aesop.RuleSetExtension ×
                Lean.Name × Lean.Meta.SimpExtension × Lean.Name × Lean.Meta.Simp.SimprocExtension)
-- Lean.Server.Requests
_private.Lean.Server.Requests.0.Lean.Server.getState! : String → Dynamic → (stateType : Type) → [TypeName stateType] → Lean.Server.RequestM stateType
-- Mathlib.Algebra.Order.Quantale
AddQuantale.add_bot : ∀ {α : Type u_3} [inst : AddSemigroup α] [inst_1 : CompleteLattice α] [IsAddQuantale α] {x : α}, x + ⊥ = ⊥
-- Mathlib.Algebra.Field.Basic
div_sub_div_same : ∀ {K : Type u_1} [inst : DivisionRing K] (a b c : K), a / c - b / c = (a - b) / c
-- Init.Data.Array.Attach
Array.flatMap_unattach : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : Array (Subtype P)} {f : α → Array β},
  Array.flatMap f xs.unattach =
    Array.flatMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
      xs
-- Lean.Message
Lean.MessageData.ofLazy.injEq : ∀ (f : Option Lean.PPContext → BaseIO Dynamic) (hasSyntheticSorry : Lean.MetavarContext → Bool)
  (f_1 : Option Lean.PPContext → BaseIO Dynamic) (hasSyntheticSorry_1 : Lean.MetavarContext → Bool),
  (Lean.MessageData.ofLazy f hasSyntheticSorry = Lean.MessageData.ofLazy f_1 hasSyntheticSorry_1) =
    (f = f_1 ∧ hasSyntheticSorry = hasSyntheticSorry_1)
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ_w_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q₁ q₂ : ℕ) (hq : q₁ ≤ q₂)
  {Z : CochainComplex C ℤ}
  (h : ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op q₁)).obj.mid ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q₂)
      (CategoryTheory.CategoryStruct.comp
        ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).map (CategoryTheory.homOfLE hq).op).hom.h
        h) =
    CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q₁) h
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_eq_cfc_norm : ∀ {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] (a : A),
  autoParam (IsSelfAdjoint a) CFC.abs_eq_cfc_norm._auto_1 → CFC.abs a = cfc (fun x => ‖x‖) a
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.submodule_mk'' : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (H : Submodule K V) (h : Module.finrank K ↥H = 1), (Projectivization.mk'' H h).submodule = H
-- Mathlib.Geometry.Euclidean.MongePoint
/-- `mongePointVSubFaceCentroidWeightsWithCircumcenter` sums to 0.  -/
Affine.Simplex.sum_mongePointVSubFaceCentroidWeightsWithCircumcenter : ∀ {n : ℕ} {i₁ i₂ : Fin (n + 3)},
  i₁ ≠ i₂ → ∑ i, Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ i = 0
-- Mathlib.Data.List.Intervals
List.Ico.eq_cons : ∀ {n m : ℕ}, n < m → List.Ico n m = n :: List.Ico (n + 1) m
-- Mathlib.Order.Defs.Unbundled
/-- **Alias** of `Std.Asymm.irrefl`. -/
Std.Asymm.isIrrefl : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Asymm r], Std.Irrefl r
-- Std.Time.DateTime.PlainDateTime
/-- Getter for the `Millisecond` inside of a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.millisecond : Std.Time.PlainDateTime → Std.Time.Millisecond.Ordinal
-- Mathlib.Analysis.SpecialFunctions.Bernstein
bernstein_nonneg : ∀ {n ν : ℕ} {x : ↑unitInterval}, 0 ≤ (bernstein n ν) x
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
/-- A flat morphism, locally of finite presentation is universally open.  -/
AlgebraicGeometry.UniversallyOpen.of_flat : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f]
  [AlgebraicGeometry.LocallyOfFinitePresentation f], AlgebraicGeometry.UniversallyOpen f
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_lt_iff_lt : ∀ {a b : BitVec 16}, { toBitVec := a } < { toBitVec := b } ↔ a < b
-- Lean.DocString.Types
Lean.Doc.Block.ol.sizeOf_spec : ∀ {i : Type u} {b : Type v} [inst : SizeOf i] [inst_1 : SizeOf b] (start : ℤ)
  (items : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))),
  sizeOf (Lean.Doc.Block.ol start items) = 1 + sizeOf start + sizeOf items
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_X₂ : ∀ {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₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁._auto_3),
  (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₂ = X.opcycles f₁₂ f₃ n₁
-- Init.Data.Order.Factories
/-- If an `LE α` instance is transitive and total, then it represents a linear preorder.
 -/
Std.IsLinearPreorder.of_le : ∀ {α : Type u} [inst : LE α]
  (le_trans :
    autoParam (Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2)
      Std.IsLinearPreorder.of_le._auto_1),
  autoParam (Std.Total fun x1 x2 => x1 ≤ x2) Std.IsLinearPreorder.of_le._auto_3 → Std.IsLinearPreorder α
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.addUnit_eq_addUnit_of_mem_ofAddUnits : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h₁ : IsAddUnit x) (h₂ : x ∈ S.ofAddUnits),
  h₁.addUnit = S.addUnit_of_mem_ofAddUnits h₂
-- Mathlib.Topology.Sheaves.Presheaf
/-- Pulling back along a homeomorphism is the same as pushing forward along its inverse.  -/
TopCat.Presheaf.pullbackHomIsoPushforwardInv : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} → (H : X ≅ Y) → TopCat.Presheaf.pullback C H.hom ≅ TopCat.Presheaf.pushforward C H.inv
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAtFilter.isTheta_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L → f' ≠ 0 → (fun p => f p.1 - f p.2) =Θ[L] fun p => p.1 - p.2
-- Mathlib.Analysis.RCLike.Basic
RCLike.nnratCast_re : ∀ {K : Type u_1} [inst : RCLike K] (q : ℚ≥0), RCLike.re ↑q = ↑q
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- If `L` preserves colimits and `ℰ` has them, then it is a left adjoint. Note this is a (partial)
converse to `leftAdjointPreservesColimits`.
 -/
CategoryTheory.Presheaf.isLeftAdjoint_of_preservesColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (L : CategoryTheory.Functor (CategoryTheory.Functor C (Type (max w v₁ v₂))) ℰ)
  [CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
        max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
      L]
  [CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension
      (CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp
        ((CategoryTheory.opOpEquivalence C).congrLeft.functor.comp L))],
  L.IsLeftAdjoint
-- Mathlib.Topology.Order.WithTop
WithTop.continuousOn_untopA : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [inst_3 : Nonempty ι],
  ContinuousOn WithTop.untopA {a | a ≠ ⊤}
-- Lean.ErrorExplanation
Lean.ErrorExplanation.mk.sizeOf_spec : ∀ (doc : String) (metadata : Lean.ErrorExplanation.Metadata) (declLoc? : Option Lean.DeclarationLocation),
  sizeOf { doc := doc, metadata := metadata, declLoc? := declLoc? } = 1 + sizeOf doc + sizeOf metadata + sizeOf declLoc?
-- Init.Data.Array.Lemmas
/-- Converts an array to a list that contains the same elements in the opposite order.

This is equivalent to, but more efficient than, `Array.toList ∘ List.reverse`.

Examples:
* `#[1, 2, 3].toListRev = [3, 2, 1]`
* `#["blue", "yellow"].toListRev = ["yellow", "blue"]`
 -/
Array.toListRev : {α : Type u_1} → Array α → List α
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFinset_map_of_equiv : ∀ {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) [inst : Fintype α] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] [inst_3 : Fintype β] [inst_4 : DecidableEq β] (e : α ≃ β) (n : ℕ),
  (SimpleGraph.map (⇑e) G).cliqueFinset n =
    Finset.map { toFun := Finset.map e.toEmbedding, inj' := ⋯ } (G.cliqueFinset n)
-- Mathlib.Control.Bifunctor
Bifunctor.fst_comp_snd : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α₀ α₁ : Type u₀} {β₀ β₁ : Type u₁}
  (f : α₀ → α₁) (f' : β₀ → β₁), Bifunctor.fst f ∘ Bifunctor.snd f' = bimap f f'
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.val_step_filterMap.match_1.splitter : {γ : Type u_1} →
  (motive : Option γ → Sort u_2) → (x : Option γ) → (Unit → motive none) → ((out' : γ) → motive (some out')) → motive x
-- Mathlib.Tactic.CongrExclamation
CongrState : Type
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A minimally connected graph is a tree.  -/
SimpleGraph.isTree_of_minimal_connected : ∀ {V : Type u_1} {G : SimpleGraph V}, Minimal SimpleGraph.Connected G → G.IsTree
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_subgroup_left_iff_existsUnique_quotientMk'' : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G},
  Subgroup.IsComplement (↑H) T ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t, Quotient.mk'' ↑t = q
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.HasTemperateGrowth.const : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (c : F), Function.HasTemperateGrowth fun x => c
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (f : CategoryTheory.MonoOver X),
  CategoryTheory.Mono f.arrow
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.comap_le_comap_of_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {K L : Subgroup N},
  Function.Surjective ⇑f → (Subgroup.comap f K ≤ Subgroup.comap f L ↔ K ≤ L)
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.instConcreteCategorySubtypeForallCarrierUniformContinuous : CategoryTheory.ConcreteCategory UniformSpaceCat fun x1 x2 => { f // UniformContinuous f }
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.Iter.Equiv.toIterM : ∀ {α₁ α₂ β : Type u_1} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] {ita : Std.Iter β}
  {itb : Std.Iter β}, ita.Equiv itb → ita.toIterM.Equiv itb.toIterM
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.LaxMonoidalFunctor.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (toFunctor : CategoryTheory.Functor C D) →
              autoParam toFunctor.LaxMonoidal CategoryTheory.LaxMonoidalFunctor.laxMonoidal._autoParam →
                CategoryTheory.LaxMonoidalFunctor C D
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The type of objects for the diagram indexing a pushout, defined as a special case of
`WidePushoutShape`.
 -/
CategoryTheory.Limits.WalkingSpan : Type
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ContinuousOn.const_cpow : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℂ} {s : Set α} {b : ℂ},
  ContinuousOn f s → (b ≠ 0 ∨ ∀ a ∈ s, f a ≠ 0) → ContinuousOn (fun x => b ^ f x) s
-- Mathlib.Order.WellFoundedSet
/-- `a` is accessible under the relation `r` iff `r` is well-founded on the downward transitive
closure of `a` under `r` (including `a` or not).  -/
Set.WellFoundedOn.acc_iff_wellFoundedOn : ∀ {α : Type u_6} {r : α → α → Prop} {a : α},
  [Acc r a, {b | Relation.ReflTransGen r b a}.WellFoundedOn r, {b | Relation.TransGen r b a}.WellFoundedOn r].TFAE
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
range_pow_padicValNat_subset_divisors : ∀ {p n : ℕ}, n ≠ 0 → Finset.image (fun x => p ^ x) (Finset.range (padicValNat p n + 1)) ⊆ n.divisors
-- Mathlib.Tactic.TacticAnalysis
/-- Stores the configuration for a tactic analysis pass.

This provides the low-level interface into the tactic analysis framework.
 -/
Mathlib.TacticAnalysis.Config : Type
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- The category of augmented simplicial sets, as a particular case of
augmented simplicial objects.  -/
SSet.Augmented : Type (u + 1)
-- Lean.Util.MonadCache
Lean.instMonadCacheExceptTOfMonad : {α β ε : Type} → {m : Type → Type} → [Lean.MonadCache α β m] → [Monad m] → Lean.MonadCache α β (ExceptT ε m)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasSum_single : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} (b : β),
  (∀ (b' : β), b' ≠ b → f b' = 0) →
    ∀ (L : optParam (SummationFilter β) (SummationFilter.unconditional β)) [L.LeAtTop], HasSum f (f b) L
-- Mathlib.Analysis.RCLike.Basic
IsSelfAdjoint.I_smul_mem_skewAdjoint : ∀ {K : Type u_1} [inst : RCLike K] {A : Type u_3} [inst_1 : AddCommGroup A] [inst_2 : StarAddMonoid A]
  [inst_3 : Module K A] [StarModule K A] {a : A}, IsSelfAdjoint a → RCLike.I • a ∈ skewAdjoint A
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.continuousGeneratedBy_def : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] (g : Y → Z),
  Topology.ContinuousGeneratedBy X g ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous (g ∘ ⇑f)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j'),
  c.prev j = i →
    c'.prev j' = i' →
      ∀ (hk : c.next j = k) (hk' : c'.next j' = k') (cone : CategoryTheory.Limits.KernelFork (K.d j k))
        (hcone : CategoryTheory.Limits.IsLimit cone) ⦃W : C⦄ (φ : cone.pt ⟶ W),
        CategoryTheory.CategoryStruct.comp (hcone.lift (CategoryTheory.Limits.KernelFork.ofι (K.d i j) ⋯)) φ = 0 ↔
          CategoryTheory.CategoryStruct.comp
              ((HomologicalComplex.extend.leftHomologyData.isLimitKernelFork K e hj' hk hk' cone hcone).lift
                (CategoryTheory.Limits.KernelFork.ofι ((K.extend e).d i' j') ⋯))
              φ =
            0