mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.BorrowedAnnotation
Lean.isMarkedBorrowed : Lean.Expr → Bool
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_set_mk : ∀ {R : Type u} [inst : NonAssocSemiring R] {toSubmonoid : Submonoid R}
  (add_mem : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier)
  (zero_mem : 0 ∈ toSubmonoid.carrier),
  ↑{ toSubmonoid := toSubmonoid, add_mem' := add_mem, zero_mem' := zero_mem } = ↑toSubmonoid
-- Mathlib.Algebra.DirectSum.Ring
/-- A direct sum of copies of a `CommSemiring` inherits the commutative multiplication structure.  -/
CommSemiring.directSumGCommSemiring : (ι : Type u_1) →
  {R : Type u_2} → [inst : AddCommMonoid ι] → [inst_1 : CommSemiring R] → DirectSum.GCommSemiring fun x => R
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂Iso_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : C ≌ A} {G : D ≌ B}
  (α : F.functor.comp U ⟶ S.comp G.functor) (α' : F.inverse.comp S ⟶ U.comp G.inverse)
  (hα'α :
    CategoryTheory.CategoryStruct.comp S.leftUnitor.hom
        (CategoryTheory.CategoryStruct.comp S.rightUnitor.inv
          (CategoryTheory.CategoryStruct.comp (S.whiskerLeft G.unitIso.hom) (S.associator G.functor G.inverse).inv)) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom S)
        (CategoryTheory.CategoryStruct.comp (F.functor.associator F.inverse S).hom
          (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft α')
            (CategoryTheory.CategoryStruct.comp (F.functor.associator U G.inverse).inv
              (CategoryTheory.Functor.whiskerRight α G.inverse)))))
  (hαα' :
    CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft α)
        (CategoryTheory.CategoryStruct.comp (F.inverse.associator S G.functor).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α' G.functor)
            (CategoryTheory.CategoryStruct.comp (U.associator G.inverse G.functor).hom
              (U.whiskerLeft G.counitIso.hom)))) =
      CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor U).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.counitIso.hom U)
          (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv)))
  (β : G.functor.obj T ⟶ V) (β' : G.inverse.obj V ⟶ T)
  (hββ' : CategoryTheory.CategoryStruct.comp (G.inverse.map β) β' = G.unitIso.inv.app T)
  (hβ'β : CategoryTheory.CategoryStruct.comp (G.functor.map β') β = G.counitIso.hom.app V),
  (CategoryTheory.CostructuredArrow.map₂Iso α α' hα'α hαα' β β' hββ' hβ'β).counitIso =
    CategoryTheory.CostructuredArrow.map₂CompMap₂Iso α β α' β' ≪≫
      CategoryTheory.CostructuredArrow.map₂Congr
          (CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor U).hom
            (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft α)
              (CategoryTheory.CategoryStruct.comp (F.inverse.associator S G.functor).inv
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α' G.functor)
                  (U.associator G.inverse G.functor).hom))))
          (CategoryTheory.CategoryStruct.comp (G.functor.map β') β) F.counitIso G.counitIso
          (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv)
          (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id B).obj V)) ⋯ ⋯ ≪≫
        CategoryTheory.CostructuredArrow.map₂IdIso
          (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv) V
          (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id B).obj V)) ⋯ ⋯
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_symm_apply_mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Sₚ : Type u_4) [inst_4 : CommRing Sₚ] [inst_5 : Algebra S Sₚ]
  [inst_6 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] (P : Ideal S) [hPp : P.LiesOver p]
  [inst_7 : P.IsMaximal] (x : S) (s : ↥(Algebra.algebraMapSubmonoid S p.primeCompl)),
  (IsLocalization.AtPrime.equivQuotientMapOfIsMaximal p Sₚ P).symm
      ((Ideal.Quotient.mk (Ideal.map (algebraMap S Sₚ) P)) (IsLocalization.mk' Sₚ x s)) =
    (Ideal.Quotient.mk P) x * ((Ideal.Quotient.mk P) ↑s)⁻¹
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.neg : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {l : Filter α} {f : α → E}, MeasureTheory.IntegrableAtFilter f l μ → MeasureTheory.IntegrableAtFilter (-f) l μ
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The median of a simplex is the line through the vertex and the centroid.  -/
Affine.Simplex.median_eq_line_point_centroid : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.median i = line[k, s.points i, s.centroid]
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_subgroupOf : ∀ {G : Type u_1} [inst : Group G] {H K L : Subgroup G},
  K ≤ L → (H.subgroupOf L).relIndex (K.subgroupOf L) = H.relIndex K
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.mk.sizeOf_spec : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} [inst_5 : SizeOf R] [inst_6 : SizeOf M₁] [inst_7 : SizeOf M₂]
  (toLinearMap : M₁ →ₗ[R] M₂) (map_app' : ∀ (m m' : M₁), (B₂ (toLinearMap.toFun m)) (toLinearMap.toFun m') = (B₁ m) m'),
  sizeOf { toLinearMap := toLinearMap, map_app' := map_app' } = 1 + sizeOf toLinearMap
-- Mathlib.Data.PFun
PFun.bind_defined : ∀ {α : Type u_7} {β γ : Type u_8} (p : Set α) {f : α →. β} {g : β → α →. γ},
  p ⊆ f.Dom → (∀ (x : β), p ⊆ (g x).Dom) → p ⊆ (f >>= g).Dom
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.isOpen_compl_lattice_sdiff : ∀ (L : PeriodPair) {s : Set ℂ}, IsOpen (↑L.lattice \ s)ᶜ
-- Mathlib.RingTheory.Polynomial.Pochhammer
/-- `descPochhammer S n` is monotone on `[n-1, ∞)`.  -/
monotoneOn_descPochhammer_eval : ∀ {S : Type u_1} [inst : Ring S] [inst_1 : PartialOrder S] [IsStrictOrderedRing S] (n : ℕ),
  MonotoneOn (fun x => Polynomial.eval x (descPochhammer S n)) (Set.Ici (↑n - 1))
-- Init.Data.Int.Order
Int.neg_le_iff : ∀ {x y : ℤ}, -x ≤ y ↔ -y ≤ x
-- Mathlib.Order.RelIso.Basic
RelIso.cast_toEquiv : ∀ {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} (h₁ : α = β) (h₂ : r ≍ s),
  (RelIso.cast h₁ h₂).toEquiv = Equiv.cast h₁
-- Mathlib.Topology.NhdsWithin
Filter.Eventually.self_of_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {p : α → Prop} {s : Set α} {x : α},
  (∀ᶠ (y : α) in nhdsWithin x s, p y) → x ∈ s → p x
-- Lean.Parser.Syntax
Lean.Parser.syntaxParser.parenthesizer : optParam ℕ 0 → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.mul : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [inst : Mul β] {g : α → β},
  Filter.EventuallyConst f l → Filter.EventuallyConst g l → Filter.EventuallyConst (f * g) l
-- Mathlib.Algebra.Lie.Submodule
LieModuleHom.ker_id : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], LieModuleHom.id.ker = ⊥
-- Std.Http.Data.Status
Std.Http.Status.methodNotAllowed.sizeOf_spec : sizeOf Std.Http.Status.methodNotAllowed = 1
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.foldr_cons : ∀ {α : Type u_1} (t : RBTree.RBNode.Stream α) (l : List α),
  RBTree.RBNode.Stream.foldr (fun x1 x2 => x1 :: x2) t l = t.toList ++ l
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedHull_mono : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s t : Set E},
  s ⊆ t → balancedHull 𝕜 s ⊆ balancedHull 𝕜 t
