mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Ring.Limits
/-- Witness that the limit cone in `SemiRingCat` is a limit cone.
(Internal use only; use the limits API.)
 -/
SemiRingCat.HasLimits.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J SemiRingCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] →
        CategoryTheory.Limits.IsLimit (SemiRingCat.HasLimits.limitCone F)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ioi : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x * a) ⁻¹' Set.Ioi b = Set.Ioi (b / a)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.instHaveLebesgueDecompositionZeroLeft : ∀ {α : Type u_1} {m : MeasurableSpace α} {ν : MeasureTheory.Measure α},
  MeasureTheory.Measure.HaveLebesgueDecomposition 0 ν
-- Mathlib.Topology.Separation.Basic
specializes_iff_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x y : X}, x ⤳ y ↔ x = y
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- Implementation of `SheafConditionPairwiseIntersections.coneEquiv`.  -/
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              CategoryTheory.Functor
                (CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
                (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
ruzsaSzemerediNumberNat_mono : Monotone ruzsaSzemerediNumberNat
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.nontrivial_of_rankAtStalk_pos : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  0 < Module.rankAtStalk M → Nontrivial M
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.IsSubordinate.support_subset : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} {fs : SmoothBumpCovering ι I M s}
  {U : M → Set M}, fs.IsSubordinate U → ∀ (i : ι), Function.support ↑(fs.toFun i) ⊆ U (fs.c i)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.of_apply : ∀ (k : Type u_1) (G : Type u_2) [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k] (a : G),
  (SkewMonoidAlgebra.of k G) a = SkewMonoidAlgebra.single a 1
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.isExtensionPair_iff_cod : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.IsExtensionPair M N ↔ ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g
-- Mathlib.Order.WithBot
WithBot.instWellFoundedLT : ∀ {α : Type u_1} [inst : LT α] [WellFoundedLT α], WellFoundedLT (WithBot α)
-- Init.Data.UInt.Lemmas
UInt8.instIsLinearOrder : Std.IsLinearOrder UInt8
-- Mathlib.CategoryTheory.Monoidal.Braided.Transport
CategoryTheory.Monoidal.fromInducedCoreMonoidal.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategoryStruct D]
  (F : CategoryTheory.Functor D C) [inst_4 : F.Faithful] (fData : CategoryTheory.Monoidal.InducingFunctorData F),
  CategoryTheory.Monoidal.fromInducedCoreMonoidal F fData =
    { εIso := fData.εIso, μIso := fData.μIso, μIso_hom_natural_left := ⋯, μIso_hom_natural_right := ⋯,
      associativity := ⋯, left_unitality := ⋯, right_unitality := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.horn.IsCompatible.lift_comp_assoc : ∀ {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)}
  (hf : SSet.horn.IsCompatible f) {Y : SSet} (p : X ⟶ Y) [inst : HomotopicalAlgebra.Fibration p]
  (b : SSet.stdSimplex.obj { len := n + 1 } ⟶ Y)
  (comm :
    ∀ (j : Fin (n + 2)) (hj : j ≠ i),
      CategoryTheory.CategoryStruct.comp (f j hj) p = CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) b)
  {Z : SSet} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hf.lift p b comm) (CategoryTheory.CategoryStruct.comp p h) =
    CategoryTheory.CategoryStruct.comp b h
