mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- For a simplicial set `X`, if an edge in `X` is equal to the image of `hom`
under a morphism of simplicial sets, this edge has an inverse.  -/
SSet.coherentIso.invStructOfEqMapHom : {X : SSet} →
  {x₀ x₁ : X.obj (Opposite.op { len := 0 })} →
    {f : SSet.Edge x₀ x₁} →
      {g : SSet.coherentIso ⟶ X} →
        f.edge = (CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op { len := 1 }))) SSet.coherentIso.hom.edge →
          f.InvStruct
-- Init.MetaTypes
/-- Do reductions of proof terms. Default: `false`.  -/
Lean.Meta.Command.ReduceConfig.proofs : Lean.Meta.Command.ReduceConfig → Bool
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.singleContinuousLinearMap_apply : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedRing 𝕜] [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)]
  [inst_4 : DecidableEq α] [inst_5 : Fact (1 ≤ p)] (i : α) (x : E i),
  (lp.singleContinuousLinearMap 𝕜 E p i) x = lp.single p i x
-- Mathlib.Analysis.BoxIntegral.Partition.Split
/-- Since the definition of `BoxIntegral.Prepartition.compl` uses `Exists.choose`,
the result depends only on `π.iUnion`.  -/
BoxIntegral.Prepartition.compl_congr : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι] {π₁ π₂ : BoxIntegral.Prepartition I},
  π₁.iUnion = π₂.iUnion → π₁.compl = π₂.compl
-- Init.Data.List.MinMaxOn
List.le_apply_maxOn_of_mem : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} {y : α} (hx : y ∈ xs), f y ≤ f (List.maxOn f xs ⋯)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeSet α cmp),
  t = t_1 → t.min? = t_1.min?
-- Init.Data.Nat.Gcd
Nat.dvd_gcd_mul_iff_dvd_mul : ∀ {k n m : ℕ}, k ∣ k.gcd n * m ↔ k ∣ n * m
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.apply_natAbs_eq : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : PartialOrder S] [IsOrderedRing S] [inst_3 : Ring R]
  (abv : AbsoluteValue R S) [NoZeroDivisors S] (x : ℤ), abv ↑x.natAbs = abv ↑x
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.aeval_T : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : Algebra R R'] (x : R') (n : ℤ),
  (Polynomial.aeval x) (Polynomial.Chebyshev.T R n) = Polynomial.eval x (Polynomial.Chebyshev.T R' n)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- If `G` preserves the terminal object and `C` has a terminal object, then the image of the terminal
object is terminal.
 -/
CategoryTheory.Limits.isLimitOfHasTerminalOfPreservesLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          [inst_2 : CategoryTheory.Limits.HasTerminal C] →
            [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] →
              CategoryTheory.Limits.IsTerminal (G.obj (⊤_ C))
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.toAddSubmonoid : {M : Type u_1} → [inst : AddZeroClass M] → SaturatedAddSubmonoid M → AddSubmonoid M
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_range_eq_add_Ico : ∀ {M : Type u_3} [inst : AddCommMonoid M] (f : ℕ → M) {n : ℕ},
  0 < n → ∑ x ∈ Finset.range n, f x = f 0 + ∑ x ∈ Finset.Ico 1 n, f x
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.isScalarTower_of_liesOver : ∀ (R : Type u_2) [inst : CommSemiring R] {A : Type u_3} {B : Type u_4} [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [IsScalarTower R A B] (P : Ideal B) (p : Ideal A)
  [inst_7 : P.LiesOver p], IsScalarTower R (A ⧸ p) (B ⧸ P)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanIdentifier.fromJson : Lean.Json → Except String Lean.Lsp.LeanIdentifier
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_series_eq_zero_of_scalar_zero : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E], FormalMultilinearSeries.ofScalars E 0 = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_add_left : ∀ {α : Type u_2} [inst : AddGroup α] {t : Set α} {a : α}, (fun x => a + x) '' t = (fun x => -a + x) ⁻¹' t
-- Mathlib.Algebra.Homology.CochainComplexPlus
CochainComplex.Plus.instMonoIntHomFullSubcategoryPlusOfHasLimitsOfShapeWalkingCospan : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C] {X Y : CochainComplex.Plus C}
  (f : X ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.Mono f.hom
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.instAdditiveFullSubcategoryLift : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor D C) [F.Additive]
  (P : CategoryTheory.ObjectProperty C) (hF : ∀ (X : D), P (F.obj X)), (P.lift F hF).Additive
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.comp_assoc : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G] {H : Type u → Type s}
  [inst_2 : Applicative H] {I : Type u → Type t} [inst_3 : Applicative I] (η'' : ApplicativeTransformation H I)
  (η' : ApplicativeTransformation G H) (η : ApplicativeTransformation F G), (η''.comp η').comp η = η''.comp (η'.comp η)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.add_nonneg`.  -/
Left.add_nonneg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b : α}, 0 ≤ a → 0 ≤ b → 0 ≤ a + b
-- Mathlib.Algebra.Group.Basic
ite_vadd : ∀ {α : Type u_1} {β : Type u_2} [inst : VAdd β α] (p : Prop) [inst_1 : Decidable p] (a : α) (b c : β),
  (if p then b else c) +ᵥ a = if p then b +ᵥ a else c +ᵥ a
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.addEquivOfAddEquiv.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {Q : Type u_4} [inst_3 : AddCommMonoid Q]
  (k : T.LocalizationMap Q) {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T),
  f.addEquivOfAddEquiv k H = f.addEquivOfLocalizations (k.ofAddEquivOfDom H)