-- Mathlib.Order.RelIso.Basic
/-- For a `β`-relation `r`, an embedding `f : α ↪ β` induces a relation embedding from `r.onFun f`
to `r`.  -/
RelEmbedding.ofOnFun : {α : Type u_1} → {β : Type u_2} → (r : β → β → Prop) → (f : α ↪ β) → Function.onFun r ⇑f ↪r r
-- Init.Data.Array.Lemmas
Array.flatMap_push : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {x : α} {f : α → Array β},
  Array.flatMap f (xs.push x) = Array.flatMap f xs ++ f x
-- Mathlib.FieldTheory.Normal.Basic
/-- If `E/Kᵢ/F` are towers of fields with `E/F` normal then we can lift
an algebra homomorphism `ϕ : K₁ →ₐ[F] K₂` to `ϕ.liftNormal E : E →ₐ[F] E`.  -/
AlgHom.liftNormal : {F : Type u_1} →
  [inst : Field F] →
    {K₁ : Type u_3} →
      {K₂ : Type u_4} →
        [inst_1 : Field K₁] →
          [inst_2 : Field K₂] →
            [inst_3 : Algebra F K₁] →
              [inst_4 : Algebra F K₂] →
                (K₁ →ₐ[F] K₂) →
                  (E : Type u_6) →
                    [inst_5 : Field E] →
                      [inst_6 : Algebra F E] →
                        [inst_7 : Algebra K₁ E] →
                          [inst_8 : Algebra K₂ E] →
                            [IsScalarTower F K₁ E] → [IsScalarTower F K₂ E] → [h : Normal F E] → E →ₐ[F] E
