mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} {S : C}
  {toPreOneHypercover : CategoryTheory.PreOneHypercover S} {mem₀ : toPreOneHypercover.sieve₀ ∈ J S}
  {mem₁ :
    ∀ (i₁ i₂ : toPreOneHypercover.I₀) ⦃W : C⦄ (p₁ : W ⟶ toPreOneHypercover.X i₁) (p₂ : W ⟶ toPreOneHypercover.X i₂),
      CategoryTheory.CategoryStruct.comp p₁ (toPreOneHypercover.f i₁) =
          CategoryTheory.CategoryStruct.comp p₂ (toPreOneHypercover.f i₂) →
        toPreOneHypercover.sieve₁ p₁ p₂ ∈ J W}
  {toPreOneHypercover_1 : CategoryTheory.PreOneHypercover S} {mem₀_1 : toPreOneHypercover_1.sieve₀ ∈ J S}
  {mem₁_1 :
    ∀ (i₁ i₂ : toPreOneHypercover_1.I₀) ⦃W : C⦄ (p₁ : W ⟶ toPreOneHypercover_1.X i₁)
      (p₂ : W ⟶ toPreOneHypercover_1.X i₂),
      CategoryTheory.CategoryStruct.comp p₁ (toPreOneHypercover_1.f i₁) =
          CategoryTheory.CategoryStruct.comp p₂ (toPreOneHypercover_1.f i₂) →
        toPreOneHypercover_1.sieve₁ p₁ p₂ ∈ J W},
  { toPreOneHypercover := toPreOneHypercover, mem₀ := mem₀, mem₁ := mem₁ } =
      { toPreOneHypercover := toPreOneHypercover_1, mem₀ := mem₀_1, mem₁ := mem₁_1 } →
    toPreOneHypercover = toPreOneHypercover_1
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.comp_map : ∀ {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f : SSet.RelativeMorphism A B φ)
  {C : Z.Subcomplex} {ψ : B.toSSet ⟶ C.toSSet} (f' : SSet.RelativeMorphism B C ψ) {φψ : A.toSSet ⟶ C.toSSet}
  (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ),
  (f.comp f' fac).map = CategoryTheory.CategoryStruct.comp f.map f'.map
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.mapPower_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β : Type t}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] [inst_2 : CategoryTheory.Limits.HasProductsOfShape β C]
  (f : α → β),
  (U.mapPower f).φ = fun x => CategoryTheory.Limits.Pi.lift fun x_1 => CategoryTheory.Limits.Pi.π (U.obj ∘ x) (f x_1)
-- Mathlib.LinearAlgebra.Complex.Module
star_mul_self_eq_realPart_sq_add_imaginaryPart_sq : ∀ {A : Type u_1} [inst : NonUnitalNonAssocRing A] [inst_1 : StarRing A] [inst_2 : Module ℂ A] [IsScalarTower ℂ A A]
  [SMulCommClass ℂ A A] [inst_5 : StarModule ℂ A] (x : A) [hx : IsStarNormal x],
  star x * x = ↑(realPart x) * ↑(realPart x) + ↑(imaginaryPart x) * ↑(imaginaryPart x)
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.smul_apply_apply : ∀ {R : Type u_1} [inst : CommRing R] {L : Type u_2} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (r : R) (a : ↥(LieModule.Cohomology.twoCochain R L M)) (x y : L),
  ((r • a) x) y = r • (a x) y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.insertManyIfNewUnit_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp}, t.insertManyIfNewUnit [] = t
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.lintegral_rnDeriv : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] {κ η : ProbabilityTheory.Kernel α γ}
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {a : α},
  (κ a).AbsolutelyContinuous (η a) → ∫⁻ (c : γ), κ.rnDeriv η a c ∂η a = (κ a) Set.univ