-- Mathlib.Order.Atoms.Finite
instIsStronglyAtomic : ∀ {α : Type u_1} [inst : Preorder α] [LocallyFiniteOrder α], IsStronglyAtomic α
-- Lean.Elab.InfoTree.Main
Lean.Elab.pushInfoTree : {m : Type → Type} → [Monad m] → [Lean.Elab.MonadInfoTree m] → Lean.Elab.InfoTree → m Unit
-- Init.Prelude
eq_false_of_ne_true : ∀ {b : Bool}, ¬b = true → b = false
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.Algebra.Group.InjSurj
/-- A type has right-cancellative multiplication, if it admits an injective map that
preserves `*` to another type with right-cancellative multiplication.  -/
Function.Injective.isRightCancelMul : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : Mul M₂] [IsRightCancelMul M₂] (f : M₁ → M₂),
  Function.Injective f → (∀ (x y : M₁), f (x * y) = f x * f y) → IsRightCancelMul M₁
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.toRingEquiv_symm_uniqueAlgEquiv : ∀ (R : Type u_1) {A : Type u_4} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] [inst_4 : Unique M],
  ↑(MonoidAlgebra.uniqueAlgEquiv R M).symm = (MonoidAlgebra.uniqueRingEquiv M).symm
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.Eqv.of_zero_right : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m : M),
  TensorProduct.Eqv R M N (FreeAddMonoid.of (m, 0)) 0
