mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
/-- Postcompose a simplicial homotopy with a functor `F : C ⥤ D`.  -/
CategoryTheory.SimplicialObject.Homotopy.whiskerRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : CategoryTheory.SimplicialObject C} →
      {f g : X ⟶ Y} →
        CategoryTheory.SimplicialObject.Homotopy f g →
          {D : Type u'} →
            [inst_1 : CategoryTheory.Category.{v', u'} D] →
              (F : CategoryTheory.Functor C D) →
                CategoryTheory.SimplicialObject.Homotopy
                  (((CategoryTheory.SimplicialObject.whiskering C D).obj F).map f)
                  (((CategoryTheory.SimplicialObject.whiskering C D).obj F).map g)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- If `t` is a limit pullback cone over `f` and `g` and `h : W ⟶ X` and `k : W ⟶ Y` are such that
`h ≫ f = k ≫ g`, then we get `l : W ⟶ t.pt`, which satisfies `l ≫ fst t = h`
and `l ≫ snd t = k`, see `IsLimit.lift_fst` and `IsLimit.lift_snd`.  -/
CategoryTheory.Limits.PullbackCone.IsLimit.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          {t : CategoryTheory.Limits.PullbackCone f g} →
            CategoryTheory.Limits.IsLimit t →
              {W : C} →
                (h : W ⟶ X) →
                  (k : W ⟶ Y) →
                    CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g → (W ⟶ t.pt)
-- Batteries.Data.PairingHeap
/-- `O(1)`. Make a new heap containing `a`.  -/
Batteries.PairingHeap.singleton : {α : Type u} → {le : α → α → Bool} → α → Batteries.PairingHeap α le
-- Init.Data.Iterators.Basic
/-- Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means
is up to the `Iterator` instance but it should be strong enough to allow termination proofs.
 -/
Std.IterM.IsPlausibleStep : {α : Type w} →
  {m : Type w → Type w'} → {β : Type w} → [Std.Iterator α m β] → Std.IterM m β → Std.IterStep (Std.IterM m β) β → Prop
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.instIsLocallyInjectiveFunιOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  (F : CategoryTheory.Functor Cᵒᵖ (Type w)) (G : CategoryTheory.Subfunctor F),
  CategoryTheory.Presheaf.IsLocallyInjective J G.ι
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.modify_eq_empty_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β}, t.modify k f = ∅ ↔ t = ∅
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- Restrict from a superfield automorphism into a member of `gal p`.  -/
Polynomial.Gal.restrict : {F : Type u_1} →
  [inst : Field F] →
    (p : Polynomial F) →
      (E : Type u_2) →
        [inst_1 : Field E] →
          [inst_2 : Algebra F E] → [Fact (Polynomial.map (algebraMap F E) p).Splits] → Gal(E/F) →* p.Gal
-- Mathlib.Data.Finset.Image
Finset.image_inter_of_injOn : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] {f : α → β} (s t : Finset α),
  Set.InjOn f (↑s ∪ ↑t) → Finset.image f (s ∩ t) = Finset.image f s ∩ Finset.image f t
-- Mathlib.Combinatorics.Matroid.Circuit
/-- A version of `Matroid.isCocircuit_iff_minimal_compl_nonspanning` with a support assumption
in the minimality.  -/
Matroid.isCocircuit_iff_minimal_compl_nonspanning' : ∀ {α : Type u_1} {M : Matroid α} {K : Set α}, M.IsCocircuit K ↔ Minimal (fun X => ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- `quotQuotToQuotSup` and `liftSupQuotQuotMk` are inverse isomorphisms. In the case where
`I ≤ J`, this is the Third Isomorphism Theorem (see `DoubleQuot.quotQuotEquivQuotOfLE`).  -/
DoubleQuot.quotQuotEquivQuotSupₐ : (R : Type u) →
  {A : Type u_1} →
    [inst : CommSemiring R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] → (I J : Ideal A) → ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J) ≃ₐ[R] A ⧸ I ⊔ J
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientAtFilter_const : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (x : F) (L : Filter F) (c : 𝕜), HasGradientAtFilter (fun x => c) 0 x L
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasStrictDerivAt.sin : ∀ {f : ℝ → ℝ} {f' x : ℝ}, HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') x
-- Init.Grind.Ring.Field
Lean.Grind.Field.div_mul : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {x y z : α}, x / y * z = x * z / y
-- Mathlib.Topology.Compactness.Lindelof
/-- For every family of closed sets whose intersection avoids a Lindelöf set,
there exists a countable subfamily whose intersection avoids this Lindelöf set.  -/
IsLindelof.elim_countable_subfamily_closed : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
  IsLindelof s →
    ∀ (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
-- Mathlib.GroupTheory.Finiteness
/-- An additive monoid is finitely generated iff there exists a surjective
homomorphism from a `FreeAddMonoid` on finitely many generators. -/
AddMonoid.fg_iff_exists_freeAddMonoid_hom_surjective : ∀ {M : Type u_1} [inst : AddMonoid M], AddMonoid.FG M ↔ ∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ
-- Mathlib.GroupTheory.HNNExtension
/-- The list of pairs `(ℤˣ × G)`, where each pair `(u, g)` represents the element `t^u * g` of
`HNNExtension G A B φ`  -/
HNNExtension.NormalWord.ReducedWord.toList : {G : Type u_1} → [inst : Group G] → {A B : Subgroup G} → HNNExtension.NormalWord.ReducedWord G A B → List (ℤˣ × G)
-- Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap
QuadraticMap.lineDeriv : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : QuadraticMap 𝕜 E F),
  lineDeriv 𝕜 ⇑f = QuadraticMap.polar ⇑f