-- Mathlib.Algebra.Order.Ring.Synonym
toDual_intCast : ∀ {R : Type u_1} [inst : IntCast R] (n : ℤ), OrderDual.toDual ↑n = ↑n
-- Lean.Expr
Lean.Expr.getForallBodyMaxDepth : ℕ → Lean.Expr → Lean.Expr
-- Mathlib.GroupTheory.Coxeter.Basic
/-- Push a Coxeter system through a group isomorphism.  -/
CoxeterSystem.map : {B : Type u_1} →
  {W : Type u_3} →
    {H : Type u_4} →
      [inst : Group W] → [inst_1 : Group H] → {M : CoxeterMatrix B} → CoxeterSystem M W → W ≃* H → CoxeterSystem M H
-- Mathlib.Algebra.Category.BialgCat.Monoidal
BialgCat.leftUnitor_def : ∀ (R : Type u) [inst : CommRing R] (X : BialgCat R),
  CategoryTheory.MonoidalCategoryStruct.leftUnitor X = (Bialgebra.TensorProduct.lid R X.carrier).toBialgIso
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProduct_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P Q : CategoryTheory.ObjectProperty C) (X : C),
  P.extensionProduct Q X ↔
    ∃ Y Z f g h,
      CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ∧
        P Y ∧ Q Z
-- Init.Data.BitVec.Bootstrap
BitVec.eq_of_getElem_eq_iff : ∀ {n : ℕ} {x y : BitVec n}, x = y ↔ ∀ (i : ℕ) (hi : i < n), x[i] = y[i]
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropEndWhile_append_takeEndWhile : ∀ {ρ : Type} {pat : ρ} [String.Slice.Pattern.Model.PatternModel pat] [inst : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.LawfulBackwardPattern pat] {s : String},
  (s.dropEndWhile pat).copy ++ (s.takeEndWhile pat).copy = s