-- Mathlib.NumberTheory.Padics.PadicNumbers
Rat.padicValuation_self : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], (Rat.padicValuation p) ↑p = WithZero.exp (-1)
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.supIndep_torsionBy : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_3}
  {S : Finset ι} {q : ι → R},
  (↑S).Pairwise (Function.onFun IsCoprime q) → S.SupIndep fun i => Submodule.torsionBy R M (q i)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlong.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y},
  (∀ {Z W : C} {f' : W ⟶ Z} {g' : W ⟶ X} {g : Z ⟶ Y}, CategoryTheory.IsPullback f' g' g f → P g → P g') →
    P.IsStableUnderBaseChangeAlong f
-- Mathlib.Analysis.Convex.Quasiconvex
AntitoneOn.quasilinearOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, AntitoneOn f s → Convex 𝕜 s → QuasilinearOn 𝕜 s f
-- Mathlib.Order.Filter.Pi
Filter.compl_mem_coprodᵢ : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : Set ((i : ι) → α i)},
  sᶜ ∈ Filter.coprodᵢ f ↔ ∀ (i : ι), (Function.eval i '' s)ᶜ ∈ f i
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (a b n : ℤ) (h : a + b = n) (b' : ℤ) (hb' : b' = b + y) (n' : ℤ) (hn' : n' = n + y) {Z : C}
  (h_1 :
    ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).obj (K.total (ComplexShape.up ℤ))).X n ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h)
      (CategoryTheory.CategoryStruct.comp ((K.totalShift₂Iso y).hom.f n) h_1) =
    CategoryTheory.CategoryStruct.comp
      ((a * y).negOnePow •
        CategoryTheory.CategoryStruct.comp (K.shiftFunctor₂XXIso a b y b' hb').hom
          (CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a b' n' ⋯)
            (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv))
      h_1
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instForInOfMonad : {α : Type u} → {m : Type v → Type w} → [Monad m] → ForIn m (Std.HashSet.Raw α) α
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.FunctionTheorem.mk : Lean.Name →
  Mathlib.Meta.FunProp.Origin →
    Mathlib.Meta.FunProp.Origin →
      Array ℕ → ℕ → ℕ → Mathlib.Meta.FunProp.TheoremForm → Mathlib.Meta.FunProp.FunctionTheorem
-- Mathlib.GroupTheory.Goursat
AddSubgroup.normal_goursatSnd : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {I : AddSubgroup (G × H)},
  Function.Surjective (Prod.snd ∘ ⇑I.subtype) → I.goursatSnd.Normal
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- A morphism of pre-`0`-hypercovers of `S` is a family of refinement morphisms commuting
with the structure morphisms of `E` and `F`.  -/
CategoryTheory.PreZeroHypercover.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → CategoryTheory.PreZeroHypercover S → CategoryTheory.PreZeroHypercover S → Type (max (max v w) w')
-- Init.Grind.Module.Basic
Lean.Grind.AddRightCancel.mk : ∀ {M : Type u} [inst : Add M], (∀ (a b c : M), a + c = b + c → a = b) → Lean.Grind.AddRightCancel M
-- Init.Data.Ord.Vector
Vector.compareLex_eq_compareLex_toList : ∀ {α : Type u_1} {n : ℕ} {cmp : α → α → Ordering} {a b : Vector α n},
  Vector.compareLex cmp a b = List.compareLex cmp a.toList b.toList
-- Mathlib.Topology.AlexandrovDiscrete
isClosed_iUnion : ∀ {ι : Sort u_1} {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {f : ι → Set α},
  (∀ (i : ι), IsClosed (f i)) → IsClosed (⋃ i, f i)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₀_app_fst : ∀ {X : SSet} {m : SimplexCategoryᵒᵖ} (x : X.obj m), ((CategoryTheory.ConcreteCategory.hom (SSet.ι₀.app m)) x).1 = x
-- Mathlib.Logic.IsEmpty.Defs
instIsEmptyForallOfNonempty : ∀ {α : Sort u} {p : α → Sort v} [∀ (x : α), IsEmpty (p x)] [h : Nonempty α], IsEmpty ((x : α) → p x)
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- Any action on `ℝ` which factors through `ℝ≥0` applies to an `AddGroupSeminorm`.  -/
AddGroupSeminorm.toSMul : {R : Type u_1} →
  {E : Type u_3} →
    [inst : AddGroup E] →
      [inst_1 : SMul R ℝ] → [inst_2 : SMul R NNReal] → [IsScalarTower R NNReal ℝ] → SMul R (AddGroupSeminorm E)
-- Mathlib.Control.Monad.Cont
LawfulMonadCont.callCC_bind_right : ∀ {m : Type u → Type v} {inst : Monad m} {inst_1 : MonadCont m} [self : LawfulMonadCont m] {α ω γ : Type u} (cmd : m α)
  (next : MonadCont.Label ω m γ → α → m ω),
  (MonadCont.callCC fun f => cmd >>= next f) = do
    let x ← cmd
    MonadCont.callCC fun f => next f x
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂_map_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (Y_1 X_1 : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂ C).map f).app Y_1).app X_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X_1 X Y_1).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X_1
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y_1))
        (CategoryTheory.MonoidalCategoryStruct.associator X_1 Y Y_1).inv)
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList_sublist_right : ∀ {n k : ℕ}, k ≠ 0 → n.primeFactorsList.Sublist (n * k).primeFactorsList
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.Props : Type
-- Lean.Server.Requests
/-- See `withWaitFindSnap`.  -/
Lean.Server.RequestM.bindWaitFindSnap : {β : Type} →
  Lean.Server.FileWorker.EditableDocument →
    (Lean.Server.Snapshots.Snapshot → Bool) →
      Lean.Server.RequestM (Lean.Server.RequestTask β) →
        (Lean.Server.Snapshots.Snapshot → Lean.Server.RequestM (Lean.Server.RequestTask β)) →
          Lean.Server.RequestM (Lean.Server.RequestTask β)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.PreElabHeaderResult.mk : Lean.Elab.Command.InductiveView →
  List Lean.Name → ℕ → Lean.Expr → Array Lean.Expr → Lean.Elab.Command.PreElabHeaderResult
