mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.rightUnitor_tensor_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator X Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
        h)
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_eq_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c x : P} {R : ℝ}, R ≠ 0 → (EuclideanGeometry.inversion c R x = c ↔ x = c)
-- Init.Data.SInt.Bitwise
Int16.ofBitVec_intMin : Int16.ofBitVec (BitVec.intMin 16) = Int16.minValue
-- Init.Data.BitVec.Lemmas
/-- The 'master theorem' for extracting bits from `(xhi ++ xlo)`,
which performs a case analysis on the start index, length, and the lengths of `xlo, xhi`.
· If the start index is entirely out of the `xlo` bitvector, then grab the bits from `xhi`.
· If the start index is entirely contained in the `xlo` bitvector, then grab the bits from `xlo`.
· If the start index is split between the two bitvectors,
  then append `(w - start)` bits from `xlo` with `(len - (w - start))` bits from xhi.
  Diagrammatically:
  ```
                 xhi                      xlo
          (<---------------------](<-------w--------]
  start+len..start:  (<-----len---*------]
  w - start:                      *------*
  len - (w -start):  *------------*
  ```
 -/
BitVec.extractLsb'_append_eq_ite : ∀ {v w : ℕ} {xhi : BitVec v} {xlo : BitVec w} {start len : ℕ},
  BitVec.extractLsb' start len (xhi ++ xlo) =
    if hstart : start < w then
      if hlen : start + len ≤ w then BitVec.extractLsb' start len xlo
      else
        BitVec.cast ⋯
          (BitVec.extractLsb' (start - w) (len - (w - start)) xhi ++ BitVec.extractLsb' start (w - start) xlo)
    else BitVec.extractLsb' (start - w) len xhi
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k fallback : α},
  (Std.DTreeMap.filterMap f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => (f x (Std.DTreeMap.Const.get t x ⋯)).isSome).getD fallback
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasSeparator.hasCoseparator_of_hasSeparator_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [h : CategoryTheory.HasSeparator Cᵒᵖ],
  CategoryTheory.HasCoseparator C
-- Mathlib.Data.Option.Defs
Option.elim'_none : ∀ {α : Type u_1} {β : Type u_2} (b : β) (f : α → β), Option.elim' b f none = b
-- Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
/-- If `G : D ⥤ C` is a right adjoint it satisfies the solution set condition.  -/
CategoryTheory.solutionSetCondition_of_isRightAdjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (G : CategoryTheory.Functor D C) [G.IsRightAdjoint], CategoryTheory.SolutionSetCondition G
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.mapSnakeInput_f₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂)
  (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j),
  (HomologicalComplex.HomologySequence.mapSnakeInput φ hS₁ hS₂ i j hij).f₃ =
    (HomologicalComplex.homologyFunctor C c j).mapShortComplex.map φ
-- Init.Data.Rat.Lemmas
Rat.mul_div_cancel : ∀ {a b : ℚ}, b ≠ 0 → a * b / b = a
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.comp_eq_zero_iff : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p q : Polynomial R},
  p.comp q = 0 ↔ p = 0 ∨ Polynomial.eval (q.coeff 0) p = 0 ∧ q = Polynomial.C (q.coeff 0)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.Hereditarily.empty : ∀ {p : ZFSet.{u} → Prop} {x : ZFSet.{u}}, ZFSet.Hereditarily p x → p ∅
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.subsingleton_of_isTerminal : ∀ {X : CommRingCat} (hX : CategoryTheory.Limits.IsTerminal X), Subsingleton ↑X
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedLevelMVarErrorInfo : Inhabited Lean.Elab.Term.LevelMVarErrorInfo
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.induction_on' : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {motive : AddMonoid.Coprod M N → Prop}
  (m : AddMonoid.Coprod M N),
  motive 0 →
    (∀ (m : M) (x : AddMonoid.Coprod M N), motive x → motive (AddMonoid.Coprod.inl m + x)) →
      (∀ (n : N) (x : AddMonoid.Coprod M N), motive x → motive (AddMonoid.Coprod.inr n + x)) → motive m