-- Mathlib.Order.Category.BddLat
BddLat.ext : ∀ {X Y : BddLat} {f g : X ⟶ Y},
  (∀ (x : ↑X.toLat), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.standardσ.congr_simp : ∀ (L L_1 : List ℕ) (e_L : L = L_1) {m₁ m₂ : ℕ} (h : m₂ + L.length = m₁),
  SimplexCategoryGenRel.standardσ L h = SimplexCategoryGenRel.standardσ L_1 ⋯
-- Mathlib.Tactic.WLOG
/-- `wlog h : P` adds an assumption `h : P` to the main goal, and adds a side goal that
requires showing that the case `h : ¬ P` can be reduced to the case where `P` holds
(typically by symmetry). The side goal will be at the top of the stack. In this side goal,
there will be two additional assumptions:
- `h : ¬ P`: the assumption that `P` does not hold
- `this`: which is the statement that in the old context `P` suffices to prove the goal.
  By default, the entire context is reverted to produce `this`.

* `wlog h : P with H` gives the name `H` to the statement that `P` proves the goal.
* `wlog h : P generalizing x y ...` reverts certain parts of the context before creating the new
  goal. In this way, the wlog-claim `this` can be applied to `x` and `y` in different orders
  (exploiting symmetry, which is the typical use case).
* `wlog! h : P` also calls `push Not` at the generated hypothesis `h`.
  `wlog! h : P ∧ Q` will transform `¬ (P ∧ Q)` to `P → ¬ Q`
* `wlog! +distrib h : P` also calls `push +distrib Not` at the generated hypothesis `h`.
  `wlog! +distrib h : P ∧ Q` will transform `¬ (P ∧ Q)` to `¬P ∨ ¬Q`.
 -/
Mathlib.Tactic.wlog : Lean.ParserDescr
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
/-- Given a family of opens `U` and an open `Y` equal to the union of opens in `U`, we may
take the presieve on `Y` associated to `U` and the sieve generated by it, and form the
full subcategory (subposet) of opens contained in `Y` (`over Y`) consisting of arrows
in the sieve. This full subcategory is equivalent to `OpensLeCover U`, the (poset)
category of opens contained in some `U i`.  -/
TopCat.Presheaf.generateEquivalenceOpensLe : {X : TopCat} →
  {ι : Type u_2} →
    (U : ι → TopologicalSpace.Opens ↑X) →
      {Y : TopologicalSpace.Opens ↑X} →
        Y = iSup U →
          ((CategoryTheory.ObjectProperty.FullSubcategory fun f =>
              (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows f.hom) ≌
            TopCat.Presheaf.SheafCondition.OpensLeCover U)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.contDiffOn_arccos : ∀ {n : WithTop ℕ∞}, ContDiffOn ℝ n Real.arccos {-1, 1}ᶜ
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.postCongr_hom_app_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {F G : CategoryTheory.Functor T D} (e : F ≅ G) (X_1 : CategoryTheory.Over X),
  ((CategoryTheory.Over.postCongr e).hom.app X_1).left = e.hom.app X_1.left
-- Mathlib.GroupTheory.Index
Subgroup.inf_eq_bot_of_coprime : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, (Nat.card ↥H).Coprime (Nat.card ↥K) → H ⊓ K = ⊥
-- Mathlib.Order.WithBot
Equiv.withBotCongr_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e₁ : α ≃ β) (e₂ : β ≃ γ),
  (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.awayToSection_comp_appLE : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) {i : ℕ} {s : A},
  s ∈ 𝒜 i →
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayToSection 𝒜 s)
        (AlgebraicGeometry.Scheme.Hom.appLE (AlgebraicGeometry.Proj.map f hf) (AlgebraicGeometry.Proj.basicOpen 𝒜 s)
          (AlgebraicGeometry.Proj.basicOpen ℬ (f s)) ⋯) =
      CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (HomogeneousLocalization.Away.map f s))
        (AlgebraicGeometry.Proj.awayToSection ℬ (f s))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblY_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R) (u : R),
  W'.dblY (u • P) = u ^ 4 * W'.dblY P
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_zero : ∀ {R : Type u} (M : Type v) [inst : Zero R] [inst_1 : Zero M], TrivSqZeroExt.inl 0 = 0
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHomClass.toMonoidHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : FunLike F M N]
  [inst_3 : MonoidHomClass F M N] (f : F), ↑f = { toFun := (↑f).toFun, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaRepresentableBy_homEquiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] (X : C)
  {X_1 : C}, (CategoryTheory.shrinkYonedaRepresentableBy X).homEquiv = CategoryTheory.shrinkYonedaObjObjEquiv.symm
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- Given all wide pullbacks in `C`, construct products in `C/B`.  -/
CategoryTheory.Over.ConstructProducts.over_products_of_widePullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWidePullbacks C] {B : C},
  CategoryTheory.Limits.HasProducts (CategoryTheory.Over B)