-- Mathlib.FieldTheory.Finite.GaloisField
/-- Any finite field is (possibly noncanonically) isomorphic to some Galois field.  -/
GaloisField.algEquivGaloisFieldOfFintype : (p : ℕ) →
  [h_prime : Fact (Nat.Prime p)] →
    (n : ℕ) →
      {K : Type u_1} →
        [inst : Field K] →
          [inst_1 : Fintype K] → [inst_2 : Algebra (ZMod p) K] → Fintype.card K = p ^ n → K ≃ₐ[ZMod p] GaloisField p n
-- Mathlib.Tactic.Simps.NotationClass
Simps.AutomaticProjectionData.mk : Lean.Name → Bool → Lean.Name → Simps.AutomaticProjectionData
-- Init.Data.List.Pairwise
List.pairwise_of_forall : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, (∀ (x y : α), R x y) → List.Pairwise R l
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.l_naturality : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y), CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_smul_iff_of_pos_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [PosSMulStrictMono α β] [PosSMulReflectLT α β], 0 < a → (a • b₁ < a • b₂ ↔ b₁ < b₂)
-- Aesop.Percent
Aesop.Percent.mk.injEq : ∀ (toFloat toFloat_1 : Float), ({ toFloat := toFloat } = { toFloat := toFloat_1 }) = (toFloat = toFloat_1)
-- Mathlib.LinearAlgebra.Prod
LinearMap.prod_eq_sup_map : ∀ {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₂] (p : Submodule R M) (q : Submodule R M₂),
  p.prod q = Submodule.map (LinearMap.inl R M M₂) p ⊔ Submodule.map (LinearMap.inr R M M₂) q
-- Mathlib.Data.ENNReal.Inv
/-- **Alias** of the reverse direction of `ENNReal.inv_ne_top`. -/
ENNReal.Finiteness.inv_ne_top : ∀ {a : ENNReal}, a ≠ 0 → a⁻¹ ≠ ⊤
-- Std.Data.ExtTreeMap.Basic
/-- Inserts multiple elements into the tree map by iterating over the given collection and calling
`insertIfNew`. If the same key appears multiple times, the first occurrence takes precedence.
 -/
Std.ExtTreeMap.insertManyIfNewUnit : {α : Type u} →
  {cmp : α → α → Ordering} →
    [Std.TransCmp cmp] → {ρ : Type u_1} → [ForIn Id ρ α] → Std.ExtTreeMap α Unit cmp → ρ → Std.ExtTreeMap α Unit cmp
