mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.ι_D₂ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : ⋯ = j)
  [inst_23 : ⋯], ⋯
-- Init.Control.State
StateT.monadControl : (σ : Type u) → (m : Type u → Type v) → [Monad m] → MonadControl m (StateT σ m)
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.snd_comp_inl : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β], (OrderAddMonoidHom.snd α β).comp (OrderAddMonoidHom.inl α β) = 0
-- Mathlib.Logic.Equiv.Defs
/-- The `Sort` of proofs of a true proposition is equivalent to `PUnit`.  -/
Equiv.propEquivPUnit : {p : Prop} → p → p ≃ PUnit.{0}
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- Stereographic projection, reverse direction.  This is a map from the orthogonal complement of a
unit vector `v` in an inner product space `E` to the unit sphere in `E`.  -/
stereoInvFun : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] → {v : E} → ‖v‖ = 1 → ↥(ℝ ∙ v)ᗮ → ↑(Metric.sphere 0 1)
-- Mathlib.GroupTheory.Nilpotent
Group.IsNilpotent.mk : ∀ {G : Type u_2} [inst : Group G], (∃ n, Subgroup.upperCentralSeries G n = ⊤) → Group.IsNilpotent G
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.equivMapDomain_eq_mapDomain : ∀ {k : Type u_1} {G : Type u_2} {H : Type u_3} [inst : AddCommMonoid k] (f : G ≃ H) (l : SkewMonoidAlgebra k G),
  SkewMonoidAlgebra.equivMapDomain f l = (SkewMonoidAlgebra.mapDomain ⇑f) l
-- Mathlib.Order.Lattice.Nat
Nat.sInf_empty : sInf ∅ = 0
-- Batteries.Tactic.NoMatch
/-- The syntax `match ⋯ with.` has been deprecated in favor of `nomatch ⋯`.

Both now support multiple discriminants.
 -/
Batteries.Tactic.matchWithDot : Lean.ParserDescr
-- Mathlib.RingTheory.Ideal.Operations
Finsupp.mem_ideal_span_range_iff_exists_finsupp : ∀ {α : Type u_1} {R : Type u_2} [inst : Semiring R] {x : R} {v : α → R},
  x ∈ Ideal.span (Set.range v) ↔ ∃ c, (c.sum fun i a => a * v i) = x
-- Mathlib.Order.SuccPred.Basic
SuccOrder.ofCore_succ : ∀ {α : Type u_1} [inst : LinearOrder α] (succ : α → α) (hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b)
  (hm : ∀ (a : α), IsMax a → succ a = a) (a : α), SuccOrder.succ a = succ a
-- Init.Data.List.MinMaxIdx
List.maxIdxOn.congr_simp : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] {inst_1 : DecidableLE β} [inst_2 : DecidableLE β] (f f_1 : α → β),
  f = f_1 → ∀ (xs xs_1 : List α) (e_xs : xs = xs_1) (h : xs ≠ []), List.maxIdxOn f xs h = List.maxIdxOn f_1 xs_1 ⋯
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
/-- This is the map from `i`-cochains to `j`-cocycles induced by the differential in the complex of
inhomogeneous cochains.  -/
groupCohomology.toCocycles : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → (i j : ℕ) → (groupCohomology.inhomogeneousCochains A).X i ⟶ groupCohomology.cocycles A j
-- Mathlib.Order.Category.HeytAlg
HeytAlg.ofHom_hom : ∀ {X Y : HeytAlg} (f : X ⟶ Y), HeytAlg.ofHom (HeytAlg.Hom.hom f) = f
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
/-- In the category of simplicial sets, an *inner* anodyne extension is a morphism
that has the left lifting property with respect to *inner* fibrations, where
an inner fibration is a morphism that has the right lifting property with respect
to inner horn inclusions.  -/
SSet.innerAnodyneExtensions : CategoryTheory.MorphismProperty SSet
-- Init.Data.UInt.Lemmas
USize.ofBitVec_add : ∀ (a b : BitVec System.Platform.numBits), { toBitVec := a + b } = { toBitVec := a } + { toBitVec := b }
-- Lean.Elab.App
Lean.Elab.Term.ElabElim.State.mk.sizeOf_spec : ∀ (f fType : Lean.Expr) (namedArgs : List Lean.Elab.Term.NamedArg) (args : List Lean.Elab.Term.Arg)
  (instMVars : Array Lean.MVarId) (idx : ℕ) (motive? : Option Lean.Expr),
  sizeOf
      { f := f, fType := fType, namedArgs := namedArgs, args := args, instMVars := instMVars, idx := idx,
        motive? := motive? } =
    1 + sizeOf f + sizeOf fType + sizeOf namedArgs + sizeOf args + sizeOf instMVars + sizeOf idx + sizeOf motive?