-- Init.Data.UInt.Lemmas
UInt8.toUSize_div : ∀ (a b : UInt8), (a / b).toUSize = a.toUSize / b.toUSize
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- Some chosen `EffectiveEpiFamilyStruct` associated to an effective epi family.  -/
CategoryTheory.EffectiveEpiFamily.getStruct : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {B : C} →
      {α : Type u_2} →
        (X : α → C) →
          (π : (a : α) → X a ⟶ B) →
            [CategoryTheory.EffectiveEpiFamily X π] → CategoryTheory.EffectiveEpiFamilyStruct X π
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `𝓕 : ι → β → α` is uniformly equicontinuous on `S` iff `range 𝓕` is uniformly
equicontinuous on `S`, i.e the family `(↑) : range F → β → α` is uniformly equicontinuous on `S`.  -/
uniformEquicontinuousOn_iff_range : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α} {S : Set β},
  UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn Subtype.val S
-- Mathlib.Algebra.Order.Group.Equiv
/-- `toLex` as an `AddEquiv`.  -/
toLexAddEquiv : (α : Type u_1) → [inst : Add α] → α ≃+ Lex α
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
_private.Mathlib.Topology.UniformSpace.UniformConvergenceTopology.0.UniformFun.termLowerAdjoint : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic.0.IsCovariantDerivativeOn.differenceAux_tensorial : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V]
  {cov cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {s : Set M},
  IsCovariantDerivativeOn F cov s →
    IsCovariantDerivativeOn F cov' s →
      ∀ x ∈ s, TensorialAt I F (fun x_1 => IsCovariantDerivativeOn.differenceAux✝ cov cov' x_1 x) x
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.forgetCreatesLimitsOfShape : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {T : CategoryTheory.Comonad C} →
          [CategoryTheory.Limits.PreservesLimitsOfShape J T.toFunctor] → CategoryTheory.CreatesLimitsOfShape J T.forget
-- Lean.Meta.Tactic.Simp.Types
/-- Similar to `Result.getProof`, but adds a `mkExpectedTypeHint` if `proof?` is `none`
(i.e., result is definitionally equal to input), but we cannot establish that
`source` and `r.expr` are definitionally when using `TransparencyMode.reducible`.  -/
Lean.Meta.Simp.Result.getProof' : Lean.Expr → Lean.Meta.Simp.Result → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_const_mul_left_iff' : ∀ {α : Type u_1} {F : Type u_4} {R : Type u_13} [inst : Norm F] [inst_1 : SeminormedRing R] {g : α → F} {l : Filter α}
  {f : α → R} {c : R}, IsUnit c → ((fun x => c * f x) =O[l] g ↔ f =O[l] g)
-- Mathlib.Data.List.DropRight
_private.Mathlib.Data.List.DropRight.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Batteries.Data.BinomialHeap.Basic
/-- `O(1)`. The heap containing a single value `a`.  -/
Batteries.BinomialHeap.Imp.Heap.singleton : {α : Type u_1} → α → Batteries.BinomialHeap.Imp.Heap α
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- For real `s > 1`, the logarithm of the (real) Riemann zeta function equals
`∑' n, Λ n / (n ^ s * Real.log n)`, where `Λ` is the von Mangoldt function.
 -/
log_riemannZeta_eq : ∀ {s : ℝ}, 1 < s → Real.log (riemannZeta ↑s).re = ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n / (↑n ^ s * Real.log ↑n)
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_add_right_mul : ∀ {α : Type u} [inst : CommRing α] (x y z : α), Ideal.span {x + y * z, y} = Ideal.span {x, y}
-- Mathlib.ModelTheory.Syntax
/-- Puts an `∃` quantifier on a bounded formula.  -/
FirstOrder.«term∃'_» : Lean.ParserDescr
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SSameSide.not_sOppSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SSameSide x y → ¬s.SOppSide x y
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- Zero semiconjugates any element to itself.  -/
AddSemiconjBy.zero_left : ∀ {M : Type u_2} [inst : AddZeroClass M] (x : M), AddSemiconjBy 0 x x
-- Lean.Compiler.IR.CompilerM
Lean.IR.LogEntry.message.inj : ∀ {msg msg_1 : Std.Format}, Lean.IR.LogEntry.message msg = Lean.IR.LogEntry.message msg_1 → msg = msg_1
-- Init.Data.List.Sublist
List.suffix_iff_exists_append_eq : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ ↔ ∃ l₃, l₃ ++ l₁ = l₂
-- Mathlib.Order.SupClosed
SupClosed.image : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] {s : Set α}
  [inst_2 : FunLike F α β] [SupHomClass F α β], SupClosed s → ∀ (f : F), SupClosed (⇑f '' s)
-- Init.Data.String.Lemmas.Iter
Std.Iter.intercalateString_eq : ∀ {α β : Type} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : ToString β] {s : String.Slice}
  {it : Std.Iter β}, Std.Iter.intercalateString s it = s.copy.intercalate (List.map toString it.toList)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- This definition allows to endow `α × β` with a normed space structure corresponding to