-- Mathlib.Analysis.Convex.Function
ConvexOn.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α}, ConvexOn 𝕜 (f '' s) g → ConvexOn 𝕜 s f → MonotoneOn g (f '' s) → ConvexOn 𝕜 s (g ∘ f)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_eq_head!_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.minKey! = t.keys.head!
-- Init.Data.Nat.Lemmas
Nat.dvd_of_pow_dvd : ∀ {p k m : ℕ}, 1 ≤ k → p ^ k ∣ m → p ∣ m
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zigzag.refl : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] (X : J), CategoryTheory.Zigzag X X
-- Mathlib.LinearAlgebra.Matrix.Kronecker
/-- The Kronecker product. This is just a shorthand for `kroneckerMap (*)`. Prefer the notation
`⊗ₖ` rather than this definition.  -/
Matrix.kronecker : {α : Type u_3} →
  {l : Type u_9} →
    {m : Type u_10} →
      {n : Type u_11} → {p : Type u_12} → [Mul α] → Matrix l m α → Matrix n p α → Matrix (l × n) (m × p) α
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₁_comp_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] {υ : Type u_6} (f : σ → MvPolynomial τ R)
  (g : τ → MvPolynomial υ R),
  (MvPolynomial.bind₁ g).comp (MvPolynomial.bind₁ f) = MvPolynomial.bind₁ fun i => (MvPolynomial.bind₁ g) (f i)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableAt_pi'' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_6} {F' : ι → Type u_7} [inst_3 : (i : ι) → NormedAddCommGroup (F' i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  (∀ (i : ι), DifferentiableAt 𝕜 (fun x => Φ x i) x) → DifferentiableAt 𝕜 Φ x
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.toSubmonoid_inj : ∀ {G : Type u_1} [inst : Group G] {p q : Subgroup G}, p.toSubmonoid = q.toSubmonoid ↔ p = q
-- Mathlib.NumberTheory.Niven
niven_fract_angle_div_pi_eq : ∀ {r : ℚ}, (∃ q, Real.cos (↑r * Real.pi) = ↑q) → Int.fract r ∈ {0, 1 / 3, 1 / 2, 2 / 3}
-- Batteries.Data.Nat.Bisect
Nat.bisect.congr_simp : ∀ {start start_1 : ℕ} (e_start : start = start_1) {stop stop_1 : ℕ} (e_stop : stop = stop_1) {p p_1 : ℕ → Bool}
  (e_p : p = p_1) (h : start < stop) (hstart : p start = true) (hstop : p stop = false),
  Nat.bisect h hstart hstop = Nat.bisect ⋯ ⋯ ⋯
-- Init.Prelude
Applicative.toPure : {f : Type u → Type v} → [self : Applicative f] → Pure f
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_eq_false_iff_exists_isSome_getValueCast? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)},
  l.isEmpty = false ↔ ∃ a, (Std.Internal.List.getValueCast? a l).isSome = true