-- Mathlib.Data.Fintype.BigOperators
Finset.card_pi : ∀ {ι : Type u_4} {α : ι → Type u_6} [inst : DecidableEq ι] (s : Finset ι) (t : (i : ι) → Finset (α i)),
  (s.pi t).card = ∏ i ∈ s, (t i).card
-- Init.Control.Except
/-- Returns `none` if an exception was thrown, or `some` around the value on success.

Examples:
* `(pure 10 : Except String Nat).toOption = some 10`
* `(throw "Failure" : Except String Nat).toOption = none`
 -/
Except.toOption : {ε : Type u} → {α : Type u_1} → Except ε α → Option α
-- Lean.Parser.Types
Lean.Parser.ParserState.next' : Lean.Parser.ParserState →
  (c : Lean.Parser.ParserContext) → (pos : String.Pos.Raw) → ¬c.atEnd pos = true → Lean.Parser.ParserState
-- Std.Time.Format.Modifier
/-- `h`: Clock hour of AM/PM (1-12) (e.g., 12).
 -/
Std.Time.Modifier.h : Std.Time.Number → Std.Time.Modifier
-- Batteries.Data.Fin.Lemmas
Fin.exists_minimal_of_findSomeRev?_eq_some : ∀ {n : ℕ} {α : Type u_1} {x : α} {f : Fin n → Option α},
  Fin.findSomeRev? f = some x → ∃ i, f i = some x ∧ ∀ (j : Fin n), i < j → f j = none
-- Mathlib.Data.Part
Part.instMul : {α : Type u_1} → [Mul α] → Mul (Part α)
-- Mathlib.CategoryTheory.Monoidal.Skeleton
CategoryTheory.Skeleton.mul_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y : CategoryTheory.Skeleton C),
  X * Y = CategoryTheory.toSkeleton (CategoryTheory.MonoidalCategoryStruct.tensorObj (Quotient.out X) (Quotient.out Y))
-- Init.MetaTypes
/-- When `true` (default: `true`), reduces projections of structure constructors.
 -/
Lean.Meta.Simp.Config.proj : Lean.Meta.Simp.Config → Bool
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.basisLeft.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  Algebra.Generators.PresentationOfFreeCotangent.Aux.basisLeft✝ D =
    b.map (Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentEquiv✝ D).symm
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
  (∃ inv,
      CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id X ∧
        CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id Y) →
    CategoryTheory.IsIso f
-- Init.Data.BitVec.Lemmas
BitVec.add_left_neg : ∀ {w : ℕ} (x : BitVec w), -x + x = 0#w
-- Init.Data.List.Lemmas
List.init_eq_of_concat_eq : ∀ {α : Type u_1} {a b : α} {l₁ l₂ : List α}, l₁.concat a = l₂.concat b → l₁ = l₂
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.extendWith_none : ∀ {ι : Type u} {α : Option ι → Type v} [inst : (i : Option ι) → Zero (α i)] (f : Π₀ (i : ι), α (some i)) (a : α none),
  (DFinsupp.extendWith a f) none = a
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanIso.congr : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f₁ f₂ : α → β}
  {n : ℕ}, IsMulFreimanIso n A B f₁ → Set.EqOn f₁ f₂ A → IsMulFreimanIso n A B f₂
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
/-- If `G` preserves equalizers and `C` has them, then the fork constructed of the mapped morphisms of
a fork is a limit.
 -/