the Lp norm. It is useful for type synonyms of `α × β`.  -/
WithLp.normedSpaceSeminormedAddCommGroupToProd : (p : ENNReal) →
  [hp : Fact (1 ≤ p)] →
    (α : Type u_4) →
      (β : Type u_5) →
        [inst : SeminormedAddCommGroup α] →
          [inst_1 : SeminormedAddCommGroup β] →
            {R : Type u_6} → [inst_2 : NormedField R] → [NormedSpace R α] → [NormedSpace R β] → NormedSpace R (α × β)
-- Mathlib.Topology.Inseparable
SeparationQuotient.nontrivial_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α], Nontrivial (SeparationQuotient α) ↔ NontrivialTopology α
-- Init.Data.String.Basic
String.Slice.Pos.copy_eq_append_get : ∀ {s : String.Slice} {pos : s.Pos} (h : pos ≠ s.endPos),
  ∃ t₁ t₂, s.copy = t₁ ++ String.singleton (pos.get h) ++ t₂ ∧ t₁.utf8ByteSize = pos.offset.byteIdx
-- Mathlib.CategoryTheory.Yoneda
/-- See also `map_yonedaEquiv'` for a more general version.  -/
CategoryTheory.map_yonedaEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
  (f : CategoryTheory.yoneda.obj X ⟶ F) (g : Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (F.map g.op)) (CategoryTheory.yonedaEquiv f) =
    (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op Y))) g
-- Std.Do.SPred.SVal
/-- A tuple capturing the whole state of an `SVal`.  -/
Std.Do.SVal.StateTuple : List (Type u) → Type u
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
/-- The inverse system of finite homomorphisms.  -/
SimpleGraph.finsubgraphHomFunctor : {V : Type u} →
  {W : Type v} → (G : SimpleGraph V) → SimpleGraph W → CategoryTheory.Functor G.Finsubgraphᵒᵖ (Type (max u v))
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.mem_horn_iff : ∀ {n : ℕ} (i : Fin (n + 1)) {m : SimplexCategoryᵒᵖ} (x : (SSet.stdSimplex.obj { len := n }).obj m),
  x ∈ (SSet.horn n i).obj m ↔ Set.range ⇑(SSet.stdSimplex.asOrderHom x) ∪ {i} ≠ Set.univ
-- Mathlib.Order.DirSupClosed
DirSupInaccOn.sUnion : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α] {s : Set (Set α)},
  (∀ x ∈ s, DirSupInaccOn D x) → DirSupInaccOn D (⋃₀ s)
-- Init.Data.String.Defs
String.utf8ByteSize_empty : "".utf8ByteSize = 0
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.rightHom_comp_inl : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (S : GroupExtension N E G), S.rightHom.comp S.inl = 1
-- Init.Data.Range.Polymorphic.IntLemmas
/-- Induction principle for proving properties of `Int`-based ranges of the form `a<...=b`
by varying the lower bound.