-- Mathlib.Analysis.Normed.Module.Basic
/-- If `E` is a normed algebra over `𝕜'` and `𝕜` is a normed algebra over `𝕜'`, then
`RestrictScalars.module` is additionally a `NormedAlgebra`.  -/
RestrictScalars.normedAlgebra : (𝕜 : Type u_1) →
  (𝕜' : Type u_2) →
    (E : Type u_3) →
      [inst : NormedField 𝕜] →
        [inst_1 : NormedField 𝕜'] →
          [NormedAlgebra 𝕜 𝕜'] →
            [inst_3 : SeminormedRing E] → [NormedAlgebra 𝕜' E] → NormedAlgebra 𝕜 (RestrictScalars 𝕜 𝕜' E)
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.CommRingCat.Colimits.descFunLift.match_1.eq_6 : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (motive : CommRingCat.Colimits.Prequotient F → Sort u_2) (x y : CommRingCat.Colimits.Prequotient F)
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (CommRingCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive CommRingCat.Colimits.Prequotient.zero) (h_3 : Unit → motive CommRingCat.Colimits.Prequotient.one)
  (h_4 : (x : CommRingCat.Colimits.Prequotient F) → motive x.neg)
  (h_5 : (x y : CommRingCat.Colimits.Prequotient F) → motive (x.add y))
  (h_6 : (x y : CommRingCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match x.mul y with
    | CommRingCat.Colimits.Prequotient.of j x => h_1 j x
    | CommRingCat.Colimits.Prequotient.zero => h_2 ()
    | CommRingCat.Colimits.Prequotient.one => h_3 ()
    | x.neg => h_4 x
    | x.add y => h_5 x y
    | x.mul y => h_6 x y) =
    h_6 x y
-- Std.Time.Format
/-- Formats a `PlainDateTime` value into a LongDateFormat string.
 -/
Std.Time.PlainDateTime.toLongDateFormatString : Std.Time.PlainDateTime → String
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_compl_sum_single : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α],
  0 < p.toReal →
    ∀ (f : ↥(lp E p)) (s : Finset α),
      ‖f - ∑ i ∈ s, lp.single p i (↑f i)‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Collects the terms into a product of sets.  -/
BigOperators.bigOpBindersProd : Array (Lean.Term × Lean.Term) → Lean.MacroM Lean.Term
-- Mathlib.Algebra.Regular.SMul
/-- **Alias** of the reverse direction of `isSMulRegular_map`. -/
IsSMulRegular.map : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [inst : SMul R M] [inst_1 : SMul S M] (f : R → S),
  (∀ (m : M), f a • m = a • m) → IsSMulRegular M a → IsSMulRegular M (f a)
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsImmersion
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.negate : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n → Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
-- Mathlib.Topology.Covering.AddCircle
AddCircle.isCoveringMap_coe : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜]
  [DiscreteTopology ↥(AddSubgroup.zmultiples p)], IsCoveringMap QuotientAddGroup.mk
-- Mathlib.Analysis.Seminorm
/-- **Alias** of `FunLike.coeAddMonoidHom_apply`. -/
Seminorm.coeFnAddMonoidHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β] (f : F), (FunLike.coeAddMonoidHom F α β) f = ⇑f
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.faithful_preadditiveYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.preadditiveYoneda.Faithful
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_diff_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ((m₁ \ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∈ m₂)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.toSingleMk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {q n : ℤ}
  (α : CochainComplex.HomComplex.Cocycle K ((CochainComplex.singleFunctor C q).obj X) n) (p : ℤ) (h : p + n = q)
  (p' : ℤ) (hp' : p' + 1 = p),
  ∃ f,
    ∃ (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0),
      CochainComplex.HomComplex.Cocycle.toSingleMk f h p' hp' hf = α
-- Mathlib.LinearAlgebra.ExteriorPower.Pairing
exteriorPower.alternatingMapToDual.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ),
  exteriorPower.alternatingMapToDual R M n =
    {
      toMultilinearMap :=
        (exteriorPower.toTensorPower R M n).dualMap.compMultilinearMap (TensorPower.multilinearMapToDual R M n),
      map_eq_zero_of_eq' := ⋯ }
-- Std.Data.String.ToInt
Int.toInt?_repr : ∀ (a : ℤ), a.repr.toInt? = some a
-- Aesop.Stats.Basic
Aesop.instToJsonForwardClusterStateStats.toJson : Aesop.ForwardClusterStateStats → Lean.Json
-- Mathlib.GroupTheory.Coset.Basic
/-- An equivalence between any two fibers of a surjective `MonoidHom`.  -/
MonoidHom.fiberEquivOfSurjective : {α : Type u_1} →
  [inst : Group α] →
    {H : Type u_2} →
      [inst_1 : Group H] → {f : α →* H} → Function.Surjective ⇑f → (h h' : H) → ↑(⇑f ⁻¹' {h}) ≃ ↑(⇑f ⁻¹' {h'})
-- Mathlib.Data.Set.Sups
Set.singleton_sups_singleton : ∀ {α : Type u_2} [inst : SemilatticeSup α] {a b : α}, {a} ⊻ {b} = {a ⊔ b}
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.snd_comp_inl : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W},
  (Representation.IntertwiningMap.snd A ρ σ).comp (Representation.IntertwiningMap.inl A ρ σ) = 0
-- Mathlib.Topology.Bases
TopologicalSpace.IsSeparable.eq_1 : ∀ {α : Type u} [t : TopologicalSpace α] (s : Set α), TopologicalSpace.IsSeparable s = ∃ c, c.Countable ∧ s ⊆ closure c
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `==` on `BitVec`s.  -/
BitVec.reduceBEq : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mkAux.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) →
      (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0),
  ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ 0 = { X₁ := X₂, X₂ := X₁, X₃ := X₀, f := d₁, g := d₀, zero := s }
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- Introduction rule to prove that `b` is the infimum of `f`: it suffices to check that `b`
is smaller than `f i` for all `i`, and that this is not the case of any `w>b`.
See `iInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices.  -/
ciInf_eq_of_forall_ge_of_forall_gt_exists_lt : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {b : α} [Nonempty ι] {f : ι → α},
  (∀ (i : ι), b ≤ f i) → (∀ (w : α), b < w → ∃ i, f i < w) → ⨅ i, f i = b
-- Lean.Parser.Term.Basic
Lean.Parser.Term.strictImplicitBinder.formatter : optParam Bool false → Lean.PrettyPrinter.Formatter
-- Lean.Elab.Binders
Lean.Elab.Term.LetIdDeclView.mk.sizeOf_spec : ∀ (id : Lean.Syntax) (binders : Array Lean.Syntax) (type value : Lean.Syntax),
  sizeOf { id := id, binders := binders, type := type, value := value } =
    1 + sizeOf id + sizeOf binders + sizeOf type + sizeOf value
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- The tautological cocone with point `P` is a colimit cocone, exhibiting `P` as a colimit of
representables.

Proposition 2.6.3(i) in [Kashiwara2006]  -/
CategoryTheory.Presheaf.isColimitTautologicalCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) →
      CategoryTheory.Limits.IsColimit (CategoryTheory.Presheaf.tautologicalCocone P)
-- Init.System.IO
/-- Writes the provided bytes to the stream.

If the stream represents a physical output device such as a file on disk, then the results may be
buffered. Call `FS.Stream.flush` to synchronize their contents.
 -/
IO.FS.Stream.write : IO.FS.Stream → ByteArray → IO Unit