CategoryTheory.Limits.isLimitOfHasEqualizerOfPreservesLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {X Y : C} →
            (f g : X ⟶ Y) →
              [inst_2 : CategoryTheory.Limits.HasEqualizer f g] →
                [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G] →
                  CategoryTheory.Limits.IsLimit
                    (CategoryTheory.Limits.Fork.ofι (G.map (CategoryTheory.Limits.equalizer.ι f g)) ⋯)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.finrank_top' : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  Module.finrank F ↥⊤ = Module.finrank F E
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.congr_arg : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] {e : A ≃ₗc[R] B} {x x' : A}, x = x' → e x = e x'
-- Mathlib.Algebra.Ring.Units
Units.divp_add_divp_same : ∀ {α : Type u} [inst : Semiring α] (a b : α) (u : αˣ), a /ₚ u + b /ₚ u = (a + b) /ₚ u
-- Mathlib.Data.Nat.Bits
Nat.bodd_add : ∀ (m n : ℕ), (m + n).bodd = (m.bodd ^^ n.bodd)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreToInt.injEq : ∀ (e : Lean.Expr) (pos : Bool) (toIntThm : Lean.Expr) (lhs rhs : Int.Internal.Linear.Expr) (e_1 : Lean.Expr)
  (pos_1 : Bool) (toIntThm_1 : Lean.Expr) (lhs_1 rhs_1 : Int.Internal.Linear.Expr),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreToInt e pos toIntThm lhs rhs =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreToInt e_1 pos_1 toIntThm_1 lhs_1 rhs_1) =
    (e = e_1 ∧ pos = pos_1 ∧ toIntThm = toIntThm_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.continuousAt_iff_isLittleO : ∀ {F : Type u_4} [inst : Norm F] {α : Type u_17} {E : Type u_18} [inst_1 : NormedRing E] [inst_2 : One F]
  [NormOneClass F] [inst_4 : TopologicalSpace α] {f : α → E} {x : α},
  ContinuousAt f x ↔ (fun x_1 => f x_1 - f x) =o[nhds x] fun x => 1
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.mk.sizeOf_spec : ∀ {A : Type u} [inst : Ring A] [inst_1 : SizeOf A] (G : Type w₀) (R : Type w₁) (relation : R → G →₀ A),
  sizeOf { G := G, R := R, relation := relation } = 1 + sizeOf G + sizeOf R
-- Mathlib.Algebra.Order.Group.Cone
LinearOrder.mkOfGroupCone.eq_1 : ∀ {S : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : SetLike S G] (C : S) [inst_2 : GroupConeClass S G]
  [inst_3 : HasMemOrInvMem C] [inst_4 : DecidablePred fun x => x ∈ C],
  LinearOrder.mkOfGroupCone C =
    { toPartialOrder := PartialOrder.mkOfGroupCone C, min := fun a b => if a ≤ b then a else b,
      max := fun a b => if a ≤ b then b else a, compare := fun a b => compareOfLessAndEq a b, le_total := ⋯,
      toDecidableLE := fun x b => inst_4 (b / x), toDecidableEq := decidableEqOfDecidableLE,
      toDecidableLT := decidableLTOfDecidableLE, min_def := ⋯, max_def := ⋯, compare_eq_compareOfLessAndEq := ⋯ }
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.Result.ofNat_ctorIdx : ∀ (x : Std.Tactic.BVDecide.LRAT.Internal.Result), Std.Tactic.BVDecide.LRAT.Internal.Result.ofNat x.ctorIdx = x
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.minValueSealed_def : Int32.minValueSealed✝ = Int32.minValue
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
/-- If `R` is a projective resolution of `X`, then `Ext X Y n` identifies
to the type of cohomology classes of degree `n` from `R.cochainComplex`
to `(singleFunctor C 0).obj Y`.  -/
CategoryTheory.ProjectiveResolution.extEquivCohomologyClass : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y : C} →
          (R : CategoryTheory.ProjectiveResolution X) →
            {n : ℕ} →
              CategoryTheory.Abelian.Ext X Y n ≃
                CochainComplex.HomComplex.CohomologyClass R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n
-- Init.Data.Nat.Lemmas
Nat.mul_dvd_mul_iff_left : ∀ {a b c : ℕ}, 0 < a → (a * b ∣ a * c ↔ b ∣ c)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.isFiniteMeasure_map_iff : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [mβ : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : α → β},
  AEMeasurable f μ → (MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.IsFiniteMeasure μ)