-- Mathlib.Probability.Independence.Conditional
/-- Two functions are conditionally independent if the two measurable space structures they generate
are conditionally independent. For a function `f` with codomain having measurable space structure
`m`, the generated measurable space structure is `m.comap f`.
See `ProbabilityTheory.condIndepFun_iff`.
We use the notation `X ⟂ᵢ[Z, hZ; μ] Y` to write that `X` and `Y` are conditionally independent
given (the σ-algebra generated by) `Z` (scoped in `ProbabilityTheory`).  -/
ProbabilityTheory.CondIndepFun : {Ω : Type u_1} →
  (m' : MeasurableSpace Ω) →
    {mΩ : MeasurableSpace Ω} →
      [StandardBorelSpace Ω] →
        m' ≤ mΩ →
          {β : Type u_3} →
            {γ : Type u_4} →
              [MeasurableSpace β] →
                [MeasurableSpace γ] →
                  (Ω → β) →
                    (Ω → γ) →
                      (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.CondIndepFun._auto_1) →
                        [MeasureTheory.IsFiniteMeasure μ] → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Filter.Tendsto.arccos_nhdsGE : ∀ {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ},
  Filter.Tendsto f l (nhdsWithin x (Set.Ici x)) →
    Filter.Tendsto (fun x => Real.arccos (f x)) l (nhdsWithin (Real.arccos x) (Set.Iic (Real.arccos x)))
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
IsLinearSet.exists_fg_eq_subtypeVal : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M},
  IsLinearSet s → ∃ P s', P.FG ∧ IsLinearSet s' ∧ s = Subtype.val '' s'
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sSup_sub : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : AddGroup M] [AddLeftMono M] [AddRightMono M] (s t : Set M),
  sSup (s - t) = sSup s - sInf t
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const_ext : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f₁ f₂ : M} {g₁ g₂ : R}
  {U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)} {hu₁ : U ≤ PrimeSpectrum.basicOpen g₁}
  {hu₂ : U ≤ PrimeSpectrum.basicOpen g₂},
  g₂ • f₁ = g₁ • f₂ →
    AlgebraicGeometry.StructureSheaf.const f₁ g₁ U hu₁ = AlgebraicGeometry.StructureSheaf.const f₂ g₂ U hu₂
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.ExactPairing.evaluation_coevaluation' : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {X Y : C}
  [self : CategoryTheory.ExactPairing X Y],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ExactPairing.coevaluation' X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y X).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.ExactPairing.evaluation')) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.CreatesColimitsOfSize.CreatesColimitsOfShape : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {F : CategoryTheory.Functor C D} →
          [self : CategoryTheory.CreatesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] →
            {J : Type w} → [inst_2 : CategoryTheory.Category.{w', w} J] → CategoryTheory.CreatesColimitsOfShape J F
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.natCast_mul_omega0 : ∀ {n : ℕ}, 0 < n → ↑n * Ordinal.omega0 = Ordinal.omega0
-- Lean.Elab.DeprecatedSyntax
/-- Optional version or date at which the syntax was deprecated.  -/
Lean.Elab.SyntaxDeprecationEntry.since? : Lean.Elab.SyntaxDeprecationEntry → Option String
-- Init.Data.Vector.Lemmas
Vector.getElem?_setIfInBounds_self : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n} {x : α}, (xs.setIfInBounds i x)[i]? = if i < n then some x else none
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- setoid instance identifying two isometric nonempty compact subspaces of ℓ^∞(ℝ)  -/
GromovHausdorff.IsometryRel.setoid : Setoid (TopologicalSpace.NonemptyCompacts ↥(lp (fun n => ℝ) ⊤))
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
Finset.sum_sq_le_sq_sum_of_nonneg : ∀ {ι : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {f : ι → R}
  {s : Finset ι}, (∀ i ∈ s, 0 ≤ f i) → ∑ i ∈ s, f i ^ 2 ≤ (∑ i ∈ s, f i) ^ 2
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_eq_detp_sub_detp : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R),
  M.det = Matrix.detp 1 M - Matrix.detp (-1) M
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.zipWith.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (x : α) (xs : List α) (y : β) (ys : List β)
  (h_1 : (x : α) → (xs : List α) → (y : β) → (ys : List β) → motive (x :: xs) (y :: ys))
  (h_2 : (x : List α) → (x_1 : List β) → motive x x_1),
  (match x :: xs, y :: ys with
    | x :: xs, y :: ys => h_1 x xs y ys
    | x, x_1 => h_2 x x_1) =
    h_1 x xs y ys
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instPowInt16SintOfNatNat : Lean.Grind.ToInt.Pow Int16 (Lean.Grind.IntInterval.sint 16)
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
/-- The first horizontal arrow in the top row.  -/
_private.Mathlib.RingTheory.AdicCompletion.AsTensorProduct.0.AdicCompletion.lTensorKerIncl : {R : Type u} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {ι : Type} →
              (f : (ι → R) →ₗ[R] M) →
                TensorProduct R (AdicCompletion I R) ↥f.ker →ₗ[AdicCompletion I R]
                  TensorProduct R (AdicCompletion I R) (ι → R)
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- The quotient functor from the category of fibrant objects to its
homotopy category.  -/
HomotopicalAlgebra.FibrantObject.toHoCat : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.Functor (HomotopicalAlgebra.FibrantObject C) (HomotopicalAlgebra.FibrantObject.HoCat C)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
CategoryTheory.Limits.pointwiseBinaryBicone_inr_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [inst_3 : CategoryTheory.Category.{v_2, u_2} D]
  (F G : CategoryTheory.Functor D C) (X : D),
  (CategoryTheory.Limits.pointwiseBinaryBicone F G).inr.app X = CategoryTheory.Limits.biprod.inr
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.coe_neg : ∀ {G : Type u_2} [inst : AddGroup G] (S : AddSubmonoid G), ↑(-S) = -↑S
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.curry_inv_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_4} {Z : Type u_5} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : Inv Z] [inst_4 : ContinuousInv Z] (f : C(X × Y, Z)) (x : X),
  f⁻¹.curry x = (f.curry x)⁻¹
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.ofPowerSeries_C : ∀ {Γ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : Semiring Γ] [inst_2 : PartialOrder Γ]
  [inst_3 : IsStrictOrderedRing Γ] (r : R), (HahnSeries.ofPowerSeries Γ R) (PowerSeries.C r) = HahnSeries.C r
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.union_sdiv : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s₁ s₂ t : Set β}, s₁ ∪ s₂ /ₛ t = s₁ /ₛ t ∪ (s₂ /ₛ t)
-- Mathlib.Data.Set.Sigma
Set.mem_sigma_iff : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {x : (i : ι) × α i},
  x ∈ s.sigma t ↔ x.fst ∈ s ∧ x.snd ∈ t x.fst
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.emb_injective : ∀ {n : ℕ} (c : OrderedFinpartition n), Function.Injective fun p => c.emb p.fst p.snd
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst : Inhabited β], k ∉ t₁ → (t₁ ∪ t₂)[k]! = t₂[k]!
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalGroup.leftUniformSpace.congr_simp : ∀ (G : Type u_1) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  IsTopologicalGroup.leftUniformSpace G = IsTopologicalGroup.leftUniformSpace G
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.embDomain_notin_image_support : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'}, b ∉ ⇑f '' x.support → (HahnSeries.embDomain f x).coeff b = 0
-- Mathlib.CategoryTheory.Comma.Final
/-- Let `A` and `B` be cofiltered categories, `L : A ⥤ T` be initial and `R : B ⥤ T`. Then, the
projection `fst L R : Comma L R ⥤ A` is initial.  -/
CategoryTheory.Comma.initial_fst : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [CategoryTheory.IsCofiltered A] [CategoryTheory.IsCofiltered B] [L.Initial],
  (CategoryTheory.Comma.fst L R).Initial