-- Mathlib.Analysis.Normed.Group.Basic
ne_zero_of_nnnorm_ne_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a : E}, ‖a‖₊ ≠ 0 → a ≠ 0
-- Mathlib.Algebra.Category.Ring.Basic
/-- The underlying type.  -/
RingCat.carrier : RingCat → Type u
-- Init.Classical
/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches.  -/
Classical.ite_not : ∀ {α : Sort u_1} (p : Prop) [inst : Decidable ¬p] (x y : α), (if ¬p then x else y) = if p then y else x
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.curry_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁) (t : ↑unitInterval) (x : X), (F.curry t) x = F (t, x)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.projKerOfRightInverse_comp_inv : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Ring R₁] [inst_1 : Ring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] {M₁ : Type u_4} {M₂ : Type u_5} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommGroup M₁] [inst_5 : Module R₁ M₁] [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommGroup M₂]
  [inst_8 : Module R₂ M₂] [inst_9 : IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁)
  (h : Function.RightInverse ⇑f₂ ⇑f₁) (y : M₂), (f₁.projKerOfRightInverse f₂ h) (f₂ y) = 0
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.lt_rpow_inv_iff : ∀ {x y : NNReal} {z : ℝ}, 0 < z → (x < y ^ z⁻¹ ↔ x ^ z < y)
-- Lean.Server.FileWorker.Utils
/-- Old representation for backward compatibility.  -/
Lean.Server.FileWorker.EditableDocumentCore.cmdSnaps : Lean.Server.FileWorker.EditableDocumentCore → Lean.AsyncList IO.Error Lean.Server.Snapshots.Snapshot
-- Mathlib.Algebra.Order.Group.Synonym
toDual_mul : ∀ {α : Type u_1} [inst : Mul α] (a b : α), OrderDual.toDual (a * b) = OrderDual.toDual a * OrderDual.toDual b
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.mk_simplex : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })) (hx : x ∈ X.nonDegenerate n), (SSet.N.mk x hx).simplex = x
-- Mathlib.Data.Finmap
/-- `NodupKeys s` means that `s` has no duplicate keys.  -/
Multiset.NodupKeys : {α : Type u} → {β : α → Type v} → Multiset (Sigma β) → Prop
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.basisFun_repr : ∀ (ι : Type u_1) (𝕜 : Type u_3) [inst : RCLike 𝕜] [inst_1 : Fintype ι] (x : EuclideanSpace 𝕜 ι) (i : ι),
  ((EuclideanSpace.basisFun ι 𝕜).repr x).ofLp i = x.ofLp i
-- Mathlib.FieldTheory.KummerExtension
X_pow_sub_C_irreducible_iff_of_odd : ∀ {K : Type u} [inst : Field K] {n : ℕ},
  Odd n → ∀ {a : K}, Irreducible (Polynomial.X ^ n - Polynomial.C a) ↔ ∀ (d : ℕ), d ∣ n → d ≠ 1 → ∀ (b : K), b ^ d ≠ a
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.State.mk.inj : ∀ {α : Type} {producers : Std.Queue (α × IO.Promise Bool)} {consumers : Std.Queue (Std.CloseableChannel.Consumer✝ α)}
  {closed : Bool} {producers_1 : Std.Queue (α × IO.Promise Bool)}
  {consumers_1 : Std.Queue (Std.CloseableChannel.Consumer✝ α)} {closed_1 : Bool},
  { producers := producers, consumers := consumers, closed := closed } =
      { producers := producers_1, consumers := consumers_1, closed := closed_1 } →
    producers = producers_1 ∧ consumers = consumers_1 ∧ closed = closed_1
-- Mathlib.Order.Hom.Basic
OrderHom.dual_apply_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (a : αᵒᵈ),
  (OrderHom.dual f) a = (⇑OrderDual.toDual ∘ ⇑f ∘ ⇑OrderDual.ofDual) a
-- Mathlib.Topology.Defs.Filter
/-- `Filter.cocompact` is the filter generated by complements to compact sets.  -/
Filter.cocompact : (X : Type u_1) → [TopologicalSpace X] → Filter X
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.coe_zsmul : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G]
  (x : ↥H) (n : ℤ), ↑(n • x) = n • ↑x
-- Init.Data.String.Slice
/-- Checks whether the slice \(`s`\) ends with the pattern \(`pat`\).

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".toSlice.endsWith "blue" = true`

* `"red green blue".toSlice.endsWith "green" = false`

* `"red green blue".toSlice.endsWith "" = true`

* `"red green blue".toSlice.endsWith 'e' = true`

* `"red green blue".toSlice.endsWith Char.isLower = true`
 -/
String.Slice.endsWith : {ρ : Type} → String.Slice → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → Bool
-- Mathlib.Analysis.Seminorm
Seminorm.coe_bot : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E], ⇑⊥ = 0
-- Mathlib.FieldTheory.Normal.Defs
AlgEquiv.restrictNormalHom.eq_1 : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} [inst_1 : Field K₁] [inst_2 : Algebra F K₁] (E : Type u_6)
  [inst_3 : Field E] [inst_4 : Algebra F E] [inst_5 : Algebra E K₁] [inst_6 : IsScalarTower F E K₁]
  [inst_7 : Normal F E], AlgEquiv.restrictNormalHom E = MonoidHom.mk' (fun χ => χ.restrictNormal E) ⋯