-- Mathlib.Data.Sum.Order
Sum.Lex.preorder : {α : Type u_1} → {β : Type u_2} → [Preorder α] → [Preorder β] → Preorder (α ⊕ₗ β)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.exists_restrict_isOver : ∀ {X Y : AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme) [inst : X.Over S] [inst_1 : Y.Over S]
  (f : X.PartialMap Y) [AlgebraicGeometry.Scheme.RationalMap.IsOver S f.toRationalMap],
  ∃ U, ∃ (hU : Dense ↑U) (hU' : U ≤ f.domain), AlgebraicGeometry.Scheme.PartialMap.IsOver S (f.restrict U hU hU')
-- Mathlib.GroupTheory.OrderOfElement
/-- Commuting elements of finite additive order are closed under addition.  -/
AddCommute.isOfFinAddOrder_add : ∀ {G : Type u_1} [inst : AddMonoid G] {x y : G},
  AddCommute x y → IsOfFinAddOrder x → IsOfFinAddOrder y → IsOfFinAddOrder (x + y)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
HomogeneousLocalization.awayMapₐ.congr_simp : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {e e_1 : ι} (e_e : e = e_1) {f g g_1 : A} (e_g : g = g_1) (hg : g ∈ 𝒜 e) {x : A}
  (hx : x = f * g), HomogeneousLocalization.awayMapₐ 𝒜 hg hx = HomogeneousLocalization.awayMapₐ 𝒜 ⋯ ⋯
-- Mathlib.Data.Ordmap.Ordnode
/-- **Internal use only**, because it violates the BST property on the original order.

O(n). The dual of a tree is a tree with its left and right sides reversed throughout.
The dual of a valid BST is valid under the dual order. This is convenient for exploiting
symmetries in the algorithms.  -/
Ordnode.dual : {α : Type u_1} → Ordnode α → Ordnode α
-- Std.Time.Time.Unit.Second
Std.Time.Second.instDecidableEqOrdinal : {leap : Bool} → DecidableEq (Std.Time.Second.Ordinal leap)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.mdata : Lean.Option Bool
-- Mathlib.Algebra.Group.Action.Opposite
/-- With `open scoped RightActions`, a shorthand for right actions, `op r +ᵥ m`.

In lemma names this is still called `op_vadd`.  -/
RightActions.«term_<+ᵥ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Round
round_add_natCast : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α)
  (y : ℕ), round (x + ↑y) = round x + ↑y
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.erase_eq_eraseₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α} {t : Std.DTreeMap.Internal.Impl α β} {h : t.Balanced},
  (Std.DTreeMap.Internal.Impl.erase k t h).impl = Std.DTreeMap.Internal.Impl.eraseₘ k t h
-- Mathlib.Algebra.Group.Subsemigroup.Membership
AddSubsemigroup.mem_iSup_prop : ∀ {M : Type u_2} [inst : Add M] {p : Prop} {S : p → AddSubsemigroup M} {x : M}, x ∈ ⨆ (h : p), S h ↔ ∃ (h : p), x ∈ S h
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.edgeSetSumEquiv.match_1.congr_eq_3 : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}
  (motive : (x x_1 : V ⊕ W) → (G ⊕g H).Adj x x_1 → Sort u_3) (x x_1 : V ⊕ W) (x_2 : (G ⊕g H).Adj x x_1)
  (h_1 : (u v : V) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)) → motive (Sum.inl u) (Sum.inl v) h)
  (h_2 : (u v : W) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)) → motive (Sum.inr u) (Sum.inr v) h)
  (h_3 : (u : V) → (v : W) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)) → motive (Sum.inl u) (Sum.inr v) h)
  (h_4 : (u : W) → (v : V) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)) → motive (Sum.inr u) (Sum.inl v) h) (u : V)
  (v : W) (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)),
  x = Sum.inl u →
    x_1 = Sum.inr v →
      x_2 ≍ h →
        (match x, x_1, x_2 with
          | Sum.inl u, Sum.inl v, h => h_1 u v h
          | Sum.inr u, Sum.inr v, h => h_2 u v h
          | Sum.inl u, Sum.inr v, h => h_3 u v h
          | Sum.inr u, Sum.inl v, h => h_4 u v h) ≍
          h_3 u v h
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.weightEquiv_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) (m : M),
  (RootPairing.Equiv.weightEquiv P Q e) m = (↑e).weightMap m
