mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.NoncommCoprod
AddMonoidHom.noncommCoprod_apply : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) (mn : M × N),
  (f.noncommCoprod g comm) mn = f mn.1 + g mn.2
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
MeasureTheory.VectorMeasure.norm_apply_le_bound : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  {μ : MeasureTheory.VectorMeasure X E} {s : Set X}, ‖μ s‖ ≤ ↑μ.bound
-- Mathlib.Data.Bool.Basic
Bool.bne_eq_xor : bne = xor
-- Mathlib.Order.GaloisConnection.Basic
/-- Makes a Galois insertion from an order-preserving bijection.  -/
OrderIso.toGaloisInsertion : {α : Type u} → {β : Type v} → [inst : Preorder α] → [inst_1 : Preorder β] → (e : α ≃o β) → GaloisInsertion ⇑e ⇑e.symm
-- Mathlib.FieldTheory.Fixed
FixedPoints.minpoly.monic : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [inst_3 : Fintype G]
  (x : F), (FixedPoints.minpoly G F x).Monic
-- Batteries.Lean.LawfulMonad
instLawfulMonadIO_batteries : LawfulMonad IO
-- Std.Data.ExtTreeMap.Basic
/-- Transforms a list of keys into a tree map.  -/
Std.ExtTreeMap.unitOfList : {α : Type u} →
  List α → (cmp : autoParam (α → α → Ordering) Std.ExtTreeMap.unitOfList._auto_1) → Std.ExtTreeMap α Unit cmp
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- Given a valuation `x` of the variable in an `R`-algebra `A`, `aeval R A x` is
the unique `R`-algebra homomorphism from `R[X]` to `A` sending `X` to `x`.

This is a stronger variant of the linear map `Polynomial.leval`.  -/
Polynomial.aeval : {R : Type u} →
  {A : Type z} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → A → Polynomial R →ₐ[R] A
-- Mathlib.Data.Fin.Tuple.Basic
/-- `Fin.sigma_eq_of_eq_comp_cast` as an `iff`.  -/
Fin.sigma_eq_iff_eq_comp_cast : ∀ {α : Type u_1} {a b : (ii : ℕ) × (Fin ii → α)}, a = b ↔ ∃ (h : a.fst = b.fst), a.snd = b.snd ∘ Fin.cast h
-- Mathlib.CategoryTheory.Sites.Point.Comap
/-- If `F : C ⥤ D` is a representably flat and cover preserving functor between sites, then
any point on `D` induces a point on `C` by precomposing the fiber functor with `F`.  -/
CategoryTheory.GrothendieckTopology.Point.comap : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {K : CategoryTheory.GrothendieckTopology D} →
          (Φ : K.Point) →
            (F : CategoryTheory.Functor C D) →
              [CategoryTheory.RepresentablyFlat F] →
                {J : CategoryTheory.GrothendieckTopology C} →
                  CategoryTheory.CoverPreserving J K F →
                    [CategoryTheory.InitiallySmall (F.comp Φ.fiber).Elements] → J.Point
-- Init.Data.String.Basic
String.Slice.Pos.ofSliceFrom_lt_ofSliceFrom_iff : ∀ {s : String.Slice} {p : s.Pos} {q r : (s.sliceFrom p).Pos},
  String.Slice.Pos.ofSliceFrom q < String.Slice.Pos.ofSliceFrom r ↔ q < r
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_eq_var_const_cert : Int.Internal.Linear.Expr → Int.Internal.Linear.Expr → Int.Internal.Linear.Var → ℤ → Bool
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.mk_ne_zero : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  {x : ArchimedeanClass.FiniteElement K}, ArchimedeanClass.FiniteResidueField.mk x ≠ 0 ↔ ArchimedeanClass.mk ↑x = 0
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.instSemilatticeSup : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → SemilatticeSup (CategoryTheory.Coverage C)
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.productIso_inv_comp_π_apply : ∀ {J : Type v} (F : J → Type (max v u)) (j : J) (x : (j : J) → F j),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.productIso F).inv) x) =
    x j
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- The `unusedDecidableInType` linter checks if a theorem's hypotheses include `Decidable*` instances
which are not used in the remainder of the type. If so, it suggests removing the instances and using
`classical` or `open scoped Classical in`, as appropriate, in the theorem's proof instead.