-- Lean.Elab.Command
Lean.Elab.Command.moduleLintersRef : IO.Ref (Array Lean.Elab.Command.ModuleLinter)
-- Mathlib.Algebra.CharP.Algebra
/-- If the algebra map `R →+* A` is injective then `A` has the same exponential characteristic
as `R`.  -/
expChar_of_injective_algebraMap : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Function.Injective ⇑(algebraMap R A) → ∀ (q : ℕ) [ExpChar R q], ExpChar A q
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalGroup.of_nhds_one : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G],
  Filter.Tendsto (Function.uncurry fun x1 x2 => x1 * x2) (nhds 1 ×ˢ nhds 1) (nhds 1) →
    Filter.Tendsto (fun x => x⁻¹) (nhds 1) (nhds 1) →
      (∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ * x) (nhds 1)) →
        (∀ (x₀ : G), Filter.Tendsto (fun x => x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) → IsTopologicalGroup G
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.map_edge : ∀ {X Y : SSet.Truncated 2}
  {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  (e : SSet.Truncated.Edge x₀ x₁) (f : X ⟶ Y),
  (e.map f).edge =
    (CategoryTheory.ConcreteCategory.hom
        (f.app (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 })))
      e.edge
-- Mathlib.CategoryTheory.Sums.Basic
_private.Mathlib.CategoryTheory.Sums.Basic.0.CategoryTheory.sum.match_3.eq_2 : ∀ (C : Type u_1) (D : Type u_2) (motive : C ⊕ D → Sort u_3) (X : D) (h_1 : (X : C) → motive (Sum.inl X))
  (h_2 : (X : D) → motive (Sum.inr X)),
  (match Sum.inr X with
    | Sum.inl X => h_1 X
    | Sum.inr X => h_2 X) =
    h_2 X
-- Mathlib.Algebra.Homology.LocalCohomology
/-- The natural isomorphism between local cohomology defined using the `of_self_le_radical`
diagram, assuming `J.radical = K.radical`.  -/
localCohomology.SelfLERadical.isoOfSameRadical : {R : Type u} →
  [inst : CommRing R] →
    {J K : Ideal R} →
      J.radical = K.radical → (i : ℕ) → localCohomology.ofSelfLERadical J i ≅ localCohomology.ofSelfLERadical K i
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.Decomposition.mk : {ι : Type u_1} →
  {M : Type u_3} →
    {σ : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : SetLike σ M] →
            [inst_3 : AddSubmonoidClass σ M] →
              {ℳ : ι → σ} →
                (decompose' : M → DirectSum ι fun i => ↥(ℳ i)) →
                  Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose' →
                    Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose' → DirectSum.Decomposition ℳ
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_zero_radius : ∀ (c : ℂ), circleMap c 0 = Function.const ℝ c
-- Mathlib.Algebra.Quandle
Quandle.Conj.quandle : (G : Type u_2) → [Group G] → Quandle (Quandle.Conj G)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contMDiff_comp_diffeomorph_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {G : Type u_7} [inst_9 : TopologicalSpace G]
  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9}
  [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H M] {M' : Type u_10} [inst_12 : TopologicalSpace M']
  [inst_13 : ChartedSpace H' M'] {N : Type u_11} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n m : WithTop ℕ∞} (h : Diffeomorph I J M N n) {f : N → M'}, m ≤ n → (ContMDiff I I' m (f ∘ ⇑h) ↔ ContMDiff J I' m f)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The canonical isomorphism `K.homology i ≅ K.opcycles i`
when the differential from `i` is zero.  -/
HomologicalComplex.isoHomologyι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            (i j : ι) → c.next i = j → K.d i j = 0 → [inst_2 : K.HasHomology i] → K.homology i ≅ K.opcycles i
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- a bijection between the types of objects  -/
CategoryTheory.CoreSmallCategoryOfSet.objEquiv : {Ω : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] → (self : CategoryTheory.CoreSmallCategoryOfSet Ω C) → ↑self.obj ≃ C
-- Init.Classical
Classical.forall_or_exists_not : ∀ {α : Sort u_1} (P : α → Prop), (∀ (a : α), P a) ∨ ∃ a, ¬P a
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.exists_ne_zero_of_integral_ne_zero : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  ∫ᵛ (a : X), f a ∂[B; μ] ≠ 0 → ∃ a, f a ≠ 0
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- A prefunctor preserving reversal of arrows  -/
Prefunctor.MapReverse : {U : Type u_1} →
  {V : Type u_2} →
    [inst : Quiver U] → [inst_1 : Quiver V] → [Quiver.HasReverse U] → [Quiver.HasReverse V] → U ⥤q V → Prop
-- Lean.MetavarContext
Lean.MetavarContext.findLevelIndex? : Lean.MetavarContext → Lean.LMVarId → Option ℕ
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- If `C` has finite coproducts, a functor `Discrete α ⥤ C` lifts to a functor
`Finset (Discrete α) ⥤ C` by taking coproducts.  -/
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type w} →
      [CategoryTheory.Limits.HasFiniteCoproducts C] →
        CategoryTheory.Functor (CategoryTheory.Discrete α) C →
          CategoryTheory.Functor (Finset (CategoryTheory.Discrete α)) C
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.map_algebraMap_ne_top_iff_disjoint : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (I : Ideal R), Ideal.map (algebraMap R S) I ≠ ⊤ ↔ Disjoint ↑M ↑I
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftHom.associatorHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y Z : C) →
        [inst_2 : Mathlib.Tactic.Coherence.LiftObj X] →
          [inst_3 : Mathlib.Tactic.Coherence.LiftObj Y] →
            [inst_4 : Mathlib.Tactic.Coherence.LiftObj Z] →
              Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.span_map_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.span f g).map CategoryTheory.Limits.WalkingSpan.Hom.snd = g