-- Mathlib.Dynamics.Ergodic.Function
QuasiErgodic.eq_const_of_compQuasiMeasurePreserving_eq : ∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace X]
  [TopologicalSpace.MetrizableSpace X] [Nonempty X] {f : α → α} (h : QuasiErgodic f μ) {g : α →ₘ[μ] X},
  g.compQuasiMeasurePreserving f ⋯ = g → ∃ c, g = MeasureTheory.AEEqFun.const α c
-- Mathlib.Order.Interval.Finset.Defs
/-- Note we define `Iic (toDual a)` as `Ici a` (which has type `Finset α` not `Finset αᵒᵈ`!)
instead of `(Ici a).map toDual.toEmbedding` as this means the following is defeq:
```
lemma this : (Iic (toDual (toDual a)) :) = (Iic a :) := rfl
```
 -/
OrderDual.instLocallyFiniteOrderBot : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderTop α] → LocallyFiniteOrderBot αᵒᵈ
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.prob_compl_eq_zero_iff₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.NullMeasurableSet s μ → (μ sᶜ = 0 ↔ μ s = 1)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.core : Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneUnopOfCoconeEquiv_inverse_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} {Y X : CategoryTheory.Limits.Cone F.unop} (f : Y ⟶ X),
  CategoryTheory.Limits.coneUnopOfCoconeEquiv.inverse.map f = Opposite.op { hom := f.hom.op, w := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.lift_mk_factorThruImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.image.lift
        { I := CategoryTheory.Limits.image f, m := CategoryTheory.Limits.image.ι f, m_mono := ⋯,
          e := CategoryTheory.Limits.factorThruImage f, fac := ⋯ })
      (CategoryTheory.Limits.image.ι f) =
    CategoryTheory.Limits.image.ι f
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.one : ∀ {M : Type u_1} [inst : CommMonoid M], IsPrimitiveRoot 1 1
-- Mathlib.Logic.Encodable.Basic
Encodable.encode_sigma_val : ∀ {α : Type u_1} {γ : α → Type u_3} [inst : Encodable α] [inst_1 : (a : α) → Encodable (γ a)] (a : α) (b : γ a),
  Encodable.encode ⟨a, b⟩ = Nat.pair (Encodable.encode a) (Encodable.encode b)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ofLinearEquiv_toLinearEquiv : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (map_mul : ↑e 1 = 1)
  (map_one : ∀ (x y : A₁), ↑e (x * y) = ↑e x * ↑e y), AlgEquiv.ofLinearEquiv (↑e) map_mul map_one = e
-- Mathlib.Data.Sign.Defs
sign_eq_sign_or_eq_neg : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : LinearOrder α] {a b : α},
  a ≠ 0 → b ≠ 0 → SignType.sign a = SignType.sign b ∨ SignType.sign a = -SignType.sign b
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The rpc method of the `rw??` widget.  -/
Mathlib.Tactic.LibraryRewrite.rpc : SelectInsertParams → Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)