-- Mathlib.Algebra.Group.Action.Defs
/-- Note that the `IsScalarTower α β β` and `SMulCommClass α β β` typeclass arguments are usually
satisfied by `Algebra α β`.  -/
smul_mul_smul_comm : ∀ {α : Type u_5} {β : Type u_6} [inst : Mul α] [inst_1 : Mul β] [inst_2 : SMul α β] [IsScalarTower α β β]
  [IsScalarTower α α β] [SMulCommClass α β β] (a : α) (b : β) (c : α) (d : β), a • b * c • d = (a * c) • (b * d)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- `fderivLM 𝕜 n k` is the `𝕜`-linear-map sending `f : 𝓓^{n}_{K}(E, F)` to
its derivative as an element of `𝓓^{k}_{K}(E, E →L[ℝ] F)`.
This only makes mathematical sense if `k + 1 ≤ n`, otherwise we define it as the zero map.

This is subsumed by `fderivCLM`, which also bundles the continuity.  -/
ContDiffMapSupportedIn.fderivLM : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace ℝ E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace ℝ F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] →
                    (n k : ℕ∞) →
                      {K : TopologicalSpace.Compacts E} →
                        ContDiffMapSupportedIn E F n K →ₗ[𝕜] ContDiffMapSupportedIn E (E →L[ℝ] F) k K
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_neg_eq_neg : ∀ {R : Type u_8} {M : Type u_9} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (s : Set M),
  Submodule.span R (-s) = -Submodule.span R s
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableLocallyUniformlyOn_congr : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {s : Set β} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β] {f f' : ι → β → α},
  (∀ (i : ι), Set.EqOn (f i) (f' i) s) → SummableLocallyUniformlyOn f s → SummableLocallyUniformlyOn f' s
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.image_vadd_distrib : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Add α]
  [inst_3 : Add β] [inst_4 : FunLike F α β] [AddHomClass F α β] (f : F) (a : α) (s : Finset α),
  Finset.image (⇑f) (a +ᵥ s) = f a +ᵥ Finset.image (⇑f) s
-- Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
/-- Given a sequence of complex polynomials `fₚ`, a complex constant `s`, and a real constant `c` such
that `|fₚ(xs)| ≤ c ^ p` for all `p ∈ ℕ` and `x ∈ Ioc 0 1`, then there is also a nonnegative
constant `c'` such that for all nonzero `p ∈ ℕ`, `|P(fₚ, s)| ≤ c' ^ p`.
 -/
_private.Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart.0.LindemannWeierstrass.P_le_aux : ∀ (f : ℕ → Polynomial ℂ) (s : ℂ) (c : ℝ),
  (∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖Polynomial.eval (x • s) (f p)‖ ≤ c ^ p) →
    ∃ c' ≥ 0, ∀ (p : ℕ), ‖LindemannWeierstrass.P✝ (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
-- Mathlib.GroupTheory.Sylow
Sylow.coe_smul : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {g : G} {P : Sylow p G}, ↑(g • P) = MulAut.conj g • ↑P
-- Mathlib.Probability.Independence.InfinitePi
ProbabilityTheory.iIndepFun_iff_hasLaw_Pi_infinitePi : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : ι → Type u_3}
  {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} [MeasureTheory.IsProbabilityMeasure P]
  {μ : (i : ι) → MeasureTheory.Measure (𝓧 i)},
  (∀ (i : ι), ProbabilityTheory.HasLaw (X i) (μ i) P) →
    AEMeasurable (fun ω i => X i ω) P →
      (ProbabilityTheory.iIndepFun X P ↔
        ProbabilityTheory.HasLaw (fun ω i => X i ω) (MeasureTheory.Measure.infinitePi μ) P)
-- Mathlib.Data.Num.Lemmas
Num.le_to_nat : ∀ {m n : Num}, ↑m ≤ ↑n ↔ m ≤ n
-- Init.Prelude
/-- A failure value of type `ε`  -/
Except.error : {ε : Type u} → {α : Type v} → ε → Except ε α
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
/-- A proof that the possible return values are equivalent to a `w`-small type.
 -/
Std.Iterators.HetT.small : ∀ {m : Type w → Type w'} {α : Type v} (self : Std.Iterators.HetT m α), Std.Internal.Small (Subtype self.Property)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.zpowersEquivSupport_apply : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {σ : Equiv.Perm α} (hσ : σ.IsCycle) {n : ℕ},
  hσ.zpowersEquivSupport ⟨σ ^ n, ⋯⟩ = ⟨(σ ^ n) (Classical.choose hσ), ⋯⟩
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The set of points.  -/
Projectivization.Subspace.carrier : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Projectivization.Subspace K V → Set (Projectivization K V)
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.evalGrindTrace : Lean.Elab.Tactic.Tactic
-- Init.Data.List.Lemmas
List.foldrM_append : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → β → m β} {b : β}
  {l l' : List α},
  List.foldrM f b (l ++ l') = do
    let init ← List.foldrM f b l'
    List.foldrM f init l
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyπ_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i],
  CategoryTheory.CategoryStruct.comp (K.homologyπ i) (HomologicalComplex.homologyMap φ i) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i) (L.homologyπ i)
-- Init.Grind.Ring.Field
Lean.Grind.Field.inv_eq_iff_eq_iff : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a b : α), a⁻¹ = b ↔ a = b⁻¹
-- Init.Data.List.Basic
/-- Splits a list at an index, resulting in the first `n` elements of `l` paired with the remaining
elements.