-- Mathlib.LinearAlgebra.Finsupp.LSum
LinearMap.CompatibleSMul.finsupp_cod : ∀ (R : Type u_9) (S : Type u_10) (M : Type u_11) (N : Type u_12) (ι : Type u_13) [inst : Semiring S]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module S M] [inst_4 : Module S N] [inst_5 : SMul R M]
  [inst_6 : SMulZeroClass R N] [LinearMap.CompatibleSMul M N R S], LinearMap.CompatibleSMul M (ι →₀ N) R S
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_comp_tensorHom_η : ∀ {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.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] {X : C} {Y : D} (f : F.obj X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.Functor.OplaxMonoidal.η F)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)))
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_apply_finset : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) [MeasurableSingletonClass α] (s : Finset α),
  p.toMeasure ↑s = ∑ x ∈ s, p x
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.foldM_eq_foldlM_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α} {δ : Type v} {m' : Type v → Type w}
  [inst_2 : Monad m'] [LawfulMonad m'],
  m.WF → ∀ {f : δ → α → m' δ} {init : δ}, Std.HashSet.Raw.foldM f init m = List.foldlM f init m.toList
-- Mathlib.Order.Interval.Set.Basic
IsMin.Iic_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, IsMin a → Set.Iic a = {a}
-- Mathlib.Topology.Homeomorph.Lemmas
Topology.IsEmbedding.toHomeomorph_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : Topology.IsEmbedding f) (x : X), hf.toHomeomorph.symm ⟨f x, ⋯⟩ = x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.ofList_singleton : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {k : α} {v : β},
  Std.HashMap.Raw.ofList [(k, v)] = ∅.insert k v
-- Mathlib.Algebra.Group.Defs
SubNegMonoid.zsmul_succ' : ∀ {G : Type u} [self : SubNegMonoid G] (n : ℕ) (a : G), ↑n.succ • a = ↑n • a + a
-- Mathlib.CategoryTheory.EffectiveEpi.Comp
CategoryTheory.effectiveEpiFamilyStructCompIso_aux : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B B' : C} {α : Type u_2} (X : α → C)
  (π : (a : α) → X a ⟶ B) (i : B ⟶ B') {W : C} (e : (a : α) → X a ⟶ W),
  (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.comp (π a₁) i) =
          CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.CategoryStruct.comp (π a₂) i) →
        CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) →
    ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
        CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.instT0SpaceSetOfT1Space : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T1Space α], T0Space (Set α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insert_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {kmi : α},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKey?.get ⋯ = kmi → (compare kmi k).isLE = true
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : SizeOf C] (X : C) (p : X ⟶ X)
  (idem : autoParam (CategoryTheory.CategoryStruct.comp p p = p) CategoryTheory.Idempotents.Karoubi.idem._autoParam),
  sizeOf { X := X, p := p, idem := idem } = 1 + sizeOf X + sizeOf p + sizeOf idem
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- the condition that the given endomorphism is an idempotent  -/
CategoryTheory.Idempotents.Karoubi.idem_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (self : CategoryTheory.Idempotents.Karoubi C) {Z : C}
  (h : self.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.p (CategoryTheory.CategoryStruct.comp self.p h) =
    CategoryTheory.CategoryStruct.comp self.p h
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_left : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.OplaxLeftLinear C] {c c' : C}
  (f : c ⟶ c') (d : D),
  CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d))
      (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c' d) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f (F.obj d))
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.reflexivePair.match_3.eq_2 : ∀ (motive : (X Y : CategoryTheory.Limits.WalkingReflexivePair) → (X ⟶ Y) → Sort u_1)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingReflexivePair) → motive x x (CategoryTheory.Limits.WalkingReflexivePair.Hom.id x))
  (h_2 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
        CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
  (h_3 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.zero
        CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
  (h_4 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.zero CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
  (h_5 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion)
  (h_6 :
    Unit →
      motive CategoryTheory.Limits.WalkingReflexivePair.one CategoryTheory.Limits.WalkingReflexivePair.one
        CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion),
  (match CategoryTheory.Limits.WalkingReflexivePair.one, CategoryTheory.Limits.WalkingReflexivePair.zero,
      CategoryTheory.Limits.WalkingReflexivePair.Hom.left with
    | x, .(x), CategoryTheory.Limits.WalkingReflexivePair.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.zero),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.left => h_2 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.zero),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.right => h_3 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.zero), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion => h_4 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.rightCompReflexion => h_5 ()
    | .(CategoryTheory.Limits.WalkingReflexivePair.one), .(CategoryTheory.Limits.WalkingReflexivePair.one),
      CategoryTheory.Limits.WalkingReflexivePair.Hom.leftCompReflexion => h_6 ()) =
    h_2 ()
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `extractLsb'` on `BitVec`s.  -/
BitVec.reduceExtractLsb' : Lean.Meta.Simp.DSimproc
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- The convex body defined by `f`: the set of points `x : E` such that `‖x w‖ < f w` for all
infinite places `w`.  -/
NumberField.mixedEmbedding.convexBodyLT : (K : Type u_1) →
  [inst : Field K] → (NumberField.InfinitePlace K → NNReal) → Set (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.Algebra.Group.Defs
AddCommMagma.ext : ∀ {G : Type u} {x y : AddCommMagma G}, Add.add = Add.add → x = y
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.IsIsolated.eq_1 : ∀ {V : Type u} (G : SimpleGraph V) (v : V), G.IsIsolated v = ∀ (w : V), ¬G.Adj v w
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `none` if no such pair exists.
 -/
Std.DTreeMap.Raw.Const.getEntryLT? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α → Option (α × β)
-- Init.Omega.Constraint
Lean.Omega.instDecidableEqConstraint.decEq : (x x_1 : Lean.Omega.Constraint) → Decidable (x = x_1)
-- Mathlib.Order.BooleanGenerators
/-- **Alias** of `IsCompactlyGenerated.BooleanGenerators.booleanAlgebraOfSSupEqTop`.

---

A compactly generated complete lattice generated by Boolean generators is a Boolean algebra.  -/
IsCompactlyGenerated.BooleanGenerators.booleanAlgebra_of_sSup_eq_top : {α : Type u_1} →
  [inst : CompleteLattice α] →
    {S : Set α} → [IsCompactlyGenerated α] → IsCompactlyGenerated.BooleanGenerators S → sSup S = ⊤ → BooleanAlgebra α
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.Path.mk₂.congr_simp : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (p p_1 : X.Path 1) (e_p : p = p_1) (q q_1 : X.Path 1) (e_q : q = q_1)
  (h : p.vertex 1 = q.vertex 0), p.mk₂ q h = p_1.mk₂ q_1 ⋯