This linter fires only on theorems. (This includes `lemma`s and `instance`s of `Prop` classes.)

Note: `set_option linter.unusedDecidableInType _ in <command>` currently only works at the
outermost level of a command due to working around [lean4#11313](https://github.com/leanprover/lean4/pull/11313).
 -/
Mathlib.Linter.UnusedInstancesInType.linter.unusedDecidableInType : Lean.Option Bool
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_d : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)) (i j : α),
  ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.obj K).X.d i j = (K.d i j).f
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- notation for continuous intertwining maps  -/
ContRepresentation.«term_→ⁱL_» : Lean.TrailingParserDescr
-- Mathlib.Data.Num.Bitwise
SNum.bit_one : ∀ (b : Bool), SNum.bit b (SNum.zero (decide ¬b = true)) = SNum.nz (NzsNum.msb b)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f)
        (CategoryTheory.Limits.pullback.fst g g)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g)
        (CategoryTheory.Limits.pullback.fst f g))
      (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.instSFiniteFstOfProd : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)} [MeasureTheory.SFinite ρ], MeasureTheory.SFinite ρ.fst
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_quotient_le : ∀ {α : Type u} {s : Setoid α}, Cardinal.mk (Quotient s) ≤ Cardinal.mk α
-- Mathlib.Algebra.Order.SuccPred
strictAnti_of_add_one_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : One α]
  [inst_4 : SuccAddOrder α] [IsSuccArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMax a → f (a + 1) < f a) → StrictAnti f
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.zero_kronecker : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : MulZeroClass α]
  (B : Matrix n p α), Matrix.kroneckerMap (fun x1 x2 => x1 * x2) 0 B = 0
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.top_eq_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (B : C),
  ⊤ = CategoryTheory.Subobject.mk (CategoryTheory.CategoryStruct.id B)
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_pos : ∀ {R : Type u_1} [inst : AddCommGroupWithOne R] [inst_1 : PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1]
  {n : ℤ}, 0 < ↑n ↔ 0 < n
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.not_continuousAt_deriv_mul_log_zero : ¬ContinuousAt (deriv fun x => x * Real.log x) 0
-- Mathlib.Logic.Equiv.Basic
Equiv.instNontrivialPerm : ∀ (α : Type u_9) [Nontrivial α], Nontrivial (Equiv.Perm α)
-- Lean.Data.Lsp.Extra
/-- `meta` flag was set on this import.  -/
Lean.Lsp.LeanImportMetaKind.meta : Lean.Lsp.LeanImportMetaKind
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
UniformEquiv.neg.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  UniformEquiv.neg G = { toEquiv := Equiv.neg G, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.toPoly'.go.match_1.eq_5 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (k : ℤ) (a : Int.Internal.Linear.Expr)
  (h_1 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_2 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_3 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_4 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b))
  (h_5 : (k : ℤ) → (a : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k a))
  (h_6 : (a : Int.Internal.Linear.Expr) → (k : ℤ) → motive (a.mulR k))
  (h_7 : (a : Int.Internal.Linear.Expr) → motive a.neg),
  (match Int.Internal.Linear.Expr.mulL k a with
    | Int.Internal.Linear.Expr.num k => h_1 k
    | Int.Internal.Linear.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Int.Internal.Linear.Expr.mulL k a => h_5 k a
    | a.mulR k => h_6 a k
    | a.neg => h_7 a) =
    h_5 k a
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.mk : ∀ {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4} [inst : ENorm 𝕜] [inst_1 : TopologicalSpace E]
  [inst_2 : TopologicalSpace F] [inst_3 : Zero E] [inst_4 : Zero F] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 F]
  {l : Filter α} {f : α → E} {g : α → F},
  (∀ U ∈ nhds 0,
      ∃ V ∈ nhds 0, ∀ (ε : NNReal), ε ≠ 0 → (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => ↑ε * egauge 𝕜 V (g x)) →
    f =o[𝕜; l] g
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.karoubiUniversal₂_functor_eq : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.IsIdempotentComplete D],
  (CategoryTheory.Idempotents.karoubiUniversal₂ C D).functor = CategoryTheory.Idempotents.functorExtension₂ C D