-- Mathlib.Algebra.Category.MonCat.Colimits
_private.Mathlib.Algebra.Category.MonCat.Colimits.0.MonCat.Colimits.descFunLift.match_1.eq_1 : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J] (F : CategoryTheory.Functor J MonCat)
  (motive : MonCat.Colimits.Prequotient F → Sort u_3) (j : J) (x : ↑(F.obj j))
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (MonCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive MonCat.Colimits.Prequotient.one)
  (h_3 : (x y : MonCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match MonCat.Colimits.Prequotient.of j x with
    | MonCat.Colimits.Prequotient.of j x => h_1 j x
    | MonCat.Colimits.Prequotient.one => h_2 ()
    | x.mul y => h_3 x y) =
    h_1 j x
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.isDigit_of_mem_toDigitsCore : ∀ {b : ℕ} {cs : List Char} {c : Char} {fuel n : ℕ},
  (c ∈ cs → c.isDigit = true) → 0 < b → b ≤ 10 → c ∈ b.toDigitsCore fuel n cs → c.isDigit = true
-- Mathlib.Data.PNat.Defs
Nat.canLiftPNat : CanLift ℕ ℕ+ PNat.val fun n => 0 < n
-- Mathlib.Topology.Separation.Regular
/-- A space is a `T5Space` iff all its open subspaces are `T4Space`.
 -/
t5Space_iff_forall_isOpen_t4Space : ∀ {X : Type u_1} [inst : TopologicalSpace X], T5Space X ↔ ∀ (s : Set X), IsOpen s → T4Space ↑s
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.nondegenerate_def : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Fintype m]
  [inst_2 : Fintype n],
  M.Nondegenerate ↔
    (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M.mulVec w = 0) → v = 0) ∧
      ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M.mulVec w = 0) → w = 0