If `n` is greater than the length of `l`, then the resulting pair consists of `l` and the empty
list. `List.splitAt` is equivalent to a combination of `List.take` and `List.drop`, but it is more
efficient.

Examples:
* `["red", "green", "blue"].splitAt 2 = (["red", "green"], ["blue"])`
* `["red", "green", "blue"].splitAt 3 = (["red", "green", "blue], [])`
* `["red", "green", "blue"].splitAt 4 = (["red", "green", "blue], [])`
 -/
List.splitAt : {α : Type u} → ℕ → List α → List α × List α
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The canonical functor from the costructured arrow category on the diagonal functor
`T ⥤ T × T` to the costructured arrow category on `Under.forget`.  -/
CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    (X : T × T) →
      CategoryTheory.Functor (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X)
        (CategoryTheory.CostructuredArrow (CategoryTheory.Over.forget X.1) X.2)
-- Mathlib.Order.Hom.CompleteLattice
/-- The map `(a, b) ↦ a ⊓ b` as an `sInfHom`.  -/
infsInfHom : {α : Type u_2} → [inst : CompleteLattice α] → sInfHom (α × α) α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- A monoid morphism `f : M ⟶ N` induces a monoid homomorphism `M(X) →* N(X)` for every `X`.  -/
CategoryTheory.IsMonHom.monoidHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {M N : C} →
        [inst_2 : CategoryTheory.MonObj M] →
          [inst_3 : CategoryTheory.MonObj N] → (f : M ⟶ N) → [CategoryTheory.IsMonHom f] → (X : C) → (X ⟶ M) →* (X ⟶ N)
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_3 : CategoryTheory.ConcreteCategory A FC]
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)]
  [CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.Limits.PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ (CategoryTheory.forget A)
-- Init.Data.UInt.Bitwise
UInt8.toNat_xor : ∀ (a b : UInt8), (a ^^^ b).toNat = a.toNat ^^^ b.toNat
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.op_pOpcycles_opcyclesOpIso_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {Z : Cᵒᵖ} (h : Opposite.op S.cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.op.pOpcycles (CategoryTheory.CategoryStruct.comp S.opcyclesOpIso.hom h) =
    CategoryTheory.CategoryStruct.comp S.iCycles.op h
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Replacing an empty cocone in `IsColimit` by another with the same cocone point
is an equivalence.  -/
CategoryTheory.Limits.isColimitEmptyCoconeEquiv : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F₁ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C} →
      {F₂ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w' + 1}) C} →
        (c₁ : CategoryTheory.Limits.Cocone F₁) →
          (c₂ : CategoryTheory.Limits.Cocone F₂) →
            (c₁.pt ≅ c₂.pt) → CategoryTheory.Limits.IsColimit c₁ ≃ CategoryTheory.Limits.IsColimit c₂
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instIsTopologicalGroupCoePrincipal : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  {T : Set ι} [inst_1 : (i : ι) → TopologicalSpace (R i)] [inst_2 : (i : ι) → Group (R i)]
  [inst_3 : ∀ (i : ι), SubgroupClass (S i) (R i)] [∀ (i : ι), IsTopologicalGroup (R i)],
  IsTopologicalGroup (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) (Filter.principal T))
-- Mathlib.RingTheory.Coalgebra.Basic
/-- A representation of an element `a` of a coalgebra `A` is a finite sum of pure tensors `∑ xᵢ ⊗ yᵢ`
that is equal to `comul a`.
 -/
Coalgebra.Repr : (R : Type u) →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [CoalgebraStruct R A] → A → Type u_1 → Type (max u_1 v)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.sep_infinite : ∀ {α : Type u_1} [Countable α] {S : Set (Set α)}, MeasurableSet S → MeasurableSet {s | s ∈ S ∧ s.Infinite}
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.instIsProbabilityMeasureToFiniteOfNeZeroMeasure : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SFinite μ] [NeZero μ],
  MeasureTheory.IsProbabilityMeasure μ.toFinite