In the `base` case, one proves that for any `a : Int` and `b : Int` with
`b ≤ a`, the statement holds for the empty range `a<...=b`.

In the `step` case, one proves that for any `a : Int` and `b : Int`, the
statement holds for nonempty ranges `a<...=b` if it holds for the smaller range
`(a + 1)<...=b`.

The following is an example reproving `length_toList_roc`.

```
example (a b : Int) : (a<...=b).toList.length = (b - a).toNat := by
  induction a, b using Int.induct_roc_left
  case base =>
    simp only [Int.toList_roc_eq_nil, List.length_nil, Int.zero_eq_toNat_sub_iff, *]
  case step =>
    simp only [Int.toList_roc_eq_cons, List.length_cons, *]; omega
``` -/
Int.induct_roc_left : ∀ (motive : ℤ → ℤ → Prop),
  (∀ (a b : ℤ), b ≤ a → motive a b) → (∀ (a b : ℤ), a < b → motive (a + 1) b → motive a b) → ∀ (a b : ℤ), motive a b
-- Mathlib.Analysis.Normed.Algebra.Basic
IntermediateField.instNontriviallyNormedFieldSubtypeMem : {K : Type u_1} →
  {L : Type u_2} →
    [inst : NontriviallyNormedField K] →
      [inst_1 : NormedField L] → [inst_2 : NormedAlgebra K L] → (F : IntermediateField K L) → NontriviallyNormedField ↥F
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_right₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Sub β]
  [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.Kernel.IndepFun (f i) (f j - f k) κ μ
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flipFunctor_map_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  (CategoryTheory.Square.flipFunctor.map φ).τ₂ = φ.τ₃
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_nonneg_of_predicate : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : LE A]
  [inst_10 : ContinuousFunctionalCalculus R A fun x => 0 ≤ x] {f : R → R} {a : A}, 0 ≤ cfc f a
-- Mathlib.Topology.Algebra.MulAction
/-- Class `ContinuousVAdd M X` says that the additive action `(+ᵥ) : M → X → X`
is continuous in both arguments. We use the same class for all kinds of additive actions,
including (semi)modules and algebras.  -/
ContinuousVAdd : (M : Type u_1) → (X : Type u_2) → [VAdd M X] → [TopologicalSpace M] → [TopologicalSpace X] → Prop
-- Mathlib.Analysis.Convex.Between
wbtw_swap_left_iff : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] {x y : P}
  (z : P), Wbtw R x y z ∧ Wbtw R y x z ↔ x = y
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- Turn a comonoid object into a monoid object in the opposite category.
 -/