-- Lean.Elab.MutualInductive
/-- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.checkParamsAndResultType : Lean.Expr → Lean.Expr → ℕ → Lean.Elab.TermElabM Unit
-- Mathlib.Topology.UniformSpace.Equicontinuity
Set.UniformEquicontinuous.uniformContinuous_of_mem : ∀ {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {H : Set (β → α)},
  H.UniformEquicontinuous → ∀ {f : β → α}, f ∈ H → UniformContinuous f
-- Mathlib.Topology.Bases
TopologicalSpace.IsSeparable.univ_pi : ∀ {ι : Type u_2} [Countable ι] {X : ι → Type u_3} {s : (i : ι) → Set (X i)} [inst : (i : ι) → TopologicalSpace (X i)],
  (∀ (i : ι), TopologicalSpace.IsSeparable (s i)) → TopologicalSpace.IsSeparable (Set.univ.pi s)
-- Mathlib.Data.List.Induction
/-- Bidirectional induction principle for lists: if a property holds for the empty list, the
singleton list, and `a :: (l ++ [b])` from `l`, then it holds for all lists. This can be used to
prove statements about palindromes. The principle is given for a `Sort`-valued predicate, i.e., it
can also be used to construct data.  -/
List.bidirectionalRec : {α : Type u_1} →
  {motive : List α → Sort u_2} →
    motive [] →
      ((a : α) → motive [a]) →
        ((a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) → (l : List α) → motive l
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_of_mono₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, CategoryTheory.Mono T.mor₂ → T.mor₁ = 0
-- Mathlib.Data.Bracket
/-- `⁅x, y⁆` is the result of a bracket operation on elements `x` and `y`.
It is supported by the `Bracket` typeclass.  -/
«term⁅_,_⁆» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.hasProduct_of_equiv_of_iso : ∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : α → C) (g : β → C)
  [CategoryTheory.Limits.HasProduct f] (e : β ≃ α) (iso : (j : β) → g j ≅ f (e j)), CategoryTheory.Limits.HasProduct g
-- Std.Net.Addr
Std.Net.InterfaceAddress.mk.injEq : ∀ (name : String) (physicalAddress : Std.Net.MACAddr) (isLoopback : Bool) (address netMask : Std.Net.IPAddr)
  (name_1 : String) (physicalAddress_1 : Std.Net.MACAddr) (isLoopback_1 : Bool) (address_1 netMask_1 : Std.Net.IPAddr),
  ({ name := name, physicalAddress := physicalAddress, isLoopback := isLoopback, address := address,
        netMask := netMask } =
      { name := name_1, physicalAddress := physicalAddress_1, isLoopback := isLoopback_1, address := address_1,
        netMask := netMask_1 }) =
    (name = name_1 ∧
      physicalAddress = physicalAddress_1 ∧ isLoopback = isLoopback_1 ∧ address = address_1 ∧ netMask = netMask_1)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Obj.mk.inj : ∀ {e? e?_1 : Option Lean.Expr}, { e? := e? } = { e? := e?_1 } → e? = e?_1
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.lift.eq_1 : ∀ {α : Type u_3} {M : Type u_4} [inst : Monoid M] (f : α → M) {rels : FreeMonoid α → FreeMonoid α → Prop}
  (h : ∀ (a b : FreeMonoid α), rels a b → (FreeMonoid.lift f) a = (FreeMonoid.lift f) b),
  PresentedMonoid.lift f h = (conGen rels).lift (FreeMonoid.lift f) ⋯
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.prop_product : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderFiniteProducts] {J : Type u_2} [Finite J] {f : J → C} [inst_3 : CategoryTheory.Limits.HasProduct f],
  (∀ (j : J), P (f j)) → P (∏ᶜ f)
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.Edge.map_whiskerLeft : ∀ {X Y Y' : SSet.Truncated 2}
  {x x' : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₁ : SSet.Truncated.Edge x x')
  {y y' : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e₂ : SSet.Truncated.Edge y y') (g : Y ⟶ Y'),
  (e₁.tensor e₂).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) = e₁.tensor (e₂.map g)
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.hasBasis : ∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G) (x : G),
  (B.N x).HasBasis (fun V => V ∈ B) fun V => (fun y => x + y) '' V
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.andIntro.injEq : ∀ (ak : Mathlib.Tactic.ITauto.AndKind) (p₁ p₂ : Mathlib.Tactic.ITauto.Proof) (ak_1 : Mathlib.Tactic.ITauto.AndKind)
  (p₁_1 p₂_1 : Mathlib.Tactic.ITauto.Proof),
  (Mathlib.Tactic.ITauto.Proof.andIntro ak p₁ p₂ = Mathlib.Tactic.ITauto.Proof.andIntro ak_1 p₁_1 p₂_1) =
    (ak = ak_1 ∧ p₁ = p₁_1 ∧ p₂ = p₂_1)
-- Init.Data.Array.Nat
Array.prod_eq_foldl_nat : ∀ {xs : Array ℕ}, xs.prod = Array.foldl (fun x1 x2 => x1 * x2) 1 xs
-- Mathlib.RingTheory.Smooth.Kaehler
retractionOfSectionOfKerSqZero.eq_1 : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S] (g : S →ₐ[R] P)
  (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S),
  retractionOfSectionOfKerSqZero g hf' hg =
    ↑P
      (LinearMap.liftBaseChange S
        (derivationOfSectionOfKerSqZero (IsScalarTower.toAlgHom R P S) hf' g hg).liftKaehlerDifferential)