-- Mathlib.RingTheory.OreLocalization.Basic
/-- Auxiliary definition for addition on the Ore localization.  -/
_private.Mathlib.RingTheory.OreLocalization.Basic.0.OreLocalization.add'' : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : AddMonoid X] → [inst_3 : DistribMulAction R X] → X → ↥S → X → ↥S → OreLocalization S X
-- Std.Internal.Parsec.String
_private.Std.Internal.Parsec.String.0.Std.Internal.Parsec.String.skipWs.eq_def : ∀ {s : String} (it : s.Pos),
  Std.Internal.Parsec.String.skipWs✝ it =
    if h : ¬it.IsAtEnd then
      have c := it.get h;
      if c = '\t' ∨ c = '\n' ∨ c = '\x0d' ∨ c = ' ' then Std.Internal.Parsec.String.skipWs✝ (it.next h) else it
    else it
-- Mathlib.Algebra.Order.Monoid.Canonical.Basic
forall_lt_add_iff_lt_right : ∀ {α : Type u_1} [inst : LinearOrder α] {P : α → Prop} {b c : α} [inst_1 : AddCommMagma α] [CanonicallyOrderedAdd α]
  [AddLeftReflectLT α] [IsLeftCancelAdd α], (∀ a < b + c, P a) ↔ (∀ a < c, P a) ∧ ∀ d < b, P (d + c)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (obj : (X : Cᵒᵖ) → ModuleCat ↑(R.obj X))
  (map : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (obj Y))
  (map_id :
    autoParam
      (∀ (X : Cᵒᵖ),
        map (CategoryTheory.CategoryStruct.id X) =
          (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.id X))) ⋯).inv.app
            (obj X))
      PresheafOfModules.map_id._autoParam)
  (map_comp :
    autoParam
      (∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
        map (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (map f)
            (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (map g))
              ((ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                      (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.comp f g))) ⋯).inv.app
                (obj Z))))
      PresheafOfModules.map_comp._autoParam)
  (obj_1 : (X : Cᵒᵖ) → ModuleCat ↑(R.obj X))
  (map_1 : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → obj_1 X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (obj_1 Y))
  (map_id_1 :
    autoParam
      (∀ (X : Cᵒᵖ),
        map_1 (CategoryTheory.CategoryStruct.id X) =
          (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.id X))) ⋯).inv.app
            (obj_1 X))
      PresheafOfModules.map_id._autoParam)
  (map_comp_1 :
    autoParam
      (∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
        map_1 (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (map_1 f)
            (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (map_1 g))
              ((ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                      (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.comp f g))) ⋯).inv.app
                (obj_1 Z))))
      PresheafOfModules.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)