CategoryTheory.Comon.ComonToMonOpOpObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Comon C → CategoryTheory.Mon Cᵒᵖ
-- Mathlib.Order.CountableSupClosed
finsetSup'_mem_countableSupClosure : ∀ {α : Type u_2} {s : Set α} {ι : Type u_4} [inst : SemilatticeSup α] {t : Finset ι} (ht : t.Nonempty) {f : ι → α},
  (∀ i ∈ t, f i ∈ s) → t.sup' ht f ∈ countableSupClosure s
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
/-- Define the equalizing object  -/
CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.constructEqualizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasBinaryProducts C] →
      [CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C → C
-- Mathlib.Algebra.Torsor.Basic
Set.prod_sdiv_prod_comm : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : Group G] [inst_1 : Group G']
  [inst_2 : Torsor G P] [inst_3 : Torsor G' P'] (s₁ s₂ : Set P) (t₁ t₂ : Set P'),
  s₁ ×ˢ t₁ /ₛ s₂ ×ˢ t₂ = (s₁ /ₛ s₂) ×ˢ (t₁ /ₛ t₂)
-- Mathlib.Algebra.Exact.Basic
/-- Given an exact sequence `M → N → P → 0`, giving a retraction `N → M` is equivalent to giving a
splitting `N ≃ M × P`.  -/
Function.Exact.splitInjectiveEquiv : {R : Type u_8} →
  {M : Type u_9} →
    {N : Type u_10} →
      {P : Type u_11} →
        [inst : Semiring R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      {f : M →ₗ[R] N} →
                        {g : N →ₗ[R] P} →
                          Function.Exact ⇑f ⇑g →
                            Function.Surjective ⇑g →
                              { l // l ∘ₗ f = LinearMap.id } ≃
                                { e // f = ↑e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ ↑e }
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.Ctx.mk.sizeOf_spec : ∀ (root : Lean.TSyntax `tactic) (terminal : Bool) (config : Lean.Try.Config) (originalMaxHeartbeats : ℕ),
  sizeOf { root := root, terminal := terminal, config := config, originalMaxHeartbeats := originalMaxHeartbeats } =
    1 + sizeOf root + sizeOf terminal + sizeOf config + sizeOf originalMaxHeartbeats
-- Mathlib.FieldTheory.AbsoluteGaloisGroup
Field.instGroupAbsoluteGaloisGroup : (K : Type u_1) → [inst : Field K] → Group (Field.absoluteGaloisGroup K)
-- Lean.Parser.Command
Lean.Parser.Command.example : Lean.Parser.Parser
-- Mathlib.Algebra.Category.BoolRing
_private.Mathlib.Algebra.Category.BoolRing.0.BoolRing.Hom.mk.inj : ∀ {R : BoolRing} {S : BoolRing} {hom' hom'_1 : ↑R →+* ↑S}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Init.Data.SInt.Lemmas
Int64.toInt_ofNat' : ∀ {n : ℕ}, (Int64.ofNat n).toInt = (↑n).bmod Int64.size
-- Mathlib.Algebra.Homology.Homotopy
/-- The forward chain map  -/
HomotopyEquiv.hom : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → HomotopyEquiv C D → (C ⟶ D)
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
/-- Assume that the processes $((X^t_s)_{s \in S_t})_{t \in T}$ are jointly Gaussian. Then they are
independent if for all $t_1, t_2 \in T$ with $t_1 \ne t_2$ and
$s_1 \in S_{t_1}$, $s_2 \in S_{t_2}$, $X^{t_1}_{s_1}$ and $X^{t_2}_{s_2}$ are uncorrelated.  -/
ProbabilityTheory.IsGaussianProcess.iIndepFun_of_covariance_eq_zero : ∀ {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : T → Type u_4}
  {X : (t : T) → S t → Ω → ℝ},
  ProbabilityTheory.IsGaussianProcess (fun p ω => X p.fst p.snd ω) P →
    (∀ (t : T) (s : S t), AEMeasurable (X t s) P) →
      (∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂), ProbabilityTheory.covariance (X t₁ s₁) (X t₂ s₂) P = 0) →
        ProbabilityTheory.iIndepFun (fun t ω s => X t s ω) P
-- Mathlib.Algebra.Lie.Basic
LieEquiv.mk.injEq : ∀ {R : Type u} {L : Type v} {L' : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (toLieHom : L →ₗ⁅R⁆ L') (invFun : L' → L)
  (left_inv : autoParam (Function.LeftInverse invFun (↑toLieHom).toFun) LieEquiv.left_inv._autoParam)
  (right_inv : autoParam (Function.RightInverse invFun (↑toLieHom).toFun) LieEquiv.right_inv._autoParam)
  (toLieHom_1 : L →ₗ⁅R⁆ L') (invFun_1 : L' → L)
  (left_inv_1 : autoParam (Function.LeftInverse invFun_1 (↑toLieHom_1).toFun) LieEquiv.left_inv._autoParam)
  (right_inv_1 : autoParam (Function.RightInverse invFun_1 (↑toLieHom_1).toFun) LieEquiv.right_inv._autoParam),
  ({ toLieHom := toLieHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toLieHom := toLieHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }) =
    (toLieHom = toLieHom_1 ∧ invFun = invFun_1)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.powerSeriesPart_zero : ∀ {R : Type u_1} [inst : Semiring R], LaurentSeries.powerSeriesPart 0 = 0
-- Mathlib.AlgebraicGeometry.Birational.Composition
AlgebraicGeometry.Scheme.PartialMap.id_comp : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : IrreducibleSpace ↥X] (f : X.PartialMap Y),
  (AlgebraicGeometry.Scheme.PartialMap.id X).comp f = f
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgHom.range_comp : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : NonUnitalNonAssocSemiring C] [inst_8 : Module R C] [inst_9 : Star C] (f : A →⋆ₙₐ[R] B) (g : B →⋆ₙₐ[R] C),
  NonUnitalStarAlgHom.range (g.comp f) = NonUnitalStarSubalgebra.map g (NonUnitalStarAlgHom.range f)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.instUniformSpaceRatFuncAdicCompl : (K : Type u_2) → [inst : Field K] → UniformSpace (LaurentSeries.RatFuncAdicCompl K)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofZeros_g' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0),
  (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg).g' = 0