-- Mathlib.FieldTheory.KummerExtension
adjoinRootXPowSubCEquiv.eq_1 : ∀ {K : Type u} [inst : Field K] {n : ℕ} {a : K} {L : Type u_1} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L}
  (hζ : (primitiveRoots n K).Nonempty) (H : Irreducible (Polynomial.X ^ n - Polynomial.C a))
  (hα : α ^ n = (algebraMap K L) a),
  adjoinRootXPowSubCEquiv hζ H hα =
    AlgEquiv.ofBijective (AdjoinRoot.liftAlgHom (Polynomial.X ^ n - Polynomial.C a) (Algebra.ofId K L) α ⋯) ⋯
-- Lean.Util.Trace
Lean.ExceptToTraceResult.toTraceResult : {ε α : Type} → [self : Lean.ExceptToTraceResult ε α] → Except ε α → Lean.TraceResult
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- Express the absolute value of a bounded continuous function in terms of its
positive and negative parts.  -/
BoundedContinuousFunction.abs_self_eq_nnrealPart_add_nnrealPart_neg : ∀ {α : Type u} [inst : TopologicalSpace α] (f : BoundedContinuousFunction α ℝ),
  abs ∘ ⇑f = NNReal.toReal ∘ ⇑f.nnrealPart + NNReal.toReal ∘ ⇑(-f).nnrealPart
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- The forgetful functor from commutative monoid objects to monoid objects
is fully faithful.  -/
CategoryTheory.CommMon.fullyFaithfulForget₂Mon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.CommMon.forget₂Mon C).FullyFaithful
-- Aesop.Tree.Data
Aesop.Rapp.scriptSteps? : Aesop.Rapp → Option (Array Aesop.Script.LazyStep)
-- Mathlib.Util.Export
Lean.Export.instOfStateName : Lean.Export.OfState Lean.Name
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.coe_toEquiv : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), ⇑e.toEquiv = ⇑e
-- Mathlib.Tactic.Ring.RingNF
/-- The normalization style.  -/
Mathlib.Tactic.RingNF.Config.mode : Mathlib.Tactic.RingNF.Config → Mathlib.Tactic.RingNF.RingMode
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.State.mk.sizeOf_spec : ∀ (patternVars : Array Lean.Expr), sizeOf { patternVars := patternVars } = 1 + sizeOf patternVars
-- Mathlib.Computability.NFA
NFA.reverse_start : ∀ {α : Type u} {σ : Type v} (M : NFA α σ), M.reverse.start = M.accept
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.combine.go.match_1.eq_3 : ∀ (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon)
  (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ)
  (h_1 : (k₁ k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_2 :
    (k₁ k₂ : ℤ) →
      (m₂ : Lean.Grind.CommRing.Mon) →
        (p₂ : Lean.Grind.CommRing.Poly) →
          motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂))
  (h_3 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_4 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) →
            (m₂ : Lean.Grind.CommRing.Mon) →
              (p₂ : Lean.Grind.CommRing.Poly) →
                motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂)),
  (match Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.num k₂ with
    | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.num k₂ => h_1 k₁ k₂
    | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_2 k₁ k₂ m₂ p₂
    | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.num k₂ => h_3 k₁ m₁ p₁ k₂
    | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_4 k₁ m₁ p₁ k₂ m₂ p₂) =
    h_3 k₁ m₁ p₁ k₂
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat : Type
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.Hom.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  {S₁ S₂ : CategoryTheory.Span Wₗ Wᵣ c c'} {hom : S₁.apex ⟶ S₂.apex}
  {hom_l : autoParam (CategoryTheory.CategoryStruct.comp hom S₂.l = S₁.l) CategoryTheory.Span.Hom.hom_l._autoParam}
  {hom_r : autoParam (CategoryTheory.CategoryStruct.comp hom S₂.r = S₁.r) CategoryTheory.Span.Hom.hom_r._autoParam}
  {hom_1 : S₁.apex ⟶ S₂.apex}
  {hom_l_1 : autoParam (CategoryTheory.CategoryStruct.comp hom_1 S₂.l = S₁.l) CategoryTheory.Span.Hom.hom_l._autoParam}
  {hom_r_1 : autoParam (CategoryTheory.CategoryStruct.comp hom_1 S₂.r = S₁.r) CategoryTheory.Span.Hom.hom_r._autoParam},
  { hom := hom, hom_l := hom_l, hom_r := hom_r } = { hom := hom_1, hom_l := hom_l_1, hom_r := hom_r_1 } → hom = hom_1
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : CancelMonoid α],
  OrderDual.instCancelMonoid = { toLeftCancelMonoid := OrderDual.instLeftCancelMonoid, toIsRightCancelMul := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.HasZeroObject.instFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] {B : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} B], CategoryTheory.Limits.HasZeroObject (CategoryTheory.Functor B C)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.zero_point : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [inst_1 : Nontrivial R],
  WeierstrassCurve.Projective.Point.point 0 = ⟦![0, 1, 0]⟧