-- Mathlib.CategoryTheory.Monad.Algebra
/-- A morphism of Eilenberg–Moore algebras for the monad `T`.  -/
CategoryTheory.Monad.Algebra.Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {T : CategoryTheory.Monad C} → T.Algebra → T.Algebra → Type v₁
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (aig : Std.Sat.AIG α) → Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput aig → Std.Sat.AIG.Entrypoint α
-- Mathlib.Topology.Algebra.InfiniteSum.Module
HasSum.smul_const : ∀ {ι : Type u_5} {R : Type u_7} {M : Type u_9} [inst : Semiring R] [inst_1 : TopologicalSpace R]
  [inst_2 : TopologicalSpace M] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [ContinuousSMul R M] {f : ι → R}
  {L : SummationFilter ι} {r : R}, HasSum f r L → ∀ (a : M), HasSum (fun z => f z • a) (r • a) L
-- Init.Grind.Order
Lean.Grind.Order.le_of_eq_2 : ∀ {α : Type u_1} [inst : LE α] [Std.IsPreorder α] {a b : α}, a = b → b ≤ a
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- A rewrite with a lemma from the current file  -/
Mathlib.Tactic.LibraryRewrite.Kind.fromFile : Mathlib.Tactic.LibraryRewrite.Kind
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear equivs on the right respects higher differentiability on
domains.  -/
ContinuousLinearEquiv.contDiffOn_comp_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {n : WithTop ℕ∞} (e : G ≃L[𝕜] E),
  ContDiffOn 𝕜 n (f ∘ ⇑e) (⇑e ⁻¹' s) ↔ ContDiffOn 𝕜 n f s
-- Mathlib.Order.Filter.Pointwise
Filter.zero_prod_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Zero β], 0 ×ˢ 0 = 0
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.mor.sizeOf_spec : ∀ (thm : Mathlib.Meta.FunProp.GeneralTheorem), sizeOf (Mathlib.Meta.FunProp.Theorem.mor thm) = 1 + sizeOf thm
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- The isomorphism giving rise to the oplax unity constraint  -/
CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F : CategoryTheory.OplaxFunctor B C} →
          F.PseudoCore →
            (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a)
-- Mathlib.Order.Bounds.Basic
bddBelow_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, BddBelow (Set.Ioi a)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.instT0Space : ∀ {R : Type u} [inst : CommSemiring R], T0Space (PrimeSpectrum R)
-- Init.Data.Vector.Lemmas
Vector.reverse_reverse : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n), xs.reverse.reverse = xs
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.any_eq_true_iff_exists_mem_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  {p : α → β → Bool}, m.WF → (m.any p = true ↔ ∃ a, ∃ (h : a ∈ m), p a (Std.DHashMap.Raw.Const.get m a h) = true)
-- Mathlib.Probability.Kernel.Composition.CompMap
ProbabilityTheory.Kernel.snd_comp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  (η : ProbabilityTheory.Kernel β (γ × δ)), (η.comp κ).snd = η.snd.comp κ
-- Mathlib.LinearAlgebra.AffineSpace.Restrict
AffineEquiv.affineSubspaceMap_apply_symm_apply : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (s : AffineSubspace k P₁)
  [inst_7 : Nonempty ↥s] (x : ↥(AffineSubspace.map (↑e) s)), e ↑((e.affineSubspaceMap s).symm x) = ↑x
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- The canonical isomorphism `𝟙_ (ModuleCat R) ≅ (free R).obj (𝟙_ (Type u))`.
(This should not be used directly: it is part of the implementation of the
monoidal structure on the functor `free R`.)  -/
ModuleCat.FreeMonoidal.εIso : (R : Type u) →
  [inst : CommRing R] →
    CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R) ≅
      (ModuleCat.free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Type u))
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- `Differentiable 𝕜 f` means that `f` is differentiable at any point.  -/
Differentiable : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [Module 𝕜 E] →
          [TopologicalSpace E] →
            {F : Type u_3} → [inst_4 : AddCommGroup F] → [Module 𝕜 F] → [TopologicalSpace F] → (E → F) → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Any morphism between initial objects is an isomorphism.  -/