-- Mathlib.Data.Bool.Basic
Bool.coe_sort_false : (false = true) = False
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.mk.injEq : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (obj : C → D → Type w) (map : {X X' : C} → {Y Y' : D} → (X ⟶ X') → (Y ⟶ Y') → (obj X Y' ⟶ obj X' Y))
  (map_id :
    autoParam
      (∀ (X : C) (Y : D),
        map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) =
          CategoryTheory.CategoryStruct.id (obj X Y))
      CategoryTheory.ProfunctorCore.map_id._autoParam)
  (map_comp :
    autoParam
      (∀ {X₁ X₂ X₃ : C} {Y₁ Y₂ Y₃ : D} (f : X₁ ⟶ X₂) (f' : X₂ ⟶ X₃) (g : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃),
        map (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g') =
          CategoryTheory.CategoryStruct.comp (map f g') (map f' g))
      CategoryTheory.ProfunctorCore.map_comp._autoParam)
  (obj_1 : C → D → Type w) (map_1 : {X X' : C} → {Y Y' : D} → (X ⟶ X') → (Y ⟶ Y') → (obj_1 X Y' ⟶ obj_1 X' Y))
  (map_id_1 :
    autoParam
      (∀ (X : C) (Y : D),
        map_1 (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) =
          CategoryTheory.CategoryStruct.id (obj_1 X Y))
      CategoryTheory.ProfunctorCore.map_id._autoParam)
  (map_comp_1 :
    autoParam
      (∀ {X₁ X₂ X₃ : C} {Y₁ Y₂ Y₃ : D} (f : X₁ ⟶ X₂) (f' : X₂ ⟶ X₃) (g : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃),
        map_1 (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g') =
          CategoryTheory.CategoryStruct.comp (map_1 f g') (map_1 f' g))
      CategoryTheory.ProfunctorCore.map_comp._autoParam),
  ({ obj := obj, map := map, map_id := map_id, map_comp := map_comp } =
      { obj := obj_1, map := map_1, map_id := map_id_1, map_comp := map_comp_1 }) =
    (obj = obj_1 ∧ map ≍ map_1)
-- Std.Internal.Do.Order.PreservesSup
/-- Frame a single state coordinate: from the function-order premise `(fun u => ⌜u = s⌝ ⊓ pre) ⊑ Q`
conclude the point entailment `pre ⊑ Q s`. Instantiating the premise at `u := s` collapses
`⌜s = s⌝ ⊓ pre` to `pre`. Iterating it over a state chain point-frames `pre ⊑ Q s₁ … sₙ` to the
function-order goal `(fun u⃗ => ⌜u⃗ = s⃗⌝ ⊓ pre) ⊑ Q`.  -/
Lean.Order.le_apply_of_point_meet_le : ∀ {σ : Type v} {β : Type w} [inst : Lean.Order.CompleteLattice β] (s : σ) (pre : β) (Q : σ → β),
  Lean.Order.PartialOrder.rel (fun u => Lean.Order.meet (Lean.Order.CompleteLattice.ofProp (u = s)) pre) Q →
    Lean.Order.PartialOrder.rel pre (Q s)
-- Init.Data.Nat.ToString
Nat.isDigit_of_mem_toDigits : ∀ {b n : ℕ} {c : Char}, 0 < b → b ≤ 10 → c ∈ b.toDigits n → c.isDigit = true
-- Mathlib.CategoryTheory.Limits.Cones
/-- Contravariantly associated to each functor `J ⥤ C`, we have the `C`-copresheaf consisting of
cocones with a given cocone point.
 -/
CategoryTheory.cocones : (J : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    (C : Type u₃) →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        CategoryTheory.Functor (CategoryTheory.Functor J C)ᵒᵖ (CategoryTheory.Functor C (Type (max u₁ v₃)))
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- `∑' i, f i` is the unconditional sum of `f` if it exists, or 0 otherwise.

More generally, if `L` is a `SummationFilter`, `∑'[L] i, f i` is the sum of `f` with respect to
`L` if it exists, and `0` otherwise.

(Note that even if the unconditional sum exists, it might not be unique if the topology is not
separated. When the support of `f` is finite, we make the most reasonable choice, to use the sum
over the support. Otherwise, we choose arbitrarily an `a` satisfying `HasSum f a`. Similar remarks
apply to more general summation filters.)
 -/
«term∑'[_]_,_» : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_sin' : ∀ {x : ℝ}, x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → Real.arcsin (Real.sin x) = x
-- Init.Data.Range.Polymorphic.UInt
UInt32.instHasSize_1 : Std.Rxo.HasSize UInt32
-- Init.Grind.Norm
Lean.Grind.natCast_mul : ∀ (a b : ℕ), ↑(a * b) = ↑a * ↑b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.getKey? t.minKey! = some t.minKey!
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsUnramified.comap_algHom : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] {F : Type u_3} [inst_2 : Field F]
  [inst_3 : Algebra k K] [inst_4 : Algebra k F] {w : NumberField.InfinitePlace F},
  NumberField.InfinitePlace.IsUnramified k w → ∀ (f : K →ₐ[k] F), NumberField.InfinitePlace.IsUnramified k (w.comap ↑f)
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoEMetricSpace E]
  {f : ℕ → α → E} {g : α → E} (hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g),
  StrictMono (MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq hfg)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.gradedHomologyFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) [inst_2 : CategoryTheory.CategoryWithHomology C] {X Y : HomologicalComplex C c}
  (f : X ⟶ Y) (i : ι), (HomologicalComplex.gradedHomologyFunctor C c).map f i = HomologicalComplex.homologyMap f i
-- Mathlib.Topology.MetricSpace.CantorScheme
CantorScheme.VanishingDiam.dist_lt : ∀ {β : Type u_1} {α : Type u_2} {A : List β → Set α} [inst : PseudoMetricSpace α],
  CantorScheme.VanishingDiam A →
    ∀ (ε : ℝ), 0 < ε → ∀ (x : ℕ → β), ∃ n, ∀ y ∈ A (PiNat.res x n), ∀ z ∈ A (PiNat.res x n), dist y z < ε
-- Mathlib.Algebra.Group.Action.Units
AddUnits.vadd_def : ∀ {M : Type u_3} {α : Type u_5} [inst : AddMonoid M] [inst_1 : VAdd M α] (m : AddUnits M) (a : α), m +ᵥ a = ↑m +ᵥ a
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `FunLike.coe_add`. -/
ContinuousLinearMap.coe_add' : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Analysis.CStarAlgebra.Spectrum
CStarAlgebra.toReal_spectralRadius_self_mul_star_eq_norm_sq : ∀ {A : Type u_1} [inst : CStarAlgebra A] (a : A), (spectralRadius ℂ (a * star a)).toReal = ‖a‖ ^ 2
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {x : α} (n : ℕ),
  UniqueFactorizationMonoid.normalizedFactors (x ^ n) = n • UniqueFactorizationMonoid.normalizedFactors x
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.NormalizedMooreComplex.objX.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  AlgebraicTopology.NormalizedMooreComplex.objX X n.succ =
    Finset.univ.inf fun k => CategoryTheory.Limits.kernelSubobject (X.δ k.succ)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instAddCommGroup : {R : Type u_1} → [inst : AddCommGroup R] → AddCommGroup (ArithmeticFunction R)
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.omega_im : ∀ {R : Type u_2} {a b : R} [inst : Zero R] [inst_1 : One R], QuadraticAlgebra.omega.im = 1
-- Mathlib.Data.Int.Log
Int.log_mono_right : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ} {r₁ r₂ : R}, 0 < r₁ → r₁ ≤ r₂ → Int.log b r₁ ≤ Int.log b r₂
-- Lean.Meta.Basic
/-- Execute `k` using a local context where any `x` in `xs` that is tagged as
instance implicit is treated as a regular implicit.  -/
Lean.Meta.withInstImplicitAsImplicit : {α : Type} → Array Lean.Expr → Lean.MetaM α → Lean.MetaM α