CategoryTheory.Limits.isIso_of_isInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (hX : CategoryTheory.Limits.IsInitial X)
  (hY : CategoryTheory.Limits.IsInitial Y) (f : X ⟶ Y), CategoryTheory.IsIso f
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.compress_mem_compression : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v a : α} [inst_3 : DecidableEq α], a ∈ s → UV.compress u v a ∈ UV.compression u v s
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.im_natCast : ∀ {R : Type u_1} {a b : R} [inst : AddCommMonoidWithOne R] (n : ℕ), (↑n).im = 0
-- Mathlib.Topology.Compactness.SigmaCompact
/-- An [exhaustion by compact sets](https://en.wikipedia.org/wiki/Exhaustion_by_compact_sets) of a
topological space is a sequence of compact sets `K n` such that `K n ⊆ interior (K (n + 1))` and
`⋃ n, K n = univ`.

If `X` is a locally compact sigma compact space, then `CompactExhaustion.choice X` provides
a choice of an exhaustion by compact sets. This choice is also available as
`(default : CompactExhaustion X)`.  -/
CompactExhaustion : (X : Type u_4) → [TopologicalSpace X] → Type u_4
-- Mathlib.Algebra.Order.Hom.Basic
/-- The argument is zero if its image under the map is zero.  -/
RingNormClass.eq_zero_of_map_eq_zero : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : NonUnitalNonAssocRing α}
  {inst_1 : Semiring β} {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : RingNormClass F α β] (f : F) {a : α},
  f a = 0 → a = 0
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- A dependent arrow.  -/
Lean.Meta.RefinedDiscrTree.Key.forall : Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.degree_basisDivisor_self : ∀ {F : Type u_1} [inst : Field F] {x : F}, (Lagrange.basisDivisor x x).degree = ⊥
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.coe_toOrderHom : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (f : α →𝒄 β), ⇑f.toOrderHom = ⇑f
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- A linearly ordered commutative monoid with a zero element.  -/
LinearOrderedCommMonoidWithZero : Type u_3 → Type u_3
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
/-- A type with an iterator typeclass and an inhabitant bundled together. This represents an
arbitrarily typed iterator. It only exists for the construction of the equivalence relation
on iterators.

This type is not meant to be used in executable code. Unbundled `Iter` or `IterM` iterators of a
specific type have better library support and are more efficient.
 -/
Std.BundledIterM : (Type w → Type w') → Type w → Type (max (w + 1) w')
-- Std.Http.Data.Headers.Value
/-- The string data.
 -/
Std.Http.Header.Value.value : Std.Http.Header.Value → String
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.lift.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (x : R) [inst_4 : IsLocalization.Away x S] {g : R →+* P} (hg : IsUnit (g x)),
  IsLocalization.Away.lift x hg = IsLocalization.lift ⋯
-- Mathlib.Order.Hom.Lattice
/-- An `InfHom` preserves infima.

Do not use this directly. Use `map_inf` instead.  -/
InfHom.map_inf' : ∀ {α : Type u_6} {β : Type u_7} [inst : Min α] [inst_1 : Min β] (self : InfHom α β) (a b : α),
  self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.exists_mul_sub_mem_of_sub_one_mem_jacobson : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} (r : R), r - 1 ∈ I.jacobson → ∃ s, s * r - 1 ∈ I
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.instInhabitedOfHasZeroObject : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → [CategoryTheory.Limits.HasZeroObject V] → Inhabited (HomologicalComplex V c)
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
tsum_eq_of_summable_unconditional : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  {f : β → α} [T2Space α] [L.NeBot] [L.LeAtTop], Summable f → ∑'[L] (b : β), f b = ∑' (b : β), f b
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.comp_iff_of_bijective_right : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (e : M →ₗ[R] M') {f : M' →ₗ[R] M''},
  Function.Bijective ⇑e → (IsLocalizedModule S (f ∘ₗ e) ↔ IsLocalizedModule S f)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.ι_ofι : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {P : C} (ι : P ⟶ X)
  (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)),
  (CategoryTheory.Limits.Trident.ofι ι w).ι = ι
-- Plausible.Gen
Plausible.instMonadErrorGen : MonadExcept Plausible.GenError Plausible.Gen